From c01c24ba8b4d7b97ea18e9ef42b7487b128cbf12 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Thu, 15 Oct 2020 14:14:15 +0200
Subject: [PATCH 01/15] Initial work towards #796

---
 compiler/backend/stackLangScript.sml | 1 +
 compiler/backend/wordLangScript.sml  | 1 +
 2 files changed, 2 insertions(+)

diff --git a/compiler/backend/stackLangScript.sml b/compiler/backend/stackLangScript.sml
index 007f0fd3d0..083388f93c 100644
--- a/compiler/backend/stackLangScript.sml
+++ b/compiler/backend/stackLangScript.sml
@@ -26,6 +26,7 @@ val _ = Datatype `
        | Inst ('a inst)
        | Get num store_name
        | Set store_name num
+       | GetOp binop num num store_name
        | Call ((stackLang$prog # num # num # num) option)
               (* return-handler code, link reg, labels l1,l2*)
               (num + num) (* target of call *)
diff --git a/compiler/backend/wordLangScript.sml b/compiler/backend/wordLangScript.sml
index f4aace5feb..2f13ee2522 100644
--- a/compiler/backend/wordLangScript.sml
+++ b/compiler/backend/wordLangScript.sml
@@ -15,6 +15,7 @@ val _ = Datatype `
       | Lookup store_name
       | Load exp
       | Op binop (exp list)
+      | OpLookup binop exp store_name
       | Shift shift exp num`
 
 Theorem MEM_IMP_exp_size:

From 6898ff227b9e37692bb7db979d99cee06d0ba1c9 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Thu, 15 Oct 2020 14:23:47 +0200
Subject: [PATCH 02/15] Update data_to_word impl. for #796

---
 compiler/backend/data_to_wordScript.sml | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

diff --git a/compiler/backend/data_to_wordScript.sml b/compiler/backend/data_to_wordScript.sml
index bc0169de70..ecde3f3ec0 100644
--- a/compiler/backend/data_to_wordScript.sml
+++ b/compiler/backend/data_to_wordScript.sml
@@ -111,12 +111,11 @@ val real_addr_def = Define `
   (real_addr (conf:data_to_word$config) r): 'a wordLang$exp =
     let k = shift (:'a) in
       if k <= conf.pad_bits + 1 then
-        Op Add [Lookup CurrHeap;
-                Shift Lsr (Var r) (shift_length conf - k)]
+        OpLookup Add
+          (Shift Lsr (Var r) (shift_length conf - k)) CurrHeap
       else
-        Op Add [Lookup CurrHeap;
-                Shift Lsl (Shift Lsr (Var r)
-                  (shift_length conf)) k]`
+        OpLookup Add
+          (Shift Lsl (Shift Lsr (Var r) (shift_length conf)) k) CurrHeap`
 
 val real_offset_def = Define `
   (real_offset (conf:data_to_word$config) r): 'a wordLang$exp =
@@ -331,7 +330,7 @@ val RefByte_code_def = Define `
                              Shift Lsl (Var 5) (shift (:'a))]);
            Set NextFree (Op Add [Var 1; Const bytes_in_word]);
            (* 3 := return value *)
-           Assign 3 (Op Or [Shift Lsl (Op Sub [Var 9; Lookup CurrHeap])
+           Assign 3 (Op Or [Shift Lsl (OpLookup Sub (Var 9) CurrHeap)
                (shift_length c − shift (:'a)); Const (1w:'a word)]);
            (* compute header *)
            Assign 5 (Op Or [Op Or [y; Const 7w]; Var 6]);
@@ -361,7 +360,7 @@ val Maxout_bits_code_def = Define `
 val Make_ptr_bits_code_def = Define `
   Make_ptr_bits_code c tag len dest =
     list_Seq [Assign dest (Op Or
-       [Const 1w; Shift Lsl (Op Sub [Lookup NextFree; Lookup CurrHeap])
+       [Const 1w; Shift Lsl (OpLookup Sub (Lookup NextFree) CurrHeap)
            (shift_length c − shift (:'a))]);
         Maxout_bits_code c.tag_bits (1 + c.len_bits) dest tag;
         Maxout_bits_code c.len_bits 1 dest len] :'a wordLang$prog`
@@ -415,7 +414,7 @@ val RefArray_code_def = Define `
            Assign 1 (Op Sub [Lookup EndOfHeap; Var 1]);
            Set EndOfHeap (Var 1);
            (* 3 := return value *)
-           Assign 3 (Op Or [Shift Lsl (Op Sub [Var 1; Lookup CurrHeap])
+           Assign 3 (Op Or [Shift Lsl (OpLookup Sub (Var 1) CurrHeap)
                (shift_length c − shift (:'a)); Const (1w:'a word)]);
            (* compute header *)
            Assign 5 (Op Or [Shift Lsl (Var 2)
@@ -542,7 +541,7 @@ val AnyArith_code_def = Define `
                        ShiftVar Lsl 6 (dimindex (:'a) − c.len_size);
                        ShiftVar Lsl 8 4]);
       Store (Var 5) 7;
-      Assign 1 (Op Sub [Var 5; Lookup CurrHeap]);
+      Assign 1 (OpLookup Sub (Var 5) CurrHeap);
       Assign 1 (Op Or [ShiftVar Lsl 1 (shift_length c − shift (:'a)); Const 1w]);
       Set NextFree (Op Add [Var 5; Const bytes_in_word;
                             ShiftVar Lsl 6 (shift (:'a))]);
@@ -1094,7 +1093,7 @@ val def = assign_Define `
                          Assign 3 (Const header);
                          StoreEach 1 (3::MAP adjust_var args) 0w;
                          Assign (adjust_var dest)
-                           (Op Or [Shift Lsl (Op Sub [Var 1; Lookup CurrHeap])
+                           (Op Or [Shift Lsl (OpLookup Sub (Var 1) CurrHeap)
                                      (shift_length c − shift (:'a));
                                    Const (1w ||
                                            (small_shift_length c − 1 -- 0)
@@ -1164,7 +1163,7 @@ val def = assign_Define `
                   Assign 3 (Const header);
                   StoreEach 1 (3::MAP adjust_var args) 0w;
                   Assign (adjust_var dest)
-                    (Op Or [Shift Lsl (Op Sub [Var 1; Lookup CurrHeap])
+                    (Op Or [Shift Lsl (OpLookup Sub (Var 1) CurrHeap)
                               (shift_length c − shift (:'a));
                             Const 1w])],l))
       : 'a wordLang$prog # num`;

From d69f27e94dea70f5e310a13d7dfa9d1666c6761e Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Thu, 15 Oct 2020 22:19:10 +0200
Subject: [PATCH 03/15] Update backend/semantics for #796

---
 compiler/backend/semantics/stackSemScript.sml | 15 ++++++++----
 .../backend/semantics/wordPropsScript.sml     | 10 ++++----
 compiler/backend/semantics/wordSemScript.sml  | 23 +++++++++++++++----
 compiler/backend/wordLangScript.sml           |  1 +
 4 files changed, 36 insertions(+), 13 deletions(-)

diff --git a/compiler/backend/semantics/stackSemScript.sml b/compiler/backend/semantics/stackSemScript.sml
index 10703c4537..9c57c8f65c 100644
--- a/compiler/backend/semantics/stackSemScript.sml
+++ b/compiler/backend/semantics/stackSemScript.sml
@@ -126,6 +126,8 @@ val word_exp_def = tDefine "word_exp" `
      case FLOOKUP s.store name of
      | SOME (Word w) => SOME w
      | _ => NONE) /\
+  (word_exp s (OpLookup op x name) =
+     word_exp s (Op op [x; Lookup name])) /\
   (word_exp s (Load addr) =
      case word_exp s addr of
      | SOME w => (case mem_load w s of
@@ -139,10 +141,10 @@ val word_exp_def = tDefine "word_exp" `
      case word_exp s wexp of
      | NONE => NONE
      | SOME w => word_sh sh w n)`
-  (WF_REL_TAC `measure (exp_size ARB o SND)`
-   \\ REPEAT STRIP_TAC \\ IMP_RES_TAC wordLangTheory.MEM_IMP_exp_size
-   \\ TRY (FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `ARB`))
-   \\ DECIDE_TAC)
+  (WF_REL_TAC `measure (word_exp_size o SND)`
+   \\ fs [wordSemTheory.word_exp_size_def]
+   \\ Induct \\ fs [] \\ rw []
+   \\ fs [] \\ res_tac \\ fs []);
 
 val get_var_def = Define `
   get_var v (s:('a,'c,'ffi) stackSem$state) = FLOOKUP s.regs v`;
@@ -545,6 +547,11 @@ val evaluate_def = tDefine "evaluate" `
      case get_var v s of
      | SOME w => (NONE, set_store name w s)
      | NONE => (SOME Error, s)) /\
+  (evaluate (GetOp binop v src name,s) =
+     if ¬s.use_store then (SOME Error,s) else
+     case word_exp s (OpLookup binop (Var src) name) of
+     | SOME w => (NONE, set_var v (Word w) s)
+     | _ => (SOME Error, s)) /\
   (evaluate (Tick,s) =
      if s.clock = 0 then (SOME TimeOut,empty_env s)
                     else (NONE,dec_clock s)) /\
diff --git a/compiler/backend/semantics/wordPropsScript.sml b/compiler/backend/semantics/wordPropsScript.sml
index 33cac47243..0a5f76903b 100644
--- a/compiler/backend/semantics/wordPropsScript.sml
+++ b/compiler/backend/semantics/wordPropsScript.sml
@@ -2477,11 +2477,11 @@ Proof
 QED
 
 Theorem locals_rel_word_exp:
-    ∀s exp w.
-  every_var_exp (λx. x < temp) exp ∧
-  word_exp s exp = SOME w ∧
-  locals_rel temp s.locals loc ⇒
-  word_exp (s with locals:=loc) exp = SOME w
+  ∀s exp w.
+    every_var_exp (λx. x < temp) exp ∧
+    word_exp s exp = SOME w ∧
+    locals_rel temp s.locals loc ⇒
+    word_exp (s with locals:=loc) exp = SOME w
 Proof
   ho_match_mp_tac word_exp_ind>>srw_tac[][]>>
   full_simp_tac(srw_ss())[word_exp_def,every_var_exp_def,locals_rel_def]
diff --git a/compiler/backend/semantics/wordSemScript.sml b/compiler/backend/semantics/wordSemScript.sml
index 3eb836bd62..8c0255949c 100644
--- a/compiler/backend/semantics/wordSemScript.sml
+++ b/compiler/backend/semantics/wordSemScript.sml
@@ -175,10 +175,25 @@ val the_words_def = Define `
      | SOME (Word x), SOME xs => SOME (x::xs)
      | _ => NONE)`
 
+Definition word_exp_size_def:
+  word_exp_size (Op _ xs) = SUM (MAP word_exp_size xs) + 1 ∧
+  word_exp_size (Shift _ x _) = word_exp_size x + 1 ∧
+  word_exp_size (OpLookup _ x _) = word_exp_size x + 3 ∧
+  word_exp_size (Load x) = word_exp_size x + 1 ∧
+  word_exp_size _ = 1
+Termination
+  WF_REL_TAC `measure (exp_size ARB)`
+  \\ REPEAT STRIP_TAC \\ IMP_RES_TAC MEM_IMP_exp_size
+  \\ TRY (FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `ARB`))
+  \\ DECIDE_TAC
+End
+
 val word_exp_def = tDefine "word_exp" `
   (word_exp ^s (Const w) = SOME (Word w)) /\
   (word_exp s (Var v) = lookup v s.locals) /\
   (word_exp s (Lookup name) = FLOOKUP s.store name) /\
+  (word_exp s (OpLookup op x name) =
+     word_exp s (Op op [x; Lookup name])) /\
   (word_exp s (Load addr) =
      case word_exp s addr of
      | SOME (Word w) => mem_load w s
@@ -191,10 +206,10 @@ val word_exp_def = tDefine "word_exp" `
      case word_exp s wexp of
      | SOME (Word w) => OPTION_MAP Word (word_sh sh w n)
      | _ => NONE)`
-  (WF_REL_TAC `measure (exp_size ARB o SND)`
-   \\ REPEAT STRIP_TAC \\ IMP_RES_TAC MEM_IMP_exp_size
-   \\ TRY (FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `ARB`))
-   \\ DECIDE_TAC)
+  (WF_REL_TAC `measure (word_exp_size o SND)`
+   \\ fs [word_exp_size_def]
+   \\ Induct \\ fs [] \\ rw []
+   \\ fs [] \\ res_tac \\ fs [])
 
 val get_var_def = Define `
   get_var v ^s = sptree$lookup v s.locals`;
diff --git a/compiler/backend/wordLangScript.sml b/compiler/backend/wordLangScript.sml
index 2f13ee2522..1632fe2479 100644
--- a/compiler/backend/wordLangScript.sml
+++ b/compiler/backend/wordLangScript.sml
@@ -67,6 +67,7 @@ val raise_stub_location_eq = save_thm("raise_stub_location_eq",
 val every_var_exp_def = tDefine "every_var_exp" `
   (every_var_exp P (Var num) = P num) ∧
   (every_var_exp P (Load exp) = every_var_exp P exp) ∧
+  (every_var_exp P (OpLookup _ exp _) = every_var_exp P exp) ∧
   (every_var_exp P (Op wop ls) = EVERY (every_var_exp P) ls) ∧
   (every_var_exp P (Shift sh exp n) = every_var_exp P exp) ∧
   (every_var_exp P expr = T)`

From 314a7dd02b755aa0a77653c72c16f8fc25ed2b4f Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Fri, 16 Oct 2020 12:35:30 +0200
Subject: [PATCH 04/15] Update stack_to_*Proof files for #796

---
 .../proofs/stack_removeProofScript.sml        | 87 +++++++++++--------
 .../backend/semantics/stackPropsScript.sml    |  6 ++
 compiler/backend/semantics/stackSemScript.sml |  4 +-
 compiler/backend/stackLangScript.sml          |  2 +-
 compiler/backend/stack_removeScript.sml       |  2 +
 5 files changed, 64 insertions(+), 37 deletions(-)

diff --git a/compiler/backend/proofs/stack_removeProofScript.sml b/compiler/backend/proofs/stack_removeProofScript.sml
index cd8c62f38a..5478332631 100644
--- a/compiler/backend/proofs/stack_removeProofScript.sml
+++ b/compiler/backend/proofs/stack_removeProofScript.sml
@@ -9,7 +9,7 @@ open preamble
      set_sepTheory
      semanticsPropsTheory
      helperLib
-local open dep_rewrite blastLib in end
+local open dep_rewrite blastLib labPropsTheory in end
 
 val _ = new_theory"stack_removeProof";
 
@@ -597,6 +597,7 @@ Theorem state_rel_word_exp:
    word_exp t e = SOME w
 Proof
   ho_match_mp_tac word_exp_ind
+  \\ rpt conj_tac
   \\ simp[word_exp_def]
   \\ rw[]
   \\ imp_res_tac state_rel_mem_load_imp
@@ -990,7 +991,7 @@ val name_cases = prove(
 (* Significantly faster than SEP_R_TAC *)
 val mem_load_lemma = Q.prove(`
   MEM name store_list ∧
-  FLOOKUP (s:('a,'c,'b)state).store name = SOME x ∧
+  FLOOKUP (s:('a,'c,'b)stackSem$state).store name = SOME x ∧
   (memory s.memory s.mdomain *
         word_list
           (the_SOME_Word (FLOOKUP s.store BitmapBase) ≪ word_shift (:α))
@@ -1001,7 +1002,7 @@ val mem_load_lemma = Q.prove(`
            bytes_in_word *
            n2w (LENGTH s.data_buffer.buffer + LENGTH s.bitmaps))
           s.data_buffer.space_left * word_store c s.store *
-        word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) state).mdomain)) ⇒
+        word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) stackSem$state).mdomain)) ⇒
   mem_load (c+store_offset name) t1 = SOME x`,
   strip_tac >>
   drule fun2set_STAR_IMP>>
@@ -1041,7 +1042,7 @@ val mem_load_lemma2 = Q.prove(`
            bytes_in_word *
            n2w (LENGTH s.data_buffer.buffer + LENGTH s.bitmaps))
           s.data_buffer.space_left * word_store c s.store *
-        word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) state).mdomain)) ⇒
+        word_list c s.stack) (fun2set (t1.memory,(t1:('a,'c,'b) stackSem$state).mdomain)) ⇒
   c+store_offset name ∈ t1.mdomain`,
   strip_tac >>
   drule fun2set_STAR_IMP>>
@@ -1142,28 +1143,31 @@ Proof
   srw_tac[][FUN_EQ_THM,prog_comp_def,FORALL_PROD,LAMBDA_PROD]
 QED
 
-val comp_correct = Q.prove(
-  `!p s1 r s2 t1 k off jump.
+Theorem comp_correct[local]:
+  !p s1 r s2 t1 k off jump.
      evaluate (p,s1) = (r,s2) /\ r <> SOME Error /\
      state_rel jump off k s1 t1 /\ reg_bound p k ==>
      ?ck t2. evaluate (comp jump off k p,t1 with clock := ck + t1.clock) = (r,t2) /\
              (case r of
-               | SOME (Halt _) => t2.ffi = s2.ffi
-               | SOME TimeOut => t2.ffi = s2.ffi
-               | SOME (FinalFFI _) => t2.ffi = s2.ffi
-               | _ =>  (state_rel jump off k s2 t2))`,
+              | SOME (Halt _) => t2.ffi = s2.ffi
+              | SOME TimeOut => t2.ffi = s2.ffi
+              | SOME (FinalFFI _) => t2.ffi = s2.ffi
+              | _ =>  (state_rel jump off k s2 t2))
+Proof
   recInduct evaluate_ind \\ rpt strip_tac
-  THEN1 (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ rpt var_eq_tac \\ qexists_tac`0` \\ full_simp_tac(srw_ss())[])
-  THEN1
+  THEN1 (* Skip *)
+   (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ rpt var_eq_tac \\ qexists_tac`0` \\ full_simp_tac(srw_ss())[])
+  THEN1 (* Halt *)
    (full_simp_tac(srw_ss())[comp_def,evaluate_def,reg_bound_def]
     \\ imp_res_tac state_rel_get_var \\ full_simp_tac(srw_ss())[]
     \\ qexists_tac`0`
     \\ BasicProvers.TOP_CASE_TAC \\ srw_tac[][] \\ full_simp_tac(srw_ss())[]
     \\ BasicProvers.TOP_CASE_TAC \\ srw_tac[][] \\ full_simp_tac(srw_ss())[]
     \\ full_simp_tac(srw_ss())[state_rel_def])
-  THEN1 (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ full_simp_tac(srw_ss())[state_rel_def])
-  THEN1 (
-    full_simp_tac(srw_ss())[comp_def,evaluate_def]
+  THEN1 (* Alloc *)
+   (full_simp_tac(srw_ss())[comp_def,evaluate_def] \\ full_simp_tac(srw_ss())[state_rel_def])
+  THEN1 (* Inst *)
+   (full_simp_tac(srw_ss())[comp_def,evaluate_def]
     \\ last_x_assum mp_tac
     \\ BasicProvers.TOP_CASE_TAC \\ full_simp_tac(srw_ss())[]
     \\ strip_tac \\ rveq
@@ -1224,6 +1228,19 @@ val comp_correct = Q.prove(
     \\ Q.ABBREV_TAC `d = t1.mdomain`
     \\ drule name_cases
     \\ metis_tac[store_write_lemma])
+  THEN1 (* OpCurrHeap *)
+   (qexists_tac`0`
+    \\ `s.use_store` by full_simp_tac(srw_ss())[state_rel_def]
+    \\ full_simp_tac(srw_ss())[comp_def,evaluate_def,reg_bound_def]
+    \\ gvs [AllCaseEqs(),word_exp_def]
+    \\ every_case_tac \\ full_simp_tac(srw_ss())[] \\ srw_tac[][]
+    \\ fs [inst_def,assign_def,word_exp_def]
+    \\ gvs [AllCaseEqs(),word_exp_def,PULL_EXISTS]
+    \\ rename [‘FLOOKUP s.regs src = SOME (Word c1)’]
+    \\ rename [‘FLOOKUP s.store CurrHeap = SOME (Word c2)’]
+    \\ qsuff_tac ‘FLOOKUP t1.regs src = SOME (Word c1) ∧
+                  FLOOKUP t1.regs (k + 2) = SOME (Word c2)’ THEN1 fs []
+    \\ fs [state_rel_def])
   THEN1 (* Tick *)
    (full_simp_tac(srw_ss())[comp_def,evaluate_def]
     \\ `s.clock = t1.clock` by full_simp_tac(srw_ss())[state_rel_def] \\ full_simp_tac(srw_ss())[]
@@ -1516,7 +1533,7 @@ val comp_correct = Q.prove(
     \\ disch_then(qspec_then`ck2`mp_tac)
     \\ simp[] \\ ntac 2 strip_tac
     \\ qexists_tac`ck' + ck2` \\  simp[] )
- THEN1 ( (* Install *)
+  THEN1 ( (* Install *)
     rw[comp_def]
     \\ fs[evaluate_def]
     \\ fs[reg_bound_def]
@@ -1968,7 +1985,8 @@ val comp_correct = Q.prove(
       \\ full_simp_tac(srw_ss())[mem_load_def]  \\ SEP_R_TAC \\ full_simp_tac(srw_ss())[])
     \\ `good_dimindex(:'a)` by full_simp_tac(srw_ss())[state_rel_def]
     \\ full_simp_tac(srw_ss())[labPropsTheory.good_dimindex_def,word_shift_def,FLOOKUP_UPDATE]
-    \\ full_simp_tac(srw_ss())[mem_load_def] \\ full_simp_tac(srw_ss())[GSYM mem_load_def] \\ full_simp_tac(srw_ss())[GSYM set_var_def]));
+    \\ full_simp_tac(srw_ss())[mem_load_def] \\ full_simp_tac(srw_ss())[GSYM mem_load_def] \\ full_simp_tac(srw_ss())[GSYM set_var_def])
+QED
 
 Theorem compile_semantics:
    state_rel jump off k s1 s2 /\ semantics start s1 <> Fail ==>
@@ -3442,8 +3460,8 @@ Proof
 QED
 
 Theorem stack_remove_lab_pres:
-    ∀jump off k p.
-  extract_labels p = extract_labels (comp jump off k p)
+  ∀jump off k p.
+    extract_labels p = extract_labels (comp jump off k p)
 Proof
   ho_match_mp_tac comp_ind>>Cases_on`p`>>rw[]>>
   once_rewrite_tac [comp_def]>>fs[extract_labels_def]>>
@@ -3474,25 +3492,26 @@ Proof
 QED
 
 Theorem stack_remove_comp_stack_asm_name:
-    ∀jump off k p.
-  stack_asm_name c p ∧ stack_asm_remove (c:'a asm_config) p ∧
-  addr_offset_ok c 0w ∧
-  good_dimindex (:'a) ∧
-  (∀n. n ≤ max_stack_alloc ⇒
-  c.valid_imm (INL Sub) (n2w (n * (dimindex (:'a) DIV 8))) ∧
-  c.valid_imm (INL Add) (n2w (n * (dimindex (:'a) DIV 8)))) ∧
-  (* Needed to implement the global store *)
-  (∀s. addr_offset_ok c (store_offset s)) ∧
-  reg_name (k+2) c ∧
-  reg_name (k+1) c ∧
-  reg_name k c ∧
-  off = c.addr_offset ⇒
-  stack_asm_name c (comp jump off k p)
+  ∀jump off k p.
+    stack_asm_name c p ∧ stack_asm_remove (c:'a asm_config) p ∧
+    addr_offset_ok c 0w ∧
+    good_dimindex (:'a) ∧
+    (∀n. n ≤ max_stack_alloc ⇒
+    c.valid_imm (INL Sub) (n2w (n * (dimindex (:'a) DIV 8))) ∧
+    c.valid_imm (INL Add) (n2w (n * (dimindex (:'a) DIV 8)))) ∧
+    (* Needed to implement the global store *)
+    (∀s. addr_offset_ok c (store_offset s)) ∧
+    reg_name (k+2) c ∧
+    reg_name (k+1) c ∧
+    reg_name k c ∧
+    off = c.addr_offset ⇒
+    stack_asm_name c (comp jump off k p)
 Proof
   ho_match_mp_tac comp_ind>>Cases_on`p`>>rw[]>>
   simp[Once comp_def]>>
   rw[]>>
-  fs[stack_asm_name_def,inst_name_def,stack_asm_remove_def,addr_name_def,arith_name_def,reg_imm_name_def,stackLangTheory.list_Seq_def]
+  fs[stack_asm_name_def,inst_name_def,stack_asm_remove_def,addr_name_def,
+     arith_name_def,reg_imm_name_def,stackLangTheory.list_Seq_def]
   >-
     (every_case_tac>>fs[])
   >-
diff --git a/compiler/backend/semantics/stackPropsScript.sml b/compiler/backend/semantics/stackPropsScript.sml
index a419025e56..5ad5c42b53 100644
--- a/compiler/backend/semantics/stackPropsScript.sml
+++ b/compiler/backend/semantics/stackPropsScript.sml
@@ -751,6 +751,8 @@ val inst_name_def = Define`
 
 val stack_asm_name_def = Define`
   (stack_asm_name c ((Inst i):'a stackLang$prog) ⇔ inst_name c i) ∧
+  (stack_asm_name c (OpCurrHeap b r1 r2) ⇔
+    (c.two_reg_arith ⇒ r1 = r2) ∧ reg_name r1 c ∧ reg_name r2 c) ∧
   (stack_asm_name c (CodeBufferWrite r1 r2) ⇔ reg_name r1 c ∧ reg_name r2 c) ∧
   (stack_asm_name c (DataBufferWrite r1 r2) ⇔ reg_name r1 c ∧ reg_name r2 c) ∧
   (stack_asm_name c (Seq p1 p2) ⇔ stack_asm_name c p1 ∧ stack_asm_name c p2) ∧
@@ -777,6 +779,7 @@ val fixed_names_def = Define`
 
 val stack_asm_remove_def = Define`
   (stack_asm_remove c ((Get n s):'a stackLang$prog) ⇔ reg_name n c) ∧
+  (stack_asm_remove c (OpCurrHeap binop v src) ⇔ reg_name v c ∧ reg_name src c) ∧
   (stack_asm_remove c (Set s n) ⇔ reg_name n c) ∧
   (stack_asm_remove c (StackStore n n0) ⇔ reg_name n c) ∧
   (stack_asm_remove c (StackStoreAny n n0) ⇔ reg_name n c ∧ reg_name n0 c) ∧
@@ -826,6 +829,7 @@ val reg_bound_exp_def = tDefine"reg_bound_exp"`
   (reg_bound_exp (Load e) k ⇔ reg_bound_exp e k) ∧
   (reg_bound_exp (Shift _ e _) k ⇔ reg_bound_exp e k) ∧
   (reg_bound_exp (Lookup _) _ ⇔ F) ∧
+  (reg_bound_exp (OpLookup _ _ _) _ ⇔ F) ∧
   (reg_bound_exp (Op _ es) k ⇔ EVERY (λe. reg_bound_exp e k) es) ∧
   (reg_bound_exp _ _ ⇔ T)`
   (WF_REL_TAC`measure ((exp_size ARB) o FST)` \\ simp[]
@@ -859,6 +863,8 @@ val reg_bound_def = Define `
      v1 < k) /\
   (reg_bound (Get v1 n) k <=>
      v1 < k) /\
+  (reg_bound (OpCurrHeap op v1 v2) k <=>
+     v1 < k ∧ v2 < k) /\
   (reg_bound (Set n v1) k <=>
      v1 < k /\ n <> BitmapBase) /\
   (reg_bound (LocValue v1 l1 l2) k <=>
diff --git a/compiler/backend/semantics/stackSemScript.sml b/compiler/backend/semantics/stackSemScript.sml
index 9c57c8f65c..c43b328a9e 100644
--- a/compiler/backend/semantics/stackSemScript.sml
+++ b/compiler/backend/semantics/stackSemScript.sml
@@ -547,9 +547,9 @@ val evaluate_def = tDefine "evaluate" `
      case get_var v s of
      | SOME w => (NONE, set_store name w s)
      | NONE => (SOME Error, s)) /\
-  (evaluate (GetOp binop v src name,s) =
+  (evaluate (OpCurrHeap binop v src,s) =
      if ¬s.use_store then (SOME Error,s) else
-     case word_exp s (OpLookup binop (Var src) name) of
+     case word_exp s (OpLookup binop (Var src) CurrHeap) of
      | SOME w => (NONE, set_var v (Word w) s)
      | _ => (SOME Error, s)) /\
   (evaluate (Tick,s) =
diff --git a/compiler/backend/stackLangScript.sml b/compiler/backend/stackLangScript.sml
index 083388f93c..893de68c97 100644
--- a/compiler/backend/stackLangScript.sml
+++ b/compiler/backend/stackLangScript.sml
@@ -26,7 +26,7 @@ val _ = Datatype `
        | Inst ('a inst)
        | Get num store_name
        | Set store_name num
-       | GetOp binop num num store_name
+       | OpCurrHeap binop num num
        | Call ((stackLang$prog # num # num # num) option)
               (* return-handler code, link reg, labels l1,l2*)
               (num + num) (* target of call *)
diff --git a/compiler/backend/stack_removeScript.sml b/compiler/backend/stack_removeScript.sml
index 7e56adf7bd..f80ea05841 100644
--- a/compiler/backend/stack_removeScript.sml
+++ b/compiler/backend/stack_removeScript.sml
@@ -125,6 +125,8 @@ val comp_def = Define `
     | Set name r =>
         if name = CurrHeap then move (k+2) r
         else Inst (Mem Store r (Addr (k+1) (store_offset name)))
+    | OpCurrHeap op r n =>
+        Inst (Arith (Binop op r n (Reg (k+2))))
     (* remove stack operations *)
     | StackFree n => stack_free k n
     | StackAlloc n => stack_alloc jump k n

From aa8156b22fba76af51a8cb99b550a0c98f332ed7 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Fri, 16 Oct 2020 13:42:03 +0200
Subject: [PATCH 05/15] More updates to stack*Proofs for #796

---
 .../backend/proofs/stack_allocProofScript.sml | 13 ++++++++++
 .../backend/proofs/stack_namesProofScript.sml |  2 +-
 .../proofs/stack_rawcallProofScript.sml       | 24 ++-----------------
 .../proofs/stack_to_labProofScript.sml        |  4 ++++
 4 files changed, 20 insertions(+), 23 deletions(-)

diff --git a/compiler/backend/proofs/stack_allocProofScript.sml b/compiler/backend/proofs/stack_allocProofScript.sml
index 3b65cde177..10e8dfe62e 100644
--- a/compiler/backend/proofs/stack_allocProofScript.sml
+++ b/compiler/backend/proofs/stack_allocProofScript.sml
@@ -5215,6 +5215,19 @@ Proof
     \\ BasicProvers.TOP_CASE_TAC \\ fs[] \\ rw[]
     \\ imp_res_tac FLOOKUP_SUBMAP \\ fs[]
     \\ full_simp_tac(srw_ss())[state_component_equality] )
+  \\ conj_tac (* OpCurrHeap *) >- (
+    fs[Once comp_def,evaluate_def,get_var_def,word_exp_def]
+    \\ fs [AllCaseEqs(),set_var_def]
+    \\ full_simp_tac(srw_ss())[state_component_equality]
+    \\ rw [] \\ fs [PULL_EXISTS]
+    \\ gs [optionTheory.IS_SOME_EXISTS,AllCaseEqs()]
+    \\ qpat_x_assum`_ = t.regs`(assume_tac o SYM) \\ fs[]
+    \\ rename [‘FLOOKUP s.regs src = SOME (Word x7)’]
+    \\ ‘FLOOKUP regs src = SOME (Word x7)’ by fs [FLOOKUP_DEF,SUBMAP_DEF]
+    \\ fs []
+    \\ match_mp_tac SUBMAP_mono_FUPDATE
+    \\ rw[GSYM SUBMAP_DOMSUB_gen]
+    \\ metis_tac[SUBMAP_TRANS,SUBMAP_DOMSUB] )
   \\ conj_tac (* Tick *) >- (
     rpt strip_tac
     \\ qexists_tac `0` \\ full_simp_tac(srw_ss())[Once comp_def,evaluate_def,dec_clock_def]
diff --git a/compiler/backend/proofs/stack_namesProofScript.sml b/compiler/backend/proofs/stack_namesProofScript.sml
index 3a6a16ca32..63149c6118 100644
--- a/compiler/backend/proofs/stack_namesProofScript.sml
+++ b/compiler/backend/proofs/stack_namesProofScript.sml
@@ -208,7 +208,6 @@ val comp_correct = Q.prove(
      s.compile = (λcfg. c cfg o (stack_names$compile f))
      ==>
      evaluate (comp f p, rename_state c f s) = (r, rename_state c f t)`,
-
   recInduct evaluate_ind \\ rpt strip_tac
   THEN1 (fs [evaluate_def,comp_def] \\ rpt var_eq_tac)
   THEN1 (fs [evaluate_def,comp_def] \\ rpt var_eq_tac \\ CASE_TAC \\ fs []
@@ -219,6 +218,7 @@ val comp_correct = Q.prove(
     imp_res_tac inst_rename >> fs[])
   THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[])
   THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[])
+  THEN1 (fs [evaluate_def,comp_def,rename_state_def] >> rveq >> fs[])
   THEN1 (fs [evaluate_def,comp_def,rename_state_def] \\ rw []
          \\ fs [] \\ rw [] \\ fs [empty_env_def,dec_clock_def])
   THEN1
diff --git a/compiler/backend/proofs/stack_rawcallProofScript.sml b/compiler/backend/proofs/stack_rawcallProofScript.sml
index e3a3491bb4..fba0237dab 100644
--- a/compiler/backend/proofs/stack_rawcallProofScript.sml
+++ b/compiler/backend/proofs/stack_rawcallProofScript.sml
@@ -157,6 +157,8 @@ Proof
    (rename [`Get`] \\ simple_case)
   THEN1
    (rename [`Set`] \\ simple_case)
+  THEN1
+   (rename [`OpCurrHeap`] \\ simple_case)
   THEN1
    (rename [`Tick`] \\ simple_case)
   THEN1
@@ -940,26 +942,4 @@ Proof
   \\ simp [stack_get_handler_labels_def]
 QED
 
-(*
-Theorem get_code_labels_comp:
-  !i p.
-    get_code_labels (comp i p) = get_code_labels p /\
-    get_code_labels (comp_top i p) = get_code_labels p
-Proof
-  recInduct comp_ind \\ rpt gen_tac \\ strip_tac
-  \\ Cases_on `p` \\ fs [] \\ simp [comp_top_def]
-  \\ simp [Once comp_def]
-  \\ TRY (fs [get_code_labels_def] \\ NO_TAC)
-  THEN1 (every_case_tac \\ fs [get_code_labels_def])
-  \\ reverse conj_asm2_tac THEN1 fs [get_code_labels_def]
-  \\ rename [`comp_seq p1 p2`]
-  \\ Cases_on `comp_seq p1 p2 i (Seq (comp i p1) (comp i p2)) =
-               Seq (comp i p1) (comp i p2)` \\ simp []
-  \\ drule comp_seq_neq_IMP \\ strip_tac \\ rveq \\ fs []
-  \\ fs [comp_seq_def,dest_case_def,CaseEq"option",CaseEq"bool"]
-  \\ Cases_on `lookup dest i` \\ fs []  \\ rw []
-  \\ simp [get_code_labels_def]
-QED
-*)
-
 val _ = export_theory();
diff --git a/compiler/backend/proofs/stack_to_labProofScript.sml b/compiler/backend/proofs/stack_to_labProofScript.sml
index 7d84ea03e2..6d37a6f0ed 100644
--- a/compiler/backend/proofs/stack_to_labProofScript.sml
+++ b/compiler/backend/proofs/stack_to_labProofScript.sml
@@ -1167,6 +1167,10 @@ Proof
     rename [`Set`] >>
     srw_tac[][stackSemTheory.evaluate_def,flatten_def] >>
     full_simp_tac(srw_ss())[state_rel_def] ) >>
+  conj_tac >- (
+    rename [`OpCurrHeap`] >>
+    srw_tac[][stackSemTheory.evaluate_def,flatten_def] >>
+    full_simp_tac(srw_ss())[state_rel_def] ) >>
   conj_tac >- (
     rename [`Tick`] >>
     simp[stackSemTheory.evaluate_def,flatten_def] >>

From f4ecfe79e599c62cafe7f4cb0aea733689b2a90b Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Sat, 7 Nov 2020 09:57:01 +0100
Subject: [PATCH 06/15] Revert "Update data_to_word impl. for #796"

This reverts commit 6898ff227b9e37692bb7db979d99cee06d0ba1c9.
---
 compiler/backend/data_to_wordScript.sml | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/compiler/backend/data_to_wordScript.sml b/compiler/backend/data_to_wordScript.sml
index ecde3f3ec0..bc0169de70 100644
--- a/compiler/backend/data_to_wordScript.sml
+++ b/compiler/backend/data_to_wordScript.sml
@@ -111,11 +111,12 @@ val real_addr_def = Define `
   (real_addr (conf:data_to_word$config) r): 'a wordLang$exp =
     let k = shift (:'a) in
       if k <= conf.pad_bits + 1 then
-        OpLookup Add
-          (Shift Lsr (Var r) (shift_length conf - k)) CurrHeap
+        Op Add [Lookup CurrHeap;
+                Shift Lsr (Var r) (shift_length conf - k)]
       else
-        OpLookup Add
-          (Shift Lsl (Shift Lsr (Var r) (shift_length conf)) k) CurrHeap`
+        Op Add [Lookup CurrHeap;
+                Shift Lsl (Shift Lsr (Var r)
+                  (shift_length conf)) k]`
 
 val real_offset_def = Define `
   (real_offset (conf:data_to_word$config) r): 'a wordLang$exp =
@@ -330,7 +331,7 @@ val RefByte_code_def = Define `
                              Shift Lsl (Var 5) (shift (:'a))]);
            Set NextFree (Op Add [Var 1; Const bytes_in_word]);
            (* 3 := return value *)
-           Assign 3 (Op Or [Shift Lsl (OpLookup Sub (Var 9) CurrHeap)
+           Assign 3 (Op Or [Shift Lsl (Op Sub [Var 9; Lookup CurrHeap])
                (shift_length c − shift (:'a)); Const (1w:'a word)]);
            (* compute header *)
            Assign 5 (Op Or [Op Or [y; Const 7w]; Var 6]);
@@ -360,7 +361,7 @@ val Maxout_bits_code_def = Define `
 val Make_ptr_bits_code_def = Define `
   Make_ptr_bits_code c tag len dest =
     list_Seq [Assign dest (Op Or
-       [Const 1w; Shift Lsl (OpLookup Sub (Lookup NextFree) CurrHeap)
+       [Const 1w; Shift Lsl (Op Sub [Lookup NextFree; Lookup CurrHeap])
            (shift_length c − shift (:'a))]);
         Maxout_bits_code c.tag_bits (1 + c.len_bits) dest tag;
         Maxout_bits_code c.len_bits 1 dest len] :'a wordLang$prog`
@@ -414,7 +415,7 @@ val RefArray_code_def = Define `
            Assign 1 (Op Sub [Lookup EndOfHeap; Var 1]);
            Set EndOfHeap (Var 1);
            (* 3 := return value *)
-           Assign 3 (Op Or [Shift Lsl (OpLookup Sub (Var 1) CurrHeap)
+           Assign 3 (Op Or [Shift Lsl (Op Sub [Var 1; Lookup CurrHeap])
                (shift_length c − shift (:'a)); Const (1w:'a word)]);
            (* compute header *)
            Assign 5 (Op Or [Shift Lsl (Var 2)
@@ -541,7 +542,7 @@ val AnyArith_code_def = Define `
                        ShiftVar Lsl 6 (dimindex (:'a) − c.len_size);
                        ShiftVar Lsl 8 4]);
       Store (Var 5) 7;
-      Assign 1 (OpLookup Sub (Var 5) CurrHeap);
+      Assign 1 (Op Sub [Var 5; Lookup CurrHeap]);
       Assign 1 (Op Or [ShiftVar Lsl 1 (shift_length c − shift (:'a)); Const 1w]);
       Set NextFree (Op Add [Var 5; Const bytes_in_word;
                             ShiftVar Lsl 6 (shift (:'a))]);
@@ -1093,7 +1094,7 @@ val def = assign_Define `
                          Assign 3 (Const header);
                          StoreEach 1 (3::MAP adjust_var args) 0w;
                          Assign (adjust_var dest)
-                           (Op Or [Shift Lsl (OpLookup Sub (Var 1) CurrHeap)
+                           (Op Or [Shift Lsl (Op Sub [Var 1; Lookup CurrHeap])
                                      (shift_length c − shift (:'a));
                                    Const (1w ||
                                            (small_shift_length c − 1 -- 0)
@@ -1163,7 +1164,7 @@ val def = assign_Define `
                   Assign 3 (Const header);
                   StoreEach 1 (3::MAP adjust_var args) 0w;
                   Assign (adjust_var dest)
-                    (Op Or [Shift Lsl (OpLookup Sub (Var 1) CurrHeap)
+                    (Op Or [Shift Lsl (Op Sub [Var 1; Lookup CurrHeap])
                               (shift_length c − shift (:'a));
                             Const 1w])],l))
       : 'a wordLang$prog # num`;

From c202a8c4f9e4addaac862b18161c6c0d44386daa Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Wed, 11 Nov 2020 14:05:33 +0100
Subject: [PATCH 07/15] Progress on #796

---
 compiler/backend/presLangScript.sml           |   4 +
 .../proofs/word_to_stackProofScript.sml       | 143 +++++++++++++-----
 .../backend/semantics/stackPropsScript.sml    |   1 -
 compiler/backend/semantics/stackSemScript.sml |  12 +-
 .../backend/semantics/wordPropsScript.sml     |  46 ++++--
 compiler/backend/semantics/wordSemScript.sml  |  27 +---
 compiler/backend/wordLangScript.sml           |   5 +-
 compiler/backend/word_allocScript.sml         |   7 +
 compiler/backend/word_to_stackScript.sml      |   3 +
 9 files changed, 173 insertions(+), 75 deletions(-)

diff --git a/compiler/backend/presLangScript.sml b/compiler/backend/presLangScript.sml
index 9d504b5e88..bd4fe859a1 100644
--- a/compiler/backend/presLangScript.sml
+++ b/compiler/backend/presLangScript.sml
@@ -630,6 +630,8 @@ val stack_prog_to_display_def = Define`
         store_name_to_display sn]
     | Set sn n => Item NONE «Set» [store_name_to_display sn;
         num_to_display n]
+    | OpCurrHeap b n1 n2 => Item NONE «OpCurrHeap»
+        [asm_binop_to_display b; num_to_display n1; num_to_display n2]
     | Call rh tgt eh => Item NONE «Call»
         [(case rh of
             | NONE => empty_item «Tail»
@@ -761,6 +763,8 @@ val word_prog_to_display_def = tDefine "word_prog_to_display" `
     [word_prog_to_display_ret a; option_to_display num_to_display b;
         list_to_display num_to_display c;
         word_prog_to_display_handler d]) /\
+  (word_prog_to_display (OpCurrHeap b n1 n2) = Item NONE «OpCurrHeap»
+    [asm_binop_to_display b; num_to_display n1; num_to_display n2]) /\
   (word_prog_to_display (Seq prog1 prog2) = Item NONE (strlit "Seq")
     [word_prog_to_display prog1; word_prog_to_display prog2]) /\
   (word_prog_to_display (If cmp n reg p1 p2) = Item NONE (strlit "If")
diff --git a/compiler/backend/proofs/word_to_stackProofScript.sml b/compiler/backend/proofs/word_to_stackProofScript.sml
index ed4692fd4f..18cf5b1ce5 100644
--- a/compiler/backend/proofs/word_to_stackProofScript.sml
+++ b/compiler/backend/proofs/word_to_stackProofScript.sml
@@ -5697,6 +5697,54 @@ Proof
   \\ metis_tac[state_rel_set_store]
 QED
 
+Theorem comp_OpCurrHeap_correct:
+  ^(get_goal "OpCurrHeap")
+Proof
+  REPEAT STRIP_TAC \\ fs[get_labels_def]
+  \\ fs[flat_exp_conventions_def]
+  \\ fs[comp_def,LET_THM]
+  \\ pairarg_tac \\ fs[]
+  \\ fs[wordSemTheory.evaluate_def,wordSemTheory.word_exp_def,the_words_def,AllCaseEqs()]
+  \\ gvs [] \\ qexists_tac`0` \\ simp[]
+  \\ CONV_TAC SWAP_EXISTS_CONV
+  \\ qexists_tac`NONE` \\ simp[]
+  \\ CONV_TAC (PATH_CONV "ralrlrrlrr" (UNBETA_CONV “src_r:num”))
+  \\ match_mp_tac (GEN_ALL wStackLoad_thm1_weak)
+  \\ gvs[convs_def,reg_allocTheory.is_phy_var_def,GSYM EVEN_MOD2,EVEN_EXISTS]
+  \\ asm_exists_tac \\ fs []
+  \\ fs [get_var_def]
+  \\ asm_exists_tac \\ fs [] \\ rw []
+  \\ ‘t.use_store’ by fs [state_rel_def]
+  THEN1
+   (qmatch_goalsub_abbrev_tac `wRegWrite1 kont (2 * m)`
+    \\ qmatch_goalsub_abbrev_tac `state_rel _ _ _ (set_var _ v _)`
+    \\ drule_then(qspecl_then [`v`,`m`,`kont`] mp_tac) (GEN_ALL wRegWrite1_thm1)
+    \\ unabbrev_all_tac
+    \\ fs[wordLangTheory.max_var_def,GSYM LEFT_ADD_DISTRIB]
+    \\ reverse impl_tac >- metis_tac[]
+    \\ rw [] \\ fs [stackSemTheory.evaluate_def,stackSemTheory.word_exp_def]
+    \\ fs [AllCaseEqs()]
+    \\ ‘FLOOKUP t.store CurrHeap = FLOOKUP s.store CurrHeap’ by
+          fs [state_rel_def,DOMSUB_FLOOKUP_THM] \\ fs []
+    \\ ‘get_var (2 * m') s = SOME (Word x)’ by fs [get_var_def]
+    \\ imp_res_tac state_rel_get_var_imp \\ fs [])
+  \\ qmatch_goalsub_abbrev_tac `wRegWrite1 kont (2 * m)`
+  \\ qmatch_goalsub_abbrev_tac `state_rel _ _ _ (set_var _ v _)`
+  \\ qmatch_goalsub_abbrev_tac ‘_,set_var _ kval _’
+  \\ ‘state_rel k f f' s (set_var k kval t) lens’ by fs []
+  \\ drule_then(qspecl_then [`v`,`m`,`kont`] mp_tac) (GEN_ALL wRegWrite1_thm1)
+  \\ unabbrev_all_tac
+  \\ fs[wordLangTheory.max_var_def,GSYM LEFT_ADD_DISTRIB]
+  \\ reverse impl_tac >- metis_tac[]
+  \\ rw [] \\ fs [stackSemTheory.evaluate_def,stackSemTheory.word_exp_def]
+  \\ fs [AllCaseEqs()]
+  \\ ‘FLOOKUP t.store CurrHeap = FLOOKUP s.store CurrHeap’ by
+    fs [state_rel_def,DOMSUB_FLOOKUP_THM] \\ fs []
+  \\ ‘get_var (2 * m') s = SOME (Word x)’ by fs [get_var_def]
+  \\ imp_res_tac state_rel_get_var_imp2 \\ fs []
+  \\ fs [stackSemTheory.set_var_def,FLOOKUP_UPDATE]
+QED
+
 Theorem comp_Store_correct:
   ^(get_goal "Store")
 Proof
@@ -8264,7 +8312,7 @@ Proof
      comp_Get_correct,comp_Set_correct,comp_Store_correct,comp_Tick_correct,comp_MustTerminate_correct,
      comp_Seq_correct,comp_Return_correct,comp_Raise_correct,comp_If_correct,comp_LocValue_correct,
      comp_Install_correct,comp_CodeBufferWrite_correct,comp_DataBufferWrite_correct,
-     comp_FFI_correct,comp_Call_correct
+     comp_FFI_correct,comp_OpCurrHeap_correct,comp_Call_correct
     ]
 QED
 
@@ -8930,6 +8978,7 @@ Proof
     TRY(Cases_on`b`>>Cases_on`r`)>>EVAL_TAC>>
     EVERY_CASE_TAC>>EVAL_TAC)
   >- rpt (EVERY_CASE_TAC>>EVAL_TAC)
+  >- rpt (EVERY_CASE_TAC>>EVAL_TAC)
   >- (rpt(pairarg_tac>>fs[])>>EVAL_TAC)
   >-
     (Cases_on`ri`>>fs[wRegImm2_def,wReg2_def]>>EVERY_CASE_TAC>>
@@ -9099,6 +9148,14 @@ Proof
     (PairCases_on`kf'`>>
     ntac 3 (EVAL_TAC>>rw[])>>
     rpt(EVAL_TAC>>rw[]))
+  >-
+    (PairCases_on`kf` \\ EVAL_TAC
+    \\ rw [] \\ EVAL_TAC
+    \\ fs[inst_ok_less_def,inst_arg_convention_def,every_inst_def,
+          two_reg_inst_def,wordLangTheory.every_var_inst_def,full_inst_ok_less_def,
+          reg_allocTheory.is_phy_var_def,asmTheory.fp_reg_ok_def]
+    \\ rw [] \\ EVAL_TAC \\ fs [] \\ gvs []
+    \\ CCONTR_TAC \\ gvs [])
   >-
     (fs wconvs>>
     ntac 4 (pop_assum mp_tac)>>
@@ -9198,6 +9255,9 @@ Proof
   >-
     (PairCases_on`kf'`>>
     rpt(EVAL_TAC>>rw[]))
+  >-
+    (PairCases_on`kf`>>
+    rpt(EVAL_TAC>>rw[]))
   >-
     (rpt(pairarg_tac>>fs[])>>
     EVAL_TAC>>fs[])
@@ -9275,16 +9335,16 @@ Proof
 QED
 
 Theorem stack_move_alloc_arg:
-    ∀n st off i p.
-  alloc_arg p ⇒
-  alloc_arg (stack_move n st off i p)
+  ∀n st off i p.
+    alloc_arg p ⇒
+    alloc_arg (stack_move n st off i p)
 Proof
   Induct>>rw[stack_move_def,alloc_arg_def]
 QED
 
 Theorem word_to_stack_alloc_arg:
-    ∀p n args.
-  alloc_arg (FST(word_to_stack$comp p n args))
+  ∀p n args.
+    alloc_arg (FST(word_to_stack$comp p n args))
 Proof
   recInduct comp_ind >>
   fs[comp_def,alloc_arg_def,FORALL_PROD,wRegWrite1_def,wLive_def]>>
@@ -9301,7 +9361,12 @@ Proof
     fs[wInst_def,wRegWrite1_def,wReg1_def,wReg2_def,wRegWrite2_def]>>
     BasicProvers.EVERY_CASE_TAC>>
     fs[wStackLoad_def,alloc_arg_def])
-  >- (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>fs[alloc_arg_def,wStackLoad_def])
+  >-
+    (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>
+    fs[alloc_arg_def,wStackLoad_def])
+  >-
+    (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>
+    fs[alloc_arg_def,wStackLoad_def])
   >- rpt (pairarg_tac>>fs[alloc_arg_def])
   >- (rpt (pairarg_tac>>fs[alloc_arg_def])>>
   Cases_on`ri`>>fs[wReg1_def,wRegImm2_def,wReg2_def]>>BasicProvers.EVERY_CASE_TAC>>fs[]>>rveq>>fs[wStackLoad_def,alloc_arg_def])
@@ -9329,19 +9394,19 @@ Proof
 QED
 
 Theorem stack_move_reg_bound:
-    ∀n st off i p k.
-  i < k ∧
-  reg_bound p k ⇒
-  reg_bound (stack_move n st off i p) k
+  ∀n st off i p k.
+    i < k ∧
+    reg_bound p k ⇒
+    reg_bound (stack_move n st off i p) k
 Proof
   Induct>>rw[stack_move_def,reg_bound_def]
 QED
 
 Theorem word_to_stack_reg_bound:
-    ∀p n args.
-  post_alloc_conventions (FST args) p ∧
-  4 ≤ FST args ⇒
-  reg_bound (FST(word_to_stack$comp p n args)) (FST args+2)
+  ∀p n args.
+    post_alloc_conventions (FST args) p ∧
+    4 ≤ FST args ⇒
+    reg_bound (FST(word_to_stack$comp p n args)) (FST args+2)
 Proof
   recInduct comp_ind >>fs[comp_def,reg_bound_def,FORALL_PROD,wRegWrite1_def,wLive_def]>>rw[]>>
   fs[reg_bound_def,convs_def]
@@ -9360,7 +9425,12 @@ Proof
     fs[wInst_def,wRegWrite1_def,wReg1_def,wReg2_def,wRegWrite2_def]>>
     BasicProvers.EVERY_CASE_TAC>>
     fs[wStackLoad_def,reg_bound_def]>>fs [reg_bound_def,convs_def,inst_arg_convention_def])
-  >- (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>fs[reg_bound_def,wStackLoad_def])
+  >-
+    (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>
+    fs[reg_bound_def,wStackLoad_def])
+  >-
+    (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>
+    fs[reg_bound_def,wStackLoad_def])
   >- rpt (pairarg_tac>>fs [reg_bound_def])
   >- (rpt (pairarg_tac>>fs [reg_bound_def])>>
   Cases_on`ri`>>fs[wReg1_def,wRegImm2_def,wReg2_def]>>BasicProvers.EVERY_CASE_TAC>>fs[]>>rveq>>fs[wStackLoad_def,reg_bound_def])
@@ -9389,17 +9459,17 @@ Proof
 QED
 
 Theorem stack_move_call_args:
-    ∀n st off i p.
-  call_args p 1 2 3 4 0 ⇒
-  call_args (stack_move n st off i p) 1 2 3 4 0
+  ∀n st off i p.
+    call_args p 1 2 3 4 0 ⇒
+    call_args (stack_move n st off i p) 1 2 3 4 0
 Proof
   Induct>>rw[stack_move_def,call_args_def]
 QED
 
 Theorem word_to_stack_call_args:
-    ∀p n args.
-  post_alloc_conventions (FST args) p ⇒
-  call_args (FST(word_to_stack$comp p n args)) 1 2 3 4 0
+  ∀p n args.
+    post_alloc_conventions (FST args) p ⇒
+    call_args (FST(word_to_stack$comp p n args)) 1 2 3 4 0
 Proof
   ho_match_mp_tac comp_ind >>
   fs[comp_def,call_args_def,FORALL_PROD,wRegWrite1_def,wLive_def,convs_def]>>rw[]>>
@@ -9419,6 +9489,7 @@ Proof
     BasicProvers.EVERY_CASE_TAC>>
     fs[wStackLoad_def,convs_def]>>fs [call_args_def])
   >- (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>fs[call_args_def,wStackLoad_def])
+  >- (fs[wReg1_def,SeqStackFree_def]>>BasicProvers.EVERY_CASE_TAC>>fs[call_args_def,wStackLoad_def])
   >- rpt (pairarg_tac>>fs [call_args_def,convs_def])
   >- (rpt (pairarg_tac>>fs [call_args_def])>>
   Cases_on`ri`>>fs[wReg1_def,wRegImm2_def,wReg2_def]>>BasicProvers.EVERY_CASE_TAC>>fs[]>>rveq>>fs[wStackLoad_def,call_args_def])
@@ -9449,10 +9520,10 @@ val reg_bound_def = stackPropsTheory.reg_bound_def
 val reg_bound_inst_def = stackPropsTheory.reg_bound_inst_def
 
 Theorem reg_bound_mono:
-    ∀p k k'.
-  reg_bound p k ∧
-  k ≤ k' ⇒
-  reg_bound p k'
+  ∀p k k'.
+    reg_bound p k ∧
+    k ≤ k' ⇒
+    reg_bound p k'
 Proof
   ho_match_mp_tac reg_bound_ind>>rw[reg_bound_def]>>
   rpt(TOP_CASE_TAC>>fs[])>>
@@ -9520,7 +9591,7 @@ Proof
 QED
 
 Theorem compile_word_to_stack_convs:
-   ∀p bm q bm'.
+  ∀p bm q bm'.
    compile_word_to_stack k p bm = (q,bm') ∧
    EVERY (λ(n,m,p).
      full_inst_ok_less c p ∧
@@ -9582,9 +9653,10 @@ val stack_move_code_labels = Q.prove(`
 
 Theorem word_to_stack_comp_code_labels:
   ∀prog bs kf n.
-  good_handlers n prog ⇒
-  get_code_labels (FST (comp prog bs kf)) ⊆
-  (raise_stub_location,0n) INSERT ((IMAGE (λn.(n,0)) (get_code_labels prog)) ∪ stack_get_handler_labels n (FST (comp prog bs kf)))
+    good_handlers n prog ⇒
+    get_code_labels (FST (comp prog bs kf)) ⊆
+    (raise_stub_location,0n) INSERT ((IMAGE (λn.(n,0)) (get_code_labels prog)) ∪
+      stack_get_handler_labels n (FST (comp prog bs kf)))
 Proof
   ho_match_mp_tac word_to_stackTheory.comp_ind>>
   rw[word_to_stackTheory.comp_def]>>
@@ -9609,6 +9681,7 @@ Proof
   >>
     rpt(first_x_assum drule)>>rw[]>>
     TRY(fs[SUBSET_DEF]>>metis_tac[])
+  >- (rw [wRegWrite1_def])
   >-
     (TOP_CASE_TAC>>fs[]>>pairarg_tac>>fs[get_code_handler_labels_wStackLoad])
   >-
@@ -9656,7 +9729,7 @@ Proof
   >>
   fs[SUBSET_DEF]>>
   metis_tac[]
-QED;
+QED
 
 Theorem word_to_stack_good_code_labels:
   compile asm_conf progs = (bs,fs,prog') ∧
@@ -9682,7 +9755,7 @@ Proof
     metis_tac[])
   >>
     fs[SUBSET_DEF]
-QED;
+QED
 
 Theorem word_to_stack_good_code_labels_incr:
   raise_stub_location ∈ elabs ∧
@@ -9704,7 +9777,7 @@ Proof
     metis_tac[])
   >>
     fs[SUBSET_DEF]
-QED;
+QED
 
 Triviality sub_union_lemma:
   x SUBSET y ==> x SUBSET y UNION z
@@ -9736,7 +9809,7 @@ Proof
     (simp[backendPropsTheory.restrict_nonzero_def,Abbr`xxx`,EXTENSION,MEM_MAP]>>
     metis_tac[SND])>>
   simp[]
-QED;
+QED
 
 Theorem word_to_stack_good_handler_labels_incr:
   EVERY (λ(n,m,pp). good_handlers n pp) prog ⇒
@@ -9760,6 +9833,6 @@ Proof
     (simp[backendPropsTheory.restrict_nonzero_def,Abbr`xxx`,EXTENSION,MEM_MAP]>>
     metis_tac[SND])>>
   simp[]
-QED;
+QED
 
 val _ = export_theory();
diff --git a/compiler/backend/semantics/stackPropsScript.sml b/compiler/backend/semantics/stackPropsScript.sml
index 5ad5c42b53..68bd1f9436 100644
--- a/compiler/backend/semantics/stackPropsScript.sml
+++ b/compiler/backend/semantics/stackPropsScript.sml
@@ -829,7 +829,6 @@ val reg_bound_exp_def = tDefine"reg_bound_exp"`
   (reg_bound_exp (Load e) k ⇔ reg_bound_exp e k) ∧
   (reg_bound_exp (Shift _ e _) k ⇔ reg_bound_exp e k) ∧
   (reg_bound_exp (Lookup _) _ ⇔ F) ∧
-  (reg_bound_exp (OpLookup _ _ _) _ ⇔ F) ∧
   (reg_bound_exp (Op _ es) k ⇔ EVERY (λe. reg_bound_exp e k) es) ∧
   (reg_bound_exp _ _ ⇔ T)`
   (WF_REL_TAC`measure ((exp_size ARB) o FST)` \\ simp[]
diff --git a/compiler/backend/semantics/stackSemScript.sml b/compiler/backend/semantics/stackSemScript.sml
index c43b328a9e..2b4c3ee800 100644
--- a/compiler/backend/semantics/stackSemScript.sml
+++ b/compiler/backend/semantics/stackSemScript.sml
@@ -126,8 +126,6 @@ val word_exp_def = tDefine "word_exp" `
      case FLOOKUP s.store name of
      | SOME (Word w) => SOME w
      | _ => NONE) /\
-  (word_exp s (OpLookup op x name) =
-     word_exp s (Op op [x; Lookup name])) /\
   (word_exp s (Load addr) =
      case word_exp s addr of
      | SOME w => (case mem_load w s of
@@ -141,10 +139,10 @@ val word_exp_def = tDefine "word_exp" `
      case word_exp s wexp of
      | NONE => NONE
      | SOME w => word_sh sh w n)`
-  (WF_REL_TAC `measure (word_exp_size o SND)`
-   \\ fs [wordSemTheory.word_exp_size_def]
-   \\ Induct \\ fs [] \\ rw []
-   \\ fs [] \\ res_tac \\ fs []);
+  (WF_REL_TAC `measure (exp_size ARB o SND)`
+   \\ REPEAT STRIP_TAC \\ IMP_RES_TAC wordLangTheory.MEM_IMP_exp_size
+   \\ TRY (FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `ARB`))
+   \\ DECIDE_TAC);
 
 val get_var_def = Define `
   get_var v (s:('a,'c,'ffi) stackSem$state) = FLOOKUP s.regs v`;
@@ -549,7 +547,7 @@ val evaluate_def = tDefine "evaluate" `
      | NONE => (SOME Error, s)) /\
   (evaluate (OpCurrHeap binop v src,s) =
      if ¬s.use_store then (SOME Error,s) else
-     case word_exp s (OpLookup binop (Var src) CurrHeap) of
+     case word_exp s (Op binop [Var src; Lookup CurrHeap]) of
      | SOME w => (NONE, set_var v (Word w) s)
      | _ => (SOME Error, s)) /\
   (evaluate (Tick,s) =
diff --git a/compiler/backend/semantics/wordPropsScript.sml b/compiler/backend/semantics/wordPropsScript.sml
index 0a5f76903b..769711ce4b 100644
--- a/compiler/backend/semantics/wordPropsScript.sml
+++ b/compiler/backend/semantics/wordPropsScript.sml
@@ -675,6 +675,7 @@ Proof
   >- tac
   >- tac
   >- tac
+  >- tac
   >- (tac>>imp_res_tac mem_store_const>>full_simp_tac(srw_ss())[])
   >- DECIDE_TAC
   >- `F`by DECIDE_TAC
@@ -1484,6 +1485,13 @@ Proof
     rpt strip_tac>>
     HINT_EXISTS_TAC>>
     full_simp_tac(srw_ss())[GEN_ALL(SYM(SPEC_ALL word_exp_stack_swap)),s_key_eq_refl])
+  >-(*OpCurrHeap*)
+    (fs[evaluate_def]>>every_case_tac>>
+    fs[set_var_def,s_key_eq_refl]>>
+    full_simp_tac(srw_ss())[set_store_def,s_key_eq_refl]>>
+    rpt strip_tac>>
+    HINT_EXISTS_TAC>>
+    full_simp_tac(srw_ss())[GEN_ALL(SYM(SPEC_ALL word_exp_stack_swap)),s_key_eq_refl])
   >-(*Store*)
     (full_simp_tac(srw_ss())[evaluate_def]>>every_case_tac>>
     full_simp_tac(srw_ss())[mem_store_def,state_component_equality,s_key_eq_refl]>>
@@ -2199,6 +2207,8 @@ Proof
     (every_case_tac>>fs[state_component_equality])
   >-
     (fs[]>>every_case_tac>>fs[set_store_def,state_component_equality])
+  >-
+    (fs[]>>every_case_tac>>fs[set_store_def,state_component_equality])
   >-
     (fs[]>>every_case_tac>>fs[set_store_def,state_component_equality,mem_store_perm])
   >-
@@ -2573,19 +2583,19 @@ val locals_rel_cut_env = Q.prove(`
 (*Extra temporaries not mentioned in program
   do not affect evaluation*)
 
-val srestac = qpat_x_assum`A=res`sym_sub_tac>>full_simp_tac(srw_ss())[]
+val srestac = qpat_x_assum`A=res`sym_sub_tac>>full_simp_tac(srw_ss())[];
 
 Theorem locals_rel_evaluate_thm:
-    ∀prog st res rst loc temp.
-  evaluate (prog,st) = (res,rst) ∧
-  res ≠ SOME Error ∧
-  every_var (λx.x < temp) prog ∧
-  locals_rel temp st.locals loc ⇒
-  ∃loc'.
-  evaluate (prog,st with locals:=loc) = (res,rst with locals:=loc') ∧
-  case res of
-    NONE => locals_rel temp rst.locals loc'
-  |  SOME _ => rst.locals = loc'
+  ∀prog st res rst loc temp.
+    evaluate (prog,st) = (res,rst) ∧
+    res ≠ SOME Error ∧
+    every_var (λx.x < temp) prog ∧
+    locals_rel temp st.locals loc ⇒
+    ∃loc'.
+      evaluate (prog,st with locals:=loc) = (res,rst with locals:=loc') ∧
+      case res of
+      | NONE => locals_rel temp rst.locals loc'
+      | SOME _ => rst.locals = loc'
 Proof
   completeInduct_on`prog_size (K 0) prog`>>
   rpt strip_tac>>
@@ -2760,6 +2770,12 @@ Proof
   >-
     (IF_CASES_TAC>>full_simp_tac(srw_ss())[call_env_def,flush_state_def,state_component_equality,dec_clock_def]>>
     srestac>>full_simp_tac(srw_ss())[]>>metis_tac[])
+  >-
+    (gvs[every_var_def,word_exp_def,AllCaseEqs(),the_words_def]>>
+     fs [PULL_EXISTS,state_component_equality,set_var_def] >>
+     imp_res_tac locals_rel_get_var>>
+     fs [get_var_def] \\ res_tac \\ fs [] >>
+     fs [locals_rel_def,lookup_insert])
   >-
     (rw[]>>fs[set_var_def,state_component_equality]>>rveq>>fs[]>>
     qpat_x_assum`A=rst.locals` sym_sub_tac>>
@@ -2936,6 +2952,8 @@ val full_inst_ok_less_def = Define`
     ((case ri of Imm w => c.valid_imm (INR cmp) w | _ => T) ∧
     full_inst_ok_less c c1 ∧ full_inst_ok_less c c2)) ∧
   (full_inst_ok_less c (MustTerminate p) ⇔ full_inst_ok_less c p) ∧
+  (full_inst_ok_less c (OpCurrHeap b r1 r2) ⇔
+    (c.two_reg_arith ==> (r2 = r1))) ∧
   (full_inst_ok_less c (Call ret dest args handler)
     ⇔ (case ret of
         NONE => T
@@ -3375,6 +3393,8 @@ Proof
    every_case_tac >> fs [set_vars_def] >> rveq >> fs [state_fn_updates])
   >- (
    every_case_tac >> fs [set_store_def] >> rveq >> fs [state_fn_updates])
+  >- (
+   every_case_tac >> fs [set_store_def] >> rveq >> fs [state_fn_updates])
   >- (
    every_case_tac >> fs [mem_store_def] >> rveq >> fs [state_fn_updates])
   >- (
@@ -3928,6 +3948,10 @@ Proof
    (fs [wordSemTheory.evaluate_def] \\ rveq
     \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs []
     \\ fs [set_var_def])
+  THEN1 (* OpCurrHeap *)
+   (fs [wordSemTheory.evaluate_def] \\ rveq
+    \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs []
+    \\ fs [set_var_def])
   THEN1 (* Store *)
    (fs [wordSemTheory.evaluate_def,mem_store_def] \\ rveq
     \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs []
diff --git a/compiler/backend/semantics/wordSemScript.sml b/compiler/backend/semantics/wordSemScript.sml
index 8c0255949c..fecc45091e 100644
--- a/compiler/backend/semantics/wordSemScript.sml
+++ b/compiler/backend/semantics/wordSemScript.sml
@@ -175,25 +175,10 @@ val the_words_def = Define `
      | SOME (Word x), SOME xs => SOME (x::xs)
      | _ => NONE)`
 
-Definition word_exp_size_def:
-  word_exp_size (Op _ xs) = SUM (MAP word_exp_size xs) + 1 ∧
-  word_exp_size (Shift _ x _) = word_exp_size x + 1 ∧
-  word_exp_size (OpLookup _ x _) = word_exp_size x + 3 ∧
-  word_exp_size (Load x) = word_exp_size x + 1 ∧
-  word_exp_size _ = 1
-Termination
-  WF_REL_TAC `measure (exp_size ARB)`
-  \\ REPEAT STRIP_TAC \\ IMP_RES_TAC MEM_IMP_exp_size
-  \\ TRY (FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `ARB`))
-  \\ DECIDE_TAC
-End
-
 val word_exp_def = tDefine "word_exp" `
   (word_exp ^s (Const w) = SOME (Word w)) /\
   (word_exp s (Var v) = lookup v s.locals) /\
   (word_exp s (Lookup name) = FLOOKUP s.store name) /\
-  (word_exp s (OpLookup op x name) =
-     word_exp s (Op op [x; Lookup name])) /\
   (word_exp s (Load addr) =
      case word_exp s addr of
      | SOME (Word w) => mem_load w s
@@ -206,10 +191,10 @@ val word_exp_def = tDefine "word_exp" `
      case word_exp s wexp of
      | SOME (Word w) => OPTION_MAP Word (word_sh sh w n)
      | _ => NONE)`
-  (WF_REL_TAC `measure (word_exp_size o SND)`
-   \\ fs [word_exp_size_def]
-   \\ Induct \\ fs [] \\ rw []
-   \\ fs [] \\ res_tac \\ fs [])
+  (WF_REL_TAC `measure (exp_size ARB o SND)`
+   \\ REPEAT STRIP_TAC \\ IMP_RES_TAC MEM_IMP_exp_size
+   \\ TRY (FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `ARB`))
+   \\ DECIDE_TAC);
 
 val get_var_def = Define `
   get_var v ^s = sptree$lookup v s.locals`;
@@ -714,6 +699,10 @@ val evaluate_def = tDefine "evaluate" `
      case word_exp s exp of
      | NONE => (SOME Error, s)
      | SOME w => (NONE, set_store v w s)) /\
+  (evaluate (OpCurrHeap b dst src,s) =
+     case word_exp s (Op b [Var src; Lookup CurrHeap]) of
+     | NONE => (SOME Error, s)
+     | SOME w => (NONE, set_var dst w s)) /\
   (evaluate (Store exp v,s) =
      case (word_exp s exp, get_var v s) of
      | (SOME (Word a), SOME w) =>
diff --git a/compiler/backend/wordLangScript.sml b/compiler/backend/wordLangScript.sml
index 1632fe2479..0c8e24b0d7 100644
--- a/compiler/backend/wordLangScript.sml
+++ b/compiler/backend/wordLangScript.sml
@@ -15,7 +15,6 @@ val _ = Datatype `
       | Lookup store_name
       | Load exp
       | Op binop (exp list)
-      | OpLookup binop exp store_name
       | Shift shift exp num`
 
 Theorem MEM_IMP_exp_size:
@@ -47,6 +46,7 @@ val _ = Datatype `
        | Raise num
        | Return num num
        | Tick
+       | OpCurrHeap binop num num (* special case compiled well in stackLang *)
        | LocValue num num        (* assign v1 := Loc v2 0 *)
        | Install num num num num num_set (* code buffer start, length of new code,
                                       data buffer start, length of new data, cut-set *)
@@ -67,7 +67,6 @@ val raise_stub_location_eq = save_thm("raise_stub_location_eq",
 val every_var_exp_def = tDefine "every_var_exp" `
   (every_var_exp P (Var num) = P num) ∧
   (every_var_exp P (Load exp) = every_var_exp P exp) ∧
-  (every_var_exp P (OpLookup _ exp _) = every_var_exp P exp) ∧
   (every_var_exp P (Op wop ls) = EVERY (every_var_exp P) ls) ∧
   (every_var_exp P (Shift sh exp n) = every_var_exp P exp) ∧
   (every_var_exp P expr = T)`
@@ -143,6 +142,7 @@ val every_var_def = Define `
     (P num ∧ every_name P numset)) ∧
   (every_var P (Raise num) = P num) ∧
   (every_var P (Return num1 num2) = (P num1 ∧ P num2)) ∧
+  (every_var P (OpCurrHeap _ num1 num2) = (P num1 ∧ P num2)) ∧
   (every_var P Tick = T) ∧
   (every_var P (Set n exp) = every_var_exp P exp) ∧
   (every_var P p = T)`
@@ -247,6 +247,7 @@ val max_var_def = Define `
   (max_var (FFI ffi_index ptr1 len1 ptr2 len2 numset) =
     list_max (ptr1::len1::ptr2::len2::MAP FST (toAList numset))) ∧
   (max_var (Raise num) = num) ∧
+  (max_var (OpCurrHeap _ num1 num2) = MAX num1 num2) ∧
   (max_var (Return num1 num2) = MAX num1 num2) ∧
   (max_var Tick = 0) ∧
   (max_var (LocValue r l1) = r) ∧
diff --git a/compiler/backend/word_allocScript.sml b/compiler/backend/word_allocScript.sml
index 442603de37..af08bd75c3 100644
--- a/compiler/backend/word_allocScript.sml
+++ b/compiler/backend/word_allocScript.sml
@@ -298,6 +298,10 @@ val ssa_cc_trans_def = Define`
     let num' = option_lookup ssa num in
     let mov = Move 0 [(2,num')] in
     (Seq mov (Raise 2),ssa,na)) ∧
+  (ssa_cc_trans (OpCurrHeap b num1 num2) ssa na=
+    let num1' = option_lookup ssa num1 in
+    let num2' = option_lookup ssa num2 in
+    (OpCurrHeap b num1' num2',ssa,na)) ∧
   (ssa_cc_trans (Return num1 num2) ssa na=
     let num1' = option_lookup ssa num1 in
     let num2' = option_lookup ssa num2 in
@@ -483,6 +487,7 @@ val apply_colour_def = Define `
   (apply_colour f (Return num1 num2) = Return (f num1) (f num2)) ∧
   (apply_colour f Tick = Tick) ∧
   (apply_colour f (Set n exp) = Set n (apply_colour_exp f exp)) ∧
+  (apply_colour f (OpCurrHeap b n1 n2) = OpCurrHeap b (f n1) (f n2)) ∧
   (apply_colour f p = p )`
 
 val _ = export_rewrites ["apply_nummap_key_def","apply_colour_exp_def"
@@ -622,6 +627,7 @@ val get_live_def = Define`
   (get_live Tick live = live) ∧
   (get_live (LocValue r l1) live = delete r live) ∧
   (get_live (Set n exp) live = union (get_live_exp exp) live) ∧
+  (get_live (OpCurrHeap b n1 n2) live = insert n2 () (delete n1 live)) ∧
   (*Cut-set must be live, args input must be live
     For tail calls, there shouldn't be a liveset since control flow will
     never return into the same instance
@@ -863,6 +869,7 @@ val get_clash_tree_def = Define`
   (get_clash_tree Tick = Delta [] []) ∧
   (get_clash_tree (LocValue r l1) = Delta [r] []) ∧
   (get_clash_tree (Set n exp) = Delta [] (get_reads_exp exp)) ∧
+  (get_clash_tree (OpCurrHeap b _ num) = Delta [] [num]) ∧
   (get_clash_tree (Call ret dest args h) =
     let args_set = numset_list_insert args LN in
     dtcase ret of
diff --git a/compiler/backend/word_to_stackScript.sml b/compiler/backend/word_to_stackScript.sml
index ef304cbe21..b0ec8866eb 100644
--- a/compiler/backend/word_to_stackScript.sml
+++ b/compiler/backend/word_to_stackScript.sml
@@ -252,6 +252,9 @@ val comp_def = Define `
      let (xs,x) = wReg1 v1 kf in
        (wStackLoad xs (SeqStackFree (FST (SND kf)) (Return x 1)),bs)) /\
   (comp (Raise v) bs kf = (Call NONE (INL raise_stub_location) NONE,bs)) /\
+  (comp (OpCurrHeap b dst src) bs kf =
+     let (xs,src_r) = wReg1 src kf in
+       (wStackLoad xs (wRegWrite1 (\dst_r. OpCurrHeap b dst_r src_r) dst kf),bs)) /\
   (comp (Tick) bs kf = (Tick,bs)) /\
   (comp (MustTerminate p1) gs kf = comp p1 gs kf) /\
   (comp (Seq p1 p2) bs kf =

From b894b93979238931cc12b13b3c7812b4bc1c5716 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Thu, 12 Nov 2020 22:30:35 +0100
Subject: [PATCH 08/15] More progress on #796

---
 .../backend/proofs/word_allocProofScript.sml  | 191 ++++++++++++------
 .../backend/proofs/word_depthProofScript.sml  |   4 +
 .../backend/proofs/word_elimProofScript.sml   |   9 +
 .../backend/proofs/word_instProofScript.sml   |  48 ++---
 .../backend/proofs/word_simpProofScript.sml   |  12 +-
 .../proofs/word_to_wordProofScript.sml        |  30 ++-
 .../backend/semantics/wordPropsScript.sml     |   8 +-
 compiler/backend/word_allocScript.sml         |  18 +-
 compiler/backend/word_instScript.sml          |   4 +
 compiler/backend/word_simpScript.sml          |   3 +
 10 files changed, 214 insertions(+), 113 deletions(-)

diff --git a/compiler/backend/proofs/word_allocProofScript.sml b/compiler/backend/proofs/word_allocProofScript.sml
index 0c580c1803..51d096cbe1 100644
--- a/compiler/backend/proofs/word_allocProofScript.sml
+++ b/compiler/backend/proofs/word_allocProofScript.sml
@@ -1197,7 +1197,7 @@ Proof
     impl_tac>-
       (unabbrev_all_tac>>full_simp_tac(srw_ss())[state_component_equality])>>
     srw_tac[][]>>full_simp_tac(srw_ss())[]>>NO_TAC)
-   >- (*Seq*)
+  >- (*Seq*)
     (srw_tac[][]>>fs[evaluate_def,colouring_ok_def,LET_THM,get_live_def]>>
     last_assum(qspecl_then[`p`,`st`,`cst`,`f`,`get_live p0 live`]
       mp_tac)>>
@@ -1347,7 +1347,20 @@ Proof
     TOP_CASE_TAC>>full_simp_tac(srw_ss())[])
   >- (* Tick *)
     (exists_tac>>IF_CASES_TAC>>full_simp_tac(srw_ss())[call_env_def, flush_state_def,dec_clock_def])
-  >- (*LocValue*)
+  >- (* OpCurrHeap *)
+    (exists_tac>>
+    full_simp_tac(srw_ss())[evaluate_def,LET_THM,word_state_eq_rel_def,
+      get_live_def,colouring_ok_def,word_exp_def,the_words_def] >>
+    Cases_on ‘lookup n0 st.locals’ THEN1 fs [] >>
+    ‘lookup (f n0) cst.locals = lookup n0 st.locals’ by fs [strong_locals_rel_def] >>
+    fs [] >> Cases_on ‘x’ >> fs [] >>
+    Cases_on ‘FLOOKUP st.store CurrHeap’ >> fs [] >> Cases_on ‘x’ >> fs []>>
+    EVERY_CASE_TAC>>fs [set_var_def]>>
+    match_mp_tac strong_locals_rel_insert >>
+    fs [get_writes_def,domain_union] >>
+    metis_tac[INSERT_SING_UNION,strong_locals_rel_subset,SUBSET_OF_INSERT
+             ,strong_locals_rel_insert,SUBSET_UNION])
+  >- (* LocValue *)
     (exists_tac>>fs[set_var_def,strong_locals_rel_def]>>rw[]>>
     fs[lookup_insert]>>
     Cases_on`n'=n`>>fs[]>>
@@ -1359,7 +1372,7 @@ Proof
       rpt (pop_assum kall_tac)>>
       simp[])>>
     fs[])
-  >-
+  >- (* Install *)
     (exists_tac>>
     pairarg_tac>>fs[case_eq_thms]>>
     pop_assum mp_tac>>pairarg_tac>>strip_tac>>rfs[case_eq_thms]>>rw[]>>
@@ -1389,14 +1402,14 @@ Proof
     match_mp_tac (GEN_ALL strong_locals_rel_subset|>SIMP_RULE std_ss[Once CONJ_COMM])>>
     asm_exists_tac>>
     fs[SUBSET_DEF])
-  >- (*DBW*)
+  >- (* DBW *)
     (exists_tac>>pairarg_tac>>fs[case_eq_thms]>>
     imp_res_tac strong_locals_rel_get_var>>fs[list_insert_def]>>
     rw[]>>fs[]>>
     match_mp_tac (GEN_ALL strong_locals_rel_subset|>SIMP_RULE std_ss[Once CONJ_COMM])>>
     asm_exists_tac>>
     fs[SUBSET_DEF])
-    >> (* FFI *)
+  >> (* FFI *)
      (exists_tac>>Cases_on`get_var n st`>>Cases_on`get_var n0 st`>>
       Cases_on`get_var n1 st`>>Cases_on`get_var n2 st`>>
       full_simp_tac(srw_ss())[get_writes_def,LET_THM,get_var_perm]>>
@@ -1448,11 +1461,12 @@ val get_clash_sets_hd = Q.prove(
     full_simp_tac(srw_ss())[get_live_def,LET_THM]>>metis_tac[]);
 
 (*The liveset passed in at the back is always satisfied*)
-val get_clash_sets_tl = Q.prove(
-`∀prog live f.
+Theorem get_clash_sets_tl[local]:
+ ∀prog live f.
   let (hd,ls) = get_clash_sets prog live in
   EVERY (λs. INJ f (domain s) UNIV) ls ⇒
-  INJ f (domain live) UNIV`,
+  INJ f (domain live) UNIV
+Proof
   completeInduct_on`prog_size (K 0) prog`>>
   full_simp_tac(srw_ss())[PULL_FORALL]>>
   rpt strip_tac>>
@@ -1479,8 +1493,8 @@ val get_clash_sets_tl = Q.prove(
     TRY(first_x_assum(qspecl_then[`p0`,`live`,`f`]mp_tac)>>
     impl_tac>-size_tac>>srw_tac[][]>>
     full_simp_tac(srw_ss())[UNCURRY])
-  >- metis_tac[INJ_UNION,domain_union,INJ_SUBSET,SUBSET_UNION]
-  >- metis_tac[INJ_UNION,domain_union,INJ_SUBSET,SUBSET_UNION]);
+  >> metis_tac[INJ_UNION,domain_union,INJ_SUBSET,SUBSET_UNION]
+QED
 
 Theorem colouring_ok_alt_thm:
  ∀f prog live.
@@ -1921,6 +1935,13 @@ val subset_tac =
   HINT_EXISTS_TAC>>fs[domain_numset_list_insert_eq_union,SUBSET_DEF]>>
   simp[domain_union];
 
+Theorem IMAGE_DIFF:
+  INJ f (s UNION t) UNIV ⇒
+  IMAGE f (s DIFF t) = IMAGE f s DIFF IMAGE f t
+Proof
+  fs [EXTENSION,INJ_DEF] \\ rw [] \\ metis_tac []
+QED
+
 Theorem clash_tree_colouring_ok:
     ∀prog f live flive livein flivein.
   wf_cutsets prog ∧
@@ -2172,7 +2193,7 @@ Proof
     drule check_partial_col_INJ>> rpt (disch_then drule)>>
     rw[hide_def,numset_list_insert_def,list_insert_def]>>
     fs[domain_insert])
-  >-
+  >- (* FFI *)
     (EVERY_CASE_TAC>>fs[]>>
     imp_res_tac check_col_INJ>>
     fs[numset_list_delete_def]>>
@@ -2180,31 +2201,43 @@ Proof
     rpt (qpat_x_assum `!P. Q` kall_tac)>>
     rfs[AND_IMP_INTRO]>>
     fs[hide_def,numset_list_insert_def,wf_cutsets_def])
-  >-
+  >- (* Raise *)
     (start_tac>>
     fs[numset_list_delete_def,numset_list_insert_def]>>
     metis_tac[INSERT_SING_UNION,UNION_COMM])
-  >-
+  >- (* Return *)
     (start_tac>>
     fs[numset_list_delete_def,numset_list_insert_def]>>
     `domain live ∪ {num1;num2} = num1 INSERT num2 INSERT domain live` by
       (fs[EXTENSION]>>metis_tac[])>>
     fs[])
-  >-
+  >- (* Tick *)
     (start_tac>>
     fs[numset_list_delete_def,numset_list_insert_def])
-  >-
+  >- (* LocValue *)
     (start_tac>>
     fs[numset_list_delete_def,numset_list_insert_def,domain_union,DELETE_DEF,UNION_COMM]>>
     CONJ_TAC>- subset_tac>>
     fs[INJ_IMP_IMAGE_DIFF_single])
-  >-
+  >- (* Set *)
     (start_tac>>
     fs[numset_list_delete_def,numset_list_insert_def,domain_union,DELETE_DEF,UNION_COMM,get_reads_exp_get_live_exp]>>
     match_mp_tac numset_list_insert_eq_UNION>>
     fs[wf_get_live_exp,get_reads_exp_get_live_exp])
-  >-
-    (*Call*)
+  >- (* OpCurrHeap *)
+    (start_tac>>
+    fs[numset_list_delete_def,numset_list_insert_def,domain_union,DELETE_DEF,
+       UNION_COMM,get_reads_exp_get_live_exp]>>
+    ‘INJ f (domain live DIFF {dst}) 𝕌(:num)’ by
+      (qpat_x_assum ‘INJ f (domain live ∪ {dst}) 𝕌(:num)’ mp_tac
+       \\ rpt (pop_assum kall_tac)
+       \\ rewrite_tac [INJ_DEF,IN_DIFF,IN_UNION,NOT_IN_EMPTY,IN_UNIV,IN_INSERT]
+       \\ metis_tac [])
+    \\ gvs [IMAGE_DIFF] \\ rw []
+    \\ rpt (pop_assum mp_tac)
+    \\ rewrite_tac [INJ_DEF,IN_UNION,IN_INSERT]
+    \\ metis_tac [])
+  >- (*Call*)
     (Cases_on`ret`>>fs[]
     >-
       (fs[check_clash_tree_def,hide_def,wf_cutsets_def,colouring_ok_def,get_live_def,get_writes_def]>>
@@ -2685,6 +2718,8 @@ Proof
     rm_tac
   >- (* get *)
     rm_tac
+  >- (* OpCurrHeap *)
+    cheat
   >- (* loc value *)
     rm_tac
   >- (* seq *)
@@ -2706,8 +2741,7 @@ Proof
     rpt var_eq_tac>>fs[evaluate_def]>>
     first_x_assum (qspecl_then [`st with <|clock := MustTerminate_limit (:'a) ; termdep := st.termdep -1|>` ] mp_tac)>>
     fs[]>>disch_then drule>>rw[]>>fs[state_component_equality])
-   >-
-    (* if *)
+  >- (* if *)
     (rpt (pairarg_tac>>fs[])>>
     qpat_x_assum`A=(res,rst)` mp_tac>>
     ntac 4 (TOP_CASE_TAC>>fs[])>>
@@ -2722,10 +2756,6 @@ Proof
     TRY(first_assum match_mp_tac>>fs[strong_locals_rel_def,domain_union]>>
     NO_TAC)>>
     last_assum match_mp_tac>>fs[strong_locals_rel_def,domain_union])
-
-
-
-
   >- (*call*)
     (qpat_x_assum`A=(res,rst)` mp_tac>>
     ntac 7 (TOP_CASE_TAC>>fs[])>>
@@ -2863,7 +2893,9 @@ Proof
       pop_assum(qspecl_then[`t`,`domain v40`] mp_tac)>>
       impl_tac>- (fs[strong_locals_rel_def]>>metis_tac[]))>>
     rw[state_component_equality]>>
-    fs[strong_locals_rel_def])
+    fs[strong_locals_rel_def] >>
+    fs [PULL_EXISTS,get_var_def] >>
+    metis_tac [])
   >- (* CBW *)
     (fs[case_eq_thms,list_insert_def]>>
     imp_res_tac strong_locals_rel_I_get_var>>
@@ -4048,7 +4080,7 @@ val ssa_map_ok_inter = Q.prove(`
 
 
 (*Prove the properties that hold of ssa_cc_trans independent of semantics*)
-val ssa_cc_trans_props = Q.prove(`
+Theorem ssa_cc_trans_props[local]:
   ∀prog ssa na prog' ssa' na'.
   ssa_cc_trans prog ssa na = (prog',ssa',na') ∧
   ssa_map_ok na ssa ∧
@@ -4056,7 +4088,8 @@ val ssa_cc_trans_props = Q.prove(`
   ⇒
   na ≤ na' ∧
   is_alloc_var na' ∧
-  ssa_map_ok na' ssa'`,
+  ssa_map_ok na' ssa'
+Proof
   ho_match_mp_tac ssa_cc_trans_ind>>
   full_simp_tac(srw_ss())[ssa_cc_trans_def]>>
   strip_tac >-
@@ -4107,6 +4140,8 @@ val ssa_cc_trans_props = Q.prove(`
     exp_tac>>
   strip_tac >-
     exp_tac>>
+  strip_tac >-
+    exp_tac>>
   strip_tac >-
     (* Install *)
     (rpt gen_tac>> strip_tac>>
@@ -4226,7 +4261,8 @@ val ssa_cc_trans_props = Q.prove(`
       full_simp_tac(srw_ss())[next_var_rename_def]>>
       DECIDE_TAC)>>
     imp_res_tac fix_inconsistencies_props>>
-    DECIDE_TAC);
+    DECIDE_TAC
+QED
 
 val PAIR_ZIP_MEM = Q.prove(`
   LENGTH c = LENGTH d ∧
@@ -5905,6 +5941,20 @@ Proof
   >- (* Tick *)
     (exists_tac>>
     EVERY_CASE_TAC>>full_simp_tac(srw_ss())[call_env_def, flush_state_def,dec_clock_def])
+  >- (* OpCurrHeap *)
+    (exists_tac>>
+    fs [word_exp_def,the_words_def] >>
+    Cases_on ‘lookup n0 st.locals’ >> fs []>> Cases_on ‘x’ \\ fs []>>
+    Cases_on ‘FLOOKUP st.store CurrHeap’ >> fs []>> Cases_on ‘x’ \\ fs []>>
+    Cases_on ‘word_op b [c; c']’ >> fs [] >>
+    full_simp_tac(srw_ss())[next_var_rename_def,ssa_cc_trans_inst_def,inst_def,
+      assign_def,word_exp_perm,evaluate_def,LET_THM,word_exp_def,the_words_def] >>
+    imp_res_tac ssa_locals_rel_get_var >>
+    fs[set_vars_def,get_var_def,lookup_alist_insert]>>
+    first_x_assum drule >> fs [set_var_def] >>
+    full_simp_tac(srw_ss())[ssa_locals_rel_def]>>
+    srw_tac[][]>>full_simp_tac(srw_ss())[lookup_insert] >>
+    pop_assum mp_tac >> cheat)
   >-
     exp_tac
   >- (* Install *)
@@ -6729,12 +6779,13 @@ val fake_moves_distinct_tar_reg = Q.prove(`
   unabbrev_all_tac>>
   metis_tac[fake_move_def,every_inst_def,distinct_tar_reg_def]);
 
-val ssa_cc_trans_distinct_tar_reg = Q.prove(`
+Theorem ssa_cc_trans_distinct_tar_reg:
   ∀prog ssa na.
-  is_alloc_var na ∧
-  every_var (λx. x < na) prog ∧
-  ssa_map_ok na ssa ⇒
-  every_inst distinct_tar_reg (FST (ssa_cc_trans prog ssa na))`,
+    is_alloc_var na ∧
+    every_var (λx. x < na) prog ∧
+    ssa_map_ok na ssa ⇒
+    every_inst distinct_tar_reg (FST (ssa_cc_trans prog ssa na))
+Proof
   ho_match_mp_tac ssa_cc_trans_ind>>full_simp_tac(srw_ss())[ssa_cc_trans_def]>>srw_tac[][]>>
   unabbrev_all_tac>>
   full_simp_tac(srw_ss())[every_inst_def]>>imp_res_tac ssa_cc_trans_props>>full_simp_tac(srw_ss())[]
@@ -6769,6 +6820,14 @@ val ssa_cc_trans_distinct_tar_reg = Q.prove(`
   >> TRY
     (full_simp_tac(srw_ss())[list_next_var_rename_move_def]>>rpt (pop_assum mp_tac)>>
     LET_ELIM_TAC>>full_simp_tac(srw_ss())[every_inst_def,EQ_SYM_EQ]>>NO_TAC)
+  >-
+   (rename [‘OpCurrHeap’]>>
+    full_simp_tac(srw_ss())[ssa_cc_trans_inst_def,LET_THM,next_var_rename_def]>>
+    every_case_tac>> rw[]>>
+    fs[every_var_def,every_var_inst_def,every_var_imm_def,every_inst_def]>>
+    full_simp_tac(srw_ss())[distinct_tar_reg_def,ssa_map_ok_def,option_lookup_def]>>
+    EVERY_CASE_TAC>>srw_tac[][]>>res_tac>>full_simp_tac(srw_ss())[]>>
+    fs[is_alloc_var_def]>>CCONTR_TAC>>fs[])
   >>
   FULL_CASE_TAC>>full_simp_tac(srw_ss())[every_var_def,every_inst_def]
   >-
@@ -6834,11 +6893,12 @@ val ssa_cc_trans_distinct_tar_reg = Q.prove(`
       full_simp_tac(srw_ss())[list_next_var_rename_move_def]>>
       rpt(qpat_x_assum`A=(B,C,D)` mp_tac)>>
       LET_ELIM_TAC>>full_simp_tac(srw_ss())[EQ_SYM_EQ,every_inst_def]>>
-      metis_tac[fake_moves_distinct_tar_reg]);
+      metis_tac[fake_moves_distinct_tar_reg]
+QED
 
 Theorem full_ssa_cc_trans_distinct_tar_reg:
-    ∀n prog.
-  every_inst distinct_tar_reg (full_ssa_cc_trans n prog)
+  ∀n prog.
+    every_inst distinct_tar_reg (full_ssa_cc_trans n prog)
 Proof
   srw_tac[][]>>
   full_simp_tac(srw_ss())[full_ssa_cc_trans_def]>>
@@ -6862,7 +6922,7 @@ Proof
   full_simp_tac(srw_ss())[]
 QED
 
-val fake_moves_conventions2 = Q.prove(`
+Theorem fake_moves_conventions2[local]:
   ∀ls ssal ssar na l r a b c conf.
   fake_moves ls ssal ssar na = (l,r,a,b,c) ⇒
   flat_exp_conventions l ∧
@@ -6870,12 +6930,14 @@ val fake_moves_conventions2 = Q.prove(`
   full_inst_ok_less conf l ∧
   full_inst_ok_less conf r ∧
   every_inst distinct_tar_reg l ∧
-  every_inst distinct_tar_reg r`,
+  every_inst distinct_tar_reg r
+Proof
   Induct>>full_simp_tac(srw_ss())[fake_moves_def]>>srw_tac[][]>>full_simp_tac(srw_ss())[flat_exp_conventions_def,full_inst_ok_less_def,every_inst_def]>>
   pop_assum mp_tac>> LET_ELIM_TAC>> EVERY_CASE_TAC>> full_simp_tac(srw_ss())[LET_THM]>>
   unabbrev_all_tac>>
   rveq>>fs[flat_exp_conventions_def,fake_move_def,full_inst_ok_less_def,inst_ok_less_def,every_inst_def,distinct_tar_reg_def]>>
-  metis_tac[]);
+  metis_tac[]
+QED
 
 val ssa_cc_trans_flat_exp_conventions = Q.prove(`
   ∀prog ssa na.
@@ -6928,13 +6990,14 @@ QED
 
 val _ = diminish_srw_ss ["NORMEQ_ss"];
 
-val ssa_cc_trans_full_inst_ok_less = Q.prove(`
+Theorem ssa_cc_trans_full_inst_ok_less[local]:
   ∀prog ssa na c.
-  every_var (λx. x < na) prog ∧
-  is_alloc_var na ∧
-  ssa_map_ok na ssa ∧
-  full_inst_ok_less c prog ⇒
-  full_inst_ok_less c (FST (ssa_cc_trans prog ssa na))`,
+    every_var (λx. x < na) prog ∧
+    is_alloc_var na ∧
+    ssa_map_ok na ssa ∧
+    full_inst_ok_less c prog ⇒
+    full_inst_ok_less c (FST (ssa_cc_trans prog ssa na))
+Proof
   ho_match_mp_tac ssa_cc_trans_ind>>full_simp_tac(srw_ss())[ssa_cc_trans_def]>>srw_tac[][]>>
   unabbrev_all_tac>>
   full_simp_tac(srw_ss())[full_inst_ok_less_def]
@@ -7041,7 +7104,8 @@ val ssa_cc_trans_full_inst_ok_less = Q.prove(`
           (match_mp_tac (GEN_ALL ssa_map_ok_more)>>
           qexists_tac`n'`>>fs[])>>
         metis_tac[convention_partitions])
-    >- metis_tac[fake_moves_conventions2,full_inst_ok_less_def]);
+    >- metis_tac[fake_moves_conventions2,full_inst_ok_less_def]
+QED
 
 Theorem full_ssa_cc_trans_full_inst_ok_less:
     ∀prog n c.
@@ -7317,16 +7381,19 @@ Proof
 QED
 
 (*word_alloc preserves syntactic conventions*)
-val word_alloc_two_reg_inst_lem = Q.prove(`
+Theorem word_alloc_two_reg_inst_lem[local]:
   ∀f prog.
   every_inst two_reg_inst prog ⇒
-  every_inst two_reg_inst (apply_colour f prog)`,
+  every_inst two_reg_inst (apply_colour f prog)
+Proof
   ho_match_mp_tac apply_colour_ind>>full_simp_tac(srw_ss())[every_inst_def]>>srw_tac[][]
   >-
     (Cases_on`i`>>TRY(Cases_on`a`)>>TRY(Cases_on`m`)>>TRY(Cases_on`f'`)>>
     full_simp_tac(srw_ss())[apply_colour_inst_def,two_reg_inst_def])
   >>
-    EVERY_CASE_TAC>>unabbrev_all_tac>>full_simp_tac(srw_ss())[every_inst_def]);
+    EVERY_CASE_TAC>>unabbrev_all_tac>>full_simp_tac(srw_ss())[every_inst_def]>>
+    full_simp_tac(srw_ss())[apply_colour_inst_def,two_reg_inst_def]
+QED
 
 Theorem word_alloc_two_reg_inst:
     ∀fc c alg k prog col_opt.
@@ -7451,14 +7518,16 @@ Proof
   fs[]
 QED
 
-val apply_colour_lab_pres = Q.prove(`
+Theorem apply_colour_lab_pres[local]:
   ∀col prog.
-  extract_labels prog = extract_labels (apply_colour col prog)`,
+    extract_labels prog = extract_labels (apply_colour col prog)
+Proof
   ho_match_mp_tac apply_colour_ind>>fs[extract_labels_def]>>rw[]>>
-  EVERY_CASE_TAC>>fs[]);
+  EVERY_CASE_TAC>>fs[]
+QED
 
 Theorem word_alloc_lab_pres:
-    extract_labels prog = extract_labels (word_alloc fc c alg k prog col_opt)
+  extract_labels prog = extract_labels (word_alloc fc c alg k prog col_opt)
 Proof
   fs[word_alloc_def,oracle_colour_ok_def]>>
   EVERY_CASE_TAC>>fs[]>>
@@ -7471,14 +7540,14 @@ QED
 val convs = [flat_exp_conventions_def,full_inst_ok_less_def,every_inst_def,pre_alloc_conventions_def,call_arg_convention_def,every_stack_var_def,every_var_def,extract_labels_def,wf_cutsets_def];
 
 Theorem remove_dead_conventions:
-   ∀p live c k.
-  let comp = FST (remove_dead p live) in
-  (flat_exp_conventions p ⇒ flat_exp_conventions comp) ∧
-  (full_inst_ok_less c p ⇒ full_inst_ok_less c comp) ∧
-  (pre_alloc_conventions p ⇒ pre_alloc_conventions comp) ∧
-  (every_inst distinct_tar_reg p ⇒ every_inst distinct_tar_reg comp) ∧
-  (wf_cutsets p ⇒ wf_cutsets comp) ∧
-  (extract_labels p = extract_labels comp)
+  ∀p live c k.
+    let comp = FST (remove_dead p live) in
+    (flat_exp_conventions p ⇒ flat_exp_conventions comp) ∧
+    (full_inst_ok_less c p ⇒ full_inst_ok_less c comp) ∧
+    (pre_alloc_conventions p ⇒ pre_alloc_conventions comp) ∧
+    (every_inst distinct_tar_reg p ⇒ every_inst distinct_tar_reg comp) ∧
+    (wf_cutsets p ⇒ wf_cutsets comp) ∧
+    (extract_labels p = extract_labels comp)
 Proof
   ho_match_mp_tac remove_dead_ind>>rw[]>>
   fs[remove_dead_def]>>
diff --git a/compiler/backend/proofs/word_depthProofScript.sml b/compiler/backend/proofs/word_depthProofScript.sml
index 215e0f3b59..4996269068 100644
--- a/compiler/backend/proofs/word_depthProofScript.sml
+++ b/compiler/backend/proofs/word_depthProofScript.sml
@@ -275,6 +275,10 @@ Proof
    (fs [wordSemTheory.evaluate_def] \\ rveq
     \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs []
     \\ fs [])
+  THEN1 (* OpCurrHeap *)
+   (fs [wordSemTheory.evaluate_def] \\ rveq
+    \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs []
+    \\ fs [])
   THEN1 (* Store *)
    (fs [wordSemTheory.evaluate_def,mem_store_def] \\ rveq
     \\ fs [CaseEq"option",CaseEq"word_loc",bool_case_eq] \\ rveq \\ fs []
diff --git a/compiler/backend/proofs/word_elimProofScript.sml b/compiler/backend/proofs/word_elimProofScript.sml
index d852a2c5a2..b74b427f7e 100644
--- a/compiler/backend/proofs/word_elimProofScript.sml
+++ b/compiler/backend/proofs/word_elimProofScript.sml
@@ -141,6 +141,7 @@ Proof
     >- (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)` >>
@@ -1559,6 +1560,14 @@ Proof
             fs[SUBSET_DEF]) >>
         fs[SUBSET_DEF] >> metis_tac[]
         )
+    >- ( (* OpCurrHeap *)
+        simp[wordSemTheory.evaluate_def,word_exp_def,the_words_def]
+        \\ simp [AllCaseEqs(),PULL_EXISTS] \\ rpt gen_tac \\ strip_tac
+        \\ gvs [dest_result_loc_def,set_var_def]
+        \\ fs[word_state_rel_def, domain_find_loc_state, dest_result_loc_def]
+        \\ qspecl_then [`dst`, `Word z`, `s.locals`] mp_tac get_locals_insert
+        \\ fs[dest_word_loc_def] \\ metis_tac[SUBSET_TRANS]
+        )
     >- ( (* Set *)
         simp[wordSemTheory.evaluate_def] >>
         Cases_on `v = Handler ∨ v = BitmapBase` >> fs[] >>
diff --git a/compiler/backend/proofs/word_instProofScript.sml b/compiler/backend/proofs/word_instProofScript.sml
index 173062a19a..7b22959dd9 100644
--- a/compiler/backend/proofs/word_instProofScript.sml
+++ b/compiler/backend/proofs/word_instProofScript.sml
@@ -590,7 +590,7 @@ Theorem inst_select_thm:
 Proof
   ho_match_mp_tac inst_select_ind>>srw_tac[][]>>
   full_simp_tac(srw_ss())[inst_select_def,locals_rel_evaluate_thm]
-  >-
+  >- (* Assign *)
     (full_simp_tac(srw_ss())[evaluate_def]>>last_x_assum mp_tac>>FULL_CASE_TAC>>srw_tac[][]>>
     full_simp_tac(srw_ss())[every_var_def]>>
     imp_res_tac pull_exp_every_var_exp>>
@@ -606,7 +606,7 @@ Proof
     srw_tac[][]>>full_simp_tac(srw_ss())[lookup_insert]>>
     IF_CASES_TAC>>fs[]>>
     metis_tac[])
-  >-
+  >- (* Set *)
     (full_simp_tac(srw_ss())[evaluate_def]>>last_x_assum mp_tac>>
     ntac 2 FULL_CASE_TAC>>full_simp_tac(srw_ss())[]>>strip_tac>>
     full_simp_tac(srw_ss())[every_var_def]>>
@@ -819,8 +819,8 @@ val inst_select_exp_flat_exp_conventions = Q.prove(`
   EVERY_CASE_TAC>>full_simp_tac(srw_ss())[flat_exp_conventions_def,inst_select_exp_def,LET_THM]);
 
 Theorem inst_select_flat_exp_conventions:
-    ∀c temp prog.
-  flat_exp_conventions (inst_select c temp prog)
+  ∀c temp prog.
+    flat_exp_conventions (inst_select c temp prog)
 Proof
   ho_match_mp_tac inst_select_ind >>srw_tac[][]>>
   full_simp_tac(srw_ss())[flat_exp_conventions_def,inst_select_def,LET_THM]>>
@@ -840,11 +840,11 @@ val inst_select_exp_full_inst_ok_less = Q.prove(`
   );
 
 Theorem inst_select_full_inst_ok_less:
-    ∀c temp prog.
-  addr_offset_ok c 0w ∧
-  every_inst (inst_ok_less c) prog
-  ⇒
-  full_inst_ok_less c (inst_select c temp prog)
+  ∀c temp prog.
+    addr_offset_ok c 0w ∧
+    every_inst (inst_ok_less c) prog
+    ⇒
+    full_inst_ok_less c (inst_select c temp prog)
 Proof
   ho_match_mp_tac inst_select_ind>>
   rw[inst_select_def,full_inst_ok_less_def,every_inst_def]>>
@@ -857,11 +857,11 @@ QED
 
 (*Semantics preservation*)
 Theorem three_to_two_reg_correct:
-    ∀prog s res s'.
-  every_inst distinct_tar_reg prog ∧
-  evaluate (prog,s) = (res,s') ∧ res ≠ SOME Error
-  ⇒
-  evaluate(three_to_two_reg prog,s) = (res,s')
+  ∀prog s res s'.
+    every_inst distinct_tar_reg prog ∧
+    evaluate (prog,s) = (res,s') ∧ res ≠ SOME Error
+    ⇒
+    evaluate(three_to_two_reg prog,s) = (res,s')
 Proof
   ho_match_mp_tac three_to_two_reg_ind>>
   srw_tac[][]>>full_simp_tac(srw_ss())[three_to_two_reg_def,evaluate_def,state_component_equality]>>
@@ -903,20 +903,20 @@ QED
 
 (* Syntactic three_to_two_reg *)
 Theorem three_to_two_reg_two_reg_inst:
-    ∀prog. every_inst two_reg_inst (three_to_two_reg prog)
+  ∀prog. every_inst two_reg_inst (three_to_two_reg prog)
 Proof
   ho_match_mp_tac three_to_two_reg_ind>>srw_tac[][]>>full_simp_tac(srw_ss())[every_inst_def,two_reg_inst_def,three_to_two_reg_def,LET_THM]>>EVERY_CASE_TAC>>full_simp_tac(srw_ss())[]
 QED
 
 Theorem three_to_two_reg_wf_cutsets:
-   ∀prog. wf_cutsets prog ⇒ wf_cutsets (three_to_two_reg prog)
+  ∀prog. wf_cutsets prog ⇒ wf_cutsets (three_to_two_reg prog)
 Proof
   ho_match_mp_tac three_to_two_reg_ind>>srw_tac[][]>>
   full_simp_tac(srw_ss())[wf_cutsets_def,three_to_two_reg_def,LET_THM]>>EVERY_CASE_TAC>>full_simp_tac(srw_ss())[]
 QED
 
 Theorem three_to_two_reg_pre_alloc_conventions:
-   ∀prog. pre_alloc_conventions prog ⇒ pre_alloc_conventions (three_to_two_reg prog)
+  ∀prog. pre_alloc_conventions prog ⇒ pre_alloc_conventions (three_to_two_reg prog)
 Proof
   ho_match_mp_tac three_to_two_reg_ind>>srw_tac[][]>>
   full_simp_tac(srw_ss())[pre_alloc_conventions_def,every_stack_var_def,three_to_two_reg_def,LET_THM,call_arg_convention_def,inst_arg_convention_def]>>
@@ -927,15 +927,15 @@ Proof
 QED
 
 Theorem three_to_two_reg_flat_exp_conventions:
-   ∀prog. flat_exp_conventions prog ⇒ flat_exp_conventions (three_to_two_reg prog)
+  ∀prog. flat_exp_conventions prog ⇒ flat_exp_conventions (three_to_two_reg prog)
 Proof
   ho_match_mp_tac three_to_two_reg_ind>>srw_tac[][]>>
   full_simp_tac(srw_ss())[flat_exp_conventions_def,three_to_two_reg_def,LET_THM]>>EVERY_CASE_TAC>>full_simp_tac(srw_ss())[]
 QED
 
 Theorem three_to_two_reg_full_inst_ok_less:
-   ∀prog. full_inst_ok_less c prog ⇒
-  full_inst_ok_less c (three_to_two_reg prog)
+  ∀prog. full_inst_ok_less c prog ⇒
+         full_inst_ok_less c (three_to_two_reg prog)
 Proof
   ho_match_mp_tac three_to_two_reg_ind>>srw_tac[][]>>
   full_simp_tac(srw_ss())[three_to_two_reg_def,LET_THM]>>EVERY_CASE_TAC>>fs[full_inst_ok_less_def]
@@ -955,8 +955,8 @@ val inst_select_exp_no_lab = Q.prove(`
   rpt(TOP_CASE_TAC>>fs[extract_labels_def,inst_select_exp_def]))
 
 Theorem inst_select_lab_pres:
-    ∀c temp prog.
-  extract_labels prog = extract_labels (inst_select c temp prog)
+  ∀c temp prog.
+    extract_labels prog = extract_labels (inst_select c temp prog)
 Proof
   ho_match_mp_tac inst_select_ind>>rw[inst_select_def,extract_labels_def]>>
   TRY(metis_tac[inst_select_exp_no_lab])>>
@@ -965,8 +965,8 @@ Proof
 QED
 
 Theorem three_to_two_reg_lab_pres:
-    ∀prog.
-  extract_labels prog = extract_labels (three_to_two_reg prog)
+  ∀prog.
+    extract_labels prog = extract_labels (three_to_two_reg prog)
 Proof
   ho_match_mp_tac three_to_two_reg_ind>>rw[three_to_two_reg_def,extract_labels_def]>>EVERY_CASE_TAC>>fs[]
 QED
diff --git a/compiler/backend/proofs/word_simpProofScript.sml b/compiler/backend/proofs/word_simpProofScript.sml
index 06a857093e..ab6cda6bc0 100644
--- a/compiler/backend/proofs/word_simpProofScript.sml
+++ b/compiler/backend/proofs/word_simpProofScript.sml
@@ -968,6 +968,10 @@ Proof
   (fs [const_fp_loop_def] \\ rw [evaluate_def] \\
   every_case_tac \\ fs [] \\ metis_tac [cs_delete_if_set])
 
+  >- (** OpCurrHeap **)
+  (fs [const_fp_loop_def] \\ rw [evaluate_def] \\
+  every_case_tac \\ fs [] \\ metis_tac [cs_delete_if_set])
+
   >- (** MustTerminate **)
   (rpt (rpt gen_tac \\ DISCH_TAC) \\ fs [const_fp_loop_def] \\ pairarg_tac \\
   fs [] \\ qpat_x_assum `_ = p'` (assume_tac o GSYM) \\ fs [evaluate_def] \\
@@ -998,6 +1002,7 @@ Proof
     \\ (* Otherwise *)
     (rpt (pairarg_tac \\ fs []) \\ every_case_tac \\ rw [evaluate_def] \\
     res_tac \\ fs [lookup_inter_eq] \\ every_case_tac \\ rw []))
+
   >- (** Call **)
   (rpt (rpt gen_tac \\ DISCH_TAC) \\ fs [const_fp_loop_def, evaluate_def] \\
   qpat_x_assum `_ = (res, s')` mp_tac \\
@@ -1038,6 +1043,7 @@ Proof
     >- (imp_res_tac evaluate_consts \\ imp_res_tac pop_env_gc_fun \\
        fs [set_var_def, push_env_gc_fun])
     >- rw[])
+
   >- (** FFI **)
   (fs [const_fp_loop_def] \\ rw [evaluate_def] \\
   every_case_tac \\ fs [] \\
@@ -1195,9 +1201,9 @@ val Seq_assoc_no_inst = Q.prove(`
   every_case_tac>>fs[])
 
 Theorem compile_exp_no_inst:
-    ∀prog.
-  every_inst (inst_ok_less ac) prog ⇒
-  every_inst (inst_ok_less ac) (compile_exp prog)
+  ∀prog.
+    every_inst (inst_ok_less ac) prog ⇒
+    every_inst (inst_ok_less ac) (compile_exp prog)
 Proof
   fs[compile_exp_def]>>
   metis_tac[simp_if_no_inst,Seq_assoc_no_inst,every_inst_def,
diff --git a/compiler/backend/proofs/word_to_wordProofScript.sml b/compiler/backend/proofs/word_to_wordProofScript.sml
index 3b819a4880..5370e93829 100644
--- a/compiler/backend/proofs/word_to_wordProofScript.sml
+++ b/compiler/backend/proofs/word_to_wordProofScript.sml
@@ -175,7 +175,7 @@ val code_rel_union_fromAList = Q.prove(`
     first_x_assum drule>>rw[]>>
     simp[]>>metis_tac[]);
 
-val compile_single_correct = Q.prove(`
+Theorem compile_single_correct[local]:
   ∀prog (st:('a,'c,'ffi) wordSem$state) l coracle cc.
   code_rel st.code l /\
   (domain st.code = domain l) ∧
@@ -196,8 +196,8 @@ val compile_single_correct = Q.prove(`
           rst1 = rst with <|
             code:=rst1.code ;
             compile_oracle := (I ## MAP (λp. compile_single tt kk aa co (p,NONE))) o rst.compile_oracle;
-            compile:=cc |>`, (* todo: rst1.perm? *)
-
+            compile:=cc |> (* todo: rst1.perm? *)
+Proof
   (*recInduct doesn't seem to give a nice induction thm*)
   completeInduct_on`((st:('a,'c,'ffi)wordSem$state).termdep)`>>
   completeInduct_on`((st:('a,'c,'ffi)wordSem$state).clock)`>>
@@ -234,8 +234,6 @@ val compile_single_correct = Q.prove(`
     rw[] >> rw[]>>
     fs[state_component_equality])
 
-
-
   >- (*Call -- the hard case*)
     (fs[evaluate_def]>>
      TOP_CASE_TAC>> fs [] >>
@@ -547,7 +545,7 @@ val compile_single_correct = Q.prove(`
       rw[]>>fs[]>>
       pairarg_tac>>fs[]>>
       qpat_x_assum`rst1 = _` SUBST_ALL_TAC>>fs[])
-  >-
+  >- (* If *)
     (simp[evaluate_def,get_var_def,get_var_imm_def]>>
     ntac 2 (TOP_CASE_TAC>>full_simp_tac(srw_ss())[])>>
     Cases_on`r`>>full_simp_tac(srw_ss())[get_var_imm_def,get_var_def]>>
@@ -556,7 +554,7 @@ val compile_single_correct = Q.prove(`
     TRY(qpat_abbrev_tac`prog = p0`)>>
     first_x_assum(qspecl_then[`prog`,`st`,`l`,`cc`] mp_tac)>>
     (impl_tac>-size_tac>>srw_tac[][]))
-  >-
+  >- (* Alloc *)
     (qexists_tac`st.permute`>>fs[rm_perm]>>
     fs[evaluate_def,get_var_def]>>
     ntac 2 (TOP_CASE_TAC>>fs[])>>
@@ -571,10 +569,11 @@ val compile_single_correct = Q.prove(`
     Cases_on`x'`>>fs[]>>Cases_on`h`>>fs[]>>
     EVERY_CASE_TAC>>fs[has_space_def]>>
     rfs[call_env_def,flush_state_def])
-  >- tac
-  >- tac
-  >- tac
-  >- (tac \\ fs[domain_lookup] \\ metis_tac[] )
+  >- (rename [‘Raise’] \\ tac)
+  >- (rename [‘Return’] \\ tac)
+  >- (rename [‘Tick’] \\ tac)
+  >- (rename [‘OpCurrHeap’] \\ tac)
+  >- (rename [‘LocValue’] \\ tac \\ fs[domain_lookup] \\ metis_tac[])
   >- (* Install *)
     (qexists_tac`st.permute`>>fs[rm_perm]>>
     ntac 3 (last_x_assum kall_tac)>>
@@ -596,11 +595,10 @@ val compile_single_correct = Q.prove(`
       simp[domain_fromAList]>>AP_TERM_TAC>>
       simp[EXTENSION,MAP_MAP_o,compile_single_def,MEM_MAP,EXISTS_PROD])>>
     simp[state_component_equality,o_DEF])
-  >- (*CBW*) tac
-  >- (*DBW*) tac
-  >- (*FFI*)
-    (tac>>
-     Cases_on`call_FFI st.ffi s x'' x'`>>simp[]));
+  >- (rename [‘CodeBufferWrite’] \\ tac)
+  >- (rename [‘DataBufferWrite’] \\ tac)
+  >- (rename [‘FFI’] \\ tac \\ Cases_on`call_FFI st.ffi s x'' x'` \\ simp[])
+QED
 
 Theorem compile_word_to_word_thm:
      code_rel (st:('a,'c,'ffi) wordSem$state).code l ∧
diff --git a/compiler/backend/semantics/wordPropsScript.sml b/compiler/backend/semantics/wordPropsScript.sml
index 769711ce4b..f44a79d67b 100644
--- a/compiler/backend/semantics/wordPropsScript.sml
+++ b/compiler/backend/semantics/wordPropsScript.sml
@@ -2929,10 +2929,11 @@ val two_reg_inst_def = Define`
   (two_reg_inst _ ⇔ T)`
 
 (* Recursor over instructions *)
-val every_inst_def = Define`
+Definition every_inst_def:
   (every_inst P (Inst i) ⇔ P i) ∧
   (every_inst P (Seq p1 p2) ⇔ (every_inst P p1 ∧ every_inst P p2)) ∧
   (every_inst P (If cmp r1 ri c1 c2) ⇔ every_inst P c1 ∧ every_inst P c2) ∧
+  (every_inst P (OpCurrHeap bop r1 r2) ⇔ P (Arith (Binop bop r1 r2 (Reg r2)))) ∧
   (every_inst P (MustTerminate p) ⇔ every_inst P p) ∧
   (every_inst P (Call ret dest args handler)
     ⇔ (case ret of
@@ -2941,7 +2942,8 @@ val every_inst_def = Define`
       (case handler of
         NONE => T
       | SOME (n,h,l1,l2) => every_inst P h))) ∧
-  (every_inst P prog ⇔ T)`
+  (every_inst P prog ⇔ T)
+End
 
 (* Every instruction is well-formed, including the jump hidden in If *)
 val full_inst_ok_less_def = Define`
@@ -2952,8 +2954,6 @@ val full_inst_ok_less_def = Define`
     ((case ri of Imm w => c.valid_imm (INR cmp) w | _ => T) ∧
     full_inst_ok_less c c1 ∧ full_inst_ok_less c c2)) ∧
   (full_inst_ok_less c (MustTerminate p) ⇔ full_inst_ok_less c p) ∧
-  (full_inst_ok_less c (OpCurrHeap b r1 r2) ⇔
-    (c.two_reg_arith ==> (r2 = r1))) ∧
   (full_inst_ok_less c (Call ret dest args handler)
     ⇔ (case ret of
         NONE => T
diff --git a/compiler/backend/word_allocScript.sml b/compiler/backend/word_allocScript.sml
index af08bd75c3..f4688845ea 100644
--- a/compiler/backend/word_allocScript.sml
+++ b/compiler/backend/word_allocScript.sml
@@ -298,10 +298,10 @@ val ssa_cc_trans_def = Define`
     let num' = option_lookup ssa num in
     let mov = Move 0 [(2,num')] in
     (Seq mov (Raise 2),ssa,na)) ∧
-  (ssa_cc_trans (OpCurrHeap b num1 num2) ssa na=
-    let num1' = option_lookup ssa num1 in
-    let num2' = option_lookup ssa num2 in
-    (OpCurrHeap b num1' num2',ssa,na)) ∧
+  (ssa_cc_trans (OpCurrHeap b dst src) ssa na=
+    let src' = option_lookup ssa src in
+    let (dst',ssa',na') = next_var_rename dst ssa na in
+      (OpCurrHeap b dst' src',ssa',na')) ∧
   (ssa_cc_trans (Return num1 num2) ssa na=
     let num1' = option_lookup ssa num1 in
     let num2' = option_lookup ssa num2 in
@@ -686,6 +686,10 @@ val remove_dead_def = Define`
     if lookup num live = NONE then
       (Skip,live)
     else (Get num store,delete num live)) ∧
+  (remove_dead (OpCurrHeap b num src) live =
+    if lookup num live = NONE then
+      (Skip,live)
+    else (OpCurrHeap b num src,insert src () (delete num live))) ∧
   (remove_dead (LocValue r l1) live =
     if lookup r live = NONE then
       (Skip,live)
@@ -739,6 +743,7 @@ val get_writes_def = Define`
   (get_writes (Get num store) = insert num () LN) ∧
   (get_writes (LocValue r l1) = insert r () LN) ∧
   (get_writes (Install r1 _ _ _ _) = insert r1 () LN) ∧
+  (get_writes (OpCurrHeap b r1 _) = insert r1 () LN) ∧
   (get_writes prog = LN)`
 
 Theorem get_writes_pmatch:
@@ -751,6 +756,7 @@ Theorem get_writes_pmatch:
     | Get num store => insert num () LN
     | LocValue r l1 => insert r () LN
     | Install r1 _ _ _ _ => insert r1 () LN
+    | OpCurrHeap b r1 _ => insert r1 () LN
     | prog => LN
 Proof
   rpt strip_tac
@@ -869,7 +875,7 @@ val get_clash_tree_def = Define`
   (get_clash_tree Tick = Delta [] []) ∧
   (get_clash_tree (LocValue r l1) = Delta [r] []) ∧
   (get_clash_tree (Set n exp) = Delta [] (get_reads_exp exp)) ∧
-  (get_clash_tree (OpCurrHeap b _ num) = Delta [] [num]) ∧
+  (get_clash_tree (OpCurrHeap b dst src) = Delta [dst] [src]) ∧
   (get_clash_tree (Call ret dest args h) =
     let args_set = numset_list_insert args LN in
     dtcase ret of
@@ -1079,6 +1085,8 @@ val get_heu_def = Define `
     (dtcase exp of (Var r) =>
        (add1_rhs_mem r lr,calls)
     | _ => (lr,calls))) ∧ (* General Set exp ignored *)
+  (get_heu fc (OpCurrHeap b dst src) (lr,calls) =
+    (add1_lhs_reg dst (add1_rhs_reg src lr),calls)) ∧
   (get_heu fc (LocValue r l1) (lr,calls) =
     (add1_lhs_reg r lr,calls)) ∧
   (get_heu fc (Seq s1 s2) lr = get_heu fc s2 (get_heu fc s1 lr)) ∧
diff --git a/compiler/backend/word_instScript.sml b/compiler/backend/word_instScript.sml
index ca30f8715d..51c4e65959 100644
--- a/compiler/backend/word_instScript.sml
+++ b/compiler/backend/word_instScript.sml
@@ -426,6 +426,8 @@ val three_to_two_reg_def = Define`
     Seq (Move 0 [r1,r2]) (Inst (Arith (AddOverflow r1 r1 r3 r4)))) ∧
   (three_to_two_reg (Inst (Arith (SubOverflow r1 r2 r3 r4))) =
     Seq (Move 0 [r1,r2]) (Inst (Arith (SubOverflow r1 r1 r3 r4)))) ∧
+  (three_to_two_reg (OpCurrHeap bop r1 r2) =
+    Seq (Move 0 [r1,r2]) (OpCurrHeap bop r1 r1)) ∧
   (three_to_two_reg (Seq p1 p2) =
     Seq (three_to_two_reg p1) (three_to_two_reg p2)) ∧
   (three_to_two_reg (MustTerminate p1) =
@@ -459,6 +461,8 @@ Theorem three_to_two_reg_pmatch:
     Seq (Move 0 [r1,r2]) (Inst (Arith (AddOverflow r1 r1 r3 r4)))
   | (Inst (Arith (SubOverflow r1 r2 r3 r4))) =>
     Seq (Move 0 [r1,r2]) (Inst (Arith (SubOverflow r1 r1 r3 r4)))
+  | (OpCurrHeap bop r1 r2) =>
+    Seq (Move 0 [r1,r2]) (OpCurrHeap bop r1 r1)
   | (Seq p1 p2) =>
     Seq (three_to_two_reg p1) (three_to_two_reg p2)
   | (MustTerminate p1) =>
diff --git a/compiler/backend/word_simpScript.sml b/compiler/backend/word_simpScript.sml
index cd0e2497a3..f282204efe 100644
--- a/compiler/backend/word_simpScript.sml
+++ b/compiler/backend/word_simpScript.sml
@@ -322,6 +322,7 @@ val const_fp_loop_def = Define `
          | Const c => (Assign v const_fp_e, insert v c cs)
          | _ => (Assign v const_fp_e, delete v cs)) /\
   (const_fp_loop (Get v name) cs = (Get v name, delete v cs)) /\
+  (const_fp_loop (OpCurrHeap b v w) cs = (OpCurrHeap b v w, delete v cs)) /\
   (const_fp_loop (MustTerminate p) cs =
     let (p', cs') = const_fp_loop p cs in
       (MustTerminate p', cs')) /\
@@ -363,6 +364,7 @@ Theorem const_fp_loop_pmatch:
        | Const c => (Assign v (Const c), insert v c cs)
        | const_fp_e => (Assign v const_fp_e, delete v cs))
   | (Get v name) => (Get v name, delete v cs)
+  | (OpCurrHeap b v w) => (OpCurrHeap b v w, delete v cs)
   | (MustTerminate p) =>
     (let (p', cs') = const_fp_loop p cs in
       (MustTerminate p', cs'))
@@ -403,6 +405,7 @@ Proof
   >- fs[const_fp_loop_def,pairTheory.ELIM_UNCURRY]
   >- fs[const_fp_loop_def,pairTheory.ELIM_UNCURRY]
   >- fs[const_fp_loop_def,pairTheory.ELIM_UNCURRY]
+  >- fs[const_fp_loop_def,pairTheory.ELIM_UNCURRY]
   >- (CONV_TAC(RAND_CONV(patternMatchesLib.PMATCH_ELIM_CONV))
               >> every_case_tac >> fs[Once const_fp_loop_def])
   >- (CONV_TAC(RAND_CONV(patternMatchesLib.PMATCH_ELIM_CONV))

From df68183ffae235c8df12abf39ae99a77614bf471 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Fri, 13 Nov 2020 13:32:48 +0100
Subject: [PATCH 09/15] Remove cheats, progress on #796

---
 .../backend/proofs/word_allocProofScript.sml  | 28 +++++++++----------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/compiler/backend/proofs/word_allocProofScript.sml b/compiler/backend/proofs/word_allocProofScript.sml
index 51d096cbe1..fa17a0af4d 100644
--- a/compiler/backend/proofs/word_allocProofScript.sml
+++ b/compiler/backend/proofs/word_allocProofScript.sml
@@ -2719,7 +2719,11 @@ Proof
   >- (* get *)
     rm_tac
   >- (* OpCurrHeap *)
-    cheat
+   (rm_tac \\ fs[evaluate_def,state_component_equality,set_var_def,word_exp_def,
+       the_words_def,AllCaseEqs(),PULL_EXISTS,get_live_exp_def,big_union_def]>>
+    first_x_assum (qspecl_then [‘t’,‘delete num live’] mp_tac) >>
+    impl_tac >- (fs [domain_delete] \\ metis_tac []) >>
+    strip_tac \\ fs [] \\ rw [lookup_insert])
   >- (* loc value *)
     rm_tac
   >- (* seq *)
@@ -5942,19 +5946,15 @@ Proof
     (exists_tac>>
     EVERY_CASE_TAC>>full_simp_tac(srw_ss())[call_env_def, flush_state_def,dec_clock_def])
   >- (* OpCurrHeap *)
-    (exists_tac>>
-    fs [word_exp_def,the_words_def] >>
-    Cases_on ‘lookup n0 st.locals’ >> fs []>> Cases_on ‘x’ \\ fs []>>
-    Cases_on ‘FLOOKUP st.store CurrHeap’ >> fs []>> Cases_on ‘x’ \\ fs []>>
-    Cases_on ‘word_op b [c; c']’ >> fs [] >>
-    full_simp_tac(srw_ss())[next_var_rename_def,ssa_cc_trans_inst_def,inst_def,
-      assign_def,word_exp_perm,evaluate_def,LET_THM,word_exp_def,the_words_def] >>
-    imp_res_tac ssa_locals_rel_get_var >>
-    fs[set_vars_def,get_var_def,lookup_alist_insert]>>
-    first_x_assum drule >> fs [set_var_def] >>
-    full_simp_tac(srw_ss())[ssa_locals_rel_def]>>
-    srw_tac[][]>>full_simp_tac(srw_ss())[lookup_insert] >>
-    pop_assum mp_tac >> cheat)
+    (last_x_assum kall_tac>>
+    exists_tac>>
+    EVERY_CASE_TAC>>full_simp_tac(srw_ss())[next_var_rename_def]>>
+    imp_res_tac ssa_locals_rel_get_var>>
+    imp_res_tac ssa_cc_trans_exp_correct>>full_simp_tac(srw_ss())[word_state_eq_rel_def]>>
+    rev_full_simp_tac(srw_ss())[word_exp_perm,evaluate_def]>>
+    fs[set_var_def,set_store_def,ssa_cc_trans_exp_def]>>
+    match_mp_tac ssa_locals_rel_set_var>>
+    full_simp_tac(srw_ss())[every_var_def])
   >-
     exp_tac
   >- (* Install *)

From 8921d1740e80f61806839d5ddc72fd004c145db2 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Fri, 13 Nov 2020 14:31:30 +0100
Subject: [PATCH 10/15] Generate OpCurrHeap in word_inst

---
 .../backend/proofs/word_instProofScript.sml   | 68 +++++++++++++------
 compiler/backend/word_instScript.sml          | 30 +++++++-
 2 files changed, 77 insertions(+), 21 deletions(-)

diff --git a/compiler/backend/proofs/word_instProofScript.sml b/compiler/backend/proofs/word_instProofScript.sml
index de5d3cd49e..0263e391b0 100644
--- a/compiler/backend/proofs/word_instProofScript.sml
+++ b/compiler/backend/proofs/word_instProofScript.sml
@@ -367,16 +367,18 @@ val flatten_exp_binary_branch_exp = Q.prove(`
   binary_branch_exp (flatten_exp exp)`,
   ho_match_mp_tac flatten_exp_ind>>full_simp_tac(srw_ss())[op_consts_def,flatten_exp_def,binary_branch_exp_def,EVERY_MEM,EVERY_MAP]);
 
-val flatten_exp_every_var_exp = Q.prove(`
+Theorem flatten_exp_every_var_exp[local]:
   ∀exp.
   every_var_exp P exp ⇒
-  every_var_exp P (flatten_exp exp)`,
-  ho_match_mp_tac flatten_exp_ind>>full_simp_tac(srw_ss())[op_consts_def,flatten_exp_def,every_var_exp_def,EVERY_MEM,EVERY_MAP]);
+  every_var_exp P (flatten_exp exp)
+Proof
+  ho_match_mp_tac flatten_exp_ind>>full_simp_tac(srw_ss())[op_consts_def,flatten_exp_def,every_var_exp_def,EVERY_MEM,EVERY_MAP]
+QED
 
 (* inst_select correctness
   Main difficulty: Dealing with multiple choice of optimizations, depending on whether we are allowed to use them w.r.t. to the asm configuration
 *)
-val inst_select_exp_thm = Q.prove(`
+Theorem inst_select_exp_thm[local]:
   ∀c tar temp exp s w loc.
   binary_branch_exp exp ∧
   every_var_exp (λx. x < temp) exp ∧
@@ -388,29 +390,34 @@ val inst_select_exp_thm = Q.prove(`
   ∀x.
     if x = tar then lookup x loc' = SOME w
     else if x < temp then lookup x loc' = lookup x s.locals
-    else T`,
+    else T
+Proof
+
   completeInduct_on`exp_size (K 0) exp`>>
   rpt strip_tac>>
   Cases_on`exp`>>
   full_simp_tac(srw_ss())[evaluate_def,binary_branch_exp_def,every_var_exp_def]
   >-
-    (simp[inst_select_exp_def]>>
+    (rename [‘Const’]>>
+    simp[inst_select_exp_def]>>
     full_simp_tac(srw_ss())[LET_THM,evaluate_def,inst_def,mem_load_def,assign_def,word_exp_def,set_var_def,mem_load_def,word_op_def]>>
     simp[state_component_equality,locals_rel_def,lookup_insert]>>
     full_simp_tac(srw_ss())[locals_rel_def])
   >-
-    (simp[inst_select_exp_def]>>
+    (rename [‘Var’] >>
+    simp[inst_select_exp_def]>>
     full_simp_tac(srw_ss())[LET_THM,evaluate_def,inst_def,mem_load_def,assign_def,word_exp_def,set_var_def,mem_load_def,word_op_def,get_vars_def,set_vars_def,get_var_def]>>
     full_simp_tac(srw_ss())[locals_rel_def]>>
     res_tac>>fs[alist_insert_def]>>
     simp[state_component_equality,lookup_insert])
   >-
-    (simp[inst_select_exp_def]>>
+    (rename [‘Lookup’]>>
+    simp[inst_select_exp_def]>>
     full_simp_tac(srw_ss())[LET_THM,evaluate_def,inst_def,mem_load_def,assign_def,word_exp_def,set_var_def,mem_load_def,word_op_def,get_vars_def,set_vars_def,get_var_def]>>
     fs[locals_rel_def,state_component_equality,lookup_insert])
   >-
-    (*Load*)
-    (Cases_on`∃exp' w'. e = Op Add[exp';Const w']` >>full_simp_tac(srw_ss())[]
+    (rename [‘Load’]>>
+    Cases_on`∃exp' w'. e = Op Add[exp';Const w']` >>full_simp_tac(srw_ss())[]
     >-
       (simp[Once inst_select_exp_def]>>IF_CASES_TAC
       >-
@@ -452,11 +459,20 @@ val inst_select_exp_thm = Q.prove(`
       simp[state_component_equality,set_var_def,lookup_insert]>>
       srw_tac[][]>>DISJ2_TAC>>strip_tac>>
       `x ≠ temp` by DECIDE_TAC>>metis_tac[])
+
   >-
-    (*Op*)
-    (Cases_on`∃e1 e2. l = [e1;e2]`>>full_simp_tac(srw_ss())[inst_select_exp_def]
+    (rename [‘Op’]>>
+    Cases_on`∃e1 e2. l = [e1;e2]`>>full_simp_tac(srw_ss())[inst_select_exp_def]
     >-
-      (`binary_branch_exp e1` by
+      (IF_CASES_TAC THEN1
+
+
+
+cheat >>
+      pop_assum mp_tac >>
+      IF_CASES_TAC THEN1 cheat >>
+      pop_assum mp_tac>>
+      `binary_branch_exp e1` by
         (Cases_on`b`>>full_simp_tac(srw_ss())[binary_branch_exp_def])>>
       full_simp_tac(srw_ss())[word_exp_def,the_words_def,IS_SOME_EXISTS]>>
       last_x_assum mp_tac>>simp[Once PULL_FORALL]>>
@@ -469,7 +485,8 @@ val inst_select_exp_thm = Q.prove(`
       pop_assum(qspecl_then[`temp`,`c`] assume_tac)>>full_simp_tac(srw_ss())[]>>
       Cases_on`∃w. e2 = Const w`
       >-
-        (full_simp_tac(srw_ss())[]>>IF_CASES_TAC
+        (rpt (disch_then kall_tac) >>
+        full_simp_tac(srw_ss())[]>>IF_CASES_TAC
         >-
           (full_simp_tac(srw_ss())[evaluate_def]>>
           simp[LET_THM,inst_def,mem_load_def,word_exp_def,assign_def,the_words_def]>>
@@ -496,15 +513,25 @@ val inst_select_exp_thm = Q.prove(`
           DISJ2_TAC>>strip_tac>-`F` by DECIDE_TAC>>
           `x ≠ temp` by DECIDE_TAC>>
           `¬ (temp+1 < temp)` by DECIDE_TAC>>
-          metis_tac[]))
+          metis_tac[])) >>
+      ntac 2 (disch_then assume_tac)
       >>
         `inst_select_exp c tar temp (Op b [e1;e2]) =
         let p1 = inst_select_exp c temp temp e1 in
         let p2 = inst_select_exp c (temp+1) (temp+1) e2 in
-        Seq p1 (Seq p2 (Inst (Arith (Binop b tar temp (Reg (temp+1))))))` by
-        (full_simp_tac(srw_ss())[inst_select_exp_def,LET_THM]>>EVERY_CASE_TAC>>full_simp_tac(srw_ss())[])>>
+          Seq p1 (Seq p2 (Inst (Arith (Binop b tar temp (Reg (temp+1))))))` by
+            (full_simp_tac(srw_ss())[inst_select_exp_def,LET_THM]>>
+             EVERY_CASE_TAC>>full_simp_tac(srw_ss())[])>>
+        pop_assum mp_tac >>
+        pop_assum mp_tac >>
+        pop_assum mp_tac >>
         full_simp_tac(srw_ss())[inst_select_exp_def,LET_THM]>>pop_assum kall_tac>>
+        ntac 2 (disch_then assume_tac) >>
+        IF_CASES_TAC THEN1 fs [] >>
+        rpt (qpat_x_assum ‘~(_:bool)’ kall_tac) >>
+        rpt (qpat_x_assum ‘_ ∨ _’ kall_tac) >>
         full_simp_tac(srw_ss())[evaluate_def,LET_THM]>>
+        disch_then kall_tac >>
         first_x_assum(qspecl_then[`e2`] mp_tac)>>
         simp[exp_size_def]>>
         disch_then(qspecl_then [`c`,`temp+1`,`temp+1`,`s with locals:=loc''`,`Word c''`,`loc''`] mp_tac)>>
@@ -544,8 +571,8 @@ val inst_select_exp_thm = Q.prove(`
       Cases_on`t'`>>fs[the_words_def]>>
       EVERY_CASE_TAC>>fs[]))
   >-
-    (*Shift*)
-    (simp[inst_select_exp_def]>>last_x_assum mp_tac>>simp[Once PULL_FORALL]>>disch_then (qspec_then`e`mp_tac)>>impl_tac>-(full_simp_tac(srw_ss())[exp_size_def]>>DECIDE_TAC)>>
+    (rename [‘Shift’]>>
+    simp[inst_select_exp_def]>>last_x_assum mp_tac>>simp[Once PULL_FORALL]>>disch_then (qspec_then`e`mp_tac)>>impl_tac>-(full_simp_tac(srw_ss())[exp_size_def]>>DECIDE_TAC)>>
     full_simp_tac(srw_ss())[LET_THM,word_exp_def]>>EVERY_CASE_TAC>>full_simp_tac(srw_ss())[]
     >-
       (`word_sh s' c' n = SOME c'` by
@@ -571,7 +598,8 @@ val inst_select_exp_thm = Q.prove(`
       metis_tac[])
     >-
       (`n ≥ dimindex(:'a)` by DECIDE_TAC>>
-      full_simp_tac(srw_ss())[word_sh_def])));
+      full_simp_tac(srw_ss())[word_sh_def]))
+QED
 
 val locals_rm = Q.prove(`
   D with locals := D.locals = D`,
diff --git a/compiler/backend/word_instScript.sml b/compiler/backend/word_instScript.sml
index 51c4e65959..62dccffd52 100644
--- a/compiler/backend/word_instScript.sml
+++ b/compiler/backend/word_instScript.sml
@@ -175,6 +175,20 @@ val test = EVAL ``flatten_exp (pull_exp (Op Sub [Const 1w; Op Sub[Const 2w;Const
  Op Add [Const 4w; Const 5w; Op Add[Const 6w; Const 7w];Op Xor[Const 1w;Var y;Var x]] ; Const (8w:8 word)]))``
 *)
 
+Definition is_Lookup_CurrHeap_def:
+  is_Lookup_CurrHeap (Lookup CurrHeap) = T ∧
+  is_Lookup_CurrHeap _ = F
+End
+
+Theorem is_Lookup_CurrHeap_pmatch:
+  is_Lookup_CurrHeap e =
+    (case e of Lookup CurrHeap => T | _ => F)
+Proof
+  rpt(CONV_TAC(RAND_CONV patternMatchesLib.PMATCH_ELIM_CONV) >> every_case_tac >>
+         PURE_ONCE_REWRITE_TAC[LET_DEF] >> BETA_TAC) >>
+  fs [is_Lookup_CurrHeap_def]
+QED
+
 (*
   Maximal Munch instruction selection on (binary) expressions
   c is an asm_config to check validity of imms (TODO: assume 0w is accepted?)
@@ -208,6 +222,13 @@ val inst_select_exp_def = tDefine "inst_select_exp" `
     Get tar store_name) ∧
   (*All ops are binary branching*)
   (inst_select_exp c tar temp (Op op [e1;e2]) =
+    if is_Lookup_CurrHeap e2 then
+      (let p1 = inst_select_exp c temp temp e1 in
+        Seq p1 (OpCurrHeap op tar temp))
+    else if is_Lookup_CurrHeap e1 ∧ op ≠ Sub then
+      (let p2 = inst_select_exp c temp temp e2 in
+        Seq p2 (OpCurrHeap op tar temp))
+    else
     let p1 = inst_select_exp c temp temp e1 in
     dtcase e2 of
     | Const w =>
@@ -262,7 +283,14 @@ Theorem inst_select_exp_pmatch:
     Get tar store_name
   (*All ops are binary branching*)
   | Op op [e1;e2] =>
-    (case e2 of
+    (if is_Lookup_CurrHeap e2 then
+      (let p1 = inst_select_exp c temp temp e1 in
+        Seq p1 (OpCurrHeap op tar temp))
+    else if is_Lookup_CurrHeap e1 ∧ op ≠ Sub then
+      (let p2 = inst_select_exp c temp temp e2 in
+        Seq p2 (OpCurrHeap op tar temp))
+    else
+     case e2 of
       Const w =>
       (*t = r op const*)
       if c.valid_imm (INL op) w then

From 8781d12545e56073405234bb6c16544086e54863 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Fri, 13 Nov 2020 15:03:10 +0100
Subject: [PATCH 11/15] Finish work for #796

Closes #796
---
 compiler/backend/backendComputeLib.sml        |  1 +
 .../backend/proofs/word_instProofScript.sml   | 41 +++++++++++++++----
 .../translation/to_word32ProgScript.sml       |  1 +
 .../translation/to_word64ProgScript.sml       |  1 +
 4 files changed, 37 insertions(+), 7 deletions(-)

diff --git a/compiler/backend/backendComputeLib.sml b/compiler/backend/backendComputeLib.sml
index 9d5d0fc62b..269e841955 100644
--- a/compiler/backend/backendComputeLib.sml
+++ b/compiler/backend/backendComputeLib.sml
@@ -631,6 +631,7 @@ val add_backend_compset = computeLib.extend_compset
       (* ---- wordLang inst_select and inst flattening ---- *)
     ,word_instTheory.three_to_two_reg_def
     ,word_instTheory.pull_exp_def
+    ,word_instTheory.is_Lookup_CurrHeap_def
     ,word_instTheory.inst_select_def
     ,word_instTheory.inst_select_exp_def
     ,word_instTheory.flatten_exp_def
diff --git a/compiler/backend/proofs/word_instProofScript.sml b/compiler/backend/proofs/word_instProofScript.sml
index 0263e391b0..055a0eba57 100644
--- a/compiler/backend/proofs/word_instProofScript.sml
+++ b/compiler/backend/proofs/word_instProofScript.sml
@@ -392,7 +392,6 @@ Theorem inst_select_exp_thm[local]:
     else if x < temp then lookup x loc' = lookup x s.locals
     else T
 Proof
-
   completeInduct_on`exp_size (K 0) exp`>>
   rpt strip_tac>>
   Cases_on`exp`>>
@@ -459,18 +458,46 @@ Proof
       simp[state_component_equality,set_var_def,lookup_insert]>>
       srw_tac[][]>>DISJ2_TAC>>strip_tac>>
       `x ≠ temp` by DECIDE_TAC>>metis_tac[])
-
   >-
     (rename [‘Op’]>>
     Cases_on`∃e1 e2. l = [e1;e2]`>>full_simp_tac(srw_ss())[inst_select_exp_def]
     >-
       (IF_CASES_TAC THEN1
-
-
-
-cheat >>
+       (gvs[PULL_FORALL] >>
+        first_x_assum (qspec_then ‘e1’ mp_tac) >>
+        fs [exp_size_def,binary_branch_exp_def] >>
+        ‘binary_branch_exp e1’ by
+           (Cases_on ‘b’ \\ fs [binary_branch_exp_def]) >> fs [] >>
+        disch_then drule >>
+        gvs [word_exp_def,AllCaseEqs(),the_words_def,GSYM PULL_FORALL] >>
+        disch_then (qspecl_then [‘c’,‘temp’] strip_assume_tac) >>
+        pop_assum drule >> fs [] >> strip_tac >>
+        gvs [evaluate_def,word_exp_def,the_words_def] >>
+        first_assum (qspec_then ‘temp’ assume_tac) >> fs [] >>
+        Cases_on ‘e2’ >> fs [is_Lookup_CurrHeap_def] >>
+        rename [‘Lookup ss’] \\ Cases_on ‘ss’ >> fs [is_Lookup_CurrHeap_def] >>
+        gvs [word_exp_def,set_var_def,state_component_equality,lookup_insert] >>
+        rw [] >> metis_tac [prim_recTheory.LESS_REFL]) >>
       pop_assum mp_tac >>
-      IF_CASES_TAC THEN1 cheat >>
+      IF_CASES_TAC THEN1
+       (gvs[PULL_FORALL] >>
+        first_x_assum (qspec_then ‘e2’ mp_tac) >>
+        fs [exp_size_def,binary_branch_exp_def] >>
+        ‘binary_branch_exp e2’ by
+           (Cases_on ‘b’ \\ fs [binary_branch_exp_def]) >> fs [] >>
+        disch_then drule >>
+        gvs [word_exp_def,AllCaseEqs(),the_words_def,GSYM PULL_FORALL] >>
+        disch_then (qspecl_then [‘c’,‘temp’] strip_assume_tac) >>
+        pop_assum drule >> fs [] >> strip_tac >>
+        gvs [evaluate_def,word_exp_def,the_words_def] >>
+        first_assum (qspec_then ‘temp’ assume_tac) >> fs [] >>
+        Cases_on ‘e1’ >> fs [is_Lookup_CurrHeap_def] >>
+        rename [‘Lookup ss’] \\ Cases_on ‘ss’ >> fs [is_Lookup_CurrHeap_def] >>
+        rename [‘word_op b [x1; x2] = SOME x3’] >>
+        ‘word_op b [x2; x1] = SOME x3’ by
+          (Cases_on ‘b’ \\ fs [word_op_def,AllCaseEqs()]) >>
+        gvs [word_exp_def,set_var_def,state_component_equality,lookup_insert] >>
+        rw [] >> metis_tac [prim_recTheory.LESS_REFL]) >>
       pop_assum mp_tac>>
       `binary_branch_exp e1` by
         (Cases_on`b`>>full_simp_tac(srw_ss())[binary_branch_exp_def])>>
diff --git a/compiler/bootstrap/translation/to_word32ProgScript.sml b/compiler/bootstrap/translation/to_word32ProgScript.sml
index 4f0a39353d..af4ed85bc6 100644
--- a/compiler/bootstrap/translation/to_word32ProgScript.sml
+++ b/compiler/bootstrap/translation/to_word32ProgScript.sml
@@ -251,6 +251,7 @@ val _ = translate (spec32 wordLangTheory.max_var_def)
 val _ = translate (conv32_RHS integer_wordTheory.WORD_LEi)
 
 val _ = translate (asmTheory.offset_ok_def |> SIMP_RULE std_ss [alignmentTheory.aligned_bitwise_and] |> conv32)
+val _ = translate (is_Lookup_CurrHeap_pmatch |> conv32)
 val res = translate_no_ind (inst_select_exp_pmatch |> conv32 |> SIMP_RULE std_ss [word_mul_def,word_2comp_def] |> conv32)
 
 val ind_lemma = Q.prove(
diff --git a/compiler/bootstrap/translation/to_word64ProgScript.sml b/compiler/bootstrap/translation/to_word64ProgScript.sml
index a2a15cad12..358218c732 100644
--- a/compiler/bootstrap/translation/to_word64ProgScript.sml
+++ b/compiler/bootstrap/translation/to_word64ProgScript.sml
@@ -250,6 +250,7 @@ val _ = translate (spec64 wordLangTheory.max_var_def)
 val _ = translate (conv64_RHS integer_wordTheory.WORD_LEi)
 
 val _ = translate (asmTheory.offset_ok_def |> SIMP_RULE std_ss [alignmentTheory.aligned_bitwise_and] |> conv64)
+val _ = translate (is_Lookup_CurrHeap_pmatch |> conv32)
 val res = translate_no_ind (inst_select_exp_pmatch |> conv64 |> SIMP_RULE std_ss [word_mul_def,word_2comp_def] |> conv64)
 
 val ind_lemma = Q.prove(

From 2c83bd888fb9359bf66cc2f3bde4a72d56488094 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Sat, 14 Nov 2020 09:11:45 +0100
Subject: [PATCH 12/15] Add special case to code for address computation

Thanks to @sorear for pointing out that this optimisation is possible.
---
 compiler/backend/data_to_wordScript.sml       | 12 +++----
 .../proofs/data_to_word_assignProofScript.sml |  2 +-
 .../proofs/data_to_word_memoryProofScript.sml | 35 +++++++++++++++++--
 3 files changed, 39 insertions(+), 10 deletions(-)

diff --git a/compiler/backend/data_to_wordScript.sml b/compiler/backend/data_to_wordScript.sml
index bc0169de70..6dc680d416 100644
--- a/compiler/backend/data_to_wordScript.sml
+++ b/compiler/backend/data_to_wordScript.sml
@@ -110,13 +110,13 @@ val ptr_bits_def = Define `
 val real_addr_def = Define `
   (real_addr (conf:data_to_word$config) r): 'a wordLang$exp =
     let k = shift (:'a) in
-      if k <= conf.pad_bits + 1 then
-        Op Add [Lookup CurrHeap;
-                Shift Lsr (Var r) (shift_length conf - k)]
+    let l = shift_length conf in
+      if k = l ∧ conf.len_bits = 0 ∧ conf.tag_bits = 0 then
+        Op Add [Lookup CurrHeap; Op Sub [Var r; Const 1w]]
+      else if k <= conf.pad_bits + 1 then
+        Op Add [Lookup CurrHeap; Shift Lsr (Var r) (l - k)]
       else
-        Op Add [Lookup CurrHeap;
-                Shift Lsl (Shift Lsr (Var r)
-                  (shift_length conf)) k]`
+        Op Add [Lookup CurrHeap; Shift Lsl (Shift Lsr (Var r) l) k]`
 
 val real_offset_def = Define `
   (real_offset (conf:data_to_word$config) r): 'a wordLang$exp =
diff --git a/compiler/backend/proofs/data_to_word_assignProofScript.sml b/compiler/backend/proofs/data_to_word_assignProofScript.sml
index 6f5bf22062..354a88bf3f 100644
--- a/compiler/backend/proofs/data_to_word_assignProofScript.sml
+++ b/compiler/backend/proofs/data_to_word_assignProofScript.sml
@@ -8474,7 +8474,7 @@ Theorem word_exp_insert:
       word_exp t (real_addr c m)))
 Proof
   fs [wordSemTheory.word_exp_def,real_addr_def]
-  \\ IF_CASES_TAC \\ fs []
+  \\ rpt (IF_CASES_TAC \\ fs [])
   \\ fs [wordSemTheory.word_exp_def,real_addr_def] \\ fs [lookup_insert]
 QED
 
diff --git a/compiler/backend/proofs/data_to_word_memoryProofScript.sml b/compiler/backend/proofs/data_to_word_memoryProofScript.sml
index ade13e0c89..d569bcced8 100644
--- a/compiler/backend/proofs/data_to_word_memoryProofScript.sml
+++ b/compiler/backend/proofs/data_to_word_memoryProofScript.sml
@@ -4609,9 +4609,12 @@ val get_real_addr_def = Define `
     let k = shift (:α) in
       case FLOOKUP st CurrHeap of
       | SOME (Word curr) =>
-          if k <= conf.pad_bits + 1
-          then SOME (curr + (w >>> (shift_length conf - k)))
-          else SOME (curr + (w >>> (shift_length conf) << k))
+          if k = shift_length conf ∧ conf.len_bits = 0 ∧ conf.tag_bits = 0
+          then SOME (curr + w - 1w)
+          else
+            if k <= conf.pad_bits + 1
+            then SOME (curr + (w >>> (shift_length conf - k)))
+            else SOME (curr + (w >>> (shift_length conf) << k))
       | _ => NONE`
 
 val get_real_offset_def = Define `
@@ -4619,6 +4622,15 @@ val get_real_offset_def = Define `
     if dimindex (:'a) = 32
     then SOME (w + bytes_in_word) else SOME (w << 1 + bytes_in_word)`
 
+Triviality or_1:
+  ∀w. (0 -- 0) w ‖ 1w = 1w :'a word
+Proof
+  fs [fcpTheory.CART_EQ,word_or_def,fcpTheory.FCP_BETA,word_lsl_def,
+      word_0,word_bits_def]
+  \\ once_rewrite_tac [wordsTheory.word_index_n2w] \\ fs []
+  \\ rw [] \\ eq_tac \\ rw []
+QED
+
 Theorem get_real_addr_get_addr:
    heap_length heap <= dimword (:'a) DIV 2 ** shift_length c /\
     heap_lookup n heap = SOME anything /\
@@ -4635,6 +4647,23 @@ Proof
     \\ match_mp_tac LESS_LESS_EQ_TRANS
     \\ once_rewrite_tac [CONJ_COMM]
     \\ asm_exists_tac \\ fs [])
+  \\ IF_CASES_TAC
+  THEN1
+   (Cases_on ‘w’
+    \\ fs [get_lowerbits_def,small_shift_length_def,or_1]
+    \\ ‘0w = n2w n ≪ shift_length c && 1w’ by
+     (fs [fcpTheory.CART_EQ,word_and_def,fcpTheory.FCP_BETA,word_lsl_def,word_0]
+      \\ rewrite_tac [word_1comp_def]
+      \\ once_rewrite_tac [wordsTheory.word_index_n2w] \\ fs []
+      \\ gvs [good_dimindex_def,shift_def])
+    \\ drule (GSYM WORD_ADD_OR)
+    \\ pop_assum kall_tac
+    \\ fs []
+    \\ gvs [WORD_MUL_LSL,bytes_in_word_def,word_mul_n2w,good_dimindex_def,
+            dimword_def,shift_def]
+    \\ qpat_x_assum ‘_ = shift_length _’ (assume_tac o GSYM)
+    \\ fs [])
+  \\ pop_assum kall_tac
   \\ reverse IF_CASES_TAC THEN1
    (drule lsl_lsr \\ fs [get_lowerbits_LSL_shift_length]
     \\ fs [] \\ rw []

From 9962f61c52c582fcd43ffacda21f089f0bd90cf3 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Sun, 15 Nov 2020 21:16:12 +0100
Subject: [PATCH 13/15] Fix a silly copy-paste mistake

---
 compiler/bootstrap/translation/to_word64ProgScript.sml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/compiler/bootstrap/translation/to_word64ProgScript.sml b/compiler/bootstrap/translation/to_word64ProgScript.sml
index 358218c732..e10b1a6d05 100644
--- a/compiler/bootstrap/translation/to_word64ProgScript.sml
+++ b/compiler/bootstrap/translation/to_word64ProgScript.sml
@@ -250,7 +250,7 @@ val _ = translate (spec64 wordLangTheory.max_var_def)
 val _ = translate (conv64_RHS integer_wordTheory.WORD_LEi)
 
 val _ = translate (asmTheory.offset_ok_def |> SIMP_RULE std_ss [alignmentTheory.aligned_bitwise_and] |> conv64)
-val _ = translate (is_Lookup_CurrHeap_pmatch |> conv32)
+val _ = translate (is_Lookup_CurrHeap_pmatch |> conv64)
 val res = translate_no_ind (inst_select_exp_pmatch |> conv64 |> SIMP_RULE std_ss [word_mul_def,word_2comp_def] |> conv64)
 
 val ind_lemma = Q.prove(

From ac5c74531f672da189747a095e1b6664f3b9ce21 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Sun, 15 Nov 2020 21:20:31 +0100
Subject: [PATCH 14/15] Replace a Q.prove with Theorem ... QED

---
 compiler/backend/proofs/word_instProofScript.sml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/compiler/backend/proofs/word_instProofScript.sml b/compiler/backend/proofs/word_instProofScript.sml
index 055a0eba57..f0f59e2278 100644
--- a/compiler/backend/proofs/word_instProofScript.sml
+++ b/compiler/backend/proofs/word_instProofScript.sml
@@ -17,10 +17,12 @@ val _ = set_grammar_ancestry ["wordLang", "wordProps", "word_inst", "wordSem"];
 Type result[pp] = “:'a wordSem$result”
 
 (* TODO: Move, but some of these are specific instantiations *)
-val PERM_SWAP_SIMP = Q.prove(`
-  PERM (A ++ (B::C)) (B::(A++C))`,
+Theorem PERM_SWAP_SIMP[local]:
+  PERM (A ++ (B::C)) (B::(A++C))
+Proof
   match_mp_tac APPEND_PERM_SYM>>full_simp_tac(srw_ss())[]>>
-  metis_tac[PERM_APPEND]);
+  metis_tac[PERM_APPEND]
+QED
 
 val EL_FILTER = Q.prove(`
   ∀ls x. x < LENGTH (FILTER P ls) ⇒ P (EL x (FILTER P ls))`,

From 3db683866a83cfd415bb8ccf8dbd3ddabde79154 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Mon, 16 Nov 2020 08:44:55 +0100
Subject: [PATCH 15/15] Prove alternative phrasing of AppReturns as lemma

---
 translator/ml_translatorScript.sml | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/translator/ml_translatorScript.sml b/translator/ml_translatorScript.sml
index 301b725abb..d6003510cd 100644
--- a/translator/ml_translatorScript.sml
+++ b/translator/ml_translatorScript.sml
@@ -101,6 +101,27 @@ val PreImpEval_def = Define`
 
 (* Theorems *)
 
+Theorem AppReturns_thm:
+  AppReturns P cl Q ⇔
+    ∀v. P v ⇒
+        ∃env exp.
+          do_opapp [cl;v] = SOME (env,exp) ∧
+          ∀refs.
+            ∃refs' u.
+              eval_rel (empty_state with refs := refs) env exp
+                       (empty_state with refs := refs++refs') u ∧
+              Q u
+Proof
+  fs [AppReturns_def] \\ eq_tac \\ rw []
+  \\ first_x_assum drule
+  \\ Cases_on ‘cl’ \\ fs [do_opapp_def,AllCaseEqs()]
+  \\ rename [‘find_recfun x1 x2’]
+  \\ Cases_on ‘find_recfun x1 x2’ \\ fs []
+  \\ PairCases_on ‘x’ \\ fs []
+  \\ rename [‘ALL_DISTINCT xx’]
+  \\ Cases_on ‘ALL_DISTINCT xx’ \\ fs []
+QED
+
 local
   val Eval_lemma = prove(
     ``∀env exp P.