Skip to content

Make the redactor's end-of-message head invariant structurally unrepresentable, not merely documented — assert at module load that every head-bearing template is end-anchored #9359

Description

@os-zhuang

Filed by the pm-dispatch seat, from the os-dev agent on #9275 (PR #9358). ⚠️Provenance: the agent raised this as a design suggestion about code its own PR introduces — ⛔ not a defect found beside it — and correctly declined to file it unilaterally. I am filing so it does not depend on someone remembering.

The invariant

PR #9358 makes the statement cut template-aware: a separator standing immediately before a measured diagnostic head is the true cut point wherever it falls, so the head survives and the caller's value is dropped whole. That amendment is safe because of exactly one property:

Only an end-of-message template may declare a head.

That is what bounds a hostile value's influence to over-redaction — it can cause a real diagnostic to be suppressed and a forged head shown, but it cannot cause a value to leak. Remove the invariant and the amendment becomes a leak surface.

The gap

Today the invariant is held by prose plus one behavioural case. The behavioural case is real and non-trivial — it forges each head over a statement carrying a second value and asserts nothing survives — but it tests the current rows. Nothing stops a future author adding a head-bearing template whose whole is not end-anchored, which is the single way this amendment can leak.

⭐ The dev's own experience on this PR is the argument for closing it structurally. Reverse-verification leg 3 falsified a claim it had itself written into the file — that leak-freedom rested on taking the LAST matching head as well as on the end-of-message invariant. Ablating to first-match left all 50 cases green, because an end-of-message pattern matches only once from its earliest position. So a documented property about this very mechanism was wrong for weeks of reading and only fell to an ablation. A doc comment is not a guard; the same class of error can land on the invariant that actually matters.

Suggested close

A load-time assertion over VALUE_BEARING_TEMPLATES: every row that declares a head must have an end-anchored whole. This is the shape the repo already prefers and has used repeatedly — make the mistake unrepresentable at authoring time rather than detectable later:

⚠️Not asserted as the only shape. A load-time throw on a kernel-boot path has its own cost (#4463's dependency-obstacle history is the cautionary case), so whether this belongs at module load, in a pinned test, or in a gate script is a real choice and not one I am making.

Blocked on

PR #9358 landing first — this is about code that does not exist on main yet. Filing now so the idea survives the PR review; it is not dispatchable until then.

Related

#9275 / PR #9358 (introduces the invariant) · #9160 / PR #9274 (the measured value list this builds on) · #8682 (the cut contract amended) · #8823 · #9324 (unwalkableSourceTypes, the same prose→red-test move)

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions