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