Issue 924 contract and proof pass#995
Closed
keyboardDrummer wants to merge 112 commits intostrata-org:mainfrom
Closed
Issue 924 contract and proof pass#995keyboardDrummer wants to merge 112 commits intostrata-org:mainfrom
keyboardDrummer wants to merge 112 commits intostrata-org:mainfrom
Conversation
…aurelTypes - Add FunctionsAndProofsProgram structure with functions, proofs, datatypes, constants - Add temporary laurelToFunctionsAndProofs translation (functional → functions, non-functional → proofs) - Rename OrderedLaurel to CoreWithLaurelTypes - Change OrderedDecl: replace 'procs' with 'funcs' (for function SCCs) and 'procedure' (for individual proofs) - Rewire pipeline: Laurel → FunctionsAndProofs → CoreWithLaurelTypes → Core - Both functions and proofs participate in topological ordering via the call graph Addresses steps (c) and (d) of strata-org#924.
(a) Contract pass (ContractPass.lean): - Generates precondition/postcondition helper procedures for non-functional procedures with contracts - Transforms procedure bodies to add assume/assert for own contracts - Not yet wired into pipeline (needs call-site rewriting for full activation) (b) Proof pass improvements (FunctionsAndProofs.lean): - Add stripAssertAssume utility for deep traversal that removes Assert/Assume nodes (to be used when full proof pass generates both functions and proofs for every procedure) - Import MapStmtExpr for AST traversal support - Improve documentation describing the future full proof pass Also: - CoreGroupingAndOrdering: use isFunctional flag instead of name lookup to partition functions and proofs in orderFunctionsAndProofs (more robust when functions and proofs share names) - Pipeline: import ContractPass, update documentation for new pipeline stages
…to pipeline; proof pass: every procedure generates function + proof Changes based on review feedback: 1. Contract pass treats all procedures the same — removed isFunctional guard from collectContractInfo, contractPass, and helper generation. 2. Call-site rewriting — added rewriteCallSites which uses mapStmtExpr for bottom-up traversal and handles three patterns: - Assign targets (StaticCall callee args) → Block [assert pre; assign; assume post] - LocalVariable name type (some (StaticCall callee args)) → Block [assert pre; decl; assume post] - Bare StaticCall callee args → Block [assert pre; call] 3. Contract pass wired into pipeline — replaced placeholder comment with actual contractPass call. 4. Full proof pass — every procedure now generates both a function copy (isFunctional=true, body only for transparent procedures, with Assert/Assume stripped) and a proof copy (isFunctional=false).
…riting and proof pass Three issues caused CI failures: 1. Call-site rewriting used bottom-up mapStmtExpr, which processed StaticCall nodes inside expressions (e.g., inside Assign/LocalVariable initializers) before the parent pattern could match. This created Block[Assert; StaticCall] inside expression positions, which the function translator rejected. Fixed by rewriting at the Block (statement) level instead. 2. The proof pass created both function and proof copies for every procedure with the same name, causing 'declaration already exists' errors in the Core type checker. Reverted to partition behavior (functional → functions, non-functional → proofs). 3. The contract pass changes verification diagnostics from 'precondition does not hold' to 'assertion does not hold', breaking test expectations. Disabled the contract pass in the pipeline pending test updates. The contract pass code (ContractPass.lean) is preserved with the fixes above and can be re-enabled. stripAssertAssume and mkFunctionCopy are also preserved for when the full proof pass is activated.
…-org/Strata into issue-924-contract-and-proof-pass
- Add 'opaque' keyword to the Laurel grammar (LaurelGrammar.st) that groups ensures and modifies clauses under it - Update ConcreteToAbstractTreeTranslator to parse the new opaqueSpec grammar node (8 args instead of 9) - Update AbstractToConcreteTreeTranslator to emit opaqueSpec when formatting procedures with Opaque bodies - Update all Laurel test files to mark all procedures as opaque - Update .lr.st and .laurel.st test files accordingly
Keep both the FunctionsAndProofs pipeline from this branch and the overflowChecks field added on main.
Adds a new Laurel-to-Laurel pass that replaces return statements with assignments to output parameters followed by exit to a labelled block wrapping the procedure body. This ensures postcondition assertions (inserted by the contract pass) are checked on all return paths. The pass runs after EliminateReturnsInExpression and before ConstrainedTypeElim/ContractPass in the pipeline.
…' into opaque-keyword-grammar
…assertions When a requires or ensures clause has a summary annotation, the contract pass now propagates that summary to the generated assert statement. This means verification errors will display the user-provided summary (e.g., 'divisor is non-zero does not hold') instead of the generic 'precondition does not hold' or 'postcondition does not hold'. - Added combinedSummary helper to extract summaries from clause metadata - Added preSummary/postSummary fields to ContractInfo - Updated all assertion generation sites to use clause summaries when available
…opaqueSpec - Changed procedureToOp to produce opaqueSpec op with ensures and modifies as nested args (matching the grammar), instead of separate top-level args - Added missing opaque keyword in MapStmtExprTest and T2_ModifiesClauses tests
…lator - Add `axioms : List StmtExprMd` field to Laurel's Procedure structure - In ContractPass, build axiom expressions from invokeOn trigger + ensures clauses (nested Forall with trigger on innermost quantifier), then clear the invokeOn field - Update LaurelToCoreTranslator to translate proc.axioms directly instead of using the now-removed translateInvokeOnAxiom function - Update CoreGroupingAndOrdering to use axioms instead of invokeOn for procedure ordering and callee collection - Update Resolution to preserve axioms through name resolution - Update MapStmtExpr to traverse axioms in mapProcedureM - Fix InvokeOn test expected error messages
…transparent-statement-bodies
- Grammar: Add `modifiesWildcard` op for `modifies *` syntax - Parser: Handle `modifiesWildcard` by producing `StmtExpr.All` in modifies list - Printer: Emit `modifiesWildcard` when modifies list contains `All` - ModifiesClauses: Skip frame condition generation for wildcard modifies - FilterNonCompositeModifies: Preserve `All` entries (don't filter as non-composite) - HeapParameterization: Don't treat wildcard `All` as evidence of heap access - PythonToLaurel: Use `modifies *` for all opaque procedures - Specs/ToLaurel: Use `modifies *` for spec procedures - T2_ModifiesClauses: Uncomment wildcard test case
…ontract-and-proof-pass
Two issues were causing the Python test failures: 1. dbg_trace statements in LaurelCompilationPipeline.lean were printing massive debug output that polluted #guard_msgs test expectations. 2. The contract pass (ContractPass.lean) created Assert/Assume nodes with source := none (via mkMd). When these reached the Core translator, getNameFromMd triggered 'BUG: metadata without a filerange' debug traces, further polluting test output. Fix: propagate source locations from the original preconditions and body to the Assert/Assume/Block nodes created by transformProcBody.
Prefix `program` parameter with underscore to suppress the 'unused variable' warning that causes the docs build to fail with --wfail.
…-org/Strata into issue-924-contract-and-proof-pass
Change Test 12 (Java compilation test) to use logInfo instead of logError when javac or ion-java jar is not found. This makes the test skip gracefully rather than failing the build, matching the pattern used by Python tests that skip when strata.gen is not installed.
This reverts commit f56e6cd.
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.
Builds on:
Summary
TODO
Follow-up work