feat(macro): support external calls in contract bodies - #2245
Conversation
…t/1003-external-call-body
…t/1003-external-call-body
…t/1003-external-call-body
…t/1003-external-call-body
…t/1003-external-call-body
…3-external-call-body
|
@codex review |
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_64828aaf-87f1-4a26-bfc8-609ee159bba2) |
![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: 86047a7c40
ℹ️ 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".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_1ebd808e-3d0f-49f1-9a23-68a7bf44bd1f) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 82e0dacf76
ℹ️ 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".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_f3492584-6922-42d2-93f1-10958ffa837a) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a0fc36bd96
ℹ️ 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".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_aac5618f-061d-441f-9c7b-9cbd14c80072) |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_e1b437d5-72bc-4493-a6df-9a1ec3bec8d5) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 219088e97f
ℹ️ 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".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_8f3c87a2-f97e-4b4f-afe6-15785cf7862b) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b01c8fd73a
ℹ️ 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".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_9a8039dc-5a67-4d7a-93ee-ce20318ad176) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 7318a33aab
ℹ️ 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".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_5e6f26db-3060-44fd-8634-8bcc845772ad) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b0772c63be
ℹ️ 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".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_254cede4-043c-4be2-9c88-65a4624252da) |
There was a problem hiding this comment.
💡 Codex Review
verity/Verity/Macro/Translate/Expr.lean
Lines 2178 to 2180 in 1d87201
Reject linked calls in mulDivUp's reused divisor
Fresh evidence beyond the existing duplicated-operand report is the mulDivUp path: when c contains callExternal, this arm accepts it, but Compiler/CompilationModel/ExpressionCompile.lean:629-640 substitutes the compiled divisor both into sub(c, 1) and as the final denominator. The external is consequently invoked twice and the numerator may be computed with a different value than the division; apply the same effectful-operand rejection used for ceilDiv and wDivUp.
ℹ️ 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".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_5114288f-4d02-4a24-b597-d2cdc6041e7a) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 59439b619f
ℹ️ 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".
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage + 0/3 paquet(s) reviewés sémantiquement. 5 finding(s) (1 medium / 4 low); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- Contracts/Smoke/ExternalCallInBodySmoke.lean — timeout (spawnSync ocr ETIMEDOUT)
- Verity/Macro/Translate/Expr.lean — timeout (spawnSync ocr ETIMEDOUT)
- Verity/Macro/Translate.lean — timeout (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 6 Lean file(s), 2358 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 5/8 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 5 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 8 supported / 8 total; Lean 6, trust docs 0, workflow/scripts 0, contracts 2, docs 0
- Changed lines: 2358 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 5; files 3; tokens 0; tool calls 0; warnings 1; duration 2412s
- Largest changed files: Verity/Macro/Translate/Expr.lean (+615/-310), Contracts/Smoke/ExternalCallInBodySmoke.lean (+664/-0), Verity/Macro/Translate.lean (+274/-143), artifacts/macro_property_tests/PropertyExternalCallInBodySmoke.t.sol (+293/-0), Verity/Macro/Syntax.lean (+26/-0)
Packet coverage
- Packet review: enabled; selected 5/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 5 scout-ranked packet(s); remaining changed hunks/files require Codex or human proof review, and selected packets still need strong reviewer analysis.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
- Covered packets:
- Contracts/Smoke/ExternalCallInBodySmoke.lean:1 score 86 [lenses: provenance, proof-soundness] — public declaration/signature changed, changed imports; ask: What mechanism binds every generated artifact derived from this smoke module—especially artifacts/macro_property_tests/PropertyExternalCallInBodySmoke.t.sol—to this exact Lean source, generator version, configuration, and complete artifact set, and would adding or swapping an unlisted Solidity artifact cause verification to fail?
- Verity/Macro/Translate/Expr.lean:3258 score 57 [lenses: proof-soundness] — large deleted proof obligation; ask: Compare every deleted and replacement branch in this window: do unsupported or effectful expressions still fail elaboration, and does each accepted external/linked call preserve arguments, return type, state effects, and failure behavior? Look specifically for fallbacks that now emit a literal, empty expression, or generic term instead of rejecting the source.
- Verity/Macro/Translate.lean:665 score 54 [lenses: proof-soundness] — large deleted proof obligation; ask: Trace the before/after lowering of safeTransfer and all newly supported external-call-in-body forms. Does each source operation produce the same or stronger compilation-model effects and validation obligations, with no branch that drops a statement, ignores a return value, or bypasses type/effect checks?
- Verity/Macro/Translate/Expr.lean:199 score 47 [lenses: proof-soundness] — public declaration/signature changed; ask: Verify that bitAnd with 255 or 65535 exactly matches the source and EVM semantics at every use of normalizeTranslatedExprForType. Should out-of-range values be truncated, rejected, or accompanied by a range obligation, and are literals, parameters, returns, storage writes, and external-call results treated consistently?
- Verity/Macro/Translate/Expr.lean:2797 score 46 [lenses: proof-soundness] — public declaration/signature changed; ask: Inspect all constructors and call sites of LinkedExternalLowerer. What invariant guarantees that lower and inferType describe the same external operation and return type? Can a caller provide a lowerer that emits a semantically unrelated term, omits effects, or reports a convenient type that suppresses a required rejection?
Pilot mode: advisory only. Codex Review remains the merge gate.
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_a97d42e3-2c6d-43c3-a6fc-c14e72760a66) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0a92c5a84b
ℹ️ 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".
| `(Compiler.CompilationModel.Expr.intrinsic "clz" | ||
| (Verity.Core.Intrinsics.YulLowering.verbatim 1 1 "1e") | ||
| Verity.Core.Intrinsics.HardFork.osaka | ||
| [$xExpr]) | ||
| | `(term| msb $x:term) => | ||
| let xExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals x visitingConstants | ||
| let xExpr ← translatePureExprWithTypes fields constDecls immutableDecls params locals x visitingConstants linkedExternalLowerer? |
There was a problem hiding this comment.
Although direct ite operands containing linked calls are rejected, msb (callExternal nextValue()) reaches this declaration-aware lowering and reuses xExpr in both the zero check and clzExpr. The synthesized Expr.ite is then compiled branchlessly and duplicates its condition at Compiler/CompilationModel/ExpressionCompile.lean:691-701, so the external is invoked three times and the zero check may inspect a different result from the value whose MSB is returned; bind the operand once or reject linked calls in msb.
Useful? React with 👍 / 👎.
| @@ -4048,7 +4191,7 @@ def tupleLiteralOrStructValueExprs? | |||
| let _ ← lookupStructMemberDecl fields fieldName memberName false | |||
| `(Compiler.CompilationModel.Expr.structMember | |||
| $(strTerm fieldName) | |||
| $(← translatePureExprWithTypes fields constDecls immutableDecls params locals key) | |||
| $(← translateExpr key) | |||
There was a problem hiding this comment.
When structMembers requests multiple fields and its key contains a linked call, for example structMembers records (callExternal nextKey()) ["a", "b"], this loop translates and embeds the key separately for every member. A stateful external is therefore invoked once per field, so the tuple can combine fields from different mapping entries while also repeating side effects; evaluate the key into one synthetic local before constructing the member expressions (and do the same for both structMembers2 keys).
Useful? React with 👍 / 👎.
1 participant
Summary
verity_contractbodiesreturnDataSize()in pure and bind contexts without a globalInhabited ContractinstanceDependency
Targets
feat/uint-narrow-typesand depends on #2240. Candidatec2ee709cdebad3c43c09c3ebf499275f1a33447ccontains live dependency headed5c9105c8649aeb4a183278d13adbb49e11bd04. No merge was performed.Validation
make check— pass (641 tests)81f9f4a0689fc21e1adfb6d903a8d3fc0ad51efe, focused job3e8fa70a-808b-45dd-8ba3-108dbf6a44bd, full job60870907-2fec-40e8-8f97-9e69342c902b, digeste6080dbef8c338a662ddc990dbb1dbf12ed0c4570cd4a02aac36eb608dbef605invalid remote build token; no older receipt is being treated as a current gateCloses #1003
Note
Medium Risk
Large changes to the contract macro translator affect all
verity_contractlowering; mistakes could miscompile external calls or accept unsafe nested effectful expressions, though coverage is heavy on smoke and guard regressions.Overview
Contract bodies can now use declaration-driven
callExternal,evmCall/evmStaticCall,memoryLoad/memoryStore,returnDataCopy, andreturnDataSize()(new syntax inVerity/Macro/Syntax.leanplus translation inTranslate.lean). Linked calls lower toexternalCallBind/ pureexternalCallwith bit/sign masks for narrow integer, address, bool, and bytes types;tryExternalCallbinds also get a bool success normalization assign (updated expectations inExternalCalls.lean).Translation routes most pure operands through
translateDeclaredPureExpr(withexternalDecls) so nested externals work in emits, ECM/ERC-20 helpers, ADT payloads, and statement binds;callExternalis validated for arity, void vs returning, and single-word binds. Fail-closed errors block effectfulcallExternalinside duplicated-expression contexts (conditionals,&&,safeAdd,min, transparent helpers, dynamic projections, etc.) and invalid memory/returndata operand types.Tests: new
ExternalCallInBodySmoke.lean(IRrflexamples, semantic-preservation proofs,#guard_msgsnegative cases) and import fromContracts/Smoke.lean.Reviewed by Cursor Bugbot for commit 0a92c5a. Bugbot is set up for automated code reviews on this repo. Configure here.