Changeset 2047 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 Jun 12, 2012, 2:18:16 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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 *)
Note: See TracChangeset
for help on using the changeset viewer.