Changeset 1983


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

Changes to simplify the simpler cases of the main_lemma.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1975 r1983  
    14351435  [ nil ⇒ eq_bv … pc final_pc = true
    14361436  | cons i tl ⇒
    1437     let fetched ≝ fetch code_memory pc in
    1438     let 〈instr_pc, ticks〉 ≝ fetched in
    1439     let 〈instr,pc'〉 ≝ instr_pc in
    1440       eq_instruction instr i = true ∧
    1441         ticks = (ticks_of_instruction i) ∧
    1442         fetch_many code_memory final_pc pc' tl
     1437      (∃pc': Word. 〈i, pc', ticks_of_instruction i〉 = fetch code_memory pc ∧
     1438        fetch_many code_memory final_pc pc' tl)
    14431439  ].
    14441440
     
    15061502    #i #tl #IH #pc #H whd
    15071503    cases (encoding_check_append ????? H) -H #H1 #H2
    1508     @pair_elim #instr_pc #ticks #fetch_refl normalize nodelta
    1509     @pair_elim #instr #pc' #instr_pc_refl normalize nodelta
    1510     lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);
    1511     #H3 lapply (H3 H1) -H3 >fetch_refl >instr_pc_refl normalize nodelta
    1512     #H3 lapply (conjunction_true ?? H3) * #H4 #H5 %
    1513     [1:
    1514       lapply (conjunction_true … H4) * #B1 #B2
    1515       % try assumption @eqb_true_to_eq
    1516       <(eq_instruction_to_eq … B1) assumption
    1517     |2:
    1518       >(eq_bv_eq … H5) @IH @H2
    1519     ]
     1504    lapply (fetch_assembly pc i code_memory (assembly1 i) (refl …)) whd in ⊢ (% → ?);   
     1505    cases (fetch ??) * #instr #pc' #ticks
     1506    #H3 lapply (H3 H1) -H3 normalize nodelta #H3
     1507    lapply (conjunction_true ?? H3) * #H4 #H5
     1508    lapply (conjunction_true … H4) * #B1 #B2
     1509    %{pc'} <(eq_instruction_to_eq … B1) >(eq_bv_eq … H5)
     1510    >(eqb_true_to_refl … B2) % try % @IH @H2
    15201511  ]
    15211512qed.
  • 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.