diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml
index 14a555948..e07e25385 100644
--- a/sledge/semantics/llairScript.sml
+++ b/sledge/semantics/llairScript.sml
@@ -8,7 +8,7 @@
 (* A mini-LLAIR model, based on the files in sledge/src/llair *)
 
 open HolKernel boolLib bossLib Parse;
-open settingsTheory;
+open settingsTheory memory_modelTheory;
 
 new_theory "llair";
 
@@ -120,25 +120,19 @@ End
 
 (* ----- Semantic states ----- *)
 
-(* TODO Given the similarities with LLVM, consider moving some definitions into
- * a common predecessor theory *)
-
-Datatype:
-  addr = A num
-End
-
 (* 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.
  *)
 Datatype:
-  v =
+  flat_v =
   | LocV num
   | SizeV num
   | IntV int num
-  | AggV (v list)
 End
 
+Type v = ``:flat_v reg_v``
+
 Datatype:
   pc = <| l : label; i : num |>
 End
@@ -153,15 +147,7 @@ Datatype:
        globals : var |-> word64;
        locals : var |-> v;
        stack : frame list;
-       (* The set of allocated ranges.
-        * The llvm model had a bool to indicate whether the range is free-able
-        * or not, since the memory that the globals is in should never be freed.
-        * llair does not currently catch this error, so we won't either. If
-        * llair wants to catch the error in the future, then we can adapt the
-        * semantics. *)
-       allocations : (num # num) set;
-       (* A byte addressed heap *)
-       heap : addr |-> word8 |>
+       heap : unit heap |>
 End
 
 (* ----- Semantic transitions ----- *)
diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index 03d096d9f..d77e35485 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -9,7 +9,7 @@
  * are relevant for the LLVM -> LLAIR translation, especially exceptions. *)
 
 open HolKernel boolLib bossLib Parse;
-open settingsTheory;
+open settingsTheory memory_modelTheory;
 
 new_theory "llvm";
 
@@ -137,20 +137,17 @@ End
 (* ----- Semantic states ----- *)
 
 Datatype:
-  addr = A num
-End
-
-Datatype:
-  v =
+  flat_v =
   | W1V word1
   | W8V word8
   | W32V word32
   | W64V word64
-  | AggV (v list)
   | PtrV word64
   | UndefV
 End
 
+Type v = ``:flat_v reg_v``
+
 Datatype:
   pv = <| poison : bool; value : v |>
 End
@@ -170,11 +167,7 @@ Datatype:
        globals : glob_var |-> (num # word64);
        locals : reg |-> pv;
        stack : frame list;
-       (* The set of allocated ranges. The bool indicates whether the range is
-        * free-able or not *)
-       allocations : (bool # num # num) set;
-       (* A byte addressed heap, with a poison tag *)
-       heap : addr |-> bool # word8 |>
+       heap : bool heap |>
 End
 
 (* ----- Things about types ----- *)
@@ -217,11 +210,11 @@ Definition indices_ok_def:
 End
 
 Inductive value_type:
-  (value_type (IntT W1) (W1V w1)) ∧
-  (value_type (IntT W8) (W8V w8)) ∧
-  (value_type (IntT W32) (W32V w32)) ∧
-  (value_type (IntT W64) (W64V w64)) ∧
-  (value_type (PtrT _) (PtrV w64)) ∧
+  (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))) ∧
   (every (value_type t) vs ∧ length vs = n ∧ first_class_type t
    ⇒
    value_type (ArrT n t) (AggV vs)) ∧
@@ -230,30 +223,19 @@ Inductive value_type:
    value_type (StrT ts) (AggV vs))
 End
 
-(* ----- Semantic transitions ----- *)
-
-Definition w64_cast_def:
-  (w64_cast w (IntT W1) = Some (W1V (w2w w))) ∧
-  (w64_cast w (IntT W8) = Some (W8V (w2w w))) ∧
-  (w64_cast w (IntT W32) = Some (W32V (w2w w))) ∧
-  (w64_cast w (IntT W64) = Some (W64V w)) ∧
-  (w64_cast _ _ = None)
-End
-
-Definition cast_w64_def:
-  (cast_w64 (W1V w) = Some (w2w w)) ∧
-  (cast_w64 (W8V w) = Some (w2w w)) ∧
-  (cast_w64 (W32V w) = Some (w2w w)) ∧
-  (cast_w64 (W64V w) = Some w) ∧
-  (cast_w64 _ = None)
-End
-
-Definition cast_num_def:
-  cast_num v = option_map w2n (cast_w64 v)
-End
-
-Definition bool_to_v_def:
-  bool_to_v b = if b then W1V 1w else W1V 0w
+Definition extract_type_def:
+  (extract_type t [] = Some t) ∧
+  (extract_type (ArrT n t) (i::idx) =
+    if i < n then
+      extract_type t idx
+    else
+      None) ∧
+  (extract_type (StrT ts) (i::idx) =
+    if i < length ts then
+      extract_type (el i ts) idx
+    else
+      None) ∧
+  (extract_type _ _ = None)
 End
 
 (* Calculate the offset given by a list of indices *)
@@ -273,26 +255,52 @@ Definition get_offset_def:
   (get_offset _ _ = Some 0)
 End
 
+(* ----- Semantic transitions ----- *)
+
+Definition w64_cast_def:
+  (w64_cast w (IntT W1) = Some (FlatV (W1V (w2w w)))) ∧
+  (w64_cast w (IntT W8) = Some (FlatV (W8V (w2w w)))) ∧
+  (w64_cast w (IntT W32) = Some (FlatV (W32V (w2w w)))) ∧
+  (w64_cast w (IntT W64) = Some (FlatV (W64V w))) ∧
+  (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)
+End
+
+Definition cast_num_def:
+  cast_num v = option_map w2n (cast_w64 v)
+End
+
+Definition bool_to_v_def:
+  bool_to_v b = if b then FlatV (W1V 1w) else FlatV (W1V 0w)
+End
+
 Definition eval_const_def:
-  (eval_const g (IntC W1 i) = W1V (i2w i)) ∧
-  (eval_const g (IntC W8 i) = W8V (i2w i)) ∧
-  (eval_const g (IntC W32 i) = W32V (i2w i)) ∧
-  (eval_const g (IntC W64 i) = W64V (i2w i)) ∧
+  (eval_const g (IntC W1 i) = FlatV (W1V (i2w i))) ∧
+  (eval_const g (IntC W8 i) = FlatV (W8V (i2w i))) ∧
+  (eval_const g (IntC W32 i) = FlatV (W32V (i2w i))) ∧
+  (eval_const g (IntC W64 i) = FlatV (W64V (i2w i))) ∧
   (eval_const g (StrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧
   (eval_const g (ArrC tconsts) = AggV (map (eval_const g) (map snd tconsts))) ∧
   (eval_const g (GepC ty ptr (t, idx) indices) =
     case (eval_const g ptr, cast_num (eval_const g idx)) of
-    | (PtrV w, Some n) =>
+    | (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 get_offset ty ns of
-         | None => UndefV
-         | Some off => PtrV (n2w (w2n w + sizeof ty * n + off)))
-    | _ => UndefV) ∧
+         | None => FlatV UndefV
+         | Some off => FlatV (PtrV (n2w (w2n w + sizeof ty * n + off))))
+    | _ => FlatV UndefV) ∧
   (eval_const g (GlobalC var) =
     case flookup g var of
-    | None => PtrV 0w
-    | Some (s,w) => PtrV w) ∧
-  (eval_const g UndefC = UndefV)
+    | None => FlatV (PtrV 0w)
+    | Some (s,w) => FlatV (PtrV w)) ∧
+  (eval_const g UndefC = FlatV UndefV)
 Termination
   WF_REL_TAC `measure (const_size o snd)` >> rw [listTheory.MEM_MAP] >>
   TRY
@@ -306,140 +314,64 @@ End
 Definition eval_def:
   (eval s (Variable v) =
     case flookup s.locals v of
-    | None => <| poison := F; value := W1V 0w |>
+    | 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 (W1V b) = Some (if T then 1 else 0)) ∧
-  (v2n (W8V w8) = Some (w2n w8)) ∧
-  (v2n (W32V w32) = Some (w2n w32)) ∧
-  (v2n (W64V w64) = Some (w2n w64)) ∧
+  (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)
 End
 
-Definition interval_to_set_def:
-  interval_to_set (_, start,stop) =
-    { n | start ≤ n ∧ n < stop }
-End
-
-Definition interval_ok_def:
-  interval_ok ((_:bool), i1, i2) ⇔
-    i1 ≤ i2 ∧ i2 < 2 ** 64
-End
-
-Definition is_allocated_def:
-  is_allocated b1 allocs ⇔
-    interval_ok b1 ∧
-    ∃b2. b2 ∈ allocs ∧ fst b1 = fst b2 ∧ interval_to_set b1 ⊆ interval_to_set b2
-End
-
-Definition is_free_def:
-  is_free b1 allocs ⇔
-    interval_ok b1 ∧
-    ∀b2. b2 ∈ allocs ⇒ interval_to_set b1 ∩ interval_to_set b2 = ∅
-End
-
-Definition get_bytes_def:
-  get_bytes h (_, start, stop) =
-    map
-      (λoff.
-        case flookup h (A (start + off)) of
-        | None => (F, 0w)
-        | Some w => w)
-      (count_list (stop - start))
+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)) ∧
+  (type_to_shape (ArrT n t) = Array (type_to_shape t) n) ∧
+  (type_to_shape (StrT ts) = Tuple (map type_to_shape ts))
+Termination
+  WF_REL_TAC `measure ty_size` >> rw [] >>
+  Induct_on `ts` >> rw [definition "ty_size_def"] >>
+  res_tac >> simp []
 End
 
-Definition set_bytes_def:
-  (set_bytes p [] n h = h) ∧
-  (set_bytes p (b::bs) n h =
-    set_bytes p bs (Suc n) (h |+ (A n, (p, b))))
+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)
 End
 
-(* Allocate a free chunk of memory, and write non-deterministic bytes into it *)
-Inductive allocate:
-  v2n v.value = Some m ∧
-   b = (T, w2n w, w2n w + m * len) ∧
-   is_free b s.allocations ∧
-   length bytes = m * len
-   ⇒
-   allocate s v len
-     (<| poison := v.poison; value := PtrV w |>,
-         s with <| allocations := { b } ∪ s.allocations;
-                   heap := set_bytes v.poison bytes (w2n w) s.heap |>)
+Definition bytes_to_llvm_value_def:
+  bytes_to_llvm_value t bs =
+    (bytes_to_value (λn t w. convert_value t w) (type_to_shape t) bs)
 End
 
-Definition deallocate_def:
-  deallocate addrs allocs h =
-    let to_remove = { (T, n, stop) | A n ∈ set addrs ∧ (T, n, stop) ∈ allocs } in
-      (allocs DIFF to_remove, fdiff h (image A (bigunion (image interval_to_set to_remove))))
+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))
 End
 
-(* Read len bytes from the list of bytes, and convert it into a word value,
- * little-endian encoding *)
-Definition le_read_w_def:
-  le_read_w len (bs : word8 list) =
-    if length bs < len then
-      (l2w 256 (map w2n bs), [])
-    else
-      (l2w 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
-      take len (l ++ replicate (len - length l) 0w)
-End
-
-Definition bytes_to_value_def:
-  (bytes_to_value (IntT W1) (b::bs) = (W1V (w2w b), bs)) ∧
-  (bytes_to_value (IntT W8) (b::bs) = (W8V b, bs)) ∧
-  (bytes_to_value (IntT W32) bs = (W32V ## I) (le_read_w 4 bs)) ∧
-  (bytes_to_value (IntT W64) bs = (W64V ## I) (le_read_w 8 bs)) ∧
-  (bytes_to_value (PtrT _) bs = (PtrV ## I) (le_read_w 8 bs)) ∧
-  (bytes_to_value (ArrT n t) bs = (AggV ## I) (read_array n t bs)) ∧
-  (bytes_to_value (StrT ts) bs = (AggV ## I) (read_str ts bs)) ∧
-  (read_array 0 t bs = ([], bs)) ∧
-  (read_array (Suc n) t bs =
-    let (v, bs) = bytes_to_value t bs in
-    let (rest, bs) = read_array n t bs in
-      (v::rest, bs)) ∧
-  (read_str [] bs = ([], bs)) ∧
-  (read_str (t::ts) bs =
-    let (v, bs) = bytes_to_value t bs in
-    let (rest, bs) = read_str ts bs in
-      (v::rest, bs))
-Termination
-  WF_REL_TAC `measure (λx. case x of
-                           | INL (t, bs) => ty_size t
-                           | INR (INL (n, t, bs)) => n + ty_size t
-                           | INR (INR (ts, bs)) => ty1_size ts)`
-End
-
-Definition value_to_bytes_def:
-  (value_to_bytes (W1V w) = [w2w w]) ∧
-  (value_to_bytes (W8V w) = [w]) ∧
-  (value_to_bytes (W32V w) = le_write_w 4 w) ∧
-  (value_to_bytes (W64V w) = le_write_w 8 w) ∧
-  (value_to_bytes (PtrV n) = le_write_w 8 n) ∧
-  (value_to_bytes (AggV vs) = flat (map value_to_bytes vs))
-Termination
-  WF_REL_TAC `measure v_size` >>
-  Induct >> rw [definition "v_size_def"] >>
-  TRY (first_x_assum drule) >>
-  decide_tac
+Definition llvm_value_to_bytes_def:
+  llvm_value_to_bytes v =
+    value_to_bytes unconvert_value v
 End
 
 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
-      | (W1V w1, W1V w2) => (W1V ## I) (add_with_carry (w1, ¬w2, T))
-      | (W8V w1, W8V w2) => (W8V ## I) (add_with_carry (w1, ¬w2, T))
-      | (W32V w1, W32V w2) => (W32V ## I) (add_with_carry (w1, ¬w2, T))
-      | (W64V w1, W64V w2) => (W64V ## I) (add_with_carry (w1, ¬w2, T))
+      | (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))
     in
     let p = ((nuw ∧ u_overflow) ∨ (nsw ∧ s_overflow) ∨ v1.poison ∨ v2.poison) in
       <| poison := p; value := diff |>
@@ -456,11 +388,11 @@ Definition do_icmp_def:
     <| poison := (v1.poison ∨ v2.poison);
        value := bool_to_v (
          case (v1.value, v2.value) of
-         | (W1V w1, W1V w2) => (get_comp c) w1 w2
-         | (W8V w1, W8V w2) => (get_comp c) w1 w2
-         | (W32V w1, W32V w2) => (get_comp c) w1 w2
-         | (W64V w1, W64V w2) => (get_comp c) w1 w2
-         | (PtrV w1, PtrV w2) => (get_comp c) w1 w2) |>
+         | (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) |>
 End
 
 Definition do_phi_def:
@@ -468,21 +400,6 @@ Definition do_phi_def:
     option_map (λarg. (id, eval s arg)) (alookup entries from_l)
 End
 
-Definition extract_type_def:
-  (extract_type t [] = Some t) ∧
-  (extract_type (ArrT n t) (i::idx) =
-    if i < n then
-      extract_type t idx
-    else
-      None) ∧
-  (extract_type (StrT ts) (i::idx) =
-    if i < length ts then
-      extract_type (el i ts) idx
-    else
-      None) ∧
-  (extract_type _ _ = None)
-End
-
 Definition extract_value_def:
   (extract_value v [] = Some v) ∧
   (extract_value (AggV vs) (i::indices) =
@@ -519,7 +436,7 @@ End
 Inductive step_instr:
 
   (s.stack = fr::st ∧
-   deallocate fr.stack_allocs s.allocations s.heap = (new_allocs, new_h)
+   deallocate fr.stack_allocs s.heap = new_h
    ⇒
    step_instr prog s
      (Ret (t, a))
@@ -528,7 +445,6 @@ Inductive step_instr:
           globals := s.globals;
           locals := fr.saved_locals;
           stack := st;
-          allocations := new_allocs;
           heap := new_h |>)) ∧
 
 (* Do the phi assignments in parallel. The manual says "For the purposes of the
@@ -542,7 +458,7 @@ Inductive step_instr:
  * %r2 = phi [%r1, %l]
  * %r1 = phi [0, %l]
  *)
-  (eval s a = <| poison := p; value := W1V tf |> ∧
+  (eval s a = <| 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 |> ∧
@@ -579,27 +495,29 @@ Inductive step_instr:
      (inc_pc (update_result r
                 <| poison := (v1.poison ∨ v2.poison); value := result |> s))) ∧
 
-  (allocate s (eval s a1) (sizeof t) (v2, s2)
+  (eval s a1 = v ∧
+   v2n v.value = Some n ∧
+   allocate s.heap (n * sizeof t) v.poison (v2, new_h)
    ⇒
    step_instr prog s
      (Alloca r t (t1, a1))
-     (inc_pc (update_result r v2 s2))) ∧
+     (inc_pc (update_result r v2 (s with heap := new_h)))) ∧
 
-  (eval s a1 = <| poison := p1; value := PtrV w |> ∧
-   interval = (freeable, w2n w, w2n w + sizeof t) ∧
-   is_allocated interval s.allocations ∧
+  (eval s a1 = <| poison := p1; value := FlatV (PtrV w) |> ∧
+   interval = Interval freeable (w2n w) (w2n w + sizeof t) ∧
+   is_allocated interval s.heap ∧
    pbytes = get_bytes s.heap interval
    ⇒
    step_instr prog s
      (Load r t (t1, a1))
      (inc_pc (update_result r <| poison := (T ∈ set (map fst pbytes));
-                                 value := fst (bytes_to_value t (map snd pbytes)) |>
+                                 value := fst (bytes_to_llvm_value t (map snd pbytes)) |>
                             s))) ∧
 
-  (eval s a2 = <| poison := p2; value := PtrV w |> ∧
-   interval = (freeable, w2n w, w2n w + sizeof t) ∧
-   is_allocated interval s.allocations ∧
-   bytes = value_to_bytes (eval s a1).value ∧
+  (eval s a2 = <| poison := p2; value := FlatV (PtrV w) |> ∧
+   interval = Interval freeable (w2n w) (w2n w + sizeof t) ∧
+   is_allocated interval s.heap ∧
+   bytes = llvm_value_to_bytes (eval s a1).value ∧
    length bytes = sizeof t
    ⇒
    step_instr prog s
@@ -607,7 +525,7 @@ Inductive step_instr:
      (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 = PtrV w1 ∧
+   (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
@@ -616,11 +534,11 @@ Inductive step_instr:
     (Gep r t ((PtrT t1), a1) tindices)
     (inc_pc (update_result r
                <| poison := (v1.poison ∨ i1.poison ∨ exists (λv. v.poison) indices);
-                  value := PtrV (n2w (w2n w1 + sizeof t1 * n + off)) |>
+                  value := FlatV (PtrV (n2w (w2n w1 + sizeof t1 * n + off))) |>
                s))) ∧
 
   (eval s a1 = v1 ∧
-   v1.value = PtrV w ∧
+   v1.value = FlatV (PtrV w) ∧
    w64_cast w t = Some int_v
    ⇒
    step_instr prog s
@@ -632,7 +550,7 @@ Inductive step_instr:
    ⇒
    step_instr prog s
     (Inttoptr r (t1, a1) t)
-    (inc_pc (update_result r <| poison := v1.poison; value := PtrV w |> s))) ∧
+    (inc_pc (update_result r <| poison := v1.poison; value := FlatV (PtrV w) |> s))) ∧
 
   (step_instr prog s
     (Icmp r c t a1 a2)
@@ -645,7 +563,6 @@ Inductive step_instr:
      <| ip := <| f := fname; b := None; i := 0 |>;
         locals := alist_to_fmap (zip (map snd d.params, map (eval s o snd) targs));
         globals := s.globals;
-        allocations:= s.allocations;
         stack :=
           <| ret := s.ip with i := s.ip.i + 1;
              saved_locals := s.locals;
@@ -682,29 +599,13 @@ End
 
 (* ----- Invariants on state ----- *)
 
-(* The allocations are of intervals that don't overlap *)
-Definition allocations_ok_def:
-  allocations_ok s ⇔
-    ∀i1 i2.
-      i1 ∈ s.allocations ∧ i2 ∈ s.allocations
-      ⇒
-      interval_ok i1 ∧ interval_ok i2 ∧
-      (interval_to_set i1 ∩ interval_to_set i2 ≠ ∅ ⇒ i1 = i2)
-End
-
-(* The heap maps exactly the address in the allocations *)
-Definition heap_ok_def:
-  heap_ok s ⇔
-    ∀n. flookup s.heap (A n) ≠ None ⇔ ∃i. i ∈ s.allocations ∧ n ∈ interval_to_set i
-End
-
 (* All global variables are allocated in non-freeable memory *)
 Definition globals_ok_def:
   globals_ok s ⇔
     ∀g n w.
       flookup s.globals g = Some (n, w)
       ⇒
-      is_allocated (F, w2n w, w2n w + n) s.allocations
+      is_allocated (Interval F (w2n w) (w2n w + n)) s.heap
 End
 
 (* Instruction pointer points to an instruction *)
@@ -733,7 +634,7 @@ End
 Definition frame_ok_def:
   frame_ok p s f ⇔
     ip_ok p f.ret ∧
-    every (λn. ∃start stop. n = A start ∧ (T, start, stop) ∈ s.allocations) f.stack_allocs
+    every (λn. ∃start stop. n = A start ∧ Interval T start stop ∈ s.heap.allocations) f.stack_allocs
 End
 
 (* The frames are all of, and no two stack allocations have the same address *)
@@ -745,7 +646,7 @@ End
 
 Definition state_invariant_def:
   state_invariant p s ⇔
-    ip_ok p s.ip ∧ allocations_ok s ∧ heap_ok s ∧ globals_ok s ∧ stack_ok p s
+    ip_ok p s.ip ∧ heap_ok s.heap ∧ globals_ok s ∧ stack_ok p s
 End
 
 (* ----- Initial state ----- *)
@@ -758,19 +659,19 @@ Definition is_init_state_def:
     s.ip.i = 0 ∧
     s.locals = fempty ∧
     s.stack = [] ∧
-    allocations_ok s ∧
     globals_ok s ∧
-    heap_ok s ∧
+    heap_ok s.heap ∧
     fdom s.globals = fdom global_init ∧
+    s.heap.valid_addresses =  { A n | n < dimword (:64) } ∧
     (* The initial allocations for globals are not freeable *)
-    s.allocations ⊆ { (F, start, stop) | T } ∧
+    s.heap.allocations ⊆ { Interval F start stop | T } ∧
     (* The heap starts with the initial values of the globals written to their
      * addresses *)
     ∀g w t v n.
       flookup s.globals g = Some (n, w) ∧ flookup global_init g = Some (t,v) ⇒
       ∃bytes.
-        get_bytes s.heap (F, w2n w, w2n w + sizeof t) = map (λb. (F,b)) bytes ∧
-        bytes_to_value t bytes = (v, [])
+        get_bytes s.heap (Interval F (w2n w) (w2n w + sizeof t)) = map (λb. (F,b)) bytes ∧
+        bytes_to_llvm_value t bytes = (v, [])
 End
 
 export_theory();
diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml
index bf91f304e..8553be87f 100644
--- a/sledge/semantics/llvm_propScript.sml
+++ b/sledge/semantics/llvm_propScript.sml
@@ -11,393 +11,95 @@ open HolKernel boolLib bossLib Parse;
 open pairTheory listTheory rich_listTheory arithmeticTheory wordsTheory;
 open pred_setTheory finite_mapTheory;
 open logrootTheory numposrepTheory;
-open settingsTheory llvmTheory;
+open settingsTheory miscTheory llvmTheory memory_modelTheory;
 
 new_theory "llvm_prop";
 
 numLib.prefer_num();
 
-(* ----- Theorems about list library functions ----- *)
-(* Could be upstreamed to HOL *)
-
-Theorem dropWhile_map:
-  ∀P f l. dropWhile P (map f l) = map f (dropWhile (P o f) l)
-Proof
-  Induct_on `l` >> rw []
-QED
-
-Theorem dropWhile_prop:
-  ∀P l x. x < length l - length (dropWhile P l) ⇒ P (el x l)
-Proof
-  Induct_on `l` >> rw [] >>
-  Cases_on `x` >> fs []
-QED
-
-Theorem dropWhile_rev_take:
-  ∀P n l x.
-    let len = length (dropWhile P (reverse (take n l))) in
-      x + len < n ∧ n ≤ length l ⇒ P (el (x + len) l)
-Proof
-  rw [] >>
-  `P (el ((n - 1 - x - length (dropWhile P (reverse (take n l))))) (reverse (take n l)))`
-  by (irule dropWhile_prop >> simp [LENGTH_REVERSE]) >>
-  rfs [EL_REVERSE, EL_TAKE, PRE_SUB1]
-QED
-
-Theorem take_replicate:
-  ∀m n x. take m (replicate n x) = replicate (min m n) x
-Proof
-  Induct_on `n` >> rw [TAKE_def, MIN_DEF] >> fs [] >>
-  Cases_on `m` >> rw []
-QED
-
-Theorem length_take_less_eq:
-  ∀n l. length (take n l) ≤ n
-Proof
-  Induct_on `l` >> rw [TAKE_def] >>
-  Cases_on `n` >> fs []
-QED
-
-Theorem flat_drop:
-  ∀n m ls. flat (drop m ls) = drop (length (flat (take m ls))) (flat ls)
-Proof
-  Induct_on `ls` >> rw [DROP_def, DROP_APPEND] >>
-  irule (GSYM DROP_LENGTH_TOO_LONG) >> simp []
-QED
-
-Theorem take_is_prefix:
-  ∀n l. take n l ≼ l
-Proof
-  Induct_on `l` >> rw [TAKE_def]
-QED
-
-Theorem sum_prefix:
-  ∀l1 l2. l1 ≼ l2 ⇒ sum l1 ≤ sum l2
-Proof
-  Induct >> rw [] >> Cases_on `l2` >> fs []
-QED
-
-Theorem flookup_fdiff:
-  ∀m s k.
-    flookup (fdiff m s) k =
-      if k ∈ s then None else flookup m k
-Proof
-  rw [FDIFF_def, FLOOKUP_DRESTRICT] >> fs []
-QED
-
-(* ----- Theorems about log ----- *)
-
-(* Could be upstreamed to HOL *)
-Theorem mul_div_bound:
-  ∀m n. n ≠ 0 ⇒ m - (n - 1) ≤ n * (m DIV n) ∧ n * (m DIV n) ≤ m
-Proof
-  rw [] >>
-  `0 < n` by decide_tac >>
-  drule DIVISION >> disch_then (qspec_then `m` mp_tac) >>
-  decide_tac
-QED
-
-Theorem exp_log_bound:
-  ∀b n. 1 < b ∧ n ≠ 0 ⇒ n DIV b + 1 ≤ b ** (log b n) ∧ b ** (log b n) ≤ n
-Proof
-  rw [] >> `0 < n` by decide_tac >>
-  drule LOG >> disch_then drule >> rw [] >>
-  fs [ADD1, EXP_ADD] >>
-  simp [DECIDE ``∀x y. x + 1 ≤ y ⇔ x < y``] >>
-  `∃x. b = Suc x` by intLib.COOPER_TAC >>
-  `b * (n DIV b) < b * b ** log b n` suffices_by metis_tac [LESS_MULT_MONO] >>
-  pop_assum kall_tac >>
-  `b ≠ 0` by decide_tac >>
-  drule mul_div_bound >> disch_then (qspec_then `n` mp_tac) >>
-  decide_tac
-QED
-
-Theorem log_base_power:
-  ∀n b. 1 < b ⇒ log b (b ** n) = n
-Proof
-  Induct >> rw [EXP, LOG_1] >>
-  Cases_on `n` >> rw [LOG_BASE] >>
-  first_x_assum drule >> rw [] >>
-  simp [Once EXP, LOG_MULT]
-QED
-
-Theorem log_change_base_power:
-  ∀m n b. 1 < b ∧ m ≠ 0 ∧ n ≠ 0 ⇒ log (b ** n) m = log b m DIV n
-Proof
-  rw [] >> irule LOG_UNIQUE >>
-  rw [ADD1, EXP_MUL, LEFT_ADD_DISTRIB] >>
-  qmatch_goalsub_abbrev_tac `x DIV _` >>
-  drule mul_div_bound >> disch_then (qspec_then `x` mp_tac) >> rw []
-  >- (
-    irule LESS_LESS_EQ_TRANS >>
-    qexists_tac `b ** (x+1)` >> rw [] >>
-    unabbrev_all_tac >>
-    simp [EXP_ADD] >>
-    `b * (m DIV b + 1) ≤ b * b ** log b m`
-    by metis_tac [exp_log_bound, LESS_MONO_MULT, MULT_COMM] >>
-    `m < b * (m DIV b + 1)` suffices_by decide_tac >>
-    simp [LEFT_ADD_DISTRIB] >>
-    `b ≠ 0` by decide_tac >>
-    `m - (b - 1) ≤ b * (m DIV b)` by metis_tac [mul_div_bound] >>
-    fs [])
-  >- (
-    irule LESS_EQ_TRANS >>
-    qexists_tac `b ** (log b m)` >> rw [] >>
-    unabbrev_all_tac >>
-    metis_tac [exp_log_bound])
-QED
-
-(* ----- Theorems about word stuff ----- *)
-
-Theorem l2n_padding:
-  ∀ws n. l2n 256 (ws ++ map w2n (replicate n 0w)) = l2n 256 ws
-Proof
-  Induct >> rw [l2n_def] >>
-  Induct_on `n` >> rw [l2n_def]
-QED
-
-Theorem l2n_0:
-  ∀l b. b ≠ 0 ∧ every ($> b)  l⇒ (l2n b l = 0 ⇔ every ($= 0) l)
-Proof
-  Induct >> rw [l2n_def] >>
-  eq_tac >> rw []
-QED
-
-Theorem mod_n2l:
-  ∀d n. 0 < d ⇒ map (\x. x MOD d) (n2l d n) = n2l d n
-Proof
-  rw [] >> drule n2l_BOUND >> disch_then (qspec_then `n` mp_tac) >>
-  qspec_tac (`n2l d n`, `l`) >>
-  Induct >> rw []
-QED
-
 (* ----- Theorems about converting between values and byte lists ----- *)
 
-Theorem le_write_w_length:
-  ∀l x. length (le_write_w l w) = l
+Theorem value_type_is_fc:
+  ∀t v. value_type t v ⇒ first_class_type t
 Proof
-  rw [le_write_w_def]
+  ho_match_mp_tac value_type_ind >> rw [first_class_type_def] >>
+  fs [LIST_REL_EL_EQN, EVERY_EL]
 QED
 
-Theorem v2b_size:
-  ∀t v. value_type t v ⇒ length (value_to_bytes v) = sizeof t
+Theorem sizeof_type_to_shape:
+  ∀t. first_class_type t ⇒ sizeof (type_to_shape t) = sizeof t
 Proof
-  ho_match_mp_tac value_type_ind >>
-  rw [value_to_bytes_def, sizeof_def]
-  >- metis_tac [le_write_w_length]
-  >- metis_tac [le_write_w_length]
-  >- metis_tac [le_write_w_length]
-  >- (Induct_on `vs` >> rw [ADD1] >> fs [])
-  >- (
-    pop_assum mp_tac >>
-    qid_spec_tac `vs` >> qid_spec_tac `ts` >>
-    ho_match_mp_tac LIST_REL_ind >> rw [])
+  recInduct type_to_shape_ind >>
+  rw [type_to_shape_def, memory_modelTheory.sizeof_def, llvmTheory.sizeof_def,
+      first_class_type_def, EVERY_MEM] >>
+    qid_spec_tac `vs` >> Induct_on `ts` >> rw [] >> fs []
 QED
 
-Theorem b2v_size:
-  (∀t bs. first_class_type t ∧ sizeof t ≤ length bs ⇒
-    ∃v. bytes_to_value t bs = (v, drop (sizeof t) bs)) ∧
-  (∀n t bs. first_class_type t ∧ n * sizeof t ≤ length bs ⇒
-    ∃vs. read_array n t bs = (vs, drop (n * sizeof t) bs)) ∧
-  (∀ts bs. every first_class_type ts ∧ sum (map sizeof ts) ≤ length bs ⇒
-    ∃vs. read_str ts bs = (vs, drop (sum (map sizeof ts)) bs))
+Theorem value_type_to_shape:
+  ∀t v.
+    value_type t v ⇒
+    ∀s.
+    value_shape (\n t x. n = fst (unconvert_value x) ∧ value_type t (FlatV x)) (type_to_shape t) v
 Proof
-  ho_match_mp_tac bytes_to_value_ind >>
-  rw [sizeof_def, bytes_to_value_def, le_read_w_def] >>
-  fs [first_class_type_def]
-  >- (simp [PAIR_MAP] >> metis_tac [SND])
-  >- (
-    pairarg_tac >> rw [] >> pairarg_tac >> rw [] >>
-    fs [ADD1] >> rw [] >> fs [DROP_DROP_T, LEFT_ADD_DISTRIB])
-  >- fs [DROP_DROP_T, LEFT_ADD_DISTRIB]
+  ho_match_mp_tac value_type_ind >>
+  rw [memory_modelTheory.sizeof_def, llvmTheory.sizeof_def, type_to_shape_def,
+      unconvert_value_def, value_shape_def] >>
+  fs [value_shapes_list_rel, LIST_REL_CONJ, ETA_THM, EVERY2_MAP] >>
+  metis_tac [value_type_rules]
 QED
 
-Theorem b2v_smaller:
-   ∀t bs. first_class_type t ∧ sizeof t ≤ length bs ⇒
-    length (snd (bytes_to_value t bs)) = length bs - sizeof t
+Theorem llvm_v2b_size:
+  ∀t v. value_type t v ⇒ length (llvm_value_to_bytes v) = sizeof t
 Proof
-  rw [] >> imp_res_tac b2v_size >>
-  Cases_on `bytes_to_value t bs` >> fs []
+  rw [llvm_value_to_bytes_def] >>
+  drule value_type_to_shape >> rw [] >>
+  drule value_type_is_fc >> rw [] >>
+  drule sizeof_type_to_shape >>
+  disch_then (mp_tac o GSYM) >> rw [] >>
+  irule v2b_size >> rw [] >>
+  qmatch_assum_abbrev_tac `value_shape f _ _` >>
+  qexists_tac `f` >> rw [] >>
+  unabbrev_all_tac >> fs []
 QED
 
-Theorem b2v_append:
-  (∀t bs. first_class_type t ∧ sizeof t ≤ length bs ⇒
-    bytes_to_value t (bs ++ bs') = (I ## (λx. x ++ bs')) (bytes_to_value t bs)) ∧
-  (∀n t bs. first_class_type t ∧ n * sizeof t ≤ length bs ⇒
-    ∃vs. read_array n t (bs ++ bs') = (I ## (λx. x ++ bs')) (read_array n t bs)) ∧
-  (∀ts bs. every first_class_type ts ∧ sum (map sizeof ts) ≤ length bs ⇒
-    ∃vs. read_str ts (bs ++ bs') = (I ## (λx. x ++ bs')) (read_str ts bs))
+Theorem b2llvm_v_size:
+  ∀t bs. first_class_type t ∧ sizeof t ≤ length bs ⇒
+    ∃v. bytes_to_llvm_value t bs = (v, drop (sizeof t) bs)
 Proof
-  ho_match_mp_tac bytes_to_value_ind >>
-  rw [sizeof_def, bytes_to_value_def, le_read_w_def] >>
-  fs [first_class_type_def, TAKE_APPEND, DROP_APPEND,
-      DECIDE ``!x y. x ≤ y ⇒ x - y = 0n``, ETA_THM]
-  >- (simp [PAIR_MAP] >> metis_tac [SND])
-  >- (simp [PAIR_MAP] >> metis_tac [SND])
-  >- (
-    rpt (pairarg_tac >> simp []) >> fs [ADD1] >>
-    BasicProvers.VAR_EQ_TAC >> fs [LEFT_ADD_DISTRIB] >>
-    first_x_assum irule >>
-    `sizeof t ≤ length bs` by decide_tac >>
-    imp_res_tac b2v_smaller >> rfs [])
-  >- (
-    rpt (pairarg_tac >> simp []) >> fs [ADD1] >>
-    BasicProvers.VAR_EQ_TAC >> fs [LEFT_ADD_DISTRIB] >>
-    first_x_assum irule >>
-    `sizeof t ≤ length bs` by decide_tac >>
-    imp_res_tac b2v_smaller >> rfs [])
+  rw [bytes_to_llvm_value_def] >>
+  drule sizeof_type_to_shape >> disch_then (mp_tac o GSYM) >> rw [] >>
+  fs [PAIR_MAP] >>
+  metis_tac [SND, b2v_size]
 QED
 
-Theorem le_read_write:
-  ∀n w bs.
-    n ≠ 0 ∧ dimword (:'a) ≤ 256 ** n ⇒ le_read_w n (le_write_w n (w :'a word) ⧺ bs) = (w, bs)
+Theorem b2llvm_v_smaller:
+   ∀t bs. first_class_type t ∧ sizeof t ≤ length bs ⇒
+    length (snd (bytes_to_llvm_value t bs)) = length bs - sizeof t
 Proof
-  rw [le_read_w_def, le_write_w_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] >>
-    simp [MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF, mod_n2l] >>
-    rename1 `n2l 256 m` >>
-    `length (n2l 256 m) ≤ n`
-    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 [] >>
-      drule LOG2_w2n_lt >> 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 (2 ** dimindex (:'a)) ≤ LOG 2 (256 ** n)` by simp [LOG_LE_MONO] >>
-      pop_assum mp_tac >>
-      `256 = 2 ** 8` by EVAL_TAC >>
-      ASM_REWRITE_TAC [EXP_MUL] >> simp [log_base_power]) >>
-    simp [mod_n2l, l2n_n2l, TAKE_LENGTH_TOO_LONG])
-  >- metis_tac [le_write_w_length, DROP_LENGTH_APPEND]
+  rw [bytes_to_llvm_value_def] >>
+  metis_tac [b2v_smaller, sizeof_type_to_shape]
 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')
-    ⇒
-    le_write_w n w ++ bs' = bs
+Theorem b2llvm_v_append:
+  ∀t bs bs'. first_class_type t ∧ sizeof t ≤ length bs ⇒
+    bytes_to_llvm_value t (bs ++ bs') = (I ## (λx. x ++ bs')) (bytes_to_llvm_value t 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`
-  by (
-    `n ≤ 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 [] >>
-    rpt (pop_assum kall_tac) >>
-    Induct_on `bs` >> rw [] >>
-    Cases_on `h` >> fs []) >>
-  rw [n2l_l2n]
-  >- (
-    rw [TAKE_def, take_replicate] >>
-    Cases_on `n` >> fs [] >>
-    rfs [l2n_0] >> unabbrev_all_tac >> fs [EVERY_MAP] >>
-    ONCE_REWRITE_TAC [GSYM REPLICATE] >>
-    qmatch_goalsub_abbrev_tac `take n _` >>
-    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 [] >>
-    Cases_on `bs` >> rw [] >> fs [] >>
-    Cases_on `h` >> fs [] >>
-    first_x_assum irule >> rw [] >>
-    irule MONO_EVERY >>
-    qexists_tac `(λx. 0 = w2n x)` >> rw []) >>
-  fs [MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF] >>
-  `exists (\y. 0 ≠ y) l`
-  by (
-    fs [l2n_eq_0, combinTheory.o_DEF] >> fs [EXISTS_MEM, EVERY_MEM] >>
-    qexists_tac `x` >> rfs [MOD_MOD, GREATER_DEF]) >>
-  simp [LOG_l2n_dropWhile] >>
-  `length (dropWhile ($= 0) (reverse l)) ≠ 0`
-  by (
-    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`
-  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`
-  by metis_tac [LESS_EQ_TRANS, LENGTH_dropWhile_LESS_EQ, LENGTH_REVERSE] >>
-  rw [MIN_DEF] >> fs []
-  >- (
-    simp [TAKE_APPEND, TAKE_TAKE_MIN, MIN_DEF, take_replicate] >>
-    `replicate (length l − length (dropWhile ($= 0) (reverse l))) 0w =
-     take (length l − (length (dropWhile ($= 0) (reverse l)))) (drop (length (dropWhile ($= 0) (reverse l))) bs)`
-    suffices_by (rw [] >> irule take_drop_partition >> simp []) >>
-    rw [LIST_EQ_REWRITE, EL_REPLICATE, EL_TAKE, EL_DROP] >>
-   `length (dropWhile ($= 0) (reverse l)) =
-     length (dropWhile (λx. 0 = w2n x) (reverse (take (length l) bs)))`
-    by (
-      `reverse l = reverse (take (length l) (map w2n bs))` by metis_tac [] >>
-      ONCE_ASM_REWRITE_TAC [] >>
-      qpat_x_assum `Abbrev (l = _)` kall_tac >>
-      simp [GSYM MAP_TAKE, GSYM MAP_REVERSE, dropWhile_map, combinTheory.o_DEF]) >>
-    fs [] >>
-    `x + length (dropWhile (λx. 0 = w2n x) (reverse (take (length l) bs))) < length l` by decide_tac >>
-    drule (SIMP_RULE std_ss [LET_THM] dropWhile_rev_take) >>
-    rw [] >>
-    REWRITE_TAC [GSYM w2n_11, word_0_n2w] >>
-    simp [])
-  >- rw [TAKE_APPEND, TAKE_TAKE]
+  rw [bytes_to_llvm_value_def] >>
+  drule sizeof_type_to_shape >> disch_then (mp_tac o GSYM) >> rw [] >> fs [] >>
+  rw [PAIR_MAP, b2v_append]
 QED
 
-Theorem b2v_v2b:
-  ∀v t bs. value_type t v ⇒ bytes_to_value t (value_to_bytes v ++ bs) = (v, bs)
+Theorem b2v_llvm_v2b:
+  ∀v t bs. value_type t v ⇒ bytes_to_llvm_value t (llvm_value_to_bytes v ++ bs) = (v, bs)
 Proof
-  gen_tac >> completeInduct_on `v_size v` >>
-  rw [] >>
-  pop_assum mp_tac >> simp [value_type_cases] >>
-  rw [] >>
-  rw [bytes_to_value_def, value_to_bytes_def, le_read_write]
-  >- wordsLib.WORD_DECIDE_TAC
-  >- (
-    qmatch_abbrev_tac `_ x = _` >>
-    `x = (vs, bs)` suffices_by (simp [PAIR_MAP] >> metis_tac [PAIR_EQ, FST, SND]) >>
-    unabbrev_all_tac >>
-    qid_spec_tac `bs` >> Induct_on `vs` >> simp [bytes_to_value_def] >>
-    rw [] >> fs [v_size_def] >>
-    pairarg_tac >> fs [] >>
-    pairarg_tac >> fs [] >>
-    rename1 `value_type t v1` >>
-    first_x_assum (qspec_then `v_size v1` mp_tac) >> simp [] >>
-    disch_then (qspec_then `v1` mp_tac) >> simp [] >>
-    disch_then (qspec_then `t` mp_tac) >> simp [] >>
-    qmatch_assum_abbrev_tac `bytes_to_value _ (_ ++ bs1 ++ _) = _` >>
-    disch_then (qspec_then `bs1++bs` mp_tac) >> simp [] >>
-    unabbrev_all_tac >> strip_tac >> fs [] >>
-    first_x_assum (qspec_then `bs` mp_tac) >> rw [])
-  >- (
-    qmatch_abbrev_tac `_ x = _` >>
-    `x = (vs, bs)` suffices_by (simp [PAIR_MAP] >> metis_tac [PAIR_EQ, FST, SND]) >>
-    unabbrev_all_tac >>
-    pop_assum mp_tac >>
-    qid_spec_tac `bs` >> qid_spec_tac `ts` >> Induct_on `vs` >> simp [bytes_to_value_def] >>
-    rw [] >> fs [v_size_def, bytes_to_value_def] >>
-    pairarg_tac >> fs [] >>
-    pairarg_tac >> fs [] >>
-    rename1 `value_type t v1` >>
-    first_x_assum (qspec_then `v_size v1` mp_tac) >> simp [] >>
-    disch_then (qspec_then `v1` mp_tac) >> simp [] >>
-    disch_then (qspec_then `t` mp_tac) >> simp [] >>
-    qmatch_assum_abbrev_tac `bytes_to_value _ (_ ++ bs1 ++ _) = _` >>
-    disch_then (qspec_then `bs1++bs` mp_tac) >> simp [] >>
-    unabbrev_all_tac >> strip_tac >> fs [] >>
-    first_x_assum drule >> metis_tac [PAIR_EQ])
+  rw [bytes_to_llvm_value_def, llvm_value_to_bytes_def] >>
+  drule value_type_to_shape >> rw [] >>
+  qmatch_assum_abbrev_tac `value_shape f _ _` >>
+  irule b2v_v2b >>
+  qexists_tac `f` >> rw [] >>
+  unabbrev_all_tac >> fs [] >>
+  fs [unconvert_value_def, convert_value_def, value_type_cases] >>
+  wordsLib.WORD_DECIDE_TAC
 QED
 
 (* ----- Theorems about insert/extract value and get_offset ----- *)
@@ -482,7 +184,7 @@ Theorem offset_size_leq:
     ⇒
     n ≤ sizeof t
 Proof
-  recInduct get_offset_ind >> rw [get_offset_def, sizeof_def, indices_in_range_def] >>
+  recInduct get_offset_ind >> rw [get_offset_def, llvmTheory.sizeof_def, indices_in_range_def] >>
   BasicProvers.EVERY_CASE_TAC >> fs [] >> rw [] >> rfs []
   >- (
     `x + i * sizeof t ≤ (i + 1) * sizeof t` by decide_tac >>
@@ -495,13 +197,6 @@ Proof
   drule sum_prefix >> rw [SUM_APPEND]
 QED
 
-Theorem value_type_is_fc:
-  ∀t v. value_type t v ⇒ first_class_type t
-Proof
-  ho_match_mp_tac value_type_ind >> rw [first_class_type_def] >>
-  fs [LIST_REL_EL_EQN, EVERY_EL]
-QED
-
 Theorem extract_type_fc:
   ∀t is t'. extract_type t is = Some t' ∧ first_class_type t ⇒ first_class_type t'
 Proof
@@ -517,7 +212,7 @@ Theorem extract_offset_size:
     sizeof t' ≤ sizeof t - n
 Proof
   recInduct get_offset_ind >> rw [get_offset_def, extract_type_def] >>
-  BasicProvers.EVERY_CASE_TAC >> fs [sizeof_def] >> rfs [] >> rw [ETA_THM]
+  BasicProvers.EVERY_CASE_TAC >> fs [llvmTheory.sizeof_def] >> rfs [] >> rw [ETA_THM]
   >- (
     `sizeof t ≤ (v1  − i) * sizeof t` suffices_by decide_tac  >>
     `1 ≤ v1 - i` by decide_tac >>
@@ -529,6 +224,12 @@ Proof
   Induct_on `ts` >> rw [TAKE_def, EL_CONS, PRE_SUB1]
 QED
 
+Theorem llvm_value_to_bytes_agg:
+  ∀vs. llvm_value_to_bytes (AggV vs) = flat (map llvm_value_to_bytes vs)
+Proof
+  Induct >> rw [] >> fs [llvm_value_to_bytes_def, value_to_bytes_def]
+QED
+
 Theorem read_from_offset_extract:
   ∀t indices n v t'.
     indices_in_range t indices ∧
@@ -536,55 +237,55 @@ Theorem read_from_offset_extract:
     value_type t v ∧
     extract_type t indices = Some t'
     ⇒
-    extract_value v indices = Some (fst (bytes_to_value t' (drop n (value_to_bytes v))))
+    extract_value v indices = Some (fst (bytes_to_llvm_value t' (drop n (llvm_value_to_bytes v))))
 Proof
   recInduct get_offset_ind >>
   rw [extract_value_def, get_offset_def, extract_type_def, indices_in_range_def] >>
   simp [DROP_0]
-  >- metis_tac [APPEND_NIL, FST, b2v_v2b] >>
+  >- metis_tac [APPEND_NIL, FST, b2v_llvm_v2b] >>
   qpat_x_assum `value_type _ _` mp_tac >>
   simp [Once value_type_cases] >> rw [] >> simp [extract_value_def] >>
   qpat_x_assum `_ = Some n` mp_tac >> CASE_TAC >> rw [] >> rfs [] >>
-  simp [value_to_bytes_def]
+  simp [llvm_value_to_bytes_agg]
   >- (
     `value_type t (el i vs)` by metis_tac [EVERY_EL] >>
     first_x_assum drule >>
     rw [] >> simp [GSYM DROP_DROP_T, ETA_THM] >>
-    `i * sizeof t = length (flat (take i (map value_to_bytes vs)))`
+    `i * sizeof t = length (flat (take i (map llvm_value_to_bytes vs)))`
     by (
       simp [LENGTH_FLAT, MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF] >>
-      `map (λx. length (value_to_bytes x)) vs = replicate (length vs) (sizeof t)`
+      `map (λx. length (llvm_value_to_bytes x)) vs = replicate (length vs) (sizeof t)`
       by (
         qpat_x_assum `every _ _` mp_tac >> rpt (pop_assum kall_tac) >>
-        Induct_on `vs` >> rw [v2b_size]) >>
+        Induct_on `vs` >> rw [llvm_v2b_size]) >>
       rw [take_replicate, MIN_DEF]) >>
     rw [GSYM flat_drop, GSYM MAP_DROP] >>
     drule DROP_CONS_EL >> simp [DROP_APPEND] >> disch_then kall_tac >>
     `first_class_type t'` by metis_tac [value_type_is_fc, extract_type_fc] >>
-    `sizeof t' ≤ length (drop x (value_to_bytes (el i vs)))`
-    by (simp [LENGTH_DROP] >> drule v2b_size >> rw [] >> metis_tac [extract_offset_size]) >>
-    simp [b2v_append])
+    `sizeof t' ≤ length (drop x (llvm_value_to_bytes (el i vs)))`
+    by (simp [LENGTH_DROP] >> drule llvm_v2b_size >> rw [] >> metis_tac [extract_offset_size]) >>
+    simp [b2llvm_v_append])
   >- metis_tac [LIST_REL_LENGTH]
   >- (
     `value_type (el i ts) (el i vs)` by metis_tac [LIST_REL_EL_EQN] >>
     first_x_assum drule >>
     rw [] >> simp [GSYM DROP_DROP_T, ETA_THM] >>
-    `sum (map sizeof (take i ts)) = length (flat (take i (map value_to_bytes vs)))`
+    `sum (map sizeof (take i ts)) = length (flat (take i (map llvm_value_to_bytes vs)))`
     by (
       simp [LENGTH_FLAT, MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF] >>
-      `map sizeof ts = map (\x. length (value_to_bytes x)) vs`
+      `map sizeof ts = map (\x. length (llvm_value_to_bytes x)) vs`
       by (
         qpat_x_assum `list_rel _ _ _` mp_tac >> rpt (pop_assum kall_tac) >>
         qid_spec_tac `ts` >>
-        Induct_on `vs` >> rw [] >> rw [v2b_size]) >>
+        Induct_on `vs` >> rw [] >> rw [llvm_v2b_size]) >>
       rw []) >>
     rw [GSYM flat_drop, GSYM MAP_DROP] >>
     `i < length vs` by metis_tac [LIST_REL_LENGTH] >>
     drule DROP_CONS_EL >> simp [DROP_APPEND] >> disch_then kall_tac >>
     `first_class_type t'` by metis_tac [value_type_is_fc, extract_type_fc] >>
-    `sizeof t' ≤ length (drop x (value_to_bytes (el i vs)))`
-    by (simp [LENGTH_DROP] >> drule v2b_size >> rw [] >> metis_tac [extract_offset_size]) >>
-    simp [b2v_append])
+    `sizeof t' ≤ length (drop x (llvm_value_to_bytes (el i vs)))`
+    by (simp [LENGTH_DROP] >> drule llvm_v2b_size >> rw [] >> metis_tac [extract_offset_size]) >>
+    simp [b2llvm_v_append])
 QED
 
 (* ----- Theorems about the step function ----- *)
@@ -615,53 +316,28 @@ Proof
       globals_ok_def, stack_ok_def, heap_ok_def, EVERY_EL, frame_ok_def]
 QED
 
-Theorem flookup_set_bytes:
-  ∀poison bytes n h n'.
-    flookup (set_bytes poison bytes n h) (A n') =
-      if n ≤ n' ∧ n' < n + length bytes then
-        Some (poison, el (n' - n) bytes)
-      else
-        flookup h (A n')
-Proof
-  Induct_on `bytes` >> rw [set_bytes_def, EL_CONS, PRE_SUB1] >>
-  fs [ADD1, FLOOKUP_UPDATE] >>
-  `n = n'` by decide_tac >>
-  rw []
-QED
-
 Theorem allocate_invariant:
-  ∀p s1 v1 t v2 s2.
-    state_invariant p s1 ∧ allocate s1 v1 t (v2,s2) ⇒ state_invariant p s2
+  ∀p s1 v1 t v2 h2.
+    state_invariant p s1 ∧ allocate s1.heap v1 t (v2,h2) ⇒ state_invariant p (s1 with heap := h2)
 Proof
-  rw [allocate_cases, state_invariant_def, ip_ok_def, heap_ok_def,
-      globals_ok_def, stack_ok_def] >>
-  rw [] >> fs []
+  rw [state_invariant_def, ip_ok_def, globals_ok_def, stack_ok_def]
+  >- metis_tac [allocate_heap_ok]
+  >- (fs [is_allocated_def] >> metis_tac [allocate_unchanged, SUBSET_DEF])
   >- (
-    fs [allocations_ok_def] >> rpt gen_tac >> disch_tac >> fs [is_free_def] >> rw [] >>
-    metis_tac [INTER_COMM])
-  >- (
-    rw [flookup_set_bytes]
-    >- rw [RIGHT_AND_OVER_OR, EXISTS_OR_THM, interval_to_set_def] >>
-    eq_tac >> rw [] >> fs [interval_to_set_def] >>
-    metis_tac [])
-  >- (fs [is_allocated_def] >> metis_tac [])
-  >- (fs [EVERY_EL, frame_ok_def] >> rw [] >> metis_tac [])
+    fs [EVERY_EL, frame_ok_def, allocate_unchanged] >> rw [] >>
+    metis_tac [allocate_unchanged, SUBSET_DEF])
 QED
 
 Theorem set_bytes_invariant:
   ∀s poison bytes n prog b.
-    state_invariant prog s ∧ is_allocated (b, n, n + length bytes) s.allocations
+    state_invariant prog s ∧ is_allocated (Interval b n (n + length bytes)) s.heap
     ⇒
     state_invariant prog (s with heap := set_bytes poison bytes n s.heap)
 Proof
   rw [state_invariant_def]
-  >- (fs [allocations_ok_def] >> rw [] >> metis_tac [])
-  >- (
-    fs [heap_ok_def, flookup_set_bytes] >> rw [] >>
-    fs [is_allocated_def, interval_to_set_def, SUBSET_DEF] >>
-    metis_tac [LESS_EQ_REFL, DECIDE ``!x y. x < x + SUC y``])
-  >- (fs [globals_ok_def] >> metis_tac [])
-  >- (fs [stack_ok_def, EVERY_EL, frame_ok_def])
+  >- metis_tac [set_bytes_heap_ok]
+  >- (fs [globals_ok_def, is_allocated_def, set_bytes_unchanged] >> metis_tac [])
+  >- (fs [stack_ok_def, EVERY_EL, frame_ok_def, set_bytes_unchanged])
 QED
 
 Theorem step_instr_invariant:
@@ -676,8 +352,10 @@ Proof
     >- (
       fs [stack_ok_def] >> rfs [EVERY_EL, frame_ok_def] >>
       first_x_assum (qspec_then `0` mp_tac) >> simp [])
-    >- (fs [deallocate_def, allocations_ok_def] >> rw [] >> metis_tac [])
     >- (
+      fs [heap_ok_def, deallocate_def, allocations_ok_def] >> rw []
+      >- metis_tac []
+      >- metis_tac [] >>
       fs [deallocate_def, heap_ok_def] >> rw [flookup_fdiff] >>
       eq_tac >> rw []
       >- metis_tac [optionTheory.NOT_IS_SOME_EQ_NONE]
@@ -686,7 +364,7 @@ Proof
     >- (
       fs [globals_ok_def, deallocate_def] >> rw [] >>
       first_x_assum drule >> rw [] >> fs [is_allocated_def] >>
-      qexists_tac `b2` >> rw [] >> CCONTR_TAC >> fs [])
+      qexists_tac `b2` >> rw [] >> CCONTR_TAC >> fs [interval_freeable_def])
     >- (
       fs [stack_ok_def, EVERY_MEM, frame_ok_def, deallocate_def] >> rfs [] >>
       rw []
@@ -702,8 +380,6 @@ Proof
       rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >>
       qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >>
       last_x_assum drule >> disch_then drule >> fs [])
-    >- (fs [allocations_ok_def] >> metis_tac [])
-    >- (fs [heap_ok_def] >> metis_tac [])
     >- (fs [globals_ok_def] >> metis_tac [])
     >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
   >- ( (* Br *)
@@ -712,8 +388,6 @@ Proof
       rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >>
       qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >>
       last_x_assum drule >> disch_then drule >> fs [])
-    >- (fs [allocations_ok_def] >> metis_tac [])
-    >- (fs [heap_ok_def] >> metis_tac [])
     >- (fs [globals_ok_def] >> metis_tac [])
     >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
   >- (
@@ -752,7 +426,6 @@ Proof
   >- ( (* Call *)
     rw [state_invariant_def]
     >- (fs [prog_ok_def, ip_ok_def] >> metis_tac [NOT_NIL_EQ_LENGTH_NOT_0])
-    >- (fs [state_invariant_def, allocations_ok_def] >> metis_tac [])
     >- (fs [state_invariant_def, heap_ok_def] >> metis_tac [])
     >- (fs [state_invariant_def, globals_ok_def] >> metis_tac [])
     >- (
diff --git a/sledge/semantics/llvm_to_llairScript.sml b/sledge/semantics/llvm_to_llairScript.sml
index e007dcc1b..f16294d77 100644
--- a/sledge/semantics/llvm_to_llairScript.sml
+++ b/sledge/semantics/llvm_to_llairScript.sml
@@ -344,7 +344,7 @@ Definition generate_move_blocks_list_def:
       (used_names, new_blocks :: new_blocks2))
 End
 
-(* Givel an association list of labels and phi-block pairs, remove the phi's,
+(* Given an association list of labels and phi-block pairs, remove the phi's,
  * by generating an extra block along each control flow edge that does the move
  * corresponding to the relevant phis. *)
 Definition remove_phis_def:
diff --git a/sledge/semantics/memory_modelScript.sml b/sledge/semantics/memory_modelScript.sml
new file mode 100644
index 000000000..af9f49f69
--- /dev/null
+++ b/sledge/semantics/memory_modelScript.sml
@@ -0,0 +1,570 @@
+(*
+ * 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.
+ *)
+
+(* A simple, concrete memory model where the heap is an array of bytes. This is
+ * how llair views memory, and how we give semantics to llvm. Although LLVM's
+ * real memory model is still a subject of research, this is mostly to do with
+ * enabling the right collection of compiler optimisations. Since we only want to
+ * think about LLVM semantics after optimisation, the concrete model is likely to
+ * be sufficient. *)
+
+open HolKernel boolLib bossLib Parse;
+open arithmeticTheory listTheory rich_listTheory pairTheory;
+open logrootTheory numposrepTheory wordsTheory pred_setTheory finite_mapTheory;
+open settingsTheory miscTheory;
+
+new_theory "memory_model";
+
+numLib.prefer_num ();
+
+(* Heap addresses *)
+Datatype:
+  addr = A num
+End
+
+(* Values that fit in registers *)
+Datatype:
+  reg_v =
+  | FlatV 'a
+  | AggV (reg_v list)
+End
+
+(* An interval of allocated memory.
+ * Args: whether it's freeable, the starting address (inclusive), and the ending address
+ * (exclusive)
+ *)
+Datatype:
+  interval = Interval bool num num
+End
+
+Datatype:
+  heap = <| memory : addr |-> 'a # word8;
+            allocations : interval set;
+            valid_addresses : addr set|>
+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
+ *)
+Datatype:
+  shape =
+  | Flat num 'a
+  | Array shape num
+  | Tuple (shape list)
+End
+
+(* Does a value have a given shape. The function argument answers the question
+ * for flat values/shapes.
+ * We use mutual recursion instead of list_rel to work around a HOL bug. *)
+Definition value_shape_def:
+  (value_shape f (Flat n t) (FlatV x) ⇔ f n t x) ∧
+  (value_shape f (Array s n) (AggV vs) ⇔
+    every (value_shape f s) vs ∧ length vs = n) ∧
+  (value_shape f (Tuple ss) (AggV vs) ⇔
+    value_shapes f ss vs) ∧
+  (value_shape _ _ _ ⇔ F) ∧
+  (value_shapes f [] [] ⇔ T) ∧
+  (value_shapes f (s::ss) (v::vs) ⇔
+    value_shape f s v ∧ value_shapes f ss vs) ∧
+  (value_shapes _ _ _ ⇔ F)
+Termination
+  WF_REL_TAC `measure (\x. case x of | INL (_, x, _) => shape_size (\x.0) x | INR (_, y, _) => shape1_size (\x.0) y)`
+End
+
+Theorem value_shapes_list_rel:
+  ∀f ss vs. value_shapes f ss vs ⇔ list_rel (value_shape f) ss vs
+Proof
+  Induct_on `ss` >> Cases_on `vs` >> rw [value_shape_def]
+QED
+
+Theorem value_shape_cases:
+  ∀f s v.
+    value_shape f s v ⇔
+      (∃n t x. s = Flat n t ∧ v = FlatV x ∧ f n t x) ∨
+      (∃s2 n vs. s = Array s2 n ∧ v = AggV vs ∧
+        every (value_shape f s2) vs ∧ length vs = n) ∨
+      (∃ss vs. s = Tuple ss ∧ v = AggV vs ∧ value_shapes f ss vs)
+Proof
+  rw [] >>
+  Cases_on `s` >> Cases_on `v` >> rw [value_shape_def] >> metis_tac []
+QED
+
+Definition sizeof_def:
+  (sizeof (Flat n t) = n) ∧
+  (sizeof (Array s n) = n * sizeof s) ∧
+  (sizeof (Tuple ss) = sum (map sizeof ss))
+Termination
+  WF_REL_TAC `measure (shape_size (\x.0))` >> rw [] >>
+  Induct_on `ss` >> rw [definition "shape_size_def"] >>
+  res_tac >> decide_tac
+End
+
+Definition interval_to_set_def:
+  interval_to_set (Interval _ start stop) =
+    { n | start ≤ n ∧ n < stop }
+End
+
+Definition interval_ok_def:
+  interval_ok (Interval b i1 i2) valid_addresses ⇔
+    i1 ≤ i2 ∧ image A (interval_to_set (Interval b i1 i2)) ⊆ valid_addresses
+End
+
+Definition interval_freeable_def:
+  interval_freeable (Interval b _ _) ⇔ b
+End
+
+Definition is_allocated_def:
+  is_allocated b1 h ⇔
+    interval_ok b1 h.valid_addresses ∧
+    ∃b2. b2 ∈ h.allocations ∧ (interval_freeable b1 ⇔ interval_freeable b2) ∧
+         interval_to_set b1 ⊆ interval_to_set b2
+End
+
+Definition is_free_def:
+  is_free b1 h ⇔
+    interval_ok b1 h.valid_addresses ∧
+    ∀b2. b2 ∈ h.allocations ⇒ interval_to_set b1 ∩ interval_to_set b2 = ∅
+End
+
+(* The allocations are of intervals that don't overlap *)
+Definition allocations_ok_def:
+  allocations_ok h ⇔
+    ∀i1 i2.
+      i1 ∈ h.allocations ∧ i2 ∈ h.allocations
+      ⇒
+      interval_ok i1 h.valid_addresses ∧ interval_ok i2 h.valid_addresses ∧
+      (interval_to_set i1 ∩ interval_to_set i2 ≠ ∅ ⇒ i1 = i2)
+End
+
+(* The heap maps exactly the address in the allocations *)
+Definition heap_ok_def:
+  heap_ok h ⇔
+    allocations_ok h ∧
+    ∀n. flookup h.memory (A n) ≠ None ⇔ ∃i. i ∈ h.allocations ∧ n ∈ interval_to_set i
+End
+
+Definition get_bytes_def:
+  get_bytes h (Interval _ start stop) =
+    map
+      (λoff.
+        case flookup h.memory (A (start + off)) of
+        | None => (F, 0w)
+        | Some w => w)
+      (count_list (stop - start))
+End
+
+Definition set_bytes_def:
+  (set_bytes p [] n h = h) ∧
+  (set_bytes p (b::bs) n h =
+    set_bytes p bs (Suc n) (h with memory := h.memory |+ (A n, (p, b))))
+End
+
+(* Allocate a free chunk of memory, and write non-deterministic bytes into it *)
+Inductive allocate:
+   b = Interval T p (p + size) ∧
+   is_free b h ∧
+   length bytes = size
+   ⇒
+   allocate h size tag (w, set_bytes tag bytes p
+                           <| memory := h.memory;
+                              allocations := { b } ∪ h.allocations;
+                              valid_addresses := h.valid_addresses |>)
+End
+
+Definition deallocate_def:
+  deallocate addrs h =
+    let to_remove = { Interval T n stop | A n ∈ set addrs ∧ Interval T n stop ∈ h.allocations } in
+      <| memory := fdiff h.memory (image A (bigunion (image interval_to_set to_remove)));
+         allocations := h.allocations DIFF to_remove;
+         valid_addresses := h.valid_addresses |>
+End
+
+
+(* Read len bytes from the list of bytes, and convert it into a word value,
+ * little-endian encoding *)
+Definition le_read_w_def:
+  le_read_w len (bs : word8 list) =
+    if length bs < len then
+      (l2w 256 (map w2n bs), [])
+    else
+      (l2w 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
+      take len (l ++ replicate (len - length l) 0w)
+End
+
+(* Read a from a list of bytes bs to build a register value described by a
+ * 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 (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)) ∧
+  (read_array f (Suc n) s bs =
+    let (v, bs) = bytes_to_value f s bs in
+    let (rest, bs) = read_array f n s bs in
+      (v::rest, bs)) ∧
+  (read_str f [] bs = ([], bs)) ∧
+  (read_str f (s::ss) bs =
+    let (v, bs) = bytes_to_value f s bs in
+    let (rest, bs) = read_str f ss bs in
+      (v::rest, bs))
+Termination
+  WF_REL_TAC `measure (λx. case x of
+                           | INL (_, t, bs) => shape_size (\x.0) t
+                           | INR (INL (_, n, t, bs)) => n + shape_size (\x.0) t
+                           | INR (INR (_, ts, bs)) => shape1_size (\x.0) ts)`
+End
+
+(* Convert the given value to a list of bytes, the function gives the size, and
+ * a machine word for a flat value *)
+Definition value_to_bytes_def:
+  (value_to_bytes f (FlatV x) =
+    let (size, word) = f x in
+      le_write_w 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)` >>
+  Induct >> rw [definition "reg_v_size_def"] >>
+  TRY (first_x_assum drule) >>
+  decide_tac
+End
+
+(* ----- Theorems about converting between values and byte lists ----- *)
+
+Theorem le_write_w_length:
+  ∀l x. length (le_write_w l w) = l
+Proof
+  rw [le_write_w_def]
+QED
+
+Theorem v2b_size_lem:
+  (∀(f:num->'a->'b->bool) s v. (∀n t x. f n t x ⇒ fst (g x) = n) ∧ value_shape f s v ⇒ length (value_to_bytes g v) = sizeof s) ∧
+  (∀(f:num->'a->'b->bool) ss vs. (∀n t x. f n t x ⇒ fst (g x) = n) ∧ value_shapes f ss vs ⇒ sum (map (length o value_to_bytes g) vs) = sum (map sizeof ss))
+Proof
+  ho_match_mp_tac value_shape_ind >>
+  rw [value_to_bytes_def, sizeof_def, value_shape_def]
+  >- (
+    pairarg_tac >> simp [] >>
+    metis_tac [FST, le_write_w_length])
+  >- (
+    simp [LENGTH_FLAT, MAP_MAP_o, combinTheory.o_DEF] >>
+    Induct_on `vs` >> rw [ADD1] >> fs [LEFT_ADD_DISTRIB] >>
+    metis_tac [])
+  >- (fs [LENGTH_FLAT, ETA_THM, MAP_MAP_o, combinTheory.o_DEF] >> metis_tac [])
+  >- metis_tac [ADD_COMM]
+QED
+
+Theorem v2b_size:
+  ∀f s v g. (∀n t x. f n t x ⇒ fst (g x) = n) ∧ value_shape f s v ⇒ length (value_to_bytes g v) = sizeof s
+Proof
+  metis_tac [v2b_size_lem]
+QED
+
+Theorem b2v_size_lem:
+  (∀(f:num->'c ->'a word -> '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 ⇒
+    ∃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 ⇒
+    ∃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] >>
+  fs []
+  >- (simp [PAIR_MAP] >> metis_tac [SND])
+  >- (
+    pairarg_tac >> rw [] >> pairarg_tac >> rw [] >>
+    fs [ADD1] >> rw [] >> fs [DROP_DROP_T, LEFT_ADD_DISTRIB])
+  >- fs [DROP_DROP_T, LEFT_ADD_DISTRIB]
+QED
+
+Theorem b2v_size:
+  ∀f s bs. sizeof s ≤ length bs ⇒
+    ∃v. bytes_to_value f s bs = (v, drop (sizeof s) bs)
+Proof
+  metis_tac [b2v_size_lem]
+QED
+
+Theorem b2v_smaller:
+  ∀f s bs. sizeof s ≤ length bs ⇒
+    length (snd (bytes_to_value f s bs)) = length bs - sizeof s
+Proof
+  rw [] >> imp_res_tac b2v_size >>
+  Cases_on `bytes_to_value f s bs` >> fs [] >>
+  first_x_assum (qspec_then `f` mp_tac) >> rw []
+QED
+
+Theorem b2v_append_lem:
+  (∀(f:num->'c->'a word -> '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 ⇒
+    ∃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 ⇒
+    ∃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] >>
+  fs [TAKE_APPEND, DROP_APPEND,
+      DECIDE ``!x y. x ≤ y ⇒ x - y = 0n``, ETA_THM]
+  >- (simp [PAIR_MAP] >> metis_tac [SND])
+  >- (simp [PAIR_MAP] >> metis_tac [SND])
+  >- (
+    rpt (pairarg_tac >> simp []) >> fs [ADD1] >>
+    BasicProvers.VAR_EQ_TAC >> fs [LEFT_ADD_DISTRIB] >>
+    first_x_assum irule >>
+    `sizeof s ≤ length bs` by decide_tac >>
+    qspec_then `f` drule b2v_smaller >>
+    disch_then (qspec_then `f` mp_tac) >>
+    rw [])
+  >- (
+    rpt (pairarg_tac >> simp []) >> fs [ADD1] >>
+    BasicProvers.VAR_EQ_TAC >> fs [LEFT_ADD_DISTRIB] >>
+    first_x_assum irule >>
+    `sizeof s ≤ length bs` by decide_tac >>
+    qspec_then `f` drule b2v_smaller >>
+    disch_then (qspec_then `f` mp_tac) >>
+    rw [])
+QED
+
+Theorem b2v_append:
+  ∀f s bs bs'. sizeof s ≤ length bs ⇒
+    bytes_to_value f s (bs ++ bs') = (I ## (λx. x ++ bs')) (bytes_to_value f s bs)
+Proof
+  metis_tac [b2v_append_lem]
+QED
+
+Theorem le_read_write:
+  ∀n w bs.
+    w2n w < 256 ** n ⇒ le_read_w n (le_write_w n w ⧺ bs) = (w, bs)
+Proof
+  rw [le_read_w_def, le_write_w_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] >>
+    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`
+    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] >>
+      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 [] >>
+      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 [] >>
+      fs [EXP_EXP_MULT] >>
+      `2 ** log 2 m ≤ m` by rw [exp_log_bound] >>
+      decide_tac) >>
+    simp [mod_n2l, l2n_n2l, TAKE_LENGTH_TOO_LONG])
+  >- metis_tac [le_write_w_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')
+    ⇒
+    le_write_w n w ++ 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`
+  by (
+    `n ≤ 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 [] >>
+    rpt (pop_assum kall_tac) >>
+    Induct_on `bs` >> rw [] >>
+    Cases_on `h` >> fs []) >>
+  rw [n2l_l2n]
+  >- (
+    rw [TAKE_def, take_replicate] >>
+    Cases_on `n` >> fs [] >>
+    rfs [l2n_0] >> unabbrev_all_tac >> fs [EVERY_MAP] >>
+    ONCE_REWRITE_TAC [GSYM REPLICATE] >>
+    qmatch_goalsub_abbrev_tac `take n _` >>
+    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 [] >>
+    Cases_on `bs` >> rw [] >> fs [] >>
+    Cases_on `h` >> fs [] >>
+    first_x_assum irule >> rw [] >>
+    irule MONO_EVERY >>
+    qexists_tac `(λx. 0 = w2n x)` >> rw []) >>
+  fs [MAP_TAKE, MAP_MAP_o, combinTheory.o_DEF] >>
+  `exists (\y. 0 ≠ y) l`
+  by (
+    fs [l2n_eq_0, combinTheory.o_DEF] >> fs [EXISTS_MEM, EVERY_MEM] >>
+    qexists_tac `x` >> rfs [MOD_MOD, GREATER_DEF]) >>
+  simp [LOG_l2n_dropWhile] >>
+  `length (dropWhile ($= 0) (reverse l)) ≠ 0`
+  by (
+    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`
+  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`
+  by metis_tac [LESS_EQ_TRANS, LENGTH_dropWhile_LESS_EQ, LENGTH_REVERSE] >>
+  rw [MIN_DEF] >> fs []
+  >- (
+    simp [TAKE_APPEND, TAKE_TAKE_MIN, MIN_DEF, take_replicate] >>
+    `replicate (length l − length (dropWhile ($= 0) (reverse l))) 0w =
+     take (length l − (length (dropWhile ($= 0) (reverse l)))) (drop (length (dropWhile ($= 0) (reverse l))) bs)`
+    suffices_by (rw [] >> irule take_drop_partition >> simp []) >>
+    rw [LIST_EQ_REWRITE, EL_REPLICATE, EL_TAKE, EL_DROP] >>
+   `length (dropWhile ($= 0) (reverse l)) =
+     length (dropWhile (λx. 0 = w2n x) (reverse (take (length l) bs)))`
+    by (
+      `reverse l = reverse (take (length l) (map w2n bs))` by metis_tac [] >>
+      ONCE_ASM_REWRITE_TAC [] >>
+      qpat_x_assum `Abbrev (l = _)` kall_tac >>
+      simp [GSYM MAP_TAKE, GSYM MAP_REVERSE, dropWhile_map, combinTheory.o_DEF]) >>
+    fs [] >>
+    `x + length (dropWhile (λx. 0 = w2n x) (reverse (take (length l) bs))) < length l` by decide_tac >>
+    drule (SIMP_RULE std_ss [LET_THM] dropWhile_rev_take) >>
+    rw [] >>
+    REWRITE_TAC [GSYM w2n_11, word_0_n2w] >>
+    simp [])
+  >- rw [TAKE_APPEND, TAKE_TAKE]
+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) ⇒
+    ∀bs.
+      bytes_to_value (g:num -> 'c -> 'a word -> 'b) 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) ⇒
+    ∀bs.
+      read_str (g:num -> 'c -> 'a word -> 'b) 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 []
+  >- (
+    pairarg_tac >> fs [] >>
+    first_x_assum drule >> simp [] >> rw [] >>
+    simp [le_read_write])
+  >- (
+    qmatch_abbrev_tac `_ x = _` >>
+    `x = (vs, bs)` suffices_by (simp [PAIR_MAP] >> metis_tac [PAIR_EQ, FST, SND]) >>
+    unabbrev_all_tac >>
+    qid_spec_tac `bs` >> Induct_on `vs` >> simp [bytes_to_value_def] >>
+    rw [] >> fs [definition "reg_v_size_def"] >>
+    pairarg_tac >> fs [] >>
+    pairarg_tac >> fs [] >>
+    rename1 `value_shape _ s v1` >>
+    qpat_x_assum `_ ⇒ !bs. P bs` mp_tac >> impl_tac >> simp [] >>
+    metis_tac [APPEND_ASSOC, PAIR_EQ])
+  >- (
+    qmatch_abbrev_tac `_ x = _` >>
+    `x = (vs, bs)` suffices_by (simp [PAIR_MAP] >> metis_tac [PAIR_EQ, FST, SND]) >>
+    metis_tac [])
+  >- (
+    pairarg_tac >> fs [] >>
+    pairarg_tac >> fs [] >>
+    metis_tac [APPEND_ASSOC, PAIR_EQ])
+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) ⇒
+      bytes_to_value g s (value_to_bytes h v ++ bs) = (v, bs)
+Proof
+  metis_tac [b2v_v2b_lem]
+QED
+
+Theorem flookup_set_bytes:
+  ∀tag bytes n h n'.
+    flookup ((set_bytes tag bytes n h).memory) (A n') =
+      if n ≤ n' ∧ n' < n + length bytes then
+        Some (tag, el (n' - n) bytes)
+      else
+        flookup h.memory (A n')
+Proof
+  Induct_on `bytes` >> rw [set_bytes_def, EL_CONS, PRE_SUB1] >>
+  fs [ADD1, FLOOKUP_UPDATE] >>
+  `n = n'` by decide_tac >>
+  rw []
+QED
+
+Theorem set_bytes_unchanged:
+  ∀t bs p h. (set_bytes t bs p h).valid_addresses = h.valid_addresses ∧
+             (set_bytes t bs p h).allocations = h.allocations
+Proof
+  Induct_on `bs` >> rw [set_bytes_def]
+QED
+
+Theorem allocate_unchanged:
+  ∀h1 v1 t h2 v2.
+    allocate h1 v1 t (v2, h2)
+    ⇒
+    h1.valid_addresses = h2.valid_addresses ∧
+    h1.allocations ⊆ h2.allocations
+Proof
+  rw [allocate_cases] >> rw [set_bytes_unchanged]
+QED
+
+Theorem allocate_heap_ok:
+  ∀h1 v1 t v2 h2. heap_ok h1 ∧ allocate h1 v1 t (v2,h2) ⇒ heap_ok h2
+Proof
+  rw [allocate_cases, heap_ok_def]
+  >- (
+    fs [allocations_ok_def] >> rpt gen_tac >> disch_tac >> fs [is_free_def] >> rw [] >>
+    fs [set_bytes_unchanged] >> metis_tac [INTER_COMM])
+  >- (
+    rw [flookup_set_bytes, set_bytes_unchanged]
+    >- rw [RIGHT_AND_OVER_OR, EXISTS_OR_THM, interval_to_set_def] >>
+    eq_tac >> rw [] >> fs [interval_to_set_def] >>
+    metis_tac [])
+QED
+
+Theorem set_bytes_heap_ok:
+  ∀h tag bytes n b.
+    heap_ok h ∧ is_allocated (Interval b n (n + length bytes)) h
+    ⇒
+    heap_ok (set_bytes tag bytes n h)
+Proof
+  rw [heap_ok_def]
+  >- (fs [allocations_ok_def] >> rw [set_bytes_unchanged] >> metis_tac [])
+  >- (
+    fs [flookup_set_bytes, set_bytes_unchanged] >> rw [] >>
+    fs [is_allocated_def, interval_to_set_def, SUBSET_DEF] >>
+    metis_tac [LESS_EQ_REFL, DECIDE ``!x y. x < x + SUC y``])
+QED
+
+export_theory ();
diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml
new file mode 100644
index 000000000..953161431
--- /dev/null
+++ b/sledge/semantics/miscScript.sml
@@ -0,0 +1,172 @@
+(*
+ * 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.
+ *)
+
+(* Misc. theorems that aren't specific to the semantics of LLVM or Sledge. These
+ * could be upstreamed to HOL, and should eventually. *)
+
+open HolKernel boolLib bossLib Parse;
+open listTheory rich_listTheory arithmeticTheory wordsTheory;
+open finite_mapTheory open logrootTheory numposrepTheory;
+open settingsTheory;
+
+new_theory "misc";
+
+numLib.prefer_num ();
+
+(* ----- Theorems about list library functions ----- *)
+
+Theorem dropWhile_map:
+  ∀P f l. dropWhile P (map f l) = map f (dropWhile (P o f) l)
+Proof
+  Induct_on `l` >> rw []
+QED
+
+Theorem dropWhile_prop:
+  ∀P l x. x < length l - length (dropWhile P l) ⇒ P (el x l)
+Proof
+  Induct_on `l` >> rw [] >>
+  Cases_on `x` >> fs []
+QED
+
+Theorem dropWhile_rev_take:
+  ∀P n l x.
+    let len = length (dropWhile P (reverse (take n l))) in
+      x + len < n ∧ n ≤ length l ⇒ P (el (x + len) l)
+Proof
+  rw [] >>
+  `P (el ((n - 1 - x - length (dropWhile P (reverse (take n l))))) (reverse (take n l)))`
+  by (irule dropWhile_prop >> simp [LENGTH_REVERSE]) >>
+  rfs [EL_REVERSE, EL_TAKE, PRE_SUB1]
+QED
+
+Theorem take_replicate:
+  ∀m n x. take m (replicate n x) = replicate (min m n) x
+Proof
+  Induct_on `n` >> rw [TAKE_def, MIN_DEF] >> fs [] >>
+  Cases_on `m` >> rw []
+QED
+
+Theorem length_take_less_eq:
+  ∀n l. length (take n l) ≤ n
+Proof
+  Induct_on `l` >> rw [TAKE_def] >>
+  Cases_on `n` >> fs []
+QED
+
+Theorem flat_drop:
+  ∀n m ls. flat (drop m ls) = drop (length (flat (take m ls))) (flat ls)
+Proof
+  Induct_on `ls` >> rw [DROP_def, DROP_APPEND] >>
+  irule (GSYM DROP_LENGTH_TOO_LONG) >> simp []
+QED
+
+Theorem take_is_prefix:
+  ∀n l. take n l ≼ l
+Proof
+  Induct_on `l` >> rw [TAKE_def]
+QED
+
+Theorem sum_prefix:
+  ∀l1 l2. l1 ≼ l2 ⇒ sum l1 ≤ sum l2
+Proof
+  Induct >> rw [] >> Cases_on `l2` >> fs []
+QED
+
+Theorem flookup_fdiff:
+  ∀m s k.
+    flookup (fdiff m s) k =
+      if k ∈ s then None else flookup m k
+Proof
+  rw [FDIFF_def, FLOOKUP_DRESTRICT] >> fs []
+QED
+
+(* ----- Theorems about log ----- *)
+
+Theorem mul_div_bound:
+  ∀m n. n ≠ 0 ⇒ m - (n - 1) ≤ n * (m DIV n) ∧ n * (m DIV n) ≤ m
+Proof
+  rw [] >>
+  `0 < n` by decide_tac >>
+  drule DIVISION >> disch_then (qspec_then `m` mp_tac) >>
+  decide_tac
+QED
+
+Theorem exp_log_bound:
+  ∀b n. 1 < b ∧ n ≠ 0 ⇒ n DIV b + 1 ≤ b ** (log b n) ∧ b ** (log b n) ≤ n
+Proof
+  rw [] >> `0 < n` by decide_tac >>
+  drule LOG >> disch_then drule >> rw [] >>
+  fs [ADD1, EXP_ADD] >>
+  simp [DECIDE ``∀x y. x + 1 ≤ y ⇔ x < y``] >>
+  `∃x. b = Suc x` by intLib.COOPER_TAC >>
+  `b * (n DIV b) < b * b ** log b n` suffices_by metis_tac [LESS_MULT_MONO] >>
+  pop_assum kall_tac >>
+  `b ≠ 0` by decide_tac >>
+  drule mul_div_bound >> disch_then (qspec_then `n` mp_tac) >>
+  decide_tac
+QED
+
+Theorem log_base_power:
+  ∀n b. 1 < b ⇒ log b (b ** n) = n
+Proof
+  Induct >> rw [EXP, LOG_1] >>
+  Cases_on `n` >> rw [LOG_BASE] >>
+  first_x_assum drule >> rw [] >>
+  simp [Once EXP, LOG_MULT]
+QED
+
+Theorem log_change_base_power:
+  ∀m n b. 1 < b ∧ m ≠ 0 ∧ n ≠ 0 ⇒ log (b ** n) m = log b m DIV n
+Proof
+  rw [] >> irule LOG_UNIQUE >>
+  rw [ADD1, EXP_MUL, LEFT_ADD_DISTRIB] >>
+  qmatch_goalsub_abbrev_tac `x DIV _` >>
+  drule mul_div_bound >> disch_then (qspec_then `x` mp_tac) >> rw []
+  >- (
+    irule LESS_LESS_EQ_TRANS >>
+    qexists_tac `b ** (x+1)` >> rw [] >>
+    unabbrev_all_tac >>
+    simp [EXP_ADD] >>
+    `b * (m DIV b + 1) ≤ b * b ** log b m`
+    by metis_tac [exp_log_bound, LESS_MONO_MULT, MULT_COMM] >>
+    `m < b * (m DIV b + 1)` suffices_by decide_tac >>
+    simp [LEFT_ADD_DISTRIB] >>
+    `b ≠ 0` by decide_tac >>
+    `m - (b - 1) ≤ b * (m DIV b)` by metis_tac [mul_div_bound] >>
+    fs [])
+  >- (
+    irule LESS_EQ_TRANS >>
+    qexists_tac `b ** (log b m)` >> rw [] >>
+    unabbrev_all_tac >>
+    metis_tac [exp_log_bound])
+QED
+
+(* ----- Theorems about word stuff ----- *)
+
+Theorem l2n_padding:
+  ∀ws n. l2n 256 (ws ++ map w2n (replicate n 0w)) = l2n 256 ws
+Proof
+  Induct >> rw [l2n_def] >>
+  Induct_on `n` >> rw [l2n_def]
+QED
+
+Theorem l2n_0:
+  ∀l b. b ≠ 0 ∧ every ($> b)  l⇒ (l2n b l = 0 ⇔ every ($= 0) l)
+Proof
+  Induct >> rw [l2n_def] >>
+  eq_tac >> rw []
+QED
+
+Theorem mod_n2l:
+  ∀d n. 0 < d ⇒ map (\x. x MOD d) (n2l d n) = n2l d n
+Proof
+  rw [] >> drule n2l_BOUND >> disch_then (qspec_then `n` mp_tac) >>
+  qspec_tac (`n2l d n`, `l`) >>
+  Induct >> rw []
+QED
+
+export_theory ();