Changeset 1897
 Timestamp:
 Apr 23, 2012, 3:46:35 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCostsSplit.ma
r1896 r1897 113 113 (good_program_witness: good_program code_memory fixed_program_size) 114 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)115 (fixed_program_size_limit: fixed_program_size ≤ 2^16) 116 116 on program_size: 117 117 Σcost_map: identifier_map CostTag nat. … … 179 179 destruct 180 180 @succ_nat_of_bitvector_half_add_1 181 @(plus_lt_to_lt ? (S n') (2^16  1))182 181 @le_plus_to_minus_r 183 change with (? < ?) 184 <plus_n_Sm <plus_n_O >plus_n_Sm assumption 182 @(transitive_le … fixed_program_size_limit) 183 change with (S ? ≤ ?) >plus_n_Sm 184 @monotonic_le_plus_r 185 @le_S_S @le_S_S @le_O_n 185 186 2: 186 187 #S_assm … … 297 298 destruct 298 299 @succ_nat_of_bitvector_half_add_1 299 @(plus_lt_to_lt ? (S n') (2^16  1))300 300 @le_plus_to_minus_r 301 change with (? < ?) 302 <plus_n_Sm <plus_n_O >plus_n_Sm assumption 301 @(transitive_le … fixed_program_size_limit) 302 change with (S ? ≤ ?) >plus_n_Sm 303 @monotonic_le_plus_r 304 @le_S_S @le_S_S @le_O_n 303 305 2: 304 306 #Sn_refl_assm >Sn_refl_assm <NEW_PC' @le_n … … 315 317 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) 316 318 [1: 319 destruct 317 320 @succ_nat_of_bitvector_half_add_1 318 @(plus_lt_to_lt ? (S n') (2^16  1))319 321 @le_plus_to_minus_r 320 change with (? < ?) 321 <plus_n_Sm <plus_n_O >plus_n_Sm assumption 322 @(transitive_le … fixed_program_size_limit) 323 change with (S ? ≤ ?) >plus_n_Sm 324 @monotonic_le_plus_r 325 @le_S_S @le_S_S @le_O_n 322 326 2: 323 327 #S_assm … … 347 351 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) 348 352 [1: 353 destruct 349 354 @succ_nat_of_bitvector_half_add_1 350 355 @le_plus_to_minus_r 351 356 @(transitive_le … fixed_program_size_limit) 352 destruct <plus_n_Sm <plus_n_Sm353 change with (S (S ?) + ? ≤ S (S ?) + ?)354 @ monotonic_le_plus_r@le_O_n357 change with (S ? ≤ ?) >plus_n_Sm 358 @monotonic_le_plus_r 359 @le_S_S @le_S_S @le_O_n 355 360 2: 356 361 #S_assm … … 375 380 qed. 376 381 382 (* 383 let rec traverse_code_internal 384 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 385 (program_counter: Word) (fixed_program_size: nat) (program_size: nat) 386 (reachable_program_counter_witness: 387 ∀lbl: costlabel. 388 ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels → 389 reachable_program_counter code_memory fixed_program_size program_counter) 390 (good_program_witness: good_program code_memory fixed_program_size) 391 (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size) 392 (fixed_program_size_limit: fixed_program_size < 2^16) 393 on program_size: 394 Σcost_map: identifier_map CostTag nat. 395 (∀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) ∧ 396 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → 397 ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc. 398 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝ 399 *) 400 377 401 definition traverse_code: 378 402 ∀code_memory: BitVectorTrie Byte 16. 379 403 ∀cost_labels: BitVectorTrie costlabel 16. 380 404 ∀program_size: nat. 405 ∀program_size_limit: program_size ≤ 2^16. 381 406 ∀reachable_program_counter_witness: 382 407 ∀lbl: costlabel. … … 385 410 ∀good_program_witness: good_program code_memory program_size. 386 411 Σcost_map: identifier_map CostTag nat. 412 (∀pc,k. nat_of_bitvector … pc < program_size → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧ 387 413 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → 388 414 ∃reachable_witness: reachable_program_counter code_memory program_size pc. … … 391 417 λcost_labels: BitVectorTrie costlabel 16. 392 418 λprogram_size: nat. 419 λprogram_size_limit: program_size ≤ 2^16. 393 420 λreachable_program_counter_witness: 394 421 ∀lbl: costlabel. … … 396 423 reachable_program_counter code_memory program_size program_counter. 397 424 λgood_program_witness: good_program code_memory program_size. 398 traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness. 399 425 pi1 ? ? (traverse_code_internal code_memory cost_labels (zero …) program_size program_size reachable_program_counter_witness good_program_witness ? program_size_limit). 426 [1: 427 @or_intror % 428 2: 429 cases (traverse_code_internal ? ? ? ? ? ? ? ? ?) 430 #cost_mapping * #inductive_hypothesis1 #inductive_hypothesis2 % 431 try assumption #pc #k #pc_program_size_assm 432 @inductive_hypothesis1 433 [1: 434 @le_O_n 435 2: 436 normalize in match (nat_of_bitvector 16 (zero 16)); 437 <plus_n_O assumption 438 ] 439 ] 440 qed. 441 400 442 definition compute_costs ≝ 401 443 λprogram: list Byte. 402 444 λcost_labels: BitVectorTrie costlabel 16. 403 445 λreachable_program_witness. 404 λgood_program_witness: good_program (load_code_memory program) (program + 1). 405 let program_size ≝ program + 1 in 446 λgood_program_witness: good_program (load_code_memory program) (program). 447 λprogram_size_limit: program ≤ 2^16. 448 let program_size ≝ program in 406 449 let code_memory ≝ load_code_memory program in 407 traverse_code code_memory cost_labels program_size reachable_program_witness ?. 408 @good_program_witness 409 qed. 450 traverse_code code_memory cost_labels program_size program_size_limit reachable_program_witness good_program_witness.
Note: See TracChangeset
for help on using the changeset viewer.