feat: expand proven fragment with assignStorage constructors#1732
feat: expand proven fragment with assignStorage constructors#1732
Conversation
) Add `assignStorageField` and `assignStorageAddrField` constructors to `SupportedStmtList`, extending the proven fragment to cover `assignVar` with `Expr.storage` and `Expr.storageAddr` — mirroring the existing `letStorageField` / `letStorageAddrField` constructors. Each constructor includes: - Full `compiledStmtStep_*` proof in GenericInduction.lean - Singleton wrapper and surface bridge theorems - Match cases in all 3 assembly chain theorems - Helper surface closed theorems and 5 match cases in SupportedSpec.lean Zero new sorries. Lean hygiene check passes. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
| \n### CI Failure Hints\n\nFailed jobs: `build`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1023eea583
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| def mkViewTheoremCommand (fnDecl : FunctionDecl) : CommandElabM Cmd := do | ||
| let viewName ← mkSuffixedIdent fnDecl.ident "_is_view" | ||
| let modelName ← mkSuffixedIdent fnDecl.ident "_model" |
There was a problem hiding this comment.
_is_view helper names in name validation
mkViewTheoremCommand now generates a declaration named <function>_is_view, but validateGeneratedDefNamesPublic still only reserves _modelBody, _model, _bridge, and _semantic_preservation. That means a contract can pass validation with a user declaration like currentOwner_is_view and then fail later during elaboration when this theorem is emitted as a duplicate declaration. Please add _is_view to the generated-name collision checks so this is caught deterministically at validation time.
Useful? React with 👍 / 👎.
2 participants
Summary
assignStorageFieldandassignStorageAddrFieldconstructors toSupportedStmtList, coveringStmt.assignVarwithExpr.storage/Expr.storageAddrreadsletStorageField/letStorageAddrFieldconstructors (same semantics viabindValue, only IR instruction differs:assignvslet_)Closes #1723 (partial — first two constructors of many needed)
Test plan
lake buildpasses (full project, 99/100 modules)python3 scripts/check_lean_hygiene.pypasses (0 sorries, 0 debug commands)🤖 Generated with Claude Code
Note
Medium Risk
Medium risk because it expands the proven supported-statement fragment and updates source semantics/spec “unsupported surface” classifiers (including
emit), which can affect what programs are considered provable/executable under the proof framework.Overview
Extends the proven supported statement fragment to cover
Stmt.assignVarthat reads from storage viaExpr.storageandExpr.storageAddr, including new compilation-step proofs that these compile tosloadand preserve the source/IR state relation.Adds minimal source semantics for
Stmt.emit(evaluate args; no state change) and threadsemitthrough the various “unsupported surface” predicates and related lemmas/induction machinery, including a small refactor to factor outstmtTouchesUnsupportedCallSurface_eq_featureOr.Adds macro generation of per-function
@[simp]theorems*_is_viewfor view functions, a newviewPreservesStateframe predicate, and a smoke test that references an auto-generated_is_viewtheorem to ensure it is emitted.Reviewed by Cursor Bugbot for commit 1023eea. Bugbot is set up for automated code reviews on this repo. Configure here.