G2b amendments: undo restores the seed, epoch 10 lands, and a real touch table
Documentation only. Ready for dispatch after these four repairs. Replaces pin 5 and t7. The earlier draft required undo to distinguish "never authored" from "authored to the default", which PLAN_GENESIS_OPS.md section 5 trap 5 explicitly withdrew - and SetMetadata is the disproof: Score::empty seeds metadata exactly as it seeds tuning_context, and base ingest runs metadata_chain.seed precisely so a value-restoring undo of the first operational write restores the pre-operational state. Undo restores the seeded base settings, default or not, and the distinction must stay UNOBSERVABLE - code that can tell the two apart is a defect, not a safeguard. Predecessor::Base vs ::Write earns its keep only for the bookkeeping families, where a base predecessor returns a map key to absence; ScoreTuningContext is always-valued like metadata and has no absent state to return to. t7 now asserts the two cases are indistinguishable rather than that they differ. Appends epoch 10 to the authoritative ladder with G2b as the event. It stays monotonic and prefix-closed, and it is the first exercise of the ladder's own growth path - G-minor's wildcard-free introduced_minor means kind 34 cannot compile without one. Adds the explicit non-goal the plan requires: G2b authorizes no pruning or compaction of the canonical operation log. The rung sharpens that prohibition rather than relaxing it, because after G2b pruning would discard authored genesis state rather than merely re-derivable state. Adds the touch table the gate already referred to but which did not exist, derived from G2a's actual thirty-file footprint plus G1's one extra rather than from recollection: the new core type and its export, full ops plumbing including envdecode/migrate/v0/valuegen/fuzz/vectors, the bundle accept-set raise and its falsified rationale, the four budgeted boundary crossings, text projection with companion 0.11.0, all four .tex sources with all four PDFs, both vector corpora, and P13-S13's closure. Ratifications folded in: subset design, epiphany_core::TuningContextSettings, epoch 10. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QjsEnYhm1gPpf6ii2iFxFV
This commit is contained in:
parent
0a35697d8e
commit
039a8ddec8
|
|
@ -99,8 +99,9 @@ test (`codec.rs:3725`, `textvalue_graph.rs:1092`). The **text projection drops
|
|||
it too** (`textvalue_graph.rs:1123`), so it already survives no persistence
|
||||
surface at all. The subset type ratifies the status quo rather than changing it.
|
||||
|
||||
**Open for ratification:** the type's **name**. `TuningContextSettings` is the
|
||||
default. It must not be named so as to imply it is the whole context.
|
||||
**RATIFIED 2026-07-28:** the subset design, and the type's name and path —
|
||||
**`epiphany_core::TuningContextSettings`**. It lives in `epiphany-core`
|
||||
alongside the type it narrows, and is publicly exported at that exact path.
|
||||
|
||||
---
|
||||
|
||||
|
|
@ -140,18 +141,43 @@ G-minor's `introduced_minor()` is **exhaustive with no wildcard arm**, so
|
|||
kind/tag 34 **cannot compile** without an epoch. That is the control working as
|
||||
designed — do not defeat it.
|
||||
|
||||
**Epoch 10, for the genesis G2b event.** This extends the ratified ladder
|
||||
(`PLAN_GMINOR_SCHEMA_MINOR.md` §4, minors 2–9) by one, monotonically. **This
|
||||
addition requires ratification** alongside this contract; it is the first
|
||||
exercise of the ladder's own growth path.
|
||||
**Epoch 10, for the genesis G2b event — RATIFIED 2026-07-28** and already
|
||||
recorded in the authoritative ladder (`PLAN_GMINOR_SCHEMA_MINOR.md` §4).
|
||||
**Transcribe it; do not edit that plan.** This is the first exercise of the
|
||||
ladder's own growth path, and it stayed monotonic and prefix-closed.
|
||||
|
||||
### Pin 5 — undo must distinguish never-authored from authored-to-default
|
||||
### Pin 5 — undo restores the **seeded base**, and the never-authored /
|
||||
authored-to-default distinction must stay **unobservable**
|
||||
|
||||
`Score::empty` seeds `tuning_context` with a **default value**, so the
|
||||
`WriteChain` cannot treat "no base" and "base equals default" alike. Follow
|
||||
G2a's chain shape (`reduce.rs`), and note the chain's value type is the
|
||||
**subset type**, not `ScoreTuningContext` — `accidental_extensions` never
|
||||
participates in undo because no operation ever writes it.
|
||||
**An earlier draft of this contract had this backwards.** It required undo to
|
||||
distinguish "never authored" from "authored to the default value".
|
||||
`spec/PLAN_GENESIS_OPS.md` §5 trap 5 **withdrew** that on 2026-07-28, and
|
||||
`SetMetadata` is the disproof: `Score::empty` seeds `metadata` exactly as it
|
||||
seeds `tuning_context` (`graph.rs:1749`, `:1757`), and base ingest then runs
|
||||
`metadata_chain.seed(score.metadata.clone())` (`reduce.rs:1385`) precisely so a
|
||||
value-restoring undo of the *first* operational write restores the
|
||||
pre-operational state.
|
||||
|
||||
**The rule:**
|
||||
|
||||
* From-empty reduces **onto** `Score::empty` (via `reduce_operation_set_onto`),
|
||||
so **the seed runs**. Undoing the first write yields
|
||||
`Restore(Some(Predecessor::Base(seeded)))`.
|
||||
* **Undo restores the seeded base settings — default or non-default alike.**
|
||||
Restoring the seeded value is correct in *both* cases, so the distinction is
|
||||
unobservable, **and this contract must keep it so.** Writing code that can
|
||||
tell them apart is a defect, not a safeguard.
|
||||
* **`Predecessor::Base` vs `::Write` earns its keep only for the canonical
|
||||
bookkeeping families** (`spellings`, `breaks`, `page_breaks`,
|
||||
`reduce.rs:707`), where a base predecessor returns a **map key to absence**.
|
||||
`ScoreTuningContext` is an **always-valued** `Score` field, like `metadata`:
|
||||
**there is no absent state to return to.**
|
||||
* **Copy `set_metadata` structurally**, as all three G2 setters do. Do not
|
||||
invent a chain shape for this field.
|
||||
|
||||
The chain's value type is the **subset type**, not `ScoreTuningContext`:
|
||||
`accidental_extensions` never participates in undo, because no operation ever
|
||||
writes it and undo must leave it exactly as it found it.
|
||||
|
||||
### Pin 6 — P13-S13 closes here
|
||||
|
||||
|
|
@ -189,7 +215,25 @@ Five non-compiler-checked sites (`layout_stub`'s is now derived):
|
|||
Plus `editor-core/src/barriers.rs`'s `subjects_of`, which the compiler forces.
|
||||
**Prefer deriving over extending** wherever the site allows it.
|
||||
|
||||
### Pin 9 — P13-S15 stays open
|
||||
### Pin 9 — explicit non-goal: G2b authorizes **no** pruning or compaction
|
||||
|
||||
**G2b does not authorize pruning or compaction of the canonical operation
|
||||
log**, and nothing in this packet may implement, enable, or prepare either.
|
||||
|
||||
`spec/PLAN_GENESIS_OPS.md` §3 requires this stated outright, and the reason is
|
||||
that G2b **sharpens** the standing prohibition rather than relaxing it. Before
|
||||
this rung, pruning was a performance concern: it would have discarded
|
||||
re-derivable state. **The moment G2b lands, pruning would discard *authored
|
||||
genesis state*** — the tuning context exists canonically only in the op log,
|
||||
because the canonical base embeds no graph values for any field.
|
||||
|
||||
The prohibition remains blocked on **disposition C** (the canonical base
|
||||
carrying graph values). There is no `fn prune` in the tree today, which is
|
||||
exactly why the prohibition is free now and would be catastrophic later. **If
|
||||
the implementation finds itself wanting a prune or compaction step for any
|
||||
reason, that is a finding to report, not a feature to add.**
|
||||
|
||||
### Pin 10 — P13-S15 stays open
|
||||
|
||||
The golden lock ends at 29 and **this rung must not extend it**. Adding 34 while
|
||||
30–33 remain unlocked would make the table look maintained while the gap
|
||||
|
|
@ -197,7 +241,88 @@ persists. S15 lands as its own rung with its own mutation evidence.
|
|||
|
||||
---
|
||||
|
||||
## 3. Tests — each with the mutation that must kill it
|
||||
## 3. Touch table
|
||||
|
||||
**Derived from G2a's actual footprint** (`git show 7df5ca1 --name-only`, thirty
|
||||
files) plus G1's one extra, then extended for what G2b does that neither did.
|
||||
It is a **floor, not a ceiling** — a touch outside it is a finding to report,
|
||||
but a file here that turns out not to need changing is fine, said plainly.
|
||||
|
||||
### Core — the new type
|
||||
|
||||
| # | File | Change |
|
||||
|---|---|---|
|
||||
| 1 | `core/src/graph.rs` | **new `TuningContextSettings`** (the five wire-bearing fields, in codec order); doc it as the authored subset of `ScoreTuningContext` and say why `accidental_extensions` is absent |
|
||||
| 2 | `core/src/lib.rs` | **public export** `epiphany_core::TuningContextSettings` (the ratified path) |
|
||||
| 3 | `core/src/codec.rs` | its `Codec` — **byte-identical to `ScoreTuningContext`'s existing five-field walk**; add the assertion that the two encodings agree |
|
||||
| 4 | `core/DECISIONS.md` | the subset ruling and its rationale |
|
||||
|
||||
### Ops — the operation
|
||||
|
||||
| # | File | Change |
|
||||
|---|---|---|
|
||||
| 5 | `ops/src/payload.rs` | `SetTuningContext` **kind 34** in the enum, the hand-written `discriminant()` match, `schema_major()` → **3** (pin 2), `tag()`, tag **34** inside `operation_kind_tag_vocabulary!`, and **`introduced_minor()` → epoch 10 in both spaces** (pin 4) |
|
||||
| 6 | `ops/src/reduce.rs` | the `WriteChain<TuningContextSettings>` — decl, snapshot, init, **seed**, setter, undo verdict, restoration apply, working-snapshot save/restore. **Copy `set_metadata` structurally** (pin 5) |
|
||||
| 7 | `ops/src/envdecode.rs` | envelope decode arm |
|
||||
| 8 | `ops/src/migrate.rs` | migration arm |
|
||||
| 9 | `ops/src/v0.rs` | v0-catalog arm |
|
||||
| 10 | `ops/src/valuegen.rs` | a generator for the payload |
|
||||
| 11 | `ops/src/vectors.rs` | **decode vectors pinned to literal bytes, not round-trip** (plan trap 4: a self-consistent reorder passed 1283 tests and 8/8) |
|
||||
| 12 | `ops/src/fuzz.rs` | fuzz arm |
|
||||
| 13 | `ops/src/textproj_kind.rs` | the kind **count** — hand-maintained (pin 8) |
|
||||
| 14 | `ops/src/lib.rs` | public exports |
|
||||
| 15 | `ops/DECISIONS.md` | the rung's decisions |
|
||||
|
||||
### Bundle — the accept-set raise (**new to G2b; G2a touched no bundle file**)
|
||||
|
||||
| # | File | Change |
|
||||
|---|---|---|
|
||||
| 16 | `bundle/src/bundle.rs` | `max_supported_major(OperationEnvelopeBlock)` **2 → 3** (:69) **and the rewritten rationale at :53-58** whose current text this rung falsifies (pin 3) |
|
||||
| 17 | `bundle/DECISIONS.md` | why the raise is charged to this surface alone |
|
||||
|
||||
### Boundary crossings — budgeted up front (pin 8)
|
||||
|
||||
| # | File | Change |
|
||||
|---|---|---|
|
||||
| 18 | `editor-core/src/barriers.rs` | `subjects_of` arm — **compiler-forced**; without it the workspace does not build and the gate cannot run at all |
|
||||
| 19 | `layout-ir/src/barrier.rs` | the "one past the vocabulary" literal → 35 |
|
||||
| 20 | `testkit/src/generators.rs` | the `rng.below(N)` bound |
|
||||
| 21 | `testkit/src/layout_stub.rs` | confirm the derived `PAYLOAD_FREE` path still holds — **prefer deriving over extending** |
|
||||
| 22 | `testkit/tests/text_projection_grammar.rs` | the kind **count** |
|
||||
|
||||
### Text projection
|
||||
|
||||
| # | File | Change |
|
||||
|---|---|---|
|
||||
| 23 | `textproj/src/parse.rs` | the kind production |
|
||||
| 24 | `textproj/src/project.rs` | the projection arm (G1 touched this; G2a did not — **check, don't assume**) |
|
||||
| 25 | `textproj/src/vectors.rs` | vector coverage for the new kind |
|
||||
| 26 | `textproj/src/lib.rs` | **`COMPANION_VERSION` 0.10.0 → 0.11.0** |
|
||||
|
||||
### Normative documents — the four-document ritual (pin 7)
|
||||
|
||||
| # | File | Change |
|
||||
|---|---|---|
|
||||
| 27 | `spec/binary_format.tex` | payload-layout row, tag row, the **accept-set/major-3 text**, the §2373 minor-additive history (kind 34 / epoch 10), version, Revision History row |
|
||||
| 28 | `spec/operation_catalog.tex` | a `\section{SetTuningContext}`, version, changelog |
|
||||
| 29 | `spec/core_spec.tex` | the **normative `OperationKind` *and* `OperationKindTag` listings**, plus any spelled-out payload count |
|
||||
| 30 | `spec/text_projection.tex` | kind production, companion 0.11.0, changelog |
|
||||
| 31–34 | `spec/binary_format.pdf`, `operation_catalog.pdf`, `core_spec.pdf`, `text_projection.pdf` | **all four regenerate and are committed** — every `.tex` source changes here |
|
||||
|
||||
### Vectors and tracking
|
||||
|
||||
| # | File | Change |
|
||||
|---|---|---|
|
||||
| 35 | `spec/vectors/decode_vectors.txt` | regenerate |
|
||||
| 36 | `spec/vectors/textproj_document_vectors.txt` | regenerate |
|
||||
| 37 | `spec/PASS13_CANDIDATES.md` | **close P13-S13**, citing this rung and the `metadata` precedent (pin 6) |
|
||||
| 38 | `spec/PLAN_GENESIS_OPS.md` | mark G2b complete; ladder advances to G3 |
|
||||
|
||||
**Already done by the ratification, do NOT redo:** epoch 10 is recorded in
|
||||
`spec/PLAN_GMINOR_SCHEMA_MINOR.md` §4. Transcribe it into code; do not edit that
|
||||
plan.
|
||||
|
||||
## 4. Tests — each with the mutation that must kill it
|
||||
|
||||
| # | Test | Required mutation |
|
||||
|---|---|---|
|
||||
|
|
@ -207,14 +332,14 @@ persists. S15 lands as its own rung with its own mutation evidence.
|
|||
| t4 | That block is **admitted** by the accept-set | Revert the cap to 2; must fail |
|
||||
| t5 | **The subset pin holds**: an op authored live and the same op reloaded from bytes produce **identical** graph states, with a pre-existing non-empty `accidental_extensions` **preserved across both** | Make the payload carry the full `ScoreTuningContext`; must fail — this is the pin's whole reason for existing |
|
||||
| t6 | Undo restores the previous five-field value | Restore the default instead of the predecessor; must fail |
|
||||
| t7 | Undo of the **first** authoring returns to never-written, distinguished from authored-to-default | Treat the `Score::empty` seed as a base write; must fail |
|
||||
| t7 | Undo of the **first** authoring restores the **seeded base** settings, and does so identically whether the seed was the default or a non-default value — with `accidental_extensions` untouched throughout | Skip `seed()` on the tuning chain during base ingest, so the first undo yields `NotWritten` instead of `Restore(Base)`; must fail. **Assert the two cases are indistinguishable**, not that they differ |
|
||||
| t8 | Kind 34 carries **epoch 10** and a block containing it stamps minor 10 | Assign epoch 9; must fail |
|
||||
| t9 | The from-empty spine still reaches a note, now with a tuning context authored | — regression guard; mutation is t2's |
|
||||
| t10 | The accept-set prose no longer claims no payload embeds the tuning context | Grep-assert the stale sentence is absent; restore it to see the test fail |
|
||||
|
||||
---
|
||||
|
||||
## 4. Gate
|
||||
## 5. Gate
|
||||
|
||||
`cargo fmt --check`; `cargo clippy --workspace --all-targets` **0 warnings**;
|
||||
`cargo test --workspace` green with the count; conformance suites with counts
|
||||
|
|
@ -223,10 +348,10 @@ vectors regenerated; **all four PDFs at 0 undefined references**, committing
|
|||
`binary_format.pdf`, `operation_catalog.pdf`, `core_spec.pdf` and
|
||||
`text_projection.pdf` (**all four `.tex` sources change here**, unlike G-minor);
|
||||
and `git status --short` **before and after**, whose only differences may be
|
||||
this contract's own touch set — the editor track's dirt must appear unchanged
|
||||
the §3 touch table — the editor track's dirt must appear unchanged
|
||||
in both.
|
||||
|
||||
## 5. Report
|
||||
## 6. Report
|
||||
|
||||
The gate outputs; every mutation with the failure actually observed; any touch
|
||||
outside this contract; and **any place where this contract's own assumptions
|
||||
|
|
|
|||
|
|
@ -177,6 +177,14 @@ numbering spaces are unrelated and must not be cross-read.
|
|||
| 7 | Push 4a | `OperationKind`/`OperationKindTag` 30; `PreconditionFailureReason` 14–15 |
|
||||
| 8 | Genesis G1 | `OperationKind`/`OperationKindTag` 31 |
|
||||
| 9 | Genesis G2a | `OperationKind`/`OperationKindTag` 32–33 |
|
||||
| 10 | Genesis G2b | `OperationKind`/`OperationKindTag` 34 (`SetTuningContext`) |
|
||||
|
||||
> **Epoch 10 ratified 2026-07-28**, with G2b as the event. This is the **first
|
||||
> exercise of the ladder's own growth path**: G-minor's `introduced_minor()` is
|
||||
> exhaustive with no wildcard arm, so kind/tag 34 *cannot compile* without an
|
||||
> epoch — the control working exactly as designed. The ladder stays monotonic
|
||||
> (G2b follows G2a) and prefix-closed. Epoch assignment remains a ratified
|
||||
> schema decision, never an implementer's choice.
|
||||
|
||||
**The ladder is complete against the audit** — every post-baseline variant in
|
||||
`AUDIT_GMINOR_VOCABULARIES.md` appears exactly once: all ten kind/tag pairs,
|
||||
|
|
|
|||
Loading…
Reference in New Issue