Changeset 1891


Ignore:
Timestamp:
Apr 18, 2012, 2:52:24 PM (8 years ago)
Author:
mulligan
Message:

Nightmarish proofs on bitvectors. Trying to find some way of making sense of these.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1869 r1891  
    15351535qed.
    15361536
     1537inverter 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. *)
     1542axiom 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
     1549lemma 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  ]
     1564qed.
     1565
     1566definition nat_of_bool:
     1567    bool → nat ≝
     1568  λb: bool.
     1569  match b with
     1570  [ true ⇒ 1
     1571  | false ⇒ 0
     1572  ].
     1573
     1574axiom 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
     1581axiom 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
     1587axiom 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
     1591axiom 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
     1595axiom 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
     1609lemma 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  ]
     1645qed.
     1646
     1647axiom 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
     1661lemma 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 %
     1668qed.
     1669
     1670lemma 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  ]
     1695qed.
     1696
    15371697let rec traverse_code_internal
    15381698  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     
    15441704        (good_program_witness: good_program code_memory fixed_program_size)
    15451705        (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)
    15471707        on program_size:
    15481708          Σcost_map: identifier_map CostTag nat.
     
    15681728  ] (refl … program_size).
    15691729  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
    15711740  |14:
    15721741    cases daemon (* XXX: russell error here i think *)
     
    16131782          #hyp cases hyp
    16141783          [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))
    16201793          |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: ??? *)
    16291799          ]
    16301800        |2:
     
    16651835    [1:
    16661836      #pc #k #H1 #H2 #lookup_opt_assm
    1667       whd >lookup_opt_assm
     1837      whd
    16681838    |2:
     1839      #k #k_pres
    16691840    ]
    16701841  ]
Note: See TracChangeset for help on using the changeset viewer.