Merge pull request #909 from mktnk3/word_to_word_Pancake

CakeML · Oct 1, 2022 · 59e14a9 · 59e14a9
2 parents 8787dfe + 0651323
commit 59e14a9
Show file tree

Hide file tree

Showing 5 changed files with 1,137 additions and 42 deletions.
diff --git a/compiler/backend/proofs/backendProofScript.sml b/compiler/backend/proofs/backendProofScript.sml
@@ -3333,7 +3333,7 @@ Proof
  match_mp_tac ALOOKUP_ALL_DISTINCT_MEM \\
  simp[MAP_MAP_o,o_DEF,LAMBDA_PROD,data_to_wordTheory.compile_part_def,FST_triple,MEM_MAP,EXISTS_PROD] \\
  metis_tac[ALOOKUP_MEM] ) \\
- `data_to_wordProof$code_rel_ext (fromAList t_code) (fromAList p5)` by metis_tac[code_rel_ext_word_to_word] \\
+ `word_to_wordProof$code_rel_ext (fromAList t_code) (fromAList p5)` by metis_tac[word_to_wordProofTheory.code_rel_ext_word_to_word] \\
  qpat_x_assum`Abbrev(tar_st = _)`kall_tac \\
  (* syntactic properties from stack_to_lab *)
  `all_enc_ok_pre c4.lab_conf.asm_conf p7` by (

diff --git a/compiler/backend/proofs/data_to_wordProofScript.sml b/compiler/backend/proofs/data_to_wordProofScript.sml
@@ -1097,17 +1097,6 @@ Proof
  \\ disch_then drule \\ fs [extend_with_resource_limit'_def]
 QED
 
-val code_rel_ext_def = Define`
- code_rel_ext code l ⇔
- (∀n p_1 p_2.
- SOME (p_1,p_2) = lookup n code ⇒
- ∃t' k' a' c' col.
- SOME
- (SND (full_compile_single t' k' a' c' ((n,p_1,p_2),col))) =
- lookup n l)`
-
-val code_rel_ext_def = definition"code_rel_ext_def";
-
 Definition get_limits_def:
  get_limits c (t :('a, 'c, 'ffi) wordSem$state) =
  <| stack_limit := t.stack_limit
@@ -1603,35 +1592,6 @@ Proof
  \\ strip_tac \\ rveq \\ EVAL_TAC
 QED
 
-Theorem code_rel_ext_word_to_word:
- ∀code c1 col code'.
- compile c1 c2 code = (col,code') ⇒
- code_rel_ext (fromAList code) (fromAList code')
-Proof
- simp[word_to_wordTheory.compile_def,code_rel_ext_def] \\
- rw[]>>
- pairarg_tac>>fs[]>>rw[]>>
- `LENGTH n_oracles = LENGTH code` by
- (fs[word_to_wordTheory.next_n_oracle_def]>>
- every_case_tac>>rw[]>>fs[])>>
- last_x_assum mp_tac>>
- pop_assum mp_tac>>
- pop_assum kall_tac>>
- map_every qid_spec_tac [`n_oracles`,`p_1`,`p_2`,`n`]>>
- Induct_on`code` \\ rw[] \\
- fs[lookup_fromAList]>>
- Cases_on`n_oracles`>>fs[]>>
- Cases_on`h`>>fs[]>>
- simp[word_to_wordTheory.full_compile_single_def,SimpRHS] \\
- pairarg_tac \\ fs[] \\
- qmatch_asmsub_rename_tac`((q,p),h)` \\
- PairCases_on`p` \\ fs[word_to_wordTheory.compile_single_def] \\
- rveq \\ fs[] \\
- IF_CASES_TAC \\ fs[] \\
- simp[word_to_wordTheory.full_compile_single_def,word_to_wordTheory.compile_single_def]>>
- metis_tac[]
-QED
-
 Theorem max_heap_limit_has_fp_ops[simp]:
  max_heap_limit (:α) (conf with has_fp_ops := b) =
  max_heap_limit (:α) conf