From dc4b11689131bdb41a43e5aca76538556a3a120c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 29 Nov 2023 15:45:27 +0100
Subject: Add support for more bitwise operations and update the extraction

---
 backends/coq/Primitives.v                 |  76 ++++++++++++++
 backends/fstar/Primitives.fst             | 167 ++++++++++++++++++++++++++++--
 backends/lean/Base/Primitives/Scalar.lean |  42 +++++++-
 3 files changed, 275 insertions(+), 10 deletions(-)

(limited to 'backends')

diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
index 83f860b6..99ffe070 100644
--- a/backends/coq/Primitives.v
+++ b/backends/coq/Primitives.v
@@ -255,6 +255,12 @@ Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty
   
 Definition scalar_neg {ty} (x: scalar ty) : result (scalar ty) := mk_scalar ty (-(to_Z x)).
 
+Axiom scalar_xor : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *)
+Axiom scalar_or : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *)
+Axiom scalar_and : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *)
+Axiom scalar_shl : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *)
+Axiom scalar_shr : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *)
+
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
 (* TODO: check the semantics of casts in Rust *)
 Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) :=
@@ -372,6 +378,76 @@ Definition u32_mul   := @scalar_mul U32.
 Definition u64_mul   := @scalar_mul U64.
 Definition u128_mul  := @scalar_mul U128.
 
+(** Xor *)
+Definition u8_xor := @scalar_xor U8.
+Definition u16_xor := @scalar_xor U16.
+Definition u32_xor := @scalar_xor U32.
+Definition u64_xor := @scalar_xor U64.
+Definition u128_xor := @scalar_xor U128.
+Definition usize_xor := @scalar_xor Usize.
+Definition i8_xor := @scalar_xor I8.
+Definition i16_xor := @scalar_xor I16.
+Definition i32_xor := @scalar_xor I32.
+Definition i64_xor := @scalar_xor I64.
+Definition i128_xor := @scalar_xor I128.
+Definition isize_xor := @scalar_xor Isize.
+
+(** Or *)
+Definition u8_or := @scalar_or U8.
+Definition u16_or := @scalar_or U16.
+Definition u32_or := @scalar_or U32.
+Definition u64_or := @scalar_or U64.
+Definition u128_or := @scalar_or U128.
+Definition usize_or := @scalar_or Usize.
+Definition i8_or := @scalar_or I8.
+Definition i16_or := @scalar_or I16.
+Definition i32_or := @scalar_or I32.
+Definition i64_or := @scalar_or I64.
+Definition i128_or := @scalar_or I128.
+Definition isize_or := @scalar_or Isize.
+
+(** And *)
+Definition u8_and := @scalar_and U8.
+Definition u16_and := @scalar_and U16.
+Definition u32_and := @scalar_and U32.
+Definition u64_and := @scalar_and U64.
+Definition u128_and := @scalar_and U128.
+Definition usize_and := @scalar_and Usize.
+Definition i8_and := @scalar_and I8.
+Definition i16_and := @scalar_and I16.
+Definition i32_and := @scalar_and I32.
+Definition i64_and := @scalar_and I64.
+Definition i128_and := @scalar_and I128.
+Definition isize_and := @scalar_and Isize.
+
+(** Shift left *)
+Definition u8_shl {ty} := @scalar_shl U8 ty.
+Definition u16_shl {ty} := @scalar_shl U16 ty.
+Definition u32_shl {ty} := @scalar_shl U32 ty.
+Definition u64_shl {ty} := @scalar_shl U64 ty.
+Definition u128_shl {ty} := @scalar_shl U128 ty.
+Definition usize_shl {ty} := @scalar_shl Usize ty.
+Definition i8_shl {ty} := @scalar_shl I8 ty.
+Definition i16_shl {ty} := @scalar_shl I16 ty.
+Definition i32_shl {ty} := @scalar_shl I32 ty.
+Definition i64_shl {ty} := @scalar_shl I64 ty.
+Definition i128_shl {ty} := @scalar_shl I128 ty.
+Definition isize_shl {ty} := @scalar_shl Isize ty.
+
+(** Shift right *)
+Definition u8_shr {ty} := @scalar_shr U8 ty.
+Definition u16_shr {ty} := @scalar_shr U16 ty.
+Definition u32_shr {ty} := @scalar_shr U32 ty.
+Definition u64_shr {ty} := @scalar_shr U64 ty.
+Definition u128_shr {ty} := @scalar_shr U128 ty.
+Definition usize_shr {ty} := @scalar_shr Usize ty.
+Definition i8_shr {ty} := @scalar_shr I8 ty.
+Definition i16_shr {ty} := @scalar_shr I16 ty.
+Definition i32_shr {ty} := @scalar_shr I32 ty.
+Definition i64_shr {ty} := @scalar_shr I64 ty.
+Definition i128_shr {ty} := @scalar_shr I128 ty.
+Definition isize_shr {ty} := @scalar_shr Isize ty.
+
 (** Small utility *)
 Definition usize_to_nat (x: usize) : nat := Z.to_nat (to_Z x).
 
diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
index 94322ead..dd340c00 100644
--- a/backends/fstar/Primitives.fst
+++ b/backends/fstar/Primitives.fst
@@ -65,6 +65,10 @@ type const_raw_ptr (t : Type0) = { v : t }
 (*** Scalars *)
 /// Rem.: most of the following code was partially generated
 
+assume val size_numbits : pos
+
+// TODO: we could use FStar.Int.int_t and FStar.UInt.int_t
+
 let isize_min : int = -9223372036854775808 // TODO: should be opaque
 let isize_max : int = 9223372036854775807 // TODO: should be opaque
 let i8_min : int = -128
@@ -108,7 +112,6 @@ let is_unsigned = function
   | Isize | I8 | I16 | I32 | I64 | I128 -> false
   | Usize | U8 | U16 | U32 | U64 | U128 -> true
 
-
 let scalar_min (ty : scalar_ty) : int =
   match ty with
   | Isize -> isize_min
@@ -171,7 +174,7 @@ let scalar_sub (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
 let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scalar ty) =
   mk_scalar ty (x * y)
 
-let scalar_lxor (#ty : scalar_ty { is_unsigned ty && ty <> Usize })
+let scalar_xor (#ty : scalar_ty)
     (x : scalar ty) (y : scalar ty) : scalar ty =
   match ty with
   | U8 -> FStar.UInt.logxor #8 x y
@@ -179,6 +182,91 @@ let scalar_lxor (#ty : scalar_ty { is_unsigned ty && ty <> Usize })
   | U32 -> FStar.UInt.logxor #32 x y
   | U64 -> FStar.UInt.logxor #64 x y
   | U128 -> FStar.UInt.logxor #128 x y
+  | Usize -> admit() // TODO
+  | I8 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 8);
+    normalize_spec (scalar I8);
+    FStar.Int.logxor #8 x y
+  | I16 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 16);
+    normalize_spec (scalar I16);
+    FStar.Int.logxor #16 x y
+  | I32 -> FStar.Int.logxor #32 x y
+  | I64 -> FStar.Int.logxor #64 x y
+  | I128 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 128);
+    normalize_spec (scalar I128);
+    FStar.Int.logxor #128 x y
+  | Isize -> admit() // TODO
+
+let scalar_or (#ty : scalar_ty)
+    (x : scalar ty) (y : scalar ty) : scalar ty =
+  match ty with
+  | U8 -> FStar.UInt.logor #8 x y
+  | U16 -> FStar.UInt.logor #16 x y
+  | U32 -> FStar.UInt.logor #32 x y
+  | U64 -> FStar.UInt.logor #64 x y
+  | U128 -> FStar.UInt.logor #128 x y
+  | Usize -> admit() // TODO
+  | I8 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 8);
+    normalize_spec (scalar I8);
+    FStar.Int.logor #8 x y
+  | I16 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 16);
+    normalize_spec (scalar I16);
+    FStar.Int.logor #16 x y
+  | I32 -> FStar.Int.logor #32 x y
+  | I64 -> FStar.Int.logor #64 x y
+  | I128 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 128);
+    normalize_spec (scalar I128);
+    FStar.Int.logor #128 x y
+  | Isize -> admit() // TODO
+
+let scalar_and (#ty : scalar_ty)
+    (x : scalar ty) (y : scalar ty) : scalar ty =
+  match ty with
+  | U8 -> FStar.UInt.logand #8 x y
+  | U16 -> FStar.UInt.logand #16 x y
+  | U32 -> FStar.UInt.logand #32 x y
+  | U64 -> FStar.UInt.logand #64 x y
+  | U128 -> FStar.UInt.logand #128 x y
+  | Usize -> admit() // TODO
+  | I8 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 8);
+    normalize_spec (scalar I8);
+    FStar.Int.logand #8 x y
+  | I16 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 16);
+    normalize_spec (scalar I16);
+    FStar.Int.logand #16 x y
+  | I32 -> FStar.Int.logand #32 x y
+  | I64 -> FStar.Int.logand #64 x y
+  | I128 ->
+    // Encoding issues...
+    normalize_spec (FStar.Int.int_t 128);
+    normalize_spec (scalar I128);
+    FStar.Int.logand #128 x y
+  | Isize -> admit() // TODO
+
+// Shift left
+let scalar_shl (#ty0 #ty1 : scalar_ty)
+    (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
+  admit()
+
+// Shift right
+let scalar_shr (#ty0 #ty1 : scalar_ty)
+    (x : scalar ty0) (y : scalar ty1) : result (scalar ty0) =
+  admit()
 
 (** Cast an integer from a [src_ty] to a [tgt_ty] *)
 // TODO: check the semantics of casts in Rust
@@ -304,12 +392,75 @@ let u32_mul = scalar_mul #U32
 let u64_mul = scalar_mul #U64
 let u128_mul = scalar_mul #U128
 
-/// Logical operators, defined for unsigned types only, so far
-let u8_xor = scalar_lxor #U8
-let u16_xor = scalar_lxor #U16
-let u32_xor = scalar_lxor #U32
-let u64_xor = scalar_lxor #U64
-let u128_xor = scalar_lxor #U128
+/// Xor
+let u8_xor = scalar_xor #U8
+let u16_xor = scalar_xor #U16
+let u32_xor = scalar_xor #U32
+let u64_xor = scalar_xor #U64
+let u128_xor = scalar_xor #U128
+let usize_xor = scalar_xor #Usize
+let i8_xor = scalar_xor #I8
+let i16_xor = scalar_xor #I16
+let i32_xor = scalar_xor #I32
+let i64_xor = scalar_xor #I64
+let i128_xor = scalar_xor #I128
+let isize_xor = scalar_xor #Isize
+
+/// Or
+let u8_or = scalar_or #U8
+let u16_or = scalar_or #U16
+let u32_or = scalar_or #U32
+let u64_or = scalar_or #U64
+let u128_or = scalar_or #U128
+let usize_or = scalar_or #Usize
+let i8_or = scalar_or #I8
+let i16_or = scalar_or #I16
+let i32_or = scalar_or #I32
+let i64_or = scalar_or #I64
+let i128_or = scalar_or #I128
+let isize_or = scalar_or #Isize
+
+/// And
+let u8_and = scalar_and #U8
+let u16_and = scalar_and #U16
+let u32_and = scalar_and #U32
+let u64_and = scalar_and #U64
+let u128_and = scalar_and #U128
+let usize_and = scalar_and #Usize
+let i8_and = scalar_and #I8
+let i16_and = scalar_and #I16
+let i32_and = scalar_and #I32
+let i64_and = scalar_and #I64
+let i128_and = scalar_and #I128
+let isize_and = scalar_and #Isize
+
+/// Shift left
+let u8_shl #ty = scalar_shl #U8 #ty
+let u16_shl #ty = scalar_shl #U16 #ty
+let u32_shl #ty = scalar_shl #U32 #ty
+let u64_shl #ty = scalar_shl #U64 #ty
+let u128_shl #ty = scalar_shl #U128 #ty
+let usize_shl #ty = scalar_shl #Usize #ty
+let i8_shl #ty = scalar_shl #I8 #ty
+let i16_shl #ty = scalar_shl #I16 #ty
+let i32_shl #ty = scalar_shl #I32 #ty
+let i64_shl #ty = scalar_shl #I64 #ty
+let i128_shl #ty = scalar_shl #I128 #ty
+let isize_shl #ty = scalar_shl #Isize #ty
+
+/// Shift right
+let u8_shr #ty = scalar_shr #U8 #ty
+let u16_shr #ty = scalar_shr #U16 #ty
+let u32_shr #ty = scalar_shr #U32 #ty
+let u64_shr #ty = scalar_shr #U64 #ty
+let u128_shr #ty = scalar_shr #U128 #ty
+let usize_shr #ty = scalar_shr #Usize #ty
+let i8_shr #ty = scalar_shr #I8 #ty
+let i16_shr #ty = scalar_shr #I16 #ty
+let i32_shr #ty = scalar_shr #I32 #ty
+let i64_shr #ty = scalar_shr #I64 #ty
+let i128_shr #ty = scalar_shr #I128 #ty
+let isize_shr #ty = scalar_shr #Isize #ty
 
 (*** core::ops *)
 
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index ec9665a5..cdd6d6f9 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -386,10 +386,28 @@ def Scalar.sub {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar
 def Scalar.mul {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Result (Scalar ty) :=
   Scalar.tryMk ty (x.val * y.val)
 
--- TODO: instances of +, -, * etc. for scalars
+-- TODO: shift left
+def Scalar.shiftl {ty0 ty1 : ScalarTy} (x : Scalar ty0) (y : Scalar ty1) : Result (Scalar ty0) :=
+  sorry
+
+-- TODO: shift right
+def Scalar.shiftr {ty0 ty1 : ScalarTy} (x : Scalar ty0) (y : Scalar ty1) : Result (Scalar ty0) :=
+  sorry
+
+-- TODO: xor
+def Scalar.xor {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty :=
+  sorry
+
+-- TODO: and
+def Scalar.and {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty :=
+  sorry
+
+-- TODO: or
+def Scalar.or {ty : ScalarTy} (x : Scalar ty) (y : Scalar ty) : Scalar ty :=
+  sorry
 
 -- Cast an integer from a [src_ty] to a [tgt_ty]
--- TODO: check the semantics of casts in Rust
+-- TODO: double-check the semantics of casts in Rust
 def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Result (Scalar tgt_ty) :=
   Scalar.tryMk tgt_ty x.val
 
@@ -486,6 +504,26 @@ instance {ty} : HDiv (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
 instance {ty} : HMod (Scalar ty) (Scalar ty) (Result (Scalar ty)) where
   hMod x y := Scalar.rem x y
 
+-- Shift left
+instance {ty0 ty1} : HShiftLeft (Scalar ty0) (Scalar ty1) (Result (Scalar ty0)) where
+  hShiftLeft x y := Scalar.shiftl x y
+
+-- Shift right
+instance {ty0 ty1} : HShiftRight (Scalar ty0) (Scalar ty1) (Result (Scalar ty0)) where
+  hShiftRight x y := Scalar.shiftr x y
+
+-- Xor
+instance {ty} : HXor (Scalar ty) (Scalar ty) (Scalar ty) where
+  hXor x y := Scalar.xor x y
+
+-- Or
+instance {ty} : HOr (Scalar ty) (Scalar ty) (Scalar ty) where
+  hOr x y := Scalar.or x y
+
+-- And
+instance {ty} : HAnd (Scalar ty) (Scalar ty) (Scalar ty) where
+  hAnd x y := Scalar.and x y
+
 -- Generic theorem - shouldn't be used much
 @[cpspec]
 theorem Scalar.add_spec {ty} {x y : Scalar ty}
-- 
cgit v1.2.3