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 ();