Add bitvector types (bv8, bv16, bv32, bv64) to Laurel#701
Add bitvector types (bv8, bv16, bv32, bv64) to Laurel#701tautschnig wants to merge 3 commits intomainfrom
Conversation
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 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
- T19_BitvectorTypes.lean: Lean test exercising bv8/bv16/bv32/bv64 in parameters, return types, local variables, opaque contracts, and mixed with int. - test_bitvector_types.lr.st: CBMC pipeline test for BV types. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
There was a problem hiding this comment.
Pull request overview
Adds first-class bitvector types to the Laurel language so front-ends can model bit-precise values without encoding them as constrained integers, and wires those types through parsing, formatting, and Laurel→Core translation.
Changes:
- Introduce
HighType.TBv (size : Nat)and extendhighEqto compare bitvector widths. - Extend Laurel grammar + CST→AST translation with
bv8/bv16/bv32/bv64type tokens. - Translate
TBv nto Core/LambdaLMonoTy.bitvec nand add end-to-end tests/examples.
Reviewed changes
Copilot reviewed 9 out of 9 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| Strata/Languages/Laurel/Laurel.lean | Adds HighType.TBv and equality support for bitvector types. |
| Strata/Languages/Laurel/Grammar/LaurelGrammar.st | Adds grammar tokens for bv8/bv16/bv32/bv64. |
| Strata/Languages/Laurel/Grammar/LaurelGrammar.lean | Forces rebuild after grammar change (comment bump). |
| Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean | Maps new grammar ops to HighType.TBv widths. |
| Strata/Languages/Laurel/LaurelToCoreTranslator.lean | Lowers TBv n to LMonoTy.bitvec n. |
| Strata/Languages/Laurel/LaurelFormat.lean | Formats TBv n as bv{n}. |
| StrataTest/Languages/Python/ToLaurelTest.lean | Updates pretty-printing helper to handle TBv. |
| StrataTest/Languages/Laurel/tests/test_bitvector_types.lr.st | Adds a pipeline test exercising bitvector types in signatures/locals. |
| StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean | Adds a diagnostic-based Laurel example covering bv8/16/32/64. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
The error message listed only the original type operators. Replace with a generic message that won't go stale as new types are added. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
| | 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 |
There was a problem hiding this comment.
Could we abstract over the amount of bits? Also, I think the right default SMT encoding is to use an int with constraints, not an SMT bitvector. Until Core supports that, can we really define this with the correct verification behavior in Laurel? Right now I think the front-ends can't use these types because of the default SMT bitvector behavior, so it seems confusing to add them.
Also, should we think about this end-to-end? How will users indicate what SMT encoding they want to use for particular variables? Can we infer the probably best encoding based on which operators the variables are applied to? My guess would be that a good heuristic is that if no bit specific operators are used, use an int and otherwise a bv.
Introduce explicit bitvector types in Laurel so that front-ends can use them directly rather than encoding them as constrained integer types.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.