Fix cost examples

CakeML · May 21, 2021 · e186cc1 · e186cc1
1 parent 1739080
commit e186cc1
Show file tree

Hide file tree

Showing 5 changed files with 89 additions and 52 deletions.
diff --git a/examples/cost/allProofScript.sml b/examples/cost/allProofScript.sml
@@ -187,6 +187,12 @@ Proof
   \\ fs [lookup_insert] \\ rfs []
 QED
 
+val fields = TypeBase.fields_of “:('c,'ffi) dataSem$state”;
+
+Overload state_locals_fupd = (fields |> assoc "locals" |> #fupd);
+Overload state_stack_max_fupd = (fields |> assoc "stack_max" |> #fupd);
+Overload state_safe_for_space_fupd = (fields |> assoc "safe_for_space" |> #fupd);
+
 Theorem foldl_evaluate:
   ∀n s vl ts_f tag_f tag_acc tsl sstack lsize smax ts.
     (* Sizes *)
@@ -295,7 +301,7 @@ in
   \\ ‘safe’ by
      (qunabbrev_tac ‘safe’ \\ fs [size_of_stack_def,GREATER_DEF] \\ EVAL_TAC)
   \\ simp [] \\ ntac 2 (pop_assum kall_tac)
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ qunabbrev_tac ‘rest_call’
   \\ simp [move_def,lookup_def,set_var_def,lookup_insert]
   \\ IF_CASES_TAC
@@ -317,7 +323,7 @@ in
           >- (qmatch_goalsub_abbrev_tac ‘size_of_heap s'’
               \\ ‘size_of_heap s' ≤ size_of_heap s’ suffices_by fs []
               \\ qunabbrev_tac ‘s'’
-              \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+              \\ eval_goalsub_tac ``state_locals_fupd _ _``
               \\ simp [size_of_heap_def,stack_to_vs_def,toList_def,toListA_def]
               \\ qmatch_goalsub_abbrev_tac ‘f1::f2::Block 0 1 []::rest_v’
               \\ qmatch_goalsub_abbrev_tac ‘f1::rest::f3::rest_v’
@@ -393,7 +399,7 @@ in
       >- (qmatch_goalsub_abbrev_tac ‘size_of_heap s'’
           \\ ‘size_of_heap s' ≤ size_of_heap s’ suffices_by fs []
           \\ qunabbrev_tac ‘s'’
-          \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+          \\ eval_goalsub_tac ``state_locals_fupd _ _``
           \\ simp [size_of_heap_def,stack_to_vs_def,toList_def,toListA_def]
           \\ qmatch_goalsub_abbrev_tac ‘_ (size_of _ (f1::rest::_::rest_v) _ _) ≤
                                         _ (size_of _ (_::f2::_) _ _)’

diff --git a/examples/cost/cyesProofScript.sml b/examples/cost/cyesProofScript.sml
@@ -31,6 +31,14 @@ val printLoop_body =
   |> (REWRITE_CONV [cyes_data_prog_def] THENC EVAL)
   |> concl |> rand |> rand |> rand
 
+val fields = TypeBase.fields_of “:('c,'ffi) dataSem$state”;
+
+Overload state_refs_fupd = (fields |> assoc "refs" |> #fupd);
+Overload state_locals_fupd = (fields |> assoc "locals" |> #fupd);
+Overload state_stack_max_fupd = (fields |> assoc "stack_max" |> #fupd);
+Overload state_safe_for_space_fupd = (fields |> assoc "safe_for_space" |> #fupd);
+Overload state_peak_heap_length_fupd = (fields |> assoc "peak_heap_length" |> #fupd);
+
 Theorem data_safe_cyes_code:
   ∀s ts smax sstack lsize.
    s.safe_for_space ∧
@@ -99,7 +107,7 @@ Proof
   \\ ntac 2 strip_assign
   \\ strip_assign \\ fs []
   \\ ntac 3 (strip_assign \\ fs [])
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   (* strip_call *)
   \\ qmatch_goalsub_abbrev_tac (`bind _ rest_call2 _`)
   \\ ONCE_REWRITE_TAC [bind_def]
@@ -133,7 +141,7 @@ Proof
   \\ ASM_REWRITE_TAC [] \\ ntac 2 (pop_assum kall_tac)
   \\ IF_CASES_TAC >- simp [data_safe_def]
   \\ REWRITE_TAC [ push_env_def , to_shallow_def , to_shallow_thm]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   (* strip_assign *)
   \\ strip_assign
   \\ make_if
@@ -169,7 +177,7 @@ Proof
   \\ REWRITE_TAC [ call_env_def   , dec_clock_def
                  , to_shallow_thm , to_shallow_def ]
   \\ simp [LET_DEF]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ strip_assign
   \\ make_if
   \\ Q.UNABBREV_TAC `rest_call2`
@@ -178,7 +186,7 @@ Proof
   \\ Q.ABBREV_TAC `pred = ∃w. 0 = w2n (w:word8)`
   \\ `pred` by (UNABBREV_ALL_TAC \\ qexists_tac `n2w 0` \\ rw [])
   \\ fs [] \\ pop_assum kall_tac \\ pop_assum kall_tac
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ qmatch_goalsub_abbrev_tac (`bind _ rest_call2 _`)
   \\ ONCE_REWRITE_TAC [bind_def]
   \\ simp [ call_def     , find_code_def  , push_env_def
@@ -214,7 +222,7 @@ Proof
   \\ ASM_REWRITE_TAC [] \\ ntac 2 (pop_assum kall_tac)
   \\ IF_CASES_TAC >- simp [data_safe_def]
   \\ REWRITE_TAC [ push_env_def , to_shallow_def , to_shallow_thm]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   (* strip_assign *)
   \\ strip_assign
   \\ make_if
@@ -279,7 +287,7 @@ Proof
   \\ REWRITE_TAC [ call_env_def   , dec_clock_def
                  , to_shallow_thm , to_shallow_def ]
   \\ simp [LET_DEF]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ strip_assign
   \\ make_if
   \\ Q.UNABBREV_TAC `rest_call2`
@@ -289,7 +297,7 @@ Proof
   \\ Q.ABBREV_TAC `pred = ∃w. 0 = w2n (w:word8)`
   \\ `pred` by (UNABBREV_ALL_TAC \\ qexists_tac `n2w 0` \\ rw [])
   \\ fs [] \\ pop_assum kall_tac \\ pop_assum kall_tac
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ qmatch_goalsub_abbrev_tac `insert p2 _ (insert p1 _ s.refs)`
   \\ strip_assign
   \\ fs [lookup_insert]
@@ -396,7 +404,7 @@ Proof
   \\ REWRITE_TAC [ call_env_def   , dec_clock_def
                  , to_shallow_thm , to_shallow_def ]
   \\ simp [LET_DEF]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ ho_match_mp_tac data_safe_res
   \\ reverse conj_tac >- (rw [] \\ pairarg_tac \\ rw [])
   (* Make stack_max sane to look at *)
@@ -511,7 +519,7 @@ Proof
   \\ REWRITE_TAC [ call_env_def   , dec_clock_def
                  , to_shallow_thm , to_shallow_def ]
   \\ simp [LET_DEF]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ strip_assign
   \\ make_if
   \\ Q.UNABBREV_TAC `rest_call_1`
@@ -533,7 +541,7 @@ Proof
           , size_of_stack_frame_def]
   \\ IF_CASES_TAC >- simp []
   \\ REWRITE_TAC [ push_env_def , to_shallow_def , to_shallow_thm]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ strip_assign
   \\ make_if
   \\ strip_assign
@@ -557,7 +565,7 @@ Proof
   \\ REWRITE_TAC [ call_env_def   , dec_clock_def
                  , to_shallow_thm , to_shallow_def ]
   \\ simp[LET_THM]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ strip_assign
   \\ make_if
   \\ Q.UNABBREV_TAC `rest_call_1`
@@ -593,7 +601,7 @@ Proof
   \\ reverse (Cases_on `call_FFI s.ffi "put_char" [97w] []`) >- simp []
   \\ strip_assign (* \\ strip_assign *)
   \\ rw [return_def,lookup_def]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ Q.UNABBREV_TAC `rest_call`
   (*  make_tailcall *)
   \\ ASM_REWRITE_TAC [ tailcall_def , find_code_def

diff --git a/examples/cost/lcgLoopProofScript.sml b/examples/cost/lcgLoopProofScript.sml
@@ -29,6 +29,14 @@ val coeff_bounds_def = Define`
   small_num T (&m) ∧
   small_num T (&(a*m + c))`
 
+val fields = TypeBase.fields_of “:('c,'ffi) dataSem$state”;
+
+Overload state_refs_fupd = (fields |> assoc "refs" |> #fupd);
+Overload state_locals_fupd = (fields |> assoc "locals" |> #fupd);
+Overload state_stack_max_fupd = (fields |> assoc "stack_max" |> #fupd);
+Overload state_safe_for_space_fupd = (fields |> assoc "safe_for_space" |> #fupd);
+Overload state_peak_heap_length_fupd = (fields |> assoc "peak_heap_length" |> #fupd);
+
 Theorem size_of_Number_head_append:
   ∀ls.
   EVERY (λl. case l of Number n => small_num lims.arch_64_bit n | _ => F) ls ⇒
@@ -1254,7 +1262,7 @@ in
   \\ qmatch_goalsub_abbrev_tac `bind _ rest_mkspc _`
   \\ ASM_REWRITE_TAC [ bind_def, makespace_def, add_space_def]
   \\ eval_goalsub_tac ``dataSem$cut_env _ _`` \\ simp []
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ Q.UNABBREV_TAC `rest_mkspc`
   \\ still_safe
   \\ rename1`state_peak_heap_length_fupd (K pkheap1) _`
@@ -1340,7 +1348,7 @@ in
   \\ Q.ABBREV_TAC `pred = ∃w. 0 = w2n (w:word8)`
   \\ `pred` by (UNABBREV_ALL_TAC \\ qexists_tac `n2w 0` \\ rw [])
   \\ fs [] \\ pop_assum kall_tac \\ pop_assum kall_tac
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ still_safe
   >- (rfs [size_of_Number_head,small_num_def]
       \\ qmatch_asmsub_abbrev_tac ‘size_of _ (_::ll)’
@@ -1464,7 +1472,7 @@ in
   \\ Q.ABBREV_TAC `pred = ∃w. 0 = w2n (w:word8)`
   \\ `pred` by (UNABBREV_ALL_TAC \\ qexists_tac `n2w 0` \\ rw [])
   \\ fs [] \\ pop_assum kall_tac \\ pop_assum kall_tac
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ qmatch_goalsub_abbrev_tac `insert p2 _ (insert p1 _ s.refs)`
   \\ simp []
   \\ `p1 ≠ p2` by
@@ -2201,7 +2209,7 @@ in
   \\ pop_assum kall_tac
   (* move 14 13 *)
   \\ simp [move_def,lookup_def,set_var_def]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   (* Exit if *)
   \\ Q.UNABBREV_TAC ‘if_rest_ass’
   (* make_space 3 ... *)
@@ -2296,7 +2304,7 @@ in
   \\ strip_tac \\ simp[]
   >- simp[data_safe_def]
   \\ simp[pop_env_def,set_var_def]
-  \\ eval_goalsub_tac “dataSem$state_locals_fupd _ _”>>
+  \\ eval_goalsub_tac “state_locals_fupd _ _”>>
   (* call_put_chars (21,⦕ 1; 2; 3; 14 ⦖) [20] NONE; *)
   simp[Once bind_def]>>
   simp [ call_def      , find_code_def  , push_env_def
@@ -2363,7 +2371,7 @@ in
   simp[]
   >- simp[data_safe_def]>>
   simp[pop_env_def,set_var_def] >>
-  eval_goalsub_tac “dataSem$state_locals_fupd _ _”>>
+  eval_goalsub_tac “state_locals_fupd _ _”>>
   (* tailcall_lcgLoop [14; 1; 2; 3] *)
   ASM_REWRITE_TAC [ tailcall_def , find_code_def
                   , get_vars_def , get_var_def
@@ -2437,9 +2445,9 @@ in
       simp[closed_ptrs_APPEND])>>
     rw[])>>
   simp[to_shallow_thm]>>
-  eval_goalsub_tac “dataSem$state_locals_fupd _ _”>>
+  eval_goalsub_tac “state_locals_fupd _ _”>>
   strip_tac>>
-  eval_goalsub_tac “dataSem$state_locals_fupd _ _”>>
+  eval_goalsub_tac “state_locals_fupd _ _”>>
   pairarg_tac>>fs[]>>
   rw[]>>fs[data_safe_def]
 end
@@ -2574,7 +2582,7 @@ in
   drop_state>>
   (* move 14 13 *)
   simp [move_def,lookup_def,set_var_def]
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``>>
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``>>
   (* Exit if *)
   Q.UNABBREV_TAC ‘if_rest_ass’ >>
   (* make_space 3 ... *)

diff --git a/examples/cost/sumProofScript.sml b/examples/cost/sumProofScript.sml
@@ -24,6 +24,14 @@ val sum_x64_conf = (rand o rator o lhs o concl) sum_thm
 val _ = install_naming_overloads "sumProg";
 val _ = write_to_file sum_data_prog_def;
 
+val fields = TypeBase.fields_of “:('c,'ffi) dataSem$state”;
+
+Overload state_refs_fupd = (fields |> assoc "refs" |> #fupd);
+Overload state_locals_fupd = (fields |> assoc "locals" |> #fupd);
+Overload state_stack_max_fupd = (fields |> assoc "stack_max" |> #fupd);
+Overload state_safe_for_space_fupd = (fields |> assoc "safe_for_space" |> #fupd);
+Overload state_peak_heap_length_fupd = (fields |> assoc "peak_heap_length" |> #fupd);
+
 val foldl_body = ``lookup_List_foldl (fromAList sum_data_prog)``
            |> (REWRITE_CONV [sum_data_code_def] THENC EVAL)
            |> concl |> rhs |> rand |> rand
@@ -184,7 +192,7 @@ Proof
   \\ simp [return_def,flush_state_def,state_component_equality]
   \\ fs [size_of_stack_def] \\ rfs []
   \\ (conj_tac
-      >- (eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+      >- (eval_goalsub_tac ``state_locals_fupd _ _``
           \\ qmatch_goalsub_abbrev_tac ‘size_of_heap ss’
           \\ ‘ss = s’ suffices_by rw []
           \\ UNABBREV_ALL_TAC \\ rw [state_component_equality])
@@ -586,7 +594,7 @@ in
   \\ qunabbrev_tac ‘s'’
   \\ simp [pop_env_def,set_var_def]
   \\ qunabbrev_tac ‘rest_call’
-  \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+  \\ eval_goalsub_tac ``state_locals_fupd _ _``
   \\ max_is ‘MAX smax (lsize + sstack + x1 + 4)’
   >- fs [MAX_DEF]
   \\ simp [move_def,lookup_def,set_var_def,lookup_insert]
@@ -620,7 +628,7 @@ in
          \\ `size_of_heap s' + bb' ≤ size_of_heap s + bb` suffices_by fs[]
          \\ pop_assum kall_tac
          \\ qunabbrev_tac ‘s'’
-         \\ eval_goalsub_tac ``dataSem$state_locals_fupd _ _``
+         \\ eval_goalsub_tac ``state_locals_fupd _ _``
          \\ simp [size_of_heap_def,stack_to_vs_def,toList_def,toListA_def,extract_stack_def]
          \\ qmatch_goalsub_abbrev_tac ‘Number acc::rest_v’
          \\ rpt (pairarg_tac \\ fs[]) \\ rveq \\ fs []