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".
| \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``` |
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_61c4f093-af47-400b-b3ca-ba8c0e05e9c0) |
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), 725 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: 23 supported / 23 total; Lean 15, trust docs 0, workflow/scripts 4, contracts 2, docs 2
- Changed lines: 725 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 (+97/-0), artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol (+81/-0), test/EnumFeature.t.sol (+71/-0), Verity/Macro/Translate/Expr.lean (+48/-22)
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: 68d65b49db
ℹ️ 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_bb26e76d-db9a-44a6-aeee-0ecfb4966273) |
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: 16 Lean file(s), 798 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 16, trust docs 0, workflow/scripts 4, contracts 2, docs 2
- Changed lines: 798 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 (+194/-54), Contracts/Smoke/EnumFeatureTest.lean (+100/-0), artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol (+81/-0), test/EnumFeature.t.sol (+77/-0), Verity/Macro/Translate/Expr.lean (+52/-23)
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_0ae51cad-0b93-4b46-bbed-19a74e3bd2b7) |
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: 16 Lean file(s), 798 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 16, trust docs 0, workflow/scripts 4, contracts 2, docs 2
- Changed lines: 798 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 (+194/-54), Contracts/Smoke/EnumFeatureTest.lean (+100/-0), artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol (+81/-0), test/EnumFeature.t.sol (+77/-0), Verity/Macro/Translate/Expr.lean (+52/-23)
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_09107e87-4c20-4f2f-910b-288360456622) |
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: 16 Lean file(s), 804 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 16, trust docs 0, workflow/scripts 4, contracts 2, docs 2
- Changed lines: 804 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 (+194/-54), Contracts/Smoke/EnumFeatureTest.lean (+100/-0), artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol (+87/-0), test/EnumFeature.t.sol (+77/-0), Verity/Macro/Translate/Expr.lean (+52/-23)
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: 97c9b9e66f
ℹ️ 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_86304b10-e40c-4d07-998d-c0dbbbe0b78c) |
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: 16 Lean file(s), 827 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 16, trust docs 0, workflow/scripts 4, contracts 2, docs 2
- Changed lines: 827 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 (+205/-56), Contracts/Smoke/EnumFeatureTest.lean (+100/-0), artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol (+87/-0), test/EnumFeature.t.sol (+77/-0), Verity/Macro/Translate/Expr.lean (+52/-23)
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: 7264756c3e
ℹ️ 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_9d3454d0-07ca-4a15-b597-a9e0f6108aaa) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8dbe9b0708
ℹ️ 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 only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 16 Lean file(s), 827 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 16, trust docs 0, workflow/scripts 4, contracts 2, docs 2
- Changed lines: 827 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 (+205/-56), Contracts/Smoke/EnumFeatureTest.lean (+100/-0), artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol (+87/-0), test/EnumFeature.t.sol (+77/-0), Verity/Macro/Translate/Expr.lean (+52/-23)
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_3597c86a-2c84-4f75-b42c-db19cbb659d0) |
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: 16 Lean file(s), 894 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 16, trust docs 0, workflow/scripts 4, contracts 2, docs 2
- Changed lines: 894 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 (+217/-56), Contracts/Smoke/EnumFeatureTest.lean (+133/-0), Verity/Macro/Translate/Expr.lean (+73/-24), artifacts/macro_property_tests/PropertyMacroEnumUsage.t.sol (+87/-0), test/EnumFeature.t.sol (+77/-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: a9e0f56109
ℹ️ 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 eventParamTypeCompatible (actual expected : ParamType) : Bool := | ||
| actual == expected || | ||
| match actual, expected with | ||
| | .newtypeOf "__verity_enum" .uint256, .uint8 => true |
There was a problem hiding this comment.
Fresh evidence beyond the earlier event-parameter issue is that this compatibility shortcut accepts the shared enum marker for every enum-valued event field after the expected type has been erased to uint8. If an event expects a two-member Status but a function passes a parameter of a different three-member enum, value 2 passes both that parameter's range guard and this check, emitting an invalid Status event value. Validate event arguments against the semantic ValueType.enum name and member count before lowering the event definition to uint8.
Useful? React with 👍 / 👎.
| -- Admit only an in-range literal here; all non-literal enum expressions must | ||
| -- retain their exact enum type. | ||
| let compatibleEnumLiteral := match expectedTy, actualTy, stx.isNatLit? with | ||
| | .enum _ memberCount, .uint256, some value => value < memberCount |
There was a problem hiding this comment.
Fresh evidence after the exact-type fix is this newly added exception, which cannot distinguish a generated member body from user syntax. Consequently setStorage status 1, return 1 from an enum function, or assigning 1 to an enum local now passes validation whenever the literal is in range, bypassing the checked Status(1) cast and the intended rejection of implicit numeric-to-enum conversions. Apply this exemption only while validating compiler-generated member constants.
Useful? React with 👍 / 👎.
| | .uint256 | .int256 | .uint8 | .uint16 | .uintN _ | .intN _ | .bytesN _ | ||
| | .address | .bytes32 => true | ||
| | .newtype _ baseType => isWordLikeValueType baseType | ||
| | .enum _ _ => true |
There was a problem hiding this comment.
Although conditional branches now special-case enums, classifying every enum as generically word-like still makes requireEqComparableTypes and the arithmetic/comparison classifiers accept unrelated enum types or raw words. For example, Status.Active == Role.Admin compiles and compares their numeric ordinals instead of reporting the cross-enum type error, so a mistaken authorization condition can silently behave as a valid comparison. Permit same-enum equality explicitly and require toUint256 before generic word operations.
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 typing, compilation model, ABI layout, and executable codegen across many surfaces; behavior changes are broad but gated by new smoke/Foundry tests and explicit rejections for unsafe external enum returns.
Overview
Adds Solidity-style enums to
verity_contractvia anenumsblock: members get numeric constants,EnumName(x)is a checked cast, and values are ABI-encoded asuint8while storage/mappings still use a word.The macro and compiler paths now understand enum params, returns, storage, mappings, events, and errors, with stricter typing (no mixing enums with raw
uint256inite/assignments) and entrypoint guards that panic with0x21on out-of-range values. Enum returns from typed interfaces and linked externals are still rejected until safe decoding exists.Supporting tweaks include
revertPanicAsfor expression-bodied panics, event param compatibility for enum-vs-uint8ABI shapes, CI smoke forEnumFeatureTest, and Foundry/property-test generation for enum fixtures.Reviewed by Cursor Bugbot for commit a9e0f56. Bugbot is set up for automated code reviews on this repo. Configure here.