This directory contains the correctness proofs for all of the different phases of the compiler backend.
backendProofScript.sml: Composes the correctness theorems for all of the compiler phases.
backend_itreeProofScript.sml: Compiler correctness for the itree CakeML semantics
bvi_letProofScript.sml: Correctness proof for bvi_let
bvi_tailrecProofScript.sml: Correctness proof for bvi_tailrec
bvi_to_dataProofScript.sml: Correctness proof for bvi_to_data
bvl_constProofScript.sml: Correctness proof for bvl_const
bvl_handleProofScript.sml: Correctness proof for bvl_handle
bvl_inlineProofScript.sml: Correctness proof for bvi_inline
bvl_jumpProofScript.sml: Correctness proof for bvl_jump
bvl_to_bviProofScript.sml: Correctness proof for bvl_to_bvi
clos_annotateProofScript.sml: Correctness proof for clos_annotate
clos_callProofScript.sml: Correctness proof for clos_call
clos_constantProofScript.sml: Some functions that flatten a closLang/BVL/BVI/dataLang const tree into a sequence of operations that share common data.
clos_fvsProofScript.sml: Correctness proof for clos_fvs
clos_interpProofScript.sml: Correctness proof for closLang interpreter used by the REPL, i.e. Install, to avoid spending time compiling simple run-once code in declarations.
clos_knownProofScript.sml: Correctness proof for clos_known
clos_knownPropsScript.sml: Lemmas used in proof of clos_known
clos_letopProofScript.sml: Correctness proof for clos_letop
clos_mtiProofScript.sml: Correctness proof for the clos_mti compiler pass. The theorem is proved using a backwards simulation, i.e. against the direction of compilation.
clos_numberProofScript.sml: Correctness proof for clos_number
clos_opProofScript.sml: Correctness proof for clos_op
clos_ticksProofScript.sml: Correctness proof for clos_ticks
clos_to_bvlProofScript.sml: Correctness proof for clos_to_bvl
data_liveProofScript.sml: Correctness proof for data_live
data_simpProofScript.sml: Correctness proof for data_simp
data_spaceProofScript.sml: Correctness proof for data_space
data_to_wordProofScript.sml: Correctness proof for data_to_word
data_to_word_assignProofScript.sml: Part of the correctness proof for data_to_word
data_to_word_bignumProofScript.sml: Part of the correctness proof for data_to_word
data_to_word_gcProofScript.sml: Part of the correctness proof for data_to_word
data_to_word_memoryProofScript.sml: Part of the correctness proof for data_to_word
experimentalLib.sml: Some proof tools, mostly quite experimental, used in some of the proofs in this directory
flat_elimProofScript.sml: Correctness proof for flatLang dead code elimination
flat_patternProofScript.sml: Correctness proof for flat_pattern
flat_to_closProofScript.sml: Correctness proof for flat_to_clos
lab_filterProofScript.sml: Correctness proof for lab_filter
lab_to_targetProofScript.sml: Correctness proof for lab_to_target
source_evalProofScript.sml: Proofs that the eval mode of the source semantics can be switched to one that includes an oracle.
source_letProofScript.sml: Correctness for the source_let pass.
source_to_flatProofScript.sml: Correctness proof for source_to_flat
source_to_sourceProofScript.sml: Proof of correctness for source_to_source.
stack_allocProofScript.sml: Correctness proof for stack_alloc
stack_namesProofScript.sml: Correctness proof for stack_names
stack_rawcallProofScript.sml: Correctness proof for stack_rawcall
stack_removeProofScript.sml: Correctness proof for stack_remove
stack_to_labProofScript.sml: Correctness proof for stack_to_lab
wordConvsProofScript.sml: Syntactic properties proofs for word_to_word.
word_allocProofScript.sml: Correctness proof for word_alloc
word_bignumProofScript.sml: Correctness proof for word_bignum
word_copyProofScript.sml: Correctness proof for word_copy
word_cseProofScript.sml: Correctness proof for word_cse
word_depthProofScript.sml: Proves correctness of the max_depth applied to the call graph of a wordLang program as produced by the word_depth$call_graph function.
word_elimProofScript.sml: Correctness proof for word_elim
word_gcFunctionsScript.sml: Shallow embedding of garbage collector implementation
word_instProofScript.sml: Correctness proof for word_inst
word_removeProofScript.sml: Correctness proof for word_remove
word_simpProofScript.sml: Correctness proof for word_simp
word_to_stackProofScript.sml: Correctness proof for word_to_stack
word_to_wordProofScript.sml: Correctness proof for word_to_word
word_unreachProofScript.sml: Correctness proof for word_unreach