source: src/ASM/CostsProof.ma @ 1503

Last change on this file since 1503 was 1503, checked in by mulligan, 8 years ago

inductive type complete
File size: 6.3 KB
Line 
1include "ASM/ASMCosts.ma".
2include "ASM/WellLabeled.ma".
3include "ASM/Status.ma".
4
5definition is_jump_p ≝
6  λs.
7  match s with
8  [ AJMP _ ⇒ True
9  | LJMP _ ⇒ True
10  | SJMP _ ⇒ True
11  | JMP _ ⇒ True
12  | RealInstruction ri ⇒
13    match ri with
14    [ JZ _ ⇒ True
15    | JNZ _ ⇒ True
16    | JC _ ⇒ True
17    | JNC _ ⇒ True
18    | JB _ _ ⇒ True
19    | JNB _ _ ⇒ True
20    | JBC _ _ ⇒ True
21    | CJNE _ _ ⇒ True
22    | DJNZ _ _ ⇒ True
23    | _ ⇒ False
24    ]
25  | _ ⇒ False
26  ].
27
28definition is_call_p ≝
29  λs.
30  match s with
31  [ ACALL _ ⇒ True
32  | LCALL _ ⇒ True
33  | _ ⇒ False
34  ].
35
36definition size_of_next_instruction ≝
37  λs: Status.
38  let 〈ignore, ignore, cost〉 ≝ fetch (code_memory … s) (program_counter … s) in
39    cost.
40
41definition next_instruction_properly_relates_program_counters ≝
42  λbefore: Status.
43  λafter : Status.
44  let size ≝ size_of_next_instruction before in
45  let pc_before ≝ program_counter … before in
46  let pc_after ≝ program_counter … after in
47  let 〈carry, sum〉 ≝ half_add … pc_before (bitvector_of_nat … size) in
48    sum = pc_after.
49
50definition next_instruction ≝
51  λs: Status.
52  let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in
53    instruction.
54
55inductive trace_ends_with_ret: Type[0] ≝
56  | ends_with_ret: trace_ends_with_ret
57  | doesnt_end_with_ret: trace_ends_with_ret.
58
59axiom next_instruction_is_labelled:
60  ∀s: Status. Prop.
61
62inductive trace_label_return (cost_labels: BitVectorTrie Byte 16): Status → Status → Type[0] ≝
63  | tlr_base:
64      ∀status_before: Status.
65      ∀status_after: Status.
66        trace_label_label cost_labels ends_with_ret status_before status_after →
67        trace_label_return cost_labels status_before status_after
68  | tlr_step:
69      ∀status_initial: Status.
70      ∀status_pre_fun_call: Status.
71        trace_label_label cost_labels doesnt_end_with_ret status_initial status_pre_fun_call →
72          ∀status_start_fun_call: Status.
73          ∀status_end_fun_call: Status.
74          ∀fun_call_trace: trace_label_return cost_labels status_start_fun_call status_end_fun_call.
75            execute 1 status_pre_fun_call = status_start_fun_call →
76              trace_label_return cost_labels status_initial status_end_fun_call
77with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝
78  | tllp_base_not_return:
79      ∀status: Status.
80        next_instruction status ≠ (RealInstruction … (RET [[relative]])) →
81        ¬ (is_jump_p (next_instruction status)) →
82        lookup_opt … (program_counter … (execute 1 status)) cost_labels = None … →
83          trace_label_label_pre cost_labels doesnt_end_with_ret status status
84  | tllp_base_return:
85      ∀status: Status.
86         next_instruction status = (RealInstruction … (RET [[relative]])) →
87           trace_label_label_pre cost_labels ends_with_ret status status
88  | tllp_base_jump:
89      ∀status: Status.
90      ∀cost_label: Byte.
91        is_jump_p (next_instruction status) →
92        lookup_opt … (program_counter … (execute 1 status)) cost_labels = Some … cost_label →
93          trace_label_label_pre cost_labels doesnt_end_with_ret status status
94  | tllp_step_call:
95      ∀end_flag: trace_ends_with_ret.
96      ∀status_pre_fun_call: Status.
97      ∀status_start_fun_call: Status.
98      ∀status_end_fun_call: Status.
99      ∀status_after_fun_call: Status.
100      ∀status_final: Status.
101      ∀fun_call_trace: trace_label_return cost_labels status_start_fun_call status_end_fun_call.
102        is_call_p (next_instruction status_pre_fun_call) →
103        next_instruction_properly_relates_program_counters status_pre_fun_call status_after_fun_call →
104        execute 1 status_pre_fun_call = status_start_fun_call →
105        execute 1 status_end_fun_call = status_after_fun_call →
106        trace_label_label_pre cost_labels end_flag status_after_fun_call status_final →
107        trace_label_label_pre cost_labels end_flag status_pre_fun_call status_final
108  | tllp_step_default:
109      ∀end_flag: trace_ends_with_ret.
110      ∀status_pre: Status.
111      ∀status_init: Status.
112      ∀status_end: Status.
113        trace_label_label_pre cost_labels end_flag status_init status_end →
114        ¬ (is_call_p (next_instruction status_pre)) →
115        ¬ (is_jump_p (next_instruction status_pre)) →
116        (next_instruction status_pre) ≠ (RealInstruction … (RET [[relative]])) →
117        lookup_opt … (program_counter … status_init) cost_labels = None … →
118          trace_label_label_pre cost_labels end_flag status_pre status_end
119with trace_label_label: trace_ends_with_ret → Status → Status → Type[0] ≝
120  | tll_base:
121      ∀ends_flag: trace_ends_with_ret.
122      ∀start_status: Status.
123      ∀end_status: Status.
124        trace_label_label_pre cost_labels ends_flag start_status end_status →
125        next_instruction_is_labelled start_status →
126        trace_label_label cost_labels ends_flag start_status end_status.
127
128definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
129
130lemma simple_path_ok:
131 ∀st: Status.∀H.
132 let p ≝ compute_simple_path0 st H in
133   ∀n.
134    nth_path n p = execute n st ∧
135     (execute' (path_length p) st = 〈st',τ〉 →
136      τ = cost_trace p)
137  ].
138
139let rec trace_lab_rec_cost (p: trace_lab_ret) : nat. COUNTS EVERYTHING
140
141lemma trace_lab_rec_cost_ok:
142 ∀p: trace_lab_rec.
143  trace_lab_rec_cost p = Timer (last p) - Timer (first p).
144
145let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
146 match p with
147 [ call ⇒ DO NOT ADD ANYTHING
148 | _ ⇒ DO ADD ].
149
150let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
151 | (call b bf tr af tl) as self ⇒
152    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
153    trace_lab_rec_cost' tl
154
155theorem main_lemma:
156 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
157
158axiom lemma1:
159 ∀p: simple_path.
160  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
161
162axiom lemma2:
163 ∀s,l,cost_map.
164  is_labelled l s →
165   traverse_cost_internal s = cost_map l.
166
167axiom main_statement:
168 ∀s.
169 ∀cost_map.
170 let p ≝ compute_simple_path0 s in
171 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
172
173axiom main_statement:
174 ∀s.
175 ∀cost_map.
176 let p ≝ compute_simple_path0 s in
177  execute' (path_length p) s = 〈s',τ〉 →
178   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracBrowser for help on using the repository browser.