Move no_install definition to wordProps (placed with no_alloc)

so that no_install_evaluate_const_code is available earlier
CakeML · Sep 6, 2022 · 9a04a01 · 9a04a01
1 parent 7e1f263
commit 9a04a01
Show file tree

Hide file tree

Showing 3 changed files with 132 additions and 132 deletions.
diff --git a/compiler/backend/proofs/word_elimProofScript.sml b/compiler/backend/proofs/word_elimProofScript.sml
@@ -36,84 +36,6 @@ Proof
 QED
 
 
-(**************************** no_install *****************************)
-
-(*  ensures there are no install instructions in the code to be optimised -
-    these will break the dead code elimination
-    pass as they introduce new code at runtime,
-    which may reference code that has been eliminated *)
-
-val no_install_def = Define `
-    (no_install (MustTerminate p) = no_install p) ∧
-    (no_install (Call ret _ _ handler) = (case ret of
-        | NONE => (case handler of
-            | NONE => T
-            | SOME (_,ph,_,_) => no_install ph)
-        | SOME (_,_,pr,_,_) => (case handler of
-            | NONE => no_install pr
-            | SOME (_,ph,_,_) => no_install ph ∧ no_install pr))) ∧
-    (no_install (Seq p1 p2) = (no_install p1 ∧ no_install p2)) ∧
-    (no_install (If _ _ _ p1 p2) = (no_install p1 ∧ no_install p2)) ∧
-    (no_install (Install _ _ _ _ _) = F) ∧
-    (no_install _ = T)
-`
-
-val no_install_ind = theorem "no_install_ind";
-
-val no_install_code_def = Define `
-    no_install_code (code : (num # ('a wordLang$prog)) num_map) ⇔
-        ∀ k n p . lookup k code = SOME (n, p) ⇒ no_install p
-`
-
-Theorem no_install_find_code:
-     ∀ code dest args lsize args1 expr ps.
-    no_install_code code ∧ find_code dest args code lsize = SOME (args1, expr, ps)
-    ⇒ no_install expr
-Proof
-  rw[no_install_code_def] >> Cases_on `dest` >> fs[find_code_def] >>
-  EVERY_CASE_TAC >> fs [] >> rveq >>
-  metis_tac[]
-QED
-
-Theorem no_install_evaluate_const_code:
-  ∀ prog s result s1 .
-    evaluate (prog, s) = (result, s1) ∧
-    no_install prog ∧ no_install_code s.code
-    ⇒ s.code = s1.code
-Proof
-    recInduct evaluate_ind >> rw[] >> qpat_x_assum `evaluate _ = _` mp_tac >>
-    fs[evaluate_def]
-    >- (EVERY_CASE_TAC >> fs[] >> rw[] >> imp_res_tac alloc_const >> fs[set_var_def])
-    >- (EVERY_CASE_TAC >> fs[] >> rw[] >> fs[set_var_def,unset_var_def])
-    >- (fs[get_vars_def, set_vars_def] >> EVERY_CASE_TAC >>
-        fs[] >> rw[] >> fs[get_vars_def])
-    >- (rw[] >> EVERY_CASE_TAC >> imp_res_tac inst_const_full >>
-        fs[] >> rveq >> fs[])
-    >- (EVERY_CASE_TAC >> fs[set_var_def] >> rw[] >> fs[])
-    >- (EVERY_CASE_TAC >> fs[set_var_def] >> rw[] >> fs[])
-    >- (EVERY_CASE_TAC >> fs[set_store_def] >> rw[] >> fs[])
-    >- (EVERY_CASE_TAC >> fs[set_var_def] >> rw[] >> fs[])
-    >- (EVERY_CASE_TAC >> fs[mem_store_def] >> rw[] >> fs[])
-    >- (EVERY_CASE_TAC >> fs[call_env_def, flush_state_def, dec_clock_def] >> rw[] >> fs[])
-    >- (EVERY_CASE_TAC >> fs[] >> rename1 `evaluate (p, st)` >>
-        Cases_on `evaluate (p, st)` >>
-        fs[no_install_def] >> EVERY_CASE_TAC >> fs[] >> rw[] >> fs[])
-    >- (Cases_on `evaluate (c1,s)` >> fs[no_install_def] >> CASE_TAC >> rfs[])
-    >- (EVERY_CASE_TAC >> fs[call_env_def, flush_state_def] >> rw[] >> fs[])
-    >- (fs[jump_exc_def] >> EVERY_CASE_TAC >> rw[] >> fs[])
-    >- (fs[no_install_def] >> EVERY_CASE_TAC >> rw[] >> fs[])
-    >- (EVERY_CASE_TAC >> fs[set_var_def] >> rw[] >> fs[])
-    >- (fs[no_install_def])
-    >- (EVERY_CASE_TAC >> rw[] >> fs[])
-    >- (EVERY_CASE_TAC >> rw[] >> fs[])
-    >- (EVERY_CASE_TAC >> rw[] >> fs[] >> fs[ffiTheory.call_FFI_def] >>
-        EVERY_CASE_TAC >> rw[] >> fs[state_component_equality])
-    >- (fs[no_install_def, dec_clock_def, call_env_def, flush_state_def, push_env_def,
-        cut_env_def, pop_env_def, set_var_def] >>
-        EVERY_CASE_TAC >> rw[] >> fs[] >> metis_tac[no_install_find_code])
-QED
-
-
 
 (**************************** DEFINITIONS *****************************)