machine_utils.finz
machine_utils.finz_base
machine_utils.finz_interval
machine_utils.finz_lemmas
machine_utils.solve_finz
machine_utils.classes
machine_utils.class_instances
machine_utils.solve_pure
machine_utils.tactics
cap_machine.iris_extra
cap_machine.stdpp_extra
cap_machine.stdpp_img
cap_machine.stdpp_comp
cap_machine.map_simpl
cap_machine.addr_reg
cap_machine.linking
- Various examples of WR predicates
- Main definitions
- Lemmas about resolve_imports: specification and utilities
- well_formedness of a ⋈ b and useful lemmas
- Lemmas on the symmetry/commutativity of links
- Lemmas on the associativity of links
- Component size and induction schemes
- Weakening of WR
- solve_can_link tactic
cap_machine.solve_addr
cap_machine.machine_base
cap_machine.machine_parameters
cap_machine.machine_run
cap_machine.classes
cap_machine.class_instances
cap_machine.solve_addr_extra
cap_machine.cap_lang
cap_machine.region
cap_machine.rules.rules_base
cap_machine.rules.rules_Get
cap_machine.rules.rules_Load
cap_machine.rules.rules_Store
cap_machine.rules.rules_AddSubLt
cap_machine.rules.rules_Lea
cap_machine.rules.rules_Mov
cap_machine.rules.rules_Restrict
cap_machine.rules.rules_IsPtr
cap_machine.rules.rules_Jmp
cap_machine.rules.rules_Jnz
cap_machine.rules.rules_Subseg
cap_machine.rules.rules_Seal
cap_machine.rules.rules_UnSeal
cap_machine.rules
cap_machine.rules_binary.rules_binary_base
cap_machine.rules_binary.rules_binary_Get
cap_machine.rules_binary.rules_binary_Load
cap_machine.rules_binary.rules_binary_Store
cap_machine.rules_binary.rules_binary_AddSubLt
cap_machine.rules_binary.rules_binary_Lea
cap_machine.rules_binary.rules_binary_Mov
cap_machine.rules_binary.rules_binary_Restrict
cap_machine.rules_binary.rules_binary_Jmp
cap_machine.rules_binary.rules_binary_Jnz
cap_machine.rules_binary.rules_binary_Subseg
cap_machine.rules_binary.rules_binary_IsPtr
cap_machine.rules_binary
cap_machine.solve_pure
cap_machine.NamedProp
cap_machine.proofmode_instr_rules
cap_machine.proofmode
cap_machine.seal_store
cap_machine.logrel
cap_machine.logrel_binary
cap_machine.monotone
cap_machine.ftlr.ftlr_base
cap_machine.ftlr.interp_weakening
cap_machine.ftlr.Get
cap_machine.ftlr.Load
cap_machine.ftlr.Store
cap_machine.ftlr.AddSubLt
cap_machine.ftlr.Lea
cap_machine.ftlr.Mov
cap_machine.ftlr.Restrict
cap_machine.ftlr.IsPtr
cap_machine.ftlr.Jmp
cap_machine.ftlr.Jnz
cap_machine.ftlr.Subseg
cap_machine.ftlr.Seal
cap_machine.ftlr.UnSeal
cap_machine.fundamental
cap_machine.register_tactics
cap_machine.ftlr_binary.ftlr_base_binary
cap_machine.ftlr_binary.interp_weakening
cap_machine.ftlr_binary.Load_binary
cap_machine.ftlr_binary.Mov_binary
cap_machine.ftlr_binary.AddSubLt_binary
cap_machine.ftlr_binary.Get_binary
cap_machine.ftlr_binary.IsPtr_binary
cap_machine.ftlr_binary.Jmp_binary
cap_machine.ftlr_binary.Jnz_binary
cap_machine.ftlr_binary.Lea_binary
cap_machine.ftlr_binary.Subseg_binary
cap_machine.ftlr_binary.Restrict_binary
cap_machine.ftlr_binary.Store_binary
cap_machine.ftlr_binary.Seal_binary
cap_machine.ftlr_binary.UnSeal_binary
cap_machine.fundamental_binary
cap_machine.contextual_refinement_adequacy
- interp_exports relation
- adequacy_hypothesis and lemma
- Memory and register map allocation
- Adequacy theorems
cap_machine.examples.addr_reg_sample
cap_machine.contextual_refinement
- Reserved context size
- Contextual Refinement definition
- Easy results about contextual refinement
- Dummy exports and registers
- Simplified results when Symbols is Infinite