Repository navigation
Conversation
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. |
![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
🟠 2 finding(s) (1 medium / 1 low) — see inline comments.
✅ Posted 2 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: small-lean (router-v11)
- Changed files: 8 supported / 8 total; Lean 1, trust docs 1, workflow/scripts 4, contracts 1, docs 1
- Changed lines: 41 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 2; files 8; tokens 353317; tool calls 41; warnings 0; duration 329s
- Largest changed files: docs/TRUST_ASSUMPTIONS.md (+16/-1), Compiler/SolidityImport/Import.lean (+8/-0), scripts/solidity_differential/check_storage_rejections.py (+5/-1), docs/SOLIDITY_IMPORT.md (+2/-1), Contracts/SolidityImportSmoke/NumericLiteralSequence.sol (+1/-1)
Pilot mode: advisory only. Codex Review remains the merge gate.
| | `if` / `else` statements | Root statements lower to `Stmt.ite` on a boolean condition evaluated once; a branch `return` stops execution and the continuation runs only on fallthrough. In inlined single-value helpers, the continuation after a returning branch is lowered once into the other branch and both results assign one fresh local; a helper that can fall off its end without a result rejects. Unsupported constructs still reject in unreachable branches. | | ||
| | Numeric literals and units (development) | Exact integral decimal/scientific/hex literals, including leading-dot fractions and digit separators, unsigned/bool named constants, and bounded sums of exact natural constant operands; seconds, minutes, hours, days, weeks, wei, gwei, ether. Fractional results, oversized words and general rational constant expressions reject. Focused checks pass 96 A/B/C transactions, 56 acceptance/rejection controls and 16 semantic mutants with minimal witnesses; exact-head release gates pending. | | ||
| | Numeric literals and units (development) | Exact integral decimal/scientific/hex literals, including leading-dot fractions and digit separators, unsigned/bool named constants, and bounded sums of exact natural constant operands; seconds, minutes, hours, days, weeks, wei, gwei, ether. Fractional results, oversized words and general rational constant expressions reject. Focused checks pass 96 A/B/C transactions, 56 acceptance/rejection controls and 16 semantic mutants with minimal witnesses; the numeric parent `b0fa7b0e2` passed all 12 exact-head gates. | | ||
| | Exact natural constant products (development) | `int_const` multiplication of two lowered natural literals with empty preludes uses unbounded arithmetic and requires a uint256 result. Includes `100 * 365 days`; fractional operands, oversized intermediates and general rational operations reject. Focused checks at `bbc8fe0ad` pass 96 A/B/C transactions, 60 acceptance/rejection controls and a product mutant with a replayed minimal witness; full exact-head gates pending. | |
There was a problem hiding this comment.
OpenCodeReview [documentation · medium]
The status "full exact-head gates pending" appears to contradict the stated validation for this change: the change description reports "Validation on exact head b3fce332...: all 12 local gates passed" (make check, smoke build, importer mutations, differential campaigns, etc.). Note the numeric-literals row directly above was updated in this same diff from "release gates pending" to "passed all 12 exact-head gates", suggesting this row should follow the same pattern once gates complete. If the exact-head gates have in fact passed for the products feature, this statement (and the matching "Full exact-head gates remain pending" in TRUST_ASSUMPTIONS.md) is stale; if they have not, the change description overstates the validation. Please confirm and align the status.
Suggested change:
+| Exact natural constant products (development) | `int_const` multiplication of two lowered natural literals with empty preludes uses unbounded arithmetic and requires a uint256 result. Includes `100 * 365 days`; fractional operands, oversized intermediates and general rational operations reject. Focused checks at `bbc8fe0ad` pass 96 A/B/C transactions, 60 acceptance/rejection controls and a product mutant with a replayed minimal witness; exact head `b3fce332` passed all 12 gates. |
| passed 96 A/B/C transactions across three equivalent variants, 60 | ||
| acceptance/rejection controls (including an oversized intermediate), and a | ||
| product mutant detected after a positive control and reduced to a replayed | ||
| single-call deletion-minimal witness. Full exact-head gates remain pending. |
There was a problem hiding this comment.
OpenCodeReview [documentation · low]
This section states "Full exact-head gates remain pending", but the commit message for this change reports that all 12 exact-head gates passed on exact head b3fce3325741d5623daa418b433d0f59b90090f0. The preceding section in this same file was updated in this very diff to record that its parent passed the exact-head gates, so this new entry appears stale at commit time. The direction is conservative (understating validation rather than overstating trust), so the trust model is not weakened — but please confirm the intended state: either the gates genuinely have not run on the exact head and the commit message overstates, or this line should record the pass like the numeric-parent entry above. Trust-assumption docs and release-gate status should not disagree.
This branch has not been deployed
1 participant
Midnight uses
100 * 365 days; the importer previously rejected this exact natural constant product. Lower multiplication of two literal natural operands with empty preludes using unbounded arithmetic, accepting only results that fit uint256. Fractional operands, oversized intermediates and other rational operations remain located rejections.Adds an A/B/C fixture extension, an equivalent normalized generated variant, acceptance and near-miss controls, and a detected importer mutation with a replayed minimal witness. No golden model or pilot provenance changes.
Validation on exact head
b3fce3325741d5623daa418b433d0f59b90090f0: all 12 local gates passed: make check, full Contracts/Verity/smoke build, importer mutations, smoke/loss/generated-program differential campaigns, axiom generator, pinned pilot check, stateful differential, require/custom-error differential and proof axiom audit. Pinned pilot:a9826f245b22d545321544bcc40b325f63ebe021. Focused checks passed 96 A/B/C transactions and 60 acceptance/rejection controls.Pinned corpus coverage completed with zero tool errors; Midnight remains 23/45 excluding multicall, with the previous product blocker replaced by subsequent unsupported constructs. This is a small stacked PR on the numeric-literals branch. Documentation’s pending-gates wording records the pre-release checkpoint; terminal validation evidence above is newer.