From 5e8396654fef9bbbb760fd68ce456e3f3f354d70 Mon Sep 17 00:00:00 2001 From: Hrutvik Kanabar Date: Mon, 13 Mar 2023 17:42:13 +0000 Subject: [PATCH] Prove end-to-end correctness Builds directly on cakeml/cakeml#933, including tidying up to account for its various changes. --- .../passes/proofs/pure_to_cakeProofScript.sml | 4 +- .../proofs/state_to_cakeProofScript.sml | 108 ++++++++++++++---- compiler/proofs/Holmakefile | 3 +- compiler/proofs/pure_compilerProofScript.sml | 11 +- .../proofs/pure_end_to_endProofScript.sml | 38 ++++++ 5 files changed, 134 insertions(+), 30 deletions(-) create mode 100644 compiler/proofs/pure_end_to_endProofScript.sml diff --git a/compiler/backend/passes/proofs/pure_to_cakeProofScript.sml b/compiler/backend/passes/proofs/pure_to_cakeProofScript.sml index 86dd5123..a3da9fd2 100644 --- a/compiler/backend/passes/proofs/pure_to_cakeProofScript.sml +++ b/compiler/backend/passes/proofs/pure_to_cakeProofScript.sml @@ -69,7 +69,9 @@ Theorem pure_to_cake_correct: ⇒ state_to_cakeProof$itree_rel (itree_of (exp_of x)) - (state_to_cakeProof$itree_semantics (pure_to_cake c ns x)) + (itree_semantics$itree_semantics (pure_to_cake c ns x)) ∧ + itree_semantics$safe_itree state_to_cakeProof$ffi_convention + (itree_semantics$itree_semantics (pure_to_cake c ns x)) Proof strip_tac \\ drule_all pure_to_state_correct diff --git a/compiler/backend/passes/proofs/state_to_cakeProofScript.sml b/compiler/backend/passes/proofs/state_to_cakeProofScript.sml index 2c872908..e8b3ab67 100644 --- a/compiler/backend/passes/proofs/state_to_cakeProofScript.sml +++ b/compiler/backend/passes/proofs/state_to_cakeProofScript.sml @@ -692,6 +692,10 @@ CoInductive itree_rel: ⇒ itree_rel (Vis (ch,conf) srest) (Vis (ch, compile_conf conf, ws) crest)) End +Definition ffi_convention_def: + ffi_convention = SUM_ALL (K T) (λbs. ∃s. compile_input_rel s bs) +End + (******************** Results ********************) @@ -2450,6 +2454,81 @@ Proof goal_assum drule >> gvs[state_rel] >> gvs[Once cont_rel_cases] QED +Theorem compile_safe_itree: + safe_itree (sinterp sr st sk) ∧ + dstep_rel (sr,st,sk) (step_n benv n dr) + ⇒ safe_itree ffi_convention (interp benv dr) +Proof + qsuff_tac + `∀d. + (∃s sr st sk benv n dr. + s = sinterp sr st sk ∧ d = interp benv dr ∧ + safe_itree (sinterp sr st sk) ∧ + dstep_rel (sr,st,sk) (step_n benv n dr) + ) ∨ + (∃out k. d = Ret (FinalFFI out k)) + ⇒ safe_itree ffi_convention d` + >- ( + rw[] >> first_x_assum irule >> disj1_tac >> + rpt $ goal_assum $ drule_at Any >> simp[] + ) >> + ho_match_mp_tac safe_itree_coind >> rw[] >> + `interp benv dr = interp benv (step_n benv n dr)` by simp[interp_take_steps] >> + pop_assum SUBST_ALL_TAC >> qmatch_goalsub_abbrev_tac `interp benv d'` >> + `step_until_halt (sr,st,sk) ≠ Err` by ( + gvs[Once sinterp] >> FULL_CASE_TAC >> gvs[] >> + gvs[Once pure_semanticsTheory.safe_itree_cases]) >> + drule_all step_until_halt_rel >> disch_then $ qspec_then `benv` assume_tac >> + gvs[next_res_rel_cases] + >- (once_rewrite_tac[sinterp, interp] >> simp[]) + >- (once_rewrite_tac[sinterp, interp] >> simp[]) >> + ntac 3 disj2_tac >> simp[Once sinterp, Once interp] >> + drule $ iffLR dstep_rel_cases >> rw[] >> gvs[] >> + drule $ iffLR step_rel_cases >> strip_tac >> gvs[] >> + qmatch_goalsub_abbrev_tac `ExpVal _ _ ffi_exp` >> + `LENGTH ws = max_FFI_return_size + 2` by gvs[state_rel, store_lookup_def] >> + Cases >> rw[Once ffi_convention_def] >> gvs[compile_input_rel_def] >> + disj1_tac >> irule_at Any EQ_REFL >> + qexistsl [`SOME sst`,`Val $ Atom $ Str s`,`sk'`] >> rw[GSYM PULL_EXISTS] + >- ( + last_x_assum mp_tac >> simp[Once sinterp] >> + simp[Once pure_semanticsTheory.safe_itree_cases] >> + disch_then $ qspec_then `INR s` mp_tac >> simp[Once sinterp] + ) >> + unabbrev_all_tac >> + ntac 7 (qrefine `SUC m` >> simp[dstep, cstep]) >> + simp[namespaceTheory.nsOptBind_def] >> + `nsLookup cenv.v (Short "ffi_array") = SOME (Loc 0)` by gvs[env_ok_def] >> + simp[] >> qrefine `SUC m` >> simp[dstep, cstep, do_app_def] >> + Cases_on `dst.refs` >> gvs[store_lookup_def, LUPDATE_DEF] >> + ntac 9 (qrefine `SUC m` >> simp[dstep, cstep, do_app_def]) >> + simp[store_lookup_def] >> + ntac 21 (qrefine `SUC m` >> simp[dstep, cstep, do_app_def]) >> + simp[opb_lookup_def, opn_lookup_def, do_if_def] >> + `&(256 * (STRLEN s DIV 256) MOD dimword (:8)) + &(STRLEN s MOD dimword (:8)) = + &(STRLEN s) : int` by ( + simp[wordsTheory.dimword_def, wordsTheory.dimindex_8] >> + gvs[max_FFI_return_size_def] >> ARITH_TAC) >> + pop_assum SUBST_ALL_TAC >> simp[] >> + ntac 9 (qrefine `SUC m` >> simp[dstep, cstep, do_app_def]) >> + simp[store_lookup_def, copy_array_def, integerTheory.INT_ADD_CALCULATE] >> + qmatch_goalsub_abbrev_tac `StrLit str1` >> + `str1 = s` by ( + unabbrev_all_tac >> simp[TAKE_APPEND, GSYM MAP_TAKE] >> + simp[ws_to_chars_def, MAP_MAP_o, combinTheory.o_DEF, IMPLODE_EXPLODE_I]) >> + pop_assum SUBST_ALL_TAC >> + Cases_on `ck'` >> gvs[] + >- ( + qrefine `SUC m` >> simp[dstep] >> + simp[astTheory.pat_bindings_def, pmatch_def] >> + ntac 2 (qrefine `SUC m` >> simp[dstep]) >> + simp[dstep_rel_cases] >> gvs[Once cont_rel_cases] + ) >> + qexists0 >> simp[dstep, store_lookup_def] >> + simp[dstep_rel_cases, step_rel_cases, PULL_EXISTS] >> + goal_assum drule >> gvs[state_rel] >> gvs[Once cont_rel_cases] +QED + (****************************** Lifting to cexp ******************************) @@ -2916,26 +2995,6 @@ QED (****************************** CakeML semantics ******************************) -(* Copied from CakeML backend_itreeProofTheory *) -val (_,start_env) = - prim_sem_env_eq |> Q.INST [`ffi` |-> `ARB`] |> - concl |> rhs |> optionSyntax.dest_some |> pairSyntax.dest_pair; - -Definition start_dstate_def: - start_dstate : dstate = - <| refs := []; next_type_stamp := 2; next_exn_stamp := 4; eval_state := NONE |> -End - -Definition start_env_def: - start_env = ^start_env -End - -Definition itree_semantics_def: - itree_semantics prog = - interp start_env (Dstep start_dstate (Decl (Dlocal [] prog)) []) -End -(* End copy *) - Theorem check_dup_ctors_ALL_DISTINCT[simp]: check_dup_ctors (tvs,tn,condefs) ⇔ ALL_DISTINCT (MAP FST condefs) Proof @@ -3538,10 +3597,12 @@ Theorem compile_correct: namespace_init_ok ns ∧ safe_itree (itree_of (exp_of e)) ⇒ itree_rel (itree_of (exp_of e)) - (itree_semantics (compile_with_preamble ns e)) + (itree_semantics (compile_with_preamble ns e)) ∧ + safe_itree ffi_convention (itree_semantics (compile_with_preamble ns e)) Proof - rw[itree_of_def, semantics_def, itree_semantics_def, cns_ok_def] >> - irule compile_itree_rel >> + simp[itree_of_def, semantics_def, itree_semantics_def, cns_ok_def] >> strip_tac >> + irule_at Any compile_itree_rel >> irule_at Any compile_safe_itree >> + goal_assum drule >> qrefinel [`n`,`n`] >> simp[] >> simp[dstep_rel_cases, step_rel_cases, PULL_EXISTS] >> simp[Once cont_rel_cases, env_rel_def, state_rel] >> gvs[namespace_init_ok_def] >> @@ -3619,7 +3680,6 @@ Proof rpt $ goal_assum drule >> simp[] >> gvs[cnenv_rel_def, prim_types_ok_def] QED - (**********) val _ = export_theory (); diff --git a/compiler/proofs/Holmakefile b/compiler/proofs/Holmakefile index 952915a3..8c3f0288 100644 --- a/compiler/proofs/Holmakefile +++ b/compiler/proofs/Holmakefile @@ -8,4 +8,5 @@ INCLUDES = .. \ ../backend/passes \ ../backend/passes/proofs \ $(CAKEMLDIR)/compiler/parsing \ - $(HOLDIR)/examples/bootstrap + $(HOLDIR)/examples/bootstrap \ + $(CAKEMLDIR)/compiler/backend/proofs diff --git a/compiler/proofs/pure_compilerProofScript.sml b/compiler/proofs/pure_compilerProofScript.sml index de0b8476..591f7374 100644 --- a/compiler/proofs/pure_compilerProofScript.sml +++ b/compiler/proofs/pure_compilerProofScript.sml @@ -26,7 +26,8 @@ Theorem compiler_correctness: safe_itree $ itree_of (exp_of pure_ce) ∧ itree_rel (itree_of (exp_of pure_ce)) - (itree_semantics cake) + (itree_semantics cake) ∧ + itree_semantics$safe_itree ffi_convention (itree_semantics cake) Proof strip_tac \\ gvs [compile_to_ast_def,frontend_def,AllCaseEqs()] \\ qabbrev_tac ‘e4 = transform_cexp c e1’ @@ -63,7 +64,7 @@ Proof \\ qsuff_tac ‘itree_of (exp_of e4) = itree_of (exp_of e2)’ >- ( disch_then $ rewrite_tac o single \\ simp[] - \\ irule_at Any pure_to_cakeProofTheory.pure_to_cake_correct + \\ irule pure_to_cakeProofTheory.pure_to_cake_correct \\ fs [cns_ok_def, pure_typingTheory.namespace_init_ok_def, EXISTS_PROD] ) >> qspec_then `e4` mp_tac clean_cexp_correct >> strip_tac >> @@ -89,7 +90,8 @@ Theorem alternative_compiler_correctness: compile_to_ast c s = SOME cake ∧ itree_rel (itree_of (exp_of pure_ce)) - (itree_semantics cake) + (itree_semantics cake) ∧ + itree_semantics$safe_itree ffi_convention (itree_semantics cake) Proof strip_tac >> assume_tac $ Q.GEN `cake` compiler_correctness >> gvs[compile_to_ast_alt_def] @@ -130,7 +132,8 @@ Theorem pure_compiler_to_string_correct: safe_exp (exp_of pure_ce) ∧ itree_rel (itree_of (exp_of pure_ce)) - (itree_semantics cake_prog) + (itree_semantics cake_prog) ∧ + itree_semantics$safe_itree ffi_convention (itree_semantics cake_prog) Proof rw[compile_to_string] >> simp[string_to_ast_ast_to_string] >> drule compiler_correctness >> rw[] >> gvs[frontend_def, AllCaseEqs()] >> diff --git a/compiler/proofs/pure_end_to_endProofScript.sml b/compiler/proofs/pure_end_to_endProofScript.sml new file mode 100644 index 00000000..9c9b196d --- /dev/null +++ b/compiler/proofs/pure_end_to_endProofScript.sml @@ -0,0 +1,38 @@ +(* + End-to-end correctness for the PureCake compiler +*) +open HolKernel Parse boolLib bossLib; +open pure_compilerProofTheory backend_itreeProofTheory state_to_cakeProofTheory; + +val _ = new_theory "pure_end_to_endProof"; + +Overload cake_compile = ``backend$compile``; + +Overload target_configs_ok = + ``λconf (mc,ms). backend_config_ok conf ∧ mc_conf_ok mc ∧ mc_init_ok conf mc`` + +Overload code_in_memory = + ``λconf (bytes,bitmaps,c') (mc,ms). + ∃cbspace data_sp. + installed bytes cbspace bitmaps data_sp c'.lab_conf.ffi_names + (backendProof$heap_regs conf.stack_conf.reg_names) mc ms`` + +Overload prunes = ``λpt mt. ∃ct. itree_rel pt ct ∧ prune ffi_convention F ct mt`` + +Theorem end_to_end_correctness: + compile_to_ast c s = SOME cake ∧ + cake_compile conf cake = SOME code ∧ + target_configs_ok conf m ∧ + code_in_memory conf code m + ⇒ ∃ce ns. frontend c s = SOME (ce,ns) ∧ + prunes (pure_semantics$itree_of (exp_of ce)) (machine_sem_itree m) +Proof + rw[] >> drule pure_compilerProofTheory.compiler_correctness >> rw[] >> + rpt $ goal_assum drule >> PairCases_on `m` >> PairCases_on `code` >> gvs[] >> + gvs[ffi_convention_def] >> + irule itree_compile_correct >> gvs[PULL_EXISTS, GSYM ffi_convention_def] >> + rpt $ goal_assum $ drule_at Any >> simp[] +QED + +val _ = export_theory(); +