Changeset 2317 for src/ASM/Policy.ma
 Timestamp:
 Sep 3, 2012, 11:36:43 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2316 r2317 566 566 ] 567 567  @(equal_compact_unsafe_compact ? Fp) 568 [ lapply (jump_pc_equal program (2*(program))) >Feq >Geq normalize nodelta 569 #H @H #i #Hi 568 [1,2: 569 [1: lapply (jump_pc_equal program (2*(program))) >Feq >Geq normalize nodelta 570 #H @H ] 571 #i #Hi 570 572 inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 571 [ #Hj whd in match (jump_expansion_internal program (S (2*program))) in Geq; (*85s*)573 [1,3: #Hj whd in match (jump_expansion_internal program (S (2*program))) in Geq; (*85s*) 572 574 >Feq in Geq; normalize nodelta cases Fno_ch 573 [ normalize nodelta #Heq575 [1,3: normalize nodelta #Heq 574 576 >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) % 575  normalize nodelta cases (jump_expansion_step ???)577 2,4: normalize nodelta cases (jump_expansion_step ???) 576 578 #x cases x x #stch #sto normalize nodelta cases sto 577 [ normalize nodelta #_ #X destruct (X)578  sto #stp normalize nodelta #Hst #Heq579 [1,3: normalize nodelta #_ #X destruct (X) 580 2,4: sto #stp normalize nodelta #Hst #Heq 579 581 <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) 580 582 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi)) 581 lapply (Hfull i Hi ?) [ >Hj %]583 lapply (Hfull i Hi ?) [1,3: >Hj %] 582 584 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 583 585 #fp #fj #Hfj >Hfj normalize nodelta 584 586 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉) 585 587 #stp #stj cases stj normalize nodelta 586 [1,2 : #H cases H #H2 cases H2 destruct (H2)587 3 : #_ @refl588 [1,2,4,5: #H cases H #H2 cases H2 destruct (H2) 589 3,6: #_ @refl 588 590 ] 589 ] 590 ] 591  #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2:>Hj %] 592 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2:>Hj] % 591 ] 593 592 ] 594  cases daemon (* true, but have to add to properties in some way *)595  @(proj2 ?? (proj1 ?? HGp))593 2,4: #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2,4:>Hj %] 594 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2,4:>Hj] % 596 595 ] 597 ] 598  @(proj2 ?? HGp) 596  cases daemon (* true, but have to add to properties in some way *) 597  cases daemon 598  @(proj2 ?? (proj1 ?? HGp)) 599 599 ] 600 600 ] 601  @(proj2 ?? HGp) 602 ] 601 603 ] 602 604 ] 603  #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) 604 #x cases x x #nch #npol normalize nodelta #Hnpol 605 #x cases x x #Sch #Spol normalize nodelta #HSpol 606 cases npol in Hnpol; cases Spol in HSpol; 607 [ #Hnpol #HSpol %1 // 608 2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); // 609 #H destruct (H) 610 4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m 611 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 612 #x1 #x2 613 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 614 #y1 #y2 normalize nodelta 615 @dec_eq_jump_length 616 ] 617 ] 605 ] 606  #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) 607 #x cases x x #nch #npol normalize nodelta #Hnpol 608 #x cases x x #Sch #Spol normalize nodelta #HSpol 609 cases npol in Hnpol; cases Spol in HSpol; 610 [ #Hnpol #HSpol %1 // 611 2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); // 612 #H destruct (H) 613 4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m 614 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 615 #x1 #x2 616 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 617 #y1 #y2 normalize nodelta 618 @dec_eq_jump_length 619 ] 620 ] 618 621 qed. 619 622
Note: See TracChangeset
for help on using the changeset viewer.