Lean: Fixing Lean style and wrong definition in Sail.lean (#891)

rems-project · Jan 16, 2025 · bf921f9 · bf921f9
1 parent 9addae9
commit bf921f9
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 8 deletions.
diff --git a/lib/vector.sail b/lib/vector.sail
@@ -144,7 +144,7 @@ val truncateLSB = pure {
   interpreter: "vector_truncateLSB",
   lem: "vector_truncateLSB",
   coq: "vector_truncateLSB",
-  lean: "Sail.BitVec.truncateLSB",
+  lean: "Sail.BitVec.truncateLsb",
   _: "sail_truncateLSB"
 } : forall 'm 'n, 'm >= 0 & 'm <= 'n. (bits('n), int('m)) -> bits('m)
 

diff --git a/src/sail_lean_backend/Sail/Sail.lean b/src/sail_lean_backend/Sail/Sail.lean
@@ -1,19 +1,19 @@
 namespace Sail
 namespace BitVec
 
-def length {w: Nat} (_: BitVec w): Nat := w
+def length {w : Nat} (_ : BitVec w) : Nat := w
 
-def signExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
+def signExtend {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' :=
   x.signExtend w'
 
-def zeroExtend {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
+def zeroExtend {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' :=
   x.zeroExtend w'
 
-def truncate {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
+def truncate {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' :=
   x.truncate w'
 
-def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
-  x.extractLsb' 0 w'
+def truncateLsb {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' :=
+  x.extractLsb' (w - w') w'
 
 end BitVec
 end Sail
diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
@@ -19,7 +19,7 @@ def bitvector_truncate (x : BitVec 32) : BitVec 16 :=
   (Sail.BitVec.truncate x 16)
 
 def bitvector_truncateLSB (x : BitVec 32) : BitVec 16 :=
-  (Sail.BitVec.truncateLSB x 16)
+  (Sail.BitVec.truncateLsb x 16)
 
 def bitvector_append (x : BitVec 16) (y : BitVec 16) : BitVec 32 :=
   (BitVec.append x y)