Changeset 2272 for src/ASM/Test.ma


Ignore:
Timestamp:
Jul 27, 2012, 5:53:25 PM (8 years ago)
Author:
mulligan
Message:

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2258 r2272  
    9696  λM, sigma, v.
    9797  match \snd M with
    98   [ data ⇒ v
    99   | address upper_lower word ⇒
    100     let mapped ≝ sigma word in
    101     let 〈high, low〉 ≝ vsplit bool 8 8 mapped in
     98  [ None ⇒ v
     99  | Some upper_lower_addr ⇒
     100    let 〈upper_lower, addr〉 ≝ upper_lower_addr in
    102101      if eq_upper_lower upper_lower upper then
    103         high
     102        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (v@@addr)) in
     103          high
    104104      else
    105         low
     105        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (addr@@v)) in
     106          low
    106107  ].
    107108
     
    113114  λaddress: Byte.
    114115  λvalue: Byte.
    115   match assoc_list_lookup ?? address (eq_bv …) (\fst M) with
     116  match lookup_from_internal_ram … address M with
    116117  [ None ⇒ value
    117118  | Some upper_lower_word ⇒
    118119    let 〈upper_lower, word〉 ≝ upper_lower_word in
    119     let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in
    120120      if eq_upper_lower upper_lower upper then
    121         high
     121        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (value@@word)) in
     122          high
    122123      else
    123         low
     124        let 〈high, low〉 ≝ vsplit bool 8 8 (sigma (word@@value)) in
     125          low
    124126  ].
    125127
     
    216218qed.
    217219
     220lemma get_index_v_set_index_hit:
     221  ∀A: Type[0].
     222  ∀n: nat.
     223  ∀v: Vector A n.
     224  ∀i: nat.
     225  ∀e: A.
     226  ∀i_lt_n_proof: i < n.
     227  ∀i_lt_n_proof': i < n.
     228    get_index_v A n (set_index A n v i e i_lt_n_proof) i i_lt_n_proof' = e.
     229  #A #n #v elim v
     230  [1:
     231    #i #e #i_lt_n_proof
     232    cases (lt_to_not_zero … i_lt_n_proof)
     233  |2:
     234    #n' #hd #tl #inductive_hypothesis #i #e
     235    cases i
     236    [1:
     237      #i_lt_n_proof #i_lt_n_proof' %
     238    |2:
     239      #i' #i_lt_n_proof' #i_lt_n_proof''
     240      whd in ⊢ (??%?); @inductive_hypothesis
     241    ]
     242  ]
     243qed.
     244
    218245lemma set_index_status_of_pseudo_status:
    219246  ∀M, code_memory, sigma, policy, s, sfr, v, v'.
     
    230257  whd in match status_of_pseudo_status; normalize nodelta
    231258  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
    232   inversion (\snd M) try (#upper_lower #address) #sndM_refl normalize nodelta
     259  inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta
    233260  [1:
    234261    <sfr_neq_acc_a_assm cases sfr
     
    240267    %
    241268  |2:
     269    inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
    242270    @pair_elim #high #low #high_low_refl normalize nodelta
    243     inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta
    244     <sfr_neq_acc_a_assm cases sfr
     271    whd in match set_8051_sfr; normalize nodelta
     272    <sfr_neq_acc_a_assm
     273    cases sfr in high_low_refl sfr_neq_acc_a_assm;
    245274    [18,37:
     275      @pair_elim #high' #low' #high_low_refl'
     276      #high_low_refl
    246277      whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    247278      whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta
    248       >sndM_refl normalize nodelta >high_low_refl normalize nodelta
     279      >sndM_refl normalize nodelta
    249280      >eq_upper_lower_refl normalize nodelta
    250       whd in match (set_8051_sfr ?????);
    251281      [1:
     282        #relevant >relevant
    252283        <set_index_set_index_overwrite in ⊢ (??%?);
    253         <set_index_set_index_overwrite in ⊢ (???%); %
     284        <set_index_set_index_overwrite in ⊢ (???%);
     285        >get_index_v_set_index_hit in high_low_refl';
     286        #assm >assm in relevant; normalize nodelta * %
    254287      |2:
     288        #relevant >relevant
    255289        <set_index_set_index_overwrite in ⊢ (??%?);
    256         <set_index_set_index_overwrite in ⊢ (???%); %
     290        <set_index_set_index_overwrite in ⊢ (???%);
     291        >get_index_v_set_index_hit in high_low_refl';
     292        #assm >assm in relevant; normalize nodelta * %
    257293      ]
    258294    ]
    259295    whd in match map_address_using_internal_pseudo_address_map; normalize nodelta
    260     whd in match (set_8051_sfr ?????); @set_index_set_index_commutation normalize
    261     @nmk #absurd destruct(absurd)
     296    #relevant * >get_index_v_set_index_miss
     297    try (% #absurd normalize in absurd; destruct(absurd))
     298    >relevant normalize nodelta
     299    @set_index_set_index_commutation % #absurd normalize in absurd; destruct(absurd)
    262300  ]
    263301qed.
    264302
     303(*
    265304lemma get_index_v_status_of_pseudo_status:
    266305  ∀M, code_memory, sigma, policy, s, s', sfr.
     
    301340  ]
    302341qed.
     342*)
    303343
    304344lemma set_8051_sfr_status_of_pseudo_status:
     
    313353qed.
    314354
     355(*
    315356lemma get_8051_sfr_status_of_pseudo_status:
    316357  ∀M, code_memory, sigma, policy, s, s', s'', sfr.
     
    324365  whd in match get_8051_sfr; normalize nodelta
    325366  @get_index_v_status_of_pseudo_status %
    326 qed.
     367qed.*)
    327368
    328369lemma get_8052_sfr_status_of_pseudo_status:
     
    424465  (code_memory_of_pseudo_assembly_program cm sigma policy)
    425466  s'
    426   (low_internal_ram_of_pseudo_low_internal_ram M ram)
     467  (low_internal_ram_of_pseudo_low_internal_ram M sigma ram)
    427468  = status_of_pseudo_status M cm
    428469    (set_low_internal_ram pseudo_assembly_program cm s ram) sigma policy.
     
    435476 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' →
    436477  insert Byte 7 addr v'
    437   (low_internal_ram_of_pseudo_low_internal_ram M
     478  (low_internal_ram_of_pseudo_low_internal_ram M sigma
    438479   (low_internal_ram pseudo_assembly_program cm s))
    439   =low_internal_ram_of_pseudo_low_internal_ram M
     480  =low_internal_ram_of_pseudo_low_internal_ram M sigma
    440481   (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).
    441482               
     
    447488    (code_memory_of_pseudo_assembly_program cm sigma policy)
    448489    (status_of_pseudo_status M cm s sigma policy))
    449   = low_internal_ram_of_pseudo_low_internal_ram M
     490  = low_internal_ram_of_pseudo_low_internal_ram M sigma
    450491     (insert Byte 7 addr v
    451492      (low_internal_ram pseudo_assembly_program cm s)).
     
    458499 map_internal_ram_address_using_pseudo_address_map M sigma (true:::addr) v = v' →
    459500  insert Byte 7 addr v'
    460   (high_internal_ram_of_pseudo_high_internal_ram M
     501  (high_internal_ram_of_pseudo_high_internal_ram M sigma
    461502   (high_internal_ram pseudo_assembly_program cm s))
    462   =high_internal_ram_of_pseudo_high_internal_ram M
     503  =high_internal_ram_of_pseudo_high_internal_ram M sigma
    463504   (insert Byte 7 addr v (high_internal_ram pseudo_assembly_program cm s)).
    464505
     
    470511    (code_memory_of_pseudo_assembly_program cm sigma policy)
    471512    (status_of_pseudo_status M cm s sigma policy))
    472   = high_internal_ram_of_pseudo_high_internal_ram M
     513  = high_internal_ram_of_pseudo_high_internal_ram M sigma
    473514     (insert Byte 7 addr v
    474515      (high_internal_ram pseudo_assembly_program cm s)).
     
    13741415  >get_index_v_set_index_miss [2,4: /2/] %
    13751416qed.
     1417
     1418lemma get_8051_sfr_status_of_pseudo_status:
     1419  ∀M.
     1420  ∀cm, ps, sigma, policy.
     1421  ∀sfr.
     1422    (sfr = SFR_ACC_A → \snd M = None …) →
     1423    get_8051_sfr (BitVectorTrie Byte 16)
     1424      (code_memory_of_pseudo_assembly_program cm sigma policy)
     1425      (status_of_pseudo_status M cm ps sigma policy) sfr =
     1426    get_8051_sfr pseudo_assembly_program cm ps sfr.
     1427  #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant
     1428  [18:
     1429     >relevant %
     1430  ]
     1431  cases sndM try % * #address
     1432  whd in match get_8051_sfr;
     1433  whd in match status_of_pseudo_status; normalize nodelta
     1434  whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address
     1435  cases (eq_upper_lower ??) normalize nodelta
     1436  @pair_elim #upper #lower #upper_lower_refl
     1437  @get_index_v_set_index_miss @nmk #relevant
     1438  normalize in relevant; destruct(relevant)
     1439qed.
     1440
     1441lemma get_arg_8_pseudo_addressing_mode_ok:
     1442  ∀M: internal_pseudo_address_map.
     1443  ∀cm: pseudo_assembly_program.
     1444  ∀ps: PreStatus pseudo_assembly_program cm.
     1445  ∀sigma: Word → Word.
     1446  ∀policy: Word → bool.
     1447  ∀addr1: [[registr; direct]].
     1448    assert_data pseudo_assembly_program M cm ps addr1 = true →
     1449      get_arg_8 (BitVectorTrie Byte 16)
     1450        (code_memory_of_pseudo_assembly_program cm sigma policy)
     1451        (status_of_pseudo_status M cm ps sigma policy) true addr1 =
     1452      get_arg_8 pseudo_assembly_program cm ps true addr1.
     1453  [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
     1454  #M #cm #ps #sigma #policy #addr1
     1455  @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);
     1456  [1:
     1457    whd in ⊢ (??%? → ??%?);
     1458    whd in match bit_address_of_register; normalize nodelta
     1459    @pair_elim #un #ln #un_ln_refl
     1460    lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl
     1461    @(pair_replace ?????????? un_ln_refl)
     1462    [1:
     1463      whd in match get_8051_sfr; normalize nodelta
     1464      whd in match sfr_8051_index; normalize nodelta
     1465      @eq_f <get_index_v_special_function_registers_8051_not_acc_a
     1466      try % #absurd destruct(absurd)
     1467    |2:
     1468      #assembly_mode_ok_refl
     1469      >low_internal_ram_of_pseudo_internal_ram_miss
     1470      [1:
     1471        %
     1472      |2:
     1473        cases (data_or_address ?????) in assembly_mode_ok_refl; normalize nodelta
     1474        [1:
     1475          #absurd destruct(absurd)
     1476        |2:
     1477          * normalize nodelta
     1478          [1:
     1479          |2:
     1480            #_ #absurd destruct(absurd)
     1481          ]
     1482        #absurd try % @sym_eq assumption
     1483      ]
     1484    ]
     1485  |2:
     1486    #addressing_mode_ok_refl whd in ⊢ (??%?);
     1487    @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*
     1488    @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta
     1489    inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta
     1490    [1:
     1491      whd in ⊢ (??%%); normalize nodelta
     1492      cases (eqb ??) normalize nodelta [1: % ]
     1493      cases (eqb ??) normalize nodelta [1: % ]
     1494      cases (eqb ??) normalize nodelta [1: % ]
     1495      cases (eqb ??) normalize nodelta [1: % ]
     1496      cases (eqb ??) normalize nodelta [1:
     1497        @get_8051_sfr_status_of_pseudo_status
     1498        #absurd destruct(absurd)
     1499      ]
     1500      cases (eqb ??) normalize nodelta [1:
     1501        @get_8051_sfr_status_of_pseudo_status
     1502        #absurd destruct(absurd)
     1503      ]
     1504      cases (eqb ??) normalize nodelta [1:
     1505        @get_8051_sfr_status_of_pseudo_status
     1506        #absurd destruct(absurd)
     1507      ]
     1508      cases (eqb ??) normalize nodelta [1:
     1509        @get_8051_sfr_status_of_pseudo_status
     1510        #absurd destruct(absurd)
     1511      ]
     1512      cases (eqb ??) normalize nodelta [1:
     1513        @get_8051_sfr_status_of_pseudo_status
     1514        #absurd destruct(absurd)
     1515      ]
     1516      cases (eqb ??) normalize nodelta [1: % ]
     1517      cases (eqb ??) normalize nodelta [1: % ]
     1518      cases (eqb ??) normalize nodelta [1: % ]
     1519      cases (eqb ??) normalize nodelta [1: % ]
     1520      cases (eqb ??) normalize nodelta [1: % ]
     1521      cases (eqb ??) normalize nodelta [1:
     1522        @get_8051_sfr_status_of_pseudo_status
     1523        #absurd destruct(absurd)
     1524      ]
     1525      cases (eqb ??) normalize nodelta [1:
     1526        @get_8051_sfr_status_of_pseudo_status
     1527        #absurd destruct(absurd)
     1528      ]
     1529      cases (eqb ??) normalize nodelta [1:
     1530        @get_8051_sfr_status_of_pseudo_status
     1531        #absurd destruct(absurd)
     1532      ]
     1533      cases (eqb ??) normalize nodelta [1:
     1534        @get_8051_sfr_status_of_pseudo_status
     1535        #absurd destruct(absurd)
     1536      ]
     1537      cases (eqb ??) normalize nodelta [1:
     1538        @get_8051_sfr_status_of_pseudo_status
     1539        #absurd destruct(absurd)
     1540      ]
     1541      cases (eqb ??) normalize nodelta [1:
     1542        @get_8051_sfr_status_of_pseudo_status
     1543        #absurd destruct(absurd)
     1544      ]
     1545      cases (eqb ??) normalize nodelta [1:
     1546        @get_8051_sfr_status_of_pseudo_status
     1547        #absurd destruct(absurd)
     1548      ]
     1549      cases (eqb ??) normalize nodelta [1:
     1550        @get_8051_sfr_status_of_pseudo_status
     1551        #absurd destruct(absurd)
     1552      ]
     1553      cases (eqb ??) normalize nodelta [1:
     1554        @get_8051_sfr_status_of_pseudo_status
     1555        #absurd destruct(absurd)
     1556      ]
     1557      cases (eqb ??) normalize nodelta [1:
     1558        @get_8051_sfr_status_of_pseudo_status
     1559        #absurd destruct(absurd)
     1560      ]
     1561      inversion (eqb ??) #eqb_refl normalize nodelta [1:
     1562        @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl
     1563        whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)
     1564        >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta
     1565        #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_
     1566        #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %
     1567      ]
     1568      cases (eqb ??) normalize nodelta [1:
     1569        @get_8051_sfr_status_of_pseudo_status
     1570        #absurd destruct(absurd)
     1571      ] %
     1572    |2:
     1573      lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant
     1574      whd in match status_of_pseudo_status; normalize nodelta
     1575      >low_internal_ram_of_pseudo_internal_ram_miss try %
     1576      cut(arg = false:::(three_bits@@nl))
     1577      [1:
     1578        <get_index_v_refl
     1579        cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)
     1580        [1:
     1581          cut(ignore = [[get_index_v bool 4 nu 0 ?]])
     1582          [1:
     1583            @le_S_S @le_O_n
     1584          |2:
     1585            cut(ignore = \fst (vsplit bool 1 3 nu))
     1586            [1:
     1587              >ignore_three_bits_refl %
     1588            |2:
     1589              #ignore_refl >ignore_refl
     1590              cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl
     1591              >nu_refl %
     1592            ]
     1593          |3:
     1594            #ignore_refl >ignore_refl in ignore_three_bits_refl;
     1595            #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))
     1596            #nu_refl <nu_refl %
     1597          ]
     1598        |2:
     1599          #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl
     1600          @sym_eq @vsplit_ok >nu_nl_refl %
     1601        ]
     1602      |2:
     1603        #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;
     1604        normalize nodelta
     1605        [1:
     1606          cases (eq_bv ???) normalize #absurd destruct(absurd)
     1607        |2:
     1608          #_ %
     1609        ]
     1610      ]
     1611    ]
     1612  ] *)
     1613qed.
Note: See TracChangeset for help on using the changeset viewer.