source: src/common/stacksize.ma @ 3367

Last change on this file since 3367 was 3145, checked in by tranquil, 7 years ago
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File size: 3.9 KB
Line 
1include "basics/lists/list.ma".
2include "common/StructuredTraces.ma".
3
4inductive call_ud : Type [0] ≝
5  | up: ident → call_ud    (* call *)
6  | down: ident → call_ud. (* return *)
7
8record stacksize_info : Type[0] ≝
9{ current : ℕ ; maximum : ℕ }.
10
11definition 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
29lemma foldr_append : ∀A,B,f,b,l1,l2.
30foldr 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 %
33qed.
34
35lemma foldl_append : ∀A,B,f,b,l1,l2.
36foldl 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 %
39qed.
40
41lemma update_stacksize_info_append :
42∀ss,info,l1,l2.
43update_stacksize_info ss info (l1 @ l2) =
44update_stacksize_info ss (update_stacksize_info ss info l1) l2.
45#ss #info @foldl_append qed.
46
47definition extract_call_ud_from_observables :
48  list intensional_event → list call_ud ≝
49let f ≝ λev.match ev with
50[ IEVcall i ⇒ [up i] | IEVtailcall i j ⇒ [down i; up j] | IEVret i ⇒ [down i] | _ ⇒ [ ]] in
51foldr ?? (λev.append ? (f ev)) [ ].
52
53lemma 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
59lemma 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
63whd in match (update_stacksize_info ???); normalize nodelta
64change with (update_stacksize_info ???) in ⊢ (??(?%));
65@(transitive_le ???? (IH …))
66[ whd in ⊢ (??%); @(leb_elim (?:ℕ)) #H ] //
67qed.
68
69definition 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
74definition 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
79lemma 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
91qed.
92
93lemma 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
105qed.
Note: See TracBrowser for help on using the repository browser.