feat(edsl): add uint8-backed enum support - #2248
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
699878b to
f448cc5
Compare
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_877ff25a-7097-4a3a-b62b-859422de00bc) |
![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: 30ec7fb761
ℹ️ 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_e23cc544-18b2-46f6-9d74-869a829e1376) |
![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 only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 14 Lean file(s), 666 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: 21 supported / 21 total; Lean 14, trust docs 0, workflow/scripts 3, contracts 2, docs 2
- Changed lines: 666 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 (+119/-33), Contracts/Smoke/EnumFeatureTest.lean (+92/-0), artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol (+81/-0), Verity/Macro/Translate/Expr.lean (+51/-22), test/EnumFeature.t.sol (+62/-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.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: dbd1eec43e
ℹ️ 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_43bfdf7f-5d09-4328-9c33-c88014c7971f) |
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: 14 Lean file(s), 673 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: 21 supported / 21 total; Lean 14, trust docs 0, workflow/scripts 3, contracts 2, docs 2
- Changed lines: 673 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 (+126/-34), Contracts/Smoke/EnumFeatureTest.lean (+94/-0), artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol (+81/-0), Verity/Macro/Translate/Expr.lean (+48/-22), test/EnumFeature.t.sol (+62/-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.
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_0716b10c-5b62-4cd6-b3b4-8dc3f0c4d1f8) |
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: 15 Lean file(s), 711 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: 22 supported / 22 total; Lean 15, trust docs 0, workflow/scripts 3, contracts 2, docs 2
- Changed lines: 711 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 (+160/-37), Contracts/Smoke/EnumFeatureTest.lean (+94/-0), artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol (+81/-0), Verity/Macro/Translate/Expr.lean (+48/-22), test/EnumFeature.t.sol (+62/-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.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: fb5bbc1681
ℹ️ 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".
| | .uint256 | .int256 | .uint8 | .uint16 | .uintN _ | .intN _ | .bytesN _ | ||
| | .address | .bytes32 => true | ||
| | .newtype _ baseType => isWordLikeValueType baseType | ||
| | .enum _ _ => true |
There was a problem hiding this comment.
Fresh evidence beyond the stated storage-write fix is that requireDeclaredValueType accepts any pair of word-like types, and this new branch classifies enums as word-like. Consequently the added checks around setStorage, mapping writes, and struct-member writes still accept a numeric literal or a value from another enum, allowing invalid enum words to be persisted. Use an enum-specific exact-type check rather than the generic word-like compatibility rule.
Useful? React with 👍 / 👎.
| `(Compiler.CompilationModel.Expr.bitAnd $expr | ||
| (Compiler.CompilationModel.Expr.literal $(natTerm mask))) | ||
| | .newtype _ baseType => normalizeTranslatedExprForType baseType source expr | ||
| | .enum _ _ => `(Compiler.CompilationModel.Expr.bitAnd $expr (Compiler.CompilationModel.Expr.literal 255)) |
There was a problem hiding this comment.
When a mutable local is initialized from an enum and later assigned a raw word, such as let mut value := Status.Active; value := 999, assignment validation only infers the RHS type and this normalization silently turns it into 999 & 255 = 231. The local remains semantically typed as Status, so it can subsequently pass the enum storage-write checks even though a three-member enum has no member 231. Require an exact enum RHS or a checked enum cast instead of byte-masking arbitrary assignments.
Useful? React with 👍 / 👎.
| | .newtype name baseType => do | ||
| let baseTerm ← modelParamTypeTerm baseType | ||
| `([Compiler.CompilationModel.ParamType.newtypeOf $(Lean.quote name) $baseTerm]) | ||
| | .enum _ _ => `([Compiler.CompilationModel.ParamType.uint8]) |
There was a problem hiding this comment.
A function declared to return an enum can currently use return 999, because return-expression validation merely infers the expression and never compares it with the declared return type, while the executable enum type is erased to Uint256. This line nevertheless advertises the result as ABI uint8, and Stmt.return emits the raw word without normalization, so callers receive noncanonical ABI data; an internal helper can also have that result treated as the enum and store it. Require the returned expression to have the exact enum type, obtainable through a checked cast or member constant.
Useful? React with 👍 / 👎.
| private def guardEnumParams (fn : FunctionDecl) : CommandElabM FunctionDecl := do | ||
| pure { fn with body := ← prependEnumGuards fn.params fn.body } |
There was a problem hiding this comment.
Injecting the enum guard into fn.body does not make it the first executed statement: translateBodyToStmtTerms prepends initializer, role, and modifier statements before the translated body. Thus an out-of-range enum call to an annotated function can execute a modifier or fail an authorization/initializer check instead of immediately producing Solidity panic 0x21, unlike ABI decoding before function entry. Place the range guard at the dispatch boundary or before all generated function preludes.
Useful? React with 👍 / 👎.
1 participant
Summary
EnumName(x)castsuint8throughout ABI/compiler paths while supporting params, returns, storage, mappings, events, and errors0x21, and reject implicit raw numeric literals where an enum is requiredCloses #2088.
Base and dependency audit
Targets live
mainat4369b1dfbc42c65ceb76a668f748e9336f0d948f. Narrow integer support from #2240 is already merged. Open PRs #2245, #2247, #2249, and #2250 remain independent and were not rebased, modified, or merged.Exact-head validation
Validated on CPU at exact head
f448cc50d65ddd2182dbe89001a81bd005a0b939:lake build Contracts.Smoke.EnumFeatureTest— pass (includes member constants, ABI erasure, checked cast, storage/mapping, event/error, and invalid enum parameter regressions)make checks— pass (641 Python tests; generated artifacts current; zero source axioms orsorry)Compiler.Proofs.EndToEnd— passlake build Compiler.ModuleInputTest Compiler.CompileDriverTest— passlake build PrintAxioms Compiler— passlake build PrintAxioms Compiler Contractscompiled all requested modules (Contracts,Compiler, andPrintAxiomseach built), then exited on the repository's existing aggregate library-collection diagnostic:Contracts: some modules have bad importsgit diff --check— passFoundry/solc are not installed in this local environment.
test/EnumFeature.t.solincludes solc differential coverage for valid and out-of-range casts, enum params/returns, storage, and mappings; the exact-head PR CI Foundry jobs are the execution gate.No merge is requested; Phase 2 exact-head self-review/merge remains separate after CI.
Note
Medium Risk
Touches macro parsing, compilation model, and ABI lowering across many contract surfaces; incorrect range or erasure behavior could change on-chain encoding or revert semantics, though smoke and differential tests cover the main paths.
Overview
Adds native enum declarations via an
enumsblock onverity_contract, with ordered members,Enum.Memberconstants, and checkedEnumName(x)casts. Enums are modeled as word-like types but ABI-erase touint8across JSON ABI, Solidity signatures, interfaces, events, and custom errors; function/constructor enum inputs use a__verity_enumparam wrapper so calldata staysuint8while the runtime still sees a full word for validation.The macro path wires enums through storage scalars and mappings (including chained keys), type checking on writes, translation to
setStorage/ mapping IR, and injected entrypoint guards that revert with panic0x21when a value is out of range; nested enum parameters in composites are rejected. Supporting tweaks includerevertPanicAsfor panics in expression-valued bodies,ident(...)call syntax for enum cast lowering, frame predicates for enum-valued mappings, and generated Foundry/property tests plus parity doc updates.Reviewed by Cursor Bugbot for commit fb5bbc1. Bugbot is set up for automated code reviews on this repo. Configure here.