source: src/ASM/CostsProof.ma @ 1501

Last change on this file since 1501 was 1501, checked in by sacerdot, 8 years ago

We must take in account the labelled_p predicate.

File size: 2.6 KB
Line 
1include "ASM/ASMCosts.ma".
2include "ASM/WellLabeled.ma".
3include "ASM/Status.ma".
4
5inductive trace_lab_ret: Type[0] ≝
6   sing: ∀p. trace_lab_lab true p → structured_trace
7 | cons:
8    ∀p. trace_lab_lab false p → ∀tr:trace_lab_ret.
9     execute 1 (last p) = hd tr →
10      structured_trace
11
12with trace_lab_lab0: bool → Type[0] ≝ (* true = ends with ret *)
13   final:
14    ∀hd.
15     fetch hd ≠ Ret … ≠ JmpA →
16     fetch (execute 1 hd) = Cost … →
17      trace_lab_lab0 false
18 | final_ret:
19    ∀hd.
20     fetch hd = Ret … → trace_lab_lab0 true
21 | final_jmp:
22    ∀hd.
23     fetch hd = JmpA … →
24      fetch (execute 1 hd) = Cost … →
25       trace_lab_lab0 false
26 | call:
27    ∀b.∀bf.∀trace:trace_lab_ret.∀af,tl.
28     trace_lab_lab0 b tl →
29     fetch bf = Call … →
30     pc af = pc bf + 2 →
31      execute 1 bf = hd trace →
32      execute 1 (last trace) = af →
33       trace_lab_lab
34 | other:
35    ∀b.∀hd,tl.
36     trace_lab_lab0 b tl →
37     fetch hd ≠ Call … →
38     fetch (execute 1 hd) ≠ Cost … →
39     fetch hd ≠ Ret … ≠ JmpA →
40      simple_path_0
41
42with trace_lab_lab: bool → Type[0] ≝
43 mk_trace_lab_lab: ∀b.∀p:trace_lab_lab0 b → is_labelled (hd p) → trace_lab_lab b.
44
45definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
46
47lemma simple_path_ok:
48 ∀st: Status.∀H.
49 let p ≝ compute_simple_path0 st H in
50   ∀n.
51    nth_path n p = execute n st ∧
52     (execute' (path_length p) st = 〈st',τ〉 →
53      τ = cost_trace p)
54  ].
55
56let rec trace_lab_rec_cost (p: trace_lab_ret) : nat. COUNTS EVERYTHING
57
58lemma trace_lab_rec_cost_ok:
59 ∀p: trace_lab_rec.
60  trace_lab_rec_cost p = Timer (last p) - Timer (first p).
61
62let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
63 match p with
64 [ call ⇒ DO NOT ADD ANYTHING
65 | _ ⇒ DO ADD ].
66
67let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
68 | (call b bf tr af tl) as self ⇒
69    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
70    trace_lab_rec_cost' tl
71
72theorem main_lemma:
73 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
74
75axiom lemma1:
76 ∀p: simple_path.
77  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
78
79axiom lemma2:
80 ∀s,l,cost_map.
81  is_labelled l s →
82   traverse_cost_internal s = cost_map l.
83
84axiom main_statement:
85 ∀s.
86 ∀cost_map.
87 let p ≝ compute_simple_path0 s in
88 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
89
90axiom main_statement:
91 ∀s.
92 ∀cost_map.
93 let p ≝ compute_simple_path0 s in
94  execute' (path_length p) s = 〈s',τ〉 →
95   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracBrowser for help on using the repository browser.