Changeset 2131 for src/ASM/AssemblyProofSplitSplit.ma
 Timestamp:
 Jun 28, 2012, 12:55:05 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplitSplit.ma
r2129 r2131 63 63 lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled 64 64 @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta 65 @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels65 @(pose … (λx. bitvector_of_nat ? (lookup_def … labels x 0))) #lookup_labels #EQlookup_labels 66 66 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels 67 67 whd in match execute_1_pseudo_instruction; normalize nodelta 68 68 whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta 69 69 lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc 70 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?) 71 [1: >fetch_pseudo_refl % 2: skip 3: assumption ] 70 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc … pi … lookup_labels lookup_datalabels) 71 [1: assumption 2: assumption] >create_label_cost_refl 72 #X lapply (X EQlookup_labels EQlookup_datalabels ?) X 73 [1: >fetch_pseudo_refl %] 72 74 #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3; 73 75 generalize in match assm1; assm1 assm2 assm3 74 76 normalize nodelta 75 77 inversion pi 76 [ (*2,3:78 [2,3: 77 79 #arg #_ 78 80 (* XXX: we first work on sigma_increment_commutation *) … … 138 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))) 139 141 (refl …) ? (refl …)) 140 try assumption try %>assembly_refl assumption142 [1,2,3: try assumption try %] >assembly_refl assumption 141 143 4: (* Jmp *) 142 144 #arg1 #pi_refl … … 182 184 >EQnewpc 183 185 inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta 184 @sym_eq >address_of_word_labels_assm 185 [1: 186 >EQlookup_labels in mjc_refl; #mjc_refl 187 @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl)) 188 >(andb_true_l … mj_possible_refl) @I 189 ] 186 @sym_eq 187 >EQlookup_labels in mjc_refl; #mjc_refl 188 @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl)) 189 >(andb_true_l … mj_possible_refl) @I 190 190 3: 191 >EQlookup_labels normalize nodelta 192 >address_of_word_labels_assm try % 191 >EQlookup_labels normalize nodelta % 193 192 5: 194 193 >EQnewpc 195 194 inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta 196 @sym_eq >address_of_word_labels_assm 197 [1: 198 >EQlookup_labels in sjc_refl; #sjc_refl 199 >(pair_destruct_2 ????? (sym_eq … half_add_refl)) 200 @(short_jump_cond_ok ???? (sym_eq … sjc_refl)) 201 >(andb_true_l … sj_possible_refl) @I 202 ] 195 @sym_eq 196 >EQlookup_labels in sjc_refl; #sjc_refl 197 >(pair_destruct_2 ????? (sym_eq … half_add_refl)) 198 @(short_jump_cond_ok ???? (sym_eq … sjc_refl)) 199 >(andb_true_l … sj_possible_refl) @I 203 200 ] 204 201 @(is_well_labelled_witness … fetch_pseudo_refl) … … 212 209 @commutative_plus 213 210 ] 214  *)5: (* Call *)211 5: (* Call *) 215 212 #arg1 #pi_refl 216 213 (* XXX: we first work on sigma_increment_commutation *) … … 249 246 @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl') 250 247 try /demod nohyps/ [1: %] 251 @pair_elim #thr #eig #thr_eig_refl252 248 @pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%); 253 249 @split_eq_status try /demod nohyps/ try % … … 256 252 cases daemon 257 253 3: 258 >program_counter_set_program_counter259 254 whd in ajc_refl:(??%?); lapply ajc_refl ajc_refl map_refl_assm Mrefl 260 255 >EQlookup_labels normalize nodelta … … 262 257 <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta 263 258 #relevant >fst_5_rest_refl 264 check absolute_jump_cond265 <(vsplit_ok ?????? (sym_eq … thr_eig_refl))266 259 lapply pc_bu_bl_refl' pc_bu_bl_refl' 267 260 >program_counter_set_8051_sfr >set_clock_set_program_counter
Note: See TracChangeset
for help on using the changeset viewer.