Add bitvector types (bv8, bv16, bv32, bv64) to Laurel (#701)

Introduce explicit bitvector types in Laurel so that front-ends can use
them directly rather than encoding them as constrained integer types.

- Add TBv(size) to HighType with equality support
- Add bv8, bv16, bv32, bv64 grammar rules in LaurelGrammar.st
- Translate to Core's LMonoTy.bitvec in LaurelToCoreTranslator
- Add formatting and fix exhaustive match in ToLaurelTest


By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>

Author: 3 people

Strata/Languages/Laurel/FilterPrelude.lean

@@ -78,7 +78,7 @@ private partial def collectHighTypeNames (ty : HighTypeMd) : CollectM Unit := do
   | .Pure base => collectHighTypeNames base
   | .Intersection types => types.forM collectHighTypeNames
   | .TVoid | .TBool | .TInt | .TFloat64 | .TReal | .TString | .THeap
-  | .Unknown => pure ()
+  | .TBv _ | .Unknown => pure ()
 
 /-- Collect all referenced names (procedure calls, type references) from a StmtExpr tree. -/
 private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do

Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean

@@ -43,6 +43,7 @@ partial def highTypeValToArg : HighType → Arg
   | .TFloat64 => laurelOp "float64Type"
   | .TReal => laurelOp "realType"
   | .TString => laurelOp "stringType"
+  | .TBv n => laurelOp "bvType" #[.num sr n]
   | .TMap k v => laurelOp "mapType" #[highTypeToArg k, highTypeToArg v]
   | .UserDefined name => laurelOp "compositeType" #[ident name.text]
   | .TCore s => laurelOp "coreType" #[ident s]

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -83,6 +83,11 @@ instance : Inhabited Parameter where
 def mkHighTypeMd (t : HighType) (md : MetaData) : HighTypeMd := ⟨t, md⟩
 def mkStmtExprMd (e : StmtExpr) (md : MetaData) : StmtExprMd := ⟨e, md⟩
 
+def translateNat (arg : Arg) : TransM Nat := do
+  let .num _ n := arg
+    | TransM.error s!"translateNat expects num literal"
+  return n
+
 partial def translateHighType (arg : Arg) : TransM HighTypeMd := do
   let md ← getArgMetaData arg
   match arg with
@@ -93,6 +98,9 @@ partial def translateHighType (arg : Arg) : TransM HighTypeMd := do
     | q`Laurel.float64Type, _ => return mkHighTypeMd .TFloat64 md
     | q`Laurel.realType, _ => return mkHighTypeMd .TReal md
     | q`Laurel.stringType, _ => return mkHighTypeMd .TString md
+    | q`Laurel.bvType, #[widthArg] =>
+      let width ← translateNat widthArg
+      return mkHighTypeMd (.TBv width) md
     | q`Laurel.coreType, #[.ident _ name] => return mkHighTypeMd (.TCore name) md
     | q`Laurel.mapType, #[keyArg, valArg] =>
       let keyType ← translateHighType keyArg
@@ -101,14 +109,9 @@ partial def translateHighType (arg : Arg) : TransM HighTypeMd := do
     | q`Laurel.compositeType, #[nameArg] =>
       let name ← translateIdent nameArg
       return mkHighTypeMd (.UserDefined name) md
-    | _, _ => TransM.error s!"translateHighType expects intType, boolType, arrayType or compositeType, got {repr op.name}"
+    | _, _ => TransM.error s!"translateHighType: unsupported type operator {repr op.name}"
   | _ => TransM.error s!"translateHighType expects operation"
 
-def translateNat (arg : Arg) : TransM Nat := do
-  let .num _ n := arg
-    | TransM.error s!"translateNat expects num literal"
-  return n
-
 def translateString (arg : Arg) : TransM String := do
   let .strlit _ s := arg
     | TransM.error s!"translateString expects string literal"

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -9,7 +9,7 @@ module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: added space before while/for loop body in format strings.
+-- Last grammar change: parameterized bvType with arbitrary width
 public import Strata.DDM.Integration.Lean
 public meta import Strata.DDM.Integration.Lean
 

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -9,6 +9,7 @@ op boolType : LaurelType => "bool";
 op realType : LaurelType => "real";
 op float64Type : LaurelType => "float64";
 op stringType : LaurelType => "string";
+op bvType (width: Num): LaurelType => "bv" width;
 // Core type passthrough: parsed as Ident, translated to HighType.TCore
 op coreType (name: Ident): LaurelType => "Core " name;
 op mapType (keyType: LaurelType, valueType: LaurelType): LaurelType => "Map " keyType " " valueType;

Strata/Languages/Laurel/Laurel.lean

@@ -155,6 +155,8 @@ inductive HighType : Type where
   | Pure (base : WithMetadata HighType)
   /-- An intersection of types. Used for implicit intersection types, e.g. `Scientist & Scandinavian`. -/
   | Intersection (types : List (WithMetadata HighType))
+  /-- Bitvector type of a given width. -/
+  | TBv (size : Nat)
   /-- Temporary construct meant to aid the migration of Python->Core to Python->Laurel.
   Type "passed through" from Core. Intended to allow translations to Laurel to refer directly to Core. -/
   | TCore (s: String)
@@ -336,6 +338,7 @@ def highEq (a : HighTypeMd) (b : HighTypeMd) : Bool := match _a: a.val, _b: b.va
   | HighType.TReal, HighType.TReal => true
   | HighType.TString, HighType.TString => true
   | HighType.THeap, HighType.THeap => true
+  | HighType.TBv n1, HighType.TBv n2 => n1 == n2
   | HighType.TTypedField t1, HighType.TTypedField t2 => highEq t1 t2
   | HighType.TSet t1, HighType.TSet t2 => highEq t1 t2
   | HighType.TMap k1 v1, HighType.TMap k2 v2 => highEq k1 k2 && highEq v1 v2

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -84,6 +84,7 @@ def translateType (ty : HighTypeMd) : TranslateM LMonoTy := do
   | .TInt => return LMonoTy.int
   | .TBool => return LMonoTy.bool
   | .TString => return LMonoTy.string
+  | .TBv n => return LMonoTy.bitvec n
   | .TVoid => return LMonoTy.bool -- Using bool as placeholder for void
   | .THeap => return .tcons "Heap" []
   | .TTypedField _ => return .tcons "Field" []

StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean

@@ -0,0 +1,49 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+
+namespace Strata
+namespace Laurel
+
+def bvProgram := r"
+// Bitvector types in procedure signatures and variable declarations.
+
+// Parameters and return types
+procedure identity32(x: bv 32) returns (r: bv 32) {
+  r := x
+};
+
+procedure identity8(x: bv 8) returns (r: bv 8) {
+  r := x
+};
+
+// Local variable with bv type
+procedure localBv() returns (r: bv 16) {
+  var x: bv 16 := r;
+  r := x
+};
+
+// Opaque procedure returning bv64 — caller gets typed result
+procedure opaqueBv64() returns (r: bv 64);
+procedure callOpaque() returns (r: bv 64) {
+  r := opaqueBv64()
+};
+
+// Mixed bv and int parameters
+procedure mixedTypes(a: bv 32, b: int) returns (r: int) {
+  r := b
+};
+"
+
+#guard_msgs(drop info, error) in
+#eval testInputWithOffset "BitvectorTypes" bvProgram 14 processLaurelFile
+
+end Laurel
+end Strata

StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean

@@ -30,7 +30,7 @@ procedure simpleAssign() {
   var c: Container := new Container;
   var iv: int := c#intValue;
   var rv: real := c#realValue;
-  var bv: bool := c#boolValue;
+  var boolVar: bool := c#boolValue;
   var sv: string := c#stringValue;
 
   c#intValue := 2;

StrataTest/Languages/Laurel/tests/test_bitvector_types.lr.st

@@ -0,0 +1,14 @@
+// Bitvector types through the GOTO/CBMC pipeline.
+
+procedure identity32(x: bv 32) returns (r: bv 32) {
+  r := x
+};
+
+procedure identity8(x: bv 8) returns (r: bv 8) {
+  r := x
+};
+
+procedure localBv() returns (r: bv 16) {
+  var x: bv 16 := r;
+  r := x
+};