[sledge sem] Update LLVM and LLAIR sem for consistent stuckness

Summary:
Previously, the LLVM semantics could be stuck where the LLAIR semantics
was not yet stuck, but would become stuck (at the same place) after
taking a step. This was due to LLVM using the traditional definition of
stuck states: any state from which there are no transitions. However,
LLAIR cannot do that because it might get stuck in the middle of a block
that contains several visible stores. We don't want to consider the
whole block stuck, nor can we finish it. Thus, the LLAIR definition of
stuckness is when the state has the stuck flag set which happens when
stopping in the middle of a block after encountering a stuck
instruction. Now LLVM takes the same approach.

Reviewed By: jberdine

Differential Revision: D17855085

fbshipit-source-id: a094d25d5

sledge/semantics/llairScript.sml

@@ -433,7 +433,7 @@ Inductive step_term:
    Lab_name fname bname = (case alookup table idx of Some lab => lab | None => default)
    ⇒
    step_term prog s
-     (Switch e table default)
+     (Switch e table default) Tau
      (s with bp := Lab_name fname bname)) ∧
 
   (∀prog s e labs i idx idx_size.
@@ -441,7 +441,7 @@ Inductive step_term:
    idx < length labs
    ⇒
    step_term prog s
-     (Iswitch e labs)
+     (Iswitch e labs) Tau
      (s with bp := el i labs)) ∧
 
   (∀prog s v fname bname es t ret1 ret2 vals f.
@@ -450,7 +450,7 @@ Inductive step_term:
    list_rel (eval_exp s) es vals
    ⇒
    step_term prog s
-     (Call v (Lab_name fname bname) es t ret1 ret2)
+     (Call v (Lab_name fname bname) es t ret1 ret2) Tau
      <| bp := Lab_name fname bname;
         glob_addrs := s.glob_addrs;
         locals := alist_to_fmap (zip (f.params, vals));
@@ -466,7 +466,7 @@ Inductive step_term:
    s.stack = top::rest
    ⇒
    step_term prog s
-     (Return e)
+     (Return e) Tau
      <| bp := top.ret;
         glob_addrs := s.glob_addrs;
         locals := top.saved_locals |+ (top.ret_var, r);
@@ -476,7 +476,7 @@ Inductive step_term:
   (∀prog s e i size.
    eval_exp s e (FlatV (IntV i size))
    ⇒
-   step_term prog s (Exit e) (s with status := Complete i))
+   step_term prog s (Exit e) (Exit i) (s with status := Complete i))
   (* TODO Throw *)
 
 End
@@ -485,22 +485,26 @@ End
  * instruction pointer and do a big-step evaluation for each block *)
 Inductive step_block:
 
-  (∀prog s1 t s2.
-   step_term prog s1 t s2
+  (∀prog s1 t l s2.
+   step_term prog s1 t l s2
    ⇒
-   step_block prog s1 [] [] t s2) ∧
+   step_block prog s1 [] t [l] s2) ∧
 
-  (∀prog s1 i1 i2 l1 is t s2.
-   step_inst s1 i1 l1 s2 ∧
-   (¬?l2 s3. step_inst s2 i2 l2 s3)
+  (∀prog s1 t.
+   ¬(∃s2 (l:var obs). step_term prog s1 t l s2)
    ⇒
-   step_block prog s1 (i1::i2::is) [l1] t (s2 with status := Stuck)) ∧
+   step_block prog s1 [] t [Error] (s1 with status := Stuck)) ∧
+
+  (∀prog s1 i1 is t.
+   (¬∃l s2. step_inst s1 i1 l s2)
+   ⇒
+   step_block prog s1 (i1::is) t [Error] (s1 with status := Stuck)) ∧
 
   (∀prog s1 i l is ls t s2 s3.
    step_inst s1 i l s2 ∧
-   step_block prog s2 is ls t s3
+   step_block prog s2 is t ls s3
    ⇒
-   step_block prog s1 (i::is) (l::ls) t s3)
+   step_block prog s1 (i::is) t (l::ls) s3)
 
 End
 
@@ -516,7 +520,7 @@ End
 Inductive step:
   ∀prog s b ls s'.
     get_block prog s.bp b ∧
-    step_block prog s b.cmnd ls b.term s' ∧
+    step_block prog s b.cmnd b.term ls s' ∧
     s.status = Partial
     ⇒
     step prog s ls s'

sledge/semantics/llvmScript.sml

@@ -197,7 +197,7 @@ Datatype:
        locals : reg |-> pv;
        stack : frame list;
        heap : bool heap;
-       exited : int option |>
+       status : trace_type |>
 End
 
 (* ----- Things about types ----- *)
@@ -513,7 +513,8 @@ Inductive step_instr:
           globals := s.globals;
           locals := fr.saved_locals;
           stack := st;
-          heap := new_h |>)) ∧
+          heap := new_h;
+          status := s.status |>)) ∧
 
   (eval s a = Some <| poison := p; value := FlatV (W1V tf) |> ∧
    l = Some (if tf = 0w then l2 else l1)
@@ -529,8 +530,8 @@ Inductive step_instr:
   signed_v_to_int v1.value = Some exit_code
    ⇒
    step_instr prog s
-     (Exit a) Tau
-     (s with exited := Some (exit_code))) ∧
+     (Exit a) (Exit exit_code)
+     (s with status := Complete exit_code)) ∧
 
   (eval s a1 = Some v1 ∧
    eval s a2 = Some v2 ∧
@@ -651,7 +652,8 @@ Inductive step_instr:
              saved_locals := s.locals;
              result_var := r;
              stack_allocs := [] |> :: s.stack;
-        heap := s.heap |>)(* ∧
+        heap := s.heap;
+        status := s.status |>)(* ∧
 
   (* TODO *)
   (step_instr prog s (Cxa_allocate_exn r a) Tau s) ∧
@@ -685,7 +687,6 @@ 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') ∧
@@ -702,21 +703,20 @@ 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)))
-
 End
 
-Definition get_observation_def:
-  get_observation prog last_s =
-    if last_s.exited ≠ None then
-      Complete (THE last_s.exited)
-    else if ∃s l. step prog last_s l s then
-      Partial
-    else
-      Stuck
+Inductive sem_step:
+  (step p s1 l s2 ∧
+   s1.status = Partial
+   ⇒
+   sem_step p s1 l s2) ∧
+  ((¬∃l s2. step p s1 l s2) ∧
+   s1.status = Partial
+   ⇒
+   sem_step p s1 Error (s1 with status := Stuck))
 End
 
 (* The semantics of a program will be the finite traces of stores to global
@@ -724,8 +724,8 @@ End
  * *)
 Definition sem_def:
   sem p s1 =
-    { (get_observation p (last path), filter ($≠ Tau) l)  | (path, l) |
-      toList (labels path) = Some l ∧ finite path ∧ okpath (step p) path ∧ first path = s1 }
+    { ((last path).status, filter ($≠ Tau) l)  | (path, l) |
+      toList (labels path) = Some l ∧ finite path ∧ okpath (sem_step p) path ∧ first path = s1 }
 End
 
 (* ----- Invariants on state ----- *)
@@ -756,14 +756,15 @@ End
 Definition prog_ok_def:
   prog_ok p ⇔
     ((* All blocks end with terminators and terminators only appear at the end.
-      * All labels mentioned in instructions actually exist *)
+      * All labels mentioned in branches actually exist, and target non-entry
+      * blocks *)
      ∀fname dec bname block.
        alookup p fname = Some dec ∧
        alookup dec.blocks bname = Some block
        ⇒
        block.body ≠ [] ∧ terminator (last block.body) ∧
        every (λi. ¬terminator i) (front block.body) ∧
-       every (λlab. alookup dec.blocks (Some lab) ≠ None)
+       every (λlab. ∃b. alookup dec.blocks (Some lab) = Some b ∧ b.h ≠ Entry)
              (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)) ∧
@@ -809,7 +810,7 @@ Definition is_init_state_def:
     s.ip.i = Offset 0 ∧
     s.locals = fempty ∧
     s.stack = [] ∧
-    s.exited = None ∧
+    s.status = Partial ∧
     globals_ok s ∧
     heap_ok s.heap ∧
     fdom s.globals = fdom global_init ∧

sledge/semantics/llvm_propScript.sml

@@ -498,11 +498,13 @@ Proof
   >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac [])
 QED
 
+(* TODO: remove
 Theorem exit_no_step:
   !p s1. s1.exited ≠ None ⇒ ¬?l s2. step p s1 l s2
 Proof
   rw [step_cases, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``]
 QED
+*)
 
 Definition is_call_def:
   (is_call (Call _ _ _ _) ⇔ T) ∧
@@ -534,30 +536,33 @@ Proof
   >- rw [stack_ok_def]
 QED
 
-
 (* ----- A bigger-step semantics ----- *)
 
-Definition last_step_def:
-  last_step p s1 l s2 ⇔
-   ∃i.
+Inductive last_step:
+  (∀p s1 l s2 i.
     step p s1 l s2 ∧ get_instr p s1.ip i ∧
-     ((∃x. i = Inr x) ∨
-      (∃i'. i = Inl 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')))
+    ⇒
+    last_step p s1 l s2) ∧
+  (∀p s1.
+   (¬∃l s2. step p s1 l s2)
+   ⇒
+   last_step p s1 Error (s1 with status := Stuck))
 End
 
 (* Run all of the instructions up-to-and-including the next Call or terminator.
  * Stop after the phis too.
  * *)
 Inductive multi_step:
-
   (∀p s1 s2 l.
-   last_step p s1 l s2
+   last_step p s1 l s2 ∧
+   s1.status = Partial
    ⇒
    multi_step p s1 [l] s2) ∧
 
   (∀p s1 s2 s3 i l ls.
    step p s1 l s2 ∧
+   s1.status = Partial ∧
    get_instr p s1.ip (Inl i) ∧
    ¬(terminator i ∨ is_call i) ∧
    multi_step p s2 ls s3
@@ -567,7 +572,7 @@ End
 
 Definition multi_step_sem_def:
   multi_step_sem p s1 =
-    { l1 | ∃path l2. l1 ∈ observation_prefixes (get_observation p (last path), flat l2) ∧
+    { l1 | ∃path l2. l1 ∈ observation_prefixes ((last path).status, flat l2) ∧
            toList (labels path) = Some l2 ∧
            finite path ∧ okpath (multi_step p) path ∧ first path = s1 }
 End
@@ -576,15 +581,15 @@ Theorem multi_step_to_step_path:
   ∀p s1 l s2.
     multi_step p s1 l s2 ⇒
       ∃path.
-        finite path ∧ okpath (step p) path ∧ first path = s1 ∧ last path = s2 ∧
+        finite path ∧ okpath (sem_step p) path ∧ first path = s1 ∧ last path = s2 ∧
         toList (labels path) = Some l
 Proof
   ho_match_mp_tac multi_step_ind >> conj_tac
-  >- (rw [] >> qexists_tac `pcons s1 l (stopped_at s2)` >> fs [toList_THM, last_step_def]) >>
+  >- (rw [] >> qexists_tac `pcons s1 l (stopped_at s2)` >> fs [sem_step_cases, toList_THM, last_step_cases]) >>
   rw [] >>
   qexists_tac `pcons s1 l path` >> rw [toList_THM] >>
   `LFINITE (labels path)` by metis_tac [finite_labels] >>
-  drule LFINITE_toList >> rw [] >> rw []
+  simp [sem_step_cases]
 QED
 
 Theorem expand_multi_step_path:
@@ -592,7 +597,7 @@ Theorem expand_multi_step_path:
     !l. toList (labels path) = Some l ⇒
     ∃path'.
       toList (labels path') = Some (flat l) ∧ finite path' ∧
-      okpath (step prog) path' ∧ first path' = first path ∧ last path' = last path
+      okpath (sem_step prog) path' ∧ first path' = first path ∧ last path' = last path
 Proof
   ho_match_mp_tac finite_okpath_ind >> rw []
   >- (qexists_tac `stopped_at x` >> fs [toList_THM] >> rw []) >>
@@ -606,8 +611,10 @@ Proof
 QED
 
 Theorem contract_step_path:
-  ∀path. okpath (step prog) path ∧ finite path ⇒
-    ∀l1 l s. last_step prog (last path) l s ∧
+  ∀path. okpath (sem_step prog) path ∧ finite path ⇒
+    ∀l1 l s.
+      last_step prog (last path) l s ∧
+      (last path).status = Partial ∧
       toList (labels path) = Some l1
     ⇒
     ∃path' l2.
@@ -626,19 +633,23 @@ Proof
   Cases_on `last_step prog x r (first path)`
   >- (
     qexists_tac `pcons x [r] path'` >> simp [] >>
-    simp [Once multi_step_cases, toList_THM])
+    fs [sem_step_cases] >>
+    simp [Once multi_step_cases, toList_THM] >>
+    simp [last_step_cases])
   >- (
     qpat_x_assum `okpath (multi_step _) _` mp_tac >>
     simp [Once okpath_cases] >> rw [] >> fs [toList_THM] >> rw [] >> fs [] >>
     qexists_tac `pcons x (r::r') p` >> fs [toList_THM] >> rw [Once multi_step_cases] >>
-    disj2_tac >> qexists_tac `first path` >> rw [] >> fs [last_step_def] >> rfs [] >>
-    fs [step_cases, get_instr_cases] >>
-    metis_tac [])
+    disj2_tac >> qexists_tac `first path` >> rw [] >> fs [sem_step_cases]
+    >- (fs [last_step_cases, step_cases, get_instr_cases] >> metis_tac []) >>
+    qpat_x_assum `okpath (sem_step _) _` mp_tac >>
+    simp [Once okpath_cases, sem_step_cases] >> CCONTR_TAC >> fs [] >> rw [] >>
+    fs [first_def, last_thm] >> rw [] >> fs [])
 QED
 
 Definition get_next_step_def:
   get_next_step p s1 =
-    some (s2, l). step p s1 l s2 ∧ ¬last_step p s1 l s2
+    some (s2, l). sem_step p s1 l s2 ∧ ¬last_step p s1 l s2
 End
 
 Triviality finite_plink_trivial:
@@ -660,12 +671,61 @@ Definition instrs_left_def:
         | Offset idx => length b.body - idx
 End
 
+Theorem sem_step_stuck:
+  ∀p s1. (∀l s2. ¬sem_step p s1 l s2) ⇔ s1.status ≠ Partial
+Proof
+  rw [sem_step_cases] >> metis_tac []
+QED
+
+Theorem sem_step_then_stuck:
+  ∀p s1 l1 s2.
+    sem_step p s1 l1 s2 ∧ (∀l2 s3. ¬sem_step p s2 l2 s3)
+    ⇒
+    (l1 = Error ∧ s2 = s1 with status := Stuck ∧ ∀l2 s3. ¬step p s1 l2 s3) ∨
+    (∃i e. l1 = Exit i ∧ s2 = s1 with status := Complete i ∧
+      get_instr p s1.ip (Inl (Exit e)))
+Proof
+  rw [sem_step_stuck] >>
+  fs [sem_step_cases] >>
+  disj2_tac >> fs [step_cases] >> rfs [inc_pc_def] >>
+  fs [step_instr_cases] >> rfs [update_result_def, inc_pc_def] >>
+  metis_tac []
+QED
+
+Theorem sem_step_not_last:
+  ∀p s1 l1 s2.
+    sem_step p s1 l1 s2 ∧ ¬last_step p s1 l1 s2 ⇒
+    ∃l2 s3. sem_step p s2 l2 s3
+Proof
+  rw [] >> CCONTR_TAC >> fs [] >> drule sem_step_then_stuck >>
+  simp [] >>
+  CCONTR_TAC >> fs [] >> rw []
+  >- fs [last_step_cases] >>
+  fs [last_step_cases, sem_step_cases] >> rw [] >>
+  first_x_assum (qspec_then `Inl (Exit e)` mp_tac) >>
+  rw [terminator_def]
+QED
+
+Triviality some_lemma:
+  ∀P a b. (some (x, y). P x y) = Some (a, b) ⇒ P a b
+Proof
+  rw [optionTheory.some_def] >>
+  qmatch_assum_abbrev_tac `(@x. Q x) = _` >>
+  `Q (@x. Q x)` suffices_by (rw [Abbr `Q`]) >>
+  `?x. Q x` suffices_by rw [SELECT_THM] >>
+  unabbrev_all_tac >> rw [] >>
+  pairarg_tac >> fs [] >> rw [EXISTS_PROD] >>
+  metis_tac []
+QED
+
 Theorem extend_step_path:
   ∀path.
-    okpath (step p) path ∧ finite path
+    okpath (sem_step p) path ∧ finite path
     ⇒
-    (∀s. path = stopped_at s ⇒ ∃s' l. step p s l s') ⇒
-    ?path' l s n. finite path' ∧ okpath (step p) path' ∧ last_step p (last path') l s ∧
+    (∀s. path = stopped_at s ⇒ ∃s' l. sem_step p s l s') ⇒
+    ∃path' l s n.
+      finite path' ∧ okpath (sem_step p) path' ∧ (last path').status = Partial ∧
+      last_step p (last path') l s ∧
       length path = Some (Suc n) ∧ n ∈ PL (pconcat path' l (stopped_at s)) ∧
       path = take n (pconcat path' l (stopped_at s))
 Proof
@@ -673,8 +733,8 @@ Proof
   Cases_on `get_next_step p (last path) = None ∧ ∀s. path ≠ stopped_at s`
   >- (
     fs [get_next_step_def, optionTheory.some_def, FORALL_PROD, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
-    Cases_on `?l2 s2. step p (last path) l2 s2` >> fs []
-    >- (
+    Cases_on `∃l2 s2. sem_step p (last path) l2 s2` >> fs []
+    >- ( (* Can take a last step from the end of the path *)
       first_x_assum drule >> rw [] >>
       qexists_tac `path` >> qexists_tac `l2` >> qexists_tac `s2` >> rw [] >>
       fs [finite_length] >>
@@ -684,21 +744,21 @@ Proof
       `length (pconcat path l2 (stopped_at s2)) = Some (n + 1)`
       by metis_tac [length_pconcat, alt_length_thm] >>
       rw [take_pconcat]
+      >- fs [sem_step_cases]
       >- metis_tac [take_all] >>
       fs [PL_def] >> rfs [])
-    >- (
+    >- ( (* The path is stuck, so we need to extract the last step from it *)
       drule finite_path_end_cases >>
       rw [] >> fs [] >> rfs [] >>
       qexists_tac `p'` >> rw [] >>
       qexists_tac `l` >> qexists_tac `s` >> rw [] >>
       fs [finite_length] >>
-      qexists_tac `n` >> rw []
-      >- (
-        qpat_x_assum `step _ _ _ _` mp_tac >>
-        rw [last_step_def, step_cases] >> metis_tac []) >>
+      qexists_tac `n` >> rw [] >>
       `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 []
+      >- fs [sem_step_cases]
+      >- metis_tac [sem_step_not_last]
       >- (
         rw [PL_def] >> fs [finite_length] >>
         `length (pconcat p' l (stopped_at s)) = Some (n + 1)`
@@ -718,19 +778,21 @@ Proof
     simp [Abbr `path1`] >> irule unfold_finite >>
     WF_REL_TAC `measure (instrs_left p)` >>
     rpt gen_tac >>
-    simp [instrs_left_def, get_next_step_def, optionTheory.some_def, EXISTS_PROD] >>
-    qmatch_goalsub_abbrev_tac `@x. P x` >> rw [] >>
-    `?x. P x` by (fs [Abbr `P`, EXISTS_PROD] >> metis_tac []) >>
-    `P (@x. P x)` by metis_tac [SELECT_THM] >>
-    qunabbrev_tac `P` >> pop_assum mp_tac >> simp [] >>
-    simp [last_step_def] >> rw [] >>
-    pop_assum mp_tac >> simp [] >>
+    rw [instrs_left_def, get_next_step_def] >>
+    qabbrev_tac `P = (\s3 l. sem_step p s2 l s3 ∧ ¬last_step p s2 l s3)` >>
+    `P s3 l` by (irule some_lemma >> simp [Abbr `P`]) >>
+    pop_assum mp_tac >> simp [Abbr `P`] >> strip_tac >>
+    drule sem_step_not_last >> simp [] >> strip_tac >>
+    qpat_x_assum `sem_step p s2 l s3` mp_tac >> rw [Once sem_step_cases]
+    >- (
       `?i. get_instr p s2.ip i` by metis_tac [get_instr_cases, step_cases] >>
-    disch_then (qspec_then `i` mp_tac) >> simp [] >>
+      `?x. i = Inl x` by (fs [last_step_cases] >> metis_tac [sumTheory.sum_CASES]) >>
       drule step_same_block >> disch_then drule >> simp [] >>
-    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 []) >>
+      impl_tac
+      >- (fs [last_step_cases] >> metis_tac []) >>
+      fs [step_cases, get_instr_cases, inc_bip_def] >> rw [] >> fs [] >>
+      rw [inc_bip_def] >> fs [])
+    >- fs [last_step_cases]) >>
  `last path = first path1`
   by (
     unabbrev_all_tac >> simp [Once unfold_thm] >>
@@ -741,68 +803,63 @@ Proof
     unabbrev_all_tac >>
     irule okpath_unfold >> rw [] >>
     qexists_tac `\x.T` >> rw [get_next_step_def] >>
-    fs [optionTheory.some_def] >>
-    pairarg_tac >> fs [] >>
-    qmatch_assum_abbrev_tac `(@x. P x) = _` >>
-    `P (@x. P x)`
-    by (
-      simp [SELECT_THM] >>
-      unabbrev_all_tac >> fs [EXISTS_PROD] >>
-      metis_tac []) >>
-    rfs [] >>
-    unabbrev_all_tac >> fs []) >>
+    qabbrev_tac `P = (\s2 l. sem_step p s l s2 ∧ ¬last_step p s l s2)` >>
+    `P s' l` by (irule some_lemma >> simp [Abbr `P`]) >>
+    pop_assum mp_tac >> simp [Abbr `P`]) >>
   `?n. length path1 = Some n` by fs [finite_length] >>
   `n ≠ 0` by metis_tac [length_never_zero] >>
   `length (plink path path1) = Some (Suc m + n - 1)` by metis_tac [length_plink] >>
   simp [take_pconcat, PL_def, finite_pconcat, length_plink] >>
   `!l s. length (pconcat (plink path path1) l (stopped_at s)) = Some ((Suc m + n − 1) + 1)`
   by metis_tac [length_pconcat, alt_length_thm] >>
-  rw [GSYM PULL_EXISTS]
-  >- (
+  simp [GSYM PULL_EXISTS] >>
   unabbrev_all_tac >> drule unfold_last >>
   qmatch_goalsub_abbrev_tac `last_step _ (last path1) _ _` >>
-    simp [get_next_step_def, optionTheory.some_def, FORALL_PROD] >>
-    rw [METIS_PROVE [] ``~x ∨ y ⇔ (~y ⇒ ~x)``] >> CCONTR_TAC >>
-    Cases_on `1 ∈ PL path1`
+  simp [Once get_next_step_def, optionTheory.some_def, FORALL_PROD] >>
+  strip_tac >>
+  simp [CONJ_ASSOC, Once CONJ_SYM] >>
+  simp [GSYM CONJ_ASSOC] >>
+  conj_tac
   >- (
-      fs [] >> pairarg_tac >> fs [] >> rw [] >>
-      qmatch_assum_abbrev_tac `(@x. P x) = _` >>
-      `P (@x. P x)`
-      by (
-        simp [SELECT_THM] >>
-        unabbrev_all_tac >> fs [EXISTS_PROD] >>
-        metis_tac []) >>
-      fs [Abbr `P`] >> pairarg_tac >> fs [] >> rw [] >>
-      fs [last_step_def] >> rfs  [] >>
-      `?i. get_instr p x.ip i` by (fs [step_cases] >> metis_tac []) >>
-      metis_tac []) >>
-    `n = 1` by (rfs [PL_def, finite_length] >> decide_tac) >> rw [] >>
+    rw [take_plink]
+    >- (imp_res_tac take_all >> fs []) >>
+    metis_tac [finite_plink_trivial]) >>
+  pop_assum mp_tac >>
+  Cases_on `1 ∈ PL path1` >> simp []
+  >- (
+    simp [get_next_step_def] >> strip_tac >>
+    qabbrev_tac `P = (\s2 l. sem_step p x l s2 ∧ ¬last_step p x l s2)` >>
+    `P (last path1) l` by (irule some_lemma >> simp [Abbr `P`]) >>
+    pop_assum mp_tac >> simp [Abbr `P`] >>
+    strip_tac >>
+    drule sem_step_not_last >> rw []
+    >- fs [sem_step_cases] >>
+    metis_tac [])
+  >- (
+    `n = 1` by (rfs [PL_def, finite_length] >> decide_tac) >>
     qspec_then `path1` strip_assume_tac path_cases
     >- (
-      unabbrev_all_tac >> fs [] >> rw [] >>
-      fs [Once unfold_thm] >>
+      unabbrev_all_tac >> simp [] >>
+      fs [] >> fs [Once unfold_thm] >>
       Cases_on `get_next_step p (last path)` >> simp [] >> fs [] >> rw [] >>
       fs [get_next_step_def, optionTheory.some_def, FORALL_PROD] >>
-      split_pair_case_tac >> fs []) >>
-    fs [alt_length_thm, length_never_zero])
-  >- (
-    rw [take_plink]
-    >-  (imp_res_tac take_all >> fs []) >>
-    metis_tac [finite_plink_trivial])
+      TRY split_pair_case_tac >> fs [sem_step_cases] >>
+      metis_tac [])
+    >- fs [alt_length_thm, length_never_zero])
 QED
 
 Theorem find_path_prefix:
   ∀path.
-     okpath (step p) path ∧ finite path
+     okpath (sem_step p) path ∧ finite path
     ⇒
     !obs l1. toList (labels path) = Some l1 ∧
-    obs ∈ observation_prefixes (get_observation p (last path), l1)
+    obs ∈ observation_prefixes ((last path).status, l1)
     ⇒
     ∃n l2. n ∈ PL path ∧ toList (labels (take n path)) = Some l2 ∧
-      obs = (get_observation p (last (take n path)), filter ($≠ Tau) l2)
+      obs = ((last (take n path)).status, filter ($≠ Tau) l2)
 Proof
   ho_match_mp_tac finite_okpath_ind >> rw [toList_THM]
-  >- fs [observation_prefixes_cases, get_observation_def, IN_DEF] >>
+  >- fs [observation_prefixes_cases, IN_DEF] >>
   `?s ls. obs = (s, ls)` by metis_tac [pairTheory.pair_CASES] >>
   fs [] >>
   `∃l. length path = Some l ∧ l ≠ 0` by metis_tac [finite_length, length_never_zero] >>
@@ -821,11 +878,11 @@ Proof
   rename1 `short_l ≼ first_l::long_l` >>
   Cases_on `short_l` >> fs []
   >- (
-    qexists_tac `0` >> rw [toList_THM, get_observation_def] >>
-    metis_tac [exit_no_step]) >>
+    qexists_tac `0` >> rw [toList_THM] >>
+    fs [sem_step_cases]) >>
   rename1 `short_l ≼ long_l` >>
   rfs [] >>
-  `(Partial, filter ($≠ Tau) short_l) ∈ observation_prefixes (get_observation p (last path),long_l)`
+  `(Partial, filter ($≠ Tau) short_l) ∈ observation_prefixes ((last path).status,long_l)`
   by (simp [observation_prefixes_cases, IN_DEF] >> metis_tac []) >>
   first_x_assum drule >> strip_tac >>
   qexists_tac `Suc n` >> simp [toList_THM] >> rw [] >> rfs [last_take]
@@ -839,7 +896,7 @@ Proof
 QED
 
 Theorem big_sem_equiv:
-  !p s1. multi_step_sem p s1 = sem p s1
+  ∀p s1. multi_step_sem p s1 = sem p s1
 Proof
   rw [multi_step_sem_def, sem_def, EXTENSION] >> eq_tac >> rw []
   >- (
@@ -848,15 +905,16 @@ Proof
     `?n short_l.
       n ∈ PL s_path ∧
       toList (labels (take n s_path)) = Some short_l ∧
-      x = (get_observation p (last (take n s_path)), filter ($≠ Tau) short_l)`
+      x = ((last (take n s_path)).status, filter ($≠ Tau) short_l)`
     by metis_tac [find_path_prefix] >>
     qexists_tac `take n s_path` >> rw [])
   >- (
-    Cases_on `¬∀s. path = stopped_at s ⇒ ∃s' l. step p s l s'`
+    Cases_on `¬∀s. path = stopped_at s ⇒ ∃s' l. sem_step p s l s'`
     >- (
       fs [] >> rw [] >> fs [toList_THM] >> rw [] >>
       qexists_tac `stopped_at s` >> rw [toList_THM] >>
-      rw [observation_prefixes_cases, IN_DEF, get_observation_def]) >>
+      rw [observation_prefixes_cases, IN_DEF] >>
+      metis_tac [trace_type_nchotomy]) >>
     drule extend_step_path >> disch_then drule >>
     impl_tac >> rw []
     >- metis_tac [] >>
@@ -877,7 +935,7 @@ Proof
       rw [observation_prefixes_cases, IN_DEF] >> rw [] >>
       unabbrev_all_tac >> rw [last_pconcat] >> fs [] >>
       drule toList_LAPPEND_APPEND >> rw [toList_THM] >>
-      Cases_on `get_observation p (last m_path)` >> simp [] >>
+      Cases_on `(last m_path).status` >> simp [] >>
       qexists_tac `s_ext_l ++ [last_l]` >> rw []) >>
     fs [PL_def, finite_pconcat] >> rfs [] >>
     `?m. length s_ext_path = Some m` by metis_tac [finite_length] >>
@@ -887,7 +945,7 @@ Proof
     fs [] >>
     `n < m` by decide_tac >> fs [] >> rw [] >>
     `n ∈ PL s_ext_path` by rw [PL_def] >>
-    Cases_on `get_observation p (last orig_path) = Partial`
+    Cases_on `(last orig_path).status = Partial`
     >- (
       rw [observation_prefixes_cases, IN_DEF] >> rw [] >>
       unabbrev_all_tac >> fs [] >>
@@ -901,16 +959,14 @@ Proof
         fs [ltake_fromList2] >>
         rw [take_is_prefix])
       >- (drule LTAKE_LENGTH >> rw [])) >>
-    `¬∃l s. step p (last orig_path) l s`
-    by (fs [get_observation_def] >> BasicProvers.EVERY_CASE_TAC >> fs [] >> metis_tac [exit_no_step]) >>
     unabbrev_all_tac >> rfs [last_take] >>
     fs [okpath_pointwise] >>
     Cases_on `Suc n ∈ PL s_ext_path` >> rw []
-    >- (last_x_assum (qspec_then `n` mp_tac) >> rw []) >>
+    >- (last_x_assum (qspec_then `n` mp_tac) >> rw [sem_step_cases]) >>
     `n = m - 1` by (fs [PL_def] >> rfs []) >>
     rw [] >>
     `el (m - 1) s_ext_path = last s_ext_path` by metis_tac [take_all, pathTheory.last_take] >>
-    fs [last_step_def])
+    fs [last_step_cases])
 QED
 
 export_theory ();

sledge/semantics/llvm_ssaScript.sml

@@ -151,6 +151,7 @@ Definition instr_uses_def:
   (instr_uses (Invoke _ _ a targs _ _) =
     arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
   (instr_uses Unreachable = {}) ∧
+  (instr_uses (Exit a) = arg_to_regs a) ∧
   (instr_uses (Sub _ _ _ _ a1 a2) =
     arg_to_regs a1 ∪ arg_to_regs a2) ∧
   (instr_uses (Extractvalue _ (_, a) _) = arg_to_regs a) ∧

sledge/semantics/llvm_to_llairScript.sml

@@ -187,8 +187,10 @@ End
 
 (* TODO *)
 Definition translate_instr_to_term_def:
-  translate_instr_to_term f emap (Br a l1 l2) =
-    Switch (translate_arg emap a) [(0, translate_label f l2)] (translate_label f l1)
+  (translate_instr_to_term f emap (Br a l1 l2) =
+    Switch (translate_arg emap a) [(0, translate_label f l2)] (translate_label f l1)) ∧
+  (translate_instr_to_term f emap (Exit a) =
+    Exit (translate_arg emap a))
 End
 
 Datatype:

sledge/semantics/llvm_to_llair_propScript.sml

@@ -44,7 +44,7 @@ End
 Inductive pc_rel:
  (* LLVM side points to a normal instruction *)
  (∀prog emap ip bp d b idx b' prev_i fname.
-    (* Both are valid pointers to blocks n the same function *)
+    (* Both are valid pointers to blocks in the same function *)
     dest_fn ip.f = fst (dest_llair_lab bp) ∧
     alookup prog ip.f = Some d ∧
     alookup d.blocks ip.b = Some b ∧
@@ -74,12 +74,6 @@ 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
@@ -100,7 +94,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 ∧
-    complete_trace_rel s.exited s'.status
+    s.status = s'.status
 End
 
 (* Define when an LLVM state is related to a llair one
@@ -110,12 +104,11 @@ 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' ∧
-    s'.status = get_observation prog s
+    (s.status = Partial ⇒ pc_rel prog emap s.ip s'.bp) ∧
+    mem_state_rel prog emap s s'
 End
 
-Theorem mem_state_ignore_bp:
+Theorem mem_state_ignore_bp[simp]:
   ∀prog emap s s' b. mem_state_rel prog emap s (s' with bp := b) ⇔ mem_state_rel prog emap s s'
 Proof
   rw [mem_state_rel_def] >> eq_tac >> rw [] >>
@@ -125,6 +118,22 @@ Proof
   metis_tac []
 QED
 
+Triviality lemma:
+  ((s:llair$state) with status := Complete code).locals = s.locals
+Proof
+  rw []
+QED
+
+Theorem mem_state_rel_exited:
+  ∀prog emap s s' code.
+    mem_state_rel prog emap s s'
+    ⇒
+    mem_state_rel prog emap (s with status := Complete code) (s' with status := Complete code)
+Proof
+  rw [mem_state_rel_def] >>
+  metis_tac [eval_exp_ignores, lemma]
+QED
+
 Theorem mem_state_rel_no_update:
   ∀prog emap s1 s1' v res_v r i i'.
   assigns prog s1.ip = {} ∧
@@ -723,7 +732,9 @@ QED
 *)
 
 Definition translate_trace_def:
-  (translate_trace types Tau = Tau ) ∧
+  (translate_trace types Tau = Tau) ∧
+  (translate_trace types Error = Error) ∧
+  (translate_trace types (Exit i) = (Exit i)) ∧
   (translate_trace types (W gv bytes) = W (translate_glob_var gv (types gv)) bytes)
 End
 
@@ -732,7 +743,9 @@ Definition untranslate_glob_var_def:
 End
 
 Definition untranslate_trace_def:
-  (untranslate_trace Tau = Tau ) ∧
+  (untranslate_trace Tau = Tau) ∧
+  (untranslate_trace Error = Error) ∧
+  (untranslate_trace (Exit i) = (Exit i)) ∧
   (untranslate_trace (W gv bytes) = W (untranslate_glob_var gv) bytes)
 End
 
@@ -763,9 +776,8 @@ QED
 Theorem translate_instrs_correct1:
   ∀prog s1 tr s2.
     multi_step prog s1 tr s2 ⇒
-    !s1' b' emap regs_to_keep d b types idx.
-      prog_ok prog ∧
-      is_ssa prog ∧
+    ∀s1' b' emap regs_to_keep d b types idx.
+      prog_ok prog ∧ is_ssa prog ∧
       mem_state_rel prog emap s1 s1' ∧
       alookup prog s1.ip.f = Some d ∧
       alookup d.blocks s1.ip.b = Some b ∧
@@ -773,32 +785,55 @@ Theorem translate_instrs_correct1:
       b' = fst (translate_instrs (dest_fn s1.ip.f) emap regs_to_keep (take_to_call (drop idx b.body)))
       ⇒
       ∃emap s2' tr'.
-        step_block (translate_prog prog) s1' b'.cmnd tr' b'.term s2' ∧
+        step_block (translate_prog prog) s1' b'.cmnd b'.term tr' s2' ∧
         filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace types) tr)  ∧
         state_rel prog emap s2 s2'
 Proof
   ho_match_mp_tac multi_step_ind >> rw_tac std_ss []
   >- (
-    fs [last_step_def]
+    fs [last_step_cases]
     >- ( (* Phi (not handled here) *)
       fs [get_instr_cases])
     >- ( (* Terminator *)
-      `l = Tau`
+      `(∃code. l = Exit code) ∨ l = Tau `
       by (
         fs [llvmTheory.step_cases] >>
         `i' = i''` by metis_tac [get_instr_func, sumTheory.INL_11] >>
         fs [step_instr_cases] >> rfs [terminator_def]) >>
-      fs [get_instr_cases] >> rw [] >>
+      fs [get_instr_cases, translate_trace_def] >> rw [] >>
       `el idx b.body = el 0 (drop idx b.body)` by rw [EL_DROP] >>
       fs [] >>
-      Cases_on `drop idx b.body` >> fs [DROP_NIL] >> rw [] >>
+      Cases_on `drop idx b.body` >> fs [DROP_NIL] >> rw []
+      >- ( (* Exit *)
+        fs [llvmTheory.step_cases, get_instr_cases, step_instr_cases,
+            translate_instrs_def, take_to_call_def, classify_instr_def,
+            translate_instr_to_term_def, translate_instr_to_inst_def,
+            llvmTheory.get_obs_cases] >>
+        simp [Once step_block_cases, step_term_cases, PULL_EXISTS, step_inst_cases] >>
+        drule translate_arg_correct >>
+        disch_then drule >> impl_tac
+        >- (
+          `get_instr prog s1.ip (Inl (Exit a))` by rw [get_instr_cases] >>
+          drule get_instr_live >>
+          simp [uses_cases, SUBSET_DEF, IN_DEF, PULL_EXISTS] >>
+          rw [] >> first_x_assum irule >>
+          disj1_tac >>
+          metis_tac [instr_uses_def]) >>
+        rw [] >>
+        qexists_tac `emap` >>
+        qexists_tac `s1' with status := Complete code` >>
+        qexists_tac `[Exit code]` >>
+        rw []
+        >- (fs [v_rel_cases] >> fs [signed_v_to_int_def] >> metis_tac []) >>
+        rw [state_rel_def] >>
+        metis_tac [mem_state_rel_exited]) >>
       simp [take_to_call_def, translate_instrs_def] >>
       Cases_on `el idx b.body` >> fs [terminator_def, classify_instr_def, translate_trace_def] >> rw []
       >- ( (* Ret *)
         cheat)
       >- ( (* Br *)
         simp [translate_instr_to_term_def, Once step_block_cases] >>
-        simp [step_term_cases, PULL_EXISTS] >>
+        simp [step_term_cases, PULL_EXISTS, RIGHT_AND_OVER_OR, EXISTS_OR_THM] >>
         fs [llvmTheory.step_cases] >>
         drule get_instr_live >> disch_tac >>
         drule translate_arg_correct >>
@@ -838,8 +873,7 @@ Proof
           >- (
             qpat_x_assum `!r. r ∈ live _ _ ⇒ P r` mp_tac >>
             simp [Once live_gen_kill] >> disch_then (qspec_then `r` mp_tac) >>
-            impl_tac >> rw []
-            >- (
+            impl_tac >> rw [] >>
             rw [PULL_EXISTS] >>
             disj1_tac >>
             qexists_tac `<|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|>` >>
@@ -848,30 +882,31 @@ Proof
               disj1_tac >>
               qexists_tac `Br a l1 l2` >>
               rw [instr_next_ips_def, Abbr `target`] >>
-                cheat) >>
+              fs [prog_ok_def, get_instr_cases] >>
+              last_x_assum drule >> disch_then drule >> rw [] >>
+              `last b.body = Br a l1 l2` by cheat >>
+              fs [instr_to_labs_def] >>
+              metis_tac [blockHeader_nchotomy]) >>
             CCONTR_TAC >> fs [] >>
             imp_res_tac get_instr_func >> fs [] >> rw [] >>
             fs [instr_assigns_def])
-            >- (
-              rpt HINT_EXISTS_TAC >> rw [] >>
-              qmatch_goalsub_abbrev_tac `eval_exp s3 _` >>
-              `s1'.locals = s3.locals` by fs [Abbr `s3`] >>
-              metis_tac [eval_exp_ignores]))
-          >- cheat
-          >- cheat)
-        >- (
-          cheat))
+          >- cheat))
       >- ( (* Invoke *)
         cheat)
       >- ( (* Unreachable *)
         cheat)
       >- ( (* Exit *)
-        cheat)
+        fs [llvmTheory.step_cases, get_instr_cases, step_instr_cases])
       >- ( (* Throw *)
         cheat))
     >- ( (* Call *)
       cheat)
     >- ( (* Stuck *)
+      rw [translate_trace_def] >>
+      (* TODO: need to know that stuck LLVM instructions translate to stuck
+       * llair instructions. This will follow from knowing that when a llair
+       * instruction takes a step, the LLVM source can take the same step, ie,
+       * the backward direction of the proof. *)
       cheat))
   >- ( (* Middle of the block *)
     fs [llvmTheory.step_cases] >> TRY (fs [get_instr_cases] >> NO_TAC) >>
@@ -910,11 +945,12 @@ Theorem multi_step_to_step_block:
   ∀prog s1 tr s2 s1'.
     prog_ok prog ∧ is_ssa prog ∧
     multi_step prog s1 tr s2 ∧
+    s1.status = Partial ∧
     state_rel prog emap s1 s1'
     ⇒
     ∃s2' emap2 b tr'.
       get_block (translate_prog prog) s1'.bp b ∧
-      step_block (translate_prog prog) s1' b.cmnd tr' b.term s2' ∧
+      step_block (translate_prog prog) s1' b.cmnd b.term tr' s2' ∧
       filter ($≠ Tau) tr' = filter ($≠ Tau) (map (translate_trace types) tr) ∧
       state_rel prog emap2 s2 s2'
 Proof
@@ -932,9 +968,11 @@ Proof
   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
@@ -943,7 +981,7 @@ Theorem step_block_to_multi_step:
   ∀prog s1 s1' tr s2' b.
     state_rel prog emap s1 s1' ∧
     get_block (translate_prog prog) s1'.bp b ∧
-    step_block (translate_prog prog) s1' b.cmnd tr b.term s2'
+    step_block (translate_prog prog) s1' b.cmnd b.term tr s2'
     ⇒
     ∃s2.
       multi_step prog s1 (map untranslate_trace tr) s2 ∧
@@ -986,16 +1024,19 @@ Proof
   ho_match_mp_tac finite_okpath_ind >> rw []
   >- (qexists_tac `stopped_at s1'` >> rw [] >> metis_tac []) >>
   fs [] >>
-  drule multi_step_to_step_block >> ntac 3 (disch_then drule) >>
+  rename1 `state_rel _ _ s1 s1'` >>
+  Cases_on `s1.status ≠ Partial`
+  >- fs [Once multi_step_cases, llvmTheory.step_cases, last_step_cases] >>
+  fs [] >>
+  drule multi_step_to_step_block >> ntac 4 (disch_then drule) >>
   disch_then (qspec_then `types` mp_tac) >> rw [] >>
   first_x_assum drule >> rw [] >>
   qexists_tac `pcons s1' tr' path'` >> rw [] >>
   rw [FILTER_MAP, combinTheory.o_DEF, trans_trace_not_tau] >>
   HINT_EXISTS_TAC >> simp [] >>
   simp [step_cases] >> qexists_tac `b` >> simp [] >>
-  fs [state_rel_def, mem_state_rel_def] >> simp [get_observation_def] >>
-  fs [Once multi_step_cases, last_step_def] >> rw [] >>
-  metis_tac [get_instr_func, exit_no_step]
+  qpat_x_assum `state_rel _ _ _ s1'` mp_tac >>
+  rw [state_rel_def, mem_state_rel_def]
 QED
 
 Theorem translate_prog_correct_lem2:
@@ -1035,6 +1076,42 @@ Proof
   cheat
 QED
 
+Theorem prefix_take_filter_lemma:
+  ∀l lsub.
+    lsub ≼ l
+    ⇒
+    filter (λy. Tau ≠ y) lsub =
+    take (length (filter (λy. Tau ≠ y) lsub)) (filter (λy. Tau ≠ y) l)
+Proof
+  Induct_on `lsub` >> rw [] >>
+  Cases_on `l` >> fs [] >> rw []
+QED
+
+Theorem multi_step_lab_label:
+  ∀prog s1 ls s2.
+    multi_step prog s1 ls s2 ⇒ s2.status ≠ Partial
+    ⇒
+    ∃ls'. (∃i. ls = ls' ++ [Exit i]) ∨ ls = ls' ++ [Error]
+Proof
+  ho_match_mp_tac multi_step_ind >> rw [] >> fs [] >>
+  fs [last_step_cases, llvmTheory.step_cases, step_instr_cases,
+      update_result_def, llvmTheory.inc_pc_def] >>
+  rw [] >> fs []
+QED
+
+Theorem prefix_filter_len_eq:
+  ∀l1 l2 x.
+    l1 ≼ l2 ++ [x] ∧
+    length (filter P l1) = length (filter P (l2 ++ [x])) ∧
+    P x
+    ⇒
+    l1 = l2 ++ [x]
+Proof
+  Induct_on `l1` >> rw [FILTER_APPEND] >>
+  Cases_on `l2` >> fs [] >> rw [] >> rfs [ADD1] >>
+  first_x_assum irule >> rw [FILTER_APPEND]
+QED
+
 Theorem translate_prog_correct:
   ∀prog s1 s1'.
     prog_ok prog ∧ is_ssa prog ∧
@@ -1063,16 +1140,36 @@ 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`] >>
-    cheat)
-(*
-    `INJ (translate_trace types) (set l2' ∪ set (flat l2)) UNIV`
-    by (
-      simp [INJ_DEF] >> rpt gen_tac >>
-      Cases_on `x` >> Cases_on `y` >> simp [translate_trace_def] >>
-      Cases_on `a` >> Cases_on `a'` >> simp [translate_glob_var_def]) >>
-    fs [INJ_MAP_EQ_IFF, inj_map_prefix_iff] >> rw [] >>
-    fs [state_rel_def, mem_state_rel_def])
-    *)
+    Cases_on `lsub = flat l` >> fs []
+    >- (
+      qexists_tac `flat l'` >>
+      rw [FILTER_FLAT, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF] >>
+      fs [state_rel_def, mem_state_rel_def]) >>
+    `filter (λy. Tau ≠ y) (flat l') = map (translate_trace types) (filter (λy. Tau ≠ y) (flat l))`
+    by rw [FILTER_FLAT, MAP_FLAT, MAP_MAP_o, combinTheory.o_DEF, FILTER_MAP] >>
+    qexists_tac `take_prop ($≠ Tau) (length (filter ($≠ Tau) lsub)) (flat l')` >>
+    rw [] >> rw [GSYM MAP_TAKE]
+    >- metis_tac [prefix_take_filter_lemma] >>
+    CCONTR_TAC >> fs [] >>
+    `(last path).status = (last path').status` by fs [state_rel_def, mem_state_rel_def] >>
+    drule take_prop_eq >> strip_tac >>
+    `length (filter (λy. Tau ≠ y) (flat l')) = length (filter (λy. Tau ≠ y) (flat l))`
+    by rw [] >>
+    fs [] >> drule filter_is_prefix >>
+    disch_then (qspec_then `$≠ Tau` assume_tac) >>
+    drule IS_PREFIX_LENGTH >> strip_tac >> fs [] >>
+    `length (filter (λy. Tau ≠ y) lsub) = length (filter (λy. Tau ≠ y) (flat l))` by rw [] >>
+    fs [] >> rw [] >>
+    qspec_then `path` assume_tac finite_path_end_cases >> rfs [] >> fs [] >> rw []
+    >- (`l = []` by metis_tac [llistTheory.fromList_EQ_LNIL] >> fs [] >> rfs []) >>
+    rfs [labels_plink] >>
+    rename1 `LAPPEND (labels path) [|last_l'|] = _` >>
+    `toList (LAPPEND (labels path) [|last_l'|]) = Some l` by metis_tac [llistTheory.from_toList] >>
+    drule llistTheory.toList_LAPPEND_APPEND >> strip_tac >>
+    fs [llistTheory.toList_THM] >> rw [] >>
+    drule multi_step_lab_label >> strip_tac >> rfs [] >> fs [] >>
+    drule prefix_filter_len_eq >> rw [] >>
+    qexists_tac `$≠ Tau` >> rw [])
   >- (
     fs [toList_some] >>
     drule translate_prog_correct_lem2 >> simp [] >>

sledge/semantics/miscScript.sml

@@ -25,6 +25,8 @@ Datatype:
   obs =
   | Tau
   | W 'a (word8 list)
+  | Exit int
+  | Error
 End
 
 Datatype:
@@ -43,6 +45,55 @@ Inductive observation_prefixes:
     observation_prefixes (x, l1) (Partial, filter ($≠ Tau) l2))
 End
 
+Definition take_prop_def:
+  (take_prop P n [] = []) ∧
+  (take_prop P n (x::xs) =
+    if n = 0 then
+      []
+    else if P x then
+      x :: take_prop P (n - 1) xs
+    else
+      x :: take_prop P n xs)
+End
+
+Theorem filter_take_prop[simp]:
+  ∀P n l. filter P (take_prop P n l) = take n (filter P l)
+Proof
+  Induct_on `l` >> rw [take_prop_def]
+QED
+
+Theorem take_prop_prefix[simp]:
+  ∀P n l. take_prop P n l ≼ l
+Proof
+  Induct_on `l` >> rw [take_prop_def]
+QED
+
+(*
+Theorem take_prop_eq:
+  ∀P n l. take_prop P n l = l ∧ l ≠ [] ∧ n ≤ length (filter P l) ⇒ P (last l)
+Proof
+  Induct_on `l` >> simp_tac (srw_ss()) [take_prop_def] >> rpt gen_tac >>
+  Cases_on `n = 0` >> pop_assum mp_tac >> simp_tac (srw_ss()) [] >>
+  Cases_on `P h` >> pop_assum mp_tac >> simp_tac (srw_ss()) [] >>
+  strip_tac >> strip_tac >>
+  Cases_on `l` >> pop_assum mp_tac >> simp_tac (srw_ss()) []
+  >- metis_tac [take_prop_def] >>
+  ntac 2 strip_tac >> first_x_assum drule >>
+  simp []
+QED
+*)
+
+Theorem take_prop_eq:
+  ∀P n l. take_prop P n l = l ⇒ length (filter P l) ≤ n
+Proof
+  Induct_on `l` >> simp_tac (srw_ss()) [take_prop_def] >> rpt gen_tac >>
+  Cases_on `n = 0` >> pop_assum mp_tac >> simp_tac (srw_ss()) [] >>
+  Cases_on `P h` >> pop_assum mp_tac >> simp_tac (srw_ss()) [] >>
+  strip_tac >> strip_tac >>
+  Cases_on `l` >> pop_assum mp_tac >> simp_tac (srw_ss()) [] >>
+  ntac 2 strip_tac >> first_x_assum drule >> simp []
+QED
+
 (* ----- Theorems about list library functions ----- *)
 
 Theorem dropWhile_map:
@@ -143,6 +194,12 @@ Proof
   rw [] >> fs []
 QED
 
+Theorem filter_is_prefix:
+  ∀l1 l2 P. l1 ≼ l2 ⇒ filter P l1 ≼ filter P l2
+Proof
+  Induct >> rw [] >> Cases_on `l2` >> fs []
+QED
+
 (* ----- Theorems about log ----- *)
 
 Theorem mul_div_bound: