Changeset 2032 for src/ASM/Interpret.ma
- Timestamp:
- Jun 8, 2012, 4:32:03 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret.ma
r2014 r2032 13 13 qed. 14 14 15 lemma eq_a_to_eq:16 ∀a,b.17 eq_a a b = true → a = b.18 #a #b19 cases a cases b20 #K21 try cases (eq_true_false K)22 %23 qed.24 25 lemma is_a_to_mem_to_is_in:26 ∀he,a,m,q.27 is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.28 #he #a #m #q29 elim q30 [1:31 #_ #K assumption32 |2:33 #m' #t #q' #II #H1 #H234 normalize35 change with (orb ??) in H2:(??%?);36 cases (inclusive_disjunction_true … H2)37 [1:38 #K39 <(eq_a_to_eq … K) >H1 %40 |2:41 #K42 >II43 try assumption44 cases (is_a t a)45 normalize46 %47 ]48 ]49 qed.50 51 15 lemma execute_1_technical: 52 16 ∀n, m: nat. … … 261 225 | DA addr ⇒ λinstr_refl. 262 226 let s ≝ add_ticks1 s in 263 let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in227 let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in 264 228 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then 265 229 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in 266 230 let cy_flag ≝ get_index' ? O ? flags in 267 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in231 let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in 268 232 if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then 269 233 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in … … 339 303 let s ≝ add_ticks1 s in 340 304 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 341 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in305 let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in 342 306 let new_acc ≝ nl @@ nu in 343 307 set_8051_sfr … s SFR_ACC_A new_acc … … 365 329 | XCHD addr1 addr2 ⇒ λinstr_refl. 366 330 let s ≝ add_ticks1 s in 367 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in368 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in331 let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in 332 let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in 369 333 let new_acc ≝ acc_nu @@ arg_nl in 370 334 let new_arg ≝ arg_nu @@ acc_nl in … … 685 649 | DA addr ⇒ λinstr_refl. 686 650 let s ≝ add_ticks1 s in 687 let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in651 let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in 688 652 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then 689 653 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in 690 654 let cy_flag ≝ get_index' ? O ? flags in 691 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in655 let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in 692 656 if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then 693 657 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in … … 763 727 let s ≝ add_ticks1 s in 764 728 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 765 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in729 let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in 766 730 let new_acc ≝ nl @@ nu in 767 731 set_8051_sfr … s SFR_ACC_A new_acc … … 789 753 | XCHD addr1 addr2 ⇒ λinstr_refl. 790 754 let s ≝ add_ticks1 s in 791 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in792 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in755 let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in 756 let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in 793 757 let new_acc ≝ acc_nu @@ arg_nl in 794 758 let new_arg ≝ arg_nu @@ acc_nl in … … 1026 990 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with 1027 991 [ ADDR11 a ⇒ λaddr11: True. 1028 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 program_counter in1029 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in992 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 program_counter in 993 let 〈nu, nl〉 ≝ vsplit ? 4 4 pc_bu in 1030 994 let bit ≝ get_index' ? O ? nl in 1031 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in995 let 〈relevant1, relevant2〉 ≝ vsplit ? 3 8 a in 1032 996 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 1033 997 let 〈carry, new_pc〉 ≝ half_add ? program_counter new_addr in … … 1049 1013 | _ ⇒ false 1050 1014 ]. 1051 1052 let rec member_addressing_mode_tag1053 (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)1054 on v: Prop ≝1055 match v with1056 [ VEmpty ⇒ False1057 | VCons n' hd tl ⇒1058 bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a1059 ].1060 1061 lemma is_a_decidable:1062 ∀hd.1063 ∀element.1064 is_a hd element = true ∨ is_a hd element = false.1065 #hd #element //1066 qed.1067 1068 lemma mem_decidable:1069 ∀n: nat.1070 ∀v: Vector addressing_mode_tag n.1071 ∀element: addressing_mode_tag.1072 mem … eq_a n v element = true ∨1073 mem … eq_a … v element = false.1074 #n #v #element //1075 qed.1076 1077 lemma eq_a_elim:1078 ∀tag.1079 ∀hd.1080 ∀P: bool → Prop.1081 (tag = hd → P (true)) →1082 (tag ≠ hd → P (false)) →1083 P (eq_a tag hd).1084 #tag #hd #P1085 cases tag1086 cases hd1087 #true_hyp #false_hyp1088 try @false_hyp1089 try @true_hyp1090 try %1091 #absurd destruct(absurd)1092 qed.1093 1094 lemma is_a_true_to_is_in:1095 ∀n: nat.1096 ∀x: addressing_mode.1097 ∀tag: addressing_mode_tag.1098 ∀supervector: Vector addressing_mode_tag n.1099 mem addressing_mode_tag eq_a n supervector tag →1100 is_a tag x = true →1101 is_in … supervector x.1102 #n #x #tag #supervector1103 elim supervector1104 [1:1105 #absurd cases absurd1106 |2:1107 #n' #hd #tl #inductive_hypothesis1108 whd in match (mem … eq_a (S n') (hd:::tl) tag);1109 @eq_a_elim normalize nodelta1110 [1:1111 #tag_hd_eq #irrelevant1112 whd in match (is_in (S n') (hd:::tl) x);1113 <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta1114 @I1115 |2:1116 #tag_hd_neq1117 whd in match (is_in (S n') (hd:::tl) x);1118 change with (1119 mem … eq_a n' tl tag)1120 in match (fold_right … n' ? false tl);1121 #mem_hyp #is_a_hyp1122 cases(is_a hd x)1123 [1:1124 normalize nodelta //1125 |2:1126 normalize nodelta1127 @inductive_hypothesis assumption1128 ]1129 ]1130 ]1131 qed.1132 1133 lemma is_in_subvector_is_in_supervector:1134 ∀m, n: nat.1135 ∀subvector: Vector addressing_mode_tag m.1136 ∀supervector: Vector addressing_mode_tag n.1137 ∀element: addressing_mode.1138 subvector_with … eq_a subvector supervector →1139 is_in m subvector element → is_in n supervector element.1140 #m #n #subvector #supervector #element1141 elim subvector1142 [1:1143 #subvector_with_proof #is_in_proof1144 cases is_in_proof1145 |2:1146 #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof1147 whd in match (is_in … (hd':::tl') element);1148 cases (is_a_decidable hd' element)1149 [1:1150 #is_a_true >is_a_true1151 #irrelevant1152 whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;1153 @(is_a_true_to_is_in … is_a_true)1154 lapply(subvector_with_proof)1155 cases(mem … eq_a n supervector hd') //1156 |2:1157 #is_a_false >is_a_false normalize nodelta1158 #assm1159 @inductive_hypothesis1160 [1:1161 generalize in match subvector_with_proof;1162 whd in match (subvector_with … eq_a (hd':::tl') supervector);1163 cases(mem_decidable n supervector hd')1164 [1:1165 #mem_true >mem_true normalize nodelta1166 #assm assumption1167 |2:1168 #mem_false >mem_false #absurd1169 cases absurd1170 ]1171 |2:1172 assumption1173 ]1174 ]1175 ]1176 qed.1177 1178 let rec subaddressing_mode_elim_type1179 (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)1180 (Q: addressing_mode → T → Prop)1181 (p_addr11: ∀w: Word11. is_in m fixed_v (ADDR11 w) → T)1182 (p_addr16: ∀w: Word. is_in m fixed_v (ADDR16 w) → T)1183 (p_direct: ∀w: Byte. is_in m fixed_v (DIRECT w) → T)1184 (p_indirect: ∀w: Bit. is_in m fixed_v (INDIRECT w) → T)1185 (p_ext_indirect: ∀w: Bit. is_in m fixed_v (EXT_INDIRECT w) → T)1186 (p_acc_a: is_in m fixed_v ACC_A → T)1187 (p_register: ∀w: BitVector 3. is_in m fixed_v (REGISTER w) → T)1188 (p_acc_b: is_in m fixed_v ACC_B → T)1189 (p_dptr: is_in m fixed_v DPTR → T)1190 (p_data: ∀w: Byte. is_in m fixed_v (DATA w) → T)1191 (p_data16: ∀w: Word. is_in m fixed_v (DATA16 w) → T)1192 (p_acc_dptr: is_in m fixed_v ACC_DPTR → T)1193 (p_acc_pc: is_in m fixed_v ACC_PC → T)1194 (p_ext_indirect_dptr: is_in m fixed_v EXT_INDIRECT_DPTR → T)1195 (p_indirect_dptr: is_in m fixed_v INDIRECT_DPTR → T)1196 (p_carry: is_in m fixed_v CARRY → T)1197 (p_bit_addr: ∀w: Byte. is_in m fixed_v (BIT_ADDR w) → T)1198 (p_n_bit_addr: ∀w: Byte. is_in m fixed_v (N_BIT_ADDR w) → T)1199 (p_relative: ∀w: Byte. is_in m fixed_v (RELATIVE w) → T)1200 (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)1201 on v: Prop ≝1202 match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with1203 [ VEmpty ⇒ λm_refl. λv_refl.1204 ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.1205 Q addr (1206 match addr return λx: addressing_mode. is_in … fixed_v x → T with1207 [ ADDR11 x ⇒ p_addr11 x1208 | ADDR16 x ⇒ p_addr16 x1209 | DIRECT x ⇒ p_direct x1210 | INDIRECT x ⇒ p_indirect x1211 | EXT_INDIRECT x ⇒ p_ext_indirect x1212 | ACC_A ⇒ p_acc_a1213 | REGISTER x ⇒ p_register x1214 | ACC_B ⇒ p_acc_b1215 | DPTR ⇒ p_dptr1216 | DATA x ⇒ p_data x1217 | DATA16 x ⇒ p_data16 x1218 | ACC_DPTR ⇒ p_acc_dptr1219 | ACC_PC ⇒ p_acc_pc1220 | EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr1221 | INDIRECT_DPTR ⇒ p_indirect_dptr1222 | CARRY ⇒ p_carry1223 | BIT_ADDR x ⇒ p_bit_addr x1224 | N_BIT_ADDR x ⇒ p_n_bit_addr x1225 | RELATIVE x ⇒ p_relative x1226 ] p)1227 | VCons n' hd tl ⇒ λm_refl. λv_refl.1228 let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr111229 p_addr16 p_direct p_indirect p_ext_indirect p_acc_a1230 p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr1231 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry1232 p_bit_addr p_n_bit_addr p_relative n' tl ?1233 in1234 match hd return λa: addressing_mode_tag. a = hd → ? with1235 [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call1236 | addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call1237 | direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call1238 | indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call1239 | ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call1240 | acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call1241 | registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call1242 | acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call1243 | dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call1244 | data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call1245 | data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call1246 | acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call1247 | acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call1248 | ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call1249 | indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call1250 | carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call1251 | bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call1252 | n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call1253 | relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call1254 ] (refl … hd)1255 ] (refl … n) (refl_jmeq … v).1256 [20:1257 generalize in match proof; destruct1258 whd in match (subvector_with … eq_a (hd:::tl) fixed_v);1259 cases (mem … eq_a m fixed_v hd) normalize nodelta1260 [1:1261 whd in match (subvector_with … eq_a tl fixed_v);1262 #assm assumption1263 |2:1264 normalize in ⊢ (% → ?);1265 #absurd cases absurd1266 ]1267 ]1268 @(is_in_subvector_is_in_supervector … proof)1269 destruct @I1270 qed.1271 1272 (* XXX: todo *)1273 lemma subaddressing_mode_elim':1274 ∀T: Type[2].1275 ∀n: nat.1276 ∀o: nat.1277 ∀v1: Vector addressing_mode_tag n.1278 ∀v2: Vector addressing_mode_tag o.1279 ∀Q: addressing_mode → T → Prop.1280 ∀fixed_v: Vector addressing_mode_tag (n + o).1281 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.1282 ∀fixed_v_proof: fixed_v = v1 @@ v2.1283 ∀subaddressing_mode_proof.1284 subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P71285 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.1286 #T #n #o #v1 #v21287 elim v1 cases v21288 [1:1289 #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P101290 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof1291 #subaddressing_mode_proof destruct normalize1292 #addr #absurd cases absurd1293 |2:1294 #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P101295 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof1296 destruct normalize in match ([[]]@@hd:::tl);1297 ]1298 cases daemon1299 qed.1300 1301 (* XXX: todo *)1302 lemma subaddressing_mode_elim:1303 ∀T: Type[2].1304 ∀m: nat.1305 ∀n: nat.1306 ∀Q: addressing_mode → T → Prop.1307 ∀fixed_v: Vector addressing_mode_tag m.1308 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.1309 ∀v: Vector addressing_mode_tag n.1310 ∀proof.1311 subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P71312 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.1313 #T #m #n #Q #fixed_v1314 elim fixed_v1315 [1:1316 #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P131317 #P14 #P15 #P16 #P17 #P18 #P19 #v #proof1318 normalize1319 |2:1320 ]1321 cases daemon1322 qed.1323 1015 1324 1016 definition program_counter_after_other ≝ … … 1397 1089 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1398 1090 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1399 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in1091 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in 1400 1092 let s ≝ write_at_stack_pointer … s pc_bl in 1401 1093 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1402 1094 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1403 1095 let s ≝ write_at_stack_pointer … s pc_bu in 1404 let 〈thr, eig〉 ≝ split ? 3 8 a in1405 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in1096 let 〈thr, eig〉 ≝ vsplit ? 3 8 a in 1097 let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in 1406 1098 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 1407 1099 set_program_counter … s new_addr … … 1415 1107 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1416 1108 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1417 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in1109 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in 1418 1110 let s ≝ write_at_stack_pointer … s pc_bl in 1419 1111 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in … … 1515 1207 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1516 1208 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1517 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in1209 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in 1518 1210 let s ≝ write_at_stack_pointer … s pc_bl in 1519 1211 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
Note: See TracChangeset
for help on using the changeset viewer.