Coq: switch to computable versions of BBV shifts

2 files changed, 5 insertions, 5 deletions

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index cca52c1d..9b5888c7 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -396,9 +396,9 @@ val arith_shiftr : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val rotl         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a
 val rotr         : forall 'a. Size 'a => mword 'a -> integer -> mword 'a*)
 (* TODO: check/redefine behaviour on out-of-range n *)
-Definition shiftl       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wlshift w (Z.to_nat n)) v.
-Definition shiftr       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshift w (Z.to_nat n)) v.
-Definition arith_shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshifta w (Z.to_nat n)) v.
+Definition shiftl       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wlshift' w (Z.to_nat n)) v.
+Definition shiftr       {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshift' w (Z.to_nat n)) v.
+Definition arith_shiftr {a} (v : mword a) n : mword a := with_word (P := id) (fun w => Word.wrshifta' w (Z.to_nat n)) v.
 (*
 Definition rotl         := rotl_bv
 Definition rotr         := rotr_bv
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 04fc3413..99f67d19 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -907,7 +907,7 @@ Parameter undefined_bit : bool.
 Definition getBit {n} :=
 match n with
 | O => fun (w : word O) i => undefined_bit
-| S n => fun (w : word (S n)) i => wlsb (wrshift w i)
+| S n => fun (w : word (S n)) i => wlsb (wrshift' w i)
 end.
 
 Definition access_mword_dec {m} (w : mword m) n := bitU_of_bool (getBit (get_word w) (Z.to_nat n)).
@@ -925,7 +925,7 @@ Definition setBit {n} :=
 match n with
 | O => fun (w : word O) i b => w
 | S n => fun (w : word (S n)) i (b : bool) =>
-  let bit : word (S n) := wlshift (natToWord _ 1) i in
+  let bit : word (S n) := wlshift' (natToWord _ 1) i in
   let mask : word (S n) := wnot bit in
   let masked := wand mask w in
   if b then masked else wor masked bit