diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml
index 36d04ba55..72daf7d43 100644
--- a/sledge/semantics/llairScript.sml
+++ b/sledge/semantics/llairScript.sml
@@ -94,7 +94,7 @@ Datatype:
   | Return exp
   | Throw exp
   | Unreachable
-  | Exit
+  | Exit exp
 End
 
 Datatype:
@@ -473,7 +473,10 @@ Inductive step_term:
         stack := rest;
         heap := s.heap |>) ∧
 
-  (∀prog s. step_term prog s Exit (s with status := Complete))
+  (∀prog s e i size.
+   eval_exp s e (FlatV (IntV i size))
+   ⇒
+   step_term prog s (Exit e) (s with status := Complete i))
   (* TODO Throw *)
 
 End
@@ -487,7 +490,6 @@ Inductive step_block:
    ⇒
    step_block prog s1 [] [] t s2) ∧
 
-
   (∀prog s1 i1 i2 l1 is t s2.
    step_inst s1 i1 l1 s2 ∧
    (¬?l2 s3. step_inst s2 i2 l2 s3)
diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml
index 491fd3054..ffe8ac3e0 100644
--- a/sledge/semantics/llvmScript.sml
+++ b/sledge/semantics/llvmScript.sml
@@ -90,7 +90,7 @@ Datatype:
   | Br arg label label
   | Invoke reg ty arg (targ list) label label
   | Unreachable
-  | Exit
+  | Exit arg
   (* Non-terminators *)
   | Sub reg bool bool ty arg arg
   | Extractvalue reg targ (const list)
@@ -144,7 +144,7 @@ Definition terminator_def:
   (terminator (Br _ _ _) ⇔ T) ∧
   (terminator (Invoke _ _ _ _ _ _) ⇔ T) ∧
   (terminator Unreachable ⇔ T) ∧
-  (terminator Exit ⇔ T) ∧
+  (terminator (Exit _) ⇔ T) ∧
   (terminator (Cxa_throw _ _ _) ⇔ T) ∧
   (terminator _ ⇔ F)
 End
@@ -196,7 +196,8 @@ Datatype:
        globals : glob_var |-> (num # word64);
        locals : reg |-> pv;
        stack : frame list;
-       heap : bool heap |>
+       heap : bool heap;
+       exited : int option |>
 End
 
 (* ----- Things about types ----- *)
@@ -524,6 +525,13 @@ Inductive step_instr:
   (* TODO *)
   (step_instr prog s (Invoke r t a args l1 l2) Tau s) ∧
 
+  (eval s a = Some v1 ∧
+  signed_v_to_int v1.value = Some exit_code
+   ⇒
+   step_instr prog s
+     (Exit a) Tau
+     (s with exited := Some (exit_code))) ∧
+
   (eval s a1 = Some v1 ∧
    eval s a2 = Some v2 ∧
    do_sub nuw nsw v1 v2 t = Some v3
@@ -677,6 +685,7 @@ End
 
 Inductive step:
  (get_instr p s.ip (Inl i) ∧
+  s.exited = None ∧
   step_instr p s i l s'
   ⇒
   step p s l s') ∧
@@ -693,6 +702,7 @@ Inductive step:
  * %r1 = phi [0, %l]
  *)
  (get_instr p s.ip (Inr (from_l, phis)) ∧
+  s.exited = None ∧
   map (do_phi from_l s) phis = map Some updates
   ⇒
   step p s Tau (inc_pc (s with locals := locals |++ updates)))
@@ -701,8 +711,8 @@ End
 
 Definition get_observation_def:
   get_observation prog last_s =
-    if get_instr prog last_s.ip (Inl Exit) then
-      Complete
+    if last_s.exited ≠ None then
+      Complete (THE last_s.exited)
     else if ∃s l. step prog last_s l s then
       Partial
     else
@@ -799,6 +809,7 @@ Definition is_init_state_def:
     s.ip.i = Offset 0 ∧
     s.locals = fempty ∧
     s.stack = [] ∧
+    s.exited = None ∧
     globals_ok s ∧
     heap_ok s.heap ∧
     fdom s.globals = fdom global_init ∧
diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml
index 7175ed739..6ba346fb1 100644
--- a/sledge/semantics/llvm_propScript.sml
+++ b/sledge/semantics/llvm_propScript.sml
@@ -427,6 +427,10 @@ Proof
       metis_tac [])
     >- (fs [globals_ok_def] >> metis_tac [])
     >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
+  >- (
+    fs [state_invariant_def, globals_ok_def, stack_ok_def, frame_ok_def,
+        EVERY_MEM] >>
+    metis_tac [])
   >- (
     irule inc_pc_invariant >> rw [get_instr_update, update_invariant]>>
     metis_tac [terminator_def])
@@ -495,13 +499,9 @@ Proof
 QED
 
 Theorem exit_no_step:
-  !p s1. get_instr p s1.ip (Inl Exit) ⇒ ¬?l s2. step p s1 l s2
+  !p s1. s1.exited ≠ None ⇒ ¬?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, sumTheory.INL_11] >>
-    rw [step_instr_cases]) >>
-  metis_tac [get_instr_func, sumTheory.sum_distinct]
 QED
 
 Definition is_call_def:
diff --git a/sledge/semantics/llvm_ssaScript.sml b/sledge/semantics/llvm_ssaScript.sml
index 6a10ba79a..55c735939 100644
--- a/sledge/semantics/llvm_ssaScript.sml
+++ b/sledge/semantics/llvm_ssaScript.sml
@@ -31,7 +31,7 @@ Definition instr_next_ips_def:
   (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 Exit ip = {}) ∧
+  (instr_next_ips (Exit _) 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 }) ∧
diff --git a/sledge/semantics/llvm_to_llairScript.sml b/sledge/semantics/llvm_to_llairScript.sml
index 9c5d255fd..d37975f88 100644
--- a/sledge/semantics/llvm_to_llairScript.sml
+++ b/sledge/semantics/llvm_to_llairScript.sml
@@ -219,7 +219,7 @@ Definition classify_instr_def:
   (classify_instr (Br _ _ _) = Term) ∧
   (classify_instr (Invoke _ _ _ _ _ _) = Term) ∧
   (classify_instr Unreachable = Term) ∧
-  (classify_instr Exit = Term) ∧
+  (classify_instr (Exit _) = Term) ∧
   (classify_instr (Load _ _ _) = Non_exp) ∧
   (classify_instr (Store _ _) = Non_exp) ∧
   (classify_instr (Cxa_throw _ _ _) = Non_exp) ∧
diff --git a/sledge/semantics/llvm_to_llair_propScript.sml b/sledge/semantics/llvm_to_llair_propScript.sml
index 30b91d316..a8759aab7 100644
--- a/sledge/semantics/llvm_to_llair_propScript.sml
+++ b/sledge/semantics/llvm_to_llair_propScript.sml
@@ -74,6 +74,12 @@ Definition untranslate_reg_def:
   untranslate_reg (Var_name x t) = Reg x
 End
 
+Inductive complete_trace_rel:
+  (∀i. complete_trace_rel (Some i) (Complete i)) ∧
+  (complete_trace_rel None Partial) ∧
+  (complete_trace_rel None Stuck)
+End
+
 (* Define when an LLVM state is related to a llair one.
  * Parameterised on a map for locals relating LLVM registers to llair
  * expressions that compute the value in that register. This corresponds to part
@@ -94,7 +100,7 @@ Definition mem_state_rel_def:
           ∃ip2. untranslate_reg r' ∈ assigns prog ip2 ∧ dominates prog ip2 ip1))) ∧
     reachable prog s.ip ∧
     erase_tags s.heap = s'.heap ∧
-    s'.status = get_observation prog s
+    complete_trace_rel s.exited s'.status
 End
 
 (* Define when an LLVM state is related to a llair one
@@ -105,7 +111,8 @@ End
 Definition state_rel_def:
   state_rel prog emap (s:llvm$state) (s':llair$state) ⇔
     pc_rel prog emap s.ip s'.bp ∧
-    mem_state_rel prog emap s s'
+    mem_state_rel prog emap s s' ∧
+    s'.status = get_observation prog s
 End
 
 Theorem mem_state_ignore_bp:
@@ -132,7 +139,6 @@ Proof
     first_x_assum (qspec_then `r` mp_tac) >> simp [Once live_gen_kill, PULL_EXISTS] >>
     metis_tac [next_ips_same_func])
   >- metis_tac [next_ips_reachable]
-  >- cheat
 QED
 
 Theorem mem_state_rel_update:
@@ -170,7 +176,6 @@ Proof
     simp [Once live_gen_kill, PULL_EXISTS, METIS_PROVE [] ``x ∨ y ⇔ (~y ⇒ x)``] >>
     metis_tac [])
   >- metis_tac [next_ips_reachable]
-  >- cheat
 QED
 
 Theorem mem_state_rel_update_keep:
@@ -224,7 +229,6 @@ Proof
       first_x_assum irule >> rw [] >>
       metis_tac [next_ips_same_func]))
   >- metis_tac [next_ips_reachable]
-  >- cheat
 QED
 
 Theorem v_rel_bytes:
@@ -267,6 +271,7 @@ Proof
     simp [v_rel_cases, PULL_EXISTS, MAP_MAP_o] >>
     fs [combinTheory.o_DEF, pairTheory.LAMBDA_PROD] >>
     metis_tac [])
+  (* TODO: unimplemented stuff *)
   >- cheat
   >- cheat
   >- cheat
@@ -290,6 +295,7 @@ Proof
   TRY pairarg_tac >> fs []
   >- metis_tac []
   >- metis_tac [] >>
+  (* TODO: unimplemented stuff *)
   cheat
 QED
 
@@ -488,8 +494,7 @@ QED
 
 Theorem translate_instr_to_exp_correct:
   ∀emap instr r t s1 s1' s2 prog l.
-    is_ssa prog ∧
-    prog_ok prog ∧
+    is_ssa prog ∧ prog_ok prog ∧
     classify_instr instr = Exp r t ∧
     mem_state_rel prog emap s1 s1' ∧
     get_instr prog s1.ip (Inl instr) ∧
@@ -528,17 +533,18 @@ Proof
     >- (
       simp [step_inst_cases, PULL_EXISTS] >>
       qexists_tac `res_v` >> rw []
-      >- simp [inc_pc_def, llvmTheory.inc_pc_def] >>
-      rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
-      simp [llvmTheory.inc_pc_def] >>
-      irule mem_state_rel_update_keep >> rw []
-      >- rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def]
+      >- simp [inc_pc_def, llvmTheory.inc_pc_def]
       >- (
-        drule prog_ok_nonterm >>
-        simp [get_instr_cases, PULL_EXISTS] >>
-        ntac 3 (disch_then drule) >>
-        simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def])
-      >- fs [mem_state_rel_def])
+        rw [update_results_def, GSYM FUPDATE_EQ_FUPDATE_LIST] >>
+        simp [llvmTheory.inc_pc_def] >>
+        irule mem_state_rel_update_keep >> rw []
+        >- rw [assigns_cases, EXTENSION, IN_DEF, get_instr_cases, instr_assigns_def]
+        >- (
+          drule prog_ok_nonterm >>
+          simp [get_instr_cases, PULL_EXISTS] >>
+          ntac 3 (disch_then drule) >>
+          simp [terminator_def, next_ips_cases, IN_DEF, inc_pc_def])
+        >- fs [mem_state_rel_def]))
     >- rw [inc_pc_def, llvmTheory.inc_pc_def]
     >- (
       simp [llvmTheory.inc_pc_def] >>
@@ -580,6 +586,7 @@ Proof
       simp [step_inst_cases, PULL_EXISTS] >>
       qexists_tac `res_v` >> rw [] >>
       rw [update_results_def] >>
+      (* TODO: unfinished *)
       cheat)
     >- cheat) >>
   conj_tac
@@ -611,6 +618,7 @@ Proof
       simp [step_inst_cases, PULL_EXISTS] >>
       qexists_tac `res_v` >> rw [] >>
       rw [update_results_def] >>
+      (* TODO: unfinished *)
       cheat)
     >- cheat) >>
   cheat
@@ -741,6 +749,17 @@ Proof
   metis_tac [un_translate_glob_inv]
 QED
 
+Theorem take_to_call_lem:
+  ∀i idx body.
+    idx < length body ∧ el idx body = i ∧ ¬terminator i ∧ ¬is_call i ⇒
+    take_to_call (drop idx body) = i :: take_to_call (drop (idx + 1) body)
+Proof
+  Induct_on `idx` >> rw []
+  >- (Cases_on `body` >> fs [take_to_call_def] >> rw []) >>
+  Cases_on `body` >> fs [] >>
+  first_x_assum drule >> simp [ADD1]
+QED
+
 Theorem translate_instrs_correct1:
   ∀prog s1 tr s2.
     multi_step prog s1 tr s2 ⇒
@@ -839,8 +858,9 @@ Proof
               `s1'.locals = s3.locals` by fs [Abbr `s3`] >>
               metis_tac [eval_exp_ignores]))
           >- cheat
-          >- (
-            cheat)))
+          >- cheat)
+        >- (
+          cheat))
       >- ( (* Invoke *)
         cheat)
       >- ( (* Unreachable *)
@@ -872,7 +892,9 @@ Proof
       rename1 `state_rel prog emap3 s3 s3'` >>
       qexists_tac `emap3` >> qexists_tac `s3'` >> rw [] >>
       `take_to_call (drop idx b.body) = i :: take_to_call (drop (idx + 1) b.body)`
-      by cheat >>
+      by (
+        irule take_to_call_lem >> simp [] >>
+        fs [get_instr_cases]) >>
       simp [translate_instrs_def] >>
       Cases_on `r ∉ regs_to_keep` >> fs [] >> rw []
       >- metis_tac [] >>
@@ -898,6 +920,7 @@ Theorem multi_step_to_step_block:
 Proof
   rw [] >> pop_assum mp_tac >> simp [Once state_rel_def] >> rw [pc_rel_cases]
   >- (
+    (* Non-phi instruction *)
     drule translate_instrs_correct1 >> simp [] >>
     disch_then drule >>
     disch_then (qspecl_then [`regs_to_keep`, `types`] mp_tac) >> simp [] >>
@@ -905,13 +928,14 @@ Proof
     qexists_tac `s2'` >> simp [] >>
     ntac 3 HINT_EXISTS_TAC >>
     rw [] >> fs [dest_fn_def]) >>
-  (* Phi nodes *)
+  (* Phi instruction *)
   reverse (fs [Once multi_step_cases])
   >- metis_tac [get_instr_func, sumTheory.sum_distinct] >>
   qpat_x_assum `last_step _ _ _ _` mp_tac >>
   simp [last_step_def] >> simp [Once llvmTheory.step_cases] >>
   rw [] >> imp_res_tac get_instr_func >> fs [] >> rw [] >>
   fs [translate_trace_def] >>
+  (* TODO: unfinished *)
   cheat
 QED
 
@@ -1027,7 +1051,11 @@ Proof
     >- rw [MAP_MAP_o, combinTheory.o_DEF, un_translate_trace_inv] >>
     qexists_tac `path'` >> rw [] >>
     fs [IN_DEF, observation_prefixes_cases, toList_some] >> rw [] >>
-    `?labs. labels path' = fromList labs` by cheat >>
+    `?labs. labels path' = fromList labs`
+    by (
+      fs [GSYM finite_labels] >>
+      imp_res_tac llistTheory.LFINITE_toList >>
+      fs [toList_some]) >>
     fs [] >>
     rfs [lmap_fromList, combinTheory.o_DEF, MAP_MAP_o] >>
     simp [FILTER_FLAT, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF, FILTER_MAP]
@@ -1035,8 +1063,6 @@ Proof
     >- fs [state_rel_def, mem_state_rel_def] >>
     rename [`labels path' = fromList l'`, `labels path = fromList l`,
             `state_rel _ _ (last path) (last path')`, `lsub ≼ flat l`] >>
-    qexists_tac `map (translate_trace types) lsub` >>
-    fs [FILTER_MAP, trans_trace_not_tau] >>
     cheat)
 (*
     `INJ (translate_trace types) (set l2' ∪ set (flat l2)) UNIV`
diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml
index be4b799d7..df57ee0bc 100644
--- a/sledge/semantics/miscScript.sml
+++ b/sledge/semantics/miscScript.sml
@@ -30,12 +30,12 @@ End
 Datatype:
   trace_type =
   | Stuck
-  | Complete
+  | Complete int
   | Partial
 End
 
 Inductive observation_prefixes:
-  (∀l. observation_prefixes (Complete, l) (Complete, filter ($≠ Tau) l)) ∧
+  (∀l i. observation_prefixes (Complete i, l) (Complete i, filter ($≠ Tau) l)) ∧
   (∀l. observation_prefixes (Stuck, l) (Stuck, filter ($≠ Tau) l)) ∧
   (∀l1 l2 x.
     l2 ≼ l1 ∧ (l2 = l1 ⇒ x = Partial)