proof(reentrancy): generate guarded entrypoint registry - #2406
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
|
@codex review |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
| \n### CI Failure Hints\n\nFailed jobs: `compiler-regressions`\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: ed2b7c089e
ℹ️ 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".
| let fnExecutableBody ← match fn.nonReentrantLock with | ||
| | some lockIdent => | ||
| let lockName := toString lockIdent.getId | ||
| let some lockField := fields.find? (fun field => field.name == lockName) | ||
| | throwErrorAt lockIdent s!"unknown nonreentrant lock field '{lockName}'" | ||
| `(Verity.Core.NonReentrantGuard.guarded $(natTerm lockField.slotNum) $fnExecutableBody) |
There was a problem hiding this comment.
When the transient lock contains a nonzero value other than 1, wrapping the executable with NonReentrantGuard.guarded makes the source execution revert, because that helper accepts only 0; the compiled guard in nonReentrantGuardPrologue, however, reverts only when tload(slot) == 1 and otherwise executes the function. Since transient storage can be written directly and ContractState permits arbitrary values, this introduces a source/compiled semantic mismatch and can make registry proofs claim a call is blocked when the emitted EVM code allows it.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d51100ab7a
ℹ️ 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".
| let lockName := toString lockIdent.getId | ||
| let some lockField := fields.find? (fun field => field.name == lockName) | ||
| | throwErrorAt lockIdent s!"unknown nonreentrant lock field '{lockName}'" | ||
| `(Verity.Core.NonReentrantGuard.guarded $(natTerm lockField.slotNum) $fnExecutableBody) |
There was a problem hiding this comment.
When a nonreentrant(lock) reentrancy_trusted entrypoint is invoked from another entrypoint guarded by the same lock, this wrapper also runs for the Lean executable's internal call, sees the outer call's held lock, and reverts the entire execution. The compiled path deliberately lowers that call to the lock-free internal-helper shadow (as documented in mkSpecCommand and exercised by NonreentrantTrustedInternalHelperAccepted), so the emitted contract executes the callee instead. Generate separate guarded external and unguarded internal executable definitions, or rewrite internal calls to an unguarded shadow.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d946bdf145
ℹ️ 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".
| | some helper => | ||
| let target ← | ||
| if helper.nonReentrantLock.isSome && helper.reentrancyTrusted then | ||
| mkSuffixedIdent name "_unguarded" |
There was a problem hiding this comment.
When a nonreentrant(lock) reentrancy_trusted entrypoint with no external calls is invoked from another entrypoint guarded by the same lock, it is absent from adversarialHelpers, so threadHelperApp? never selects this new _unguarded target and the executable still calls the guarded public definition. The inner call therefore sees the outer lock and reverts, while compilation lowers it to the unguarded internal-helper shadow and executes it. Fresh evidence beyond the prior comment is that the fix performs this rewrite only after finding the callee in adversarialHelpers, leaving no-call trusted callees unchanged.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: d7cd60058b
ℹ️ 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".
|
@codex review |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e55fba5f8a
ℹ️ 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".
| match elem with | ||
| | `(doElem| let $name:ident := $rhs:term) => infer name rhs | ||
| | `(doElem| let mut $name:ident := $rhs:term) => infer name rhs | ||
| | `(doElem| let $name:ident ← $rhs:term) => |
There was a problem hiding this comment.
When a guarded/trusted overloaded helper is called using a value introduced by supported tuple destructuring, such as let (x, y) ← makePair ...; let z ← overloadedTrusted x, this collector does not match the tuple binding, so x never enters locals. resolveLocalFunctionApp? then cannot infer the argument type, its exception is converted to none, and executable rewriting leaves the call at its unmangled source name even though the selected overload is emitted as a mangled _unguarded definition, causing contract elaboration to fail. Fresh evidence beyond the prior local-type comment is that the new collector handles only $name:ident binders while the main translator explicitly supports tuple bind patterns.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 22ee53c7bf
ℹ️ 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".
|
@codex review Current head: |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 22ee53c7bf
ℹ️ 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".
| match ← inferTupleSourceTypes? fields constDecls immutableDecls externalDecls | ||
| helpers params scope rhs with |
There was a problem hiding this comment.
When a tuple is destructured from a qualified helper and one of its bindings is later passed to an overloaded guarded or adversarial local helper, inferTupleSourceTypes? returns none because it only resolves local helper applications. The validation walk explicitly handles qualified tuple calls via resolveQualifiedFunctionApp?, so this is accepted source, but the executable rewrite drops the bound types; overload resolution then fails and leaves the call unmangled and unthreaded, causing elaboration to fail. Extend this collector with the same qualified-tuple handling used by validation.
Useful? React with 👍 / 👎.
|
@codex review Please review exact head aa806ce, which fixes the two current-head findings by recursively traversing non-exact qualified helper applications and tracking synthesized Uint256 loop binders during overload rewriting. Focused family regressions cover a nested linked external call plus trusted/adversarial overloads across forEach and forEachSetBit. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: aa806ce13f
ℹ️ 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".
|
@codex review Please review exact head 9cf62cb. This head addresses every unresolved, non-outdated Codex thread from aa806ce, including explicit-adversary registry executables for static-call-dependent state, exact nonreentrant sentinel semantics, callback frame context/restore, generated-name and include-alias hygiene, and nested/qualified/typed helper rewriting. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 9cf62cb584
ℹ️ 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: 01b17a9f34
ℹ️ 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: ded1d3155b
ℹ️ 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".
| let mut registryBody : Term ← | ||
| `(($transition:ident : Verity.ContractState → Verity.ContractState) = | ||
| Compiler.CompilationModel.DenoteExternalCalls.callbackTransition | ||
| $context:ident ($applied).runState) |
There was a problem hiding this comment.
For every nonpayable function, the existential CallbackContext can choose a nonzero msgValue, yet this predicate invokes the executable body directly and registers the resulting transition. The compiled dispatcher installs callvalueGuard for such functions and reverts before executing that body, so the registry admits impossible storage and balance transitions and can make RegistryPreserves obligations fail for behavior that cannot occur. Restrict nonpayable entries to zero-value contexts or model the dispatch revert before applying the function.
Useful? React with 👍 / 👎.
|
@codex review Please review exact head c7e0fa6. This successor preserves callback success/revert outcomes through the generated registry so reverted callbacks roll back their value credit, and restricts generated nonpayable entrypoints to zero-value callback contexts. Scope remains AdversaryModel PR4 only. |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c7e0fa6d09
ℹ️ 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".
| matchesExactHelper helper then | ||
| mkSuffixedIdent helper.ident "_unguarded" | ||
| else | ||
| pure name |
There was a problem hiding this comment.
When an overloaded local helper opens an external-call window but is not a guarded/trusted helper, overload resolution succeeds and the adversary is added, but this branch retains the source identifier (for example, foo adv x). Overloaded definitions are emitted under mangled helper.ident names, so a valid caller of a CEI-compliant overload that returns an external-call result fails during Lean elaboration. Fresh evidence beyond the earlier guarded-overload finding is that this non-guarded adversarial path still falls through to the unmangled name; use the resolved identifier here as well.
Useful? React with 👍 / 👎.
| match ← threadHelperApp? fields constDecls immutableDecls externalDecls | ||
| helpers adversarialHelpers registryOnlyHelpers params locals name rewrittenArgs adv with |
There was a problem hiding this comment.
When a parenthesized call to an overloaded guarded or adversarial helper contains a nested external call, such as overloadedTrusted(externalCall "echo" [x]), the arguments are first replaced with fresh temporary identifiers and only then passed to overload resolution. Those generated temporaries are absent from locals, so type inference fails, the exception fallback leaves the unmangled and unthreaded source call in place, and the otherwise valid contract fails elaboration because only mangled helper definitions exist. Resolve against the original arguments before hoisting, or add the generated temporaries and their result types to the resolution environment.
Useful? React with 👍 / 👎.
1 participant
Summary
nonreentrantexecutable entrypoints withNonReentrantGuard.guardedCallbackBoundedand consume that boundary inReentrancyRelyGuaranteeScope
This is PR4 in the ordered
AdversaryModelmigration. It does not add PR5 trusted-reentrancy reporting or PR6 lint/docs, and it does not widen Yul bindings, add mutual recursion, refine read-only reentrancy, or remove executable semantics.The new focused consumer contains the minimum external-call contract required to establish registry/guard semantics; no existing contract source is changed.
Validation
Exact-head SHA
f036c9b3dd1016c1bd547224ae1bd98c53980212oncodex/adversary-model-pr4-registryvsorigin/main5e602b335278f309b3939ea6fc9dfee9668aff64.Verify proofs run 34136052552 success:
checks101787544195build(lake build+ PrintAxioms prebuild) 101787999848build-audits(PrintAxioms/trust, axiom report PASS, 4966 theorems) 101794182871build-compiler-binaries101794182787compiler-audits(Yul/parity/gas) 101796260914compiler-regressions101796261001foundryshards 0–3 101796260933 / 101796260947 / 101796260946 / 101796260952foundry-patched101796260989foundry-gas-calibration101796260863Local/static:
make check(666 script tests; all audits passed)git diff --check origin/main...HEADsorry,admit,axiom, orunsafeContracts/**ortest//foundry.tomldiff againstorigin/main