Changeset 2152 for src/ASM/Policy.ma
 Timestamp:
 Jul 4, 2012, 1:23:00 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2141 r2152 12 12 [ None ⇒ True 13 13  Some x ⇒ 14 And (And (And (And (And 15 (out_of_program_none program x) 16 (not_jump_default program x)) 14 And (And (And (And 15 (not_jump_default program x) 17 16 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd x) 〈0,short_jump〉) = 0)) 18 17 (\fst x = \fst (bvt_lookup … (bitvector_of_nat ? (program)) (\snd x) 〈0,short_jump〉))) 19 ( \fst x < 2^16))20 ( no_ch = true → sigma_compact program (create_label_map program) x)18 (sigma_compact_unsafe program (create_label_map program) x)) 19 (\fst x < 2^16) 21 20 ]) ≝ 22 21 let labels ≝ create_label_map program in … … 34 33 #x cases x x 35 34 [ #H / by I/ 36  #sigma normalize nodelta #H @conj [ @conj [ @conj [ @conj 37 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 38  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H))))) 39 ] 40  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H)))) 35  #sigma normalize nodelta #H @conj [ @conj 36 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 37  (* #Ht destruct (Ht) *) @(proj2 ?? (proj1 ?? (proj1 ?? H))) 41 38 ] 42 39  @(proj2 ?? H) 43 ]44  #H destruct (H)45 40 ] 46 41 ] … … 51 46 #x cases x x #ch2 #z2 cases z2 normalize nodelta 52 47 [ #_ / by I/ 53  #j2 #H2 @conj [ @conj [ @conj [ @conj 54 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))) 55  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))))) 56 ] 57  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))))) 58 ] 48  #j2 #H2 @conj [ @conj 49 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))) 50  (*#Ht @(equal_compact_unsafe_compact ?? op) 51 [ @(proj2 ?? (proj1 ?? H2)) @Ht 52  cases daemon (* add sigma_safe to properties *) 53  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))) 54 ]*) 55 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))) 56 ] 59 57  @(proj2 ?? H2) 60 58 ] 61  #Ht @(equal_compact_unsafe_compact ?? op)62 [ @(proj2 ?? (proj1 ?? (proj1 ?? H2))) @Ht63  cases daemon (* add to invvariants *)64  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2))))65 ]66 ]67 59 ] 68 60 ] … … 71 63 [ #_ >p2 #ABS destruct (ABS) 72 64  #map >p2 normalize nodelta 73 #H #eq destruct (eq) cases daemon (* change order *)65 #H #eq destruct (eq) @H 74 66 ] 75 67 ] … … 396 388 match p with 397 389 [ None ⇒ True 398  Some pol ⇒ And ( And (out_of_program_none program pol)399 (sigma_compact program (create_label_map program) pol) )390  Some pol ⇒ And (*And (out_of_program_none program pol)*) 391 (sigma_compact program (create_label_map program) pol) 400 392 (\fst (bvt_lookup … (bitvector_of_nat ? 0) (\snd pol) 〈0,short_jump〉) = 0) 401 393 ]. … … 419 411 [ #H #Feq whd in match policy_equal_opt; normalize nodelta #ABS destruct (ABS) 420 412  Fo #Fp #HFp #Feq whd in match policy_equal_opt; normalize nodelta #Heq 421 @conj [ @conj 422 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))) 423  @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*program))) in Geq; (*80s*) 413 @conj 414 [ @(equal_compact_unsafe_compact ?? Fp) 415 [ cases daemon 416  cases daemon 417  @(proj2 ?? (proj1 ?? HGp)) 418 ] 419 (* @(proj2 ?? HGp) whd in match (jump_expansion_internal program (S (2*program))) in Geq; (*80s*) 424 420 >Feq in Geq; cases Fno_ch in HFp Feq; normalize nodelta #HFp #Feq #Geq 425 421 [ destruct (Geq) / by / … … 436 432 ] 437 433 ] 434 ]*) 435  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) 438 436 ] 439  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))))440 ]441 437 ] 442 438 ] … … 525 521 >Feq normalize nodelta cases Fno_ch in HFp Feq; #HFp #Feq 526 522 normalize nodelta 527 [ @conj [ @conj 528 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))))) 529  @((proj2 ?? HFp) (refl ? true)) ] 523 [ @conj 524 [ cases daemon (* XXX *) 530 525  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) 531 526 ] 532 527  cases (jump_expansion_step ???); #z cases z z #stch #sto cases sto 533 528 [ #_ / by I/ 534  sto #stp normalize nodelta #Hstp @conj [ @conj 535 [ @(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))))) 536  @(equal_compact_unsafe_compact ?? Fp) 537 [ @(proj2 ?? (proj1 ?? (proj1 ?? Hstp))) @(proj2 ?? (proj1 ?? Hstp)) 529  sto #stp normalize nodelta #Hstp @conj 530 [ @(equal_compact_unsafe_compact ?? Fp) 531 [ @(proj2 ?? (proj1 ?? Hstp)) @(proj2 ?? (proj1 ?? (proj1 ?? Hstp))) 538 532 #i #Hi 539 533 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) … … 548 542 3: #_ @refl 549 543 ] 550  #Hj >(proj 2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) i Hi Hj)551 >(proj 2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) i Hi Hj) @refl544  #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) i Hi Hj) 545 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl 552 546 ] 553 547  cases daemon 554 548  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))) 555 549 ] 550  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))))) 556 551 ] 557  @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))) ]558 552 ] 559 553 ] … … 583 577 (*CSC: modified to really use the specification in Assembly.ma.*) 584 578 definition jump_expansion': 585 ∀program:preamble × (Σl:list labelled_instruction.S (l) < 2^16 ).579 ∀program:preamble × (Σl:list labelled_instruction.S (l) < 2^16 ∧ is_well_labelled_p l). 586 580 option (Σsigma_policy:(Word → Word) × (Word → bool). 587 581 let 〈sigma,policy〉≝ sigma_policy in … … 604 598 [ lapply (proj2 ?? Hfpol) cases (bvt_lookup ??? fpol 〈0,short_jump〉) 605 599 #x #y #Hx normalize nodelta >Hx / by refl/ 606  #ppc #ppc_ok @conj 600  cases daemon (* leaving this until stabilisation of sigma predicate *) 601 (*#ppc #ppc_ok normalize nodelta @conj 607 602 [ #Hppc lapply (proj2 ?? (proj1 ?? Hfpol) (nat_of_bitvector 16 ppc) ppc_ok) 608 603 >bitvector_of_nat_inverse_nat_of_bitvector … … 651 646 ] 652 647 ] 653 ] 648 ] 654 649  cases daemon (* XXX remains to be done *) 655 ] 650 ] *) 656 651 ] 657 652 qed.
Note: See TracChangeset
for help on using the changeset viewer.