feat: first-class modifiers and single inheritance (#2087) - #2247
feat: first-class modifiers and single inheritance (#2087)#2247Th0rgal wants to merge 22 commits into
Conversation
|
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_281230ca-7518-4b58-b0df-0ed86f2cd454) |
![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: 42c1c6ea6d
ℹ️ 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".
| \n### CI Failure Hints\n\nFailed jobs: `build-compiler-binaries`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
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_12134abc-7e73-431c-9b95-65cda2729f2c) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 699c553ebb
ℹ️ 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 low); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- Verity/Macro/Translate.lean — timeout (spawnSync ocr ETIMEDOUT)
- artifacts/macro_property_tests/PropertyModifierInheritanceBase.t.sol — timeout (spawnSync ocr ETIMEDOUT)
- Verity/Macro/Translate/Parsing.lean — timeout (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 6 Lean file(s), 389 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: 11 supported / 11 total; Lean 6, trust docs 0, workflow/scripts 0, contracts 1, docs 4
- Changed lines: 389 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 2389s
- Largest changed files: Verity/Macro/Translate.lean (+185/-20), Verity/Macro/Translate/Parsing.lean (+47/-1), Contracts/Smoke/Helpers.lean (+39/-0), artifacts/macro_property_tests/PropertyModifierInheritanceBase.t.sol (+26/-0), docs/MODIFIERS_AND_INHERITANCE.md (+26/-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/Macro/Translate.lean:2705 score 53 [lenses: verification-independence, proof-soundness] — public declaration/signature changed; ask: Which checks of inheritance and modifier behavior re-derive expected parent resolution, storage offsets, constructor arguments, and method specialization without importing or invoking these translation/flattening routines or consuming their generated outputs? Identify every supposedly independent verifier that shares ParsedContractSyntax or downstream producer state.
- artifacts/macro_property_tests/PropertyModifierInheritanceBase.t.sol:1 score 31 [lenses: provenance, verification-independence, environment-determinism] — changed imports; ask: Is there a trusted manifest or reproducible generation check that content-hashes every dependency of this test—the exact Helpers.lean source revision, generator/toolchain, generated Solidity file, YulTestBase.sol, and the deployed ModifierInheritanceBase Yul artifact—and does it reject added, omitted, or substituted artifacts rather than merely checking a listed subset?
- Verity/Macro/Translate/Parsing.lean:520 score 14 [lenses: proof-soundness] — hotspot path/churn; ask: Does dispatch validation reject every invalid virtual/override configuration—duplicates, override without a matching parent function, signature mismatch, overriding non-virtual functions, and ambiguous inherited targets—and is the validated target the same implementation used by both semantic translation and the proof model?
- Verity/Macro/Translate.lean:2974 score 14 [lenses: environment-determinism, proof-soundness] — hotspot path/churn; ask: Trace
defaultStorageNamespaceEnabledto its configuration source: can environment variables, command-line options, imported initialization, or build profiles override it, and do CI, local builds, artifact generation, and verification explicitly pin and report the same value?
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_c314312f-ea0b-45e0-8556-7e107801cf32) |
|
@codex review Please perform a fresh read-only review of exact head |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ef488882c7
ℹ️ 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_3d136767-0fbe-4962-bab1-f5418363a4fb) |
|
@codex review Please perform a fresh read-only review of exact head |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4a8d92049a
ℹ️ 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_59f00897-d8cb-42b3-820c-bab17e73f021) |
|
@codex review Please perform a fresh read-only review of exact head |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 466dcec696
ℹ️ 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_ede0680a-5e15-402b-aed8-ffc088862a5d) |
|
@codex review Please perform a fresh read-only review of exact head |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: bfaf0f7cad
ℹ️ 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: a6b4771bfd
ℹ️ 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_207aed29-fba1-439a-82ff-f280c5f10e6f) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1011bc6695
ℹ️ 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_a3146a6e-a4ba-442d-8792-4f3606a9d31a) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 9d2747fe8c
ℹ️ 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_8f3652a9-c76f-4b72-b0bd-3e00049d4a38) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 651bf5f0e7
ℹ️ 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_96aa166d-6bad-4d0d-939e-cd7ee0cfd77b) |
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_1bb3b9b6-ddcf-4be7-93dd-56f2e7360bb3) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e2a2d69fa9
ℹ️ 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_24a4ea02-154a-4981-a45f-fa173347609a) |
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_b9dc8a50-0863-447d-ba41-22d5e7152fb4) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 299b359a82
ℹ️ 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".
| -- unqualified type written in the child may carry its resolved | ||
| -- namespace here. Contract-local type tables store the source-local | ||
| -- name; compare that final component consistently. | ||
| let tyName := id.getId.getString! |
There was a problem hiding this comment.
When a qualified type has the same final component as a contract-local or inherited type, getString! discards the qualifier and silently resolves the wrong declaration. For example, with local Amount : Uint256, a parameter explicitly written as Other.Amount is compiled as the local Amount even if Other.Amount denotes Address (or should be rejected as unsupported), changing the public ABI from the type the source names. Match qualified identifiers against their actual declaration identity instead of every local declaration with the same basename.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 658dea6671
ℹ️ 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".
| if !isIdentityArg then | ||
| if child.params.any (fun childParam => paramReservesName childParam param.name) then | ||
| throwErrorAt arg s!"parent constructor parameter '{param.name}' conflicts with a child constructor parameter; rename the child parameter" | ||
| let binding ← `(doElem| let $param.ident := $arg) |
There was a problem hiding this comment.
When a parent argument is a compatible numeric literal, such as Base(1) for a Uint24 parameter, the preceding check accepts it, but this unannotated let is later inferred as Uint256 rather than param.ty. An inherited body that uses the parameter in width-sensitive operations such as narrowAddPanic therefore rejects an otherwise valid child because the flattened local is no longer a UintN, and other narrow/newtype uses similarly lose their declared semantics. Emit a typed/normalized binding using the parent parameter's type.
Useful? React with 👍 / 👎.
| constructor=child_constructor, | ||
| functions=tuple(inherited_functions.values()), | ||
| storage_slots=parent.storage_slots | child.storage_slots, | ||
| storage_types=parent.storage_types | child.storage_types, |
There was a problem hiding this comment.
When child storage uses a type inherited from the parent, this merge leaves the child's raw storage type unresolved even though function and constructor signatures are resolved against merged_newtypes and merged_structs. For example, with a parent Amount : Uint256 and child fields a : Amount and b : Amount, generating a property for a function that reads both fields and returns a + b reaches _sol_type('Amount') and raises ValueError: unsupported Lean type for Solidity signature mapping. Resolve child storage types using the merged type tables before combining them.
Useful? React with 👍 / 👎.
1 participant
Summary
Implements issue #2087 for the
verity_contractEDSL:virtual/overridevalidation and compile-time specializationonlyOwner, and override specializationValidation
make checks— passed (641 Python tests plus all CI-equivalent checks)#check_contractforModifierInheritanceBaseandModifierInheritanceChild— passedmake test-evmyullean-fork— passed (fork audit, bridge lemmas/test, native harness, EndToEnd)lake build PrintAxioms Compiler Contracts— all Lean modules and targets compile, including PrintAxioms, Compiler, Contracts, smoke, and feature tests; Lake exits 1 on its aggregate import-graph job with the generic existing diagnosticContracts: some modules have bad importssorry,admit,axiom, orunsafeCloses #2087.
Note
High Risk
Large macro/elaboration changes affect contract layout, constructors, dispatch, and ABI generation across the compiler pipeline; mistakes could silently change semantics or break imported inheritance.
Overview
Extends
verity_contractwithmodifier/with,Child is Parent, parentConstructor(args)calls, andvirtual/overrideon functions. Modifiers are inlined as scoped precondition prefixes before function bodies; terminating returns in modifiers are rejected.Inheritance flattens one parent into the child at elaboration: storage, types, interfaces, roles, immutables (with constructor-arg substitution), and functions merge with duplicate/collision checks.
overridemust target a virtual inherited signature and cannot weaken payability, view/pure, visibility, or return type. Constructor binding uses nested lexical scopes so parameter names do not rewrite storage operands; ancestor/child/modifier name clashes are compile-time errors.Parent contracts are recorded in a persistent env extension (
registerContractSyntax) so children can resolve parents from imported.oleanfiles, not only same-module declarations. Cross-namespace inheritance is rejected.Syntax/parser updates cover
is Parent, parent constructor clauses, and dispatch annotations. Empty marker interfaces are allowed. Docs and parity tables (Morpho, Lido, ERC-4337) reflect supported single inheritance and modifiers. Smoke tests inContracts/Smoke/Helpers.leanand import split files exercise positive and#guard_msgsnegative cases; macro property-test generation merges inherited ABI and emits role-rejection stubs.Reviewed by Cursor Bugbot for commit 658dea6. Bugbot is set up for automated code reviews on this repo. Configure here.