Changeset 2264 for src/ASM/AssemblyProofSplitSplit.ma
 Timestamp:
 Jul 26, 2012, 12:38:42 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplitSplit.ma
r2140 r2264 38 38 >(eq_bv_eq … relevant) % 39 39 qed. 40 40 41 41 theorem main_thm: 42 42 ∀M, M': internal_pseudo_address_map. 43 43 ∀program: pseudo_assembly_program. 44 44 ∀program_in_bounds: \snd program ≤ 2^16. 45 ∀addr_of: Identifier → PreStatus pseudo_assembly_program program → BitVector 16. 45 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 46 let addr_of ≝ λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in 46 47 ∀is_well_labelled: is_well_labelled_p (\snd program). 47 48 ∀sigma: Word → Word. … … 53 54 ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) = 54 55 status_of_pseudo_status M' … 55 (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy. 56 #M #M' * #preamble #instr_list #program_in_bounds #addr_of 56 (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps) sigma policy) ps program_counter_in_bounds) sigma policy. 57 #M #M' * #preamble #instr_list #program_in_bounds 58 @pair_elim #labels #cost #create_label_cost_refl 57 59 #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps 58 60 letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds 59 61 change with (next_internal_pseudo_address_map0 ?????? = ? → ?) 60 62 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?; 61 @pair_elim #labels #costs #create_label_cost_refl normalize nodelta63 >create_label_cost_refl normalize nodelta 62 64 @pair_elim #assembled #costs' #assembly_refl normalize nodelta 63 65 lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled … … 87 89 (* XXX: we give the existential *) 88 90 %{0} 91 whd in match execute_1_pseudo_instruction0; normalize nodelta 92 change with (status_of_pseudo_status ????? = ?) cases daemon (*CSC: ??? 89 93 whd in match (execute_1_pseudo_instruction0 ?????); 90 94 (* XXX: work on the left hand side of the equality *) 91 95 whd in ⊢ (??%?); 92 96 @split_eq_status try % 93 /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) 97 /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) *) 94 98 6: (* Mov *) 95 99 #arg1 #arg2 #_ … … 114 118 #fetch_many_assm whd in fetch_many_assm; 115 119 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 116 destruct whd in ⊢ (??%?);120 destruct 117 121 (* XXX: now we start to work on the mk_PreStatus equality *) 118 122 (* XXX: lhs *) 119 123 change with (set_arg_16 ????? = ?) 120 >set_program_counter_mk_Status_commutation 121 >set_clock_mk_Status_commutation 122 >set_arg_16_mk_Status_commutation 123 (* XXX: rhs *) 124 change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%); 125 >set_program_counter_mk_Status_commutation 126 >set_clock_mk_Status_commutation 127 >set_arg_16_mk_Status_commutation in ⊢ (???%); 128 (* here we are *) 129 @split_eq_status try % 130 [1: 131 assumption 132 2: 133 @special_function_registers_8051_set_arg_16 % 134 ] 124 @set_arg_16_status_of_pseudo_status 125 [3: @(subaddressing_mode_elim … arg1) % 126 2: % 127  @sym_eq @set_clock_status_of_pseudo_status 128 [ @sym_eq @set_program_counter_status_of_pseudo_status [<EQnewpc %  %] 129  % ]] 135 130 1: (* Instruction *) 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 …) 140 (λ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))) 141 (refl …) ? (refl …)) 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 7: 153 <EQassembled assumption 154 ] 131 #instr #pi_refl 132 change with (execute_1_preinstruction ???????) in match (execute_1_pseudo_instruction0 ?????); 133 >EQassembled whd in match address_of_word_labels; normalize nodelta 134 >create_label_cost_refl in ⊢ (? → ? → ? → %); 135 @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness 136 ps ppc ? ? labels cost create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels 137 EQnewppc instr ? ? (refl …) ? (refl …) 138 (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1))) 139 (refl …) ? (refl …)) 140 try % try assumption >fetch_pseudo_refl assumption 155 141 4: (* Jmp *) 156 142 #arg1 #pi_refl
Note: See TracChangeset
for help on using the changeset viewer.