Changeset 1895 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Apr 20, 2012, 6:40:51 PM (8 years ago)
Author:
mulligan
Message:

Split the ASMCosts files while working on traverse_code_internal. A lot of refactoring of the proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1894 r1895  
    15641564qed.
    15651565
    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 mult_refl_to_refl_lor_refl:
    1588   ∀m, m', n, n': nat.
    1589     m * m' = n * n' → (m = n ∧ m' = n') ∨ (m = n' ∧ n = m').
    1590 
    1591 (*
    1592 lemma BitVector_inv_ind_2:
    1593   ∀n: nat.
    1594   ∀left: Vector bool n.
    1595   ∀right: Vector bool n.
    1596   ∀P: (∀m: nat. Vector bool m → Vector bool m → Prop).
    1597     (n ≃ O → left ≃ VEmpty bool → right ≃ VEmpty bool → (P 0 [[ ]] [[ ]])) →
    1598     (∀m: nat.
    1599      ∀hd, hd': bool.
    1600      ∀tl, tl': Vector bool m.
    1601        (n ≃ m → left ≃ tl → right ≃ tl' → P m tl tl') →
    1602        (n ≃ S m → left ≃ hd:::tl → right ≃ hd':::tl' → P (S m) (hd:::tl) (hd':::tl'))) →
    1603     P n left right.
    1604   #n #left
    1605   elim left
    1606   [1:
    1607     #right #P #base #step
    1608     >(BitVector_O right)
    1609     @base
    1610     try %
    1611     >(BitVector_O right) %
    1612   |2:
    1613     #n' #hd #tl #inductive_hypothesis #right #P #base #step
    1614     cases (BitVector_Sn … right)
    1615     #hd' #right_tail_exists_assm
    1616     cases right_tail_exists_assm #right_tl #right_tl_refl
    1617     destruct @step try %
    1618     #n_refl' #left_refl #right_refl destruct
    1619     @inductive_hypothesis
    1620 *)
    1621 
    16221566include "arithmetics/div_and_mod.ma".
    16231567
     
    18061750  ]
    18071751qed.
    1808 
    1809 (*
    1810 lemma two_times_m_plus_one_refl_2_times_n_to_m_refl_0_land_n_refl_1:
    1811   ∀m, n: nat.
    1812     2 * m + 1 = 2 * n → m = 0 ∧ n = 1.
    1813 (*
    1814   #m #n
    1815   lapply (generalized_nat_cases m)
    1816   lapply (generalized_nat_cases n)
    1817   #n_assms #m_assms
    1818   cases n_assms
    1819   [1:
    1820     #left_n_assms
    1821     cases left_n_assms #n_O_refl destruct
    1822     normalize cases m normalize
    1823     [1,3:
    1824       #absurd destruct(absurd)
    1825     |2,4:
    1826       #m' normalize
    1827       <plus_n_Sm <plus_n_Sm #absurd
    1828       destruct(absurd)
    1829     ]
    1830   |2:
    1831     #right_n_assms
    1832     cases m_assms
    1833     [1:
    1834       #left_m_assms
    1835       cases left_m_assms
    1836       [1:
    1837         #m_0_refl destruct normalize
    1838         cases n
    1839         [1:
    1840           normalize
    1841           #absurd destruct(absurd)
    1842         |2:
    1843           #n' normalize
    1844           <plus_n_Sm #absurd
    1845           destruct(absurd)
    1846         ]
    1847       |2:
    1848         #m_1_refl destruct normalize
    1849         cases n
    1850         [1:
    1851           normalize #absurd destruct(absurd)
    1852         |2:
    1853           #n' <plus_n_Sm #assm
    1854           lapply (injective_S … assm)
    1855           -assm #assm lapply (injective_S … assm)
    1856           cases n'
    1857           [1:
    1858             normalize #absurd destruct(absurd)
    1859           |2:
    1860             #n'' normalize <plus_n_Sm #absurd destruct(absurd)
    1861           ]
    1862         ]
    1863       ]
    1864     |2:
    1865       #right_m_assms cases right_n_assms cases right_m_assms
    1866       #n' #n_assm #m' #m_assm destruct normalize
    1867       <plus_n_Sm <plus_n_Sm <plus_n_Sm <plus_n_O <plus_n_O <plus_n_O <plus_n_Sm
    1868       <plus_n_Sm #assm destruct(assm)
    1869     ]
    1870   ]
    1871  
    1872   #relevant_m
    1873   cases relevant_m
    1874   -relevant_m
    1875   [1:
    1876     lapply(generalized_nat_cases n)
    1877     #relevant_n
    1878     cases relevant_n
    1879     -relevant_n
    1880     [1:
    1881       #relevant_n cases relevant_n
    1882       #n_assm #relevant_m cases relevant_m
    1883       #m_assm destruct normalize
    1884       #absurd destruct(absurd)
    1885     |2:
    1886       #relevant_m cases relevant_m
    1887 *)
    1888   cases daemon
    1889 qed.
    1890 *)
    18911752
    18921753lemma nat_of_bitvector_aux_injective:
     
    20191880  ]
    20201881qed.
    2021 
    2022 let rec traverse_code_internal
    2023   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    2024     (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
    2025       (reachable_program_counter_witness:
    2026           ∀lbl: costlabel.
    2027           ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    2028             reachable_program_counter code_memory fixed_program_size program_counter)
    2029         (good_program_witness: good_program code_memory fixed_program_size)
    2030         (program_size_invariant: nat_of_bitvector … program_counter + program_size = fixed_program_size)
    2031         (fixed_program_size_limit: fixed_program_size < 2^16 - 1)
    2032         on program_size:
    2033           Σcost_map: identifier_map CostTag nat.
    2034             (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    2035             (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
    2036               ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
    2037                 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    2038   match program_size return λx. x = program_size → Σcost_map: ?. ? with
    2039   [ O ⇒ λprogram_size_refl. empty_map …
    2040   | S program_size' ⇒ λprogram_size_refl. pi1 …
    2041     (let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
    2042     let 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in
    2043     let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' fixed_program_size program_size' ? good_program_witness ? fixed_program_size_limit in
    2044     match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    2045             (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
    2046               ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
    2047                 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) with
    2048     [ None ⇒ λlookup_refl. pi1 … cost_mapping
    2049     | Some lbl ⇒ λlookup_refl.
    2050       let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
    2051         add … cost_mapping lbl cost
    2052     ] (refl … (lookup_opt … program_counter cost_labels)))
    2053   ] (refl … program_size).
    2054   cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
    2055   [1:
    2056     destruct
    2057     @succ_nat_of_bitvector_half_add_1
    2058     <plus_n_O in fixed_program_size_limit;
    2059     #assumption assumption
    2060   |3,5,7,9,11,13:
    2061     destruct
    2062     @succ_nat_of_bitvector_half_add_1
    2063     @(plus_lt_to_lt ? (S program_size') (2^16 - 1))
    2064     assumption
    2065   |14:
    2066     cases daemon (* XXX: russell error here i think *)
    2067   |2:
    2068     #_ %
    2069     [1:
    2070       #pc #k #absurd1 #absurd2
    2071       @⊥ lapply(lt_to_not_le … absurd2) *
    2072       #absurd @absurd assumption
    2073     |2:
    2074       #k #k_pres
    2075       @⊥ normalize in k_pres; /2/
    2076     ]
    2077   |4:
    2078     #S_assm
    2079     cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
    2080     [1:
    2081       <NEW_PC' %
    2082     |2:
    2083       #new_program_counter_assm' >new_program_counter_assm'
    2084       <program_size_invariant <program_size_refl
    2085       <S_assm normalize <plus_n_Sm %
    2086     ]
    2087   |6:
    2088     #_ assumption
    2089   |8:
    2090     #_ @(reachable_program_counter_witness lbl)
    2091     assumption
    2092   |10:
    2093     #S_assm %
    2094     [1:
    2095       #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
    2096       [1:
    2097         #eq_assm >eq_assm
    2098         cases cost_mapping #cost_mapping' * #ind_hyp #_
    2099         @present_add_hit
    2100       |2:
    2101         #neq_assm @present_add_miss try assumption
    2102         cases cost_mapping #cost_mapping' * #ind_hyp #_
    2103         @(ind_hyp … lookup_opt_assm)
    2104         [1:
    2105           generalize in match (eqb_decidable (nat_of_bitvector … program_counter)
    2106             (nat_of_bitvector … pc));
    2107           #hyp cases hyp
    2108           [1:
    2109             #eqb_assm generalize in match (eqb_true_to_refl … eqb_assm);
    2110             #eqb_refl_assm
    2111             -eqb_assm -hyp -ind_hyp -H1 -H2
    2112             lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm)
    2113             #program_counter_refl_assm -eqb_refl_assm
    2114             <program_counter_refl_assm in lookup_opt_assm; <lookup_refl
    2115             #Some_assm destruct(Some_assm)
    2116             cases neq_assm #absurd_assm
    2117             cases (absurd_assm (refl … k))
    2118           |2:
    2119             #eqb_assm generalize in match (eqb_false_to_not_refl … eqb_assm);
    2120             #eqb_refl_assm
    2121             -eqb_assm -hyp -ind_hyp -H1 -H2 -cost_mapping -traverse_code_internal
    2122             <NEW_PC' in S_assm; #relevant <relevant -relevant
    2123             cases daemon (* XXX: ??? *)
    2124           ]
    2125         |2:
    2126           generalize in match H2; <program_size_refl whd in ⊢ (??% → ?);
    2127           >plus_n_Sm in ⊢ (% → ?);
    2128           cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
    2129           [1:
    2130             <NEW_PC' %
    2131           |2:
    2132             #new_program_counter_assm' >new_program_counter_assm'
    2133             >S_assm #relevant assumption
    2134           ]
    2135         ]
    2136       ]
    2137     |2:
    2138       #k #k_pres
    2139       @(eq_identifier_elim … k lbl)
    2140       [1:
    2141         #eq_assm %{program_counter} #lookup_opt_assm
    2142         %{(reachable_program_counter_witness …)} try assumption
    2143         >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
    2144       |2:
    2145         #neq_assm
    2146         cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
    2147         cases ind_hyp #_ #relevant cases (relevant k ?)
    2148         [2:
    2149           @(present_add_present … present_assm) assumption
    2150         |1:
    2151           #program_counter' #ind_hyp' %{program_counter'}
    2152           #relevant cases (ind_hyp' relevant) #reachable_witness'
    2153           #ind_hyp'' %{reachable_witness'} >ind_hyp''
    2154           @sym_eq @lookup_present_add_miss assumption
    2155         ]
    2156       ]
    2157     ]
    2158   |12:
    2159     #S_assm %
    2160     [1:
    2161       #pc #k #H1 #H2 #lookup_opt_assm
    2162       whd
    2163     |2:
    2164       #k #k_pres
    2165     ]
    2166   ]
    2167    
    2168   |5:
    2169     %
    2170     [2:
    2171       #k #k_pres
    2172       @(eq_identifier_elim … k lbl)
    2173       [1:
    2174         #eq_assm %{program_counter} #lookup_opt_assm
    2175         %{(reachable_program_counter_witness …)} try assumption
    2176         >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
    2177       |2:
    2178         #neq_assm
    2179         cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
    2180         cases ind_hyp #_ #relevant cases (relevant k ?)
    2181         [2:
    2182           @(present_add_present … present_assm) assumption
    2183         |1:
    2184           #program_counter' #ind_hyp' %{program_counter'}
    2185           #relevant cases (ind_hyp' relevant) #reachable_witness'
    2186           #ind_hyp'' %{reachable_witness'} >ind_hyp''
    2187           @sym_eq @lookup_present_add_miss assumption
    2188         ]
    2189       ]
    2190     |1:
    2191       #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
    2192       [1:
    2193         #eq_assm >eq_assm
    2194         cases cost_mapping #cost_mapping' * #ind_hyp #_
    2195         @present_add_hit
    2196       |2:
    2197         #neq_assm @present_add_miss try assumption
    2198         cases cost_mapping #cost_mapping' * #ind_hyp #_
    2199         @(ind_hyp … lookup_opt_assm)
    2200         [1:
    2201           generalize in match (eqb_decidable (nat_of_bitvector … program_counter)
    2202             (nat_of_bitvector … pc));
    2203           #hyp cases hyp
    2204           [1:
    2205             #relevant
    2206             generalize in match (eqb_true_to_refl … relevant);
    2207             #rewrite_assm <rewrite_assm
    2208           |2:
    2209             #relevant
    2210             generalize in match (eqb_false_to_not_refl … relevant);
    2211             #rewrite_assm
    2212             @⊥
    2213             cases rewrite_assm #relevant @relevant -relevant
    2214             -rewrite_assm -relevant -hyp
    2215           ]
    2216           (* XXX: case analysis over pc = new_program_counter' *)
    2217         |2:
    2218           generalize in match H2; whd in ⊢ (??% → ?);
    2219           >plus_n_Sm in ⊢ (% → ?);
    2220           cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
    2221           [1:
    2222             <NEW_PC' %
    2223           |2:
    2224             #new_program_counter_assm' >new_program_counter_assm'
    2225             cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
    2226             [1:
    2227               (* XXX: todo *)
    2228             |2:
    2229               #S_program_counter_assm >S_program_counter_assm
    2230               #relevant <program_size_refl in relevant;
    2231               change with (
    2232                 nat_of_bitvector 16 pc < S (program_size'+nat_of_bitvector 16 program_counter)
    2233               ) in ⊢ (% → ?);
    2234               >plus_n_Sm in ⊢ (% → ?);
    2235               <S_program_counter_assm
    2236               #relevant assumption
    2237             ]
    2238           ]
    2239         ]
    2240       ]
    2241     ]
    2242   |6:
    2243   ]
    2244 qed.
    2245 
    2246 
    2247 
    2248 let rec traverse_code_internal
    2249   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    2250     (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
    2251       (label_map_correctness_:
    2252           ∀lbl: costlabel.
    2253           ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    2254             reachable_program_counter code_memory fixed_program_size program_counter)
    2255         (good_program_witness: good_program code_memory fixed_program_size)
    2256         on program_size:
    2257           fixed_program_size < nat_of_bitvector … program_counter + program_size →
    2258           Σcost_map: identifier_map CostTag nat.
    2259             (∀pc,k. nat_of_bitvector … program_counter < nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    2260             (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
    2261               ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
    2262                 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    2263   match program_size return λx. fixed_program_size < nat_of_bitvector … program_counter + x → Σx: ?. ? with
    2264   [ O ⇒ λabsrd. ⊥
    2265   | S program_size' ⇒ λstep_case.
    2266     (let 〈instruction, new_program_counter, ticks〉 ≝ fetch … code_memory program_counter in
    2267       if ltb (nat_of_bitvector … new_program_counter) fixed_program_size then
    2268         let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size' ? good_program_witness ? in
    2269         match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
    2270         [ None ⇒ λlookup_refl. pi1 … cost_mapping
    2271         | Some lbl ⇒ λlookup_refl.
    2272           let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
    2273             add … cost_mapping lbl cost
    2274         ] (refl … (lookup_opt … program_counter cost_labels))
    2275       else
    2276         (empty_map ? ?))
    2277   ].
    2278   [2:
    2279     @pi2
    2280   |6:
    2281     @(reachable_program_counter_witness lbl)
    2282     assumption
    2283   |8:
    2284     assumption
    2285   |3:
    2286   (*
    2287     %
    2288     [1:
    2289       #pc #k #absurd1 #absurd2
    2290       @⊥ lapply(lt_to_not_le … absurd1) #absurd
    2291       cases absurd #absurd @absurd
    2292       @(lt_to_le_to_le … absurd2)
    2293       @(transitive_le)
    2294     |2:
    2295       #k #k_pres
    2296       @⊥ normalize in k_pres; /2/
    2297     ] *)
    2298   |1:
    2299     generalize in match (reachable_program_counter_to_0_lt_total_program_size code_memory program_counter fixed_program_size);
    2300     #reachable_program_counter_assm
    2301     letin dummy_cost_label ≝ (an_identifier CostTag one)
    2302     lapply (reachable_program_counter_witness dummy_cost_label program_counter)
    2303     normalize in absurd;
    2304   |5:
    2305     %
    2306     [2:
    2307       #k #k_pres
    2308       @(eq_identifier_elim … k lbl)
    2309       [1:
    2310         #eq_assm %{program_counter} #lookup_opt_assm
    2311         %{(reachable_program_counter_witness …)} try assumption
    2312         >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
    2313       |2:
    2314         #neq_assm
    2315         cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
    2316         cases ind_hyp #_ #relevant cases (relevant k ?)
    2317         [2:
    2318           @(present_add_present … present_assm) assumption
    2319         |1:
    2320           #program_counter' #ind_hyp' %{program_counter'}
    2321           #relevant cases (ind_hyp' relevant) #reachable_witness'
    2322           #ind_hyp'' %{reachable_witness'} >ind_hyp''
    2323           @sym_eq @lookup_present_add_miss assumption
    2324         ]
    2325       ]
    2326     |1:
    2327       #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
    2328       [1:
    2329         #eq_assm >eq_assm
    2330         cases cost_mapping #cost_mapping' * #ind_hyp #_
    2331         @present_add_hit
    2332       |2:
    2333         #neq_assm @present_add_miss try assumption
    2334         cases cost_mapping #cost_mapping' * #ind_hyp #_
    2335         cases daemon (* XXX: !!! *)
    2336       ]
    2337     ]
    2338   |6:
    2339   ]
    2340 qed.
    2341 
    2342 definition traverse_code:
    2343   ∀code_memory: BitVectorTrie Byte 16.
    2344   ∀cost_labels: BitVectorTrie costlabel 16.
    2345   ∀program_size: nat.
    2346   ∀reachable_program_counter_witness:
    2347     ∀lbl: costlabel.
    2348     ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    2349       reachable_program_counter code_memory program_size program_counter.
    2350   ∀good_program_witness: good_program code_memory program_size.
    2351     Σcost_map: identifier_map CostTag nat.
    2352       (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
    2353         ∃reachable_witness: reachable_program_counter code_memory program_size pc.
    2354           pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    2355   λcode_memory: BitVectorTrie Byte 16.
    2356   λcost_labels: BitVectorTrie costlabel 16.
    2357   λprogram_size: nat.
    2358   λreachable_program_counter_witness:
    2359           ∀lbl: costlabel.
    2360           ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    2361             reachable_program_counter code_memory program_size program_counter.
    2362   λgood_program_witness: good_program code_memory program_size.
    2363     traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness.
    2364  
    2365 definition compute_costs ≝
    2366   λprogram: list Byte.
    2367   λcost_labels: BitVectorTrie costlabel 16.
    2368   λreachable_program_witness.
    2369   λgood_program_witness: good_program (load_code_memory program) (|program| + 1).
    2370     let program_size ≝ |program| + 1 in
    2371     let code_memory ≝ load_code_memory program in
    2372       traverse_code code_memory cost_labels program_size reachable_program_witness ?.
    2373   @good_program_witness
    2374 qed.
Note: See TracChangeset for help on using the changeset viewer.