Changeset 2051
 Timestamp:
 Jun 12, 2012, 5:49:02 PM (6 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2048 r2051 20 20 λpc_plus_jmp_length.λaddr.(*λinstr.*) 21 21 let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in 22 let 〈upper, lower〉 ≝ vsplit ? 8 8result in22 let 〈upper, lower〉 ≝ vsplit ? 9 7 result in 23 23 if get_index' ? 2 0 flags then 24 〈eq_bv 8 upper [[true;true;true;true;true;true;true;true]],lower〉24 〈eq_bv 9 upper [[true;true;true;true;true;true;true;true;true]], true:::lower〉 25 25 else 26 〈eq_bv 8 upper (zero 8), zero 8〉.26 〈eq_bv 9 upper (zero …), false:::lower〉. 27 27 28 28 definition medium_jump_cond: Word → Word → (*pseudo_instruction →*) 
src/ASM/AssemblyProofSplitSplit.ma
r2047 r2051 1 1 include "ASM/AssemblyProofSplit.ma". 2 2 include "common/LabelledObjects.ma". 3 4 check pseudo_instruction5 3 6 4 definition instruction_has_label ≝ … … 35 33 occurs_exactly_once ASMTag pseudo_instruction id instr_list. 36 34 35 (*CSC: move elsewhere *) 36 axiom sub_16_to_add_16_8_0: 37 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 38 get_index' ? 2 0 flags = false → 39 sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 → 40 v1 = add ? v2 (sign_extension (false:::v3)). 41 42 (*CSC: move elsewhere *) 43 axiom sub_16_to_add_16_8_1: 44 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 45 get_index' ? 2 0 flags = true → 46 sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 → 47 v1 = add ? v2 (sign_extension (true:::v3)). 48 49 (*CSC: move elsewhere *) 50 lemma vsplit_ok: 51 ∀A: Type[0]. 52 ∀m, n: nat. 53 ∀v: Vector A (m + n). 54 ∀upper: Vector A m. 55 ∀lower: Vector A n. 56 〈upper, lower〉 = vsplit A m n v → 57 upper @@ lower = v. 58 #A #m #n #v #upper #lower 59 cases daemon 60 qed. 61 62 lemma short_jump_cond_ok: 63 ∀v1, v2: Word. 64 ∀is_possible, offset. 65 〈is_possible, offset〉 = short_jump_cond v1 v2 → 66 is_possible → v2 = add 16 v1 (sign_extension offset). 67 #v1 #v2 #is_possible #offset 68 whd in match short_jump_cond; normalize nodelta 69 @pair_elim #result #flags #sub16_refl 70 @pair_elim #upper #lower #vsplit_refl 71 inversion (get_index' bool ???) #get_index_refl normalize nodelta 72 #relevant destruct(relevant) #relevant 73 [1: 74 @(sub_16_to_add_16_8_1 … flags) 75 2: 76 @(sub_16_to_add_16_8_0 … flags) 77 ] 78 try assumption >sub16_refl 79 <(eq_bv_eq … relevant) 80 >(vsplit_ok … (sym_eq … vsplit_refl)) % 81 qed. 82 83 lemma medium_jump_cond_ok: 84 ∀v1, v2: Word. 85 ∀is_possible, offset, v1_upper, v1_lower. 86 〈is_possible, offset〉 = medium_jump_cond v1 v2 → 87 〈v1_upper, v1_lower〉 = vsplit ? 5 11 v1 → 88 is_possible → v2 = v1_upper @@ offset. 89 #v1 #v2 #is_possible #offset #v1_upper #v1_lower 90 whd in match medium_jump_cond; normalize nodelta 91 @pair_elim #fst_5_addr #rest_addr #vsplit_v2_refl 92 @pair_elim #fst_5_pc #rest_pc #vsplit_v1_refl 93 #relevant destruct(relevant) normalize nodelta #relevant 94 destruct(relevant) #relevant 95 <(vsplit_ok … (sym_eq … vsplit_v2_refl)) 96 >(eq_bv_eq … relevant) % 97 qed. 98 37 99 theorem main_thm: 38 100 ∀M, M': internal_pseudo_address_map. … … 81 143 (* XXX: work on the left hand side of the equality *) 82 144 whd in ⊢ (??%?); 83 @split_eq_status //84 [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ]145 @split_eq_status try % 146 /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) 85 147 6: (* Mov *) 86 148 #arg1 #arg2 #_ … … 137 199 whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?); 138 200 whd in match (expand_pseudo_instruction ??????); 139 (* generalize in match (refl … (expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels (Jmp arg1))); 140 whd in match (expand_pseudo_instruction ??????) in ⊢ (??%? → % → ?); *) 141 inversion (sub_16_with_carry ???) #result #flags #sub16_refl normalize nodelta 142 inversion (vsplit ????) #upper #lower #vsplit_refl normalize nodelta 143 inversion (eq_bv ??? ∧ ¬ policy ?) #eq_bv_policy_refl normalize nodelta 201 inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta 202 inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta 144 203 [2: 145 inversion (vsplit ????) #fst_5_addr #rest_addr #addr_refl normalize nodelta 146 inversion (vsplit ????) #fst_5_pc #rest_pc #pc_refl normalize nodelta 147 cases (eq_bv ??? ∧ ¬ policy ?) normalize nodelta 204 inversion (medium_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta 205 inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta 148 206 ] 149 207 #sigma_increment_commutation … … 160 218 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 161 219 whd in fetch_many_assm; 162 >EQassembled in fetch_refl; #fetch_refl <fetch_refl fetch_refl220 >EQassembled in fetch_refl; #fetch_refl <fetch_refl 163 221 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 164 222 whd in ⊢ (??%%); … … 177 235 normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm 178 236 [1: 179 address_of_word_labels_assm >EQnewpc >pc_refl normalize nodelta 180 >(pair_destruct_2 ????? (sym_eq … addr_refl)) 181 >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc 182 (* XXX: true but needs lemma about splitting *) 183 cases daemon 237 >EQnewpc 238 inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta 239 @sym_eq >address_of_word_labels_assm 240 [1: 241 >EQlookup_labels in mjc_refl; #mjc_refl 242 @(medium_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl)) 243 >(andb_true_l … mj_possible_refl) @I 244 ] 184 245 3: 185 >EQnewpc >pc_refl normalize nodelta186 >(pair_destruct_2 ????? (sym_eq … addr_refl))187 >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc188 246 >EQlookup_labels normalize nodelta 189 247 >address_of_word_labels_assm try % 190 248 5: 191 249 >EQnewpc 250 inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta 251 @sym_eq >address_of_word_labels_assm 252 [1: 253 >EQlookup_labels in sjc_refl; #sjc_refl 254 >(pair_destruct_2 ????? (sym_eq … half_add_refl)) 255 @(short_jump_cond_ok ???? (sym_eq … sjc_refl)) 256 >(andb_true_l … sj_possible_refl) @I 257 ] 192 258 ] 193 259 @(is_well_labelled_witness … fetch_pseudo_refl) 194 260 >pi_refl % 195 261 2: 196 whd in match compute_target_of_unconditional_jump; normalize nodelta 197 >program_counter_set_program_counter 198 cases (vsplit ????) #pc_bu #pc_bl normalize nodelta 199 cases (vsplit ????) #nu #nl normalize nodelta 200 cases (vsplit ????) #relevant1 #relevant2 normalize nodelta 201 change with (add ???) in match (\snd (half_add ???)); >EQnewpc 202 cases daemon 203 3: 204 whd in ⊢ (??%%); 205 /demod nohyps/ 206 cases daemon 262 whd in ⊢ (??(?%%)%); 263 cut (∃b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11. address = [[b1;b2;b3;b4;b5;b6;b7;b8;b9;b10;b11]]) 264 [1: 265 cases daemon (* XXX: easy but massive proof, move into separate lemma *) 266 2: 267 * * * * * * * #b4 * #b5 268 * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl 269 normalize in match (fetch ??); <plus_n_Sm @eq_f 270 @commutative_plus 271 ] 207 272 ] 208 273 5: (* Call *) 
src/ASM/Interpret.ma
r2047 r2051 1170 1170 1171 1171 lemma execute_1_ok: ∀cm.∀s. 1172 let instr_pc_ticks ≝ fetch cm (program_counter … s) in1173 (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧1172 (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧ 1173 let instr_pc_ticks ≝ fetch cm (program_counter … s) in 1174 1174 (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other → 1175 1175 program_counter ? cm (execute_1 cm s) =
Note: See TracChangeset
for help on using the changeset viewer.