1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Arithmetic.ma". |
---|
3 | include "ASM/Fetch.ma". |
---|
4 | include "ASM/Interpret.ma". |
---|
5 | include "common/StructuredTraces.ma". |
---|
6 | |
---|
7 | definition current_instruction0 ≝ |
---|
8 | λmem,pc. \fst (\fst (fetch … mem pc)). |
---|
9 | |
---|
10 | definition current_instruction ≝ |
---|
11 | λs:Status. current_instruction0 (code_memory … s) (program_counter … s). |
---|
12 | |
---|
13 | definition ASM_classify0: instruction → status_class ≝ |
---|
14 | λi. |
---|
15 | match i with |
---|
16 | [ RealInstruction pre ⇒ |
---|
17 | match pre with |
---|
18 | [ RET ⇒ cl_return |
---|
19 | | JZ _ ⇒ cl_jump |
---|
20 | | JNZ _ ⇒ cl_jump |
---|
21 | | JC _ ⇒ cl_jump |
---|
22 | | JNC _ ⇒ cl_jump |
---|
23 | | JB _ _ ⇒ cl_jump |
---|
24 | | JNB _ _ ⇒ cl_jump |
---|
25 | | JBC _ _ ⇒ cl_jump |
---|
26 | | CJNE _ _ ⇒ cl_jump |
---|
27 | | DJNZ _ _ ⇒ cl_jump |
---|
28 | | _ ⇒ cl_other |
---|
29 | ] |
---|
30 | | ACALL _ ⇒ cl_call |
---|
31 | | LCALL _ ⇒ cl_call |
---|
32 | | JMP _ ⇒ cl_call |
---|
33 | | AJMP _ ⇒ cl_jump |
---|
34 | | LJMP _ ⇒ cl_jump |
---|
35 | | SJMP _ ⇒ cl_jump |
---|
36 | | _ ⇒ cl_other |
---|
37 | ]. |
---|
38 | |
---|
39 | definition ASM_classify: Status → status_class ≝ |
---|
40 | λs.ASM_classify0 (current_instruction s). |
---|
41 | |
---|
42 | definition current_instruction_is_labelled ≝ |
---|
43 | λcost_labels: BitVectorTrie costlabel 16. |
---|
44 | λs: Status. |
---|
45 | let pc ≝ program_counter … s in |
---|
46 | match lookup_opt … pc cost_labels with |
---|
47 | [ None ⇒ False |
---|
48 | | _ ⇒ True |
---|
49 | ]. |
---|
50 | |
---|
51 | definition label_of_current_instruction: |
---|
52 | BitVectorTrie costlabel 16 → Status → list costlabel |
---|
53 | ≝ |
---|
54 | λcost_labels,s. |
---|
55 | let pc ≝ program_counter … s in |
---|
56 | match lookup_opt … pc cost_labels with |
---|
57 | [ None ⇒ [] |
---|
58 | | Some l ⇒ [l] |
---|
59 | ]. |
---|
60 | |
---|
61 | definition next_instruction_properly_relates_program_counters ≝ |
---|
62 | λbefore: Status. |
---|
63 | λafter : Status. |
---|
64 | let size ≝ current_instruction_cost before in |
---|
65 | let pc_before ≝ program_counter … before in |
---|
66 | let pc_after ≝ program_counter … after in |
---|
67 | let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in |
---|
68 | sum = pc_after. |
---|
69 | |
---|
70 | definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝ |
---|
71 | λcost_labels. |
---|
72 | mk_abstract_status |
---|
73 | Status |
---|
74 | (λs,s'. eject … (execute_1 s) = s') |
---|
75 | (λs,class. ASM_classify s = class) |
---|
76 | (current_instruction_is_labelled cost_labels) |
---|
77 | next_instruction_properly_relates_program_counters. |
---|
78 | |
---|
79 | (* To be moved in ASM/arithmetic.ma *) |
---|
80 | definition addr16_of_addr11: Word → Word11 → Word ≝ |
---|
81 | λpc: Word. |
---|
82 | λa: Word11. |
---|
83 | let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in |
---|
84 | let 〈n1, n2〉 ≝ split … 4 4 pc_upper in |
---|
85 | let 〈b123, b〉 ≝ split … 3 8 a in |
---|
86 | let b1 ≝ get_index_v … b123 0 ? in |
---|
87 | let b2 ≝ get_index_v … b123 1 ? in |
---|
88 | let b3 ≝ get_index_v … b123 2 ? in |
---|
89 | let p5 ≝ get_index_v … n2 0 ? in |
---|
90 | (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b. |
---|
91 | // |
---|
92 | qed. |
---|
93 | |
---|
94 | axiom size: |
---|
95 | ∀a: Type[0]. |
---|
96 | ∀n: nat. |
---|
97 | BitVectorTrie Byte 16 → nat. |
---|
98 | |
---|
99 | (* XXX: need some precondition about pc not being too "big" to avoid overflow *) |
---|
100 | axiom fetch_pc_lt_new_pc: |
---|
101 | ∀mem: BitVectorTrie Byte 16. |
---|
102 | ∀pc: Word. |
---|
103 | ∀proof: nat_of_bitvector … pc < size Byte 16 mem. |
---|
104 | nat_of_bitvector … pc < nat_of_bitvector … (\snd (\fst (fetch … mem pc))). |
---|
105 | |
---|
106 | axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o: |
---|
107 | ∀m, n, o: nat. |
---|
108 | m - n ≤ m - S o → S m - n ≤ m - o. |
---|
109 | |
---|
110 | axiom strengthened_invariant: |
---|
111 | ∀code_memory: BitVectorTrie Byte 16. |
---|
112 | ∀program_size: nat. |
---|
113 | ∀code_memory_size: nat. |
---|
114 | ∀new_program_counter: Word. |
---|
115 | ∀program_counter: Word. |
---|
116 | code_memory_size ≤ size Byte 16 code_memory → |
---|
117 | program_size < code_memory_size → |
---|
118 | let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … program_size))) in |
---|
119 | Or (ASM_classify0 end_instr = cl_jump) (ASM_classify0 end_instr = cl_return) → |
---|
120 | new_program_counter = \snd (\fst (fetch … code_memory program_counter)) → |
---|
121 | nat_of_bitvector … program_counter < program_size → |
---|
122 | nat_of_bitvector … new_program_counter < program_size. |
---|
123 | |
---|
124 | (* XXX: use memoisation here in the future *) |
---|
125 | let rec block_cost |
---|
126 | (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) |
---|
127 | (program_counter: Word) (program_size: nat) (code_memory_size: nat) |
---|
128 | (size_invariant: code_memory_size ≤ size Byte 16 code_memory) |
---|
129 | (pc_invariant: nat_of_bitvector … program_counter < code_memory_size) |
---|
130 | (final_instr_invariant: |
---|
131 | let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … initial_program_size))) in |
---|
132 | Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return)) |
---|
133 | on program_size: initial_program_size - nat_of_bitvector … program_counter < program_size → nat ≝ |
---|
134 | match program_size return λprogram_size: nat. initial_program_size - nat_of_bitvector … program_counter < program_size → nat with |
---|
135 | [ O ⇒ λabsurd. ⊥ |
---|
136 | | S program_size ⇒ λrecursive_case. |
---|
137 | let ticks ≝ \snd (fetch … code_memory pc) in |
---|
138 | let instr ≝ \fst (\fst (fetch … mem pc)) in |
---|
139 | let newpc ≝ \snd (\fst (fetch … mem pc)) in |
---|
140 | match lookup_opt … newpc cost_labels return λx: option costlabel. nat with |
---|
141 | [ None ⇒ |
---|
142 | let classify ≝ ASM_classify0 instr in |
---|
143 | match classify return λx. ∀classify_refl: x = classify. nat with |
---|
144 | [ cl_jump ⇒ λclassify_refl. ticks |
---|
145 | | cl_call ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?) |
---|
146 | | cl_return ⇒ λclassify_refl. ticks |
---|
147 | | cl_other ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?) |
---|
148 | ] (refl … classify) |
---|
149 | | Some _ ⇒ ticks |
---|
150 | ] |
---|
151 | ]. |
---|
152 | [1: |
---|
153 | cases(lt_to_not_zero … absurd) |
---|
154 | |2,4: |
---|
155 | cut(nat_of_bitvector … pc < nat_of_bitvector … newpc) |
---|
156 | [1,3: |
---|
157 | @fetch_pc_lt_new_pc |
---|
158 | lapply(transitive_lt |
---|
159 | (nat_of_bitvector 16 pc) |
---|
160 | initial_program_size |
---|
161 | (size Byte 16 mem) ? ?) |
---|
162 | [1,2,4,5: |
---|
163 | assumption |
---|
164 | |3,6: |
---|
165 | #assm assumption |
---|
166 | ] |
---|
167 | |2,4: |
---|
168 | change with ( |
---|
169 | S (nat_of_bitvector … 16 pc) ≤ nat_of_bitvector … newpc |
---|
170 | ) in ⊢ (% → ?); |
---|
171 | #first_le_assm |
---|
172 | normalize in recursive_case; |
---|
173 | change with ( |
---|
174 | S (initial_program_size - nat_of_bitvector … newpc) ≤ program_size) |
---|
175 | lapply (le_S_S_to_le … recursive_case) |
---|
176 | change with ( |
---|
177 | initial_program_size - (nat_of_bitvector … pc) ≤ program_size |
---|
178 | ) in ⊢ (% → ?); |
---|
179 | #second_le_assm |
---|
180 | @(transitive_le |
---|
181 | (S (initial_program_size-nat_of_bitvector 16 newpc)) |
---|
182 | (initial_program_size-nat_of_bitvector_aux 16 O pc) |
---|
183 | program_size ? second_le_assm) |
---|
184 | change with ( |
---|
185 | initial_program_size - nat_of_bitvector … pc |
---|
186 | ) in ⊢ (??%); |
---|
187 | lapply (minus_Sn_m (nat_of_bitvector … newpc) initial_program_size) |
---|
188 | #assm <assm in ⊢ (?%?); |
---|
189 | [1,3: |
---|
190 | @minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o |
---|
191 | @monotonic_le_minus_r |
---|
192 | assumption |
---|
193 | |2,4: |
---|
194 | @(strengthened_invariant mem initial_program_size newpc pc size_invariant final_instr_invariant) |
---|
195 | [1,3: |
---|
196 | % |
---|
197 | |2,4: |
---|
198 | assumption |
---|
199 | ] |
---|
200 | ] |
---|
201 | ] |
---|
202 | |3,5: |
---|
203 | ] |
---|
204 | qed. |
---|
205 | |
---|
206 | let rec traverse_code_internal |
---|
207 | (program: list Byte) (mem: BitVectorTrie Byte 16) |
---|
208 | (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat) |
---|
209 | on program: identifier_map CostTag nat ≝ |
---|
210 | let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in |
---|
211 | match program with |
---|
212 | [ nil ⇒ empty_map … |
---|
213 | | cons hd tl ⇒ |
---|
214 | match lookup_opt … pc cost_labels with |
---|
215 | [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size |
---|
216 | | Some lbl ⇒ |
---|
217 | let cost ≝ block_cost mem cost_labels pc program_size in |
---|
218 | let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in |
---|
219 | add … cost_mapping lbl cost ]]. |
---|
220 | |
---|
221 | definition traverse_code ≝ |
---|
222 | λprogram: list Byte. |
---|
223 | λmem: BitVectorTrie Byte 16. |
---|
224 | λcost_labels. |
---|
225 | λprogram_size: nat. |
---|
226 | traverse_code_internal program mem cost_labels (zero …) program_size. |
---|
227 | |
---|
228 | definition compute_costs ≝ |
---|
229 | λprogram: list Byte. |
---|
230 | λcost_labels: BitVectorTrie costlabel 16. |
---|
231 | λhas_main: bool. |
---|
232 | let program_size ≝ |program| + 1 in |
---|
233 | let memory ≝ load_code_memory program in |
---|
234 | traverse_code program memory cost_labels program_size. |
---|