Changeset 1515 for src/ASM/Status.ma
 Timestamp:
 Nov 18, 2011, 1:03:14 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Status.ma
r1459 r1515 702 702 λr: BitVector 3. 703 703 let address ≝ bit_address_of_register ? s r in 704 lookup …address (low_internal_ram ? s) (zero 8).704 lookup ?? address (low_internal_ram ? s) (zero 8). 705 705 706 706 definition set_register ≝ … … 717 717 λM: Type[0]. 718 718 λs: PreStatus M. 719 let 〈 nu, nl 〉 ≝ split …4 4 (get_8051_sfr ? s SFR_SP) in719 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_SP) in 720 720 let m ≝ get_index_v … nu O ? in 721 721 let r1 ≝ get_index_v … nu 1 ? in … … 804 804 λext_indirect_dptr: True. 805 805 let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 806 lookup …16 address (external_ram ? s) (zero 8)806 lookup ? 16 address (external_ram ? s) (zero 8) 807 807  EXT_INDIRECT e ⇒ 808 808 λext_indirect: True. 809 809 let address ≝ get_register ? s [[ false; false; e ]] in 810 810 let padded_address ≝ pad 8 8 address in 811 lookup …16 padded_address (external_ram ? s) (zero 8)811 lookup ? 16 padded_address (external_ram ? s) (zero 8) 812 812  ACC_DPTR ⇒ 813 813 λacc_dptr: True. … … 815 815 let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in 816 816 let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in 817 lookup …16 address (external_ram ? s) (zero 8)817 lookup ? 16 address (external_ram ? s) (zero 8) 818 818  ACC_PC ⇒ 819 819 λacc_pc: True. 820 820 let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in 821 821 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ? s) padded_acc in 822 lookup …16 address (external_ram ? s) (zero 8)822 lookup ? 16 address (external_ram ? s) (zero 8) 823 823  DIRECT d ⇒ 824 824 λdirect: True. 825 let 〈 nu, nl 〉 ≝ split …4 4 d in825 let 〈 nu, nl 〉 ≝ split ? 4 4 d in 826 826 let bit_one ≝ get_index_v ? ? nu 0 ? in 827 827 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in … … 836 836 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ? s [[ false; false; i]]) in 837 837 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 838 let bit_1 ≝ get_index_v …bit_one_v O ? in838 let bit_1 ≝ get_index_v ?? bit_one_v O ? in 839 839 match bit_1 with 840 840 [ false ⇒ … … 1002 1002 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1003 1003 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1004 let trans ≝ lookup …7 address' (low_internal_ram ? s) (zero 8) in1004 let trans ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in 1005 1005 ¬(get_index_v … trans (modulus address 8) ?) 1006 1006 ] … … 1038 1038 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1039 1039 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1040 let t ≝ lookup …7 address' (low_internal_ram ? s) (zero 8) in1040 let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in 1041 1041 let n_bit ≝ set_index … t (modulus address 8) v ? in 1042 1042 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in … … 1096 1096 match \fst x with 1097 1097 [ None ⇒ false 1098  Some x ⇒ eq_ bv? x y1098  Some x ⇒ eq_identifier ? x y 1099 1099 ]. 1100 1100 … … 1114 1114 lemma does_not_occur_Some: 1115 1115 ∀id,id',i,list_instr. 1116 eq_ bv? id' id = false →1116 eq_identifier ? id' id = false → 1117 1117 does_not_occur id (list_instr@[〈Some ? id',i〉]) = 1118 1118 does_not_occur id list_instr. … … 1126 1126 does_not_occur id (list_instr@[〈Some ? id,i〉]) = false. 1127 1127 #id #i #list_instr elim list_instr 1128 [ normalize change with (if (if eq_ bv??? then ? else ?) then ? else ? = ?)1129 >eq_ bv_refl %1128 [ normalize change with (if (if eq_identifier ??? then ? else ?) then ? else ? = ?) 1129 >eq_identifier_refl % 1130 1130  * #x #i' #tl #IH whd in ⊢ (??%%) >IH cases (notb ?) %] 1131 1131 qed. … … 1151 1151 lemma occurs_exactly_once_Some: 1152 1152 ∀id,id',i,prefix. 1153 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_ bv? id' id ∨ occurs_exactly_once id prefix.1153 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → eq_identifier ? id' id ∨ occurs_exactly_once id prefix. 1154 1154 #id #id' #i #prefix elim prefix 1155 [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) 1156 change with (? → eq_v ?? eq_b id' id ∨ ?) cases (eq_v ?????) normalize nodelta; /2/ 1155 [ whd in ⊢ (?% → ?) 1156 change in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) with (eq_identifier ? id' id) 1157 @eq_identifier_elim normalize nodelta; /2/ 1157 1158  *; #he #i' #tl #IH whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) 1158 1159 cases he; normalize nodelta 1159 1160 [ #H @ (IH H) 1160  #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??)1161 change in match (eq_v ???x id) with (eq_bv ? x id) cases (eq_bv ???) normalize nodelta;1162 [ generalize in match (refl … (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)normalize nodelta;1163 /2/ #H >does_not_occur_Some / /1161  #x whd in ⊢ (? → ?(??%)) change in match (instruction_matches_identifier ??) with (eq_identifier ? x id) 1162 @eq_identifier_elim #E normalize nodelta 1163 [ destruct @eq_identifier_elim normalize nodelta; 1164 /2/ #H >does_not_occur_Some /2/ 1164 1165  #H @IH @H]]] 1165 1166 qed. … … 1168 1169 ∀id,id',i,prefix. 1169 1170 occurs_exactly_once id (prefix@[〈Some ? id',i〉]) → 1170 (eq_ bv? id' id ∧ does_not_occur id prefix) ∨1171 (¬eq_ bv? id' id ∧ occurs_exactly_once id prefix).1171 (eq_identifier ? id' id ∧ does_not_occur id prefix) ∨ 1172 (¬eq_identifier ? id' id ∧ occurs_exactly_once id prefix). 1172 1173 #id #id' #i #prefix elim prefix 1173 [ whd in ⊢ (?% → ?) whd in ⊢ (?(match % with [_ ⇒ ? _ ⇒ ?]) →?)1174 change with (? → eq_v ?? eq_b id' id∧?∨?) cases (eq_v ?????)1174 [ whd in ⊢ (?% → ?) change in ⊢ (?(match % with [_ ⇒ ? _ ⇒ ?]) → ?) with (eq_identifier ???) 1175 @eq_identifier_elim #E 1175 1176 [ normalize // 1176 1177  normalize #H @⊥ @H … … 1179 1180 cases he; normalize nodelta 1180 1181 [ #H @ (IH H) 1181  #x whd in ⊢ (? → ?(??%)) whd in match (instruction_matches_identifier ??) 1182 generalize in match (refl ? (eq_bv 16 x id)) change in match (eq_v ???x id) with (eq_bv ? x id) 1183 cases (eq_bv ???) in ⊢ (???% → %) #Heq 1184 [ generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta 1185 [ #H >(eq_bv_eq … (sym_eq … H)) >does_not_occur_absurd #Hf @⊥ @Hf 1182  #x @eq_identifier_elim #Heq 1183 [ @eq_identifier_elim normalize nodelta 1184 [ #H >H >does_not_occur_absurd #Hf @⊥ @Hf 1186 1185  #H >(does_not_occur_Some) 1187 [ #H2 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier ??) 1188 change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta 1189 @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) whd in match (instruction_matches_identifier ??) 1190 change in match (eq_v ???x id) with (eq_bv ? x id) >Heq normalize nodelta @H2 1191  @(sym_eq … H) 1186 [ #H2 whd in match (does_not_occur ??) 1187 change in match (instruction_matches_identifier ??) with (eq_identifier ???) 1188 >Heq >eq_identifier_refl normalize nodelta 1189 @orb_elim normalize nodelta whd in match (occurs_exactly_once ??) 1190 change in match (instruction_matches_identifier ??) with (eq_identifier ???) 1191 >eq_identifier_refl 1192 normalize nodelta @H2 1193  /2/ 1192 1194 ] 1193 1195 ] 1194  normalize nodelta #H lapply (IH H) IH H; #Hor @orb_elim1195 generalize in match (refl ? (eq_bv 16 id' id)) cases (eq_bv ???) in ⊢ (??%? → %)1196 #H eq21197 [ normalize nodelta<Heq2 in Hor; #Hor normalize in Hor;1198 whd in match (does_not_occur ??) whd in match (instruction_matches_identifier??)1199 change in match (eq_v ???x id) with (eq_bv ? x id) >Heqnormalize nodelta1200 cases (does_not_occur id tl) in Hor; normalize nodelta //1196  normalize nodelta #H lapply (IH H) IH H; 1197 @eq_identifier_elim #Heq2 1198 #Hor @orb_elim 1199 [ <Heq2 in Hor; #Hor normalize in Hor; 1200 whd in match (does_not_occur ??) change in match (instruction_matches_identifier ??) with (eq_identifier ???) 1201 >eq_identifier_false // normalize nodelta 1202 cases (does_not_occur id' tl) in Hor; normalize nodelta // 1201 1203  normalize nodelta whd in match (occurs_exactly_once ??) 1202 whd in match (instruction_matches_identifier ??) change in match (eq_v ???x id) with (eq_bv ? x id)1203 > Heq normalize nodelta <Heq2 in Hor; normalize //1204 change in match (instruction_matches_identifier ??) with (eq_identifier ???) 1205 >eq_identifier_false // 1204 1206 ] 1205 1207 ] … … 1241 1243 1242 1244 lemma index_of_internal_Some_miss: ∀i,id,id'. 1243 eq_ bv? id' id = false →1245 eq_identifier ? id' id = false → 1244 1246 ∀instr_list,n. 1245 1247 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) → … … 1259 1261 = instr_list + n. 1260 1262 #i #id #instr_list elim instr_list 1261 [ #n #_ whd in ⊢ (??%%) change with (if eq_ bv … id id then ? else ? = ?) >eq_bv_refl %1263 [ #n #_ whd in ⊢ (??%%) change with (if eq_identifier … id id then ? else ? = ?) >eq_identifier_refl % 1262 1264  #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta; 1263 [ >does_not_occur_absurd #abs cases abs  #H applyS (IH (S n)) //]]1265 [ >does_not_occur_absurd #abs cases abs  #H >plus_n_Sm applyS (IH (S n)) //]] 1264 1266 qed. 1265 1267 … … 1278 1280 1279 1281 lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list. 1280 eq_ bv? id' id = false →1282 eq_identifier ? id' id = false → 1281 1283 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) → 1282 1284 address_of_word_labels_code_mem instr_list id = 1283 1285 address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id. 1284 1286 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?)) 1285 >(index_of_internal_Some_miss … H) //1287 >(index_of_internal_Some_miss … H) [ @refl  // ] 1286 1288 qed. 1287 1289 … … 1291 1293 = bitvector_of_nat … (instr_list). 1292 1294 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?) 1293 >(index_of_internal_Some_hit … H) //1295 >(index_of_internal_Some_hit … H) <plus_n_O @refl 1294 1296 qed. 1295 1297 … … 1301 1303 definition construct_datalabels ≝ 1302 1304 λpreamble. 1303 \fst (foldl (( BitVectorTrie Identifier 16) × nat) ? (1305 \fst (foldl ((identifier_map ASMTag Word) × nat) ? ( 1304 1306 λt. λpreamble. 1305 1307 let 〈datalabels, addr〉 ≝ t in 1306 1308 let 〈name, size〉 ≝ preamble in 1307 1309 let addr_16 ≝ bitvector_of_nat 16 addr in 1308 〈 insert ? ? name addr_16 datalabels, addr + size〉)1309 〈 (Stub ? ?), 0〉 preamble).1310 〈add ? ? datalabels name addr_16, addr + size〉) 1311 〈empty_map …, 0〉 preamble).
Note: See TracChangeset
for help on using the changeset viewer.