Ignore:
Timestamp:
May 22, 2012, 11:15:12 AM (7 years ago)
Author:
mulligan
Message:

Changes to simplify the simpler cases of the main_lemma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r1979 r1983  
    4545        (clock … s).
    4646  //
    47 qed.       
     47qed.
    4848
    4949lemma set_clock_mk_Status_commutation:
     
    158158  #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm
    159159  assumption
     160qed.
     161
     162lemma fetch_many_singleton:
     163  ∀code_memory: BitVectorTrie Byte 16.
     164  ∀final_pc, start_pc: Word.
     165  ∀i: instruction.
     166    fetch_many code_memory final_pc start_pc [i] →
     167      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc.
     168  #code_memory #final_pc #start_pc #i * #new_pc *
     169  #fetch_refl #fetch_many_assm whd in fetch_many_assm;
     170  cases (eq_bv_eq … fetch_many_assm) assumption
    160171qed.
    161172
     
    181192 ∀EQlookup_labels : lookup_labels = (λx:Identifier.sigma (address_of_word_labels_code_mem instr_list x)).
    182193 ∀lookup_datalabels : identifier ASMTag→Word.
    183  ∀ EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
     194 ∀EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
    184195 ∀EQnewppc : newppc=add 16 ppc (bitvector_of_nat 16 1).
    185196 ∀instr: preinstruction Identifier.
     
    209220    M cm ps
    210221    =Some internal_pseudo_address_map M'
    211     →fetch_many (load_code_memory assembled)
    212      (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma ppc)
    213      (expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels
     222    →fetch_many (load_code_memory (\fst  (assembly cm sigma policy)))
     223     (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps))
     224     (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels
    214225      (Instruction instr))
    215226     →P (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm
     
    640651  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
    641652  (* XXX: work on fetch_many *)
    642   <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
    643   whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    644   whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
    645   <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
    646   #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
    647   >(eq_bv_eq … fetch_many_assm) -newpc
    648   >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
     653  <instr_refl in fetch_many_assm; #fetch_many_assm
     654  <(fetch_many_singleton … fetch_many_assm) whd in ⊢ (??%?);
    649655  (* XXX: work on sigma commutation *)
    650   <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 
     656  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
    651657  (* XXX: work on both sides *)
    652658  [1,2,3,4,5:
     
    662668  normalize nodelta
    663669  (* XXX: work on ticks (of all kinds) *)
    664   >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
     670  <instr_refl in EQticks; #EQticks >EQticks
    665671  (* XXX: removes status 's' *)
    666672  normalize nodelta >EQs -s -ticks
Note: See TracChangeset for help on using the changeset viewer.