 Timestamp:
 Feb 15, 2012, 6:02:22 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1696 r1697 497 497 qed. 498 498 499 (* XXX: indexing bug reemerges! *)500 example fetch_half_add:501 ∀code_memory: BitVectorTrie Byte 16.502 ∀cost_labels: BitVectorTrie costlabel 16.503 ∀the_status : ASM_abstract_status code_memory cost_labels.504 \snd (\fst (fetch code_memory (program_counter … the_status))) =505 \snd (half_add 16 (program_counter … the_status)506 (bitvector_of_nat … (\snd (fetch code_memory (program_counter … the_status))))).507 cases daemon508 qed.509 510 axiom half_add_minus_right:511 ∀size : nat.512 ∀left : BitVector size.513 ∀right: nat.514 nat_of_bitvector … (\snd (half_add … left (bitvector_of_nat … right))) 515 nat_of_bitvector … left = right.516 517 499 lemma minus_plus_cancel: 518 500 ∀m, n : nat. … … 529 511 program_counter … (execute_1 … start_status). 530 512 cases daemon 531 qed. (* 532 #code_memory #start_status 533 whd in match (execute_1 code_memory start_status); 534 whd in match (execute_1' code_memory start_status); normalize nodelta 535 cases (fetch code_memory (program_counter … start_status)) #instruction_pc #ticks 536 cases instruction_pc #instruction #pc normalize nodelta *) 513 qed. 537 514 538 515 lemma reachable_program_counter_to_0_lt_total_program_size: … … 1468 1445 qed. 1469 1446 1447 lemma present_add_hit: 1448 ∀tag, a, map, k, v. 1449 present tag a (add tag a map k v) k. 1450 #tag #a #map #k #v 1451 whd >lookup_add_hit 1452 % #absurd destruct 1453 qed. 1454 1455 lemma present_add_miss: 1456 ∀tag, a, map, k, k', v. 1457 k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'. 1458 #tag #a #map #k #k' #v #neq_assm #present_assm 1459 whd >lookup_add_miss assumption 1460 qed. 1461 1470 1462 let rec traverse_code_internal 1471 1463 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) … … 1478 1470 on program_size: 1479 1471 Σcost_map: identifier_map CostTag nat. 1472 (∀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) ∧ 1480 1473 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → 1481 1474 ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc. … … 1483 1476 match program_size with 1484 1477 [ O ⇒ empty_map … 1485  S program_size ⇒ 1486 let 〈instruction, new_program_counter, ticks〉 ≝ fetch … code_memory program_counter in 1487 let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size ? good_program_witness in 1478  S program_size' ⇒ pi1 … 1479 1480 (let 〈instruction, new_program_counter, ticks〉 ≝ fetch … code_memory program_counter in 1481 let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size' ? good_program_witness in 1488 1482 match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with 1489 [ None ⇒ λlookup_refl. cost_mapping1483 [ None ⇒ λlookup_refl. pi1 … cost_mapping 1490 1484  Some lbl ⇒ λlookup_refl. 1491 1485 let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in 1492 1486 add … cost_mapping lbl cost 1493 ] (refl … (lookup_opt … program_counter cost_labels)) 1487 ] (refl … (lookup_opt … program_counter cost_labels))) 1494 1488 ]. 1495 [3: 1489 [2: 1490 @pi2 1491 4: 1496 1492 @(reachable_program_counter_witness lbl) 1497 1493 assumption 1498  4:1494 3: 1499 1495 assumption 1500 1496 1: 1501 #k #k_pres 1502 @⊥ normalize in k_pres; /2/ 1503 2: 1504 #k #k_pres 1505 @(eq_identifier_elim … k lbl) 1497 % 1506 1498 [1: 1507 #eq_assm %{program_counter} #lookup_opt_assm 1508 %{(reachable_program_counter_witness …)} try assumption 1509 >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % 1499 #pc #k #absurd1 #absurd2 1500 @⊥ lapply(lt_to_not_le … absurd1) #absurd 1501 cases absurd #absurd @absurd 1502 @(transitive_le … absurd2) @le_S @le_n 1510 1503 2: 1511 #neq_assm 1512 cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm 1513 cases (ind_hyp k ?) 1514 [2: 1515 @(present_add_present … present_assm) assumption 1516 1: 1517 #program_counter' #ind_hyp' %{program_counter'} 1518 #relevant cases (ind_hyp' relevant) #reachable_witness' 1519 #ind_hyp'' %{reachable_witness'} >ind_hyp'' 1520 @sym_eq @lookup_present_add_miss assumption 1504 #k #k_pres 1505 @⊥ normalize in k_pres; /2/ 1506 ] 1507 5: 1508 % 1509 [2: 1510 #k #k_pres 1511 @(eq_identifier_elim … k lbl) 1512 [1: 1513 #eq_assm %{program_counter} #lookup_opt_assm 1514 %{(reachable_program_counter_witness …)} try assumption 1515 >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % 1516 2: 1517 #neq_assm 1518 cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm 1519 cases ind_hyp #_ #relevant cases (relevant k ?) 1520 [2: 1521 @(present_add_present … present_assm) assumption 1522 1: 1523 #program_counter' #ind_hyp' %{program_counter'} 1524 #relevant cases (ind_hyp' relevant) #reachable_witness' 1525 #ind_hyp'' %{reachable_witness'} >ind_hyp'' 1526 @sym_eq @lookup_present_add_miss assumption 1527 ] 1521 1528 ] 1522 ] 1529 1: 1530 #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl) 1531 [1: 1532 #eq_assm >eq_assm 1533 cases cost_mapping #cost_mapping' * #ind_hyp #_ 1534 @present_add_hit 1535 2: 1536 #neq_assm @present_add_miss try assumption 1537 cases cost_mapping #cost_mapping' * #ind_hyp #_ 1538 cases daemon (* XXX: !!! *) 1539 ] 1540 ] 1541 6: 1523 1542 ] 1524 1543 qed.
Note: See TracChangeset
for help on using the changeset viewer.