Changeset 2122 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Jun 27, 2012, 3:36:54 PM (7 years ago)
Author:
sacerdot
Message:

More stuff moved around in proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r2121 r2122  
    235235  ∀b: BitVector n.
    236236    String.
     237
     238example 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.
     243qed.
     244
     245axiom 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  //
     255qed.
     256
     257axiom 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
     263axiom 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.