diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml
index e75a92971..090c75056 100644
--- a/sledge/semantics/llairScript.sml
+++ b/sledge/semantics/llairScript.sml
@@ -19,6 +19,7 @@ numLib.prefer_num ();
 Datatype:
   typ =
   | FunctionT typ (typ list)
+  (* How many bits the integer occupies *)
   | IntegerT num
   | PointerT typ
   | ArrayT typ num
@@ -121,13 +122,11 @@ End
 (* ----- Semantic states ----- *)
 
 (* These are the values that can be stored in registers. The implementation uses
- * integers with a bit-width to represent numbers, and keeps locations and sizes
- * separate.
+ * integers with a bit-width to represent numbers and pointers. Here we
+ * interpret the bit width b as meaning the int should be in the range [-2^(b-1),2^(b-1))
  *)
 Datatype:
   flat_v =
-  | LocV num
-  | SizeV num
   | IntV int num
 End
 
@@ -143,34 +142,28 @@ Datatype:
        globals : var |-> word64;
        locals : var |-> v;
        stack : frame list;
-       pointer_size : 'a itself;
        heap : unit heap |>
 End
 
+(* Assume that all pointers can fit in 64 bits *)
+Definition pointer_size_def:
+  pointer_size = 64
+End
+
 (* ----- Semantic transitions ----- *)
 
+(* The size of a type in bytes, rounded up *)
 Definition sizeof_def:
-  (sizeof (:'a) (IntegerT n) = n) ∧
-  (sizeof (:'a) (PointerT t) = dimindex (:'a)) ∧
-  (sizeof (:'a) (ArrayT t n) = n * sizeof (:'a) t) ∧
-  (sizeof (:'a) (TupleT ts) = sum (map (sizeof (:'a)) ts))
+  (sizeof (IntegerT n) = (n+7) DIV 8) ∧
+  (sizeof (PointerT t) = (pointer_size+7) DIV 8) ∧
+  (sizeof (ArrayT t n) = n * sizeof t) ∧
+  (sizeof (TupleT ts) = sum (map sizeof ts))
 Termination
-  WF_REL_TAC `measure (typ_size o snd)` >> simp [] >>
+  WF_REL_TAC `measure typ_size` >> simp [] >>
   Induct >> rw [definition "typ_size_def"] >> simp [] >>
   first_x_assum drule >> decide_tac
 End
 
-Definition type_to_shape_def:
-  (type_to_shape (:'a) (IntegerT n) = Flat (sizeof (:'a) (IntegerT n)) (IntegerT n)) ∧
-  (type_to_shape (:'a) (ArrayT t n) = Array (type_to_shape (:'a) t) n) ∧
-  (type_to_shape (:'a) (TupleT ts) = Tuple (map (type_to_shape (:'a)) ts))
-Termination
-  WF_REL_TAC `measure (typ_size o snd)` >>
-  rw [] >>
-  Induct_on `ts` >> rw [definition "typ_size_def"] >>
-  res_tac >> decide_tac
-End
-
 Definition first_class_type_def:
   (first_class_type (IntegerT _) ⇔ T) ∧
   (first_class_type (PointerT _) ⇔ T) ∧
@@ -185,34 +178,53 @@ Termination
 End
 
 Inductive value_type:
-  (value_type (IntegerT n) (FlatV (IntV i n))) ∧
-  (value_type (PointerT _) (FlatV (LocV n))) ∧
-  (every (value_type t) vs ∧ length vs = n ∧ first_class_type t
+  (∀n i. value_type (IntegerT n) (FlatV (IntV i n))) ∧
+  (∀t vs n.
+   every (value_type t) vs ∧ length vs = n ∧ first_class_type t
    ⇒
    value_type (ArrayT t n) (AggV vs)) ∧
-  (list_rel value_type ts vs
+  (∀ts vs.
+   list_rel value_type ts vs
    ⇒
-   value_type (StrT ts) (AggV vs))
+   value_type (TupleT ts) (AggV vs))
 End
 
 Definition bool2v_def:
   bool2v b = FlatV (IntV (if b then 1 else 0) 1)
 End
 
-Definition int2unsigned_def:
-  int2unsigned (i:int) size =
+(* The integer, interpreted as 2's complement, fits in the given number of bits *)
+Definition ifits_def:
+  ifits (i:int) size ⇔
+    0 < size ∧ -(2 ** (size - 1)) ≤ i ∧ i < 2 ** (size - 1)
+End
+
+(* The natural number, interpreted as unsigned, fits in the given number of bits *)
+Definition nfits_def:
+  nfits (n:num) size ⇔
+    0 < size ∧ n < 2 ** size
+End
+
+(* Convert an integer to an unsigned number, following the 2's complement,
+ * assuming (ifits i size) *)
+Definition i2n_def:
+  i2n (IntV i size) : num =
     if i < 0 then
-      256 ** size + i
+      Num (2 ** size + i)
     else
-      i
+      Num i
 End
 
-Definition fits_def:
-  fits (i:int) size ⇔
-    0 < size ∧ 0 - (256 ** (size - 1)) ≤ i ∧ i < 256 ** (size - 1)
+(* Convert an unsigned number into the integer that it would be in 2's
+ * compliment with the given size, assuming (nfits n size) *)
+Definition n2i_def:
+  n2i n size =
+    if 2 ** (size - 1) ≤ n then
+      (IntV (&n - &(2 ** size)) size)
+    else
+      (IntV (&n) size)
 End
 
-(* TODO: We never create anything that is a SizeV *)
 Inductive eval_exp:
   (∀s v r.
    flookup s.locals v = Some r
@@ -222,17 +234,19 @@ Inductive eval_exp:
   (* TODO: Nondet I guess we need to know the type here *)
   (* TODO: Label *)
 
-  (∀s e1 e2 size byte.
-   eval_exp s e1 (FlatV (IntV byte 1)) ∧
-   eval_exp s e2 (FlatV (SizeV size))
+  (∀s e1 e2 n byte n_size.
+   eval_exp s e1 (FlatV (IntV byte 8)) ∧
+   (* This idiom means that e2 evaluates to a non-negative integer n, and is
+    * used throughout *)
+   eval_exp s e2 (FlatV (IntV (&n) n_size))
    ⇒
-   eval_exp s (Splat e1 e2) (AggV (replicate size (FlatV (IntV byte 1))))) ∧
+   eval_exp s (Splat e1 e2) (AggV (replicate n (FlatV (IntV byte 8))))) ∧
 
    (* TODO Question: What if size <> vals? *)
-  (∀s e1 e2 size vals.
+  (∀s e1 e2 l vals n_size.
    eval_exp s e1 (AggV vals) ∧
-   eval_exp s e2 (FlatV (SizeV size)) ∧
-   size = length vals
+   eval_exp s e2 (FlatV (IntV (&l) n_size)) ∧
+   l = length vals
    ⇒
    eval_exp s (Memory e1 e2) (AggV vals)) ∧
 
@@ -242,7 +256,7 @@ Inductive eval_exp:
    eval_exp s (Concat es) (AggV (flat vals))) ∧
 
   (∀s i size.
-   eval_exp s (Integer i (IntegerT size)) (FlatV (IntV i size))) ∧
+   eval_exp s (Integer i (IntegerT size)) (FlatV (IntV (truncate_2comp i size) size))) ∧
 
   (* TODO Question: Should the same integer with two different sizes be equal *)
   (∀s e1 e2 r1 r2.
@@ -254,136 +268,146 @@ Inductive eval_exp:
   (∀s e1 e2 i1 size1 i2 size2.
    eval_exp s e1 (FlatV (IntV i1 size1)) ∧
    eval_exp s e2 (FlatV (IntV i2 size2)) ∧
-   fits i1 size1 ∧
-   fits i2 size2
+   ifits i1 size1 ∧
+   ifits i2 size2
    ⇒
    eval_exp s (Lt e1 e2) (bool2v (i1 < i2))) ∧
 
-  (∀s e1 e2 i1 size1 i2 size2.
+  (∀s e1 e2 i1 i2 size1 size2.
    eval_exp s e1 (FlatV (IntV i1 size1)) ∧
    eval_exp s e2 (FlatV (IntV i2 size2)) ∧
-   fits i1 size1 ∧
-   fits i2 size2
+   ifits i1 size1 ∧
+   ifits i2 size2
    ⇒
-   eval_exp s (Ult e1 e2) (bool2v (int2unsigned i1 size1 < int2unsigned i2 size2))) ∧
+   eval_exp s (Ult e1 e2) (bool2v (i2n (IntV i1 size1) < i2n (IntV i2 size2)))) ∧
 
   (∀s size e1 e2 i1 i2.
    eval_exp s e1 (FlatV (IntV i1 size)) ∧
-   eval_exp s e2 (FlatV (IntV i2 size)) ∧
-   fits i1 size ∧
-   fits i2 size
+   eval_exp s e2 (FlatV (IntV i2 size))
    ⇒
-   eval_exp s (Sub (IntegerT size) e1 e2) (FlatV (IntV (i1 - i2) size))) ∧
+   eval_exp s (Sub (IntegerT size) e1 e2) (FlatV (IntV (truncate_2comp (i1 - i2) size) size))) ∧
 
   (∀s es vals.
    list_rel (eval_exp s) es vals
    ⇒
    eval_exp s (Record es) (AggV vals)) ∧
 
-  (∀s e1 e2 vals size.
+  (∀s e1 e2 vals idx idx_size.
    eval_exp s e1 (AggV vals) ∧
-   eval_exp s e2 (FlatV (SizeV size)) ∧
-   size < length vals
+   eval_exp s e2 (FlatV (IntV (&idx) idx_size)) ∧
+   idx < length vals
    ⇒
-   eval_exp s (Select e1 e2) (el size vals)) ∧
+   eval_exp s (Select e1 e2) (el idx vals)) ∧
 
-  (∀s e1 e2 e3 vals size r.
+  (∀s e1 e2 e3 vals r idx idx_size.
    eval_exp s e1 (AggV vals) ∧
-   eval_exp s e2 (FlatV (SizeV size)) ∧
+   eval_exp s e2 (FlatV (IntV (&idx) idx_size)) ∧
    eval_exp s e3 r ∧
-   size < length vals
+   idx < length vals
    ⇒
-   eval_exp s (Update e1 e2 e3) (AggV (list_update r size vals)))
+   eval_exp s (Update e1 e2 e3) (AggV (list_update r idx vals)))
 
 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 (ArrayT t n) = Array (type_to_shape t) n) ∧
+  (type_to_shape (TupleT ts) = Tuple (map type_to_shape ts))
+Termination
+  WF_REL_TAC `measure typ_size` >>
+  rw [] >>
+  Induct_on `ts` >> rw [definition "typ_size_def"] >>
+  res_tac >> decide_tac
+End
+
 Definition convert_value_def:
-  (convert_value (IntegerT n) w = IntV (w2i w) n) ∧
-  (convert_value (PointerT t) w = LocV (w2n w))
+  convert_value (IntegerT size) n = IntV (&n) size
 End
 
 Definition bytes_to_llair_value_def:
-  bytes_to_llair_value (:'a) t bs =
-    (bytes_to_value (λn t (w:'a word). convert_value t w) (type_to_shape (:'a) t) bs)
+  bytes_to_llair_value t bs =
+    (bytes_to_value (λn t w. convert_value t w) (type_to_shape t) bs)
 End
 
 Definition unconvert_value_def:
-  (unconvert_value (:'a) (IntV i size) = (size, i2w i)) ∧
-  (unconvert_value (:'a) (LocV n) = (dimindex (:'a), n2w n))
+  unconvert_value (IntV i size) = ((size + 7) DIV 8, i2n (IntV i size))
 End
 
 Definition llair_value_to_bytes_def:
-  llair_value_to_bytes (:'a) v =
-    value_to_bytes (unconvert_value (:'a) : flat_v -> num # 'a word) v
+  llair_value_to_bytes v =
+    value_to_bytes unconvert_value v
 End
+(* END Functions to interface to the generic memory model *)
 
 Definition update_results_def:
   update_results xvs s = s with locals := s.locals |++ xvs
 End
 
 Inductive step_inst:
-  (∀s ves r.
-    eval_exp s e r
+  (∀s ves rs.
+    list_rel (eval_exp s) (map snd ves) rs
     ⇒
     step_inst s
     (Move ves)
-    (update_results (map (λ(v,e). (v, r)) ves) s)) ∧
+    (update_results (map (λ(v,r). (v, r)) (zip (map fst ves, rs))) s)) ∧
 
-  (∀(s:'a state) x t e size ptr freeable interval bytes.
-   eval_exp s e (FlatV (LocV ptr)) ∧
-   interval = Interval freeable ptr (ptr + size) ∧
+  (∀s x t e size ptr freeable interval bytes.
+   eval_exp s e (FlatV ptr) ∧
+   interval = Interval freeable (i2n ptr) (i2n ptr + size) ∧
    is_allocated interval s.heap ∧
    bytes = map snd (get_bytes s.heap interval)
    ⇒
    step_inst s
     (Load (Var_name x t) e size)
-    (update_results [(Var_name x t, fst (bytes_to_llair_value (:'a) t bytes))] s)) ∧
+    (update_results [(Var_name x t, fst (bytes_to_llair_value t bytes))] s)) ∧
 
   (∀s e1 e2 size ptr bytes freeable interval r.
-   eval_exp s e1 (FlatV (LocV ptr)) ∧
+   eval_exp s e1 (FlatV ptr) ∧
    eval_exp s e2 r ∧
-   interval = Interval freeable ptr (ptr + size) ∧
+   interval = Interval freeable (i2n ptr) (i2n ptr + size) ∧
    is_allocated interval s.heap ∧
-   bytes = llair_value_to_bytes (:'a) r ∧
+   bytes = llair_value_to_bytes r ∧
    length bytes = size
    ⇒
    step_inst s
      (Store e1 e2 size)
-     (s with heap := set_bytes () bytes ptr s.heap)) ∧
+     (s with heap := set_bytes () bytes (i2n ptr) s.heap)) ∧
 
   (* TODO memset *)
 
   (∀s e1 e2 e3 dest_ptr src_ptr size src_interval freeable1 freeable2 bytes.
-   eval_exp s e1 (FlatV (LocV dest_ptr)) ∧
-   eval_exp s e2 (FlatV (LocV src_ptr)) ∧
-   eval_exp s e3 (FlatV (SizeV size)) ∧
-   src_interval = Interval freeable1 src_ptr (src_ptr + size) ∧
+   eval_exp s e1 (FlatV dest_ptr) ∧
+   eval_exp s e2 (FlatV src_ptr) ∧
+   eval_exp s e3 (FlatV size) ∧
+   src_interval = Interval freeable1 (i2n src_ptr) (i2n src_ptr + i2n size) ∧
    is_allocated src_interval s.heap ∧
-   is_allocated (Interval freeable2 dest_ptr (dest_ptr + size)) s.heap ∧
+   is_allocated (Interval freeable2 (i2n dest_ptr) (i2n dest_ptr + i2n size)) s.heap ∧
    (* TODO Question: should we allow overlap? *)
    bytes = map snd (get_bytes s.heap src_interval)
    ⇒
    step_inst s
     (Memcpy e1 e2 e3)
-    (s with heap := set_bytes () bytes dest_ptr s.heap)) ∧
+    (s with heap := set_bytes () bytes (i2n dest_ptr) s.heap)) ∧
 
   (* TODO memmove *)
 
-  (∀s v e1 e2 n size ptr new_h.
-   eval_exp s e1 (FlatV (SizeV n)) ∧
-   eval_exp s e2 (FlatV (SizeV size)) ∧
-   allocate s.heap (n * size) () (ptr, new_h)
+  (∀s v e1 e2 n size ptr new_h size_size.
+   eval_exp s e1 (FlatV n) ∧
+   eval_exp s e2 (FlatV (IntV (&size) size_size)) ∧
+   allocate s.heap (i2n n * size) () (ptr, new_h) ∧
+   nfits ptr pointer_size
    ⇒
    step_inst s
      (Alloc v e1 e2)
-     (update_results [(v, FlatV (LocV ptr))] (s with heap := new_h))) ∧
+     (update_results [(v, FlatV (n2i ptr pointer_size))] (s with heap := new_h))) ∧
 
   (∀s e ptr.
-   eval_exp s e (FlatV (LocV ptr))
+   eval_exp s e (FlatV ptr)
    ⇒
    step_inst s
      (Free e)
-     (s with heap := deallocate [A ptr] s.heap)) ∧
+     (s with heap := deallocate [A (i2n ptr)] s.heap)) ∧
 
   (∀s x t nondet.
    value_type t nondet
@@ -396,22 +420,22 @@ End
 
 Inductive step_term:
 
-  (∀prog s e table default size fname bname bname'.
-   eval_exp s e (FlatV (SizeV size)) ∧
-   Lab_name fname bname = (case alookup table size of Some lab => lab | None => default) ∧
+  (∀prog s e table default idx fname bname bname' idx_size.
+   eval_exp s e (FlatV (IntV (&idx) idx_size)) ∧
+   Lab_name fname bname = (case alookup table idx of Some lab => lab | None => default) ∧
    s.bp = Lab_name fname bname'
    ⇒
    step_term prog s
      (Switch e table default)
      (s with bp := Lab_name fname bname)) ∧
 
-  (∀prog s e labs size.
-   eval_exp s e (FlatV (SizeV size)) ∧
-   size < length labs
+  (∀prog s e labs i idx idx_size.
+   eval_exp s e (FlatV (IntV (&idx) idx_size)) ∧
+   idx < length labs
    ⇒
    step_term prog s
      (Iswitch e labs)
-     (s with bp := el size labs)) ∧
+     (s with bp := el i labs)) ∧
 
   (∀prog s v fname bname es t ret1 ret2 vals f.
    alookup prog.functions fname = Some f ∧
@@ -428,7 +452,6 @@ Inductive step_term:
              exn_ret := ret2;
              ret_var := v;
              saved_locals := s.locals |> :: s.stack;
-        pointer_size := s.pointer_size;
         heap := s.heap |>) ∧
 
   (∀prog s e r top rest.
@@ -441,7 +464,6 @@ Inductive step_term:
         globals := s.globals;
         locals := top.saved_locals |+ (top.ret_var, r);
         stack := rest;
-        pointer_size := s.pointer_size;
         heap := s.heap |>)
 
   (* TODO Throw *)
@@ -452,12 +474,12 @@ End
  * instruction pointer and do a big-step evaluation for each block *)
 Inductive step_block:
 
-  (!prog s1 t s2.
+  (∀prog s1 t s2.
    step_term prog s1 t s2
    ⇒
    step_block prog s1 [] t s2) ∧
 
-  (!prog s1 i is t s2 s3.
+  (∀prog s1 i is t s2 s3.
    step_inst s1 i s2 ∧
    step_block prog s2 is t s3
    ⇒
diff --git a/sledge/semantics/llair_propScript.sml b/sledge/semantics/llair_propScript.sml
new file mode 100644
index 000000000..456d92251
--- /dev/null
+++ b/sledge/semantics/llair_propScript.sml
@@ -0,0 +1,141 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(* Properties of the llair model *)
+
+open HolKernel boolLib bossLib Parse;
+open arithmeticTheory integerTheory integer_wordTheory wordsTheory;
+open settingsTheory miscTheory llairTheory;
+
+new_theory "llair_prop";
+
+numLib.prefer_num ();
+
+Theorem ifits_w2i:
+  ∀(w : 'a word). ifits (w2i w) (dimindex (:'a))
+Proof
+  rw [ifits_def, GSYM INT_MIN_def] >>
+  metis_tac [INT_MIN, w2i_ge, integer_wordTheory.INT_MAX_def, w2i_le,
+             intLib.COOPER_PROVE ``!(x:int) y. x ≤ y - 1 ⇔ x < y``]
+QED
+
+Theorem truncate_2comp_fits:
+  ∀i size. 0 < size ⇒ ifits (truncate_2comp i size) size
+Proof
+  rw [truncate_2comp_def, ifits_def] >>
+  qmatch_goalsub_abbrev_tac `(i + s1) % s2` >>
+  `s2 ≠ 0 ∧ ¬(s2 < 0)` by rw [Abbr `s2`]
+  >- (
+    `0 ≤ (i + s1) % s2` suffices_by intLib.COOPER_TAC >>
+    drule INT_MOD_BOUNDS >>
+    rw [])
+  >- (
+    `(i + s1) % s2 < 2 * s1` suffices_by intLib.COOPER_TAC >>
+    `2 * s1 = s2` by rw [Abbr `s1`, Abbr `s2`, GSYM EXP] >>
+    drule INT_MOD_BOUNDS >>
+    rw [Abbr `s1`, Abbr `s2`])
+QED
+
+Theorem fits_ident:
+  ∀i size. 0 < size ⇒ (ifits i size ⇔ truncate_2comp i size = i)
+Proof
+  rw [ifits_def, truncate_2comp_def] >>
+  rw [intLib.COOPER_PROVE ``!(x:int) y z. x - y = z <=> x = y + z``] >>
+  qmatch_goalsub_abbrev_tac `(_ + s1) % s2` >>
+  `s2 ≠ 0 ∧ ¬(s2 < 0)` by rw [Abbr `s2`] >>
+  `2 * s1 = s2` by rw [Abbr `s1`, Abbr `s2`, GSYM EXP] >>
+  eq_tac >>
+  rw []
+  >- (
+    simp [Once INT_ADD_COMM] >>
+    irule INT_LESS_MOD >>
+    rw [] >>
+    intLib.COOPER_TAC)
+  >- (
+   `0 ≤ (i + s1) % (2 * s1)` suffices_by intLib.COOPER_TAC >>
+    drule INT_MOD_BOUNDS >>
+    simp [])
+  >- (
+   `(i + s1) % (2 * s1) < 2 * s1` suffices_by intLib.COOPER_TAC >>
+    drule INT_MOD_BOUNDS >>
+    simp [])
+QED
+
+Theorem i2n_n2i:
+  !n size. 0 < size ⇒ (nfits n size ⇔ (i2n (n2i n size) = n))
+Proof
+  rw [nfits_def, n2i_def, i2n_def] >> rw []
+  >- intLib.COOPER_TAC
+  >- (
+    `2 ** size ≤ n` by intLib.COOPER_TAC >> simp [INT_SUB] >>
+    Cases_on `n = 0` >> fs [] >>
+    `n - 2 ** size < n` suffices_by intLib.COOPER_TAC >>
+    irule SUB_LESS >> simp [])
+  >- (
+    `2 ** (size - 1) < 2 ** size` suffices_by intLib.COOPER_TAC >>
+    fs [])
+QED
+
+Theorem n2i_i2n:
+  !i size. 0 < size ⇒ (ifits i size ⇔ (n2i (i2n (IntV i size)) size) = IntV i size)
+Proof
+  rw [ifits_def, n2i_def, i2n_def] >> rw [] >> fs []
+  >- (
+    eq_tac >> rw []
+    >- (
+      simp [intLib.COOPER_PROVE ``∀(x:int) y z. x - y = z ⇔ x = y + z``] >>
+      `2 ** (size - 1) < 2 ** size` suffices_by intLib.COOPER_TAC >>
+      fs [INT_OF_NUM])
+    >- (
+      fs [intLib.COOPER_PROVE ``∀(x:int) y z. x - y = z ⇔ x = y + z``] >>
+      fs [INT_OF_NUM] >>
+      `?j. i = -j` by intLib.COOPER_TAC >> rw [] >> fs [] >>
+      qpat_x_assum `_ ≤ Num _` mp_tac >>
+      fs [GSYM INT_OF_NUM] >>
+      ASM_REWRITE_TAC [GSYM INT_LE] >> rw [] >>
+      `2 ** size = 2 * 2 ** (size - 1)` by rw [GSYM EXP, ADD1] >> fs [] >>
+      intLib.COOPER_TAC)
+    >- intLib.COOPER_TAC)
+  >- (
+    eq_tac >> rw []
+    >- intLib.COOPER_TAC
+    >- intLib.COOPER_TAC >>
+    `0 ≤ i` by intLib.COOPER_TAC >>
+    fs [GSYM INT_OF_NUM] >>
+    `&(2 ** size) = 0` by intLib.COOPER_TAC >>
+    fs [])
+  >- (
+    eq_tac >> rw []
+    >- (
+      `2 ** size = 2 * 2 ** (size - 1)` by rw [GSYM EXP, ADD1] >> fs [] >>
+      intLib.COOPER_TAC)
+    >- intLib.COOPER_TAC
+    >- intLib.COOPER_TAC)
+  >- intLib.COOPER_TAC
+QED
+
+Theorem w2n_i2n:
+  ∀w. w2n (w : 'a word) = i2n (IntV (w2i w) (dimindex (:'a)))
+Proof
+  rw [i2n_def] >> Cases_on `w` >> fs []
+  >- (
+    `INT_MIN (:α) ≤ n`
+    by (
+      fs [w2i_def] >> rw [] >>
+      BasicProvers.EVERY_CASE_TAC >> fs [word_msb_n2w_numeric] >>
+      rfs []) >>
+    rw [w2i_n2w_neg, dimword_def, int_arithTheory.INT_NUM_SUB])
+  >- (
+    `n < INT_MIN (:'a)`
+    by (
+      fs [w2i_def] >> rw [] >>
+      BasicProvers.EVERY_CASE_TAC >> fs [word_msb_n2w_numeric] >>
+      rfs []) >>
+    rw [w2i_n2w_pos])
+QED
+
+export_theory ();
diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index cdd24bc8f..da4914ab5 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -136,12 +136,17 @@ End
 
 (* ----- Semantic states ----- *)
 
+Definition pointer_size_def:
+  pointer_size = 8
+End
+
 Datatype:
   flat_v =
   | W1V word1
   | W8V word8
   | W32V word32
   | W64V word64
+  (* LLVM guarantees that 64 bits is enough to hold a pointer *)
   | PtrV word64
   | UndefV
 End
@@ -172,13 +177,21 @@ End
 
 (* ----- Things about types ----- *)
 
+(* Given a number n that fits into pointer_size number of bytes, create the
+ * pointer value. Since the pointer is represented as a 64-bit word,
+ * pointer_size must be 8 or less, which LLVM guarantees *)
+Definition mk_ptr_def:
+  mk_ptr n =
+    if n < 256 ** pointer_size then Some (FlatV (PtrV (n2w n))) else None
+End
+
 (* How many bytes a value of the given type occupies *)
 Definition sizeof_def:
   (sizeof (IntT W1) = 1) ∧
   (sizeof (IntT W8) = 1) ∧
   (sizeof (IntT W32) = 4) ∧
   (sizeof (IntT W64) = 8) ∧
-  (sizeof (PtrT _) = 8) ∧
+  (sizeof (PtrT _) = pointer_size) ∧
   (sizeof (ArrT n t) = n * sizeof t) ∧
   (sizeof (StrT ts) = sum (map sizeof ts))
 Termination
@@ -200,6 +213,7 @@ Termination
   res_tac >> decide_tac
 End
 
+(* Are the indices all in bounds? *)
 Definition indices_ok_def:
   (indices_ok _ [] ⇔ T) ∧
   (indices_ok (ArrT n t) (i::indices) ⇔
@@ -209,12 +223,13 @@ Definition indices_ok_def:
   (indices_ok _ _ ⇔ F)
 End
 
+(* Which values have which types *)
 Inductive value_type:
   (value_type (IntT W1) (FlatV (W1V w1))) ∧
   (value_type (IntT W8) (FlatV (W8V w8))) ∧
   (value_type (IntT W32) (FlatV (W32V w32))) ∧
   (value_type (IntT W64) (FlatV (W64V w64))) ∧
-  (value_type (PtrT _) (FlatV (PtrV w64))) ∧
+  (value_type (PtrT _) (FlatV (PtrV ptr))) ∧
   (every (value_type t) vs ∧ length vs = n ∧ first_class_type t
    ⇒
    value_type (ArrT n t) (AggV vs)) ∧
@@ -223,6 +238,7 @@ Inductive value_type:
    value_type (StrT ts) (AggV vs))
 End
 
+(* Get the component of a type referred by the indices *)
 Definition extract_type_def:
   (extract_type t [] = Some t) ∧
   (extract_type (ArrT n t) (i::idx) =
@@ -257,6 +273,7 @@ End
 
 (* ----- Semantic transitions ----- *)
 
+(* Put a 64-bit word into a smaller value, truncating if necessary *)
 Definition w64_cast_def:
   (w64_cast w (IntT W1) = Some (FlatV (W1V (w2w w)))) ∧
   (w64_cast w (IntT W8) = Some (FlatV (W8V (w2w w)))) ∧
@@ -265,22 +282,37 @@ Definition w64_cast_def:
   (w64_cast _ _ = None)
 End
 
-Definition cast_w64_def:
-  (cast_w64 (FlatV (W1V w)) = Some (w2w w)) ∧
-  (cast_w64 (FlatV (W8V w)) = Some (w2w w)) ∧
-  (cast_w64 (FlatV (W32V w)) = Some (w2w w)) ∧
-  (cast_w64 (FlatV (W64V w)) = Some w) ∧
-  (cast_w64 _ = None)
+Definition bool_to_v_def:
+  bool_to_v b = if b then FlatV (W1V 1w) else FlatV (W1V 0w)
 End
 
-Definition cast_num_def:
-  cast_num v = option_map w2n (cast_w64 v)
+(* Convert a word value into an integer, interpreting the word in 2's complement *)
+Definition signed_v_to_int_def:
+  (signed_v_to_int (FlatV (W1V w)) = Some (w2i w)) ∧
+  (signed_v_to_int (FlatV (W8V w)) = Some (w2i w)) ∧
+  (signed_v_to_int (FlatV (W32V w)) = Some (w2i w)) ∧
+  (signed_v_to_int (FlatV (W64V w)) = Some (w2i w)) ∧
+  (signed_v_to_int _ = None)
 End
 
-Definition bool_to_v_def:
-  bool_to_v b = if b then FlatV (W1V 1w) else FlatV (W1V 0w)
+(* Convert a non-negative word value (interpreted as 2's complement) into a natural number *)
+Definition signed_v_to_num_def:
+  signed_v_to_num v =
+    option_join
+      (option_map (\i. if i < 0 then None else Some (Num i)) (signed_v_to_int v))
+End
+
+(* Convert a word value into a natural number, interpreting the word as unsigned *)
+Definition unsigned_v_to_num_def:
+  (unsigned_v_to_num (FlatV (W1V w)) = Some (w2n w)) ∧
+  (unsigned_v_to_num (FlatV (W8V w)) = Some (w2n w)) ∧
+  (unsigned_v_to_num (FlatV (W32V w)) = Some (w2n w)) ∧
+  (unsigned_v_to_num (FlatV (W64V w)) = Some (w2n w)) ∧
+  (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))) ∧
@@ -289,12 +321,12 @@ Definition eval_const_def:
   (eval_const g (StrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧
   (eval_const g (ArrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧
   (eval_const g (GepC ty ptr (t, idx) indices) =
-    case (eval_const g ptr, cast_num (eval_const g idx)) of
-    | (FlatV (PtrV w), Some n) =>
-      let ns = map (λ(t,ci). case cast_num (eval_const g ci) of None => 0 | Some n => n) indices in
+    case (eval_const g ptr, signed_v_to_num (eval_const g idx)) of
+    | (FlatV (PtrV ptr), Some n) =>
+      let ns = map (λ(t,ci). case signed_v_to_num (eval_const g ci) of None => 0 | Some n => n) indices in
         (case get_offset ty ns of
          | None => FlatV UndefV
-         | Some off => FlatV (PtrV (n2w (w2n w + sizeof ty * n + off))))
+         | Some off => FlatV (PtrV (n2w ((w2n ptr) + (sizeof ty) * n + off))))
     | _ => FlatV UndefV) ∧
   (eval_const g (GlobalC var) =
     case flookup g var of
@@ -312,21 +344,11 @@ Termination
 End
 
 Definition eval_def:
-  (eval s (Variable v) =
-    case flookup s.locals v of
-    | None => <| poison := F; value := FlatV (W1V 0w) |>
-    | Some v => v) ∧
-  (eval s (Constant c) = <| poison := F; value := eval_const s.globals c |>)
-End
-
-Definition v2n_def:
-  (v2n (FlatV (W1V b)) = Some (if T then 1 else 0)) ∧
-  (v2n (FlatV (W8V w8)) = Some (w2n w8)) ∧
-  (v2n (FlatV (W32V w32)) = Some (w2n w32)) ∧
-  (v2n (FlatV (W64V w64)) = Some (w2n w64)) ∧
-  (v2n _ = None)
+  (eval s (Variable v) = flookup s.locals v) ∧
+  (eval s (Constant c) = Some <| poison := F; value := eval_const s.globals c |>)
 End
 
+(* BEGIN Functions to interface to the generic memory model *)
 Definition type_to_shape_def:
   (type_to_shape (IntT s) = Flat (sizeof (IntT s)) (IntT s)) ∧
   (type_to_shape (PtrT t) = Flat (sizeof (PtrT t)) (PtrT t)) ∧
@@ -339,11 +361,11 @@ Termination
 End
 
 Definition convert_value_def:
-  (convert_value (IntT W1) w = W1V (w2w w)) ∧
-  (convert_value (IntT W8) w = W8V (w2w w)) ∧
-  (convert_value (IntT W32) w = W32V (w2w w)) ∧
-  (convert_value (IntT W64) w = W64V w) ∧
-  (convert_value (PtrT _) w = PtrV w)
+  (convert_value (IntT W1) n = W1V (n2w n)) ∧
+  (convert_value (IntT W8) n = W8V (n2w n)) ∧
+  (convert_value (IntT W32) n = W32V (n2w n)) ∧
+  (convert_value (IntT W64) n = W64V (n2w n)) ∧
+  (convert_value (PtrT _) n = PtrV (n2w n))
 End
 
 Definition bytes_to_llvm_value_def:
@@ -352,11 +374,11 @@ Definition bytes_to_llvm_value_def:
 End
 
 Definition unconvert_value_def:
-  (unconvert_value (W1V w) = (1, w2w w)) ∧
-  (unconvert_value (W8V w) = (1, w2w w)) ∧
-  (unconvert_value (W32V w) = (4, w2w w)) ∧
-  (unconvert_value (W64V w) = (8, w)) ∧
-  (unconvert_value (PtrV w) = (8, w))
+  (unconvert_value (W1V w) = (1, w2n w)) ∧
+  (unconvert_value (W8V w) = (1, w2n w)) ∧
+  (unconvert_value (W32V w) = (4, w2n w)) ∧
+  (unconvert_value (W64V w) = (8, w2n w)) ∧
+  (unconvert_value (PtrV w) = (pointer_size, w2n w))
 End
 
 Definition llvm_value_to_bytes_def:
@@ -364,17 +386,27 @@ Definition llvm_value_to_bytes_def:
     value_to_bytes unconvert_value v
 End
 
+(* END Functions to interface to the generic memory model *)
+
 Definition do_sub_def:
-  do_sub (nuw:bool) (nsw:bool) (v1:pv) (v2:pv) =
-    let (diff, u_overflow, s_overflow) =
-      case (v1.value, v2.value) of
-      | (FlatV (W1V w1), FlatV (W1V w2)) => (FlatV o W1V ## I) (add_with_carry (w1, ¬w2, T))
-      | (FlatV (W8V w1), FlatV (W8V w2)) => (FlatV o W8V ## I) (add_with_carry (w1, ¬w2, T))
-      | (FlatV (W32V w1), FlatV (W32V w2)) => (FlatV o W32V ## I) (add_with_carry (w1, ¬w2, T))
-      | (FlatV (W64V w1), FlatV (W64V w2)) => (FlatV o W64V ## I) (add_with_carry (w1, ¬w2, T))
+  do_sub (nuw:bool) (nsw:bool) (v1:pv) (v2:pv) t =
+    let diff =
+      case (v1.value, v2.value, t) of
+      | (FlatV (W1V w1), FlatV (W1V w2), IntT W1) =>
+        Some ((FlatV o W1V ## I) (add_with_carry (w1, ¬w2, T)))
+      | (FlatV (W8V w1), FlatV (W8V w2), IntT W8) =>
+        Some ((FlatV o W8V ## I) (add_with_carry (w1, ¬w2, T)))
+      | (FlatV (W32V w1), FlatV (W32V w2), IntT W32) =>
+        Some ((FlatV o W32V ## I) (add_with_carry (w1, ¬w2, T)))
+      | (FlatV (W64V w1), FlatV (W64V w2), IntT W64) =>
+        Some ((FlatV o W64V ## I) (add_with_carry (w1, ¬w2, T)))
+      | _ => None
     in
-    let p = ((nuw ∧ u_overflow) ∨ (nsw ∧ s_overflow) ∨ v1.poison ∨ v2.poison) in
-      <| poison := p; value := diff |>
+      option_map
+        (\(diff, u_overflow, s_overflow).
+           let p = ((nuw ∧ u_overflow) ∨ (nsw ∧ s_overflow) ∨ v1.poison ∨ v2.poison) in
+             <| poison := p; value := diff |>)
+        diff
 End
 
 Definition get_comp_def:
@@ -385,19 +417,19 @@ End
 
 Definition do_icmp_def:
   do_icmp c v1 v2 =
-    <| poison := (v1.poison ∨ v2.poison);
-       value := bool_to_v (
-         case (v1.value, v2.value) of
-         | (FlatV (W1V w1), FlatV (W1V w2)) => (get_comp c) w1 w2
-         | (FlatV (W8V w1), FlatV (W8V w2)) => (get_comp c) w1 w2
-         | (FlatV (W32V w1), FlatV (W32V w2)) => (get_comp c) w1 w2
-         | (FlatV (W64V w1), FlatV (W64V w2)) => (get_comp c) w1 w2
-         | (FlatV (PtrV w1), FlatV (PtrV w2)) => (get_comp c) w1 w2) |>
+    option_map (\b. <| poison := (v1.poison ∨ v2.poison); value := bool_to_v b |>)
+      (case (v1.value, v2.value) of
+       | (FlatV (W1V w1), FlatV (W1V w2)) => Some ((get_comp c) w1 w2)
+       | (FlatV (W8V w1), FlatV (W8V w2)) => Some ((get_comp c) w1 w2)
+       | (FlatV (W32V w1), FlatV (W32V w2)) => Some ((get_comp c) w1 w2)
+       | (FlatV (W64V w1), FlatV (W64V w2)) => Some ((get_comp c) w1 w2)
+       | (FlatV (PtrV w1), FlatV (PtrV w2)) => Some ((get_comp c) w1 w2)
+       | _ => None)
 End
 
 Definition do_phi_def:
   do_phi from_l s (Phi id _ entries) =
-    option_map (λarg. (id, eval s arg)) (alookup entries from_l)
+    option_join (option_map (λarg. option_map (\v. (id, v)) (eval s arg)) (alookup entries from_l))
 End
 
 Definition extract_value_def:
@@ -436,11 +468,12 @@ End
 Inductive step_instr:
 
   (s.stack = fr::st ∧
-   deallocate fr.stack_allocs s.heap = new_h
+   deallocate fr.stack_allocs s.heap = new_h ∧
+   eval s a = Some v
    ⇒
    step_instr prog s
      (Ret (t, a))
-     (update_result fr.result_var (eval s a)
+     (update_result fr.result_var v
        <| ip := fr.ret;
           globals := s.globals;
           locals := fr.saved_locals;
@@ -458,7 +491,7 @@ Inductive step_instr:
  * %r2 = phi [%r1, %l]
  * %r1 = phi [0, %l]
  *)
-  (eval s a = <| poison := p; value := FlatV (W1V tf) |> ∧
+  (eval s a = Some <| poison := p; value := FlatV (W1V tf) |> ∧
    l = Some (if tf = 1w then l1 else l2) ∧
    alookup prog s.ip.f = Some d ∧
    alookup d.blocks l = Some <| h := Head phis None; body := b |> ∧
@@ -472,22 +505,29 @@ Inductive step_instr:
   (* TODO *)
   (step_instr prog s (Invoke r t a args l1 l2) s) ∧
 
-  (step_instr prog s
+  (eval s a1 = Some v1 ∧
+   eval s a2 = Some v2 ∧
+   do_sub nuw nsw v1 v2 t = Some v3
+   ⇒
+   step_instr prog s
      (Sub r nuw nsw t a1 a2)
-     (inc_pc (update_result r (do_sub nuw nsw (eval s a1) (eval s a2)) s))) ∧
+     (inc_pc (update_result r v3 s))) ∧
 
-  (eval s a = v ∧
-   map (λci. cast_num (eval_const s.globals ci)) const_indices = map Some ns ∧
+  (eval s a = Some v ∧
+   (* The manual implies (but does not explicitly state) that the indices are
+    * interpreted as signed numbers *)
+   map (λci. signed_v_to_num (eval_const s.globals ci)) const_indices = map Some ns ∧
    extract_value v.value ns = Some result
    ⇒
    step_instr prog s
      (Extractvalue r (t, a) const_indices)
-     (inc_pc (update_result r
-                <| poison := v.poison; value := result |> s))) ∧
+     (inc_pc (update_result r <| poison := v.poison; value := result |> s))) ∧
 
-  (eval s a1 = v1 ∧
-   eval s a2 = v2 ∧
-   map (λci. cast_num (eval_const s.globals ci)) const_indices = map Some ns ∧
+  (eval s a1 = Some v1 ∧
+   eval s a2 = Some v2 ∧
+   (* The manual implies (but does not explicitly state) that the indices are
+    * interpreted as signed numbers *)
+   map (λci. signed_v_to_num (eval_const s.globals ci)) const_indices = map Some ns ∧
    insert_value v1.value v2.value ns = Some result
    ⇒
    step_instr prog s
@@ -495,16 +535,19 @@ Inductive step_instr:
      (inc_pc (update_result r
                 <| poison := (v1.poison ∨ v2.poison); value := result |> s))) ∧
 
-  (eval s a1 = v ∧
-   v2n v.value = Some n ∧
-   allocate s.heap (n * sizeof t) v.poison (n2, new_h)
+  (eval s a1 = Some v ∧
+   (* TODO Question is the number to allocate interpreted as a signed or
+    * unsigned quantity. E.g., if we allocate i8 0xFF does that do 255 or -1? *)
+   signed_v_to_num v.value = Some n ∧
+   allocate s.heap (n * sizeof t) v.poison (n2, new_h) ∧
+   mk_ptr n2 = Some ptr
    ⇒
    step_instr prog s
      (Alloca r t (t1, a1))
-     (inc_pc (update_result r <| poison := v.poison; value := FlatV (PtrV (n2w n2)) |>
+     (inc_pc (update_result r <| poison := v.poison; value := ptr |>
                 (s with heap := new_h)))) ∧
 
-  (eval s a1 = <| poison := p1; value := FlatV (PtrV w) |> ∧
+  (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
@@ -515,30 +558,34 @@ Inductive step_instr:
                                  value := fst (bytes_to_llvm_value t (map snd pbytes)) |>
                             s))) ∧
 
-  (eval s a2 = <| poison := p2; value := FlatV (PtrV w) |> ∧
+  (eval s a2 = Some <| poison := p2; value := FlatV (PtrV w) |> ∧
+   eval s a1 = Some v1 ∧
    interval = Interval freeable (w2n w) (w2n w + sizeof t) ∧
    is_allocated interval s.heap ∧
-   bytes = llvm_value_to_bytes (eval s a1).value ∧
+   bytes = llvm_value_to_bytes v1.value ∧
    length bytes = sizeof t
    ⇒
    step_instr prog s
      (Store (t1, a1) (t2, a2))
      (inc_pc (s with heap := set_bytes p2 bytes (w2n w) s.heap))) ∧
 
-  (map (eval s o snd) tindices = i1::indices ∧
-   (eval s a1).value = FlatV (PtrV w1) ∧
-   cast_num i1.value = Some n ∧
-   map (λx. cast_num x.value) indices = map Some ns ∧
-   get_offset t1 ns = Some off
+  (map (eval s o snd) tindices = map Some (i1::indices) ∧
+   eval s a1 = Some v ∧
+   v.value = FlatV (PtrV w1) ∧
+   (* The manual states that the indices are interpreted as signed numbers *)
+   signed_v_to_num i1.value = Some i ∧
+   map (λx. signed_v_to_num x.value) indices = map Some is ∧
+   get_offset t1 is = Some off ∧
+   mk_ptr (w2n w1 + sizeof t1 * i + off) = Some ptr
    ⇒
    step_instr prog s
     (Gep r t ((PtrT t1), a1) tindices)
     (inc_pc (update_result r
                <| poison := (v1.poison ∨ i1.poison ∨ exists (λv. v.poison) indices);
-                  value := FlatV (PtrV (n2w (w2n w1 + sizeof t1 * n + off))) |>
+                  value := ptr |>
                s))) ∧
 
-  (eval s a1 = v1 ∧
+  (eval s a1 = Some v1 ∧
    v1.value = FlatV (PtrV w) ∧
    w64_cast w t = Some int_v
    ⇒
@@ -546,23 +593,29 @@ Inductive step_instr:
     (Ptrtoint r (t1, a1) t)
     (inc_pc (update_result r <| poison := v1.poison; value := int_v |> s))) ∧
 
-  (eval s a1 = v1 ∧
-   cast_w64 v1.value = Some w
+  (eval s a1 = Some v1 ∧
+   unsigned_v_to_num v1.value = Some n ∧
+   mk_ptr n = Some ptr
    ⇒
    step_instr prog s
     (Inttoptr r (t1, a1) t)
-    (inc_pc (update_result r <| poison := v1.poison; value := FlatV (PtrV w) |> s))) ∧
+    (inc_pc (update_result r <| poison := v1.poison; value := ptr |> s))) ∧
 
-  (step_instr prog s
+  (eval s a1 = Some v1 ∧
+   eval s a2 = Some v2 ∧
+   do_icmp c v1 v2 = Some v3
+   ⇒
+   step_instr prog s
     (Icmp r c t a1 a2)
-    (inc_pc (update_result r (do_icmp c (eval s a1) (eval s a2)) s))) ∧
+    (inc_pc (update_result r v3 s))) ∧
 
-  (alookup prog fname = Some d
+  (alookup prog fname = Some d ∧
+   map (eval s o snd) targs = map Some vs
    ⇒
    step_instr prog s
      (Call r t fname targs)
      <| ip := <| f := fname; b := None; i := 0 |>;
-        locals := alist_to_fmap (zip (map snd d.params, map (eval s o snd) targs));
+        locals := alist_to_fmap (zip (map snd d.params, vs));
         globals := s.globals;
         stack :=
           <| ret := s.ip with i := s.ip.i + 1;
@@ -663,7 +716,7 @@ Definition is_init_state_def:
     globals_ok s ∧
     heap_ok s.heap ∧
     fdom s.globals = fdom global_init ∧
-    s.heap.valid_addresses =  { A n | n < dimword (:64) } ∧
+    s.heap.valid_addresses =  { A n | n < 256 ** pointer_size } ∧
     (* The initial allocations for globals are not freeable *)
     s.heap.allocations ⊆ { Interval F start stop | T } ∧
     (* The heap starts with the initial values of the globals written to their
diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml
index 8553be87f..6142b75fb 100644
--- a/sledge/semantics/llvm_propScript.sml
+++ b/sledge/semantics/llvm_propScript.sml
@@ -98,7 +98,7 @@ Proof
   irule b2v_v2b >>
   qexists_tac `f` >> rw [] >>
   unabbrev_all_tac >> fs [] >>
-  fs [unconvert_value_def, convert_value_def, value_type_cases] >>
+  fs [unconvert_value_def, convert_value_def, value_type_cases, pointer_size_def] >>
   wordsLib.WORD_DECIDE_TAC
 QED
 
diff --git a/sledge/semantics/llvm_to_llairScript.sml b/sledge/semantics/llvm_to_llairScript.sml
index 7ec5151d1..2d573bc55 100644
--- a/sledge/semantics/llvm_to_llairScript.sml
+++ b/sledge/semantics/llvm_to_llairScript.sml
@@ -61,9 +61,16 @@ Definition translate_size_def:
   (translate_size W64 = 64)
 End
 
-(* TODO *)
 Definition translate_ty_def:
-  translate_ty = ARB : ty -> typ
+  (translate_ty (FunT t ts) = FunctionT (translate_ty t) (map translate_ty ts)) ∧
+  (translate_ty (IntT s) = IntegerT (translate_size s)) ∧
+  (translate_ty (PtrT t) = PointerT (translate_ty t)) ∧
+  (translate_ty (ArrT n t) = ArrayT (translate_ty t) n) ∧
+  (translate_ty (StrT ts) = TupleT (map translate_ty ts))
+Termination
+  WF_REL_TAC `measure ty_size` >> rw [] >>
+  Induct_on `ts` >> rw [ty_size_def] >>
+  res_tac >> decide_tac
 End
 
 Definition translate_glob_var_def:
@@ -96,10 +103,13 @@ Termination
 End
 
 Definition translate_arg_def:
-  (translate_arg emap (Constant c) t = translate_const c) ∧
-  (translate_arg emap (Variable r) t =
+  (translate_arg emap (Constant c) = translate_const c) ∧
+  (translate_arg emap (Variable r) =
     case flookup emap r of
-    | None => Var (translate_reg r t)
+    (* With the current strategy of threading the emap through the whole
+     * function, we should never get a None here.
+     *)
+    | None => Var (translate_reg r (IntT W64))
     | Some e => e)
 End
 
@@ -113,11 +123,11 @@ 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 ty) (translate_arg emap a2 ty)) ∧
+    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 t) 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 t1) (translate_arg emap a2 t2) cs)
+    translate_updatevalue (translate_arg emap a1) (translate_arg emap a2) cs)
 End
 
 (* This translation of insertvalue to update and select is quadratic in the
@@ -170,15 +180,15 @@ End
 (* TODO *)
 Definition translate_instr_to_inst_def:
   (translate_instr_to_inst emap (llvm$Store (t1, a1) (t2, a2)) =
-    llair$Store (translate_arg emap a1 t1) (translate_arg emap a2 t2) (sizeof t2)) ∧
+    llair$Store (translate_arg emap a1) (translate_arg emap a2) (sizeof t2)) ∧
   (translate_instr_to_inst emap (Load r t (t1, a1)) =
-    Load (translate_reg r t1) (translate_arg emap a1 t1) (sizeof t))
+    Load (translate_reg r t) (translate_arg emap a1) (sizeof t))
 End
 
 (* TODO *)
 Definition translate_instr_to_term_def:
   translate_instr_to_term f emap (Br a l1 l2) =
-    Iswitch (translate_arg emap a (IntT W1)) [translate_label f l2; translate_label f l1]
+    Iswitch (translate_arg emap a) [translate_label f l2; translate_label f l1]
 End
 
 Datatype:
@@ -232,7 +242,9 @@ 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
- * structure. * emap is a mapping of registers to expressions that compute the
+ * structure.
+ *
+ * emap is a mapping of registers to expressions that compute the
  * value that should have been in the expression.
  *
  * This tries to build large expressions, and omits intermediate assignments
@@ -288,7 +300,8 @@ Definition translate_header_def:
     map
       (λ(r, t, largs).
         (translate_reg r t,
-         map (λ(l, arg). (translate_label_opt f entry l, translate_arg fempty arg t)) largs))
+        (* TODO: shouldn't use fempty here *)
+         map (λ(l, arg). (translate_label_opt f entry l, translate_arg fempty arg)) largs))
       (map dest_phi phis))
 End
 
@@ -357,7 +370,7 @@ Definition translate_param_def:
 End
 
 Definition translate_def_def:
-  translate_def (Lab f) d =
+  translate_def f d =
     let used_names = ARB in
     let entry_name = gen_name used_names "entry" in
     (* TODO *)
@@ -383,4 +396,14 @@ Definition translate_def_def:
         fthrow := ARB |>
 End
 
+Definition dest_fn_def:
+  dest_fn (Fn f) = f
+End
+
+Definition translate_prog_def:
+  translate_prog p =
+    <| globals := ARB;
+       functions := map (\(fname, d). (dest_fn fname, translate_def (dest_fn fname) d)) p |>
+End
+
 export_theory ();
diff --git a/sledge/semantics/llvm_to_llair_propScript.sml b/sledge/semantics/llvm_to_llair_propScript.sml
new file mode 100644
index 000000000..9efdfb781
--- /dev/null
+++ b/sledge/semantics/llvm_to_llair_propScript.sml
@@ -0,0 +1,278 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(* Proofs about llvm to llair translation *)
+
+open HolKernel boolLib bossLib Parse;
+open listTheory arithmeticTheory pred_setTheory finite_mapTheory wordsTheory integer_wordTheory;
+open settingsTheory miscTheory llvmTheory llairTheory llair_propTheory llvm_to_llairTheory;
+
+new_theory "llvm_to_llair_prop";
+
+numLib.prefer_num ();
+
+Inductive v_rel:
+  (∀w. v_rel (FlatV (PtrV w)) (FlatV (IntV (w2i w) pointer_size))) ∧
+  (∀w. v_rel (FlatV (W1V w)) (FlatV (IntV (w2i w) 1))) ∧
+  (∀w. v_rel (FlatV (W8V w)) (FlatV (IntV (w2i w) 8))) ∧
+  (∀w. v_rel (FlatV (W32V w)) (FlatV (IntV (w2i w) 32))) ∧
+  (∀w. v_rel (FlatV (W64V w)) (FlatV (IntV (w2i w) 64))) ∧
+  (∀vs1 vs2.
+    list_rel v_rel vs1 vs2
+    ⇒
+    v_rel (AggV vs1) (AggV vs2))
+End
+
+(* Define when an LLVM state is related to a llair one. Parameterised over a
+ * relation on program counters, which chould be generated by the
+ * transformation. It is not trivial because the translation cuts up blocks at
+ * function calls and for remiving phi nodes.
+ *
+ * Also parameterised on a map for locals relating LLVM registers to llair
+ * expressions that compute the value in that register. This corresponds to part
+ * of the translation's state.
+ *)
+Definition state_rel_def:
+  state_rel pc_rel emap (s:llvm$state) (s':llair$state) ⇔
+    pc_rel s.ip s'.bp ∧
+    (* Unmapped registers in LLVM are unmapped in llair too *)
+    (∀r. flookup s.locals r = None ⇒ flookup emap r = None) ∧
+    (* Mapped LLVM registers have a related value in the emap (after
+     * evaluating) *)
+    (∀r v. flookup s.locals r = Some v ⇒
+      ∃v' e.
+        v_rel v.value v' ∧
+        flookup emap r = Some e ∧ eval_exp s' e v') ∧
+    erase_tags s.heap = s'.heap
+End
+
+Theorem translate_arg_correct:
+  ∀s a v pc_rel emap s'.
+  state_rel pc_rel emap s s' ∧
+  eval s a = Some v
+  ⇒
+  ∃v'. eval_exp s' (translate_arg emap a) v' ∧ v_rel v.value v'
+Proof
+  Cases_on `a` >> rw [eval_def, translate_arg_def]
+  >- cheat >>
+  CASE_TAC >> fs [PULL_EXISTS, state_rel_def] >>
+  res_tac >> rfs [] >> metis_tac []
+QED
+
+Theorem translate_constant_correct_lem:
+  (∀c s pc_rel emap s' (g : glob_var |-> β # word64).
+   state_rel pc_rel emap s s'
+   ⇒
+   ∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v') ∧
+  (∀(cs : (ty # const) list) s pc_rel emap s' (g : glob_var |-> β # word64).
+   state_rel pc_rel 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 pc_rel emap s' (g : glob_var |-> β # word64).
+   state_rel pc_rel emap s s'
+   ⇒
+   ∃v'. eval_exp s' (translate_const (snd tc)) v' ∧ v_rel (eval_const g (snd tc)) v')
+Proof
+  ho_match_mp_tac const_induction >> rw [translate_const_def] >>
+  simp [Once eval_exp_cases, eval_const_def]
+  >- (
+    Cases_on `s` >> simp [eval_const_def, translate_size_def, v_rel_cases] >>
+    metis_tac [truncate_2comp_i2w_w2i, dimindex_1, dimindex_8, dimindex_32, dimindex_64])
+  >- (
+    simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
+    fs [combinTheory.o_DEF, pairTheory.LAMBDA_PROD] >>
+    metis_tac [])
+  >- (
+    simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
+    fs [combinTheory.o_DEF, pairTheory.LAMBDA_PROD] >>
+    metis_tac [])
+  >- cheat
+  >- cheat
+  >- cheat
+  >- cheat
+QED
+
+Theorem translate_constant_correct:
+  ∀c s pc_rel emap s' g.
+   state_rel pc_rel emap s s'
+   ⇒
+   ∃v'. eval_exp s' (translate_const c) v' ∧ v_rel (eval_const g c) v'
+Proof
+  metis_tac [translate_constant_correct_lem]
+QED
+
+Theorem restricted_i2w_11:
+  ∀i (w:'a word). INT_MIN (:'a) ≤ i ∧ i ≤ INT_MAX (:'a) ⇒ (i2w i : 'a word) = i2w (w2i w) ⇒ i = w2i w
+Proof
+  rw [i2w_def]
+  >- (
+    Cases_on `n2w (Num (-i)) = INT_MINw` >>
+    rw [w2i_neg, w2i_INT_MINw] >>
+    fs [word_L_def] >>
+    `?j. 0 ≤ j ∧ i = -j` by intLib.COOPER_TAC >>
+    rw [] >>
+    fs [] >>
+    `INT_MIN (:'a) < dimword (:'a)` by metis_tac [INT_MIN_LT_DIMWORD] >>
+    `Num j MOD dimword (:'a) = Num j`
+    by (irule LESS_MOD >> intLib.COOPER_TAC) >>
+    fs []
+    >- intLib.COOPER_TAC
+    >- (
+      `Num j < INT_MIN (:'a)` by intLib.COOPER_TAC >>
+      fs [w2i_n2w_pos, integerTheory.INT_OF_NUM]))
+  >- (
+    fs [GSYM INT_MAX, INT_MAX_def] >>
+    `Num i < INT_MIN (:'a)` by intLib.COOPER_TAC >>
+    rw [w2i_n2w_pos, integerTheory.INT_OF_NUM] >>
+    intLib.COOPER_TAC)
+QED
+
+Theorem translate_extract_correct:
+  ∀pc_rel emap s1 s1' a v v1' e1' cs ns result.
+    state_rel pc_rel 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' ∧
+      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'`
+  by metis_tac [translate_constant_correct] >>
+  Cases_on `v` >> fs [extract_value_def] >>
+  qpat_x_assum `v_rel (AggV _) _` mp_tac >>
+  simp [Once v_rel_cases] >> rw [] >>
+  simp [Once eval_exp_cases, PULL_EXISTS] >>
+  fs [LIST_REL_EL_EQN] >>
+  qmatch_assum_rename_tac `_ = map Some is` >>
+  Cases_on `eval_const s1.globals c` >> fs [signed_v_to_num_def, signed_v_to_int_def] >> rw [] >>
+  `?i. v2' = FlatV i` by fs [v_rel_cases] >> fs [] >>
+  qmatch_assum_rename_tac `option_join _ = Some x` >>
+  `?size. i = IntV (&x) size` suffices_by metis_tac [] >> rw [] >>
+  qpat_x_assum `v_rel _ _` mp_tac >>
+  simp [v_rel_cases] >> rw [] >> fs [signed_v_to_int_def] >> rw [] >>
+  intLib.COOPER_TAC
+QED
+
+Theorem translate_update_correct:
+  ∀pc_rel emap s1 s1' a v1 v1' v2 v2' e2 e2' e1' cs ns result.
+    state_rel pc_rel 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' ∧
+    v_rel v1 v1' ∧
+    eval_exp s1' e2' v2' ∧
+    v_rel v2 v2'
+    ⇒
+    ∃v3'.
+      eval_exp s1' (translate_updatevalue e1' e2' cs) v3' ∧
+      v_rel result v3'
+Proof
+  Induct_on `cs` >> rw [] >> fs [insert_value_def, translate_updatevalue_def]
+  >- metis_tac [] >>
+  simp [Once eval_exp_cases, PULL_EXISTS] >>
+  Cases_on `ns` >> fs [] >>
+  Cases_on `v1` >> fs [insert_value_def] >>
+  rename [`insert_value (el x _) _ ns`] >>
+  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` >>
+  qexists_tac `vs2` >> simp [] >>
+  `?v4'. eval_exp s1' (translate_const 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 (
+    pop_assum mp_tac >> simp [Once v_rel_cases] >>
+    rw [] >> fs [signed_v_to_num_def, signed_v_to_int_def] >>
+    intLib.COOPER_TAC) >>
+  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) >>
+  simp [Once eval_exp_cases] >>
+  metis_tac [EVERY2_LUPDATE_same, LIST_REL_LENGTH, LIST_REL_EL_EQN]
+QED
+
+Theorem translate_instr_to_exp_correct:
+  ∀emap instr r t s1 s1'.
+    classify_instr instr = Exp r t ∧
+    state_rel pc_rel emap s1 s1'
+    ⇒
+    (∀s2. step_instr prog s1 instr s2 ⇒
+      (∃v pv. eval_exp s1' (translate_instr_to_exp emap instr) v ∧
+              flookup s2.locals r = Some pv ∧ v_rel pv.value v))
+Proof
+  recInduct translate_instr_to_exp_ind >>
+  simp [translate_instr_to_exp_def, classify_instr_def] >>
+  conj_tac
+  >- ( (* Sub *)
+    rw [step_instr_cases, Once eval_exp_cases, do_sub_def, PULL_EXISTS] >>
+    simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
+    simp [v_rel_cases, PULL_EXISTS] >>
+    first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
+    disch_then drule >>
+    first_x_assum (mp_then.mp_then mp_then.Any mp_tac translate_arg_correct) >>
+    disch_then drule >>
+    BasicProvers.EVERY_CASE_TAC >> fs [translate_ty_def, translate_size_def] >>
+    rfs [v_rel_cases] >>
+    pairarg_tac >> fs [] >>
+    fs [pairTheory.PAIR_MAP, wordsTheory.FST_ADD_WITH_CARRY] >>
+    qmatch_goalsub_abbrev_tac `eval_exp _ _ (FlatV (IntV i1 _))` >> strip_tac >>
+    qmatch_goalsub_abbrev_tac `eval_exp _ _ (FlatV (IntV i2 _))` >> strip_tac >>
+    qexists_tac `i1` >> qexists_tac `i2` >> simp [] >>
+    unabbrev_all_tac >>
+    rw []
+    >- (
+      irule restricted_i2w_11 >> simp [word_sub_i2w] >>
+      `dimindex (:1) = 1` by rw [] >>
+      drule truncate_2comp_i2w_w2i >>
+      rw [word_sub_i2w] >>
+      metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:1)``,
+                 SIMP_CONV (srw_ss()) [] ``INT_MAX (:1)``])
+    >- (
+      irule restricted_i2w_11 >> simp [word_sub_i2w] >>
+      `dimindex (:8) = 8` by rw [] >>
+      drule truncate_2comp_i2w_w2i >>
+      rw [word_sub_i2w] >>
+      metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:8)``,
+                 SIMP_CONV (srw_ss()) [] ``INT_MAX (:8)``])
+    >- (
+      irule restricted_i2w_11 >> simp [word_sub_i2w] >>
+      `dimindex (:32) = 32` by rw [] >>
+      drule truncate_2comp_i2w_w2i >>
+      rw [word_sub_i2w] >>
+      metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:32)``,
+                 SIMP_CONV (srw_ss()) [] ``INT_MAX (:32)``])
+    >- (
+      irule restricted_i2w_11 >> simp [word_sub_i2w] >>
+      `dimindex (:64) = 64` by rw [] >>
+      drule truncate_2comp_i2w_w2i >>
+      rw [word_sub_i2w] >>
+      metis_tac [w2i_ge, w2i_le, SIMP_CONV (srw_ss()) [] ``INT_MIN (:64)``,
+                 SIMP_CONV (srw_ss()) [] ``INT_MAX (:64)``])) >>
+  conj_tac
+  >- (
+    rw [step_instr_cases] >>
+    simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
+    metis_tac [translate_arg_correct, translate_extract_correct]) >>
+  conj_tac
+  >- (
+    rw [step_instr_cases] >>
+    simp [inc_pc_def, update_result_def, FLOOKUP_UPDATE] >>
+    metis_tac [translate_arg_correct, translate_update_correct]) >>
+  cheat
+QED
+
+export_theory ();
diff --git a/sledge/semantics/memory_modelScript.sml b/sledge/semantics/memory_modelScript.sml
index 549be0955..2712063c4 100644
--- a/sledge/semantics/memory_modelScript.sml
+++ b/sledge/semantics/memory_modelScript.sml
@@ -47,6 +47,13 @@ Datatype:
             valid_addresses : addr set|>
 End
 
+Definition erase_tags_def:
+  erase_tags h =
+    <| memory := (λ(t,b). ((), b)) o_f h.memory;
+       allocations := h.allocations;
+       valid_addresses := h.valid_addresses |>
+End
+
 (* shapes statically describe the shape of a value in a register. Flat shapes
  * take a given number of bytes, Array shapes are replicated a certain number of
  * times
@@ -184,20 +191,21 @@ Definition deallocate_def:
 End
 
 
-(* Read len bytes from the list of bytes, and convert it into a word value,
+(* Read len bytes from the list of bytes, and convert it into a number,
  * little-endian encoding *)
-Definition le_read_w_def:
-  le_read_w len (bs : word8 list) =
+Definition le_read_num_def:
+  le_read_num len (bs : word8 list) =
     if length bs < len then
-      (l2w 256 (map w2n bs), [])
+      (l2n 256 (map w2n bs), [])
     else
-      (l2w 256 (map w2n (take len bs)), drop len bs)
+      (l2n 256 (map w2n (take len bs)), drop len bs)
 End
 
-(* Return len bytes that are the little-endian encoding of the argument word *)
-Definition le_write_w_def:
-  le_write_w len w =
-    let (l : word8 list) = map n2w (w2l 256 w) in
+(* Return len bytes that are the little-endian encoding of the argument number,
+ * assuming that it fits*)
+Definition le_write_num_def:
+  le_write_num len n =
+    let (l : word8 list) = map n2w (n2l 256 n) in
       take len (l ++ replicate (len - length l) 0w)
 End
 
@@ -205,7 +213,7 @@ End
  * shape. The function f is applied to the word read from a flat list of bytes
  * in little-endian order. *)
 Definition bytes_to_value_def:
-  (bytes_to_value f (Flat n t) bs = (FlatV o f n t ## I) (le_read_w n bs)) ∧
+  (bytes_to_value f (Flat n t) bs = (FlatV o f n t ## I) (le_read_num n bs)) ∧
   (bytes_to_value f (Array s n) bs = (AggV ## I) (read_array f n s bs)) ∧
   (bytes_to_value f (Tuple ts) bs = (AggV ## I) (read_str f ts bs)) ∧
   (read_array f 0 s bs = ([], bs)) ∧
@@ -230,7 +238,7 @@ End
 Definition value_to_bytes_def:
   (value_to_bytes f (FlatV x) =
     let (size, word) = f x in
-      le_write_w size word) ∧
+      le_write_num size word) ∧
   (value_to_bytes f (AggV vs) = flat (map (value_to_bytes f) vs))
 Termination
   WF_REL_TAC `measure (reg_v_size (\x. 0) o snd)` >>
@@ -241,10 +249,10 @@ End
 
 (* ----- Theorems about converting between values and byte lists ----- *)
 
-Theorem le_write_w_length:
-  ∀l x. length (le_write_w l w) = l
+Theorem le_write_num_length:
+  ∀l x. length (le_write_num l w) = l
 Proof
-  rw [le_write_w_def]
+  rw [le_write_num_def]
 QED
 
 Theorem v2b_size_lem:
@@ -255,7 +263,7 @@ Proof
   rw [value_to_bytes_def, sizeof_def, value_shape_def]
   >- (
     pairarg_tac >> simp [] >>
-    metis_tac [FST, le_write_w_length])
+    metis_tac [FST, le_write_num_length])
   >- (
     simp [LENGTH_FLAT, MAP_MAP_o, combinTheory.o_DEF] >>
     Induct_on `vs` >> rw [ADD1] >> fs [LEFT_ADD_DISTRIB] >>
@@ -271,15 +279,15 @@ Proof
 QED
 
 Theorem b2v_size_lem:
-  (∀(f:num->'c ->'a word -> 'b) s bs. sizeof s ≤ length bs ⇒
+  (∀(f:num->'c ->num -> 'b) s bs. sizeof s ≤ length bs ⇒
     ∃v. bytes_to_value f s bs = (v, drop (sizeof s) bs)) ∧
-  (∀(f:num->'c ->'a word -> 'b) n s bs. n * sizeof s ≤ length bs ⇒
+  (∀(f:num->'c ->num -> 'b) n s bs. n * sizeof s ≤ length bs ⇒
     ∃vs. read_array f n s bs = (vs, drop (n * sizeof s) bs)) ∧
-  (∀(f:num->'c ->'a word -> 'b) ss bs. sum (map sizeof ss) ≤ length bs ⇒
+  (∀(f:num->'c ->num -> 'b) ss bs. sum (map sizeof ss) ≤ length bs ⇒
     ∃vs. read_str f ss bs = (vs, drop (sum (map sizeof ss)) bs))
 Proof
   ho_match_mp_tac bytes_to_value_ind >>
-  rw [sizeof_def, bytes_to_value_def, le_read_w_def] >>
+  rw [sizeof_def, bytes_to_value_def, le_read_num_def] >>
   fs []
   >- (simp [PAIR_MAP] >> metis_tac [SND])
   >- (
@@ -305,15 +313,15 @@ Proof
 QED
 
 Theorem b2v_append_lem:
-  (∀(f:num->'c->'a word -> 'b) s bs. sizeof s ≤ length bs ⇒
+  (∀(f:num->'c->num -> 'b) s bs. sizeof s ≤ length bs ⇒
     bytes_to_value f s (bs ++ bs') = (I ## (λx. x ++ bs')) (bytes_to_value f s bs)) ∧
-  (∀(f:num->'c->'a word -> 'b) n s bs. n * sizeof s ≤ length bs ⇒
+  (∀(f:num->'c->num -> 'b) n s bs. n * sizeof s ≤ length bs ⇒
     ∃vs. read_array f n s (bs ++ bs') = (I ## (λx. x ++ bs')) (read_array f n s bs)) ∧
-  (∀(f:num->'c->'a word -> 'b) ss bs. sum (map sizeof ss) ≤ length bs ⇒
+  (∀(f:num->'c-> num -> 'b) ss bs. sum (map sizeof ss) ≤ length bs ⇒
     ∃vs. read_str f ss (bs ++ bs') = (I ## (λx. x ++ bs')) (read_str f ss bs))
 Proof
   ho_match_mp_tac bytes_to_value_ind >>
-  rw [sizeof_def, bytes_to_value_def, le_read_w_def] >>
+  rw [sizeof_def, bytes_to_value_def, le_read_num_def] >>
   fs [TAKE_APPEND, DROP_APPEND,
       DECIDE ``!x y. x ≤ y ⇒ x - y = 0n``, ETA_THM]
   >- (simp [PAIR_MAP] >> metis_tac [SND])
@@ -344,31 +352,30 @@ Proof
 QED
 
 Theorem le_read_write:
-  ∀n w bs.
-    w2n w < 256 ** n ⇒ le_read_w n (le_write_w n w ⧺ bs) = (w, bs)
+  ∀size n  bs.
+    n < 256 ** size ⇒ le_read_num size (le_write_num size n ⧺ bs) = (n, bs)
 Proof
-  rw [le_read_w_def, le_write_w_length]
+  rw [le_read_num_def, le_write_num_length]
   >- (
-    `take n (le_write_w n w ⧺ bs) = le_write_w n w`
-    by metis_tac [le_write_w_length, TAKE_LENGTH_APPEND] >>
-    simp [le_write_w_def, w2l_def, l2w_def] >>
-    Cases_on `w` >> simp [] >> fs [l2n_padding, TAKE_APPEND, take_replicate] >>
+    `take size (le_write_num size n ⧺ bs) = le_write_num size n`
+    by metis_tac [le_write_num_length, TAKE_LENGTH_APPEND] >>
+    simp [le_write_num_def, w2l_def, l2w_def] >>
+    fs [l2n_padding, TAKE_APPEND, take_replicate] >>
     simp [MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF, mod_n2l] >>
     rename1 `n2l 256 m` >>
-    Cases_on `n = 0` >> fs [] >>
-    `length (n2l 256 m) ≤ n`
+    Cases_on `size = 0` >> fs [] >>
+    `length (n2l 256 m) ≤ size`
     by (
       rw [LENGTH_n2l] >>
       `256 = 2 ** 8` by EVAL_TAC >>
       ASM_REWRITE_TAC [] >> simp [log_change_base_power, GSYM LESS_EQ] >>
-      `n2w m ≠ 0w` by simp [] >>
       rw [] >> fs [bitTheory.LOG2_def, dimword_def] >>
       `8 * (log 2 m DIV 8) ≤ log 2 m` by metis_tac [mul_div_bound, EVAL ``8 ≠ 0n``] >>
-      `LOG 2 m ≤ LOG 2 (256 ** n)` by simp [LOG_LE_MONO] >>
+      `LOG 2 m ≤ LOG 2 (256 ** size)` by simp [LOG_LE_MONO, LESS_IMP_LESS_OR_EQ] >>
       pop_assum mp_tac >>
       `256 = 2 ** 8` by EVAL_TAC >>
       ASM_REWRITE_TAC [EXP_MUL] >> simp [log_base_power] >>
-      Cases_on `log 2 m DIV 8 = n` >> rw [] >>
+      Cases_on `log 2 m DIV 8 = size` >> rw [] >>
       CCONTR_TAC >> fs [] >>
       `log 2 m = (8 * (log 2 m DIV 8))` by intLib.COOPER_TAC >> fs [] >>
       `2 ** log 2 m = 2 ** (8 * (log 2 m DIV 8))` by rw [] >>
@@ -376,26 +383,24 @@ Proof
       `2 ** log 2 m ≤ m` by rw [exp_log_bound] >>
       decide_tac) >>
     simp [mod_n2l, l2n_n2l, TAKE_LENGTH_TOO_LONG])
-  >- metis_tac [le_write_w_length, DROP_LENGTH_APPEND]
+  >- metis_tac [le_write_num_length, DROP_LENGTH_APPEND]
 QED
 
 Theorem le_write_read:
-  ∀n w bs bs'.
-    256 ** n ≤ dimword (:'a) ∧
-    n ≤ length bs ∧
-    le_read_w n bs = (w:'a word, bs')
+  ∀size n bs bs'.
+    size ≤ length bs ∧
+    le_read_num size bs = (n, bs')
     ⇒
-    le_write_w n w ++ bs' = bs
+    le_write_num size n ++ bs' = bs
 Proof
-  rw [le_read_w_def] >>
-  qmatch_goalsub_abbrev_tac `l2w _ l` >>
-  `le_write_w n (l2w 256 l) = take n bs` suffices_by metis_tac [TAKE_DROP] >>
-  simp [le_write_w_def, w2l_l2w] >>
-  `l2n 256 l < 256 ** n`
+  rw [le_read_num_def] >>
+  qmatch_goalsub_abbrev_tac `l2n _ l` >>
+  `le_write_num size (l2n 256 l) = take size bs` suffices_by metis_tac [TAKE_DROP] >>
+  simp [le_write_num_def, w2l_l2w] >>
+  `l2n 256 l < 256 ** size`
   by (
-    `n ≤ length bs` by decide_tac >>
+    `size ≤ length bs` by decide_tac >>
     metis_tac [l2n_lt, LENGTH_TAKE, LENGTH_MAP, EVAL ``0n < 256``]) >>
-  fs [] >>
   `every ($> 256) l`
   by (
     simp [EVERY_MAP, Abbr `l`] >> irule EVERY_TAKE >> simp [] >>
@@ -405,15 +410,15 @@ Proof
   rw [n2l_l2n]
   >- (
     rw [TAKE_def, take_replicate] >>
-    Cases_on `n` >> fs [] >>
+    Cases_on `size` >> fs [] >>
     rfs [l2n_0] >> unabbrev_all_tac >> fs [EVERY_MAP] >>
     ONCE_REWRITE_TAC [GSYM REPLICATE] >>
-    qmatch_goalsub_abbrev_tac `take n _` >>
+    qmatch_goalsub_abbrev_tac `take size _` >>
     qpat_assum `¬(_ < _)` mp_tac >>
     qpat_assum `every (\x. 0 = w2n x) _` mp_tac >>
     rpt (pop_assum kall_tac) >>
     qid_spec_tac `bs` >>
-    Induct_on `n` >> rw [] >>
+    Induct_on `size` >> rw [] >>
     Cases_on `bs` >> rw [] >> fs [] >>
     Cases_on `h` >> fs [] >>
     first_x_assum irule >> rw [] >>
@@ -430,11 +435,11 @@ Proof
     Cases_on `l` >> fs [dropWhile_eq_nil, combinTheory.o_DEF, EXISTS_REVERSE]) >>
   `0 < length (dropWhile ($= 0) (reverse l))` by decide_tac >>
   fs [SUC_PRE] >>
-  `map n2w l = take n bs`
+  `map n2w l = take size bs`
   by (simp [Abbr `l`, MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF, n2w_w2n]) >>
   simp [TAKE_TAKE_MIN] >>
-  `length l = n` by simp [Abbr `l`] >>
-  `length (dropWhile ($= 0) (reverse l)) ≤ n`
+  `length l = size` by simp [Abbr `l`] >>
+  `length (dropWhile ($= 0) (reverse l)) ≤ size`
   by metis_tac [LESS_EQ_TRANS, LENGTH_dropWhile_LESS_EQ, LENGTH_REVERSE] >>
   rw [MIN_DEF] >> fs []
   >- (
@@ -462,14 +467,14 @@ QED
 Theorem b2v_v2b_lem:
   (∀f s v.
     value_shape f s v ⇒
-    (∀x t n. f n t x ⇒ fst (h x) = n ∧ g n t (snd (h x)) = x ∧ w2n (snd (h x)) < 256 ** n) ⇒
+    (∀x t n. f n t x ⇒ fst (h x) = n ∧ g n t (snd (h x)) = x ∧ snd (h x) < 256 ** n) ⇒
     ∀bs.
-      bytes_to_value (g:num -> 'c -> 'a word -> 'b) s (value_to_bytes h v ++ bs) = (v, bs)) ∧
+      bytes_to_value g s (value_to_bytes h v ++ bs) = (v, bs)) ∧
   (∀f ss vs.
     value_shapes f ss vs ⇒
-    (∀x t n. f n t x ⇒ fst (h x) = n ∧ g n t (snd (h x)) = x ∧ w2n (snd (h x)) < 256 ** n) ⇒
+    (∀x t n. f n t x ⇒ fst (h x) = n ∧ g n t (snd (h x)) = x ∧ snd (h x) < 256 ** n) ⇒
     ∀bs.
-      read_str (g:num -> 'c -> 'a word -> 'b) ss (flat (map (value_to_bytes h) vs) ++ bs) = (vs, bs))
+      read_str g ss (flat (map (value_to_bytes h) vs) ++ bs) = (vs, bs))
 Proof
   ho_match_mp_tac value_shape_ind >> rw [value_shape_def] >>
   fs [bytes_to_value_def, value_to_bytes_def] >> rw []
@@ -501,7 +506,7 @@ QED
 Theorem b2v_v2b:
   ∀f g h s v bs.
     value_shape f s v ⇒
-    (∀x n t. f n t x ⇒ fst (h x) = n ∧ g n t (snd (h x)) = x ∧ w2n (snd (h x)) < 256 ** n) ⇒
+    (∀x n t. f n t x ⇒ fst (h x) = n ∧ g n t (snd (h x)) = x ∧ snd (h x) < 256 ** n) ⇒
       bytes_to_value g s (value_to_bytes h v ++ bs) = (v, bs)
 Proof
   metis_tac [b2v_v2b_lem]
diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml
index 953161431..58eac9995 100644
--- a/sledge/semantics/miscScript.sml
+++ b/sledge/semantics/miscScript.sml
@@ -9,7 +9,8 @@
  * could be upstreamed to HOL, and should eventually. *)
 
 open HolKernel boolLib bossLib Parse;
-open listTheory rich_listTheory arithmeticTheory wordsTheory;
+open listTheory rich_listTheory arithmeticTheory integerTheory;
+open integer_wordTheory wordsTheory;
 open finite_mapTheory open logrootTheory numposrepTheory;
 open settingsTheory;
 
@@ -169,4 +170,75 @@ Proof
   Induct >> rw []
 QED
 
+Definition truncate_2comp_def:
+  truncate_2comp (i:int) size =
+    (i + 2 ** (size - 1)) % 2 ** size - 2 ** (size - 1)
+End
+
+Theorem truncate_2comp_i2w_w2i:
+  ∀i size. dimindex (:'a) = size ⇒ truncate_2comp i size = w2i (i2w i : 'a word)
+Proof
+  rw [truncate_2comp_def, w2i_def, word_msb_i2w, w2n_i2w] >>
+  qmatch_goalsub_abbrev_tac `(_ + s1) % s2` >>
+  `2 * s1 = s2` by rw [Abbr `s1`, Abbr `s2`, GSYM EXP, DIMINDEX_GT_0] >>
+  `0 ≠ s2 ∧ ¬(s2 < 0)` by rw [Abbr `s2`] >>
+  fs [MULT_MINUS_ONE, w2n_i2w] >>
+  fs [GSYM dimword_def, dimword_IS_TWICE_INT_MIN]
+  >- (
+    `-i % s2 = -((i + s1) % s2 - s1)` suffices_by intLib.COOPER_TAC >>
+    simp [] >>
+    irule INT_MOD_UNIQUE >>
+    simp [GSYM PULL_EXISTS] >>
+    conj_tac
+    >- (
+      simp [int_mod, INT_ADD_ASSOC,
+            intLib.COOPER_PROVE ``!x y (z:int). x - (y + z - a) = x - y - z + a``] >>
+      qexists_tac `-((i + s1) / s2)` >>
+      intLib.COOPER_TAC) >>
+    `&INT_MIN (:α) = s1` by (unabbrev_all_tac >> rw [INT_MIN_def]) >>
+    fs [INT_SUB_LE] >>
+    `0 ≤ (i + s1) % s2` by metis_tac [INT_MOD_BOUNDS] >>
+    strip_tac
+    >- (
+      `(i + s1) % s2 = (i % s2 + s1 % s2) % s2`
+      by (irule (GSYM INT_MOD_PLUS) >> rw []) >>
+      simp [] >>
+      `(i % s2 + s1 % s2) % s2 = (-1 * s2 + (i % s2 + s1 % s2)) % s2`
+      by (metis_tac [INT_MOD_ADD_MULTIPLES]) >>
+      simp [GSYM INT_NEG_MINUS1, INT_ADD_ASSOC] >>
+      `i % s2 < s2 ∧ s1 % s2 < s2 ∧ i % s2 ≤ s2` by metis_tac [INT_MOD_BOUNDS, INT_LT_IMP_LE] >>
+      `0 ≤ s1 ∧ s1 < s2 ∧ -s2 + i % s2 + s1 % s2 < s2` by intLib.COOPER_TAC >>
+      `0 ≤ -s2 + i % s2 + s1 % s2`
+      by (
+        `s2 = s1 + s1` by intLib.COOPER_TAC >>
+        fs [INT_LESS_MOD] >>
+        intLib.COOPER_TAC) >>
+      simp [INT_LESS_MOD] >>
+      intLib.COOPER_TAC)
+    >- intLib.COOPER_TAC)
+  >- (
+    `(i + s1) % s2 = i % s2 + s1` suffices_by intLib.COOPER_TAC >>
+    `(i + s1) % s2 = i % s2 + s1 % s2`
+    suffices_by (
+      rw [] >>
+      irule INT_LESS_MOD >> rw [] >>
+      intLib.COOPER_TAC) >>
+    `(i + s1) % s2 = (i % s2 + s1 % s2) % s2`
+    suffices_by (
+      fs [Abbr `s2`] >>
+      `s1 = &INT_MIN (:'a)` by intLib.COOPER_TAC >> rw [] >>
+      irule INT_LESS_MOD >> rw [] >>
+      fs [intLib.COOPER_PROVE ``!(x:int) y. ¬(x ≤ y) ⇔ y < x``] >> rw [] >>
+      full_simp_tac std_ss [GSYM INT_MUL] >>
+      qpat_abbrev_tac `s = &INT_MIN (:α)`
+      >- (
+        `2*s ≠ 0 ∧ ¬(2*s < 0) ∧ ¬(s < 0)`
+        by (unabbrev_all_tac >> rw []) >>
+        drule INT_MOD_BOUNDS >> simp [] >>
+        disch_then (qspec_then `i` mp_tac) >> simp [] >>
+        intLib.COOPER_TAC)
+      >- intLib.COOPER_TAC) >>
+    simp [INT_MOD_PLUS])
+QED
+
 export_theory ();
diff --git a/sledge/semantics/settingsScript.sml b/sledge/semantics/settingsScript.sml
index f5cb4095f..2213357c7 100644
--- a/sledge/semantics/settingsScript.sml
+++ b/sledge/semantics/settingsScript.sml
@@ -53,5 +53,7 @@ overload_on ("alookup", ``ALOOKUP``);
 overload_on ("filter", ``FILTER``);
 overload_on ("map2", ``list$MAP2``);
 overload_on ("foldl", ``FOLDL``);
+overload_on ("foldr", ``FOLDR``);
+overload_on ("option_rel", ``OPTREL``);
 
 export_theory ();