- Timestamp:
- Jul 24, 2012, 11:51:49 AM (9 years ago)
- File:
-
- 1 edited
-
src/ASM/PolicyStep.ma (modified) (3 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/PolicyStep.ma
r2240 r2241 1420 1420 ] 1421 1421 ] 1422 ] *)1422 ] *) 1423 1423 qed. 1424 1424 … … 1590 1590 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi 1591 1591 [ >nth_append_first [2: @Hi] 1592 < (proj2 ?? (pair_destruct ?????? Heq2))>lookup_insert_miss1592 <Heq2b >lookup_insert_miss 1593 1593 [ >lookup_insert_miss 1594 1594 [ >lookup_insert_miss 1595 1595 [ elim (le_to_or_lt_eq … Hi) -Hi #Hi 1596 1596 [ >lookup_insert_miss 1597 [ (* USE[pass]: sigma_safe *) 1598 lapply ((proj2 ?? Hpolicy) i (le_S_to_le … Hi)) 1599 cases (bvt_lookup … (bitvector_of_nat ? i) inc_sigma 〈0,short_jump〉) 1600 #pc #j normalize nodelta 1601 cases (bvt_lookup … (bitvector_of_nat ? (S i)) inc_sigma 〈0,short_jump〉) 1602 #Spc #Sj normalize nodelta 1603 cases (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins normalize nodelta 1604 #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj 1605 lapply (refl ? (leb (lookup_def … labels dest 0) (S (|prefix|)))) 1606 cases (leb (lookup_def … labels dest 0) (S (|prefix|))) in ⊢ (???% → %); #H 1607 [ cases (le_to_or_lt_eq … (leb_true_to_le … H)) -H #H 1608 [ >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta 1609 >lookup_insert_miss 1610 [ cases (le_to_or_lt_eq … (le_S_S_to_le … H)) -H #H 1611 [ >lookup_insert_miss 1612 [ #H2 @H2 1613 | @bitvector_of_nat_abs 1614 [3: @lt_to_not_eq @H 1615 |1: @(transitive_lt ??? H) 1616 ] 1617 @prefix_ok 1618 ] 1619 | >H >lookup_insert_hit 1620 (* USE: inc_pc = lookup |prefix| *) 1621 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1622 #H2 @H2 1623 ] 1624 | @bitvector_of_nat_abs 1625 [3: @lt_to_not_eq @H 1626 |1: @(transitive_lt ??? H) 1627 ] 1628 @prefix_ok1 1629 ] 1630 | >H >lookup_insert_hit normalize nodelta 1631 >(not_le_to_leb_false … (lt_to_not_le ?? (le_S_S ?? (le_n (|prefix|))))) 1632 normalize nodelta 1633 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1634 #H2 >(proj2 ?? (proj1 ?? Hpolicy)) 1635 ] 1636 | 1637 1638 1639 1640 [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta 1641 [1,4,7: cases (decidable_le (lookup_def … labels dest 0) (S (|prefix|))) #H 1642 [1,3,5: >(le_to_leb_true … H) normalize nodelta cases (le_to_or_lt_eq … H) -H #H 1643 [1,3,5: >(le_to_leb_true … (le_S_S_to_le … H)) normalize nodelta 1644 >lookup_insert_miss 1645 [2,4,6: @bitvector_of_nat_abs 1646 [3,6,9: @lt_to_not_eq @H 1647 |1,4,7: @(transitive_lt ??? H) 1648 ] 1649 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 1650 @le_S_S >append_length <plus_n_Sm @le_S_S @le_plus_n_r 1651 ] 1652 cases (le_to_or_lt_eq … H) -H #H 1653 [1,3,5: >lookup_insert_miss 1654 [1,3,5: #H @H 1655 |2,4,6: @bitvector_of_nat_abs 1656 [3,6,9: @lt_to_not_eq @(le_S_S_to_le … H) 1657 |1,4,7: @(transitive_lt ??? (le_S_S_to_le … H)) 1658 ] 1659 @(transitive_lt … (proj1 ?? (pi2 ?? program))) >prf 1660 >append_length @le_S_S @le_plus_n_r 1661 ] 1662 |2,4,6: >(injective_S … H) >lookup_insert_hit 1663 (* USE: blerp *) 1664 >(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1665 #H @H 1666 ] 1667 |2,4,6: >H >lookup_insert_hit >(not_le_to_leb_false) 1668 [2,4,6: @le_to_not_lt @le_n] 1669 normalize nodelta 1670 lapply (proj2 ?? (proj1 ?? (pi2 ?? old_sigma)) (|prefix|) ?) 1671 [1,3,5: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r] 1672 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma))) 1673 cases (lookup_opt … (bitvector_of_nat ? (|prefix|)) (\snd old_sigma)) in ⊢ (???% → %); 1674 [1,3,5: normalize nodelta #_ #abs cases abs 1675 |2,4,6: #x cases x -x #ppc #pj normalize nodelta #PEQ 1676 lapply (refl ? (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma))) 1677 cases (lookup_opt … (bitvector_of_nat ? (S (|prefix|))) (\snd old_sigma)) in ⊢ (???% → %); 1678 [1,3,5: normalize nodelta #_ #abs cases abs 1679 |2,4,6: #x cases x -x #Sppc #Spj normalize nodelta #SPEQ #Pcompact 1680 >(lookup_opt_lookup_hit … SPEQ 〈0,short_jump〉) 1681 >(lookup_opt_lookup_hit … PEQ 〈0,short_jump〉) in Holdeq; 1682 #H >Pcompact >(proj1 ?? (pair_destruct ?????? H)) 1683 >commutative_plus >assoc_plus1 <(proj2 ?? (proj1 ?? Hpolicy)) 1684 <(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hpolicy)))))))) 1685 >prf >nth_append_second 1686 [1,3,5: <minus_n_n whd in match (nth ????); >p1 1687 cases daemon (* to be lemmatized *) 1688 |2,4,6: @le_n 1689 ] 1690 ] 1691 ] 1692 ] 1693 |2,4,6: >(not_le_to_leb_false … H) 1694 >not_le_to_leb_false 1695 [2,4,6: @lt_to_not_le @le_S_to_le @not_le_to_lt @H 1696 |1,3,5: normalize nodelta #H @H 1697 ] 1698 ] 1699 |2,5,8: cases daemon (* like previous case *) 1700 |3,6,9: cases daemon (* like previous case *) 1701 ] 1702 |4,5: #x normalize nodelta cases daemon (* blerp *) 1703 |1: cases daemon (* blerp *) 1704 ] 1705 1706 1707 1708 1709 (*(\fst (short_jump_cond (bitvector_of_nat 16 Spc) 1710 (bitvector_of_nat 16 1711 (inc_pc 1712 +instruction_size_jmplen 1713 (max_length old_length 1714 (select_jump_length labels old_sigma inc_pc_sigma inc_added 1715 (|prefix|) xx)) (Jmp xx)))) 1716 =true *) 1717 1718 1719 ] 1597 1720 [ >lookup_insert_miss 1598 1721 [ (* USE[pass]: sigma_safe *) … … 1605 1728 #Hind #dest #Hj lapply (Hind dest Hj) -Hind -Hj lapply (proj1 ?? (pair_destruct ?????? Heq2)) cases instr 1606 1729 [2,3,6: [3: #x] #y normalize nodelta #EQ <EQ cases j normalize nodelta 1607 [1,4,7: 1608 *) 1730 [1,4,7: *) 1609 1731 qed. 1610 1732
Note: See TracChangeset
for help on using the changeset viewer.
