From 0a35b1da35e080c2c69110e72afbc503a358f2a6 Mon Sep 17 00:00:00 2001
From: Scott Owens <sowens@fb.com>
Date: Thu, 24 Oct 2019 05:55:43 -0700
Subject: [PATCH] [sledge sem] Prove the Load and Store cases (mostly)

Summary:
This required some minor tweaks to how the semantics encode values into
and out of byte lists. The remaining problems have to do with how LLVM
globals are translated into llair. At the moment, llair semantic's state
keeps a mapping for globals to their addresses, following the LLVM
semantics. However, it is not used because the translation (following
the code in frontend.ml) translates LLVM globals into llair locals,
which the llair semantics isn't set up to handle.

Reviewed By: jberdine

Differential Revision: D17930787

fbshipit-source-id: 06c6368e0
---
 sledge/semantics/llairScript.sml              |   9 +-
 sledge/semantics/llair_propScript.sml         |  10 +
 sledge/semantics/llvmScript.sml               |   7 +-
 sledge/semantics/llvm_to_llairScript.sml      | 108 ++--
 sledge/semantics/llvm_to_llair_propScript.sml | 584 ++++++++++++------
 sledge/semantics/memory_modelScript.sml       |  55 ++
 6 files changed, 521 insertions(+), 252 deletions(-)

diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml
index f10cb4330..42b8c669f 100644
--- a/sledge/semantics/llairScript.sml
+++ b/sledge/semantics/llairScript.sml
@@ -314,6 +314,7 @@ End
 (* BEGIN Functions to interface to the generic memory model *)
 Definition type_to_shape_def:
   (type_to_shape (IntegerT n) = Flat (sizeof (IntegerT n)) (IntegerT n)) ∧
+  (type_to_shape (PointerT t) = Flat (sizeof (PointerT t)) (PointerT t)) ∧
   (type_to_shape (ArrayT t n) = Array (type_to_shape t) n) ∧
   (type_to_shape (TupleT ts) = Tuple (map type_to_shape ts))
 Termination
@@ -324,7 +325,13 @@ Termination
 End
 
 Definition convert_value_def:
-  convert_value (IntegerT size) n = IntV (&n) size
+  (convert_value (IntegerT size) n =
+    if size = 1 then
+      IntV (if n = 0 then 0 else -1) size
+    else
+      n2i n size) ∧
+  (convert_value (PointerT t) n =
+    n2i n pointer_size)
 End
 
 Definition bytes_to_llair_value_def:
diff --git a/sledge/semantics/llair_propScript.sml b/sledge/semantics/llair_propScript.sml
index 9b7312c95..f31d29883 100644
--- a/sledge/semantics/llair_propScript.sml
+++ b/sledge/semantics/llair_propScript.sml
@@ -139,6 +139,16 @@ Proof
     rw [w2i_n2w_pos])
 QED
 
+Theorem w2i_n2w:
+  ∀n. n < dimword (:'a) ⇒ IntV (w2i (n2w n : 'a word)) (dimindex (:'a)) = n2i n (dimindex (:'a))
+Proof
+  rw [n2i_def]
+  >- (
+    qspec_then `n` mp_tac w2i_n2w_neg >>
+    fs [dimword_def, INT_MIN_def] >> rw [GSYM INT_SUB])
+  >- (irule w2i_n2w_pos >> rw [INT_MIN_def])
+QED
+
 Theorem eval_exp_ignores_lem:
   ∀s1 e v. eval_exp s1 e v ⇒ ∀s2. s1.locals = s2.locals ⇒ eval_exp s2 e v
 Proof
diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index 9d5624da4..f2345618f 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -336,8 +336,6 @@ Definition unsigned_v_to_num_def:
   (unsigned_v_to_num _ = None)
 End
 
-(* TODO: This is a bit of a mess. Consider changing to a relation to deal with
- * partiality *)
 Definition eval_const_def:
   (eval_const g (IntC W1 i) = FlatV (W1V (i2w i))) ∧
   (eval_const g (IntC W8 i) = FlatV (W8V (i2w i))) ∧
@@ -386,7 +384,7 @@ Termination
 End
 
 Definition convert_value_def:
-  (convert_value (IntT W1) n = W1V (n2w n)) ∧
+  (convert_value (IntT W1) n = W1V (if n = 0 then 0w else 1w)) ∧
   (convert_value (IntT W8) n = W8V (n2w n)) ∧
   (convert_value (IntT W32) n = W32V (n2w n)) ∧
   (convert_value (IntT W64) n = W64V (n2w n)) ∧
@@ -578,7 +576,8 @@ Inductive step_instr:
   (eval s a1 = Some <| 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
+   pbytes = get_bytes s.heap interval ∧
+   first_class_type t
    ⇒
    step_instr prog s
      (Load r t (t1, a1)) Tau
diff --git a/sledge/semantics/llvm_to_llairScript.sml b/sledge/semantics/llvm_to_llairScript.sml
index fb6e335ae..93d69e64a 100644
--- a/sledge/semantics/llvm_to_llairScript.sml
+++ b/sledge/semantics/llvm_to_llairScript.sml
@@ -74,7 +74,10 @@ Termination
 End
 
 Definition translate_glob_var_def:
-  translate_glob_var (Glob_var g) t = Var_name g (translate_ty t)
+  translate_glob_var gmap (Glob_var g) =
+    case flookup gmap (Glob_var g) of
+    | None => Var_name g (PointerT (IntegerT 64))
+    | Some t => Var_name g (translate_ty (PtrT t))
 End
 
 Definition translate_reg_def:
@@ -86,25 +89,24 @@ Definition translate_label_def:
 End
 
 Definition translate_const_def:
-  (translate_const (IntC s i) = Integer i (IntegerT (translate_size s))) ∧
-  (translate_const (StrC tcs) =
-    Record (map (λ(ty, c). translate_const c) tcs)) ∧
-  (translate_const (ArrC tcs) =
-    Record (map (λ(ty, c). translate_const c) tcs)) ∧
+  (translate_const gmap (IntC s i) = Integer i (IntegerT (translate_size s))) ∧
+  (translate_const gmap (StrC tcs) =
+    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)) ∧
   (* TODO *)
-  (translate_const (GlobalC g) = Var (translate_glob_var g ARB)) ∧
-  (* TODO *)
-  (translate_const (GepC _ _ _ _) = ARB) ∧
-  (translate_const UndefC = Nondet)
+  (translate_const gmap (GepC _ _ _ _) = ARB) ∧
+  (translate_const gmap UndefC = Nondet)
 Termination
-  WF_REL_TAC `measure const_size` >>
+  WF_REL_TAC `measure (const_size o snd)` >>
   Induct_on `tcs` >> rw [] >> rw [const_size_def] >>
   first_x_assum drule >> decide_tac
 End
 
 Definition translate_arg_def:
-  (translate_arg emap (Constant c) = translate_const c) ∧
-  (translate_arg emap (Variable r) =
+  (translate_arg gmap emap (Constant c) = translate_const gmap c) ∧
+  (translate_arg gmap emap (Variable r) =
     case flookup emap r of
     (* With the current strategy of threading the emap through the whole
      * function, we should never get a None here.
@@ -114,20 +116,20 @@ Definition translate_arg_def:
 End
 
 Definition translate_updatevalue_def:
-  (translate_updatevalue a v [] = v) ∧
-  (translate_updatevalue a v (c::cs) =
-    let c' = translate_const c in
-      Update a c' (translate_updatevalue (Select a c') v cs))
+  (translate_updatevalue gmap a v [] = v) ∧
+  (translate_updatevalue gmap a v (c::cs) =
+    let c' = translate_const gmap c in
+      Update a c' (translate_updatevalue gmap (Select a c') v cs))
 End
 
 (* TODO *)
 Definition translate_instr_to_exp_def:
-  (translate_instr_to_exp emap (llvm$Sub _ _ _ ty a1 a2) =
-    llair$Sub (translate_ty ty) (translate_arg emap a1) (translate_arg emap a2)) ∧
-  (translate_instr_to_exp emap (Extractvalue _ (t, a) cs) =
-    foldl (λe c. Select e (translate_const c)) (translate_arg emap a) cs) ∧
-  (translate_instr_to_exp emap (Insertvalue _ (t1, a1) (t2, a2) cs) =
-    translate_updatevalue (translate_arg emap a1) (translate_arg emap a2) cs)
+  (translate_instr_to_exp gmap emap (llvm$Sub _ _ _ ty a1 a2) =
+    llair$Sub (translate_ty ty) (translate_arg gmap emap a1) (translate_arg gmap emap a2)) ∧
+  (translate_instr_to_exp gmap emap (Extractvalue _ (t, a) cs) =
+    foldl (λe c. Select e (translate_const gmap c)) (translate_arg gmap emap a) cs) ∧
+  (translate_instr_to_exp gmap emap (Insertvalue _ (t1, a1) (t2, a2) cs) =
+    translate_updatevalue gmap (translate_arg gmap emap a1) (translate_arg gmap emap a2) cs)
 End
 
 (* This translation of insertvalue to update and select is quadratic in the
@@ -179,18 +181,18 @@ End
 
 (* TODO *)
 Definition translate_instr_to_inst_def:
-  (translate_instr_to_inst emap (llvm$Store (t1, a1) (t2, a2)) =
-    llair$Store (translate_arg emap a2) (translate_arg emap a1) (sizeof t1)) ∧
-  (translate_instr_to_inst emap (Load r t (t1, a1)) =
-    Load (translate_reg r t) (translate_arg emap a1) (sizeof t))
+  (translate_instr_to_inst gmap emap (llvm$Store (t1, a1) (t2, a2)) =
+    llair$Store (translate_arg gmap emap a2) (translate_arg gmap emap a1) (sizeof t1)) ∧
+  (translate_instr_to_inst gmap emap (Load r t (t1, a1)) =
+    Load (translate_reg r t) (translate_arg gmap emap a1) (sizeof t))
 End
 
 (* TODO *)
 Definition translate_instr_to_term_def:
-  (translate_instr_to_term f emap (Br a l1 l2) =
-    Switch (translate_arg emap a) [(0, translate_label f l2)] (translate_label f l1)) ∧
-  (translate_instr_to_term f emap (Exit a) =
-    Exit (translate_arg emap a))
+  (translate_instr_to_term f gmap emap (Br a l1 l2) =
+    Switch (translate_arg gmap emap a) [(0, translate_label f l2)] (translate_label f l1)) ∧
+  (translate_instr_to_term f gmap emap (Exit a) =
+    Exit (translate_arg gmap emap a))
 End
 
 Datatype:
@@ -224,7 +226,7 @@ Definition classify_instr_def:
   (classify_instr (Exit _) = Term) ∧
   (classify_instr (Load _ _ _) = Non_exp) ∧
   (classify_instr (Store _ _) = Non_exp) ∧
-  (classify_instr (Cxa_throw _ _ _) = Non_exp) ∧
+  (classify_instr (Cxa_throw _ _ _) = Term) ∧
   (classify_instr Cxa_end_catch = Non_exp) ∧
   (classify_instr (Cxa_begin_catch _ _) = Non_exp) ∧
   (classify_instr (Sub r _ _ t _ _) = Exp r t) ∧
@@ -242,6 +244,11 @@ Definition classify_instr_def:
   (classify_instr (Cxa_get_exception_ptr r _) = Exp r ARB)
 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 _ = emap)
+End
+
 (* Translate a list of instructions into an block. f is the name of the function
  * that the instructions are in, reg_to_keep is the set of variables that we
  * want to keep assignments to (e.g., because of sharing in the expression
@@ -264,22 +271,22 @@ End
  *
  *)
 Definition translate_instrs_def:
-  (translate_instrs f emap reg_to_keep [] = (<| cmnd := []; term := Unreachable |>, emap)) ∧
-  (translate_instrs f emap reg_to_keep (i :: is) =
+  (translate_instrs f gmap emap reg_to_keep [] = (<| cmnd := []; term := Unreachable |>, emap)) ∧
+  (translate_instrs f gmap emap reg_to_keep (i :: is) =
     case classify_instr i of
     | Exp r t =>
       let x = translate_reg r t in
-      let e = translate_instr_to_exp emap i in
+      let e = translate_instr_to_exp gmap emap i in
         if r ∈ reg_to_keep then
-          let (b, emap') = translate_instrs f (emap |+ (r, Var x)) reg_to_keep is in
+          let (b, emap') = translate_instrs f gmap (emap |+ (r, Var x)) reg_to_keep is in
             (b with cmnd := Move [(x, e)] :: b.cmnd, emap')
         else
-          translate_instrs f (emap |+ (r, e)) reg_to_keep is
+          translate_instrs f gmap (emap |+ (r, e)) reg_to_keep is
     | Non_exp =>
-        let (b, emap') = translate_instrs f emap reg_to_keep is in
-          (b with cmnd := translate_instr_to_inst emap i :: b.cmnd, emap')
+        let (b, emap') = translate_instrs f gmap (extend_emap_non_exp emap i) reg_to_keep is in
+          (b with cmnd := translate_instr_to_inst gmap emap i :: b.cmnd, emap')
     | Term =>
-        (<| cmnd := []; term := translate_instr_to_term f emap i |>, emap)
+        (<| cmnd := []; term := translate_instr_to_term f gmap emap i |>, emap)
     (* TODO *)
     | Call => ARB)
 End
@@ -298,21 +305,21 @@ Definition translate_label_opt_def:
 End
 
 Definition translate_header_def:
-  (translate_header f entry Entry = []) ∧
-  (translate_header f entry (Head phis _) =
+  (translate_header f gmap entry Entry = []) ∧
+  (translate_header f gmap entry (Head phis _) =
     map
       (λ(r, t, largs).
         (translate_reg r t,
         (* TODO: shouldn't use fempty here *)
-         map (λ(l, arg). (translate_label_opt f entry l, translate_arg fempty arg)) largs))
+         map (λ(l, arg). (translate_label_opt f entry l, translate_arg gmap fempty arg)) largs))
       (map dest_phi phis))
 End
 
 Definition translate_block_def:
-  translate_block f entry_n emap regs_to_keep (l, b) =
-    let (b', emap') = translate_instrs f emap regs_to_keep b.body in
+  translate_block f entry_n gmap emap regs_to_keep (l, b) =
+    let (b', emap') = translate_instrs f gmap emap regs_to_keep b.body in
       ((Lab_name f (the (option_map dest_label l) entry_n),
-       (translate_header f entry_n b.h, b')),
+       (translate_header f gmap entry_n b.h, b')),
        emap')
 End
 
@@ -373,7 +380,7 @@ Definition translate_param_def:
 End
 
 Definition translate_def_def:
-  translate_def f d =
+  translate_def f d gmap =
     let used_names = ARB in
     let entry_name = gen_name used_names "entry" in
     (* TODO *)
@@ -386,7 +393,7 @@ Definition translate_def_def:
     let (bs, emap) =
       foldl
         (λ(bs, emap) b.
-          let (b', emap') = translate_block f entry_name emap regs_to_keep b in
+          let (b', emap') = translate_block f entry_name gmap emap regs_to_keep b in
             (b'::bs, emap'))
         ([], fempty) d.blocks
     in
@@ -405,8 +412,9 @@ End
 
 Definition translate_prog_def:
   translate_prog p =
-    <| glob_init := ARB;
-       functions := map (\(fname, d). (dest_fn fname, translate_def (dest_fn fname) d)) p |>
+    let gmap = ARB in
+      <| glob_init := ARB;
+         functions := map (\(fname, d). (dest_fn fname, translate_def (dest_fn fname) d gmap)) p |>
 End
 
 export_theory ();
diff --git a/sledge/semantics/llvm_to_llair_propScript.sml b/sledge/semantics/llvm_to_llair_propScript.sml
index 5f4f69ca5..6c34aeea2 100644
--- a/sledge/semantics/llvm_to_llair_propScript.sml
+++ b/sledge/semantics/llvm_to_llair_propScript.sml
@@ -19,6 +19,13 @@ set_grammar_ancestry ["llvm", "llair", "llair_prop", "llvm_to_llair", "llvm_ssa"
 
 numLib.prefer_num ();
 
+Definition translate_trace_def:
+  (translate_trace gmap Tau = Tau) ∧
+  (translate_trace gmap Error = Error) ∧
+  (translate_trace gmap (Exit i) = (Exit i)) ∧
+  (translate_trace gmap (W gv bytes) = W (translate_glob_var gmap gv) bytes)
+End
+
 Inductive v_rel:
   (∀w. v_rel (FlatV (PtrV w)) (FlatV (IntV (w2i w) llair$pointer_size))) ∧
   (∀w. v_rel (FlatV (W1V w)) (FlatV (IntV (w2i w) 1))) ∧
@@ -43,7 +50,7 @@ End
 
 Inductive pc_rel:
  (* LLVM side points to a normal instruction *)
- (∀prog emap ip bp d b idx b' prev_i fname.
+ (∀prog emap ip bp d b idx b' prev_i fname gmap.
     (* Both are valid pointers to blocks in the same function *)
     dest_fn ip.f = fst (dest_llair_lab bp) ∧
     alookup prog ip.f = Some d ∧
@@ -56,9 +63,9 @@ Inductive pc_rel:
     (ip.i ≠ Offset 0 ⇒ get_instr prog (ip with i := Offset (idx - 1)) (Inl prev_i) ∧ is_call prev_i) ∧
     ip.f = Fn fname ∧
     (∃regs_to_keep.
-      b' = fst (translate_instrs fname emap regs_to_keep (take_to_call (drop idx b.body))))
+      b' = fst (translate_instrs fname gmap emap regs_to_keep (take_to_call (drop idx b.body))))
     ⇒
-    pc_rel prog emap ip bp) ∧
+    pc_rel prog gmap emap ip bp) ∧
 
  (* If the LLVM side points to phi instructions, the llair side
   * should point to a block generated from them *)
@@ -67,7 +74,7 @@ Inductive pc_rel:
     (* TODO: constrain b to be generated from the phis *)
     get_block (translate_prog prog) bp b
     ⇒
-    pc_rel prog emap ip bp)
+    pc_rel prog gmap emap ip bp)
 End
 
 Definition untranslate_reg_def:
@@ -80,7 +87,7 @@ End
  * of the translation's state.
  *)
 Definition mem_state_rel_def:
-  mem_state_rel prog emap (s:llvm$state) (s':llair$state) ⇔
+  mem_state_rel prog gmap emap (s:llvm$state) (s':llair$state) ⇔
     (* Live LLVM registers are mapped and have a related value in the emap
      * (after evaluating) *)
     (∀r. r ∈ live prog s.ip ⇒
@@ -93,6 +100,10 @@ Definition mem_state_rel_def:
         (∀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))) ∧
     reachable prog s.ip ∧
+    fmap_rel (\(_,n) n'. w2n n = n')
+      s.globals
+      (s'.glob_addrs f_o translate_glob_var gmap) ∧
+    heap_ok s.heap ∧
     erase_tags s.heap = s'.heap ∧
     s.status = s'.status
 End
@@ -103,13 +114,15 @@ End
  * of the translation's state.
  *)
 Definition state_rel_def:
-  state_rel prog emap (s:llvm$state) (s':llair$state) ⇔
-    (s.status = Partial ⇒ pc_rel prog emap s.ip s'.bp) ∧
-    mem_state_rel prog emap s s'
+  state_rel prog gmap emap (s:llvm$state) (s':llair$state) ⇔
+    (s.status = Partial ⇒ pc_rel prog gmap emap s.ip s'.bp) ∧
+    mem_state_rel prog gmap emap s s'
 End
 
 Theorem mem_state_ignore_bp[simp]:
-  ∀prog emap s s' b. mem_state_rel prog emap s (s' with bp := b) ⇔ mem_state_rel prog emap s s'
+  ∀prog gmap emap s s' b.
+    mem_state_rel prog gmap emap s (s' with bp := b) ⇔
+    mem_state_rel prog gmap emap s s'
 Proof
   rw [mem_state_rel_def] >> eq_tac >> rw [] >>
   first_x_assum drule >> rw [] >>
@@ -125,23 +138,22 @@ Proof
 QED
 
 Theorem mem_state_rel_exited:
-  ∀prog emap s s' code.
-    mem_state_rel prog emap s s'
+  ∀prog gmap emap s s' code.
+    mem_state_rel prog gmap emap s s'
     ⇒
-    mem_state_rel prog emap (s with status := Complete code) (s' with status := Complete code)
+    mem_state_rel prog gmap emap (s with status := Complete code) (s' with status := Complete code)
 Proof
   rw [mem_state_rel_def] >>
   metis_tac [eval_exp_ignores, lemma]
 QED
 
 Theorem mem_state_rel_no_update:
-  ∀prog emap s1 s1' v res_v r i i'.
+  ∀prog gmap emap s1 s1' v res_v r i i'.
   assigns prog s1.ip = {} ∧
-  mem_state_rel prog emap s1 s1' ∧
-  v_rel v.value res_v ∧
+  mem_state_rel prog gmap emap s1 s1' ∧
   i ∈ next_ips prog s1.ip
   ⇒
-  mem_state_rel prog emap (s1 with ip := i) s1'
+  mem_state_rel prog gmap emap (s1 with ip := i) s1'
 Proof
   rw [mem_state_rel_def]
   >- (
@@ -151,17 +163,17 @@ Proof
 QED
 
 Theorem mem_state_rel_update:
-  ∀prog emap s1 s1' v res_v r e i.
+  ∀prog gmap emap s1 s1' v res_v r e i.
   is_ssa prog ∧
   assigns prog s1.ip = {r} ∧
-  mem_state_rel prog emap s1 s1' ∧
+  mem_state_rel prog gmap emap s1 s1' ∧
   eval_exp s1' e res_v ∧
   v_rel v.value res_v ∧
   i ∈ next_ips prog s1.ip ∧
   (∀r_use. r_use ∈ exp_uses e ⇒
-    ∃r_tmp. r_use ∈ exp_uses (translate_arg emap (Variable r_tmp)) ∧ r_tmp ∈ live prog s1.ip)
+    ∃r_tmp. r_use ∈ exp_uses (translate_arg gmap emap (Variable r_tmp)) ∧ r_tmp ∈ live prog s1.ip)
   ⇒
-  mem_state_rel prog (emap |+ (r, e))
+  mem_state_rel prog gmap (emap |+ (r, e))
         (s1 with <|ip := i; locals := s1.locals |+ (r, v) |>)
         s1'
 Proof
@@ -188,15 +200,15 @@ Proof
 QED
 
 Theorem mem_state_rel_update_keep:
-  ∀prog emap s1 s1' v res_v r i ty.
+  ∀prog gmap emap s1 s1' v res_v r i ty.
   is_ssa prog ∧
   assigns prog s1.ip = {r} ∧
-  mem_state_rel prog emap s1 s1' ∧
+  mem_state_rel prog gmap emap s1 s1' ∧
   v_rel v.value res_v ∧
   reachable prog s1.ip ∧
   i ∈ next_ips prog s1.ip
   ⇒
-  mem_state_rel prog (emap |+ (r, Var (translate_reg r ty)))
+  mem_state_rel prog gmap (emap |+ (r, Var (translate_reg r ty)))
         (s1 with <|ip := i; locals := s1.locals |+ (r, v)|>)
         (s1' with locals := s1'.locals |+ (translate_reg r ty, res_v))
 Proof
@@ -240,6 +252,29 @@ Proof
   >- metis_tac [next_ips_reachable]
 QED
 
+Triviality lemma:
+  ((s:llair$state) with heap := h).locals = s.locals
+Proof
+  rw []
+QED
+
+Theorem mem_state_rel_heap_update:
+  ∀prog gmap emap s s' h h'.
+    mem_state_rel prog gmap emap s s' ∧
+    heap_ok h ∧
+    erase_tags h = erase_tags h'
+    ⇒
+    mem_state_rel prog gmap emap (s with heap := h) (s' with heap := h')
+Proof
+  rw [mem_state_rel_def, erase_tags_def]
+  >- metis_tac [eval_exp_ignores, lemma] >>
+  rw [heap_component_equality] >>
+  fs [fmap_eq_flookup, FLOOKUP_o_f] >> rw [] >>
+  first_x_assum (qspec_then `x` mp_tac) >>
+  BasicProvers.EVERY_CASE_TAC >> rw [] >>
+  Cases_on `x'` >> Cases_on `x''` >> fs []
+QED
+
 Theorem v_rel_bytes:
   ∀v v'. v_rel v v' ⇒ llvm_value_to_bytes v = llair_value_to_bytes v'
 Proof
@@ -253,19 +288,116 @@ Proof
   Induct_on `vs2` >> rw [] >> rw []
 QED
 
+Theorem bytes_v_rel_lem:
+  (∀f s bs t.
+    f = (λn t w. convert_value t w) ∧
+    s = type_to_shape t ∧
+    first_class_type t
+    ⇒
+    (quotient_pair$### v_rel $=)
+      (bytes_to_value f s bs)
+      (bytes_to_value (λn t w. convert_value t w) (type_to_shape (translate_ty t)) bs)) ∧
+  (∀f n s bs t.
+    f = (λn t w. convert_value t w) ∧
+    s = type_to_shape t ∧
+    first_class_type t
+    ⇒
+    (quotient_pair$### (list_rel v_rel) $=)
+      (read_array f n s bs)
+      (read_array (λn t w. convert_value t w) n (type_to_shape (translate_ty t)) bs)) ∧
+  (∀f ss bs ts.
+    f = (λn t w. convert_value t w) ∧
+    ss = map type_to_shape ts ∧
+    every first_class_type ts
+    ⇒
+    (quotient_pair$### (list_rel v_rel) $=)
+      (read_str f ss bs)
+      (read_str (λn t w. convert_value t w) (map (type_to_shape o translate_ty) ts) bs))
+Proof
+  ho_match_mp_tac bytes_to_value_ind >>
+  rw [llvmTheory.type_to_shape_def, translate_ty_def, type_to_shape_def,
+      sizeof_def, llvmTheory.sizeof_def, bytes_to_value_def, pointer_size_def,
+      convert_value_def, llvmTheory.convert_value_def, quotient_pairTheory.PAIR_REL]
+  >- (
+    Cases_on `t'` >>
+    fs [llvmTheory.type_to_shape_def, llvmTheory.sizeof_def, llvmTheory.first_class_type_def] >>
+    TRY (Cases_on `s`) >>
+    rw [llvmTheory.sizeof_def, le_read_num_def, translate_size_def,
+        convert_value_def, llvmTheory.convert_value_def, translate_ty_def,
+        type_to_shape_def, bytes_to_value_def, sizeof_def, llvmTheory.sizeof_def] >>
+    simp [v_rel_cases] >> rw [word_0_w2i, w2i_1] >>
+    fs [pointer_size_def, llvmTheory.pointer_size_def] >>
+    qmatch_goalsub_abbrev_tac `l2n 256 l` >>
+    qmatch_goalsub_abbrev_tac `n2i n dim` >>
+    `n < 2 ** dim`
+    by (
+      qspecl_then [`l`, `256`] mp_tac numposrepTheory.l2n_lt >>
+      rw [] >>
+      `256 ** length l ≤ 2 ** dim` suffices_by decide_tac >>
+      `256 = 2 ** 8` by rw [] >>
+      full_simp_tac bool_ss [] >>
+      REWRITE_TAC [GSYM EXP_EXP_MULT] >>
+      rw [EXP_BASE_LE_MONO] >>
+      unabbrev_all_tac >> rw []) >>
+    metis_tac [w2i_n2w, dimword_def, dimindex_8, dimindex_32, dimindex_64])
+  >- (
+    Cases_on `t` >>
+    fs [llvmTheory.type_to_shape_def, llvmTheory.sizeof_def, llvmTheory.first_class_type_def] >>
+    rw [pairTheory.PAIR_MAP] >>
+    pairarg_tac >> fs [type_to_shape_def, translate_ty_def, bytes_to_value_def] >>
+    first_x_assum (qspec_then `t'` mp_tac) >> simp [] >>
+    simp [v_rel_cases] >>
+    pairarg_tac >> fs [] >>
+    pairarg_tac >> fs [] >> rw [])
+  >- (
+    Cases_on `t` >>
+    fs [llvmTheory.type_to_shape_def, llvmTheory.sizeof_def, llvmTheory.first_class_type_def] >>
+    rw [pairTheory.PAIR_MAP] >>
+    fs [type_to_shape_def, translate_ty_def, bytes_to_value_def] >>
+    pairarg_tac >> fs [pairTheory.PAIR_MAP] >>
+    first_x_assum (qspec_then `l` mp_tac) >> simp [] >>
+    simp [v_rel_cases] >>
+    pairarg_tac >> fs [] >>
+    pairarg_tac >> fs [MAP_MAP_o] >> rw [] >> fs [ETA_THM])
+  >- (
+    rpt (pairarg_tac >> fs []) >>
+    first_x_assum (qspec_then `t` mp_tac) >> rw [] >>
+    first_x_assum (qspec_then `t` mp_tac) >> rw [])
+  >- (
+    Cases_on `ts` >> fs [bytes_to_value_def] >>
+    rpt (pairarg_tac >> fs []) >>
+    first_x_assum (qspec_then `h` mp_tac) >> simp [] >> strip_tac >>
+    fs [] >> rfs [] >> fs [] >>
+    first_x_assum (qspec_then `t` mp_tac) >> simp [] >> strip_tac >>
+    fs [MAP_MAP_o] >> rw [])
+QED
+
+Theorem bytes_v_rel:
+  ∀t bs.
+    first_class_type t ⇒
+    v_rel (fst (bytes_to_llvm_value t bs))
+          (fst (bytes_to_llair_value (translate_ty t) bs))
+Proof
+  rw [bytes_to_llvm_value_def, bytes_to_llair_value_def] >>
+  qspecl_then [`bs`, `t`] mp_tac (CONJUNCT1 (SIMP_RULE (srw_ss()) [] bytes_v_rel_lem)) >>
+  rw [quotient_pairTheory.PAIR_REL] >>
+  pairarg_tac >> fs [] >>
+  pairarg_tac >> fs []
+QED
+
 Theorem translate_constant_correct_lem:
-  (∀c s prog emap s' (g : glob_var |-> β # word64).
-   mem_state_rel prog emap s s'
+  (∀c s prog gmap emap s'.
+   mem_state_rel prog gmap emap s s'
    ⇒
-   ∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v') ∧
-  (∀(cs : (ty # const) list) s prog emap s' (g : glob_var |-> β # word64).
-   mem_state_rel prog emap s s'
+   ∃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'. list_rel (eval_exp s') (map (translate_const o snd) cs) v' ∧ list_rel v_rel (map (eval_const g o snd) cs) v') ∧
-  (∀(tc : ty # const) s prog emap s' (g : glob_var |-> β # word64).
-   mem_state_rel prog emap s s'
+   ∃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'. eval_exp s' (translate_const (snd tc)) v' ∧ v_rel (eval_const g (snd tc)) v')
+   ∃v'. eval_exp s' (translate_const gmap (snd tc)) v' ∧ v_rel (eval_const s.globals (snd tc)) v')
 Proof
   ho_match_mp_tac const_induction >> rw [translate_const_def] >>
   simp [Once eval_exp_cases, eval_const_def]
@@ -282,39 +414,46 @@ Proof
     metis_tac [])
   (* TODO: unimplemented stuff *)
   >- cheat
-  >- 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 [optionTheory.OPTREL_def] >>
+    (* TODO: false at the moment, need to work out the llair story on globals *)
+    cheat)
+  (* TODO: unimplemented stuff *)
   >- cheat
   >- cheat
 QED
 
 Theorem translate_constant_correct:
-  ∀c s prog emap s' g.
-   mem_state_rel prog emap s s'
+  ∀c s prog gmap emap s' g.
+   mem_state_rel prog gmap emap s s'
    ⇒
-   ∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v'
+   ∃v'. eval_exp s' (translate_const gmap c) v' ∧ v_rel (eval_const s.globals c) 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]:
-  ∀c. r ∉ exp_uses (translate_const c)
+  ∀gmap c. r ∉ exp_uses (translate_const gmap c)
 Proof
   ho_match_mp_tac translate_const_ind >>
-  rw [translate_const_def, exp_uses_def, MEM_MAP, METIS_PROVE [] ``x ∨ y ⇔ (~x ⇒ y)``] >>
-  TRY pairarg_tac >> fs []
-  >- metis_tac []
-  >- metis_tac [] >>
-  (* TODO: unimplemented stuff *)
-  cheat
+  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
+  >- cheat
 QED
 
 Theorem translate_arg_correct:
-  ∀s a v prog emap s'.
-  mem_state_rel prog emap s s' ∧
+  ∀s a v prog gmap emap s'.
+  mem_state_rel prog gmap emap s s' ∧
   eval s a = Some v ∧
   arg_to_regs a ⊆ live prog s.ip
   ⇒
-  ∃v'. eval_exp s' (translate_arg emap a) v' ∧ v_rel v.value v'
+  ∃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 []
   >- metis_tac [translate_constant_correct] >>
@@ -323,8 +462,8 @@ Proof
 QED
 
 Theorem is_allocated_mem_state_rel:
-  ∀prog emap s1 s1'.
-    mem_state_rel prog emap s1 s1'
+  ∀prog gmap emap s1 s1'.
+    mem_state_rel prog gmap emap s1 s1'
     ⇒
     (∀i. is_allocated i s1.heap ⇔ is_allocated i s1'.heap)
 Proof
@@ -359,8 +498,8 @@ Proof
 QED
 
 Theorem translate_sub_correct:
-  ∀prog emap s1 s1' nsw nuw ty v1 v1' v2 v2' e2' e1' result.
-    mem_state_rel prog emap s1 s1' ∧
+  ∀prog gmap emap s1 s1' nsw nuw ty v1 v1' v2 v2' e2' e1' result.
+    mem_state_rel prog gmap emap s1 s1' ∧
     do_sub nuw nsw v1 v2 ty = Some result ∧
     eval_exp s1' e1' v1' ∧
     v_rel v1.value v1' ∧
@@ -413,23 +552,23 @@ Proof
 QED
 
 Theorem translate_extract_correct:
-  ∀prog emap s1 s1' a v v1' e1' cs ns result.
-    mem_state_rel prog emap s1 s1' ∧
+  ∀prog gmap emap s1 s1' a v v1' e1' cs 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 ∧
     extract_value v ns = Some result ∧
     eval_exp s1' e1' v1' ∧
     v_rel v v1'
     ⇒
     ∃v2'.
-      eval_exp s1' (foldl (λe c. Select e (translate_const c)) e1' cs) v2' ∧
+      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]
   >- metis_tac [] >>
   first_x_assum irule >>
   Cases_on `ns` >> fs [] >>
-  qmatch_goalsub_rename_tac `translate_const c` >>
-  `?v2'. eval_exp s1' (translate_const c) v2' ∧ v_rel (eval_const s1.globals c) v2'`
+  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'`
   by metis_tac [translate_constant_correct] >>
   Cases_on `v` >> fs [extract_value_def] >>
   qpat_x_assum `v_rel (AggV _) _` mp_tac >>
@@ -447,8 +586,8 @@ Proof
 QED
 
 Theorem translate_update_correct:
-  ∀prog emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs ns result.
-    mem_state_rel prog emap s1 s1' ∧
+  ∀prog gmap emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs 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 ∧
     insert_value v1 v2 ns = Some result ∧
     eval_exp s1' e1' v1' ∧
@@ -457,7 +596,7 @@ Theorem translate_update_correct:
     v_rel v2 v2'
     ⇒
     ∃v3'.
-      eval_exp s1' (translate_updatevalue e1' e2' cs) v3' ∧
+      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]
@@ -469,9 +608,9 @@ Proof
   Cases_on `insert_value (el x l) v2 ns` >> fs [] >> rw [] >>
   qpat_x_assum `v_rel (AggV _) _` mp_tac >> simp [Once v_rel_cases] >> rw [] >>
   simp [v_rel_cases] >>
-  qmatch_goalsub_rename_tac `translate_const c` >>
+  qmatch_goalsub_rename_tac `translate_const gmap c` >>
   qexists_tac `vs2` >> simp [] >>
-  `?v4'. eval_exp s1' (translate_const c) v4' ∧ v_rel (eval_const s1.globals c) v4'`
+  `?v4'. eval_exp s1' (translate_const gmap c) v4' ∧ v_rel (eval_const s1.globals c) v4'`
   by metis_tac [translate_constant_correct] >>
   `?idx_size. v4' = FlatV (IntV (&x) idx_size)`
   by (
@@ -481,7 +620,7 @@ Proof
   first_x_assum drule >>
   disch_then drule >>
   disch_then drule >>
-  disch_then (qspecl_then [`el x vs2`, `v2'`, `e2'`, `Select e1' (translate_const c)`] mp_tac) >>
+  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]
 QED
@@ -502,20 +641,20 @@ Proof
 QED
 
 Theorem translate_instr_to_exp_correct:
-  ∀emap instr r t s1 s1' s2 prog l.
+  ∀gmap emap instr r t s1 s1' s2 prog l.
     is_ssa prog ∧ prog_ok prog ∧
     classify_instr instr = Exp r t ∧
-    mem_state_rel prog emap s1 s1' ∧
+    mem_state_rel prog gmap emap s1 s1' ∧
     get_instr prog s1.ip (Inl instr) ∧
     step_instr prog s1 instr l s2 ⇒
     ∃pv emap' s2'.
       l = Tau ∧
       s2.ip = inc_pc s1.ip ∧
-      mem_state_rel prog emap' s2 s2' ∧
-      (r ∉ regs_to_keep ⇒ s1' = s2' ∧ emap' = emap |+ (r, translate_instr_to_exp emap instr)) ∧
+      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)) ∧
-       step_inst s1' (Move [(translate_reg r t, translate_instr_to_exp emap instr)]) Tau s2')
+       step_inst s1' (Move [(translate_reg r t, translate_instr_to_exp gmap emap instr)]) Tau s2')
 Proof
   recInduct translate_instr_to_exp_ind >>
   simp [translate_instr_to_exp_def, classify_instr_def] >>
@@ -619,7 +758,7 @@ Proof
    disch_then (qspecl_then [`v'`, `v''`] mp_tac) >> simp [] >>
    disch_then drule >> disch_then drule >>
    rw [] >>
-   rename1 `eval_exp _ (translate_updatevalue _ _ _) res_v` >>
+   rename1 `eval_exp _ (translate_updatevalue _ _ _ _) res_v` >>
    rw [inc_pc_def, inc_bip_def] >>
    rename1 `r ∈ _` >>
    Cases_on `r ∈ regs_to_keep` >> rw []
@@ -630,6 +769,7 @@ Proof
       (* TODO: unfinished *)
       cheat)
     >- cheat) >>
+  (* Other expressions, Icmp, Inttoptr, Ptrtoint, Gep, Alloca *)
   cheat
 QED
 
@@ -639,104 +779,112 @@ Proof
   rw []
 QED
 
-Theorem erase_tags_set_bytes:
-  ∀p v l h. erase_tags (set_bytes p v l h) = set_bytes () v l (erase_tags h)
-Proof
-  Induct_on `v` >> rw [set_bytes_def] >>
-  irule (METIS_PROVE [] ``x = y ⇒ f a b c x = f a b c y``) >>
-  rw [erase_tags_def]
-QED
-
-(*
 Theorem translate_instr_to_inst_correct:
-  ∀prog emap instr s1 s1' s2.
+  ∀gmap emap instr r t s1 s1' s2 prog l.
     classify_instr instr = Non_exp ∧
-    state_rel prog emap s1 s1' ∧
-    get_instr prog s1.ip instr ∧
-    step_instr prog s1 instr s2 ⇒
-    ∃s2'.
-      step_inst s1' (translate_instr_to_inst emap instr) s2' ∧
-      state_rel prog emap s2 s2'
-
+    prog_ok prog ∧ is_ssa prog ∧
+    mem_state_rel prog gmap emap s1 s1' ∧
+    get_instr prog s1.ip (Inl instr) ∧
+    step_instr prog s1 instr l s2
+    ⇒
+    ∃pv s2'.
+      s2.ip = inc_pc s1.ip ∧
+      mem_state_rel prog gmap (extend_emap_non_exp emap instr) s2 s2' ∧
+      step_inst s1' (translate_instr_to_inst gmap emap instr) (translate_trace gmap l) s2'
 Proof
-
   rw [step_instr_cases] >>
   fs [classify_instr_def, translate_instr_to_inst_def]
   >- ( (* Load *)
-    cheat)
+    fs [step_inst_cases, get_instr_cases, PULL_EXISTS] >>
+    qpat_x_assum `Load _ _ _ = el _ _` (assume_tac o GSYM) >>
+    `arg_to_regs a1 ⊆ live prog s1.ip`
+    by (
+      simp [Once live_gen_kill, SUBSET_DEF, uses_cases, IN_DEF, get_instr_cases,
+            instr_uses_def] >>
+      metis_tac []) >>
+    fs [] >>
+    first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
+    disch_then drule >> disch_then drule >> rw [] >>
+    qpat_x_assum `v_rel (FlatV _) _` mp_tac >> simp [Once v_rel_cases] >> rw [] >>
+    `∃n. r = Reg n` by (Cases_on `r` >> metis_tac []) >>
+    qexists_tac `n` >> qexists_tac `translate_ty t` >>
+    HINT_EXISTS_TAC >> rw [] >>
+    qexists_tac `freeable` >> rw [translate_trace_def]
+    >- rw [inc_pc_def, llvmTheory.inc_pc_def, update_result_def]
+    >- (
+      simp [GSYM translate_reg_def, llvmTheory.inc_pc_def, update_result_def,
+            update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST,
+            extend_emap_non_exp_def] >>
+      irule mem_state_rel_update_keep >>
+      rw []
+      >- rw [assigns_cases, IN_DEF, EXTENSION, get_instr_cases, instr_assigns_def]
+      >- (
+        `s1.ip with i := inc_bip (Offset idx) = inc_pc s1.ip` by rw [inc_pc_def] >>
+        simp [] >> irule prog_ok_nonterm >>
+        simp [get_instr_cases, terminator_def])
+      >- metis_tac [next_ips_reachable, mem_state_rel_def]
+      >- (
+        fs [w2n_i2n, pointer_size_def, mem_state_rel_def] >>
+        metis_tac [bytes_v_rel, get_bytes_erase_tags]))
+    >- rw [translate_reg_def]
+    >- (
+      fs [w2n_i2n, pointer_size_def, mem_state_rel_def] >>
+      metis_tac [is_allocated_erase_tags]))
   >- ( (* Store *)
-    simp [step_inst_cases, PULL_EXISTS] >>
-    drule get_instr_live >> rw [uses_def] >>
-    drule translate_arg_correct >> disch_then drule >> disch_then drule >>
-    qpat_x_assum `eval _ _ = Some _` mp_tac >>
-    drule translate_arg_correct >> disch_then drule >> disch_then drule >>
-    rw [] >>
+    fs [step_inst_cases, get_instr_cases, PULL_EXISTS] >>
+    qpat_x_assum `Store _ _ = el _ _` (assume_tac o GSYM) >>
+    `bigunion (image arg_to_regs {a1; a2}) ⊆ live prog s1.ip`
+    by (
+      simp [Once live_gen_kill, SUBSET_DEF, uses_cases, IN_DEF, get_instr_cases,
+            instr_uses_def] >>
+      metis_tac []) >>
+    fs [] >>
+    first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
+    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 >> rw [] >>
     qpat_x_assum `v_rel (FlatV _) _` mp_tac >> simp [Once v_rel_cases] >> rw [] >>
+    drule v_rel_bytes >> rw [] >>
+    fs [w2n_i2n, pointer_size_def] >>
     HINT_EXISTS_TAC >> rw [] >>
     qexists_tac `freeable` >> rw [] >>
-    HINT_EXISTS_TAC >> rw []
-    >- metis_tac [v_rel_bytes]
+    qexists_tac `v'` >> rw []
+    >- rw [llvmTheory.inc_pc_def, inc_pc_def]
     >- (
-      fs [w2n_i2n, pointer_size_def] >>
-      metis_tac [v_rel_bytes, is_allocated_state_rel, ADD_COMM]) >>
-    fs [state_rel_def] >>
-    rw []
-    >- cheat
-    >- (
-      fs [llvmTheory.inc_pc_def] >>
-      `r ∈ live prog s1.ip`
-      by (
-        drule live_gen_kill >>
-        rw [next_ips_def, assigns_def, uses_def, inc_pc_def]) >>
-      first_x_assum drule >> rw [] >>
-      metis_tac [eval_exp_ignores, eval_exp_help])
+      simp [llvmTheory.inc_pc_def] >>
+      irule mem_state_rel_no_update >> rw []
+      >- rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def]
+      >- (
+        `s1.ip with i := inc_bip (Offset idx) = inc_pc s1.ip` by rw [inc_pc_def] >>
+        simp [] >> irule prog_ok_nonterm >>
+        simp [get_instr_cases, terminator_def]) >>
+      irule mem_state_rel_heap_update >>
+      rw [set_bytes_unchanged, erase_tags_set_bytes] >>
+      fs [mem_state_rel_def, extend_emap_non_exp_def] >>
+      metis_tac [set_bytes_heap_ok])
     >- (
-      rw [llvmTheory.inc_pc_def, w2n_i2n, pointer_size_def, erase_tags_set_bytes] >>
-      metis_tac[v_rel_bytes]))
-  >- cheat
-  >- cheat
-  >- cheat
-QED
-
-
-    simp [step_inst_cases, PULL_EXISTS] >>
-    Cases_on `r` >> simp [translate_reg_def] >>
-    drule get_instr_live >> rw [uses_def] >>
-    drule translate_arg_correct >> disch_then drule >> disch_then drule >>
-    simp [Once v_rel_cases] >> rw [] >>
-    qexists_tac `IntV (w2i w) pointer_size` >> rw [] >>
-    qexists_tac `freeable` >> rw []
-    >- (fs [w2n_i2n, pointer_size_def] >> metis_tac [is_allocated_state_rel]) >>
-    fs [state_rel_def] >> rw []
-    >- cheat
+      fs [mem_state_rel_def] >>
+      fs [is_allocated_def, heap_component_equality, erase_tags_def] >>
+      metis_tac [])
     >- (
-      fs [llvmTheory.inc_pc_def, update_results_def, update_result_def] >>
-      rw [] >> fs [FLOOKUP_UPDATE] >> rw []
+      (* 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]
       >- (
-        cheat)
-      >- (
-        `r ∈ live prog s1.ip`
-        by (
-          drule live_gen_kill >>
-          rw [next_ips_def, assigns_def, uses_def, inc_pc_def]) >>
-        first_x_assum drule >> rw [] >>
-        qexists_tac `v` >>
-        qexists_tac `v'` >>
-        qexists_tac `e` >>
-        rw []
-        metis_tac [eval_exp_ignores, eval_exp_help])
-
-
-    >- fs [update_results_def, llvmTheory.inc_pc_def, update_result_def]
-
-*)
+        first_x_assum (qspec_then `x` mp_tac) >> rw [] >>
+        rename1 `option_rel _ _ opt` >> Cases_on `opt` >>
+        fs [optionTheory.OPTREL_def] >>
+        cheat) >>
+      cheat))
+QED
 
-Definition translate_trace_def:
-  (translate_trace types Tau = Tau) ∧
-  (translate_trace types Error = Error) ∧
-  (translate_trace types (Exit i) = (Exit i)) ∧
-  (translate_trace types (W gv bytes) = W (translate_glob_var gv (types gv)) bytes)
-End
+Theorem classify_instr_term_call:
+  ∀i. (classify_instr i = Term ⇔ terminator i) ∧
+      (classify_instr i = Call ⇔ is_call i)
+Proof
+  Cases >> rw [classify_instr_def, is_call_def, terminator_def] >>
+  Cases_on `p` >> rw [classify_instr_def]
+QED
 
 Definition untranslate_glob_var_def:
   untranslate_glob_var (Var_name n ty) = Glob_var n
@@ -750,13 +898,14 @@ Definition untranslate_trace_def:
 End
 
 Theorem un_translate_glob_inv:
-  ∀x t. untranslate_glob_var (translate_glob_var x t) = x
+  ∀x t. untranslate_glob_var (translate_glob_var gmap x) = x
 Proof
-  Cases_on `x` >> rw [untranslate_glob_var_def, translate_glob_var_def]
+  Cases_on `x` >> rw [translate_glob_var_def] >>
+  CASE_TAC >> rw [untranslate_glob_var_def]
 QED
 
 Theorem un_translate_trace_inv:
-  ∀x. untranslate_trace (translate_trace types x) = x
+  ∀x. untranslate_trace (translate_trace gmap x) = x
 Proof
   Cases >> rw [translate_trace_def, untranslate_trace_def] >>
   metis_tac [un_translate_glob_inv]
@@ -776,18 +925,18 @@ QED
 Theorem translate_instrs_correct1:
   ∀prog s1 tr s2.
     multi_step prog s1 tr s2 ⇒
-    ∀s1' b' emap regs_to_keep d b types idx.
+    ∀s1' b' gmap emap regs_to_keep d b idx.
       prog_ok prog ∧ is_ssa prog ∧
-      mem_state_rel prog emap s1 s1' ∧
+      mem_state_rel prog gmap emap s1 s1' ∧
       alookup prog s1.ip.f = Some d ∧
       alookup d.blocks s1.ip.b = Some b ∧
       s1.ip.i = Offset idx ∧
-      b' = fst (translate_instrs (dest_fn s1.ip.f) emap regs_to_keep (take_to_call (drop idx b.body)))
+      b' = fst (translate_instrs (dest_fn s1.ip.f) gmap emap regs_to_keep (take_to_call (drop idx b.body)))
       ⇒
       ∃emap s2' tr'.
         step_block (translate_prog prog) s1' b'.cmnd b'.term tr' s2' ∧
-        filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace types) tr)  ∧
-        state_rel prog emap s2 s2'
+        filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace gmap) tr) ∧
+        state_rel prog gmap emap s2 s2'
 Proof
   ho_match_mp_tac multi_step_ind >> rw_tac std_ss []
   >- (
@@ -855,6 +1004,27 @@ Proof
         qexists_tac `if 0 = w2i tf then dest_label lab2 else dest_label lab1` >> simp [] >>
         qpat_abbrev_tac `target = if tf = 0w then l2 else l1` >>
         qpat_abbrev_tac `target' = if 0 = w2i tf then dest_label lab2 else dest_label lab1` >>
+        `last b.body = Br a l1 l2 ∧
+         <|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|> ∈ next_ips prog s1.ip`
+        by (
+          fs [prog_ok_def, get_instr_cases] >>
+          last_x_assum drule >> disch_then drule >>
+          strip_tac >> conj_asm1_tac
+          >- (
+            CCONTR_TAC >>
+            `Br a l1 l2 ∈ set (front (b.body))`
+            by (
+              `mem (Br a l1 l2) (front b.body ++ [last b.body])`
+              by metis_tac [EL_MEM, APPEND_FRONT_LAST] >>
+              fs [] >> metis_tac []) >>
+            fs [EVERY_MEM] >> first_x_assum drule >> rw [terminator_def])
+          >- (
+            rw [next_ips_cases, IN_DEF, assigns_cases] >>
+            disj1_tac >>
+            qexists_tac `Br a l1 l2` >>
+            rw [instr_next_ips_def, Abbr `target`] >>
+            fs [get_instr_cases, instr_to_labs_def] >>
+            metis_tac [blockHeader_nchotomy])) >>
         rw [] >>
         `translate_label (dest_fn s1.ip.f) target = Lab_name (dest_fn s1.ip.f) target' `
         by (
@@ -867,7 +1037,16 @@ Proof
         >- (Cases_on `lab2` >> rw [Abbr `target'`, translate_label_def, dest_label_def])
         >- (Cases_on `lab1` >> rw [Abbr `target'`, translate_label_def, dest_label_def])
         >- (
-          rw [pc_rel_cases] >> cheat)
+          fs [get_instr_cases] >>
+          `every (λlab. ∃b. alookup d.blocks (Some lab) = Some b ∧ b.h ≠ Entry)
+                 (instr_to_labs (last b.body))`
+          by metis_tac [prog_ok_def] >>
+          rfs [instr_to_labs_def] >>
+          rw [pc_rel_cases, get_instr_cases, get_block_cases, GSYM PULL_EXISTS]
+          >- metis_tac [blockHeader_nchotomy] >>
+          fs [translate_prog_def] >>
+          (* Unfinished *)
+          cheat)
         >- (
           fs [mem_state_rel_def] >> rw []
           >- (
@@ -877,20 +1056,16 @@ Proof
             rw [PULL_EXISTS] >>
             disj1_tac >>
             qexists_tac `<|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|>` >>
-            rw [next_ips_cases, IN_DEF, assigns_cases]
-            >- (
-              disj1_tac >>
-              qexists_tac `Br a l1 l2` >>
-              rw [instr_next_ips_def, Abbr `target`] >>
-              fs [prog_ok_def, get_instr_cases] >>
-              last_x_assum drule >> disch_then drule >> rw [] >>
-              `last b.body = Br a l1 l2` by cheat >>
-              fs [instr_to_labs_def] >>
-              metis_tac [blockHeader_nchotomy]) >>
+            rw [] >>
+            rw [IN_DEF, assigns_cases] >>
             CCONTR_TAC >> fs [] >>
             imp_res_tac get_instr_func >> fs [] >> rw [] >>
             fs [instr_assigns_def])
-          >- cheat))
+          >- (
+            fs [reachable_def] >>
+            qexists_tac `path ++ [<|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|>]` >>
+            rw_tac std_ss [good_path_append, GSYM APPEND] >> rw [] >>
+            rw [Once good_path_cases] >> fs [next_ips_cases, IN_DEF] >> metis_tac [])))
       >- ( (* Invoke *)
         cheat)
       >- ( (* Unreachable *)
@@ -911,8 +1086,8 @@ Proof
   >- ( (* Middle of the block *)
     fs [llvmTheory.step_cases] >> TRY (fs [get_instr_cases] >> NO_TAC) >>
     `i' = i` by metis_tac [get_instr_func, sumTheory.INL_11] >> fs [] >>
-    rename [`step_instr _ _ _ _ s2`, `state_rel _ _ s3 _`,
-            `mem_state_rel _ _ s1 s1'`] >>
+    rename [`step_instr _ _ _ _ s2`, `state_rel _ _ _ s3 _`,
+            `mem_state_rel _ _ _ s1 s1'`] >>
     Cases_on `∃r t. classify_instr i = Exp r t` >> fs []
     >- ( (* instructions that compile to expressions *)
       drule translate_instr_to_exp_correct >>
@@ -923,8 +1098,8 @@ Proof
       by metis_tac [prog_ok_nonterm, next_ips_reachable, mem_state_rel_def] >>
       first_x_assum drule >>
       simp [inc_pc_def, inc_bip_def] >>
-      disch_then (qspecl_then [`regs_to_keep`, `types`] mp_tac) >> rw [] >>
-      rename1 `state_rel prog emap3 s3 s3'` >>
+      disch_then (qspecl_then [`regs_to_keep`] mp_tac) >> rw [] >>
+      rename1 `state_rel prog gmap emap3 s3 s3'` >>
       qexists_tac `emap3` >> qexists_tac `s3'` >> rw [] >>
       `take_to_call (drop idx b.body) = i :: take_to_call (drop (idx + 1) b.body)`
       by (
@@ -938,7 +1113,24 @@ Proof
       pairarg_tac >> rw [] >> fs [] >>
       metis_tac [])
     >- ( (* Non-expression instructions *)
-      cheat))
+      Cases_on `classify_instr i` >> fs [classify_instr_term_call] >>
+      drule translate_instr_to_inst_correct >>
+      ntac 5 (disch_then drule) >>
+      strip_tac >> fs [] >>
+      first_x_assum drule >> simp [inc_pc_def, inc_bip_def] >>
+      disch_then (qspecl_then [`regs_to_keep`] mp_tac) >> simp [] >>
+      strip_tac >>
+      rename1 `state_rel prog gmap emap3 s3 s3'` >>
+      qexists_tac `emap3` >> qexists_tac `s3'` >> simp [] >>
+      `take_to_call (drop idx b.body) = i :: take_to_call (drop (idx + 1) b.body)`
+      by (
+        irule take_to_call_lem >> simp [] >>
+        fs [get_instr_cases]) >>
+      simp [translate_instrs_def] >>
+      qexists_tac `translate_trace gmap l::tr'` >> rw [] >>
+      simp [Once step_block_cases] >> pairarg_tac >> rw [] >> fs [] >>
+      disj2_tac >>
+      qexists_tac `s2'` >> rw []))
 QED
 
 Theorem multi_step_to_step_block:
@@ -946,20 +1138,20 @@ Theorem multi_step_to_step_block:
     prog_ok prog ∧ is_ssa prog ∧
     multi_step prog s1 tr s2 ∧
     s1.status = Partial ∧
-    state_rel prog emap s1 s1'
+    state_rel prog gmap emap s1 s1'
     ⇒
     ∃s2' emap2 b tr'.
       get_block (translate_prog prog) s1'.bp b ∧
       step_block (translate_prog prog) s1' b.cmnd b.term tr' s2' ∧
-      filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace types) tr) ∧
-      state_rel prog emap2 s2 s2'
+      filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace gmap) tr) ∧
+      state_rel prog gmap emap2 s2 s2'
 Proof
   rw [] >> pop_assum mp_tac >> simp [Once state_rel_def] >> rw [pc_rel_cases]
   >- (
     (* Non-phi instruction *)
     drule translate_instrs_correct1 >> simp [] >>
     disch_then drule >>
-    disch_then (qspecl_then [`regs_to_keep`, `types`] mp_tac) >> simp [] >>
+    disch_then (qspecl_then [`regs_to_keep`] mp_tac) >> simp [] >>
     rw [] >>
     qexists_tac `s2'` >> simp [] >>
     ntac 3 HINT_EXISTS_TAC >>
@@ -979,13 +1171,13 @@ QED
 
 Theorem step_block_to_multi_step:
   ∀prog s1 s1' tr s2' b.
-    state_rel prog emap s1 s1' ∧
+    state_rel prog gmap emap s1 s1' ∧
     get_block (translate_prog prog) s1'.bp b ∧
     step_block (translate_prog prog) s1' b.cmnd b.term tr s2'
     ⇒
     ∃s2.
       multi_step prog s1 (map untranslate_trace tr) s2 ∧
-      state_rel prog emap s2 s2'
+      state_rel prog gmap emap s2 s2'
 Proof
   cheat
 QED
@@ -1008,34 +1200,33 @@ Theorem translate_prog_correct_lem1:
   ∀path.
     okpath (multi_step prog) path ∧ finite path
     ⇒
-    ∀emap s1'.
+    ∀gmap emap s1'.
     prog_ok prog ∧
     is_ssa prog ∧
-    state_rel prog emap (first path) s1'
+    state_rel prog gmap emap (first path) s1'
     ⇒
     ∃path' emap.
       finite path' ∧
       okpath (step (translate_prog prog)) path' ∧
       first path' = s1' ∧
       LMAP (filter ($≠ Tau)) (labels path') =
-      LMAP (map (translate_trace types) o filter ($≠ Tau)) (labels path) ∧
-      state_rel prog emap (last path) (last path')
+      LMAP (map (translate_trace gmap) o filter ($≠ Tau)) (labels path) ∧
+      state_rel prog gmap emap (last path) (last path')
 Proof
   ho_match_mp_tac finite_okpath_ind >> rw []
   >- (qexists_tac `stopped_at s1'` >> rw [] >> metis_tac []) >>
   fs [] >>
-  rename1 `state_rel _ _ s1 s1'` >>
+  rename1 `state_rel _ _ _ s1 s1'` >>
   Cases_on `s1.status ≠ Partial`
   >- fs [Once multi_step_cases, llvmTheory.step_cases, last_step_cases] >>
   fs [] >>
-  drule multi_step_to_step_block >> ntac 4 (disch_then drule) >>
-  disch_then (qspec_then `types` mp_tac) >> rw [] >>
+  drule multi_step_to_step_block >> ntac 4 (disch_then drule) >> rw [] >>
   first_x_assum drule >> rw [] >>
   qexists_tac `pcons s1' tr' path'` >> rw [] >>
   rw [FILTER_MAP, combinTheory.o_DEF, trans_trace_not_tau] >>
   HINT_EXISTS_TAC >> simp [] >>
   simp [step_cases] >> qexists_tac `b` >> simp [] >>
-  qpat_x_assum `state_rel _ _ _ s1'` mp_tac >>
+  qpat_x_assum `state_rel _ _ _ _ s1'` mp_tac >>
   rw [state_rel_def, mem_state_rel_def]
 QED
 
@@ -1045,14 +1236,14 @@ Theorem translate_prog_correct_lem2:
     ⇒
     ∀s1.
     prog_ok prog ∧
-    state_rel prog emap s1 (first path')
+    state_rel prog gmap emap s1 (first path')
     ⇒
     ∃path.
       finite path ∧
       okpath (multi_step prog) path ∧
       first path = s1 ∧
       labels path = LMAP (map untranslate_trace) (labels path') ∧
-      state_rel prog emap (last path) (last path')
+      state_rel prog gmap emap (last path) (last path')
 Proof
   ho_match_mp_tac finite_okpath_ind >> rw []
   >- (qexists_tac `stopped_at s1` >> rw []) >>
@@ -1115,16 +1306,15 @@ QED
 Theorem translate_prog_correct:
   ∀prog s1 s1'.
     prog_ok prog ∧ is_ssa prog ∧
-    state_rel prog emap s1 s1'
+    state_rel prog gmap emap s1 s1'
     ⇒
     multi_step_sem prog s1 = image (I ## map untranslate_trace) (sem (translate_prog prog) s1')
 Proof
   rw [sem_def, multi_step_sem_def, EXTENSION] >> eq_tac >> rw []
   >- (
-    drule translate_prog_correct_lem1 >> ntac 4 (disch_then drule) >>
-    disch_then (qspec_then `types` mp_tac) >> rw [pairTheory.EXISTS_PROD] >>
+    drule translate_prog_correct_lem1 >> ntac 4 (disch_then drule) >> rw [pairTheory.EXISTS_PROD] >>
     PairCases_on `x` >> rw [] >>
-    qexists_tac `map (translate_trace types) x1` >> rw []
+    qexists_tac `map (translate_trace gmap) x1` >> rw []
     >- rw [MAP_MAP_o, combinTheory.o_DEF, un_translate_trace_inv] >>
     qexists_tac `path'` >> rw [] >>
     fs [IN_DEF, observation_prefixes_cases, toList_some] >> rw [] >>
@@ -1139,13 +1329,13 @@ Proof
     >- fs [state_rel_def, mem_state_rel_def]
     >- fs [state_rel_def, mem_state_rel_def] >>
     rename [`labels path' = fromList l'`, `labels path = fromList l`,
-            `state_rel _ _ (last path) (last path')`, `lsub ≼ flat l`] >>
+            `state_rel _ _ _ (last path) (last path')`, `lsub ≼ flat l`] >>
     Cases_on `lsub = flat l` >> fs []
     >- (
       qexists_tac `flat l'` >>
       rw [FILTER_FLAT, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF] >>
       fs [state_rel_def, mem_state_rel_def]) >>
-    `filter (λy. Tau ≠ y) (flat l') = map (translate_trace types) (filter (λy. Tau ≠ y) (flat l))`
+    `filter (λy. Tau ≠ y) (flat l') = map (translate_trace gmap) (filter (λy. Tau ≠ y) (flat l))`
     by rw [FILTER_FLAT, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF, FILTER_MAP] >>
     qexists_tac `take_prop ($≠ Tau) (length (filter ($≠ Tau) lsub)) (flat l')` >>
     rw [] >> rw [GSYM MAP_TAKE]
diff --git a/sledge/semantics/memory_modelScript.sml b/sledge/semantics/memory_modelScript.sml
index 2712063c4..7a8d38fef 100644
--- a/sledge/semantics/memory_modelScript.sml
+++ b/sledge/semantics/memory_modelScript.sml
@@ -570,5 +570,60 @@ Proof
     fs [is_allocated_def, interval_to_set_def, SUBSET_DEF] >>
     metis_tac [LESS_EQ_REFL, DECIDE ``!x y. x < x + SUC y``])
 QED
+Theorem erase_tags_set_bytes:
+  ∀p v l h. erase_tags (set_bytes p v l h) = set_bytes () v l (erase_tags h)
+Proof
+  Induct_on `v` >> rw [set_bytes_def] >>
+  irule (METIS_PROVE [] ``x = y ⇒ f a b c x = f a b c y``) >>
+  rw [erase_tags_def]
+QED
+
+Theorem erase_tags_unit_id[simp]:
+  ∀h. erase_tags h = h
+Proof
+  rw [erase_tags_def, theorem "heap_component_equality", fmap_eq_flookup, FLOOKUP_o_f] >>
+  CASE_TAC >> rw [] >>
+  Cases_on `x'` >> rw []
+QED
+
+Theorem is_allocated_suc:
+  n ≤ n' ⇒ is_allocated (Interval b n (Suc n')) h ⇒ is_allocated (Interval b n n') h
+Proof
+  rw [is_allocated_def, interval_ok_def, interval_to_set_def, SUBSET_DEF,
+      interval_freeable_def]
+  >- (first_x_assum irule >> rw [])
+  >- (qexists_tac `b2` >> rw [])
+QED
+
+Theorem get_bytes_erase_tags:
+  ∀h i. heap_ok h ∧ is_allocated i h ⇒ map snd (get_bytes (erase_tags h) i) = map snd (get_bytes h i)
+Proof
+  Cases_on `i` >> rw [get_bytes_def, MAP_MAP_o, combinTheory.o_DEF, erase_tags_def] >>
+  Induct_on `n0 - n` >> rw [erase_tags_def, FLOOKUP_o_f]
+  >- (`n0 - n = 0` by decide_tac >> rw [COUNT_LIST_def]) >>
+  Cases_on `n0` >> fs [] >>
+  `Suc n' - n = Suc (n' - n)` by decide_tac >>
+  asm_simp_tac std_ss [COUNT_LIST_SNOC] >>
+  `v = n' - n` by decide_tac >> fs [] >>
+  first_x_assum (qspecl_then [`n'`, `n`] mp_tac) >> rw []
+  >- (
+    fs [LIST_EQ_REWRITE, EL_MAP, FLOOKUP_o_f] >> rw [] >>
+    `n ≤ n'` by decide_tac >>
+    drule is_allocated_suc >> disch_then drule >> rw []) >>
+  BasicProvers.EVERY_CASE_TAC >> rw []
+  >- (
+    fs [heap_ok_def] >> rfs [is_allocated_def] >>
+    first_x_assum (qspec_then `n'` mp_tac) >> rw [] >>
+    pop_assum (qspec_then `b2` mp_tac) >> rw [] >>
+    fs [interval_to_set_def, SUBSET_DEF] >>
+    first_x_assum (qspec_then `n'` mp_tac) >> rw []) >>
+  pairarg_tac >> rw []
+QED
+
+Theorem is_allocated_erase_tags[simp]:
+  ∀i h. is_allocated i (erase_tags h) ⇔ is_allocated i h
+Proof
+  rw [is_allocated_def, erase_tags_def]
+QED
 
 export_theory ();