Library FreeSpec.Core.Init

• Utils Functions
• Tactics
• Notations
• Generalizable Functions Equality
• Hint Databases

Library FreeSpec.Core.Interface

• Definition
• Polymorphic Interface Composites
• Composing Interfaces

Library FreeSpec.Core.Impure

• Definition
• Monad Instances
• Defining Impure Computations
• Lift

Library FreeSpec.Core.Semantics

• Definition
• Interpreting Impure Computations
• In-place Primitives Handling

Library FreeSpec.Core.Component

• Definition
• Semantics Derivation
• In-place Primitives Handling

Library FreeSpec.Core.Contract

• Definition
• Composing Contracts

Library FreeSpec.Core.ImpureFacts

• Equivalence
  • Definition
  • Proper Instances
• Equations

Library FreeSpec.Core.SemanticsFacts

• Semantics Compliance
• Equivalences
  • Semantics
  • Interpretation Results
  • Proper Instances
• General Lemmas

Library FreeSpec.Core.Hoare

• Definition
• Instances
  • Functor
  • Applicative
  • Monad
• Reasoning about Programs

Library FreeSpec.Core.HoareFacts

• Equivalence Relation
• Proper Instances
• General Lemmas

Library FreeSpec.Core.Instrument

Library FreeSpec.Core.InstrumentFacts

Library FreeSpec.Core.ComponentFacts

• • Component Correctness

Library FreeSpec.Core.Tactics

Library FreeSpec.Core.Core

Library FreeSpec.Core.CoreFacts

Library FreeSpec.Core.Extraction

• How to
• Extraction Configuration

Library FreeSpec.FFI.Refs

• Types
• Impure Primitives
  • Monad
  • IO Instance
  • Interface Definition

Library FreeSpec.FFI.FFI

Library FreeSpec.FFI.ML

Library FreeSpec.Exec.Eval

Library FreeSpec.Exec.Exec

• Extending FreeSpec.Exec

Library airlock

• Specifying
  • Doors
  • Controller
• Verifying the Airlock Controller
  • Doors Specification
    • Witness States
    • Requirements
    • Promises
  • Intermediary Lemmas
  • Main Theorem

Library smram

• The Verification Problem
• Specifying the Subsystem
  • Addressing Memories
  • VGA and DRAM Controllers
  • Memory Controller
• Verifying our Subsystem
  • Memory View
  • Specification
    • DRAM Controller Specification
    • Memory Controller Specification
  • Main Theorem

Library heap