| 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 ≝ λacc,ud. |
|---|
| 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 | foldl ?? f. |
|---|
| 28 | |
|---|
| 29 | lemma foldr_append : ∀A,B,f,b,l1,l2. |
|---|
| 30 | foldr A B f b (l1@l2) = foldr A B f (foldr A B f b l2) l1. |
|---|
| 31 | #A #B #f #b #l1 elim l1 -l1 [#l2 %] |
|---|
| 32 | #hd #tl #IH #l2 whd in ⊢ (??%%); >IH % |
|---|
| 33 | qed. |
|---|
| 34 | |
|---|
| 35 | lemma foldl_append : ∀A,B,f,b,l1,l2. |
|---|
| 36 | foldl A B f b (l1@l2) = foldl A B f (foldl A B f b l1) l2. |
|---|
| 37 | #A #B #f #b #l1 lapply b -b elim l1 -l1 [#b #l2 %] |
|---|
| 38 | #hd #tl #IH #b #l2 whd in ⊢ (??%(????%?)); >IH % |
|---|
| 39 | qed. |
|---|
| 40 | |
|---|
| 41 | lemma update_stacksize_info_append : |
|---|
| 42 | ∀ss,info,l1,l2. |
|---|
| 43 | update_stacksize_info ss info (l1 @ l2) = |
|---|
| 44 | update_stacksize_info ss (update_stacksize_info ss info l1) l2. |
|---|
| 45 | #ss #info @foldl_append qed. |
|---|
| 46 | |
|---|
| 47 | definition extract_call_ud_from_observables : |
|---|
| 48 | list intensional_event → list call_ud ≝ |
|---|
| 49 | let f ≝ λev.match ev with |
|---|
| 50 | [ IEVcall i ⇒ [up i] | IEVtailcall i j ⇒ [down i; up j] | IEVret i ⇒ [down i] | _ ⇒ [ ]] in |
|---|
| 51 | foldr ?? (λev.append ? (f ev)) [ ]. |
|---|
| 52 | |
|---|
| 53 | lemma extract_call_ud_from_observables_append : |
|---|
| 54 | ∀l1,l2.extract_call_ud_from_observables (l1@l2) = |
|---|
| 55 | extract_call_ud_from_observables l1 @ extract_call_ud_from_observables l2. |
|---|
| 56 | #l1 elim l1 -l1 [ #l2 % ] |
|---|
| 57 | #hd #tl #IH #l2 whd in ⊢ (??%(??%?)); >associative_append @eq_f @IH qed. |
|---|
| 58 | |
|---|
| 59 | lemma update_stacksize_info_max_monotone : |
|---|
| 60 | ∀ss,info,l.maximum info ≤ maximum (update_stacksize_info ss info l). |
|---|
| 61 | #ss #info #l lapply info elim l -l [ #info % ] |
|---|
| 62 | * #id #tl #IH #info |
|---|
| 63 | whd in match (update_stacksize_info ???); normalize nodelta |
|---|
| 64 | change with (update_stacksize_info ???) in ⊢ (??(?%)); |
|---|
| 65 | @(transitive_le ???? (IH …)) |
|---|
| 66 | [ whd in ⊢ (??%); @(leb_elim (?:ℕ)) #H ] // |
|---|
| 67 | qed. |
|---|
| 68 | |
|---|
| 69 | definition extract_call_ud_from_tlr : |
|---|
| 70 | ∀S,st1,st2.trace_label_return S st1 st2 → ident → list call_ud ≝ |
|---|
| 71 | λS,st1,st2,tlr,curr. |
|---|
| 72 | extract_call_ud_from_observables … (observables_trace_label_return … tlr curr). |
|---|
| 73 | |
|---|
| 74 | definition extract_call_ud_from_tll : |
|---|
| 75 | ∀S,fl,st1,st2.trace_label_label fl S st1 st2 → ident → list call_ud ≝ |
|---|
| 76 | λS,fl,st1,st2,tll,curr. |
|---|
| 77 | extract_call_ud_from_observables … (observables_trace_label_label … tll curr). |
|---|
| 78 | |
|---|
| 79 | lemma tlr_rel_same_stacksize_info : |
|---|
| 80 | ∀stacksizes. |
|---|
| 81 | ∀S1,S2,s1,s1',s2,s2'. |
|---|
| 82 | ∀tlr1 : trace_label_return S1 s1 s1'. |
|---|
| 83 | ∀tlr2 : trace_label_return S2 s2 s2'. |
|---|
| 84 | ∀curr.∀curr_stacksize. |
|---|
| 85 | tlr_rel … tlr1 tlr2 → |
|---|
| 86 | update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tlr … tlr1 curr) = |
|---|
| 87 | update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tlr … tlr2 curr). |
|---|
| 88 | #stacksizes #S1 #S2 #s1 #s1' #s2 #s2' #tlr1 #tlr2 #curr #info |
|---|
| 89 | #equiv @eq_f whd in ⊢ (??%%); @eq_f |
|---|
| 90 | @tlr_rel_to_traces_same_observables assumption |
|---|
| 91 | qed. |
|---|
| 92 | |
|---|
| 93 | lemma tll_rel_same_stacksize_info : |
|---|
| 94 | ∀stacksizes. |
|---|
| 95 | ∀S1,S2,fl1,fl2,s1,s1',s2,s2'. |
|---|
| 96 | ∀tll1 : trace_label_label S1 fl1 s1 s1'. |
|---|
| 97 | ∀tll2 : trace_label_label S2 fl2 s2 s2'. |
|---|
| 98 | ∀curr.∀curr_stacksize. |
|---|
| 99 | tll_rel … tll1 tll2 → |
|---|
| 100 | update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tll … tll1 curr) = |
|---|
| 101 | update_stacksize_info stacksizes curr_stacksize (extract_call_ud_from_tll … tll2 curr). |
|---|
| 102 | #stacksizes #S1 #S2 #fl1 #fl2 #s1 #s1' #s2 #s2' #tlr1 #tlr2 #curr #info |
|---|
| 103 | #equiv @eq_f whd in ⊢ (??%%); @eq_f |
|---|
| 104 | @tll_rel_to_traces_same_observables assumption |
|---|
| 105 | qed. |
|---|
