From 3080fba8fa31b638c9fb67f4c40e669a07a7dcae Mon Sep 17 00:00:00 2001 From: Scott Owens Date: Tue, 15 Oct 2019 08:37:39 -0700 Subject: [PATCH] [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 | 34 +-- sledge/semantics/llvmScript.sml | 43 +-- sledge/semantics/llvm_propScript.sml | 254 +++++++++++------- sledge/semantics/llvm_ssaScript.sml | 1 + sledge/semantics/llvm_to_llairScript.sml | 6 +- sledge/semantics/llvm_to_llair_propScript.sml | 219 ++++++++++----- sledge/semantics/miscScript.sml | 57 ++++ 7 files changed, 416 insertions(+), 198 deletions(-) diff --git a/sledge/semantics/llairScript.sml b/sledge/semantics/llairScript.sml index 72daf7d43..f10cb4330 100644 --- a/sledge/semantics/llairScript.sml +++ b/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' diff --git a/sledge/semantics/llvmScript.sml b/sledge/semantics/llvmScript.sml index ffe8ac3e0..9d5624da4 100644 --- a/sledge/semantics/llvmScript.sml +++ b/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 ∧ diff --git a/sledge/semantics/llvm_propScript.sml b/sledge/semantics/llvm_propScript.sml index 6ba346fb1..14950149c 100644 --- a/sledge/semantics/llvm_propScript.sml +++ b/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. - 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) +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'))) + ⇒ + 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 [] >> - `?i. get_instr p s2.ip i` by metis_tac [get_instr_cases, step_cases] >> - disch_then (qspec_then `i` mp_tac) >> simp [] >> - 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 []) >> + 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] >> + `?x. i = Inl x` by (fs [last_step_cases] >> metis_tac [sumTheory.sum_CASES]) >> + drule step_same_block >> disch_then drule >> simp [] >> + 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 [Once get_next_step_def, optionTheory.some_def, FORALL_PROD] >> + strip_tac >> + simp [CONJ_ASSOC, Once CONJ_SYM] >> + simp [GSYM CONJ_ASSOC] >> + conj_tac >- ( - 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` - >- ( - 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 (); diff --git a/sledge/semantics/llvm_ssaScript.sml b/sledge/semantics/llvm_ssaScript.sml index 55c735939..414e5646f 100644 --- a/sledge/semantics/llvm_ssaScript.sml +++ b/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) ∧ diff --git a/sledge/semantics/llvm_to_llairScript.sml b/sledge/semantics/llvm_to_llairScript.sml index d37975f88..fb6e335ae 100644 --- a/sledge/semantics/llvm_to_llairScript.sml +++ b/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: diff --git a/sledge/semantics/llvm_to_llair_propScript.sml b/sledge/semantics/llvm_to_llair_propScript.sml index a8759aab7..5f4f69ca5 100644 --- a/sledge/semantics/llvm_to_llair_propScript.sml +++ b/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,40 +873,40 @@ 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|>` >> + rw [next_ips_cases, IN_DEF, assigns_cases] >- ( - rw [PULL_EXISTS] >> disj1_tac >> - qexists_tac `<|f := s1.ip.f; b := Some target; i := Phi_ip s1.ip.b|>` >> - rw [next_ips_cases, IN_DEF, assigns_cases] - >- ( - disj1_tac >> - qexists_tac `Br a l1 l2` >> - rw [instr_next_ips_def, Abbr `target`] >> - cheat) >> - 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)) + qexists_tac `Br a l1 l2` >> + rw [instr_next_ips_def, Abbr `target`] >> + 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]) + >- 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 [] >> diff --git a/sledge/semantics/miscScript.sml b/sledge/semantics/miscScript.sml index df57ee0bc..93679f2c5 100644 --- a/sledge/semantics/miscScript.sml +++ b/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: