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

resolved conflict, work from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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) =
Note: See TracChangeset for help on using the changeset viewer.