1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Arithmetic.ma". |
---|
3 | include "ASM/Fetch.ma". |
---|
4 | include "ASM/Interpret.ma". |
---|
5 | |
---|
6 | inductive instruction_nature: Type[0] ≝ |
---|
7 | | goto: Word → instruction_nature |
---|
8 | | branch: Word → instruction_nature |
---|
9 | | direct_fun_call: Word → instruction_nature |
---|
10 | | ret: instruction_nature |
---|
11 | | other: instruction_nature. |
---|
12 | |
---|
13 | definition addr16_of_addr11: Word → Word11 → Word ≝ |
---|
14 | λpc: Word. |
---|
15 | λa: Word11. |
---|
16 | let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in |
---|
17 | let 〈n1, n2〉 ≝ split … 4 4 pc_upper in |
---|
18 | let 〈b123, b〉 ≝ split … 3 8 a in |
---|
19 | let b1 ≝ get_index_v … b123 0 ? in |
---|
20 | let b2 ≝ get_index_v … b123 1 ? in |
---|
21 | let b3 ≝ get_index_v … b123 2 ? in |
---|
22 | let p5 ≝ get_index_v … n2 0 ? in |
---|
23 | (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b. |
---|
24 | // |
---|
25 | qed. |
---|
26 | |
---|
27 | definition instruction_nature_next_pc_length ≝ |
---|
28 | λvariety: instruction_nature. |
---|
29 | match variety with |
---|
30 | [ ret ⇒ 0 |
---|
31 | | branch _ ⇒ 2 |
---|
32 | | goto _ ⇒ 1 |
---|
33 | | direct_fun_call _ ⇒ 1 |
---|
34 | | other ⇒ 1 |
---|
35 | ]. |
---|
36 | |
---|
37 | definition instruction_info: |
---|
38 | BitVectorTrie Byte 16 → Word → Σprod: (instruction_nature × Word × (list Word) × nat). |\snd (\fst prod)| = instruction_nature_next_pc_length (\fst (\fst (\fst prod))) ≝ |
---|
39 | λmem. |
---|
40 | λpc. |
---|
41 | let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in |
---|
42 | let nature_next_pcs_proof ≝ |
---|
43 | match inst return λx. Σpair: (instruction_nature × (list Word)). |(\snd pair)| = instruction_nature_next_pc_length (\fst pair) with |
---|
44 | [ RealInstruction ri ⇒ |
---|
45 | match ri with |
---|
46 | [ RET ⇒ dp … 〈ret, [ ]〉 ? |
---|
47 | | RETI ⇒ dp … 〈ret, [ ]〉 ? |
---|
48 | | JC addr ⇒ |
---|
49 | match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
50 | [ RELATIVE addr ⇒ λ_. |
---|
51 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
52 | dp … 〈branch addr, [ next_pc; addr ]〉 ? |
---|
53 | | _ ⇒ λp. match p in False with [ ] |
---|
54 | ] (subaddressing_modein … addr) |
---|
55 | | JNC addr ⇒ |
---|
56 | match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
57 | [ RELATIVE addr ⇒ λ_. |
---|
58 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
59 | dp … 〈branch addr, [ next_pc; addr ]〉 ? |
---|
60 | | _ ⇒ λp. match p in False with [ ] |
---|
61 | ] (subaddressing_modein … addr) |
---|
62 | | JZ addr ⇒ |
---|
63 | match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
64 | [ RELATIVE addr ⇒ λ_. |
---|
65 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
66 | dp … 〈branch addr, [ next_pc; addr ]〉 ? |
---|
67 | | _ ⇒ λp. match p in False with [ ] |
---|
68 | ] (subaddressing_modein … addr) |
---|
69 | | JNZ addr ⇒ |
---|
70 | match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
71 | [ RELATIVE addr ⇒ λ_. |
---|
72 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
73 | dp … 〈branch addr, [ next_pc; addr ]〉 ? |
---|
74 | | _ ⇒ λp. match p in False with [ ] |
---|
75 | ] (subaddressing_modein … addr) |
---|
76 | | JB addr1 addr2 ⇒ |
---|
77 | match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
78 | [ RELATIVE addr ⇒ λ_. |
---|
79 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
80 | dp … 〈branch addr, [ next_pc; addr ]〉 ? |
---|
81 | | _ ⇒ λp. match p in False with [ ] |
---|
82 | ] (subaddressing_modein … addr2) |
---|
83 | | JNB addr1 addr2 ⇒ |
---|
84 | match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
85 | [ RELATIVE addr ⇒ λ_. |
---|
86 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
87 | dp … 〈branch addr, [ next_pc; addr ]〉 ? |
---|
88 | | _ ⇒ λp. match p in False with [ ] |
---|
89 | ] (subaddressing_modein … addr2) |
---|
90 | | JBC addr1 addr2 ⇒ |
---|
91 | match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
92 | [ RELATIVE addr ⇒ λ_. |
---|
93 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
94 | dp … 〈branch addr, [ next_pc; addr ]〉 ? |
---|
95 | | _ ⇒ λp. match p in False with [ ] |
---|
96 | ] (subaddressing_modein … addr2) |
---|
97 | | DJNZ addr1 addr2 ⇒ |
---|
98 | match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
99 | [ RELATIVE addr ⇒ λ_. |
---|
100 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
101 | dp … 〈branch addr, [ next_pc; addr ]〉 ? |
---|
102 | | _ ⇒ λp. match p in False with [ ] |
---|
103 | ] (subaddressing_modein … addr2) |
---|
104 | | CJNE addr1 addr2 ⇒ |
---|
105 | match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
106 | [ RELATIVE addr ⇒ λ_. |
---|
107 | let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in |
---|
108 | dp … 〈branch addr, [ next_pc; addr ]〉 ? |
---|
109 | | _ ⇒ λp. match p in False with [ ] |
---|
110 | ] (subaddressing_modein … addr2) |
---|
111 | | _ ⇒ dp … 〈other, [ next_pc ]〉 ? |
---|
112 | ] |
---|
113 | | ACALL addr ⇒ |
---|
114 | match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with |
---|
115 | [ ADDR11 addr ⇒ λ_. |
---|
116 | let addr ≝ addr16_of_addr11 pc addr in |
---|
117 | dp … 〈direct_fun_call addr, [ next_pc ]〉 ? |
---|
118 | | _ ⇒ λp. match p in False with [ ] |
---|
119 | ] (subaddressing_modein … addr) |
---|
120 | | LCALL addr ⇒ |
---|
121 | match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with |
---|
122 | [ ADDR16 addr ⇒ λ_. dp … 〈direct_fun_call addr, [ next_pc ]〉 ? |
---|
123 | | _ ⇒ λp. match p in False with [ ] |
---|
124 | ] (subaddressing_modein … addr) |
---|
125 | | AJMP addr ⇒ |
---|
126 | match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with |
---|
127 | [ ADDR11 addr ⇒ λ_. |
---|
128 | let addr ≝ addr16_of_addr11 pc addr in |
---|
129 | dp … 〈goto addr, [ addr ]〉 ? |
---|
130 | | _ ⇒ λp. match p in False with [ ] |
---|
131 | ] (subaddressing_modein … addr) |
---|
132 | | LJMP addr ⇒ |
---|
133 | match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with |
---|
134 | [ ADDR16 addr ⇒ λ_. dp … 〈goto addr, [ addr ]〉 ? |
---|
135 | | _ ⇒ λp. match p in False with [ ] |
---|
136 | ] (subaddressing_modein … addr) |
---|
137 | | SJMP addr ⇒ |
---|
138 | match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with |
---|
139 | [ RELATIVE addr ⇒ λ_. |
---|
140 | let 〈carry, addr〉 ≝ half_add 16 next_pc (sign_extend 8 8 addr) in |
---|
141 | dp … 〈goto addr, [ addr ]〉 ? |
---|
142 | | _ ⇒ λp. match p in False with [ ] |
---|
143 | ] (subaddressing_modein … addr) |
---|
144 | | JMP addr ⇒ dp … 〈other, [ next_pc ]〉 ? |
---|
145 | | MOVC acc_a addr ⇒ dp … 〈other, [ next_pc ]〉 ? |
---|
146 | ] |
---|
147 | in |
---|
148 | match nature_next_pcs_proof with |
---|
149 | [ dp nature_next_pcs their_proof ⇒ |
---|
150 | let nature ≝ \fst nature_next_pcs in |
---|
151 | let next_pcs ≝ \snd nature_next_pcs in |
---|
152 | dp … 〈〈〈nature, next_pc〉, next_pcs〉, inst_cost〉 ? |
---|
153 | ]. |
---|
154 | [1: >their_proof % |
---|
155 | |*: % |
---|
156 | ] |
---|
157 | qed. |
---|
158 | |
---|
159 | let rec compare |
---|
160 | (a: Type[0]) (the_list: list (a × nat)) |
---|
161 | on the_list: nat ≝ |
---|
162 | match the_list with |
---|
163 | [ nil ⇒ ⊥ (* XXX: was assert false *) |
---|
164 | | cons hd tl ⇒ |
---|
165 | match tl with |
---|
166 | [ nil ⇒ |
---|
167 | let 〈pc, cost〉 ≝ hd in |
---|
168 | cost |
---|
169 | | cons hd' tl' ⇒ |
---|
170 | let 〈pc1, cost1〉 ≝ hd in |
---|
171 | let 〈pc2, cost2〉 ≝ hd' in |
---|
172 | match eq_nat cost1 cost2 with |
---|
173 | [ true ⇒ max cost1 (compare … tl) |
---|
174 | | false ⇒ compare … tl' |
---|
175 | ] |
---|
176 | ] |
---|
177 | ]. |
---|
178 | cases daemon |
---|
179 | qed. |
---|
180 | |
---|
181 | let rec block_cost' |
---|
182 | (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16) |
---|
183 | (program_counter: Word) (program_size: nat) (cost_so_far: nat) |
---|
184 | on program_size ≝ |
---|
185 | match program_size with |
---|
186 | [ O ⇒ 0 |
---|
187 | | S program_size ⇒ |
---|
188 | let sigma ≝ instruction_info mem program_counter in |
---|
189 | match sigma with |
---|
190 | [ dp variety_costs their_proof ⇒ |
---|
191 | let variety ≝ \fst (\fst (\fst variety_costs)) in |
---|
192 | let next_pc ≝ \snd (\fst (\fst variety_costs)) in |
---|
193 | let next_pcs ≝ \snd (\fst variety_costs) in |
---|
194 | let inst_cost ≝ \snd variety_costs in |
---|
195 | match variety return λx. |next_pcs| = instruction_nature_next_pc_length x → nat with |
---|
196 | [ other ⇒ λproof. |
---|
197 | match next_pcs return λx. |x| = 1 → nat with |
---|
198 | [ nil ⇒ λabsurd. ⊥ |
---|
199 | | cons hd tl ⇒ λproof. |
---|
200 | match lookup_opt … hd cost_labels with |
---|
201 | [ None ⇒ block_cost' mem cost_labels hd program_size (cost_so_far + inst_cost) |
---|
202 | | Some _ ⇒ inst_cost + cost_so_far |
---|
203 | ] |
---|
204 | ] proof |
---|
205 | | _ ⇒ λ_. inst_cost + cost_so_far |
---|
206 | ] their_proof |
---|
207 | ] |
---|
208 | ]. |
---|
209 | normalize in absurd |
---|
210 | destruct(absurd) |
---|
211 | qed. |
---|
212 | |
---|
213 | definition block_cost ≝ |
---|
214 | λmem: BitVectorTrie Byte 16. |
---|
215 | λcost_labels: BitVectorTrie Byte 16. |
---|
216 | λprogram_counter: Word. |
---|
217 | λprogram_size: nat. |
---|
218 | block_cost' mem cost_labels program_counter program_size 0. |
---|
219 | |
---|
220 | let rec traverse_code_internal |
---|
221 | (program: list Byte) (mem: BitVectorTrie Byte 16) |
---|
222 | (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat) |
---|
223 | on program: BitVectorTrie nat 8 ≝ |
---|
224 | match instruction_info mem pc with |
---|
225 | [ dp info proof ⇒ |
---|
226 | let newpc ≝ \snd (\fst (\fst info)) in |
---|
227 | match program with |
---|
228 | [ nil ⇒ Stub … |
---|
229 | | cons hd tl ⇒ |
---|
230 | match lookup_opt … pc cost_labels with |
---|
231 | [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size |
---|
232 | | Some lbl ⇒ |
---|
233 | let cost ≝ block_cost mem cost_labels pc program_size in |
---|
234 | let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in |
---|
235 | insert … lbl cost cost_mapping |
---|
236 | ] |
---|
237 | ] |
---|
238 | ]. |
---|
239 | |
---|
240 | definition traverse_code ≝ |
---|
241 | λprogram: list Byte. |
---|
242 | λmem: BitVectorTrie Byte 16. |
---|
243 | λcost_labels. |
---|
244 | λprogram_size: nat. |
---|
245 | traverse_code_internal program mem cost_labels (zero …) program_size. |
---|
246 | |
---|
247 | let rec first_cost_label_internal |
---|
248 | (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16) |
---|
249 | (program_size: nat) (oldpc: Word) |
---|
250 | on program_size: (Byte × nat) ≝ |
---|
251 | match program_size with |
---|
252 | [ O ⇒ ⊥ (* XXX: ummm ... ? *) |
---|
253 | | S program_size ⇒ |
---|
254 | match lookup_opt … oldpc cost_labels with |
---|
255 | [ None ⇒ |
---|
256 | match instruction_info mem oldpc with |
---|
257 | [ dp info proof ⇒ |
---|
258 | let nature ≝ \fst (\fst (\fst info)) in |
---|
259 | let pc ≝ \snd (\fst (\fst info)) in |
---|
260 | let inst_cost ≝ \snd info in |
---|
261 | match nature with |
---|
262 | [ direct_fun_call addr ⇒ |
---|
263 | let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size addr in |
---|
264 | 〈lbl, inst_cost + cost〉 |
---|
265 | | other ⇒ |
---|
266 | let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size pc in |
---|
267 | 〈lbl, inst_cost + cost〉 |
---|
268 | | _ ⇒ ⊥ (* XXX: was assert false in o'caml *) |
---|
269 | ] |
---|
270 | ] |
---|
271 | | Some cost ⇒ 〈cost, 0〉 |
---|
272 | ] |
---|
273 | ]. |
---|
274 | cases daemon |
---|
275 | qed. |
---|
276 | |
---|
277 | definition first_cost_label ≝ |
---|
278 | λmem: BitVectorTrie Byte 16. |
---|
279 | λcost_labels: BitVectorTrie Byte 16. |
---|
280 | λprogram_size: nat. |
---|
281 | first_cost_label_internal mem cost_labels program_size (zero …). |
---|
282 | |
---|
283 | definition initialize_costs ≝ |
---|
284 | λmem: BitVectorTrie Byte 16. |
---|
285 | λcost_labels: BitVectorTrie Byte 16. |
---|
286 | λcost_mapping: BitVectorTrie nat 8. |
---|
287 | λprogram_size: nat. |
---|
288 | let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in |
---|
289 | let old_cost ≝ |
---|
290 | match lookup_opt … lbl cost_mapping with |
---|
291 | [ None ⇒ 0 |
---|
292 | | Some cost ⇒ cost |
---|
293 | ] |
---|
294 | in |
---|
295 | let new_cost ≝ old_cost + cost in |
---|
296 | insert … lbl new_cost cost_mapping. |
---|
297 | |
---|
298 | definition compute_costs ≝ |
---|
299 | λprogram: list Byte. |
---|
300 | λcost_labels: BitVectorTrie Byte 16. |
---|
301 | λhas_main: bool. |
---|
302 | let program_size ≝ |program| in |
---|
303 | let memory ≝ load_code_memory program in |
---|
304 | let costs_mapping ≝ traverse_code program memory cost_labels program_size in |
---|
305 | match has_main with |
---|
306 | [ true ⇒ |
---|
307 | initialize_costs memory cost_labels costs_mapping program_size |
---|
308 | | false ⇒ costs_mapping |
---|
309 | ]. |
---|