Ignore:
Timestamp:
Jun 28, 2012, 5:42:22 PM (7 years ago)
Author:
mulligan
Message:

Changes to get the main lemma compiling again. Changes pushed into
the first half of the proof of the main theorem, too.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplitSplit.ma

    r2131 r2139  
    134134      ]
    135135    |1: (* Instruction *)
    136       #instr #_ #EQP #EQnext #fetch_many_assm
    137       @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness
    138         ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
    139         EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
     136      #instr #pi_refl #EQP #EQnext #fetch_many_assm
     137      @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
     138        ps ppc ? ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
     139        EQnewppc instr ? (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
    140140        (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
    141141        (refl …) ? (refl …))
    142       [1,2,3: try assumption try %] >assembly_refl assumption
     142      [1,2:
     143        assumption
     144      |3:
     145        %
     146      |4:
     147        >fetch_pseudo_refl @pi_refl
     148      |5:
     149        <EQP %
     150      |6:
     151        >assembly_refl assumption
     152      ]
    143153    |4: (* Jmp *)
    144154      #arg1 #pi_refl
     
    199209          >(andb_true_l … sj_possible_refl) @I
    200210        ]
    201         @(is_well_labelled_witness … fetch_pseudo_refl)
     211        whd in is_well_labelled_witness;
     212        @(is_well_labelled_witness ? ppc ppc_in_bounds pi)
     213        try (>fetch_pseudo_refl %)
    202214        >pi_refl %
    203215      |2:
     
    256268          @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl normalize nodelta
    257269          <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
    258           #relevant >fst_5_rest_refl
     270          #relevant
    259271          lapply pc_bu_bl_refl' -pc_bu_bl_refl'
    260272          >program_counter_set_8051_sfr >set_clock_set_program_counter
     
    278290              <(vsplit_ok ?????? (sym_eq … thr_eig_refl)) @eq_f
    279291            ]
    280           ]
     292          ] *)
    281293        |4:
    282294          >set_program_counter_mk_Status_commutation in ⊢ (???%);
Note: See TracChangeset for help on using the changeset viewer.