 Timestamp:
 Mar 13, 2012, 4:13:08 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1807 r1831 1396 1396 eqb l r = false → l ≠ r. 1397 1397 1398 axiom le_neq_to_lt: 1399 ∀m, n: nat. 1400 m ≤ n → m ≠ n → m < n. 1401 1398 1402 let rec traverse_code_internal 1399 1403 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) … … 1428 1432 ] (refl … (lookup_opt … program_counter cost_labels))) 1429 1433 ] (refl … program_size). 1430 [1: 1431 % 1434 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) 1435 [1,3,5,7,9,11,13: 1436 14: 1437 cases daemon (* XXX: russell error here i think *) 1438 2: 1439 #_ % 1432 1440 [1: 1433 1441 #pc #k #absurd1 #absurd2 … … 1438 1446 @⊥ normalize in k_pres; /2/ 1439 1447 ] 1440 2: 1448 4: 1449 #S_assm 1441 1450 cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter)) 1442 1451 [1: 1443 1452 <NEW_PC' % 1444 1453 2: 1445 1454 #new_program_counter_assm' >new_program_counter_assm' 1455 <program_size_invariant <program_size_refl 1456 <S_assm normalize <plus_n_Sm % 1446 1457 ] 1447 3: 1458 6: 1459 #_ assumption 1460 8: 1461 #_ @(reachable_program_counter_witness lbl) 1448 1462 assumption 1449 4: 1450 @(reachable_program_counter_witness lbl) 1451 assumption 1463 10: 1464 #S_assm % 1465 [1: 1466 #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl) 1467 [1: 1468 #eq_assm >eq_assm 1469 cases cost_mapping #cost_mapping' * #ind_hyp #_ 1470 @present_add_hit 1471 2: 1472 #neq_assm @present_add_miss try assumption 1473 cases cost_mapping #cost_mapping' * #ind_hyp #_ 1474 @(ind_hyp … lookup_opt_assm) 1475 [1: 1476 generalize in match (eqb_decidable (nat_of_bitvector … program_counter) 1477 (nat_of_bitvector … pc)); 1478 #hyp cases hyp 1479 [1: 1480 #relevant 1481 generalize in match (eqb_true_to_refl … relevant); 1482 #rewrite_assm <rewrite_assm 1483 cases daemon 1484 (* XXX: ??? *) 1485 2: 1486 #relevant 1487 generalize in match (eqb_false_to_not_refl … relevant); 1488 #rewrite_assm 1489 @⊥ 1490 cases rewrite_assm #relevant @relevant relevant 1491 rewrite_assm relevant hyp 1492 cases daemon 1493 (* XXX: ??? *) 1494 ] 1495 2: 1496 generalize in match H2; <program_size_refl whd in ⊢ (??% → ?); 1497 >plus_n_Sm in ⊢ (% → ?); 1498 cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)) 1499 [1: 1500 <NEW_PC' % 1501 2: 1502 #new_program_counter_assm' >new_program_counter_assm' 1503 >S_assm #relevant assumption 1504 ] 1505 ] 1506 ] 1507 2: 1508 #k #k_pres 1509 @(eq_identifier_elim … k lbl) 1510 [1: 1511 #eq_assm %{program_counter} #lookup_opt_assm 1512 %{(reachable_program_counter_witness …)} try assumption 1513 >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % 1514 2: 1515 #neq_assm 1516 cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm 1517 cases ind_hyp #_ #relevant cases (relevant k ?) 1518 [2: 1519 @(present_add_present … present_assm) assumption 1520 1: 1521 #program_counter' #ind_hyp' %{program_counter'} 1522 #relevant cases (ind_hyp' relevant) #reachable_witness' 1523 #ind_hyp'' %{reachable_witness'} >ind_hyp'' 1524 @sym_eq @lookup_present_add_miss assumption 1525 ] 1526 ] 1527 ] 1528 12: 1529 #S_assm % 1530 [1: 1531 #pc #k #H1 #H2 #lookup_opt_assm 1532 whd >lookup_opt_assm 1533 2: 1534 ] 1535 ] 1536 1452 1537 5: 1453 1538 % … … 1483 1568 @(ind_hyp … lookup_opt_assm) 1484 1569 [1: 1485 generalize in match (eqb_decidable (nat_of_bitvector … p c)1486 (nat_of_bitvector … new_program_counter'));1570 generalize in match (eqb_decidable (nat_of_bitvector … program_counter) 1571 (nat_of_bitvector … pc)); 1487 1572 #hyp cases hyp 1488 1573 [1: 1489 1574 #relevant 1490 1575 generalize in match (eqb_true_to_refl … relevant); 1491 #re fl_assm >refl_assm @le_n1576 #rewrite_assm <rewrite_assm 1492 1577 2: 1493 1578 #relevant 1494 1579 generalize in match (eqb_false_to_not_refl … relevant); 1495 #refl_assm 1496 cases refl_assm #refl_assm 1580 #rewrite_assm 1581 @⊥ 1582 cases rewrite_assm #relevant @relevant relevant 1583 rewrite_assm relevant hyp 1497 1584 ] 1498 1585 (* XXX: case analysis over pc = new_program_counter' *)
Note: See TracChangeset
for help on using the changeset viewer.