Library compcert.lib.Coqlib

• Useful tactics
• Definitions and theorems over the type positive
• Definitions and theorems over the type Z
• Definitions and theorems on the data types option, sum and list
• Definitions and theorems over boolean types
• Well-founded orderings
• Nonempty lists

Library compcert.lib.Maps

• The abstract signatures of trees
• The abstract signatures of maps
• An implementation of trees over type positive
• An implementation of maps over type positive
• An implementation of maps over any type that injects into type positive
• An implementation of maps over any type with decidable equality
• A partial implementation of trees over any type that injects into type positive
• Additional properties over trees
• Useful notations

Library compcert.common.Errors

• Representation of error messages.
• The error monad
• Reasoning over monadic computations

Library compcert.flocq.Core.Fcore_Zaux

Library compcert.flocq.Core.Fcore_Raux

• Missing definitions/lemmas

Library compcert.flocq.Core.Fcore_defs

• Basic definitions: float and rounding property

Library compcert.flocq.Core.Fcore_float_prop

• Basic properties of floating-point formats: lemmas about mantissa, exponent...

Library compcert.flocq.Core.Fcore_rnd

• Roundings: properties and/or functions

Library compcert.flocq.Core.Fcore_generic_fmt

• What is a real number belonging to a format, and many properties.

Library compcert.flocq.Core.Fcore_ulp

• Unit in the Last Place: our definition using fexp and its properties, successor and predecessor

Library compcert.flocq.Core.Fcore_rnd_ne

• Rounding to nearest, ties to even: existence, unicity...

Library compcert.flocq.Core.Fcore_FIX

• Fixed-point format

Library compcert.flocq.Core.Fcore_FLX

• Floating-point format without underflow

Library compcert.flocq.Core.Fcore_FLT

• Floating-point format with gradual underflow

Library compcert.flocq.Core.Fcore

Library compcert.flocq.Core.Fcore_digits

Library compcert.flocq.Calc.Fcalc_digits

• Functions for computing the number of digits of integers and related theorems.

Library compcert.flocq.Calc.Fcalc_bracket

• Locations: where a real number is positioned with respect to its rounded-down value in an arbitrary format.

Library compcert.flocq.Calc.Fcalc_round

• Helper function for computing the rounded value of a real number.
• Instances of the theorems above, for the usual rounding modes.

Library compcert.flocq.Calc.Fcalc_ops

Library compcert.flocq.Calc.Fcalc_div

• Helper function and theorem for computing the rounded quotient of two floating-point numbers.

Library compcert.flocq.Calc.Fcalc_sqrt

• Helper functions and theorems for computing the rounded square root of a floating-point number.

Library compcert.flocq.Prop.Fprop_relative

• Relative error of the roundings

Library compcert.flocq.Appli.Fappli_IEEE

• IEEE-754 arithmetic

Library compcert.flocq.Appli.Fappli_IEEE_bits

• IEEE-754 encoding of binary floating-point data

Library compcert.x86_64.Archi

Library compcert.lib.Integers

• Comparisons
• Parameterization by the word size, in bits.
• Representation of machine integers
• Arithmetic and logical operations over machine integers
• Properties of integers and integer arithmetic
  • Properties of modulus, max_unsigned, etc.
  • Modulo arithmetic
  • Properties of the coercions between Z and int
  • Properties of zero, one, minus one
  • Properties of equality
  • Properties of addition
  • Properties of negation
  • Properties of subtraction
  • Properties of multiplication
  • Properties of division and modulus
  • Bit-level properties
  • Properties of bit-level operations over Z
  • Bit-level reasoning over type int
  • Properties of bitwise and, or, xor
  • Properties of shifts
  • Properties of rotations
  • Properties of Z_one_bits and is_power2.
  • Relation between bitwise operations and multiplications / divisions by powers of 2
  • Properties of shrx (signed division by a power of 2)
  • Properties of integer zero extension and sign extension.
  • Properties of one_bits (decomposition in sum of powers of two)
  • Properties of comparisons
• Specialization to integers of size 8, 32, and 64 bits
• Specialization to offsets in pointer values

Library compcert.flocq.Prop.Fprop_Sterbenz

• Sterbenz conditions for exact subtraction

Library compcert.flocq.Appli.Fappli_rnd_odd

• Rounding to odd and its properties, including the equivalence

Library compcert.lib.Fappli_IEEE_extra

• • Decidable equality
  • Conversion from an integer to a FP number
  • Conversion from a FP number to an integer
  • Algebraic identities
  • Conversion from scientific notation
  • Conversions between two FP formats

Library compcert.lib.Floats

• Double-precision FP numbers
  • NaN payload manipulations
  • Operations over double-precision floats
  • Properties
• Single-precision FP numbers
  • NaN payload manipulations
  • Operations over single-precision floats
  • Properties

Library compcert.common.AST

• Syntactic elements
• Generic transformations over programs
• External functions
• Register pairs
• Arguments and results to builtin functions

Library compcert.common.Values

• Operations over values
• Values and memory injections

Library compcert.lib.Axioms

• Extensionality axioms
• Proof irrelevance

Library compcert.common.Linking

• Syntactic linking
• Matching between two programs
• Commutation between linking and program transformations
• Linking a set of compilation units
• Linking and composition of compilation passes

Library compcert.lib.Intv

• Membership
• Emptyness
• Disjointness
• Shifting an interval by some amount
• Enumerating the elements of an interval
• Checking properties on all elements of an interval
• Folding a function over all elements of an interval

Library compcert.common.Memdata

• Properties of memory chunks
• Memory values
• Encoding and decoding integers
• Encoding and decoding values
• Compatibility with memory injections
• Breaking 64-bit memory accesses into two 32-bit accesses

Library compcert.common.Memtype

• Operations on memory states
• Permissions, block validity, access validity, and bounds
• Relating two memory states.
  • Memory extensions
  • Memory injections
  • Invariance properties between two memory states
• Properties of the memory operations
  • Properties of the initial memory state.
  • Properties of load.
  • Properties of loadbytes.
  • Properties of store.
  • Properties of storebytes.
  • Properties of alloc.
  • Properties of free.
  • Properties of drop_perm.
  • Properties of extends.
  • Properties of magree.
  • Properties of inject.
  • Properties of inject_neutral
  • Properties of unchanged_on and strong_unchanged_on

Library compcert.common.Memory

Library compcert.common.Globalenvs

• Symbol environments
• Global environments
  • Lookup functions
  • Constructing the global environment
  • Properties of the operations over global environments
  • Coercing a global environment into a symbol environment
• Construction of the initial memory state
  • Compatibility with memory injections
  • Sufficient and necessary conditions for the initial memory to exist.
• Commutation with program transformations

Library compcert.common.Events

• Events and traces
• Relating values and event values
• Matching traces.
• Semantics of volatile memory accesses
• Semantics of external functions
  • Semantics of volatile loads
  • Semantics of volatile stores
  • Semantics of dynamic memory allocation (malloc)
  • Semantics of dynamic memory deallocation (free)
  • Semantics of memcpy operations.
  • Semantics of annotations.
  • Semantics of external functions.
  • Combined semantics of external calls
• Evaluation of builtin arguments

Library compcert.common.Smallstep

• Closures of transitions relations
• Transition semantics
• Forward simulations between two transition semantics.
  • Forward simulation diagrams.
  • Forward simulation of transition sequences
  • Composing two forward simulations
• Receptiveness and determinacy
• Backward simulations between two transition semantics.
  • Backward simulation diagrams.
  • Backward simulation of transition sequences
  • Composing two backward simulations
  • Converting a forward simulation to a backward simulation
• Transforming a semantics into a single-event, equivalent semantics
• Connections with big-step semantics

Library compcert.cfrontend.Ctypes

• Syntax of types
• Operations over types
  • Conversions
  • Complete types
  • Alignment of a type
  • Size of a type
  • Size and alignment for composite definitions
  • Byte offset for a field of a structure
  • Access modes
  • Alignment for block copy operations
  • C types and back-end types
• Construction of the composite environment
• Programs and compilation units
• Separate compilation and linking
  • Linking types
  • Linking composite definitions
  • Linking function definitions
  • Linking programs
  • Commutation between linking and program transformations

Library compcert.cfrontend.Cop

• Syntax of operators.
• Type classification and semantics of operators.
  • Casts and truth values
  • Unary operators
    • Boolean negation
    • Opposite and absolute value
    • Bitwise complement
  • Binary operators
    • Addition
    • Subtraction
    • Multiplication, division, modulus
    • Shifts
    • Comparisons
  • Function applications
  • Argument of a switch statement
• Combined semantics of unary and binary operators
• Compatibility with extensions and injections
• Some properties of operator semantics

Library compcert.cfrontend.Clight

• Abstract syntax
  • Expressions
  • Statements
  • Functions
  • Programs
• Operational semantics
  • Evaluation of expressions
  • Transition semantics for statements and functions
  • Whole-program semantics

Library liblayers.lib.Decision

• MathClasses-style "Decision" class.
• Instances
• Decision procedures for lists
• Decision procedures from compare

Library coqrel.Delay

• The delayed/delay tactics
• Hints
• Example: reifying eapply

Library coqrel.RelDefinitions

• Prerequisites
• Relations
  • Proof step
  • Proof automation
  • Introduction rules
  • Using relations
  • Destructing relational hypotheses
  • Monotonicity properties
  • Order on relations
• Core relators
  • • Non-dependent function types
    • Dependent products
  • Inverse relation

Library coqrel.RelClasses

• More classes for relation properties
  • Coreflexive relations

Library coqrel.Relators

• Relators
  • A note about universes
  • Relators for function types
    • Pointwise extension of a relation
    • Dependent pointwise extension
    • Dependent products (restricted version)
    • Sets (A → Prop)
  • Inductive types
    • Nullary type constructors
    • Sum types
    • Pairs
    • Option types
    • Lists
  • Monotonicity of logical connectives

Library coqrel.RelOperators

• • Union of relations
  • Intersection of relations
  • Implication
  • The bottom and top relations
  • Relation equivalence
  • Relation composition
  • Pulling a relation along functions
  • Pushing a relation along functions
  • Relation currying
  • The req relation
  • Checking predicates on the left and right elements
  • Relation versions of ex and all
  • The rel_incr construction

Library coqrel.Monotonicity

• • The monotonicity tactic
    • Truncating applications
    • Selecting a relational property
    • Using subrel
    • Main tactic
    • subrel constraint as a subgoal
  • Generic instances

Library coqrel.RDestruct

• The RDestruct class
  • Introducing the hypothesis to be destructed
  • RDestruct steps
  • Choosing to discard or keep equations
  • Default instance

Library coqrel.MorphismsInterop

• Interoperation with Coq.Classes.Morphisms
  • Using Morphisms-style relational properties
    • Relators
    • Morphisms.Proper instances
    • subrelation instances
  • Satisfying Morphisms.Proper queries

Library coqrel.Transport

• • The transport tactic
    • Transportable hypotheses

Library coqrel.PreOrderTactic

Library coqrel.LogicalRelations

Library liblayers.logic.Structures

• Generic operations
• Generic properties
  • Heterogenous transitivity
  • Hints for eauto and autorewrite
  • Some properties of properties
• Logical relationish kind of things
  • Generic instances for relation properties
• Basic instances
  • Prop
  • Booleans
  • The Equivalence derived from a PreOrder
  • Trivial order

Library liblayers.logic.LayerData

• Categories of abstract data and simulation relations
• Associated concrete simulation relations

Library liblayers.logic.PseudoJoin

• Pseudo-joins and some properties
• Data-indexed version
  • Deriving the PseudoJoins on (T D)
  • A more complete join
• Normalization procedure
• Booleans have a pseudo-join structure
• Product of pseudo-join structures
• Adjoining an extra element

Library liblayers.logic.PseudoJoinReflection

• Syntax
• Semantics
• Verification conditions

Library liblayers.lib.ExtensionalityAxioms

Library liblayers.lib.Functor

• Interface of functors
• Simple instances
  • Constant
  • Identity
  • Product
  • Option
• Some helper instances

Library liblayers.lib.Monad

• Interface of monads
• Normalization
• Monad inversion
• Properties
• Some instances

Library liblayers.lib.OptionMonad

• The option monad
  • option is a fully invertible monad
  • Some option-specific rewrite rule
  • Some option-specific definition
• option-related decision procedures

Library liblayers.logic.OptionOrders

• Discussion
• Simple order
  • Option predicates
  • Monad operations

Library liblayers.compcertx.ErrorMonad

• res is a monad
• Lifting orders on res
  • Data-indexed version
• Orders for res ∘ option
• Decision-related definitions
  • The res version of assert.
  • Whether a res A is OK or Error
    • Some lemmas and eauto hints.
• Miscellaneous helpers
  • Flip option (res -) <-> res (option -)
• PseudoJoin structure for res (option -)

Library liblayers.logic.GlobalVars

Library liblayers.logic.Modules

• Modules
• Properties of modules
• Well-formed modules
  • ModuleOK is decidable
  • Monotonicity
  • Basic instances
  • Other lemmas

Library liblayers.logic.Primitives

Library liblayers.logic.Layers

• Layers
• Asserting a property for all primitives
• Well-formed layers
  • Monotonicity
  • Basic instances
• Other properties

Library liblayers.logic.Semantics

• Semantics of modules
• Semantics of individual function definitions
• Specification
• Properties
  • Propeties of semof_fundef
  • Properties of semof
  • Disjointness of modules and layers

Library liblayers.logic.PTrees

• Generic operations on PTrees
• Decidable properties of PTrees
  • Some property holds for all bindings
  • Two PTrees have disjoint domains
• Applying a partial function to all data of a tree.
  • Monotonicity wrt. ptree_rel

Library liblayers.logic.PTreeModules

• Construction of modules
  • Querying functions
  • Instance of Modules
• Enumeration of module functions and variables.

Library liblayers.logic.PTreeLayers

• Construction of layers
  • Querying functions
• Additional properties

Library liblayers.logic.PTreeSemantics

• Preliminaries
• Semantics of ptree_modules

Library liblayers.compcertx.GenSem

• Generic semantics from abstract functions
  • Basic instances

Library compcertx.common.MemoryX

Library liblayers.lib.Lens

• Interface
• Theory
  • Getters are measures, cf. Coq.Classes.RelationPairs
  • The modify operation
  • The same_context relation
  • Consequences of LensGetSet
  • Consequences of LensSetGet
  • Orthogonal lenses
• Tactics
• Instances
  • Pairs
  • Composing lens
  • Initial and terminal objects

Library liblayers.lib.PowersetMonad

• - → Prop is a Functor
• - → Prop is also a monad

Library liblayers.lib.Lift

• Lifting operations
  • The lift_peel tactic
  • Expressing everything in terms of lift
  • Simplifying occurences of lift
  • Solving the residual goals
  • Properties of lifted operations

Library compcert.lib.Ordered

Library compcert.lib.Decidableplus

Library compcert.lib.BoolEqual

Library compcert.x86.Op

• Evaluation functions
• Static typing of conditions, operators and addressing modes.
• Manipulating and transforming operations
• Invariance and compatibility properties.

Library compcert.x86.Machregs

• • Machine registers
  • Names of registers
  • Destroyed registers, preferred registers

Library compcert.backend.Locations

• Representation of locations
  • Processor registers
  • Slots in activation records
  • Locations
• Mappings from locations to values
• Total ordering over locations

Library compcert.common.Separation

• Assertions about memory
• Separating conjunction
• Basic memory assertions.

Library compcert.x86.Conventions1

• Classification of machine registers
• Function calling conventions
  • Location of function result
  • Location of function arguments

Library compcert.backend.Conventions

• • Location of function parameters
• Tail calls

Library compcert.backend.LTL

• Abstract syntax
• Operational semantics
• Operations over LTL

Library compcert.backend.Linear

• Abstract syntax
• Operational semantics

Library compcert.backend.Bounds

• Resource bounds for a function
• Inference of resource bounds for a function

Library compcert.x86.Stacklayout

Library compcert.backend.EraseArgs

Library compcert.x86.Asm

• Abstract syntax
  • Registers.
  • Instruction set.
• Operational semantics

Library liblayers.compcertx.CompcertStructures

• Prerequisites
• Relations on programs and global environments
  • The glob_threshold constant
  • Programs
  • Global environments
  • Monotonicity of Genv.globalenv
  • Additional definitions
• Clight signatures
  • Decision procedures
  • Helper functions
• Injection-related properties
  • Lemmas about extcall_arguments
• Names of external functions
• Lists

Library liblayers.compcertx.LiftMem

• Prerequisites
  • Properties of the inject_incr relation
• Lifting the properties

Library liblayers.compcertx.LiftMemX

• Prerequisites

Library liblayers.simrel.AbstractData

• Types of abstract data

Library liblayers.compcertx.InitMem

• Miscellaneous properties of Genv.init_mem

Library liblayers.simrel.MemWithData

• Memory with abstract data
  • Base memory model
  • Memory with data

Library coqrel.BoolRel

• Relations for sumbool
  • Symmetric relation
  • Directed relation
• Definitions for leb
  • Properties
  • Monotonicity of various definitions

Library liblayers.simrel.SimrelDefinition

• Preliminaries
• Simulation relations blueprints
  • Components
  • Relations derived from simrel_meminj
  • simrel_option_le
  • Initial memory
  • Properties
  • Packaging them up
  • Properties of derived relations
    • Compatibility with the accessibility relation
    • Functionality
    • Shift-invariance
    • Relationships between match_foo relations
    • Global blocks
    • Miscellaneous
  • Properties of derived memory operations
  • Strengthened properties for memory operations
• Tactics

Library liblayers.simrel.SimrelEquivalence

• Equivalences
  • Definition
  • Rewriting tactic
  • Basic equivalences
    • Identity
    • Composition
    • Inverse
  • The simrel_equiv relation

Library liblayers.simrel.MemoryRel

• Relational version of memory model properties
  • Properties of the relations involved
  • Mem.extends properties

Library liblayers.compcertx.MakeProgramSpec

• Prerequisites
• Relations
• Specification of make_program

Library liblayers.compcertx.InitMemRel

• Monotonicity of Genv.alloc_global
  • Helper definitions
  • Requirements
• Relational property for Genv.init_mem

Library liblayers.simrel.SimrelInitMem

Library liblayers.simrel.MemOpv

• Memory operation helpers
• Monotonicity properties

Library liblayers.simrel.SimrelCategory

• Categorical structure
  • Identity
  • Composition
  • Categorical properties
  • simrel is a Category

Library liblayers.simrel.SimrelFunctor

• Simrel functors
  • Relations without worlds
    • Definition
    • Properties
  • Relations indexed by simrel_worlds
    • Definition
    • Properties

Library liblayers.simrel.SimulationRelation

Library liblayers.simrel.SimrelInvariant

• • Invariants
    • Definition
    • Properties
    • Initial states

Library liblayers.compcertx.SimValues

• Prerequisites
  • Typeclass version of Archi.ptr64
  • Typed match_val
    • Definition
    • Properties
  • Miscellaneous
• Properties of match_val_of_type_× wrt. equivalence
• Operations over values
  • Preparations
  • Constants
  • Arithmetic operations
  • Operations on 64-bit integers
  • Comparisons
    • Prerequisites
    • Comparison operations

Library liblayers.compcertx.SimEvents

• • Semantics of volatile memory accesses
• Semantics of external functions

Library compcert.common.Switch

Library compcert.backend.Cminor

• Abstract syntax
• Operational semantics (small-step)
• Alternate operational semantics (big-step)
  • Correctness of the big-step semantics with respect to the transition semantics

Library compcert.backend.CminorSel

• Abstract syntax
• Operational semantics
• Lifting of let-bound variables

Library compcert.driver.Compopts

Library compcert.x86.SelectOp

• • Constants
  • Integer logical negation
  • Integer addition and pointer addition
  • Opposite
  • Integer and pointer subtraction
  • Immediate shifts
  • Integer multiply
  • Bitwise and, or, xor
  • Integer division and modulus
  • General shifts
  • Floating-point arithmetic
  • Comparisons
  • Integer conversions
  • Addressing modes
  • Arguments of builtins

Library compcert.x86.SelectOpproof

• Useful lemmas and tactics
• Correctness of the smart constructors

Library compcert.backend.SplitLong

Library compcert.backend.SplitLongproof

• Axiomatization of the helper functions
• Correctness of the instruction selection functions for 64-bit operators

Library compcert.x86.SelectLong

Library compcert.x86.SelectLongproof

• Correctness of the instruction selection functions for 64-bit operators

Library compcertx.driver.CompCertBuiltins

Library liblayers.compcertx.SimCompCertBuiltins

Library liblayers.compcertx.SimCop

Library compcertx.common.EventsX

Library liblayers.compcertx.SimClight

Library liblayers.compcertx.CompCertGlobalVars

Library liblayers.compcertx.CGlobalVars

Library liblayers.simrel.SimrelLessdef

• lessdef (and Mem.extends) as a simulation relation
• Strong version of extends for ec_mem_extends. Coincidentally,

Library liblayers.simrel.SimrelInject

• inject as a simulation relation
• Wrap simrel_inject into a stronger version, for ec_mem_inject

Library liblayers.compcertx.CPrimitives

• • Invariant
  • Properties
• User diagrams
  • Identity diagram
  • General diagram with invariants
  • Inclusion diagram with invariants

Library liblayers.compcertx.CGenSem

Library liblayers.logic.Language

• Language definitions
  • Layer logic
• Derived rules

Library liblayers.logic.LayerLogicImpl

Library liblayers.compcertx.ClightModules

Library liblayers.compcertx.MakeProgramFacts

• Preliminaries
  • Using make_program_noconflict
  • Elementary relations for make_program_rel
  • Other useful lemmas
• Properties relating module-layer pairs with their global environments
  • Intensional properties about single-binding module-layer pairs
  • Extensional properties
  • Consequences of single hypotheses
• Alternative monotonicity theorems
• Other global properties

Library liblayers.compcertx.MakeProgramInv

• The inv_make_globalenv tactic
• Test

Library liblayers.compcertx.MakeProgram

Library liblayers.compcertx.InitMemMakeProgram

• Prerequisites
• Proving simrel_program_rel

Library liblayers.compcertx.ClightWellTyped

• • Function execution is well-typed at return.

Library liblayers.compcertx.ClightXSemantics

• LayerLib Semantics of ClightX
  • Monotonicity in terms of genv_sim

Library liblayers.simrel.AbstractionRelation

• Definition
• Embedding as simrel
  • Definition
  • Lemmas
  • Initial states
  • Main proof

Library tutorial.common.TutoLib

• TutoLib.v
• A library of tactics and lemmas used in the layer tutorial.
  • Helper tactics
    • Code and Refinement Proof Helpers
    • General Helpers
    • Linking Helpers

Library tutorial.container.ContainerType

• ContainerType.v
• Definitions and properties of container data.
  • Abstract Data
  • Properties of a Valid Container
  • Container Properties
    • Child Quotas Bounded
    • Invariant Preservation
    • Container Struct Field Offsets

Library tutorial.container.Container

• Container.v
• Primitives to initialize and manage containers.
  • Abstract Data
  • High Level Specifications
  • Module Implementation
  • Low Level Specifications
  • Code Proofs
  • Layer Relation
  • Refinement Proofs
  • Linking

Library tutorial.container.ContainerIntro

• ContainerIntro.v
• Getter/setter layer.
  • Abstract Data
    • Underlay
    • Overlay
  • High Level Specifications
  • Module Implementation
  • Low Level Specifications
  • Code Proofs
  • Layer Relation
  • Refinement Proofs
  • Linking

Library tutorial.queue.AbsQueue

• AbsQueue.v
• Abstract queue representation.
  • Abstract Data
  • High Level Specifications
  • Layer Relation
  • Refinement Proofs
  • Linking

Library tutorial.queue.Node

• Node.v
• Node getter/setters.
  • High Level Specifications
  • Module Implementation
  • Low Level Specifications
  • Code Proofs
  • Refinement Proofs
  • Linking.

Library tutorial.queue.Queue

• Queue.v
• Low level queue representation.
  • Abstract Data
  • High Level Specifications
  • Module Implementation
  • Low Level Specifications
  • Code Proofs
  • Layer Relation
  • Refinement Proofs
  • Linking

Library tutorial.queue.QueueData

• QueueData.v
• Definitions and properties of queue and node data.
  • Node Representations
    • Low Level Definition
    • Abstract Definition
  • Queue Representations
    • Low Level Definition
  • Abstract Definition
  • Abstract Data
  • Node Properties
  • Composite Environments
  • Intro Layer Relations
    • Node
    • QueueIntro
  • Helper Lemmas

Library tutorial.queue.QueueIntro

• QueueIntro.v
• Queue getter/setters.
  • High Level Specifications
  • Module Implementation
  • Low Level Specifications
  • Code Proofs
  • Refinement Proofs
  • Linking

Library tutorial.stack.Stack

• Stack.v
• A layer implementing a bounded stack using a bounded counter.
  • Abstract Data
  • High Level Specifications
  • Module Implementation
  • Low Level Specifications
  • Code Proofs
  • Layer Relation
  • Refinement Proofs
  • Linking

Library tutorial.stack.Counter

• Counter.v
• A single layer implementing a bounded counter.
  • Abstract Data
    • Underlay
    • Overlay
  • High Level Specifications
  • Module Implementation
  • Low Level Specifications
  • Code Proofs
  • Layer Relation
  • Refinement Proofs
  • Linking