- Timestamp:
- Jul 4, 2012, 3:38:52 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Policy.ma
r2152 r2153 35 35 | #sigma normalize nodelta #H @conj [ @conj 36 36 [ @(proj1 ?? (proj1 ?? (proj1 ?? H))) 37 | (* #Ht destruct (Ht) *)@(proj2 ?? (proj1 ?? (proj1 ?? H)))37 | @(proj2 ?? (proj1 ?? (proj1 ?? H))) 38 38 ] 39 39 | @(proj2 ?? H) … … 48 48 | #j2 #H2 @conj [ @conj 49 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)))) 50 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? H2)))) 56 51 ] 57 52 | @(proj2 ?? H2) … … 68 63 qed. 69 64 65 70 66 lemma pe_int_refl: ∀program.reflexive ? (sigma_jump_equal program). 71 67 #program whd #x whd #n #Hn … … 153 149 ] 154 150 qed. 151 152 lemma jump_pc_equal: ∀program.∀n. 153 match \snd (jump_expansion_internal program n) with 154 [ None ⇒ True 155 | Some p1 ⇒ match \snd (jump_expansion_internal program (S n)) with 156 [ None ⇒ True 157 | Some p2 ⇒ sigma_jump_equal program p1 p2 → sigma_pc_equal program p1 p2 158 ] 159 ]. 160 #program #n lapply (refl ? (jump_expansion_internal program n)) 161 cases (jump_expansion_internal program n) in ⊢ (???% → %); #x cases x -x 162 #Nno_ch #No cases No 163 [ normalize nodelta #HN #NEQ @I 164 | #Npol normalize nodelta #HN #NEQ lapply (refl ? (jump_expansion_internal program (S n))) 165 cases (jump_expansion_internal program (S n)) in ⊢ (???% → %); #x cases x -x 166 #Sno_ch #So cases So 167 [ normalize nodelta #HS #SEQ @I 168 | #Spol normalize nodelta #HS #SEQ #Hj 169 whd in match (jump_expansion_internal program (S n)) in SEQ; (*80s*) 170 >NEQ in SEQ; normalize nodelta cases Nno_ch in HN; 171 [ #HN normalize nodelta #SEQ >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? SEQ)))) 172 / by / 173 | #HN normalize nodelta cases (jump_expansion_step program (create_label_map program) «Npol,?») 174 #x cases x -x #Stno_ch #Stno_o normalize nodelta cases Stno_o 175 [ normalize nodelta #_ #H destruct (H) 176 | #Stno_p normalize nodelta #HSt #STeq 177 <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? STeq)))) in Hj; #Hj 178 @(proj2 ?? (proj1 ?? HSt)) @(proj2 ?? (proj1 ?? (proj1 ?? HSt))) @Hj 179 ] 180 ] 181 ] 182 ] 183 qed. 184 155 185 156 186 lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l). … … 413 443 @conj 414 444 [ @(equal_compact_unsafe_compact ?? Fp) 415 [ cases daemon 445 [ lapply (jump_pc_equal program (2*|program|)) 446 >Feq >Geq normalize nodelta #H @H @Heq 416 447 | cases daemon 417 448 | @(proj2 ?? (proj1 ?? HGp)) … … 487 518 normalize nodelta #Hpe 488 519 lapply (measure_incr_or_equal program Xp program (le_n (|program|)) 0) 489 [ cases daemon (* reorder *)520 [ @HXp 490 521 | lapply (Hfa x Hx) >Xeq >Seq 491 522 lapply (measure_special program «Xp,?») 492 [ cases daemon (* reorder *)523 [ @HXp 493 524 | lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*) 494 525 >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq … … 517 548 ] 518 549 ] 519 | #Hfull 520 whd in match (jump_expansion_internal program (S (2*|program|))); (*65s*) 521 >Feq normalize nodelta cases Fno_ch in HFp Feq; #HFp #Feq 522 normalize nodelta 523 [ @conj 524 [ cases daemon (* XXX *) 525 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp)))) 526 ] 527 | cases (jump_expansion_step ???); #z cases z -z #stch #sto cases sto 528 [ #_ / by I/ 529 | -sto #stp normalize nodelta #Hstp @conj 530 [ @(equal_compact_unsafe_compact ?? Fp) 531 [ @(proj2 ?? (proj1 ?? Hstp)) @(proj2 ?? (proj1 ?? (proj1 ?? Hstp))) 532 #i #Hi 533 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 534 [ #Hj 535 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))) i (le_S_to_le … Hi)) 536 lapply (Hfull i Hi Hj) 537 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 538 #fp #fj #Hfj >Hfj normalize nodelta 539 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉) 540 #stp #stj cases stj normalize nodelta 541 [1,2: #H cases H #H2 cases H2 destruct (H2) 542 |3: #_ @refl 543 ] 544 | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))) i Hi Hj) 550 | #Hfull lapply (refl ? (jump_expansion_internal program (S (2*|program|)))) 551 cases (jump_expansion_internal program (S (2*|program|))) in ⊢ (???% → %); 552 #z cases z -z #Gch #Go cases Go normalize nodelta 553 [ #HGp #Geq @I 554 | -Go #Gp normalize nodelta #HGp #Geq @conj 555 [ @(equal_compact_unsafe_compact ?? Fp) 556 [ lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta 557 #H @H #i #Hi 558 cases (dec_is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 559 [ #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*) 560 >Feq in Geq; normalize nodelta cases Fno_ch 561 [ normalize nodelta #Heq 562 >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) % 563 | normalize nodelta cases (jump_expansion_step program (create_label_map program) «Fp,?») 564 #x cases x -x #stch #sto normalize nodelta cases sto 565 [ normalize nodelta #_ #X destruct (X) 566 | -sto #stp normalize nodelta #Hst #Heq 567 <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) 568 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi)) 569 lapply (Hfull i Hi Hj) 570 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 571 #fp #fj #Hfj >Hfj normalize nodelta 572 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉) 573 #stp #stj cases stj normalize nodelta 574 [1,2: #H cases H #H2 cases H2 destruct (H2) 575 |3: #_ @refl 576 ] 577 ] 578 ] 579 | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi Hj) 545 580 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi Hj) @refl 546 581 ] 547 | cases daemon 548 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp))))582 | cases daemon 583 | @(proj2 ?? (proj1 ?? HGp)) 549 584 ] 550 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hstp)))))))585 | @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp)))) 551 586 ] 552 587 ] 553 588 ] 554 589 ] 555 ] 556 | #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) 557 #x cases x -x #nch #npol normalize nodelta #Hnpol 558 #x cases x -x #Sch #Spol normalize nodelta #HSpol 559 cases npol in Hnpol; cases Spol in HSpol; 560 [ #Hnpol #HSpol %1 // 561 |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); // 562 #H destruct (H) 563 |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m 564 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 565 #x1 #x2 566 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 567 #y1 #y2 normalize nodelta 568 @dec_eq_jump_length 569 ] 570 ] 590 | #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) 591 #x cases x -x #nch #npol normalize nodelta #Hnpol 592 #x cases x -x #Sch #Spol normalize nodelta #HSpol 593 cases npol in Hnpol; cases Spol in HSpol; 594 [ #Hnpol #HSpol %1 // 595 |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); // 596 #H destruct (H) 597 |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m 598 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 599 #x1 #x2 600 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 601 #y1 #y2 normalize nodelta 602 @dec_eq_jump_length 603 ] 604 ] 571 605 qed. 572 606
Note: See TracChangeset
for help on using the changeset viewer.