 Timestamp:
 Mar 5, 2012, 12:40:02 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1711 r1807 1370 1370 qed. 1371 1371 1372 lemma lt_to_le_to_le: 1373 ∀n, m, p: nat. 1374 n < m → m ≤ p → n ≤ p. 1375 #n #m #p #H #H1 1376 elim H 1377 [1: 1378 @(transitive_le n m p) /2/ 1379 2: 1380 /2/ 1381 ] 1382 qed. 1383 1384 lemma eqb_decidable: 1385 ∀l, r: nat. 1386 (eqb l r = true) ∨ (eqb l r = false). 1387 #l #r // 1388 qed. 1389 1390 axiom eqb_true_to_refl: 1391 ∀l, r: nat. 1392 eqb l r = true → l = r. 1393 1394 axiom eqb_false_to_not_refl: 1395 ∀l, r: nat. 1396 eqb l r = false → l ≠ r. 1397 1372 1398 let rec traverse_code_internal 1373 1399 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) … … 1378 1404 reachable_program_counter code_memory fixed_program_size program_counter) 1379 1405 (good_program_witness: good_program code_memory fixed_program_size) 1406 (program_size_invariant: nat_of_bitvector … program_counter + program_size = fixed_program_size) 1407 (fixed_program_size_limit: fixed_program_size < 2^16 + 1) 1380 1408 on program_size: 1409 Σcost_map: identifier_map CostTag nat. 1410 (∀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) ∧ 1411 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → 1412 ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc. 1413 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝ 1414 match program_size return λx. x = program_size → Σcost_map: ?. ? with 1415 [ O ⇒ λprogram_size_refl. empty_map … 1416  S program_size' ⇒ λprogram_size_refl. pi1 … 1417 (let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in 1418 let 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in 1419 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 1420 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) ∧ 1421 (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k → 1422 ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc. 1423 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) with 1424 [ None ⇒ λlookup_refl. pi1 … cost_mapping 1425  Some lbl ⇒ λlookup_refl. 1426 let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in 1427 add … cost_mapping lbl cost 1428 ] (refl … (lookup_opt … program_counter cost_labels))) 1429 ] (refl … program_size). 1430 [1: 1431 % 1432 [1: 1433 #pc #k #absurd1 #absurd2 1434 @⊥ lapply(lt_to_not_le … absurd2) * 1435 #absurd @absurd assumption 1436 2: 1437 #k #k_pres 1438 @⊥ normalize in k_pres; /2/ 1439 ] 1440 2: 1441 cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter)) 1442 [1: 1443 1444 2: 1445 #new_program_counter_assm' >new_program_counter_assm' 1446 ] 1447 3: 1448 assumption 1449 4: 1450 @(reachable_program_counter_witness lbl) 1451 assumption 1452 5: 1453 % 1454 [2: 1455 #k #k_pres 1456 @(eq_identifier_elim … k lbl) 1457 [1: 1458 #eq_assm %{program_counter} #lookup_opt_assm 1459 %{(reachable_program_counter_witness …)} try assumption 1460 >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit % 1461 2: 1462 #neq_assm 1463 cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm 1464 cases ind_hyp #_ #relevant cases (relevant k ?) 1465 [2: 1466 @(present_add_present … present_assm) assumption 1467 1: 1468 #program_counter' #ind_hyp' %{program_counter'} 1469 #relevant cases (ind_hyp' relevant) #reachable_witness' 1470 #ind_hyp'' %{reachable_witness'} >ind_hyp'' 1471 @sym_eq @lookup_present_add_miss assumption 1472 ] 1473 ] 1474 1: 1475 #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl) 1476 [1: 1477 #eq_assm >eq_assm 1478 cases cost_mapping #cost_mapping' * #ind_hyp #_ 1479 @present_add_hit 1480 2: 1481 #neq_assm @present_add_miss try assumption 1482 cases cost_mapping #cost_mapping' * #ind_hyp #_ 1483 @(ind_hyp … lookup_opt_assm) 1484 [1: 1485 generalize in match (eqb_decidable (nat_of_bitvector … pc) 1486 (nat_of_bitvector … new_program_counter')); 1487 #hyp cases hyp 1488 [1: 1489 #relevant 1490 generalize in match (eqb_true_to_refl … relevant); 1491 #refl_assm >refl_assm @le_n 1492 2: 1493 #relevant 1494 generalize in match (eqb_false_to_not_refl … relevant); 1495 #refl_assm 1496 cases refl_assm #refl_assm 1497 ] 1498 (* XXX: case analysis over pc = new_program_counter' *) 1499 2: 1500 generalize in match H2; whd in ⊢ (??% → ?); 1501 >plus_n_Sm in ⊢ (% → ?); 1502 cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter)) 1503 [1: 1504 <NEW_PC' % 1505 2: 1506 #new_program_counter_assm' >new_program_counter_assm' 1507 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd (half_add 16 (bitvector_of_nat 16 1) program_counter))) 1508 [1: 1509 (* XXX: todo *) 1510 2: 1511 #S_program_counter_assm >S_program_counter_assm 1512 #relevant <program_size_refl in relevant; 1513 change with ( 1514 nat_of_bitvector 16 pc < S (program_size'+nat_of_bitvector 16 program_counter) 1515 ) in ⊢ (% → ?); 1516 >plus_n_Sm in ⊢ (% → ?); 1517 <S_program_counter_assm 1518 #relevant assumption 1519 ] 1520 ] 1521 ] 1522 ] 1523 ] 1524 6: 1525 ] 1526 qed. 1527 1528 1529 1530 let rec traverse_code_internal 1531 (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 1532 (program_counter: Word) (fixed_program_size: nat) (program_size: nat) 1533 (label_map_correctness_: 1534 ∀lbl: costlabel. 1535 ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels → 1536 reachable_program_counter code_memory fixed_program_size program_counter) 1537 (good_program_witness: good_program code_memory fixed_program_size) 1538 on program_size: 1539 fixed_program_size < nat_of_bitvector … program_counter + program_size → 1381 1540 Σcost_map: identifier_map CostTag nat. 1382 1541 (∀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) ∧ … … 1384 1543 ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc. 1385 1544 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝ 1386 match program_size with 1387 [ O ⇒ empty_map … 1388  S program_size' ⇒ pi1 … 1389 1545 match program_size return λx. fixed_program_size < nat_of_bitvector … program_counter + x → Σx: ?. ? with 1546 [ O ⇒ λabsrd. ⊥ 1547  S program_size' ⇒ λstep_case. 1390 1548 (let 〈instruction, new_program_counter, ticks〉 ≝ fetch … code_memory program_counter in 1391 let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size' ? good_program_witness in 1392 match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with 1393 [ None ⇒ λlookup_refl. pi1 … cost_mapping 1394  Some lbl ⇒ λlookup_refl. 1395 let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in 1396 add … cost_mapping lbl cost 1397 ] (refl … (lookup_opt … program_counter cost_labels))) 1549 if ltb (nat_of_bitvector … new_program_counter) fixed_program_size then 1550 let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size' ? good_program_witness ? in 1551 match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with 1552 [ None ⇒ λlookup_refl. pi1 … cost_mapping 1553  Some lbl ⇒ λlookup_refl. 1554 let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in 1555 add … cost_mapping lbl cost 1556 ] (refl … (lookup_opt … program_counter cost_labels)) 1557 else 1558 (empty_map ? ?)) 1398 1559 ]. 1399 1560 [2: 1400 1561 @pi2 1401  4:1562 6: 1402 1563 @(reachable_program_counter_witness lbl) 1403 1564 assumption 1565 8: 1566 assumption 1404 1567 3: 1405 assumption 1406 1: 1568 (* 1407 1569 % 1408 1570 [1: … … 1410 1572 @⊥ lapply(lt_to_not_le … absurd1) #absurd 1411 1573 cases absurd #absurd @absurd 1412 @(transitive_le … absurd2) @le_S @le_n 1574 @(lt_to_le_to_le … absurd2) 1575 @(transitive_le) 1413 1576 2: 1414 1577 #k #k_pres 1415 1578 @⊥ normalize in k_pres; /2/ 1416 ] 1579 ] *) 1580 1: 1581 generalize in match (reachable_program_counter_to_0_lt_total_program_size code_memory program_counter fixed_program_size); 1582 #reachable_program_counter_assm 1583 letin dummy_cost_label ≝ (an_identifier CostTag one) 1584 lapply (reachable_program_counter_witness dummy_cost_label program_counter) 1585 normalize in absurd; 1417 1586 5: 1418 1587 %
Note: See TracChangeset
for help on using the changeset viewer.