chore: merge train 239 (v0.5.1618) - #10800
Merged
Merged
Conversation
… proof (#10793) `repsel-census` has been red on `main` since v0.5.1613 on one hard check: batch: 1 selected ptr-shape promotion(s) were not consumed, and not one of them names a mechanism. The wasted promotion is `row` in `buildRows` (benchmarks/app-patterns/ kernels/batch.ts). Its only use is `rows.push(row)`, a contained element push, so it clears rule 2 with no property access anywhere in the body: the proof is sound and there is nothing to spend it on. That is the residue `check_unconsumed_is_explained` already described as "dropped by nobody" and then tolerated, on condition that some OTHER promotion in the same workload named a rule. Nobody is a mechanism; it just had no recorder. #10769 exposed it without causing it, established by A/B rather than inferred: subtracting only #10769's `RepselContextFlags::derive` `Entry` hunk from today's `main` reproduces the v0.5.1612 `batch` report entry-for-entry and the census goes green. What that hunk moved is `batch`'s other wasted promotion -- `totals`, in the module-init body, until then dropped by `module_init_context` and now consumed. Removing the workload's only named mechanism left the pre-existing residue as its only wasted promotion, and so the only one the check could see. So this names the mechanism rather than undoing anything. No floor lowered, no allowance widened. * `PTR_SHAPE_NO_ACCESS_SITE` ("no_access_site") joins `module_init_context` and `scalar_replaced`. The three are disjoint by construction: `module_init_context` fires from `ptr_shape_receiver_fact`, which only runs AT an access site, and `scalar_replaced` fires for objects whose HIR field accesses are exactly what scalar replacement rewrites. * `ptr_shape_report::note_no_access_site` records it, from the same loop iteration as the `select()` it annuls. The verdict reads the use walk's own containment bookkeeping -- `field_stores`, `method_calls`, plus a new `UseWalk::field_reads` for the one shape that stores nothing -- rather than a second, separately-drifting definition of "access site". Report-only. * Inferring the rule at render time from `selected - consumed` was rejected: it would name a mechanism for every gap and permanently disarm the check. * `report_early_bail` moves to `ptr_shape_report.rs` as `report::early_bail` (it calls nothing but `report::`), keeping `ptr_shape.rs` under the 2000-line cap. Corpus effect is one report entry: the full 29-workload run against the v0.5.1616 release compiler differs from the fixed compiler by `no_access_site 1` and nothing else -- every count, floor and advisory line byte-identical. The gate still discriminates, checked both ways. Disabling the new recorder returns `batch` to the original failure; disabling the pre-existing `scalar_replaced` recorder reddens fixture_alloc_buckets, suite_07_object_create and suite_12_binary_trees, which `no_access_site` does not paper over. The new test asserts both halves and fails under either sabotage, including a recorder that fires on a local that does have an access site -- the direction that would turn the census permanently green.
…c field vouches as canonical raw f64 (#10777) `expr_produces_canonical_raw_f64` refused every `PropertyGet` on principle, so an arithmetic leaf reading a field whose shape already records it as numeric kept a per-iteration tag test. The fact was present and consumed — `property_get.rs:1523` emits `load(DOUBLE, ...)` with `rep: F64` — and then re-derived syntactically from the Expr node at the add, which is also why `o.a * 1` reaches 9 where `o.a` does not: `Binary` is a shape that predicate recognises, and the multiply normalises nothing. The arm admits a `PropertyGet` whose receiver carries `ptr_shape_receiver_fact(...).numeric_fields.contains(property)`. h += o.a 35 -> 33 h += o.a + o.b 50 -> 43 o.a = o.a + 1; h += o.a 97 -> 94 That is 2-7 instructions per iteration on one shape, and it does NOT reach parity: node is 6.5-7.1 on the same fixtures. Two named blockers remain, and neither is this arm. Module-global receivers carry no Ptr<Shape> fact at all (#7109), so every fixture in #10777 and #10761 is an absence rather than a zero. And `SlotRep` has no F64 variant (slot_rep.rs:80, whose own doc says it "grows richer reps (F64, Ptr, ...) in later phases"), so `const v = <any read>` re-boxes at the binding and the LocalGet refusal is correct there — the slot really is boxed. The precondition is discharged by construction: `expr_numeric_by_construction` has no Call, MethodCall or FFI arm, so an FFI return can never enter numeric_fields. The one raw-byte source that can is the ArrayBuffer conduit, closed by #10779.
|
Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Advanced Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (10)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
This was referenced Sep 20, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Merge train 239 — a red gate turned green, released as v0.5.1618.
Contents
fix(codegen): name the mechanism that drops an unspendablePtr<Shape>proof —repsel-censusis green for the first time since v0.5.1613perf(codegen): a property read on aPtr<Shape>receiver with a numeric field vouches as canonical raw f64#10774 was the trigger, not the fault
repsel-censuswent red at v0.5.1613 (merge train 234, mine). The failing message was1 selected ptr-shape promotion was not consumed, and not one of them names a mechanism, with promotion counts up across thirteen workloads — which reads like #10774 creating a wasted promotion. It did not.Diffing the two runs, exactly one entry changed on
batch:totals@module_initmodule_init_contextrow@buildRowsv0.5.1612: two wasted, one mechanism → passes on the residue allowance. v0.5.1613: one wasted, zero mechanisms → red. #10774 consumed
totals, which is it working as intended — and that removed the workload's only named mechanism, exposing a pre-existing unnamed residue as the only wasted promotion the check could see.The attribution is not subsystem-matching: reconstructing "today's
mainminus #10769" reproduces the v0.5.1612 report entry-for-entry.The residue is
rowinbuildRows, whose only use isrows.push(row)— contained enough to clear the rule, but with no property access anywhere in the body. The field reads happen later through the array's own element-shape fact, on a different value. The proof is sound and there is nothing to spend it on.check_unconsumed_is_explained's own docstring already named the shape: "a promotion with no access site at all is dropped by nobody." The fix names it (PTR_SHAPE_NO_ACCESS_SITE). No floor lowered, no allowance widened, nothing reverted.The green was proven not to be a disarm
The failure mode for any "make the red gate green" change is that the greenness comes from relaxed config rather than from the fix:
Independent of the branch's own three sabotages, the most important of which is that disabling the pre-existing
scalar_replacedrecorder still redsfixture_alloc_buckets,suite_07_object_createandsuite_12_binary_trees— the new recorder does not paper over other mechanisms.This train's landing gate now requires
repsel_census rc=0, rather than carrying forward the known-red tolerance it had. A baseline that still accepts the failure it just fixed is how a fix silently stops holding.Why #10787 travels with it
It is a
Ptr<Shape>/numeric_fieldschange in the same subsystem, so it was deliberately held back one train. That is only safe because the #10793-only census was verified green before assembly — so a wasted promotion here would be unambiguously #10787's. There is none:repsel_census rc=0 wasted_promotion=False.#10787's own honesty is worth preserving: it moves three rows by 2–7 instructions against node's 6.9–9.2 and says plainly that this does not reach parity and is not close. Its two blockers are named as absences rather than zeros — #7109 (module-global receivers carry no
Ptr<Shape>fact at all, so the arm cannot fire) and the missingSlotRep::F64(soconst v = <any read>re-boxes at the binding and theLocalGetrefusal is correct there). Both are planned work, not new design.One transient, named rather than written off
cor_native-abi-proofreportedfailed_workloads=["native_memory_fixture"]during the run. It does not reproduce — the fixture compiles standalone, and a full re-run of the suite isrc=0, failed_workloads: [].The cause is specific:
native_memory_fixture_projectis the only fixture in the corpus that shells out tocargo buildfor a Rust staticlib mid-check, so it is uniquely exposed to concurrent cargo activity and disk pressure — and the box was at 19–24 GB with this train's own release build and gap sweep in flight. The landing gate accepts that one workload only and refuses any other compiler-output failure, rather than marking the whole gate noisy.Validation
Assembled on
1a4fa6507e; both source heads asserted fresh; no attribution trailers. Nine cheap gates,cargo check --workspace --all-targetsunder-D warnings, all five pinned artifacts byte-identical before and after, six unit suites with an empty failing set,lintcomplete at 6-of-6 with nothing outside the known-red public-baseline step.Four "missing" insertions were flagged and all four were correct absences — including
blk.fcmp("uno", value, value)innanbox_inline.rs, which looks exactly like the call train 238 just fixed. It is the f64 canonicaliser, correctly still using thedouble-defaultingfcmp();canonicalize_lane_f32twelve lines below usesfcmp_ty(F32, …). Restoring it would have reintroduced the compile break.Gap sweep at
PERRY_RUN_TIMEOUT=30, seven areas over the shared subsystem, every one asserted live, zero unexplained regressions: