Repository navigation
T-Modeling int-literal magnitude consumer - #897
Conversation
|
Blocking feedback on the draft:
Suggested next step: pause code changes, post the pre-flight audit on #870, and in that audit explicitly answer whether the existing |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
69e9a3f1· Trigger:schedule - Thinking:
304s wall
BLOCKING (1)
Root Cause
src/v3/compiler/src/infer.rslowering seeds annotated let literal ports with the declared type, but infer now treats that seed as already validated → gate this retry behind the same diagnostic-producing range/refinement checks used for call-site narrowing, or move annotated-let literal narrowing through that path.
| if let PortState::Resolved(existing) = dag.port(v.output).state() { | ||
| if let Some(int_sh) = dag.int_shape() { | ||
| if !type_shapes_equivalent(dag, &existing, &int_sh) { | ||
| return Decision::Retry; |
There was a problem hiding this comment.
BLOCKING: The int-literal retry path accepts any already-resolved non-Int port without range/refinement validation, so an annotated let like let x: UInt8 = 256 can keep the annotation by fiat instead of failing closed (C-8 / API-level enforcement).
|
Manager audit: marking ready so CI/review can run. The required pre-flight is now posted on #870, and this PR includes focused tests for annotated/call-site UInt8 narrowing plus Rust emit shape. Reviewers should still look closely at the inference design: the PR adds a top-level Scope remains partial Goal 2 / i64-bounded range-facts consumption only: no |
|
Blocking review is valid. The new can keep the seeded Please fix before merge by either:
Add a regression for the negative annotated-let case ( |
![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: 69e9a3f1ff
ℹ️ 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 int_literal_magnitude_narrow_merge(dag, port, &existing, &ty) { | ||
| dag.set_port_type(port, ty); | ||
| changed = true; |
There was a problem hiding this comment.
This merge path now rewrites an Int literal port to a fixed-width type (for example UInt8) during inference, but the Rust emitter still lacks a realization for that narrowed declaration, so newly accepted programs fail later with MissingTypeRealization (the new emit_let_uint8_uses_narrow_rust_type case reproduces it with let x: UInt8 = 5). In practice this turns a type-check success into a codegen failure, so the narrowing should be blocked until realization exists (or the emitter updated to handle the narrowed primitive).
Useful? React with 👍 / 👎.
|
CI triage on head
Please focus the next patch on narrowing the inference intervention. The likely risky surface is the new top-level Requested verification before re-requesting review:
|
|
Current-head CI triage for The remaining failing check is still
So the latest patch did not localize the inference behavior enough. The current diff still shows two broad mechanisms:
Direction: stop trying to make both broad hooks work. Rebase the fix around the existing diagnostic-producing expected-type path in Also address the backend-realizability finding: either update Rust realization for the narrowed primitive declarations so Before the next review request, please run/post results for:
Do not broaden beyond partial/i64-bounded range-facts consumption. |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
359cbb42· Trigger:schedule - Thinking:
316s wall
|
Review metadata
1. Story of the diffThis PR changes integer-literal inference so default 2. Invariant categories
Finding [BLOCKING] — illegal Dag port-state preservation.
Finding [BLOCKING] — Fail-Closed / Illegal States Unrepresentable. The comment says “If the port is already a non-
Compliant. The new narrowing logic is factored as small free functions / decisions over explicit inputs rather than method-style hidden state:
Finding [BLOCKING with the inference issue] — missing negative regression coverage. The added tests cover valid happy paths only: annotated
N/A — the diff consumes the existing integer-literal /
N/A — no new TODO, scaffold, temporary bridge, or dual representation is introduced. The 3. VerdictREQUEST_CHANGES. The core narrowing direction is right, and the call-site merge path does validate magnitude before setting the expected type, but the value-node retry path currently trusts any pre-resolved non- |
|
Verified current head
Required next patch is now very specific:
Do not request review again until the targeted diagnostic tests from the prior comment pass, especially |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
97fd6171· Trigger:schedule - Thinking:
79s wall
|
Current-head triage for Progress: the prior broad diagnostic/M0/TypeMismatch failures are gone.
The
Please rerun/post: |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
968288e0· Trigger:schedule - Thinking:
33s wall
|
Re-dashboard item (22:20:57): |
|
Re-dashboard item (22:21:59): |
|
Re-dashboard item (22:22:59) — superseded #897 is merged ( Note: GitHub briefly returned mergeable: UNKNOWN while merge state settled; current PR state is MERGED. |
|
Re-dashboard item (22:24:07): Re-checked — #897 remains MERGED to |
|
Re-dashboard item (22:39:09): Verified again — MERGED, merge OID |
|
Re-dashboard item (22:40:09): |
|
Re-dashboard item (22:41:04): Re- |
|
Re: “no [api-review] diff artifact / no fix commit” — verified, no code action Checked Why there is no fix commit: the Codex [api-review] entry never produced a diff-based finding because Post-merge: merged PRs are not the right vehicle for a “fix” here anyway; if a future diff review surfaces a real defect against |
|
Review metadata
Verdict: APPROVE — diff is narrowly scoped, fails closed, and is grounded in range facts. The change is a clean T-Modeling consumer for int-literal narrowing:
Minor exploratory note (non-blocking): the |
|
Review metadata
Verdict: APPROVE The diff is narrowly scoped to consuming existing integer range facts for literal narrowing, adds the Rust |
Single control surface for cleanup-lane harvest of #900/#901/#920/#897/#824/#825 per dispatch from tidy-dove-734 (#941). No ctrl#263 in repo; this docs/audit artifact is the agreed fallback. Rows: source PR, gap, file/invariant, owner lane, dissolution trigger, acceptance check, tracking authority, disposition.
Per bright-wolf-465 (inbox #945), no missed BLOCKING findings on these PRs; flip rows 6/7/8 to closed with audit citation.
* docs(audit): W-C1 follow-up harvest table Single control surface for cleanup-lane harvest of #900/#901/#920/#897/#824/#825 per dispatch from tidy-dove-734 (#941). No ctrl#263 in repo; this docs/audit artifact is the agreed fallback. Rows: source PR, gap, file/invariant, owner lane, dissolution trigger, acceptance check, tracking authority, disposition. * docs(audit): close #897/#824/#825 rows per bright-wolf-465 audit Per bright-wolf-465 (inbox #945), no missed BLOCKING findings on these PRs; flip rows 6/7/8 to closed with audit citation. * docs(audit): reconcile note with row dispositions for #897/#824/#825 * WIP: calm-ant-861 * chore: apply cargo fmt * WIP: calm-ant-861 * fix(test): fold B5 Loop closure receipt into m1_substrate_test SG-0 census ratchet forbids new hand-authored .rs files. Move the every_loop_node_originates_from_recursive_function_lowering test (and the LoopNode/LoopBound import + two helper fns) into the existing m1_substrate_test.rs and drop the standalone file + its integration.rs registration. Behavior unchanged. * docs: correct B5 receipt file path in synthesis doc (m1_substrate_test, not standalone file) * docs: mark ROADMAP loop-emission row resolved + correct synthesis cite Codex BLOCKING on be4a6ab: ROADMAP.md still listed the loop-emission semantic invariant as open debt while the synthesis doc declared it resolved — tracker-authority mismatch. - ROADMAP.md:436: rewrite the row as RESOLVED 2026-04-27 with PR cite, audit summary (two production sites in lower.rs), receipt location (m1_substrate_test.rs), and marker-retired note. - synthesis-doc §3 line 155: fix the receipt path (loop_construction_closure_test.rs → m1_substrate_test.rs after the SG-0 fold). * fix(test): split global vs fixture-scoped Loop closure assertions Codex BLOCKING on db7b773: previous test mixed a global all-Dag closure check with fixture-only variant claims, so bootstrap loops could mask the fixture-coverage claim. Split into two phases: - Global: every Behavior::Loop in the Dag (fixture + bootstrap) satisfies the recursive-function-lowering signature (loop.output is a Bind value port + Descent cluster id resolves). This is the closure invariant. - Fixture-scoped: filter loops by span.file == fixture file before claiming both LoopBound variants are produced by THIS fixture. Bootstrap loops are excluded so the variant claim is mechanically about the fixture's recursive functions. * post-merge: drop superseded artifacts; correct ROADMAP B5 receipt cite The parallel B5 lane landed `r2_b5_loop_construction_closure_test.rs` on main with a more rigorous receipt (substring push-site ratchet + per-fixture DAG walk + Origin::Accumulated provenance). The harvest table in this PR is also being landed via aggregate #949. Drop: - `docs/audit/w-c1-followup-harvest-2026-04-27.md` (canonical surface is #949). - The m1_substrate_test additions (auto-reverted via merge --theirs; superseded by the standalone r2_b5_loop_construction_closure_test.rs on main). Keep: - `ROADMAP.md` row marking loop-emission RESOLVED, with citation rewritten to point at the actual landed receipt file (r2_b5_…) instead of the retired m1_substrate_test cite.
* docs: forward-fix audit for merged PR #897 and #824 Static review maps prior BLOCKING threads to current main with file/line evidence; no code fix needed. Notes cargo verification for operators. Made-with: Cursor * docs: fix v3-compiler test target in forward-fix audit (§5) --test boundary does not exist; m1_4_emit_python_test lives in the consolidated integration test binary. Document the real layout. Made-with: Cursor * docs: polish forward-fix audit (section order, bootstrap pointer) Renumber §5–§6 to §4–§5 so the outline is contiguous after §3. Replace fragile bootstrap_generated.rs line-6 cite with an rg search pattern stable across regen (per PR review feedback). Made-with: Cursor
* docs(std.unicode): cite UCD 15.x / UAX-11 authority Closes the #920 post-merge citation gap. Header now states the file is sourced from UCD 15.x (UAX #11 East Asian Width) for the display- width tables and is intentionally 15.x compatible rather than pinned to a specific minor. UAX #9 is explicitly not consulted (no bidi). No behavior changes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs: tighten P5 per-PR dissolution gate (b) for ROADMAP-cited deferrals Require exactly one checkable receipt: delete path, SG-0 census before/after counts, or lane plus concrete ROADMAP row/link. Call out vague deferrals as insufficient. Align INVARIANTS §P5 (b) with the template without duplicating the checklist. Made-with: Cursor * docs(audit): W-C1 follow-up harvest table Single control surface for cleanup-lane harvest of #900/#901/#920/#897/#824/#825 per dispatch from tidy-dove-734 (#941). No ctrl#263 in repo; this docs/audit artifact is the agreed fallback. Rows: source PR, gap, file/invariant, owner lane, dissolution trigger, acceptance check, tracking authority, disposition. * docs(audit): mark #920 citation follow-up closed * docs(audit): close #897 #824 #825 harvest rows * docs(audit): cite closure evidence for harvest rows * WIP: Cleanup * docs(std.unicode): clarify UAX 11 coverage * docs: link cleanup harvest from roadmap * docs(std.unicode): refresh bootstrap spans * docs(std.unicode): refresh full bootstrap spans * docs(std.unicode): refresh no-parse bootstrap spans * docs(audit): stabilize harvest code references --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 participant
Summary
Implements the T-Modeling int-literal magnitude consumer slice over the merged Substrate cardinality/range-facts carrier from #806.
This is a partial, i64-bounded Goal 2 close only. It does not widen
LiteralBits::Int(i64), does not close thei64::MINsingle-token limitation, and does not implement Int128/Word128 carrier work.Downstream Consumer Audit
infer.rsvalue/transform pathsint_literal_fits_expected_type; preserves narrowed annotated literals only after fit-check; emitsMagnitudeOutOfRangefor out-of-rangeUInt8literals.Intliteral arguments to satisfy range-backed expected primitive types when the literal magnitude fits, soid_u8(7)narrows without broadening the conflict path.rust_uint8: TypeRealizationmappingUInt8tou8; emitted Rust can realize narrowedUInt8lets.rust.dagrealization change; parse corpus manifest refreshed.Verification
GitHub checks on head
19557885c57df0461111f214492e119c8b485cff:fmt: passedci: passedv3: passedself_host_ratchet: passedWorker also reported local targeted verification for all
int_literal_cardinality_testtests and the handwritten parse manifest test after merging currentmain.DB-8 / Closure
self_host_ratchetpassed in CI. This closes the Modeling int-lit consumer slice as partial/i64-bounded; full int-lit closure still depends on the separate Int128/Word128 lane.