Changeset 1983
 Timestamp:
 May 22, 2012, 11:15:12 AM (7 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1975 r1983 1435 1435 [ nil ⇒ eq_bv … pc final_pc = true 1436 1436  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) 1443 1439 ]. 1444 1440 … … 1506 1502 #i #tl #IH #pc #H whd 1507 1503 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 1520 1511 ] 1521 1512 qed. 
src/ASM/AssemblyProofSplit.ma
r1979 r1983 45 45 (clock … s). 46 46 // 47 qed. 47 qed. 48 48 49 49 lemma set_clock_mk_Status_commutation: … … 158 158 #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm 159 159 assumption 160 qed. 161 162 lemma 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 160 171 qed. 161 172 … … 181 192 ∀EQlookup_labels : lookup_labels = (λx:Identifier.sigma (address_of_word_labels_code_mem instr_list x)). 182 193 ∀lookup_datalabels : identifier ASMTag→Word. 183 ∀ 194 ∀EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). 184 195 ∀EQnewppc : newppc=add 16 ppc (bitvector_of_nat 16 1). 185 196 ∀instr: preinstruction Identifier. … … 209 220 M cm ps 210 221 =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 ppclookup_datalabels222 →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 214 225 (Instruction instr)) 215 226 →P (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm … … 640 651 >EQP <instr_refl normalize nodelta whd in ⊢ (??%?); 641 652 (* 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 ⊢ (??%?); 649 655 (* 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 651 657 (* XXX: work on both sides *) 652 658 [1,2,3,4,5: … … 662 668 normalize nodelta 663 669 (* XXX: work on ticks (of all kinds) *) 664 >EQticks' ticks'<instr_refl in EQticks; #EQticks >EQticks670 <instr_refl in EQticks; #EQticks >EQticks 665 671 (* XXX: removes status 's' *) 666 672 normalize nodelta >EQs s ticks
Note: See TracChangeset
for help on using the changeset viewer.