source: src/ASM/CostsProof.ma @ 1500

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

Proof sketch for one of the two main proofs.

File size: 2.4 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 … →
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 | call:
22    ∀b.∀bf.∀trace:trace_lab_ret.∀af,tl.
23     trace_lab_lab0 b tl →
24     fetch bf = Call … →
25     pc af = pc bf + 2 →
26      execute 1 bf = hd trace →
27      execute 1 (last trace) = af →
28       trace_lab_lab
29 | other:
30    ∀b.∀hd,tl.
31     trace_lab_lab0 b tl →
32     fetch hd ≠ Call … →
33     fetch (execute 1 hd) ≠ Cost … →
34     fetch hd ≠ Ret … →
35      simple_path_0
36
37with trace_lab_lab: bool → Type[0] ≝
38 mk_trace_lab_lab: ∀b.∀p:trace_lab_lab0 b → is_labelled (hd p) → trace_lab_lab b.
39
40definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s): trace_lab_ret ≝ ….
41
42lemma simple_path_ok:
43 ∀st: Status.∀H.
44 let p ≝ compute_simple_path0 st H in
45   ∀n.
46    nth_path n p = execute n st ∧
47     (execute' (path_length p) st = 〈st',τ〉 →
48      τ = cost_trace p)
49  ].
50
51let rec trace_lab_rec_cost (p: trace_lab_ret) : nat. COUNTS EVERYTHING
52
53lemma trace_lab_rec_cost_ok:
54 ∀p: trace_lab_rec.
55  trace_lab_rec_cost p = Timer (last p) - Timer (first p).
56
57let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
58 match p with
59 [ call ⇒ DO NOT ADD ANYTHING
60 | _ ⇒ DO ADD ].
61
62let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
63 | (call b bf tr af tl) as self ⇒
64    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
65    trace_lab_rec_cost' tl
66
67theorem main_lemma:
68 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
69
70axiom lemma1:
71 ∀p: simple_path.
72  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
73
74axiom lemma2:
75 ∀s,l,cost_map.
76  is_labelled l s →
77   traverse_cost_internal s = cost_map l.
78
79axiom main_statement:
80 ∀s.
81 ∀cost_map.
82 let p ≝ compute_simple_path0 s in
83 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
84
85axiom main_statement:
86 ∀s.
87 ∀cost_map.
88 let p ≝ compute_simple_path0 s in
89  execute' (path_length p) s = 〈s',τ〉 →
90   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracBrowser for help on using the repository browser.