Changeset 1895
 Timestamp:
 Apr 20, 2012, 6:40:51 PM (8 years ago)
 Location:
 src/ASM
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1894 r1895 1564 1564 qed. 1565 1565 1566 definition nat_of_bool:1567 bool → nat ≝1568 λb: bool.1569 match b with1570 [ true ⇒ 11571  false ⇒ 01572 ].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 #left1605 elim left1606 [1:1607 #right #P #base #step1608 >(BitVector_O right)1609 @base1610 try %1611 >(BitVector_O right) %1612 2:1613 #n' #hd #tl #inductive_hypothesis #right #P #base #step1614 cases (BitVector_Sn … right)1615 #hd' #right_tail_exists_assm1616 cases right_tail_exists_assm #right_tl #right_tl_refl1617 destruct @step try %1618 #n_refl' #left_refl #right_refl destruct1619 @inductive_hypothesis1620 *)1621 1622 1566 include "arithmetics/div_and_mod.ma". 1623 1567 … … 1806 1750 ] 1807 1751 qed. 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 #n1815 lapply (generalized_nat_cases m)1816 lapply (generalized_nat_cases n)1817 #n_assms #m_assms1818 cases n_assms1819 [1:1820 #left_n_assms1821 cases left_n_assms #n_O_refl destruct1822 normalize cases m normalize1823 [1,3:1824 #absurd destruct(absurd)1825 2,4:1826 #m' normalize1827 <plus_n_Sm <plus_n_Sm #absurd1828 destruct(absurd)1829 ]1830 2:1831 #right_n_assms1832 cases m_assms1833 [1:1834 #left_m_assms1835 cases left_m_assms1836 [1:1837 #m_0_refl destruct normalize1838 cases n1839 [1:1840 normalize1841 #absurd destruct(absurd)1842 2:1843 #n' normalize1844 <plus_n_Sm #absurd1845 destruct(absurd)1846 ]1847 2:1848 #m_1_refl destruct normalize1849 cases n1850 [1:1851 normalize #absurd destruct(absurd)1852 2:1853 #n' <plus_n_Sm #assm1854 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_assms1866 #n' #n_assm #m' #m_assm destruct normalize1867 <plus_n_Sm <plus_n_Sm <plus_n_Sm <plus_n_O <plus_n_O <plus_n_O <plus_n_Sm1868 <plus_n_Sm #assm destruct(assm)1869 ]1870 ]1871 1872 #relevant_m1873 cases relevant_m1874 relevant_m1875 [1:1876 lapply(generalized_nat_cases n)1877 #relevant_n1878 cases relevant_n1879 relevant_n1880 [1:1881 #relevant_n cases relevant_n1882 #n_assm #relevant_m cases relevant_m1883 #m_assm destruct normalize1884 #absurd destruct(absurd)1885 2:1886 #relevant_m cases relevant_m1887 *)1888 cases daemon1889 qed.1890 *)1891 1752 1892 1753 lemma nat_of_bitvector_aux_injective: … … 2019 1880 ] 2020 1881 qed. 2021 2022 let rec traverse_code_internal2023 (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: ?. ? with2039 [ 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 in2042 let 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in2043 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 in2044 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) with2048 [ None ⇒ λlookup_refl. pi1 … cost_mapping2049  Some lbl ⇒ λlookup_refl.2050 let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in2051 add … cost_mapping lbl cost2052 ] (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 destruct2057 @succ_nat_of_bitvector_half_add_12058 <plus_n_O in fixed_program_size_limit;2059 #assumption assumption2060 3,5,7,9,11,13:2061 destruct2062 @succ_nat_of_bitvector_half_add_12063 @(plus_lt_to_lt ? (S program_size') (2^16  1))2064 assumption2065 14:2066 cases daemon (* XXX: russell error here i think *)2067 2:2068 #_ %2069 [1:2070 #pc #k #absurd1 #absurd22071 @⊥ lapply(lt_to_not_le … absurd2) *2072 #absurd @absurd assumption2073 2:2074 #k #k_pres2075 @⊥ normalize in k_pres; /2/2076 ]2077 4:2078 #S_assm2079 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_refl2085 <S_assm normalize <plus_n_Sm %2086 ]2087 6:2088 #_ assumption2089 8:2090 #_ @(reachable_program_counter_witness lbl)2091 assumption2092 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_assm2098 cases cost_mapping #cost_mapping' * #ind_hyp #_2099 @present_add_hit2100 2:2101 #neq_assm @present_add_miss try assumption2102 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 hyp2108 [1:2109 #eqb_assm generalize in match (eqb_true_to_refl … eqb_assm);2110 #eqb_refl_assm2111 eqb_assm hyp ind_hyp H1 H22112 lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm)2113 #program_counter_refl_assm eqb_refl_assm2114 <program_counter_refl_assm in lookup_opt_assm; <lookup_refl2115 #Some_assm destruct(Some_assm)2116 cases neq_assm #absurd_assm2117 cases (absurd_assm (refl … k))2118 2:2119 #eqb_assm generalize in match (eqb_false_to_not_refl … eqb_assm);2120 #eqb_refl_assm2121 eqb_assm hyp ind_hyp H1 H2 cost_mapping traverse_code_internal2122 <NEW_PC' in S_assm; #relevant <relevant relevant2123 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 assumption2134 ]2135 ]2136 ]2137 2:2138 #k #k_pres2139 @(eq_identifier_elim … k lbl)2140 [1:2141 #eq_assm %{program_counter} #lookup_opt_assm2142 %{(reachable_program_counter_witness …)} try assumption2143 >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %2144 2:2145 #neq_assm2146 cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm2147 cases ind_hyp #_ #relevant cases (relevant k ?)2148 [2:2149 @(present_add_present … present_assm) assumption2150 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 assumption2155 ]2156 ]2157 ]2158 12:2159 #S_assm %2160 [1:2161 #pc #k #H1 #H2 #lookup_opt_assm2162 whd2163 2:2164 #k #k_pres2165 ]2166 ]2167 2168 5:2169 %2170 [2:2171 #k #k_pres2172 @(eq_identifier_elim … k lbl)2173 [1:2174 #eq_assm %{program_counter} #lookup_opt_assm2175 %{(reachable_program_counter_witness …)} try assumption2176 >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %2177 2:2178 #neq_assm2179 cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm2180 cases ind_hyp #_ #relevant cases (relevant k ?)2181 [2:2182 @(present_add_present … present_assm) assumption2183 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 assumption2188 ]2189 ]2190 1:2191 #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)2192 [1:2193 #eq_assm >eq_assm2194 cases cost_mapping #cost_mapping' * #ind_hyp #_2195 @present_add_hit2196 2:2197 #neq_assm @present_add_miss try assumption2198 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 hyp2204 [1:2205 #relevant2206 generalize in match (eqb_true_to_refl … relevant);2207 #rewrite_assm <rewrite_assm2208 2:2209 #relevant2210 generalize in match (eqb_false_to_not_refl … relevant);2211 #rewrite_assm2212 @⊥2213 cases rewrite_assm #relevant @relevant relevant2214 rewrite_assm relevant hyp2215 ]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_assm2230 #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_assm2236 #relevant assumption2237 ]2238 ]2239 ]2240 ]2241 ]2242 6:2243 ]2244 qed.2245 2246 2247 2248 let rec traverse_code_internal2249 (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: ?. ? with2264 [ O ⇒ λabsrd. ⊥2265  S program_size' ⇒ λstep_case.2266 (let 〈instruction, new_program_counter, ticks〉 ≝ fetch … code_memory program_counter in2267 if ltb (nat_of_bitvector … new_program_counter) fixed_program_size then2268 let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size' ? good_program_witness ? in2269 match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with2270 [ None ⇒ λlookup_refl. pi1 … cost_mapping2271  Some lbl ⇒ λlookup_refl.2272 let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in2273 add … cost_mapping lbl cost2274 ] (refl … (lookup_opt … program_counter cost_labels))2275 else2276 (empty_map ? ?))2277 ].2278 [2:2279 @pi22280 6:2281 @(reachable_program_counter_witness lbl)2282 assumption2283 8:2284 assumption2285 3:2286 (*2287 %2288 [1:2289 #pc #k #absurd1 #absurd22290 @⊥ lapply(lt_to_not_le … absurd1) #absurd2291 cases absurd #absurd @absurd2292 @(lt_to_le_to_le … absurd2)2293 @(transitive_le)2294 2:2295 #k #k_pres2296 @⊥ 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_assm2301 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_pres2308 @(eq_identifier_elim … k lbl)2309 [1:2310 #eq_assm %{program_counter} #lookup_opt_assm2311 %{(reachable_program_counter_witness …)} try assumption2312 >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %2313 2:2314 #neq_assm2315 cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm2316 cases ind_hyp #_ #relevant cases (relevant k ?)2317 [2:2318 @(present_add_present … present_assm) assumption2319 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 assumption2324 ]2325 ]2326 1:2327 #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)2328 [1:2329 #eq_assm >eq_assm2330 cases cost_mapping #cost_mapping' * #ind_hyp #_2331 @present_add_hit2332 2:2333 #neq_assm @present_add_miss try assumption2334 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 in2371 let code_memory ≝ load_code_memory program in2372 traverse_code code_memory cost_labels program_size reachable_program_witness ?.2373 @good_program_witness2374 qed.
Note: See TracChangeset
for help on using the changeset viewer.