From 8d95ef7e3c640a3e9cd77bc664372a7e4aca4cfa Mon Sep 17 00:00:00 2001
From: Scott Owens <sowens@fb.com>
Date: Mon, 3 Feb 2020 03:42:26 -0800
Subject: [PATCH] [sledge sem] Fix global variables

Summary:
Add a field to LLAIR variables to indicate whether they are global or
local. Update the LLVM semantics for constant expression evaluation to
be relational, so that it doesn't have to have an answer for references
to undefined globals.

Reviewed By: jberdine

Differential Revision: D19446312

fbshipit-source-id: 9bbfd180e
---
 sledge/semantics/llairScript.sml              |  10 +-
 sledge/semantics/llair_propScript.sml         |  16 +-
 sledge/semantics/llvmScript.sml               | 127 +++----
 sledge/semantics/llvm_to_llairScript.sml      |  12 +-
 sledge/semantics/llvm_to_llair_propScript.sml | 334 ++++++++++--------
 sledge/semantics/memory_modelScript.sml       |   5 +-
 sledge/semantics/miscScript.sml               |   2 +-
 7 files changed, 282 insertions(+), 224 deletions(-)

diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml
index ebae11c19..029d8394b 100644
--- a/sledge/semantics/llairScript.sml
+++ b/sledge/semantics/llairScript.sml
@@ -54,7 +54,8 @@ End
 (* Based on the constructor functions in exp.mli rather than the type definition *)
 Datatype:
   exp =
-  | Var var
+  (* Args: variable name, true for globals *)
+  | Var var bool
   | Nondet
   (* Args: function name, block name *)
   | Label label
@@ -262,7 +263,12 @@ Inductive eval_exp:
   (∀s v r.
    flookup s.locals v = Some r
    ⇒
-   eval_exp s (Var v) r) ∧
+   eval_exp s (Var v F) r) ∧
+
+  (∀s v r.
+   flookup s.glob_addrs v = Some r
+   ⇒
+   eval_exp s (Var v T) (FlatV (n2i r pointer_size))) ∧
 
   (* TODO: Nondet I guess we need to know the type here *)
   (* TODO: Label *)
diff --git a/sledge/semantics/llair_propScript.sml b/sledge/semantics/llair_propScript.sml
index 202771cb2..abc0ad7f1 100644
--- a/sledge/semantics/llair_propScript.sml
+++ b/sledge/semantics/llair_propScript.sml
@@ -124,7 +124,7 @@ Proof
 QED
 
 Theorem eval_exp_ignores_lem:
-  ∀s1 e v. eval_exp s1 e v ⇒ ∀s2. s1.locals = s2.locals ⇒ eval_exp s2 e v
+  ∀s1 e v. eval_exp s1 e v ⇒ ∀s2. s1.locals = s2.locals ∧ s1.glob_addrs = s2.glob_addrs ⇒ eval_exp s2 e v
 Proof
   ho_match_mp_tac eval_exp_ind >>
   rw [] >> simp [Once eval_exp_cases] >>
@@ -134,13 +134,14 @@ Proof
 QED
 
 Theorem eval_exp_ignores:
-  ∀s1 e v s2. s1.locals = s2.locals ⇒ (eval_exp s1 e v ⇔ eval_exp s2 e v)
+  ∀s1 e v s2. s1.locals = s2.locals ∧ s1.glob_addrs = s2.glob_addrs ⇒ (eval_exp s1 e v ⇔ eval_exp s2 e v)
 Proof
   metis_tac [eval_exp_ignores_lem]
 QED
 
 Definition exp_uses_def:
-  (exp_uses (Var x) = {x}) ∧
+  (exp_uses (Var x T) = {}) ∧
+  (exp_uses (Var x F) = {x}) ∧
   (exp_uses Nondet = {}) ∧
   (exp_uses (Label _) = {}) ∧
   (exp_uses (Splat e1 e2) = exp_uses e1 ∪ exp_uses e2) ∧
@@ -164,7 +165,8 @@ End
 Theorem eval_exp_ignores_unused_lem:
   ∀s1 e v.
     eval_exp s1 e v ⇒
-    ∀s2. DRESTRICT s1.locals (exp_uses e) = DRESTRICT s2.locals (exp_uses e) ⇒
+    ∀s2. DRESTRICT s1.locals (exp_uses e) = DRESTRICT s2.locals (exp_uses e) ∧
+         s1.glob_addrs = s2.glob_addrs ⇒
     eval_exp s2 e v
 Proof
   ho_match_mp_tac eval_exp_ind >>
@@ -199,7 +201,11 @@ Proof
 QED
 
 Theorem eval_exp_ignores_unused:
-  ∀s1 e v s2. DRESTRICT s1.locals (exp_uses e) = DRESTRICT s2.locals (exp_uses e) ⇒ (eval_exp s1 e v ⇔ eval_exp s2 e v)
+  ∀s1 e v s2.
+    DRESTRICT s1.locals (exp_uses e) = DRESTRICT s2.locals (exp_uses e) ∧
+    s1.glob_addrs = s2.glob_addrs
+    ⇒
+    (eval_exp s1 e v ⇔ eval_exp s2 e v)
 Proof
   metis_tac [eval_exp_ignores_unused_lem]
 QED
diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index 45e1628ec..784c2991b 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -341,39 +341,43 @@ Definition unsigned_v_to_num_def:
   (unsigned_v_to_num _ = None)
 End
 
-Definition eval_const_def:
-  (eval_const g (IntC W1 i) = FlatV (W1V (i2w i))) ∧
-  (eval_const g (IntC W8 i) = FlatV (W8V (i2w i))) ∧
-  (eval_const g (IntC W32 i) = FlatV (W32V (i2w i))) ∧
-  (eval_const g (IntC W64 i) = FlatV (W64V (i2w i))) ∧
-  (eval_const g (StrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧
-  (eval_const g (ArrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧
-  (eval_const g (GepC ty ptr (t, idx) indices) =
-    case (eval_const g ptr, signed_v_to_num (eval_const g idx)) of
-    | (FlatV (PtrV ptr), Some n) =>
-      let ns = map (λ(t,ci). case signed_v_to_num (eval_const g ci) of None => 0 | Some n => n) indices in
-        (case get_offset ty ns of
-         | None => FlatV UndefV
-         | Some off => FlatV (PtrV (n2w ((w2n ptr) + (sizeof ty) * n + off))))
-    | _ => FlatV UndefV) ∧
-  (eval_const g (GlobalC var) =
-    case flookup g var of
-    | None => FlatV (PtrV 0w)
-    | Some (s,w) => FlatV (PtrV w)) ∧
-  (eval_const g UndefC = FlatV UndefV)
-Termination
-  WF_REL_TAC `measure (const_size o snd)` >> rw [listTheory.MEM_MAP] >>
-  TRY
-    (TRY (PairCases_on `y`) >> simp [] >>
-    Induct_on `tconsts` >> rw [] >> rw [definition "const_size_def"] >>
-    res_tac >> fs [] >> NO_TAC) >>
-  Induct_on `indices` >> rw [] >> rw [definition "const_size_def"] >>
-  fs []
-End
-
-Definition eval_def:
-  (eval s (Variable v) = flookup s.locals v) ∧
-  (eval s (Constant c) = Some <| poison := F; value := eval_const s.globals c |>)
+Inductive eval_const:
+  (∀g i. eval_const g (IntC W1 i) (FlatV (W1V (i2w i)))) ∧
+  (∀g i. eval_const g (IntC W8 i) (FlatV (W8V (i2w i)))) ∧
+  (∀g i. eval_const g (IntC W32 i) (FlatV (W32V (i2w i)))) ∧
+  (∀g i. eval_const g (IntC W64 i) (FlatV (W64V (i2w i)))) ∧
+  (∀g tconsts rs.
+    list_rel (eval_const g) (map snd tconsts) rs
+    ⇒
+    eval_const g (StrC tconsts) (AggV rs)) ∧
+  (∀g tconsts rs.
+    list_rel (eval_const g) (map snd tconsts) rs
+    ⇒
+    eval_const g (ArrC tconsts) (AggV rs)) ∧
+  (∀g ty ptr t idx indices ptr' n ns off vs v.
+    eval_const g ptr (FlatV (PtrV ptr')) ∧
+    eval_const g idx v ∧
+    signed_v_to_num v = Some n ∧
+    list_rel (λ(t, ci) v. eval_const g ci v) indices vs ∧
+    map signed_v_to_num vs = map Some ns ∧
+    get_offset ty ns = Some off
+    ⇒
+    eval_const g (GepC ty ptr (t, idx) indices) (FlatV (PtrV (n2w ((w2n ptr') + (sizeof ty) * n + off))))) ∧
+  (∀g var s w.
+    flookup g var = Some (s, w)
+    ⇒
+    eval_const g (GlobalC var) (FlatV (PtrV w)))
+End
+
+Inductive eval:
+  (∀s x v.
+    flookup s.locals x = Some v
+    ⇒
+    eval s (Variable x) v) ∧
+  (∀s c v.
+    eval_const s.globals c v
+    ⇒
+    eval s (Constant c) <| poison := F; value := v |>)
 End
 
 (* BEGIN Functions to interface to the generic memory model *)
@@ -483,9 +487,12 @@ Definition do_icmp_def:
        | _ => None)
 End
 
-Definition do_phi_def:
-  do_phi from_l s (Phi id _ entries) =
-    option_join (option_map (λarg. option_map (\v. (id, v)) (eval s arg)) (alookup entries from_l))
+Inductive do_phi:
+  (∀from_l s id lands entries e v.
+    alookup entries from_l = Some e ∧
+    eval s e v
+    ⇒
+    do_phi from_l s (Phi id lands entries) (id, v))
 End
 
 Definition extract_value_def:
@@ -536,7 +543,7 @@ Inductive step_instr:
   (∀prog s t a fr v st new_h.
    s.stack = fr::st ∧
    deallocate fr.stack_allocs s.heap = new_h ∧
-   eval s a = Some v
+   eval s a v
    ⇒
    step_instr prog s
      (Ret (t, a)) Tau
@@ -549,7 +556,7 @@ Inductive step_instr:
           status := s.status |>)) ∧
 
   (∀prog s a l1 l2 tf l p.
-   eval s a = Some <| poison := p; value := FlatV (W1V tf) |> ∧
+   eval s a <| poison := p; value := FlatV (W1V tf) |> ∧
    l = Some (if tf = 0w then l2 else l1)
    ⇒
    step_instr prog s
@@ -560,7 +567,7 @@ Inductive step_instr:
   (∀prog s r t a args l1 l2. step_instr prog s (Invoke r t a args l1 l2) Tau s) ∧
 
   (∀prog s a exit_code v1.
-   eval s a = Some v1 ∧
+   eval s a v1 ∧
    signed_v_to_int v1.value = Some exit_code
    ⇒
    step_instr prog s
@@ -568,31 +575,33 @@ Inductive step_instr:
      (s with status := Complete exit_code)) ∧
 
   (∀prog s r nuw nsw t a1 a2 v3 v1 v2.
-   eval s a1 = Some v1 ∧
-   eval s a2 = Some v2 ∧
+   eval s a1 v1 ∧
+   eval s a2 v2 ∧
    do_sub nuw nsw v1 v2 t = Some v3
    ⇒
    step_instr prog s
      (Sub r nuw nsw t a1 a2) Tau
      (inc_pc (update_result r v3 s))) ∧
 
-  (∀prog s r t a const_indices v ns result.
-   eval s a = Some v ∧
+  (∀prog s r t a const_indices v vs ns result.
+   eval s a v ∧
+   list_rel (eval_const s.globals) const_indices vs ∧
    (* The manual implies (but does not explicitly state) that the indices are
     * interpreted as signed numbers *)
-   map (λci. signed_v_to_num (eval_const s.globals ci)) const_indices = map Some ns ∧
+   map signed_v_to_num vs = map Some ns ∧
    extract_value v.value ns = Some result
    ⇒
    step_instr prog s
      (Extractvalue r (t, a) const_indices) Tau
      (inc_pc (update_result r <| poison := v.poison; value := result |> s))) ∧
 
-  (∀prog s r t1 a1 t2 a2 const_indices result v1 v2 ns.
-   eval s a1 = Some v1 ∧
-   eval s a2 = Some v2 ∧
+  (∀prog s r t1 a1 t2 a2 const_indices result v1 v2 ns vs.
+   eval s a1 v1 ∧
+   eval s a2 v2 ∧
+   list_rel (eval_const s.globals) const_indices vs ∧
    (* The manual implies (but does not explicitly state) that the indices are
     * interpreted as signed numbers *)
-   map (λci. signed_v_to_num (eval_const s.globals ci)) const_indices = map Some ns ∧
+   map signed_v_to_num vs = map Some ns ∧
    insert_value v1.value v2.value ns = Some result
    ⇒
    step_instr prog s
@@ -601,7 +610,7 @@ Inductive step_instr:
                 <| poison := (v1.poison ∨ v2.poison); value := result |> s))) ∧
 
   (∀prog s r t t1 a1 ptr new_h v n n2.
-   eval s a1 = Some v ∧
+   eval s a1 v ∧
    (* TODO Question is the number to allocate interpreted as a signed or
     * unsigned quantity. E.g., if we allocate i8 0xFF does that do 255 or -1? *)
    signed_v_to_num v.value = Some n ∧
@@ -614,7 +623,7 @@ Inductive step_instr:
                 (s with heap := new_h)))) ∧
 
   (∀prog s r t t1 a1 pbytes w interval freeable p1.
-   eval s a1 = Some <| poison := p1; value := FlatV (PtrV w) |> ∧
+   eval s a1 <| poison := p1; value := FlatV (PtrV w) |> ∧
    interval = Interval freeable (w2n w) (w2n w + sizeof t) ∧
    is_allocated interval s.heap ∧
    pbytes = get_bytes s.heap interval ∧
@@ -627,8 +636,8 @@ Inductive step_instr:
                             s))) ∧
 
   (∀prog s t1 a1 t2 a2 obs p2 bytes w v1 freeable interval.
-   eval s a2 = Some <| poison := p2; value := FlatV (PtrV w) |> ∧
-   eval s a1 = Some v1 ∧
+   eval s a2 <| poison := p2; value := FlatV (PtrV w) |> ∧
+   eval s a1 v1 ∧
    interval = Interval freeable (w2n w) (w2n w + sizeof t1) ∧
    is_allocated interval s.heap ∧
    bytes = llvm_value_to_bytes v1.value ∧
@@ -640,8 +649,8 @@ Inductive step_instr:
      (inc_pc (s with heap := set_bytes p2 bytes (w2n w) s.heap))) ∧
 
   (∀prog s r t t1 a1 tindices v1 i1 indices v w1 i is off ptr.
-   map (eval s o snd) tindices = map Some (i1::indices) ∧
-   eval s a1 = Some v ∧
+   list_rel (eval s o snd) tindices (i1::indices) ∧
+   eval s a1 v ∧
    v.value = FlatV (PtrV w1) ∧
    (* The manual states that the indices are interpreted as signed numbers *)
    signed_v_to_num i1.value = Some i ∧
@@ -657,7 +666,7 @@ Inductive step_instr:
                s))) ∧
 
   (∀prog s cop r t1 a1 t v1 v2.
-   eval s a1 = Some v1 ∧
+   eval s a1 v1 ∧
    do_cast cop v1.value t = Some v2
    ⇒
    step_instr prog s
@@ -665,8 +674,8 @@ Inductive step_instr:
     (inc_pc (update_result r <| poison := v1.poison; value := v2 |> s))) ∧
 
   (∀prog s r c t a1 a2 v3 v1 v2.
-   eval s a1 = Some v1 ∧
-   eval s a2 = Some v2 ∧
+   eval s a1 v1 ∧
+   eval s a2 v2 ∧
    do_icmp c v1 v2 = Some v3
    ⇒
    step_instr prog s
@@ -675,7 +684,7 @@ Inductive step_instr:
 
   (∀prog s r t fname targs d vs.
    alookup prog fname = Some d ∧
-   map (eval s o snd) targs = map Some vs
+   list_rel (eval s o snd) targs vs
    ⇒
    step_instr prog s
      (Call r t fname targs) Tau
@@ -741,7 +750,7 @@ Inductive step:
  *)
  (∀p s updates from_l phis.
   get_instr p s.ip (Inr (from_l, phis)) ∧
-  map (do_phi from_l s) phis = map Some updates
+  list_rel (do_phi from_l s) phis updates
   ⇒
   step p s Tau (inc_pc (s with locals := s.locals |++ updates)))
 End
diff --git a/sledge/semantics/llvm_to_llairScript.sml b/sledge/semantics/llvm_to_llairScript.sml
index 62c45e03b..272f01a86 100644
--- a/sledge/semantics/llvm_to_llairScript.sml
+++ b/sledge/semantics/llvm_to_llairScript.sml
@@ -95,7 +95,7 @@ Definition translate_const_def:
     Record (map (λ(ty, c). translate_const gmap c) tcs)) ∧
   (translate_const gmap (ArrC tcs) =
     Record (map (λ(ty, c). translate_const gmap c) tcs)) ∧
-  (translate_const gmap (GlobalC g) = Var (translate_glob_var gmap g)) ∧
+  (translate_const gmap (GlobalC g) = Var (translate_glob_var gmap g) T) ∧
   (* TODO *)
   (translate_const gmap (GepC _ _ _ _) = ARB) ∧
   (translate_const gmap UndefC = Nondet)
@@ -112,7 +112,7 @@ Definition translate_arg_def:
     (* With the current strategy of threading the emap through the whole
      * function, we should never get a None here.
      *)
-    | None => Var (translate_reg r (IntT W64))
+    | None => Var (translate_reg r (IntT W64)) F
     | Some e => e)
 End
 
@@ -271,8 +271,8 @@ Definition classify_instr_def:
 End
 
 Definition extend_emap_non_exp_def:
-  (extend_emap_non_exp emap (Load r t _) = emap |+ (r, Var (translate_reg r t))) ∧
-  (extend_emap_non_exp emap (Call r t _ _) = emap |+ (r, Var (translate_reg r t))) ∧
+  (extend_emap_non_exp emap (Load r t _) = emap |+ (r, Var (translate_reg r t) F)) ∧
+  (extend_emap_non_exp emap (Call r t _ _) = emap |+ (r, Var (translate_reg r t) F)) ∧
   (extend_emap_non_exp emap _ = emap)
 End
 
@@ -317,7 +317,7 @@ Definition translate_instrs_def:
       let x = translate_reg r t in
       let e = translate_instr_to_exp gmap emap i in
         if r ∈ reg_to_keep then
-          let (bs, emap') = translate_instrs l gmap (emap |+ (r, Var x)) reg_to_keep is in
+          let (bs, emap') = translate_instrs l gmap (emap |+ (r, Var x F)) reg_to_keep is in
             (add_to_first_block (Move [(x, e)]) bs, emap')
         else
           translate_instrs l gmap (emap |+ (r, e)) reg_to_keep is
@@ -367,7 +367,7 @@ End
 Definition header_to_emap_upd_def:
   (header_to_emap_upd Entry = []) ∧
   (header_to_emap_upd (Head phis _) =
-    map (λx. case x of Phi r t largs => (r, Var (translate_reg r t))) phis)
+    map (λx. case x of Phi r t largs => (r, Var (translate_reg r t) F)) phis)
 End
 
 Definition translate_block_def:
diff --git a/sledge/semantics/llvm_to_llair_propScript.sml b/sledge/semantics/llvm_to_llair_propScript.sml
index 25d2eac83..c8dbe2dcb 100644
--- a/sledge/semantics/llvm_to_llair_propScript.sml
+++ b/sledge/semantics/llvm_to_llair_propScript.sml
@@ -48,19 +48,6 @@ Definition num_calls_def:
   num_calls is = length (filter is_call is)
 End
 
-(* TODO: remove?
-Definition build_phi_block_def:
-  build_phi_block gmap emap f entry from_l to_l phis =
-    generate_move_block [(to_l, (translate_header (dest_fn f) gmap emap entry (Head phis ARB), (ARB:block)))]
-      (translate_label_opt (dest_fn f) entry from_l) to_l
-End
-
-Definition build_phi_emap_def:
-  build_phi_emap phis =
-    map (\x. case x of Phi r t _ => (r, Var (translate_reg r t))) phis
-End
-*)
-
 Inductive pc_rel:
  (* LLVM side points to a normal instruction *)
  (∀prog emap ip bp d b idx b' prev_i gmap rest.
@@ -105,31 +92,37 @@ End
  *)
 
 Definition emap_invariant_def:
-  emap_invariant prog emap ip locals locals' r =
+  emap_invariant prog emap s s' r =
     ∃v v' e.
       v_rel v.value v' ∧
-      flookup locals r = Some v ∧
-      flookup emap r = Some e ∧ eval_exp <| locals := locals' |> e v' ∧
+      flookup s.locals r = Some v ∧
+      flookup emap r = Some e ∧ eval_exp s' e v' ∧
       (* Each register used in e is dominated by an assignment to that
        * register for the entire live range of r. *)
-      (∀ip1 r'. ip1.f = ip.f ∧ r ∈ live prog ip1 ∧ r' ∈ exp_uses e ⇒
+      (∀ip1 r'. ip1.f = s.ip.f ∧ r ∈ live prog ip1 ∧ r' ∈ exp_uses e ⇒
         ∃ip2. untranslate_reg r' ∈ assigns prog ip2 ∧ dominates prog ip2 ip1)
 End
 
 Definition local_state_rel_def:
-  local_state_rel prog emap ip locals locals' ⇔
+  local_state_rel prog emap s s' ⇔
     (* Live LLVM registers are mapped and have a related value in the emap
      * (after evaluating) *)
-    (∀r. r ∈ live prog ip ⇒ emap_invariant prog emap ip locals locals' r)
+    (∀r. r ∈ live prog s.ip ⇒ emap_invariant prog emap s s' r)
+End
+
+Definition globals_rel_def:
+  globals_rel gmap gl gl' ⇔
+    BIJ (translate_glob_var gmap) (fdom gl) (fdom gl') ∧
+    ∀k. k ∈ fdom gl ⇒
+      nfits (w2n (snd (gl ' k))) llair$pointer_size ∧
+      w2n (snd (gl ' k)) = gl' ' (translate_glob_var gmap k)
 End
 
 Definition mem_state_rel_def:
   mem_state_rel prog gmap emap (s:llvm$state) (s':llair$state) ⇔
-    local_state_rel prog emap s.ip s.locals s'.locals ∧
+    local_state_rel prog emap s s' ∧
     reachable prog s.ip ∧
-    fmap_rel (\(_,n) n'. w2n n = n')
-      s.globals
-      (s'.glob_addrs f_o translate_glob_var gmap) ∧
+    globals_rel gmap s.globals s'.glob_addrs ∧
     heap_ok s.heap ∧
     erase_tags s.heap = s'.heap ∧
     s.status = s'.status
@@ -159,7 +152,8 @@ Proof
 QED
 
 Triviality lemma:
-  ((s:llair$state) with status := Complete code).locals = s.locals
+  ((s:llair$state) with status := Complete code).locals = s.locals ∧
+  ((s:llair$state) with status := Complete code).glob_addrs = s.glob_addrs
 Proof
   rw []
 QED
@@ -189,12 +183,6 @@ Proof
   >- metis_tac [next_ips_reachable]
 QED
 
-Triviality record_lemma:
-  (<|locals := x|> :llair$state).locals = x
-Proof
-  rw []
-QED
-
 Theorem mem_state_rel_update:
   ∀prog gmap emap s1 s1' v res_v r e i.
   is_ssa prog ∧
@@ -214,8 +202,7 @@ Proof
   >- (
     rw [FLOOKUP_UPDATE]
     >- (
-      HINT_EXISTS_TAC >> rw []
-      >- metis_tac [eval_exp_ignores, record_lemma] >>
+      HINT_EXISTS_TAC >> rw [] >>
       first_x_assum drule >> rw [] >>
       first_x_assum drule >> rw [] >>
       fs [exp_uses_def, translate_arg_def] >>
@@ -234,15 +221,15 @@ Proof
 QED
 
 Theorem emap_inv_updates_keep_same_ip1:
-  ∀prog emap ip locals locals' vs res_vs rtys r.
+  ∀prog emap ip s s' vs res_vs rtys r.
   is_ssa prog ∧
   list_rel v_rel (map (\v. v.value) vs) res_vs ∧
   length rtys = length vs ∧
   r ∈ set (map fst rtys)
   ⇒
-  emap_invariant prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty))) rtys) ip
-        (locals |++ zip (map fst rtys, vs))
-        (locals' |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs))
+  emap_invariant prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty) F)) rtys)
+        (s with locals := s.locals |++ zip (map fst rtys, vs))
+        (s' with locals := s'.locals |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs))
         r
 Proof
   rw [emap_invariant_def, flookup_fupdate_list] >>
@@ -308,9 +295,10 @@ Proof
   >- (
     fs [exp_uses_def] >> rw [] >>
     Cases_on `fst rty` >> simp [translate_reg_def, untranslate_reg_def] >>
-    `∃ip. ip.f = ip1.f ∧ Reg s ∈ uses prog ip`
+    rename1 `Reg r ∈ assigns _ _` >>
+    `∃ip. ip.f = ip1.f ∧ Reg r ∈ uses prog ip`
     by (
-      qabbrev_tac `x = (ip1.f = ip.f)` >>
+      qabbrev_tac `x = (ip1.f = s.ip.f)` >>
       fs [live_def] >> qexists_tac `last (ip1::path)` >> rw [] >>
       irule good_path_same_func >>
       qexists_tac `ip1::path` >> rw [MEM_LAST] >>
@@ -319,19 +307,19 @@ Proof
 QED
 
 Theorem emap_inv_updates_keep_same_ip2:
-  ∀prog emap ip locals locals' vs res_vs rtys r.
+  ∀prog emap s s' vs res_vs rtys r.
   is_ssa prog ∧
-  r ∈ live prog ip ∧
-  assigns prog ip = set (map fst rtys) ∧
-  emap_invariant prog emap ip locals locals' r ∧
+  r ∈ live prog s.ip ∧
+  assigns prog s.ip = set (map fst rtys) ∧
+  emap_invariant prog emap s s' r ∧
   list_rel v_rel (map (\v. v.value) vs) res_vs ∧
   length rtys = length vs ∧
-  reachable prog ip ∧
+  reachable prog s.ip ∧
   ¬mem r (map fst rtys)
   ⇒
-  emap_invariant prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty))) rtys) ip
-        (locals |++ zip (map fst rtys, vs))
-        (locals' |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs))
+  emap_invariant prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty) F)) rtys)
+        (s with locals := s.locals |++ zip (map fst rtys, vs))
+        (s' with locals := s'.locals |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs))
         r
 Proof
   rw [emap_invariant_def, alistTheory.flookup_fupdate_list] >> rw [] >>
@@ -340,10 +328,11 @@ Proof
     CASE_TAC >> rw []
     >- (
       qexists_tac `v'` >> rw [] >>
-      `DRESTRICT (locals' |++ zip (map (λ(r,ty). translate_reg r ty) rtys, res_vs)) (exp_uses e) =
-       DRESTRICT locals' (exp_uses e)`
-      suffices_by metis_tac [eval_exp_ignores_unused, record_lemma] >>
-      rw [] >>
+      qmatch_goalsub_abbrev_tac `eval_exp s_upd _ _` >>
+      `DRESTRICT s_upd.locals (exp_uses e) = DRESTRICT s'.locals (exp_uses e) ∧
+       s_upd.glob_addrs = s'.glob_addrs`
+      suffices_by metis_tac [eval_exp_ignores_unused] >>
+      rw [Abbr `s_upd`] >>
       qmatch_goalsub_abbrev_tac `_ |++ l = _` >>
       `l = []` suffices_by rw [FUPDATE_LIST_THM] >>
       rw [Abbr `l`, FILTER_EQ_NIL, LAMBDA_PROD] >>
@@ -353,13 +342,14 @@ Proof
       rw [every_zip_fst, EVERY_MAP] >> rw [LAMBDA_PROD] >>
       rw [EVERY_EL] >> pairarg_tac >> rw [] >>
       qmatch_goalsub_rename_tac `translate_reg r1 ty1 ∉ exp_uses _` >>
-      first_x_assum (qspecl_then [`ip`, `translate_reg r1 ty1`] mp_tac) >> rw [] >>
+      first_x_assum (qspecl_then [`s.ip`, `translate_reg r1 ty1`] mp_tac) >> rw [] >>
       CCONTR_TAC >> fs [] >>
-      `ip2 = ip`
+      `ip2 = s.ip`
       by (
         fs [is_ssa_def, EXTENSION, IN_DEF] >>
         Cases_on `r1` >> fs [translate_reg_def, untranslate_reg_def] >>
-        `assigns prog ip (Reg s)` suffices_by metis_tac [reachable_dominates_same_func] >>
+        rename1 `Reg reg` >>
+        `assigns prog s.ip (Reg reg)` suffices_by metis_tac [reachable_dominates_same_func] >>
         rw [LIST_TO_SET_MAP, MEM_EL] >>
         metis_tac [FST]) >>
       metis_tac [dominates_irrefl]) >>
@@ -371,15 +361,15 @@ Proof
 QED
 
 Theorem local_state_rel_next_ip:
-  ∀prog emap ip1 ip2 locals locals'.
-  local_state_rel prog emap ip1 locals locals' ∧
-  ip2 ∈ next_ips prog ip1 ∧
-  (∀r. r ∈ assigns prog ip1 ⇒ emap_invariant prog emap ip1 locals locals' r)
+  ∀prog emap ip2 s s'.
+  local_state_rel prog emap s s' ∧
+  ip2 ∈ next_ips prog s.ip ∧
+  (∀r. r ∈ assigns prog s.ip ⇒ emap_invariant prog emap s s' r)
   ⇒
-  local_state_rel prog emap ip2 locals locals'
+  local_state_rel prog emap (s with ip := ip2) s'
 Proof
   rw [local_state_rel_def, emap_invariant_def] >>
-  Cases_on `r ∈ live prog ip1` >> fs []
+  Cases_on `r ∈ live prog s.ip` >> fs []
   >- (
     last_x_assum drule >> rw [] >>
     ntac 3 HINT_EXISTS_TAC >> rw [] >>
@@ -394,44 +384,43 @@ Proof
 QED
 
 Theorem local_state_rel_updates_keep:
-  ∀rtys prog emap ip locals locals' vs res_vs i.
+  ∀rtys prog emap s s' vs res_vs i.
   is_ssa prog ∧
-  set (map fst rtys) = assigns prog ip ∧
-  local_state_rel prog emap ip locals locals' ∧
+  set (map fst rtys) = assigns prog s.ip ∧
+  local_state_rel prog emap s s' ∧
   length vs = length rtys ∧
   list_rel v_rel (map (\v. v.value) vs) res_vs ∧
-  i ∈ next_ips prog ip ∧
-  reachable prog ip
+  i ∈ next_ips prog s.ip ∧
+  reachable prog s.ip
   ⇒
-  local_state_rel prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty))) rtys) i
-        (locals |++ zip (map fst rtys, vs))
-        (locals' |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs))
+  local_state_rel prog (emap |++ map (\(r,ty). (r, Var (translate_reg r ty) F)) rtys)
+        (s with <| ip := i; locals := s.locals |++ zip (map fst rtys, vs) |>)
+        (s' with locals := s'.locals |++ zip (map (\(r,ty). translate_reg r ty) rtys, res_vs))
 Proof
   rw [] >> irule local_state_rel_next_ip >>
-  qexists_tac `ip` >> rw [] >>
   fs [local_state_rel_def] >> rw []
   >- (irule emap_inv_updates_keep_same_ip1 >> rw []) >>
-  fs [local_state_rel_def] >> rw [] >>
   Cases_on `mem r (map fst rtys)`
   >- (irule emap_inv_updates_keep_same_ip1 >> rw []) >>
   irule emap_inv_updates_keep_same_ip2 >> rw []
 QED
 
 Theorem local_state_rel_update_keep:
-  ∀prog emap ip locals locals' v res_v r i ty.
+  ∀prog emap s s' v res_v r i ty.
   is_ssa prog ∧
-  assigns prog ip = {r} ∧
-  local_state_rel prog emap ip locals locals' ∧
+  assigns prog s.ip = {r} ∧
+  local_state_rel prog emap s s' ∧
   v_rel v.value res_v ∧
-  reachable prog ip ∧
-  i ∈ next_ips prog ip
+  reachable prog s.ip ∧
+  i ∈ next_ips prog s.ip
   ⇒
-  local_state_rel prog (emap |+ (r, Var (translate_reg r ty)))
-        i (locals |+ (r, v)) (locals' |+ (translate_reg r ty, res_v))
+  local_state_rel prog (emap |+ (r, Var (translate_reg r ty) F))
+        (s with <| ip := i; locals := s.locals |+ (r, v) |>)
+        (s' with locals := s'.locals |+ (translate_reg r ty, res_v))
 Proof
   rw [] >>
   drule local_state_rel_updates_keep >>
-  disch_then (qspecl_then [`[(r,ty)]`, `emap`, `ip`] mp_tac) >>
+  disch_then (qspecl_then [`[(r,ty)]`, `emap`, `s`] mp_tac) >>
   simp [] >> disch_then drule >>
   disch_then (qspecl_then [`[v]`, `[res_v]`] mp_tac) >>
   simp [] >> disch_then drule >>
@@ -447,7 +436,7 @@ Theorem mem_state_rel_update_keep:
   reachable prog s.ip ∧
   i ∈ next_ips prog s.ip
   ⇒
-  mem_state_rel prog gmap (emap |+ (r, Var (translate_reg r ty)))
+  mem_state_rel prog gmap (emap |+ (r, Var (translate_reg r ty) F))
         (s with <| ip := i; locals := s.locals |+ (r, v) |>)
         (s' with locals := s'.locals |+ (translate_reg r ty, res_v))
 Proof
@@ -457,7 +446,8 @@ Proof
 QED
 
 Triviality lemma:
-  ((s:llair$state) with heap := h).locals = s.locals
+  ((s:llair$state) with heap := h).locals = s.locals ∧
+  ((s:llair$state) with heap := h).glob_addrs = s.glob_addrs
 Proof
   rw []
 QED
@@ -475,6 +465,9 @@ Proof
   fs [fmap_eq_flookup, FLOOKUP_o_f] >> rw [] >>
   first_x_assum (qspec_then `x` mp_tac) >>
   BasicProvers.EVERY_CASE_TAC >> rw [] >>
+  fs [emap_invariant_def]
+  >- metis_tac [eval_exp_ignores, lemma]
+  >- metis_tac [eval_exp_ignores, lemma] >>
   Cases_on `x'` >> Cases_on `x''` >> fs []
 QED
 
@@ -988,57 +981,82 @@ Proof
   pairarg_tac >> fs []
 QED
 
+Triviality n2i_lem:
+  ∀n. nfits n llair$pointer_size ⇒
+    n2i n llair$pointer_size = IntV (w2i (n2w n : word64)) llair$pointer_size
+Proof
+  rw [pointer_size_def] >>
+  `2 ** 64 = dimword (:64)` by rw [dimword_64] >>
+  full_simp_tac bool_ss [nfits_def] >>
+  drule w2i_n2w >> rw []
+QED
+
 Theorem translate_constant_correct_lem:
-  (∀c s prog gmap emap s'.
-   mem_state_rel prog gmap emap s s'
+  (∀c s prog gmap emap s' v.
+   mem_state_rel prog gmap emap s s' ∧
+   eval_const s.globals c v
    ⇒
-   ∃v'. eval_exp s' (translate_const gmap c) v' ∧ v_rel (eval_const s.globals c) v') ∧
-  (∀(cs : (ty # const) list) s prog gmap emap s'.
-   mem_state_rel prog gmap emap s s'
+   ∃v'. eval_exp s' (translate_const gmap c) v' ∧ v_rel v v') ∧
+  (∀(cs : (ty # const) list) s prog gmap emap s' vs.
+   mem_state_rel prog gmap emap s s' ∧
+   list_rel (eval_const s.globals o snd) cs vs
    ⇒
-   ∃v'. list_rel (eval_exp s') (map (translate_const gmap o snd) cs) v' ∧ list_rel v_rel (map (eval_const s.globals o snd) cs) v') ∧
-  (∀(tc : ty # const) s prog gmap emap s'.
-   mem_state_rel prog gmap emap s s'
+   ∃v'. list_rel (eval_exp s') (map (translate_const gmap o snd) cs) v' ∧ list_rel v_rel vs v') ∧
+  (∀(tc : ty # const) s prog gmap emap s' v.
+   mem_state_rel prog gmap emap s s' ∧
+   eval_const s.globals (snd tc) v
    ⇒
-   ∃v'. eval_exp s' (translate_const gmap (snd tc)) v' ∧ v_rel (eval_const s.globals (snd tc)) v')
+   ∃v'. eval_exp s' (translate_const gmap (snd tc)) v' ∧ v_rel v v')
 Proof
   ho_match_mp_tac const_induction >> rw [translate_const_def] >>
-  simp [Once eval_exp_cases, eval_const_def]
+  pop_assum mp_tac >> simp [Once eval_const_cases]
   >- (
-    Cases_on `s` >> simp [eval_const_def, translate_size_def, v_rel_cases] >>
+    rw [Once eval_exp_cases] >>
+    simp [Once eval_const_cases, translate_size_def, v_rel_cases] >>
     metis_tac [truncate_2comp_i2w_w2i, dimindex_1, dimindex_8, dimindex_32, dimindex_64])
   >- (
+    rw [Once eval_exp_cases] >>
     simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
-    fs [combinTheory.o_DEF, LAMBDA_PROD] >>
-    metis_tac [])
+    fs [combinTheory.o_DEF, LAMBDA_PROD] >> rw [] >>
+    first_x_assum drule >> disch_then irule >>
+    fs [LIST_REL_EL_EQN] >> rw [] >> rfs [] >>
+    first_x_assum drule  >>
+    simp [EL_MAP] >>
+    Cases_on `el n cs` >> simp [])
   >- (
+    rw [Once eval_exp_cases] >>
     simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
-    fs [combinTheory.o_DEF, LAMBDA_PROD] >>
-    metis_tac [])
-  (* TODO: unimplemented stuff *)
+    fs [combinTheory.o_DEF, LAMBDA_PROD] >> rw [] >>
+    first_x_assum drule >> disch_then irule >>
+    fs [LIST_REL_EL_EQN] >> rw [] >> rfs [] >>
+    first_x_assum drule  >>
+    simp [EL_MAP] >>
+    Cases_on `el n cs` >> simp [])
+  (* TODO: unimplemented GEP stuff *)
   >- cheat
   >- (
-    fs [mem_state_rel_def, fmap_rel_OPTREL_FLOOKUP] >>
-    CASE_TAC >> fs [] >> first_x_assum (qspec_then `g` mp_tac) >> rw [] >>
-    rename1 `option_rel _ _ opt` >> Cases_on `opt` >> fs [OPTREL_def] >>
-    (* TODO: false at the moment, need to work out the llair story on globals *)
-    cheat)
-  (* TODO: unimplemented stuff *)
-  >- cheat
-  >- cheat
+    rw [Once eval_exp_cases] >> simp [v_rel_cases] >>
+    fs [mem_state_rel_def, globals_rel_def] >>
+    first_x_assum (qspec_then `g` mp_tac) >> rw [] >>
+    qexists_tac `w2n w` >> rw [] >> fs [FLOOKUP_DEF]
+    >- (
+      rfs [] >>
+      qpat_x_assum `w2n _ = _` (mp_tac o GSYM) >> rw [] >>
+      simp [n2i_lem])
+    >- rfs [BIJ_DEF, INJ_DEF, SURJ_DEF])
+  >- metis_tac []
 QED
 
 Theorem translate_constant_correct:
-  ∀c s prog gmap emap s' g.
-   mem_state_rel prog gmap emap s s'
+  ∀c s prog gmap emap s' g v.
+   mem_state_rel prog gmap emap s s' ∧
+   eval_const s.globals c v
    ⇒
-   ∃v'. eval_exp s' (translate_const gmap c) v' ∧ v_rel (eval_const s.globals c) v'
+   ∃v'. eval_exp s' (translate_const gmap c) v' ∧ v_rel v v'
 Proof
   metis_tac [translate_constant_correct_lem]
 QED
 
-(* TODO: This isn't true, since the translation turns LLVM globals into llair
- * locals *)
 Theorem translate_const_no_reg[simp]:
   ∀gmap c. r ∉ exp_uses (translate_const gmap c)
 Proof
@@ -1046,22 +1064,22 @@ Proof
   rw [translate_const_def, exp_uses_def, MEM_MAP, METIS_PROVE [] ``x ∨ y ⇔ (~x ⇒ y)``]
   >- (pairarg_tac >> fs [] >> metis_tac [])
   >- (pairarg_tac >> fs [] >> metis_tac [])
-  >- cheat
+  (* TODO: unimplemented GEP stuff *)
   >- cheat
 QED
 
 Theorem translate_arg_correct:
   ∀s a v prog gmap emap s'.
   mem_state_rel prog gmap emap s s' ∧
-  eval s a = Some v ∧
+  eval s a v ∧
   arg_to_regs a ⊆ live prog s.ip
   ⇒
   ∃v'. eval_exp s' (translate_arg gmap emap a) v' ∧ v_rel v.value v'
 Proof
-  Cases_on `a` >> rw [eval_def, translate_arg_def] >> rw []
+  Cases_on `a` >> rw [eval_cases, translate_arg_def] >> rw []
   >- metis_tac [translate_constant_correct] >>
   CASE_TAC >> fs [PULL_EXISTS, mem_state_rel_def, local_state_rel_def, emap_invariant_def, arg_to_regs_def] >>
-  res_tac >> rfs [] >> metis_tac [eval_exp_ignores, record_lemma]
+  res_tac >> rfs [] >> metis_tac [eval_exp_ignores]
 QED
 
 Theorem is_allocated_mem_state_rel:
@@ -1154,9 +1172,10 @@ Proof
 QED
 
 Theorem translate_extract_correct:
-  ∀prog gmap emap s1 s1' a v v1' e1' cs ns result.
+  ∀prog gmap emap s1 s1' a v v1' e1' cs vs ns result.
     mem_state_rel prog gmap emap s1 s1' ∧
-    map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧
+    list_rel (eval_const s1.globals) cs vs ∧
+    map signed_v_to_num vs = map Some ns ∧
     extract_value v ns = Some result ∧
     eval_exp s1' e1' v1' ∧
     v_rel v v1'
@@ -1165,12 +1184,13 @@ Theorem translate_extract_correct:
       eval_exp s1' (foldl (λe c. Select e (translate_const gmap c)) e1' cs) v2' ∧
       v_rel result v2'
 Proof
-  Induct_on `cs` >> rw [] >> fs [extract_value_def]
+  Induct_on `cs` >> rw [] >> rfs [] >> fs [extract_value_def]
   >- metis_tac [] >>
   first_x_assum irule >>
   Cases_on `ns` >> fs [] >>
   qmatch_goalsub_rename_tac `translate_const gmap c` >>
-  `∃v2'. eval_exp s1' (translate_const gmap c) v2' ∧ v_rel (eval_const s1.globals c) v2'`
+  qmatch_assum_rename_tac `eval_const _ _ v3` >>
+  `∃v2'. eval_exp s1' (translate_const gmap c) v2' ∧ v_rel v3 v2'`
   by metis_tac [translate_constant_correct] >>
   Cases_on `v` >> fs [extract_value_def] >>
   qpat_x_assum `v_rel (AggV _) _` mp_tac >>
@@ -1178,7 +1198,7 @@ Proof
   simp [Once eval_exp_cases, PULL_EXISTS] >>
   fs [LIST_REL_EL_EQN] >>
   qmatch_assum_rename_tac `_ = map Some is` >>
-  Cases_on `eval_const s1.globals c` >> fs [signed_v_to_num_def, signed_v_to_int_def] >> rw [] >>
+  Cases_on `v3` >> fs [signed_v_to_num_def, signed_v_to_int_def] >> rw [] >>
   `∃i. v2' = FlatV i` by fs [v_rel_cases] >> fs [] >>
   qmatch_assum_rename_tac `option_join _ = Some x` >>
   `∃size. i = IntV (&x) size` suffices_by metis_tac [] >> rw [] >>
@@ -1188,9 +1208,10 @@ Proof
 QED
 
 Theorem translate_update_correct:
-  ∀prog gmap emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs ns result.
+  ∀prog gmap emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs vs ns result.
     mem_state_rel prog gmap emap s1 s1' ∧
-    map (λci. signed_v_to_num (eval_const s1.globals ci)) cs = map Some ns ∧
+    list_rel (eval_const s1.globals) cs vs ∧
+    map signed_v_to_num vs = map Some ns ∧
     insert_value v1 v2 ns = Some result ∧
     eval_exp s1' e1' v1' ∧
     v_rel v1 v1' ∧
@@ -1201,7 +1222,7 @@ Theorem translate_update_correct:
       eval_exp s1' (translate_updatevalue gmap e1' e2' cs) v3' ∧
       v_rel result v3'
 Proof
-  Induct_on `cs` >> rw [] >> fs [insert_value_def, translate_updatevalue_def]
+  Induct_on `cs` >> rw [] >> rfs [] >> fs [insert_value_def, translate_updatevalue_def]
   >- metis_tac [] >>
   simp [Once eval_exp_cases, PULL_EXISTS] >>
   Cases_on `ns` >> fs [] >>
@@ -1212,7 +1233,8 @@ Proof
   simp [v_rel_cases] >>
   qmatch_goalsub_rename_tac `translate_const gmap c` >>
   qexists_tac `vs2` >> simp [] >>
-  `∃v4'. eval_exp s1' (translate_const gmap c) v4' ∧ v_rel (eval_const s1.globals c) v4'`
+  qmatch_assum_rename_tac `eval_const _ _ v3` >>
+  `∃v4'. eval_exp s1' (translate_const gmap c) v4' ∧ v_rel v3 v4'`
   by metis_tac [translate_constant_correct] >>
   `∃idx_size. v4' = FlatV (IntV (&x) idx_size)`
   by (
@@ -1222,6 +1244,7 @@ Proof
   first_x_assum drule >>
   disch_then drule >>
   disch_then drule >>
+  disch_then drule >>
   disch_then (qspecl_then [`el x vs2`, `v2'`, `e2'`, `Select e1' (translate_const gmap c)`] mp_tac) >>
   simp [Once eval_exp_cases] >>
   metis_tac [EVERY2_LUPDATE_same, LIST_REL_LENGTH, LIST_REL_EL_EQN]
@@ -1344,8 +1367,7 @@ Theorem const_idx_uses[simp]:
   ∀cs gmap e.
     exp_uses (foldl (λe c. Select e (translate_const gmap c)) e cs) = exp_uses e
 Proof
-  Induct_on `cs` >> rw [exp_uses_def] >>
-  rw [translate_const_no_reg, EXTENSION]
+  Induct_on `cs` >> rw [exp_uses_def] >> rw [EXTENSION]
 QED
 
 Theorem exp_uses_trans_upd_val[simp]:
@@ -1353,7 +1375,7 @@ Theorem exp_uses_trans_upd_val[simp]:
     (if cs = [] then {} else exp_uses e1) ∪ exp_uses e2
 Proof
   Induct_on `cs` >> rw [exp_uses_def, translate_updatevalue_def] >>
-  rw [translate_const_no_reg, EXTENSION] >>
+  rw [EXTENSION] >>
   metis_tac []
 QED
 
@@ -1372,7 +1394,7 @@ Theorem translate_instr_to_exp_correct:
       mem_state_rel prog gmap emap' s2 s2' ∧
       (r ∉ regs_to_keep ⇒ s1' = s2' ∧ emap' = emap |+ (r, translate_instr_to_exp gmap emap instr)) ∧
       (r ∈ regs_to_keep ⇒
-       emap' = emap |+ (r,Var (translate_reg r t)) ∧
+       emap' = emap |+ (r,Var (translate_reg r t) F) ∧
        step_inst s1' (Move [(translate_reg r t, translate_instr_to_exp gmap emap instr)]) Tau s2')
 Proof
   recInduct translate_instr_to_exp_ind >>
@@ -1476,9 +1498,9 @@ Proof
             instr_uses_def]) >>
     drule translate_update_correct >> rpt (disch_then drule) >>
     first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
-    disch_then drule >>
+    disch_then drule >> disch_then drule >>
     first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
-    disch_then drule >>
+    disch_then drule >> disch_then drule >>
     simp [] >> strip_tac >> strip_tac >>
     disch_then (qspecl_then [`v'`, `v''`] mp_tac) >> simp [] >>
     disch_then drule >> disch_then drule >>
@@ -1658,15 +1680,25 @@ Proof
       fs [is_allocated_def, heap_component_equality, erase_tags_def] >>
       metis_tac [])
     >- (
-      (* TODO: mem_state_rel needs to relate the globals *)
       fs [get_obs_cases, llvmTheory.get_obs_cases] >> rw [translate_trace_def] >>
-      fs [mem_state_rel_def, fmap_rel_OPTREL_FLOOKUP]
+      fs [mem_state_rel_def, globals_rel_def]
       >- (
-        first_x_assum (qspec_then `x` mp_tac) >> rw [] >>
-        rename1 `option_rel _ _ opt` >> Cases_on `opt` >>
-        fs [OPTREL_def] >>
-        cheat) >>
-      cheat))
+        fs [FLOOKUP_DEF] >>
+        first_x_assum drule >> rw []
+        >- metis_tac [BIJ_DEF, SURJ_DEF] >>
+        pop_assum (mp_tac o GSYM) >> rw [w2n_i2n])
+      >- (
+        CCONTR_TAC >> fs [FRANGE_DEF] >>
+        fs [BIJ_DEF, SURJ_DEF, INJ_DEF] >>
+        first_x_assum drule >> rw [] >>
+        CCONTR_TAC >> fs [] >> rw [] >>
+        first_x_assum drule >> rw [] >>
+        CCONTR_TAC >> fs [] >> rw [] >>
+        `i2n (IntV (w2i w) (dimindex (:64))) = w2n w` by metis_tac [w2n_i2n, dimindex_64] >>
+        fs [] >> rw [] >>
+        fs [METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
+        first_x_assum drule >> rw [] >>
+        metis_tac [pair_CASES, SND])))
 QED
 
 Theorem classify_instr_term_call:
@@ -1949,7 +1981,7 @@ QED
 Theorem do_phi_vals:
   ∀prog gmap emap from_l s s' phis updates.
     mem_state_rel prog gmap emap s s' ∧
-    map (do_phi from_l s) phis = map Some updates ∧
+    list_rel (do_phi from_l s) phis updates ∧
     BIGUNION (set (map (phi_uses from_l) phis)) ⊆ live prog s.ip
     ⇒
     ∃es vs.
@@ -1963,9 +1995,9 @@ Theorem do_phi_vals:
           phis
       = map2 (\p. λe. case p of Phi r t largs => (translate_reg r t, e)) phis es
 Proof
-  Induct_on `phis` >> rw [] >> Cases_on `updates` >> fs [] >>
-  first_x_assum drule >> disch_then drule >> rw [] >>
-  Cases_on `h` >> fs [do_phi_def, OPTION_JOIN_EQ_SOME] >>
+  Induct_on `phis` >> rw [] >> fs [] >>
+  first_x_assum drule >> disch_then drule >> rw [PULL_EXISTS] >>
+  Cases_on `h` >> fs [do_phi_cases] >>
   drule translate_arg_correct >>
   disch_then drule >>
   impl_tac
@@ -2009,7 +2041,7 @@ Theorem build_phi_block_correct:
   ∀prog s1 s1' to_l from_l phis updates f gmap emap entry bloc.
     prog_ok prog ∧ is_ssa prog ∧
     get_instr prog s1.ip (Inr (from_l,phis)) ∧
-    map (do_phi from_l s1) phis = map Some updates ∧
+    list_rel (do_phi from_l s1) phis updates ∧
     mem_state_rel prog gmap emap s1 s1' ∧
     BIGUNION (set (map (phi_uses from_l) phis)) ⊆ live prog s1.ip ∧
     bloc = generate_move_block f gmap emap phis from_l to_l
@@ -2069,7 +2101,7 @@ Proof
     by (
       qpat_x_assum `map fst _ = map phi_assigns _` mp_tac >>
       simp [LIST_EQ_REWRITE, EL_MAP] >>
-      `length phis = length updates` by metis_tac [LENGTH_MAP] >>
+      `length phis = length updates` by metis_tac [LIST_REL_LENGTH] >>
       rw [EL_ZIP, LENGTH_MAP, EL_MAP] >>
       rename1 `_ = el n updates` >>
       first_x_assum drule >>
@@ -2138,6 +2170,7 @@ Theorem multi_step_to_step_block:
       filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace (get_gmap prog)) tr) ∧
       state_rel prog (get_gmap prog) emap2 s2 s2'
 Proof
+
   rw [] >> pop_assum mp_tac >> simp [Once state_rel_def] >> rw [Once pc_rel_cases]
   >- (
     (* Non-phi instruction *)
@@ -2153,6 +2186,7 @@ Proof
   qpat_x_assum `last_step _ _ _ _` mp_tac >>
   simp [last_step_cases] >> strip_tac
   >- (
+
     fs [llvmTheory.step_cases]
     >- metis_tac [get_instr_func, sum_distinct] >>
     fs [translate_trace_def] >> rw [] >>
@@ -2170,6 +2204,12 @@ Proof
       fs [get_instr_cases] >>
       rfs [] >> rw [] >> fs []) >>
     first_x_assum drule >> rw [] >>
+    rename1 `generate_move_block _ _ emap1` >>
+
+    `mem_state_rel prog (get_gmap prog) emap1 s1 s1'`
+    by (
+      fs [mem_state_rel_def, local_state_rel_def] >>
+      cheat) >>
     qmatch_assum_abbrev_tac `get_block _ _ bloc` >>
     GEN_EXISTS_TAC "b" `bloc` >>
     rw [] >>
@@ -2182,13 +2222,8 @@ Proof
       drule get_instr_live >> rw [SUBSET_DEF, uses_cases, IN_DEF] >>
       first_x_assum irule >> disj2_tac >> metis_tac []) >>
     rw [] >>
-    qexists_tac `s2'` >> qexists_tac `emap |++ header_to_emap_upd (Head phis None)` >>
-    qexists_tac `[Tau; Tau]` >> rw []
-    >- (
-      (* TODO: This isn't true and will require a more subtle treatment of the
-       * emap in this proof overall *)
-      `emap = emap'` by cheat >>
-      metis_tac []) >>
+    qexists_tac `s2'` >> qexists_tac `emap1 |++ header_to_emap_upd (Head phis None)` >>
+    qexists_tac `[Tau; Tau]` >> rw [] >>
     fs [state_rel_def] >> rw [] >>
     fs [llvmTheory.inc_pc_def] >>
     fs [pc_rel_cases, get_instr_cases, PULL_EXISTS, translate_label_def,
@@ -2206,16 +2241,17 @@ Proof
     by (
       fs [prog_ok_def] >> res_tac >> fs [] >>
       fs [EVERY_MEM]) >>
+
     drule alookup_translate_blocks >> rpt (disch_then drule) >>
     simp [translate_label_def] >>
     disch_then (qspecl_then [`s`, `get_gmap prog`, `fempty`, `get_regs_to_keep d`,
                              `map (λ(l,b). (l,get_from_ls l d.blocks)) d.blocks`]
                   mp_tac) >>
     rw [] >> rw [dest_label_def, num_calls_def] >>
-    rename1 `alookup _ _ = Some (snd (HD (fst (translate_instrs _ _ emap1 _ _))))` >>
+    rename1 `alookup _ _ = Some (snd (HD (fst (translate_instrs _ _ emap2 _ _))))` >>
     (* TODO: This isn't true and will require a more subtle treatment of the
      * emap in this proof overall *)
-    `emap1 = emap |++ header_to_emap_upd (Head phis None)` by cheat >>
+    `emap2 = emap1 |++ header_to_emap_upd (Head phis None)` by cheat >>
     rw [translate_instrs_take_to_call] >>
     qexists_tac `get_regs_to_keep d` >> rw [] >>
     qmatch_goalsub_abbrev_tac `_ = HD (fst (translate_instrs a1 b1 c1 d1 e1))` >>
diff --git a/sledge/semantics/memory_modelScript.sml b/sledge/semantics/memory_modelScript.sml
index 121576530..543342cb7 100644
--- a/sledge/semantics/memory_modelScript.sml
+++ b/sledge/semantics/memory_modelScript.sml
@@ -361,7 +361,7 @@ Proof
     `take size (le_write_num size n ⧺ bs) = le_write_num size n`
     by metis_tac [le_write_num_length, TAKE_LENGTH_APPEND] >>
     simp [le_write_num_def, w2l_def, l2w_def] >>
-    fs [l2n_padding, TAKE_APPEND, take_replicate] >>
+    fs [SIMP_RULE (srw_ss()) [map_replicate] l2n_padding, TAKE_APPEND, take_replicate] >>
     simp [MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF, mod_n2l] >>
     rename1 `n2l 256 m` >>
     Cases_on `size = 0` >> fs [] >>
@@ -383,7 +383,8 @@ Proof
       fs [EXP_EXP_MULT] >>
       `2 ** log 2 m ≤ m` by rw [exp_log_bound] >>
       decide_tac) >>
-    simp [mod_n2l, l2n_n2l, TAKE_LENGTH_TOO_LONG])
+    simp [mod_n2l, l2n_n2l, TAKE_LENGTH_TOO_LONG]
+    )
   >- metis_tac [le_write_num_length, DROP_LENGTH_APPEND]
 QED
 
diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml
index f15ed6c80..311ffdaae 100644
--- a/sledge/semantics/miscScript.sml
+++ b/sledge/semantics/miscScript.sml
@@ -361,7 +361,7 @@ QED
 Theorem l2n_padding:
   ∀ws n. l2n 256 (ws ++ map w2n (replicate n 0w)) = l2n 256 ws
 Proof
-  Induct >> rw [l2n_def] >>
+  Induct >> rw [l2n_def] >> fs [map_replicate] >>
   Induct_on `n` >> rw [l2n_def]
 QED