- Timestamp:
- Jun 12, 2012, 2:18:16 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2032 r2047 430 430 let lookup_address ≝ sigma (lookup_labels lbl) in 431 431 let pc_plus_jmp_length ≝ sigma (add … ppc (bitvector_of_nat … 1)) in 432 let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_addressfalse in432 let 〈result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length false in 433 433 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 434 434 if eq_bv ? upper (zero 8) then … … 553 553 let do_a_long ≝ policy ppc in 554 554 let lookup_address ≝ sigma (lookup_labels jmp) in 555 let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length lookup_addressfalse in555 let 〈result, flags〉 ≝ sub_16_with_carry lookup_address pc_plus_jmp_length false in 556 556 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 557 557 if eq_bv ? upper (zero 8) ∧ ¬ do_a_long then -
src/ASM/AssemblyProofSplit.ma
r2039 r2047 170 170 qed. 171 171 172 lemma pair_replace: 173 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 → 174 P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b'). 175 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct // 176 qed. 177 172 178 lemma get_arg_8_set_program_counter: 173 179 ∀M: Type[0]. … … 187 193 try (#addr1 #addr2) try #addr1 188 194 normalize nodelta try % 189 >external_ram_set_program_counter190 >program_counter_set_program_counter191 195 cases daemon (* XXX: rewrite not working but provable *) 192 196 qed. … … 354 358 include alias "basics/logic.ma". 355 359 include alias "ASM/BitVectorTrie.ma". 356 357 lemma pair_replace:358 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →359 P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b').360 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct //361 qed.362 360 363 361 lemma jmpair_as_replace: … … 407 405 include alias "ASM/Vector.ma". 408 406 407 axiom main_lemma_preinstruction: 408 ∀M, M': internal_pseudo_address_map. 409 ∀preamble: preamble. 410 ∀instr_list: list labelled_instruction. 411 ∀cm: pseudo_assembly_program. 412 ∀EQcm: cm = 〈preamble, instr_list〉. 413 ∀sigma: Word → Word. 414 ∀policy: Word → bool. 415 ∀sigma_policy_witness: sigma_policy_specification cm sigma policy. 416 ∀ps: PseudoStatus cm. 417 ∀ppc: Word. 418 ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps. 419 ∀labels: label_map. 420 ∀costs: BitVectorTrie costlabel 16. 421 ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉. 422 ∀newppc: Word. 423 ∀lookup_labels: Identifier → Word. 424 ∀EQlookup_labels: lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x). 425 ∀lookup_datalabels: Identifier → Word. 426 ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). 427 ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1). 428 ∀instr: preinstruction Identifier. 429 ∀ticks: nat × nat. 430 ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr). 431 ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16. 432 ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x). 433 ∀s: PreStatus pseudo_assembly_program cm. 434 ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))). 435 ∀P: preinstruction Identifier → PseudoStatus cm → Prop. 436 ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc) 437 (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc 438 lookup_datalabels (Instruction instr)))) → 439 next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' → 440 fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps)) 441 (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) → 442 ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) = 443 status_of_pseudo_status M' cm s sigma policy). 444 P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s). 445 446 (* 409 447 lemma main_lemma_preinstruction: 410 448 ∀M, M': internal_pseudo_address_map. … … 878 916 @(pair_replace ?????????? p) normalize nodelta 879 917 [1,3: 918 >get_arg_8_set_program_counter 880 919 cases daemon 881 920 ] … … 900 939 >EQstatus_after_1 in ⊢ (???%); 901 940 whd in ⊢ (???%); 902 [1: 941 [1:exists_labelled_instruction id instr_list → 903 942 <fetch_refl in ⊢ (???%); 904 943 |2: … … 917 956 change with (add ???) in match (\snd (half_add ???)); 918 957 >set_arg_8_set_program_counter in ⊢ (???%); 919 [2,4,6,8: cases daemon]958 [2,4,6,8: /2/ ] 920 959 >program_counter_set_program_counter in ⊢ (???%); 921 960 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') … … 1392 1431 ] 1393 1432 qed. 1394 1395 (*1396 *1397 [1,2,3: (* ADD, ADDC, SUBB *)1398 @list_addressing_mode_tags_elim_prop try % whd1399 @list_addressing_mode_tags_elim_prop try % whd #arg1400 (* XXX: we first work on sigma_increment_commutation *)1401 #sigma_increment_commutation1402 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;1403 (* XXX: we work on the maps *)1404 whd in ⊢ (??%? → ?);1405 try (change with (if ? then ? else ? = ? → ?)1406 cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta)1407 #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm1408 (* XXX: we assume the fetch_many hypothesis *)1409 #fetch_many_assm1410 (* XXX: we give the existential *)1411 %{1}1412 whd in match (execute_1_pseudo_instruction0 ?????);1413 (* XXX: work on the left hand side of the equality *)1414 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc1415 (* XXX: execute fetches some more *)1416 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta1417 whd in fetch_many_assm;1418 >EQassembled in fetch_many_assm;1419 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *1420 #eq_instr #EQticks whd in EQticks:(???%); >EQticks1421 #fetch_many_assm whd in fetch_many_assm;1422 lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc1423 >(eq_instruction_to_eq … eq_instr) -instr1424 [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs1425 @(pose …1426 (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy))1427 #Pl #EQPl1428 cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq1429 lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs1430 whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%)));1431 @pair_elim1432 >tech_pi1_let_as_commute1433 1434 1435 whd in ⊢ (??%?);1436 [ @(pose … (execute_1_preinstruction' ???????))1437 #lhs whd in ⊢ (???% → ?); #EQlhs1438 @(pose … (execute_1_preinstruction' ???????))1439 #rhs whd in ⊢ (???% → ?); #EQrhs1440 1441 1442 CSC: delirium1443 1444 >EQlhs -EQlhs >EQrhs -EQrhs1445 cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%%);1446 1447 lapply (refl ? (execute_1_preinstruction' ???????));1448 [ whd in match (execute_1_preinstruction' ???????);1449 1450 whd in ⊢ (??%?);1451 [ whd in ⊢ (??(???%)%);1452 whd in match (execute_1_preinstruction' ???????);1453 cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%?);1454 @pair_elim #result #flags #Heq11455 whd in match execute_1_preinstruction'; normalize nodelta1456 (* XXX: now we start to work on the mk_PreStatus equality *)1457 whd in ⊢ (??%?);1458 1459 1460 1461 [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg21462 (* XXX: we take up the hypotheses *)1463 #sigma_increment_commutation #next_map_assm #fetch_many_assm1464 (* XXX: we give the existential *)1465 %{1}1466 whd in match (execute_1_pseudo_instruction0 ?????);1467 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc1468 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta1469 (* XXX: fetching of the instruction *)1470 whd in fetch_many_assm;1471 >EQassembled in fetch_many_assm;1472 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *1473 #eq_instr #EQticks whd in EQticks:(???%); >EQticks1474 #fetch_many_assm whd in fetch_many_assm;1475 lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc1476 >(eq_instruction_to_eq … eq_instr) -instr1477 (* XXX: now we start to work on the mk_PreStatus equality *)1478 whd in ⊢ (??%?);1479 check execute_1_preinstruction1480 1481 1482 #MAP #H1 #H2 #EQ %[1,3,5:@1]1483 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)1484 change in ⊢ (? → ??%?) with (execute_1_0 ??)1485 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;1486 * * #H2a #H2b whd in ⊢ (% → ?) #H2c1487 >H2b >(eq_instruction_to_eq … H2a)1488 generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;1489 @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;1490 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG21491 normalize nodelta; #MAP;1492 [1: change in ⊢ (? → %) with1493 ((let 〈result,flags〉 ≝1494 add_8_with_carry1495 (get_arg_8 ? ps false ACC_A)1496 (get_arg_8 ?1497 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))1498 false (DIRECT ARG2))1499 ? in ?) = ?)1500 [2,3: %]1501 change in ⊢ (???% → ?) with1502 (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)1503 >get_arg_8_set_clock1504 [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?1505 [2,4: #abs @⊥ normalize in abs; destruct (abs)1506 |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]1507 [ change in ⊢ (? → %) with1508 ((let 〈result,flags〉 ≝1509 add_8_with_carry1510 (get_arg_8 ? ps false ACC_A)1511 (get_arg_8 ?1512 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))1513 false (DIRECT ARG2))1514 ? in ?) = ?)1515 >get_arg_8_set_low_internal_ram1516 1517 cases (add_8_with_carry ???)1518 1519 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]1520 #result #flags1521 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %1522 1523 1524 |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);1525 @Some_Some_elim #MAP cases (pol ?) normalize nodelta1526 [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'1527 whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)1528 @pair_elim' * #instr #newppc' #ticks #EQ41529 * * #H2a #H2b whd in ⊢ (% → ?) #H21530 >H2b >(eq_instruction_to_eq … H2a)1531 #EQ %[@1]1532 <MAP >(eq_bv_eq … H2) >EQ1533 whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)1534 cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %1535 whd in ⊢ (??%?)1536 whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)1537 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %1538 |5: (* Call *) #label #MAP1539 generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;1540 whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;1541 [ (* short *) #abs @⊥ destruct (abs)1542 |3: (* long *) #H1 #H2 #EQ %[@1]1543 (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)1544 change in ⊢ (? → ??%?) with (execute_1_0 ??)1545 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;1546 * * #H2a #H2b whd in ⊢ (% → ?) #H2c1547 >H2b >(eq_instruction_to_eq … H2a)1548 generalize in match EQ; -EQ;1549 whd in ⊢ (???% → ??%?);1550 generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;1551 >(eq_bv_eq … H2c)1552 change with1553 ((?=let 〈ppc_bu,ppc_bl〉 ≝ vsplit bool 8 8 newppc in ?) →1554 (let 〈pc_bu,pc_bl〉 ≝ vsplit bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)1555 generalize in match (refl … (vsplit … 8 8 newppc)) cases (vsplit bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc1556 generalize in match (refl … (vsplit … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (vsplit bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;1557 >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer1558 >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr1559 generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;1560 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)1561 @split_eq_status;1562 [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)1563 >code_memory_write_at_stack_pointer %1564 | >set_program_counter_set_low_internal_ram1565 >set_clock_set_low_internal_ram1566 @low_internal_ram_write_at_stack_pointer1567 [ >EQ0 @pol | % | %1568 | @( … EQ1)1569 | @(pair_destruct_2 … EQ2)1570 | >(pair_destruct_1 ????? EQpc)1571 >(pair_destruct_2 ????? EQpc)1572 @vsplit_elim #x #y #H <H -x y H;1573 >(pair_destruct_1 ????? EQppc)1574 >(pair_destruct_2 ????? EQppc)1575 @vsplit_elim #x #y #H <H -x y H;1576 >EQ0 % ]1577 | >set_low_internal_ram_set_high_internal_ram1578 >set_program_counter_set_high_internal_ram1579 >set_clock_set_high_internal_ram1580 @high_internal_ram_write_at_stack_pointer1581 [ >EQ0 @pol | % | %1582 | @(pair_destruct_2 … EQ1)1583 | @(pair_destruct_2 … EQ2)1584 | >(pair_destruct_1 ????? EQpc)1585 >(pair_destruct_2 ????? EQpc)1586 @vsplit_elim #x #y #H <H -x y H;1587 >(pair_destruct_1 ????? EQppc)1588 >(pair_destruct_2 ????? EQppc)1589 @vsplit_elim #x #y #H <H -x y H;1590 >EQ0 % ]1591 | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)1592 >external_ram_write_at_stack_pointer whd in ⊢ (???%)1593 >external_ram_write_at_stack_pointer whd in ⊢ (???%)1594 >external_ram_write_at_stack_pointer %1595 | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))1596 >EQ0 %1597 | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)1598 >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)1599 >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)1600 >special_function_registers_8051_write_at_stack_pointer %1601 | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)1602 >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)1603 >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)1604 >special_function_registers_8052_write_at_stack_pointer %1605 | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)1606 >p1_latch_write_at_stack_pointer whd in ⊢ (???%)1607 >p1_latch_write_at_stack_pointer whd in ⊢ (???%)1608 >p1_latch_write_at_stack_pointer %1609 | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)1610 >p3_latch_write_at_stack_pointer whd in ⊢ (???%)1611 >p3_latch_write_at_stack_pointer whd in ⊢ (???%)1612 >p3_latch_write_at_stack_pointer %1613 | >clock_write_at_stack_pointer whd in ⊢ (??%?)1614 >clock_write_at_stack_pointer whd in ⊢ (???%)1615 >clock_write_at_stack_pointer whd in ⊢ (???%)1616 >clock_write_at_stack_pointer %]1617 (*| (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;1618 @pair_elim' #fst_5_addr #rest_addr #EQ11619 @pair_elim' #fst_5_pc #rest_pc #EQ21620 generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))1621 cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]1622 generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)1623 change in ⊢ (? →??%?) with (execute_1_0 ??)1624 @pair_elim' * #instr #newppc' #ticks #EQn1625 * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)1626 generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)1627 @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ41628 @vsplit_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ51629 @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;1630 change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)1631 @vsplit_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)1632 >get_8051_sfr_set_8051_sfr1633 1634 whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)1635 change with ((let 〈pc_bu,pc_bl〉 ≝ vsplit bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)1636 generalize in match (refl … (vsplit bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))1637 cases (vsplit ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ41638 generalize in match (refl … (vsplit bool 4 4 pc_bu))1639 cases (vsplit ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ51640 generalize in match (refl … (vsplit bool 3 8 rest_addr))1641 cases (vsplit ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ61642 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)1643 generalize in match1644 (refl …1645 (half_add 16 (sigma 〈preamble,instr_list〉 newppc)1646 ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))1647 cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ71648 @split_eq_status try %1649 [ change with (? = sigma ? (address_of_word_labels ps label))1650 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)1651 | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)1652 @(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 rest_addr))) %]] *)]1653 |4: (* Jmp *) #label #MAP1654 generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;1655 whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;1656 [3: (* long *) #H1 #H2 #EQ %[@1]1657 (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)1658 change in ⊢ (? → ??%?) with (execute_1_0 ??)1659 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;1660 * * #H2a #H2b whd in ⊢ (% → ?) #H2c1661 >H2b >(eq_instruction_to_eq … H2a)1662 generalize in match EQ; -EQ;1663 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)1664 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %1665 |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;1666 generalize in match1667 (refl ?1668 (sub_16_with_carry1669 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))1670 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))1671 false))1672 cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;1673 generalize in match (refl … (vsplit … 8 8 results)) cases (vsplit ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;1674 generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;1675 #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]1676 generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)1677 change in ⊢ (? → ??%?) with (execute_1_0 ??)1678 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;1679 * * #H2a #H2b whd in ⊢ (% → ?) #H2c1680 >H2b >(eq_instruction_to_eq … H2a)1681 generalize in match EQ; -EQ;1682 whd in ⊢ (???% → ?);1683 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)1684 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)1685 generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))1686 cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ41687 @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))1688 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)1689 | (* medium *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;1690 generalize in match1691 (refl …1692 (vsplit … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))1693 cases (vsplit ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ11694 generalize in match1695 (refl …1696 (vsplit … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))1697 cases (vsplit ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ21698 generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))1699 cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]1700 generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)1701 change in ⊢ (? →??%?) with (execute_1_0 ??)1702 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;1703 * * #H2a #H2b whd in ⊢ (% → ?) #H2c1704 >H2b >(eq_instruction_to_eq … H2a)1705 generalize in match EQ; -EQ;1706 whd in ⊢ (???% → ?);1707 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)1708 change with ((let 〈pc_bu,pc_bl〉 ≝ vsplit bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)1709 generalize in match (refl … (vsplit bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))1710 cases (vsplit ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ41711 generalize in match (refl … (vsplit bool 4 4 pc_bu))1712 cases (vsplit ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ51713 generalize in match (refl … (vsplit bool 3 8 rest_addr))1714 cases (vsplit ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ61715 change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)1716 generalize in match1717 (refl …1718 (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)1719 ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))1720 cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ71721 @split_eq_status try %1722 [ change with (? = sigma ?? (address_of_word_labels ps label))1723 (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)1724 | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)1725 @(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 rest_addr))) %]]1726 | (* Instruction *) -pi; whd in ⊢ (? → ??%? → ?) *; normalize nodelta;1727 [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]1728 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)1729 change in ⊢ (? → ??%?) with (execute_1_0 ??)1730 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;1731 * * #H2a #H2b whd in ⊢ (% → ?) #H2c1732 >H2b >(eq_instruction_to_eq … H2a)1733 generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;1734 @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;1735 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG21736 normalize nodelta; #MAP;1737 [1: change in ⊢ (? → %) with1738 ((let 〈result,flags〉 ≝1739 add_8_with_carry1740 (get_arg_8 ? ps false ACC_A)1741 (get_arg_8 ?1742 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))1743 false (DIRECT ARG2))1744 ? in ?) = ?)1745 [2,3: %]1746 change in ⊢ (???% → ?) with1747 (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)1748 >get_arg_8_set_clock1749 [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?1750 [2,4: #abs @⊥ normalize in abs; destruct (abs)1751 |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]1752 [ change in ⊢ (? → %) with1753 ((let 〈result,flags〉 ≝1754 add_8_with_carry1755 (get_arg_8 ? ps false ACC_A)1756 (get_arg_8 ?1757 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))1758 false (DIRECT ARG2))1759 ? in ?) = ?)1760 >get_arg_8_set_low_internal_ram1761 1762 cases (add_8_with_carry ???)1763 1764 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]1765 #result #flags1766 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %1767 | (* INC *) #arg1 #H1 #H2 #EQ %[@1]1768 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)1769 change in ⊢ (? → ??%?) with (execute_1_0 ??)1770 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;1771 * * #H2a #H2b whd in ⊢ (% → ?) #H2c1772 >H2b >(eq_instruction_to_eq … H2a)1773 generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);1774 @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]1775 [1,2,3,4: cases (half_add ???) #carry #result1776 | cases (half_add ???) #carry #bl normalize nodelta;1777 cases (full_add ????) #carry' #bu normalize nodelta ]1778 #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';1779 [5: %1780 |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program1781 (set_program_counter pseudo_assembly_program ps newppc)1782 (\fst (ticks_of0 〈preamble,instr_list〉1783 (program_counter pseudo_assembly_program ps)1784 (Instruction (INC Identifier (DIRECT ARG))))1785 +clock pseudo_assembly_program1786 (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))1787 [2,3: // ]1788 <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]1789 whd in ⊢ (??%%)1790 cases (vsplit bool 4 4 ARG)1791 #nu' #nl'1792 normalize nodelta1793 cases (vsplit bool 1 3 nu')1794 #bit_1' #ignore'1795 normalize nodelta1796 cases (get_index_v bool 4 nu' ? ?)1797 [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %1798 |1799 ]1800 cases daemon (* EASY CASES TO BE COMPLETED *)1801 qed.1802 1433 *) -
src/ASM/AssemblyProofSplitSplit.ma
r2027 r2047 1 1 include "ASM/AssemblyProofSplit.ma". 2 include "common/LabelledObjects.ma". 3 4 check pseudo_instruction 5 6 definition instruction_has_label ≝ 7 λid: Identifier. 8 λi. 9 match i with 10 [ Jmp j ⇒ j = id 11 | Call j ⇒ j = id 12 | Instruction instr ⇒ 13 match instr with 14 [ JC j ⇒ j = id 15 | JNC j ⇒ j = id 16 | JZ j ⇒ j = id 17 | JNZ j ⇒ j = id 18 | JB _ j ⇒ j = id 19 | JBC _ j ⇒ j = id 20 | DJNZ _ j ⇒ j = id 21 | CJNE _ j ⇒ j = id 22 | _ ⇒ False 23 ] 24 | _ ⇒ False 25 ]. 26 27 28 definition is_well_labelled_p ≝ 29 λinstr_list. 30 ∀id: Identifier. 31 ∀ppc. 32 ∀i. 33 fetch_pseudo_instruction instr_list ppc = i → 34 instruction_has_label id (\fst i) → 35 occurs_exactly_once ASMTag pseudo_instruction id instr_list. 2 36 3 37 theorem main_thm: 4 38 ∀M, M': internal_pseudo_address_map. 5 39 ∀program: pseudo_assembly_program. 40 ∀is_well_labelled: is_well_labelled_p (\snd program). 6 41 ∀sigma: Word → Word. 7 42 ∀policy: Word → bool. … … 13 48 status_of_pseudo_status M' … 14 49 (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy. 15 #M #M' * #preamble #instr_list # sigma #policy #sigma_policy_witness #ps #program_counter_in_bounds50 #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps #program_counter_in_bounds 16 51 change with (next_internal_pseudo_address_map0 ????? = ? → ?) 17 52 @(pose … (program_counter ?? ps)) #ppc #EQppc … … 31 66 generalize in match assm1; -assm1 -assm2 -assm3 32 67 normalize nodelta 33 casespi68 inversion pi 34 69 [2,3: 35 #arg 70 #arg #_ 36 71 (* XXX: we first work on sigma_increment_commutation *) 37 72 #sigma_increment_commutation … … 49 84 [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ] 50 85 |6: (* Mov *) 51 #arg1 #arg2 86 #arg1 #arg2 #_ 52 87 (* XXX: we first work on sigma_increment_commutation *) 53 88 #sigma_increment_commutation … … 83 118 >set_arg_16_mk_Status_commutation in ⊢ (???%); 84 119 (* here we are *) 85 @split_eq_status //120 @split_eq_status try % 86 121 [1: 87 122 assumption 88 123 |2: 89 @special_function_registers_8051_set_arg_16 90 [2: % 91 |1: // 92 ] 124 @special_function_registers_8051_set_arg_16 % 93 125 ] 94 126 |1: (* Instruction *) 95 -pi #instr#EQP #EQnext #fetch_many_assm127 #instr #_ #EQP #EQnext #fetch_many_assm 96 128 @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness 97 129 ps ppc EQppc labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels … … 100 132 (refl …) ? (refl …)) 101 133 try assumption >assembly_refl <EQppc assumption 102 check status_of_pseudo_status103 134 |4: 135 #arg1 #pi_refl 136 (* XXX: we first work on sigma_increment_commutation *) 137 whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?); 138 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 144 [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 148 ] 149 #sigma_increment_commutation 150 normalize in sigma_increment_commutation:(???(???(??%))); 151 (* XXX: we work on the maps *) 152 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 153 (* XXX: we assume the fetch_many hypothesis *) 154 * #fetch_refl #fetch_many_assm 155 (* XXX: we give the existential *) 156 %{1} 157 (* XXX: work on the left hand side of the equality *) 158 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc 159 (* XXX: execute fetches some more *) 160 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 161 whd in fetch_many_assm; 162 >EQassembled in fetch_refl; #fetch_refl <fetch_refl -fetch_refl 163 lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc 164 whd in ⊢ (??%%); 165 (* XXX: now we start to work on the mk_PreStatus equality *) 166 (* XXX: lhs *) 167 (* XXX: rhs *) 168 (* here we are *) 169 @split_eq_status try % /demod nohyps/ 170 [1,3,4: 171 change with (add ???) in match (\snd (half_add ???)); 172 whd in match execute_1_pseudo_instruction0; normalize nodelta 173 /demod nohyps/ >set_clock_set_program_counter 174 >program_counter_set_program_counter 175 whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta 176 lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl 177 normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm 178 [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 184 |3: 185 >EQnewpc >pc_refl normalize nodelta 186 >(pair_destruct_2 ????? (sym_eq … addr_refl)) 187 >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc 188 >EQlookup_labels normalize nodelta 189 >address_of_word_labels_assm try % 190 |5: 191 >EQnewpc 192 ] 193 @(is_well_labelled_witness … fetch_pseudo_refl) 194 >pi_refl % 195 |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 207 ] 208 |5: (* Call *) 104 209 #arg1 105 210 (* XXX: we first work on sigma_increment_commutation *) … … 119 224 whd in fetch_many_assm; 120 225 >EQassembled in fetch_many_assm; 121 cases (fetch ??) * #instr #newpc # ticks normalize nodelta *226 cases (fetch ??) * #instr #newpc #?ticks normalize nodelta * 122 227 #eq_instr 123 228 #fetch_many_assm whd in fetch_many_assm; … … 145 250 ] 146 251 ] 147 |5: cases daemon148 252 ] 149 253 qed. -
src/ASM/Interpret.ma
r2040 r2047 990 990 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with 991 991 [ ADDR11 a ⇒ λaddr11: True. 992 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 program_counter in 993 let 〈nu, nl〉 ≝ vsplit ? 4 4 pc_bu in 994 let bit ≝ get_index' ? O ? nl in 995 let 〈relevant1, relevant2〉 ≝ vsplit ? 3 8 a in 996 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 997 let 〈carry, new_pc〉 ≝ half_add ? program_counter new_addr in 998 new_pc 992 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 5 11 program_counter in 993 let new_addr ≝ pc_bu @@ a in 994 new_addr 999 995 | _ ⇒ λother: False. ⊥ 1000 996 ] (subaddressing_modein … addr) -
src/ASM/PolicyFront.ma
r2034 r2047 324 324 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added 325 325 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in 326 let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length addrfalse in326 let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in 327 327 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 328 328 if eq_bv ? upper (zero 8) … … 356 356 then \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉) + added 357 357 else \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉)) in 358 let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length addrfalse in358 let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in 359 359 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 360 360 if eq_bv ? upper (zero 8) … … 748 748 definition short_jump_cond: Word → Word → pseudo_instruction → Prop ≝ 749 749 λpc_plus_jmp_length.λaddr.λinstr. 750 let 〈result, flags〉 ≝ sub_16_with_carry pc_plus_jmp_length addrfalse in750 let 〈result, flags〉 ≝ sub_16_with_carry addr pc_plus_jmp_length false in 751 751 let 〈upper, lower〉 ≝ vsplit ? 8 8 result in 752 eq_bv 8 upper (zero 8) = true. 752 if flags then 753 eq_bv 8 upper [[true;true;true;true;true;true;true;true]] = true 754 else 755 eq_bv 8 upper (zero 8) = true. 753 756 754 757 definition medium_jump_cond: Word → Word → pseudo_instruction → Prop ≝
Note: See TracChangeset
for help on using the changeset viewer.