Lean: annotate sail_arith_shiftright and _builtin_mod_nat

Author: javra

lib/mono_rewrites.sail

@@ -237,7 +237,8 @@ val _builtin_mod_nat = pure {
   ocaml: "modulus",
   lem: "integerMod",
   c: "tmod_int",
-  coq: "Z.rem"
+  coq: "Z.rem",
+  lean: "Nat.mod"
 } : forall 'n 'm, 'n >= 0 & 'm >= 0. (int('n), int('m)) -> {'r, 0 <= 'r < 'm. int('r)}
 
 /* Below we need the fact that 2 ^ 'n >= 0, so we axiomatise it in the return

lib/vector.sail

@@ -363,7 +363,9 @@ val sail_shiftright = pure {
   _: "shiftr"} : forall 'n ('ord : Order).
     (bitvector('n, 'ord), int) -> bitvector('n, 'ord)
 
-val sail_arith_shiftright = pure "arith_shiftr" : forall 'n ('ord : Order).
+val sail_arith_shiftright = pure {
+  lean: "BitVec.rotateRight",
+  _: "arith_shiftr"} : forall 'n ('ord : Order).
     (bitvector('n, 'ord), int) -> bitvector('n, 'ord)
 
 val sail_zeros = pure {

test/lean/extern_bitvec.expected.lean

@@ -137,6 +137,9 @@ def extern_count_leading_zeros (_ : Unit) : Int :=
 def extern_count_trailing_zeros (_ : Unit) : Int :=
   (BitVec.countTrailingZeros (0x00FF0FF0 : (BitVec 32)))
 
+def extern_arith_shiftright (_ : Unit) : (BitVec 32) :=
+  (BitVec.rotateRight (0xDEADBEEF : (BitVec 32)) 4)
+
 def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/extern_bitvec.sail

@@ -30,3 +30,7 @@ function extern_count_trailing_zeros() -> int = {
   return count_trailing_zeros(0x00FF0FF0)
 }
 
+function extern_arith_shiftright() -> bitvector(32) = {
+  return sail_arith_shiftright(0xDEADBEEF, 4)
+}
+