1 | include "ASM/ASMCosts.ma". |
---|
2 | include "ASM/WellLabeled.ma". |
---|
3 | include "ASM/Status.ma". |
---|
4 | |
---|
5 | definition 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 | |
---|
28 | definition is_call_p ≝ |
---|
29 | λs. |
---|
30 | match s with |
---|
31 | [ ACALL _ ⇒ True |
---|
32 | | LCALL _ ⇒ True |
---|
33 | | _ ⇒ False |
---|
34 | ]. |
---|
35 | |
---|
36 | definition size_of_next_instruction ≝ |
---|
37 | λs: Status. |
---|
38 | let 〈ignore, ignore, cost〉 ≝ fetch (code_memory … s) (program_counter … s) in |
---|
39 | cost. |
---|
40 | |
---|
41 | definition 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 | |
---|
50 | definition next_instruction ≝ |
---|
51 | λs: Status. |
---|
52 | let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in |
---|
53 | instruction. |
---|
54 | |
---|
55 | inductive trace_ends_with_ret: Type[0] ≝ |
---|
56 | | ends_with_ret: trace_ends_with_ret |
---|
57 | | doesnt_end_with_ret: trace_ends_with_ret. |
---|
58 | |
---|
59 | axiom next_instruction_is_labelled: |
---|
60 | ∀s: Status. Prop. |
---|
61 | |
---|
62 | inductive 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 |
---|
77 | with 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 |
---|
119 | with 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 | |
---|
128 | definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ …. |
---|
129 | |
---|
130 | lemma 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 | |
---|
139 | let rec trace_lab_rec_cost (p: trace_lab_ret) : nat. COUNTS EVERYTHING |
---|
140 | |
---|
141 | lemma trace_lab_rec_cost_ok: |
---|
142 | ∀p: trace_lab_rec. |
---|
143 | trace_lab_rec_cost p = Timer (last p) - Timer (first p). |
---|
144 | |
---|
145 | let 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 | |
---|
150 | let 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 | |
---|
155 | theorem main_lemma: |
---|
156 | ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p. |
---|
157 | |
---|
158 | axiom lemma1: |
---|
159 | ∀p: simple_path. |
---|
160 | traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p. |
---|
161 | |
---|
162 | axiom lemma2: |
---|
163 | ∀s,l,cost_map. |
---|
164 | is_labelled l s → |
---|
165 | traverse_cost_internal s = cost_map l. |
---|
166 | |
---|
167 | axiom 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 | |
---|
173 | axiom 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. |
---|