Laurel-to-Core translator expansion with grammar improvements#4
Draft
fabiomadge wants to merge 24 commits intokeyboardDrummer:mutableFieldsfrom
Draft
Laurel-to-Core translator expansion with grammar improvements#4fabiomadge wants to merge 24 commits intokeyboardDrummer:mutableFieldsfrom
fabiomadge wants to merge 24 commits intokeyboardDrummer:mutableFieldsfrom
Conversation
- Add binary operators: sub (-), mul (*), div (/), mod (%) - Add logical operators: and (&&), or (||) - Add unary operators: not (!), neg (-) - Use spaces around && and || operators - Fix DDM parser to always treat // as line comment (regardless of token table) The parser fix allows / to be used as a token without breaking // comments.
- Add while loop syntax to grammar with invariant clauses - Add parser for while loops (combines multiple invariants with &&) - Add While case to LaurelToCoreTranslator - Add leftassoc to arithmetic/logical operators (fixes a * b / c parsing) - Create T4_WhileBasic.lean test
- Change Procedure.precondition to preconditions : List StmtExpr - Change Body.Opaque/Abstract postcondition to postconditions : List StmtExpr - Update grammar: requires/ensures now use Seq instead of Option - Update parser to collect list of requires/ensures clauses - Update translator to generate indexed labels (proc_pre_0, proc_post_0, etc.) - Update LaurelFormat, LaurelEval for list-based contracts - Update canBeBoogieFunction to check preconditions.isEmpty
- Add constrainedType grammar rule and parser - Add topLevelConstrainedType to TopLevel - Build ConstrainedTypeMap from program type definitions - Resolve constrained types to base types in parameter translation - Generate constraint checks as preconditions for input parameters - Generate constraint checks as postconditions for output parameters - Use resolved types in type environment for expression translation - Create T10_ConstrainedTypes.lean test
- Thread ctMap through translateStmt - Resolve constrained types to base types for locals - Generate assertion after init for constrained type locals
- Thread ctMap through translateExpr and lookupType - Generate constraint assertion after assignment to constrained type variable
- Handle StaticCall specially in Assign case - Generate call statement instead of function application
- genConstraintAssert: generates constraint assertion for a variable - defaultExprForType: generates default value for a type - isHeapFunction: checks if function is heapRead/heapStore
- Grammar: forallExpr, existsExpr with (name: type) => body syntax - Parser: translate to Laurel.Forall/Exists AST nodes - Translator: varCloseByName helper, translate to Core quant expressions - Test: T5_Quantifiers.lean
- forall(x: nat) => body becomes forall x. (x >= 0) ==> body - exists(x: nat) => body becomes exists x. (x >= 0) && body - Made translateExpr partial to allow recursive constraint translation
- Add TranslatedConstraintMap with pre-translated Core constraint expressions - Add translateSimpleExpr for constraint expressions (no quantifiers) - Build tcMap upfront in translate(), pass through all functions - Quantifiers use pre-translated constraints, avoiding recursive call on external data - Restore termination proof for translateExpr
- Explicit cases for Forall/Exists with clear error message - Better error messages for unsupported operators
Reduces duplication between translateExpr and translateSimpleExpr
- Array type translates to Map int elemType - Array.Get uses select operation (Core infers types) - Array.Length uses name#len free variable - expandArrayParam expands array params to (arr, arr#len) pairs - Fixed CoreIdent visibility: use unres for operations, matching factory convention
- Sequences represented as (arr, start, end) bounds - Seq.Contains translates to existential: exists i :: start <= i < end && arr[i] == elem - Seq.Take adjusts end bound - Seq.Drop adjusts start bound - No new axioms needed - direct translation to quantifiers - Fixed identifier matching for guillemet-escaped names («Seq.Contains» etc)
- Add Forall and Exists cases to isPureExpr so pure functions with quantifiers can be translated as Core functions (fixes non-termination) - Map 'Map' type to SMT 'Array' type in both lMonoTyToSMTString and encodeType Note: There's a remaining issue with user-defined functions taking Map arguments when called in while loop invariants - the UF key mismatch between definition and call sites needs further investigation.
…lation This adds a FunctionTypeMap that maps function names to their types, built from procedures that can be translated as functions. When translating a StaticCall, we look up the function type and attach it to the .op expression. This is necessary for the SMT encoder to correctly encode user-defined function calls, as it needs the type information to create the correct uninterpreted function signatures. Note: There is still an issue where the type annotation is lost during evaluation. The type is present in the translated Core program but missing in the VCs. This needs further investigation.
Grammar: - Add spacing around operators for readable output - Add divT, modT (truncating division) and implies operators - Use NewlineSepBy + indent() for block formatting - Add newline prefixes for requires/ensures/invariant clauses - Fix call precedence for proper parsing Translator: - Replace panic! with Except String for proper error handling - Add expandArrayArgs and injectQuantifierConstraint helpers - Add normalizeCallee for «» quoted identifiers - Validate array types in Seq.From - Support multiple invariants (combined with &&) CLI: - Add laurelParse, laurelAnalyze, laurelToCore, laurelPrint commands Tests: - Add testTruncatingDiv, testUnary, implies tests - Add multiContract for multiple requires/ensures
fabiomadge
changed the title
keyboardDrummer
added a commit
that referenced
this pull request
Feb 13, 2026
### Changes - Add a Python script in `Tools` that enables automatically updating the results of `#guard_msg` - Update formatting of applications in Core. A good way to see how the formatting has changed is to look at the updated tests in this PR. Before: ``` while (((~Int.Lt i) n)) (some ((~Int.Sub n) i)) (some ((~Bool.And ((~Int.Le i) n)) (((~Int.Div ((~Int.Mul i) ((~Int.Sub i) #1))) #2) == sum))) {sum := ((~Int.Add sum) i) i := ((~Int.Add i) #1)} ``` After: ``` while (~Int.Lt i n) (some (~Int.Sub n i)) (some (~Bool.And (~Int.Le i n) ((~Int.Div (~Int.Mul i (~Int.Sub i #1)) #2) == sum))) { sum := (~Int.Add sum i) i := (~Int.Add i #1) } ``` Applications in expressions require fewer parenthesis are are shown in a tree like fashion when they do not fit on a line: Before ``` /-- info: Annotated expression: ((((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int)))) (((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string))))) (((~Prod : (arrow int (arrow string (Tup int string)))) #3) #a)) (((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string))))) (((~Prod : (arrow int (arrow string (Tup int string)))) #4) #b)) (~Nil : (List (Tup int string)))))) #0) (λ (λ (λ (((~Int.Add : (arrow int (arrow int int))) (((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int))) %2) (λ (λ %1)))) ((((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int)))) %1) #1) (λ (λ (λ (((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int))) %2) (λ (λ %1)))))))))))) ``` After ``` /-- info: Annotated expression: ((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int)))) ((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string))))) ((~Prod : (arrow int (arrow string (Tup int string)))) #3 #a) ((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string))))) ((~Prod : (arrow int (arrow string (Tup int string)))) #4 #b) (~Nil : (List (Tup int string))))) #0 (λ (λ (λ ((~Int.Add : (arrow int (arrow int int))) ((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int))) %2 (λ (λ %1))) ((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int)))) %1 #1 (λ (λ (λ ((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int))) %2 (λ (λ %1)))))))))))) ``` ### Testing Updated tests --------- Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>
github-actions
Bot
added
the
Git conflicts
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Translator:
Grammar:
CLI:
Tests: