source: src/ASM/PolicyFront.ma @ 2047

Last change on this file since 2047 was 2047, checked in by mulligan, 7 years ago

Big bugs in policy calculations found. Waiting for Jaap's commit.

File size: 29.1 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 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
327  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
328  if eq_bv ? upper (zero 8)
329  then short_jump
330  else long_jump.
331
332definition select_call_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
333  Identifier → jump_length ≝
334  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
335  let pc ≝ \fst inc_sigma in
336  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
337  let paddr ≝ lookup_def ? ? labels lbl 0 in
338  let addr ≝
339    if leb ppc paddr (* forward jump *)
340    then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉)
341            + added
342    else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉) in
343  let 〈fst_5_addr, rest_addr〉 ≝ vsplit ? 5 11 (bitvector_of_nat ? addr) in
344  let 〈fst_5_pc, rest_pc〉 ≝ vsplit ? 5 11 pc_plus_jmp_length in
345  if eq_bv ? fst_5_addr fst_5_pc
346  then medium_jump
347  else long_jump.
348 
349definition select_jump_length: label_map → ppc_pc_map → ppc_pc_map → ℕ → ℕ →
350  Identifier → jump_length ≝
351  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λlbl.
352  let pc ≝ \fst inc_sigma in
353  let pc_plus_jmp_length ≝ bitvector_of_nat ? (pc+2) in
354  let paddr ≝ lookup_def … labels lbl 0 in
355  let addr ≝ bitvector_of_nat ? (if leb ppc paddr (* forward jump *)
356  then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added
357  else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in
358  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
359  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
360  if eq_bv ? upper (zero 8)
361  then short_jump
362  else select_call_length labels old_sigma inc_sigma added ppc lbl.
363 
364definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map →
365  ℕ → ℕ → preinstruction Identifier → option jump_length ≝
366  λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi.
367  match i with
368  [ JC j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
369  | JNC j    ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
370  | JZ j     ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
371  | JNZ j    ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
372  | JB _ j   ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
373  | JBC _ j  ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
374  | JNB _ j  ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
375  | CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
376  | DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j)
377  | _        ⇒ None ?
378  ].
379
380lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x).
381#i cases i
382[#id cases id
383 [1,2,3,6,7,33,34:
384  #x #y %2 whd in match (is_jump ?); /2 by nmk/
385 |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32:
386  #x %2 whd in match (is_jump ?); /2 by nmk/
387 |35,36,37: %2 whd in match (is_jump ?); /2 by nmk/
388 |9,10,14,15: #x %1 / by I/
389 |11,12,13,16,17: #x #y %1 / by I/
390 ]
391|2,3: #x %2 /2 by nmk/
392|4,5: #x %1 / by I/
393|6: #x #y %2 /2 by nmk/
394]
395qed.
396
397lemma geb_to_leb: ∀a,b:ℕ.geb a b = leb b a.
398  #a #b / by refl/
399qed.
400
401lemma nth_last: ∀A,a,l.
402  nth (|l|) A l a = a.
403 #A #a #l elim l
404 [ / by /
405 | #h #t #Hind whd in match (nth ????); whd in match (tail ??); @Hind
406 ]
407qed.
408
409(* The first step of the jump expansion: everything to short. *)
410definition jump_expansion_start:
411  ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16).
412  ∀labels:label_map.
413  Σpolicy:option ppc_pc_map.
414    match policy with
415    [ None ⇒ True
416    | Some p ⇒
417       And (And (And (And (And (And (out_of_program_none (pi1 ?? program) p)
418       (jump_not_in_policy (pi1 ?? program) p))
419       (policy_compact_unsafe program labels p))
420       (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0))
421       (∀i.i ≤ |program| → ∃pc.
422         bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉))
423       (bvt_lookup_opt … (bitvector_of_nat ? (|program|)) (\snd p) =
424         Some ? 〈\fst p,short_jump〉))
425       (\fst p < 2^16)
426    ] ≝
427  λprogram.λlabels.
428  let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction)
429  (λprefix.Σpolicy:ppc_pc_map.
430    And (And (And (And (And (out_of_program_none prefix policy)
431    (jump_not_in_policy prefix policy))
432    (policy_compact_unsafe prefix labels policy))
433    (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0))
434    (∀i.i ≤ |prefix| → ∃pc.
435      bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉))
436    (bvt_lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd policy) =
437      Some ? 〈\fst policy,short_jump〉))
438  program
439  (λprefix.λx.λtl.λprf.λp.
440   let 〈pc,sigma〉 ≝ pi1 ?? p in
441   let 〈label,instr〉 ≝ x in
442   let isize ≝ instruction_size_jmplen short_jump instr in
443   〈pc + isize, bvt_insert … (bitvector_of_nat 16 (S (|prefix|))) 〈pc+isize,short_jump〉 sigma〉
444  ) 〈0, bvt_insert ?? (bitvector_of_nat 16 0) 〈0,short_jump〉 (Stub ??)〉 in
445  if geb (\fst (pi1 ?? final_policy)) 2^16 then
446    None ?
447  else
448    Some ? (pi1 ?? final_policy).
449[ / by I/
450| lapply p -p generalize in match (foldl_strong ?????); * #p #Hp #hg
451  @conj [ @Hp | @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ]
452| @conj [ @conj [ @conj [ @conj [ @conj
453  [ (* out_of_program_none *)
454    #i #Hi2 >append_length <commutative_plus @conj
455    [ (* → *) #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi #Hi
456      cases p -p #p cases p -p #pc #p #Hp cases x -x #l #pi
457      [ >lookup_opt_insert_miss
458        [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2))
459          @le_S_to_le @le_S_to_le @Hi
460        | @bitvector_of_nat_abs
461          [ @Hi2
462          | @(transitive_lt … Hi2) @le_S_to_le @Hi
463          | @sym_neq @lt_to_not_eq @le_S_to_le @Hi
464          ]
465        ]
466      | >lookup_opt_insert_miss
467        [ <Hi
468          @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (|prefix|))) ?))
469          [ >Hi @Hi2
470          | @le_S @le_n
471          ]
472        | @bitvector_of_nat_abs
473          [ @Hi2
474          | @(transitive_lt … Hi2) <Hi @le_n
475          | @sym_neq @lt_to_not_eq <Hi @le_n
476          ]
477        ]
478      ]
479    | (* ← *) cases p -p #p cases p -p #pc #p #Hp cases x in prf; -x #l #pi #prf
480      normalize nodelta cases (decidable_eq_nat i (S (|prefix|)))
481      [ #Hi >Hi >lookup_opt_insert_hit #H destruct (H)
482      | #Hi >lookup_opt_insert_miss
483        [ #Hl
484          elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl))
485          [ #Hi3 @Hi3
486          | #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi
487          ]
488        | @bitvector_of_nat_abs
489          [ @Hi2
490          | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length
491            <plus_n_Sm @le_S_S @le_plus_n_r
492          | @Hi
493          ]
494        ]
495      ]
496    ]
497  | (* jump_not_in_policy *) cases p -p #p cases p -p #pc #sigma #Hp
498    cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi
499    normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
500    [ >lookup_insert_miss
501      [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi)
502        >nth_append_first
503        [ #H #H2 @H @H2
504        | @Hi
505        ]
506      | @bitvector_of_nat_abs
507        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length <commutative_plus >plus_n_Sm
508          @le_plus_a @le_S @Hi
509        | @(transitive_lt … (pi2 ?? program)) @le_S_S >prf >append_length <plus_n_Sm @le_S_S
510          @le_plus_n_r
511        | @lt_to_not_eq @le_S @Hi
512        ]
513      ]
514    | >Hi >lookup_insert_miss
515      [ #_ elim (proj2 ?? (proj1 ?? Hp) (|prefix|) (le_n (|prefix|))) #pc #Hl
516        >(lookup_opt_lookup_hit … Hl 〈0,short_jump〉) @refl
517      | @bitvector_of_nat_abs
518        [ @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length @le_plus_n_r
519        | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm @le_S_S
520          @le_plus_n_r
521        | @lt_to_not_eq @le_n
522        ]
523      ]
524    ]
525  ]
526  | (* policy_compact_unsafe *) #i >append_length <commutative_plus #Hi normalize in Hi;
527    cases p -p #p cases p -p #fpc #sigma #Hp cases x #lbl #instr normalize nodelta
528    cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
529    [ >lookup_opt_insert_miss
530      [ >lookup_opt_insert_miss
531        [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)
532          lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma))
533          cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %);
534          [ #_ normalize nodelta / by /
535          | #x cases x -x #pci #ji #EQi
536            lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma))
537            cases (bvt_lookup_opt … (bitvector_of_nat ? (S i)) sigma) in ⊢ (???% → %);
538            [ #_ normalize nodelta / by /
539            | #x cases x -x #pcSi #jSi #EQSi normalize nodelta >nth_append_first
540              [ / by /
541              | @Hi
542              ]
543            ]
544          ]
545        ]
546      ]
547      [2: lapply (le_S_to_le … Hi) -Hi #Hi]
548      @bitvector_of_nat_abs
549      [1,4: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <commutative_plus
550        @le_plus_a @Hi
551      |2,5: @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
552        @le_S_S @le_plus_n_r
553      |3,6: @lt_to_not_eq @le_S_S @Hi
554      ]
555    | >lookup_opt_insert_miss
556      [ >Hi >lookup_opt_insert_hit normalize nodelta
557        >(proj2 ?? Hp) normalize nodelta >nth_append_second
558        [ <minus_n_n whd in match (nth ????); @refl
559        | @le_n
560        ]
561      | @bitvector_of_nat_abs
562        [ @(transitive_lt … (pi2 ?? program)) >Hi >prf @le_S_S >append_length <commutative_plus
563          @le_plus_a @le_n
564        | @(transitive_lt … (pi2 ?? program)) >prf @le_S_S >append_length <plus_n_Sm
565          @le_S_S @le_plus_n_r
566        | @lt_to_not_eq @le_S_S >Hi @le_n
567        ]
568      ]
569    ]
570  ]
571  | (* lookup 0 = 0 *)
572    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
573    >lookup_insert_miss
574    [ @(proj2 ?? (proj1 ?? (proj1 ?? Hp)))
575    | @bitvector_of_nat_abs
576      [ / by /
577      | @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S <plus_n_Sm
578        @le_S_S @le_plus_n_r
579      | @lt_to_not_eq / by /
580      ]
581    ]
582  ]
583  | (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi;
584    cases p -p #p cases p -p #pc #sigma #Hp cases x #lbl #instr normalize nodelta
585    cases (le_to_or_lt_eq … Hi) -Hi #Hi
586    [ >lookup_opt_insert_miss
587      [ @(proj2 ?? (proj1 ?? Hp) i (le_S_S_to_le … Hi))
588      | @bitvector_of_nat_abs
589        [ @(transitive_lt … (pi2 ?? program)) >prf >append_length @le_S_S >commutative_plus
590          @le_plus_a @le_S_S_to_le @Hi
591        | @(transitive_lt … (pi2 ?? program)) >prf >append_length <plus_n_Sm @le_S_S
592          @le_S_S @le_plus_n_r
593        | @lt_to_not_eq @Hi
594        ]
595      ]
596    | >Hi >lookup_opt_insert_hit @(ex_intro ?? (pc+instruction_size_jmplen short_jump instr))
597      @refl
598    ]
599  ]
600  | (* lookup at the end *) cases p -p #p cases p -p #pc #sigma #Hp cases x
601    #lbl #instr >append_length <plus_n_Sm <plus_n_O >lookup_opt_insert_hit
602    / by refl/
603  ]
604| @conj [ @conj [ @conj [ @conj [ @conj
605  [ #i cases i
606    [ #Hi2 @conj
607      [ (* → *) #Hi @⊥ @(absurd ? Hi) @le_to_not_lt / by /
608      | (* ← *) >lookup_opt_insert_hit #Hl destruct (Hl)
609      ]
610    | -i #i #Hi2 @conj
611      [ #Hi >lookup_opt_insert_miss
612        [ / by refl/
613        | @bitvector_of_nat_abs
614          [ @Hi2
615          | / by /
616          | @sym_neq @lt_to_not_eq / by /
617          ]
618        ]
619      | #_ @le_S_S @le_O_n
620      ]
621    ]
622  | #i cases i
623    [ #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
624    | -i #i #Hi #Hj @⊥ @(absurd … Hi) @not_le_Sn_O
625    ]
626  ]
627  | #i cases i
628    [ #Hi @⊥ @(absurd … Hi) @le_to_not_lt @le_n
629    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
630    ]
631  ]
632  | >lookup_insert_hit @refl
633  ]
634  | #i cases i
635    [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl
636    | -i #i #Hi @⊥ @(absurd … Hi) @not_le_Sn_O
637    ]
638  ]
639  | >lookup_opt_insert_hit @refl
640  ]
641]
642qed.
643
644definition policy_equal ≝
645  λprogram:list labelled_instruction.λp1,p2:ppc_pc_map.
646  (* \fst p1 = \fst p2 ∧ *)
647  (∀n:ℕ.n < |program| →
648    let pc1 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉 in
649    let pc2 ≝ bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉 in
650    \snd pc1 = \snd pc2).
651   
652definition nec_plus_ultra ≝
653  λprogram:list labelled_instruction.λp:ppc_pc_map.
654  ¬(∀i.i < |program| → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) →
655  \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump).
656 
657(*include alias "common/Identifiers.ma".*)
658include alias "ASM/BitVector.ma".
659include alias "basics/lists/list.ma".
660include alias "arithmetics/nat.ma".
661include alias "basics/logic.ma".
662
663lemma blerpque: ∀a,b,i.
664  is_jump i → instruction_size_jmplen (max_length a b) i = instruction_size_jmplen a i →
665  (max_length a b) = a.
666 #a #b #i cases i
667 [1: #pi cases pi
668   [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:
669     try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H
670   |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %)
671     try (#abs normalize in abs; destruct (abs) @I)
672     cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I)
673     try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I)
674     cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w
675     try ( #abs normalize in abs; destruct (abs) @I)
676     @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs)
677   ]
678  |2,3,6: #x [3: #y] #H cases H
679  |4,5: #id #_ cases a cases b
680    [2,3,4,6,11,12,13,15: normalize #H destruct (H)
681    |1,5,7,8,9,10,14,16,17,18: #H / by refl/
682    ]
683  ]
684qed.
685
686lemma etblorp: ∀a,b,i.is_jump i →
687  instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i.
688 #a #b #i cases i
689 [2,3,6: #x [3: #y] #H cases H
690 |4,5: #id #_ cases a cases b / by le_n/
691 |1: #pi cases pi
692   [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:
693     [1,2,3,6,7,24,25: #x #y
694     |4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x]
695     #H cases H
696   |9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y]
697     #_ cases a cases b
698     [2,3: cases x #ad cases ad
699       [15,34: #b #Hb / by le_n/
700       |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
701     |1,4,5,6,7,8,9: / by le_n/
702     |11,12: cases x #ad cases ad
703       [15,34: #b #Hb / by le_n/
704       |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
705     |10,13,14,15,16,17,18: / by le_n/
706     |20,21: cases x #ad cases ad
707       [15,34: #b #Hb / by le_n/
708       |1,2,3,4,8,9,16,17,18,19,20,21,22,23,27,28,35,36,37,38: #b] #Hb cases Hb
709     |19,22,23,24,25,26,27: / by le_n/
710     |29,30: cases x #ad cases ad #a1 #a2
711       [1,3: cases a2 #ad2 cases ad2
712         [1,8,20,27: #b #Hb / by le_n/
713         |2,3,4,9,15,16,17,18,19,21,22,23,28,34,35,36,37,38: #b] #Hb cases Hb
714       |2,4: cases a1 #ad1 cases ad1
715         [2,4,21,23: #b #Hb / by le_n/
716         |1,3,8,9,15,16,17,18,19,20,22,27,28,34,35,36,37,38: #b] #Hb cases Hb
717       ]
718     |28,31,32,33,34,35,36: / by le_n/
719     |38,39: cases x #ad cases ad
720       [1,4,20,23: #b #Hb / by le_n/
721       |2,3,8,9,15,16,17,18,19,21,22,27,28,34,35,36,37,38: #b] #Hb cases Hb
722     |37,40,41,42,43,44,45: / by le_n/
723     |46,47,48,49,50,51,52,53,54: / by le_n/
724     |55,56,57,58,59,60,61,62,63: / by le_n/
725     |64,65,66,67,68,69,70,71,72: / by le_n/
726     |73,74,75,76,77,78,79,80,81: / by le_n/
727     ]
728   ]
729 ]
730qed.
731
732lemma minus_zero_to_le: ∀n,m:ℕ.n - m = 0 → n ≤ m.
733 #n
734 elim n
735 [ #m #_ @le_O_n
736 | #n' #Hind #m cases m
737   [ #H -n whd in match (minus ??) in H; >H @le_n
738   | #m' -m #H whd in match (minus ??) in H; @le_S_S @Hind @H
739   ]
740 ]
741qed.
742
743lemma plus_zero_zero: ∀n,m:ℕ.n + m = 0 → m = 0.
744 #n #m #Hn @sym_eq @le_n_O_to_eq <Hn >commutative_plus @le_plus_n_r
745qed.
746
747(* (Intermediate) policy safety *)
748definition short_jump_cond: Word → Word → pseudo_instruction → Prop ≝
749  λpc_plus_jmp_length.λaddr.λinstr.
750  let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in
751  let 〈upper, lower〉 ≝ vsplit ? 8 8 result in
752    if flags then
753      eq_bv 8 upper [[true;true;true;true;true;true;true;true]] = true
754    else
755      eq_bv 8 upper (zero 8) = true.
756
757definition medium_jump_cond: Word → Word → pseudo_instruction → Prop ≝
758  λpc_plus_jmp_length.λaddr.λinstr.
759  let 〈fst_5_addr, rest_addr〉 ≝ vsplit bool 5 11 addr in
760  let 〈fst_5_pc, rest_pc〉 ≝ vsplit bool 5 11 pc_plus_jmp_length in
761  eq_bv 5 fst_5_addr fst_5_pc = true.
762 
763definition policy_safe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝
764 λprogram.λlabels.λsigma.
765 ∀i.i < |program| →
766 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉 in
767 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in
768 let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in
769 ∀dest.is_jump_to instr dest →
770   let paddr ≝ lookup_def … labels dest 0 in
771   let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,short_jump〉)) in
772   match j with
773   [ short_jump ⇒ short_jump_cond pc_plus_jmp_length addr instr ∧ ¬is_call instr
774   | medium_jump ⇒  medium_jump_cond pc_plus_jmp_length addr instr ∧
775       ¬short_jump_cond pc_plus_jmp_length addr instr ∧ ¬is_relative_jump instr
776   | long_jump   ⇒ ¬short_jump_cond pc_plus_jmp_length addr instr ∧
777       ¬medium_jump_cond pc_plus_jmp_length addr instr
778   ].
779
780lemma not_true_is_false:
781  ∀b:bool.b ≠ true → b = false.
782 #b cases b
783 [ #H @⊥ @(absurd ?? H) @refl
784 | #H @refl
785 ]
786qed.
Note: See TracBrowser for help on using the repository browser.