Ignore:
Timestamp:
Jun 28, 2012, 5:42:22 PM (8 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/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
Note: See TracChangeset for help on using the changeset viewer.