diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index 6fc3d9244..8027b9bd4 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -68,6 +68,21 @@ Datatype:
   cond = Eq | Ult | Slt
 End
 
+Datatype:
+  phi = Phi reg ty ((label option, arg) alist)
+End
+
+(*
+ * The Exit instruction below models a system/libc call to exit the program. The
+ * semantics needs some way to tell the difference between normally terminated
+ * programs and stuck states, and this lets it do that. From a C++ perspective,
+ * a program could call this directly, in which case it's good to model, or it
+ * might simply return from main and then the code in libc that called main will
+ * call exit. However, adding special handling for main in the semantics will
+ * cruft things up a bit, and it's not very satisfying, because it's not really
+ * an LLVM concept.
+ *)
+
 Datatype:
   instr =
   (* Terminators *)
@@ -96,10 +111,6 @@ Datatype:
   | Cxa_get_exception_ptr reg arg
 End
 
-Datatype:
-  phi = Phi reg ty ((label option, arg) alist)
-End
-
 Datatype:
   clause = Catch targ
 End
@@ -160,8 +171,17 @@ Datatype:
   pv = <| poison : bool; value : v |>
 End
 
+(* Instruction pointer into a block. Phi_ip indicates to do the phi instruction,
+ * coming from the given label. Offset points to a normal (non-phi) instruction.
+ * *)
+Datatype:
+  bip =
+  | Phi_ip (label option)
+  | Offset num
+End
+
 Datatype:
-  pc = <| f : fun_name; b : label option; i : num |>
+  pc = <| f : fun_name; b : label option; i : bip |>
 End
 
 Datatype:
@@ -461,8 +481,13 @@ Definition update_result_def:
   update_result x v s = s with locals := s.locals |+ (x, v)
 End
 
+Definition inc_bip_def:
+  (inc_bip (Phi_ip _) = Offset 0) ∧
+  (inc_bip (Offset i) = Offset (i + 1))
+End
+
 Definition inc_pc_def:
-  inc_pc s = s with ip := (s.ip with i := s.ip.i + 1)
+  inc_pc s = s with ip := (s.ip with i := inc_bip s.ip.i)
 End
 
 Inductive get_obs:
@@ -488,27 +513,12 @@ Inductive step_instr:
           stack := st;
           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
- * the corresponding predecessor block to the current block (but after any
- * definition of an 'invoke' instruction's return value on the same edge)".
- * So treat these two as equivalent
- * %r1 = phi [0, %l]
- * %r2 = phi [%r1, %l]
- * and
- * %r2 = phi [%r1, %l]
- * %r1 = phi [0, %l]
- *)
   (eval s a = Some <| poison := p; value := FlatV (W1V tf) |> ∧
-   l = Some (if tf = 1w then l1 else l2) ∧
-   alookup prog s.ip.f = Some d ∧
-   alookup d.blocks l = Some <| h := Head phis None; body := b |> ∧
-   map (do_phi l s) phis = map Some updates
+   l = Some (if tf = 1w then l1 else l2)
    ⇒
    step_instr prog s
      (Br a l1 l2) Tau
-     (s with <| ip := <| f := s.ip.f; b := l; i := 0 |>;
-                locals := s.locals |++ updates |>)) ∧
+     (s with ip := <| f := s.ip.f; b := l; i := Phi_ip s.ip.b |>)) ∧
 
   (* TODO *)
   (step_instr prog s (Invoke r t a args l1 l2) Tau s) ∧
@@ -623,11 +633,12 @@ Inductive step_instr:
    ⇒
    step_instr prog s
      (Call r t fname targs) Tau
-     <| ip := <| f := fname; b := None; i := 0 |>;
+     (* Jump to the entry block of the function which has no phis *)
+     <| ip := <| f := fname; b := None; i := Offset 0 |>;
         locals := alist_to_fmap (zip (map snd d.params, vs));
         globals := s.globals;
         stack :=
-          <| ret := s.ip with i := s.ip.i + 1;
+          <| ret := s.ip with i := inc_bip s.ip.i;
              saved_locals := s.locals;
              result_var := r;
              stack_allocs := [] |> :: s.stack;
@@ -647,24 +658,49 @@ Inductive step_instr:
 End
 
 Inductive get_instr:
-  (∀prog ip.
-   alookup prog ip.f = Some d ∧
-   alookup d.blocks ip.b = Some b ∧
-   ip.i < length b.body
-   ⇒
-   get_instr prog ip (el ip.i b.body))
+ (∀prog ip.
+  alookup prog ip.f = Some d ∧
+  alookup d.blocks ip.b = Some b ∧
+  ip.i = Offset idx ∧
+  idx < length b.body
+  ⇒
+  get_instr prog ip (Inl (el idx b.body))) ∧
+ (∀prog ip.
+  alookup prog ip.f = Some d ∧
+  alookup d.blocks ip.b = Some b ∧
+  ip.i = Phi_ip from_l ∧
+  b.h = Head phis landing
+  ⇒
+  get_instr prog ip (Inr (from_l, phis)))
 End
 
 Inductive step:
-  get_instr p s.ip i ∧
+ (get_instr p s.ip (Inl i) ∧
   step_instr p s i l s'
   ⇒
-  step p s l s'
+  step p s l s') ∧
+
+(* 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
+ * the corresponding predecessor block to the current block (but after any
+ * definition of an 'invoke' instruction's return value on the same edge)".
+ * So treat these two as equivalent
+ * %r1 = phi [0, %l]
+ * %r2 = phi [%r1, %l]
+ * and
+ * %r2 = phi [%r1, %l]
+ * %r1 = phi [0, %l]
+ *)
+ (get_instr p s.ip (Inr (from_l, phis)) ∧
+  map (do_phi from_l s) phis = map Some updates
+  ⇒
+  step p s Tau (inc_pc (s with locals := locals |++ updates)))
+
 End
 
 Definition get_observation_def:
   get_observation prog last_s =
-    if get_instr prog last_s.ip Exit then
+    if get_instr prog last_s.ip (Inl Exit) then
       Complete
     else if ∃s l. step prog last_s l s then
       Partial
@@ -695,20 +731,39 @@ End
 (* Instruction pointer points to an instruction *)
 Definition ip_ok_def:
   ip_ok p ip ⇔
-    ∃dec block. alookup p ip.f = Some dec ∧ alookup dec.blocks ip.b = Some block ∧ ip.i < length block.body
+    ∃dec block.
+      alookup p ip.f = Some dec ∧ alookup dec.blocks ip.b = Some block ∧
+      ((∃idx. ip.i = Offset idx ∧ idx < length block.body) ∨
+       (∃from_l. ip.i = Phi_ip from_l ∧ block.h ≠ Entry ∧ alookup dec.blocks from_l ≠ None))
+End
+
+Definition instr_to_labs_def:
+  (instr_to_labs (Br _ l1 l2) = [l1; l2]) ∧
+  (instr_to_labs _ = [])
 End
 
 Definition prog_ok_def:
   prog_ok p ⇔
-    ((* All blocks end with terminators *)
+    ((* All blocks end with terminators and terminators only appear at the end.
+      * All labels mentioned in instructions actually exist *)
      ∀fname dec bname block.
        alookup p fname = Some dec ∧
        alookup dec.blocks bname = Some block
        ⇒
-       block.body ≠ [] ∧ terminator (last block.body)) ∧
+       block.body ≠ [] ∧ terminator (last block.body) ∧
+       every (λi. ¬terminator i) (front block.body) ∧
+       every (λlab. alookup dec.blocks (Some lab) ≠ None)
+             (instr_to_labs (last block.body)) ∧
+       (∀phis lands. block.h = Head phis lands ⇒
+         every (λx. case x of Phi _ _ l => every (λ(lab, _). alookup dec.blocks lab ≠ None) l) phis)) ∧
     ((* All functions have an entry block *)
      ∀fname dec.
-       alookup p fname = Some dec ⇒ ∃block. alookup dec.blocks None = Some block) ∧
+       alookup p fname = Some dec ⇒
+       ∃block. alookup dec.blocks None = Some block ∧ block.h = Entry) ∧
+    ((* All non-entry blocks have a proper header *)
+     ∀fname dec l b.
+       alookup p fname = Some dec ∧ alookup dec.blocks (Some l) = Some b ⇒
+       b.h ≠ Entry) ∧
      (* There is a main function *)
      ∃dec. alookup p (Fn "main") = Some dec
 End
@@ -740,7 +795,7 @@ 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.ip.i = Offset 0 ∧
     s.locals = fempty ∧
     s.stack = [] ∧
     globals_ok s ∧
diff --git a/sledge/semantics/llvm_liveScript.sml b/sledge/semantics/llvm_liveScript.sml
index 76a9d069d..5bf85a761 100644
--- a/sledge/semantics/llvm_liveScript.sml
+++ b/sledge/semantics/llvm_liveScript.sml
@@ -16,35 +16,47 @@ new_theory "llvm_live";
 numLib.prefer_num ();
 
 Definition inc_pc_def:
-  inc_pc ip = ip with i := ip.i + 1
+  inc_pc ip = ip with i := inc_bip ip.i
 End
 
 (* The set of program counters the given instruction and starting point can
  * immediately reach, within a function *)
-Definition next_ips_def:
-  (next_ips (Ret _) ip = {}) ∧
-  (next_ips (Br _ l1 l2) ip =
-    { <| f := ip.f; b := Some l; i := 0 |> | l | l ∈ {l1; l2} }) ∧
-  (next_ips (Invoke _ _ _ _ l1 l2) ip =
-    { <| f := ip.f; b := Some l; i := 0 |> | l | l ∈ {l1; l2} }) ∧
-  (next_ips Unreachable ip = {}) ∧
-  (next_ips (Sub _ _ _ _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Extractvalue _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Insertvalue _ _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Alloca _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Load _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Store _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Gep _ _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Ptrtoint _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Inttoptr _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Icmp _ _ _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Call _ _ _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Cxa_allocate_exn _ _) ip = { inc_pc ip }) ∧
+Definition instr_next_ips_def:
+  (instr_next_ips (Ret _) ip = {}) ∧
+  (instr_next_ips (Br _ l1 l2) ip =
+    { <| f := ip.f; b := Some l; i := Phi_ip ip.b |> | l | l ∈ {l1; l2} }) ∧
+  (instr_next_ips (Invoke _ _ _ _ l1 l2) ip =
+    { <| f := ip.f; b := Some l; i := Phi_ip ip.b |> | l | l ∈ {l1; l2} }) ∧
+  (instr_next_ips Unreachable ip = {}) ∧
+  (instr_next_ips (Sub _ _ _ _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Extractvalue _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Insertvalue _ _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Alloca _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Load _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Store _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Gep _ _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Ptrtoint _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Inttoptr _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Icmp _ _ _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Call _ _ _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Cxa_allocate_exn _ _) ip = { inc_pc ip }) ∧
   (* TODO: revisit throw when dealing with exceptions *)
-  (next_ips (Cxa_throw _ _ _) ip = {  }) ∧
-  (next_ips (Cxa_begin_catch _ _) ip = { inc_pc ip }) ∧
-  (next_ips (Cxa_end_catch) ip = { inc_pc ip }) ∧
-  (next_ips (Cxa_get_exception_ptr _ _) ip = { inc_pc ip })
+  (instr_next_ips (Cxa_throw _ _ _) ip = {  }) ∧
+  (instr_next_ips (Cxa_begin_catch _ _) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Cxa_end_catch) ip = { inc_pc ip }) ∧
+  (instr_next_ips (Cxa_get_exception_ptr _ _) ip = { inc_pc ip })
+End
+
+Inductive next_ips:
+ (∀prog ip i l.
+    get_instr prog ip (Inl i) ∧
+    l ∈ instr_next_ips i ip
+    ⇒
+    next_ips prog ip l) ∧
+ (∀prog ip from_l phis.
+    get_instr prog ip (Inr (from_l, phis))
+    ⇒
+    next_ips prog ip (inc_pc ip))
 End
 
 (* The path is a list of program counters that represent a statically feasible
@@ -52,14 +64,13 @@ End
 Inductive good_path:
   (∀prog. good_path prog []) ∧
 
-  (∀ip i.
+  (∀prog ip i.
     get_instr prog ip i
     ⇒
     good_path prog [ip]) ∧
 
-  (∀prog path ip1 i1 ip2.
-    get_instr prog ip1 i1 ∧
-    ip2 ∈ next_ips i1 ip1 ∧
+  (∀prog path ip1 ip2.
+    ip2 ∈ next_ips prog ip1 ∧
     good_path prog (ip2::path)
     ⇒
     good_path prog (ip1::ip2::path))
@@ -71,65 +82,102 @@ Definition arg_to_regs_def:
 End
 
 (* The registers that an instruction uses *)
-Definition uses_def:
-  (uses (Ret (_, a)) = arg_to_regs a) ∧
-  (uses (Br a _ _) = arg_to_regs a) ∧
-  (uses (Invoke _ _ a targs _ _) =
+Definition instr_uses_def:
+  (instr_uses (Ret (_, a)) = arg_to_regs a) ∧
+  (instr_uses (Br a _ _) = arg_to_regs a) ∧
+  (instr_uses (Invoke _ _ a targs _ _) =
     arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
-  (uses Unreachable = {}) ∧
-  (uses (Sub _ _ _ _ a1 a2) =
+  (instr_uses Unreachable = {}) ∧
+  (instr_uses (Sub _ _ _ _ a1 a2) =
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
-  (uses (Extractvalue _ (_, a) _) = arg_to_regs a) ∧
-  (uses (Insertvalue _ (_, a1) (_, a2) _) =
+  (instr_uses (Extractvalue _ (_, a) _) = arg_to_regs a) ∧
+  (instr_uses (Insertvalue _ (_, a1) (_, a2) _) =
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
-  (uses (Alloca _ _ (_, a)) = arg_to_regs a) ∧
-  (uses (Load _ _ (_, a)) = arg_to_regs a) ∧
-  (uses (Store (_, a1) (_, a2)) =
+  (instr_uses (Alloca _ _ (_, a)) = arg_to_regs a) ∧
+  (instr_uses (Load _ _ (_, a)) = arg_to_regs a) ∧
+  (instr_uses (Store (_, a1) (_, a2)) =
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
-  (uses (Gep _ _ (_, a) targs) =
+  (instr_uses (Gep _ _ (_, a) targs) =
     arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
-  (uses (Ptrtoint _ (_, a) _) = arg_to_regs a) ∧
-  (uses (Inttoptr _ (_, a) _) = arg_to_regs a) ∧
-  (uses (Icmp _ _ _ a1 a2) =
+  (instr_uses (Ptrtoint _ (_, a) _) = arg_to_regs a) ∧
+  (instr_uses (Inttoptr _ (_, a) _) = arg_to_regs a) ∧
+  (instr_uses (Icmp _ _ _ a1 a2) =
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
-  (uses (Call _ _ _ targs) =
+  (instr_uses (Call _ _ _ targs) =
     BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
-  (uses (Cxa_allocate_exn _ a) = arg_to_regs a) ∧
-  (uses (Cxa_throw a1 a2 a3) =
+  (instr_uses (Cxa_allocate_exn _ a) = arg_to_regs a) ∧
+  (instr_uses (Cxa_throw a1 a2 a3) =
     arg_to_regs a1 ∪ arg_to_regs a2 ∪ arg_to_regs a3) ∧
-  (uses (Cxa_begin_catch _ a) = arg_to_regs a) ∧
-  (uses (Cxa_end_catch) = {  }) ∧
-  (uses (Cxa_get_exception_ptr _ a) = arg_to_regs a)
+  (instr_uses (Cxa_begin_catch _ a) = arg_to_regs a) ∧
+  (instr_uses (Cxa_end_catch) = {  }) ∧
+  (instr_uses (Cxa_get_exception_ptr _ a) = arg_to_regs a)
+End
+
+Definition phi_uses_def:
+  phi_uses from_l (Phi _ _ entries) =
+    case alookup entries from_l of
+    | None => {}
+    | Some a => arg_to_regs a
+End
+
+Inductive uses:
+ (∀prog ip i r.
+    get_instr prog ip (Inl i) ∧
+    r ∈ instr_uses i
+    ⇒
+    uses prog ip r) ∧
+ (∀prog ip from_l phis r.
+   get_instr prog ip (Inr (from_l, phis)) ∧
+    r ∈ BIGUNION (set (map (phi_uses from_l) phis))
+    ⇒
+    uses prog ip r)
 End
 
 (* The registers that an instruction assigns *)
-Definition assigns_def:
-  (assigns (Invoke r _ _ _ _ _) = {r}) ∧
-  (assigns (Sub r _ _ _ _ _) = {r}) ∧
-  (assigns (Extractvalue r _ _) = {r}) ∧
-  (assigns (Insertvalue r _ _ _) = {r}) ∧
-  (assigns (Alloca r _ _) = {r}) ∧
-  (assigns (Load r _ _) = {r}) ∧
-  (assigns (Gep r _ _ _) = {r}) ∧
-  (assigns (Ptrtoint r _ _) = {r}) ∧
-  (assigns (Inttoptr r _ _) = {r}) ∧
-  (assigns (Icmp r _ _ _ _) = {r}) ∧
-  (assigns (Call r _ _ _) = {r}) ∧
-  (assigns (Cxa_allocate_exn r _) = {r}) ∧
-  (assigns (Cxa_begin_catch r _) = {r}) ∧
-  (assigns (Cxa_get_exception_ptr r _) = {r}) ∧
-  (assigns _ = {})
+Definition instr_assigns_def:
+  (instr_assigns (Invoke r _ _ _ _ _) = {r}) ∧
+  (instr_assigns (Sub r _ _ _ _ _) = {r}) ∧
+  (instr_assigns (Extractvalue r _ _) = {r}) ∧
+  (instr_assigns (Insertvalue r _ _ _) = {r}) ∧
+  (instr_assigns (Alloca r _ _) = {r}) ∧
+  (instr_assigns (Load r _ _) = {r}) ∧
+  (instr_assigns (Gep r _ _ _) = {r}) ∧
+  (instr_assigns (Ptrtoint r _ _) = {r}) ∧
+  (instr_assigns (Inttoptr r _ _) = {r}) ∧
+  (instr_assigns (Icmp r _ _ _ _) = {r}) ∧
+  (instr_assigns (Call r _ _ _) = {r}) ∧
+  (instr_assigns (Cxa_allocate_exn r _) = {r}) ∧
+  (instr_assigns (Cxa_begin_catch r _) = {r}) ∧
+  (instr_assigns (Cxa_get_exception_ptr r _) = {r}) ∧
+  (instr_assigns _ = {})
+End
+
+Definition phi_assigns_def:
+  phi_assigns (Phi r _ _) = {r}
+End
+
+Inductive assigns:
+ (∀prog ip i r.
+    get_instr prog ip (Inl i) ∧
+    r ∈ instr_assigns i
+    ⇒
+    assigns prog ip r) ∧
+ (∀prog ip from_l phis r.
+    get_instr prog ip (Inr (from_l, phis)) ∧
+    r ∈ BIGUNION (set (map phi_assigns phis))
+    ⇒
+    assigns prog ip r)
 End
 
 Definition live_def:
-  live prog ip ⇔
-    { r | ∃path instr.
+  live prog ip =
+    { r | ∃path.
             good_path prog (ip::path) ∧
-            get_instr prog (last (ip::path)) instr ∧
-            r ∈ uses instr ∧
-            ∀ip2 instr2. ip2 ∈ set (front (ip::path)) ∧ get_instr prog ip2 instr2 ⇒ r ∉ assigns instr2 }
+            r ∈ uses prog (last (ip::path)) ∧
+            ∀ip2. ip2 ∈ set (front (ip::path)) ⇒ r ∉ assigns prog ip2 }
 End
 
+(*
 Theorem get_instr_live:
   ∀prog ip instr.
     get_instr prog ip instr
@@ -140,6 +188,7 @@ Proof
   qexists_tac `[]` >> rw [Once good_path_cases] >>
   qexists_tac `instr` >> simp [] >> metis_tac [IN_DEF]
 QED
+*)
 
 Triviality set_rw:
   !s P. (!x. x ∈ s ⇔ P x) ⇔ s = P
@@ -148,28 +197,24 @@ Proof
 QED
 
 Theorem live_gen_kill:
-  ∀prog ip instr ip'.
-    get_instr prog ip instr
-    ⇒
-    live prog ip = BIGUNION {live prog ip' | ip' ∈ next_ips instr ip} DIFF assigns instr ∪ uses instr
+  ∀prog ip ip'.
+    live prog ip =
+    BIGUNION {live prog ip' | ip' | ip' ∈ next_ips prog ip} DIFF assigns prog ip ∪ uses prog ip
 Proof
   rw [live_def, EXTENSION] >> eq_tac >> rw []
   >- (
-    Cases_on `path` >> fs []
-    >- metis_tac [get_instr_func] >>
+    Cases_on `path` >> fs [] >>
     rename1 `ip::ip2::path` >>
     qpat_x_assum `good_path _ _` mp_tac >> simp [Once good_path_cases] >> rw [] >>
-    Cases_on `x ∈ uses instr` >> fs [] >> simp [set_rw, PULL_EXISTS] >>
-    qexists_tac `ip2` >> qexists_tac `path` >> qexists_tac `instr'` >> rw [] >>
-    metis_tac [get_instr_func])
+    Cases_on `x ∈ uses prog ip` >> fs [] >> simp [set_rw, PULL_EXISTS] >>
+    qexists_tac `ip2` >> qexists_tac `path` >> rw [])
   >- (
     fs [] >>
-    qexists_tac `ip'::path` >> qexists_tac `instr'` >> rw []
-    >- (simp [Once good_path_cases] >> metis_tac []) >>
-    metis_tac [get_instr_func])
+    qexists_tac `ip'::path` >> rw [] >>
+    simp [Once good_path_cases])
   >- (
-    qexists_tac `[]` >> qexists_tac `instr` >> rw [] >>
-    simp [Once good_path_cases] >>
+    qexists_tac `[]` >> rw [] >>
+    fs [Once good_path_cases, uses_cases, IN_DEF] >>
     metis_tac [])
 QED
 
diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml
index 895453b61..a5f199b78 100644
--- a/sledge/semantics/llvm_propScript.sml
+++ b/sledge/semantics/llvm_propScript.sml
@@ -293,19 +293,20 @@ QED
 Theorem get_instr_func:
   ∀p ip i1 i2. get_instr p ip i1 ∧ get_instr p ip i2 ⇒ i1 = i2
 Proof
-  rw [get_instr_cases] >>
-  metis_tac [optionTheory.SOME_11]
+  rw [get_instr_cases] >> fs [] >> rw [] >> fs [] >> rw [] >> fs []
 QED
 
 Theorem inc_pc_invariant:
-  ∀p s i. prog_ok p ∧ get_instr p s.ip i ∧ ¬terminator i ∧ state_invariant p s ⇒ state_invariant p (inc_pc s)
+  ∀p s i. prog_ok p ∧ get_instr p s.ip (Inl i) ∧ ¬terminator i ∧ state_invariant p s ⇒ state_invariant p (inc_pc s)
 Proof
   rw [state_invariant_def, inc_pc_def, allocations_ok_def, globals_ok_def,
-      stack_ok_def, frame_ok_def, heap_ok_def, EVERY_EL, ip_ok_def]
+      stack_ok_def, frame_ok_def, heap_ok_def, EVERY_EL, ip_ok_def, inc_bip_def,
+      METIS_PROVE [] ``x ∨ y ⇔ ~x ⇒ y``]
   >- (
     qexists_tac `dec` >> qexists_tac `block'` >> rw [] >>
     fs [prog_ok_def, get_instr_cases] >> res_tac >> rw [] >>
-    `s.ip.i ≠ length block'.body - 1` suffices_by decide_tac >>
+    Cases_on `s.ip.i` >> fs [] >> rw [] >> fs [inc_bip_def] >>
+    `idx ≠ length block'.body - 1` suffices_by decide_tac >>
     CCONTR_TAC >> fs [] >> rfs [LAST_EL, PRE_SUB1]) >>
   metis_tac []
 QED
@@ -327,7 +328,8 @@ Theorem allocate_invariant:
   ∀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 [state_invariant_def, ip_ok_def, globals_ok_def, stack_ok_def]
+  rw [state_invariant_def, ip_ok_def, globals_ok_def, stack_ok_def,
+      METIS_PROVE [] ``x ∨ y ⇔ ~x ⇒ y``]
   >- metis_tac [allocate_heap_ok]
   >- (fs [is_allocated_def] >> metis_tac [allocate_unchanged, SUBSET_DEF])
   >- (
@@ -347,9 +349,15 @@ Proof
   >- (fs [stack_ok_def, EVERY_EL, frame_ok_def, set_bytes_unchanged])
 QED
 
+Triviality not_none_eq:
+  !x. x ≠ None ⇔ ?y. x = Some y
+Proof
+  Cases >> rw []
+QED
+
 Theorem step_instr_invariant:
   ∀i l s2.
-    step_instr p s1 i l s2 ⇒ prog_ok p ∧ get_instr p s1.ip i ∧ state_invariant p s1
+    step_instr p s1 i l s2 ⇒ prog_ok p ∧ get_instr p s1.ip (Inl i) ∧ state_invariant p s1
     ⇒
     state_invariant p s2
 Proof
@@ -384,17 +392,39 @@ Proof
   >- ( (* Br *)
     fs [state_invariant_def] >> rw []
     >- (
-      rw [ip_ok_def] >> fs [prog_ok_def, NOT_NIL_EQ_LENGTH_NOT_0] >>
+      rw [ip_ok_def] >> fs [prog_ok_def] >>
       qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >>
-      last_x_assum drule >> disch_then drule >> fs [])
+      fs [get_instr_cases] >>
+      last_x_assum drule >> disch_then drule >> fs [] >> rw [] >>
+      `terminator (el idx b.body)` by metis_tac [terminator_def] >>
+      `last b.body = el idx b.body`
+      by (
+        Cases_on `idx = PRE (length b.body)` >> fs [EL_PRE_LENGTH] >>
+        `Suc idx < length b.body` by decide_tac >>
+        drule mem_el_front >> rw [] >> fs [EVERY_MEM] >>
+        metis_tac []) >>
+      qpat_x_assum `Br _ _ _ = _` (assume_tac o GSYM) >> fs [] >>
+      fs [instr_to_labs_def, not_none_eq] >>
+      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] >>
+      rw [ip_ok_def] >> fs [prog_ok_def] >>
       qpat_x_assum `alookup _ (Fn "main") = _` kall_tac >>
-      last_x_assum drule >> disch_then drule >> fs [])
+      fs [get_instr_cases] >>
+      last_x_assum drule >> disch_then drule >> fs [] >> rw [] >>
+      `terminator (el idx b.body)` by metis_tac [terminator_def] >>
+      `last b.body = el idx b.body`
+      by (
+        Cases_on `idx = PRE (length b.body)` >> fs [EL_PRE_LENGTH] >>
+        `Suc idx < length b.body` by decide_tac >>
+        drule mem_el_front >> rw [] >> fs [EVERY_MEM] >>
+        metis_tac []) >>
+      qpat_x_assum `Br _ _ _ = _` (assume_tac o GSYM) >> fs [] >>
+      fs [instr_to_labs_def, not_none_eq] >>
+      metis_tac [])
     >- (fs [globals_ok_def] >> metis_tac [])
     >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
   >- (
@@ -438,21 +468,40 @@ Proof
     >- (
       fs [state_invariant_def, stack_ok_def] >> rw []
       >- (
-        rw [frame_ok_def] >> fs [ip_ok_def, prog_ok_def] >>
+        rw [frame_ok_def] >> fs [ip_ok_def, prog_ok_def, inc_bip_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] >>
+        Cases_on `length block'.body = idx + 1` >> fs [PRE_SUB1] >>
         fs [get_instr_cases] >>
         metis_tac [terminator_def])
       >- (fs [EVERY_MEM, frame_ok_def] >> metis_tac [])))
 QED
 
+Theorem step_invariant:
+  ∀p s1 l s2.
+    prog_ok p ∧ step p s1 l s2 ∧ state_invariant p s1
+    ⇒
+    state_invariant p s2
+Proof
+  rw [step_cases]
+  >- metis_tac [step_instr_invariant] >>
+  fs [get_instr_cases, inc_pc_def, inc_bip_def, state_invariant_def] >>
+  rw []
+  >- (
+    fs [ip_ok_def, prog_ok_def] >>
+    metis_tac [NOT_NIL_EQ_LENGTH_NOT_0])
+  >- (fs [globals_ok_def] >> metis_tac [])
+  >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac [])
+QED
+
 Theorem exit_no_step:
-  !p s1. get_instr p s1.ip Exit ⇒ ¬?l s2. step p s1 l s2
+  !p s1. get_instr p s1.ip (Inl Exit) ⇒ ¬?l s2. step p s1 l s2
 Proof
-  rw [step_cases, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
-  `i = Exit` by metis_tac [get_instr_func] >>
-  rw [step_instr_cases]
+  rw [step_cases, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``]
+  >- (
+    `i = Exit` by metis_tac [get_instr_func, sumTheory.INL_11] >>
+    rw [step_instr_cases]) >>
+  metis_tac [get_instr_func, sumTheory.sum_distinct]
 QED
 
 Definition is_call_def:
@@ -461,13 +510,17 @@ Definition is_call_def:
 End
 
 Theorem step_same_block:
-  ∀p s1 l s2 i.
-    get_instr p s1.ip i ∧ step_instr p s1 i l s2 ∧ ¬terminator i ∧ ~is_call i⇒
+  ∀p s1 l s2.
+    get_instr p s1.ip i ∧ step p s1 l s2 ∧
+    (∀i'. i = Inl i' ⇒ ¬terminator i' ∧ ¬is_call i') ⇒
     s1.ip.f = s2.ip.f ∧
     s1.ip.b = s2.ip.b ∧
-    s2.ip.i = s1.ip.i + 1
+    s2.ip.i = inc_bip s1.ip.i
 Proof
-  rw [step_instr_cases] >>
+  simp [step_cases] >>
+  rpt gen_tac >> disch_tac >> fs [inc_pc_def] >>
+  `i = Inl i'` by metis_tac [get_instr_func] >>
+  fs [step_instr_cases] >> rfs [] >>
   fs [terminator_def, is_call_def, inc_pc_def, update_result_def]
 QED
 
@@ -488,10 +541,13 @@ Definition last_step_def:
   last_step p s1 l s2 ⇔
    ∃i.
      step p s1 l s2 ∧ get_instr p s1.ip i ∧
-     (terminator i ∨ is_call i ∨ ¬∃l s3. step p s2 l s3)
+     ((∃x. i = Inr x) ∨
+      (∃i'. i = Inl i' ∧ (terminator i' ∨ is_call i')) ∨
+      ¬∃l s3. step p s2 l s3)
 End
 
-(* Run all of the instructions up-to-and-including the next Call or terminator
+(* Run all of the instructions up-to-and-including the next Call or terminator.
+ * Stop after the phis too.
  * *)
 Inductive multi_step:
 
@@ -502,7 +558,7 @@ Inductive multi_step:
 
   (∀p s1 s2 s3 i l ls.
    step p s1 l s2 ∧
-   get_instr p s1.ip i ∧
+   get_instr p s1.ip (Inl i) ∧
    ¬(terminator i ∨ is_call i) ∧
    multi_step p s2 ls s3
    ⇒
@@ -598,7 +654,10 @@ Definition instrs_left_def:
     | Some d =>
       case alookup d.blocks s.ip.b of
       | None => 0
-      | Some b => length b.body - s.ip.i
+      | Some b =>
+        case s.ip.i of
+        | Phi_ip _ => length b.body + 1
+        | Offset idx => length b.body - idx
 End
 
 Theorem extend_step_path:
@@ -635,8 +694,8 @@ Proof
       fs [finite_length] >>
       qexists_tac `n` >> rw []
       >- (
-        rw [last_step_def] >> fs [step_cases] >>
-        metis_tac []) >>
+        qpat_x_assum `step _ _ _ _` mp_tac >>
+        rw [last_step_def, step_cases] >> metis_tac []) >>
       `length (plink p' (pcons (last p') l (stopped_at s))) = Some (n + Suc 1 - 1)`
       by metis_tac [length_plink, alt_length_thm, optionTheory.OPTION_MAP_DEF] >>
       rw []
@@ -668,11 +727,10 @@ Proof
     pop_assum mp_tac >> simp [] >>
     `?i. get_instr p s2.ip i` by metis_tac [get_instr_cases, step_cases] >>
     disch_then (qspec_then `i` mp_tac) >> simp [] >>
-    pop_assum mp_tac >> pop_assum mp_tac >> simp [Once step_cases] >>
-    rw [] >>
-    `i' = i` by metis_tac [get_instr_func] >> rw [] >>
     drule step_same_block >> disch_then drule >> simp [] >>
-    rw [] >> fs [step_cases, get_instr_cases]) >>
+    pop_assum mp_tac >> pop_assum mp_tac >> simp [Once step_cases] >>
+    rw [] >> fs [get_instr_cases, inc_bip_def] >> rw [] >> fs [] >>
+    rw [inc_bip_def] >> fs []) >>
  `last path = first path1`
   by (
     unabbrev_all_tac >> simp [Once unfold_thm] >>
diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml
index 18515eff3..a17ff8e9e 100644
--- a/sledge/semantics/miscScript.sml
+++ b/sledge/semantics/miscScript.sml
@@ -123,6 +123,19 @@ Proof
   fs [INJ_IFF] >> metis_tac []
 QED
 
+Theorem is_prefix_subset:
+  ∀l1 l2. l1 ≼ l2 ⇒ set l1 ⊆ set l2
+Proof
+  Induct_on `l1` >> rw [] >>
+  Cases_on `l2` >> fs [SUBSET_DEF]
+QED
+
+Theorem mem_el_front:
+  ∀n l. Suc n < length l ⇒ mem (el n l) (front l)
+Proof
+  Induct >> rw [] >> Cases_on `l` >> fs [FRONT_DEF] >> rw [] >> fs []
+QED
+
 (* ----- Theorems about log ----- *)
 
 Theorem mul_div_bound:
diff --git a/sledge/semantics/settingsScript.sml b/sledge/semantics/settingsScript.sml
index 21b8e0464..95726c64c 100644
--- a/sledge/semantics/settingsScript.sml
+++ b/sledge/semantics/settingsScript.sml
@@ -56,5 +56,8 @@ overload_on ("foldl", ``FOLDL``);
 overload_on ("foldr", ``FOLDR``);
 overload_on ("option_rel", ``OPTREL``);
 overload_on ("front", ``FRONT``);
+overload_on ("Inl", ``INL``);
+overload_on ("Inr", ``INR``);
+overload_on ("mem", ``MEM``);
 
 export_theory ();