Changeset 1602
Legend:
 Unmodified
 Added
 Removed

src/ASM/Fetch.ma
r1600 r1602 27 27 nat_of_bitvector … v < nat_of_bitvector … (\snd (half_add … v (bitvector_of_nat … (S O)))). 28 28 29 lemma minus_leq_minus: 30 ∀m, n, o: nat. 31 n ≤ m → o ≤ m → o ≤ n → m  n ≤ m  o. 32 #m #n #o #m_le_n #m_le_o #o_le_n 33 cases daemon (* XXX: todo *) 34 qed. 35 29 36 definition next: BitVectorTrie Byte 16 → ∀program_counter: Word. 30 nat_of_bitvector … program_counter < (code_memory_size  1) → 31 Σret: Word × Byte. nat_of_bitvector … program_counter < nat_of_bitvector … (\fst ret) ≝ 37 nat_of_bitvector … program_counter < (code_memory_size  24) → 38 Σret: Word × Byte. nat_of_bitvector … program_counter < nat_of_bitvector … (\fst ret) ∧ 39 (nat_of_bitvector … (\fst ret)) ≤ code_memory_size ≝ 32 40 λpmem: BitVectorTrie Byte 16. 33 41 λpc: Word. 34 42 λproof. 35 43 〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup ? ? pc pmem (zero 8)〉. 36 @w_lt_half_add_increment @proof 44 @conj 45 [1: 46 @w_lt_half_add_increment 47 @(transitive_le 48 (S (nat_of_bitvector … pc)) 49 (code_memory_size  24) 50 (code_memory_size  1) ? ?) 51 [1: 52 @proof 53 2: 54 @(minus_leq_minus code_memory_size 24 1) // 55 ] 56 2: 57 cases daemon (* XXX: todo *) 58 ] 37 59 qed. 38 60 … … 150 172 else 151 173 let 〈b,v〉≝ head … v in if b then 152 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉174 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉 153 175 else 154 176 〈〈RealInstruction (DA … ACC_A), pc〉, 1〉 … … 191 213 let 〈b,v〉≝ head … v in if b then 192 214 let 〈b,v〉≝ head … v in if b then 193 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉194 else 195 let 〈b,v〉≝ head … v in if b then 196 let 〈b,v〉≝ head … v in if b then 197 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉198 else 199 let 〈b,v〉≝ head … v in if b then 200 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉201 else 202 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉215 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 216 else 217 let 〈b,v〉≝ head … v in if b then 218 let 〈b,v〉≝ head … v in if b then 219 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉 220 else 221 let 〈b,v〉≝ head … v in if b then 222 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉 223 else 224 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 203 225 else 204 226 let 〈b,v〉≝ head … v in if b then … … 255 277 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 256 278 else 257 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉279 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉 258 280 else 259 281 let 〈b,v〉≝ head … v in if b then … … 265 287 else 266 288 let 〈b,v〉≝ head … v in if b then 267 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉289 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉 268 290 else 269 291 〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉 … … 291 313 else 292 314 let 〈b,v〉≝ head … v in if b then 293 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉315 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉 294 316 else 295 317 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉 … … 320 342 let 〈b,v〉≝ head … v in if b then 321 343 let 〈b,v〉≝ head … v in if b then 322 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉344 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉 323 345 else 324 346 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉 … … 344 366 let 〈b,v〉≝ head … v in if b then 345 367 let 〈b,v〉≝ head … v in if b then 346 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉368 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 347 369 else 348 370 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 … … 367 389 let 〈b,v〉≝ head … v in if b then 368 390 let 〈b,v〉≝ head … v in if b then 369 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉391 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉 370 392 else 371 393 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉 … … 399 421 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 400 422 else 401 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉423 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 402 424 else 403 425 let 〈b,v〉≝ head … v in if b then … … 422 444 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 423 445 else 424 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉446 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 425 447 else 426 448 let 〈b,v〉≝ head … v in if b then … … 441 463 〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉 442 464 else 443 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉465 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉 444 466 else 445 467 let 〈b,v〉≝ head … v in if b then 446 468 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 447 469 else 448 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉470 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 449 471 else 450 472 let 〈b,v〉≝ head … v in if b then … … 464 486 〈〈RealInstruction (RR … ACC_A), pc〉, 1〉 465 487 else 466 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 ≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉488 let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉 {EQ'} ≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉 467 489 else 468 490 let 〈b,v〉≝ head … v in if b then … … 471 493 〈〈RealInstruction (NOP …), pc〉, 1〉. 472 494 try % 495 cases daemon (* 473 496 try ( 474 497 @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p … … 476 499 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof) 477 500 ) 478 [1,2,3,4,5,6,7,8: 501 [6,8,14,15,16,17,20,21,22,23,25,28,30,31,32,33,34,37,38,39,40,41,44,45,46,47, 502 50,51,52,53,56,57,58,59,65,69,71,73,75: 503 cases daemon (* XXX: segmentation fault *) 504 1,2,3,4,5,7,8,9,10,11,12,13,18,19,24,26,27,29,35,36,42,43,48,49,54,55,60,61, 505 62,63,64,66,67,68,70,72,74,76: 479 506 @breakup_pair' cases (next pmem pc ?) 480 507 normalize * normalize #pc' #byte @lt_to_le 481 3: 482 @breakup_pair' cases (next pmem pc ?) 483 normalize * normalize #pc' #byte @lt_to_le 484 2: 485 @breakup_pair' cases(next pmem pc ?) 486 normalize * normalize #pc' #byte @lt_to_le 487 [ 488  92: 489 cases (next ???) in EQ; * #pc' #content #H #EQ whd in EQ:(??%?); destruct 490 491 492 lapply(eq_pair_fst_snd ? ? (next pmem pc ?)) 493 #assm >assm 494 cut(nat_of_bitvector … pc < nat_of_bitvector … 495 (\fst (next pmem pc 496 (o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p (nat_of_bitvector 16 pc) 497 code_memory_size 24 1 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof)))) 498 [ @sig2 499  #assm @lt_to_le assumption 500 ] 501 92: 502 check next. 503 lapply pc pc 504 @sig2 505 cases daemon (* XXX: requires rewrite of the above to make it more russell friendly *) 508 [30: 509 generalize in match pc in EQ; #pc' #EQ' pc 510 cut(nat_of_bitvector … pc < nat_of_bitvector … pc') 511 [1: 512 cut(pc' = \fst (next pmem pc (o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p (nat_of_bitvector 16 pc) 513 code_memory_size 24 1 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof))) 514 [1: 515 // 516 2: 517 #assm >assm @sig2 518 ] 519  #lt_assm 520 lapply(transitive_le 521 (S (nat_of_bitvector … pc)) 522 (nat_of_bitvector … pc') 523 (S (nat_of_bitvector … pc')) lt_assm ?) 524 [1: 525 // 526 2: 527 #le_assm 528 lapply(transitive_le 529 (S (nat_of_bitvector … pc)) 530 (S (nat_of_bitvector … pc')) 531 (code_memory_size  1) le_assm ?) 532 [2: 533 // 534 1: 535 @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p 536 (nat_of_bitvector … pc) code_memory_size 24 1 ? ?) 537 [1: 538 @le_S_S @le_S_S @le_O_n 539 2: 540 assumption 541 ] 542 ] 543 ] 544 ] XXX: blah! *) 506 545 qed. 507 546 
src/ASM/Util.ma
r1600 r1602 801 801 % 802 802  normalize 803 / 2/803 /3 by trans_eq, orb_true_l/ 804 804 ] 805 805 qed.
Note: See TracChangeset
for help on using the changeset viewer.