| 1 | include "basics/lists/list.ma". |
|---|
| 2 | include "common/StructuredTraces.ma". |
|---|
| 3 | |
|---|
| 4 | inductive call_ud : Type [0] ≝ |
|---|
| 5 | | up: ident → call_ud (* call *) |
|---|
| 6 | | down: ident → call_ud. (* return *) |
|---|
| 7 | |
|---|
| 8 | record stacksize_info : Type[0] ≝ |
|---|
| 9 | { current : ℕ ; maximum : ℕ }. |
|---|
| 10 | |
|---|
| 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 |
|---|
| 57 | qed. |
|---|
| 58 | |
|---|
| 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 |
|---|
| 71 | qed. |
|---|
