Move Lem shl_int, shr_int implementations from aarch64_extras to sail lib

(note that they're already declared in lib/arith.sail)

1 files changed, 6 insertions, 0 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index a89456b9..cb2c3379 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -45,6 +45,12 @@ let negate_real r = realNegate r
 let abs_real r = realAbs r
 let power_real b e = realPowInteger b e*)
 
+val shr_int : ii -> ii -> ii
+let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
+
+val shl_int : integer -> integer -> integer
+let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
+
 let inline or_bool l r = (l || r)
 let inline and_bool l r = (l && r)
 let inline xor_bool l r = xor l r