Provide implementations for remaining bitvector primitives.

saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v

@@ -18,6 +18,7 @@ From mathcomp Require Import fintype.
 From mathcomp Require Import tuple.
 
 From Coq Require Export ZArith.BinIntDef.
+From Coq Require Export PArith.BinPos.
 
 Import VectorNotations.
 
@@ -224,6 +225,7 @@ Definition sbvToInt (n : Nat) (b : bitvector n) : Z
 (* Useful notation for bools *)
 Definition boolToInt (b : bool) : Z := if b then 1%Z else 0%Z.
 Numeral Notation bool Z.odd boolToInt : bool_scope.
+Close Scope bool_scope. (* no, don't interpret all numbers as booleans... *)
 
 (* This is annoying to implement, so using BITS conversion *)
 Definition bvAdd (n : nat) (a : bitvector n) (b : bitvector n)
@@ -248,79 +250,82 @@ Definition bvNeg (n : nat) (a : bitvector n)
   : bitvector n
   := bvSub n (intToBv n 0) a.
 
-(* FIXME this is not implemented *)
 Definition bvUDiv (n : nat) (a : bitvector n) (b : bitvector n)
   : bitvector n
-  := a.
+  := intToBv n (Z.div (bvToInt n a) (bvToInt n b)).
 Global Opaque bvUDiv.
 
-(* FIXME this is not implemented *)
 Definition bvURem (n : nat) (a : bitvector n) (b : bitvector n)
   : bitvector n
-  := a.
+  := intToBv n (Z.modulo (bvToInt n a) (bvToInt n b)).
 Global Opaque bvURem.
 
-(* FIXME this is not implemented *)
-Definition bvSDiv (n : nat) (a : bitvector n.+1) (b : bitvector n.+1)
+Definition  bvSDiv (n : nat) (a : bitvector n.+1) (b : bitvector n.+1)
   : bitvector n.+1
-  := a.
+  := intToBv (n.+1) (Z.quot (sbvToInt (n.+1) a) (sbvToInt (n.+1) b)).
 Global Opaque bvSDiv.
 
-(* FIXME this is not implemented *)
 Definition bvSRem (n : nat) (a : bitvector n.+1) (b : bitvector n.+1)
   : bitvector n.+1
-  := a.
+  := intToBv (n.+1) (Z.rem (sbvToInt (n.+1) a) (sbvToInt (n.+1) b)).
 Global Opaque bvSRem.
 
-(* FIXME this is not implemented (base 2 logarithm) *)
+Section log2_up.
+  (* TODO, really should prove something about this *)
+  Definition log2_up z : Z :=
+  match z with
+  | Z.pos 1 => 0
+  | Z.pos p => Z.add (Z.log2 (Z.pos (Pos.pred p))) 1
+  | _ => 0
+  end.
+End log2_up.
+
 Definition bvLg2 (n : nat) (a : bitvector n)
   : bitvector n
-  := a.
+  := intToBv n (log2_up (bvToInt n a)).
 Global Opaque bvLg2.
 
-(* FIXME this is not implemented *)
 Definition bvSShr (w : nat) (a : bitvector w.+1) (n : nat)
   : bitvector w.+1
-  := a.
+  := bitsToBv (iter n sarB (bvToBITS a)).
 Global Opaque bvSShr.
 
-(* FIXME this is not implemented *)
 Definition bvShl (w : nat) (a : bitvector w) (n : nat)
   : bitvector w
-  := a.
+  := bitsToBv (shlBn (bvToBITS a) n).
 Global Opaque bvShl.
 
-(* FIXME this is not implemented *)
 Definition bvShr (w : nat) (a : bitvector w) (n : nat)
   : bitvector w
-  := a.
+  := bitsToBv (shrBn (bvToBITS a) n).
 Global Opaque bvShr.
 
-(* FIXME this is not implemented *)
-Definition rotateL (n : nat) (A : Type) (v : Vector.t A n) (i : nat)
-  : Vector.t A n
-  := v.
-Global Opaque rotateL.
-
-(* FIXME this is not implemented *)
-Definition rotateR (n : nat) (A : Type) (v : Vector.t A n) (i : nat)
-  : Vector.t A n
-  := v.
-Global Opaque rotateR.
-
-Fixpoint shiftL (n : nat) (A : Type) (x : A) (v : Vector.t A n) (i : nat)
-  : Vector.t A n
-  := match i with
-     | O => v
-     | S i' => Vector.tl (Vector.shiftin x (shiftL n A x v i'))
-     end.
 
-Fixpoint shiftR (n : nat) (A : Type) (x : A) (v : Vector.t A n) (i : nat)
-  : Vector.t A n
-  := match i with
-     | O => v
-     | S i' => Vector.shiftout (cons _ x _ (shiftR n A x v i'))
-     end.
+(* left shift by one element, shifting in the value of x on the right *)
+Definition shiftL1 (n:nat) (A:Type) (x:A) (v : Vector.t A n) :=
+  Vector.tl (Vector.shiftin x v).
+
+(* right shift by one element, shifting in the value of x on the left *)
+Definition shiftR1 (n:nat) (A:Type) (x:A) (v : Vector.t A n) :=
+  Vector.shiftout (cons _ x _ v).
+
+Definition rotateL (n : nat) : forall (A : Type) (v : Vector.t A n) (i : nat), Vector.t A n :=
+  match n with
+  | O => fun A v i => v
+  | S n' => fun A v i => iter i (fun v' => shiftL1 (S n') A (Vector.hd v') v') v
+  end.
+
+Definition rotateR (n : nat) : forall (A : Type) (v : Vector.t A n) (i : nat), Vector.t A n :=
+  match n with
+  | O => fun A v i => v
+  | S n' => fun A v i => iter i (fun v' => shiftR1 (S n') A (Vector.last v') v') v
+  end.
+
+Definition shiftL (n : nat) (A : Type) (x : A) (v : Vector.t A n) (i : nat) : Vector.t A n :=
+  iter i (shiftL1 n A x) v.
+
+Definition shiftR (n : nat) (A : Type) (x : A) (v : Vector.t A n) (i : nat) : Vector.t A n :=
+  iter i (shiftR1 n A x) v.
 
 (* This is annoying to implement, so using BITS conversion *)
 Definition bvult (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
@@ -346,15 +351,15 @@ Definition sign {n : nat} (a : bitvector n) : Bool :=
 
 Definition bvslt (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
   let c := bvSub n a b
-   in (sign a && ~~ sign b) || (sign a && sign c) || (~~ sign b && sign c).
+   in ((sign a && ~~ sign b) || (sign a && sign c) || (~~ sign b && sign c))%bool.
       (* ^ equivalent to: boolEq (bvSBorrow s a b) (sign (bvSub n a b))  *)
 Global Opaque bvslt.
 
 Definition bvsgt (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
   bvslt n b a.
 
 Definition bvsle (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=
-  bvslt n a b || (Vector.eqb _ eqb a b).
+  (bvslt n a b || (Vector.eqb _ eqb a b))%bool.
 Global Opaque bvsle.
 
 Definition bvsge (n : nat) (a : bitvector n) (b : bitvector n) : Bool :=