Changeset 1697


Ignore:
Timestamp:
Feb 15, 2012, 6:02:22 PM (6 years ago)
Author:
mulligan
Message:

important bug found

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1696 r1697  
    497497qed.
    498498
    499 (* XXX: indexing bug re-emerges! *)
    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 daemon
    508 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 
    517499lemma minus_plus_cancel:
    518500  ∀m, n : nat.
     
    529511      program_counter … (execute_1 … start_status).
    530512  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 *)
     513qed.
    537514
    538515lemma reachable_program_counter_to_0_lt_total_program_size:
     
    14681445qed.
    14691446
     1447lemma 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
     1453qed.
     1454
     1455lemma 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
     1460qed.
     1461
    14701462let rec traverse_code_internal
    14711463  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     
    14781470        on program_size:
    14791471          Σ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) ∧
    14801473            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
    14811474              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
     
    14831476  match program_size with
    14841477  [ 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
    14881482    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
    1489     [ None ⇒ λlookup_refl. cost_mapping
     1483    [ None ⇒ λlookup_refl. pi1 … cost_mapping
    14901484    | Some lbl ⇒ λlookup_refl.
    14911485      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
    14921486        add … cost_mapping lbl cost
    1493     ] (refl … (lookup_opt … program_counter cost_labels))
     1487    ] (refl … (lookup_opt … program_counter cost_labels)))
    14941488  ].
    1495   [3:
     1489  [2:
     1490    @pi2
     1491  |4:
    14961492    @(reachable_program_counter_witness lbl)
    14971493    assumption
    1498   |4:
     1494  |3:
    14991495    assumption
    15001496  |1:
    1501     #k #k_pres
    1502     @⊥ normalize in k_pres; /2/
    1503   |2:
    1504     #k #k_pres
    1505     @(eq_identifier_elim … k lbl)
     1497    %
    15061498    [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
    15101503    |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        ]
    15211528      ]
    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:
    15231542  ]
    15241543qed.
Note: See TracChangeset for help on using the changeset viewer.