Changeset 1696


Ignore:
Timestamp:
Feb 15, 2012, 4:09:57 PM (6 years ago)
Author:
mulligan
Message:

finished adding russell types to the traverse_cost_* functions

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1693 r1696  
    2828    (∃n: nat. Some … program_counter = fetch_program_counter_n n code_memory (zero 16)) ∧
    2929        nat_of_bitvector 16 program_counter < program_size.
     30   
     31definition well_labelling: BitVectorTrie costlabel 16 → Prop ≝
     32  λcost_labels.
     33    injective … (λx. lookup_opt … x cost_labels).
    3034   
    3135definition good_program: ∀code_memory: BitVectorTrie Byte 16. ∀total_program_size: nat. Prop ≝
     
    14121416qed.
    14131417
     1418(* XXX: to be moved into common/Identifiers.ma *)
     1419lemma lookup_present_add_hit:
     1420  ∀tag, A, map, k, v, k_pres.
     1421    lookup_present tag A (add … map k v) k k_pres = v.
     1422  #tag #a #map #k #v #k_pres
     1423  lapply (lookup_lookup_present … (add … map k v) … k_pres)
     1424  >lookup_add_hit #Some_assm destruct(Some_assm)
     1425  <e0 %
     1426qed.
     1427
     1428lemma lookup_present_add_miss:
     1429  ∀tag, A, map, k, k', v, k_pres', k_pres''.
     1430    k' ≠ k →
     1431      lookup_present tag A (add … map k v) k' k_pres' = lookup_present tag A map k' k_pres''.
     1432  #tag #A #map #k #k' #v #k_pres' #k_pres'' #neq_assm
     1433  lapply (lookup_lookup_present … (add … map k v) ? k_pres')
     1434  >lookup_add_miss try assumption
     1435  #Some_assm
     1436  lapply (lookup_lookup_present … map k') >Some_assm #Some_assm'
     1437  lapply (Some_assm' k_pres'') #Some_assm'' destruct assumption
     1438qed.
     1439
     1440(* XXX: to be moved into basics/types.ma *)
     1441lemma not_None_to_Some:
     1442  ∀A: Type[0].
     1443  ∀o: option A.
     1444    o ≠ None A → ∃v: A. o = Some A v.
     1445  #A #o cases o
     1446  [1:
     1447    #absurd cases absurd #absurd' cases (absurd' (refl …))
     1448  |2:
     1449    #v' #ignore /2/
     1450  ]
     1451qed.
     1452
     1453lemma present_add_present:
     1454  ∀tag, a, map, k, k', v.
     1455    k' ≠ k →
     1456      present tag a (add tag a map k v) k' →
     1457        present tag a map k'.
     1458  #tag #a #map #k #k' #v #neq_hyp #present_hyp
     1459  whd in match present; normalize nodelta
     1460  whd in match present in present_hyp; normalize nodelta in present_hyp;
     1461  cases (not_None_to_Some a … present_hyp) #v' #Some_eq_hyp
     1462  lapply (lookup_add_cases tag ?????? Some_eq_hyp) *
     1463  [1:
     1464    * #k_eq_hyp @⊥ /2/
     1465  |2:
     1466    #Some_eq_hyp' /2/
     1467  ]
     1468qed.
     1469
    14141470let rec traverse_code_internal
    14151471  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     
    14201476            reachable_program_counter code_memory fixed_program_size program_counter)
    14211477        (good_program_witness: good_program code_memory fixed_program_size)
    1422         on program_size: identifier_map CostTag nat ≝
     1478        on program_size:
     1479          Σcost_map: identifier_map CostTag nat.
     1480            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
     1481              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
     1482                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    14231483  match program_size with
    14241484  [ O ⇒ empty_map …
    14251485  | S program_size ⇒
    1426     let 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
     1486    let 〈instruction, new_program_counter, ticks〉 ≝ fetch … code_memory program_counter in
    14271487    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size ? good_program_witness in
    1428     match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → ? with
     1488    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
    14291489    [ None ⇒ λlookup_refl. cost_mapping
    14301490    | Some lbl ⇒ λlookup_refl.
     
    14331493    ] (refl … (lookup_opt … program_counter cost_labels))
    14341494  ].
    1435   [1:
     1495  [3:
    14361496    @(reachable_program_counter_witness lbl)
    14371497    assumption
     1498  |4:
     1499    assumption
     1500  |1:
     1501    #k #k_pres
     1502    @⊥ normalize in k_pres; /2/
    14381503  |2:
    1439     assumption
     1504    #k #k_pres
     1505    @(eq_identifier_elim … k lbl)
     1506    [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 %
     1510    |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
     1521      ]
     1522    ]
    14401523  ]
    14411524qed.
    14421525
    1443 definition traverse_code ≝
     1526definition traverse_code:
     1527  ∀code_memory: BitVectorTrie Byte 16.
     1528  ∀cost_labels: BitVectorTrie costlabel 16.
     1529  ∀program_size: nat.
     1530  ∀reachable_program_counter_witness:
     1531    ∀lbl: costlabel.
     1532    ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
     1533      reachable_program_counter code_memory program_size program_counter.
     1534  ∀good_program_witness: good_program code_memory program_size.
     1535    Σcost_map: identifier_map CostTag nat.
     1536      (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
     1537        ∃reachable_witness: reachable_program_counter code_memory program_size pc.
     1538          pi1 … (block_cost code_memory pc program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    14441539  λcode_memory: BitVectorTrie Byte 16.
    14451540  λcost_labels: BitVectorTrie costlabel 16.
Note: See TracChangeset for help on using the changeset viewer.