source: src/ASM/PolicyFront.ma @ 2262

Last change on this file since 2262 was 2235, checked in by sacerdot, 7 years ago

Towards smaller proofs.
File size: 31.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 ≝
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     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 strip_target:
143  preinstruction Identifier →
144   ([[relative]] → preinstruction [[relative]]) ⊎ instruction ≝
145  λi.
146  match i with
147  [ JC _ ⇒ inl … (JC ?)
148  | JNC _ ⇒ inl … (JNC ?)
149  | JB baddr _ ⇒ inl … (JB ? baddr)
150  | JZ _ ⇒ inl … (JZ ?)
151  | JNZ _ ⇒ inl … (JNZ ?)
152  | JBC baddr _ ⇒ inl … (JBC ? baddr)
153  | JNB baddr _ ⇒ inl … (JNB ? baddr)
154  | CJNE addr _ ⇒ inl … (CJNE ? addr)
155  | DJNZ addr _ ⇒ inl … (DJNZ ? addr)
156  | ADD arg1 arg2 ⇒ inr … (ADD ? arg1 arg2)
157  | ADDC arg1 arg2 ⇒ inr … (ADDC ? arg1 arg2)
158  | SUBB arg1 arg2 ⇒ inr … (SUBB ? arg1 arg2)
159  | INC arg ⇒ inr … (INC ? arg)
160  | DEC arg ⇒ inr … (DEC ? arg)
161  | MUL arg1 arg2 ⇒ inr … (MUL ? arg1 arg2)
162  | DIV arg1 arg2 ⇒ inr … (DIV ? arg1 arg2)
163  | DA arg ⇒ inr … (DA ? arg)
164  | ANL arg ⇒ inr … (ANL ? arg)
165  | ORL arg ⇒ inr … (ORL ? arg)
166  | XRL arg ⇒ inr … (XRL ? arg)
167  | CLR arg ⇒ inr … (CLR ? arg)
168  | CPL arg ⇒ inr … (CPL ? arg)
169  | RL arg ⇒ inr … (RL ? arg)
170  | RR arg ⇒ inr … (RR ? arg)
171  | RLC arg ⇒ inr … (RLC ? arg)
172  | RRC arg ⇒ inr … (RRC ? arg)
173  | SWAP arg ⇒ inr … (SWAP ? arg)
174  | MOV arg ⇒ inr … (MOV ? arg)
175  | MOVX arg ⇒ inr … (MOVX ? arg)
176  | SETB arg ⇒ inr … (SETB ? arg)
177  | PUSH arg ⇒ inr … (PUSH ? arg)
178  | POP arg ⇒ inr … (POP ? arg)
179  | XCH arg1 arg2 ⇒ inr … (XCH ? arg1 arg2)
180  | XCHD arg1 arg2 ⇒ inr … (XCHD ? arg1 arg2)
181  | RET ⇒ inr … (RET ?)
182  | RETI ⇒ inr … (RETI ?)
183  | NOP ⇒ inr … (RealInstruction (NOP ?))
184  ].
185
186definition expand_relative_jump_unsafe:
187  jump_length → preinstruction Identifier → list instruction ≝
188  λjmp_len:jump_length.λi.
189  match strip_target i with
190  [ inl jmp ⇒ expand_relative_jump_internal_unsafe jmp_len jmp
191  | inr instr ⇒ [ instr ] ].
192
193definition expand_pseudo_instruction_unsafe:
194 jump_length → pseudo_instruction → list instruction ≝
195  λjmp_len.
196  λi.
197  match i with
198  [ Cost cost ⇒ [ ]
199  | Comment comment ⇒ [ ]
200  | Call call ⇒
201    match jmp_len with
202    [ short_jump ⇒ [ ] (* this should not happen *)
203    | absolute_jump ⇒ [ ACALL (ADDR11 (zero 11)) ]
204    | long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ]
205    ]
206  | Mov d trgt ⇒
207     [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))]
208  | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr
209  | Jmp jmp ⇒
210    match jmp_len with
211    [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ]
212    | absolute_jump ⇒ [ AJMP (ADDR11 (zero 11)) ]
213    | long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ]
214    ]
215  ].
216 %
217qed.
218
219definition instruction_size_jmplen:
220 jump_length → pseudo_instruction → ℕ ≝
221  λjmp_len.
222  λi.
223  let mapped ≝ map ? ? assembly1 (expand_pseudo_instruction_unsafe jmp_len i) in
224  let flattened ≝ flatten ? mapped in
225  let pc_len ≝ length ? flattened in
226    pc_len.
227
228definition sigma_compact_unsafe ≝
229 λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
230 ∀n.n < |prefix| →
231  match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
232  [ None ⇒ False
233  | Some x ⇒ let 〈pc,j〉 ≝ x in
234    match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with
235    [ None ⇒ False
236    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
237       pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment []〉))
238    ]
239  ].
240   
241(* new safety condition: sigma corresponds to program and resulting program is compact *)
242definition sigma_compact ≝
243 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
244 ∀n.n < |program| →
245  match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with
246  [ None ⇒ False
247  | Some x ⇒ let 〈pc,j〉 ≝ x in
248    match bvt_lookup_opt … (bitvector_of_nat ? (S n)) (\snd sigma) with
249    [ None ⇒ False
250    | Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in
251       pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
252         (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
253         (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉)))
254         (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment []〉))
255    ]
256  ].
257
258(* jumps are of the proper size *)
259definition sigma_safe ≝
260 λprefix:list labelled_instruction.λlabels:label_map.λadded:ℕ.
261 λold_sigma:ppc_pc_map.λsigma:ppc_pc_map.
262 ∀i.i < |prefix| →
263 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in
264 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in
265 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in
266 ∀dest.is_jump_to instr dest →
267   let paddr ≝ lookup_def … labels dest 0 in
268   let addr ≝ bitvector_of_nat ? (if leb paddr (|prefix|) (* jump to address already known *)
269   then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)
270   else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
271   match j with
272   [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧
273       bool_to_Prop (¬is_call instr)
274   | absolute_jump ⇒  \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧
275       \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
276       bool_to_Prop (¬is_relative_jump instr)
277   | long_jump   ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧
278       \fst (absolute_jump_cond pc_plus_jmp_length addr) = false
279   ].
280 
281(* Definitions and theorems for the jump_length type (itself defined in Assembly) *)
282definition max_length: jump_length → jump_length → jump_length ≝
283  λj1.λj2.
284  match j1 with
285  [ long_jump   ⇒ long_jump
286  | absolute_jump ⇒
287    match j2 with
288    [ absolute_jump ⇒ absolute_jump
289    | _           ⇒ long_jump
290    ]
291  | short_jump  ⇒
292    match j2 with
293    [ short_jump ⇒ short_jump
294    | _          ⇒ long_jump
295    ]
296  ].
297
298lemma dec_jmple: ∀x,y:jump_length.Sum (jmple x y) (¬(jmple x y)).
299 #x #y cases x cases y /3 by inl, inr, nmk, I/
300qed.
301 
302lemma jmpleq_max_length: ∀ol,nl.
303  jmpleq ol (max_length ol nl).
304 #ol #nl cases ol cases nl
305 /2 by or_introl, or_intror, I/
306qed.
307
308lemma dec_eq_jump_length: ∀a,b:jump_length.Sum (a = b) (a ≠ b).
309  #a #b cases a cases b /2/
310  %2 @nmk #H destruct (H)
311qed.
312 
313(* The function that creates the label-to-address map *)
314definition create_label_map: ∀program:list labelled_instruction.
315  (Σlabels:label_map.
316    ∀l.occurs_exactly_once ?? l program →
317    And (bitvector_of_nat ? (lookup_def ?? labels l 0) =
318     address_of_word_labels_code_mem program l)
319    (lookup_def ?? labels l 0 < |program|)
320  ) ≝
321 λprogram.
322   \fst (create_label_cost_map program).
323 #l #Hl lapply (pi2 ?? (create_label_cost_map0 program)) @pair_elim
324 #labels #costs #EQ normalize nodelta #H whd in match create_label_cost_map;
325 normalize nodelta >EQ @(H l Hl)
326qed.
327
328(* General note on jump length selection: the jump displacement is added/replaced
329 * AFTER the fetch (and attendant PC increase), but we calculate before the
330 * fetch, which means that in the case of a short and medium jump we are 2
331 * bytes off and have to compensate.
332 * For the long jump we don't care, because the PC gets replaced integrally anyway. *)
333definition select_reljump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
334  Identifier → jump_length ≝
335  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
336  let pc ≝ \fst inc_sigma in
337  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
338  let paddr ≝ lookup_def … labels lbl 0 in
339  let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *)
340  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)
341  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
342  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
343  if sj_possible
344  then short_jump
345  else long_jump.
346
347definition select_call_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 ?
354    (if leb paddr ppc (* jump to address already known *)
355    then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)
356    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
357  let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in   
358  if aj_possible
359  then absolute_jump
360  else long_jump.
361 
362definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
363  Identifier → jump_length ≝
364  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
365  let pc ≝ \fst inc_sigma in
366  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
367  let paddr ≝ lookup_def … labels lbl 0 in
368  let addr ≝ bitvector_of_nat ? (if leb paddr ppc (* jump to address already known *)
369  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)
370  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)+added) in
371  let 〈sj_possible, disp〉 ≝ short_jump_cond pc_plus_jmp_length addr in
372  if sj_possible
373  then short_jump
374  else select_call_length labels old_sigma inc_sigma added ppc lbl.
375
376definition destination_of: preinstruction Identifier → option Identifier ≝
377  λi.
378  match i with
379  [ JC j     ⇒ Some ? j
380  | JNC j    ⇒ Some ? j
381  | JZ j     ⇒ Some ? j
382  | JNZ j    ⇒ Some ? j
383  | JB _ j   ⇒ Some ? j
384  | JBC _ j  ⇒ Some ? j
385  | JNB _ j  ⇒ Some ? j
386  | CJNE _ j ⇒ Some ? j
387  | DJNZ _ j ⇒ Some ? j
388  | _        ⇒ None ?
389  ].
390
391definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map →
392  ℕ → ℕ → preinstruction Identifier → option jump_length ≝
393  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi.
394  match destination_of i with
395  [ Some j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
396  | None       ⇒ None ?
397  ].
398
399(* The first step of the jump expansion: everything to short. *)
400definition jump_expansion_start:
401  ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
402  ∀labels:label_map.
403  Σpolicy:option ppc_pc_map.
404    match policy with
405    [ None ⇒ True
406    | Some p ⇒ And (And (And (And (And
407       (not_jump_default (pi1 ?? program) p)
408       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
409       (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (|program|)) (\snd p) 〈0,short_jump〉)))
410       (sigma_compact_unsafe program labels p))
411       (∀i.i ≤ |program| → ∃pc.
412         bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉))
413       (\fst p ≤ 2^16)         
414    ] ≝
415  λprogram.λlabels.
416  let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
417  (λprefix.Σpolicy:ppc_pc_map.And (And (And (And
418    (not_jump_default prefix policy)
419    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
420    (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (|prefix|)) (\snd policy) 〈0,short_jump〉)))
421    (sigma_compact_unsafe prefix labels policy))
422    (∀i.i ≤ |prefix| → ∃pc.
423      bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))
424  program
425  (λprefix.λx.λtl.λprf.λp.
426   let 〈pc,sigma〉 ≝ pi1 ?? p in
427   let 〈label,instr〉 ≝ x in
428   let isize ≝ instruction_size_jmplen short_jump instr in
429   〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (|prefix|))) 〈pc+isize,short_jump〉 sigma〉
430  ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in
431  if gtb (\fst (pi1 ?? final_policy)) 2^16 then
432    None ?
433  else
434    Some ? (pi1 ?? final_policy).
435[ / by I/
436| lapply p -p cases final_policy -final_policy #p #Hp #hg
437  @conj [ @Hp | @not_lt_to_le @ltb_false_to_not_lt @hg ]
438| @conj [ @conj [ @conj [ @conj
439  [ (* not_jump_default *) cases p -p #p cases p -p #pc #sigma #Hp
440    cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi
441    normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
442    [ >lookup_insert_miss
443      [ (* USE[pass]: not_jump_default *)
444        lapply (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
445        >nth_append_first
446        [ #H #H2 @H @H2
447        | @Hi
448        ]
449      | @bitvector_of_nat_abs
450        [ @(transitive_lt ??? Hi) @le_S_to_le]
451        [1,2: @(transitive_lt … (proj1 ?? (pi2 ?? program))) @le_S_S >prf >append_length
452          <plus_n_Sm @le_S_S @le_plus_n_r
453        | @lt_to_not_eq @le_S @Hi
454        ]
455      ]
456    | >Hi >lookup_insert_miss
457      [ #_ (* USE: everything is short *)
458        elim ((proj2 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl
459        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl
460      | @bitvector_of_nat_abs
461        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length @le_plus_n_r
462        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm @le_S_S
463          @le_plus_n_r
464        | @lt_to_not_eq @le_n
465        ]
466      ]
467    ]
468  | (* 0 ↦ 0 *)
469    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
470    >lookup_insert_miss
471    [ (* USE[pass]: 0 ↦ 0 *)
472      @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))
473    | @bitvector_of_nat_abs
474      [ / by /
475      | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S <plus_n_Sm
476        @le_S_S @le_plus_n_r
477      | @lt_to_not_eq / by /
478      ]
479    ]
480  ]
481  | (* fst p = pc *)
482    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
483    >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl
484  ]
485  | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;
486    cases p -p #p cases p -p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta
487    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
488    [ >lookup_opt_insert_miss
489      [ >lookup_opt_insert_miss
490        [ (* USE[pass]: policy_compact_unsafe *)
491          lapply (proj2 ?? (proj1 ?? Hp) i Hi)
492          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma))
493          cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %);
494          [ #_ normalize nodelta / by /
495          | #x cases x -x #pci #ji #EQi
496            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma))
497            cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma) in ⊢ (???% → %);
498            [ #_ normalize nodelta / by /
499            | #x cases x -x #pcSi #jSi #EQSi normalize nodelta >nth_append_first
500              [ / by /
501              | @Hi
502              ]
503            ]
504          ]
505        ]
506      ]
507      [2: lapply (le_S_to_le … Hi) -Hi #Hi]
508      @bitvector_of_nat_abs
509      [1,4: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <commutative_plus
510        @le_plus_a @Hi
511      |2,5: @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm
512        @le_S_S @le_plus_n_r
513      |3,6: @lt_to_not_eq @le_S_S @Hi
514      ]
515    | >lookup_opt_insert_miss
516      [ >Hi >lookup_opt_insert_hit normalize nodelta
517        (* USE: everything is short, fst p = pc *)
518        elim ((proj2 ?? Hp) (|prefix|) (le_n ?)) #pc #Hl
519        lapply (proj2 ?? (proj1 ?? (proj1 ?? Hp))) >Hl
520        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) #EQ normalize nodelta >nth_append_second
521        [ <minus_n_n whd in match (nth ????); >EQ @refl
522        | @le_n
523        ]
524      | @bitvector_of_nat_abs
525        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >Hi >prf @le_S_S >append_length <commutative_plus
526          @le_plus_a @le_n
527        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf @le_S_S >append_length <plus_n_Sm
528          @le_S_S @le_plus_n_r
529        | @lt_to_not_eq @le_S_S >Hi @le_n
530        ]
531      ]
532    ]
533  ]
534  | (* everything is short *) #i >append_length <commutative_plus #Hi normalize in Hi;
535    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
536    cases (le_to_or_lt_eq … Hi) -Hi #Hi
537    [ >lookup_opt_insert_miss
538      [ (* USE[pass]: everything is short *)
539        @((proj2 ?? Hp) i (le_S_S_to_le … Hi))
540      | @bitvector_of_nat_abs
541        [ @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length @le_S_S
542          >commutative_plus @le_plus_a @le_S_S_to_le @Hi
543        | @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf >append_length <plus_n_Sm
544          @le_S_S @le_S_S @le_plus_n_r
545        | @lt_to_not_eq @Hi
546        ]
547      ]
548    | >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr))
549      @refl
550    ]
551  ]
552| @conj [ @conj [ @conj [ @conj
553  [ #i cases i
554    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
555    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
556    ]
557  ] ]
558  >lookup_insert_hit @refl
559  | #i cases i
560    [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n
561    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
562    ]
563  ]
564  | #i cases i
565    [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl
566    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
567    ]
568  ]
569]
570qed.
571
572(* NOTE: we only compare the first elements here because otherwise the
573 * added = 0 → policy_equal property of jump_expansion_step doesn't hold:
574 * if we have not added anything to the pc, we only know the PC hasn't changed,
575 * there might still have been a short/medium jump change *)
576definition sigma_pc_equal ≝
577  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
578  (∀n.n ≤ |program| →
579    \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) =
580    \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)).
581
582definition sigma_jump_equal ≝
583  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
584  (∀n.n < |program| →
585    \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) =
586    \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)).
587   
588definition nec_plus_ultra ≝
589  λprogram:list labelled_instruction.λp:ppc_pc_map.
590  ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) →
591  \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump).
592 
593(*include alias "common/Identifiers.ma".*)
594include alias "ASM/BitVector.ma".
595include alias "basics/lists/list.ma".
596include alias "arithmetics/nat.ma".
597include alias "basics/logic.ma".
598
599lemma jump_length_equal_max: ∀a,b,i.
600  is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i →
601  (max_length a b) = a.
602 #a #b #i cases i
603 [1: #pi cases pi
604   try (#x #y #H #EQ) try (#x #H #EQ) try (#H #EQ) cases H
605   cases a in EQ; cases b #EQ try %
606   try (normalize in EQ; destruct(EQ) @False)
607   try (lapply EQ @(subaddressing_mode_elim … x) #w #EQ normalize in EQ; destruct(EQ) @False)
608   lapply EQ -EQ cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w
609   try (#EQ normalize in EQ; destruct(EQ) @False)
610   @(subaddressing_mode_elim … a1) #w
611   #EQ normalize in EQ; destruct(EQ)
612  |2,3,6: #x [3: #y] #H cases H
613  |4,5: #id #_ cases a cases b #H try % normalize in H; destruct(H)
614 ]
615qed.
616
617lemma jump_length_le_max: ∀a,b,i.is_jump i →
618  instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i.
619 #a #b #i cases i
620 [2,3,6: #x [3: #y] #H cases H
621 |4,5: #id #_ cases a cases b / by le_n/
622 |1: #pi cases pi
623    try (#x #y #H) try (#x #H) try (#H) cases H
624    -H cases a cases b @leb_true_to_le try %
625    try (@(subaddressing_mode_elim … x) #w % @False)
626    cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try %
627    @(subaddressing_mode_elim … a1) #w %
628 ]
629qed.
630
631lemma equal_compact_unsafe_compact: ∀program:(Σl.(S (|l|)) < 2^16 ∧ is_well_labelled_p l).
632  ∀old_sigma.∀sigma.
633  sigma_pc_equal program old_sigma sigma →
634  sigma_safe program (create_label_map program) 0 old_sigma sigma →
635  sigma_compact_unsafe program (create_label_map program) sigma →
636  sigma_compact program (create_label_map program) sigma.
637  #program cases program -program #program #Hprogram #old_sigma #sigma #Hequal
638  #Hsafe #Hcp_unsafe #i #Hi
639  lapply (Hcp_unsafe i Hi) lapply (Hsafe i Hi)
640  inversion (lookup_opt … (bitvector_of_nat ? i) (\snd sigma))
641  [ / by /
642  | #x cases x -x #x1 #x2 #EQ
643    cases (lookup_opt … (bitvector_of_nat ? (S i)) (\snd sigma))
644    [ / by /
645    | #y cases y -y #y1 #y2 normalize nodelta #H #H2
646      (*CSC: make a lemma here; to shorten the proof, reimplement the
647        safe case so that it also does a pattern matching on the jump_length
648        type *)
649      cut (instruction_size_jmplen x2
650       (\snd (nth i ? program 〈None ?, Comment []〉)) =
651       instruction_size … (bitvector_of_nat ? i)
652       (\snd (nth i ? program 〈None ?, Comment []〉)))
653      [5: #H3 <H3 @H2
654      |4: whd in match (instruction_size_jmplen ??);
655          whd in match (instruction_size …);
656          whd in match (assembly_1_pseudoinstruction …);
657          whd in match (expand_pseudo_instruction …);
658          normalize nodelta whd in match (append …) in H; lapply H
659          inversion (nth i ? program 〈None ?,Comment []〉)
660          #lbl #instr cases instr
661          [2,3,6: #x [3: #y] normalize nodelta #H #_ %
662          |4,5: #x >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) #Heq #Hj
663            lapply (Hj x (refl ? x)) -Hj normalize nodelta
664            >add_bitvector_of_nat_plus <(plus_n_Sm i 0) <plus_n_O
665            cases x2 normalize nodelta
666            [1,4: whd in match short_jump_cond; normalize nodelta
667              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
668              [1,3: cases (create_label_map program) #clm #Hclm
669                @le_S_to_le @(proj2 ?? (Hclm x ?))
670                [1: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
671                |2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
672                [1,4: >nat_of_bitvector_bitvector_of_nat_inverse
673                  [2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
674                |2,5: whd in match fetch_pseudo_instruction; normalize nodelta
675                  >nth_safe_nth
676                  [1,3: >nat_of_bitvector_bitvector_of_nat_inverse
677                    [1,3: >Heq / by refl/
678                    |2,4: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
679                    ]
680                  ]
681                |3,6: / by /
682                ]
683              |2,4: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
684              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
685              #result #flags normalize nodelta
686              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
687              cases (get_index' bool 2 0 flags) normalize nodelta
688              [3,4: #H cases (proj2 ?? H)
689              |1,2: cases (eq_bv 9 upper ?)
690                [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3)
691                |1,3: #_ normalize nodelta @refl
692                ]
693              ]
694              ]
695            |2,3,5,6: whd in match short_jump_cond; whd in match absolute_jump_cond;
696              cut (lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
697              [1,3,5,7: cases (create_label_map program) #clm #Hclm
698                @le_S_to_le @(proj2 ?? (Hclm x ?))
699                [1,2: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Jmp x) ??)
700                |3,4: @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (Call x) ??)]
701                [1,4,7,10: >nat_of_bitvector_bitvector_of_nat_inverse
702                  [2,4,6,8: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
703                |2,5,8,11: whd in match fetch_pseudo_instruction; normalize nodelta
704                  >nth_safe_nth
705                  [1,3,5,7: >nat_of_bitvector_bitvector_of_nat_inverse
706                    [1,3,5,7: >Heq / by refl/
707                    |*: @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi
708                    ]
709                  ]
710                |*: / by /
711                ]
712              |*: #H >(le_to_leb_true … H) normalize nodelta <plus_n_O
713              normalize nodelta cases (vsplit bool 5 11 ?) #addr1 #addr2
714              cases (vsplit bool 5 11 ?) #pc1 #pc2 normalize nodelta
715              cases (sub_16_with_carry (bitvector_of_nat ??) (bitvector_of_nat ??) false)
716              #result #flags normalize nodelta
717              cases (vsplit bool 9 7 result) #upper #lower normalize nodelta
718              cases (get_index' bool 2 0 flags) normalize nodelta
719              #H
720              [1,2,5,6: >(proj2 ?? (proj1 ?? H)) >(proj1 ?? (proj1 ?? H)) normalize nodelta @refl
721              |*: >(proj1 ?? H) >(proj2 ?? H) normalize nodelta @refl
722              ]]]
723          |1: normalize nodelta
724              cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a))
725              [#A #B * / by refl/] #fst_foo
726              cut (∀x.
727                    instruction_has_label x (\snd  (nth i labelled_instruction program 〈None (identifier ASMTag),Comment []〉)) →
728               lookup_def ?? (create_label_map program) x 0 ≤ (|program|))
729              [#x #Heq cases (create_label_map program) #clm #Hclm
730               @le_S_to_le @(proj2 ?? (Hclm x ?))
731               @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??)
732               [ >nat_of_bitvector_bitvector_of_nat_inverse
733                 [2: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi
734               | whd in match fetch_pseudo_instruction; normalize nodelta
735                 >nth_safe_nth
736                 [ >nat_of_bitvector_bitvector_of_nat_inverse
737                   [ @pair_elim // ]
738                   @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi ]
739                 | assumption ]] #lookup_in_program
740              -H #pi cases pi
741              try (#y #x #Heq #H) try (#x #Heq #H) try (#Heq #H) try % lapply H -H
742              normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉)
743              #Hj lapply (Hj x (refl ? x)) -Hj
744              whd in match expand_relative_jump; normalize nodelta
745              whd in match expand_relative_jump_internal; normalize nodelta
746              whd in match expand_relative_jump_unsafe; normalize nodelta
747              whd in match expand_relative_jump_internal_unsafe;
748              normalize nodelta >(add_bitvector_of_nat_plus ? i 1)
749              <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta
750              [1,4,7,10,13,16,19,22,25:
751                >fst_foo @pair_elim #sj_possible #disp #H #H2
752                @(pair_replace ?????????? (eq_to_jmeq … H))
753                [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …))
754                  try % >Heq % ]
755                >(proj1 ?? H2) try (@refl) normalize nodelta
756                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
757                | cases y * #sth #sth2 @(subaddressing_mode_elim … sth)
758                  @(subaddressing_mode_elim … sth2) #x [3,4: #x2] %
759                ]
760              |2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs
761              ]
762              * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H
763              @(pair_replace ?????????? (eq_to_jmeq … H))
764                [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …))
765                  try % >Heq % ]
766                #H2 >H2 try (@refl) normalize nodelta
767                [1,2,3,5: @(subaddressing_mode_elim … y) #w %
768                | cases y * #sth #sth2 @(subaddressing_mode_elim … sth2) #w
769                  [1,2: %] whd in match (map ????); whd in match (flatten ??);
770                  whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%);
771                  >length_append >length_append %]]]]]
772qed.
773
774lemma instruction_size_irrelevant: ∀i.
775  ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i.
776 #i cases i
777 [2,3,6: #x [3: #y] #Hj #j1 #j2 %
778 |4,5: #x #Hi cases Hi
779 |1: #pi cases pi try (#x #y #Hj #j1 #j2) try (#y #Hj #j1 #j2) try (#Hj #j1 #j2)
780     try % cases Hj ]
781qed.
Note: See TracBrowser for help on using the repository browser.