Changeset 697 for src/ASM/Arithmetic.ma

Timestamp:

Mar 18, 2011, 1:28:33 PM (9 years ago)

Author:

campbell

Message:

Merge Clight branch of vectors and friends.
Start making stuff build.

Location:

src/ASM

Files:

• . (modified) (1 prop)
• Arithmetic.ma (modified) (7 diffs)

src/ASM/Arithmetic.ma

@@ -8 +8 @@
       | true ⇒ S O
       ].
+
+definition carry_of : bool → bool → bool → bool ≝
+λa,b,c. match a with [ false ⇒ b ∧ c | true ⇒ b ∨ c ].
+
+definition add_with_carries : ∀n:nat. BitVector n → BitVector n → bool →
+                                      BitVector n × (BitVector n) ≝
+  λn,x,y,init_carry.
+  fold_right2_i ???
+   (λn,b,c,r.
+     let 〈lower_bits, carries〉 ≝ r in
+     let last_carry ≝ match carries with [ VEmpty ⇒ init_carry | VCons _ cy _ ⇒ cy ] in
+     let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_carry in
+     let carry ≝ carry_of b c last_carry in
+       〈bit:::lower_bits, carry:::carries〉
+   )
+   〈[[ ]], [[ ]]〉 n x y.
+
+(* Essentially the only difference for subtraction. *)
+definition borrow_of : bool → bool → bool → bool ≝
+λa,b,c. match a with [ false ⇒ b ∨ c | true ⇒ b ∧ c ].
+
+definition sub_with_borrows : ∀n:nat. BitVector n → BitVector n → bool →
+                                      BitVector n × (BitVector n) ≝
+  λn,x,y,init_borrow.
+  fold_right2_i ???
+   (λn,b,c,r.
+     let 〈lower_bits, borrows〉 ≝ r in
+     let last_borrow ≝ match borrows with [ VEmpty ⇒ init_borrow | VCons _ bw _ ⇒ bw ] in
+     let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_borrow in
+     let borrow ≝ borrow_of b c last_borrow in
+       〈bit:::lower_bits, borrow:::borrows〉
+   )
+   〈[[ ]], [[ ]]〉 n x y.
     
 definition add_n_with_carry:
-      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
+      ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. n ≥ 5 →
+      (BitVector n) × (BitVector 3) ≝
   λn: nat.
   λb: BitVector n.
   λc: BitVector n.
   λcarry: bool.
-    let b_as_nat ≝ nat_of_bitvector n b in
-    let c_as_nat ≝ nat_of_bitvector n c in
-    let carry_as_nat ≝ nat_of_bool carry in
-    let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in
-    let ac_flag ≝ geb ((modulus b_as_nat (2 * n)) +
-                  (modulus c_as_nat (2 * n)) +
-                  c_as_nat) (2 * n) in
-    let bit_xxx ≝ geb ((modulus b_as_nat (2^(n - 1))) +
-                  (modulus c_as_nat (2^(n - 1))) +
-                  c_as_nat) (2^(n - 1)) in
-    let result ≝ modulus result_old (2^n) in
-    let cy_flag ≝ geb result_old (2^n) in
-    let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in
-      mk_pair ? ? (bitvector_of_nat n result)
-                       ([[ cy_flag ; ac_flag ; ov_flag ]]).
-
-definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝
+  λpf:n ≥ 5.
+  
+    let 〈result, carries〉 ≝ add_with_carries n b c carry in
+    let cy_flag ≝ get_index_v ?? carries 0 ? in
+    let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
+    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
+      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
+// @(transitive_le  … pf) /2/
+qed.
+
+definition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. n ≥ 5 →
+                                            (BitVector n) × (BitVector 3) ≝
   λn: nat.
   λb: BitVector n.
   λc: BitVector n.
   λcarry: bool.
-     let b_as_nat ≝ nat_of_bitvector n b in
-     let c_as_nat ≝ nat_of_bitvector n c in
-     let carry_as_nat ≝ nat_of_bool carry in
-     let temporary ≝ (b_as_nat mod (2 * n)) - (c_as_nat mod (2 * n)) in
-     let ac_flag ≝ ltb (b_as_nat mod (2 * n)) ((c_as_nat mod (2 * n)) + carry_as_nat) in
-     let bit_six ≝ ltb (b_as_nat mod (2^(n - 1))) ((c_as_nat mod (2^(n - 1))) + carry_as_nat) in
-     let 〈b',cy_flag〉 ≝
-       if geb b_as_nat (c_as_nat + carry_as_nat) then
-         〈b_as_nat, false〉
-       else
-         〈b_as_nat + (2^n), true〉
-     in
-       let ov_flag ≝ exclusive_disjunction cy_flag bit_six in
-         〈bitvector_of_nat n ((b' - c_as_nat) - carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉.         
-         
+  λpf:n ≥ 5.
+  
+    let 〈result, carries〉 ≝ sub_with_borrows n b c carry in
+    let cy_flag ≝ get_index_v ?? carries 0 ? in
+    let ov_flag ≝ exclusive_disjunction cy_flag (get_index_v ?? carries 1 ?) in
+    let ac_flag ≝ get_index_v ?? carries 4 ? in (* I'd prefer n/2, but this is easier *)
+      〈result, [[ cy_flag; ac_flag; ov_flag ]]〉.
+// @(transitive_le  … pf) /2/
+qed.
+
 definition add_8_with_carry ≝ add_n_with_carry 8.
 definition add_16_with_carry ≝ add_n_with_carry 16.
@@ -59 +83 @@
   λn: nat.
   λb: BitVector n.
-    let b_as_nat ≝ (nat_of_bitvector n b) + 1 in
-    let overflow ≝ geb b_as_nat 2^n in
-      match overflow with
-        [ false ⇒ bitvector_of_nat n b_as_nat
-        | true ⇒ zero n
-        ].
+    \fst (add_with_carries n b (zero n) true).
         
 definition decrement ≝
   λn: nat.
   λb: BitVector n.
-    let b_as_nat ≝ nat_of_bitvector n b in
-      match b_as_nat with
-        [ O ⇒ maximum n
-        | S o ⇒ bitvector_of_nat n o
-        ].
+    \fst (sub_with_borrows n b (zero n) true).
     
 definition two_complement_negation ≝
@@ -84 +99 @@
   λn: nat.
   λb, c: BitVector n.
-    let 〈res,flags〉 ≝ add_n_with_carry n b c false in
+    let 〈res,flags〉 ≝ add_with_carries n b c false in
       res.
     
@@ -111 +126 @@
         Some ? (bitvector_of_nat n result)
     ].
-    
-alias id "option1" = "cic:/matita/basics/sums/option.ind(1,0,1)".
-      
-definition division_s: ∀n. ∀b, c: BitVector n. option1 (BitVector n) ≝
+      
+definition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝
   λn.
     match n with
@@ -156 +169 @@
     let b_nat ≝ nat_of_bitvector ? b in
     let c_nat ≝ nat_of_bitvector ? c in
-    let result ≝ modulus b_nat c_nat in
-      bitvector_of_nat (n + n) result.
+    match c_nat with
+    [ O ⇒ None ?
+    | _ ⇒ 
+      let result ≝ modulus b_nat c_nat in
+      Some ? (bitvector_of_nat n result)
+    ].
             
 definition modulus_s ≝
@@ -170 +187 @@
       
 definition lt_u ≝
-  λn.
-  λb, c: BitVector n.
-    let b_nat ≝ nat_of_bitvector ? b in
-    let c_nat ≝ nat_of_bitvector ? c in
-      ltb b_nat c_nat.
+  fold_right2_i ??? 
+    (λ_.λa,b,r.
+      match a with
+      [ true ⇒ b ∧ r
+      | false ⇒ b ∨ r
+      ])
+    false.
       
 definition gt_u ≝ λn, b, c. lt_u n c b.
@@ -181 +200 @@
 
 definition gte_u ≝ λn, b, c. ¬(lt_u n b c).
-      
+
 definition lt_s ≝
   λn.
   λb, c: BitVector n.
-    let 〈result, flags〉 ≝ sub_n_with_carry n b c false in
-    let ov_flag ≝ get_index_v ? ? flags 2 ? in
-     if ov_flag then
-       true
-     else
-       ((match n return λn'.BitVector n' → bool with
-       [ O ⇒ λ_.false
-       | S o ⇒ 
-         λresult'.(get_index_v ? ? result' O ?)
-       ]) result).
-  //
-qed.
-
+    let 〈result, borrows〉 ≝ sub_with_borrows n b c false in
+    match borrows with
+    [ VEmpty ⇒ false
+    | VCons _ bwn tl ⇒
+      match tl with
+      [ VEmpty ⇒ false
+      | VCons _ bwpn _ ⇒
+        if exclusive_disjunction bwn bwpn then 
+          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
+        else
+          match result with [ VEmpty ⇒ false | VCons _ b7 _ ⇒ b7 ]
+      ]
+    ].
+    
 definition gt_s ≝ λn,b,c. lt_s n c b.