Lean: annotations for slice and vector length (#1061)

lib/smt.sail

@@ -55,6 +55,7 @@ val ediv_int = pure {
   interpreter: "quotient",
   lem: "integerDiv",
   coq: "ZEuclid.div",
+  lean: "Int.ediv",
   _: "ediv_int"
 } : forall 'n 'm. (int('n), int('m)) -> int(div('n, 'm))
 
@@ -63,6 +64,7 @@ val emod_int = pure {
   interpreter: "modulus",
   lem: "integerMod",
   coq: "ZEuclid.modulo",
+  lean: "Int.emod",
   _: "emod_int"
 } : forall 'n 'm. (int('n), int('m)) -> int(mod('n, 'm))
 

lib/vector.sail

@@ -88,6 +88,7 @@ val vector_length = pure {
   interpreter: "length",
   lem: "length_list",
   coq: "vec_length",
+  lean: "Vector.length",
   _: "length"
 } : forall 'n ('a : Type). vector('n, 'a) -> int('n)
 
@@ -369,7 +370,9 @@ function sail_ones(n) = not_vec(sail_zeros(n))
 // Some ARM specific builtins
 
 $ifdef _DEFAULT_DEC
-val slice = pure "slice" : forall 'n 'm 'o, 0 <= 'm & 0 <= 'n.
+val slice = pure {
+  lean: "BitVec.slice",
+  _: "slice"} : forall 'n 'm 'o, 0 <= 'm & 0 <= 'n.
   (bits('m), int('o), int('n)) -> bits('n)
 $else
 val slice = pure "slice_inc" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm.

src/sail_lean_backend/Sail/Sail.lean

@@ -47,6 +47,9 @@ def updateSubrange' {w : Nat} (x : BitVec w) (start len : Nat) (y : BitVec len)
   let y' := mask ||| ((y.zeroExtend w) <<< start)
   x &&& y'
 
+def slice {w : Nat} (x : BitVec w) (start len : Nat) : BitVec len :=
+  x.extractLsb' start len
+
 def updateSubrange {w : Nat} (x : BitVec w) (hi lo : Nat) (y : BitVec (hi - lo + 1)) : BitVec w :=
   updateSubrange' x lo _ y
 
@@ -457,9 +460,17 @@ def shiftr (a : Int) (n : Int) : Int :=
 
 end Int
 
+def get_slice_int (len n lo : Nat) : BitVec len :=
+  BitVec.extractLsb' lo len (BitVec.ofInt (lo + len + 1) n)
+
+def set_slice_int (len n lo : Nat) (x : BitVec len) : Int :=
+  BitVec.toInt (BitVec.updateSubrange' (BitVec.ofInt len n) lo len x)
+
 def String.leadingSpaces (s : String) : Nat :=
   s.length - (s.dropWhile (· = ' ')).length
 
+def Vector.length (_v : Vector α n) : Nat :=
+  n
 
 instance : HShiftLeft (BitVec w) Int (BitVec w) where
   hShiftLeft b i :=
@@ -471,4 +482,3 @@ instance : HShiftRight (BitVec w) Int (BitVec w) where
   hShiftRight b i := b <<< (-i)
 
 end Sail
-

test/lean/extern_bitvec.expected.lean

@@ -22,7 +22,7 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
-/-- Type quantifiers: k_ex699# : Bool, k_ex698# : Bool -/
+/-- Type quantifiers: k_ex705# : Bool, k_ex704# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
   (Bool.not (BEq.beq x y))
 
@@ -100,6 +100,12 @@ def extern_add (_ : Unit) : (BitVec 16) :=
 def extern_replicate_bits (_ : Unit) : (BitVec 64) :=
   (BitVec.replicateBits (0x1234 : (BitVec 16)) 4)
 
+def extern_slice (x : (BitVec 16)) : (BitVec 4) :=
+  (BitVec.slice x 2 4)
+
+def extern_vector_length (x : (Vector Int 3)) : Int :=
+  (Vector.length x)
+
 def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/extern_bitvec.sail

@@ -14,3 +14,11 @@ function extern_replicate_bits() -> bitvector(64) = {
   return replicate_bits(0x1234, 4)
 }
 
+function extern_slice(x : bitvector(16)) -> bitvector(4) = {
+  return slice(x, 2, 4)
+}
+
+function extern_vector_length(x : vector(3, int)) -> int = {
+  return length(x)
+}
+