Changeset 1807 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Mar 5, 2012, 12:40:02 PM (8 years ago)
Author:
mulligan
Message:

some changes, as finally worked out what i was up to prior to working on report

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1711 r1807  
    13701370qed.
    13711371
     1372lemma 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  ]
     1382qed.
     1383
     1384lemma eqb_decidable:
     1385  ∀l, r: nat.
     1386    (eqb l r = true) ∨ (eqb l r = false).
     1387  #l #r //
     1388qed.
     1389
     1390axiom eqb_true_to_refl:
     1391  ∀l, r: nat.
     1392    eqb l r = true → l = r.
     1393
     1394axiom eqb_false_to_not_refl:
     1395  ∀l, r: nat.
     1396    eqb l r = false → l ≠ r.
     1397
    13721398let rec traverse_code_internal
    13731399  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     
    13781404            reachable_program_counter code_memory fixed_program_size program_counter)
    13791405        (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)
    13801408        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  ]
     1526qed.
     1527
     1528
     1529
     1530let 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 →
    13811540          Σcost_map: identifier_map CostTag nat.
    13821541            (∀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) ∧
     
    13841543              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
    13851544                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.
    13901548    (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 ? ?))
    13981559  ].
    13991560  [2:
    14001561    @pi2
    1401   |4:
     1562  |6:
    14021563    @(reachable_program_counter_witness lbl)
    14031564    assumption
     1565  |8:
     1566    assumption
    14041567  |3:
    1405     assumption
    1406   |1:
     1568  (*
    14071569    %
    14081570    [1:
     
    14101572      @⊥ lapply(lt_to_not_le … absurd1) #absurd
    14111573      cases absurd #absurd @absurd
    1412       @(transitive_le … absurd2) @le_S @le_n
     1574      @(lt_to_le_to_le … absurd2)
     1575      @(transitive_le)
    14131576    |2:
    14141577      #k #k_pres
    14151578      @⊥ 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;
    14171586  |5:
    14181587    %
Note: See TracChangeset for help on using the changeset viewer.