Changeset 2075


Ignore:
Timestamp:
Jun 14, 2012, 10:25:45 AM (5 years ago)
Author:
mulligan
Message:

Solved conflict in AssemblyProof?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2057 r2075  
    15291529lemma assembly_ok:
    15301530  ∀program.
     1531  ∀length_proof: |\snd program| < 2^16.
    15311532  ∀sigma: Word → Word.
    15321533  ∀policy: Word → bool.
     
    15381539  let datalabels ≝ construct_datalabels preamble in
    15391540  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 →
    15411542      (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *)
    15421543        let code_memory ≝ load_code_memory assembled in
     
    15491550              encoding_check code_memory pc pc_plus_len assembled ∧
    15501551                  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''
    15531554  @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %);
    15541555  @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %);
     
    15951596lemma fetch_assembly_pseudo2:
    15961597  ∀program.
     1598  ∀length_proof: |\snd program| < 2^16.
    15971599  ∀sigma.
    15981600  ∀policy.
     
    16001602  ∀ppc.∀ppc_ok.
    16011603  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
    1602   let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in
     1604  let 〈assembled, costs'〉 ≝ pi1 … (assembly program length_proof sigma policy) in
    16031605  let code_memory ≝ load_code_memory assembled in
    16041606  let data_labels ≝ construct_datalabels (\fst program) in
     
    16081610  let instructions ≝ expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels pi in
    16091611    fetch_many code_memory (sigma newppc) (sigma ppc) instructions.
    1610   * #preamble #instr_list #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
     1612  * #preamble #instr_list #length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_ok
    16111613  @pair_elim #labels #costs #create_label_map_refl
    16121614  @pair_elim #assembled #costs' #assembled_refl
     
    16161618  letin lookup_datalabels ≝ (λx. ?)
    16171619  @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')
    16191621  normalize nodelta
    16201622  @pair_elim #labels' #costs' #create_label_map_refl' #H
     
    16771679*)
    16781680
    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*)
     1686definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)).
    16801687
    16811688axiom low_internal_ram_of_pseudo_low_internal_ram:
     
    16851692 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
    16861693
     1694include "common/AssocList.ma".
     1695
    16871696axiom 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〉)
    16901699   let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    16911700   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) in
    16931701   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).
    16961708
    16971709(* changed from add to sub *)
    16981710axiom low_internal_ram_of_pseudo_internal_ram_miss:
    16991711 ∀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 ?).
    17091715
    17101716definition addressing_mode_ok ≝
     
    17131719   match addr with
    17141720    [ 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))
    17171723    | INDIRECT i ⇒
    17181724       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))
    17211727    | EXT_INDIRECT _ ⇒ true
    17221728    | REGISTER _ ⇒ true
    1723     | ACC_A ⇒ true
     1729    | ACC_A ⇒ match \snd M with [ None ⇒ true | _ ⇒ false ]
    17241730    | ACC_B ⇒ true
    17251731    | DPTR ⇒ true
     
    17391745definition next_internal_pseudo_address_map0 ≝
    17401746  λT.
     1747  λcm:T.
     1748  λaddr_of: Identifier → PreStatus T cm → Word.
    17411749  λfetched.
    17421750  λM: internal_pseudo_address_map.
    1743   λcm:T.
    17441751  λs: PreStatus T cm.
    17451752   match fetched with
     
    17471754    | Cost _ ⇒ Some … M
    17481755    | 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〉
    17511761    | Mov _ _ ⇒ Some … M
    17521762    | Instruction instr ⇒
     
    17851795    let p ≝ pi1 … (assembly pap sigma policy) in
    17861796      load_code_memory (\fst p).
     1797
     1798definition 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  //
     1814qed.
    17871815
    17881816definition status_of_pseudo_status:
     
    22042232                     else None internal_pseudo_address_map )
    22052233                    =Some internal_pseudo_address_map M')
    2206 *)
    22072234
    22082235axiom low_internal_ram_write_at_stack_pointer:
     
    22632290  cases daemon (* XXX: !!! *)
    22642291qed.
     2292*)
    22652293
    22662294lemma Some_Some_elim:
Note: See TracChangeset for help on using the changeset viewer.