source: src/ASM/PolicyFront.ma @ 3341

Last change on this file since 3341 was 3103, checked in by mckinna, 7 years ago

Simplified "include" dependencies

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