Changeset 2122 for src/ASM/BitVector.ma

Timestamp:

Jun 27, 2012, 3:36:54 PM (9 years ago)

Author:

sacerdot

Message:

More stuff moved around in proper places

File:

• src/ASM/BitVector.ma (modified) (1 diff)

src/ASM/BitVector.ma

@@ -235 +235 @@
   ∀b: BitVector n.
     String.
+
+example sub_minus_one_seven_eight:
+  ∀v: BitVector 7.
+  false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
+  \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
+ cases daemon.
+qed.
+
+axiom sub16_with_carry_overflow:
+  ∀left, right, result: BitVector 16.
+  ∀flags: BitVector 3.
+  ∀upper: BitVector 9.
+  ∀lower: BitVector 7.
+    sub_16_with_carry left right false = 〈result, flags〉 →
+      vsplit bool 9 7 result = 〈upper, lower〉 →
+        get_index_v bool 3 flags 2 ? = true →
+          upper = [[true; true; true; true; true; true; true; true; true]].
+  //
+qed.
+
+axiom sub_16_to_add_16_8_0:
+ ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
+  get_index' ? 2 0 flags = false →
+  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
+   v1 = add ? v2 (sign_extension (false:::v3)).
+
+axiom sub_16_to_add_16_8_1:
+ ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
+  get_index' ? 2 0 flags = true →
+  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
+   v1 = add ? v2 (sign_extension (true:::v3)).