Changeset 949


Ignore:
Timestamp:
Jun 13, 2011, 6:42:14 PM (8 years ago)
Author:
mulligan
Message:

resolved conflict, work from today

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r744 r949  
    8888  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
    8989  @le_S @le_S @le_n (* ugly: fix using tacticals *)
     90qed.
     91
     92(* dpm: needed for assembly proof *)
     93definition sub_7_with_carry ≝
     94  λb, c: BitVector 7.
     95  λcarry: bool.
     96  sub_n_with_carry 7 b c carry ?.
     97  @le_S @le_S @le_n
    9098qed.
    9199
  • src/ASM/AssemblyProof.ma

    r948 r949  
    14991499    bu@@bl = sigma (code_memory … s) (pbu@@pbl).
    15001500
     1501(* changed from add to sub *)
    15011502axiom low_internal_ram_of_pseudo_internal_ram_miss:
    15021503 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.
    15031504  let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in
    1504   let 〈carr,Saddr〉 ≝ half_add ? addr (bitvector_of_nat 7 1) in
     1505  let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in
     1506  let carr ≝ get_index_v ? ? flags 1 ? in
    15051507  carr = false →
    1506   member ? (eq_bv 8) (false:::addr) M = false →
    1507    member ? (eq_bv 8) (false:::Saddr) M = false →
    1508     lookup ? 7 Saddr ram = lookup ? 7 Saddr (low_internal_ram … s).
     1508  member ? (eq_bv 8) (false:::Saddr) M = false →
     1509   member ? (eq_bv 8) (false:::addr) M = false →
     1510    lookup ? 7 addr ram (zero ?) = lookup ? 7 addr (low_internal_ram … s) (zero ?).
     1511  //
     1512qed.
    15091513
    15101514definition addressing_mode_ok ≝
     
    19911995      #bit1' #ignore'
    19921996      normalize nodelta
    1993       cases (get_index_v bool 4 nu' 1 ?)
     1997      cases (get_index_v bool 4 nu' 0 ?)
    19941998      [1,2,3,4:
    19951999        normalize nodelta
     
    20042008    ]
    20052009 ]
     2010 
     2011
    20062012qed.
    20072013
     
    21422148qed.
    21432149
    2144 (*
     2150axiom split_elim':
     2151  ∀A: Type[0].
     2152  ∀B: Type[1].
     2153  ∀l, m, v.
     2154  ∀T: Vector A l → Vector A m → B.
     2155  ∀P: B → Prop.
     2156    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt)) →
     2157      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt).
     2158
     2159axiom split_elim'':
     2160  ∀A: Type[0].
     2161  ∀B,B': Type[1].
     2162  ∀l, m, v.
     2163  ∀T: Vector A l → Vector A m → B.
     2164  ∀T': Vector A l → Vector A m → B'.
     2165  ∀P: B → B' → Prop.
     2166    (∀lft, rgt. v = lft @@ rgt → P (T lft rgt) (T' lft rgt)) →
     2167      P (let 〈lft, rgt〉 ≝ split A l m v in T lft rgt)
     2168        (let 〈lft, rgt〉 ≝ split A l m v in T' lft rgt).
     2169
     2170axiom split_append:
     2171  ∀A: Type[0].
     2172  ∀m, n: nat.
     2173  ∀v, v': Vector A m.
     2174  ∀q, q': Vector A n.
     2175    let 〈v', q'〉 ≝ split A m n (v@@q) in
     2176      v = v' ∧ q = q'.
     2177
     2178axiom split_vector_singleton:
     2179  ∀A: Type[0].
     2180  ∀n: nat.
     2181  ∀v: Vector A (S n).
     2182  ∀rest: Vector A n.
     2183  ∀s: Vector A 1.
     2184  ∀prf.
     2185    v = s @@ rest →
     2186    ((get_index_v A ? v 0 prf) ::: rest) = v.
     2187
     2188axiom sub_minus_one_seven_eight:
     2189  ∀v: BitVector 7.
     2190  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
     2191  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
     2192
    21452193lemma blah:
    2146   ∀p: pseudo_instruction.
    2147   ∀m: pseudo_internal_address_map.
     2194  ∀m: internal_pseudo_address_map.
    21482195  ∀s: PseudoStatus.
    21492196  ∀arg: Byte.
    2150     next_internal_pseudo_address_map0 p m s (DIRECT arg) = Some ? →
    2151       get_arg_8 (next_internal_pseudo_address_map0 p (internal_ram ? s) s (DIRECT arg)) =
    2152       get_arg_8 (internal_ram ? s) (DIRECT arg).
    2153 
     2197  ∀b: bool.
     2198    addressing_mode_ok m s (DIRECT arg) = true →
     2199      get_arg_8 ? (set_low_internal_ram ? s (low_internal_ram_of_pseudo_low_internal_ram m (low_internal_ram ? s))) b (DIRECT arg) =
     2200      get_arg_8 ? s b (DIRECT arg).
     2201  [2, 3: normalize % ]
     2202  #m #s #arg #b #hyp
     2203  whd in ⊢ (??%%)
     2204  @split_elim''
     2205  #nu' #nl' #arg_nu_nl_eq
     2206  normalize nodelta
     2207  generalize in match (refl ? (get_index_v bool 4 nu' ? ?))
     2208  cases (get_index_v bool 4 nu' ? ?) in ⊢ (??%? → %)
     2209  #get_index_v_eq
     2210  normalize nodelta
     2211  [2:
     2212    normalize nodelta
     2213    @split_elim''
     2214    #bit_one' #three_bits' #bit_one_three_bit_eq
     2215    generalize in match (low_internal_ram_of_pseudo_internal_ram_miss m s (three_bits'@@nl'))
     2216    normalize nodelta
     2217    generalize in match (refl ? (sub_7_with_carry ? ? ?))
     2218    cases (sub_7_with_carry ? ? ?) in ⊢ (??%? → %)
     2219    #Saddr #carr' #Saddr_carr_eq
     2220    normalize nodelta
     2221    #carr_hyp'
     2222    @carr_hyp'
     2223    [1:
     2224    |2: whd in hyp:(??%?); generalize in match hyp; -hyp;
     2225        generalize in match (refl ? (¬(member (BitVector 8) ? arg m)))
     2226        cases (¬(member (BitVector 8) ? arg m)) in ⊢ (??%? → %)
     2227        #member_eq
     2228        normalize nodelta
     2229        [2: #destr destruct(destr)
     2230        |1: -carr_hyp';
     2231            >arg_nu_nl_eq
     2232            <(split_vector_singleton ? ? nu' ? ? ? bit_one_three_bit_eq)
     2233            [1: >get_index_v_eq in ⊢ (??%? → ?)
     2234            |2: @le_S @le_S @le_S @le_n
     2235            ]
     2236            cases (member (BitVector 8) ? (\fst ?) ?)
     2237            [1: #destr normalize in destr; destruct(destr)
     2238            |2:
     2239            ]
     2240        ]
     2241    |3: >get_index_v_eq in ⊢ (??%?)
     2242        change in ⊢ (??(???%?)?) with ((? ::: three_bits') @@ nl')
     2243        >(split_vector_singleton … bit_one_three_bit_eq)
     2244        <arg_nu_nl_eq
     2245        whd in hyp:(??%?)
     2246        cases (member (BitVector 8) (eq_bv 8) arg m) in hyp
     2247        normalize nodelta [*: #ignore @sym_eq ]
     2248    ]
     2249  |
     2250  ].
     2251 
     2252(*
    21542253map_address0 ... (DIRECT arg) = Some .. →
    21552254  get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
  • src/ASM/Status.ma

    r935 r949  
    420420    let sfr ≝ special_function_registers_8051 ? s in
    421421    let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in
    422       get_index_v bool 8 psw (S O) ?.
     422      get_index_v bool 8 psw 1 ?.
    423423    normalize
    424424    repeat (@ (le_S_S ? ?))
     
    826826        λdirect: True.
    827827          let 〈 nu, nl 〉 ≝ split … 4 4 d in
    828           let bit_1 ≝ get_index_v … nu 1 ? in
    829             match bit_1 with
    830               [ true ⇒
    831                   let 〈 bit_one, three_bits 〉 ≝ split ? 1 3 nu in
     828          let bit_one ≝ get_index_v ? ? nu 0 ? in
     829          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
     830            match bit_one with
     831              [ false ⇒
    832832                  let address ≝ three_bits @@ nl in
    833833                    lookup ? 7 address (low_internal_ram ? s) (zero 8)
    834               | false ⇒ get_bit_addressable_sfr ? s 8 d l
     834              | true ⇒ get_bit_addressable_sfr ? s 8 d l
    835835              ]
    836836      | INDIRECT i ⇒
     
    839839          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
    840840          let bit_1 ≝ get_index_v … bit_one_v O ? in
    841           match bit_1 with
    842             [ true ⇒
     841          match  bit_1 with
     842            [ false ⇒
    843843                lookup ? 7 (three_bits @@ nl) (low_internal_ram ? s) (zero 8)
    844             | false ⇒
     844            | true ⇒
    845845                lookup ? 7 (three_bits @@ nl) (high_internal_ram ? s) (zero 8)
    846846            ]
     
    865865        λdirect: True.
    866866          let 〈 nu, nl 〉 ≝ split … 4 4 d in
    867           let bit_1 ≝ get_index_v … nu 1 ? in
     867          let bit_one ≝ get_index_v ? ? nu 0 ? in
    868868          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
    869             match bit_1 with
     869            match bit_one with
    870870              [ true ⇒ set_bit_addressable_sfr ? s d v
    871871              | false ⇒
     
    877877          let register ≝ get_register ? s [[ false; false; i ]] in
    878878          let 〈nu, nl〉 ≝ split ? 4 4 register in
    879           let bit_1 ≝ get_index_v … nu 1 ? in
     879          let bit_1 ≝ get_index_v … nu 0 ? in
    880880          let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in
    881881            match bit_1 with
    882               [ true ⇒
     882              [ false ⇒
    883883                let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ? s) in
    884884                  set_low_internal_ram ? s memory
    885               | false ⇒
     885              | true ⇒
    886886                let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ? s) in
    887887                  set_high_internal_ram ? s memory
     
    972972        λbit_addr: True.
    973973          let 〈 nu, nl 〉 ≝ split … 4 4 b in
    974           let bit_1 ≝ get_index_v … nu 1 ? in
     974          let bit_1 ≝ get_index_v … nu 0 ? in
    975975          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
    976976            match bit_1 with
     
    991991        λn_bit_addr: True.
    992992          let 〈 nu, nl 〉 ≝ split … 4 4 n in
    993           let bit_1 ≝ get_index_v … nu 1 ? in
     993          let bit_1 ≝ get_index_v … nu 0 ? in
    994994          let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in
    995995            match bit_1 with
     
    10261026      [ BIT_ADDR b ⇒ λbit_addr: True.
    10271027          let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in
    1028           let bit_1 ≝ get_index_v … nu 1 ? in
     1028          let bit_1 ≝ get_index_v … nu 0 ? in
    10291029          let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in
    10301030          match bit_1 with
Note: See TracChangeset for help on using the changeset viewer.