Changeset 2755 for src/common/stacksize.ma
 Timestamp:
 Mar 1, 2013, 11:06:29 AM (8 years ago)
 File:

 1 moved
Legend:
 Unmodified
 Added
 Removed

src/common/stacksize.ma
r2747 r2755 1 1 include "basics/lists/list.ma". 2 include "joint/joint_semantics.ma".3 include "common/Executions.ma".4 2 include "common/StructuredTraces.ma". 5 3 6 inductive call_ud (p: params) (globals: list ident): Type [0] ≝ 7  up: joint_internal_function p globals → call_ud p globals (* call *) 8  down: joint_internal_function p globals → call_ud p globals. (* return *) 9 10 let rec max_stacksize (p: params) (g: list ident) (fn_list: list (call_ud p g)) 11 (curr: nat) (max: nat) on fn_list: nat ≝ 12 match fn_list with 13 [ nil ⇒ max 14  cons h t ⇒ match h with 15 [ up f ⇒ let new_stack ≝ curr + joint_if_stacksize … f in 16 if leb max new_stack 17 then max_stacksize … t new_stack new_stack 18 else max_stacksize … t new_stack max 19  down f ⇒ let new_stack ≝ curr  joint_if_stacksize … f in 20 max_stacksize … t new_stack max 21 ] 22 ]. 4 inductive call_ud : Type [0] ≝ 5  up: ident → call_ud (* call *) 6  down: ident → call_ud. (* return *) 23 7 24 let rec extract_list_from_tlr (p: params) (g: list ident) 25 (lg: ident → joint_internal_function p g) (top_f: ident) 26 (S: abstract_status) (s,s':S) (tr: trace_label_return S s s') 27 (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ 28 match tr with 29 [ tlr_base s1 s2 tll ⇒ 30 extract_list_from_tll … lg top_f … tll res 31  tlr_step s1 s2 s3 tll tlr ⇒ 32 let res' ≝ extract_list_from_tll … lg top_f … tll res in 33 extract_list_from_tlr … lg top_f … tlr res' 34 ] 35 and extract_list_from_tll (p: params) (g: list ident) 36 (lg: ident → joint_internal_function p g) (top_f: ident) 37 (S: abstract_status) ends (s,s':S) (tr: trace_label_label S ends s s') 38 (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ 39 match tr with 40 [ tll_base ends s1 s2 tal co ⇒ 41 extract_list_from_tal … lg top_f … tal res 42 ] 43 and extract_list_from_tal (p: params) (g: list ident) 44 (lg: ident → joint_internal_function p g) (top_f: ident) 45 (S: abstract_status) ends (s,s':S) (tr: trace_any_label S ends s s') 46 (res: list (call_ud p g)) on tr: list (call_ud p g) ≝ 47 match tr with 48 [ tal_base_not_return s1 s2 ex cl co ⇒ res 49  tal_base_return s1 s2 ex cl ⇒ down ?? (lg top_f)::res 50  tal_base_call s1p s1s s2 ex cl ar tlr co ⇒ 51 extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr 52 (up ?? (lg (as_call_ident ? «s1p,cl»))::res) 53  tal_base_tailcall s1p s1s s2 ex cl tlr ⇒ 54 extract_list_from_tlr ?? lg (as_tailcall_ident ? «s1p,cl») … tlr 55 (up ?? (lg (as_tailcall_ident ? «s1p,cl»))::down … (lg top_f)::res) 56  tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒ 57 let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr 58 (up ?? (lg (as_call_ident ? «s1p,cl»))::res) in 59 extract_list_from_tal … lg top_f … tal res' 60  tal_step_default end s1p s1i s1e ex tal cl co ⇒ 61 extract_list_from_tal … lg top_f … tal res 62 ]. 8 record stacksize_info : Type[0] ≝ 9 { current : ℕ ; maximum : ℕ }. 63 10 64 let rec tlr_rel_extract_equal (p: params) (g: list ident) 65 (lg: ident → joint_internal_function p g) (top_f: ident) 66 S1 S2 s1 s1' s2 s2' t1 t2 on t1: 67 tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 → 68 ∀res.extract_list_from_tlr p g lg top_f S1 s1 s1' t1 res = 69 extract_list_from_tlr p g lg top_f S2 s2 s2' t2 res ≝ 70 match t1 with 71 [ tlr_base st1 st1' tll1 ⇒ ? 72  tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ? 73 ] 74 and tll_rel_extract_equal (p: params) (g: list ident) 75 (lg: ident → joint_internal_function p g) (top_f: ident) 76 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: 77 t1 ≈ t2 → 78 ∀res.extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 res = 79 extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 res ≝ 80 match t1 with 81 [ tll_base ends st1 st1' tal1 co ⇒ ? 82 ] 83 and tal_rel_extract_equal (p: params) (g: list ident) 84 (lg: ident → joint_internal_function p g) (top_f: ident) 85 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: 86 t1 ≈ t2 → 87 ∀res.extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 res = 88 extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 res ≝ 89 match t1 with 90 [ tal_base_not_return st1 st1' ex cl co ⇒ ? 91  tal_base_return st1 st1' ex cl ⇒ ? 92  tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ? 93  tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ? 94  tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ? 95  tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? 96 ]. 97 [ cases t2 98 [ #st2 #st2' #tll2 normalize #Hsim @(tll_rel_extract_equal … Hsim) 99  #st2 #st2' #st2'' #tll2 #tlr2 normalize #abs cases abs 100 ] 101  cases t2 102 [ #st2 #st2' #tll2 normalize #abs cases abs 103  #st2 #st2' #st2'' #tll2 #tlr2 normalize #Hsim #res 104 >(tll_rel_extract_equal p g lg top_f … (proj1 ?? Hsim) res) 105 @(tlr_rel_extract_equal … (proj2 ?? Hsim)) 106 ] 107  cases t2 #ends' #st2 #st2' #tal2 #co' normalize * #H1 #H2 108 @(tal_rel_extract_equal … H2) 109  cases t2 110 [ #st2 #st2' #ex' #cl' #co' normalize #Hsim #res % 111  #st2 #st2' #ex' #cl' * #abs destruct (abs) 112  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #H1 * #st2mid * 113 #taa * #H * #G * #K inversion taa in ⊢ ?; 114 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 115  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 116 normalize #abs destruct (abs) 117 ] 118  #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #H1 * #st2mid * 119 #taa * #H * #G * #K inversion taa in ⊢ ?; 120 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 121  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 122 normalize #abs destruct (abs) 123 ] 124  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize * 125 #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?; 126 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 127  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 128 normalize #abs destruct (abs) 129 ] 130  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * #taa 131 * #H * #G * #K inversion taa in ⊢ ?; 132 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 133  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 134 destruct normalize #Hsim destruct (Hsim) (* getting somewhere. Use Hind? *) 135 cases daemon 136 ] 137 ] 138  cases t2 139 [ #st2 #st2' #ex' #cl' #co' normalize * #abs destruct (abs) 140  #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % 141  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs) 142  #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #abs destruct (abs) 143  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 144 normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?; 145 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 146  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 147 normalize #abs destruct (abs) 148 ] 149  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid 150 * #taa * #H * #G inversion taa in ⊢ ?; 151 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 152  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 153 destruct normalize #Hsim destruct (Hsim) 154 cases daemon (* use Hind again? *) 155 ] 156 ] 157  cases t2 158 [ #st2 #st2' #ex' #cl' #co' normalize * #_ * #st2mid * #G * #ident_eq * #taa 159 * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2 * #L * #H1 160 [ * * #H3 #H2 #H4  #H2 ] 161 inversion taa in ⊢ ?; 162 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H3; destruct (H3) 163  #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 164 normalize in H3; destruct (H3) 165  #st2mid''' #eq1 #eq2 #eq3 destruct normalize normalize in H1; destruct (H1) 166  #st2'' #st2''' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 167 normalize in H1; destruct (H1) 168 ] 169  #st2 #st2' #ex' #cl' normalize * #abs destruct (abs) 170  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #_ * #st2mid * #G 171 * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] #K * #tlr2' * #L 172 [* #tl2] 173 inversion taa in ⊢ ?; 174 [ #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 175  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 176 destruct normalize * * #abs destruct (abs) 177  #st2mid'' #eq1 #eq2 #eq3 destruct normalize * #H1 #H2 #res 178 >(tlr_rel_extract_equal p g lg … H2) destruct (H1) 179 >ident_eq % 180  #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 181 destruct normalize * #abs destruct (abs) 182 ] 183  (* tail call case *) cases daemon 184  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize 185 * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] 186 #K * #tlr2' * #L [* #tl2] 187 inversion taa in ⊢ ?; 188 [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res 189 destruct (H1) >(tlr_rel_extract_equal … H2) >ident_eq 190 (* to do here: destruct tl2: 3 cases by contradiction, 1 by equality and 1 by 191 * not sure yet *) cases daemon 192 2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 193 destruct normalize * * [#abs destruct (abs)] #H2 #res <ident_eq 194 >(tlr_rel_extract_equal … H2) cases daemon (* stumped here *) 195 ] 196  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #H1 * #st2mid * 197 #G * #ident_eq * #taa * #st2mid' * #H * * [2: #stmid'' * ] #K * #tlr2 * #L 198 [* #tl2] 199 inversion taa in ⊢ ?; 200 [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * [*] #H1 #H2 [#H3] #res 201 destruct (H1) 202 2,4: #st2p' #st2p'' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 203 destruct normalize * [*] #H1 #H2 [#H3] #res destruct (H1) <ident_eq 204 >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *) 205 ] 206 ] 207  (* tail call case *) cases daemon 208  cases t2 209 [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa * 210 #st2mid' * #H * * [#_  #st2mid''] * #K * #tlr2 * #L [2: * #tl2] 211 inversion taa in ⊢ ?; 212 [1,3: #st2mid'' #eq1 #eq2 #eq3 destruct normalize * * #H1 destruct (H1) 213 2,4: #st2p #st2p' #st2mid'' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 214 destruct normalize * * #H1 destruct (H1) 215 ] 216  #st2 #st2' #ex' #cl' normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' 217 * #H * * [#abs destruct (abs)] #st2mid' * #K * #tlr2 * #L * #tl2 218 inversion taa in ⊢ ?; 219 [ #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 220  #st2p #st2p' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 221 normalize * * #abs destruct (abs) 222 ] 223  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #st2mid * #G * 224 #ident_eq * #taa * #st2mid' * #H * * [ #_  #st2mid'' ] * #K * #tlr2' * #L 225 [2: * #tl2] 226 inversion taa in ⊢ ?; 227 [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res 228 destruct (H1) >ident_eq >(tlr_rel_extract_equal … H3) 229 cases tal1 in H2; 230 [ #ss #sf #ex'' #cl'' #co'' normalize #_ % 231  #ss #sf #ex'' #cl'' normalize #abs cases abs 232  #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs 233  #st1p' #st1s #sf #ex'' #cl'' #tlr1' normalize #abs cases abs 234  #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1' 235 normalize #abs cases abs 236  #end' #st1p' #st1i #st1e #ex'' #tal1' #cl'' #co'' normalize 237 cases daemon (* use induction here, but no *) 238 ] 239 2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 240 destruct normalize * * #abs destruct (abs) 241 ] 242  (* tail call case *) cases daemon 243  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 244 normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * 245 [ #H1  #st2mid''] * #K * #tlr2' * #L [2: * #tl2] inversion taa in ⊢ ?; 246 [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #H1 #H2 #H3 #res 247 destruct (H1) >ident_eq >(tal_rel_extract_equal … H2) 248 >(tlr_rel_extract_equal … H3) % 249 2,4: #st2p' #st2p'' #st2mid''' #ex''' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 250 destruct normalize * * #abs destruct (abs) 251 ] 252  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' normalize * #st2mid * #G * 253 #ident_eq * #taa * #st2mid' * #H * * [ #He  #st2mid'' ] * #K * #tlr2' * #L 254 [2: * #tl2] inversion taa in ⊢ ?; 255 [1,3: #st2mid''' #eq1 #eq2 #eq3 destruct normalize * * #abs destruct (abs) 256 2,4: #st2p' #st2p'' #st2mid''' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 257 destruct normalize * * #H1 #H2 #H3 #res destruct (H1) 258 >(tlr_rel_extract_equal … H3) <ident_eq normalize cases daemon 259 (* look further here *) 260 ] 261 ] 262  cases t2 263 [ #st2 #st2' #ex' #cl' #co' 264  #ss #fs #ex' #cl' 265  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' 266  #st2p #st2s #st2' #ex' #cl' #tlr2 267  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 268  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' 269 ] 270 normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim) 271 ] 272 (* Another tailcall case escaped *) cases daemon 11 definition update_stacksize_info : 12 (ident → option ℕ) → stacksize_info → list call_ud → stacksize_info ≝ 13 λstacksizes. 14 let get_stacksize ≝ 15 λf.match stacksizes f with 16 [ Some n ⇒ n  None ⇒ 0 (* should never happen *) ] in 17 let f ≝ λud,acc. 18 match ud with 19 [ up i ⇒ 20 let new_stack ≝ get_stacksize i + current acc in 21 let new_max ≝ max (maximum acc) new_stack in 22 mk_stacksize_info new_stack new_max 23  down i ⇒ 24 let new_stack ≝ current acc  get_stacksize i in 25 mk_stacksize_info new_stack (maximum acc) 26 ] in 27 foldr ?? f. 28 29 definition extract_call_ud_from_observables : 30 list intensional_event → list call_ud ≝ 31 let f ≝ λev.match ev with 32 [ IEVcall i ⇒ [up i]  IEVtailcall i j ⇒ [down i; up j]  IEVret i ⇒ [down i]  _ ⇒ [ ]] in 33 foldr ?? (λev.append ? (f ev)) [ ]. 34 35 definition extract_call_ud_from_tlr : 36 ∀S,st1,st2.trace_label_return S st1 st2 → ident → list call_ud ≝ 37 λS,st1,st2,tlr,curr. 38 extract_call_ud_from_observables … (observables_trace_label_return … tlr curr). 39 40 definition extract_call_ud_from_tll : 41 ∀S,fl,st1,st2.trace_label_label fl S st1 st2 → ident → list call_ud ≝ 42 λS,fl,st1,st2,tll,curr. 43 extract_call_ud_from_observables … (observables_trace_label_label … tll curr). 44 45 lemma tlr_rel_same_stacksize_info : 46 ∀stacksizes. 47 ∀S1,S2,s1,s1',s2,s2'. 48 ∀tlr1 : trace_label_return S1 s1 s1'. 49 ∀tlr2 : trace_label_return S2 s2 s2'. 50 ∀curr.∀curr_stacksize. 51 tlr_rel … tlr1 tlr2 → 52 update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tlr … tlr1 curr) = 53 update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tlr … tlr2 curr). 54 #stacksizes #S1 #S2 #s1 #s1' #s2 #s2' #tlr1 #tlr2 #curr #info 55 #equiv @eq_f whd in ⊢ (??%%); @eq_f 56 @tlr_rel_to_traces_same_observables assumption 273 57 qed. 274 58 275 let rec tlr_rel_max_equal (p: params) (g: list ident) 276 (lg: ident → joint_internal_function p g) (top_f: ident) 277 S1 S2 s1 s1' s2 s2' t1 t2 on t1: 278 tlr_rel S1 s1 s1' S2 s2 s2' t1 t2 → 279 max_stacksize p g (extract_list_from_tlr p g lg top_f S1 s1 s1' t1 []) = 280 max_stacksize p g (extract_list_from_tlr p g lg top_f S2 s2 s2' t2 []) ≝ 281 match t1 with 282 [ tlr_base st1 st1' tll1 ⇒ ? 283  tlr_step st1 st1' st1'' tll1 tlr1 ⇒ ? 284 ] 285 and tll_rel_max_equal (p: params) (g: list ident) 286 (lg: ident → joint_internal_function p g) (top_f: ident) 287 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: 288 t1 ≈ t2 → 289 max_stacksize p g (extract_list_from_tll p g lg top_f S1 e1 s1 s1' t1 []) = 290 max_stacksize p g (extract_list_from_tll p g lg top_f S2 e2 s2 s2' t2 []) ≝ 291 match t1 with 292 [ tll_base ends st1 st1' tal1 co ⇒ ? 293 ] 294 and tal_rel_max_equal (p: params) (g: list ident) 295 (lg: ident → joint_internal_function p g) (top_f: ident) 296 S1 S2 e1 e2 s1 s1' s2 s2' t1 t2 on t1: 297 t1 ≈ t2 → 298 max_stacksize p g (extract_list_from_tal p g lg top_f S1 e1 s1 s1' t1 []) = 299 max_stacksize p g (extract_list_from_tal p g lg top_f S2 e2 s2 s2' t2 []) ≝ 300 match t1 with 301 [ tal_base_not_return st1 st1' ex cl co ⇒ ? 302  tal_base_return st1 st1' ex cl ⇒ ? 303  tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ? 304  tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ? 305  tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ? 306  tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? 307 ]. 308 [1,2: #Hsim >(tlr_rel_extract_equal … Hsim []) % 309 3: #Hsim >(tll_rel_extract_equal … Hsim []) % 310 *: #Hsim >(tal_rel_extract_equal … Hsim []) % 311 ] 59 lemma tll_rel_same_stacksize_info : 60 ∀stacksizes. 61 ∀S1,S2,fl1,fl2,s1,s1',s2,s2'. 62 ∀tll1 : trace_label_label S1 fl1 s1 s1'. 63 ∀tll2 : trace_label_label S2 fl2 s2 s2'. 64 ∀curr.∀curr_stacksize. 65 tll_rel … tll1 tll2 → 66 update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tll … tll1 curr) = 67 update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tll … tll2 curr). 68 #stacksizes #S1 #S2 #fl1 #fl2 #s1 #s1' #s2 #s2' #tlr1 #tlr2 #curr #info 69 #equiv @eq_f whd in ⊢ (??%%); @eq_f 70 @tll_rel_to_traces_same_observables assumption 312 71 qed.
Note: See TracChangeset
for help on using the changeset viewer.