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: `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: 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 6e1354d4aa
ℹ️ 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".
…arded Tighten generated *_entrypoint predicates so Lean arguments must ABI-decode from the same CallbackContext.calldata compiled dispatch uses, and receive is registered only for empty calldata. Make selfCallCallee? monadic so syntax quotations type-check and hops keep the public/registry guard path.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4316953d29
ℹ️ 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. 4 finding(s) (4 medium); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- Verity/Proofs/Model/GeneratedEntrypointRegistry.lean — timeout (spawnSync ocr ETIMEDOUT)
- Verity/Macro/Translate.lean — timeout (spawnSync ocr ETIMEDOUT)
- TRUST_ASSUMPTIONS.md — timeout (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 11 Lean file(s), 1778 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 4/8 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 4 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 16 supported / 16 total; Lean 11, trust docs 1, workflow/scripts 1, contracts 2, docs 1
- Changed lines: 1778 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 4; files 3; tokens 0; tool calls 0; warnings 1; duration 2443s
- Largest changed files: Verity/Macro/Translate.lean (+558/-66), Verity/Proofs/Model/GeneratedEntrypointRegistry.lean (+403/-0), Verity/Core/Model/CallbackBridge.lean (+221/-5), artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol (+220/-0), Contracts/Smoke/SecurityCombos.lean (+138/-0)
Packet coverage
- Packet review: enabled; selected 4/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 4 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:
- Verity/Proofs/Model/GeneratedEntrypointRegistry.lean:1 score 86 [lenses: provenance, verification-independence, environment-determinism] — public declaration/signature changed, changed imports; ask: Does this generated registry (and the theorems that consume it) pin every macro-emitted, externally reachable state transformer, or can Translate/Elaborate add or swap a callable entrypoint/helper that is not listed here without breaking registration proofs?
- Verity/Macro/Translate.lean:3130 score 73 [lenses: provenance, verification-independence, environment-determinism] — introduced unsafe; ask: After this threading change, can the translator emit or rewrite an executable helper/entrypoint that is not named in GeneratedEntrypointRegistry (or any other pin the verifier hashes), and does unsafe let that happen without a trusted, replayable artifact identity?
- TRUST_ASSUMPTIONS.md:638 score 62 [lenses: provenance, verification-independence, environment-determinism] — trust-boundary docs drift; ask: Does the updated registry-completeness wording still match the artifacts the proofs actually pin, or does it now claim coverage of every reachable entrypoint while only a generated subset is listed/checked?
- TRUST_ASSUMPTIONS.md:490 score 62 [lenses: verification-independence, environment-determinism] — trust-boundary docs drift; ask: Which theorems still look like they verify external-call outcomes, and do they read stub tables emitted by the same compilation/macro path instead of independently re-deriving return words from an adversary model?
Pilot mode: advisory only. Codex Review remains the merge gate.
Bring in #2436 Pareto small fidelity gaps so the PR is no longer behind main.
The bot auto-refresh of PrintAxioms.lean did not match the Verify proofs path filter, so run 35485473453 completed as action_required with zero jobs. Include PrintAxioms.lean in the check-only path filter. Regenerate artifacts/trust_surface_report.json with the other derived artifacts so make check cannot fail on a stale trust-surface report after auto-refresh (the failure on 4316953).
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ef0321d654
ℹ️ 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".
Generated *_entrypoint predicates now constrain CallbackContext.calldata with abiEncodeDispatchArgs/ToDispatchVal (compiled-dispatch ABI), not ExternalArg.toWords. Registry executables rewrite calldatasize/calldataload to state-backed live ops so callbacks that branch on calldata are registered.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8904810852
ℹ️ 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 calldataloadLive (offset : Uint256) : Contract Uint256 := fun state => | ||
| ContractResult.success | ||
| (Verity.Core.Uint256.ofNat | ||
| (Compiler.CompilationModel.Denote.calldataloadWord 0 state.calldata offset.val)) |
There was a problem hiding this comment.
When a registered entrypoint branches on calldataload 0 (or an unaligned load overlapping the first four bytes), this hard-coded selector argument makes the registry executable observe zero, while compiled execution observes that entrypoint's actual function selector. The callback can therefore take a storage transition that is absent from entrypointRegistry. Fresh evidence beyond the earlier live-calldata finding is that the new adapter installs argument words but still calls calldataloadWord with literal selector 0; thread the selected entrypoint's selector through the callback context.
Useful? React with 👍 / 👎.
| instance [ToDispatchVal α] [ToDispatchVal β] : ToDispatchVal (α × β) where | ||
| toDispatchVal p := .tuple [ToDispatchVal.toDispatchVal p.1, ToDispatchVal.toDispatchVal p.2] |
There was a problem hiding this comment.
When an entrypoint takes a dynamic tuple with three or more members, such as Tuple [Uint256, String, Uint256], its Lean value is right-nested as Uint256 × (String × Uint256), and this recursive pair instance encodes it as the ABI type (uint256,(string,uint256)). The compiled parameter remains the flat source tuple (uint256,string,uint256), whose head offsets and tail layout differ, so actual callback calldata is excluded from the registry. Encode using the declared tuple member list or flatten the right-nested representation before producing DispatchVal.tuple.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage + 0/3 paquet(s) reviewés sémantiquement. 4 finding(s) (3 high / 1 medium); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- AUDIT.md — timeout (spawnSync ocr ETIMEDOUT)
- TRUST_ASSUMPTIONS.md — timeout (spawnSync ocr ETIMEDOUT)
- Verity/Proofs/Model/GeneratedEntrypointRegistry.lean — timeout (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 11 Lean file(s), 2108 changed supported line(s). Multi-lens scout (2/4 lens(es): verification-independence, environment-determinism) surfaced 4/8 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 4 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 22 supported / 22 total; Lean 11, trust docs 2, workflow/scripts 6, contracts 2, docs 1
- Changed lines: 2108 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 4; files 3; tokens 0; tool calls 0; warnings 1; duration 2471s
- Largest changed files: Verity/Macro/Translate.lean (+577/-71), Verity/Proofs/Model/GeneratedEntrypointRegistry.lean (+472/-0), Verity/Core/Model/CallbackBridge.lean (+382/-5), artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol (+220/-0), Contracts/Smoke/SecurityCombos.lean (+138/-0)
Packet coverage
- Packet review: enabled; selected 4/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness (2 lens(es) failed; union of the rest used); rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 4 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:
- AUDIT.md:772 score 142 [lenses: verification-independence] — introduced sorry/admit, trust-boundary docs drift; ask: What command actually validates generated registry ABI calldata, and does it re-derive encoding from the Lean/Solidity signature with a verifier-owned encoder, or hash/compare bytes the producer already wrote into the entrypoint predicates?
- AUDIT.md:623 score 137 [lenses: verification-independence, environment-determinism] — introduced/changed axiom, trust-boundary docs drift; ask: For each generate_* --check path touched by this PR (including any new axiom/registry row), is the checker a distinct implementation, or does it import the same generator and treat reproduced output as independent verification?
- TRUST_ASSUMPTIONS.md:649 score 118 [lenses: verification-independence] — introduced unsafe, trust-boundary docs drift; ask: Does the updated trust-boundary text claim independent/machine-checked registry completeness, and if so what verifier re-derives the reachable-entrypoint set without trusting ReentrancySpec.entrypoints or GeneratedEntrypointRegistry output?
- Verity/Proofs/Model/GeneratedEntrypointRegistry.lean:1 score 86 [lenses: verification-independence] — public declaration/signature changed, changed imports; ask: Does this file independently reconstruct entrypoint selectors, ABI words, and adversary wiring from the contract source, or does a buggy Translate/CallbackBridge generator still 'prove' guardedPing_registered / *SeesAdversary because the verifier executes the producer-emitted expansions?
Pilot mode: advisory only. Codex Review remains the merge gate.
| - Trust docs: `TRUST_ASSUMPTIONS.md` (executable-plane stubs are closed | ||
| definitions; registry completeness remains an author obligation). | ||
| - Axiom-free; no `sorry`/`admit`/`native_decide`. | ||
|
|
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| | `artifacts/evmyullean_capability_report.json` | EVMYulLean capability surface and reference-oracle paths | `python3 scripts/generate_evmyullean_capability_report.py --check` | | ||
| | `artifacts/storage_layout_report.json` + `artifacts/STORAGE_LAYOUT_SUMMARY.md` | Per-contract storage layout for migration/audit review: explicit slots, alias ranges, reserved ranges, packed subfields, mappings, dynamic arrays, opt-in namespaces (#1897) | `python3 scripts/generate_storage_layout_report.py --check --no-lean` (drift gate in `make check`); regenerate with `make regen-storage-layout-report` | | ||
| | `PrintAxioms.lean` / generated axiom report | Axiom dependency visibility | `python3 scripts/generate_print_axioms.py --check` and `lake build PrintAxioms` | | ||
| | `PrintAxioms.lean` / generated axiom report | Axiom dependency visibility | `python3 scripts/generate_print_axioms.py --check` and `lake build PrintAxioms`. `PrintAxioms.lean` is a Verify proofs path-filter so bot auto-refresh of that file still runs `checks`. The checks job regenerates `artifacts/trust_surface_report.json` with the other derived artifacts so `make check` cannot fail on a stale trust-surface report after auto-refresh. | |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| Existing `unsafe qualifiedTupleBindTypedLocals` is elaborator-only | ||
| typed-local inference, not a kernel skip. | ||
| Author-supplied lists remain only for hand-written `ReentrancySpec` | ||
| consumers. |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| hbound.denoteCall_preserves_registry (fun _ => True) | ||
| GeneratedRegistry.entrypointRegistry hregistry site state trivial | ||
|
|
||
| end Contracts.ReentrancyRelyGuarantee |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Generated *_entrypoint predicates encode args with ToDispatchVal. Named/nested struct parameters (FeeConfig, Outer, Array Transaction) had no instance, so lake build Contracts.Smoke.StructsAndArrays failed in Verify proofs. Emit a tuple-of-fields instance next to ExternalArg.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1016f43d59
ℹ️ 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.
OpenCodeReview first-pass review
🟡 Scout triage + 0/3 paquet(s) reviewés sémantiquement. 4 finding(s) (3 high / 1 medium); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- AUDIT.md — timeout (spawnSync ocr ETIMEDOUT)
- TRUST_ASSUMPTIONS.md — timeout (spawnSync ocr ETIMEDOUT)
- Verity/Proofs/Model/GeneratedEntrypointRegistry.lean — timeout (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 11 Lean file(s), 2125 changed supported line(s). Multi-lens scout (2/4 lens(es): provenance, verification-independence) surfaced 4/8 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 4 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 22 supported / 22 total; Lean 11, trust docs 2, workflow/scripts 6, contracts 2, docs 1
- Changed lines: 2125 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 4; files 3; tokens 0; tool calls 0; warnings 1; duration 2483s
- Largest changed files: Verity/Macro/Translate.lean (+592/-71), Verity/Proofs/Model/GeneratedEntrypointRegistry.lean (+472/-0), Verity/Core/Model/CallbackBridge.lean (+382/-5), artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol (+220/-0), Contracts/Smoke/SecurityCombos.lean (+138/-0)
Packet coverage
- Packet review: enabled; selected 4/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness (2 lens(es) failed; union of the rest used); rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 4 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:
- AUDIT.md:772 score 142 [lenses: provenance, verification-independence] — introduced sorry/admit, trust-boundary docs drift; ask: Is the generated ABI-calldata encoding and the full set of *_entrypoint predicates pinned by a content-addressed manifest that an independent verifier replays, or is this section documenting producer output that is not fully covered by verify_sync_spec / trust_surface_report checks?
- AUDIT.md:623 score 137 [lenses: provenance, verification-independence] — introduced/changed axiom, trust-boundary docs drift; ask: Does the updated Audit Artifacts row (and its --check command) content-hash every artifact the new registry/guard trust claim depends on, or does it still pin only a subset of JSON reports such that Translate.lean / GeneratedEntrypointRegistry.lean / artifacts/macro_property_tests/* can change without failing the manifest?
- TRUST_ASSUMPTIONS.md:649 score 118 [lenses: provenance, verification-independence] — introduced unsafe, trust-boundary docs drift; ask: Does any checksum or sync-spec entry pin the generated entrypoints list that this completeness obligation refers to (Lean registry + CallbackBridge + property-test artifacts), or can a producer omit/swap an externally reachable transformer without invalidating the trust-surface manifest?
- Verity/Proofs/Model/GeneratedEntrypointRegistry.lean:1 score 86 [lenses: provenance, verification-independence] — public declaration/signature changed, changed imports; ask: Which manifest/checksum, if any, pins the exact bytes of GeneratedEntrypointRegistry.lean (and the entrypoints/linked_externals it declares), and would adding another generated function or swapping ping still keep verify_sync_spec and trust_surface_report green?
Pilot mode: advisory only. Codex Review remains the merge gate.
| - Trust docs: `TRUST_ASSUMPTIONS.md` (executable-plane stubs are closed | ||
| definitions; registry completeness remains an author obligation). | ||
| - Axiom-free; no `sorry`/`admit`/`native_decide`. | ||
|
|
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| | `artifacts/evmyullean_capability_report.json` | EVMYulLean capability surface and reference-oracle paths | `python3 scripts/generate_evmyullean_capability_report.py --check` | | ||
| | `artifacts/storage_layout_report.json` + `artifacts/STORAGE_LAYOUT_SUMMARY.md` | Per-contract storage layout for migration/audit review: explicit slots, alias ranges, reserved ranges, packed subfields, mappings, dynamic arrays, opt-in namespaces (#1897) | `python3 scripts/generate_storage_layout_report.py --check --no-lean` (drift gate in `make check`); regenerate with `make regen-storage-layout-report` | | ||
| | `PrintAxioms.lean` / generated axiom report | Axiom dependency visibility | `python3 scripts/generate_print_axioms.py --check` and `lake build PrintAxioms` | | ||
| | `PrintAxioms.lean` / generated axiom report | Axiom dependency visibility | `python3 scripts/generate_print_axioms.py --check` and `lake build PrintAxioms`. `PrintAxioms.lean` is a Verify proofs path-filter so bot auto-refresh of that file still runs `checks`. The checks job regenerates `artifacts/trust_surface_report.json` with the other derived artifacts so `make check` cannot fail on a stale trust-surface report after auto-refresh. | |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| Existing `unsafe qualifiedTupleBindTypedLocals` is elaborator-only | ||
| typed-local inference, not a kernel skip. | ||
| Author-supplied lists remain only for hand-written `ReentrancySpec` | ||
| consumers. |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| hbound.denoteCall_preserves_registry (fun _ => True) | ||
| GeneratedRegistry.entrypointRegistry hregistry site state trivial | ||
|
|
||
| end Contracts.ReentrancyRelyGuarantee |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
…lldata helpers Fix four Codex P1s on #2406: live calldataload observes CallbackContext.selector, FixedArray/Tuple DispatchVal matches genParamLoads, dispatchCalldataMatchesKinds accepts genScalarLoad-normalized words, and calldata-reading helpers go through *_registry. Tests in GeneratedEntrypointRegistry. Completeness remains an author obligation.
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage + 0/3 paquet(s) reviewés sémantiquement. 4 finding(s) (3 high / 1 medium); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- AUDIT.md — timeout (spawnSync ocr ETIMEDOUT)
- TRUST_ASSUMPTIONS.md — timeout (spawnSync ocr ETIMEDOUT)
- Verity/Proofs/Model/GeneratedEntrypointRegistry.lean — timeout (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 12 Lean file(s), 2497 changed supported line(s). Multi-lens scout (1/4 lens(es): provenance) surfaced 4/8 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 4 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 23 supported / 23 total; Lean 12, trust docs 2, workflow/scripts 6, contracts 2, docs 1
- Changed lines: 2497 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 4; files 3; tokens 0; tool calls 0; warnings 1; duration 2486s
- Largest changed files: Verity/Macro/Translate.lean (+721/-71), Verity/Proofs/Model/GeneratedEntrypointRegistry.lean (+616/-0), Verity/Core/Model/CallbackBridge.lean (+464/-5), artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol (+220/-0), Contracts/Smoke/SecurityCombos.lean (+138/-0)
Packet coverage
- Packet review: enabled; selected 4/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness (3 lens(es) failed; union of the rest used); rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 4 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:
- AUDIT.md:772 score 142 [lenses: provenance] — introduced sorry/admit, trust-boundary docs drift; ask: Are the generated *_entrypoint predicates and their ABI encodings listed and content-hashed by the same manifests/checks this section relies on, or can Translate/Elaborate add another generated entrypoint artifact that AUDIT claims are covered but no checksum pins?
- AUDIT.md:623 score 137 [lenses: provenance] — introduced/changed axiom, trust-boundary docs drift; ask: After this table change, does every artifact the verifier/proofs depend on (including GeneratedEntrypointRegistry.lean, artifacts/macro_property_tests/*, artifacts/trust_surface_report.json, and verify_sync_spec) have a Check that hashes file contents—not a directory listing—and fail-closed if an unlisted file is added or swapped?
- TRUST_ASSUMPTIONS.md:649 score 118 [lenses: provenance] — introduced unsafe, trust-boundary docs drift; ask: Does the updated trust-boundary text require a content-pinned, complete entrypoint manifest that is checked against generated code, or can a producer add a reachable transformer that is missing from ReentrancySpec.entrypoints without invalidating any checksum?
- Verity/Proofs/Model/GeneratedEntrypointRegistry.lean:1 score 86 [lenses: provenance] — public declaration/signature changed, changed imports; ask: Is this generated file (and the new artifacts/macro_property_tests/*.sol siblings) fully content-pinned by scripts/verify_sync_spec.json and refresh_verification_artifacts.sh, or can the macro producer emit additional entrypoints/helpers that never appear in those manifests?
Pilot mode: advisory only. Codex Review remains the merge gate.
| - Trust docs: `TRUST_ASSUMPTIONS.md` (executable-plane stubs are closed | ||
| definitions; registry completeness remains an author obligation). | ||
| - Axiom-free; no `sorry`/`admit`/`native_decide`. | ||
|
|
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| | `artifacts/evmyullean_capability_report.json` | EVMYulLean capability surface and reference-oracle paths | `python3 scripts/generate_evmyullean_capability_report.py --check` | | ||
| | `artifacts/storage_layout_report.json` + `artifacts/STORAGE_LAYOUT_SUMMARY.md` | Per-contract storage layout for migration/audit review: explicit slots, alias ranges, reserved ranges, packed subfields, mappings, dynamic arrays, opt-in namespaces (#1897) | `python3 scripts/generate_storage_layout_report.py --check --no-lean` (drift gate in `make check`); regenerate with `make regen-storage-layout-report` | | ||
| | `PrintAxioms.lean` / generated axiom report | Axiom dependency visibility | `python3 scripts/generate_print_axioms.py --check` and `lake build PrintAxioms` | | ||
| | `PrintAxioms.lean` / generated axiom report | Axiom dependency visibility | `python3 scripts/generate_print_axioms.py --check` and `lake build PrintAxioms`. `PrintAxioms.lean` is a Verify proofs path-filter so bot auto-refresh of that file still runs `checks`. The checks job regenerates `artifacts/trust_surface_report.json` with the other derived artifacts so `make check` cannot fail on a stale trust-surface report after auto-refresh. | |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| Existing `unsafe qualifiedTupleBindTypedLocals` is elaborator-only | ||
| typed-local inference, not a kernel skip. | ||
| Author-supplied lists remain only for hand-written `ReentrancySpec` | ||
| consumers. |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| hbound.denoteCall_preserves_registry (fun _ => True) | ||
| GeneratedRegistry.entrypointRegistry hregistry site state trivial | ||
|
|
||
| end Contracts.ReentrancyRelyGuarantee |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 12 Lean file(s), 2503 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 24 supported / 24 total; Lean 12, trust docs 2, workflow/scripts 7, contracts 2, docs 1
- Changed lines: 2503 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Verity/Macro/Translate.lean (+721/-71), Verity/Proofs/Model/GeneratedEntrypointRegistry.lean (+616/-0), Verity/Core/Model/CallbackBridge.lean (+464/-5), artifacts/macro_property_tests/PropertyNonreentrantQualifiedHelperResolution.t.sol (+220/-0), Contracts/Smoke/SecurityCombos.lean (+138/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; 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: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- 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.
Pilot mode: advisory only. Codex Review remains the merge gate.
Resolve Translate.lean by threading both registryMode (PR) and returnTys / G23 getter / G15 deferred-link handling (main); keep AUDIT.md deletion from main (PR content lives in docs/TRUST_ASSUMPTIONS.md); keep PrintAxioms.lean / artifacts/* CI triggers and trust-surface regen from PR on main's path lists. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…hreaded helper calls (merge of main into #2406) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
Merged current main (600014d) into this branch. Conflicts were resolved keeping main's behaviour (#2458 runtime-target dispatch, #2459 mapChain), and b25e902 threads the new Review nits (not blocking):
🤖 Generated with Claude Code |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b25e90298a
ℹ️ 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 dispatchCalldataMatches (ctx : CallbackContext) (argWords : List Nat) : Prop := | ||
| dispatchWordsMatch | ||
| (List.replicate argWords.length ScalarLoadKind.identity) | ||
| argWords (ctx.calldata.take argWords.length) = true ∧ | ||
| Verity.Core.Uint256.ofNat (4 + 32 * argWords.length) ≤ ctx.calldataSize |
There was a problem hiding this comment.
When a callback uses a valid noncanonical dynamic layout, this exact prefix comparison excludes the execution even though genDynamicParamLoads accepts it. For example, a Bytes argument may use offset 64 with a padding word instead of the canonical offset 32; an entrypoint that branches on calldataload 4 then observes 64 in compiled execution, but no matching registry context exists because argWords contains 32. Model the loader's offset and bounds relation rather than requiring canonical re-encoding.
Useful? React with 👍 / 👎.
| | .uintN bits => | ||
| `(Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind.uintN $(natTerm bits)) | ||
| | .address => `(Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind.address) | ||
| | .bytesN bytes => | ||
| `(Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind.bytesN $(natTerm bytes)) | ||
| | _ => `(Compiler.CompilationModel.DenoteExternalCalls.ScalarLoadKind.identity) |
There was a problem hiding this comment.
When an entrypoint accepts IntN bits, this fallback assigns identity, while compiled dispatch applies signextend. For example, raw Int8 calldata 0xff becomes the Lean value -1, whose ToDispatchVal word is 2^256 - 1; identity comparison rejects the raw 0xff, so a real callback transition can be absent from the registry. Add an intN load kind implementing the same sign extension as genScalarLoad.
Useful? React with 👍 / 👎.
| | .array elemTy => do | ||
| `(term| Compiler.CompilationModel.DenoteExternalCalls.DispatchVal.array | ||
| (($value).toList.map (fun x => | ||
| Compiler.CompilationModel.DenoteExternalCalls.ToDispatchVal.toDispatchVal | ||
| (x : $(← contractValueTypeTerm elemTy))))) |
There was a problem hiding this comment.
When a parameter is an Array of FixedArray, this branch erases the declared fixed-array shape and invokes the generic Array instance for each element. That marks every fixed array as a dynamic array and inserts an element length word and offsets, whereas compiled ABI dispatch decodes fixed-array elements inline without those lengths. Consequently canonical calldata for types such as FixedArray Uint256 2[] cannot satisfy the generated registry predicate; encode each element via dispatchValTermForType elemTy.
Useful? React with 👍 / 👎.
| let usesScalarNorm := fn.params.any fun p => | ||
| match p.ty with | ||
| | .bool | .uint8 | .uint16 | .uintN _ | .address | .bytesN _ => true | ||
| | _ => false |
There was a problem hiding this comment.
When a normalized scalar is nested inside a tuple, fixed array, or struct, this top-level type check selects the exact matcher instead of the compiler's scalar normalization. For example, Tuple [Bool, Uint256] calldata containing raw Bool word 2 is accepted and normalized to true by genStaticTypeLoads, but the registry compares it against canonical word 1 and omits the real callback. Moreover, mixing a multiword composite with a top-level normalized scalar produces only one kind per parameter rather than per encoded word, misaligning later kinds; derive a recursively flattened kind list matching argWords.
Useful? React with 👍 / 👎.
| registryBody ← | ||
| `(∃ $context:ident : | ||
| Compiler.CompilationModel.DenoteExternalCalls.CallbackContext, | ||
| $registryBody) |
There was a problem hiding this comment.
The new selector field fixes live reads, but this existential context is not constrained to the selector of the entrypoint whose predicate is being generated. Thus a function that branches on calldataload 0 is registered under every arbitrary selector, including selectors that could never dispatch to it, and RegistryPreserves requires proofs for impossible transitions. Bind regular functions to their computed selector and bind receive to selector zero while retaining unconstrained selectors only for fallback dispatch.
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