- Timestamp:
- Jul 6, 2012, 11:04:17 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Test.ma
r2160 r2163 185 185 186 186 lemma set_8051_sfr_status_of_pseudo_status: 187 ∀M, code_memory, sigma, policy, s, sfr, v,v'. 188 map_address_using_internal_pseudo_address_map M sigma sfr v = v' → 189 (set_8051_sfr (BitVectorTrie Byte 16) 190 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 191 (status_of_pseudo_status M code_memory s sigma policy) sfr v' 192 =status_of_pseudo_status M code_memory 193 (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy). 194 #M #code_memory #sigma #policy #s #sfr #v #v' #v_ok 195 whd in ⊢ (??%%); @split_eq_status try % /2/ 196 qed. 197 198 lemma set_8052_sfr_status_of_pseudo_status: 187 199 ∀M, code_memory, sigma, policy, s, sfr, v. 188 (set_805 1_sfr (BitVectorTrie Byte 16)200 (set_8052_sfr (BitVectorTrie Byte 16) 189 201 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 190 202 (status_of_pseudo_status M code_memory s sigma policy) sfr v 191 203 =status_of_pseudo_status M code_memory 192 (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy). 193 #M #code_memory #sigma #policy #s #sfr #v 194 whd in ⊢ (??%%); @split_eq_status try % 204 (set_8052_sfr pseudo_assembly_program code_memory s sfr v) sigma policy). 205 // 206 qed. 207 208 definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝ 209 λb: Byte. 210 let address ≝ nat_of_bitvector … b in 211 if (eqb address 128) then None ? 212 else if (eqb address 144) then Some … (inl … SFR_P1) 213 else if (eqb address 160) then None ? 214 else if (eqb address 176) then Some … (inl … SFR_P3) 215 else if (eqb address 153) then Some … (inl … SFR_SBUF) 216 else if (eqb address 138) then Some … (inl … SFR_TL0) 217 else if (eqb address 139) then Some … (inl … SFR_TL1) 218 else if (eqb address 140) then Some … (inl … SFR_TH0) 219 else if (eqb address 141) then Some … (inl … SFR_TH1) 220 else if (eqb address 200) then Some … (inr … SFR_T2CON) 221 else if (eqb address 202) then Some … (inr … SFR_RCAP2L) 222 else if (eqb address 203) then Some … (inr … SFR_RCAP2H) 223 else if (eqb address 204) then Some … (inr … SFR_TL2) 224 else if (eqb address 205) then Some … (inr … SFR_TH2) 225 else if (eqb address 135) then Some … (inl … SFR_PCON) 226 else if (eqb address 136) then Some … (inl … SFR_TCON) 227 else if (eqb address 137) then Some … (inl … SFR_TMOD) 228 else if (eqb address 152) then Some … (inl … SFR_SCON) 229 else if (eqb address 168) then Some … (inl … SFR_IE) 230 else if (eqb address 184) then Some … (inl … SFR_IP) 231 else if (eqb address 129) then Some … (inl … SFR_SP) 232 else if (eqb address 130) then Some … (inl … SFR_DPL) 233 else if (eqb address 131) then Some … (inl … SFR_DPH) 234 else if (eqb address 208) then Some … (inl … SFR_PSW) 235 else if (eqb address 224) then Some … (inl … SFR_ACC_A) 236 else if (eqb address 240) then Some … (inl … SFR_ACC_B) 237 else None ?. 195 238 196 239 definition set_bit_addressable_sfr: … … 202 245 λb: Byte. 203 246 λv: Byte. 204 let address ≝ nat_of_bitvector … b in 205 if (eqb address 128) then 206 match not_implemented in False with [ ] 207 else if (eqb address 144) then 208 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 209 let status_2 ≝ set_p1_latch ?? s v in 210 status_2 211 else if (eqb address 160) then 212 match not_implemented in False with [ ] 213 else if (eqb address 176) then 214 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 215 let status_2 ≝ set_p3_latch ?? s v in 216 status_2 217 else if (eqb address 153) then 218 set_8051_sfr ?? s SFR_SBUF v 219 else if (eqb address 138) then 220 set_8051_sfr ?? s SFR_TL0 v 221 else if (eqb address 139) then 222 set_8051_sfr ?? s SFR_TL1 v 223 else if (eqb address 140) then 224 set_8051_sfr ?? s SFR_TH0 v 225 else if (eqb address 141) then 226 set_8051_sfr ?? s SFR_TH1 v 227 else if (eqb address 200) then 228 set_8052_sfr ?? s SFR_T2CON v 229 else if (eqb address 202) then 230 set_8052_sfr ?? s SFR_RCAP2L v 231 else if (eqb address 203) then 232 set_8052_sfr ?? s SFR_RCAP2H v 233 else if (eqb address 204) then 234 set_8052_sfr ?? s SFR_TL2 v 235 else if (eqb address 205) then 236 set_8052_sfr ?? s SFR_TH2 v 237 else if (eqb address 135) then 238 set_8051_sfr ?? s SFR_PCON v 239 else if (eqb address 136) then 240 set_8051_sfr ?? s SFR_TCON v 241 else if (eqb address 137) then 242 set_8051_sfr ?? s SFR_TMOD v 243 else if (eqb address 152) then 244 set_8051_sfr ?? s SFR_SCON v 245 else if (eqb address 168) then 246 set_8051_sfr ?? s SFR_IE v 247 else if (eqb address 184) then 248 set_8051_sfr ?? s SFR_IP v 249 else if (eqb address 129) then 250 set_8051_sfr ?? s SFR_SP v 251 else if (eqb address 130) then 252 set_8051_sfr ?? s SFR_DPL v 253 else if (eqb address 131) then 254 set_8051_sfr ?? s SFR_DPH v 255 else if (eqb address 208) then 256 set_8051_sfr ?? s SFR_PSW v 257 else if (eqb address 224) then 258 set_8051_sfr ?? s SFR_ACC_A v 259 else if (eqb address 240) then 260 set_8051_sfr ?? s SFR_ACC_B v 261 else 262 match not_implemented in False with [ ]. 263 264 lemma set_bit_addressable_sfr_status_of_pseudo_status: 247 match sfr_of_Byte b with 248 [ None ⇒ match not_implemented in False with [ ] 249 | Some sfr8051_8052 ⇒ 250 match sfr8051_8052 with 251 [ inl sfr ⇒ 252 match sfr with 253 [ SFR_P1 ⇒ 254 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 255 set_p1_latch ?? s v 256 | SFR_P3 ⇒ 257 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 258 set_p3_latch ?? s v 259 | _ ⇒ set_8051_sfr ?? s sfr v ] 260 | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]. 261 262 definition map_address_Byte_using_internal_pseudo_address_map ≝ 263 λM,sigma,d,v. 264 match sfr_of_Byte d with 265 [ None ⇒ v 266 | Some sfr8051_8052 ⇒ 267 match sfr8051_8052 with 268 [ inl sfr ⇒ 269 map_address_using_internal_pseudo_address_map M sigma sfr v 270 | inr _ ⇒ v ]]. 271 272 lemma set_bit_addressable_sfr_status_of_pseudo_status': 265 273 let M ≝ pseudo_assembly_program in ∀code_memory: M. ∀s: PreStatus M code_memory. ∀d: Byte. ∀v: Byte. 266 Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy. 274 Σp: PreStatus M code_memory. ∀M. ∀sigma. ∀policy. ∀v'. 275 map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' → 267 276 (set_bit_addressable_sfr (BitVectorTrie Byte 16) 268 277 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 269 (status_of_pseudo_status M code_memory s sigma policy) d v 278 (status_of_pseudo_status M code_memory s sigma policy) d v' 270 279 =status_of_pseudo_status M code_memory 271 280 (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy). 272 whd in match set_bit_addressable_sfr; normalize nodelta 281 whd in match set_bit_addressable_sfr; 282 whd in match map_address_Byte_using_internal_pseudo_address_map; 283 normalize nodelta 273 284 @(let M ≝ pseudo_assembly_program in 274 285 λcode_memory:M. … … 276 287 λb: Byte. 277 288 λv: Byte. 278 let address ≝ nat_of_bitvector … b in 279 if (eqb address 128) then 280 match not_implemented in False with [ ] 281 else if (eqb address 144) then 282 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 283 let status_2 ≝ set_p1_latch ?? s v in 284 status_2 285 else if (eqb address 160) then 286 match not_implemented in False with [ ] 287 else if (eqb address 176) then 288 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 289 let status_2 ≝ set_p3_latch ?? s v in 290 status_2 291 else if (eqb address 153) then 292 set_8051_sfr ?? s SFR_SBUF v 293 else if (eqb address 138) then 294 set_8051_sfr ?? s SFR_TL0 v 295 else if (eqb address 139) then 296 set_8051_sfr ?? s SFR_TL1 v 297 else if (eqb address 140) then 298 set_8051_sfr ?? s SFR_TH0 v 299 else if (eqb address 141) then 300 set_8051_sfr ?? s SFR_TH1 v 301 else if (eqb address 200) then 302 set_8052_sfr ?? s SFR_T2CON v 303 else if (eqb address 202) then 304 set_8052_sfr ?? s SFR_RCAP2L v 305 else if (eqb address 203) then 306 set_8052_sfr ?? s SFR_RCAP2H v 307 else if (eqb address 204) then 308 set_8052_sfr ?? s SFR_TL2 v 309 else if (eqb address 205) then 310 set_8052_sfr ?? s SFR_TH2 v 311 else if (eqb address 135) then 312 set_8051_sfr ?? s SFR_PCON v 313 else if (eqb address 136) then 314 set_8051_sfr ?? s SFR_TCON v 315 else if (eqb address 137) then 316 set_8051_sfr ?? s SFR_TMOD v 317 else if (eqb address 152) then 318 set_8051_sfr ?? s SFR_SCON v 319 else if (eqb address 168) then 320 set_8051_sfr ?? s SFR_IE v 321 else if (eqb address 184) then 322 set_8051_sfr ?? s SFR_IP v 323 else if (eqb address 129) then 324 set_8051_sfr ?? s SFR_SP v 325 else if (eqb address 130) then 326 set_8051_sfr ?? s SFR_DPL v 327 else if (eqb address 131) then 328 set_8051_sfr ?? s SFR_DPH v 329 else if (eqb address 208) then 330 set_8051_sfr ?? s SFR_PSW v 331 else if (eqb address 224) then 332 set_8051_sfr ?? s SFR_ACC_A v 333 else if (eqb address 240) then 334 set_8051_sfr ?? s SFR_ACC_B v 335 else 336 match not_implemented in False with [ ]) 337 normalize nodelta 338 #M #sigma #policy 339 [1,2: // 340 |3: // 289 match sfr_of_Byte b with 290 [ None ⇒ match not_implemented in False with [ ] 291 | Some sfr8051_8052 ⇒ 292 match sfr8051_8052 with 293 [ inl sfr ⇒ 294 match sfr with 295 [ SFR_P1 ⇒ 296 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 297 set_p1_latch ?? s v 298 | SFR_P3 ⇒ 299 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 300 set_p3_latch ?? s v 301 | _ ⇒ set_8051_sfr ?? s sfr v ] 302 | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]) 303 normalize nodelta 304 /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/ 305 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta // 306 qed. 307 308 lemma set_bit_addressable_sfr_status_of_pseudo_status: 309 ∀code_memory: pseudo_assembly_program. ∀s: PreStatus … code_memory. ∀d: Byte. ∀v: Byte. 310 ∀M. ∀sigma. ∀policy. ∀v'. 311 map_address_Byte_using_internal_pseudo_address_map M sigma d v = v' → 312 (set_bit_addressable_sfr (BitVectorTrie Byte 16) 313 (code_memory_of_pseudo_assembly_program code_memory sigma policy) 314 (status_of_pseudo_status M code_memory s sigma policy) d v' 315 =status_of_pseudo_status M code_memory 316 (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy). 317 #code #s #d #v cases (set_bit_addressable_sfr_status_of_pseudo_status' code s d v) #_ 318 #H @H 319 qed. 320 321 check status_of_pseudo_status 322 323 lemma set_low_internal_fram_status_of_pseudo_status: 324 ∀cm,sigma,policy,M,s,ram. 325 set_low_internal_ram (BitVectorTrie Byte 16) 326 (code_memory_of_pseudo_assembly_program cm sigma policy) 327 (status_of_pseudo_status M cm s sigma policy) 328 (low_internal_ram_of_pseudo_low_internal_ram M ram) 329 = status_of_pseudo_status M cm 330 (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy. 331 // 332 qed. 333 334 lemma set_low_internal_fram_status_of_pseudo_status: 335 ∀M,cm,sigma,policy,s,addr,v. 336 insert Byte 7 addr v 337 (low_internal_ram (BitVectorTrie Byte 16) 338 (code_memory_of_pseudo_assembly_program cm sigma policy) 339 (status_of_pseudo_status M cm s sigma policy)) 340 = low_internal_ram_of_pseudo_low_internal_ram M 341 (insert Byte 7 addr v 342 (low_internal_ram pseudo_assembly_program cm s)). 343 #M #cm #sigma #policy #s #addr #v 344 345 346 definition map_address_mode_using_internal_pseudo_address_map ≝ 347 λM,sigma,addr,v. 348 match addr with 349 [ DIRECT d ⇒ 350 let 〈 nu, nl 〉 as vsplit_refl ≝ vsplit … 4 4 d in 351 match get_index_v ? ? nu 0 ? with 352 [ true ⇒ 353 map_address_Byte_using_internal_pseudo_address_map M sigma d v 354 | false ⇒ v ] 355 | _ ⇒ v ]. 356 // 357 qed. 341 358 342 359 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ; … … 398 415 ∀cm. 399 416 ∀ps. 400 ∀addr. 401 ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. 417 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]]. 418 ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'. 419 map_address_mode_using_internal_pseudo_address_map M sigma addr value = value' → 402 420 set_arg_8 (BitVectorTrie Byte 16) 403 421 (code_memory_of_pseudo_assembly_program cm sigma policy) 404 422 (status_of_pseudo_status M cm ps sigma policy) 405 addr value =423 addr value' = 406 424 status_of_pseudo_status M cm (set_arg_8 … cm ps addr value) sigma policy. 425 whd in match set_arg_8; normalize nodelta 407 426 @(let m ≝ pseudo_assembly_program in λcm, s. λa: [[ direct ; indirect ; registr ; 408 427 acc_a ; acc_b ; ext_indirect ; … … 411 430 acc_a ; acc_b ; ext_indirect ; 412 431 ext_indirect_dptr ]] addr) → 413 Σp: PreStatus m cm. ∀M. ∀sigma. ∀policy. 414 set_arg_8 (BitVectorTrie Byte 16) 415 (code_memory_of_pseudo_assembly_program cm sigma policy) 416 (status_of_pseudo_status M cm s sigma policy) 417 addr v = 418 status_of_pseudo_status M cm (set_arg_8 … cm s addr v) sigma policy 432 Σp.? 419 433 with 420 434 [ DIRECT d ⇒ 421 435 λdirect: True. 422 let 〈 nu, nl 〉≝ vsplit … 4 4 d in436 deplet 〈 nu, nl 〉 as vsplit_refl ≝ vsplit … 4 4 d in 423 437 let bit_one ≝ get_index_v ? ? nu 0 ? in 424 438 let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in … … 460 474 λother: False. 461 475 match other in False with [ ] 462 ] (subaddressing_modein … a)) 463 [3,6: // ] 464 [1: 465 #M #sigma #policy whd in ⊢ (??%(???%??)); 466 @pair_elim #nu #nl #nu_nl_refl normalize nodelta 467 @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta 468 cases (get_index_v bool ????) normalize nodelta 469 qed. 476 ] (subaddressing_modein … a)) normalize nodelta 477 [3,6: // ] #M #sigma #policy #v' whd in ⊢ (??%? → ?); 478 [1,2: 479 <vsplit_refl normalize nodelta >p normalize nodelta 480 normalize nodelta in p1; >p1 normalize nodelta 481 [ @set_bit_addressable_sfr_status_of_pseudo_status 482 | #v_ok <v_ok @set_low_internal_ram_status_of_pseudo_status 483 ] 484 |2: 485 qed.
Note: See TracChangeset
for help on using the changeset viewer.