Ignore:
Timestamp:
Jun 12, 2012, 2:18:16 PM (7 years ago)
Author:
mulligan
Message:

Big bugs in policy calculations found. Waiting for Jaap's commit.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProofSplit.ma

    r2039 r2047  
    170170qed.
    171171
     172lemma 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 //
     176qed.
     177
    172178lemma get_arg_8_set_program_counter:
    173179  ∀M: Type[0].
    … …  
    187193  try (#addr1 #addr2) try #addr1
    188194  normalize nodelta try %
    189   >external_ram_set_program_counter
    190   >program_counter_set_program_counter
    191195  cases daemon (* XXX: rewrite not working but provable *)
    192196qed.
    … …  
    354358include alias "basics/logic.ma".
    355359include 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.
    362360
    363361lemma jmpair_as_replace:
    … …  
    407405include alias "ASM/Vector.ma".
    408406
     407axiom 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(*
    409447lemma main_lemma_preinstruction:
    410448  ∀M, M': internal_pseudo_address_map.
    … …  
    878916    @(pair_replace ?????????? p) normalize nodelta
    879917    [1,3:
     918      >get_arg_8_set_program_counter
    880919      cases daemon
    881920    ]
    … …  
    900939      >EQstatus_after_1 in ⊢ (???%);
    901940      whd in ⊢ (???%);
    902       [1:
     941      [1:exists_labelled_instruction id instr_list →
    903942        <fetch_refl in ⊢ (???%);
    904943      |2:
    … …  
    917956        change with (add ???) in match (\snd (half_add ???));
    918957        >set_arg_8_set_program_counter in ⊢ (???%);
    919         [2,4,6,8: cases daemon ]
     958        [2,4,6,8: /2/ ]
    920959        >program_counter_set_program_counter in ⊢ (???%);
    921960        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
    … …  
    13921431  ]
    13931432qed.
    1394 
    1395 (* 
    1396     *
    1397     [1,2,3: (* ADD, ADDC, SUBB *)
    1398     @list_addressing_mode_tags_elim_prop try % whd
    1399     @list_addressing_mode_tags_elim_prop try % whd #arg
    1400     (* XXX: we first work on sigma_increment_commutation *)
    1401     #sigma_increment_commutation
    1402     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_assm
    1408     (* XXX: we assume the fetch_many hypothesis *)
    1409     #fetch_many_assm
    1410     (* 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 ???); <EQppc
    1415     (* XXX: execute fetches some more *)
    1416     whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    1417     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:(???%); >EQticks
    1421     #fetch_many_assm whd in fetch_many_assm;
    1422     lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    1423     >(eq_instruction_to_eq … eq_instr) -instr
    1424     [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs
    1425       @(pose …
    1426         (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy))
    1427       #Pl #EQPl
    1428       cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq
    1429       lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs
    1430       whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%)));
    1431       @pair_elim
    1432       >tech_pi1_let_as_commute
    1433    
    1434    
    1435     whd in ⊢ (??%?);
    1436     [ @(pose … (execute_1_preinstruction' ???????))
    1437       #lhs whd in ⊢ (???% → ?); #EQlhs
    1438       @(pose … (execute_1_preinstruction' ???????))
    1439       #rhs whd in ⊢ (???% → ?); #EQrhs
    1440 
    1441 
    1442       CSC: delirium
    1443      
    1444       >EQlhs -EQlhs >EQrhs -EQrhs
    1445       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 #Heq1
    1455     whd in match execute_1_preinstruction'; normalize nodelta
    1456     (* 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 #arg2
    1462     (* XXX: we take up the hypotheses *)
    1463     #sigma_increment_commutation #next_map_assm #fetch_many_assm
    1464     (* XXX: we give the existential *)
    1465     %{1}
    1466     whd in match (execute_1_pseudo_instruction0 ?????);
    1467     whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
    1468     whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
    1469     (* 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:(???%); >EQticks
    1474     #fetch_many_assm whd in fetch_many_assm;
    1475     lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
    1476     >(eq_instruction_to_eq … eq_instr) -instr
    1477     (* XXX: now we start to work on the mk_PreStatus equality *)
    1478     whd in ⊢ (??%?);
    1479     check execute_1_preinstruction
    1480    
    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 ⊢ (% → ?) #H2c
    1487        >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; #ARG2
    1491        normalize nodelta; #MAP;
    1492        [1: change in ⊢ (? → %) with
    1493         ((let 〈result,flags〉 ≝
    1494           add_8_with_carry
    1495            (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 ⊢ (???% → ?) with
    1502          (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
    1503         >get_arg_8_set_clock
    1504        [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 ⊢ (? → %) with
    1508         ((let 〈result,flags〉 ≝
    1509           add_8_with_carry
    1510            (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_ram
    1516        
    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 #flags
    1521        #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 nodelta
    1526        [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 #EQ4       
    1529          * * #H2a #H2b whd in ⊢ (% → ?) #H2
    1530          >H2b >(eq_instruction_to_eq … H2a)
    1531          #EQ %[@1]
    1532          <MAP >(eq_bv_eq … H2) >EQ
    1533          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 #MAP
    1539       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 ⊢ (% → ?) #H2c
    1547            >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 with
    1553             ((?=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 #EQppc
    1556            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_pointer
    1558            >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
    1559            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_ram
    1565               >set_clock_set_low_internal_ram
    1566               @low_internal_ram_write_at_stack_pointer
    1567                [ >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_ram
    1578               >set_program_counter_set_high_internal_ram
    1579               >set_clock_set_high_internal_ram
    1580               @high_internal_ram_write_at_stack_pointer
    1581                [ >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 #EQ1
    1619          @pair_elim' #fst_5_pc #rest_pc #EQ2
    1620          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 #EQn
    1625           * * #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 ?) ? = ? → ?) #EQ4
    1628           @vsplit_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
    1629           @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_sfr
    1633          
    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; #EQ4
    1638            generalize in match (refl … (vsplit bool 4 4 pc_bu))
    1639            cases (vsplit ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
    1640            generalize in match (refl … (vsplit bool 3 8 rest_addr))
    1641            cases (vsplit ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
    1642            change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
    1643            generalize in match
    1644             (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; #EQ7
    1648            @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 #MAP
    1654       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 ⊢ (% → ?) #H2c
    1661            >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 match
    1667             (refl ?
    1668              (sub_16_with_carry
    1669               (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 ⊢ (% → ?) #H2c
    1680            >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 #EQ4
    1687            @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 match
    1691           (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; #EQ1
    1694          generalize in match
    1695           (refl …
    1696             (vsplit … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
    1697          cases (vsplit ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
    1698          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 ⊢ (% → ?) #H2c
    1704            >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; #EQ4
    1711            generalize in match (refl … (vsplit bool 4 4 pc_bu))
    1712            cases (vsplit ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
    1713            generalize in match (refl … (vsplit bool 3 8 rest_addr))
    1714            cases (vsplit ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
    1715            change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
    1716            generalize in match
    1717             (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; #EQ7   
    1721            @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 ⊢ (% → ?) #H2c
    1732        >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; #ARG2
    1736        normalize nodelta; #MAP;
    1737        [1: change in ⊢ (? → %) with
    1738         ((let 〈result,flags〉 ≝
    1739           add_8_with_carry
    1740            (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 ⊢ (???% → ?) with
    1747          (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
    1748         >get_arg_8_set_clock
    1749        [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 ⊢ (? → %) with
    1753         ((let 〈result,flags〉 ≝
    1754           add_8_with_carry
    1755            (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_ram
    1761        
    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 #flags
    1766        #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 ⊢ (% → ?) #H2c
    1772        >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 #result
    1776        | 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_program
    1781       (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_program
    1786         (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 nodelta
    1793             cases (vsplit bool 1 3 nu')
    1794             #bit_1' #ignore'
    1795             normalize nodelta
    1796             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.
    18021433*)
Note: See TracChangeset for help on using the changeset viewer.