Add contract and transparency pass#16
Closed
keyboardDrummer wants to merge 329 commits into
Closed
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.
…nto issue-924-contract-and-proof-pass
keyboardDrummer
force-pushed
the
issue-924-contract-and-proof-pass
branch
from
da18905 to
3ce6673
Compare
github-actions
Bot
added
the
Git conflicts
Formatting improvements:
- Change block formatting to use indent(2) with newlines for vertical layout
instead of single-line '{ ... }' format
- Update semicolon separator to use newlines instead of spaces
Debugging improvements:
- Replace boolean 'coreProgramHasSuperfluousErrors' with 'coreDiagnostics' list
that records why the Core program was suppressed, enabling better error surfacing
- Add source location and reason parameters to 'invalidCoreType' for more
informative diagnostics
- Surface core diagnostics when no other diagnostics explain program suppression
- Add 'processLaurelFileKeepIntermediates' test helper for writing intermediate
pipeline files to Build/ directory
- Add Build/ to .gitignore
Test updates:
- Update all expected outputs to match new block formatting
- Add 'opaque' keyword to test procedures that need it for the new formatting
- Fix #guard_msgs whitespace formatting
Diagnostics with FileRange.unknown are not actionable for users and can arise from pre-existing resolution limitations (e.g., variables in multi-assign with field targets losing their uniqueId). Filter these out when surfacing suppression reasons to avoid spurious errors.
The CodeBuild source location was hardcoded to strata-org/Strata.git, which fails when the commit only exists in keyboardDrummer/Strata. Use github.server_url/github.repository so it resolves to the correct repo dynamically.
The CodeBuild project has credentials for strata-org/Strata only. On forks like keyboardDrummer/Strata, the job cannot access the source. Add an 'if' condition to skip the benchmark on non-upstream repos, and restore the hardcoded source URL that CodeBuild expects.
…gging-improvements # Conflicts: # Strata/Languages/Laurel/LaurelToCoreTranslator.lean
…t emitDiagnostic - Remove the FileRange.unknown filter in LaurelCompilationPipeline: all coreDiagnostics are now surfaced when no other diagnostics explain the suppression. - Remove default parameters from invalidCoreType, making source and reason explicit at every call site. - Remove redundant emitDiagnostic in the catch-all arm of translateType: invalidCoreType already records the diagnostic via coreDiagnostics.
Diagnostics without a known source location are not actionable for the user. Restore the filter that was removed in 0b6cee4 to fix the T1_MutableFields test failure.
…put params Key changes: - $post procedures are functional (isFunctional := true) - $post takes all inputs AND all outputs as parameters - $post does not call the original procedure — returns conjunction of postconditions over the combined input+output parameters - At call sites, input arguments are assigned to temporary variables; those temps are passed to both the actual call and the assumed $post call (along with the output variables after the call)
keyboardDrummer
force-pushed
the
issue-924-contract-and-proof-pass
branch
from
c6bfe97 to
87a87cd
Compare
github-actions
Bot
removed
GOTO
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
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.
Builds on:
No longer, maybe we can close this:
Summary
Add these passes:
returntoexitstatements, needed for the next pass.$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.The effect of the contract and transparency pass:
The combined effect of 2 and 4 is that there is no more difference between Laurel functions and transparent procedures.
TODO
FunctionsAndProofsProgramtoUnorderedCoreWithLaurelTypesandFunctionsAndProof.leantoTransparencyPass.leanFollow-up work