Changeset 2122 for src/ASM/BitVector.ma
 Timestamp:
 Jun 27, 2012, 3:36:54 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVector.ma
r2121 r2122 235 235 ∀b: BitVector n. 236 236 String. 237 238 example sub_minus_one_seven_eight: 239 ∀v: BitVector 7. 240 false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) = 241 \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false). 242 cases daemon. 243 qed. 244 245 axiom sub16_with_carry_overflow: 246 ∀left, right, result: BitVector 16. 247 ∀flags: BitVector 3. 248 ∀upper: BitVector 9. 249 ∀lower: BitVector 7. 250 sub_16_with_carry left right false = 〈result, flags〉 → 251 vsplit bool 9 7 result = 〈upper, lower〉 → 252 get_index_v bool 3 flags 2 ? = true → 253 upper = [[true; true; true; true; true; true; true; true; true]]. 254 // 255 qed. 256 257 axiom sub_16_to_add_16_8_0: 258 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 259 get_index' ? 2 0 flags = false → 260 sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 → 261 v1 = add ? v2 (sign_extension (false:::v3)). 262 263 axiom sub_16_to_add_16_8_1: 264 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3. 265 get_index' ? 2 0 flags = true → 266 sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 → 267 v1 = add ? v2 (sign_extension (true:::v3)).
Note: See TracChangeset
for help on using the changeset viewer.