Repository navigation
The origin relation: an added or modified hand-Rust item must show its capability was modeled before it, and that the model constrains it - #9444
Conversation
…make it the changed-item denominator the seed-growth admission join was waiting for The census had one realization, scripts/rust_item_census.py, and gunbc#9132 deleted it with the measurement corpus. Nothing replaced it, so from 2026-08-24 no route in this repository could enumerate Rust items at identity grain -- and no rung drop was declared, because the census's consumers were lanes rather than modules and no dependent could refuse. The scaffold protecting it is a live instance of the rule DESIGN 4b(3) added on 2026-08-26: its trigger read "producer lands and enrolls; Python script deleted", a conjunction whose second half an unrelated cut satisfied while the producer never landed. gunbc.rust_item_scan reads items from rustfmt-normalized source with its item-keyword population taken FROM extdeps.languages.rust.syntax rust_item_forms rather than re-coined -- the deleted script's regex ITEM_PATTERNS were exactly the second roster this reader refuses to author, and the census predicted its own failure from it. It is not a parser and does not claim to be: it refuses on any structural line it cannot classify, which is what makes an incomplete recognizer safe rather than quietly smaller. gunbc.rust_item_host_observation supplies TWO populations from TWO functions, which is the condition gunbc.seed_growth_admission's own forward-freeze row set on enrolment. seed_growth_join_declarations is replaced by the split pair plus seed_growth_admit_change; an unattributed hand-Rust change REFUSES rather than reporting an empty delta; deletions offset nothing; ExistingSeedItemModified carries capability_origin, with no value naming a capability originated in Rust. Rung: mechanically preventable AS TO THE ROUTE and no higher -- the wall executes under witnesses and no required CI phase invokes it yet. Arming it is a separate change. The terminal seed-bridge roster is deliberately not authored here. Hand-Rust delta: zero. Every file is .dag.
…s capability was modeled before it, and that the model constrains it CapabilityAlreadyModeled was payload-free, so it could be satisfied by inspecting the final candidate -- which cannot distinguish a model that existed before its realization from a model authored beside the realization that inspired it. That distinction is the whole question the arm existed to ask, so the vocabulary moves to gunbc.capability_origin and grows a payload: an authority, and where a capability introduced in this change came from. THREE TESTS, ESTABLISHING THREE DIFFERENT THINGS. The leaf test proves Rust owns no semantic decision. The origin test proves the semantics predate the Rust: remove the hand-Rust delta, build E1, and the authority must still hold. The conformance test proves the model CONSTRAINS the Rust rather than merely agreeing with it: mutate the realization alone, and the predicted evidence must go red while E1 stays green. A retro-described implementation passes the first two and fails the third, because its fixtures were derived from the behavior they check -- which is why FixtureProvenance refuses GeneratedByRealization even when the mutation went red. ADDITIONS ARE COVERED, NOT ONLY MODIFICATIONS. A newly added item can carry a perfectly good justification row and still have been retro-modeled in the same change, so the relation participates in the addition arm and roster membership is no longer sufficient. THE EPOCH IS IDENTIFIED AND EXPIRES. ModelEpochRef names the exact derived E1 population, and the subject carries both the base and the head it was derived against. A probe taken against another base refuses rather than admitting -- the reversed-diff class stated as evidence rather than as advice. RUNG: the vocabulary is structural (no arm means "the Rust behaves this way, therefore this is the intended model", and no not-executed arm has a path to an admitting verdict). The tests themselves are executed by nothing yet, so every real call today refuses. The next-rung trigger names the capability. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… the length check (review 56637) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Merge-order note, measured — not a defect in this PR, and no change requested. This branch is a descendant of #9426's branch, not an independent one: So #9426 must merge before #9444. Merging #9444 first would carry #9426's commits in with it and land that PR's content under this PR's title, unreviewed as such. Verified conflict-free in both directions as of
One caveat worth stating because the repo squash-merges: after #9426 is squashed, this branch still carries the pre-squash commits, so its merge-base with main will be stale and its diff will re-present #9426's content. Git resolves that cleanly when the content is byte-identical, which it is today — but if anything is adjusted during #9426's merge, this branch needs a fresh Flagging only so the manual merge order is explicit. Nothing to do here. — sent from merry-bear-547 |
What this adds
gunbc.capability_origin— the origin relation, the second and third tests beside the leaf test #9426 landed.CapabilityAlreadyModeledwas payload-free. It could be satisfied by inspecting the final candidate, and a final candidate cannot distinguishwhich is the entire question the arm existed to ask. The vocabulary moves here and grows a payload.
There is deliberately no arm meaning "the Rust behaves this way, therefore this is the intended model." That state is unwritable rather than refused by a check.
NoNewCapabilitystays correct for an edit that only repairs, narrows, moves or deletes.Three tests, establishing three different things
The origin test: remove the hand-Rust delta, build E1 (base + the
.dagdelta, minus every added or modified hand item), and the cited authority must still resolve, compile and pass its controls. If producing the model projection requires the new leaf, the model is not independently prior and that substrate capability separates first.The conformance test is directional: mutate only the Rust realization. The predicted evidence must go RED while E1 stays GREEN. A mutation nothing notices establishes that the fixtures follow the realization.
FixtureProvenancerefusesGeneratedByRealizationeven when the mutation went red — redness is necessary, and provenance is what makes it evidence.Additions are covered, not only modifications
#9426 closed the large-existing-function escape. But a newly added item can carry a perfectly good
SeedGrowthJustificationrow and still have been retro-modeled in the same change, so the relation participates in the addition arm too.a_roster_named_addition_still_refuses_when_no_bridge_states_its_originruns the same addition the positive control admits, with the identical justification row, and the only difference is the origin evidence.The epoch is identified, and it expires
ModelEpochRefnames the exact derived E1 population (synthetic tree identity or content identity), andModelEpochSubjectcarries both the base and the head it was derived against — one alone leaves the failure unrepresentable in one direction.This came out of a live incident on #9426, and it is recorded in the carrier rather than as advice: a structural finding reported five scm modules changed, a witness file deleted and a type removed. Every one was main's own work rendered in reverse, from a two-dot diff between current main and a branch whose base predated it. Nothing in it was true and all of it was internally consistent. So a probe taken against a different base refuses — the class is unrepresentable instead of discouraged.
Rung, stated honestly
The vocabulary is structural: no not-executed arm has a path to an admitting verdict —
ProbeNotExecuted,ConformanceProbeNotExecutedand a missing bridge all refuse, and a caller supplies probe results, never verdicts, so a conclusion cannot be written in directly.The tests are executed by nothing in this repository yet. No host supplies
ModelEpochProbeResultorConformanceProbeResult, so every real call today lands on the not-executed arms and refuses. That is the correct fail-closed reading, not a passing one, and calling this a wall would be the inflation §4b(1) names as worse than sitting low. The next-rung trigger names the capability — a route that materializes E1 against the actual proposed base, builds and runs the authority's controls inside it, and mutates the realization to observe the conformance evidence flip — with three explicit non-retirements (constructing the subject without building it; building one entry when the controls span several; deriving the base from whatever ref the caller had).What is deliberately not here
No terminal
PinnedKernel/AuthorizedTemporarySeedBridgeroster. That closes with the finalclaim_executorcut; hand-transcribing ~1,500 moving declarations today is rung inflation wearing a roster. The bridge shape is authored once and read twice — prospectively by this join, contemporaneously by the terminal join later — and no parallel list is introduced for either reader.Two proposals were considered and rejected on the ruling: requiring the model in a prior merged PR (sufficient but not necessary, and it buys another moving-base epoch per realization), and requiring model refusals the realization does not implement (it creates an incentive to author decorative refusal arms).
Base
Stacks on #9426, whose head is
5c593b2e4e. Until that merges this PR's diff againstmainshows #9426's nine files as well; the origin relation itself is the commit0b05d6a0c0and touches four files. It cannot be based onmaindirectly — it consumes the types #9426 introduces.Evidence
rust_item_host_observation_witness_test— 21 arms green, including four new ones:a_capability_modeled_in_the_same_change_refuses_until_a_probe_runsconformance_fixtures_generated_by_the_realization_refuse_despite_a_red_mutationa_realization_mutation_no_evidence_noticed_refusesa_probe_taken_against_another_base_expires_rather_than_admittingThe third test broke a control that was already green
an_addition_the_roster_already_names_is_admittedis the positive control, and it passed the leaf test and the origin test: its bridge names a capability already on base, so the origin arm admits it with no probe needed. Adding the conformance test turned it red — no conformance probe existed for its authority, and a missing probe refuses.That is the strongest available evidence the three tests are independent rather than three spellings of one: a case that satisfied the first two was refused by the third. A test that landed green everywhere would be the decoration §4b names as worse than absent. The control now supplies conforming evidence to pass — without it, the refusals above would be satisfied by a join that refuses everything.
seed_growth_admission_witness_test— 7 arms green.Hand-Rust delta: zero. Every file in this change is
.dag.