Introduction
Types
Envs
- Value
- Arch
- Metadata
- Variables
- Global
- Mem
- Heap
- Stack
- Allocated Mem Block
- Env
- Primitives
- WellFormedness
Axioms
Tactics
Syntax
CSemantics
ISemantics
Libs
- Properties of validAddress
- Properties of primitives
- storeMem and storeMemMeta preserve well-formed Envs
- Decidable primitives
- Properties of Frames and Stacks
- Properties of well-formed syntax and types
- About type size and offset
- More lemmas for Arith
WfEnv
- malloc preserves well-formed Envs.
- free preserves well-formed Envs.
- createFrame preserves well-formed Envs.
- destroyFrame preserves well-formed Envs.
Props
- s_rhs and s_cmd preserve Global and Stack.
- Lookup functions return valid Addresses.
- Inversion properties of s_lhs and s_rhs.
- Preservation
- s_rhs preserves well-formed Envs.
- s_rhs evaluates to wfData.
- dataCast preserves well-formed Datas.
- accessMemMeta returns well-formed Datas.
- Well-formed Datas are preserved by subset operations.
- s_lhs evaluates to well-formed Datas.
- s_rhs evaluates to well-formed Datas.
- s_cmd preserves well-formed Envs.
- Progress
BackSim
This page has been generated by coqdoc