Changeset 2139


Ignore:
Timestamp:
Jun 28, 2012, 5:42:22 PM (5 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.

Location:
src/ASM
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r2128 r2139  
    977977    | JNZ j ⇒ j = id
    978978    | JB _ j ⇒ j = id
     979    | JNB _ j ⇒ j = id
    979980    | JBC _ j ⇒ j = id
    980981    | DJNZ _ j ⇒ j = id
  • src/ASM/AssemblyProofSplit.ma

    r2131 r2139  
    368368  ∀cm: pseudo_assembly_program.
    369369  ∀EQcm: cm = 〈preamble, instr_list〉.
     370  ∀is_well_labelled_witness: is_well_labelled_p instr_list.
    370371  ∀sigma: Word → Word.
    371372  ∀policy: Word → bool.
     
    373374  ∀ps: PseudoStatus cm.
    374375  ∀ppc: Word.
     376  ∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < |instr_list|.
    375377  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
    376378  ∀labels: label_map.
     
    384386  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
    385387  ∀instr: preinstruction Identifier.
     388  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
    386389  ∀ticks: nat × nat.
    387390  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr).
     
    400403                      status_of_pseudo_status M' cm s sigma policy).
    401404    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
    402   #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
    403   #costs #create_label_cost_refl #newppc
    404   #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr
     405  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
     406  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
     407  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
     408  #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
    405409  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
    406410  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
     
    10411045  >p normalize nodelta
    10421046  (* XXX: switch to the left hand side *)
    1043   -instr_refl >EQP -P normalize nodelta
     1047  >EQP -P normalize nodelta
    10441048  #sigma_increment_commutation #maps_assm #fetch_many_assm
    10451049 
     
    11741178      >EQaddr_of normalize nodelta
    11751179      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
    1176       >EQcm %
     1180      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
     1181      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
     1182      >create_label_cost_refl normalize nodelta #relevant @relevant
     1183      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
     1184      try assumption whd in match instruction_has_label; normalize nodelta
     1185      <instr_refl normalize nodelta %
    11771186    |7,15,23,31,45,57,65:
    11781187      >set_clock_mk_Status_commutation >program_counter_set_program_counter
  • 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 ⊢ (???%);
  • src/ASM/Status.ma

    r2123 r2139  
    11481148  λinstr_list.
    11491149  ∀id: Identifier.
    1150   ∀ppc. ∀ppc_ok.
     1150  ∀ppc.
     1151  ∀ppc_ok.
    11511152  ∀i.
    1152     fetch_pseudo_instruction instr_list ppc ppc_ok = i →
    1153       instruction_has_label id (\fst i)
     1153    \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) = i →
     1154      instruction_has_label id i
    11541155        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
    11551156
Note: See TracChangeset for help on using the changeset viewer.