Make bvl/bvi/dataLang have ref definition separate from closLang

CakeML · Feb 10, 2024 · 48a421d · 48a421d
1 parent b76383b
commit 48a421d
Show file tree

Hide file tree

Showing 9 changed files with 66 additions and 31 deletions.
diff --git a/compiler/backend/proofs/bvl_inlineProofScript.sml b/compiler/backend/proofs/bvl_inlineProofScript.sml
@@ -1924,7 +1924,7 @@ Theorem state_cc_compile_inc_eq:
       (in_cc limit (remove_ticks_cc (let_op_cc o1 o2 cc)))
 Proof
   fs [state_cc_def,compile_inc_def,in_cc_def,FUN_EQ_THM,remove_ticks_cc_def,
-      let_op_cc_def] \\ rw []
+      let_op_cc_def,FORALL_PROD] \\ rw []
   \\ rpt (pairarg_tac \\ fs []) \\ rveq
   \\ fs [MAP_optimise]
 QED

diff --git a/compiler/backend/proofs/clos_to_bvlProofScript.sml b/compiler/backend/proofs/clos_to_bvlProofScript.sml
@@ -1022,6 +1022,19 @@ val compile_oracle_inv_def = Define`
   ^dummy_compile_oracle_inv max_app s_code s_cc s_co t_code t_cc t_co ⇔ T`;
 *)
 
+val ref_rel_def = Define`
+  (ref_rel R (closSem$ValueArray vs) (bvlSem$ValueArray ws) ⇔ LIST_REL R vs ws) ∧
+  (ref_rel R (ByteArray f as) (ByteArray g bs) ⇔ f = g ∧ as = bs) ∧
+  (ref_rel _ _ _ = F)`
+val _ = export_rewrites["ref_rel_def"];
+
+Theorem ref_rel_simp[simp]:
+   (ref_rel R (ValueArray vs) y ⇔ ∃ws. y = ValueArray ws ∧ LIST_REL R vs ws) ∧
+   (ref_rel R (ByteArray f bs) y ⇔ y = ByteArray f bs)
+Proof
+  Cases_on`y`>>simp[ref_rel_def] >> srw_tac[][EQ_IMP_THM]
+QED
+
 val state_rel_def = Define `
   state_rel f (s:('c,'ffi) closSem$state) (t:('c,'ffi) bvlSem$state) <=>
     (s.ffi = t.ffi) /\
@@ -3860,7 +3873,7 @@ Proof
       full_simp_tac(srw_ss())[SUBMAP_DEF,FAPPLY_FUPDATE_THM,FDIFF_def,DRESTRICT_DEF] >> srw_tac[][] >> METIS_TAC[])
     \\ Cases_on `op = Update` \\ full_simp_tac(srw_ss())[] THEN1
      (full_simp_tac(srw_ss())[closSemTheory.do_app_def,bvlSemTheory.do_app_def]
-      \\ fs[case_eq_thms,bool_case_eq] \\ rveq
+      \\ fs[case_eq_thms,bool_case_eq,AllCaseEqs()] \\ rveq
       \\ fs[SWAP_REVERSE_SYM]
       \\ rveq \\ fs[v_rel_SIMP] \\ rveq
       \\ fs[SWAP_REVERSE,PULL_EXISTS]
@@ -4073,7 +4086,7 @@ Proof
       simp[Abbr`pp`,LEAST_NOTIN_FDOM])
     \\ Cases_on `op = UpdateByte` \\ full_simp_tac(srw_ss())[] THEN1 (
       full_simp_tac(srw_ss())[closSemTheory.do_app_def,bvlSemTheory.do_app_def]
-      \\ fs[case_eq_thms,PULL_EXISTS,bool_case_eq]
+      \\ fs[case_eq_thms,PULL_EXISTS,bool_case_eq,AllCaseEqs()]
       \\ rw[] \\ fs[SWAP_REVERSE_SYM] \\ rw[]
       \\ fs[v_rel_SIMP] \\ rw[]
       \\ imp_res_tac evaluate_const
@@ -4297,7 +4310,7 @@ Proof
     \\ Cases_on`∃fl. op = CopyByte fl` \\ fs[] >- (
       fs[closSemTheory.do_app_def,bvlSemTheory.do_app_def,PULL_EXISTS]
       \\ Cases_on`fl`
-      \\ fs[case_eq_thms,v_case_eq_thms,PULL_EXISTS,SWAP_REVERSE_SYM]
+      \\ fs[case_eq_thms,v_case_eq_thms,PULL_EXISTS,SWAP_REVERSE_SYM,AllCaseEqs()]
       \\ rveq \\ fs[v_rel_SIMP] \\ rw[] \\ fs[FLOOKUP_UPDATE] \\ rw[]
       \\ TRY (drule (GEN_ALL state_rel_refs_lookup) \\ disch_then imp_res_tac \\ fs[FLOOKUP_UPDATE])
       \\ TRY (

diff --git a/compiler/backend/proofs/data_to_word_assignProofScript.sml b/compiler/backend/proofs/data_to_word_assignProofScript.sml
@@ -1958,7 +1958,7 @@ Theorem do_app_aux_safe_for_space_mono:
   (do_app_aux op xs s = Rval (r,s1)) /\ s1.safe_for_space ==> s.safe_for_space
 Proof
   Cases_on `op` \\
-  fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,
+  fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,AllCaseEqs(),
       bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_space_def,
       with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def,
       ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,check_lim_def,
@@ -13573,6 +13573,8 @@ Proof
   \\ gvs [good_dimindex_def,dimword_def]
 QED
 
+val _ = Parse.hide "free";
+
 Theorem assign_Build:
    (∃parts. op = Build parts) ==> ^assign_thm_goal
 Proof[exclude_simps = EXP_LE_LOG_SIMP EXP_LT_LOG_SIMP LE_EXP_LOG_SIMP

diff --git a/compiler/backend/proofs/data_to_word_memoryProofScript.sml b/compiler/backend/proofs/data_to_word_memoryProofScript.sml
@@ -12631,6 +12631,8 @@ Proof
   \\ imp_res_tac SUBSET_FINITE_I
 QED
 
+val _ = Parse.hide "free";
+
 Theorem memory_rel_do_build:
   ∀parts i st free curr sp map0 map0' refs ts refs1 v m v ws.
     do_build map0 i parts refs (SOME ts) = (v,refs1,SOME ts1) ∧

diff --git a/compiler/backend/semantics/bviSemScript.sml b/compiler/backend/semantics/bviSemScript.sml
@@ -3,6 +3,7 @@
 *)
 open preamble bviTheory;
 local open backend_commonTheory bvlSemTheory in end;
+local open backendPropsTheory in end;
 
 val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
 

diff --git a/compiler/backend/semantics/bvlPropsScript.sml b/compiler/backend/semantics/bvlPropsScript.sml
@@ -2,7 +2,7 @@
   Properties about BVL and its semantics
 *)
 open preamble bvlTheory bvlSemTheory bvl_constTheory;
-open closPropsTheory backend_commonTheory;
+open backend_commonTheory;
 
 val _ = temp_delsimps ["NORMEQ_CONV"]
 
@@ -31,9 +31,12 @@ Proof
 QED
 
 fun get_thms ty = { case_def = TypeBase.case_def_of ty, nchotomy = TypeBase.nchotomy_of ty }
-val case_eq_thms = LIST_CONJ (closSemTheory.case_eq_thms::
-                              map (prove_case_eq_thm o get_thms)
-  [``:v``,``:'a ffi_result``])
+val case_eq_thms = LIST_CONJ
+  (CaseEq "eq_result" :: CaseEq "const_part" :: CaseEq "word_size" ::
+   CaseEq "result" :: CaseEq "error_result" ::
+   map (prove_case_eq_thm o get_thms)
+  [``:v``,``:'a ref``,``:'a option``,``:'a list``,``:'a + 'b``,
+   ``:closLang$op``,``:'a ffi_result``])
 val case_eq_thms = CONJ bool_case_eq (CONJ pair_case_eq case_eq_thms)
 
 val _ = save_thm ("case_eq_thms", case_eq_thms);

diff --git a/compiler/backend/semantics/bvlSemScript.sml b/compiler/backend/semantics/bvlSemScript.sml
@@ -3,23 +3,34 @@
 *)
 open preamble bvlTheory closSemTheory
 open clos_to_bvlTheory (* for closure_tag and num_added_globals *)
+local open backendPropsTheory in end;
 
 val _ = new_theory"bvlSem"
 
 val _ = Parse.hide "str";
 
 (* --- Semantics of BVL --- *)
 
+Datatype:
+  ref = ValueArray ('a list)
+      | ByteArray bool (word8 list)
+               (* T = compare-by-contents, immutable
+                  F = compare-by-pointer, mutable *)
+               (* in closLang all are ByteArray F,
+                  ByteArray T introduced in BVL to implement ByteVector *)
+End
+
 (* these parts are shared by bytecode and, if bytecode is to be supported, need
    to move to a common ancestor *)
 
-val _ = Datatype `
+Datatype:
   v =
     Number int          (* integer *)
   | Word64 word64
   | Block num (v list)  (* cons block: tag and payload *)
   | CodePtr num         (* code pointer *)
-  | RefPtr num          (* pointer to ref cell *)`;
+  | RefPtr num          (* pointer to ref cell *)
+End
 
 val Boolv_def = Define`
   Boolv b = bvlSem$Block (bool_to_tag b) []`
@@ -29,15 +40,16 @@ val Unit_def = Define`
 
 (* -- *)
 
-val _ = Datatype `
+Datatype:
   state =
     <| globals : (bvlSem$v option) list
      ; refs    : num |-> bvlSem$v ref
      ; clock   : num
      ; compile : 'c -> (num # num # bvl$exp) list -> (word8 list # word64 list # 'c) option
      ; compile_oracle : num -> 'c # (num # num # bvl$exp) list
      ; code    : (num # bvl$exp) num_map
-     ; ffi     : 'ffi ffi_state |> `
+     ; ffi     : 'ffi ffi_state |>
+End
 
 val v_to_list_def = Define`
   (v_to_list (Block tag []) =

diff --git a/compiler/backend/semantics/dataPropsScript.sml b/compiler/backend/semantics/dataPropsScript.sml
@@ -211,7 +211,7 @@ val do_app_with_stack = time Q.prove(
   \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’)
   \\ ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,
               bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def,
-              with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def,
+              with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def,
               ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,
               semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
               pair_case_eq,consume_space_def,op_space_reset_def,check_lim_def] >>
@@ -234,7 +234,7 @@ val do_app_with_stack_and_locals = time Q.prove(
   \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’)
   \\ ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,
               bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def,
-              with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def,
+              with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def,
               ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,
               semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
               pair_case_eq,consume_space_def,op_space_reset_def,check_lim_def] >>
@@ -252,7 +252,7 @@ Proof
   \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’)
   \\ ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,
               bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def,
-              with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def,
+              with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def,
               ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,
               semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
               pair_case_eq,consume_space_def,check_lim_def] >>
@@ -268,7 +268,7 @@ Proof
   \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’)
   \\ ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,
               bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def,
-              with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def,
+              with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def,
               ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,
               semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
               pair_case_eq,consume_space_def,check_lim_def] >>
@@ -288,7 +288,7 @@ val do_app_with_locals = time Q.prove(
   \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’)
   \\ ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,
               bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def,
-              with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def,
+              with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def,
               ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,
               semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
               pair_case_eq,consume_space_def,check_lim_def] >>
@@ -432,7 +432,7 @@ val do_app_swap_tac =
               , MAX_DEF
               , check_lim_def]
   \\ TRY (pairarg_tac \\ fs [])
-  \\ TRY (fs [list_case_eq,option_case_eq,v_case_eq,bool_case_eq,closSemTheory.ref_case_eq
+  \\ TRY (fs [list_case_eq,option_case_eq,v_case_eq,bool_case_eq,bvlSemTheory.ref_case_eq
         , ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq, state_component_equality
         , semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,pair_case_eq
         , limits_component_equality,stack_consumed_def]
@@ -611,7 +611,7 @@ val full_fs = fs[ get_var_def, set_var_def
 val full_cases = fs [ list_case_eq,option_case_eq
                           , v_case_eq
                           , bool_case_eq
-                          , closSemTheory.ref_case_eq
+                          , bvlSemTheory.ref_case_eq
                           , ffiTheory.ffi_result_case_eq
                           , ffiTheory.oracle_result_case_eq
                           , semanticPrimitivesTheory.eq_result_case_eq
@@ -1622,7 +1622,7 @@ Proof
   Cases_on `op` >> TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) >>
   ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,
               bool_case_eq,ffiTheory.call_FFI_def,stack_consumed_def,
-              with_fresh_ts_def,closSemTheory.ref_case_eq,space_consumed_with_clock,
+              with_fresh_ts_def,bvlSemTheory.ref_case_eq,space_consumed_with_clock,
               ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,
               semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
               pair_case_eq,consume_space_def,size_of_heap_with_clock,check_lim_def] >>
@@ -1642,7 +1642,7 @@ Proof
   Cases_on `op` >> TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) >>
   ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,
               bool_case_eq,ffiTheory.call_FFI_def,stack_consumed_def,
-              with_fresh_ts_def,closSemTheory.ref_case_eq,space_consumed_with_clock,
+              with_fresh_ts_def,bvlSemTheory.ref_case_eq,space_consumed_with_clock,
               ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,
               semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
               pair_case_eq,consume_space_def,size_of_heap_with_clock,check_lim_def] >>
@@ -1662,7 +1662,7 @@ Proof
   Cases_on `op` >> TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) >>
   ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,
               bool_case_eq,ffiTheory.call_FFI_def,
-              with_fresh_ts_def,closSemTheory.ref_case_eq,
+              with_fresh_ts_def,bvlSemTheory.ref_case_eq,
               ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,
               semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
               pair_case_eq,consume_space_def,check_lim_def] >>
@@ -1700,7 +1700,7 @@ Proof
      \\ srw_tac[][] >> fs[])
   >- (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,cut_state_opt_def,cut_state_def
          , bool_case_eq,ffiTheory.call_FFI_def,semanticPrimitivesTheory.result_case_eq
-         , with_fresh_ts_def,closSemTheory.ref_case_eq
+         , with_fresh_ts_def,bvlSemTheory.ref_case_eq
          , ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq
          , semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq
          , pair_case_eq,consume_space_def]
@@ -1786,7 +1786,7 @@ Proof
   Cases_on `x` >> TRY (rename [‘EqualConst cc’] >> Cases_on ‘cc’) >>
   ntac 2 (fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,
               bool_case_eq,ffiTheory.call_FFI_def,
-              with_fresh_ts_def,closSemTheory.ref_case_eq,
+              with_fresh_ts_def,bvlSemTheory.ref_case_eq,
               ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,
               semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
               pair_case_eq,consume_space_def,check_lim_def] >>
@@ -2004,7 +2004,7 @@ Proof
   Cases_on `op` \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) \\
   fs [do_app_aux_def,list_case_eq,option_case_eq,v_case_eq,
       bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def,
-      with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def,
+      with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def,
       ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,check_lim_def,
       semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
       pair_case_eq,consume_space_def,op_space_reset_def,data_spaceTheory.op_space_req_def]
@@ -2553,7 +2553,7 @@ Proof
   ntac 2(
   fs[do_app_aux_def,cc_co_only_diff_def,do_app_def,do_stack_def,list_case_eq,option_case_eq,v_case_eq,
      bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def,
-     with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def,stack_consumed_def,
+     with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def,stack_consumed_def,
      ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,space_consumed_def,
      semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
      pair_case_eq,consume_space_def,op_space_reset_def,check_lim_def,
@@ -2592,7 +2592,7 @@ Proof
   Cases_on ‘op’ \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) \\ fs [] >>
   fs[do_app_aux_def,cc_co_only_diff_def,do_app_def,list_case_eq,option_case_eq,v_case_eq,
      bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def,
-     with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def,
+     with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def,
      ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,
      semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
      pair_case_eq,consume_space_def,op_space_reset_def,check_lim_def,
@@ -2771,7 +2771,7 @@ Proof
   Cases_on ‘op’ \\ TRY (rename [‘EqualConst cc’] \\ Cases_on ‘cc’) \\ fs [] >>
   fs[do_app_aux_def,cc_co_only_diff_def,do_app_def,do_stack_def,list_case_eq,option_case_eq,v_case_eq,
      bool_case_eq,ffiTheory.call_FFI_def,do_app_def,do_stack_def,do_space_def,
-     with_fresh_ts_def,closSemTheory.ref_case_eq,do_install_def,
+     with_fresh_ts_def,bvlSemTheory.ref_case_eq,do_install_def,
      ffiTheory.ffi_result_case_eq,ffiTheory.oracle_result_case_eq,
      semanticPrimitivesTheory.eq_result_case_eq,astTheory.word_size_case_eq,
      pair_case_eq,consume_space_def,op_space_reset_def,check_lim_def,

diff --git a/compiler/backend/semantics/dataSemScript.sml b/compiler/backend/semantics/dataSemScript.sml
@@ -1,8 +1,10 @@
 (*
   The formal semantics of dataLang
 *)
-open preamble data_simpTheory data_liveTheory data_spaceTheory dataLangTheory closSemTheory
+open preamble data_simpTheory data_liveTheory data_spaceTheory
+     dataLangTheory bvlSemTheory
      data_to_wordTheory (* TODO: immoral, semantics shouldn't depend on compiler *);
+local open backendPropsTheory in end;
 
 val _ = new_theory"dataSem";
 
@@ -1249,7 +1251,7 @@ val list_thms = { nchotomy = list_nchotomy, case_def = list_case_def };
 val option_thms = { nchotomy = option_nchotomy, case_def = option_case_def };
 val op_thms = { nchotomy = closLangTheory.op_nchotomy, case_def = closLangTheory.op_case_def };
 val v_thms = { nchotomy = theorem"v_nchotomy", case_def = definition"v_case_def" };
-val ref_thms = { nchotomy = closSemTheory.ref_nchotomy, case_def = closSemTheory.ref_case_def };
+val ref_thms = { nchotomy = bvlSemTheory.ref_nchotomy, case_def = bvlSemTheory.ref_case_def };
 val ffi_result_thms = { nchotomy = ffiTheory.ffi_result_nchotomy, case_def = ffiTheory.ffi_result_case_def };
 val word_size_thms = { nchotomy = astTheory.word_size_nchotomy, case_def = astTheory.word_size_case_def };
 val eq_result_thms = { nchotomy = semanticPrimitivesTheory.eq_result_nchotomy, case_def = semanticPrimitivesTheory.eq_result_case_def };