P13-S22: Registered = 16, and why the numbered tag rows do not count

Registered joins the semantic-lock inventory. Its corpus row is emitted under the
variant name at ops/src/vectors.rs:210 and its committed literal leads with 0x10
at spec/vectors/decode_vectors.txt:80, so the drift comparison binds the
association. The uncovered set narrows to 0, 2-15, 17-23, and 30-33.

Verifying that turned up a false clause of my own. The entry said the corpus's
tag coverage is unchosen and unmaintained. It is neither: vectors.rs:201-204
emits one row per tag straight from the vocabulary and states the reason -- a
hand-picked subset is how TransposeInterval shipped encoding to a byte its own
decoder rejected.

But the rows lock byte-to-byte, not variant-to-byte. Each is named
tag_{discriminant} and carries [discriminant], both derived from the value alone,
so tag_32 asserts that 0x20 round-trips and never that SetCanvasLayoutDefaults is
32. All forty rows are identical under a permutation; what moves is their order,
since PAYLOAD_FREE is declaration order. That is why the 32<->33 probe failed,
established from the committed file's ascending tag_NN rows rather than inferred.

Which sharpens the entry rather than weakening it: Registered's row has exactly
the property the numbered rows lack, because it is named for its variant. The gap
is that one row's discipline is not the vocabulary's.

Ledger-only. No code, wire, or specification change.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QjsEnYhm1gPpf6ii2iFxFV
This commit is contained in:
Levi Neuwirth 2026-07-30 21:36:43 -04:00
parent 02eb3aa32f
commit 6f790bca65
1 changed files with 1 additions and 1 deletions

View File

@ -99,4 +99,4 @@ visible — a value with a wire form and no canonical carrier to reach it.)
| P13-S19 | **`CreateMeasure`'s ordering and boundary-distance preconditions are vacuous for an instance's first measure, so pickup/anacrusis measures are unauthored by this rung.** Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9) makes clauses 1 and 3 of `create_measure`'s append-only discipline vacuous when there is no predecessor measure, and invariant 20's boundary clause is symmetrically exempt for a first measure (core specification, invariant 20's doc comment) — a partial first measure MUST NOT be refused or flagged by either. This is a scoped deferral, not an oversight: a pickup measure's *own* internal consistency (its declared duration against its content) is a decomposition-sum question, not a measure-to-measure boundary question, and modelling it correctly needs a notion of "partial measure" this rung does not introduce | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9 (filed 2026-07-30 during the G3b contract's own drafting) | **open, deliberately.** A pickup/anacrusis authoring story — whatever shape it takes — is later schema-fill work, sequenced after the genesis ladder closes |
| P13-S20 | **`decode.rs`'s `precondition_reason` decoder stopped at discriminant 13, so `PreconditionFailureReason` 14 (`AcousticRealizationPinned`) and 15 (`TranspositionOutOfRange`), both live since Push 4a, encoded but could not decode.** A materialized effect carrying either reason failed canonical round-trip in production code, undetected because `epiphany-testkit`'s `precondition_failure_reason` generator (`generators.rs:417`, then `rng.below(14)`) never drew past 13 despite its doc comment claiming "every core and registered variant" | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` §0 / touch-table row 12a (found 2026-07-30 during the G3b contract's own drafting, verified against the working tree: `decode.rs:205`ff ended at 13, `generators.rs:417` drew `below(14)`) | **RESOLVED in this rung** (genesis tranche G3b packet 1, `e64a4b7`). `decode.rs`'s `precondition_reason` now decodes discriminants 14 through 18 (the pre-existing 14/15 hole plus G3b's own 1618), and `generators.rs`'s `precondition_failure_reason` now draws `below(19)` with arms for all of them — the generator's doc comment claim is true again, and the decode hole this rung found already latent in the tree, not introduced by it, is closed alongside G3b's own additions |
| P13-S21 | **The wire specification never documented `PreconditionFailureReason` 14 and 15, so the decoder hole P13-S20 repaired had no normative text to be measured against.** `binary_format.tex`'s bounded reason table (`\sectionsc{Bounded Enumerations}`) ran `\tablenums{13}` straight to G3b's `\tablenums{16}`, and Push 4a's own Revision History row recorded only `OperationKind` `\tablenums{30}` (`TransposeInterval`) while saying nothing about the two reasons it appended in the same epoch. `AcousticRealizationPinned` and `TranspositionOutOfRange` appeared **nowhere** in the document, though the Operation Catalog documented both at 0.8.0 and `effect.rs` has carried both since Push 4a. This is P13-S20's specification-side twin: the same two variants, the same silence, and the reason a decoder that stopped at 13 could sit in the tree unchallenged — a conforming implementer reading only the wire specification would have built exactly that decoder and been right | Found 2026-07-30 while verifying genesis tranche G3b packet 3b (`d58eee8`), whose touch-table row 28 scoped the reason table to discriminants 1618 only; the executing agent correctly declined to widen scope and reported the gap instead | **RESOLVED in this rung** (the G3b pre-push repair). The bounded table gains `\tablenums{14}` and `\tablenums{15}` with their refusal conditions, and Push 4a's Revision History row is amended to record both appends in its own epoch — no version bump and no new history row, because this documents an assignment that has been normative since Push 4a rather than making one. `binary_format_history.rs` gains a bounded regression test requiring both names in the reason table **and** in Push 4a's own row segment, so neither the G3b row's prose nor the Operation Catalog's coverage can satisfy it |
| P13-S22 | **`OperationKindTag`'s normative tag-to-byte mapping is asserted for a minority of the vocabulary; the rest is defended only incidentally, by frozen byte artifacts that cannot say what broke.** P13-S15 closed the `OperationKind` half with one table covering 0..=39. The tag half has no equivalent. **Semantic locks — a named tag bound to a literal byte — exist only for:** 2429 (`phase3_tag_discriminants_are_golden`, `payload.rs:2728`), 34 (one assertion inside a G2b reduction test, `reduce.rs:12744`), 3538 (`t1_g3a_kinds_and_tags_are_35_to_38_in_both_spaces`, `reduce.rs:15931`), 39 (`payload.rs:2936`), and — incidentally — 1, spelled in a comment inside a golden blob (`barrier.rs:1058`, *"len 1, DeleteEvent (tag 1)"*). **Tags 0 and 223 and 3033 have no semantic lock at all.** The derived tests do not supply one: `the_tag_vocabulary_is_complete` (`payload.rs:2652`) proves **completeness, density, and round-trip** — that the payload-free discriminants are exactly `0..unknown` with no gaps and each decodes — which constrains the *shape* of the assignment, not *which tag holds which byte*, and `operation_kind_tag_vocabulary!` guarantees coverage rather than value. **What actually catches a permutation is byte-level goldens that embed the tag by accident**, and they diagnose it as a blob mismatch: three probes, three catches, none of them naming a tag (below) | this file (found 2026-07-30 while closing P13-S15, whose kind-side extension made the asymmetry visible; **the entry was rewritten the same day after its own probes falsified its first draft.** That draft claimed a permutation was invisible and named 32↔33 as the demonstration. Three permutations were then executed against the working tree at `dcb28f0` and **all three failed**, so the claim was wrong and the severity is lower than filed: 32↔33 (`SetCanvasLayoutDefaults`/`SetSpellingPrecedence`) → caught by `the_committed_corpus_matches_the_generator` (`testkit/src/vectors.rs:225`); 1↔2 (`DeleteEvent`/`ModifyEvent`) → caught by `edit_barriers_blob_bytes_are_golden` (`layout-ir/src/barrier.rs:1061`); 2↔3 (`ModifyEvent`/`RespellPitch`) → caught by the corpus again. Each mutation was restored by hand and the suite returned to 1541/0) | **open.** **Not a live incorrectness, and — corrected — not an undefended one either:** every tag discriminant is currently correct, `binary_format.tex:1548``:1552` carries the mapping normatively, and no probe escaped. **The gap is intent and diagnosis, not exposure.** A permutation fails as *"the committed corpus does not match the generator"* or *"blob bytes are not golden"* — artifacts that regenerate, whose failure reads as corpus drift rather than as a moved wire discriminant, and whose coverage of the tag space is whatever the vectors happened to need. Nobody chose that coverage and nobody maintains it as coverage; if a future vector set shrinks, the protection silently shrinks with it, which is the same hand-maintained-table failure mode in a different costume. **Likely shape of the repair:** one table over the whole tag vocabulary asserting tag → byte directly, superseding the five scattered fragments rather than adding a sixth — a sixth band is how this got here — so that moving a tag fails by *name*. **Probe design note for whoever takes this:** do not reuse 32↔33 or 1↔2; both are now known to be caught, and a probe that fails proves the lock exists, not that it is missing. The mutation that would sign this rung is the **inverse**: delete the proposed table and show that some permutation then passes, or show the surviving failure names no tag. **Its own rung, not a rider** |
| P13-S22 | **`OperationKindTag`'s normative tag-to-byte mapping is asserted for a minority of the vocabulary; the rest is defended only incidentally, by frozen byte artifacts that cannot say what broke.** P13-S15 closed the `OperationKind` half with one table covering 0..=39. The tag half has no equivalent. **Semantic locks — a named tag bound to a literal byte — exist only for:** 2429 (`phase3_tag_discriminants_are_golden`, `payload.rs:2728`), 34 (one assertion inside a G2b reduction test, `reduce.rs:12744`), 3538 (`t1_g3a_kinds_and_tags_are_35_to_38_in_both_spaces`, `reduce.rs:15931`), 39 (`payload.rs:2936`); **16** (`Registered`, whose corpus row is emitted under its *variant* name at `ops/src/vectors.rs:210` and whose committed literal leads with `0x10` at `spec/vectors/decode_vectors.txt:80`, so the drift comparison binds the association); and — incidentally — 1, spelled in a comment inside a golden blob (`barrier.rs:1058`, *"len 1, DeleteEvent (tag 1)"*). **Tags 0, 215, 1723, and 3033 have no semantic lock at all.** The derived tests do not supply one: `the_tag_vocabulary_is_complete` (`payload.rs:2652`) proves **completeness, density, and round-trip** — that the payload-free discriminants are exactly `0..unknown` with no gaps and each decodes — which constrains the *shape* of the assignment, not *which tag holds which byte*, and `operation_kind_tag_vocabulary!` guarantees coverage rather than value. **What actually catches a permutation is byte-level goldens that embed the tag by accident**, and they diagnose it as a blob mismatch: three probes, three catches, none of them naming a tag (below) | this file (found 2026-07-30 while closing P13-S15, whose kind-side extension made the asymmetry visible; **the entry was rewritten the same day after its own probes falsified its first draft.** That draft claimed a permutation was invisible and named 32↔33 as the demonstration. Three permutations were then executed against the working tree at `dcb28f0` and **all three failed**, so the claim was wrong and the severity is lower than filed: 32↔33 (`SetCanvasLayoutDefaults`/`SetSpellingPrecedence`) → caught by `the_committed_corpus_matches_the_generator` (`testkit/src/vectors.rs:225`); 1↔2 (`DeleteEvent`/`ModifyEvent`) → caught by `edit_barriers_blob_bytes_are_golden` (`layout-ir/src/barrier.rs:1061`); 2↔3 (`ModifyEvent`/`RespellPitch`) → caught by the corpus again. Each mutation was restored by hand and the suite returned to 1541/0) | **open.** **Not a live incorrectness, and — corrected — not an undefended one either:** every tag discriminant is currently correct, `binary_format.tex:1548``:1552` carries the mapping normatively, and no probe escaped. **The gap is intent and diagnosis, not exposure.** A permutation fails as *"the committed corpus does not match the generator"* or *"blob bytes are not golden"* — artifacts that regenerate, and whose failure reads as corpus drift rather than as a moved wire discriminant. **The corpus's tag coverage is deliberate, not accidental**`ops/src/vectors.rs:201``:204` emits one row per tag straight from the vocabulary and names the reason: *"A hand-picked subset is how `TransposeInterval` shipped encoding to a byte its own decoder rejected: the corpus never named it."* **But those rows lock byte→byte, not variant→byte.** Each is named `tag_{discriminant}` and carries `[discriminant]`, both derived from the value alone, so `tag_32` asserts that `0x20` round-trips — never that `SetCanvasLayoutDefaults` is 32. Every one of the 40 rows is identical under a permutation; what actually moves is their **order**, since `PAYLOAD_FREE` is declaration order. That is why the 32↔33 probe failed, and it is exactly the property `Registered`'s row has and the numbered rows do not — its row is named for the variant. **The gap is that one row's discipline is not the vocabulary's.** **Likely shape of the repair:** one table over the whole tag vocabulary asserting tag → byte directly, superseding the five scattered fragments rather than adding a sixth — a sixth band is how this got here — so that moving a tag fails by *name*. **Probe design note for whoever takes this:** do not reuse 32↔33 or 1↔2; both are now known to be caught, and a probe that fails proves the lock exists, not that it is missing. The mutation that would sign this rung is the **inverse**: delete the proposed table and show that some permutation then passes, or show the surviving failure names no tag. **Its own rung, not a rider** |