Ignore:
Timestamp:
Apr 23, 2012, 3:05:08 PM (8 years ago)
Author:
mulligan
Message:

Finished horror proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r1895 r1896  
    112112            reachable_program_counter code_memory fixed_program_size program_counter)
    113113        (good_program_witness: good_program code_memory fixed_program_size)
    114         (program_size_invariant: nat_of_bitvector … program_counter + program_size = fixed_program_size)
    115         (fixed_program_size_limit: fixed_program_size < 2^16 - 1)
     114        (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
     115        (fixed_program_size_limit: fixed_program_size < 2^16)
    116116        on program_size:
    117117          Σcost_map: identifier_map CostTag nat.
     
    123123  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
    124124  | S program_size' ⇒ λprogram_size_refl.
    125     (deplet 〈instruction, new_program_counter, ticks〉 as FETCH ≝ fetch … code_memory program_counter in
    126125    deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in
    127126    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
     
    131130      let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
    132131        add … cost_mapping lbl cost
    133     ] (refl … (lookup_opt … program_counter cost_labels)))
     132    ] (refl … (lookup_opt … program_counter cost_labels))
    134133  ] (refl … program_size).
    135134  [5:
     
    138137    @(reachable_program_counter_witness lbl)
    139138    @lookup_refl
    140   |3,6:
    141     cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
    142     [1,3:
    143       destruct
    144       @succ_nat_of_bitvector_half_add_1
    145       @(plus_lt_to_lt ? (S program_size') (2^16 - 1))
    146       assumption 
     139  |3:
     140    cases program_size_invariant
     141    [1:
     142      #destruct_assm @⊥ -traverse_code_internal destruct
    147143    |2:
    148       #S_assm %
     144      #program_size_invariant'
     145      %
    149146      [1:
    150147        #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
     
    156153          #neq_assm @present_add_miss try assumption
    157154          cases cost_mapping #cost_mapping' * #ind_hyp #_
    158           @(ind_hyp … lookup_opt_assm)
     155          inversion program_size'
    159156          [1:
    160             generalize in match (eqb_decidable (nat_of_bitvector … program_counter)
    161               (nat_of_bitvector … pc));
    162             #hyp cases hyp
     157            #program_size_refl_0 -traverse_code_internal destruct @⊥ cases neq_assm #assm @assm
     158            cut (Some … k = Some … lbl → k = lbl) (* XXX: lemma *)
    163159            [1:
    164               #eqb_assm generalize in match (eqb_true_to_refl … eqb_assm);
    165               #eqb_refl_assm
    166               -eqb_assm -hyp -ind_hyp -H1 -H2
    167               lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm)
    168               #program_counter_refl_assm -eqb_refl_assm
    169               <program_counter_refl_assm in lookup_opt_assm; <lookup_refl
    170               #Some_assm destruct(Some_assm)
    171               cases neq_assm #absurd_assm
    172               cases (absurd_assm (refl … k))
     160              #Some_assm destruct(Some_assm) %
    173161            |2:
    174               #eqb_assm generalize in match (eqb_false_to_not_refl … eqb_assm);
    175               #eqb_refl_assm
    176               -eqb_assm -hyp -ind_hyp -H1 -H2 -cost_mapping -traverse_code_internal
    177               <NEW_PC' in S_assm; #relevant <relevant -relevant
    178               change with (? < ?) (* XXX: open here *)
     162              #Some_assm @Some_assm <lookup_opt_assm >lookup_refl
     163              >(?:pc=program_counter)
     164              [1:
     165                %
     166              |2:
     167                @refl_nat_of_bitvector_to_refl
     168                @le_to_le_to_eq
     169                try assumption
     170                change with (? ≤ ?) in H2;
     171                @le_S_S_to_le
     172                assumption
     173              ]
    179174            ]
    180175          |2:
    181             generalize in match H2; <program_size_refl whd in ⊢ (??% → ?);
    182             >plus_n_Sm in ⊢ (% → ?);
    183             cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
     176            #n' #_ #program_size_refl_Sn' -traverse_code_internal destruct
     177            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
    184178            [1:
    185               <NEW_PC' %
     179              destruct
     180              @succ_nat_of_bitvector_half_add_1
     181              @(plus_lt_to_lt ? (S n') (2^16 - 1))
     182              @le_plus_to_minus_r
     183              change with (? < ?)
     184              <plus_n_Sm <plus_n_O >plus_n_Sm assumption
    186185            |2:
    187               #new_program_counter_assm' >new_program_counter_assm'
    188               >S_assm #relevant assumption
     186              #S_assm
     187              @(ind_hyp … lookup_opt_assm)
     188              [1:
     189                @(eqb_elim (nat_of_bitvector … program_counter)
     190                  (nat_of_bitvector … pc))
     191                [1:
     192                  #eqb_refl_assm
     193                  -ind_hyp -H1 -H2
     194                  lapply (refl_nat_of_bitvector_to_refl 16 program_counter pc eqb_refl_assm)
     195                  #program_counter_refl_assm -eqb_refl_assm
     196                  <program_counter_refl_assm in lookup_opt_assm; <lookup_refl
     197                  #Some_assm destruct(Some_assm)
     198                  cases neq_assm #absurd_assm
     199                  cases (absurd_assm (refl … k))
     200                |2:
     201                  #eqb_ref_assm
     202                  -ind_hyp
     203                  <NEW_PC' in S_assm; #relevant <relevant -relevant
     204                  change with (? < ?)
     205                  @le_neq_to_lt assumption
     206                ]
     207              |2:
     208                generalize in match H2; whd in ⊢ (??% → ?);
     209                >plus_n_Sm in ⊢ (% → ?);
     210                cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
     211                [1:
     212                  <NEW_PC' %
     213                |2:
     214                  #new_program_counter_assm' >new_program_counter_assm'
     215                  >S_assm #relevant assumption
     216                ]
     217              ]
    189218            ]
    190219          ]
     
    211240        ]
    212241      ]
    213     |4:
    214       #S_assm
    215       cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
    216       [1:
    217         <NEW_PC' %
    218       |2:
    219         #new_program_counter_assm' >new_program_counter_assm'
    220         <program_size_invariant <program_size_refl
    221         <S_assm normalize <plus_n_Sm %
    222       ]
    223242    ]
    224243  |1:
     
    237256    #inductive_hypothesis1 #inductive_hypothesis2 %
    238257    [1:
    239       #pc #k #H1 #H2 @inductive_hypothesis1
    240       try assumption
    241       (* XXX: same goal as above *)
     258      #pc #k #H1 #H2
     259      cases program_size_invariant
     260      [1:
     261        #destruct_assm @⊥ destruct
     262      |2:
     263        -program_size_invariant #program_size_invariant
     264        inversion program_size'
     265        [1:
     266          #program_size_refl_0 destruct
     267          #lookup_opt_Some_assm
     268          >(?:pc = program_counter) in lookup_opt_Some_assm;
     269          [1:
     270            #absurd <lookup_refl in absurd;
     271            #absurd destruct
     272          |2:
     273            @refl_nat_of_bitvector_to_refl
     274            @le_to_le_to_eq
     275            try assumption
     276            change with (? ≤ ?) in H2;
     277            @le_S_S_to_le
     278            assumption
     279          ]
     280        |2:
     281          #n' #_ #program_size_Sn_refl #Some_lookup_opt_refl
     282          @(inductive_hypothesis1 … pc) try assumption
     283          [1:
     284            @(eqb_elim … (nat_of_bitvector … program_counter)
     285              (nat_of_bitvector … pc));
     286            [1:
     287              #eq_assm
     288              lapply (refl_nat_of_bitvector_to_refl … eq_assm) #pc_refl
     289              <pc_refl in Some_lookup_opt_refl; <lookup_refl #absurd
     290              destruct
     291            |2:
     292              #neq_assm
     293              @(transitive_le ? (S (nat_of_bitvector … program_counter)))
     294              [1:
     295                cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
     296                [1:
     297                  destruct
     298                  @succ_nat_of_bitvector_half_add_1
     299                  @(plus_lt_to_lt ? (S n') (2^16 - 1))
     300                  @le_plus_to_minus_r
     301                  change with (? < ?)
     302                  <plus_n_Sm <plus_n_O >plus_n_Sm assumption
     303                |2:
     304                  #Sn_refl_assm >Sn_refl_assm <NEW_PC' @le_n
     305                ]
     306              |2:
     307                change with (? < ?)
     308                @le_neq_to_lt
     309                assumption
     310              ]
     311            ]
     312          |2:
     313            destruct
     314            @(transitive_le … H2)
     315            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
     316            [1:
     317              @succ_nat_of_bitvector_half_add_1
     318              @(plus_lt_to_lt ? (S n') (2^16 - 1))
     319              @le_plus_to_minus_r
     320              change with (? < ?)
     321              <plus_n_Sm <plus_n_O >plus_n_Sm assumption
     322            |2:
     323              #S_assm
     324              change with (S (S n' + ?) ≤ ?)
     325              >plus_n_Sm @monotonic_le_plus_r >S_assm
     326              <NEW_PC' @le_n
     327            ]
     328          ]
     329        ]
     330      ]
    242331    |2:
    243332      assumption
     333    ]
     334  |6:
     335    inversion program_size'
     336    [1:
     337      #_ %1 %
     338    |2:
     339      #n' #_ #program_size_refl_Sn @or_intror
     340      cases program_size_invariant
     341      [1:
     342        #absurd destruct
     343      |2:
     344        #relevant <relevant <plus_n_Sm <program_size_refl <plus_n_Sm
     345        @eq_f >program_size_refl_Sn <plus_n_Sm
     346        change with (? = (S ?) + ?) @eq_f2 try %
     347        cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
     348        [1:
     349          @succ_nat_of_bitvector_half_add_1
     350          @le_plus_to_minus_r
     351          @(transitive_le … fixed_program_size_limit)
     352          destruct <plus_n_Sm <plus_n_Sm
     353          change with (S (S ?) + ? ≤ S (S ?) + ?)
     354          @monotonic_le_plus_r @le_O_n
     355        |2:
     356          #S_assm
     357          cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
     358          [1:
     359            <NEW_PC' %
     360          |2:
     361           #new_program_counter_assm' >new_program_counter_assm'
     362           cases program_size_invariant
     363           [1:
     364             #destruct_assm destruct
     365           |2:
     366             #program_size_invariant
     367             <program_size_invariant <program_size_refl
     368             <S_assm normalize <plus_n_Sm %
     369           ]
     370         ]
     371      ]
     372    ]
    244373    ]
    245374  ]
Note: See TracChangeset for help on using the changeset viewer.