Draft
Conversation
- 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
Resolved conflicts: - AST.lean: Keep both File2dRange (branch) and DiagnosticModel (main) - MetaData.lean: Keep both formatFileRange? (branch) and toDiagnostic (main) - Translate.lean: Use main's fileRange (branch had undefined vars) - Verifier.lean: Use main's cleaner DiagnosticModel usage - Laurel files: Keep branch's extensive Laurel work (phases 1-5) - Parser.lean: Fix // comment handling to support //@tokens Additional fixes: - C_Simp/Verify.lean: Add missing md field - StrataMain.lean: Fix Python API references Note: Some #guard_msgs tests need updating due to formatting changes.
C_Simp: - Add spaces around operators, keywords, and tokens - Add newlines before //@pre and //@post Laurel: - Use NewlineSepBy for requires/ensures/invariant clauses - Update translator to accept any separator type - Remove embedded newlines from clause definitions (now handled by NewlineSepBy) - Add space after 'while' keyword
- Use NewlineSepBy for block statements - Add proper indentation with indent() for pre/post and block contents - Update translator to accept any separator type - Remove trailing newlines from statements (handled by NewlineSepBy) - Update Trivial.lean test expected output
- C_Simp: Simplify if/else formatting to put } else { on same line
- Laurel: Handle expression-like statements as implicit returns
- Laurel: Fix heapRead/heapStore visibility (use unres to match definition)
- Refactor: Extract mkReturnStmts helper, move isHeapFunction earlier
- Update expected test outputs for formatting changes
Keep our metadata-everywhere approach and list-based preconditions. Take main's moved proof files and 1d location approach (remove File2dRange). Remove duplicate proof files from StrataTest (moved to Strata).
Generate assume statements for array element accesses when the array has a constrained element type (e.g., Array<int32>). Before each statement that accesses such elements, we emit assumes ensuring the constraint holds. Limitations: Only handles identifier arrays, not complex expressions. Future: Axiom-based $Is approach would be cleaner.
…lEval - Rename Laurel tests T01-T17 with consistent numbering - Working tests first (T01-T11), placeholders after (T12-T17) - Fix insideCondition bug: restore withInsideCondition to properly save/restore flag - Add regression test for assignment lifting after conditional - Revert LaurelEval.lean changes (file is unused/dead code)
Array parameters are expanded to (arr, arr_len) pairs in procedure signatures, but the expansion was missing at call sites in translateStmt. This caused arity mismatch errors when calling procedures with array parameters. Fixed in three places: - LocalVariable initialized with procedure call - Assign with procedure call value - Standalone procedure call statement Added test case for passing arrays between procedures.
fabiomadge
force-pushed
the
jverify-strata-backend
branch
from
2924fc9 to
8122075
Compare
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
5 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.
Summary
Expands the Laurel language with additional operators, data types, and verification constructs. Improves formatting across multiple dialects.
Key Changes
Laurel Grammar & Translator
-,*,/,%,/t,%t(truncating),==>,!, unary-Array<T>type, indexing, lengthSeq.From,Seq.Take,Seq.Drop,Seq.Containsforall,existsrequires/ensuresclauses per procedureStmtExprMd,HighTypeMd) threaded through ASTInfrastructure
NewlineSepByseparator type for formatting preservationSourceRangeoverloadsCLI Commands
laurelParse,laurelAnalyze,laurelToCore,laurelPrintBug Fixes
insideConditionflag not resetting after conditionalsMaptypesubstFvarLiftingfor proper de Bruijn index handlingTests