 Timestamp:
 Apr 18, 2012, 2:52:24 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1869 r1891 1535 1535 qed. 1536 1536 1537 inverter nat_jmdiscr for nat. 1538 1539 (* XXX: this is false in the general case. For instance, if n = 0 then the 1540 base case requires us prove 1 = 0, as it is the carry bit that holds 1541 the result of the addition. *) 1542 axiom succ_nat_of_bitvector_half_add_1: 1543 ∀n: nat. 1544 ∀bv: BitVector n. 1545 ∀power_proof: nat_of_bitvector … bv < 2^n  1. 1546 S (nat_of_bitvector … bv) = nat_of_bitvector … 1547 (\snd (half_add n (bitvector_of_nat … 1) bv)). 1548 1549 lemma plus_lt_to_lt: 1550 ∀m, n, o: nat. 1551 m + n < o → m < o. 1552 #m #n #o 1553 elim n 1554 [1: 1555 <(plus_n_O m) in ⊢ (% → ?); 1556 #assumption assumption 1557 2: 1558 #n' #inductive_hypothesis 1559 <(plus_n_Sm m n') in ⊢ (% → ?); 1560 #assm @inductive_hypothesis 1561 normalize in assm; normalize 1562 /2 by lt_S_to_lt/ 1563 ] 1564 qed. 1565 1566 definition nat_of_bool: 1567 bool → nat ≝ 1568 λb: bool. 1569 match b with 1570 [ true ⇒ 1 1571  false ⇒ 0 1572 ]. 1573 1574 axiom nat_of_bitvector_aux_accum: 1575 ∀m: nat. 1576 ∀v: BitVector m. 1577 ∀acc: nat. 1578 ∃n: nat. 1579 nat_of_bitvector_aux m acc v = n + nat_of_bitvector m v. 1580 1581 axiom nat_of_bitvector_plus: 1582 ∀n: nat. 1583 ∀tl: BitVector n. 1584 ∀hd: bool. 1585 nat_of_bitvector (S n) (hd:::tl) = (2 ^ n) * nat_of_bool hd + nat_of_bitvector n tl. 1586 1587 axiom plus_refl_to_refl_lor_refl: 1588 ∀m, m', n, n': nat. 1589 m + m' = n + n' → (m = n ∧ m' = n') ∨ (m = n' ∧ m' = n). 1590 1591 axiom mult_refl_to_refl_lor_refl: 1592 ∀m, m', n, n': nat. 1593 m * m' = n * n' → (m = n ∧ m' = n') ∨ (m = n' ∧ n = m'). 1594 1595 axiom Vector_inv_ind_2: 1596 ∀a: Type[0]. 1597 ∀n: nat. 1598 ∀left: Vector a n. 1599 ∀right: Vector a n. 1600 ∀P: (∀m: nat. Vector a m → Vector a m → Prop). 1601 (n ≃ 0 → (left ≃ VEmpty a) → (right ≃ VEmpty a) → (P 0 [[ ]] [[ ]])) → 1602 (∀m: nat. 1603 ∀hd, hd': a. 1604 ∀tl, tl': Vector a m. 1605 (n ≃ m → left ≃ tl → right ≃ tl' → P m tl tl') → 1606 (n ≃ S m → left ≃ hd:::tl → right ≃ hd':::tl' → P (S m) (hd:::tl) (hd':::tl'))) → 1607 P n left right. 1608 1609 lemma nat_of_bitvector_destruct: 1610 ∀n: nat. 1611 ∀l_hd, r_hd: bool. 1612 ∀l_tl, r_tl: BitVector n. 1613 nat_of_bitvector (S n) (l_hd:::l_tl) = nat_of_bitvector (S n) (r_hd:::r_tl) → 1614 l_hd = r_hd ∧ nat_of_bitvector n l_tl = nat_of_bitvector n r_tl. 1615 #n #l_hd #r_hd #l_tl #r_tl 1616 @(Vector_inv_ind_2 bool n l_tl r_tl) 1617 [1: 1618 #length_refl #l_tl_refl #r_tl_refl 1619 destruct 1620 cases l_hd cases r_hd 1621 normalize 1622 try (#absurd destruct(absurd)) 1623 @conj % 1624 2: 1625 #m #l_hd' #r_hd' #l_tl' #r_tl' #inductive_hypothesis 1626 #n_refl #l_tl_refl #r_tl_refl 1627 destruct 1628 1629 elim l_tl 1630 [1: 1631 #r_tl 1632 >(BitVector_O r_tl) 1633 normalize 1634 cases l_hd cases r_hd 1635 normalize 1636 try (#absurd destruct(absurd)) 1637 @conj % 1638 2: 1639 #n' #hd #tl #inductive_hypothesis #r_tl 1640 cases (BitVector_Sn … r_tl) #hd' #tl_hypothesis' 1641 cases tl_hypothesis' #tl' #tl_refl' 1642 >tl_refl' 1643 cases daemon 1644 ] 1645 qed. 1646 1647 axiom Vector_inv_ind_2: 1648 ∀a: Type[0]. 1649 ∀n: nat. 1650 ∀left: Vector a n. 1651 ∀right: Vector a n. 1652 ∀P: (∀m: nat. Vector a m → Vector a m → Prop). 1653 (n ≃ 0 → (left ≃ VEmpty a) → (right ≃ VEmpty a) → (P 0 [[ ]] [[ ]])) → 1654 (∀m: nat. 1655 ∀hd, hd': a. 1656 ∀tl, tl': Vector a m. 1657 (n ≃ m → left ≃ tl → right ≃ tl' → P m tl tl') → 1658 (n ≃ S m → left ≃ hd:::tl → right ≃ hd':::tl' → P (S m) (hd:::tl) (hd':::tl'))) → 1659 P n left right. 1660 1661 lemma BitVector_cons_injective: 1662 ∀n: nat. 1663 ∀l_hd, r_hd: bool. 1664 ∀l_tl, r_tl: BitVector n. 1665 l_hd = r_hd → l_tl = r_tl → l_hd:::l_tl = r_hd:::r_tl. 1666 #l #l_hd #r_hd #l_tl #r_tl 1667 #l_refl #r_refl destruct % 1668 qed. 1669 1670 lemma refl_nat_of_bitvector_to_refl: 1671 ∀n: nat. 1672 ∀l, r: BitVector n. 1673 nat_of_bitvector n l = nat_of_bitvector n r → l = r. 1674 #n 1675 elim n 1676 [1: 1677 #l #r 1678 >(BitVector_O l) 1679 >(BitVector_O r) 1680 #_ % 1681 2: 1682 #n' #inductive_hypothesis #l #r 1683 lapply (BitVector_Sn ? l) #l_hypothesis 1684 lapply (BitVector_Sn ? r) #r_hypothesis 1685 cases l_hypothesis #l_hd #l_tail_hypothesis 1686 cases r_hypothesis #r_hd #r_tail_hypothesis 1687 cases l_tail_hypothesis #l_tl #l_hd_tl_refl 1688 cases r_tail_hypothesis #r_tl #r_hd_tl_refl 1689 destruct #cons_refl 1690 cases (nat_of_bitvector_destruct n' l_hd r_hd l_tl r_tl cons_refl) 1691 #hd_refl #tl_refl 1692 @BitVector_cons_injective try assumption 1693 @inductive_hypothesis assumption 1694 ] 1695 qed. 1696 1537 1697 let rec traverse_code_internal 1538 1698 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) … … 1544 1704 (good_program_witness: good_program code_memory fixed_program_size) 1545 1705 (program_size_invariant: nat_of_bitvector … program_counter + program_size = fixed_program_size) 1546 (fixed_program_size_limit: fixed_program_size < 2^16 +1)1706 (fixed_program_size_limit: fixed_program_size < 2^16  1) 1547 1707 on program_size: 1548 1708 Σcost_map: identifier_map CostTag nat. … … 1568 1728 ] (refl … program_size). 1569 1729 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) 1570 [1,3,5,7,9,11,13: 1730 [1: 1731 destruct 1732 @succ_nat_of_bitvector_half_add_1 1733 <plus_n_O in fixed_program_size_limit; 1734 #assumption assumption 1735 3,5,7,9,11,13: 1736 destruct 1737 @succ_nat_of_bitvector_half_add_1 1738 @(plus_lt_to_lt ? (S program_size') (2^16  1)) 1739 assumption 1571 1740 14: 1572 1741 cases daemon (* XXX: russell error here i think *) … … 1613 1782 #hyp cases hyp 1614 1783 [1: 1615 #relevant 1616 generalize in match (eqb_true_to_refl … relevant); 1617 #rewrite_assm <rewrite_assm 1618 cases daemon 1619 (* XXX: ??? *) 1784 #eqb_assm generalize in match (eqb_true_to_refl … eqb_assm); 1785 #eqb_refl_assm 1786 eqb_assm hyp ind_hyp H1 H2 1787 lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm) 1788 #program_counter_refl_assm eqb_refl_assm 1789 <program_counter_refl_assm in lookup_opt_assm; <lookup_refl 1790 #Some_assm destruct(Some_assm) 1791 cases neq_assm #absurd_assm 1792 cases (absurd_assm (refl … k)) 1620 1793 2: 1621 #relevant 1622 generalize in match (eqb_false_to_not_refl … relevant); 1623 #rewrite_assm 1624 @⊥ 1625 cases rewrite_assm #relevant @relevant relevant 1626 rewrite_assm relevant hyp 1627 cases daemon 1628 (* XXX: ??? *) 1794 #eqb_assm generalize in match (eqb_false_to_not_refl … eqb_assm); 1795 #eqb_refl_assm 1796 eqb_assm hyp ind_hyp H1 H2 cost_mapping traverse_code_internal 1797 <NEW_PC' in S_assm; #relevant <relevant relevant 1798 cases daemon (* XXX: ??? *) 1629 1799 ] 1630 1800 2: … … 1665 1835 [1: 1666 1836 #pc #k #H1 #H2 #lookup_opt_assm 1667 whd >lookup_opt_assm1837 whd 1668 1838 2: 1839 #k #k_pres 1669 1840 ] 1670 1841 ]
Note: See TracChangeset
for help on using the changeset viewer.