strata-org · tautschnig · Mar 28, 2026 · Mar 28, 2026 · Mar 28, 2026 · keyboardDrummer
@@ -92,6 +92,10 @@ 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.bv8Type, _ => return mkHighTypeMd (.TBv 8) md
+    | q`Laurel.bv16Type, _ => return mkHighTypeMd (.TBv 16) md
+    | q`Laurel.bv32Type, _ => return mkHighTypeMd (.TBv 32) md
+    | q`Laurel.bv64Type, _ => return mkHighTypeMd (.TBv 64) md
     | q`Laurel.coreType, #[.ident _ name] => return mkHighTypeMd (.TCore name) md
     | q`Laurel.mapType, #[keyArg, valArg] =>
       let keyType ← translateHighType keyArg
@@ -100,7 +104,7 @@ 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

@@ -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: replaced regexType with general coreType
+-- Last grammar change: added bv8, bv16, bv32, bv64 types
 public import Strata.DDM.Integration.Lean
 public meta import Strata.DDM.Integration.Lean
 

@@ -9,6 +9,10 @@ op boolType : LaurelType => "bool";
 op realType : LaurelType => "real";
 op float64Type : LaurelType => "float64";
 op stringType : LaurelType => "string";
+op bv8Type : LaurelType => "bv8";
+op bv16Type : LaurelType => "bv16";
+op bv32Type : LaurelType => "bv32";
+op bv64Type : LaurelType => "bv64";
 // 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;

@@ -154,6 +154,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)
@@ -346,6 +348,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

@@ -52,6 +52,7 @@ def formatHighTypeVal : HighType → Format
   | .TReal => "real"
   | .TString => "string"
   | .THeap => "Heap"
+  | .TBv n => s!"bv{n}"
   | .TTypedField valueType => "Field[" ++ formatHighType valueType ++ "]"
   | .TSet elementType => "Set[" ++ formatHighType elementType ++ "]"
   | .TMap keyType valueType => "Map[" ++ formatHighType keyType ++ ", " ++ formatHighType valueType ++ "]"

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

@@ -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: bv32) returns (r: bv32) {
+  r := x
+};
+
+procedure identity8(x: bv8) returns (r: bv8) {
+  r := x
+};
+
+// Local variable with bv type
+procedure localBv() returns (r: bv16) {
+  var x: bv16 := r;
+  r := x
+};
+
+// Opaque procedure returning bv64 — caller gets typed result
+procedure opaqueBv64() returns (r: bv64);
+procedure callOpaque() returns (r: bv64) {
+  r := opaqueBv64()
+};
+
+// Mixed bv and int parameters
+procedure mixedTypes(a: bv32, b: int) returns (r: int) {
+  r := b
+};
+"
+
+#guard_msgs(drop info, error) in
+#eval testInputWithOffset "BitvectorTypes" bvProgram 14 processLaurelFile
+
+end Laurel
+end Strata
@@ -0,0 +1,14 @@
+// Bitvector types through the GOTO/CBMC pipeline.
+
+procedure identity32(x: bv32) returns (r: bv32) {
+  r := x
+};
+
+procedure identity8(x: bv8) returns (r: bv8) {
+  r := x
+};
+
+procedure localBv() returns (r: bv16) {
+  var x: bv16 := r;
+  r := x
+};
@@ -58,8 +58,9 @@ private def fmtHighType : HighType → String
   | .Applied _ _ => "Applied"
   | .Pure _ => "Pure"
   | .Intersection _ => "Intersection"
+  | .TBv n => s!"TBv({n})"
   | .TCore s => s!"TCore({s})"
-  | HighType.Unknown => "Unknown"
+  | .Unknown => "Unknown"
 
 private def fmtParam (p : Parameter) : String :=
   s!"{p.name}:{fmtHighType p.type.val}"