Changeset 1831


Ignore:
Timestamp:
Mar 13, 2012, 4:13:08 PM (8 years ago)
Author:
mulligan
Message:

small changes to asmcosts file to refactor proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1807 r1831  
    13961396    eqb l r = false → l ≠ r.
    13971397
     1398axiom le_neq_to_lt:
     1399  ∀m, n: nat.
     1400    m ≤ n → m ≠ n → m < n.
     1401
    13981402let rec traverse_code_internal
    13991403  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     
    14281432    ] (refl … (lookup_opt … program_counter cost_labels)))
    14291433  ] (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    #_ %
    14321440    [1:
    14331441      #pc #k #absurd1 #absurd2
     
    14381446      @⊥ normalize in k_pres; /2/
    14391447    ]
    1440   |2:
     1448  |4:
     1449    #S_assm
    14411450    cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
    14421451    [1:
    1443      
     1452      <NEW_PC' %
    14441453    |2:
    14451454      #new_program_counter_assm' >new_program_counter_assm'
     1455      <program_size_invariant <program_size_refl
     1456      <S_assm normalize <plus_n_Sm %
    14461457    ]
    1447   |3:
     1458  |6:
     1459    #_ assumption
     1460  |8:
     1461    #_ @(reachable_program_counter_witness lbl)
    14481462    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   
    14521537  |5:
    14531538    %
     
    14831568        @(ind_hyp … lookup_opt_assm)
    14841569        [1:
    1485           generalize in match (eqb_decidable (nat_of_bitvector … pc)
    1486             (nat_of_bitvector … new_program_counter'));
     1570          generalize in match (eqb_decidable (nat_of_bitvector … program_counter)
     1571            (nat_of_bitvector … pc));
    14871572          #hyp cases hyp
    14881573          [1:
    14891574            #relevant
    14901575            generalize in match (eqb_true_to_refl … relevant);
    1491             #refl_assm >refl_assm @le_n
     1576            #rewrite_assm <rewrite_assm
    14921577          |2:
    14931578            #relevant
    14941579            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
    14971584          ]
    14981585          (* XXX: case analysis over pc = new_program_counter' *)
Note: See TracChangeset for help on using the changeset viewer.