source: src/ASM/PolicyFront.ma @ 2059

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