Proof files for compiling Pancake.
crep_arithProofScript.sml: Correctness proof for crep_arith pass
crep_inlineProofScript.sml: Correctness proof for function inlining pass
crep_to_loopProofScript.sml: Correctness proof for crep_to_loop
loop_callProofScript.sml: loop_call proof
loop_liveProofScript.sml: Correctness proof for loop_live
loop_removeProofScript.sml: Correctness proof for loop_remove
loop_to_wordProofScript.sml: Correctness proof for loop_to_word
pan_globalsProofScript.sml: Correctness proof for pan_globals
pan_itreeEquivProofScript.sml: Proof of correspondence between functional big-step semantics and itree semantics for Pancake.
pan_simpProofScript.sml: Correctness proof for pan_simp
pan_to_crepProofScript.sml: Correctness proof for pan_to_crep
pan_to_targetProofScript.sml: composing semantics correctness from pan to target
pan_to_wordProofScript.sml: Correctness proof for combined pan_to_word compilation.