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 | 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 | And (bitvector_of_nat ? (lookup_def ?? labels l 0) = |
---|
305 | address_of_word_labels_code_mem program l) |
---|
306 | (lookup_def ?? labels l 0 < |program|) |
---|
307 | ) ≝ |
---|
308 | λprogram. |
---|
309 | \fst (create_label_cost_map program). |
---|
310 | #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim |
---|
311 | #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map; |
---|
312 | normalize nodelta >EQ @(H l Hl) |
---|
313 | qed. |
---|
314 | |
---|
315 | (* General note on jump length selection: the jump displacement is added/replaced |
---|
316 | * AFTER the fetch (and attendant PC increase), but we calculate before the |
---|
317 | * fetch, which means that in the case of a short and medium jump we are 2 |
---|
318 | * bytes off and have to compensate. |
---|
319 | * For the long jump we don't care, because the PC gets replaced integrally anyway. *) |
---|
320 | definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
321 | Identifier → jump_length ≝ |
---|
322 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
323 | let pc ≝ \fst inc_sigma in |
---|
324 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in |
---|
325 | let paddr ≝ lookup_def … labels lbl 0 in |
---|
326 | let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *) |
---|
327 | then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) |
---|
328 | else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in |
---|
329 | let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in |
---|
330 | if sj_possible |
---|
331 | then short_jump |
---|
332 | else long_jump. |
---|
333 | |
---|
334 | definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
335 | Identifier → jump_length ≝ |
---|
336 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
337 | let pc ≝ \fst inc_sigma in |
---|
338 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in |
---|
339 | let paddr ≝ lookup_def ? ? labels lbl 0 in |
---|
340 | let addr ≝ bitvector_of_nat ? |
---|
341 | (if leb paddr ppc (* jump to address already known *) |
---|
342 | then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) |
---|
343 | else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in |
---|
344 | let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in |
---|
345 | if aj_possible |
---|
346 | then absolute_jump |
---|
347 | else long_jump. |
---|
348 | |
---|
349 | definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
350 | Identifier → jump_length ≝ |
---|
351 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
352 | let pc ≝ \fst inc_sigma in |
---|
353 | let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in |
---|
354 | let paddr ≝ lookup_def … labels lbl 0 in |
---|
355 | let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *) |
---|
356 | then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) |
---|
357 | else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in |
---|
358 | let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in |
---|
359 | if sj_possible |
---|
360 | then short_jump |
---|
361 | else select_call_length labels old_sigma inc_sigma added ppc lbl. |
---|
362 | |
---|
363 | definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map → |
---|
364 | ℕ → ℕ → preinstruction Identifier → option jump_length ≝ |
---|
365 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi. |
---|
366 | match i with |
---|
367 | [ JC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
368 | | JNC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
369 | | JZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
370 | | JNZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
371 | | JB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
372 | | JBC _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
373 | | JNB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
374 | | CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
375 | | DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
376 | | _ ⇒ None ? |
---|
377 | ]. |
---|
378 | |
---|
379 | lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x). |
---|
380 | #i cases i |
---|
381 | [#id cases id |
---|
382 | [1,2,3,6,7,33,34: |
---|
383 | #x #y %2 whd in match (is_jump ?); /2 by nmk/ |
---|
384 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: |
---|
385 | #x %2 whd in match (is_jump ?); /2 by nmk/ |
---|
386 | |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/ |
---|
387 | |9,10,14,15: #x %1 / by I/ |
---|
388 | |11,12,13,16,17: #x #y %1 / by I/ |
---|
389 | ] |
---|
390 | |2,3: #x %2 /2 by nmk/ |
---|
391 | |4,5: #x %1 / by I/ |
---|
392 | |6: #x #y %2 /2 by nmk/ |
---|
393 | ] |
---|
394 | qed. |
---|
395 | |
---|
396 | (* The first step of the jump expansion: everything to short. *) |
---|
397 | definition jump_expansion_start: |
---|
398 | ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l). |
---|
399 | ∀labels:label_map. |
---|
400 | Σpolicy:option ppc_pc_map. |
---|
401 | match policy with |
---|
402 | [ None ⇒ True |
---|
403 | | Some p ⇒ And (And (And (And (And |
---|
404 | (not_jump_default (pi1 ?? program) p) |
---|
405 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) |
---|
406 | (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉))) |
---|
407 | (sigma_compact_unsafe program labels p)) |
---|
408 | (∀i.i ≤ |program| → ∃pc. |
---|
409 | bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉)) |
---|
410 | (\fst p ≤ 2^16) |
---|
411 | ] ≝ |
---|
412 | λprogram.λlabels. |
---|
413 | let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) |
---|
414 | (λprefix.Σpolicy:ppc_pc_map.And (And (And (And |
---|
415 | (not_jump_default prefix policy) |
---|
416 | (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) |
---|
417 | (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉))) |
---|
418 | (sigma_compact_unsafe prefix labels policy)) |
---|
419 | (∀i.i ≤ |prefix| → ∃pc. |
---|
420 | bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉)) |
---|
421 | program |
---|
422 | (λprefix.λx.λtl.λprf.λp. |
---|
423 | let 〈pc,sigma〉 ≝ pi1 ?? p in |
---|
424 | let 〈label,instr〉 ≝ x in |
---|
425 | let isize ≝ instruction_size_jmplen short_jump instr in |
---|
426 | 〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (|prefix|))) 〈pc+isize,short_jump〉 sigma〉 |
---|
427 | ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in |
---|
428 | if gtb (\fst (pi1 ?? final_policy)) 2^16 then |
---|
429 | None ? |
---|
430 | else |
---|
431 | Some ? (pi1 ?? final_policy). |
---|
432 | [ / by I/ |
---|
433 | | lapply p -p cases final_policy -final_policy #p #Hp #hg |
---|
434 | @conj [ @Hp | @not_lt_to_le @ltb_false_to_not_lt @hg ] |
---|
435 | | @conj [ @conj [ @conj [ @conj |
---|
436 | [ (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp |
---|
437 | cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi |
---|
438 | normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
439 | [ >lookup_insert_miss |
---|
440 | [ (* USE[pass]: not_jump_default *) |
---|
441 | lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi) |
---|
442 | >nth_append_first |
---|
443 | [ #H #H2 @H @H2 |
---|
444 | | @Hi |
---|
445 | ] |
---|
446 | | @bitvector_of_nat_abs |
---|
447 | [ @(transitive_lt ??? Hi) @le_S_to_le] |
---|
448 | [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length |
---|
449 | <plus_n_Sm @le_S_S @le_plus_n_r |
---|
450 | | @lt_to_not_eq @le_S @Hi |
---|
451 | ] |
---|
452 | ] |
---|
453 | | >Hi >lookup_insert_miss |
---|
454 | [ #_ (* USE: everything is short *) |
---|
455 | elim ((proj2 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl |
---|
456 | >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl |
---|
457 | | @bitvector_of_nat_abs |
---|
458 | [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r |
---|
459 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S |
---|
460 | @le_plus_n_r |
---|
461 | | @lt_to_not_eq @le_n |
---|
462 | ] |
---|
463 | ] |
---|
464 | ] |
---|
465 | | (* 0 ↦ 0 *) |
---|
466 | cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
467 | >lookup_insert_miss |
---|
468 | [ (* USE[pass]: 0 ↦ 0 *) |
---|
469 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) |
---|
470 | | @bitvector_of_nat_abs |
---|
471 | [ / by / |
---|
472 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm |
---|
473 | @le_S_S @le_plus_n_r |
---|
474 | | @lt_to_not_eq / by / |
---|
475 | ] |
---|
476 | ] |
---|
477 | ] |
---|
478 | | (* fst p = pc *) |
---|
479 | cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
480 | >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl |
---|
481 | ] |
---|
482 | | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
483 | cases p -p #p cases p -p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
484 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
485 | [ >lookup_opt_insert_miss |
---|
486 | [ >lookup_opt_insert_miss |
---|
487 | [ (* USE[pass]: policy_compact_unsafe *) |
---|
488 | lapply (proj2 ?? (proj1 ?? Hp) i Hi) |
---|
489 | lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma)) |
---|
490 | cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %); |
---|
491 | [ #_ normalize nodelta / by / |
---|
492 | | #x cases x -x #pci #ji #EQi |
---|
493 | lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma)) |
---|
494 | cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma) in ⊢ (???% → %); |
---|
495 | [ #_ normalize nodelta / by / |
---|
496 | | #x cases x -x #pcSi #jSi #EQSi normalize nodelta >nth_append_first |
---|
497 | [ / by / |
---|
498 | | @Hi |
---|
499 | ] |
---|
500 | ] |
---|
501 | ] |
---|
502 | ] |
---|
503 | ] |
---|
504 | [2: lapply (le_S_to_le … Hi) -Hi #Hi] |
---|
505 | @bitvector_of_nat_abs |
---|
506 | [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus |
---|
507 | @le_plus_a @Hi |
---|
508 | |2,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm |
---|
509 | @le_S_S @le_plus_n_r |
---|
510 | |3,6: @lt_to_not_eq @le_S_S @Hi |
---|
511 | ] |
---|
512 | | >lookup_opt_insert_miss |
---|
513 | [ >Hi >lookup_opt_insert_hit normalize nodelta |
---|
514 | (* USE: everything is short, fst p = pc *) |
---|
515 | elim ((proj2 ?? Hp) (|prefix|) (le_n ?)) #pc #Hl |
---|
516 | lapply (proj2 ?? (proj1 ?? (proj1 ?? Hp))) >Hl |
---|
517 | >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #EQ normalize nodelta >nth_append_second |
---|
518 | [ <minus_n_n whd in match (nth ????); >EQ @refl |
---|
519 | | @le_n |
---|
520 | ] |
---|
521 | | @bitvector_of_nat_abs |
---|
522 | [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus |
---|
523 | @le_plus_a @le_n |
---|
524 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm |
---|
525 | @le_S_S @le_plus_n_r |
---|
526 | | @lt_to_not_eq @le_S_S >Hi @le_n |
---|
527 | ] |
---|
528 | ] |
---|
529 | ] |
---|
530 | ] |
---|
531 | | (* everything is short *) #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
532 | cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta |
---|
533 | cases (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
534 | [ >lookup_opt_insert_miss |
---|
535 | [ (* USE[pass]: everything is short *) |
---|
536 | @((proj2 ?? Hp) i (le_S_S_to_le … Hi)) |
---|
537 | | @bitvector_of_nat_abs |
---|
538 | [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S |
---|
539 | >commutative_plus @le_plus_a @le_S_S_to_le @Hi |
---|
540 | | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length <plus_n_Sm |
---|
541 | @le_S_S @le_S_S @le_plus_n_r |
---|
542 | | @lt_to_not_eq @Hi |
---|
543 | ] |
---|
544 | ] |
---|
545 | | >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr)) |
---|
546 | @refl |
---|
547 | ] |
---|
548 | ] |
---|
549 | | @conj [ @conj [ @conj [ @conj |
---|
550 | [ #i cases i |
---|
551 | [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
552 | | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
553 | ] |
---|
554 | ] ] |
---|
555 | >lookup_insert_hit @refl |
---|
556 | | #i cases i |
---|
557 | [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n |
---|
558 | | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
559 | ] |
---|
560 | ] |
---|
561 | | #i cases i |
---|
562 | [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl |
---|
563 | | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
564 | ] |
---|
565 | ] |
---|
566 | ] |
---|
567 | qed. |
---|
568 | |
---|
569 | (* NOTE: we only compare the first elements here because otherwise the |
---|
570 | * added = 0 → policy_equal property of jump_expansion_step doesn't hold: |
---|
571 | * if we have not added anything to the pc, we only know the PC hasn't changed, |
---|
572 | * there might still have been a short/medium jump change *) |
---|
573 | definition sigma_pc_equal ≝ |
---|
574 | λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. |
---|
575 | (∀n.n ≤ |program| → |
---|
576 | \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = |
---|
577 | \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). |
---|
578 | |
---|
579 | definition sigma_jump_equal ≝ |
---|
580 | λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. |
---|
581 | (∀n.n < |program| → |
---|
582 | \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = |
---|
583 | \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). |
---|
584 | |
---|
585 | definition nec_plus_ultra ≝ |
---|
586 | λprogram:list labelled_instruction.λp:ppc_pc_map. |
---|
587 | ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) → |
---|
588 | \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump). |
---|
589 | |
---|
590 | (*include alias "common/Identifiers.ma".*) |
---|
591 | include alias "ASM/BitVector.ma". |
---|
592 | include alias "basics/lists/list.ma". |
---|
593 | include alias "arithmetics/nat.ma". |
---|
594 | include alias "basics/logic.ma". |
---|
595 | |
---|
596 | lemma jump_length_equal_max: ∀a,b,i. |
---|
597 | is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i → |
---|
598 | (max_length a b) = a. |
---|
599 | #a #b #i cases i |
---|
600 | [1: #pi cases pi |
---|
601 | [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: |
---|
602 | try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H |
---|
603 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %) |
---|
604 | try (#abs normalize in abs; destruct (abs) @I) |
---|
605 | cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I) |
---|
606 | try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I) |
---|
607 | cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w |
---|
608 | try ( #abs normalize in abs; destruct (abs) @I) |
---|
609 | @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs) |
---|
610 | ] |
---|
611 | |2,3,6: #x [3: #y] #H cases H |
---|
612 | |4,5: #id #_ cases a cases b |
---|
613 | [2,3,4,6,11,12,13,15: normalize #H destruct (H) |
---|
614 | |1,5,7,8,9,10,14,16,17,18: #H / by refl/ |
---|
615 | ] |
---|
616 | ] |
---|
617 | qed. |
---|
618 | |
---|
619 | lemma jump_length_le_max: ∀a,b,i.is_jump i → |
---|
620 | instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i. |
---|
621 | #a #b #i cases i |
---|
622 | [2,3,6: #x [3: #y] #H cases H |
---|
623 | |4,5: #id #_ cases a cases b / by le_n/ |
---|
624 | |1: #pi cases pi |
---|
625 | [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: |
---|
626 | try (#x #y #H) try (#x #H) try (#H) cases H |
---|
627 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] |
---|
628 | #_ cases a cases b |
---|
629 | [1,4,5,6,7,8,9: / by le_n/ |
---|
630 | |10,13,14,15,16,17,18: / by le_n/ |
---|
631 | |19,22,23,24,25,26,27: / by le_n/ |
---|
632 | |28,31,32,33,34,35,36: / by le_n/ |
---|
633 | |37,40,41,42,43,44,45: / by le_n/ |
---|
634 | |46,47,48,49,50,51,52,53,54: / by le_n/ |
---|
635 | |55,56,57,58,59,60,61,62,63: / by le_n/ |
---|
636 | |64,65,66,67,68,69,70,71,72: / by le_n/ |
---|
637 | |73,74,75,76,77,78,79,80,81: / by le_n/ |
---|
638 | ] |
---|
639 | try (@(subaddressing_mode_elim … x) #w normalize @le_S @le_S @le_S @le_S @le_S @le_n) |
---|
640 | cases x * #ad |
---|
641 | try (@(subaddressing_mode_elim … ad) #w #z normalize @le_S @le_S @le_S @le_S @le_S @le_n) |
---|
642 | #z @(subaddressing_mode_elim … z) #w normalize / by / |
---|
643 | ] |
---|
644 | ] |
---|
645 | qed. |
---|
646 | |
---|
647 | lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (|l|)) < 2^16 ∧ is_well_labelled_p l). |
---|
648 | ∀old_sigma.∀sigma. |
---|
649 | sigma_pc_equal program old_sigma sigma → |
---|
650 | sigma_safe program (create_label_map program) 0 old_sigma sigma → |
---|
651 | sigma_compact_unsafe program (create_label_map program) sigma → |
---|
652 | sigma_compact program (create_label_map program) sigma. |
---|
653 | #program cases program -program #program #Hprogram #old_sigma #sigma #Hequal |
---|
654 | #Hsafe #Hcp_unsafe #i #Hi |
---|
655 | lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi) |
---|
656 | lapply (refl ? (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))) |
---|
657 | cases (lookup_opt … (bitvector_of_nat ? i) (\snd sigma)) in ⊢ (???% → %); |
---|
658 | [ / by / |
---|
659 | | #x cases x -x #x1 #x2 #EQ |
---|
660 | cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma)) |
---|
661 | [ / by / |
---|
662 | | #y cases y -y #y1 #y2 normalize nodelta #H #H2 |
---|
663 | cut (instruction_size_jmplen x2 |
---|
664 | (\snd (nth i ? program 〈None ?, Comment []〉)) = |
---|
665 | instruction_size … (bitvector_of_nat ? i) |
---|
666 | (\snd (nth i ? program 〈None ?, Comment []〉))) |
---|
667 | [5: #H3 <H3 @H2 |
---|
668 | |4: whd in match (instruction_size_jmplen ??); |
---|
669 | whd in match (instruction_size …); |
---|
670 | whd in match (assembly_1_pseudoinstruction …); |
---|
671 | whd in match (expand_pseudo_instruction …); |
---|
672 | normalize nodelta whd in match (append …) in H; |
---|
673 | lapply (refl ? (nth i ? program 〈None ?, Comment []〉)) lapply H |
---|
674 | cases (nth i ? program 〈None ?,Comment []〉) in ⊢ (% → ???% → %); |
---|
675 | #lbl #instr cases instr |
---|
676 | [2,3,6: #x [3: #y] normalize nodelta #H #_ % |
---|
677 | |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Hj #Heq |
---|
678 | lapply (Hj x (refl ? x)) -Hj normalize nodelta |
---|
679 | >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O |
---|
680 | cases x2 normalize nodelta |
---|
681 | [1,4: whd in match short_jump_cond; normalize nodelta |
---|
682 | cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|)) |
---|
683 | [1,3: cases (create_label_map program) #clm #Hclm |
---|
684 | @le_S_to_le @(proj2 ?? (Hclm x ?)) |
---|
685 | [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) |
---|
686 | |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] |
---|
687 | [1,4: >nat_of_bitvector_bitvector_of_nat_inverse |
---|
688 | [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi |
---|
689 | |2,5: whd in match fetch_pseudo_instruction; normalize nodelta |
---|
690 | >nth_safe_nth |
---|
691 | [1,3: >nat_of_bitvector_bitvector_of_nat_inverse |
---|
692 | [1,3: >Heq / by refl/ |
---|
693 | |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi |
---|
694 | ] |
---|
695 | ] |
---|
696 | |3,6: / by / |
---|
697 | ] |
---|
698 | |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O |
---|
699 | cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) |
---|
700 | #result #flags normalize nodelta |
---|
701 | cases (vsplit bool 9 7 result) #upper #lower normalize nodelta |
---|
702 | cases (get_index' bool 2 0 flags) normalize nodelta |
---|
703 | [3,4: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/ |
---|
704 | |1,2: cases (eq_bv 9 upper ?) |
---|
705 | [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3) |
---|
706 | |1,3: #_ normalize nodelta @refl |
---|
707 | ] |
---|
708 | ] |
---|
709 | ] |
---|
710 | |2,5: whd in match short_jump_cond; whd in match absolute_jump_cond; |
---|
711 | cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|)) |
---|
712 | [1,3: cases (create_label_map program) #clm #Hclm |
---|
713 | @le_S_to_le @(proj2 ?? (Hclm x ?)) |
---|
714 | [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) |
---|
715 | |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] |
---|
716 | [1,4: >nat_of_bitvector_bitvector_of_nat_inverse |
---|
717 | [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi |
---|
718 | |2,5: whd in match fetch_pseudo_instruction; normalize nodelta |
---|
719 | >nth_safe_nth |
---|
720 | [1,3: >nat_of_bitvector_bitvector_of_nat_inverse |
---|
721 | [1,3: >Heq / by refl/ |
---|
722 | |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi |
---|
723 | ] |
---|
724 | ] |
---|
725 | |3,6: / by / |
---|
726 | ] |
---|
727 | |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O |
---|
728 | normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2 |
---|
729 | cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta |
---|
730 | cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) |
---|
731 | #result #flags normalize nodelta |
---|
732 | cases (vsplit bool 9 7 result) #upper #lower normalize nodelta |
---|
733 | cases (get_index' bool 2 0 flags) normalize nodelta |
---|
734 | #H >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl |
---|
735 | ] |
---|
736 | |3,6: whd in match short_jump_cond; whd in match absolute_jump_cond; |
---|
737 | cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|)) |
---|
738 | [1,3: cases (create_label_map program) #clm #Hclm |
---|
739 | @le_S_to_le @(proj2 ?? (Hclm x ?)) |
---|
740 | [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??) |
---|
741 | |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)] |
---|
742 | [1,4: >nat_of_bitvector_bitvector_of_nat_inverse |
---|
743 | [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi |
---|
744 | |2,5: whd in match fetch_pseudo_instruction; normalize nodelta |
---|
745 | >nth_safe_nth |
---|
746 | [1,3: >nat_of_bitvector_bitvector_of_nat_inverse |
---|
747 | [1,3: >Heq / by refl/ |
---|
748 | |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi |
---|
749 | ] |
---|
750 | ] |
---|
751 | |3,6: / by / |
---|
752 | ] |
---|
753 | |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O |
---|
754 | cases (vsplit bool 5 11 ?) #addr1 #addr2 |
---|
755 | cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta |
---|
756 | cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false) |
---|
757 | #result #flags normalize nodelta |
---|
758 | cases (vsplit bool 9 7 result) #upper #lower normalize nodelta |
---|
759 | cases (get_index' bool 2 0 flags) normalize nodelta |
---|
760 | #H >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl |
---|
761 | ] |
---|
762 | ] |
---|
763 | |1: #pi cases pi |
---|
764 | [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: |
---|
765 | [1,2,3,6,7,24,25: #x #y |
---|
766 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] |
---|
767 | normalize nodelta #H #Heq @refl |
---|
768 | |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x] |
---|
769 | normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) |
---|
770 | #Hj #Heq lapply (Hj x (refl ? x)) -Hj |
---|
771 | whd in match expand_relative_jump; normalize nodelta |
---|
772 | whd in match expand_relative_jump_internal; normalize nodelta |
---|
773 | whd in match expand_relative_jump_unsafe; normalize nodelta |
---|
774 | whd in match expand_relative_jump_internal_unsafe; |
---|
775 | normalize nodelta >(add_bitvector_of_nat_plus ? i 1) |
---|
776 | <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta |
---|
777 | [1,4,7,10,13,16,19,22,25: |
---|
778 | cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) |
---|
779 | [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ] |
---|
780 | #fst_foo >fst_foo @pair_elim #sj_possible #disp #H #H2 |
---|
781 | @(pair_replace ?????????? (eq_to_jmeq … H)) |
---|
782 | [1,3,5,7,9,11,13,15,17: |
---|
783 | cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|)) |
---|
784 | [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm |
---|
785 | @le_S_to_le @(proj2 ?? (Hclm x ?)) |
---|
786 | @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) |
---|
787 | [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse |
---|
788 | [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi |
---|
789 | |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta |
---|
790 | >nth_safe_nth |
---|
791 | [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse |
---|
792 | [1,3,5,7,9,11,13,15,17: >Heq %] |
---|
793 | @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi |
---|
794 | ] |
---|
795 | ] |
---|
796 | >Heq / by / |
---|
797 | ] |
---|
798 | #X >(le_to_leb_true … X) @refl |
---|
799 | ] |
---|
800 | >(proj1 ?? H2) try (@refl) normalize nodelta |
---|
801 | [1,2,3,5: @(subaddressing_mode_elim … y) #w % |
---|
802 | | cases y * #sth #sth2 @(subaddressing_mode_elim … sth) |
---|
803 | @(subaddressing_mode_elim … sth2) #x [3,4: #x2] % |
---|
804 | ] |
---|
805 | |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs #abs2 @⊥ @abs2 / by I/ |
---|
806 | ] |
---|
807 | cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) |
---|
808 | [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ] |
---|
809 | #fst_foo * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H |
---|
810 | @(pair_replace ?????????? (eq_to_jmeq … H)) |
---|
811 | [1,3,5,7,9,11,13,15,17: |
---|
812 | cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|)) |
---|
813 | [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm |
---|
814 | @le_S_to_le @(proj2 ?? (Hclm x ?)) |
---|
815 | @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) |
---|
816 | [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse |
---|
817 | [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi |
---|
818 | |2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta |
---|
819 | >nth_safe_nth |
---|
820 | [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse |
---|
821 | [1,3,5,7,9,11,13,15,17: >Heq %] |
---|
822 | @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi |
---|
823 | ] |
---|
824 | ] |
---|
825 | >Heq / by / |
---|
826 | ] |
---|
827 | #X >(le_to_leb_true … X) @refl |
---|
828 | ] |
---|
829 | #H2 >H2 try (@refl) normalize nodelta |
---|
830 | [1,2,3,5: @(subaddressing_mode_elim … y) #w % |
---|
831 | | cases y * #sth #sth2 @(subaddressing_mode_elim … sth2) #w |
---|
832 | [1,2: %] whd in match (map ????); whd in match (flatten ??); |
---|
833 | whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%); |
---|
834 | >length_append >length_append @eq_f2 % |
---|
835 | ] |
---|
836 | ] |
---|
837 | ] |
---|
838 | ] |
---|
839 | ] |
---|
840 | ] |
---|
841 | qed. |
---|
842 | |
---|
843 | lemma instruction_size_irrelevant: ∀i. |
---|
844 | ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i. |
---|
845 | #i cases i |
---|
846 | [2,3,6: #x [3: #y] #Hj #j1 #j2 % |
---|
847 | |4,5: #x #Hi cases Hi #abs @⊥ @abs @I |
---|
848 | |1: #pi cases pi |
---|
849 | [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: |
---|
850 | [1,2,3,6,7,24,25: #x #y |
---|
851 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] |
---|
852 | #Hj #j1 #j2 % |
---|
853 | |9,10,11,12,13,14,15,16,17: [1,2,6,7: #x |3,4,5,8,9: #y #x] |
---|
854 | #Hi cases Hi #abs @⊥ @abs @I |
---|
855 | ] |
---|
856 | ] |
---|
857 | qed. |
---|