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 | include alias "basics/lists/list.ma". |
---|
9 | include alias "arithmetics/nat.ma". |
---|
10 | include alias "basics/logic.ma". |
---|
11 | |
---|
12 | (* Internal types *) |
---|
13 | |
---|
14 | (* ppc_pc_map: program length × (pseudo program counter ↦ 〈pc, jump_length〉) *) |
---|
15 | definition ppc_pc_map ≝ ℕ × (BitVectorTrie (ℕ × jump_length) 16). |
---|
16 | |
---|
17 | (* The different properties that we want/need to prove at some point *) |
---|
18 | (* Anything that's not in the program doesn't end up in the policy *) |
---|
19 | definition out_of_program_none: list labelled_instruction → ppc_pc_map → Prop ≝ |
---|
20 | λprefix.λsigma. |
---|
21 | ∀i:ℕ.i ≥ |prefix| → i < 2^16 → bvt_lookup_opt … (bitvector_of_nat 16 i) (\snd sigma) = None ?. |
---|
22 | |
---|
23 | (* If instruction i is a jump, then there will be something in the policy at |
---|
24 | * position i *) |
---|
25 | definition is_jump' ≝ |
---|
26 | λx:preinstruction Identifier. |
---|
27 | match x with |
---|
28 | [ JC _ ⇒ True |
---|
29 | | JNC _ ⇒ True |
---|
30 | | JZ _ ⇒ True |
---|
31 | | JNZ _ ⇒ True |
---|
32 | | JB _ _ ⇒ True |
---|
33 | | JNB _ _ ⇒ True |
---|
34 | | JBC _ _ ⇒ True |
---|
35 | | CJNE _ _ ⇒ True |
---|
36 | | DJNZ _ _ ⇒ True |
---|
37 | | _ ⇒ False |
---|
38 | ]. |
---|
39 | |
---|
40 | definition is_jump ≝ |
---|
41 | λinstr:pseudo_instruction. |
---|
42 | match instr with |
---|
43 | [ Instruction i ⇒ is_jump' i |
---|
44 | | Call _ ⇒ True |
---|
45 | | Jmp _ ⇒ True |
---|
46 | | _ ⇒ False |
---|
47 | ]. |
---|
48 | |
---|
49 | definition is_jump_to ≝ |
---|
50 | λx:pseudo_instruction.λd:Identifier. |
---|
51 | match x with |
---|
52 | [ Instruction i ⇒ match i with |
---|
53 | [ JC j ⇒ d = j |
---|
54 | | JNC j ⇒ d = j |
---|
55 | | JZ j ⇒ d = j |
---|
56 | | JNZ j ⇒ d = j |
---|
57 | | JB _ j ⇒ d = j |
---|
58 | | JNB _ j ⇒ d = j |
---|
59 | | CJNE _ j ⇒ d = j |
---|
60 | | DJNZ _ j ⇒ d = j |
---|
61 | | _ ⇒ False |
---|
62 | ] |
---|
63 | | Call c ⇒ d = c |
---|
64 | | Jmp j ⇒ d = j |
---|
65 | | _ ⇒ False |
---|
66 | ]. |
---|
67 | |
---|
68 | definition jump_not_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝ |
---|
69 | λprefix.λsigma. |
---|
70 | ∀i:ℕ.i < |prefix| → |
---|
71 | ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) → |
---|
72 | \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) = short_jump. |
---|
73 | |
---|
74 | (* if the instruction 〈p,a〉 is a jump to label l, then label l is at address a *) |
---|
75 | (* definition labels_okay: label_map → ppc_pc_map → Prop ≝ |
---|
76 | λlabels.λsigma. |
---|
77 | bvt_forall ?? (\snd sigma) (λn.λx. |
---|
78 | let 〈pc,addr_nat〉 ≝ x in |
---|
79 | ∃id:Identifier.lookup_def … labels id 0 = addr_nat |
---|
80 | ). *) |
---|
81 | |
---|
82 | (* Between two policies, jumps cannot decrease *) |
---|
83 | definition jmpeqb: jump_length → jump_length → bool ≝ |
---|
84 | λj1.λj2. |
---|
85 | match j1 with |
---|
86 | [ short_jump ⇒ match j2 with [ short_jump ⇒ true | _ ⇒ false ] |
---|
87 | | medium_jump ⇒ match j2 with [ medium_jump ⇒ true | _ ⇒ false ] |
---|
88 | | long_jump ⇒ match j2 with [ long_jump ⇒ true | _ ⇒ false ] |
---|
89 | ]. |
---|
90 | |
---|
91 | lemma jmpeqb_to_eq: ∀j1,j2.jmpeqb j1 j2 → j1 = j2. |
---|
92 | #j1 #j2 cases j1 cases j2 |
---|
93 | [1,5,9: / by /] |
---|
94 | #H cases H |
---|
95 | qed. |
---|
96 | |
---|
97 | definition jmple: jump_length → jump_length → Prop ≝ |
---|
98 | λj1.λj2. |
---|
99 | match j1 with |
---|
100 | [ short_jump ⇒ |
---|
101 | match j2 with |
---|
102 | [ short_jump ⇒ False |
---|
103 | | _ ⇒ True |
---|
104 | ] |
---|
105 | | medium_jump ⇒ |
---|
106 | match j2 with |
---|
107 | [ long_jump ⇒ True |
---|
108 | | _ ⇒ False |
---|
109 | ] |
---|
110 | | long_jump ⇒ False |
---|
111 | ]. |
---|
112 | |
---|
113 | definition jmpleq: jump_length → jump_length → Prop ≝ |
---|
114 | λj1.λj2.jmple j1 j2 ∨ j1 = j2. |
---|
115 | |
---|
116 | definition policy_increase: list labelled_instruction → ppc_pc_map → |
---|
117 | ppc_pc_map → Prop ≝ |
---|
118 | λprogram.λop.λp. |
---|
119 | ∀i.i < |program| → |
---|
120 | let 〈opc,oj〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd op) 〈0,short_jump〉 in |
---|
121 | let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉 in |
---|
122 | (*opc ≤ pc ∧*) jmpleq oj j. |
---|
123 | |
---|
124 | (* Policy safety *) |
---|
125 | (*definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝ |
---|
126 | λprogram.λlabels.λsigma. |
---|
127 | ∀i.i < |program| → |
---|
128 | let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,false〉 in |
---|
129 | let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in |
---|
130 | ∀dest.is_jump_to instr dest → |
---|
131 | let paddr ≝ lookup_def … labels dest 0 in |
---|
132 | let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,false〉) in |
---|
133 | match j with |
---|
134 | [ None ⇒ True |
---|
135 | | Some j ⇒ match j with |
---|
136 | [ short_jump ⇒ |
---|
137 | if leb pc addr |
---|
138 | then le (addr - pc) 126 |
---|
139 | else le (pc - addr) 129 |
---|
140 | | medium_jump ⇒ |
---|
141 | let a ≝ bitvector_of_nat 16 addr in |
---|
142 | let p ≝ bitvector_of_nat 16 pc in |
---|
143 | let 〈fst_5_addr, rest_addr〉 ≝ split bool 5 11 a in |
---|
144 | let 〈fst_5_pc, rest_pc〉 ≝ split bool 5 11 p in |
---|
145 | eq_bv 5 fst_5_addr fst_5_pc = true |
---|
146 | | long_jump ⇒ True |
---|
147 | ] |
---|
148 | ].*) |
---|
149 | |
---|
150 | (* this is the instruction size as determined by the distance from origin to destination *) |
---|
151 | (*definition instruction_size_sigma: label_map → ppc_pc_map → Word → pseudo_instruction → ℕ ≝ |
---|
152 | λlabels.λsigma.λpc.λi. |
---|
153 | \fst (assembly_1_pseudoinstruction |
---|
154 | (λid.bitvector_of_nat 16 (lookup_def … labels id 0)) |
---|
155 | (λi.bitvector_of_nat 16 (\fst (bvt_lookup ?? i (\snd sigma) 〈0,false〉))) pc |
---|
156 | (λx.zero 16) i).*) |
---|
157 | |
---|
158 | (* this is the instruction size as determined by the jump length given *) |
---|
159 | definition expand_relative_jump_internal_unsafe: |
---|
160 | jump_length → ([[relative]] → preinstruction [[relative]]) → list instruction ≝ |
---|
161 | λjmp_len:jump_length.λi. |
---|
162 | match jmp_len with |
---|
163 | [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ] |
---|
164 | | medium_jump ⇒ [ ] (* this should not happen *) |
---|
165 | | long_jump ⇒ |
---|
166 | [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); |
---|
167 | SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *) |
---|
168 | LJMP (ADDR16 (zero 16)) |
---|
169 | ] |
---|
170 | ]. |
---|
171 | @I |
---|
172 | qed. |
---|
173 | |
---|
174 | definition expand_relative_jump_unsafe: |
---|
175 | jump_length → preinstruction Identifier → list instruction ≝ |
---|
176 | λjmp_len:jump_length.λi. |
---|
177 | match i with |
---|
178 | [ JC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JC ?) |
---|
179 | | JNC jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNC ?) |
---|
180 | | JB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JB ? baddr) |
---|
181 | | JZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JZ ?) |
---|
182 | | JNZ jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNZ ?) |
---|
183 | | JBC baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JBC ? baddr) |
---|
184 | | JNB baddr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (JNB ? baddr) |
---|
185 | | CJNE addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (CJNE ? addr) |
---|
186 | | DJNZ addr jmp ⇒ expand_relative_jump_internal_unsafe jmp_len (DJNZ ? addr) |
---|
187 | | ADD arg1 arg2 ⇒ [ ADD ? arg1 arg2 ] |
---|
188 | | ADDC arg1 arg2 ⇒ [ ADDC ? arg1 arg2 ] |
---|
189 | | SUBB arg1 arg2 ⇒ [ SUBB ? arg1 arg2 ] |
---|
190 | | INC arg ⇒ [ INC ? arg ] |
---|
191 | | DEC arg ⇒ [ DEC ? arg ] |
---|
192 | | MUL arg1 arg2 ⇒ [ MUL ? arg1 arg2 ] |
---|
193 | | DIV arg1 arg2 ⇒ [ DIV ? arg1 arg2 ] |
---|
194 | | DA arg ⇒ [ DA ? arg ] |
---|
195 | | ANL arg ⇒ [ ANL ? arg ] |
---|
196 | | ORL arg ⇒ [ ORL ? arg ] |
---|
197 | | XRL arg ⇒ [ XRL ? arg ] |
---|
198 | | CLR arg ⇒ [ CLR ? arg ] |
---|
199 | | CPL arg ⇒ [ CPL ? arg ] |
---|
200 | | RL arg ⇒ [ RL ? arg ] |
---|
201 | | RR arg ⇒ [ RR ? arg ] |
---|
202 | | RLC arg ⇒ [ RLC ? arg ] |
---|
203 | | RRC arg ⇒ [ RRC ? arg ] |
---|
204 | | SWAP arg ⇒ [ SWAP ? arg ] |
---|
205 | | MOV arg ⇒ [ MOV ? arg ] |
---|
206 | | MOVX arg ⇒ [ MOVX ? arg ] |
---|
207 | | SETB arg ⇒ [ SETB ? arg ] |
---|
208 | | PUSH arg ⇒ [ PUSH ? arg ] |
---|
209 | | POP arg ⇒ [ POP ? arg ] |
---|
210 | | XCH arg1 arg2 ⇒ [ XCH ? arg1 arg2 ] |
---|
211 | | XCHD arg1 arg2 ⇒ [ XCHD ? arg1 arg2 ] |
---|
212 | | RET ⇒ [ RET ? ] |
---|
213 | | RETI ⇒ [ RETI ? ] |
---|
214 | | NOP ⇒ [ RealInstruction (NOP ?) ] |
---|
215 | ]. |
---|
216 | |
---|
217 | definition instruction_size_jmplen: |
---|
218 | jump_length → pseudo_instruction → ℕ ≝ |
---|
219 | λjmp_len. |
---|
220 | λi. |
---|
221 | let pseudos ≝ match i with |
---|
222 | [ Cost cost ⇒ [ ] |
---|
223 | | Comment comment ⇒ [ ] |
---|
224 | | Call call ⇒ |
---|
225 | match jmp_len with |
---|
226 | [ short_jump ⇒ [ ] (* this should not happen *) |
---|
227 | | medium_jump ⇒ [ ACALL (ADDR11 (zero 11)) ] |
---|
228 | | long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ] |
---|
229 | ] |
---|
230 | | Mov d trgt ⇒ |
---|
231 | [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))] |
---|
232 | | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr |
---|
233 | | Jmp jmp ⇒ |
---|
234 | match jmp_len with |
---|
235 | [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ] |
---|
236 | | medium_jump ⇒ [ AJMP (ADDR11 (zero 11)) ] |
---|
237 | | long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ] |
---|
238 | ] |
---|
239 | ] in |
---|
240 | let mapped ≝ map ? ? assembly1 pseudos in |
---|
241 | let flattened ≝ flatten ? mapped in |
---|
242 | let pc_len ≝ length ? flattened in |
---|
243 | pc_len. |
---|
244 | @I. |
---|
245 | qed. |
---|
246 | |
---|
247 | (* new safety condition: policy corresponds to program and resulting program is compact *) |
---|
248 | definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop ≝ |
---|
249 | λprogram.λlabels.λsigma. |
---|
250 | ∀n:ℕ.S n < |program| → |
---|
251 | match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with |
---|
252 | [ None ⇒ False |
---|
253 | | Some x ⇒ let 〈pc,j〉 ≝ x in |
---|
254 | match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with |
---|
255 | [ None ⇒ False |
---|
256 | | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in |
---|
257 | pc1 = instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) |
---|
258 | (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) |
---|
259 | (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) |
---|
260 | (bitvector_of_nat ? pc) (\snd (nth n ? program 〈None ?, Comment []〉)) |
---|
261 | ] |
---|
262 | ]. |
---|
263 | |
---|
264 | (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) |
---|
265 | definition max_length: jump_length → jump_length → jump_length ≝ |
---|
266 | λj1.λj2. |
---|
267 | match j1 with |
---|
268 | [ long_jump ⇒ long_jump |
---|
269 | | medium_jump ⇒ |
---|
270 | match j2 with |
---|
271 | [ medium_jump ⇒ medium_jump |
---|
272 | | _ ⇒ long_jump |
---|
273 | ] |
---|
274 | | short_jump ⇒ |
---|
275 | match j2 with |
---|
276 | [ short_jump ⇒ short_jump |
---|
277 | | _ ⇒ long_jump |
---|
278 | ] |
---|
279 | ]. |
---|
280 | |
---|
281 | lemma dec_jmple: ∀x,y:jump_length.Sum (jmple x y) (¬(jmple x y)). |
---|
282 | #x #y cases x cases y /3 by inl, inr, nmk, I/ |
---|
283 | qed. |
---|
284 | |
---|
285 | lemma jmpleq_max_length: ∀ol,nl. |
---|
286 | jmpleq ol (max_length ol nl). |
---|
287 | #ol #nl cases ol cases nl |
---|
288 | /2 by or_introl, or_intror, I/ |
---|
289 | qed. |
---|
290 | |
---|
291 | lemma dec_eq_jump_length: ∀a,b:jump_length.Sum (a = b) (a ≠ b). |
---|
292 | #a #b cases a cases b /2/ |
---|
293 | %2 @nmk #H destruct (H) |
---|
294 | qed. |
---|
295 | |
---|
296 | definition policy_isize_sum ≝ |
---|
297 | λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. |
---|
298 | (\fst sigma) = foldl_strong (option Identifier × pseudo_instruction) |
---|
299 | (λacc.ℕ) |
---|
300 | prefix |
---|
301 | (λhd.λx.λtl.λp.λacc. |
---|
302 | acc + (instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) |
---|
303 | (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) |
---|
304 | (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) |
---|
305 | (bitvector_of_nat 16 (\fst sigma)) (\snd x))) |
---|
306 | 0. |
---|
307 | |
---|
308 | (* The function that creates the label-to-address map *) |
---|
309 | definition create_label_map: ∀program:list labelled_instruction. |
---|
310 | (Σlabels:label_map. |
---|
311 | ∀l.occurs_exactly_once ?? l program → |
---|
312 | bitvector_of_nat ? (lookup_def ?? labels l 0) = |
---|
313 | address_of_word_labels_code_mem program l |
---|
314 | ) ≝ |
---|
315 | λprogram. |
---|
316 | \fst (create_label_cost_map program). |
---|
317 | #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim |
---|
318 | #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map; |
---|
319 | normalize nodelta >EQ @(H l Hl) |
---|
320 | qed. |
---|
321 | |
---|
322 | definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
323 | Identifier → jump_length ≝ |
---|
324 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
325 | let paddr ≝ lookup_def … labels lbl 0 in |
---|
326 | if leb ppc paddr (* forward jump *) |
---|
327 | then |
---|
328 | let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) |
---|
329 | + added in |
---|
330 | if leb (addr - \fst inc_sigma) 126 |
---|
331 | then short_jump |
---|
332 | else long_jump |
---|
333 | else |
---|
334 | let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in |
---|
335 | if leb (\fst inc_sigma - addr) 129 |
---|
336 | then short_jump |
---|
337 | else long_jump. |
---|
338 | |
---|
339 | definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
340 | Identifier → jump_length ≝ |
---|
341 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
342 | let paddr ≝ lookup_def ? ? labels lbl 0 in |
---|
343 | let addr ≝ |
---|
344 | if leb ppc paddr (* forward jump *) |
---|
345 | then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) |
---|
346 | + added |
---|
347 | else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in |
---|
348 | let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (bitvector_of_nat ? addr) in |
---|
349 | let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 (bitvector_of_nat ? (\fst inc_sigma)) in |
---|
350 | if eq_bv ? fst_5_addr fst_5_pc |
---|
351 | then medium_jump |
---|
352 | else long_jump. |
---|
353 | |
---|
354 | definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ → |
---|
355 | Identifier → jump_length ≝ |
---|
356 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl. |
---|
357 | let paddr ≝ lookup_def … labels lbl 0 in |
---|
358 | if leb ppc paddr (* forward jump *) |
---|
359 | then |
---|
360 | let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) |
---|
361 | + added in |
---|
362 | if leb (addr - \fst inc_sigma) 126 |
---|
363 | then short_jump |
---|
364 | else select_call_length labels old_sigma inc_sigma added ppc lbl |
---|
365 | else |
---|
366 | let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in |
---|
367 | if leb (\fst inc_sigma - addr) 129 |
---|
368 | then short_jump |
---|
369 | else select_call_length labels old_sigma inc_sigma added ppc lbl. |
---|
370 | |
---|
371 | definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map → |
---|
372 | ℕ → ℕ → preinstruction Identifier → option jump_length ≝ |
---|
373 | λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi. |
---|
374 | match i with |
---|
375 | [ JC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
376 | | JNC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
377 | | JZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
378 | | JNZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
379 | | JB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
380 | | JBC _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
381 | | JNB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
382 | | CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
383 | | DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) |
---|
384 | | _ ⇒ None ? |
---|
385 | ]. |
---|
386 | |
---|
387 | lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x). |
---|
388 | #i cases i |
---|
389 | [#id cases id |
---|
390 | [1,2,3,6,7,33,34: |
---|
391 | #x #y %2 whd in match (is_jump ?); /2 by nmk/ |
---|
392 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: |
---|
393 | #x %2 whd in match (is_jump ?); /2 by nmk/ |
---|
394 | |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/ |
---|
395 | |9,10,14,15: #x %1 / by I/ |
---|
396 | |11,12,13,16,17: #x #y %1 / by I/ |
---|
397 | ] |
---|
398 | |2,3: #x %2 /2 by nmk/ |
---|
399 | |4,5: #x %1 / by I/ |
---|
400 | |6: #x #y %2 /2 by nmk/ |
---|
401 | ] |
---|
402 | qed. |
---|
403 | |
---|
404 | lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a. |
---|
405 | #a #b / by refl/ |
---|
406 | qed. |
---|
407 | |
---|
408 | (* The first step of the jump expansion: everything to short. |
---|
409 | * The third condition of the dependent type implies jump_in_policy; |
---|
410 | * I've left it in for convenience of type-checking. *) |
---|
411 | definition jump_expansion_start: |
---|
412 | ∀program:(Σl:list labelled_instruction.|l| < 2^16). |
---|
413 | ∀labels:label_map. |
---|
414 | Σpolicy:option ppc_pc_map. |
---|
415 | match policy with |
---|
416 | [ None ⇒ True |
---|
417 | | Some p ⇒ |
---|
418 | And (And (out_of_program_none (pi1 ?? program) p) |
---|
419 | (jump_not_in_policy (pi1 ?? program) p)) |
---|
420 | (\fst p < 2^16) |
---|
421 | ] ≝ |
---|
422 | λprogram.λlabels. |
---|
423 | let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) |
---|
424 | (λprefix.Σpolicy:ppc_pc_map. |
---|
425 | And (out_of_program_none prefix policy) |
---|
426 | (jump_not_in_policy prefix policy)) |
---|
427 | program |
---|
428 | (λprefix.λx.λtl.λprf.λp. |
---|
429 | let 〈pc,sigma〉 ≝ p in |
---|
430 | let 〈label,instr〉 ≝ x in |
---|
431 | let isize ≝ instruction_size_jmplen short_jump instr in |
---|
432 | 〈pc + isize, |
---|
433 | match instr with |
---|
434 | [ Instruction i ⇒ match i with |
---|
435 | [ JC jmp ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
436 | | JNC _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
437 | | JZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
438 | | JNZ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
439 | | JB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
440 | | JNB _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
441 | | JBC _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
442 | | CJNE _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
443 | | DJNZ _ _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
444 | | _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
445 | ] |
---|
446 | | Call c ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
447 | | Jmp j ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
448 | | _ ⇒ bvt_insert … (bitvector_of_nat 16 (|prefix|)) 〈pc,short_jump〉 sigma |
---|
449 | ]〉 |
---|
450 | ) 〈0, Stub ? ?〉 in |
---|
451 | if geb (\fst final_policy) 2^16 then |
---|
452 | None ? |
---|
453 | else |
---|
454 | Some ? (pi1 ?? final_policy). |
---|
455 | [ / by I/ |
---|
456 | | lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg |
---|
457 | @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] |
---|
458 | | @conj |
---|
459 | [ (* out_of_program_none *) |
---|
460 | #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2 |
---|
461 | cases (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
462 | cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi cases pi |
---|
463 | [1,7: #id cases id normalize nodelta |
---|
464 | [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: |
---|
465 | [1,2,3,6,7,24,25: #x #y |
---|
466 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_opt_insert_miss |
---|
467 | [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: |
---|
468 | @bitvector_of_nat_abs |
---|
469 | [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: |
---|
470 | @Hi2 |
---|
471 | |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: |
---|
472 | @(transitive_lt … Hi2) @le_S_to_le @Hi |
---|
473 | |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: |
---|
474 | @sym_neq @lt_to_not_eq @le_S_to_le @Hi |
---|
475 | ] |
---|
476 | ] |
---|
477 | @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi |
---|
478 | |38,39,40,41,42,43,44,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74: |
---|
479 | [1,2,3,6,7,24,25: #x #y |
---|
480 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] |
---|
481 | >lookup_opt_insert_miss |
---|
482 | [2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: |
---|
483 | @bitvector_of_nat_abs |
---|
484 | [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: |
---|
485 | @Hi2 |
---|
486 | |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: |
---|
487 | @(transitive_lt … Hi2) <Hi @le_n |
---|
488 | |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: |
---|
489 | @sym_neq @lt_to_not_eq <Hi @le_n |
---|
490 | ] |
---|
491 | ] |
---|
492 | <Hi @(proj1 ?? Hp (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?) |
---|
493 | >Hi @Hi2 |
---|
494 | |9,10,11,12,13,14,15,16,17: |
---|
495 | [1,2,6,7: #x |3,4,5,8,9: #x #id] >lookup_opt_insert_miss |
---|
496 | [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs |
---|
497 | [1,4,7,10,13,16,19,22,25: @Hi2 |
---|
498 | |2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) @le_S_to_le @Hi |
---|
499 | |3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq @le_S_to_le @Hi |
---|
500 | ] |
---|
501 | |1,3,5,7,9,11,13,15,17: |
---|
502 | @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi |
---|
503 | ] |
---|
504 | |46,47,48,49,50,51,52,53,54: |
---|
505 | [1,2,6,7: #x |3,4,5,8,9: #x #id] >lookup_opt_insert_miss |
---|
506 | [2,4,6,8,10,12,14,16,18: @bitvector_of_nat_abs |
---|
507 | [1,4,7,10,13,16,19,22,25: @Hi2 |
---|
508 | |2,5,8,11,14,17,20,23,26: @(transitive_lt … Hi2) <Hi @le_n |
---|
509 | |3,6,9,12,15,18,21,24,27: @sym_neq @lt_to_not_eq <Hi @le_n |
---|
510 | ] |
---|
511 | |1,3,5,7,9,11,13,15,17: |
---|
512 | @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n |
---|
513 | ] |
---|
514 | ] |
---|
515 | |2,3,6,8,9,12: [3,6: #w] #z >lookup_opt_insert_miss |
---|
516 | [2,4,6,8,10,12: @bitvector_of_nat_abs |
---|
517 | [1,4,7,10,13,16: @Hi2 |
---|
518 | |2,8,11: @(transitive_lt … Hi2) @le_S_to_le @Hi |
---|
519 | |5,14,17: @(transitive_lt … Hi2) <Hi @le_n |
---|
520 | |3,9,12: @sym_neq @lt_to_not_eq @le_S_to_le @Hi |
---|
521 | |6,15,18: <Hi @sym_neq @lt_to_not_eq @le_n |
---|
522 | ] |
---|
523 | ] |
---|
524 | [1,3,4: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi |
---|
525 | |2,5,6: |
---|
526 | <Hi @(proj1 ?? Hp (S (|prefix|)) (le_S ?? (le_n (|prefix|))) ?) |
---|
527 | >Hi @Hi2 |
---|
528 | ] |
---|
529 | |4,5,10,11: #dst normalize nodelta >lookup_opt_insert_miss |
---|
530 | [2,4,6,8: @bitvector_of_nat_abs |
---|
531 | [1,4,7,10: @Hi2 |
---|
532 | |2,5: @(transitive_lt … Hi2) @le_S_to_le @Hi |
---|
533 | |8,11: @(transitive_lt … Hi2) <Hi @le_n |
---|
534 | |3,6: @sym_neq @lt_to_not_eq @le_S_to_le @Hi |
---|
535 | |9,12: @sym_neq @lt_to_not_eq <Hi @le_n |
---|
536 | ] |
---|
537 | |1,3: @(proj1 ?? Hp i ? Hi2) @le_S_to_le @le_S_to_le @Hi |
---|
538 | |5,7: @(proj1 ?? Hp i ? Hi2) <Hi @le_S @le_n |
---|
539 | ] |
---|
540 | ] |
---|
541 | | (* jump_not_in_policy *) #i >append_length <commutative_plus |
---|
542 | #Hi normalize in Hi; cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
543 | [ cases p -p #p cases p -p #pc #sigma #Hp cases x #l #ins cases ins |
---|
544 | [ #pi cases pi normalize nodelta |
---|
545 | [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: |
---|
546 | [1,2,3,6,7,24,25: #x #y |
---|
547 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] >lookup_insert_miss |
---|
548 | [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: |
---|
549 | >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi) |
---|
550 | |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: |
---|
551 | @bitvector_of_nat_abs |
---|
552 | [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: |
---|
553 | @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus |
---|
554 | @le_plus_a @Hi |
---|
555 | |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: |
---|
556 | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S |
---|
557 | @le_plus_n_r |
---|
558 | |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: |
---|
559 | @lt_to_not_eq @Hi |
---|
560 | ] |
---|
561 | ] |
---|
562 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] >lookup_insert_miss |
---|
563 | [1,3,5,7,9,11,13,15,17: |
---|
564 | >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi) |
---|
565 | |2,4,6,8,10,12,14,16,18: |
---|
566 | @bitvector_of_nat_abs |
---|
567 | [1,4,7,10,13,16,19,22,25: |
---|
568 | @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus |
---|
569 | @le_plus_a @Hi |
---|
570 | |2,5,8,11,14,17,20,23,26: |
---|
571 | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S |
---|
572 | @le_plus_n_r |
---|
573 | |3,6,9,12,15,18,21,24,27: |
---|
574 | @lt_to_not_eq @Hi |
---|
575 | ] |
---|
576 | ] |
---|
577 | ] |
---|
578 | |2,3,4,5,6: #x [5: #y] >lookup_insert_miss |
---|
579 | [1,3,5,7,9: |
---|
580 | >(nth_append_first ? i prefix ?? Hi) @((proj2 ?? Hp) i Hi) |
---|
581 | |2,4,6,8,10: |
---|
582 | @bitvector_of_nat_abs |
---|
583 | [1,4,7,10,13: |
---|
584 | @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus |
---|
585 | @le_plus_a @Hi |
---|
586 | |2,5,8,11,14: |
---|
587 | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S |
---|
588 | @le_plus_n_r |
---|
589 | |3,6,9,12,15: |
---|
590 | @lt_to_not_eq @Hi |
---|
591 | ] |
---|
592 | ] |
---|
593 | ] |
---|
594 | | >Hi >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); |
---|
595 | cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #ins cases ins |
---|
596 | normalize nodelta |
---|
597 | [2,3,6: #x [3: #y] >lookup_insert_hit #_ / by / |
---|
598 | |4,5: #x #H @⊥ cases H #H2 @H2 / by I/ |
---|
599 | |1: #pi cases pi |
---|
600 | [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: |
---|
601 | [1,2,3,6,7,24,25: #x #y |
---|
602 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] |
---|
603 | #_ >lookup_insert_hit / by / |
---|
604 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] |
---|
605 | #H @⊥ cases H #H2 @H2 / by I/ |
---|
606 | ] |
---|
607 | ] |
---|
608 | ] |
---|
609 | ] |
---|
610 | | @conj |
---|
611 | [ #i #_ #Hi2 / by refl/ |
---|
612 | | #i #H @⊥ @(absurd … H) @not_le_Sn_O |
---|
613 | ] |
---|
614 | ] |
---|
615 | qed. |
---|
616 | |
---|
617 | definition policy_equal ≝ |
---|
618 | λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. |
---|
619 | (* \fst p1 = \fst p2 ∧ *) |
---|
620 | (∀n:ℕ.n < |program| → |
---|
621 | let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in |
---|
622 | let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in |
---|
623 | \snd pc1 = \snd pc2). |
---|
624 | |
---|
625 | (*definition nec_plus_ultra ≝ |
---|
626 | λprogram:list labelled_instruction.λp:ppc_pc_mapjump_expansion_policy. |
---|
627 | ¬(∀i.i < |program| → \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,0,short_jump〉) = long_jump). *) |
---|
628 | |
---|
629 | (*include alias "common/Identifiers.ma".*) |
---|
630 | include alias "ASM/BitVector.ma". |
---|
631 | include alias "basics/lists/list.ma". |
---|
632 | include alias "arithmetics/nat.ma". |
---|
633 | include alias "basics/logic.ma". |
---|
634 | |
---|
635 | lemma blerpque: ∀a,b,i. |
---|
636 | is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i → |
---|
637 | (max_length a b) = a. |
---|
638 | #a #b #i cases i |
---|
639 | [1: #pi cases pi |
---|
640 | [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: |
---|
641 | [1,2,3,6,7,24,25: #x #y |
---|
642 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] |
---|
643 | #H cases H |
---|
644 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] |
---|
645 | #_ cases a cases b |
---|
646 | [1,5,7,8,9: #_ / by refl/ |
---|
647 | |10,14,16,17,18: #_ / by refl/ |
---|
648 | |19,23,25,26,27: #_ / by refl/ |
---|
649 | |28,32,34,35,36: #_ / by refl/ |
---|
650 | |37,41,43,44,45: #_ / by refl/ |
---|
651 | |46,50,52,53,54: #_ / by refl/ |
---|
652 | |55,59,61,62,63: #_ / by refl/ |
---|
653 | |64,68,70,71,72: #_ / by refl/ |
---|
654 | |73,77,79,80,81: #_ / by refl/ |
---|
655 | |2,3,4,6: cases x #a cases a |
---|
656 | [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb |
---|
657 | |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb |
---|
658 | |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb |
---|
659 | |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb |
---|
660 | |5,6,7,10,11,12,13,14: #Hb cases Hb |
---|
661 | |24,25,26,29,30,31,32,33: #Hb cases Hb |
---|
662 | |43,44,45,48,49,50,51,52: #Hb cases Hb |
---|
663 | |62,63,64,67,68,69,70,71: #Hb cases Hb |
---|
664 | |15,34,53,72: #b #Hb #H normalize in H; destruct (H) |
---|
665 | ] |
---|
666 | |11,12,13,15: cases x #a cases a |
---|
667 | [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb |
---|
668 | |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb |
---|
669 | |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb |
---|
670 | |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb |
---|
671 | |5,6,7,10,11,12,13,14: #Hb cases Hb |
---|
672 | |24,25,26,29,30,31,32,33: #Hb cases Hb |
---|
673 | |43,44,45,48,49,50,51,52: #Hb cases Hb |
---|
674 | |62,63,64,67,68,69,70,71: #Hb cases Hb |
---|
675 | |15,34,53,72: #b #Hb #H normalize in H; destruct (H) |
---|
676 | ] |
---|
677 | |20,21,22,24: cases x #a cases a |
---|
678 | [1,2,3,4,8,9,16,17,18,19: #b #Hb cases Hb |
---|
679 | |20,21,22,23,27,28,35,36,37,38: #b #Hb cases Hb |
---|
680 | |39,40,41,42,46,47,54,55,56,57: #b #Hb cases Hb |
---|
681 | |58,59,60,61,65,66,73,74,75,76: #b #Hb cases Hb |
---|
682 | |5,6,7,10,11,12,13,14: #Hb cases Hb |
---|
683 | |24,25,26,29,30,31,32,33: #Hb cases Hb |
---|
684 | |43,44,45,48,49,50,51,52: #Hb cases Hb |
---|
685 | |62,63,64,67,68,69,70,71: #Hb cases Hb |
---|
686 | |15,34,53,72: #b #Hb #H normalize in H; destruct (H) |
---|
687 | ] |
---|
688 | |29,30,31,33: cases x #a cases a #a1 #a2 |
---|
689 | [1,3,5,7: cases a2 #b cases b |
---|
690 | [2,3,4,9,15,16,17,18,19: #b #Hb cases Hb |
---|
691 | |21,22,23,28,34,35,36,37,38: #b #Hb cases Hb |
---|
692 | |40,41,42,47,53,54,55,56,57: #b #Hb cases Hb |
---|
693 | |59,60,61,66,72,73,74,75,76: #b #Hb cases Hb |
---|
694 | |5,6,7,10,11,12,13,14: #Hb cases Hb |
---|
695 | |24,25,26,29,30,31,32,33: #Hb cases Hb |
---|
696 | |43,44,45,48,49,50,51,52: #Hb cases Hb |
---|
697 | |62,63,64,67,68,69,70,71: #Hb cases Hb |
---|
698 | |1,8: #b #Hb #H normalize in H; destruct (H) |
---|
699 | |20,27: #b #Hb #H normalize in H; destruct (H) |
---|
700 | |39,46: #b #Hb #H normalize in H; destruct (H) |
---|
701 | |58,65: #b #Hb #H normalize in H; destruct (H) |
---|
702 | ] |
---|
703 | |2,4,6,8: cases a1 #b cases b |
---|
704 | [1,3,8,9,15,16,17,18,19: #b #Hb cases Hb |
---|
705 | |20,22,27,28,34,35,36,37,38: #b #Hb cases Hb |
---|
706 | |39,41,46,47,53,54,55,56,57: #b #Hb cases Hb |
---|
707 | |58,60,65,66,72,73,74,75,76: #b #Hb cases Hb |
---|
708 | |5,6,7,10,11,12,13,14: #Hb cases Hb |
---|
709 | |24,25,26,29,30,31,32,33: #Hb cases Hb |
---|
710 | |43,44,45,48,49,50,51,52: #Hb cases Hb |
---|
711 | |62,63,64,67,68,69,70,71: #Hb cases Hb |
---|
712 | |2,4: #b #Hb #H normalize in H; destruct (H) |
---|
713 | |21,23: #b #Hb #H normalize in H; destruct (H) |
---|
714 | |40,42: #b #Hb #H normalize in H; destruct (H) |
---|
715 | |59,61: #b #Hb #H normalize in H; destruct (H) |
---|
716 | ] |
---|
717 | ] |
---|
718 | |38,39,40,42: cases x #a cases a |
---|
719 | [2,3,8,9,15,16,17,18,19: #b #Hb cases Hb |
---|
720 | |21,22,27,28,34,35,36,37,38: #b #Hb cases Hb |
---|
721 | |40,41,46,47,53,54,55,56,57: #b #Hb cases Hb |
---|
722 | |59,60,65,66,72,73,74,75,76: #b #Hb cases Hb |
---|
723 | |5,6,7,10,11,12,13,14: #Hb cases Hb |
---|
724 | |24,25,26,29,30,31,32,33: #Hb cases Hb |
---|
725 | |43,44,45,48,49,50,51,52: #Hb cases Hb |
---|
726 | |62,63,64,67,68,69,70,71: #Hb cases Hb |
---|
727 | |1,4: #b #Hb #H normalize in H; destruct (H) |
---|
728 | |20,23: #b #Hb #H normalize in H; destruct (H) |
---|
729 | |39,42: #b #Hb #H normalize in H; destruct (H) |
---|
730 | |58,61: #b #Hb #H normalize in H; destruct (H) |
---|
731 | ] |
---|
732 | |47,48,49,51: cases x #a #H normalize in H; destruct (H) |
---|
733 | |56,57,58,60: cases x #a #H normalize in H; destruct (H) |
---|
734 | |65,66,67,69: cases x #a #H normalize in H; destruct (H) |
---|
735 | |74,75,76,78: cases x #a #H normalize in H; destruct (H) |
---|
736 | ] |
---|
737 | ] |
---|
738 | |2,3,6: #x [3: #y] #H cases H |
---|
739 | |4,5: #id #_ cases a cases b |
---|
740 | [2,3,4,6,11,12,13,15: normalize #H destruct (H) |
---|
741 | |1,5,7,8,9,10,14,16,17,18: #H / by refl/ |
---|
742 | ] |
---|
743 | ] |
---|
744 | qed. |
---|
745 | |
---|
746 | lemma etblorp: ∀a,b,i.is_jump i → |
---|
747 | instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i. |
---|
748 | #a #b #i cases i |
---|
749 | [2,3,6: #x [3: #y] #H cases H |
---|
750 | |4,5: #id #_ cases a cases b / by le_n/ |
---|
751 | |1: #pi cases pi |
---|
752 | [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: |
---|
753 | [1,2,3,6,7,24,25: #x #y |
---|
754 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] |
---|
755 | #H cases H |
---|
756 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] |
---|
757 | #_ cases a cases b |
---|
758 | [2,3: cases x #ad cases ad |
---|
759 | [15,34: #b #Hb / by le_n/ |
---|
760 | |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb |
---|
761 | |1,4,5,6,7,8,9: / by le_n/ |
---|
762 | |11,12: cases x #ad cases ad |
---|
763 | [15,34: #b #Hb / by le_n/ |
---|
764 | |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb |
---|
765 | |10,13,14,15,16,17,18: / by le_n/ |
---|
766 | |20,21: cases x #ad cases ad |
---|
767 | [15,34: #b #Hb / by le_n/ |
---|
768 | |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb |
---|
769 | |19,22,23,24,25,26,27: / by le_n/ |
---|
770 | |29,30: cases x #ad cases ad #a1 #a2 |
---|
771 | [1,3: cases a2 #ad2 cases ad2 |
---|
772 | [1,8,20,27: #b #Hb normalize @le_S @le_S @le_S @le_S @le_S @le_n (* auto inexplicably takes a long time here *) |
---|
773 | |2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb |
---|
774 | |2,4: cases a1 #ad1 cases ad1 |
---|
775 | [2,4,21,23: #b #Hb normalize @le_S @le_S @le_S @le_S @le_S @le_n |
---|
776 | |1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb |
---|
777 | ] |
---|
778 | |28,31,32,33,34,35,36: / by le_n/ |
---|
779 | |38,39: cases x #ad cases ad |
---|
780 | [1,4,20,23: #b #Hb / by le_n/ |
---|
781 | |2,3,8,9,15,16,17,18,19,21,22,27,28,34,35,36,37,38: #b] #Hb cases Hb |
---|
782 | |37,40,41,42,43,44,45: / by le_n/ |
---|
783 | |46,47,48,49,50,51,52,53,54: / by le_n/ |
---|
784 | |55,56,57,58,59,60,61,62,63: / by le_n/ |
---|
785 | |64,65,66,67,68,69,70,71,72: / by le_n/ |
---|
786 | |73,74,75,76,77,78,79,80,81: / by le_n/ |
---|
787 | ] |
---|
788 | ] |
---|
789 | ] |
---|
790 | qed. |
---|
791 | |
---|
792 | lemma minus_zero_to_le: ∀n,m:ℕ.n - m = 0 → n ≤ m. |
---|
793 | #n |
---|
794 | elim n |
---|
795 | [ #m #_ @le_O_n |
---|
796 | | #n' #Hind #m cases m |
---|
797 | [ #H -n whd in match (minus ??) in H; >H @le_n |
---|
798 | | #m' -m #H whd in match (minus ??) in H; @le_S_S @Hind @H |
---|
799 | ] |
---|
800 | ] |
---|
801 | qed. |
---|
802 | |
---|
803 | lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0. |
---|
804 | #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r |
---|
805 | qed. |
---|
806 | |
---|
807 | (* One step in the search for a jump expansion fixpoint. *) |
---|
808 | definition jump_expansion_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16). |
---|
809 | ∀labels:(Σlm:label_map. ∀i:ℕ.lt i (|program|) → |
---|
810 | ∀l.occurs_exactly_once ?? l program → |
---|
811 | is_label (nth i ? program 〈None ?, Comment [ ]〉) l → |
---|
812 | lookup … lm l = Some ? i). |
---|
813 | ∀old_policy:(Σpolicy:ppc_pc_map. |
---|
814 | And (And (out_of_program_none program policy) |
---|
815 | (jump_not_in_policy program policy)) |
---|
816 | (\fst policy < 2^16)). |
---|
817 | (Σx:bool × (option ppc_pc_map). |
---|
818 | let 〈no_ch,y〉 ≝ x in |
---|
819 | match y with |
---|
820 | [ None ⇒ (* nec_plus_ultra program old_policy *) True |
---|
821 | | Some p ⇒ And (And (And (And (And (out_of_program_none program p) |
---|
822 | (jump_not_in_policy program p)) |
---|
823 | (policy_increase program old_policy p)) |
---|
824 | (policy_compact program labels p)) |
---|
825 | (no_ch = true → policy_equal program old_policy p)) |
---|
826 | (\fst p < 2^16) |
---|
827 | ]) |
---|
828 | ≝ |
---|
829 | λprogram.λlabels.λold_sigma. |
---|
830 | let 〈final_added, final_policy〉 ≝ |
---|
831 | foldl_strong (option Identifier × pseudo_instruction) |
---|
832 | (λprefix.Σx:ℕ × ppc_pc_map. |
---|
833 | let 〈added,policy〉 ≝ x in |
---|
834 | And (And (And (And (out_of_program_none prefix policy) |
---|
835 | (jump_not_in_policy prefix policy)) |
---|
836 | (policy_increase prefix old_sigma policy)) |
---|
837 | (policy_compact prefix labels policy)) |
---|
838 | (added = 0 → policy_equal prefix old_sigma policy)) |
---|
839 | program |
---|
840 | (λprefix.λx.λtl.λprf.λacc. |
---|
841 | let 〈inc_added, inc_pc_sigma〉 ≝ (pi1 ?? acc) in |
---|
842 | let 〈label,instr〉 ≝ x in |
---|
843 | (* Now, we must add the current ppc and its pc translation. |
---|
844 | * Three possibilities: |
---|
845 | * - Instruction is not a jump; i.e. constant size whatever the sigma we use; |
---|
846 | * - Instruction is a backward jump; we can use the sigma we're constructing, |
---|
847 | * since it will already know the translation of its destination; |
---|
848 | * - Instruction is a forward jump; we must use the old sigma (the new sigma |
---|
849 | * does not know the translation yet), but compensate for the jumps we |
---|
850 | * have lengthened. |
---|
851 | *) |
---|
852 | let add_instr ≝ match instr with |
---|
853 | [ Jmp j ⇒ Some ? (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j) |
---|
854 | | Call c ⇒ Some ? (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) |
---|
855 | | Instruction i ⇒ jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added (|prefix|) i |
---|
856 | | _ ⇒ None ? |
---|
857 | ] in |
---|
858 | let 〈inc_pc, inc_sigma〉 ≝ inc_pc_sigma in |
---|
859 | let 〈old_pc,old_length〉 ≝ bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉 in |
---|
860 | let old_size ≝ instruction_size_jmplen old_length instr in |
---|
861 | let 〈new_length, isize〉 ≝ match add_instr with |
---|
862 | [ None ⇒ 〈short_jump, instruction_size_jmplen short_jump instr〉 |
---|
863 | | Some pl ⇒ 〈max_length old_length pl, instruction_size_jmplen (max_length old_length pl) instr〉 |
---|
864 | ] in |
---|
865 | let new_added ≝ match add_instr with |
---|
866 | [ None ⇒ inc_added |
---|
867 | | Some x ⇒ plus inc_added (minus isize old_size) |
---|
868 | ] in |
---|
869 | 〈new_added, 〈plus inc_pc isize, bvt_insert … (bitvector_of_nat ? (|prefix|)) 〈inc_pc, new_length〉 inc_sigma〉〉 |
---|
870 | ) 〈0, 〈0, Stub ??〉〉 in |
---|
871 | if geb (\fst final_policy) 2^16 then |
---|
872 | 〈eqb final_added 0, None ?〉 |
---|
873 | else |
---|
874 | 〈eqb final_added 0, Some ? final_policy〉. |
---|
875 | [ / by I/ |
---|
876 | | normalize nodelta lapply p generalize in match (foldl_strong ?????); * #x #H #H2 |
---|
877 | >H2 in H; normalize nodelta -H2 -x #H @conj |
---|
878 | [ @conj |
---|
879 | [ @(proj1 ?? H) |
---|
880 | | #H2 @(proj2 ?? H) @eqb_true_to_eq @H2 |
---|
881 | ] |
---|
882 | | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @p1 |
---|
883 | ] |
---|
884 | | lapply (pi2 ?? acc) >p cases inc_pc_sigma #inc_pc #inc_sigma |
---|
885 | lapply (refl ? (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉)) |
---|
886 | cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) in ⊢ (???% → %); |
---|
887 | #old_pc #old_length #Holdeq #Hpolicy @pair_elim #added #policy normalize nodelta |
---|
888 | @pair_elim #new_length #isize normalize nodelta #Heq1 #Heq2 |
---|
889 | @conj [ @conj [ @conj [ @conj |
---|
890 | [ (* out_of_program_none *) #i >append_length <commutative_plus #Hi normalize in Hi; #Hi2 |
---|
891 | cases instr in Heq2; normalize nodelta |
---|
892 | #x [6: #y] #H <(proj2 ?? (pair_destruct ?????? H)) >lookup_opt_insert_miss |
---|
893 | [1,3,5,7,9,11: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i ? Hi2) |
---|
894 | @le_S_to_le @Hi |
---|
895 | |2,4,6,8,10,12: @bitvector_of_nat_abs |
---|
896 | [1,4,7,10,13,16: @Hi2 |
---|
897 | |2,5,8,11,14,17: @(transitive_lt … Hi2) @Hi |
---|
898 | |3,6,9,12,15,18: @sym_neq @lt_to_not_eq @Hi |
---|
899 | ] |
---|
900 | ] |
---|
901 | | (* jump_not_in_policy *) #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
902 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
903 | [ <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss |
---|
904 | [ >(nth_append_first ? i prefix ?? Hi) |
---|
905 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i Hi) |
---|
906 | | @bitvector_of_nat_abs |
---|
907 | [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus |
---|
908 | @le_plus_a @Hi |
---|
909 | | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S |
---|
910 | @le_plus_n_r |
---|
911 | | @lt_to_not_eq @Hi |
---|
912 | ] |
---|
913 | ] |
---|
914 | | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_hit |
---|
915 | >nth_append_second |
---|
916 | [ <minus_n_n whd in match (nth ????); cases instr in Heq1; |
---|
917 | [4,5: #x #_ #H cases H #H2 @⊥ @H2 / by I/ |
---|
918 | |2,3,6: #x [3: #y] #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by / |
---|
919 | |1: #pi cases pi |
---|
920 | [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: |
---|
921 | [1,2,3,6,7,24,25: #x #y |
---|
922 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #Heq1 |
---|
923 | <(proj1 ?? (pair_destruct ?????? Heq1)) #_ / by / |
---|
924 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] |
---|
925 | #_ #H @⊥ cases H #H2 @H2 / by I/ |
---|
926 | ] |
---|
927 | ] |
---|
928 | | @le_n |
---|
929 | ] |
---|
930 | ] |
---|
931 | ] |
---|
932 | | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
933 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi; #Hi |
---|
934 | [ lapply (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy)) i Hi) |
---|
935 | <(proj2 ?? (pair_destruct ?????? Heq2)) |
---|
936 | @pair_elim #opc #oj #EQ1 >lookup_insert_miss |
---|
937 | [ @pair_elim #pc #j #EQ2 / by / |
---|
938 | | @bitvector_of_nat_abs |
---|
939 | [ @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus @le_plus_a |
---|
940 | @Hi |
---|
941 | | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r |
---|
942 | | @lt_to_not_eq @Hi |
---|
943 | ] |
---|
944 | ] |
---|
945 | | >Hi <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_hit |
---|
946 | cases (dec_is_jump instr) |
---|
947 | [ cases instr in Heq1; normalize nodelta |
---|
948 | [ #pi cases pi |
---|
949 | [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: |
---|
950 | [1,2,3,6,7,24,25: #x #y |
---|
951 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] #_ #Hj cases Hj |
---|
952 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] |
---|
953 | whd in match jump_expansion_step_instruction; normalize nodelta #Heq1 |
---|
954 | <(proj1 ?? (pair_destruct ?????? Heq1)) #_ >Holdeq normalize nodelta |
---|
955 | @jmpleq_max_length |
---|
956 | ] |
---|
957 | |2,3,6: #x [3: #y] #_ #Hj cases Hj |
---|
958 | |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) >Holdeq normalize nodelta |
---|
959 | @jmpleq_max_length |
---|
960 | ] |
---|
961 | | lapply Heq1 -Heq1; lapply (refl ? instr); cases instr in ⊢ (???% → %); normalize nodelta |
---|
962 | [ #pi cases pi |
---|
963 | [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: |
---|
964 | [1,2,3,6,7,24,25: #x #y |
---|
965 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] |
---|
966 | whd in match jump_expansion_step_instruction; normalize nodelta #Heqi #Heq1 |
---|
967 | #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) |
---|
968 | lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??) |
---|
969 | [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: |
---|
970 | >prf >nth_append_second |
---|
971 | [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: |
---|
972 | <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj |
---|
973 | |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: |
---|
974 | @le_n |
---|
975 | ] |
---|
976 | |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: |
---|
977 | >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r |
---|
978 | |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: |
---|
979 | cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) |
---|
980 | #a #b #H >H normalize nodelta %2 @refl |
---|
981 | ] |
---|
982 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] |
---|
983 | #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/ |
---|
984 | ] |
---|
985 | |2,3,6: #x [3: #y] #Heqi #Heq1 #Hj <(proj1 ?? (pair_destruct ?????? Heq1)) |
---|
986 | lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??) |
---|
987 | [1,4,7: >prf >nth_append_second |
---|
988 | [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Heqi @Hj |
---|
989 | |2,4,6: @le_n |
---|
990 | ] |
---|
991 | |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r |
---|
992 | |3,6,9: cases (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) |
---|
993 | #a #b #H >H normalize nodelta %2 @refl |
---|
994 | ] |
---|
995 | |4,5: #x #_ #_ #abs cases abs #ABS @⊥ @ABS / by I/ |
---|
996 | ] |
---|
997 | ] |
---|
998 | ] |
---|
999 | ] |
---|
1000 | | (* policy_compact *) (*XXX*) cases daemon |
---|
1001 | ] |
---|
1002 | | (* added = 0 → policy_equal *) lapply (proj2 ?? Hpolicy) |
---|
1003 | lapply Heq2 -Heq2 lapply Heq1 -Heq1 lapply (refl ? instr) |
---|
1004 | cases instr in ⊢ (???% → % → % → %); normalize nodelta |
---|
1005 | [ #pi cases pi normalize nodelta |
---|
1006 | [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: |
---|
1007 | [1,2,3,6,7,24,25: #x #y |
---|
1008 | |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] |
---|
1009 | #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) #Hadded |
---|
1010 | #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
1011 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
1012 | [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: |
---|
1013 | <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss |
---|
1014 | [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: |
---|
1015 | @(Hold Hadded i Hi) |
---|
1016 | |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: |
---|
1017 | @bitvector_of_nat_abs |
---|
1018 | [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: |
---|
1019 | @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus |
---|
1020 | @le_plus_a @Hi |
---|
1021 | |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: |
---|
1022 | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S |
---|
1023 | @le_plus_n_r |
---|
1024 | |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: |
---|
1025 | @lt_to_not_eq @Hi |
---|
1026 | ] |
---|
1027 | ] |
---|
1028 | |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: |
---|
1029 | <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit |
---|
1030 | lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??) |
---|
1031 | [1,4,7,10,13,16,19,22,25,28,31,34,37,40,43,46,49,52,55,58,61,64,67,70,73,76,79,82: |
---|
1032 | >prf >nth_append_second |
---|
1033 | [1,3,5,7,9,11,13,15,17,19,21,23,25,27,29,31,33,35,37,39,41,43,45,47,49,51,53,55: |
---|
1034 | <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H |
---|
1035 | |2,4,6,8,10,12,14,16,18,20,22,24,26,28,30,32,34,36,38,40,42,44,46,48,50,52,54,56: |
---|
1036 | @le_n |
---|
1037 | ] |
---|
1038 | |2,5,8,11,14,17,20,23,26,29,32,35,38,41,44,47,50,53,56,59,62,65,68,71,74,77,80,83: |
---|
1039 | >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r |
---|
1040 | |3,6,9,12,15,18,21,24,27,30,33,36,39,42,45,48,51,54,57,60,63,66,69,72,75,78,81,84: |
---|
1041 | cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) |
---|
1042 | #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl |
---|
1043 | ] |
---|
1044 | ] |
---|
1045 | |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #Hins #Heq1 #Heq2 #Hold |
---|
1046 | <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1)) |
---|
1047 | #H #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
1048 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
1049 | [1,3,5,7,9,11,13,15,17: <(proj2 ?? (pair_destruct ?????? Heq2)) |
---|
1050 | >lookup_insert_miss |
---|
1051 | [1,3,5,7,9,11,13,15,17: @(Hold ? i Hi) |
---|
1052 | [1,2,3,4,5,6,7,8,9: @sym_eq @le_n_O_to_eq <H @le_plus_n_r] |
---|
1053 | ] |
---|
1054 | @bitvector_of_nat_abs |
---|
1055 | [1,4,7,10,13,16,19,22,25: @(transitive_lt … (pi2 ?? program)) >prf |
---|
1056 | >append_length >commutative_plus @le_plus_a @Hi |
---|
1057 | |2,5,8,11,14,17,20,23,26: @(transitive_lt … (pi2 ?? program)) >prf |
---|
1058 | >append_length <plus_n_Sm @le_S_S |
---|
1059 | |3,6,9,12,15,18,21,24,27: @lt_to_not_eq @Hi |
---|
1060 | ] @le_plus_n_r |
---|
1061 | |2,4,6,8,10,12,14,16,18: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi |
---|
1062 | >lookup_insert_hit <(proj1 ?? (pair_destruct ?????? Heq1)) |
---|
1063 | >Holdeq normalize nodelta @sym_eq @blerpque |
---|
1064 | [3,6,9,12,15,18,21,24,27: |
---|
1065 | elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H))) |
---|
1066 | [1,3,5,7,9,11,13,15,17: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp |
---|
1067 | |2,4,6,8,10,12,14,16,18: #H @H |
---|
1068 | ] |
---|
1069 | / by I/ |
---|
1070 | |2,5,8,11,14,17,20,23,26: / by I/ |
---|
1071 | ] |
---|
1072 | ] |
---|
1073 | ] |
---|
1074 | |2,3,6: #x [3: #y] #Hins #Heq1 #Heq2 #Hold <(proj1 ?? (pair_destruct ?????? Heq2)) |
---|
1075 | #Hadded #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
1076 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
1077 | [1,3,5: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss |
---|
1078 | [1,3,5: @(Hold Hadded i Hi) |
---|
1079 | |2,4,6: @bitvector_of_nat_abs |
---|
1080 | [1,4,7: @(transitive_lt … (pi2 ?? program)) >prf >append_length >commutative_plus |
---|
1081 | @le_plus_a @Hi |
---|
1082 | |2,5,8: @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S |
---|
1083 | @le_plus_n_r |
---|
1084 | |3,6,9: @lt_to_not_eq @Hi |
---|
1085 | ] |
---|
1086 | ] |
---|
1087 | |2,4,6: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit |
---|
1088 | lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ??) |
---|
1089 | [1,4,7: >prf >nth_append_second |
---|
1090 | [1,3,5: <minus_n_n whd in match (nth ????); >p1 >Hins @nmk #H @H |
---|
1091 | |2,4,6: @le_n |
---|
1092 | ] |
---|
1093 | |2,5,8: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r |
---|
1094 | |3,6,9: cases (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma) 〈0,short_jump〉) |
---|
1095 | #a #b #H >H <(proj1 ?? (pair_destruct ?????? Heq1)) normalize nodelta @refl |
---|
1096 | ] |
---|
1097 | ] |
---|
1098 | |4,5: #x #Hins #Heq1 #Heq2 #Hold |
---|
1099 | <(proj1 ?? (pair_destruct ?????? Heq2)) <(proj2 ?? (pair_destruct ?????? Heq1)) |
---|
1100 | #H #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
1101 | cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi |
---|
1102 | [1,3: <(proj2 ?? (pair_destruct ?????? Heq2)) >lookup_insert_miss |
---|
1103 | [1,3: @(Hold ? i Hi) |
---|
1104 | [1,2: @sym_eq @le_n_O_to_eq <H @le_plus_n_r] |
---|
1105 | ] |
---|
1106 | @bitvector_of_nat_abs |
---|
1107 | [1,4: @(transitive_lt … (pi2 ?? program)) >prf |
---|
1108 | >append_length >commutative_plus @le_plus_a @Hi |
---|
1109 | |2,5: @(transitive_lt … (pi2 ?? program)) >prf |
---|
1110 | >append_length <plus_n_Sm @le_S_S |
---|
1111 | |3,6: @lt_to_not_eq @Hi |
---|
1112 | ] @le_plus_n_r |
---|
1113 | |2,4: <(proj2 ?? (pair_destruct ?????? Heq2)) >Hi >lookup_insert_hit |
---|
1114 | <(proj1 ?? (pair_destruct ?????? Heq1))>Holdeq normalize nodelta |
---|
1115 | @sym_eq @blerpque |
---|
1116 | [3,6: elim (le_to_or_lt_eq … (minus_zero_to_le … (plus_zero_zero … H))) |
---|
1117 | [1,3: #H @⊥ @(absurd ? H) @le_to_not_lt @etblorp |
---|
1118 | |2,4: #H @H |
---|
1119 | ] |
---|
1120 | / by I/ |
---|
1121 | |2,5: / by I/ |
---|
1122 | ] |
---|
1123 | ] |
---|
1124 | ] |
---|
1125 | ] |
---|
1126 | | normalize nodelta @conj [ @conj [ @conj [ @conj |
---|
1127 | [ #i #Hi / by refl/ |
---|
1128 | | / by refl/ |
---|
1129 | ]]]] |
---|
1130 | [3: #_] |
---|
1131 | #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O |
---|
1132 | ] |
---|
1133 | qed. |
---|
1134 | |
---|
1135 | |
---|
1136 | (* old proof | lapply (pi2 ?? acc) >p #Hpolicy normalize nodelta in Hpolicy; |
---|
1137 | cases (dec_eq_jump_length new_length old_length) #Hlength normalize nodelta |
---|
1138 | @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj [1,3: @conj |
---|
1139 | [1,3: (* out_of_policy_none *) |
---|
1140 | #i >append_length <commutative_plus #Hi normalize in Hi; |
---|
1141 | #Hi2 >lookup_opt_insert_miss |
---|
1142 | [1,3: @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le … Hi)) @Hi2 |
---|
1143 | |2,4: >eq_bv_sym @bitvector_of_nat_abs |
---|
1144 | [1,4: @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
1145 | @le_S_S @le_plus_n_r |
---|
1146 | |2,5: @Hi2 |
---|
1147 | |3,6: @lt_to_not_eq @Hi |
---|
1148 | ] |
---|
1149 | ] |
---|
1150 | |2,4: (* labels_okay *) |
---|
1151 | @lookup_forall #i cases i -i #i cases i -i #p #a #j #n #Hl |
---|
1152 | elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl |
---|
1153 | [1,3: elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? n Hl) |
---|
1154 | #i #Hi @(ex_intro ?? i Hi) |
---|
1155 | |2,4: normalize nodelta normalize nodelta in p2; cases instr in p2; |
---|
1156 | [2,3,8,9: #x #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
1157 | |6,12: #x #y #abs normalize nodelta in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
1158 | |1,7: #pi cases pi |
---|
1159 | [35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
1160 | |1,2,3,6,7,33,34,38,39,40,43,44,70,71: |
---|
1161 | #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
1162 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: |
---|
1163 | #x #abs normalize in abs;lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
1164 | |9,10,14,15,46,47,51,52: |
---|
1165 | #id normalize nodelta whd in match (jump_expansion_step_instruction ???); |
---|
1166 | whd in match (select_reljump_length ???); >p3 |
---|
1167 | lapply (refl ? (lookup_def ?? (pi1 ?? labels) id 〈0,\fst pol〉)) |
---|
1168 | cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2 |
---|
1169 | normalize nodelta #H |
---|
1170 | >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
1171 | >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) |
---|
1172 | cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 |
---|
1173 | [1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %); |
---|
1174 | |2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %); |
---|
1175 | ] |
---|
1176 | #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H |
---|
1177 | <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl |
---|
1178 | |11,12,13,16,17,48,49,50,53,54: |
---|
1179 | #x #id normalize nodelta whd in match (jump_expansion_step_instruction ???); |
---|
1180 | whd in match (select_reljump_length ???); >p3 |
---|
1181 | lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉)) |
---|
1182 | cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2 |
---|
1183 | normalize nodelta #H |
---|
1184 | >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
1185 | >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) |
---|
1186 | cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 |
---|
1187 | [1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %); |
---|
1188 | |2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %); |
---|
1189 | ] |
---|
1190 | #Hle2 normalize nodelta #Hli @(ex_intro ?? id) >H |
---|
1191 | <(pair_eq1 ?????? (Some_eq ??? Hli)) @refl |
---|
1192 | ] |
---|
1193 | |4,5,10,11: #id normalize nodelta whd in match (select_jump_length ???); |
---|
1194 | whd in match (select_call_length ???); >p3 |
---|
1195 | lapply (refl ? (lookup_def ?? labels id 〈0,\fst pol〉)) |
---|
1196 | cases (lookup_def ?? labels id 〈0,\fst pol〉) in ⊢ (???% → %); #q1 #q2 |
---|
1197 | normalize nodelta #H |
---|
1198 | [1,3: cases (leb (\fst pol) q2) |
---|
1199 | [1,3: cases (leb (q2-\fst pol) 126) |2,4: cases (leb (\fst pol-q2) 129) ] |
---|
1200 | [1,3,5,7: normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; |
---|
1201 | #Hli @(ex_intro ?? id) lapply (proj2 ?? Hl) |
---|
1202 | #H >(pair_eq1 ?????? (pair_eq1 ?????? H)) |
---|
1203 | >(pair_eq2 ?????? (pair_eq1 ?????? H)) >Hli @refl] |
---|
1204 | ] |
---|
1205 | cases (split ? 5 11 (bitvector_of_nat 16 q2)) #n1 #n2 |
---|
1206 | cases (split ? 5 11 (bitvector_of_nat 16 (\fst pol))) #m1 #m2 |
---|
1207 | normalize nodelta cases (eq_bv ? n1 m1) |
---|
1208 | normalize nodelta #H2 >(pair_eq1 ?????? (Some_eq ??? H2)) in H; #H |
---|
1209 | @(ex_intro ?? id) lapply (proj2 ?? Hl) #H2 |
---|
1210 | >(pair_eq1 ?????? (pair_eq1 ?????? H2)) >(pair_eq2 ?????? (pair_eq1 ?????? H2)) |
---|
1211 | >H @refl |
---|
1212 | ] |
---|
1213 | ] |
---|
1214 | ] |
---|
1215 | |2,4: (* jump_in_policy *) |
---|
1216 | #i #Hi cases (le_to_or_lt_eq … Hi) -Hi; |
---|
1217 | [1,3: >append_length <commutative_plus #Hi normalize in Hi; |
---|
1218 | >(nth_append_first ?? prefix ??(le_S_S_to_le ?? Hi)) @conj |
---|
1219 | [1,3: #Hj lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi)) |
---|
1220 | #Hacc elim (proj1 ?? Hacc Hj) #h #n elim n -n #n #H elim H -H #j #Hj |
---|
1221 | @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) whd in match (snd ???); |
---|
1222 | >lookup_opt_insert_miss [1,3: @Hj |2,4: @bitvector_of_nat_abs ] |
---|
1223 | [3,6: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi) |
---|
1224 | |1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) |
---|
1225 | ] |
---|
1226 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
1227 | @le_S_S @le_plus_n_r |
---|
1228 | |2,4: lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le … Hi)) |
---|
1229 | #Hacc #H elim H -H; #h #H elim H -H; #n #H elim H -H #j #Hl |
---|
1230 | @(proj2 ?? Hacc) @(ex_intro ?? h (ex_intro ?? n (ex_intro ?? j ?))) |
---|
1231 | <Hl @sym_eq @lookup_opt_insert_miss @bitvector_of_nat_abs |
---|
1232 | [3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) |
---|
1233 | |1,4: @(transitive_lt ??? (le_S_S_to_le ?? Hi)) |
---|
1234 | ] |
---|
1235 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
1236 | @le_S_S @le_plus_n_r |
---|
1237 | ] |
---|
1238 | |2,4: >append_length <commutative_plus #Hi normalize in Hi; >(injective_S … Hi) |
---|
1239 | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) |
---|
1240 | <minus_n_n whd in match (nth ????); normalize nodelta in p2; cases instr in p2; |
---|
1241 | [1,7: #pi | 2,3,8,9: #x | 4,5,10,11: #id | 6,12: #x #y] #Hinstr @conj normalize nodelta |
---|
1242 | [5,7,9,11,21,23: #H @⊥ @H (* instr is not a jump *) |
---|
1243 | |6,8,10,12,22,24: normalize nodelta in Hinstr; lapply (jmeq_to_eq ??? Hinstr) |
---|
1244 | #H destruct (H) |
---|
1245 | |13,15,17,19: (* instr is a jump *) #_ @(ex_intro ?? (\fst pol)) |
---|
1246 | @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) |
---|
1247 | @lookup_opt_insert_hit |
---|
1248 | |14,16,18,20: #_ / by I/ |
---|
1249 | |1,2,3,4: cases pi in Hinstr; |
---|
1250 | [35,36,37,109,110,111: #Hinstr #H @⊥ @H |
---|
1251 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,78,79,82,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106: |
---|
1252 | #x #Hinstr #H @⊥ @H |
---|
1253 | |1,2,3,6,7,33,34,75,76,77,80,81,107,108: #x #y #Hinstr #H @⊥ @H |
---|
1254 | |9,10,14,15,83,84,88,89: #id #Hinstr #_ |
---|
1255 | @(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) |
---|
1256 | @lookup_opt_insert_hit |
---|
1257 | |11,12,13,16,17,85,86,87,90,91: #x #id #Hinstr #_ |
---|
1258 | @(ex_intro ?? (\fst pol)) @(ex_intro ?? addr) @(ex_intro ?? (max_length old_length ai)) |
---|
1259 | @lookup_opt_insert_hit |
---|
1260 | |72,73,74,146,147,148: #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H) |
---|
1261 | |41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,115,116,119,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143: |
---|
1262 | #x #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H normalize in H; destruct (H) |
---|
1263 | |38,39,40,43,44,70,71,112,113,114,117,118,144,145: #x #y #Hinstr lapply (jmeq_to_eq ??? Hinstr) #H |
---|
1264 | normalize in H; destruct (H) |
---|
1265 | |46,47,51,52,120,121,125,126: #id #Hinstr #_ / by I/ |
---|
1266 | |48,49,50,53,54,122,123,124,127,128: #x #id #Hinstr #_ / by I/ |
---|
1267 | ] |
---|
1268 | ] |
---|
1269 | ] |
---|
1270 | ] |
---|
1271 | |2,4: (* policy increase *) |
---|
1272 | #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
1273 | cases (le_to_or_lt_eq … Hi) -Hi; #Hi |
---|
1274 | [1,3: >lookup_insert_miss |
---|
1275 | [1,3: @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) |
---|
1276 | |2,4: @bitvector_of_nat_abs |
---|
1277 | [3,6: @lt_to_not_eq @(le_S_S_to_le … Hi) |
---|
1278 | |1,4: @(transitive_lt ??? (le_S_S_to_le … Hi)) |
---|
1279 | ] |
---|
1280 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
1281 | @le_S_S @le_plus_n_r |
---|
1282 | ] |
---|
1283 | |2: >(injective_S … Hi) normalize nodelta in Hlength; >lookup_insert_hit normalize nodelta |
---|
1284 | >Hlength @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy |
---|
1285 | >Hl %2 @refl |
---|
1286 | |4: cases daemon (* XXX get rest of proof done first *) |
---|
1287 | ] |
---|
1288 | ] |
---|
1289 | |2,4: (* policy_safe *) |
---|
1290 | @lookup_forall #x cases x -x #x cases x -x #p #a #j #n normalize nodelta #Hl |
---|
1291 | elim (insert_lookup_opt ?? 〈p,a,j〉 ???? Hl) -Hl #Hl |
---|
1292 | [1,3: @(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl) |
---|
1293 | |2,4: normalize nodelta in p2; cases instr in p2; |
---|
1294 | [2,3,8,9: #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
1295 | |6,12: #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
1296 | |1,7: #pi cases pi normalize nodelta |
---|
1297 | [35,36,37,72,73,74: #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
1298 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,41,42,45,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69: |
---|
1299 | #x #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
1300 | |1,2,3,6,7,33,34,38,39,40,43,44,70,71: |
---|
1301 | #x #y #abs normalize in abs; lapply (jmeq_to_eq ??? abs) #H destruct (H) |
---|
1302 | |9,10,14,15,46,47,51,52: #id >p3 whd in match (jump_expansion_step_instruction ???); |
---|
1303 | whd in match (select_reljump_length ???); |
---|
1304 | cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta |
---|
1305 | >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
1306 | >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) |
---|
1307 | cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 |
---|
1308 | [1,3,5,7,9,11,13,15: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %); |
---|
1309 | |2,4,6,8,10,12,14,16: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %); |
---|
1310 | ] |
---|
1311 | #Hle2 normalize nodelta #Hli |
---|
1312 | <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 |
---|
1313 | >(pair_eq2 ?????? (proj2 ?? Hl)) <(pair_eq2 ?????? (Some_eq ??? Hli)) |
---|
1314 | cases (\snd (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_policy) ?)) |
---|
1315 | [1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91: @(leb_true_to_le … Hle2) |
---|
1316 | ] normalize @I (* much faster than / by I/, strangely enough *) |
---|
1317 | |11,12,13,16,17,48,49,50,53,54: #x #id >p3 whd in match (jump_expansion_step_instruction ???); |
---|
1318 | whd in match (select_reljump_length ???); |
---|
1319 | cases (lookup_def ?? labels id 〈0,\fst pol〉) #q1 #q2 normalize nodelta |
---|
1320 | >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
1321 | >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) lapply (refl ? (leb (\fst pol) q2)) |
---|
1322 | cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 |
---|
1323 | [1,3,5,7,9,11,13,15,17,19: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %); |
---|
1324 | |2,4,6,8,10,12,14,16,18,20: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %); |
---|
1325 | ] |
---|
1326 | #Hle2 normalize nodelta #Hli |
---|
1327 | <(pair_eq1 ?????? (Some_eq ??? Hli)) >Hle1 >(pair_eq2 ?????? (proj2 ?? Hl)) |
---|
1328 | <(pair_eq2 ?????? (Some_eq ??? Hli)) |
---|
1329 | cases (\snd (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_policy) ?)) |
---|
1330 | [1,7,13,19,25,31,37,43,49,55,61,67,73,79,85,91,97,103,109,115: @(leb_true_to_le … Hle2) |
---|
1331 | ] normalize @I (* vide supra *) |
---|
1332 | ] |
---|
1333 | |4,5,10,11: #id >p3 normalize nodelta whd in match (select_jump_length ???); |
---|
1334 | whd in match (select_call_length ???); cases (lookup_def ?? labels id 〈0,\fst pol〉) |
---|
1335 | #q1 #q2 normalize nodelta |
---|
1336 | >(pair_eq1 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
1337 | >(pair_eq2 ?????? (pair_eq1 ?????? (proj2 ?? Hl))) |
---|
1338 | [1,3: lapply (refl ? (leb (\fst pol) q2)) cases (leb (\fst pol) q2) in ⊢ (???% → %); #Hle1 |
---|
1339 | [1,3: lapply (refl ? (leb (q2-\fst pol) 126)) cases (leb (q2-\fst pol) 126) in ⊢ (???% → %); |
---|
1340 | |2,4: lapply (refl ? (leb (\fst pol-q2) 129)) cases (leb (\fst pol-q2) 129) in ⊢ (???% → %); |
---|
1341 | ] |
---|
1342 | #Hle2 normalize nodelta |
---|
1343 | ] |
---|
1344 | [2,4,6,8,9,10: lapply (refl ? (split ? 5 11 (bitvector_of_nat ? q2))) |
---|
1345 | cases (split ??? (bitvector_of_nat ? q2)) in ⊢ (???% → %); #x1 #x2 #Hle3 |
---|
1346 | lapply (refl ? (split ? 5 11 (bitvector_of_nat ? (\fst pol)))) |
---|
1347 | cases (split ??? (bitvector_of_nat ? (\fst pol))) in ⊢ (???% → %); #y1 #y2 #Hle4 |
---|
1348 | normalize nodelta lapply (refl ? (eq_bv 5 x1 y1)) |
---|
1349 | cases (eq_bv 5 x1 y1) in ⊢ (???% → %); #Hle5 |
---|
1350 | ] |
---|
1351 | #Hli <(pair_eq1 ?????? (Some_eq ??? Hli)) >(pair_eq2 ?????? (proj2 ?? Hl)) |
---|
1352 | <(pair_eq2 ?????? (Some_eq ??? Hli)) |
---|
1353 | cases (\snd (lookup ?? (bitvector_of_nat ? (|prefix|)) (\snd old_policy) ?)) |
---|
1354 | [2,8,14,20,26,32: >Hle3 @Hle5 |
---|
1355 | |37,40,43,46: >Hle1 @(leb_true_to_le … Hle2) |
---|
1356 | ] normalize @I (* here too *) |
---|
1357 | ] |
---|
1358 | ] |
---|
1359 | ] |
---|
1360 | |2,4: (* changed *) |
---|
1361 | normalize nodelta #Hc [2: destruct (Hc)] #i #Hi cases (le_to_or_lt_eq … Hi) -Hi |
---|
1362 | >append_length >commutative_plus #Hi |
---|
1363 | normalize in Hi; |
---|
1364 | [ >lookup_insert_miss |
---|
1365 | [ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi)) |
---|
1366 | | @bitvector_of_nat_abs |
---|
1367 | [3: @lt_to_not_eq @(le_S_S_to_le … Hi) |
---|
1368 | |1: @(transitive_lt ??? (le_S_S_to_le … Hi)) |
---|
1369 | ] |
---|
1370 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
1371 | @le_S_S @le_plus_n_r |
---|
1372 | ] |
---|
1373 | | >(injective_S … Hi) >lookup_insert_hit normalize nodelta in Hlength; >Hlength |
---|
1374 | normalize nodelta @pair_elim #l1 #l2 #Hl @pair_elim #y1 #y2 #Hy >Hl @refl |
---|
1375 | ] |
---|
1376 | ] |
---|
1377 | |2,4: (* policy_isize_sum XXX *) cases daemon |
---|
1378 | ] |
---|
1379 | | (* Case where add_instr = None *) normalize nodelta lapply (pi2 ?? acc) >p >p1 |
---|
1380 | normalize nodelta #Hpolicy |
---|
1381 | @conj [ @conj [ @conj [ @conj [ @conj [ @conj |
---|
1382 | [ (* out_of_program_none *) #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
1383 | #Hi2 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) i (le_S_to_le ?? Hi) Hi2) |
---|
1384 | | (* labels_okay *) @lookup_forall #x cases x -x #x cases x #p #a #j #lbl #Hl normalize nodelta |
---|
1385 | elim (forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))) ? lbl Hl) |
---|
1386 | #id #Hid @(ex_intro … id Hid) |
---|
1387 | ] |
---|
1388 | | (* jump_in_policy *) #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
1389 | elim (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
1390 | [ >(nth_append_first ?? prefix ?? (le_S_S_to_le ?? Hi)) |
---|
1391 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))) i (le_S_S_to_le ?? Hi)) |
---|
1392 | | >(injective_S … Hi) @conj |
---|
1393 | [ >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n whd in match (nth ????); |
---|
1394 | normalize nodelta in p2; cases instr in p2; |
---|
1395 | [ #pi cases pi |
---|
1396 | [1,2,3,6,7,33,34: #x #y #_ #H @⊥ @H |
---|
1397 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ #H @⊥ @H |
---|
1398 | |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta |
---|
1399 | whd in match (jump_expansion_step_instruction ???); |
---|
1400 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
1401 | |11,12,13,16,17: #x #id normalize nodelta |
---|
1402 | whd in match (jump_expansion_step_instruction ???); |
---|
1403 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
1404 | |35,36,37: #_ #H @⊥ @H |
---|
1405 | ] |
---|
1406 | |2,3: #x #_ #H @⊥ @H |
---|
1407 | |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
1408 | |6: #x #id #_ #H @⊥ @H |
---|
1409 | ] |
---|
1410 | | #H elim H -H #p #H elim H -H #a #H elim H -H #j #H |
---|
1411 | >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (|prefix|) (le_n (|prefix|)) ?) in H; |
---|
1412 | [ #H destruct (H) |
---|
1413 | | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
1414 | @le_S_S @le_plus_n_r |
---|
1415 | ] |
---|
1416 | ] |
---|
1417 | ] |
---|
1418 | ] |
---|
1419 | | (* policy_increase *) #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
1420 | elim (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
1421 | [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))) i (le_S_S_to_le … Hi)) |
---|
1422 | | >(injective_S … Hi) >lookup_opt_lookup_miss |
---|
1423 | [ >lookup_opt_lookup_miss |
---|
1424 | [ normalize nodelta %2 @refl |
---|
1425 | | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (|prefix|) (le_n (|prefix|)) ?) |
---|
1426 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
1427 | @le_S_S @le_plus_n_r |
---|
1428 | ] |
---|
1429 | | @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (|prefix|) ?)) >prf |
---|
1430 | [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r |
---|
1431 | | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p1 |
---|
1432 | whd in match (nth ????); normalize nodelta in p2; cases instr in p2; |
---|
1433 | [ #pi cases pi |
---|
1434 | [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/ |
---|
1435 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/ |
---|
1436 | |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta |
---|
1437 | whd in match (jump_expansion_step_instruction ???); |
---|
1438 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
1439 | |11,12,13,16,17: #x #id normalize nodelta |
---|
1440 | whd in match (jump_expansion_step_instruction ???); |
---|
1441 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
1442 | |35,36,37: #_ normalize /2 by nmk/ |
---|
1443 | ] |
---|
1444 | |2,3: #x #_ normalize /2 by nmk/ |
---|
1445 | |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
1446 | |6: #x #id #_ normalize /2 by nmk/ |
---|
1447 | ] |
---|
1448 | ] |
---|
1449 | ] |
---|
1450 | ] |
---|
1451 | ] |
---|
1452 | | (* policy_safe *) @lookup_forall #x cases x -x #x cases x -x #p #a #j #n #Hl |
---|
1453 | @(forall_lookup … (proj2 ?? (proj1 ?? (proj1 ?? Hpolicy))) ? n Hl) |
---|
1454 | ] |
---|
1455 | | (* changed *) #Hc #i >append_length >commutative_plus #Hi normalize in Hi; |
---|
1456 | elim (le_to_or_lt_eq … Hi) -Hi #Hi |
---|
1457 | [ @(proj2 ?? (proj1 ?? Hpolicy) Hc i (le_S_S_to_le … Hi)) |
---|
1458 | | >(injective_S … Hi) >lookup_opt_lookup_miss |
---|
1459 | [ >lookup_opt_lookup_miss |
---|
1460 | [ normalize nodelta @refl |
---|
1461 | | @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy))))) (|prefix|) (le_n (|prefix|)) ?) |
---|
1462 | @(transitive_lt … (pi2 ?? program)) >prf >append_length normalize <plus_n_Sm |
---|
1463 | @le_S_S @le_plus_n_r |
---|
1464 | ] |
---|
1465 | | @(proj1 ?? (jump_not_in_policy (pi1 … program) «pi1 ?? old_policy,proj1 ?? (proj1 ?? (pi2 ?? old_policy))» (|prefix|) ?)) >prf |
---|
1466 | [ >append_length normalize <plus_n_Sm @le_S_S @le_plus_n_r |
---|
1467 | | >(nth_append_second ?? prefix ?? (le_n (|prefix|))) <minus_n_n >p1 |
---|
1468 | whd in match (nth ????); normalize nodelta in p2; cases instr in p2; |
---|
1469 | [ #pi cases pi |
---|
1470 | [1,2,3,6,7,33,34: #x #y #_ normalize /2 by nmk/ |
---|
1471 | |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #_ normalize /2 by nmk/ |
---|
1472 | |9,10,14,15: #id (* normalize segfaults here *) normalize nodelta |
---|
1473 | whd in match (jump_expansion_step_instruction ???); |
---|
1474 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
1475 | |11,12,13,16,17: #x #id normalize nodelta |
---|
1476 | whd in match (jump_expansion_step_instruction ???); |
---|
1477 | #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
1478 | |35,36,37: #_ normalize /2 by nmk/ |
---|
1479 | ] |
---|
1480 | |2,3: #x #_ normalize /2 by nmk/ |
---|
1481 | |4,5: #id normalize nodelta #H lapply (jmeq_to_eq ??? H) #H2 destruct (H2) |
---|
1482 | |6: #x #id #_ normalize /2 by nmk/ |
---|
1483 | ] |
---|
1484 | ] |
---|
1485 | ] |
---|
1486 | ] |
---|
1487 | ] |
---|
1488 | | (* XXX policy_isize_sum *) cases daemon |
---|
1489 | ] |
---|
1490 | | @conj [ @conj [ @conj [ @conj [ @conj [ @conj |
---|
1491 | [ #i #Hi / by refl/ |
---|
1492 | | / by I/ |
---|
1493 | ] |
---|
1494 | | #i #Hi @conj [ >nth_nil #H @⊥ @H | #H elim H #x #H1 elim H1 #y #H2 elim H2 #z #H3 |
---|
1495 | normalize in H3; destruct (H3) ] |
---|
1496 | ] |
---|
1497 | | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ] |
---|
1498 | ] |
---|
1499 | | / by I/ |
---|
1500 | ] |
---|
1501 | | #_ #i #Hi @⊥ @(absurd (i < 0)) [ @Hi | @not_le_Sn_O ] |
---|
1502 | ] |
---|
1503 | | / by refl/ |
---|
1504 | ] |
---|
1505 | ] |
---|
1506 | qed.*) |
---|
1507 | |
---|
1508 | (* this might be replaced by a coercion: (∀x.A x → B x) → Σx.A x → Σx.B x *) |
---|
1509 | (* definition weaken_policy: |
---|
1510 | ∀program,op. |
---|
1511 | option (Σp:jump_expansion_policy. |
---|
1512 | And (And (And (And (out_of_program_none program p) |
---|
1513 | (labels_okay (create_label_map program op) p)) |
---|
1514 | (jump_in_policy program p)) (policy_increase program op p)) |
---|
1515 | (policy_safe p)) → |
---|
1516 | option (Σp:jump_expansion_policy.And (out_of_program_none program p) |
---|
1517 | (jump_in_policy program p)) ≝ |
---|
1518 | λprogram.λop.λx. |
---|
1519 | match x return λ_.option (Σp.And (out_of_program_none program p) (jump_in_policy program p)) with |
---|
1520 | [ None ⇒ None ? |
---|
1521 | | Some z ⇒ Some ? (mk_Sig ?? (pi1 ?? z) ?) |
---|
1522 | ]. |
---|
1523 | @conj |
---|
1524 | [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (pi2 ?? z))))) |
---|
1525 | | @(proj2 ?? (proj1 ?? (proj1 ?? (pi2 ?? z)))) |
---|
1526 | ] |
---|
1527 | qed. *) |
---|
1528 | |
---|
1529 | (* This function executes n steps from the starting point. *) |
---|
1530 | (*let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (|l|) 2^16) |
---|
1531 | (n: ℕ) on n:(Σx:bool × ℕ × (option jump_expansion_policy). |
---|
1532 | let 〈ch,pc,y〉 ≝ x in |
---|
1533 | match y with |
---|
1534 | [ None ⇒ pc > 2^16 |
---|
1535 | | Some p ⇒ And (out_of_program_none program p) (jump_in_policy program p) |
---|
1536 | ]) ≝ |
---|
1537 | match n with |
---|
1538 | [ O ⇒ 〈0,Some ? (pi1 … (jump_expansion_start program))〉 |
---|
1539 | | S m ⇒ let 〈ch,pc,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in |
---|
1540 | match z return λx. z=x → Σa:bool × ℕ × (option jump_expansion_policy).? with |
---|
1541 | [ None ⇒ λp2.〈pc,None ?〉 |
---|
1542 | | Some op ⇒ λp2.pi1 … (jump_expansion_step program (create_label_map program op) «op,?») |
---|
1543 | ] (refl … z) |
---|
1544 | ].*) |
---|
1545 | |
---|
1546 | |
---|
1547 | let rec jump_expansion_internal (program: Σl:list labelled_instruction.lt (length ? l) 2^16) (n: ℕ) |
---|
1548 | on n:(Σx:bool × (option ppc_pc_map). |
---|
1549 | let 〈c,pol〉 ≝ x in |
---|
1550 | match pol with |
---|
1551 | [ None ⇒ True |
---|
1552 | | Some x ⇒ |
---|
1553 | And (And |
---|
1554 | (out_of_program_none program x) |
---|
1555 | (policy_isize_sum program (create_label_map program) x)) |
---|
1556 | (\fst x < 2^16) |
---|
1557 | ]) ≝ |
---|
1558 | let labels ≝ create_label_map program in |
---|
1559 | match n with |
---|
1560 | [ O ⇒ 〈true,pi1 ?? (jump_expansion_start program labels)〉 |
---|
1561 | | S m ⇒ let 〈ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in |
---|
1562 | match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with |
---|
1563 | [ None ⇒ λp2.〈false,None ?〉 |
---|
1564 | | Some op ⇒ λp2.if ch |
---|
1565 | then pi1 ?? (jump_expansion_step program labels «op,?») |
---|
1566 | else (jump_expansion_internal program m) |
---|
1567 | ] (refl … z) |
---|
1568 | ]. |
---|
1569 | [ normalize nodelta cases (jump_expansion_start program (create_label_map program)) |
---|
1570 | #p cases p |
---|
1571 | [ / by I/ |
---|
1572 | | #pm / by I/ |
---|
1573 | ] |
---|
1574 | | lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / |
---|
1575 | | lapply (pi2 ?? (jump_expansion_internal program m)) <p1 >p2 normalize nodelta / by / |
---|
1576 | | normalize nodelta cases (jump_expansion_step program labels «op,?») |
---|
1577 | #p cases p -p #p #r cases r normalize nodelta |
---|
1578 | [ #H / by I/ |
---|
1579 | | #j #H @conj |
---|
1580 | [ @conj |
---|
1581 | [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) |
---|
1582 | | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) |
---|
1583 | ] |
---|
1584 | | @(proj2 ?? H) |
---|
1585 | ] |
---|
1586 | ] |
---|
1587 | ] |
---|
1588 | qed. |
---|
1589 | |
---|
1590 | lemma pe_int_refl: ∀program.reflexive ? (policy_equal program). |
---|
1591 | #program whd #x whd #n #Hn |
---|
1592 | cases (bvt_lookup … (bitvector_of_nat 16 n) (\snd x) 〈0,short_jump〉) |
---|
1593 | #y #z normalize nodelta @refl |
---|
1594 | qed. |
---|
1595 | |
---|
1596 | lemma pe_int_sym: ∀program.symmetric ? (policy_equal program). |
---|
1597 | #program whd #x #y #Hxy whd #n #Hn |
---|
1598 | lapply (Hxy n Hn) cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉) |
---|
1599 | #x1 #x2 |
---|
1600 | cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉) |
---|
1601 | #y1 #y2 normalize nodelta // |
---|
1602 | qed. |
---|
1603 | |
---|
1604 | lemma pe_int_trans: ∀program.transitive ? (policy_equal program). |
---|
1605 | #program whd #x #y #z whd in match (policy_equal ???); whd in match (policy_equal ?y ?); |
---|
1606 | whd in match (policy_equal ? x z); #Hxy #Hyz #n #Hn lapply (Hxy n Hn) -Hxy |
---|
1607 | lapply (Hyz n Hn) -Hyz cases (bvt_lookup … (bitvector_of_nat ? n) (\snd x) 〈0,short_jump〉) |
---|
1608 | #x1 #x2 |
---|
1609 | cases (bvt_lookup … (bitvector_of_nat ? n) (\snd y) 〈0,short_jump〉) #y1 #y2 |
---|
1610 | cases (bvt_lookup … (bitvector_of_nat ? n) (\snd z) 〈0,short_jump〉) #z1 #z2 |
---|
1611 | normalize nodelta // |
---|
1612 | qed. |
---|
1613 | |
---|
1614 | definition policy_equal_opt ≝ |
---|
1615 | λprogram:list labelled_instruction.λp1,p2:option ppc_pc_map. |
---|
1616 | match p1 with |
---|
1617 | [ Some x1 ⇒ match p2 with |
---|
1618 | [ Some x2 ⇒ policy_equal program x1 x2 |
---|
1619 | | _ ⇒ False |
---|
1620 | ] |
---|
1621 | | None ⇒ p2 = None ? |
---|
1622 | ]. |
---|
1623 | |
---|
1624 | lemma pe_refl: ∀program.reflexive ? (policy_equal_opt program). |
---|
1625 | #program whd #x whd cases x |
---|
1626 | [ // |
---|
1627 | | #y @pe_int_refl |
---|
1628 | ] |
---|
1629 | qed. |
---|
1630 | |
---|
1631 | lemma pe_sym: ∀program.symmetric ? (policy_equal_opt program). |
---|
1632 | #program whd #x #y #Hxy whd cases y in Hxy; |
---|
1633 | [ cases x |
---|
1634 | [ // |
---|
1635 | | #x' #H @⊥ @(absurd ? H) /2 by nmk/ |
---|
1636 | ] |
---|
1637 | | #y' cases x |
---|
1638 | [ #H @⊥ @(absurd ? H) whd in match (policy_equal_opt ???); @nmk #H destruct (H) |
---|
1639 | | #x' #H @pe_int_sym @H |
---|
1640 | ] |
---|
1641 | ] |
---|
1642 | qed. |
---|
1643 | |
---|
1644 | lemma pe_trans: ∀program.transitive ? (policy_equal_opt program). |
---|
1645 | #program whd #x #y #z cases x |
---|
1646 | [ #Hxy #Hyz >Hxy in Hyz; // |
---|
1647 | | #x' cases y |
---|
1648 | [ #H @⊥ @(absurd ? H) /2 by nmk/ |
---|
1649 | | #y' cases z |
---|
1650 | [ #_ #H @⊥ @(absurd ? H) /2 by nmk/ |
---|
1651 | | #z' @pe_int_trans |
---|
1652 | ] |
---|
1653 | ] |
---|
1654 | ] |
---|
1655 | qed. |
---|
1656 | |
---|
1657 | definition step_none: ∀program.∀n. |
---|
1658 | (\snd (pi1 ?? (jump_expansion_internal program n))) = None ? → |
---|
1659 | ∀k.(\snd (pi1 ?? (jump_expansion_internal program (n+k)))) = None ?. |
---|
1660 | #program #n lapply (refl ? (jump_expansion_internal program n)) |
---|
1661 | cases (jump_expansion_internal program n) in ⊢ (???% → %); |
---|
1662 | #x1 cases x1 #p1 #j1 -x1; #H1 #Heqj #Hj #k elim k |
---|
1663 | [ <plus_n_O >Heqj @Hj |
---|
1664 | | #k' -k <plus_n_Sm whd in match (jump_expansion_internal program (S (n+k'))); |
---|
1665 | lapply (refl ? (jump_expansion_internal program (n+k'))) |
---|
1666 | cases (jump_expansion_internal program (n+k')) in ⊢ (???% → % → %); |
---|
1667 | #x2 cases x2 -x2 #c2 #p2 normalize nodelta #H #Heqj2 |
---|
1668 | cases p2 in H Heqj2; |
---|
1669 | [ #H #Heqj2 #_ whd in match (jump_expansion_internal ??); |
---|
1670 | >Heqj2 normalize nodelta @refl |
---|
1671 | | #x #H #Heqj2 #abs destruct (abs) |
---|
1672 | ] |
---|
1673 | ] |
---|
1674 | qed. |
---|
1675 | |
---|
1676 | lemma pe_step: ∀program:(Σl:list labelled_instruction.|l| < 2^16). |
---|
1677 | ∀n.policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program n))) |
---|
1678 | (\snd (pi1 ?? (jump_expansion_internal program (S n)))) → |
---|
1679 | policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program (S n)))) |
---|
1680 | (\snd (pi1 ?? (jump_expansion_internal program (S (S n))))). |
---|
1681 | #program #n #Heq |
---|
1682 | cases daemon (* XXX *) |
---|
1683 | qed. |
---|
1684 | |
---|
1685 | (* this is in the stdlib, but commented out, why? *) |
---|
1686 | theorem plus_Sn_m1: ∀n,m:nat. S m + n = m + S n. |
---|
1687 | #n (elim n) normalize /2 by S_pred/ qed. |
---|
1688 | |
---|
1689 | lemma equal_remains_equal: ∀program:(Σl:list labelled_instruction.|l| < 2^16).∀n:ℕ. |
---|
1690 | policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n))) |
---|
1691 | (\snd (pi1 … (jump_expansion_internal program (S n)))) → |
---|
1692 | ∀k.k ≥ n → policy_equal_opt program (\snd (pi1 … (jump_expansion_internal program n))) |
---|
1693 | (\snd (pi1 … (jump_expansion_internal program k))). |
---|
1694 | #program #n #Heq #k #Hk elim (le_plus_k … Hk); #z #H >H -H -Hk -k; |
---|
1695 | lapply Heq -Heq; lapply n -n; elim z -z; |
---|
1696 | [ #n #Heq <plus_n_O @pe_refl |
---|
1697 | | #z #Hind #n #Heq <plus_Sn_m1 whd in match (plus (S n) z); |
---|
1698 | @(pe_trans … (\snd (pi1 … (jump_expansion_internal program (S n))))) |
---|
1699 | [ @Heq |
---|
1700 | | @Hind @pe_step @Heq |
---|
1701 | ] |
---|
1702 | ] |
---|
1703 | qed. |
---|
1704 | |
---|
1705 | (* this number monotonically increases over iterations, maximum 2*|program| *) |
---|
1706 | let rec measure_int (program: list labelled_instruction) (policy: ppc_pc_map) (acc: ℕ) |
---|
1707 | on program: ℕ ≝ |
---|
1708 | match program with |
---|
1709 | [ nil ⇒ acc |
---|
1710 | | cons h t ⇒ match (\snd (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) with |
---|
1711 | [ long_jump ⇒ measure_int t policy (acc + 2) |
---|
1712 | | medium_jump ⇒ measure_int t policy (acc + 1) |
---|
1713 | | _ ⇒ measure_int t policy acc |
---|
1714 | ] |
---|
1715 | ]. |
---|
1716 | |
---|
1717 | lemma measure_plus: ∀program.∀policy.∀x,d:ℕ. |
---|
1718 | measure_int program policy (x+d) = measure_int program policy x + d. |
---|
1719 | #program #policy #x #d generalize in match x; -x elim d |
---|
1720 | [ // |
---|
1721 | | -d; #d #Hind elim program |
---|
1722 | [ / by refl/ |
---|
1723 | | #h #t #Hd #x whd in match (measure_int ???); whd in match (measure_int ?? x); |
---|
1724 | cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) |
---|
1725 | [ normalize nodelta @Hd |
---|
1726 | |2,3: normalize nodelta >associative_plus >(commutative_plus (S d) ?) <associative_plus |
---|
1727 | @Hd |
---|
1728 | ] |
---|
1729 | ] |
---|
1730 | ] |
---|
1731 | qed. |
---|
1732 | |
---|
1733 | lemma measure_le: ∀program.∀policy. |
---|
1734 | measure_int program policy 0 ≤ 2*|program|. |
---|
1735 | #program #policy elim program |
---|
1736 | [ normalize @le_n |
---|
1737 | | #h #t #Hind whd in match (measure_int ???); |
---|
1738 | cases (\snd (lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) |
---|
1739 | [ normalize nodelta @(transitive_le ??? Hind) /2 by monotonic_le_times_r/ |
---|
1740 | |2,3: normalize nodelta >measure_plus <times_n_Sm >(commutative_plus 2 ?) |
---|
1741 | @le_plus [1,3: @Hind |2,4: / by le_n/ ] |
---|
1742 | ] |
---|
1743 | ] |
---|
1744 | qed. |
---|
1745 | |
---|
1746 | (* uses the second part of policy_increase *) |
---|
1747 | lemma measure_incr_or_equal: ∀program:Σl:list labelled_instruction.|l|<2^16. |
---|
1748 | ∀policy:Σp:ppc_pc_map. |
---|
1749 | out_of_program_none program p ∧ |
---|
1750 | policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16. |
---|
1751 | ∀l.|l| ≤ |program| → ∀acc:ℕ. |
---|
1752 | match \snd (jump_expansion_step program (create_label_map program) policy) with |
---|
1753 | [ None ⇒ True |
---|
1754 | | Some p ⇒ measure_int l policy acc ≤ measure_int l p acc |
---|
1755 | ]. |
---|
1756 | #program #policy #l elim l -l; |
---|
1757 | [ #Hp #acc cases (jump_expansion_step ???) #pi1 cases pi1 #p #q -pi1; cases q [ // | #x #_ @le_n ] |
---|
1758 | | #h #t #Hind #Hp #acc |
---|
1759 | lapply (refl ? (jump_expansion_step program (create_label_map program) policy)) |
---|
1760 | cases (jump_expansion_step ???) in ⊢ (???% → %); #pi1 cases pi1 -pi1 #c #r cases r |
---|
1761 | [ / by I/ |
---|
1762 | | #x normalize nodelta #Hx #Hjeq lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hx))) (|t|) Hp) |
---|
1763 | whd in match (measure_int ???); whd in match (measure_int ? x ?); |
---|
1764 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉) |
---|
1765 | #x1 #x2 cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) (\snd x) 〈0,short_jump〉) |
---|
1766 | #y1 #y2 normalize nodelta #Hblerp cases (proj2 ?? Hblerp) cases x2 cases y2 |
---|
1767 | [1,4,5,7,8,9: #H cases H |
---|
1768 | |2,3,6: #_ normalize nodelta |
---|
1769 | [1,2: @(transitive_le ? (measure_int t x acc)) |
---|
1770 | |3: @(transitive_le ? (measure_int t x (acc+1))) |
---|
1771 | ] |
---|
1772 | [2,4,5,6: >measure_plus [1,2: @le_plus_n_r] >measure_plus @le_plus / by le_n/] |
---|
1773 | >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn |
---|
1774 | |11,12,13,15,16,17: #H destruct (H) |
---|
1775 | |10,14,18: normalize nodelta #_ >Hjeq in Hind; #Hind @Hind @(transitive_le … Hp) @le_n_Sn |
---|
1776 | ] |
---|
1777 | ] |
---|
1778 | ] |
---|
1779 | qed. |
---|
1780 | |
---|
1781 | (* these lemmas seem superfluous, but not sure how *) |
---|
1782 | lemma bla: ∀a,b:ℕ.a + a = b + b → a = b. |
---|
1783 | #a elim a |
---|
1784 | [ normalize #b // |
---|
1785 | | -a #a #Hind #b cases b [ /2 by le_n_O_to_eq/ | -b #b normalize |
---|
1786 | <plus_n_Sm <plus_n_Sm #H |
---|
1787 | >(Hind b (injective_S ?? (injective_S ?? H))) // ] |
---|
1788 | ] |
---|
1789 | qed. |
---|
1790 | |
---|
1791 | lemma sth_not_s: ∀x.x ≠ S x. |
---|
1792 | #x cases x |
---|
1793 | [ // | #y // ] |
---|
1794 | qed. |
---|
1795 | |
---|
1796 | lemma measure_full: ∀program.∀policy. |
---|
1797 | measure_int program policy 0 = 2*|program| → ∀i.i<|program| → |
---|
1798 | is_jump (nth i ? program 〈None ?,Comment []〉) → |
---|
1799 | (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump. |
---|
1800 | #program #policy elim program in ⊢ (% → ∀i.% → ? → %); |
---|
1801 | [ #Hm #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O |
---|
1802 | | #h #t #Hind #Hm #i #Hi #Hj |
---|
1803 | cases (le_to_or_lt_eq … Hi) -Hi |
---|
1804 | [ #Hi @Hind |
---|
1805 | [ whd in match (measure_int ???) in Hm; |
---|
1806 | cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm; |
---|
1807 | normalize nodelta |
---|
1808 | [ #H @⊥ @(absurd ? (measure_le t policy)) >H @lt_to_not_le /2 by lt_plus, le_n/ |
---|
1809 | | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) |
---|
1810 | <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/ |
---|
1811 | | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/ |
---|
1812 | ] |
---|
1813 | | @(le_S_S_to_le … Hi) |
---|
1814 | | @Hj |
---|
1815 | ] |
---|
1816 | | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; |
---|
1817 | cases (\snd (bvt_lookup … (bitvector_of_nat ? (|t|)) (\snd policy) 〈0,short_jump〉)) in Hm; |
---|
1818 | normalize nodelta |
---|
1819 | [ #Hm @⊥ @(absurd ? (measure_le t policy)) >Hm @lt_to_not_le /2 by lt_plus, le_n/ |
---|
1820 | | >measure_plus >commutative_plus #H @⊥ @(absurd ? (measure_le t policy)) |
---|
1821 | <(plus_to_minus … (sym_eq … H)) @lt_to_not_le normalize /2 by le_n/ |
---|
1822 | | >measure_plus <times_n_Sm >commutative_plus /2 by injective_plus_r/ |
---|
1823 | ] |
---|
1824 | ] |
---|
1825 | ] |
---|
1826 | qed. |
---|
1827 | |
---|
1828 | (* uses second part of policy_increase *) |
---|
1829 | lemma measure_special: ∀program:(Σl:list labelled_instruction.|l| < 2^16). |
---|
1830 | ∀policy:Σp:ppc_pc_map. |
---|
1831 | out_of_program_none program p ∧ policy_isize_sum program (create_label_map program) p ∧ \fst p < 2^16. |
---|
1832 | match (\snd (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) with |
---|
1833 | [ None ⇒ True |
---|
1834 | | Some p ⇒ measure_int program policy 0 = measure_int program p 0 → policy_equal program policy p ]. |
---|
1835 | #program #policy lapply (refl ? (pi1 ?? (jump_expansion_step program (create_label_map program) policy))) |
---|
1836 | cases (jump_expansion_step program (create_label_map program) policy) in ⊢ (???% → %); |
---|
1837 | #p cases p -p #ch #pol normalize nodelta cases pol |
---|
1838 | [ / by I/ |
---|
1839 | | #p normalize nodelta #Hpol #eqpol lapply (le_n (|program|)) |
---|
1840 | @(list_ind ? (λx.|x| ≤ |pi1 ?? program| → |
---|
1841 | measure_int x policy 0 = measure_int x p 0 → |
---|
1842 | policy_equal x policy p) ?? (pi1 ?? program)) |
---|
1843 | [ #_ #_ #i #Hi @⊥ @(absurd ? Hi) @not_le_Sn_O |
---|
1844 | | #h #t #Hind #Hp #Hm #i #Hi cases (le_to_or_lt_eq … Hi) -Hi; |
---|
1845 | [ #Hi @Hind |
---|
1846 | [ @(transitive_le … Hp) / by / |
---|
1847 | | whd in match (measure_int ???) in Hm; whd in match (measure_int ? p ?) in Hm; |
---|
1848 | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (|t|) Hp) #Hinc |
---|
1849 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in Hm Hinc; #x1 #x2 |
---|
1850 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); #y1 #y2 |
---|
1851 | #Hm #Hinc lapply Hm -Hm; lapply Hinc -Hinc; normalize nodelta |
---|
1852 | cases x2 cases y2 normalize nodelta |
---|
1853 | [1: / by / |
---|
1854 | |2,3: >measure_plus #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt |
---|
1855 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
1856 | [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
1857 | |4,7,8: #H elim (proj2 ?? H) #H2 [1,3,5: cases H2 |2,4,6: destruct (H2) ] |
---|
1858 | |5: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 1) |
---|
1859 | #_ #H @(injective_plus_r … H) |
---|
1860 | |6: >measure_plus >measure_plus |
---|
1861 | change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) |
---|
1862 | #_ #H @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l |
---|
1863 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
1864 | [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
1865 | |9: >measure_plus >measure_plus >commutative_plus >(commutative_plus ? 2) |
---|
1866 | #_ #H @(injective_plus_r … H) |
---|
1867 | ] |
---|
1868 | | @(le_S_S_to_le … Hi) |
---|
1869 | ] |
---|
1870 | | #Hi >(injective_S … Hi) whd in match (measure_int ???) in Hm; |
---|
1871 | whd in match (measure_int ? p ?) in Hm; |
---|
1872 | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpol))) (|t|) Hp) |
---|
1873 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉) in |
---|
1874 | Hm; |
---|
1875 | #x1 #x2 |
---|
1876 | cases (bvt_lookup ?? (bitvector_of_nat ? (|t|)) ? 〈0,short_jump〉); |
---|
1877 | #y1 #y2 |
---|
1878 | normalize nodelta cases x2 cases y2 normalize nodelta |
---|
1879 | cases daemon |
---|
1880 | (* [1,5,9: #_ #_ // |
---|
1881 | |4,7,8: #_ #H elim H #H2 [1,3,5: @⊥ @H2 |2,4,6: destruct (H2) ] |
---|
1882 | |2,3: >measure_plus #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt |
---|
1883 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
1884 | [1,3: @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
1885 | |6: >measure_plus >measure_plus |
---|
1886 | change with (1+1) in match (2); >assoc_plus1 >(commutative_plus 1 (measure_int ???)) |
---|
1887 | #H #_ @⊥ @(absurd ? (eq_plus_S_to_lt … H)) @le_to_not_lt @monotonic_le_plus_l |
---|
1888 | lapply (measure_incr_or_equal program policy t ? 0) |
---|
1889 | [ @(transitive_le … Hp) @le_n_Sn ] >eqpol / by / |
---|
1890 | ] *) |
---|
1891 | ] |
---|
1892 | ] |
---|
1893 | qed. |
---|
1894 | |
---|
1895 | lemma le_to_eq_plus: ∀n,z. |
---|
1896 | n ≤ z → ∃k.z = n + k. |
---|
1897 | #n #z elim z |
---|
1898 | [ #H cases (le_to_or_lt_eq … H) |
---|
1899 | [ #H2 @⊥ @(absurd … H2) @not_le_Sn_O |
---|
1900 | | #H2 @(ex_intro … 0) >H2 // |
---|
1901 | ] |
---|
1902 | | #z' #Hind #H cases (le_to_or_lt_eq … H) |
---|
1903 | [ #H' elim (Hind (le_S_S_to_le … H')) #k' #H2 @(ex_intro … (S k')) |
---|
1904 | >H2 >plus_n_Sm // |
---|
1905 | | #H' @(ex_intro … 0) >H' // |
---|
1906 | ] |
---|
1907 | ] |
---|
1908 | qed. |
---|
1909 | |
---|
1910 | (* probably needs some kind of not_jump → short *) |
---|
1911 | lemma measure_zero: ∀l.∀program:Σl:list labelled_instruction.|l| < 2^16. |
---|
1912 | match jump_expansion_start program (create_label_map program) with |
---|
1913 | [ None ⇒ True |
---|
1914 | | Some p ⇒ |l| ≤ |program| → measure_int l p 0 = 0 |
---|
1915 | ]. |
---|
1916 | #l #program lapply (refl ? (jump_expansion_start program (create_label_map program))) |
---|
1917 | cases (jump_expansion_start program (create_label_map program)) in ⊢ (???% → %); #p #Hp #EQ |
---|
1918 | cases p in Hp EQ; |
---|
1919 | [ / by I/ |
---|
1920 | | #pl normalize nodelta #Hpl #EQ elim l |
---|
1921 | [ / by refl/ |
---|
1922 | | #h #t #Hind #Hp |
---|
1923 | cases daemon (* |
---|
1924 | cases (dec_is_jump (nth (|t|) ? program 〈None ?, Comment []〉)) #Hj |
---|
1925 | [ normalize nodelta @Hind @le_S_to_le ] |
---|
1926 | @Hp |
---|
1927 | | >(lookup_opt_lookup_miss … (proj1 ?? (jump_not_in_policy program (pi1 ?? (jump_expansion_start program)) (|t|) ?) Hj) 〈0,0,short_jump〉) |
---|
1928 | [ normalize nodelta @Hind @le_S_to_le @Hp |
---|
1929 | | @Hp |
---|
1930 | | % |
---|
1931 | [ @(proj1 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program)))) |
---|
1932 | | @(proj2 ?? (proj1 ?? (pi2 ?? (jump_expansion_start program)))) |
---|
1933 | ] |
---|
1934 | ] |
---|
1935 | ]*) |
---|
1936 | ] |
---|
1937 | qed. |
---|
1938 | |
---|
1939 | (* the actual computation of the fixpoint *) |
---|
1940 | definition je_fixpoint: ∀program:(Σl:list labelled_instruction.|l| < 2^16). |
---|
1941 | Σp:option ppc_pc_map. |
---|
1942 | And (match p with |
---|
1943 | [ None ⇒ True |
---|
1944 | | Some pol ⇒ And (And ( |
---|
1945 | (out_of_program_none program pol)) |
---|
1946 | (policy_isize_sum program (create_label_map program) pol)) |
---|
1947 | (policy_compact program (create_label_map program) pol) |
---|
1948 | ]) |
---|
1949 | (∃n.∀k.n < k → |
---|
1950 | policy_equal_opt program (\snd (pi1 ?? (jump_expansion_internal program k))) p). |
---|
1951 | #program @(\snd (pi1 ?? (jump_expansion_internal program (2*|program|)))) |
---|
1952 | cases daemon |
---|
1953 | |
---|
1954 | (* old proof |
---|
1955 | cases (dec_bounded_exists (λk.policy_equal (pi1 ?? program) |
---|
1956 | (\snd (pi1 ?? (jump_expansion_internal program k))) |
---|
1957 | (\snd (pi1 ?? (jump_expansion_internal program (S k))))) ? (2*|program|)) |
---|
1958 | cases daemon |
---|
1959 | [ #Hex elim Hex -Hex #x #Hx @(ex_intro … x) #k #Hk |
---|
1960 | @pe_trans |
---|
1961 | [ @(\snd (pi1 ?? (jump_expansion_internal program x))) |
---|
1962 | | @pe_sym @equal_remains_equal |
---|
1963 | [ @(proj2 ?? Hx) |
---|
1964 | | @le_S_S_to_le @le_S @Hk |
---|
1965 | ] |
---|
1966 | | @equal_remains_equal |
---|
1967 | [ @(proj2 ?? Hx) |
---|
1968 | | @le_S_S_to_le @le_S @(proj1 ?? Hx) |
---|
1969 | ] |
---|
1970 | ] |
---|
1971 | | #Hnex lapply (not_exists_forall … Hnex) -Hnex; #Hfa @(ex_intro … (2*|program|)) #k #Hk |
---|
1972 | @pe_sym @equal_remains_equal |
---|
1973 | [ lapply (refl ? (jump_expansion_internal program (2*|program|))) |
---|
1974 | cases (jump_expansion_internal program (2*|program|)) in ⊢ (???% → %); |
---|
1975 | #x cases x -x #Fch #Fpol normalize nodelta #HFpol cases Fpol in HFpol; normalize nodelta |
---|
1976 | [ (* if we're at None in 2*|program|, we're at None in S 2*|program| too *) |
---|
1977 | #HFpol #EQ whd in match (jump_expansion_internal ??); >EQ |
---|
1978 | normalize nodelta / by / |
---|
1979 | | #Fp #HFp #EQ whd in match (jump_expansion_internal ??); |
---|
1980 | >EQ normalize nodelta |
---|
1981 | lapply (refl ? (jump_expansion_step program (create_label_map program Fp) «Fp,?»)) |
---|
1982 | [ @HFp |
---|
1983 | | lapply (measure_full program Fp ?) |
---|
1984 | [ @le_to_le_to_eq |
---|
1985 | [ @measure_le |
---|
1986 | | cut (∀x:ℕ.x ≤ 2*|program| → |
---|
1987 | ∃p.(\snd (pi1 ?? (jump_expansion_internal program x)) = Some ? p ∧ |
---|
1988 | x ≤ measure_int program p 0)) |
---|
1989 | [ #x elim x |
---|
1990 | [ #Hx @(ex_intro ?? (jump_expansion_start program)) @conj |
---|
1991 | [ whd in match (jump_expansion_internal ??); @refl |
---|
1992 | | @le_O_n |
---|
1993 | ] |
---|
1994 | | -x #x #Hind #Hx |
---|
1995 | lapply (refl ? (jump_expansion_internal program (S x))) |
---|
1996 | cases (jump_expansion_internal program (S x)) in ⊢ (???% → %); |
---|
1997 | #z cases z -z #Sxch #Sxpol cases Sxpol -Sxpol normalize nodelta |
---|
1998 | [ #H #HeqSxpol @⊥ elim (le_to_eq_plus ?? Hx) #k #Hk |
---|
1999 | @(absurd … (step_none program (S x) ? k)) |
---|
2000 | [ >HeqSxpol / by / |
---|
2001 | | <Hk >EQ @nmk #H destruct (H) |
---|
2002 | ] |
---|
2003 | | #Sxpol #HSxpol #HeqSxpol @(ex_intro ?? Sxpol) @conj |
---|
2004 | [ @refl |
---|
2005 | | elim (Hind (transitive_le … (le_n_Sn x) Hx)) |
---|
2006 | #xpol #Hxpol @(le_to_lt_to_lt … (proj2 ?? Hxpol)) |
---|
2007 | lapply (measure_incr_or_equal program xpol program (le_n (|program|)) 0) |
---|
2008 | [ cases (jump_expansion_internal program x) in Hxpol; |
---|
2009 | #z cases z -z #xch #xpol normalize nodelta #H #H2 >(proj1 ?? H2) in H; |
---|
2010 | normalize nodelta / by / |
---|
2011 | | lapply (Hfa x Hx) lapply HeqSxpol -HeqSxpol |
---|
2012 | whd in match (jump_expansion_internal program (S x)); |
---|
2013 | lapply (refl ? (jump_expansion_internal program x)) |
---|
2014 | lapply Hxpol -Hxpol cases (jump_expansion_internal program x) in ⊢ (% → ???% → %); |
---|
2015 | #z cases z -z #xch #b normalize nodelta #H #Heq >(proj1 ?? Heq) in H; |
---|
2016 | #H #Heq cases xch in Heq; #Heq normalize nodelta |
---|
2017 | [ lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»)) |
---|
2018 | cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c |
---|
2019 | normalize nodelta cases c normalize nodelta |
---|
2020 | [ #H1 #Heq #H2 destruct (H2) |
---|
2021 | | #d #H1 #Heq #H2 destruct (H2) #Hfull #H2 elim (le_to_or_lt_eq … H2) |
---|
2022 | [ / by / |
---|
2023 | | #H3 lapply (measure_special program «xpol,H») >Heq |
---|
2024 | normalize nodelta #H4 @⊥ |
---|
2025 | @(absurd … (H4 H3)) |
---|
2026 | @Hfull |
---|
2027 | ] |
---|
2028 | ] |
---|
2029 | | lapply (refl ? (jump_expansion_step program (create_label_map (pi1 ?? program) xpol) «xpol,H»)) |
---|
2030 | cases (jump_expansion_step ???) in ⊢ (???% → %); #z cases z -z #a #c |
---|
2031 | normalize nodelta cases c normalize nodelta |
---|
2032 | [ #H1 #Heq #H2 #H3 #_ @⊥ @(absurd ?? H3) @pe_refl |
---|
2033 | | #d #H1 #Heq #H2 #H3 @⊥ @(absurd ?? H3) @pe_refl |
---|
2034 | ] |
---|
2035 | ] |
---|
2036 | ] |
---|
2037 | ] |
---|
2038 | ] |
---|
2039 | ] |
---|
2040 | | #H elim (H (2*|program|) (le_n ?)) #plp >EQ #Hplp |
---|
2041 | >(Some_eq ??? (proj1 ?? Hplp)) @(proj2 ?? Hplp) |
---|
2042 | ] |
---|
2043 | ] |
---|
2044 | | #Hfull cases (jump_expansion_step program (create_label_map program Fp) «Fp,?») in ⊢ (???% → %); |
---|
2045 | #x cases x -x #Gch #Gpol cases Gpol normalize nodelta |
---|
2046 | [ #H #EQ2 @⊥ @(absurd ?? H) @Hfull |
---|
2047 | | #Gp #HGp #EQ2 cases Fch |
---|
2048 | [ normalize nodelta #i #Hi |
---|
2049 | lapply (refl ? (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉)) |
---|
2050 | cases (lookup ?? (bitvector_of_nat 16 i) (\snd Fp) 〈0,0,short_jump〉) in ⊢ (???% → %); |
---|
2051 | #x cases x -x #p #a #j normalize nodelta #H |
---|
2052 | lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) i Hi) lapply (Hfull i Hi) >H |
---|
2053 | #H2 >H2 normalize nodelta cases (lookup ?? (bitvector_of_nat 16 i) (\snd Gp) 〈0,0,short_jump〉) |
---|
2054 | #x cases x -x #p #a #j' cases j' normalize nodelta #H elim H -H #H |
---|
2055 | [1,3: @⊥ @H |
---|
2056 | |2,4: destruct (H) |
---|
2057 | |5,6: @refl |
---|
2058 | ] |
---|
2059 | | normalize nodelta /2 by pe_int_refl/ |
---|
2060 | ] |
---|
2061 | ] |
---|
2062 | ] |
---|
2063 | ] |
---|
2064 | ] |
---|
2065 | | @le_S_S_to_le @le_S @Hk |
---|
2066 | ] |
---|
2067 | | #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) |
---|
2068 | #x cases x -x #nch #npol normalize nodelta #Hnpol |
---|
2069 | #x cases x -x #Sch #Spol normalize nodelta #HSpol |
---|
2070 | cases npol in Hnpol; cases Spol in HSpol; |
---|
2071 | [ #Hnpol #HSpol %1 // |
---|
2072 | |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal ???); // |
---|
2073 | #H destruct (H) |
---|
2074 | |4: #np #Hnp #Sp #HSp whd in match (policy_equal ???); @dec_bounded_forall #m |
---|
2075 | cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,0,short_jump〉) |
---|
2076 | #x cases x -x #x1 #x2 #x3 |
---|
2077 | cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,0,short_jump〉) |
---|
2078 | #y cases y -y #y1 #y2 #y3 normalize nodelta |
---|
2079 | @dec_eq_jump_length |
---|
2080 | ] |
---|
2081 | ] *) |
---|
2082 | qed. |
---|
2083 | |
---|
2084 | nclude alias "arithmetics/nat.ma". |
---|
2085 | include alias "basics/logic.ma". |
---|
2086 | |
---|
2087 | check create_label_cost_map |
---|
2088 | |
---|
2089 | (* The glue between Policy and Assembly. *) |
---|
2090 | definition jump_expansion': |
---|
2091 | ∀program:preamble × (Σl:list labelled_instruction.|l| < 2^16). |
---|
2092 | option (Σsigma:Word → Word × bool. |
---|
2093 | ∀ppc: Word. |
---|
2094 | let pc ≝ \fst (sigma ppc) in |
---|
2095 | let labels ≝ \fst (create_label_cost_map (\snd program)) in |
---|
2096 | let lookup_labels ≝ λx. bitvector_of_nat ? (lookup_def ?? labels x 0) in |
---|
2097 | let instruction ≝ \fst (fetch_pseudo_instruction (\snd program) ppc) in |
---|
2098 | let next_pc ≝ \fst (sigma (add … ppc (bitvector_of_nat ? 1))) in |
---|
2099 | (nat_of_bitvector … ppc ≤ |\snd program| → |
---|
2100 | next_pc = add … pc (bitvector_of_nat … (instruction_size lookup_labels sigma ppc instruction))) |
---|
2101 | ∧ |
---|
2102 | ((nat_of_bitvector … ppc < |\snd program| → |
---|
2103 | nat_of_bitvector … pc < nat_of_bitvector … next_pc) |
---|
2104 | ∨ |
---|
2105 | (nat_of_bitvector … ppc = |\snd program| → next_pc = (zero …)))). |
---|
2106 | ≝ λprogram. |
---|
2107 | let policy ≝ pi1 … (je_fixpoint (\snd program)) in |
---|
2108 | match policy with |
---|
2109 | [ None ⇒ None ? |
---|
2110 | | Some x ⇒ Some ? |
---|
2111 | «λppc.let 〈pc,jl〉 ≝ bvt_lookup ?? ppc (\snd x) 〈0,short_jump〉 in |
---|
2112 | 〈bitvector_of_nat 16 pc,jmpeqb jl long_jump〉,?» |
---|
2113 | ]. |
---|
2114 | cases daemon |
---|
2115 | qed. |
---|