Improve executable ERC-4337 semantic stubs#1746
Improve executable ERC-4337 semantic stubs#1746Th0rgal wants to merge 14 commits intocodex/native-evmyullean-transitionfrom
Conversation
| \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: 57d47acd44
ℹ️ 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".
…public - Add `callOracle` field to `ContractState` (default: sum of args, matching `Env.defaultCallOracle`) so benchmarks can supply custom oracle functions for non-vacuous proofs. - Propagate `callOracle` through `Env.ofWorld` and `World.withEnv`. - Remove `private` from `forEach.loop` so external modules can add simp lemmas that reference it directly. - Update all proof files that construct explicit `ContractState` record literals to include the new `callOracle` field. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
- Regenerate PropertyHelperExternalArgumentSmoke.t.sol (tupleExternalArg and statementExternalArg removed since externalCall is now monadic) - Regenerate verification_status.json (core_lines count updated) - Replace native_decide with decide in EndToEnd.lean to satisfy hygiene check Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4c4c9c06ff
ℹ️ 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".
Add exec_block_append_error, exec_block_append_prefix_error, exec_nativeSwitchCaseIfs_prefix_hit_error_fuel, and simpleStorage_endToEnd_native_evmYulLean_of_callDispatcher_bridge to the proof length allowlist — structural per-constructor dispatch proofs where splitting would duplicate plumbing. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d74a460e50
ℹ️ 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".
…CatchWord - Make tryCatchWord polymorphic via TryCatchAttempt typeclass so it accepts both Contract Uint256 (inline call) and Uint256 (pre-bound variable) - Add let-mut macro rewrites for call/staticcall/delegatecall so mutable low-level call bindings desugar to monadic bind correctly - Add let-mut macro rewrites for externalCall for the same reason Addresses all 5 Codex review comments on PR #1746. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
decide times out on the large compiled-output proposition in simpleStorage_lowerRuntimeContractNative_ok. Revert to native_decide and add Compiler/Proofs/EndToEnd.lean to a native_decide allowlist in the hygiene check. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b6859954d9
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 7f0f993a05
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: de9377951c
ℹ️ 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".
…on' into codex/erc4337-faithful-model
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 60036151c7
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c047819040
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 779e38958b
ℹ️ 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".
…overage Extract `Verity.defaultCallOracle` as the single source of truth for the expression-position call oracle. Both `ContractState.callOracle` field default and `Env.defaultCallOracle` now delegate to it, eliminating silent drift between pure and state paths. Add bind-RHS `externalCall` macro rules in `Contracts/Common.lean` so that `let v ← f (externalCall …)` and the mutable variant route through the state-aware `externalCallWords` helper instead of the pure fallback. This closes a P1 gap surfaced in PR #1746 review where externalCall arguments inside bind RHS were inconsistently dispatched. Update pinned snapshots in `MacroTranslateInvariantTest.lean` to cover the new `helperExternalArgRhs`, `mutableExternalArg`, `catchComputedWord`, `mutableCallBinding`, and `callExpressionPosition` smoke entries that were silently drifting since b685995. Document the executable call-oracle dispatch caveat in `TRUST_ASSUMPTIONS.md` and record PR #1746 in `AUDIT.md`. Carry forward indentation hygiene fixes in five contract proof files and regenerate `verification_status.json`. Verified: `lake build` (Verity, Contracts, Compiler, PrintAxioms) and `make check` both pass. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 61c42c023c
ℹ️ 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".
| | `(doElem| let $name:ident := call $gas:term $target:term $value:term $inOffset:term $inSize:term $outOffset:term $outSize:term) => do | ||
| let callFn := Lean.mkIdentFrom name `_root_.Contracts.callM | ||
| `(doElem| let $name ← $callFn:ident $gas $target $value $inOffset $inSize $outOffset $outSize) | ||
| | `(doElem| let mut $name:ident := call $gas:term $target:term $value:term $inOffset:term $inSize:term $outOffset:term $outSize:term) => do | ||
| let callFn := Lean.mkIdentFrom name `_root_.Contracts.callM |
There was a problem hiding this comment.
Fresh evidence in this commit is that low-level calls were made monadic (call/staticcall/delegatecall) and only let/let mut forms are desugared here, but there is still no $var := call .../$var := staticcall .../$var := delegatecall ... rewrite. That means previously valid mutable reassignment patterns now fail on the executable path with a Contract Uint256 vs Uint256 mismatch, while the compilation-model translator still accepts these RHS forms as pure word expressions.
Useful? React with 👍 / 👎.
| | `(doElem| if call $gas:term $target:term $value:term $inOffset:term $inSize:term $outOffset:term $outSize:term == $rhs:term then $thenBranch:doSeq else $elseBranch:doSeq) => do | ||
| let callFn := Lean.mkIdentFrom target `_root_.Contracts.callM | ||
| `(doElem| do | ||
| let __verity_call_cond ← $callFn:ident $gas $target $value $inOffset $inSize $outOffset $outSize | ||
| if __verity_call_cond == $rhs then $thenBranch else $elseBranch) |
There was a problem hiding this comment.
This commit adds a special-case conditional rewrite for if call ... == ..., but staticcall and delegatecall were also changed to monadic values and have no equivalent condition rewrite. As a result, conditions like if staticcall ... == 0 then ... else ... (or delegatecall) now fail on the executable path because the condition contains a Contract Uint256, while the compilation-model path still treats them as pure expressions.
Useful? React with 👍 / 👎.
2 participants
Summary
forEachexecutable loop semantics with a realUint256index argumentexternalCall,call,staticcall, anddelegatecallthrough the existing environment oracle path instead of the old arithmetic/name-length stubstryCatchuse contract rollback semantics around the oracle-backed call attemptVerification
lake build Verity Contracts Compiler.CompilationModelFeatureTestNote
Medium Risk
Changes core executable semantics for low-level calls (
call/staticcall/delegatecall),tryCatch, andforEach, which can affect many tests and any contract relying on these stubs. Risk is mitigated by updated smoke/feature tests that assert the new oracle-dispatch and loop behavior.Overview
Updates the executable contract stubs to be oracle-backed and state-aware:
externalCall,call/staticcall/delegatecall, and ERC20 read helpers now dispatch throughContractState.callOracle(with a sharedVerity.defaultCallOracle) instead of arithmetic/name-length stand-ins.Makes low-level
tryCatchoperate viaContract.tryCatch(with rollback semantics) and extends macro support sodo-notation can bind/compare low-level call results andtryCatch (call ...)directly.Implements real executable
forEachloop semantics with aUint256index parameter, adds a semantic smoke test for per-index storage writes, and expands/adjusts smoke/property tests and proofs to accommodate monadic external-call results and the newcallOraclefield threading.Reviewed by Cursor Bugbot for commit 61c42c0. Bugbot is set up for automated code reviews on this repo. Configure here.