diff --git a/basis/basis_ffi.c b/basis/basis_ffi.c
index 8251ebcaf1..644d1c1735 100644
--- a/basis/basis_ffi.c
+++ b/basis/basis_ffi.c
@@ -198,6 +198,8 @@ struct timeval t1,t2,lastT;
 long microsecs = 0;
 int numGC = 0;
 int hasT = 0;
+long prevOcc = 0;
+long numAllocBytes = 0;
 
 void cml_exit(int arg) {
 
@@ -216,6 +218,7 @@ void cml_exit(int arg) {
       fprintf(stderr,"CakeML stack space exhausted.\n");
     }
     fprintf(stderr,"GCNum: %d, GCTime(us): %ld\n",numGC,microsecs);
+    fprintf(stderr,"Total allocated heap data: %ld bytes\n",numAllocBytes);
   }
   #endif
 
@@ -240,11 +243,19 @@ void ffi (unsigned char *c, long clen, unsigned char *a, long alen) {
         microsecs += (t2.tv_usec - t1.tv_usec) + (t2.tv_sec - t1.tv_sec)*1e6;
         numGC++;
         inGC = 0;
+        long occ = (long)c; // number of bytes in occupied in heap (all live after standard GC)
+        // long len = (long)a;
+        // fprintf(stderr,"GC stops  %ld %ld \n",occ,len);
+        prevOcc = occ;
       }
       else
       {
         inGC = 1;
         gettimeofday(&t1, NULL);
+        long occ = (long)c;
+        // long len = (long)a;
+        // fprintf(stderr,"GC starts %ld %ld \n",occ,len);
+        numAllocBytes += (occ - prevOcc);
       }
     } else {
       int indent = 30;
diff --git a/compiler/backend/data_to_wordScript.sml b/compiler/backend/data_to_wordScript.sml
index 2ecd551c9f..7afbe4e2cb 100644
--- a/compiler/backend/data_to_wordScript.sml
+++ b/compiler/backend/data_to_wordScript.sml
@@ -269,7 +269,10 @@ val AppendFastLoop_location_eq = save_thm("AppendFastLoop_location_eq",
 val SilentFFI_def = Define `
   SilentFFI c n names =
     if c.call_empty_ffi then
-      Seq (Assign n (Const 0w)) (FFI "" n n n n names)
+      list_Seq [Assign n (Const 0w);
+                Assign 7 (Op Sub [Lookup NextFree; Lookup CurrHeap]);
+                Assign 9 (Lookup HeapLength);
+                FFI "" 7 n 9 n names]
     else Skip`;
 
 val AllocVar_def = Define `
diff --git a/compiler/backend/proofs/data_to_wordProofScript.sml b/compiler/backend/proofs/data_to_wordProofScript.sml
index 32ba069a7a..066b1beb8b 100644
--- a/compiler/backend/proofs/data_to_wordProofScript.sml
+++ b/compiler/backend/proofs/data_to_wordProofScript.sml
@@ -77,10 +77,10 @@ Theorem data_compile_correct:
          | SOME (Rerr (Rabort e)) => (res1 = SOME TimeOut) /\ t1.ffi = s1.ffi)
 Proof
   recInduct dataSemTheory.evaluate_ind \\ rpt strip_tac \\ full_simp_tac(srw_ss())[]
-  THEN1 (* Skip *)
+  >~ [‘evaluate (Skip,s)’] >-
    (full_simp_tac(srw_ss())[comp_def,dataSemTheory.evaluate_def,wordSemTheory.evaluate_def]
     \\ srw_tac[][] \\ fs [state_rel_def])
-  THEN1 (* Move *)
+  >~ [‘evaluate (Move dest src,s)’] >-
    (full_simp_tac(srw_ss())[comp_def,dataSemTheory.evaluate_def,wordSemTheory.evaluate_def]
     \\ Cases_on `get_var src s.locals` \\ full_simp_tac(srw_ss())[] \\ srw_tac[][]
     \\ full_simp_tac(srw_ss())[] \\ imp_res_tac state_rel_get_var_IMP \\ full_simp_tac(srw_ss())[]
@@ -92,7 +92,7 @@ Proof
     \\ full_simp_tac bool_ss [GSYM APPEND_ASSOC]
     \\ imp_res_tac word_ml_inv_get_var_IMP
     \\ match_mp_tac word_ml_inv_insert \\ full_simp_tac(srw_ss())[])
-  THEN1 (* Assign *)
+  >~ [‘evaluate (Assign _ _ _ _,s)’] >-
    (full_simp_tac(srw_ss())[comp_def,dataSemTheory.evaluate_def,wordSemTheory.evaluate_def]
     \\ imp_res_tac (METIS_PROVE [] ``(if b1 /\ b2 then x1 else x2) = y ==>
                                      b1 /\ b2 /\ x1 = y \/
@@ -121,7 +121,7 @@ Proof
     \\ Cases_on `names_opt` \\ full_simp_tac(srw_ss())[cut_state_opt_def] \\ srw_tac[][] \\ full_simp_tac(srw_ss())[]
     \\ full_simp_tac(srw_ss())[cut_state_def,cut_env_def] \\ every_case_tac
     \\ fs [] \\ rw [] \\ fs [set_var_def])
-  THEN1 (* Tick *)
+  >~ [‘evaluate (Tick,s)’] >-
    (full_simp_tac(srw_ss())[comp_def,dataSemTheory.evaluate_def,wordSemTheory.evaluate_def]
     \\ `t.clock = s.clock` by full_simp_tac(srw_ss())[state_rel_def] \\ full_simp_tac(srw_ss())[] \\ srw_tac[][]
     \\ full_simp_tac(srw_ss())[] \\ srw_tac[][] \\ rpt (pop_assum mp_tac)
@@ -129,12 +129,14 @@ Proof
     \\ full_simp_tac(srw_ss())[state_rel_def,dataSemTheory.dec_clock_def,wordSemTheory.dec_clock_def]
     \\ full_simp_tac(srw_ss())[call_env_def,wordSemTheory.call_env_def,wordSemTheory.flush_state_def,flush_state_def]
     \\ asm_exists_tac \\ fs [])
-  THEN1 (* MakeSpace *)
+  >~ [‘evaluate (MakeSpace k names,s)’] >-
    (full_simp_tac(srw_ss())[comp_def,dataSemTheory.evaluate_def,
         wordSemTheory.evaluate_def,
         GSYM alloc_size_def,LET_DEF,wordSemTheory.word_exp_def,
         wordLangTheory.word_op_def,wordSemTheory.get_var_imm_def]
-    \\ `?end next.
+    \\ `?end next hlen curr.
+          FLOOKUP t.store CurrHeap = SOME (Word curr) /\
+          FLOOKUP t.store HeapLength = SOME (Word hlen) /\
           FLOOKUP t.store TriggerGC = SOME (Word end) /\
           FLOOKUP t.store NextFree = SOME (Word next)` by
             full_simp_tac(srw_ss())[state_rel_def,heap_in_memory_store_def]
@@ -164,9 +166,9 @@ Proof
       \\ qpat_x_assum `state_rel c l1 l2 _ _ _ _` mp_tac \\ simp [state_rel_def])
     \\ fs [SilentFFI_def,wordSemTheory.evaluate_def,list_Seq_def,eq_eval]
     \\ fs [wordSemTheory.evaluate_def,SilentFFI_def,wordSemTheory.word_exp_def,
-           wordSemTheory.set_var_def,EVAL ``read_bytearray 0w 0 m``,
+           wordSemTheory.set_var_def,EVAL ``read_bytearray a 0 m``,
            ffiTheory.call_FFI_def,EVAL ``write_bytearray a [] m dm b``,
-           wordSemTheory.get_var_def,lookup_insert]
+           wordSemTheory.get_var_def,lookup_insert,cut_env_adjust_set_insert_ODD]
     \\ fs [cut_env_adjust_set_insert_1,cut_env_adjust_set_insert_3]
     \\ drule cut_env_IMP_cut_env
     \\ Cases_on `dataSem$cut_env names s.locals` \\ fs []
@@ -178,16 +180,29 @@ Proof
     \\ drule alloc_lemma \\ fs [] \\ rveq
     \\ `dataSem$cut_env names x = SOME x` by
       (fs [dataSemTheory.cut_env_def] \\ rveq \\ fs [lookup_inter_alt,domain_inter])
-    \\ rpt (disch_then drule)
+    \\ disch_then drule
     \\ qmatch_assum_abbrev_tac `alloc _ _ t5 = _`
     \\ `t5 = t with locals := insert 1 (Word (alloc_size k)) y` by
           (unabbrev_all_tac \\ fs [wordSemTheory.state_component_equality])
     \\ fs [] \\ disch_then drule
-    \\ strip_tac \\ Cases_on `res' = SOME NotEnoughSpace` \\ fs []
+    \\ strip_tac \\ Cases_on `res' = SOME NotEnoughSpace`
+    >- (fs []
+        \\ rveq \\ rfs [add_space_def,cut_locals_def] \\ fs [GSYM NOT_LESS]
+        \\ imp_res_tac alloc_NONE_IMP_cut_env \\ fs []
+        \\ fs [add_space_def] \\ fs [state_rel_thm] \\ rfs [] \\ fs [])
+    \\ `?end next hlen curr.
+          FLOOKUP s1'.store CurrHeap = SOME (Word curr) /\
+          FLOOKUP s1'.store HeapLength = SOME (Word hlen) /\
+          FLOOKUP s1'.store TriggerGC = SOME (Word end) /\
+          FLOOKUP s1'.store NextFree = SOME (Word next)` by
+            full_simp_tac(srw_ss())[state_rel_def,heap_in_memory_store_def]
+    \\ rfs [lookup_insert,cut_env_adjust_set_insert_ODD,
+            EVAL ``read_bytearray a 0 m``]
     \\ rveq \\ rfs [add_space_def,cut_locals_def] \\ fs [GSYM NOT_LESS]
     \\ imp_res_tac alloc_NONE_IMP_cut_env \\ fs []
-    \\ fs [add_space_def] \\ fs [state_rel_thm] \\ rfs [] \\ fs [])
-  THEN1 (* Raise *)
+    \\ fs [add_space_def] \\ fs [state_rel_thm] \\ rfs [] \\ fs []
+    \\ fs [wordSemTheory.write_bytearray_def])
+  >~ [‘evaluate (Raise _,s)’] >-
    (full_simp_tac(srw_ss())[comp_def,dataSemTheory.evaluate_def,wordSemTheory.evaluate_def]
     \\ Cases_on `get_var n s.locals` \\ full_simp_tac(srw_ss())[] \\ srw_tac[][]
     \\ full_simp_tac(srw_ss())[] \\ imp_res_tac state_rel_get_var_IMP \\ full_simp_tac(srw_ss())[]
@@ -196,7 +211,7 @@ Proof
     \\ srw_tac[][] \\ full_simp_tac(srw_ss())[] \\ srw_tac[][mk_loc_def]
     \\ first_x_assum (qspec_then `0` mp_tac) \\ fs [state_rel_def]
     \\ fs [set_var_def])
-  THEN1 (* Return *)
+  >~ [‘evaluate (Return _,s)’] >-
    (full_simp_tac(srw_ss())[comp_def,dataSemTheory.evaluate_def,wordSemTheory.evaluate_def]
     \\ Cases_on `get_var n s.locals` \\ full_simp_tac(srw_ss())[] \\ srw_tac[][]
     \\ `get_var 0 t = SOME (Loc l1 l2)` by
@@ -219,7 +234,7 @@ Proof
     \\ rpt_drule word_ml_inv_get_var_IMP
     \\ match_mp_tac word_ml_inv_rearrange
     \\ full_simp_tac(srw_ss())[] \\ srw_tac[][] \\ fs[EVAL ``join_env LN []``])
-  THEN1 (* Seq *)
+  >~ [‘evaluate (Seq _ _,s)’] >-
    (once_rewrite_tac [data_to_wordTheory.comp_def] \\ full_simp_tac(srw_ss())[]
     \\ Cases_on `comp c n l c1` \\ full_simp_tac(srw_ss())[LET_DEF]
     \\ Cases_on `comp c n r c2` \\ full_simp_tac(srw_ss())[LET_DEF]
@@ -257,7 +272,7 @@ Proof
     \\ imp_res_tac evaluate_mk_loc_EQ \\ full_simp_tac(srw_ss())[]
     \\ imp_res_tac eval_NONE_IMP_jump_exc_NONE_EQ
     \\ full_simp_tac(srw_ss())[jump_exc_inc_clock_EQ_NONE] \\ metis_tac [])
-  THEN1 (* If *)
+  >~ [‘evaluate (If _ _ _,s)’] >-
    (once_rewrite_tac [data_to_wordTheory.comp_def] \\ full_simp_tac(srw_ss())[]
     \\ fs [LET_DEF]
     \\ pairarg_tac \\ fs [] \\ rename1 `comp c n4 l c1 = (q4,l4)`
@@ -279,7 +294,7 @@ Proof
                first_x_assum (fn th1 => mp_tac (MATCH_MP th1 th)))
       \\ strip_tac \\ pop_assum (qspecl_then [`n4`,`l4`] mp_tac)
       \\ rpt strip_tac \\ rev_full_simp_tac(srw_ss())[]))
-  (* Call *)
+  \\ rename [‘evaluate (Call ret dest args handler,s)’]
   \\ `t.clock = s.clock` by fs [state_rel_def]
   \\ once_rewrite_tac [data_to_wordTheory.comp_def] \\ full_simp_tac(srw_ss())[]
   \\ Cases_on `ret`
diff --git a/compiler/backend/proofs/data_to_word_assignProofScript.sml b/compiler/backend/proofs/data_to_word_assignProofScript.sml
index ca75b14389..238e7bd85c 100644
--- a/compiler/backend/proofs/data_to_word_assignProofScript.sml
+++ b/compiler/backend/proofs/data_to_word_assignProofScript.sml
@@ -4524,10 +4524,17 @@ Proof
     \\ match_mp_tac memory_rel_insert
     \\ fs [] \\ match_mp_tac memory_rel_Unit \\ fs [])
   \\ fs [SilentFFI_def,wordSemTheory.evaluate_def,eq_eval]
+  \\ ‘∃nf cu hl.
+        FLOOKUP t.store NextFree = SOME (Word nf) ∧
+        FLOOKUP t.store CurrHeap = SOME (Word cu) ∧
+        FLOOKUP t.store HeapLength = SOME (Word hl)’ by
+           fs [state_rel_thm,memory_rel_def,heap_in_memory_store_def]
   \\ fs [wordSemTheory.evaluate_def,SilentFFI_def,wordSemTheory.word_exp_def,
-         wordSemTheory.set_var_def,EVAL ``read_bytearray 0w 0 m``,
+         wordSemTheory.set_var_def,EVAL ``read_bytearray a 0 m``,
          ffiTheory.call_FFI_def,EVAL ``write_bytearray a [] m dm b``,
-         wordSemTheory.get_var_def,lookup_insert]
+         wordSemTheory.get_var_def,lookup_insert,list_Seq_def,
+         wordSemTheory.the_words_def,wordLangTheory.word_op_def,
+         cut_env_adjust_set_insert_ODD]
   \\ Cases_on `names_opt`
   \\ fs [cut_state_opt_def,cut_state_def,case_eq_thms] \\ rveq \\ fs []
   \\ fs [get_names_def]
@@ -4556,6 +4563,17 @@ Proof
   >- (rw[option_le_max_right] >> res_tac >>
       simp[space_consumed_def] >> rfs[cut_locals_def] >>
       simp[NOT_LESS_EQUAL])
+  \\ ‘∃nf cu hl.
+        FLOOKUP x2.store NextFree = SOME (Word nf) ∧
+        FLOOKUP x2.store CurrHeap = SOME (Word cu) ∧
+        FLOOKUP x2.store HeapLength = SOME (Word hl)’ by
+           fs [state_rel_thm,memory_rel_def,heap_in_memory_store_def]
+  \\ fs [wordSemTheory.evaluate_def,SilentFFI_def,wordSemTheory.word_exp_def,
+         wordSemTheory.set_var_def,EVAL ``read_bytearray a 0 m``,
+         ffiTheory.call_FFI_def,EVAL ``write_bytearray a [] m dm b``,
+         wordSemTheory.get_var_def,lookup_insert,list_Seq_def,
+         wordSemTheory.the_words_def,wordLangTheory.word_op_def,
+         cut_env_adjust_set_insert_ODD]
   \\ rveq \\ fs []
   \\ imp_res_tac alloc_NONE_IMP_cut_env \\ fs []
   \\ fs [state_rel_thm,set_var_def]
@@ -12195,20 +12213,6 @@ Proof
   Induct \\ fs [wordSemTheory.get_vars_def,wordSemTheory.get_var_def,eq_eval]
 QED
 
-Theorem cut_env_adjust_set_insert_ODD:
-   ODD n ==> cut_env (adjust_set the_names) (insert n w s) =
-              cut_env (adjust_set the_names) s
-Proof
-  reverse (rw [wordSemTheory.cut_env_def] \\ fs [SUBSET_DEF])
-  \\ res_tac \\ fs []
-  THEN1 (rveq \\ fs [domain_lookup,lookup_adjust_set]
-         \\ every_case_tac \\ fs [])
-  \\ fs [lookup_inter_alt,lookup_insert]
-  \\ rw [] \\ pop_assum mp_tac
-  \\ simp [domain_lookup,lookup_adjust_set]
-  \\ rw [] \\ fs []
-QED
-
 Theorem INTRO_IS_SOME:
    (?v. x = SOME v) <=> IS_SOME x
 Proof
diff --git a/compiler/backend/proofs/data_to_word_gcProofScript.sml b/compiler/backend/proofs/data_to_word_gcProofScript.sml
index a2b498148b..59f6b14618 100644
--- a/compiler/backend/proofs/data_to_word_gcProofScript.sml
+++ b/compiler/backend/proofs/data_to_word_gcProofScript.sml
@@ -7558,6 +7558,62 @@ Proof
   \\ pairarg_tac \\ fs [EVEN_adjust_var]
 QED
 
+Theorem cut_env_adjust_set_insert_ODD:
+   ODD n ==> cut_env (adjust_set the_names) (insert n w s) =
+              cut_env (adjust_set the_names) s
+Proof
+  reverse (rw [wordSemTheory.cut_env_def] \\ fs [SUBSET_DEF])
+  \\ res_tac \\ fs []
+  THEN1 (rveq \\ fs [domain_lookup,lookup_adjust_set]
+         \\ every_case_tac \\ fs [])
+  \\ fs [lookup_inter_alt,lookup_insert]
+  \\ rw [] \\ pop_assum mp_tac
+  \\ simp [domain_lookup,lookup_adjust_set]
+  \\ rw [] \\ fs []
+QED
+
+Theorem cut_env_insert_1_insert_1:
+  wordSem$cut_env (insert 1 () (adjust_set names)) (insert 1 w t) =
+  case wordSem$cut_env (adjust_set names) (t:'a num_map) of
+  | NONE => NONE
+  | SOME e => SOME $ insert 1 w e
+Proof
+  fs [wordSemTheory.cut_env_def]
+  \\ ‘∀t. domain (adjust_set names) ⊆ 1 INSERT domain (t:'a num_map) ⇔
+          domain (adjust_set names) ⊆ domain t’ by
+    (rw [] \\ eq_tac \\ rw [SUBSET_DEF]
+     \\ res_tac \\ gvs [] \\ fs [domain_lookup,lookup_adjust_set])
+  \\ fs [] \\ IF_CASES_TAC \\ fs []
+  \\ gvs [inter_insert]
+  \\ gvs [spt_eq_thm,wf_insert,lookup_insert]
+  \\ rw [] \\ fs [lookup_inter_alt]
+QED
+
+Theorem alloc_store:
+  alloc k names t = (NONE,s1) ∧
+  t.gc_fun = word_gc_fun c ∧
+  FLOOKUP t.store CurrHeap = SOME (Word cu) ∧
+  FLOOKUP t.store TriggerGC = SOME (Word end) ∧
+  FLOOKUP t.store NextFree = SOME (Word next) ∧
+  FLOOKUP t.store HeapLength = SOME (Word heap_length1) ⇒
+  ∃end next heap_length1 cu.
+    FLOOKUP s1.store CurrHeap = SOME (Word cu) ∧
+    FLOOKUP s1.store TriggerGC = SOME (Word end) ∧
+    FLOOKUP s1.store NextFree = SOME (Word next) ∧
+    FLOOKUP s1.store HeapLength = SOME (Word heap_length1)
+Proof
+  gvs [wordSemTheory.alloc_def,AllCaseEqs(),wordSemTheory.gc_def]
+  \\ rw [] \\ gvs []
+  \\ fs [wordSemTheory.set_store_def,wordSemTheory.enc_stack_def,
+         wordSemTheory.push_env_def,wordSemTheory.pop_env_def,AllCaseEqs()]
+  \\ rpt (pairarg_tac \\ gvs [])
+  \\ fs [word_gc_fun_def,AllCaseEqs()]
+  \\ Cases_on ‘c.gc_kind’ \\ fs []
+  \\ gvs [FUPDATE_LIST,FAPPLY_FUPDATE_THM,FLOOKUP_DEF,word_full_gc_def]
+  \\ rpt (pairarg_tac \\ gvs [])
+  \\ gvs [FUPDATE_LIST,FAPPLY_FUPDATE_THM,FLOOKUP_DEF,word_full_gc_def]
+QED
+
 Theorem AllocVar_thm:
    state_rel c l1 l2 s (t:('a,'c,'ffi) wordSem$state) [] locs ∧
     dataSem$cut_env names s.locals = SOME x ∧
@@ -7580,9 +7636,11 @@ Proof
   fs [wordSemTheory.evaluate_def,AllocVar_def,list_Seq_def] \\ strip_tac
   \\ `limit < dimword (:'a)` by
         (rfs [EVAL ``good_dimindex (:'a)``,state_rel_def,dimword_def] \\ rfs [])
-  \\ `?end next.
+  \\ `?end next heap_length1 cu.
+        FLOOKUP t.store CurrHeap = SOME (Word cu) /\
         FLOOKUP t.store TriggerGC = SOME (Word end) /\
-        FLOOKUP t.store NextFree = SOME (Word next)` by
+        FLOOKUP t.store NextFree = SOME (Word next) /\
+        FLOOKUP t.store HeapLength = SOME (Word heap_length1)` by
           full_simp_tac(srw_ss())[state_rel_def,heap_in_memory_store_def]
   \\ fs [word_exp_rw,get_var_set_var_thm] \\ rfs []
   \\ rfs [wordSemTheory.get_var_def]
@@ -7616,23 +7674,17 @@ Proof
       \\ Cases_on `alloc (-1w) p2 p3` \\ fs [bool_case_eq])
     \\ fs [Once SilentFFI_def,wordSemTheory.evaluate_def]
     \\ fs [wordSemTheory.evaluate_def,SilentFFI_def,wordSemTheory.word_exp_def,
-           wordSemTheory.set_var_def,EVAL ``read_bytearray 0w 0 m``,
+           wordSemTheory.set_var_def,EVAL ``read_bytearray a 0 m``,
            ffiTheory.call_FFI_def,EVAL ``write_bytearray a [] m dm b``,
-           wordSemTheory.get_var_def,lookup_insert]
-    \\ fs [Q.SPECL [`3`,`3`] insert_insert |> SIMP_RULE std_ss []]
-    \\ fs [Q.SPECL [`3`,`1`] insert_insert |> SIMP_RULE std_ss []]
+           wordSemTheory.get_var_def,lookup_insert,list_Seq_def,
+           wordSemTheory.the_words_def,wordLangTheory.word_op_def,
+           cut_env_adjust_set_insert_ODD]
+    \\ fs [Q.SPECL [`3`,`1`] insert_insert |> SIMP_RULE std_ss [],
+           Q.SPECL [`7`,`1`] insert_insert |> SIMP_RULE std_ss [],
+           Q.SPECL [`9`,`1`] insert_insert |> SIMP_RULE std_ss []]
+    \\ fs [cut_env_insert_1_insert_1,cut_env_adjust_set_insert_ODD]
     \\ drule (GEN_ALL cut_env_IMP_cut_env)
     \\ disch_then drule \\ strip_tac \\ fs []
-    \\ `wordSem$cut_env (insert 1 () (adjust_set names))
-             (insert 1 (Word (-1w)) (insert 3 (Word 0w) t.locals)) =
-          SOME (insert 1 (Word (-1w)) y)` by
-     (fs [wordSemTheory.cut_env_def] \\ rveq \\ fs []
-      \\ conj_tac THEN1 (fs [SUBSET_DEF])
-      \\ fs [spt_eq_thm,wf_insert]
-      \\ simp [lookup_inter_alt,lookup_insert]
-      \\ strip_tac \\ Cases_on `n=1` \\ fs []
-      \\ Cases_on `n=3` \\ fs []
-      \\ rw [] \\ drule domain_adjust_set_EVEN \\ EVAL_TAC)
     \\ fs [] \\ pairarg_tac \\ fs []
     \\ drule (GEN_ALL state_rel_cut_env)
     \\ disch_then drule \\ strip_tac
@@ -7659,6 +7711,14 @@ Proof
     \\ fs [cut_env_adjust_set_insert_3]
     \\ drule alloc_NONE_IMP_cut_env
     \\ strip_tac \\ fs [] \\ rveq \\ fs []
+    \\ ‘t.gc_fun = word_gc_fun c’ by fs [state_rel_def]
+    \\ drule (GEN_ALL alloc_store) \\ fs []
+    \\ disch_then $ qspec_then ‘c’ strip_assume_tac
+    \\ gvs [lookup_insert]
+    \\ gvs [cut_env_adjust_set_insert_ODD]
+    \\ fs [cut_env_adjust_set_insert_3]
+    \\ gvs [wordSemTheory.set_var_def,EVAL ``read_bytearray a 0 m``,
+            ffiTheory.call_FFI_def,EVAL ``write_bytearray a [] m dm b``]
     \\ qmatch_asmsub_abbrev_tac `alloc _ _ t5 = _`
     \\ `t5 = t with locals := insert 1 (Word (-1w)) y` by
         (unabbrev_all_tac
@@ -7706,24 +7766,16 @@ Proof
     \\ rw[] \\ fs [])
   \\ fs [SilentFFI_def,wordSemTheory.evaluate_def,lookup_insert]
   \\ fs [wordSemTheory.evaluate_def,SilentFFI_def,wordSemTheory.word_exp_def,
-         wordSemTheory.set_var_def,EVAL ``read_bytearray 0w 0 m``,
+         wordSemTheory.set_var_def,EVAL ``read_bytearray a 0 m``,
          ffiTheory.call_FFI_def,EVAL ``write_bytearray a [] m dm b``,
-         wordSemTheory.get_var_def,lookup_insert]
-  \\ fs [Q.SPECL [`3`,`3`] insert_insert |> SIMP_RULE std_ss []]
-  \\ fs [Q.SPECL [`3`,`1`] insert_insert |> SIMP_RULE std_ss []]
+         wordSemTheory.get_var_def,lookup_insert,list_Seq_def,
+         wordSemTheory.the_words_def,wordLangTheory.word_op_def]
+  \\ fs [Q.SPECL [`3`,`1`] insert_insert |> SIMP_RULE std_ss [],
+         Q.SPECL [`7`,`1`] insert_insert |> SIMP_RULE std_ss [],
+         Q.SPECL [`9`,`1`] insert_insert |> SIMP_RULE std_ss []]
+  \\ fs [cut_env_insert_1_insert_1,cut_env_adjust_set_insert_ODD]
   \\ drule (GEN_ALL cut_env_IMP_cut_env)
   \\ disch_then drule \\ strip_tac \\ fs []
-  \\ `wordSem$cut_env (insert 1 () (adjust_set names))
-             (insert 1 (Word (alloc_size (w2n w DIV 4 + 1)))
-                (insert 3 (Word 0w) t.locals)) =
-        SOME (insert 1 (Word (alloc_size (w2n w DIV 4 + 1))) y)` by
-   (fs [wordSemTheory.cut_env_def] \\ rveq \\ fs []
-    \\ conj_tac THEN1 (fs [SUBSET_DEF])
-    \\ fs [spt_eq_thm,wf_insert]
-    \\ simp [lookup_inter_alt,lookup_insert]
-    \\ strip_tac \\ Cases_on `n=1` \\ fs []
-    \\ Cases_on `n=3` \\ fs []
-    \\ rw [] \\ drule domain_adjust_set_EVEN \\ EVAL_TAC)
   \\ fs [cut_locals_def]
   \\ match_mp_tac (alloc_alt |> SPEC_ALL
         |> Q.INST [`s`|->`s with locals := z`]
@@ -7749,9 +7801,18 @@ Proof
    (pop_assum (fn th => rewrite_tac [GSYM th])
     \\ AP_TERM_TAC
     \\ fs [wordSemTheory.state_component_equality])
+  \\ drule (GEN_ALL alloc_store) \\ fs []
+  \\ disch_then $ qspec_then ‘c’ strip_assume_tac
+  \\ ‘t.gc_fun = word_gc_fun c’ by fs [state_rel_def]
+  \\ gvs [lookup_insert]
+  \\ gvs [cut_env_adjust_set_insert_ODD]
   \\ fs [cut_env_adjust_set_insert_3]
   \\ drule alloc_NONE_IMP_cut_env
   \\ strip_tac \\ fs [] \\ rveq \\ fs []
+  \\ gvs [wordSemTheory.set_var_def,EVAL ``read_bytearray a 0 m``,
+          ffiTheory.call_FFI_def,EVAL ``write_bytearray a [] m dm b``]
+  \\ drule alloc_NONE_IMP_cut_env
+  \\ strip_tac \\ fs [] \\ rveq \\ fs []
   \\ qmatch_asmsub_abbrev_tac `alloc _ _ t5 = _`
   \\ `t5 = t with locals := insert 1 (Word (alloc_size (w2n w DIV 4 + 1))) y` by
       (unabbrev_all_tac