Changeset 2139 for src/ASM/AssemblyProofSplitSplit.ma
- Timestamp:
- Jun 28, 2012, 5:42:22 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplitSplit.ma
r2131 r2139 134 134 ] 135 135 |1: (* Instruction *) 136 #instr # _#EQP #EQnext #fetch_many_assm137 @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness138 ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels139 EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)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 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 141 (refl …) ? (refl …)) 142 [1,2,3: try assumption try %] >assembly_refl assumption 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 ] 143 153 |4: (* Jmp *) 144 154 #arg1 #pi_refl … … 199 209 >(andb_true_l … sj_possible_refl) @I 200 210 ] 201 @(is_well_labelled_witness … fetch_pseudo_refl) 211 whd in is_well_labelled_witness; 212 @(is_well_labelled_witness ? ppc ppc_in_bounds pi) 213 try (>fetch_pseudo_refl %) 202 214 >pi_refl % 203 215 |2: … … 256 268 @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl normalize nodelta 257 269 <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta 258 #relevant >fst_5_rest_refl270 #relevant 259 271 lapply pc_bu_bl_refl' -pc_bu_bl_refl' 260 272 >program_counter_set_8051_sfr >set_clock_set_program_counter … … 278 290 <(vsplit_ok ?????? (sym_eq … thr_eig_refl)) @eq_f 279 291 ] 280 ] 292 ] *) 281 293 |4: 282 294 >set_program_counter_mk_Status_commutation in ⊢ (???%);
Note: See TracChangeset
for help on using the changeset viewer.