feat: add more raw bitvector functions

src/smtencoding/FStar.SMTEncoding.Term.fst

@@ -204,6 +204,7 @@ let op_to_string = function
   | BvSub -> "bvsub"
   | BvShl -> "bvshl"
   | BvShr -> "bvlshr"
+  | BvAShr -> "bvashr"
   | BvUdiv -> "bvudiv"
   | BvMod -> "bvurem"
   | BvMul -> "bvmul"
@@ -308,6 +309,7 @@ let mkBvAdd = mk_bin_op BvAdd
 let mkBvSub = mk_bin_op BvSub
 let mkBvShl sz (t1, t2) r = mkApp'(BvShl, [t1;(mkNatToBv sz t2 r)]) r
 let mkBvShr sz (t1, t2) r = mkApp'(BvShr, [t1;(mkNatToBv sz t2 r)]) r
+let mkBvAshr sz (t1, t2) r = mkApp'(BvAshr, [t1;(mkNatToBv sz t2 r)]) r
 let mkBvUdiv sz (t1, t2) r = mkApp'(BvUdiv, [t1;(mkNatToBv sz t2 r)]) r
 let mkBvMod sz (t1, t2) r = mkApp'(BvMod, [t1;(mkNatToBv sz t2 r)]) r
 let mkBvMul sz (t1, t2) r = mkApp' (BvMul, [t1;(mkNatToBv sz t2 r)]) r
@@ -384,6 +386,7 @@ let check_pattern_ok (t:term) : option term =
                 | BvSub
                 | BvShl
                 | BvShr
+                | BvAShr
                 | BvUdiv
                 | BvMod
                 | BvMul

src/smtencoding/FStar.SMTEncoding.Term.fsti

@@ -60,7 +60,8 @@ type op =
   | BvAdd
   | BvSub
   | BvShl
-  | BvShr
+  | BvShr (* logical shift right *)
+  | BvAshr (* arithmetic shift right *)
   | BvUdiv
   | BvMod
   | BvMul
@@ -246,6 +247,7 @@ val mkBvUlt   : ((term * term) -> Range.range -> term)
 val mkBvUext  : (int -> term -> Range.range -> term)
 val mkBvShl   : (int -> (term * term) -> Range.range -> term)
 val mkBvShr   : (int -> (term * term) -> Range.range -> term)
+val mkBvAshr  : (int -> (term * term) -> Range.range -> term)
 val mkBvUdiv  : (int -> (term * term) -> Range.range -> term)
 val mkBvMod   : (int -> (term * term) -> Range.range -> term)
 val mkBvMul   : (int -> (term * term) -> Range.range -> term)

ulib/FStar.BV.fst

@@ -58,10 +58,28 @@ let bvshl = B.shift_left_vec
 let int2bv_shl #n #x #y #z pf =
   inverse_vec_lemma #n (bvshl #n (int2bv #n x) y)
 
+
+let bvshl_unsafe #n a b = bvshl #n a (bv2int #n b)
+let bvshl_unsafe_sound #n #a #b  = ()
+
 let bvshr = B.shift_right_vec
+
+
+let bvshr_unsafe #n a b = bvshr #n a (bv2int #n b)
+let bvshr_unsafe_sound #n #a #b  = ()
+
 let int2bv_shr #n #x #y #z pf =
   inverse_vec_lemma #n (bvshr #n (int2bv #n x) y)
 
+let bvashr = B.shift_arithmetic_right_vec
+
+let bvashr_unsafe #n a b = bvashr #n a (bv2int #n b)
+
+let bvashr_unsafe_sound #n #a #b = ()
+
+let int2bv_ashr #n #x #y #z pf =
+  inverse_vec_lemma #n (bvashr #n (int2bv #n x) y)
+
 
 
 let bvult #n a b = (bv2int #n a) < (bv2int #n b)
@@ -96,6 +114,11 @@ let bvdiv_unsafe_sound #n #a #b b_nonzero_pf = ()
 
 let bvmod #n a b =
     int2bv #n (U.mod #n (bv2int #n a) b)
+
+let bvmod_unsafe #n a b = if (bv2int b <> 0) then bvmod a (bv2int b) else a
+let bvmod_unsafe_sound #n #a #b b_nonzero_pf = ()
+let bvmod_unsafe_sound_nonzero #n #a #b pf = ()
+
 let int2bv_mod #n #x #y #z pf =
   inverse_vec_lemma #n (bvmod #n (int2bv #n x) y)
 

ulib/FStar.BV.fsti

@@ -140,9 +140,19 @@ val int2bv_shl:
     squash (bvshl #n (int2bv #n x) y == z)
   -> Lemma (int2bv #n (shift_left #n x y) == z)
 
-(** Bitwise shift right *)
+val bvshl_unsafe (#n: pos) (a b : bv_t n) : Tot (bv_t n)
+
+(** Bitwise shift (logical) right *)
 val bvshr (#n: pos) (a: bv_t n) (s: nat) : Tot (bv_t n)
 
+val bvshr_unsafe (#n: pos) (a b : bv_t n) : Tot (bv_t n)
+
+val bvshr_unsafe_sound :
+    #n: pos ->
+    #a : bv_t n ->
+    #b : bv_t n
+  -> Lemma (bvshr_unsafe #n a b = bvshr #n a (bv2int #n b))
+
 val int2bv_shr:
     #n: pos ->
     #x: uint_t n ->
@@ -151,6 +161,25 @@ val int2bv_shr:
     squash (bvshr #n (int2bv #n x) y == z)
   -> Lemma (int2bv #n (shift_right #n x y) == z)
 
+(** Bitwise shift (arithmetic) right *)
+val bvashr (#n: pos) (a: bv_t n) (s: nat) : Tot (bv_t n)
+
+val bvashr_unsafe (#n: pos) (a b : bv_t n) : Tot (bv_t n)
+
+val bvashr_unsafe_sound :
+    #n: pos ->
+    #a : bv_t n ->
+    #b : bv_t n
+  -> Lemma (bvashr_unsafe #n a b = bvashr #n a (bv2int #n b))
+
+val int2bv_ashr:
+    #n: pos ->
+    #x: uint_t n ->
+    #y: uint_t n ->
+    #z: bv_t n ->
+    squash (bvashr #n (int2bv #n x) y == z)
+  -> Lemma (int2bv #n (shift_arithmetic_right #n x y) == z)
+
 (**** Arithmetic operations *)
 unfold
 let bv_zero #n = int2bv #n 0
@@ -216,6 +245,15 @@ val bvdiv_unsafe_sound :
 (** Modulus *)
 val bvmod (#n: pos) (a: bv_t n) (b: uint_t n {b <> 0}) : Tot (bv_t n)
 
+val bvmod_unsafe (#n: pos) (a b: bv_t n) : Tot (bv_t n)
+
+val bvmod_unsafe_sound_nonzero :
+    #n: pos ->
+    #a : bv_t n ->
+    #b : bv_t n ->
+    squash (bv2int b <> 0)
+  -> Lemma (bvmod_unsafe #n a b = bvmod a (bv2int b))
+
 val int2bv_mod:
     #n: pos ->
     #x: uint_t n ->
@@ -234,4 +272,3 @@ val int2bv_mul:
     #z: bv_t n ->
     squash (bvmul #n (int2bv #n x) y == z)
   -> Lemma (int2bv #n (mul_mod #n x y) == z)
-

ulib/FStar.UInt.fsti

@@ -450,6 +450,9 @@ let shift_left (#n:pos) (a:uint_t n) (s:nat) : Tot (uint_t n) =
 let shift_right (#n:pos) (a:uint_t n) (s:nat) : Tot (uint_t n) =
   from_vec (shift_right_vec #n (to_vec #n a) s)
 
+let shift_arithmetic_right (#n:pos) (a:uint_t n) (s:nat) : Tot (uint_t n) =
+  from_vec (shift_arithmetic_right_vec #n (to_vec #n a) s)
+
 (* Shift operators lemmas *)
 val shift_left_lemma_1: #n:pos -> a:uint_t n -> s:nat -> i:nat{i < n && i >= n - s} ->
   Lemma (requires True)