source: src/ASM/PolicyFront.ma @ 2101

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