 Timestamp:
 Apr 23, 2012, 3:05:08 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCostsSplit.ma
r1895 r1896 112 112 reachable_program_counter code_memory fixed_program_size program_counter) 113 113 (good_program_witness: good_program code_memory fixed_program_size) 114 (program_size_invariant: nat_of_bitvector … program_counter + program_size = fixed_program_size)115 (fixed_program_size_limit: fixed_program_size < 2^16  1)114 (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size) 115 (fixed_program_size_limit: fixed_program_size < 2^16) 116 116 on program_size: 117 117 Σcost_map: identifier_map CostTag nat. … … 123 123 [ O ⇒ λprogram_size_refl. empty_map CostTag nat 124 124  S program_size' ⇒ λprogram_size_refl. 125 (deplet 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in126 125 deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in 127 126 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 … … 131 130 let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in 132 131 add … cost_mapping lbl cost 133 ] (refl … (lookup_opt … program_counter cost_labels)) )132 ] (refl … (lookup_opt … program_counter cost_labels)) 134 133 ] (refl … program_size). 135 134 [5: … … 138 137 @(reachable_program_counter_witness lbl) 139 138 @lookup_refl 140 3,6: 141 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) 142 [1,3: 143 destruct 144 @succ_nat_of_bitvector_half_add_1 145 @(plus_lt_to_lt ? (S program_size') (2^16  1)) 146 assumption 139 3: 140 cases program_size_invariant 141 [1: 142 #destruct_assm @⊥ traverse_code_internal destruct 147 143 2: 148 #S_assm % 144 #program_size_invariant' 145 % 149 146 [1: 150 147 #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl) … … 156 153 #neq_assm @present_add_miss try assumption 157 154 cases cost_mapping #cost_mapping' * #ind_hyp #_ 158 @(ind_hyp … lookup_opt_assm)155 inversion program_size' 159 156 [1: 160 generalize in match (eqb_decidable (nat_of_bitvector … program_counter) 161 (nat_of_bitvector … pc)); 162 #hyp cases hyp 157 #program_size_refl_0 traverse_code_internal destruct @⊥ cases neq_assm #assm @assm 158 cut (Some … k = Some … lbl → k = lbl) (* XXX: lemma *) 163 159 [1: 164 #eqb_assm generalize in match (eqb_true_to_refl … eqb_assm); 165 #eqb_refl_assm 166 eqb_assm hyp ind_hyp H1 H2 167 lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm) 168 #program_counter_refl_assm eqb_refl_assm 169 <program_counter_refl_assm in lookup_opt_assm; <lookup_refl 170 #Some_assm destruct(Some_assm) 171 cases neq_assm #absurd_assm 172 cases (absurd_assm (refl … k)) 160 #Some_assm destruct(Some_assm) % 173 161 2: 174 #eqb_assm generalize in match (eqb_false_to_not_refl … eqb_assm); 175 #eqb_refl_assm 176 eqb_assm hyp ind_hyp H1 H2 cost_mapping traverse_code_internal 177 <NEW_PC' in S_assm; #relevant <relevant relevant 178 change with (? < ?) (* XXX: open here *) 162 #Some_assm @Some_assm <lookup_opt_assm >lookup_refl 163 >(?:pc=program_counter) 164 [1: 165 % 166 2: 167 @refl_nat_of_bitvector_to_refl 168 @le_to_le_to_eq 169 try assumption 170 change with (? ≤ ?) in H2; 171 @le_S_S_to_le 172 assumption 173 ] 179 174 ] 180 175 2: 181 generalize in match H2; <program_size_refl whd in ⊢ (??% → ?); 182 >plus_n_Sm in ⊢ (% → ?); 183 cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)) 176 #n' #_ #program_size_refl_Sn' traverse_code_internal destruct 177 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) 184 178 [1: 185 <NEW_PC' % 179 destruct 180 @succ_nat_of_bitvector_half_add_1 181 @(plus_lt_to_lt ? (S n') (2^16  1)) 182 @le_plus_to_minus_r 183 change with (? < ?) 184 <plus_n_Sm <plus_n_O >plus_n_Sm assumption 186 185 2: 187 #new_program_counter_assm' >new_program_counter_assm' 188 >S_assm #relevant assumption 186 #S_assm 187 @(ind_hyp … lookup_opt_assm) 188 [1: 189 @(eqb_elim (nat_of_bitvector … program_counter) 190 (nat_of_bitvector … pc)) 191 [1: 192 #eqb_refl_assm 193 ind_hyp H1 H2 194 lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm) 195 #program_counter_refl_assm eqb_refl_assm 196 <program_counter_refl_assm in lookup_opt_assm; <lookup_refl 197 #Some_assm destruct(Some_assm) 198 cases neq_assm #absurd_assm 199 cases (absurd_assm (refl … k)) 200 2: 201 #eqb_ref_assm 202 ind_hyp 203 <NEW_PC' in S_assm; #relevant <relevant relevant 204 change with (? < ?) 205 @le_neq_to_lt assumption 206 ] 207 2: 208 generalize in match H2; whd in ⊢ (??% → ?); 209 >plus_n_Sm in ⊢ (% → ?); 210 cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)) 211 [1: 212 <NEW_PC' % 213 2: 214 #new_program_counter_assm' >new_program_counter_assm' 215 >S_assm #relevant assumption 216 ] 217 ] 189 218 ] 190 219 ] … … 211 240 ] 212 241 ] 213 4:214 #S_assm215 cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))216 [1:217 <NEW_PC' %218 2:219 #new_program_counter_assm' >new_program_counter_assm'220 <program_size_invariant <program_size_refl221 <S_assm normalize <plus_n_Sm %222 ]223 242 ] 224 243 1: … … 237 256 #inductive_hypothesis1 #inductive_hypothesis2 % 238 257 [1: 239 #pc #k #H1 #H2 @inductive_hypothesis1 240 try assumption 241 (* XXX: same goal as above *) 258 #pc #k #H1 #H2 259 cases program_size_invariant 260 [1: 261 #destruct_assm @⊥ destruct 262 2: 263 program_size_invariant #program_size_invariant 264 inversion program_size' 265 [1: 266 #program_size_refl_0 destruct 267 #lookup_opt_Some_assm 268 >(?:pc = program_counter) in lookup_opt_Some_assm; 269 [1: 270 #absurd <lookup_refl in absurd; 271 #absurd destruct 272 2: 273 @refl_nat_of_bitvector_to_refl 274 @le_to_le_to_eq 275 try assumption 276 change with (? ≤ ?) in H2; 277 @le_S_S_to_le 278 assumption 279 ] 280 2: 281 #n' #_ #program_size_Sn_refl #Some_lookup_opt_refl 282 @(inductive_hypothesis1 … pc) try assumption 283 [1: 284 @(eqb_elim … (nat_of_bitvector … program_counter) 285 (nat_of_bitvector … pc)); 286 [1: 287 #eq_assm 288 lapply (refl_nat_of_bitvector_to_refl … eq_assm) #pc_refl 289 <pc_refl in Some_lookup_opt_refl; <lookup_refl #absurd 290 destruct 291 2: 292 #neq_assm 293 @(transitive_le ? (S (nat_of_bitvector … program_counter))) 294 [1: 295 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) 296 [1: 297 destruct 298 @succ_nat_of_bitvector_half_add_1 299 @(plus_lt_to_lt ? (S n') (2^16  1)) 300 @le_plus_to_minus_r 301 change with (? < ?) 302 <plus_n_Sm <plus_n_O >plus_n_Sm assumption 303 2: 304 #Sn_refl_assm >Sn_refl_assm <NEW_PC' @le_n 305 ] 306 2: 307 change with (? < ?) 308 @le_neq_to_lt 309 assumption 310 ] 311 ] 312 2: 313 destruct 314 @(transitive_le … H2) 315 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) 316 [1: 317 @succ_nat_of_bitvector_half_add_1 318 @(plus_lt_to_lt ? (S n') (2^16  1)) 319 @le_plus_to_minus_r 320 change with (? < ?) 321 <plus_n_Sm <plus_n_O >plus_n_Sm assumption 322 2: 323 #S_assm 324 change with (S (S n' + ?) ≤ ?) 325 >plus_n_Sm @monotonic_le_plus_r >S_assm 326 <NEW_PC' @le_n 327 ] 328 ] 329 ] 330 ] 242 331 2: 243 332 assumption 333 ] 334 6: 335 inversion program_size' 336 [1: 337 #_ %1 % 338 2: 339 #n' #_ #program_size_refl_Sn @or_intror 340 cases program_size_invariant 341 [1: 342 #absurd destruct 343 2: 344 #relevant <relevant <plus_n_Sm <program_size_refl <plus_n_Sm 345 @eq_f >program_size_refl_Sn <plus_n_Sm 346 change with (? = (S ?) + ?) @eq_f2 try % 347 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) 348 [1: 349 @succ_nat_of_bitvector_half_add_1 350 @le_plus_to_minus_r 351 @(transitive_le … fixed_program_size_limit) 352 destruct <plus_n_Sm <plus_n_Sm 353 change with (S (S ?) + ? ≤ S (S ?) + ?) 354 @monotonic_le_plus_r @le_O_n 355 2: 356 #S_assm 357 cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter)) 358 [1: 359 <NEW_PC' % 360 2: 361 #new_program_counter_assm' >new_program_counter_assm' 362 cases program_size_invariant 363 [1: 364 #destruct_assm destruct 365 2: 366 #program_size_invariant 367 <program_size_invariant <program_size_refl 368 <S_assm normalize <plus_n_Sm % 369 ] 370 ] 371 ] 372 ] 244 373 ] 245 374 ]
Note: See TracChangeset
for help on using the changeset viewer.