Changeset 949 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 13, 2011, 6:42:14 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r948 r949 1499 1499 bu@@bl = sigma (code_memory … s) (pbu@@pbl). 1500 1500 1501 (* changed from add to sub *) 1501 1502 axiom low_internal_ram_of_pseudo_internal_ram_miss: 1502 1503 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7. 1503 1504 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 1505 1507 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 // 1512 qed. 1509 1513 1510 1514 definition addressing_mode_ok ≝ … … 1991 1995 #bit1' #ignore' 1992 1996 normalize nodelta 1993 cases (get_index_v bool 4 nu' 1?)1997 cases (get_index_v bool 4 nu' 0 ?) 1994 1998 [1,2,3,4: 1995 1999 normalize nodelta … … 2004 2008 ] 2005 2009 ] 2010 2011 2006 2012 qed. 2007 2013 … … 2142 2148 qed. 2143 2149 2144 (* 2150 axiom 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 2159 axiom 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 2170 axiom 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 2178 axiom 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 2188 axiom 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 2145 2193 lemma blah: 2146 ∀p: pseudo_instruction. 2147 ∀m: pseudo_internal_address_map. 2194 ∀m: internal_pseudo_address_map. 2148 2195 ∀s: PseudoStatus. 2149 2196 ∀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 (* 2154 2253 map_address0 ... (DIRECT arg) = Some .. → 2155 2254 get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) =
Note: See TracChangeset
for help on using the changeset viewer.