(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) include "common/StructuredTraces.ma". (* We work with two relations on states in parallel, as well as two derived ones. sem_rel is the classic semantic relation between states, keeping track of memory and how program counters are mapped between languages. call_rel keeps track of what pcs corresponding calls have and just that: this is different than corresponance between program counters in sem_rel when CALL f ↦ instr* CALL f instr* *) record status_rel (S1 : abstract_status) (S2 : abstract_status) : Type[1] ≝ { sem_rel :2> S1 → S2 → Prop (* this is kept separate, as not necessarily carrier will synchronise on calls. It should state the minimal properties necessary for as_after_return (typically just the program counter) maybe what function is called too? *) ; call_rel : (Σs.as_classifier S1 s cl_call) → (Σs.as_classifier S2 s cl_call) → Prop ; sim_final : ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2 }. (* The two derived relations are label_rel which tells that the two states are colabelled ret_rel which tells that two return states are in relation: the idea is that it happens when "going back" through as_after_return on one side we get a pair of call_rel related states, then we enjoy as_after_return also on the other. Roughly call_rel will store just enough information so that we can advance locally on a return step and build structured traces any way *) (* if we later generalise, we should move this inside status_rel *) definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2. definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2. λs1_ret,s2_ret. ∀s1_pre,s2_pre.as_after_return S1 s1_pre s1_ret → call_rel ?? R s1_pre s2_pre → as_after_return S2 s2_pre s2_ret. (* the equivalent of a collapsable trace_any_label where we do not force costedness of the lookahead status *) inductive trace_any_any_free (S : abstract_status) : S → S → Type[0] ≝ | taaf_base : ∀s.trace_any_any_free S s s | taaf_step : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 → as_classifier S s2 cl_other → trace_any_any_free S s1 s3 | taaf_step_jump : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 → as_classifier S s2 cl_jump → as_costed S s3 → trace_any_any_free S s1 s3. definition taaf_non_empty ≝ λS,s1,s2.λtaaf : trace_any_any_free S s1 s2. match taaf with [ taaf_base _ ⇒ false | _ ⇒ true ]. (* the base property we ask for simulation to work depends on the status_class S will mark semantic relation, C call relation, L label relation, R return relation *) definition status_simulation ≝ λS1 : abstract_status. λS2 : abstract_status. λsim_status_rel : status_rel S1 S2. ∀st1,st1',st2.as_execute S1 st1 st1' → sim_status_rel st1 st2 → match as_classify … st1 with [ cl_call ⇒ ∀prf. (* st1' ------------S----------\ ↑ \ \ st1 \--L--\ \ | \ \ \ S \-C-\ st2_after_call →taa→ st2' | \ ↑ st2 →taa→ st2_pre_call *) ∃st2_pre_call. as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧ call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧ ∃st2_after_call,st2'. ∃taa2 : trace_any_any … st2 st2_pre_call. ∃taa2' : trace_any_any … st2_after_call st2'. as_execute … st2_pre_call st2_after_call ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2_after_call | cl_tailcall ⇒ ∀prf. (* st1' ------------S----------\ ↑ \ \ st1 \--L--\ \ | \ \ S st2_after_call →taa→ st2' | ↑ st2 →taa→ st2_pre_call *) ∃st2_pre_call. as_tailcall_ident ? st2_pre_call = as_tailcall_ident ? («st1, prf») ∧ ∃st2_after_call,st2'. ∃taa2 : trace_any_any … st2 st2_pre_call. ∃taa2' : trace_any_any … st2_after_call st2'. as_execute … st2_pre_call st2_after_call ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2_after_call | cl_return ⇒ (* st1 / ↓ | st1'----------S,L------------\ S \ \ \ \-----R-------\ | \ | | st2 →taa→ st2_ret | | ↓ / | st2_after_ret →taaf→ st2' we also ask that st2_after_ret be not labelled if the taaf tail is not empty *) ∃st2_ret,st2_after_ret,st2'. ∃taa2 : trace_any_any … st2 st2_ret. ∃taa2' : trace_any_any_free … st2_after_ret st2'. (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ as_classifier … st2_ret cl_return ∧ as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧ ret_rel … sim_status_rel st1' st2_after_ret ∧ label_rel … st1' st2' | cl_other ⇒ (* st1 → st1' | \ S S,L | \ st2 →taaf→ st2' the taaf can be empty (e.g. tunneling) but we ask it must not be the case when both st1 and st1' are labelled (we would be able to collapse labels otherwise) *) ∃st2'. ∃taa2 : trace_any_any_free … st2 st2'. (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2' | cl_jump ⇒ (* just like cl_other, but with a hypothesis more *) as_costed … st1' → ∃st2'. ∃taa2 : trace_any_any_free … st2 st2'. (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2' ]. (* some useful lemmas *) let rec taa_append_taa S st1 st2 st3 (taa : trace_any_any S st1 st2) on taa : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝ match taa with [ taa_base st1' ⇒ λst3,taa2.taa2 | taa_step st1' st2' st3' H I J tl ⇒ λst3,taa2. taa_step ???? H I J (taa_append_taa … tl taa2) ] st3. lemma associative_taa_append_tal : ∀S,s1,s2,fl,s3,s4. ∀taa1 : trace_any_any S s1 s2. ∀taa2 : trace_any_any S s2 s3. ∀tal : trace_any_label S fl s3 s4. (taa_append_taa … taa1 taa2) @ tal = taa1 @ taa2 @ tal. #S #s1 #s2 #fl #s3 #s4 #taa1 elim taa1 -s1 -s2 [ #s1 #taa2 #tal % | #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal normalize >IH % ] qed. lemma associative_taa_append_taa : ∀S,s1,s2,s3,s4. ∀taa1 : trace_any_any S s1 s2. ∀taa2 : trace_any_any S s2 s3. ∀taa3 : trace_any_any S s3 s4. taa_append_taa … (taa_append_taa … taa1 taa2) taa3 = taa_append_taa … taa1 (taa_append_taa … taa2 taa3). #S #s1 #s2 #s3 #s4 #taa1 elim taa1 -s1 -s2 [ #s1 #taa2 #tal % | #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal normalize >IH % ] qed. let rec taa_append_tal_rel S1 fl1 st1 st1' (tal1 : trace_any_label S1 fl1 st1 st1') S2 st2 st2mid fl2 st2' (taa2 : trace_any_any S2 st2 st2mid) (tal2 : trace_any_label S2 fl2 st2mid st2') on tal1 : tal_rel … tal1 tal2 → tal_rel … tal1 (taa2 @ tal2) ≝ match tal1 return λfl1,st1,st1',tal1.? with [ tal_base_not_return st1 st1' _ _ _ ⇒ ? | tal_base_return st1 st1' _ _ ⇒ ? | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ? | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒ ? | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ? | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ? ]. [ * #EQfl *#st2mid *#taa2' *#H2 *#G2 *#K2 #EQ | * #EQfl *#st2mid *#taa2' *#H2 *#G2 #EQ | * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 * [ *#K2 *#tlr2 *#L2 * #EQ #EQ' | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll ] | * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *#tlr2 * #EQ #EQ' | * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 * [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ' | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #EQ'' ] | whd in ⊢ (%→%); @(taa_append_tal_rel … tl1) ] destruct prf % ] qed. *) lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2. if taa_non_empty … taa then ¬as_costed … s2 else True. #S #s1 #s2 #taa elim taa -s1 -s2 normalize nodelta [ #s1 % | #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl -s2 -s3 [ #s2 #H #K #_ assumption | #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I ] ] qed. let rec tal_collapsable_to_rel S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J. tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) ≝ match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J. tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) with [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_to_rel ???? tl | tal_base_not_return _ st2' _ _ K ⇒ ? | _ ⇒ Ⓧ ]. * #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| % qed. let rec tal_collapsable_eq_flag S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝ match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ? with [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl | tal_base_not_return _ st2' _ _ K ⇒ λ_.refl … | _ ⇒ Ⓧ ]. let rec tal_collapsable_split S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J. tal ≃ taa @ tal_base_not_return … st2 H I J ≝ match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J. tal ≃ taa @ tal_base_not_return … st2_mid ? H I J with [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ? | tal_base_not_return st1' st2' H I J ⇒ ? | _ ⇒ Ⓧ ]. [ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} % | #coll elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J' #EQ %{st2_mid} %{(taa_step … taa)} try assumption %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) -tl #tl #EQ >EQ % ] qed. lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal. tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J. tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal. #S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J elim (tal_collapsable_split … coll) lapply tal >(tal_collapsable_eq_flag … coll) -tal #tal #st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%] %[|%[|%[|%[|%[| % ]]]]] qed. definition taaf_append_tal : ∀S,st1,fl,st2,st3. ∀taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3 ≝ λS,st1,fl,st2,st3,taaf. match taaf return λst1,st2,taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3 with [ taaf_base s ⇒ λ_.λtal.tal | taaf_step s1 s2 s3 hd H I ⇒ λJ,tal.hd @ tal_step_default ????? H tal I J | taaf_step_jump _ _ s3 _ _ _ K ⇒ λJ.Ⓧ(absurd … K J) ]. lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2. tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 → tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2). #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * -H7 -H8 normalize [ // |3: #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 generalize in match (? : False); * ] #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????); EQ1 #EQ2 destruct % |*: @taa_append_tal_rel assumption ] ] | (* tal_base_non_return *) whd cases G -G #G lapply (sim_execute … H st1_R_st2) (* without try it fails... why? *) try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta [ #H lapply (H K) -H ] * #st2' ** -st2 -st2' [1,4: #st2 (* taa2 empty → st1' must be not cost_labelled *) ** whd in ⊢ (%→?); * [1,3: #ncost #R' #L' %2 /4 by conj/ |*: * #ABS elim (ABS K) ] |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 [2,4: #J2 ] *** #st1_R_st2' #st1_L_st2' %1 %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 ??))} [1,4: %1{I2} |7,10: %2{I2} |2,5: assumption |8,11: whd G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); * #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2' ***** #ncost #J2 #K2 #st1_Rret_st2' #st1_Rret_st2' #st1_L_st2' %[2,4:%[2,4: %{(taa_append_tal … taa2 (tal_base_return … K2 J2))} %{taa2'} % [ /4 by conj/ ] %[ % | %[|%[|%[|%[| % ]]]]]]] | (* tal_base_call *) whd lapply (sim_execute … H st1_R_st2) >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H G) -H * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 #st1_R_st2_mid #st1_L_st2_after_call elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call) #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2' [ #st2' #tlr2 ***** |*: #st2_after_ret #st2_after_ret' #st2' #taa2'' #I2 #J2 [2: #K2 ] #tlr2 **** #ncost ] #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1 %{st2'} [ %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)} [3: % [ % assumption ] % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]] ] |*: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 ??))} [2: %1{J2} |6: %2{J2} |4,8: % try (% assumption) % [1,3:%] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4: % [1,3: %{S} % ] /2 by taa_append_collapsable, I/ ]]]]]]]]]] ] ] [1,3,5: @(st1_Rret_st2' … st1_C_st2) assumption |*: whd G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H G) -H * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 #st1_R_st2_mid #st1_L_st2_after_call elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call) #st2_after_ret * #st2' * #tlr2 * #taa2'' * #props #S %{st2_after_ret} %{st2'} %{(taa2 @ tal_base_tailcall ???? H2 G2 tlr2)} %{taa2''} %{props} % [%] %[|%[| %{EQcall} %[|%[|%[|%[| %{S} % ]]]]]] | (* tal_step_call *) lapply (sim_execute … H st1_R_st2) >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H G) -H * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 #st1_R_st2_mid #st1_L_st2_after_call elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call) #st2_after_ret * #st2' * #tlr2 * #taa2'' **** #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2') cases fl1' in tl1; #tl1 * [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S' %[|%[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))} [4: %{taa2'''} % [ /4 by conj/ ] %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]] ]]] | *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1 %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))} [4: % [ /2 by conj/ ] %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]] ]] | lapply S lapply tlr2 lapply st1_Rret_st2' lapply st1_L_st2' lapply st1_R_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2' [ #st2' * #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost %1 %[| %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)} [3: % [ /2 by conj/ ] %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]] |*: #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' [2: #K2'] #ncost #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost' %1 %[2,4: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' ??))} [2: %1{J2'} |6: %2{J2'} |4,8: % [1,3: /2 by conj/] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4: %{S} % [1,3:%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/ ]]]]]]]]]] ]] ] ] [1,4,7,9,11: @(st1_Rret_st2' … st1_C_st2) assumption |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2' [1,4: #st2_after_ret * #L whd in ⊢ (?%); G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); * #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid) cases fl1' in tl1; #tl1 * [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G %[|%[| %{(taaf_append_tal … taa2 ? tal2)} [2: %{taa2'} % [/4 by conj/ ] @taaf_append_tal_rel @G ] ]] | *#st2' *#tal2 *#H #G %1 %[| %{(taaf_append_tal … taa2 ? tal2)} [2: % [/2 by conj/] @taaf_append_tal_rel @G ] ] | (* can't happen *) *** #_ #L' elim (absurd ?? K) whd >st1_L_st2_mid IH >IH >append_nil // qed. lemma ft_extend_taa_obs : ∀S,st1,st2,stack,st3,ft,taa. ft_observables … (ft_extend_taa S st1 st2 stack st3 ft taa) = ft_observables … ft @ if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]. #S #st1 #st2 #stack #st3 #ft #taa lapply ft elim taa -st2 -st3 [ #st2 #ft >append_nil % ] #st2 #st3 #st4 #H #K #G #taa #IH #ft normalize in ⊢ (??(?????%)?); >IH -IH lapply G lapply H cases taa -st3 -st4 normalize nodelta [ #st3 #H #G | #st3 #st4 #st5 #ex #H' #G' #taa #H #G >(not_costed_no_label … G) ] >append_nil whd in ⊢ (??%?); >ft_observables_aux_def >append_nil % qed. lemma ft_extend_taa_advance_call_obs : ∀S,st1,st2,stack,st3,st4. ∀ft : flat_trace S st1 st2 stack. ∀taa : trace_any_any S st2 st3. ∀H : as_execute S st3 st4.∀G. ft_observables … (ft_advance_call … (ft_extend_taa … ft taa) H G) = ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVcall (as_call_ident … «st3, G»)]. #S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G whd in ⊢ (??%?); >ft_observables_aux_def >append_nil >ft_extend_taa_obs lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3 [ #st2 * #ft #H #G >append_nil % | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G >(not_costed_no_label … K) normalize nodelta // ] qed. lemma ft_extend_taa_advance_tailcall_obs : ∀S,st1,st2,stack,f,st3,st4. ∀ft : flat_trace S st1 st2 (f :: stack). ∀taa : trace_any_any S st2 st3. ∀H : as_execute S st3 st4.∀G. ft_observables … (ft_advance_tailcall … (ft_extend_taa … ft taa) H G) = ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVtailcall f (as_tailcall_ident … «st3, G»)]. #S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G whd in ⊢ (??%?); >ft_observables_aux_def >append_nil >ft_extend_taa_obs lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3 [ #st2 * #ft #H #G >append_nil % | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G >(not_costed_no_label … K) normalize nodelta // ] qed. lemma ft_extend_taa_advance_ret_obs : ∀S,st1,st2,stack,f,st3,st4. ∀ft : flat_trace S st1 st2 (f :: stack). ∀taa : trace_any_any S st2 st3. ∀H : as_execute S st3 st4.∀G. ft_observables … (ft_advance_ret … (ft_extend_taa … ft taa) H G) = ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVret f]. #S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G whd in ⊢ (??%?); >ft_observables_aux_def >append_nil >ft_extend_taa_obs lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3 [ #st2 * #ft #H >append_nil % | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H >(not_costed_no_label … K) normalize nodelta // ] qed. lemma ft_extend_taa_advance_flat_obs : ∀S,st1,st2,stack,st3,st4. ∀ft : flat_trace S st1 st2 stack. ∀taa : trace_any_any S st2 st3. ∀H : as_execute S st3 st4.∀G. ft_observables … (ft_advance_flat … (ft_extend_taa … ft taa) H G) = ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l). #S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G whd in ⊢ (??%?); >ft_observables_aux_def >append_nil >ft_extend_taa_obs lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3 [ #st2 * #ft #H >append_nil % | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H >(not_costed_no_label … K) normalize nodelta >append_nil // ] qed. lemma ft_extend_taaf_obs : ∀S,st1,st2,stack,st3,ft,taaf. ft_observables … (ft_extend_taaf S st1 st2 stack st3 ft taaf) = ft_observables … ft @ if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]. #S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa -st2 -st3 [ #st2 #ft >append_nil % ] #st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft @ft_extend_taa_advance_flat_obs qed. (* little helper to avoid splitting equal cases *) lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed-. theorem status_simulation_produce_ft : (* from st1 →→→ft→→→ st1' | R,L | st2 we produce st1 →→→ft→→→ st1'-------\ // \ \ \\ L S // | \ st2 →→→ft→→→ st2_lab →taa→ st2' so that from any tlr or tll following st1' we can produce the corresponding structured trace from st2_lab using the previous result *) ∀S1,S2. ∀R. ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack. status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 → ∃st2_lab,st2'. ∃ft2 : flat_trace S2 st2 st2_lab stack. ∃taa : trace_any_any S2 st2_lab st2'. label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2. #S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack [ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] % |*: #st1_mid #st1' #stack [3,4: #f] #ft1 #ex [3: * [*]] #cl [#ncost_st1'] (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S [1,2: (* other/jump *) lapply (sim_execute … ex G') try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta [ #H lapply (H ncost_st1') -H ] * #st2' *#taaf ** #ncost #G'' #H'' %{st2'} %{st2'} %[1,3: @(ft_extend_taaf … taaf) @(ft_extend_taa … taa) assumption] %{(taa_base …)} % [1,3: %{H'' G''} ] whd in ⊢ (??%?); >ft_observables_aux_def >append_nil lapply ncost lapply taa lapply H'' cases taaf -st2_mid -st2' [1,4: #st2' #H'' #taa * #ncost >ft_extend_taa_obs (not_costed_no_label … ncost) >if_eq >S % |*: lapply L' lapply H'' lapply S lapply ft2 cases taa -st2_lab -st2' [1,3: #st2' #ft2 #S #H'' #L' >append_nil >not_costed_no_label [1,3: >append_nil @S ] whd in ⊢ (?%); >L' S % ] ] |*: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' [2,4: #cst ] #_ #taa * whd in ⊢ (???(?????%)); >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs >S >L' % ] |3: (* tailcall *) lapply (sim_execute … ex G') >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2' * #taa2 * #taa2' ** #ex' #G'' #H'' lapply (refl_jmeq … (ft_advance_tailcall … ft1 ex cl)) generalize in match (ft_advance_tailcall … ft1 ex cl) in ⊢ (????%→%); ft_extend_taa_advance_tailcall_obs lapply EQft1' lapply ft1' -ft1' >EQcall in ⊢ (%→???%%→%); #ft1' #EQft1' destruct (EQft1') whd in ⊢ (??%?); >ft_observables_aux_def >append_nil >S >L' % |4: (* ret *) lapply (sim_execute … ex G') >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); * #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2' ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'} %[@(ft_extend_taaf … taa2') @(ft_advance_ret … f … ex' cl') @(ft_extend_taa … (taa_append_taa … taa taa2)) assumption] %{(taa_base …)} % [ %{H'' G''} ] >ft_extend_taaf_obs >ft_extend_taa_advance_ret_obs whd in ⊢ (??%?); >ft_observables_aux_def >append_nil lapply ncost cases taa2' -st2_after_ret -st2' [ #st2' * >append_nil |*: #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' [2: #cst ] #ncost >(not_costed_no_label … ncost) >if_eq >append_nil ] >S >L' % |5: (* call *) lapply (sim_execute … ex G') >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2' * #taa2 * #taa2' ** #ex' #G'' #H'' %{st2_after_call} %{st2'} lapply (refl_jmeq … (ft_advance_call … ft1 ex cl)) generalize in match (ft_advance_call … ft1 ex cl) in ⊢ (????%→%); ft_extend_taa_advance_call_obs lapply EQft1' lapply ft1' -ft1' >EQcall in ⊢ (%→???%%→%); #ft1' #EQft1' destruct (EQft1') whd in ⊢ (??%?); >ft_observables_aux_def >append_nil >S >L' % ] ] qed.