Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Provide implementations for remaining bitvector primitives #1497

Merged
merged 1 commit into from
Nov 9, 2021
Merged

Provide implementations for remaining bitvector primitives #1497

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
91 changes: 48 additions & 43 deletions saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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)
Expand All @@ -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 :=
Expand All @@ -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 :=
Expand Down