diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index 4d101c27a..48006eed2 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -239,7 +239,7 @@ Definition get_offset_def:
     | None => None
     | Some off => Some (i * sizeof t + off)) ∧
   (get_offset (StrT ts) (i::is) =
-    if i < length ts then 
+    if i < length ts then
       case get_offset (el i ts) is of
       | None => None
       | Some off => Some (sum (map sizeof (take i ts)) + off)
@@ -282,7 +282,7 @@ Definition eval_def:
   (eval s (Variable v) =
     case flookup s.locals v of
     | None => <| poison := F; value := W1V 0w |>
-    | Some v => v) ∧ 
+    | Some v => v) ∧
   (eval s (Constant c) = <| poison := F; value := eval_const s.globals c |>)
 End
 
@@ -308,14 +308,14 @@ Definition interval_to_set_def:
 End
 
 Definition interval_ok_def:
-  interval_ok (_, i1, i2) ⇔
+  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 ∧ interval_to_set b1 ⊆ interval_to_set b2
+    ∃b2. b2 ∈ allocs ∧ fst b1 = fst b2 ∧ interval_to_set b1 ⊆ interval_to_set b2
 End
 
 Definition is_free_def:
@@ -324,23 +324,29 @@ Definition is_free_def:
     ∀b2. b2 ∈ allocs ⇒ interval_to_set b1 ∩ interval_to_set b2 = ∅
 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))))
+End
+
+(* Allocate a free chunk of memory, and write non-deterministic bytes into it *)
 Inductive allocate:
-  (v2n v.value = Some m ∧
+  v2n v.value = Some m ∧
    b = (T, w2n w, w2n w + m * len) ∧
-   is_free b s.allocations
+   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))
+         s with <| allocations := { b } ∪ s.allocations;
+                   heap := set_bytes v.poison bytes (w2n w) s.heap |>)
 End
 
 Definition deallocate_def:
-  (deallocate (A n) (Some allocs) =
-    if ∃m. (T,n,m) ∈ allocs then
-      Some { (b,start,stop) | (b,start,stop) ∈ allocs ∧ start ≠ n }
-    else
-      None) ∧
-  (deallocate _ None = None)
+  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))))
 End
 
 Definition get_bytes_def:
@@ -406,12 +412,6 @@ Termination
   decide_tac
 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))))
-End
-
 Definition do_sub_def:
   do_sub (nuw:bool) (nsw:bool) (v1:pv) (v2:pv) =
     let (diff, u_overflow, s_overflow) =
@@ -439,7 +439,7 @@ Definition do_icmp_def:
          | (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 
+         | (W64V w1, W64V w2) => (get_comp c) w1 w2
          | (PtrV w1, PtrV w2) => (get_comp c) w1 w2) |>
 End
 
@@ -476,16 +476,17 @@ End
 Inductive step_instr:
 
   (s.stack = fr::st ∧
-   FOLDR deallocate (Some s.allocations) fr.stack_allocs = Some new_allocs
+   deallocate fr.stack_allocs s.allocations s.heap = (new_allocs, new_h)
    ⇒
    step_instr prog s
      (Ret (t, a))
      (update_result fr.result_var (eval s a)
        <| ip := fr.ret;
+          globals := s.globals;
           locals := fr.saved_locals;
           stack := st;
           allocations := new_allocs;
-          heap := heap |>)) ∧
+          heap := new_h |>)) ∧
 
 (* Do the phi assignments in parallel. The manual says "For the purposes of the
  * SSA form, the use of each incoming value is deemed to occur on the edge from
@@ -500,7 +501,7 @@ Inductive step_instr:
  *)
   (eval s a = <| poison := p; value := W1V tf |> ∧
    l = Some (if tf = 1w then l1 else l2) ∧
-   flookup prog s.ip.f = Some d ∧ 
+   flookup prog s.ip.f = Some d ∧
    flookup d.blocks l = Some <| h := Head phis None; body := b |> ∧
    map (do_phi l s) phis = map Some updates
    ⇒
@@ -542,7 +543,7 @@ Inductive step_instr:
      (inc_pc (update_result r v2 s2))) ∧
 
   (eval s a1 = <| poison := p1; value := PtrV w |> ∧
-   interval = (b, w2n w, w2n w + sizeof t) ∧
+   interval = (freeable, w2n w, w2n w + sizeof t) ∧
    is_allocated interval s.allocations ∧
    pbytes = get_bytes s.heap interval
    ⇒
@@ -553,7 +554,7 @@ Inductive step_instr:
                             s))) ∧
 
   (eval s a2 = <| poison := p2; value := PtrV w |> ∧
-   interval = (b, w2n w, w2n w + sizeof t) ∧
+   interval = (freeable, w2n w, w2n w + sizeof t) ∧
    is_allocated interval s.allocations ∧
    bytes = value_to_bytes (eval s a1).value ∧
    length bytes = sizeof t
@@ -562,7 +563,7 @@ Inductive step_instr:
      (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 ∧ 
+  (map (eval s o snd) tindices = i1::indices ∧
    (eval s a1).value = PtrV w1 ∧
    cast_num i1.value = Some n ∧
    map (λx. cast_num x.value) indices = map Some ns ∧
@@ -594,7 +595,7 @@ Inductive step_instr:
     (Icmp c t a1 a2)
     (inc_pc (update_result r (do_icmp c (eval s a1) (eval s a2)) s))) ∧
 
-  (flookup prog fname = Some d 
+  (flookup prog fname = Some d
    ⇒
    step_instr prog s
      (Call r t fname targs)
@@ -620,8 +621,8 @@ Inductive step_instr:
 End
 
 Inductive next_instr:
-  flookup p s.ip.f = Some d ∧ 
-  flookup d.blocks s.ip.b = Some b ∧ 
+  flookup p s.ip.f = Some d ∧
+  flookup d.blocks s.ip.b = Some b ∧
   s.ip.i < length b.body
   ⇒
   next_instr p s (el s.ip.i b.body)
@@ -642,13 +643,12 @@ Definition allocations_ok_def:
       i1 ∈ s.allocations ∧ i2 ∈ s.allocations
       ⇒
       interval_ok i1 ∧ interval_ok i2 ∧
-      (interval_to_set i1 ∩ interval_to_set i2 ≠ ∅ ⇒
-       interval_to_set i1 = interval_to_set i2)
+      (interval_to_set i1 ∩ interval_to_set i2 ≠ ∅ ⇒ i1 = i2)
 End
 
 Definition heap_ok_def:
   heap_ok s ⇔
-    ∀i n. i ∈ s.allocations ∧ n ∈ interval_to_set i ⇒ flookup s.heap (A n) ≠ None
+    ∀n. flookup s.heap (A n) ≠ None ⇔ ∃i. i ∈ s.allocations ∧ n ∈ interval_to_set i
 End
 
 Definition globals_ok_def:
@@ -675,7 +675,7 @@ Definition is_init_state_def:
       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, []) 
+        bytes_to_value t bytes = (v, [])
 End
 
 (* ----- Invariants on state ----- *)
@@ -698,11 +698,12 @@ 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
-End    
+End
 
 Definition stack_ok_def:
   stack_ok p s ⇔
-    every (frame_ok p s) s.stack
+    every (frame_ok p s) s.stack ∧
+    all_distinct (flat (map (λf. f.stack_allocs) s.stack))
 End
 
 Definition state_invariant_def:
diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml
index 5d6fff5c0..3c58d1b2e 100644
--- a/sledge/semantics/llvm_propScript.sml
+++ b/sledge/semantics/llvm_propScript.sml
@@ -9,6 +9,7 @@
 
 open HolKernel boolLib bossLib Parse;
 open pairTheory listTheory rich_listTheory arithmeticTheory wordsTheory;
+open pred_setTheory finite_mapTheory;
 open logrootTheory numposrepTheory;
 open settingsTheory llvmTheory;
 
@@ -76,13 +77,21 @@ 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 [] >> 
+  rw [] >>
   `0 < n` by decide_tac >>
   drule DIVISION >> disch_then (qspec_then `m` mp_tac) >>
   decide_tac
@@ -194,7 +203,7 @@ Theorem b2v_size:
     ∃vs. read_str ts bs = (vs, drop (sum (map sizeof ts)) 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_w_def] >>
   fs [first_class_type_def]
   >- (simp [PAIR_MAP] >> metis_tac [SND])
   >- (
@@ -220,22 +229,22 @@ Theorem b2v_append:
     ∃vs. read_str ts (bs ++ bs') = (I ## (λx. x ++ bs')) (read_str ts 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_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] >> 
+    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 >> 
+    `sizeof t ≤ length bs` by decide_tac >>
     imp_res_tac b2v_smaller >> rfs [])
   >- (
-    rpt (pairarg_tac >> simp []) >> fs [ADD1] >> 
+    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 >> 
+    `sizeof t ≤ length bs` by decide_tac >>
     imp_res_tac b2v_smaller >> rfs [])
 QED
 
@@ -323,7 +332,7 @@ Proof
   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] >> 
+  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] >>
@@ -345,7 +354,7 @@ Proof
     REWRITE_TAC [GSYM w2n_11, word_0_n2w] >>
     simp [])
   >- rw [TAKE_APPEND, TAKE_TAKE]
-QED 
+QED
 
 Theorem b2v_v2b:
   ∀v t bs. value_type t v ⇒ bytes_to_value t (value_to_bytes v ++ bs) = (v, bs)
@@ -427,7 +436,7 @@ Theorem extract_insertvalue:
     insert_value v1 v2 indices = Some v3
     ⇒
     extract_value v3 indices = Some v2
-Proof 
+Proof
   recInduct insert_value_ind >> rw [insert_value_def, extract_value_def] >>
   pop_assum mp_tac >> CASE_TAC >> fs [] >> rfs [] >>
   rw [] >> simp [extract_value_def, EL_LUPDATE]
@@ -439,7 +448,7 @@ Theorem extract_insertvalue_other:
     ¬(indices1 ≼ indices2) ∧ ¬(indices2 ≼ indices1)
     ⇒
     extract_value v3 indices2 = extract_value v1 indices2
-Proof 
+Proof
   recInduct insert_value_ind >> rw [insert_value_def, extract_value_def] >>
   qpat_x_assum `_ = SOME _` mp_tac >> CASE_TAC >> rw [] >> rfs [] >>
   qpat_x_assum `¬case _ of [] => F | h::t => P h t` mp_tac >>
@@ -452,7 +461,7 @@ Theorem insert_extractvalue:
     extract_value v1 indices = Some v2
     ⇒
     insert_value v1 v2 indices = Some v1
-Proof 
+Proof
   recInduct extract_value_ind >> rw [insert_value_def, extract_value_def] >> fs [] >>
   rw [LUPDATE_SAME]
 QED
@@ -476,7 +485,7 @@ Definition extract_type_def:
   (extract_type (StrT ts) (i::idx) =
     if i < length ts then
       extract_type (el i ts) idx
-    else 
+    else
       None) ∧
   (extract_type _ _ = None)
 End
@@ -621,11 +630,87 @@ 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
+Proof
+  rw [allocate_cases, state_invariant_def, ip_ok_def, heap_ok_def,
+      globals_ok_def, stack_ok_def] >>
+  rw [] >> fs []
+  >- (
+    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 [])
+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 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])
+QED
+
 Theorem step_instr_invariant:
-  ∀i s2. step_instr p s1 i s2 ⇒ prog_ok p ∧ next_instr p s1 i ∧ state_invariant p s1 ⇒ state_invariant p s2
+  ∀i s2.
+    step_instr p s1 i s2 ⇒ prog_ok p ∧ next_instr p s1 i ∧ state_invariant p s1
+    ⇒
+    state_invariant p s2
 Proof
   ho_match_mp_tac step_instr_ind >> rw []
-  >- cheat
+  >- (
+    rw [update_invariant] >> fs [state_invariant_def] >> rw []
+    >- (
+      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 [deallocate_def, heap_ok_def] >> rw [flookup_fdiff] >>
+      eq_tac >> rw []
+      >- metis_tac [optionTheory.NOT_IS_SOME_EQ_NONE]
+      >- metis_tac [optionTheory.NOT_IS_SOME_EQ_NONE] >>
+      fs [allocations_ok_def, stack_ok_def, EXTENSION] >> metis_tac [])
+    >- (
+      fs [globals_ok_def, deallocate_def] >> rw [] >>
+      first_x_assum drule >> rw [] >> fs [is_allocated_def] >>
+      qexists_tac `b2` >> rw [] >> CCONTR_TAC >> fs [])
+    >- (
+      fs [stack_ok_def, EVERY_MEM, frame_ok_def, deallocate_def] >> rfs [] >>
+      rw []
+      >- (
+        res_tac >> rw [] >> qexists_tac `stop` >> rw [] >>
+        fs [ALL_DISTINCT_APPEND, MEM_FLAT, MEM_MAP] >>
+        metis_tac [])
+      >- (
+        fs [ALL_DISTINCT_APPEND])))
   >- cheat
   >- cheat
   >- (
@@ -640,7 +725,7 @@ Proof
   >- (
     (* Allocation *)
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant]
-    >- cheat
+    >- metis_tac [allocate_invariant]
     >- (fs [next_instr_cases, allocate_cases] >> metis_tac [terminator_def]))
   >- (
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
@@ -649,7 +734,7 @@ Proof
   >- (
     (* Store *)
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant]
-    >- cheat
+    >- (irule set_bytes_invariant >> rw [] >> metis_tac [])
     >- (fs [next_instr_cases] >> metis_tac [terminator_def]))
   >- (
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
diff --git a/sledge/semantics/settingsScript.sml b/sledge/semantics/settingsScript.sml
index d22722c9e..af03c3ef6 100644
--- a/sledge/semantics/settingsScript.sml
+++ b/sledge/semantics/settingsScript.sml
@@ -29,6 +29,7 @@ overload_on ("el", ``EL``);
 overload_on ("count_list", ``COUNT_LIST``);
 overload_on ("Suc", ``SUC``);
 overload_on ("flat", ``FLAT``);
+overload_on ("all_distinct", ``ALL_DISTINCT``);
 overload_on ("take", ``TAKE``);
 overload_on ("drop", ``DROP``);
 overload_on ("replicate", ``REPLICATE``);
@@ -42,5 +43,10 @@ overload_on ("option_join", ``OPTION_JOIN``);
 overload_on ("min", ``MIN``);
 overload_on ("list_update", ``LUPDATE``);
 overload_on ("last", ``LAST``);
+overload_on ("fdiff", ``FDIFF``);
+overload_on ("image", ``IMAGE``);
+overload_on ("bigunion", ``BIGUNION``);
+overload_on ("finite", ``FINITE``);
+overload_on ("card", ``CARD``);
 
 export_theory ();