Add Thunks to CakeML source

basis/fsFFIPropsScript.sml

@@ -150,7 +150,7 @@ Proof
   fs [validFD_def,nextFD_def]
   \\ qabbrev_tac `xs = MAP FST fs.infds`
   \\ match_mp_tac (SIMP_RULE std_ss []
-          (Q.ISPEC `\n:num. ~MEM n xs` whileTheory.LEAST_INTRO))
+          (Q.ISPEC `\n:num. ~MEM n xs` WhileTheory.LEAST_INTRO))
   \\ qexists_tac `SUM xs + 1`
   \\ strip_tac
   \\ qsuff_tac `!xs m:num. MEM m xs ==> m <= SUM xs`

basis/pure/mlstringScript.sml

@@ -749,10 +749,10 @@ Theorem OLEAST_LE_STEP:
     else (OLEAST j. i + 1 <= j /\ P j))
 Proof
   rw []
-  \\ simp [whileTheory.OLEAST_EQ_SOME]
+  \\ simp [WhileTheory.OLEAST_EQ_SOME]
   \\ qmatch_goalsub_abbrev_tac `opt1 = $OLEAST _`
   \\ Cases_on `opt1`
-  \\ fs [whileTheory.OLEAST_EQ_SOME]
+  \\ fs [WhileTheory.OLEAST_EQ_SOME]
   \\ rw []
   \\ fs [LESS_EQ |> REWRITE_RULE [ADD1] |> GSYM, arithmeticTheory.LT_LE]
   \\ CCONTR_TAC

candle/overloading/syntax/holSyntaxExtraScript.sml

@@ -12996,7 +12996,7 @@ Proof
   rw[] >>
   last_x_assum(qspec_then `f` mp_tac) >>
   disch_then assume_tac >>
-  pop_assum(mp_tac o Ho_Rewrite.REWRITE_RULE[whileTheory.LEAST_EXISTS]) >>
+  pop_assum(mp_tac o Ho_Rewrite.REWRITE_RULE[WhileTheory.LEAST_EXISTS]) >>
   rename1 `f n` >>
   rpt strip_tac >>
   reverse(Cases_on `R' (f n) (f (SUC n))`) >- goal_assum drule >>

candle/overloading/syntax/holSyntaxScript.sml

@@ -298,7 +298,7 @@ QED
 Theorem LEAST_EXISTS[local]:
   (∃n:num. P n) ⇒ ∃k. P k ∧ ∀m. m < k ⇒ ¬(P m)
 Proof
-  metis_tac[whileTheory.LEAST_EXISTS]
+  metis_tac[WhileTheory.LEAST_EXISTS]
 QED
 
 val VARIANT_PRIMES_def = new_specification

candle/prover/candle_basis_evaluateScript.sml

@@ -220,6 +220,7 @@ Proof
   >- (Cases_on ‘op’ \\ gs[])
   >- (Cases_on ‘op’ \\ gs[])
   >- (Cases_on ‘op’ \\ gs[])
+  >- (Cases_on ‘op’ \\ gvs [])
   >- (
     gvs [do_app_cases, Boolv_def]
     \\ rw [v_ok_def]

candle/prover/candle_prover_evaluateScript.sml

@@ -635,15 +635,175 @@ Proof
     rw[do_app_cases] \\ gs [SF SFY_ss]
     \\ first_assum (irule_at Any)
     \\ simp [v_ok_def])
+  \\ Cases_on ‘∃m. op = ThunkOp (AllocThunk m)’ \\ gs[]
+  >- (
+    rw [do_app_cases] \\ gs [thunk_op_def, AllCaseEqs()]
+    \\ pairarg_tac \\ gvs []
+    \\ gvs [v_ok_def, store_alloc_def, EVERY_EL, LLOOKUP_EQ_EL]
+    \\ first_assum (irule_at Any) \\ gs []
+    \\ rw [EL_APPEND_EQN] \\ gs [NOT_LESS, LESS_OR_EQ, ref_ok_def]
+    >- (
+      gs [kernel_loc_ok_def, LLOOKUP_EQ_EL, EL_APPEND_EQN]
+      \\ first_x_assum (drule_then strip_assume_tac)
+      \\ rw [] \\ gs [SF SFY_ss])
+    \\ strip_tac
+    \\ first_x_assum (drule_then assume_tac)
+    \\ drule kernel_loc_ok_LENGTH \\ gs [])
+  \\ Cases_on ‘∃m. op = ThunkOp (UpdateThunk m)’ \\ gs[]
+  >- (
+    rw [do_app_cases] \\ gs [thunk_op_def, AllCaseEqs()]
+    \\ first_assum (irule_at Any)
+    \\ gvs [v_ok_def, store_assign_def, EVERY_EL, EL_LUPDATE, LLOOKUP_EQ_EL]
+    \\ rw [ref_ok_def]
+    \\ irule kernel_loc_ok_LUPDATE1
+    \\ rpt strip_tac \\ gs [])
+  \\ Cases_on ‘op = ThunkOp ForceThunk’ \\ gs[]
+  >- (rw [do_app_cases] \\ gs [thunk_op_def, AllCaseEqs()])
   \\ Cases_on ‘op’ \\ gs []
+  \\ Cases_on ‘t’ \\ gs []
+QED
+
+Theorem state_ok_dest_thunk:
+  state_ok ctxt s ∧
+  EVERY (v_ok ctxt) vs ∧
+  dest_thunk (REVERSE vs) s.refs = IsThunk m v ⇒ v_ok ctxt v
+Proof
+  rw []
+  >- (
+    gvs [state_ok_def, oneline dest_thunk_def, AllCaseEqs(), v_ok_def,
+         store_lookup_def, LLOOKUP_THM]
+    \\ first_x_assum drule \\ rw [] \\ gvs [ref_ok_def])
+  \\ rw [env_ok_def, sing_env_def]
+  \\ Cases_on ‘n'’ \\ gvs []
+  \\ gvs [namespaceTheory.nsEmpty_def, namespaceTheory.nsBind_def,
+          namespaceTheory.nsLookup_def]
+  \\ gvs [oneline dest_thunk_def, AllCaseEqs(), store_lookup_def, state_ok_def,
+          LLOOKUP_THM, v_ok_def]
+  \\ first_x_assum drule_all \\ rw [] \\ gvs [ref_ok_def]
+QED
+
+Theorem state_ok_update_thunk:
+  state_ok ctxt s ∧
+  EVERY (v_ok ctxt) vs ∧
+  EVERY (v_ok ctxt) vs2 ∧
+  update_thunk (REVERSE vs) s.refs vs2 = SOME refs ⇒
+    state_ok ctxt (s with refs := refs)
+Proof
+  rw []
+  \\ gvs [oneline update_thunk_def, AllCaseEqs(), store_assign_def,
+          state_ok_def, LLOOKUP_LUPDATE, v_ok_def]
+  \\ goal_assum drule \\ gvs [] \\ rw []
+  >- (
+    irule kernel_loc_ok_LUPDATE1 \\ gvs []
+    \\ metis_tac [EXTENSION])
+  >- (first_x_assum drule \\ rw [])
+  >- gvs [ref_ok_def]
 QED
 
 Theorem evaluate_v_ok_Op:
   op ≠ Opapp ∧ op ≠ Eval ⇒ ^(get_goal "ast$App")
 Proof
   rw [evaluate_def] \\ Cases_on ‘getOpClass op’ \\ gs[]
-  >~ [‘EvalOp’] >- (Cases_on ‘op’ \\ gs[])
-  >~ [‘FunApp’] >- (Cases_on ‘op’ \\ gs[])
+  >~ [‘EvalOp’] >- (Cases_on ‘op’ \\ gs[] \\ Cases_on ‘t’ \\ gs[])
+  >~ [‘FunApp’] >- (Cases_on ‘op’ \\ gs[] \\ Cases_on ‘t’ \\ gs[])
+  >~ [‘Force’] >- (
+    Cases_on ‘op’ \\ gvs [] \\ Cases_on ‘t’ \\ gvs []
+    \\ qpat_x_assum ‘_ = (s',res)’ mp_tac
+    \\ TOP_CASE_TAC \\ gvs []
+    \\ last_x_assum drule_all \\ strip_tac
+    \\ reverse TOP_CASE_TAC \\ gvs []
+    >- (
+      rw [] \\ gvs []
+      \\ goal_assum drule \\ gvs [])
+    \\ TOP_CASE_TAC \\ gvs []
+    >~ [‘BadRef’] >- (
+      rw [] \\ gvs []
+      \\ goal_assum drule \\ gvs [state_ok_def])
+    >~ [‘NotThunk’] >- (
+      rw [] \\ gvs []
+      \\ goal_assum drule \\ gvs [state_ok_def])
+    \\ TOP_CASE_TAC \\ gvs []
+    >- (
+      rw [] \\ gvs []
+      \\ goal_assum drule \\ gvs []
+      \\ drule_all_then assume_tac state_ok_dest_thunk \\ gvs [])
+    \\ TOP_CASE_TAC \\ gvs []
+    >- (
+      rw [] \\ gvs []
+      \\ goal_assum drule \\ gvs [state_ok_def])
+    \\ ntac 2 (TOP_CASE_TAC \\ gvs [])
+    >- (
+      rw [] \\ gvs []
+      \\ goal_assum drule \\ gvs [state_ok_def])
+    \\ TOP_CASE_TAC \\ gvs []
+    \\ ‘state_ok ctxt' (dec_clock q)’
+      by (gvs [dec_clock_def, state_ok_def] \\ metis_tac [])
+    \\ Cases_on ‘kernel_vals ctxt' v’
+    >- (
+      drule (INST_TYPE [“:'a”|->“:'ffi”] kernel_vals_ok)
+      \\ ‘v_ok ctxt' (Conv NONE [])’ by gvs [v_ok_def]
+      \\ disch_then (drule_all_then (strip_assume_tac)) \\ gs []
+      >- (
+        rw [] \\ gvs []
+        \\ goal_assum drule \\ gvs [state_ok_def])
+      \\ rpt (TOP_CASE_TAC \\ gvs [])
+      >- (
+        rw [] \\ gvs []
+        \\ goal_assum drule \\ gvs [state_ok_def])
+      >- (
+        rw [] \\ gvs []
+        \\ qexists ‘ctxt''’ \\ gvs []
+        \\ drule_at (Pat ‘update_thunk _ _ _ = _’) state_ok_update_thunk
+        \\ disch_then $ qspec_then ‘ctxt''’ mp_tac
+        \\ impl_tac \\ gvs []
+        \\ gvs [EVERY_EL])
+      >- (
+        rw [] \\ gvs []
+        \\ qexists ‘ctxt''’ \\ gvs [])
+      \\ rw [] \\ gvs []
+      \\ qexists ‘ctxt''’ \\ gvs [state_ok_def])
+    \\ first_x_assum drule
+    \\ impl_tac >- (
+      gvs [do_opapp_cases]
+      >~ [‘Closure env1 n e’] >- (
+        drule_all state_ok_dest_thunk \\ strip_tac
+        \\ gvs [v_ok_def]
+        \\ irule env_ok_with_nsBind \\ gvs [v_ok_def]
+        \\ ‘env1 with c := env1.c = env1’ by simp [sem_env_component_equality]
+        \\ gvs [])
+      \\ drule_all state_ok_dest_thunk \\ strip_tac
+      \\ gvs [v_ok_def]
+      \\ gs [env_ok_def, evaluateTheory.dec_clock_def, find_recfun_ALOOKUP,
+             SF SFY_ss]
+      \\ drule_then assume_tac ALOOKUP_MEM
+      \\ gs [EVERY_MEM, EVERY_MAP, FORALL_PROD, SF SFY_ss]
+      \\ Cases \\ simp [build_rec_env_merge, ml_progTheory.nsLookup_nsBind_compute]
+      \\ rw [] \\ gs []
+      \\ gs [nsLookup_nsAppend_some, nsLookup_alist_to_ns_some,
+             nsLookup_alist_to_ns_none]
+      >- simp [v_ok_def]
+      >~ [‘ALOOKUP _ _ = SOME _’] >- (
+        drule_then assume_tac ALOOKUP_MEM
+        \\ gvs [MEM_MAP, EXISTS_PROD, v_ok_def, EVERY_MEM]
+        \\ rw [DISJ_EQ_IMP, env_ok_def] \\ gs [SF SFY_ss])
+      \\ first_x_assum irule
+      \\ gs [SF SFY_ss])
+    \\ strip_tac \\ gvs []
+    \\ reverse TOP_CASE_TAC \\ gvs []
+    >- (
+      rw [] \\ gvs []
+      \\ goal_assum $ drule_at (Pos $ el 2)
+      \\ rw [] \\ gvs [])
+    \\ TOP_CASE_TAC \\ gvs []
+    >- (
+      rw [] \\ gvs []
+      \\ goal_assum drule \\ gvs [state_ok_def])
+    \\ strip_tac \\ gvs []
+    \\ goal_assum $ drule_at (Pos $ el 3) \\ gvs []
+    \\ drule_at (Pat ‘update_thunk _ _ _ = _’) state_ok_update_thunk \\ gvs []
+    \\ disch_then drule \\ gvs []
+    \\ impl_tac \\ gvs []
+    \\ gvs [EVERY_EL])
   >~ [‘Simple’] >- (
     gvs [AllCaseEqs()]
     \\ first_x_assum (drule_all_then strip_assume_tac) \\ gs [state_ok_def]

candle/prover/candle_prover_invScript.sml

@@ -205,7 +205,8 @@ Theorem kernel_vals_ind = v_ok_ind
 Definition ref_ok_def:
   ref_ok ctxt (Varray vs) = EVERY (v_ok ctxt) vs ∧
   ref_ok ctxt (Refv v) = v_ok ctxt v ∧
-  ref_ok ctxt (W8array vs) = T
+  ref_ok ctxt (W8array vs) = T ∧
+  ref_ok ctxt (Thunk m v) = v_ok ctxt v
 End
 
 Definition kernel_loc_ok_def:

candle/prover/permsScript.sml

@@ -37,7 +37,9 @@ Definition perms_ok_exp_def:
           (op = AallocFixed ⇒ RefAlloc ∈ ps) ∧
           (op = Aw8alloc ⇒ W8Alloc ∈ ps) ∧
           (op = Opassign ⇒ RefUpdate ∈ ps) ∧
-          (∀chn. op = FFI chn ⇒ FFIWrite chn ∈ ps ∧ DoFFI ∈ ps)
+          (∀chn. op = FFI chn ⇒ FFIWrite chn ∈ ps ∧ DoFFI ∈ ps) ∧
+          (∀m. op = ThunkOp (AllocThunk m) ⇒ RefAlloc ∈ ps) ∧
+          (∀m. op = ThunkOp (UpdateThunk m) ⇒ RefUpdate ∈ ps)
       | _ => T
 End
 
@@ -182,7 +184,8 @@ QED
 Definition perms_ok_ref_def:
   perms_ok_ref ps (Refv v) = perms_ok ps v ∧
   perms_ok_ref ps (Varray vs) = EVERY (perms_ok ps) vs ∧
-  perms_ok_ref ps (W8array ws) = T
+  perms_ok_ref ps (W8array ws) = T ∧
+  perms_ok_ref ps (Thunk _ v) = perms_ok ps v
 End
 
 Definition perms_ok_state_def:
@@ -295,6 +298,8 @@ Theorem do_app_perms:
   (op = Aw8alloc ⇒ W8Alloc ∈ ps) ∧
   (op = Opassign ⇒ RefUpdate ∈ ps) ∧
   (∀chn. op = FFI chn ⇒ FFIWrite chn ∈ ps ∧ DoFFI ∈ ps) ∧
+  (∀m. op = ThunkOp (AllocThunk m) ⇒ RefAlloc ∈ ps) ∧
+  (∀m. op = ThunkOp (UpdateThunk m) ⇒ RefUpdate ∈ ps) ∧
   op ≠ Opapp ⇒
     (∀n. n < LENGTH refs1 ∧ RefMention n ∈ ps ⇒ perms_ok_ref ps (EL n refs1)) ∧
     (RefAlloc ∉ ps ∧ W8Alloc ∉ ps ⇒ LENGTH refs1 = LENGTH refs) ∧
@@ -556,7 +561,22 @@ Proof
   >- (
     rw [do_app_cases] \\ gs[]
     \\ rw [perms_ok_def])
+  \\ Cases_on ‘∃m. op = ThunkOp (AllocThunk m)’ \\ gs[]
+  >- (
+    rw [do_app_cases] \\ gs [thunk_op_def, AllCaseEqs()] \\ pairarg_tac \\ gs []
+    \\ gvs [perms_ok_def, store_alloc_def, perms_ok_ref_def, SUBSET_DEF]
+    \\ simp [EL_APPEND_EQN]
+    \\ rw [] \\ gs []
+    \\ gvs [NOT_LESS, LESS_OR_EQ, perms_ok_ref_def])
+  \\ Cases_on ‘∃m. op = ThunkOp (UpdateThunk m)’ \\ gs[]
+  >- (
+    rw [do_app_cases] \\ gs [thunk_op_def, AllCaseEqs()]
+    \\ gvs [perms_ok_def, store_assign_def]
+    \\ rw [EL_LUPDATE, perms_ok_ref_def])
+  \\ Cases_on ‘op = ThunkOp ForceThunk’ \\ gs[]
+  >- (rw [do_app_cases] \\ gvs [thunk_op_def, AllCaseEqs()])
   \\ Cases_on ‘op’ \\ gs []
+  \\ Cases_on ‘t’ \\ gs []
 QED
 
 Theorem perms_ok_do_opapp:
@@ -692,7 +712,78 @@ Proof
   >~ [‘Fun n e’] >- (
     gvs [evaluate_def, perms_ok_env_def, perms_ok_def, SF SFY_ss])
   >~ [‘App op xs’] >- (
-    gvs [evaluate_def]
+    Cases_on ‘getOpClass op = Force’ \\ gvs []
+    >- (
+      gvs [AllCaseEqs()] \\ gvs [evaluate_def] \\ gvs [AllCaseEqs()]
+      \\ gvs [perms_ok_env_BIGUNION, MEM_MAP, PULL_EXISTS, EVERY_MEM]
+      >- (
+        gvs [oneline dest_thunk_def, AllCaseEqs(), store_lookup_def,
+             perms_ok_state_def]
+        \\ last_x_assum drule \\ rw [] \\ gvs [perms_ok_def, perms_ok_ref_def])
+      \\ (
+        gvs [dec_clock_def]
+        \\ gvs [oneline dest_thunk_def, AllCaseEqs(), store_lookup_def]
+        \\ gvs [do_opapp_cases]
+        >- ((* Closure *)
+          last_x_assum mp_tac
+          \\ reverse impl_tac
+          >- (
+            rw [] \\ gs []
+            \\ gvs [oneline update_thunk_def, AllCaseEqs(), store_assign_def,
+                 perms_ok_state_def, EL_LUPDATE] \\ rw []
+            \\ gvs [perms_ok_ref_def]
+            \\ first_x_assum (drule_then assume_tac) \\ gs [])
+          \\ gvs [perms_ok_state_def]
+          \\ first_x_assum (drule_then assume_tac) \\ gvs []
+          \\ gvs [perms_ok_ref_def, perms_ok_def, perms_ok_env_def]
+          \\ Cases \\ simp [nsLookup_nsBind_compute]
+          \\ rw [] \\ gvs [perms_ok_def]
+          \\ first_x_assum irule
+          \\ first_x_assum (irule_at Any) \\ gvs [])
+        >- ((* Recclosure *)
+          last_x_assum mp_tac
+          \\ reverse impl_tac
+          >- (
+            rw [] \\ gs []
+            \\ gvs [oneline update_thunk_def, AllCaseEqs(), store_assign_def,
+                 perms_ok_state_def, EL_LUPDATE] \\ rw []
+            \\ gvs [perms_ok_ref_def]
+            \\ first_x_assum (drule_then assume_tac) \\ gs [])
+          \\ gvs [perms_ok_state_def]
+          \\ first_x_assum (drule_then assume_tac) \\ gvs []
+          \\ gvs [perms_ok_ref_def, perms_ok_def, perms_ok_env_def]
+          \\ gvs [SF DNF_ss, find_recfun_ALOOKUP, EVERY_MEM, MEM_MAP,
+                  PULL_EXISTS]
+          \\ drule_then assume_tac ALOOKUP_MEM
+          \\ qmatch_asmsub_abbrev_tac ‘MEM yyy funs’
+          \\ first_assum drule \\ simp_tac std_ss [Abbr ‘yyy’]
+          \\ strip_tac
+          \\ simp [build_rec_env_merge]
+          \\ Cases \\ simp [nsLookup_nsBind_compute]
+          \\ rw [] \\ gs [nsLookup_nsAppend_some, nsLookup_alist_to_ns_some,
+                          nsLookup_alist_to_ns_none]
+          >- gvs [perms_ok_def]
+          >~ [‘ALOOKUP _ _ = NONE’] >- (
+            first_x_assum irule
+            \\ first_assum (irule_at Any)
+            \\ gs [ALOOKUP_NONE, MAP_MAP_o, o_DEF, LAMBDA_PROD, MEM_MAP,
+                   EXISTS_PROD]
+            \\ first_assum (irule_at Any)
+            \\ first_assum (irule_at Any) \\ gs []
+            \\ strip_tac \\ gvs [])
+          >~ [‘ALOOKUP _ _ = SOME _’] >- (
+            drule_then assume_tac ALOOKUP_MEM
+            \\ gs [MEM_MAP, EXISTS_PROD, perms_ok_def, EVERY_MAP, EVERY_MEM]
+            \\ gs [perms_ok_env_def, MEM_MAP, EXISTS_PROD]
+            \\ rw [] \\ gs [FORALL_PROD, SF SFY_ss])
+          \\ first_x_assum irule
+          \\ first_assum (irule_at Any)
+          \\ gs [ALOOKUP_NONE, MAP_MAP_o, o_DEF, LAMBDA_PROD, MEM_MAP,
+                 EXISTS_PROD]
+          \\ first_assum (irule_at Any)
+          \\ first_assum (irule_at Any) \\ gs [])))
+    \\ gvs [AllCaseEqs()]
+    \\ gvs [evaluate_def]
     \\ Cases_on ‘op = Opapp’ \\ gs []
     >- ((* Opapp *)
       gvs [CaseEqs ["result", "prod", "bool", "option"],
@@ -754,6 +845,7 @@ Proof
     \\ Cases_on ‘getOpClass op’ \\ gs[]
     >~ [‘EvalOp’] >- (Cases_on ‘op’ \\ gs[])
     >~ [‘FunApp’] >- (Cases_on ‘op’ \\ gs[])
+    >~ [‘Force’] >- (Cases_on ‘op’ \\ gs[])
     >~ [‘Simple’] >- (
       gvs [CaseEqs ["result", "prod", "bool", "option"]]
       \\ drule_then (qspec_then ‘ps’ mp_tac) do_app_perms

candle/standard/syntax/holSyntaxScript.sml

@@ -271,7 +271,7 @@ QED
 Triviality LEAST_EXISTS:
   (∃n:num. P n) ⇒ ∃k. P k ∧ ∀m. m < k ⇒ ¬(P m)
 Proof
-  metis_tac[whileTheory.LEAST_EXISTS]
+  metis_tac[WhileTheory.LEAST_EXISTS]
 QED
 
 val VARIANT_PRIMES_def = new_specification

characteristic/cfAppScript.sml

@@ -613,7 +613,8 @@ Theorem do_app_io_events_ExtCall:
         ?s bs bs'. io_ev = IO_event (ExtCall s) bs bs'
 Proof
   strip_tac >>
-  gvs[DefnBase.one_line_ify NONE do_app_def,
+  gvs[oneline do_app_def,
+    oneline thunk_op_def, store_alloc_def,
     AllCaseEqs(),ffiTheory.call_FFI_def] >>
   pairarg_tac >> fs[]
 QED