Add EliminateReturnStatements and ContractPass#34
Draft
keyboardDrummer-bot wants to merge 205 commits intomainfrom
Draft
Add EliminateReturnStatements and ContractPass#34keyboardDrummer-bot wants to merge 205 commits intomainfrom
keyboardDrummer-bot wants to merge 205 commits intomainfrom
Conversation
- Add OpaqueClause category and optional opaque parameter to procedure/function grammar ops, placed between invokeOn and ensures clauses - Update ConcreteToAbstractTreeTranslator to parse the new opaque argument and use it to determine Body.Opaque vs Body.Transparent - Update LaurelFormat to output 'opaque' for Opaque bodies - Update all Laurel test files: procedures with ensures clauses now use explicit opaque keyword; procedures that only had 'ensures true' now use just 'opaque' - Remove comments about considering more explicit opaque syntax - Update PythonRuntimeLaurelPart Laurel source strings with opaque keyword Closes #9
Add a resolution check that emits a diagnostic when a non-functional procedure (declared with 'procedure', not 'function') has a transparent body (no 'ensures' clause). The diagnostic message advises adding 'ensures true' to make the procedure opaque. Changes: - Resolution.lean: Add transparent body check in resolveProcedure and resolveInstanceProcedure - LaurelToCoreTranslator.lean: Add checkTransparentBodies option to LaurelTranslateOptions, filter diagnostics when disabled - PySpecPipeline.lean: Disable transparent body check for Python pipeline (Python-generated procedures will be updated separately) - T20_TransparentBodyError.lean: New Laurel test expecting the diagnostic - T2_ModifiesClauses.lean: Updated as specified in issue #10 - All other Laurel test files: Add 'ensures true' (and 'modifies' clauses where needed) to procedures with transparent bodies - T8c_BodilessInlining.lean: Update expected assertion label offset - AnalyzeLaurelTest.lean: Filter transparent body errors in resolution test Closes #10
Merge origin/add-opaque-keyword into disallow-transparent-statement-bodies. Resolve conflicts in T8c_BodilessInlining.lean and T2_ModifiesClauses.lean. Replace all 'ensures true' with 'opaque' in Laurel test files. Update diagnostic message to reference 'opaque' keyword.
… bodies - Remove checkTransparentBodies from LaurelTranslateOptions and its filtering logic in translateWithLaurel - Remove checkTransparentBodies := false from PySpecPipeline - Change Python-generated procedure bodies from Transparent to Opaque in PythonToLaurel (method bodies and __main__) - Convert spec preconditions from body assertions to requires clauses (buildSpecBody → buildSpecPreconditions) with property summaries - Include procedures with preconditions in inlinableProcedures so the Python-to-Laurel translator generates calls for them - Pass userSourcePaths to splitProcNames in AnalyzeLaurelTest so spec procedures are classified as prelude (not inlined away) - Remove transparent body error filtering from AnalyzeLaurelTest - Broaden precondition violation test checks (no longer filter by servicelib_Storage_ prefix since labels now use callElimAssert_)
Resolve merge conflicts: - LaurelGrammar.lean: keep opaque keyword grammar change comment - PythonToLaurel.lean: keep Opaque bodies, remove non-existent md field - ToLaurel.lean: take main's buildSpecBody refactoring (SpecAssertMsg, SpecExprContext, type-checked preconditions) but return .Opaque instead of .Transparent - AbstractToConcreteTreeTranslator.lean: add opaqueClause argument to procedureToOp to match the grammar definition - Resolution.lean: fix proc.md -> proc.name.md (Procedure has no md field) - LaurelFormat.lean: accept deletion (replaced by DDM grammar formatter) - LiftHolesTest.lean: take main's DDM-based formatting - ConstrainedTypeElimTest.lean: use main's DDM format with opaque keyword - AnalyzeLaurelTest.lean: take main's entry-point/inlining refactoring, re-apply PR's foundAlwaysFalse simplification - PreludeVerifyTest.lean: take main's expected output
Resolve conflicts: - LaurelGrammar.lean: keep opaque keyword comment - LaurelFormat.lean: accept upstream deletion (replaced by AbstractToConcreteTreeTranslator) - AbstractToConcreteTreeTranslator.lean: add opaque argument to procedureToOp - LaurelGrammar.st: fix opaqueClause format string to use newline+indent prefix - LiftHolesTest.lean: add opaque to hole function expected outputs - ConstrainedTypeElimTest.lean: add opaque to test procedure expected output - AbstractToConcreteTreeTranslatorTest.lean: add opaque to roundtrip test inputs/outputs - T8d_HeapMutatingValueReturn.lean: add opaque to procedures with ensures clauses
…que in tests
- Fix opaqueClause grammar to include newline prefix ("\n opaque")
- Fix parser to still create Opaque body when postconditions are present
even without explicit opaque keyword
- Only emit opaqueClause for Opaque bodies with postconditions, impl, or modifies
(empty Opaque bodies like hole functions don't need it)
- Add opaque to remaining test procedures with transparent bodies:
T19_BitvectorTypes, T20_InferTypeError, T21_ExitMultiPathAssert,
T8d_HeapMutatingValueReturn, DuplicateNameTests
- Update expected output in AbstractToConcreteTreeTranslatorTest
The change from Transparent to Opaque bodies for spec procedures caused them to be excluded from inlinableProcedures, which meant the Python-to- Laurel translator generated Holes instead of direct calls for spec procedure invocations. This broke the AnalyzeLaurelTest precondition violation tests (no assertions were generated in the inlined body). Fix by matching on body variants: Transparent and Opaque-with-implementation are both inlinable. Also update VerifyPythonTest to expect opaque bodies for Python-generated methods.
The opaque body changes cause additional postcondition VCs to appear in test_method_call_with_kwargs and test_method_kwargs_no_hierarchy.
Procedures are now opaque, so they generate an additional postcondition verification condition. Update the 12 affected expected files.
…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
…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
Refactor StmtExpr to introduce a Variable inductive type: - Add Variable with Local (name) and Field (target, fieldName) constructors - Replace StmtExpr.Identifier with StmtExpr.Var (.Local name) - Replace StmtExpr.FieldSelect with StmtExpr.Var (.Field target fieldName) - Change Assign targets from List (AstNode StmtExpr) to List (AstNode Variable) - Add multi-target assignment (multiAssign) to the Laurel grammar - Update all pattern matches and constructors across the codebase Closes #21
The multiAssign rule (CommaSepBy Ident := StmtExpr) conflicts with call argument parsing (CommaSepBy StmtExpr), causing parse failures in HeapParameterizationConstants and PythonRuntimeLaurelPart. Multi-target assignment from Python is handled by PythonToLaurel, not the Laurel grammar parser.
Remove StmtExpr.LocalVariable and add Variable.Declare constructor.
- var x: int := 3 is now Assign [Declare {x, int}] 3
- var x: int (no init) is now Var (Declare {x, int})
Update all consumers across the codebase: grammar translators,
resolution, heap parameterization, type hierarchy, Laurel-to-Core
translator, lift imperative expressions, map/traverse utilities,
Python-to-Laurel translator, type alias/constrained type elimination,
filter prelude, infer hole types, and affected test comments.
- Add multiAssign grammar rule: var x: int, y, var z: int := call() - Parse multiAssign in ConcreteToAbstract translator - Emit multiAssign in AbstractToConcrete translator for multi-target assigns - Handle Declare targets in multi-target assign in LaurelToCore translator - Add T22_MultipleReturns test verifying the feature end-to-end
Changed the grammar so multi-target assignments use 'assign' keyword: assign var x: int, y, var z: int := multipleReturns(); assign a, var b: int, var c: int := multipleReturns(); This removes the ambiguity since the first target no longer needs to be a 'var' declaration. Single assignments still work without 'assign': var m: int := 3; n := 4; Updated test to cover both forms.
…p recursion, update docs, remove partial - ConcreteToAbstractTreeTranslator: replace silent fallback with TransM.error for non-Var assign targets - HeapParameterization: restore recursion into Field targets and value for multi-target assigns - CoreGroupingAndOrdering: clarify comment about field-target assigns being eliminated before this pass - Laurel.lean: update Variable doc to cover all three constructors - TypeHierarchy: remove partial from validateDiamondFieldAccessesForStmtExpr and provide termination proof
- Add dedicated handler for Assign (targetHead::targetTail) (StaticCall | InstanceCall) that adds heap variable to front of targets when callee writes heap - Add heap variable to call arguments when callee reads/writes heap - Extract single field-write case as separate pattern for clarity - Add test case for heap-modifying procedure with multiple returns
…fying multiple return - Add repeatedAssignTarget test to T22_MultipleReturns (passes) - Add fieldAssignsFromHeapModifyingMultipleReturnCaller test to M1_MutableFields - Add assignTargetField grammar rule for field access targets in multiAssign - Implement processFieldAssignments in HeapParameterization: replaces Field targets with fresh local variables and generates suffix heap update statements - Update ConcreteToAbstract/AbstractToConcrete for field assign targets
…e unused mkVarDecl - Replace empty string with $BUG_invalid_var in stmtExprToVar fallback - Remove unused mkVarDecl function
- Remove unused variable names (h1, h2, hmem, hval) in termination proofs - Remove unused simp argument AstNode.val - Remove unused simp argument List.cons
keyboardDrummer
force-pushed
the
contract-pass-v2
branch
from
47290be to
771104e
Compare
keyboardDrummer
changed the base branch from
issue-21-assign-variable-type
to
main
*Description of changes:* Always transform asserts in LiftImperativeExpressions to hoist imperative procedure calls out of expressions. Previously, asserts containing imperative calls were skipped, leaving procedure calls inside pure expressions that Core rejects with 'calls to procedures are not supported in functions or contracts'. Added test which produces an internal assert of the form `!Any..isexception(PSub(base, timedelta_func(...)))`. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. --------- Co-authored-by: Michael Tautschnig <tautschn@amazon.com> Co-authored-by: Kiro <kiro-agent@users.noreply.github.com> Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Repository owner
deleted a comment from
keyboardDrummer-bot
May 5, 2026
Owner
|
@keyboardDrummer-bot can you debug the failure in CI ? if you don't have a good fix, just tell me the analysis |
Two bugs in the ContractPass: 1. In functional procedures, precondition asserts at call sites caused 'asserts are not supported in functions' errors during Laurel-to-Core translation. Fix: use assume instead of assert for precondition checks inside functional procedures (RemoveFunctionAssumptions will strip them). 2. For bare StaticCall (no assignment), the postcondition function was called without output arguments, causing a type error (partial application returned arrow type instead of bool). Fix: capture outputs in temporary variables and pass them to the function. Also moves 4 tests from pending/ to tests/ that now pass due to the ContractPass handling preconditions at call sites.
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
8 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
Adds two new Laurel-to-Laurel passes, extracted from #28 with modified contract pass semantics:
EliminateReturnStatements: rewrites
returntoexitstatements by wrapping the body in a labelled block. This ensures code placed after the body (e.g., postcondition assertions) is always reached.ContractPass: translates away pre and postconditions entirely by introducing assertions and assumptions at call sites and at procedure starts and ends.
Contract Pass Design
Key differences from the version in #28:
$postprocedures are functional (isFunctional := true)$posttakes all inputs AND all outputs of the original procedure as parameters$postdoes not call the original procedure — it simply returns the conjunction of postconditions over the combined input+output parameters$postcall (along with the output variables after the call)Pipeline Integration
Both passes are integrated into
LaurelCompilationPipeline.lean, running after the existing Laurel-to-Laurel passes and before the final translation to Core.