Support contracts on functions#45
Draft
keyboardDrummer-bot wants to merge 329 commits into
Draft
Conversation
…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.
…nditions Key fixes to TransparencyPass.lean: - Keep already-functional procedures (like readField, updateField, nat$constraint) as functions instead of converting them to procedures. This fixes 'calls to procedures are not supported in functions' errors. - Only create $asFunction copies for imperative procedures, not for procedures that are already functional. - Clear preconditions on $asFunction copies to prevent spurious precondition check failures in free postconditions. Update test expectations to match the new behavior: - Functions with assert/assume now report 'not YET supported' errors (since they're properly translated as functions now) - Some assertions that previously failed now pass (transparency pass provides free postconditions that make them provable) - Error message format changes (e.g. 'does not hold' vs 'could not be proved') - T1_MutableFields remains a pre-existing failure (multi-target assignment type translation issue)
The second lifting pass (liftImperativeExpressionsInCore) was keeping variable declarations inside blocks while lifting assignments that reference those variables to the outer scope. This created dangling references that the resolution pass couldn't resolve, causing 'Unknown' types that triggered the 'Core program was suppressed due to superfluous errors' bug. Fix: restore the original behavior of prepending Declare statements from blocks to the outer scope, so they remain visible to lifted assignments that reference them. Also add a defensive check in translateExpr for Var (.Local name): when a variable's type is Unknown (unresolved), omit the type annotation instead of calling invalidCoreType, which would set coreProgramHasSuperfluousErrors without emitting a diagnostic. Update T2_ModifiesClauses test expectations: two assertions that previously failed are now provable thanks to the transparency pass providing free postconditions with correct modifies frame conditions.
The transparency pass generates free postconditions for each procedure, which adds extra passing verification conditions to the output. Update all 206 expected files to reflect the new postcondition VCs.
The benchmark job hardcodes --source-location-override to strata-org/Strata.git, so it fails on forks where the PR head SHA doesn't exist in that repo. Add an 'if' condition to only run when github.repository is strata-org/Strata.
keyboardDrummer
changed the base branch from
issue-21-assign-variable-type
to
main
github-actions
Bot
added
the
Git conflicts
Owner
|
@keyboardDrummer-bot please resolve the conflicts |
github-actions
Bot
removed
the
Git conflicts
keyboardDrummer
force-pushed
the
transparency-pass-only
branch
from
284c852 to
7380f7c
Compare
Collaborator
Author
|
@keyboardDrummer The branch |
keyboardDrummer
force-pushed
the
transparency-pass-only
branch
from
ee8185b to
bd66145
Compare
keyboardDrummer
changed the title
keyboardDrummer
changed the title
keyboardDrummer
changed the title
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
7 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
This PR is a copy of PR #28 (Add contract and transparency pass) but without the first two phases:
EliminateReturnStatements: rewrite return to exit statementsContractPass: translate away pre and postconditions entirely by introducing assertion and assumptions at call sites and at procedure starts and endsWhat's included
The remaining passes from PR #28 are kept:
$asFunction. If a Core procedure is marked as transparent, attempt to generate a functional version of it, where assertions are erased and all calls are to functional versions. Tie the functional version to the procedure using a free postcondition.Fixes included
Includes fixes from:
Changes from PR #28
ContractPass.leanandEliminateReturnStatements.leanLaurelCompilationPipelineinvokeOnaxiom handling in the translator (since the contract pass no longer populatesproc.axioms)Known issues
Related: #28, #43