Changeset 2075 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 14, 2012, 10:25:45 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2057 r2075 1529 1529 lemma assembly_ok: 1530 1530 ∀program. 1531 ∀length_proof: \snd program < 2^16. 1531 1532 ∀sigma: Word → Word. 1532 1533 ∀policy: Word → bool. … … 1538 1539 let datalabels ≝ construct_datalabels preamble in 1539 1540 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in 1540 〈assembled,costs'〉 = assembly program sigma policy →1541 〈assembled,costs'〉 = assembly program length_proof sigma policy → 1541 1542 (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *) 1542 1543 let code_memory ≝ load_code_memory assembled in … … 1549 1550 encoding_check code_memory pc pc_plus_len assembled ∧ 1550 1551 sigma newppc = add … pc (bitvector_of_nat … len). 1551 #program # sigma #policy #sigma_policy_witness #assembled #costs'1552 cases (assembly program sigma policy) * #assembled' #costs''1552 #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs' 1553 cases (assembly program length_proof sigma policy) * #assembled' #costs'' 1553 1554 @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %); 1554 1555 @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %); … … 1595 1596 lemma fetch_assembly_pseudo2: 1596 1597 ∀program. 1598 ∀length_proof: \snd program < 2^16. 1597 1599 ∀sigma. 1598 1600 ∀policy. … … 1600 1602 ∀ppc.∀ppc_ok. 1601 1603 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 1602 let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in1604 let 〈assembled, costs'〉 ≝ pi1 … (assembly program length_proof sigma policy) in 1603 1605 let code_memory ≝ load_code_memory assembled in 1604 1606 let data_labels ≝ construct_datalabels (\fst program) in … … 1608 1610 let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in 1609 1611 fetch_many code_memory (sigma newppc) (sigma ppc) instructions. 1610 * #preamble #instr_list # sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok1612 * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok 1611 1613 @pair_elim #labels #costs #create_label_map_refl 1612 1614 @pair_elim #assembled #costs' #assembled_refl … … 1616 1618 letin lookup_datalabels ≝ (λx. ?) 1617 1619 @pair_elim #pi #newppc #fetch_pseudo_refl 1618 lapply (assembly_ok 〈preamble, instr_list〉 sigma policy sigma_policy_specification_witness assembled costs')1620 lapply (assembly_ok 〈preamble, instr_list〉 sigma ? policy sigma_policy_specification_witness assembled costs') 1619 1621 normalize nodelta 1620 1622 @pair_elim #labels' #costs' #create_label_map_refl' #H … … 1677 1679 *) 1678 1680 1679 definition internal_pseudo_address_map ≝ list (BitVector 8). 1681 (* XXX: changed this type. Bool specifies whether byte is first or second 1682 component of an address, and the Word is the pseudoaddress that it 1683 corresponds to. Second component is the same principle for the accumulator 1684 A. 1685 *) 1686 definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)). 1680 1687 1681 1688 axiom low_internal_ram_of_pseudo_low_internal_ram: … … 1685 1692 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. 1686 1693 1694 include "common/AssocList.ma". 1695 1687 1696 axiom low_internal_ram_of_pseudo_internal_ram_hit: 1688 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀ addr:BitVector 7.1689 member ? (eq_bv 8) (false:::addr) M = true→1697 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀sigma:Word → Word × bool.∀high: bool. ∀points_to: Word. ∀addr:BitVector 7. 1698 assoc_list_lookup ?? (false:::addr) (eq_bv 8) (\fst M) = Some … (〈high, points_to〉) → 1690 1699 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 1691 1700 let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in 1692 let pbu ≝ lookup ? 7 (add ? addr (bitvector_of_nat 7 1)) (low_internal_ram … s) (zero 8) in1693 1701 let bl ≝ lookup ? 7 addr ram (zero 8) in 1694 let bu ≝ lookup ? 7 (add ? addr (bitvector_of_nat 7 1)) ram (zero 8) in 1695 bu@@bl = \fst (sigma (pbu@@pbl)). 1702 let 〈lower, higher〉 ≝ vsplit ? 8 8 points_to in 1703 let 〈plower, phigher〉 ≝ vsplit ? 8 8 (\fst (sigma points_to)) in 1704 if high then 1705 (pbl = higher) ∧ (bl = phigher) 1706 else 1707 (pbl = lower) ∧ (bl = plower). 1696 1708 1697 1709 (* changed from add to sub *) 1698 1710 axiom low_internal_ram_of_pseudo_internal_ram_miss: 1699 1711 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7. 1700 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 1701 let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in 1702 let carr ≝ get_index_v ? ? flags 1 ? in 1703 carr = false → 1704 member ? (eq_bv 8) (false:::Saddr) M = false → 1705 member ? (eq_bv 8) (false:::addr) M = false → 1706 lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?). 1707 // 1708 qed. 1712 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 1713 assoc_list_exists ?? (false:::addr) (eq_bv 8) (\fst M) = false → 1714 lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?). 1709 1715 1710 1716 definition addressing_mode_ok ≝ … … 1713 1719 match addr with 1714 1720 [ DIRECT d ⇒ 1715 ¬( member ? (eq_bv 8) d M) ∧1716 ¬( member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)1721 ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧ 1722 ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M)) 1717 1723  INDIRECT i ⇒ 1718 1724 let d ≝ get_register … s [[false;false;i]] in 1719 ¬( member ? (eq_bv 8) d M) ∧1720 ¬( member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M)1725 ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) ∧ 1726 ¬(assoc_list_exists ?? (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) (eq_bv 8) (\fst M)) 1721 1727  EXT_INDIRECT _ ⇒ true 1722 1728  REGISTER _ ⇒ true 1723  ACC_A ⇒ true1729  ACC_A ⇒ match \snd M with [ None ⇒ true  _ ⇒ false ] 1724 1730  ACC_B ⇒ true 1725 1731  DPTR ⇒ true … … 1739 1745 definition next_internal_pseudo_address_map0 ≝ 1740 1746 λT. 1747 λcm:T. 1748 λaddr_of: Identifier → PreStatus T cm → Word. 1741 1749 λfetched. 1742 1750 λM: internal_pseudo_address_map. 1743 λcm:T.1744 1751 λs: PreStatus T cm. 1745 1752 match fetched with … … 1747 1754  Cost _ ⇒ Some … M 1748 1755  Jmp _ ⇒ Some … M 1749  Call _ ⇒ 1750 Some … (add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1)::M) 1756  Call a ⇒ 1757 let a' ≝ addr_of a s in 1758 let 〈callM, accM〉 ≝ M in 1759 Some … 〈〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 1)), 〈false, a'〉〉:: 1760 〈(add 8 (get_8051_sfr ?? s SFR_SP) (bitvector_of_nat 8 2)), 〈true, a'〉〉::callM, accM〉 1751 1761  Mov _ _ ⇒ Some … M 1752 1762  Instruction instr ⇒ … … 1785 1795 let p ≝ pi1 … (assembly pap sigma policy) in 1786 1796 load_code_memory (\fst p). 1797 1798 definition sfr_8051_of_pseudo_sfr_8051 ≝ 1799 λM: internal_pseudo_address_map. 1800 λsfrs: Vector Byte 19. 1801 λsigma: Word → Word. 1802 match \snd M with 1803 [ None ⇒ sfrs 1804  Some s ⇒ 1805 let 〈high, address〉 ≝ s in 1806 let index ≝ sfr_8051_index SFR_ACC_A in 1807 let 〈upper, lower〉 ≝ vsplit ? 8 8 (sigma address) in 1808 if high then 1809 set_index Byte 19 sfrs index upper ? 1810 else 1811 set_index Byte 19 sfrs index lower ? 1812 ]. 1813 // 1814 qed. 1787 1815 1788 1816 definition status_of_pseudo_status: … … 2204 2232 else None internal_pseudo_address_map ) 2205 2233 =Some internal_pseudo_address_map M') 2206 *)2207 2234 2208 2235 axiom low_internal_ram_write_at_stack_pointer: … … 2263 2290 cases daemon (* XXX: !!! *) 2264 2291 qed. 2292 *) 2265 2293 2266 2294 lemma Some_Some_elim:
Note: See TracChangeset
for help on using the changeset viewer.