source: src/common/stacksize.ma @ 2768

Last change on this file since 2768 was 2755, checked in by tranquil, 7 years ago
  • changed primitives of abstract status (with stuf that is probably already there in all of its implementations): this temporarily breaks current as creations
  • generalised stacksize file and consequently moved it to common
File size: 2.7 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 ≝ λ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
29definition extract_call_ud_from_observables :
30  list intensional_event → list call_ud ≝
31let f ≝ λev.match ev with
32[ IEVcall i ⇒ [up i] | IEVtailcall i j ⇒ [down i; up j] | IEVret i ⇒ [down i] | _ ⇒ [ ]] in
33foldr ?? (λev.append ? (f ev)) [ ].
34
35definition 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
40definition 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
45lemma 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
57qed.
58
59lemma 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
71qed.
Note: See TracBrowser for help on using the repository browser.