diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index 48006eed2..d62276197 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -152,10 +152,12 @@ Datatype `
        (* 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 |>`;
 
 (* ----- Things about types ----- *)
 
+(* How many bytes a value of the given type occupies *)
 Definition sizeof_def:
   (sizeof (IntT W1) = 1) ∧
   (sizeof (IntT W8) = 1) ∧
@@ -232,6 +234,7 @@ Definition bool_to_v_def:
   bool_to_v b = if b then W1V 1w else W1V 0w
 End
 
+(* Calculate the offset given by a list of indices *)
 Definition get_offset_def:
   (get_offset _ [] = Some 0) ∧
   (get_offset (ArrT _ t) (i::is) =
@@ -294,14 +297,6 @@ Definition v2n_def:
   (v2n _ = None)
 End
 
-Definition update_result_def:
-  update_result x v s = s with locals := s.locals |+ (x, v)
-End
-
-Definition inc_pc_def:
-  inc_pc s = s with ip := (s.ip with i := s.ip.i + 1)
-End
-
 Definition interval_to_set_def:
   interval_to_set (_, start,stop) =
     { n | start ≤ n ∧ n < stop }
@@ -324,6 +319,16 @@ Definition is_free_def:
     ∀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))
+End
+
 Definition set_bytes_def:
   (set_bytes p [] n h = h) ∧
   (set_bytes p (b::bs) n h =
@@ -349,16 +354,8 @@ Definition deallocate_def:
       (allocs DIFF to_remove, fdiff h (image A (bigunion (image interval_to_set to_remove))))
 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))
-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
@@ -367,6 +364,7 @@ Definition le_read_w_def:
       (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
@@ -470,6 +468,14 @@ Definition insert_value_def:
   (insert_value _ _ _ = None)
 End
 
+Definition update_result_def:
+  update_result x v s = s with locals := s.locals |+ (x, v)
+End
+
+Definition inc_pc_def:
+  inc_pc s = s with ip := (s.ip with i := s.ip.i + 1)
+End
+
 (* NB, the semantics tracks the poison values, but not much thought has been put
  * into getting it exactly right, so we don't have much confidence that it is
  * exactly right. We also are currently ignoring the undefined value. *)
@@ -601,12 +607,14 @@ Inductive step_instr:
      (Call r t fname targs)
      <| ip := <| f := fname; b := None; i := 0 |>;
         locals := alist_to_fmap (zip (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;
              result_var := r;
              stack_allocs := [] |> :: s.stack;
-        heap := heap |>) ∧
+        heap := s.heap |>) ∧
 
   (* TODO *)
   (step_instr prog s (Cxa_allocate_exn r a) s) ∧
@@ -635,8 +643,9 @@ Inductive step:
   step p s s'
 End
 
-(* ----- Initial state ----- *)
+(* ----- Invariants on state ----- *)
 
+(* The allocations are of intervals that don't overlap *)
 Definition allocations_ok_def:
   allocations_ok s ⇔
     ∀i1 i2.
@@ -646,11 +655,13 @@ Definition allocations_ok_def:
       (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.
@@ -659,47 +670,36 @@ Definition globals_ok_def:
       is_allocated (F, w2n w, w2n w + n) s.allocations
 End
 
-(* The initial state contains allocations for the initialised global variables *)
-Definition is_init_state_def:
-  is_init_state s (global_init : glob_var |-> ty # v) ⇔
-    s.ip.f = Fn "main" ∧
-    s.ip.b = None ∧
-    s.ip.i = 0 ∧
-    s.locals = fempty ∧
-    s.stack = [] ∧
-    allocations_ok s ∧
-    globals_ok s ∧
-    fdom s.globals = fdom global_init ∧
-    s.allocations ⊆ {F, start, stop | T} ∧
-    ∀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, [])
-End
-
-(* ----- Invariants on state ----- *)
-
-Definition prog_ok_def:
-  prog_ok p ⇔
-    ∀fname dec bname block.
-      flookup p fname = Some dec ∧
-      flookup dec.blocks bname = Some block
-      ⇒
-      block.body ≠ [] ∧ terminator (last block.body)
-End
-
+(* Instruction pointer points to an instruction *)
 Definition ip_ok_def:
   ip_ok p ip ⇔
     ∃dec block. flookup p ip.f = Some dec ∧ flookup dec.blocks ip.b = Some block ∧ ip.i < length block.body
 End
 
+Definition prog_ok_def:
+  prog_ok p ⇔
+    ((* All blocks end with terminators *)
+     ∀fname dec bname block.
+       flookup p fname = Some dec ∧
+       flookup dec.blocks bname = Some block
+       ⇒
+       block.body ≠ [] ∧ terminator (last block.body)) ∧
+    ((* All functions have an entry block *)
+     ∀fname dec.
+       flookup p fname = Some dec ⇒ ∃block. flookup dec.blocks None = Some block) ∧
+     (* There is a main function *)
+     ∃dec. flookup p (Fn "main") = Some dec
+End
+
+(* All call frames have a good return address, and the stack allocations of the
+ * frame are all in freeable memory *)
 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
 
+(* The frames are all of, and no two stack allocations have the same address *)
 Definition stack_ok_def:
   stack_ok p s ⇔
     every (frame_ok p s) s.stack ∧
@@ -711,4 +711,29 @@ Definition state_invariant_def:
     ip_ok p s.ip ∧ allocations_ok s ∧ heap_ok s ∧ globals_ok s ∧ stack_ok p s
 End
 
+(* ----- Initial state ----- *)
+
+(* The initial state contains allocations for the initialised global variables *)
+Definition is_init_state_def:
+  is_init_state s (global_init : glob_var |-> ty # v) ⇔
+    s.ip.f = Fn "main" ∧
+    s.ip.b = None ∧
+    s.ip.i = 0 ∧
+    s.locals = fempty ∧
+    s.stack = [] ∧
+    allocations_ok s ∧
+    globals_ok s ∧
+    heap_ok s ∧
+    fdom s.globals = fdom global_init ∧
+    (* The initial allocations for globals are not freeable *)
+    s.allocations ⊆ { (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, [])
+End
+
 export_theory();
diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml
index 3c58d1b2e..20b8db6c6 100644
--- a/sledge/semantics/llvm_propScript.sml
+++ b/sledge/semantics/llvm_propScript.sml
@@ -686,7 +686,7 @@ Theorem step_instr_invariant:
     state_invariant p s2
 Proof
   ho_match_mp_tac step_instr_ind >> rw []
-  >- (
+  >- ( (* Ret *)
     rw [update_invariant] >> fs [state_invariant_def] >> rw []
     >- (
       fs [stack_ok_def] >> rfs [EVERY_EL, frame_ok_def] >>
@@ -711,8 +711,26 @@ Proof
         metis_tac [])
       >- (
         fs [ALL_DISTINCT_APPEND])))
-  >- cheat
-  >- cheat
+  >- ( (* Br *)
+    fs [state_invariant_def] >> rw []
+    >- (
+      rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >>
+      qpat_x_assum `flookup _ (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 *)
+    fs [state_invariant_def] >> rw []
+    >- (
+      rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >>
+      qpat_x_assum `flookup _ (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 []))
   >- (
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant]>>
     metis_tac [terminator_def])
@@ -722,8 +740,7 @@ Proof
   >- (
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
     metis_tac [terminator_def])
-  >- (
-    (* Allocation *)
+  >- ( (* Allocation *)
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant]
     >- metis_tac [allocate_invariant]
     >- (fs [next_instr_cases, allocate_cases] >> metis_tac [terminator_def]))
@@ -731,8 +748,7 @@ Proof
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
     fs [next_instr_cases] >>
     metis_tac [terminator_def])
-  >- (
-    (* Store *)
+  >- ( (* Store *)
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant]
     >- (irule set_bytes_invariant >> rw [] >> metis_tac [])
     >- (fs [next_instr_cases] >> metis_tac [terminator_def]))
@@ -748,7 +764,32 @@ Proof
   >- (
     irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
     metis_tac [terminator_def])
-  >- cheat
+  >- ( (* 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 [])
+    >- (
+      fs [state_invariant_def, stack_ok_def] >> rw []
+      >- (
+        rw [frame_ok_def] >> fs [ip_ok_def, prog_ok_def] >>
+        last_x_assum drule >> disch_then drule >> rw [] >>
+        CCONTR_TAC >> fs [] >> rfs [LAST_EL] >>
+        Cases_on `length block'.body = s1.ip.i + 1` >> fs [PRE_SUB1] >>
+        fs [next_instr_cases] >>
+        metis_tac [terminator_def])
+      >- (fs [EVERY_MEM, frame_ok_def] >> metis_tac [])))
+QED
+
+(* ----- Initial state is ok ----- *)
+
+Theorem init_invariant:
+  ∀p s init. prog_ok p ∧ is_init_state s init ⇒ state_invariant p s
+Proof
+  rw [is_init_state_def, state_invariant_def]
+  >- (rw [ip_ok_def] >> fs [prog_ok_def] >> metis_tac [NOT_NIL_EQ_LENGTH_NOT_0])
+  >- rw [stack_ok_def]
 QED
 
 export_theory ();