Changeset 2101 for src/ASM/PolicyFront.ma
 Timestamp:
 Jun 19, 2012, 4:43:50 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2059 r2101 13 13 (* The different properties that we want/need to prove at some point *) 14 14 (* During our iteration, everything not yet seen is None, and vice versa *) 15 definition 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 16i) (\snd sigma) = None ?).15 definition 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 18 19 19 (* If instruction i is a jump, then there will be something in the policy at … … 77 77 ]. 78 78 79 definition jump_not_in_policy: list labelled_instruction → ppc_pc_map → Prop ≝80 λprefix .λsigma.79 definition not_jump_default ≝ 80 λprefix:list labelled_instruction.λsigma:ppc_pc_map. 81 81 ∀i:ℕ.i < prefix → 82 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 83 \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump. 84 93 85 (* Between two policies, jumps cannot decrease *) 94 86 definition jmpeqb: jump_length → jump_length → bool ≝ … … 96 88 match j1 with 97 89 [ short_jump ⇒ match j2 with [ short_jump ⇒ true  _ ⇒ false ] 98  medium_jump ⇒ match j2 with [ medium_jump ⇒ true  _ ⇒ false ]90  absolute_jump ⇒ match j2 with [ absolute_jump ⇒ true  _ ⇒ false ] 99 91  long_jump ⇒ match j2 with [ long_jump ⇒ true  _ ⇒ false ] 100 92 ]. … … 114 106  _ ⇒ True 115 107 ] 116  medium_jump ⇒108  absolute_jump ⇒ 117 109 match j2 with 118 110 [ long_jump ⇒ True … … 125 117 λj1.λj2.jmple j1 j2 ∨ j1 = j2. 126 118 127 definition 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 119 definition 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 133 124 (*opc ≤ pc ∧*) jmpleq oj j. 134 125 … … 139 130 match jmp_len with 140 131 [ short_jump ⇒ [ RealInstruction (i (RELATIVE (zero 8))) ] 141  medium_jump ⇒ [ ] (* this should not happen *)132  absolute_jump ⇒ [ ] (* this should not happen *) 142 133  long_jump ⇒ 143 134 [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2))); … … 202 193 match jmp_len with 203 194 [ short_jump ⇒ [ ] (* this should not happen *) 204  medium_jump ⇒ [ ACALL (ADDR11 (zero 11)) ]195  absolute_jump ⇒ [ ACALL (ADDR11 (zero 11)) ] 205 196  long_jump ⇒ [ LCALL (ADDR16 (zero 16)) ] 206 197 ] … … 211 202 match jmp_len with 212 203 [ short_jump ⇒ [ SJMP (RELATIVE (zero 8)) ] 213  medium_jump ⇒ [ AJMP (ADDR11 (zero 11)) ]204  absolute_jump ⇒ [ AJMP (ADDR11 (zero 11)) ] 214 205  long_jump ⇒ [ LJMP (ADDR16 (zero 16)) ] 215 206 ] … … 222 213 qed. 223 214 224 definition policy_compact_unsafe: list labelled_instruction → label_map → ppc_pc_map → Prop ≝225 λpr ogram.λlabels.λsigma.226 ∀n :ℕ.n < program →215 definition sigma_compact_unsafe ≝ 216 λprefix:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. 217 ∀n.n < prefix → 227 218 match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with 228 219 [ None ⇒ False … … 231 222 [ None ⇒ False 232 223  Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in 233 pc1 = pc + instruction_size_jmplen j (\snd (nth n ? pr ogram〈None ?, Comment []〉))224 pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment []〉)) 234 225 ] 235 226 ]. 236 227 237 (* new safety condition: policycorresponds to program and resulting program is compact *)238 definition policy_compact: list labelled_instruction → label_map → ppc_pc_map → Prop≝239 λprogram .λlabels.λsigma.240 ∀n :ℕ.n < program →228 (* new safety condition: sigma corresponds to program and resulting program is compact *) 229 definition sigma_compact ≝ 230 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. 231 ∀n.n < program → 241 232 match bvt_lookup_opt … (bitvector_of_nat ? n) (\snd sigma) with 242 233 [ None ⇒ False … … 251 242 ] 252 243 ]. 244 245 (* jumps are of the proper size *) 246 definition sigma_safe ≝ 247 λprefix:list labelled_instruction.λlabels:label_map.λadded:ℕ. 248 λold_sigma:ppc_pc_map.λsigma:ppc_pc_map. 249 ∀i.i < prefix → 250 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in 251 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in 252 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in 253 ∀dest.is_jump_to instr dest → 254 let paddr ≝ lookup_def … labels dest 0 in 255 let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *) 256 then \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd old_sigma) 〈0,short_jump〉) + added 257 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in 258 match j with 259 [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧ 260 ¬is_call instr 261  absolute_jump ⇒ \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧ 262 \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 263 ¬is_relative_jump instr 264  long_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 265 \fst (absolute_jump_cond pc_plus_jmp_length addr) = false 266 ]. 267 253 268 254 269 (* Definitions and theorems for the jump_length type (itself defined in Assembly) *) … … 257 272 match j1 with 258 273 [ long_jump ⇒ long_jump 259  medium_jump ⇒274  absolute_jump ⇒ 260 275 match j2 with 261 [ medium_jump ⇒ medium_jump276 [ absolute_jump ⇒ absolute_jump 262 277  _ ⇒ long_jump 263 278 ] … … 283 298 %2 @nmk #H destruct (H) 284 299 qed. 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 prefix291 (λ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 300 298 301 (* The function that creates the labeltoaddress map *) … … 340 343 + added 341 344 else \fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd inc_sigma) 〈0,short_jump〉)) in 342 let 〈 mj_possible, disp〉 ≝ medium_jump_cond pc_plus_jmp_length addr in343 if mj_possible344 then medium_jump345 let 〈aj_possible, disp〉 ≝ absolute_jump_cond pc_plus_jmp_length addr in 346 if aj_possible 347 then absolute_jump 345 348 else long_jump. 346 349 … … 411 414 match policy with 412 415 [ None ⇒ True 413  Some p ⇒ 414 And (And (And (And (And (And(out_of_program_none (pi1 ?? program) p)415 ( jump_not_in_policy(pi1 ?? program) p))416 ( policy_compact_unsafe program labels p))416  Some p ⇒ And (And (And (And (And (And (And 417 (out_of_program_none (pi1 ?? program) p) 418 (not_jump_default (pi1 ?? program) p)) 419 (sigma_compact_unsafe program labels p)) 417 420 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd p) 〈0,short_jump〉) = 0)) 421 (\fst p = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd p) 〈0,short_jump〉))) 418 422 (∀i.i ≤ program → ∃pc. 419 423 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd p) = Some ? 〈pc,short_jump〉)) 420 (bvt_lookup_opt … (bitvector_of_nat ? (program)) (\snd p) = 421 Some ? 〈\fst p,short_jump〉)) 424 (bvt_lookup_opt … (bitvector_of_nat ? (program)) (\snd p) = Some ? 〈\fst p,short_jump〉)) 422 425 (\fst p < 2^16) 423 426 ] ≝ 424 427 λprogram.λlabels. 425 428 let final_policy ≝ foldl_strong (option Identifier × pseudo_instruction) 426 (λprefix.Σpolicy:ppc_pc_map. 427 And (And (And (And (And(out_of_program_none prefix policy)428 ( jump_not_in_policyprefix policy))429 ( policy_compact_unsafe prefix labels policy))429 (λprefix.Σpolicy:ppc_pc_map.And (And (And (And (And (And 430 (out_of_program_none prefix policy) 431 (not_jump_default prefix policy)) 432 (sigma_compact_unsafe prefix labels policy)) 430 433 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd policy) 〈0,short_jump〉) = 0)) 434 (\fst policy = \fst (bvt_lookup … (bitvector_of_nat ? (prefix)) (\snd policy) 〈0,short_jump〉))) 431 435 (∀i.i ≤ prefix → ∃pc. 432 436 bvt_lookup_opt … (bitvector_of_nat ? i) (\snd policy) = Some ? 〈pc,short_jump〉)) … … 447 451  lapply p p generalize in match (foldl_strong ?????); * #p #Hp #hg 448 452 @conj [ @Hp  @not_le_to_lt @leb_false_to_not_le <geb_to_leb @hg ] 449  @conj [ @conj [ @conj [ @conj [ @conj 453  @conj [ @conj [ @conj [ @conj [ @conj [ @conj 450 454 [ (* out_of_program_none *) 451 455 #i #Hi2 >append_length <commutative_plus @conj … … 453 457 cases p p #p cases p p #pc #p #Hp cases x x #l #pi 454 458 [ >lookup_opt_insert_miss 455 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2))459 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2)) 456 460 @le_S_to_le @le_S_to_le @Hi 457 461  @bitvector_of_nat_abs … … 463 467  >lookup_opt_insert_miss 464 468 [ <Hi 465 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) (S (S (prefix))) ?))469 @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) (S (S (prefix))) ?)) 466 470 [ >Hi @Hi2 467 471  @le_S @le_n … … 479 483  #Hi >lookup_opt_insert_miss 480 484 [ #Hl 481 elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi2) Hl))485 elim (le_to_or_lt_eq … (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi2) Hl)) 482 486 [ #Hi3 @Hi3 483 487  #Hi3 @⊥ @(absurd ? Hi3) @sym_neq @Hi … … 492 496 ] 493 497 ] 494  (* jump_not_in_policy*) cases p p #p cases p p #pc #sigma #Hp498  (* not_jump_default *) cases p p #p cases p p #pc #sigma #Hp 495 499 cases x in prf; #lbl #ins #prf #i >append_length <commutative_plus #Hi 496 500 normalize in Hi; normalize nodelta cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 497 501 [ >lookup_insert_miss 498 [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))))) i Hi)502 [ lapply ((proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))))) i Hi) 499 503 >nth_append_first 500 504 [ #H #H2 @H @H2 … … 526 530 [ >lookup_opt_insert_miss 527 531 [ >lookup_opt_insert_miss 528 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp))) i Hi)532 [ lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) i Hi) 529 533 lapply (refl ? (bvt_lookup_opt … (bitvector_of_nat ? i) sigma)) 530 534 cases (bvt_lookup_opt … (bitvector_of_nat ? i) sigma) in ⊢ (???% → %); … … 566 570 ] 567 571 ] 568  (* lookup 0 =0 *)572  (* 0 ↦ 0 *) 569 573 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 570 574 >lookup_insert_miss 571 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hp)))575 [ @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hp)))) 572 576  @bitvector_of_nat_abs 573 577 [ / by / … … 577 581 ] 578 582 ] 583 ] 584  (* fst p = pc *) 585 cases p p #p cases p p #pc #sigma #Hp cases x #lbl #instr normalize nodelta 586 >append_length >(commutative_plus (prefix)) >lookup_insert_hit @refl 579 587 ] 580 588  (* lookup = short_jump *) #i >append_length <commutative_plus #Hi normalize in Hi; … … 599 607 / by refl/ 600 608 ] 601  @conj [ @conj [ @conj [ @conj [ @conj 609  @conj [ @conj [ @conj [ @conj [ @conj [ @conj 602 610 [ #i cases i 603 611 [ #Hi2 @conj … … 629 637  >lookup_insert_hit @refl 630 638 ] 639  >lookup_insert_hit @refl 640 ] 631 641  #i cases i 632 642 [ #Hi >lookup_opt_insert_hit @(ex_intro ?? 0) @refl … … 643 653 * if we have not added anything to the pc, we only know the PC hasn't changed, 644 654 * there might still have been a short/medium jump change *) 645 definition policy_pc_equal ≝655 definition sigma_pc_equal ≝ 646 656 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. 647 (∀n :ℕ.n ≤ program →657 (∀n.n ≤ program → 648 658 \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = 649 659 \fst (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). 650 660 651 definition policy_jump_equal ≝661 definition sigma_jump_equal ≝ 652 662 λprogram:list labelled_instruction.λp1,p2:ppc_pc_map. 653 (∀n :ℕ.n < program →663 (∀n.n < program → 654 664 \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p1) 〈0,short_jump〉) = 655 665 \snd (bvt_lookup … (bitvector_of_nat 16 n) (\snd p2) 〈0,short_jump〉)). … … 750 760 qed. 751 761 752 definition policy_safe: list labelled_instruction → label_map → ℕ → ppc_pc_map → ppc_pc_map → Prop ≝753 λprogram.λlabels.λadded.λold_sigma.λsigma.754 ∀i.i < program →755 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉 in756 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in757 let 〈label,instr〉 ≝ nth i ? program 〈None ?, Comment [ ]〉 in758 ∀dest.is_jump_to instr dest →759 let paddr ≝ lookup_def … labels dest 0 in760 let addr ≝ bitvector_of_nat ? (if leb i paddr (* forward jump *)761 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added762 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd sigma) 〈0,short_jump〉)) in763 match j with764 [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧765 ¬is_call instr766  medium_jump ⇒ \fst (medium_jump_cond pc_plus_jmp_length addr) = true ∧767 \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧768 ¬is_relative_jump instr769  long_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧770 \fst (medium_jump_cond pc_plus_jmp_length addr) = false771 ].772 773 762 lemma not_true_is_false: 774 763 ∀b:bool.b ≠ true → b = false.
Note: See TracChangeset
for help on using the changeset viewer.