Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
..
Failed to load latest commit information.
examples
Holmakefile
README.md
cfAppLib.sig
cfAppLib.sml
cfAppScript.sml
cfAppSyntax.sig
cfAppSyntax.sml
cfComputeLib.sml
cfFFITypeScript.sml
cfHeapsBaseLib.sig
cfHeapsBaseLib.sml
cfHeapsBaseScript.sml
cfHeapsBaseSyntax.sml
cfHeapsLib.sig
cfHeapsLib.sml
cfHeapsScript.sml
cfLetAutoLib.sig
cfLetAutoLib.sml
cfLetAutoScript.sml
cfLib.sml
cfMainScript.sml
cfNormaliseLib.sig
cfNormaliseLib.sml
cfNormaliseScript.sml
cfScript.sml
cfStoreScript.sml
cfSyntax.sig
cfSyntax.sml
cfTacticsBaseLib.sig
cfTacticsBaseLib.sml
cfTacticsLib.sig
cfTacticsLib.sml
cfTacticsScript.sml
cf_examples_pmatch.sml
eqSolveRewriteLib.sig
eqSolveRewriteLib.sml
evarsConseqConvLib.sig
evarsConseqConvLib.sml
readmePrefix

README.md

A verified CakeML adaption of Arthur Charguéraud's "Characteristic Formulae for the Verification of Imperative Programs"

cfAppLib.sml: Defines app_of_Arrow_rule function that converts the translator's Arrow to CF's app judgement.

cfAppScript.sml: App: [app] is used to give a specification for the application of a value to one or multiple value arguments. It is in particular used in cf to abstract from the concrete representation of closures.

cfAppSyntax.sml: Helper functions that construct/destruct syntax from cfAppTheory.

cfComputeLib.sml: Auxiliary definitions used in cfs

cfFFITypeScript.sml: Defines a type that can be used for embedding different FFI models for parts of the FFI state.

cfHeapsBaseLib.sml: Implements CF tactics for CF-style separation logic

cfHeapsBaseScript.sml: Defines the heap type that the separation logic used by CF uses. Also defines POSTv etc.

cfHeapsBaseSyntax.sml: Functions that aid in dealing with syntax of CF-style separation logic.

cfHeapsLib.sml: Conversions etc. over hprops

cfHeapsScript.sml: Defines what is means for a CF separation logic assertion to be "local".

cfLetAutoLib.sml: Theorems, conversions, solvers used by the xlet_auto tactic.

cfLetAutoScript.sml: Definitions and lemmas that support the implementation of the xlet_auto tactic.

cfLib.sml: This library collects all CF-related libraries and theories into a single import for convenience.

cfMainScript.sml: The following section culminates in call_main_thm2 which takes a spec and some aspects of the current state, and proves a Semantics_prog statement.

cfNormaliseLib.sml: Automation that normalises a CakeML program. In particular, this means turning it into A-normal form.

cfNormaliseScript.sml: Defines the normalise_prog function which puts an arbitrary program in A-normal form.

cfScript.sml: Defines the characteristic formula (CF) function cf_def and proves that it is sound w.r.t. the evaluate semantics of CakeML.

cfStoreScript.sml: Conversion from semantic stores to heaps.

cfSyntax.sml: Helper functions for syntax from cfTheory.

cfTacticsBaseLib.sml: Various tactics for reasoning about CF-based goals in HOL.

cfTacticsLib.sml: Various tactics for reasoning about CF-based goals in HOL.

cfTacticsScript.sml: Lemmas that aid the tactics for reasoning about CF-based goals in HOL.

eqSolveRewriteLib.sml: Defines ELIM_UNKWN_CONV conversion

evarsConseqConvLib.sml: Some experimental code for emulating evars support in HOL.

examples: This directory contains examples of how the CF tactics can be used.