1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Arithmetic.ma". |
---|
3 | include "ASM/Fetch.ma". |
---|
4 | include "ASM/Status.ma". |
---|
5 | include "utilities/extralib.ma". |
---|
6 | include "ASM/Assembly.ma". |
---|
7 | |
---|
8 | (* Internal types *) |
---|
9 | |
---|
10 | (* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *) |
---|
11 | definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × jump_length) 16). |
---|
12 | |
---|
13 | (* The different properties that we want/need to prove at some point *) |
---|
14 | (* During our iteration, everything not yet seen is None, and vice versa *) |
---|
15 | definition out_of_program_none ≝ |
---|
16 | λprefix:list labelled_instruction.λsigma:ppc_pc_map. |
---|
17 | ∀i.i < 2^16 → (i > |prefix| ↔ bvt_lookup_opt … (bitvector_of_nat ? i) (\snd sigma) = None ?). |
---|
18 | |
---|
19 | (* If instruction i is a jump, then there will be something in the policy at |
---|
20 | * position i *) |
---|
21 | definition is_jump' ≝ |
---|
22 | λx:preinstruction Identifier. |
---|
23 | match x with |
---|
24 | [ JC _ ⇒ True |
---|
25 | | JNC _ ⇒ True |
---|
26 | | JZ _ ⇒ True |
---|
27 | | JNZ _ ⇒ True |
---|
28 | | JB _ _ ⇒ True |
---|
29 | | JNB _ _ ⇒ True |
---|
30 | | JBC _ _ ⇒ True |
---|
31 | | CJNE _ _ ⇒ True |
---|
32 | | DJNZ _ _ ⇒ True |
---|
33 | | _ ⇒ False |
---|
34 | ]. |
---|
35 | |
---|
36 | definition is_relative_jump ≝ |
---|
37 | λinstr:pseudo_instruction. |
---|
38 | match instr with |
---|
39 | [ Instruction i ⇒ is_jump' i |
---|
40 | | _ ⇒ False |
---|
41 | ]. |
---|
42 | |
---|
43 | definition is_jump ≝ |
---|
44 | λinstr:pseudo_instruction. |
---|
45 | match instr with |
---|
46 | [ Instruction i ⇒ is_jump' i |
---|
47 | | Call _ ⇒ True |
---|
48 | | Jmp _ ⇒ True |
---|
49 | | _ ⇒ False |
---|
50 | ]. |
---|
51 | |
---|
52 | definition is_call ≝ |
---|
53 | λinstr:pseudo_instruction. |
---|
54 | match instr with |
---|
55 | [ Call _ ⇒ True |
---|
56 | | _ ⇒ False |
---|
57 | ]. |
---|
58 | |
---|
59 | definition is_jump_to ≝ |
---|
60 | λx:pseudo_instruction.λd:Identifier. |
---|
61 | match x with |
---|
62 | [ Instruction i ⇒ match i with |
---|
63 | [ JC j ⇒ d = j |
---|
64 | | JNC j ⇒ d = j |
---|
65 | | JZ j ⇒ d = j |
---|
66 | | JNZ j ⇒ d = j |
---|
67 | | JB _ j ⇒ d = j |
---|
68 | | JNB _ j ⇒ d = j |
---|
69 | | JBC _ j ⇒ d = j |
---|
70 | | CJNE _ j ⇒ d = j |
---|
71 | | DJNZ _ j ⇒ d = j |
---|
72 | | _ ⇒ False |
---|
73 | ] |
---|
74 | | Call c ⇒ d = c |
---|
75 | | Jmp j ⇒ d = j |
---|
76 | | _ ⇒ False |
---|
77 | ]. |
---|
78 | |
---|
79 | definition not_jump_default ≝ |
---|
80 | λprefix:list labelled_instruction.λsigma:ppc_pc_map. |
---|
81 | ∀i:ℕ.i < |prefix| → |
---|
82 | ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) → |
---|
83 | \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump. |
---|
84 | |
---|
85 | (* Between two policies, jumps cannot decrease *) |
---|
86 | definition jmpeqb: jump_length → jump_length → bool ≝ |
---|
87 | λj1.λj2. |
---|
88 | match j1 with |
---|
89 | [ short_jump ⇒ match j2 with [ short_jump ⇒ true | _ ⇒ false ] |
---|
90 | | absolute_jump ⇒ match j2 with [ absolute_jump ⇒ true | _ ⇒ false ] |
---|
91 | | long_jump ⇒ match j2 with [ long_jump ⇒ true | _ ⇒ false ] |
---|
92 | ]. |
---|
93 | |
---|
94 | lemma jmpeqb_to_eq: ∀j1,j2.jmpeqb j1 j2 → j1 = j2. |
---|
95 | #j1 #j2 cases j1 cases j2 |
---|
96 | [1,5,9: / by /] |
---|
97 | #H cases H |
---|
98 | qed. |
---|
99 | |
---|
100 | definition jmple: jump_length → jump_length → Prop ≝ |
---|
101 | λj1.λj2. |
---|
102 | match j1 with |
---|
103 | [ short_jump ⇒ |
---|
104 | match j2 with |
---|
105 | [ short_jump ⇒ False |
---|
106 | | _ ⇒ True |
---|
107 | ] |
---|
108 | | absolute_jump ⇒ |
---|
109 | match j2 with |
---|
110 | [ long_jump ⇒ True |
---|
111 | | _ ⇒ False |
---|
112 | ] |
---|
113 | | long_jump ⇒ False |
---|
114 | ]. |
---|
115 | |
---|
116 | definition jmpleq: jump_length → jump_length → Prop ≝ |
---|
117 | λj1.λj2.jmple j1 j2 ∨ j1 = j2. |
---|
118 | |
---|
119 | definition jump_increase ≝ |
---|
120 | λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map. |
---|
121 | ∀i.i ≤ |prefix| → |
---|
122 | let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd op) 〈0,short_jump〉 in |
---|
123 | let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd p) 〈0,short_jump〉 in |
---|
124 | (*opc ≤ pc ∧*) jmpleq oj j. |
---|
125 | |
---|
126 | (* this is the instruction size as determined by the jump length given *) |
---|
127 | definition expand_relative_jump_internal_unsafe: |
---|
128 | jump_length → ([[relative]] → preinstruction [[relative]]) → list instruction ≝ |
---|
129 | λjmp_len:jump_length.λi. |
---|
130 | match jmp_len with |
---|
131 | [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ] |
---|
132 | | absolute_jump ⇒ [ ] (* this should not happen *) |
---|
133 | | long_jump ⇒ |
---|
134 | [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); |
---|
135 | SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *) |
---|
136 | LJMP (ADDR16 (zero 16)) |
---|
137 | ] |
---|
138 | ]. |
---|
139 | @I |
---|
140 | qed. |
---|
141 | |
---|
142 | definition expand_relative_jump_unsafe: |
---|
143 | jump_length → preinstruction Identifier → list instruction ≝ |
---|
144 | λjmp_len:jump_length.λi. |
---|
145 | match i with |
---|
146 | [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?) |
---|
147 | | JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?) |
---|
148 | | JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr) |
---|
149 | | JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?) |
---|
150 | | JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?) |
---|
151 | | JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr) |
---|
152 | | JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr) |
---|
153 | | CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr) |
---|
154 | | DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr) |
---|
155 | | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ] |
---|
156 | | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ] |
---|
157 | | SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ] |
---|
158 | | INC arg ⇒ [ INC ? arg ] |
---|
159 | | DEC arg ⇒ [ DEC ? arg ] |
---|
160 | | MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ] |
---|
161 | | DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ] |
---|
162 | | DA arg ⇒ [ DA ? arg ] |
---|
163 | | ANL arg ⇒ [ ANL ? arg ] |
---|
164 | | ORL arg ⇒ [ ORL ? arg ] |
---|
165 | | XRL arg ⇒ [ XRL ? arg ] |
---|
166 | | CLR arg ⇒ [ CLR ? arg ] |
---|
167 | | CPL arg ⇒ [ CPL ? arg ] |
---|
168 | | RL arg ⇒ [ RL ? arg ] |
---|
169 | | RR arg ⇒ [ RR ? arg ] |
---|
170 | | RLC arg ⇒ [ RLC ? arg ] |
---|
171 | | RRC arg ⇒ [ RRC ? arg ] |
---|
172 | | SWAP arg ⇒ [ SWAP ? arg ] |
---|
173 | | MOV arg ⇒ [ MOV ? arg ] |
---|
174 | | MOVX arg ⇒ [ MOVX ? arg ] |
---|
175 | | SETB arg ⇒ [ SETB ? arg ] |
---|
176 | | PUSH arg ⇒ [ PUSH ? arg ] |
---|
177 | | POP arg ⇒ [ POP ? arg ] |
---|
178 | | XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ] |
---|
179 | | XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ] |
---|
180 | | RET ⇒ [ RET ? ] |
---|
181 | | RETI ⇒ [ RETI ? ] |
---|
182 | | NOP ⇒ [ RealInstruction (NOP ?) ] |
---|
183 | ]. |
---|
184 | |
---|
185 | definition instruction_size_jmplen: |
---|
186 | jump_length → pseudo_instruction → ℕ ≝ |
---|
187 | λjmp_len. |
---|
188 | λi. |
---|
189 | let pseudos ≝ match i with |
---|
190 | [ Cost cost ⇒ [ ] |
---|
191 | | Comment comment ⇒ [ ] |
---|
192 | | Call call ⇒ |
---|
193 | match jmp_len with |
---|
194 | [ short_jump ⇒ [ ] (* this should not happen *) |
---|
195 | | absolute_jump ⇒ [ ACALL (ADDR11 (zero 11)) ] |
---|
196 | | long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ] |
---|
197 | ] |
---|
198 | | Mov d trgt ⇒ |
---|
199 | [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))] |
---|
200 | | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr |
---|
201 | | Jmp jmp ⇒ |
---|
202 | match jmp_len with |
---|
203 | [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ] |
---|
204 | | absolute_jump ⇒ [ AJMP (ADDR11 (zero 11)) ] |
---|
205 | | long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ] |
---|
206 | ] |
---|
207 | ] in |
---|
208 | let mapped ≝ map ? ? assembly1 pseudos in |
---|
209 | let flattened ≝ flatten ? mapped in |
---|
210 | let pc_len ≝ length ? flattened in |
---|
211 | pc_len. |
---|
212 | @I. |
---|
213 | qed. |
---|
214 | |
---|
215 | definition sigma_compact_unsafe ≝ |
---|
216 | λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. |
---|
217 | ∀n.n < |prefix| → |
---|
218 | match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with |
---|
219 | [ None ⇒ False |
---|
220 | | Some x ⇒ let 〈pc,j〉 ≝ x in |
---|
221 | match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with |
---|
222 | [ None ⇒ False |
---|
223 | | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in |
---|
224 | pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment []〉)) |
---|
225 | ] |
---|
226 | ]. |
---|
227 | |
---|
228 | (* new safety condition: sigma corresponds to program and resulting program is compact *) |
---|
229 | definition sigma_compact ≝ |
---|
230 | λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. |
---|
231 | ∀n.n < |program| → |
---|
232 | match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with |
---|
233 | [ None ⇒ False |
---|
234 | | Some x ⇒ let 〈pc,j〉 ≝ x in |
---|
235 | match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with |
---|
236 | [ None ⇒ False |
---|
237 | | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in |
---|
238 | pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) |
---|
239 | (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) |
---|
240 | (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) |
---|
241 | (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment []〉)) |
---|
242 | ] |
---|
243 | ]. |
---|
244 | |
---|
245 | (* jumps are of the proper size *) |
---|
246 | definition sigma_safe ≝ |
---|
247 | λprefix:list labelled_instruction.λlabels:label_map.λadded:ℕ. |
---|
248 | λold_sigma:ppc_pc_map.λsigma:ppc_pc_map. |
---|
249 | ∀i.i < |prefix| → |
---|
250 | let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in |
---|
251 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in |
---|
252 | let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in |
---|
253 | ∀dest.is_jump_to instr dest → |
---|
254 | let paddr ≝ lookup_def … labels dest 0 in |
---|
255 | let addr ≝ bitvector_of_nat ? (if leb paddr (|prefix|) (* jump to address already known *) |
---|
256 | then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉) |
---|
257 | else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in |
---|
258 | match j with |
---|
259 | [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧ |
---|
260 | ¬is_call instr |
---|
261 | | absolute_jump ⇒ \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧ |
---|
262 | \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ |
---|
263 | ¬is_relative_jump instr |
---|
264 | | long_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ |
---|
265 | \fst (absolute_jump_cond pc_plus_jmp_length addr) = false |
---|
266 | ]. |
---|
267 | |
---|
268 | (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) |
---|
269 | definition max_length: jump_length → jump_length → jump_length ≝ |
---|
270 | λj1.λj2. |
---|
271 | match j1 with |
---|
272 | [ long_jump ⇒ long_jump |
---|
273 | | absolute_jump ⇒ |
---|
274 | match j2 with |
---|
275 | [ absolute_jump ⇒ absolute_jump |
---|
276 | | _ ⇒ long_jump |
---|
277 | ] |
---|
278 | | short_jump ⇒ |
---|
279 | match j2 with |
---|
280 | [ short_jump ⇒ short_jump |
---|
281 | | _ ⇒ long_jump |
---|
282 | ] |
---|
283 | ]. |
---|
284 | |
---|
285 | lemma dec_jmple: ∀x,y:jump_length.Sum (jmple x y) (¬(jmple x y)). |
---|
286 | #x #y cases x cases y /3 by inl, inr, nmk, I/ |
---|
287 | qed. |
---|
288 | |
---|
289 | lemma jmpleq_max_length: ∀ol,nl. |
---|
290 | jmpleq ol (max_length ol nl). |
---|
291 | #ol #nl cases ol cases nl |
---|
292 | /2 by or_introl, or_intror, I/ |
---|
293 | qed. |
---|
294 | |
---|
295 | lemma dec_eq_jump_length: ∀a,b:jump_length.Sum (a = b) (a ≠ b). |
---|
296 | #a #b cases a cases b /2/ |
---|
297 | %2 @nmk #H destruct (H) |
---|
298 | qed. |
---|
299 | |
---|
300 | (* The function that creates the label-to-address map *) |
---|
301 | definition create_label_map: ∀program:list labelled_instruction. |
---|
302 | (Σlabels:label_map. |
---|
303 | ∀l.occurs_exactly_once ?? l program → |
---|
304 | bitvector_of_nat ? (lookup_def ?? labels l 0) = |
---|
305 | address_of_word_labels_code_mem program l |
---|
306 | ) ≝ |
---|
307 | λprogram. |
---|
308 | \fst (create_label_cost_map program). |
---|
309 | #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim |
---|
310 | #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map; |
---|
311 | normalize nodelta >EQ @(H l Hl) |
---|
312 | qed. |
---|
313 | |
---|
314 | (* General note on jump length selection: the jump displacement is added/replaced |
---|
315 | * AFTER the fetch (and attendant PC increase), but we calculate before the |
---|
316 | * fetch, which means that in the case of a short and medium jump we are 2 |
---|
317 | * bytes off and have to compensate. |
---|
318 | * For the long jump we don't care, because the PC gets replaced integrally anyway. *) |
---|
319 | definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
320 | Identifier → jump_length ≝ |
---|
321 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
322 | let pc ≝ \fst inc_sigma in |
---|
323 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in |
---|
324 | let paddr ≝ lookup_def … labels lbl 0 in |
---|
325 | let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *) |
---|
326 | then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) |
---|
327 | else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in |
---|
328 | let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in |
---|
329 | if sj_possible |
---|
330 | then short_jump |
---|
331 | else long_jump. |
---|
332 | |
---|
333 | definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
334 | Identifier → jump_length ≝ |
---|
335 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
336 | let pc ≝ \fst inc_sigma in |
---|
337 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in |
---|
338 | let paddr ≝ lookup_def ? ? labels lbl 0 in |
---|
339 | let addr ≝ bitvector_of_nat ? |
---|
340 | (if leb paddr ppc (* jump to address already known *) |
---|
341 | then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) |
---|
342 | else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in |
---|
343 | let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in |
---|
344 | if aj_possible |
---|
345 | then absolute_jump |
---|
346 | else long_jump. |
---|
347 | |
---|
348 | definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
349 | Identifier → jump_length ≝ |
---|
350 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
351 | let pc ≝ \fst inc_sigma in |
---|
352 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in |
---|
353 | let paddr ≝ lookup_def … labels lbl 0 in |
---|
354 | let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *) |
---|
355 | then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) |
---|
356 | else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in |
---|
357 | let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in |
---|
358 | if sj_possible |
---|
359 | then short_jump |
---|
360 | else select_call_length labels old_sigma inc_sigma added ppc lbl. |
---|
361 | |
---|
362 | definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map → |
---|
363 | ℕ → ℕ → preinstruction Identifier → option jump_length ≝ |
---|
364 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi. |
---|
365 | match i with |
---|
366 | [ JC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
367 | | JNC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
368 | | JZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
369 | | JNZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
370 | | JB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
371 | | JBC _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
372 | | JNB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
373 | | CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
374 | | DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
375 | | _ ⇒ None ? |
---|
376 | ]. |
---|
377 | |
---|
378 | lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x). |
---|
379 | #i cases i |
---|
380 | [#id cases id |
---|
381 | [1,2,3,6,7,33,34: |
---|
382 | #x #y %2 whd in match (is_jump ?); /2 by nmk/ |
---|
383 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: |
---|
384 | #x %2 whd in match (is_jump ?); /2 by nmk/ |
---|
385 | |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/ |
---|
386 | |9,10,14,15: #x %1 / by I/ |
---|
387 | |11,12,13,16,17: #x #y %1 / by I/ |
---|
388 | ] |
---|
389 | |2,3: #x %2 /2 by nmk/ |
---|
390 | |4,5: #x %1 / by I/ |
---|
391 | |6: #x #y %2 /2 by nmk/ |
---|
392 | ] |
---|
393 | qed. |
---|
394 | |
---|
395 | (* The first step of the jump expansion: everything to short. *) |
---|
396 | definition jump_expansion_start: |
---|
397 | ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l). |
---|
398 | ∀labels:label_map. |
---|
399 | Σpolicy:option ppc_pc_map. |
---|
400 | match policy with |
---|
401 | [ None ⇒ True |
---|
402 | | Some p ⇒ And (And (And (And (And |
---|
403 | (not_jump_default (pi1 ?? program) p) |
---|
404 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) |
---|
405 | (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉))) |
---|
406 | (sigma_compact_unsafe program labels p)) |
---|
407 | (∀i.i ≤ |program| → ∃pc. |
---|
408 | bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉)) |
---|
409 | (\fst p < 2^16) |
---|
410 | ] ≝ |
---|
411 | λprogram.λlabels. |
---|
412 | let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) |
---|
413 | (λprefix.Σpolicy:ppc_pc_map.And (And (And (And |
---|
414 | (not_jump_default prefix policy) |
---|
415 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) |
---|
416 | (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉))) |
---|
417 | (sigma_compact_unsafe prefix labels policy)) |
---|
418 | (∀i.i ≤ |prefix| → ∃pc. |
---|
419 | bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉)) |
---|
420 | program |
---|
421 | (λprefix.λx.λtl.λprf.λp. |
---|
422 | let 〈pc,sigma〉 ≝ pi1 ?? p in |
---|
423 | let 〈label,instr〉 ≝ x in |
---|
424 | let isize ≝ instruction_size_jmplen short_jump instr in |
---|
425 | 〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (|prefix|))) 〈pc+isize,short_jump〉 sigma〉 |
---|
426 | ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in |
---|
427 | if geb (\fst (pi1 ?? final_policy)) 2^16 then |
---|
428 | None ? |
---|
429 | else |
---|
430 | Some ? (pi1 ?? final_policy). |
---|
431 | [ / by I/ |
---|
432 | | lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg |
---|
433 | @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] |
---|
434 | | @conj [ @conj [ @conj [ @conj (*[@conj |
---|
435 | [ (* out_of_program_none *) |
---|
436 | #i #Hi2 >append_length <commutative_plus @conj |
---|
437 | [ (* → *) #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
438 | cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi |
---|
439 | [ >lookup_opt_insert_miss |
---|
440 | [ (* USE[pass]: out_of_program_none → *) |
---|
441 | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2)) |
---|
442 | @le_S_to_le @le_S_to_le @Hi |
---|
443 | | @bitvector_of_nat_abs |
---|
444 | [ @Hi2 |
---|
445 | | @(transitive_lt … Hi2) @le_S_to_le @Hi |
---|
446 | | @sym_neq @lt_to_not_eq @le_S_to_le @Hi |
---|
447 | ] |
---|
448 | ] |
---|
449 | | >lookup_opt_insert_miss |
---|
450 | [ <Hi |
---|
451 | (* USE[pass]: out_of_program_none → *) |
---|
452 | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (|prefix|))) ?)) |
---|
453 | [ >Hi @Hi2 |
---|
454 | | @le_S @le_n |
---|
455 | ] |
---|
456 | | @bitvector_of_nat_abs |
---|
457 | [ @Hi2 |
---|
458 | | @(transitive_lt … Hi2) <Hi @le_n |
---|
459 | | @sym_neq @lt_to_not_eq <Hi @le_n |
---|
460 | ] |
---|
461 | ] |
---|
462 | ] |
---|
463 | | (* ← *) cases p -p #p cases p -p #pc #p #Hp cases x in prf; -x #l #pi #prf |
---|
464 | normalize nodelta cases (decidable_eq_nat i (S (|prefix|))) |
---|
465 | [ #Hi >Hi >lookup_opt_insert_hit #H destruct (H) |
---|
466 | | #Hi >lookup_opt_insert_miss |
---|
467 | [ #Hl |
---|
468 | (* USE[pass]: out_of_program_none ← *) |
---|
469 | elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl)) |
---|
470 | [ #Hi3 @Hi3 |
---|
471 | | #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi |
---|
472 | ] |
---|
473 | | @bitvector_of_nat_abs |
---|
474 | [ @Hi2 |
---|
475 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length |
---|
476 | <plus_n_Sm @le_S_S @le_plus_n_r |
---|
477 | | @Hi |
---|
478 | ] |
---|
479 | ] |
---|
480 | ] |
---|
481 | ] |
---|
482 | | *) |
---|
483 | [ (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp |
---|
484 | cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi |
---|
485 | normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
486 | [ >lookup_insert_miss |
---|
487 | [ (* USE[pass]: not_jump_default *) |
---|
488 | lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) |
---|
489 | >nth_append_first |
---|
490 | [ #H #H2 @H @H2 |
---|
491 | | @Hi |
---|
492 | ] |
---|
493 | | @bitvector_of_nat_abs |
---|
494 | [ @(transitive_lt ??? Hi) @le_S_to_le] |
---|
495 | [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length |
---|
496 | <plus_n_Sm @le_S_S @le_plus_n_r |
---|
497 | | @lt_to_not_eq @le_S @Hi |
---|
498 | ] |
---|
499 | ] |
---|
500 | | >Hi >lookup_insert_miss |
---|
501 | [ #_ (* USE: everything is short *) |
---|
502 | elim ((proj2 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl |
---|
503 | >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl |
---|
504 | | @bitvector_of_nat_abs |
---|
505 | [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r |
---|
506 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S |
---|
507 | @le_plus_n_r |
---|
508 | | @lt_to_not_eq @le_n |
---|
509 | ] |
---|
510 | ] |
---|
511 | ] |
---|
512 | | (* 0 ↦ 0 *) |
---|
513 | cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
514 | >lookup_insert_miss |
---|
515 | [ (* USE[pass]: 0 ↦ 0 *) |
---|
516 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) |
---|
517 | | @bitvector_of_nat_abs |
---|
518 | [ / by / |
---|
519 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm |
---|
520 | @le_S_S @le_plus_n_r |
---|
521 | | @lt_to_not_eq / by / |
---|
522 | ] |
---|
523 | ] |
---|
524 | ] |
---|
525 | | (* fst p = pc *) |
---|
526 | cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
527 | >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl |
---|
528 | ] |
---|
529 | | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
530 | cases p -p #p cases p -p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
531 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
532 | [ >lookup_opt_insert_miss |
---|
533 | [ >lookup_opt_insert_miss |
---|
534 | [ (* USE[pass]: policy_compact_unsafe *) |
---|
535 | lapply (proj2 ?? (proj1 ?? Hp) i Hi) |
---|
536 | lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma)) |
---|
537 | cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %); |
---|
538 | [ #_ normalize nodelta / by / |
---|
539 | | #x cases x -x #pci #ji #EQi |
---|
540 | lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma)) |
---|
541 | cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma) in ⊢ (???% → %); |
---|
542 | [ #_ normalize nodelta / by / |
---|
543 | | #x cases x -x #pcSi #jSi #EQSi normalize nodelta >nth_append_first |
---|
544 | [ / by / |
---|
545 | | @Hi |
---|
546 | ] |
---|
547 | ] |
---|
548 | ] |
---|
549 | ] |
---|
550 | ] |
---|
551 | [2: lapply (le_S_to_le … Hi) -Hi #Hi] |
---|
552 | @bitvector_of_nat_abs |
---|
553 | [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus |
---|
554 | @le_plus_a @Hi |
---|
555 | |2,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm |
---|
556 | @le_S_S @le_plus_n_r |
---|
557 | |3,6: @lt_to_not_eq @le_S_S @Hi |
---|
558 | ] |
---|
559 | | >lookup_opt_insert_miss |
---|
560 | [ >Hi >lookup_opt_insert_hit normalize nodelta |
---|
561 | (* USE: everything is short, fst p = pc *) |
---|
562 | elim ((proj2 ?? Hp) (|prefix|) (le_n ?)) #pc #Hl |
---|
563 | lapply (proj2 ?? (proj1 ?? (proj1 ?? Hp))) >Hl |
---|
564 | >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #EQ normalize nodelta >nth_append_second |
---|
565 | [ <minus_n_n whd in match (nth ????); >EQ @refl |
---|
566 | | @le_n |
---|
567 | ] |
---|
568 | | @bitvector_of_nat_abs |
---|
569 | [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus |
---|
570 | @le_plus_a @le_n |
---|
571 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm |
---|
572 | @le_S_S @le_plus_n_r |
---|
573 | | @lt_to_not_eq @le_S_S >Hi @le_n |
---|
574 | ] |
---|
575 | ] |
---|
576 | ] |
---|
577 | ] |
---|
578 | | (* everything is short *) #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
579 | cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
580 | cases (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
581 | [ >lookup_opt_insert_miss |
---|
582 | [ (* USE[pass]: everything is short *) |
---|
583 | @((proj2 ?? Hp) i (le_S_S_to_le … Hi)) |
---|
584 | | @bitvector_of_nat_abs |
---|
585 | [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S |
---|
586 | >commutative_plus @le_plus_a @le_S_S_to_le @Hi |
---|
587 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length <plus_n_Sm |
---|
588 | @le_S_S @le_S_S @le_plus_n_r |
---|
589 | | @lt_to_not_eq @Hi |
---|
590 | ] |
---|
591 | ] |
---|
592 | | >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr)) |
---|
593 | @refl |
---|
594 | ] |
---|
595 | ] |
---|
596 | | @conj [ @conj [ @conj [ @conj (*[ @conj |
---|
597 | [ #i cases i |
---|
598 | [ #Hi2 @conj |
---|
599 | [ (* → *) #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by / |
---|
600 | | (* ← *) >lookup_opt_insert_hit #Hl destruct (Hl) |
---|
601 | ] |
---|
602 | | -i #i #Hi2 @conj |
---|
603 | [ #Hi >lookup_opt_insert_miss |
---|
604 | [ / by refl/ |
---|
605 | | @bitvector_of_nat_abs |
---|
606 | [ @Hi2 |
---|
607 | | / by / |
---|
608 | | @sym_neq @lt_to_not_eq / by / |
---|
609 | ] |
---|
610 | ] |
---|
611 | | #_ @le_S_S @le_O_n |
---|
612 | ] |
---|
613 | ] *) |
---|
614 | [ #i cases i |
---|
615 | [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
616 | | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
617 | ] |
---|
618 | ] ] |
---|
619 | >lookup_insert_hit @refl |
---|
620 | | #i cases i |
---|
621 | [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n |
---|
622 | | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
623 | ] |
---|
624 | ] |
---|
625 | | #i cases i |
---|
626 | [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl |
---|
627 | | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
628 | ] |
---|
629 | ] |
---|
630 | ] |
---|
631 | qed. |
---|
632 | |
---|
633 | (* NOTE: we only compare the first elements here because otherwise the |
---|
634 | * added = 0 → policy_equal property of jump_expansion_step doesn't hold: |
---|
635 | * if we have not added anything to the pc, we only know the PC hasn't changed, |
---|
636 | * there might still have been a short/medium jump change *) |
---|
637 | definition sigma_pc_equal ≝ |
---|
638 | λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. |
---|
639 | (∀n.n ≤ |program| → |
---|
640 | \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = |
---|
641 | \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). |
---|
642 | |
---|
643 | definition sigma_jump_equal ≝ |
---|
644 | λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. |
---|
645 | (∀n.n < |program| → |
---|
646 | \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = |
---|
647 | \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). |
---|
648 | |
---|
649 | definition nec_plus_ultra ≝ |
---|
650 | λprogram:list labelled_instruction.λp:ppc_pc_map. |
---|
651 | ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) → |
---|
652 | \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump). |
---|
653 | |
---|
654 | (*include alias "common/Identifiers.ma".*) |
---|
655 | include alias "ASM/BitVector.ma". |
---|
656 | include alias "basics/lists/list.ma". |
---|
657 | include alias "arithmetics/nat.ma". |
---|
658 | include alias "basics/logic.ma". |
---|
659 | |
---|
660 | lemma jump_length_equal_max: ∀a,b,i. |
---|
661 | is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i → |
---|
662 | (max_length a b) = a. |
---|
663 | #a #b #i cases i |
---|
664 | [1: #pi cases pi |
---|
665 | [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: |
---|
666 | try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H |
---|
667 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %) |
---|
668 | try (#abs normalize in abs; destruct (abs) @I) |
---|
669 | cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I) |
---|
670 | try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I) |
---|
671 | cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w |
---|
672 | try ( #abs normalize in abs; destruct (abs) @I) |
---|
673 | @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs) |
---|
674 | ] |
---|
675 | |2,3,6: #x [3: #y] #H cases H |
---|
676 | |4,5: #id #_ cases a cases b |
---|
677 | [2,3,4,6,11,12,13,15: normalize #H destruct (H) |
---|
678 | |1,5,7,8,9,10,14,16,17,18: #H / by refl/ |
---|
679 | ] |
---|
680 | ] |
---|
681 | qed. |
---|
682 | |
---|
683 | lemma jump_length_le_max: ∀a,b,i.is_jump i → |
---|
684 | instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i. |
---|
685 | #a #b #i cases i |
---|
686 | [2,3,6: #x [3: #y] #H cases H |
---|
687 | |4,5: #id #_ cases a cases b / by le_n/ |
---|
688 | |1: #pi cases pi |
---|
689 | [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: |
---|
690 | try (#x #y #H) try (#x #H) try (#H) cases H |
---|
691 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] |
---|
692 | #_ cases a cases b |
---|
693 | [1,4,5,6,7,8,9: / by le_n/ |
---|
694 | |10,13,14,15,16,17,18: / by le_n/ |
---|
695 | |19,22,23,24,25,26,27: / by le_n/ |
---|
696 | |28,31,32,33,34,35,36: / by le_n/ |
---|
697 | |37,40,41,42,43,44,45: / by le_n/ |
---|
698 | |46,47,48,49,50,51,52,53,54: / by le_n/ |
---|
699 | |55,56,57,58,59,60,61,62,63: / by le_n/ |
---|
700 | |64,65,66,67,68,69,70,71,72: / by le_n/ |
---|
701 | |73,74,75,76,77,78,79,80,81: / by le_n/ |
---|
702 | ] |
---|
703 | try (@(subaddressing_mode_elim … x) #w normalize @le_S @le_S @le_S @le_S @le_S @le_n) |
---|
704 | cases x * #ad |
---|
705 | try (@(subaddressing_mode_elim … ad) #w #z normalize @le_S @le_S @le_S @le_S @le_S @le_n) |
---|
706 | #z @(subaddressing_mode_elim … z) #w normalize / by / |
---|
707 | ] |
---|
708 | ] |
---|
709 | qed. |
---|
710 | |
---|
711 | lemma label_in_program: ∀program:(Σl.S (|l|) < 2^16 ∧ is_well_labelled_p l).∀labels:(Σlm. |
---|
712 | ∀l.occurs_exactly_once ?? l program → |
---|
713 | bitvector_of_nat ? (lookup_def ?? lm l 0) = |
---|
714 | address_of_word_labels_code_mem program l).∀x. |
---|
715 | occurs_exactly_once ?? x program → |
---|
716 | lookup_def ASMTag ℕ labels x O≤|program|. |
---|
717 | #program cases program -program #program #Hprogram #labels #x cases labels |
---|
718 | -labels #labels #H lapply (H x) -H |
---|
719 | generalize in match (lookup_def … labels x 0); |
---|
720 | whd in match address_of_word_labels_code_mem; |
---|
721 | whd in match index_of; normalize nodelta elim program in Hprogram; |
---|
722 | [ #Hprogram #n cases not_implemented |
---|
723 | | #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) -Hlm #Hbv |
---|
724 | whd in match (occurs_exactly_once ????) in Hocc; |
---|
725 | whd in match (index_of_internal ????) in Hbv; |
---|
726 | lapply (refl ? (instruction_matches_identifier … x h)) |
---|
727 | lapply Hocc; lapply Hbv; -Hocc -Hbv |
---|
728 | cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %); |
---|
729 | normalize nodelta #Hbv #Hocc #EQ |
---|
730 | [ >(bitvector_of_nat_ok 16 n 0) |
---|
731 | [ @le_O_n |
---|
732 | | >(eq_eq_bv … Hbv) @I |
---|
733 | | / by / |
---|
734 | | cases daemon |
---|
735 | ] |
---|
736 | | cases n in Hbv; |
---|
737 | [ #_ @le_O_n |
---|
738 | | -n #n #Hbv @le_S_S @(Hind … Hocc) |
---|
739 | [ @conj |
---|
740 | [ @(transitive_lt … (proj1 ?? Hprogram)) @le_n |
---|
741 | | cases daemon (* axiomatize this *) |
---|
742 | ] |
---|
743 | | #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???) |
---|
744 | [ >Hbv >eq_bv_refl @I |
---|
745 | | @(transitive_lt … (proj1 ?? Hprogram)) cases daemon |
---|
746 | | cases daemon |
---|
747 | | #H >(index_of_label_from_internal … Hocc) |
---|
748 | <plus_O_n >(index_of_label_from_internal … Hocc) in H; |
---|
749 | #H >(injective_S … H) <plus_O_n @refl |
---|
750 | ] |
---|
751 | ] |
---|
752 | ] |
---|
753 | ] |
---|
754 | ] |
---|
755 | qed. |
---|
756 | |
---|
757 | lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (|l|)) < 2^16 ∧ is_well_labelled_p l). |
---|
758 | ∀labels.∀old_sigma.∀sigma. |
---|
759 | sigma_pc_equal program old_sigma sigma → |
---|
760 | sigma_safe program labels 0 old_sigma sigma → |
---|
761 | sigma_compact_unsafe program labels sigma → |
---|
762 | sigma_compact program labels sigma. |
---|
763 | #program #labels #old_sigma #sigma #Hequal #Hsafe #Hcp_unsafe #i #Hi |
---|
764 | lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi) |
---|
765 | lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))) |
---|
766 | cases (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) in ⊢ (???% → %); |
---|
767 | [ / by / |
---|
768 | | #x cases x -x #x1 #x2 #EQ |
---|
769 | cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma)) |
---|
770 | [ / by / |
---|
771 | | #y cases y -y #y1 #y2 normalize nodelta #H #H2 |
---|
772 | cut (instruction_size_jmplen x2 |
---|
773 | (\snd (nth i ? program 〈None ?, Comment []〉)) = |
---|
774 | instruction_size … (bitvector_of_nat ? i) |
---|
775 | (\snd (nth i ? program 〈None ?, Comment []〉))) |
---|
776 | [5: #H3 <H3 @H2 |
---|
777 | |4: whd in match (instruction_size_jmplen ??); |
---|
778 | whd in match (instruction_size …); |
---|
779 | whd in match (assembly_1_pseudoinstruction …); |
---|
780 | whd in match (expand_pseudo_instruction …); |
---|
781 | normalize nodelta whd in match (append …) in H; |
---|
782 | cases (nth i ? program 〈None ?,Comment []〉) in H; |
---|
783 | #lbl #instr cases instr |
---|
784 | [2,3,6: #x [3: #y] normalize nodelta #H @refl |
---|
785 | |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj |
---|
786 | lapply (Hj x (refl ? x)) -Hj normalize nodelta |
---|
787 | >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O |
---|
788 | cases x2 normalize nodelta |
---|
789 | [1,4: whd in match short_jump_cond; normalize nodelta |
---|
790 | lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|))) |
---|
791 | cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab |
---|
792 | normalize nodelta |
---|
793 | >(Hequal (lookup_def ?? labels x 0) ?) |
---|
794 | [2,4,6,8: @(label_in_program program labels x) |
---|
795 | cases daemon (* XXX this has to come from somewhere else *) |
---|
796 | ] |
---|
797 | <plus_n_O |
---|
798 | cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) |
---|
799 | #result #flags normalize nodelta |
---|
800 | cases (vsplit bool 9 7 result) #upper #lower normalize nodelta |
---|
801 | cases (get_index' bool 2 0 flags) normalize nodelta |
---|
802 | [5,6,7,8: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/ |
---|
803 | |1,2,3,4: cases (eq_bv 9 upper ?) |
---|
804 | [2,4,6,8: #H lapply (proj1 ?? H) #H3 destruct (H3) |
---|
805 | |1,3,5,7: #_ normalize nodelta @refl |
---|
806 | ] |
---|
807 | ] |
---|
808 | |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond; |
---|
809 | lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|))) |
---|
810 | cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab |
---|
811 | normalize nodelta |
---|
812 | (* USE: added = 0 → policy_pc_equal (from fold) *) |
---|
813 | >(Hequal (lookup_def ?? labels x 0) ?) |
---|
814 | [2,4,6,8: @(label_in_program program labels x) |
---|
815 | cases daemon (* XXX this has to come from somewhere else *)] |
---|
816 | <plus_n_O |
---|
817 | normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 |
---|
818 | cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta |
---|
819 | cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) |
---|
820 | #result #flags normalize nodelta |
---|
821 | cases (vsplit bool 9 7 result) #upper #lower normalize nodelta |
---|
822 | cases (get_index' bool 2 0 flags) normalize nodelta |
---|
823 | #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl |
---|
824 | |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond; |
---|
825 | lapply (refl ? (leb (lookup_def ?? labels x 0) (|[]@program|))) |
---|
826 | cases (leb (lookup_def ?? labels x 0) (|[]@program|)) in ⊢ (???% → %); #Hlab |
---|
827 | normalize nodelta |
---|
828 | (* USE: added = 0 → policy_pc_equal (from fold) *) |
---|
829 | >(Hequal (lookup_def ?? labels x 0) ?) |
---|
830 | [2,4,6,8: @(label_in_program program labels x) |
---|
831 | cases daemon (* XXX this has to come from somewhere else *)] |
---|
832 | <plus_n_O normalize nodelta |
---|
833 | cases (vsplit bool 5 11 ?) #addr1 #addr2 |
---|
834 | cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta |
---|
835 | cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) |
---|
836 | #result #flags normalize nodelta |
---|
837 | cases (vsplit bool 9 7 result) #upper #lower normalize nodelta |
---|
838 | cases (get_index' bool 2 0 flags) normalize nodelta |
---|
839 | #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl |
---|
840 | ] |
---|
841 | |1: #pi cases pi |
---|
842 | [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: |
---|
843 | [1,2,3,6,7,24,25: #x #y |
---|
844 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] |
---|
845 | normalize nodelta #H @refl |
---|
846 | |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x] |
---|
847 | normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) |
---|
848 | #Hj lapply (Hj x (refl ? x)) -Hj |
---|
849 | whd in match expand_relative_jump; normalize nodelta |
---|
850 | whd in match expand_relative_jump_internal; normalize nodelta |
---|
851 | whd in match expand_relative_jump_unsafe; normalize nodelta |
---|
852 | whd in match expand_relative_jump_internal_unsafe; |
---|
853 | normalize nodelta >(add_bitvector_of_nat_plus ? i 1) |
---|
854 | <(plus_n_Sm i 0) <plus_n_O |
---|
855 | cases daemon (* XXX this needs subadressing mode magic, see above *) |
---|
856 | ] |
---|
857 | ] |
---|
858 | ] |
---|
859 | ] |
---|
860 | ] |
---|
861 | qed. |
---|
862 | |
---|
863 | lemma instruction_size_irrelevant: ∀i. |
---|
864 | ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i. |
---|
865 | #i cases i |
---|
866 | [2,3,6: #x [3: #y] #Hj #j1 #j2 % |
---|
867 | |4,5: #x #Hi cases Hi #abs @⊥ @abs @I |
---|
868 | |1: #pi cases pi |
---|
869 | [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: |
---|
870 | [1,2,3,6,7,24,25: #x #y |
---|
871 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] |
---|
872 | #Hj #j1 #j2 % |
---|
873 | |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x] |
---|
874 | #Hi cases Hi #abs @⊥ @abs @I |
---|
875 | ] |
---|
876 | ] |
---|
877 | qed. |
---|