From faea317d4a3787a1101342d9e2b0539adaeb4112 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 9 Aug 2026 11:57:04 +0200 Subject: [PATCH] =?UTF-8?q?P13-S27=20amendment=201:=20=C2=A70.4=20missed?= =?UTF-8?q?=20a=20third=20constructor;=20four=20files=20had=20no=20touch?= =?UTF-8?q?=20row?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The first independent review of the staged execution returned five findings, three blocking. The pins were frozen at ratification, so these are an amendment with its own review round rather than patches. Section 0.4 never counted Bundle::create_versioned -- a third public constructor whose signature this rung changes, three sites, and zero mentions across nineteen review rounds. It searched Bundle::open( and Bundle::create( and concluded about "the writer surface". That is the fourth instrument failure recorded in that one section, and the same shape as the first three: a count taken from one spelling and generalised. The first could not see a propagating path, the second asserted a universal negative from head-truncated output, the third resolved a method name without resolving its type, and this one enumerated two of three constructors. That omission was the root cause of the second finding. testkit/gminor.rs calls only create_versioned, so it never appeared in any surface count and never got a touch row. Gate 4 failed during execution and caught it, along with three more files in no row: bundle/src/lib.rs, whose re-export pin 3 makes unavoidable since 92 converted sites in three crates cannot name a type the crate does not export, and the two crate-root capability helpers. Touch rows 13 through 16 added. production_caps() was unpinned design scope, not merely a missed path, and in epiphany-testkit it landed as new public API. Ruled under pin 3b: sanctioned, name pinned, visibility pinned per crate. pub(crate) in epiphany-textproj, a production crate whose five uses are all in-crate, so this rung adds no public API there. pub in epiphany-testkit, a test-support crate whose integration tests and benches are external consumers and cannot reach pub(crate). The direct-construction alternative is recorded as considered and rejected: it adds no API but repeats the same wrap 23 times, and "explicit" was never the same thing as "repeated". Row 12 named one counter where a label addition necessarily moves three: core requirements, suite requirements, suite labels. Execution found the other two through four failing tests in that file. The new writer comment was false, and this is the finding to carry because it is a false rationale attached to correct behaviour. It said self.manifest.canonical_base is always None at the commit-side check, but test 9 deliberately performs an unrelated second commit on an inherited Some base. What actually holds is narrower: an inherited base can be present but never stale, because open refuses a stale one and create refuses a base-bearing manifest. So narrowing pin 3a to "any stale inherited base" is unobservable while broadening it to "any base-bearing commit" is very observable and wrong. The scope is forced on one axis and a real choice on the other, and the comment collapsed the two. Corrected in the staged code. The contract itself never made the claim -- section 7 item 10 says "stale inherited base", which is exactly right. Review confirmed M7 internally coherent against the final tree: B_raw requiring one normalisation step matches the probe history, and the mismatched-base control reaches the staged writer check and produces the required error. No additional M7 contradiction found. The staged implementation is NOT accepted. This amendment needs another independent pass first. The implementation remains staged and uncommitted. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x --- spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md | 115 +++++++++++++++++++- 1 file changed, 110 insertions(+), 5 deletions(-) diff --git a/spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md b/spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md index 2d768c9..6e2d324 100644 --- a/spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md +++ b/spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md @@ -6,9 +6,17 @@ findings.** **DISPATCHED for execution.** Which rounds closed, what each found, and the running tally are **the history table below**; this line does not restate them, having gone stale in two consecutive rounds by doing so. -**THE PINS ARE NOW FROZEN. They may be executed, not edited.** A defect found -during execution is **reported, not patched in place** — if it needs a pin -change, that is its own amendment with its own review round. +**THE PINS ARE FROZEN. They may be executed, not edited.** A defect found during +execution is **reported, not patched in place** — if it needs a pin change, that +is its own amendment with its own review round. + +**IMPLEMENTED 2026-08-09, STAGED, and NOT YET ACCEPTED.** The first independent +review of the staged execution returned **five findings, three blocking**, all +carried by **post-ratification amendment 1** (below). That amendment took the pin +changes the findings required — §0.4's missing constructor surface, four touch +rows, and a ruling on `production_caps`'s visibility — and therefore **needs +another independent pass before completion is accepted.** The work remains staged; +nothing is committed. **Round 1's ratification was WITHDRAWN**, and the distinction matters. It was claimed on 2026-08-07 after a single round; round 2 then found four more blocking @@ -187,7 +195,8 @@ rows — read it off, do not restate it. | round 17 | 10 | 5 | authored-side scan | | round 18 | 2 | 2 | **yes** | | **round 19** | **0** | **0** | **yes — first clean round** | -| **Total** | **65** | **47** | one amendment per row | +| execution review 1 | 5 | 3 | **yes — against the staged tree** | +| **Total** | **70** | **50** | one amendment per row | **This block previously read "amended three times … fifteen findings so far, eight of them blocking"** — the round-2 figures, left standing through rounds 3 @@ -590,6 +599,42 @@ sweep bought coverage of two unscanned sections at the cost of two new defects i what it wrote. That is the trade the history table now shows for every large amendment. +**Post-ratification amendment 1 — 2026-08-09, on the first independent review of +the STAGED EXECUTION.** Five findings, **three blocking**. The pins were frozen at +ratification, so these are an amendment with its own review round rather than +patches — which is the discipline working as designed: **execution reported, and +review of the report found what nineteen paper rounds had not.** + +| # | Finding | Disposition | +|---|---|---| +| **1** | **§0.4 never counted `Bundle::create_versioned`** — a third public constructor whose signature this rung changes, 3 sites, **zero mentions across nineteen rounds**. §0.4 searched `open(` and `create(` and concluded about "the writer surface" | Surface added to §0.4 and recorded as its **fourth instrument failure** — a count taken from one spelling, the same shape as the first three | +| **2** | **Gate 4 correctly failed: four required files were in no touch row**, and the staged patch alone cannot build. `bundle/src/lib.rs` (the re-export pin 3 makes unavoidable), `gminor.rs`, and the two crate-root helpers | **Touch rows 13–16** added | +| **3** | **`production_caps()` was unpinned design scope**, not merely a missed path — and in `epiphany-testkit` it landed as new **public** API | **Ruled** under pin 3b: sanctioned, name pinned, visibility pinned per crate — `pub(crate)` in the production crate, `pub` in the test-support crate whose tests and benches are external consumers. The direct-construction alternative is recorded as considered and rejected | +| 4 | **Row 12 named one counter; a label addition necessarily moves three** — core requirements, suite requirements, suite labels | Row 12 amended to name all three, with the line numbers | +| 5 | **The new writer comment was false.** It said `self.manifest.canonical_base` "is always `None` here", but **test 9 deliberately performs an unrelated second commit on an inherited `Some` base** | Corrected in code. The contract itself never made this claim — §7 item 10 says "stale *inherited* base", which is exactly right | + +**Finding 5 is the one to carry, because it is a false rationale attached to +correct behaviour.** The check does the right thing; the comment justified it with +a reachability claim that a test in the same rung disproves. **What actually holds +is narrower:** an inherited base *can* be present, but never *stale* — `open` +refuses a stale one and `create` refuses a base-bearing manifest. So **narrowing** +pin 3a to "any stale inherited base" is unobservable, while **broadening** it to +"any base-bearing commit" is very observable and wrong. The scope is forced on one +axis and a real choice on the other, and the comment collapsed the two. + +**Finding 1 is the fourth instrument failure in one section**, and its cost was +finding 2: `gminor.rs` calls *only* `create_versioned`, so no surface count ever +reached it, so no touch row existed, so gate 4 failed. **The allowlist caught what +the count missed** — which is what an allowlist is for. + +**Review confirmed M7 internally coherent against the final tree**: `B_raw` +requiring one normalisation step matches the probe history, and the mismatched-base +control reaches the staged writer check and produces the required error. **No +additional M7 contradiction found.** + +**Status: the staged implementation is NOT accepted.** This amendment needs +**another independent pass** before it can be. + **Review round 19 — 2026-08-08, independent, against the round-17/18 working tree. ZERO FINDINGS. The first clean round in nineteen.** @@ -877,6 +922,28 @@ production path, because there is not one. *Re-counted 2026-08-07 at `96b40b2`: still 32, and every per-file figure above still holds.* +**Writer surface, part two — 3 `Bundle::create_versioned(` sites. ADDED BY THE +POST-RATIFICATION AMENDMENT, 2026-08-09, on a finding from execution.** + +`bundle.rs` **2** (`:2326`, `:2367`), `testkit/gminor.rs` **1** (`:85`). + +> **This surface was missing from the contract entirely — zero mentions across +> nineteen review rounds.** `create_versioned` is a **third public constructor** +> whose signature this rung changes, distinct from `create` (which delegates to +> it). §0.4 searched `Bundle::open(` and `Bundle::create(` and concluded about +> "the writer surface". +> +> **This is the fourth instrument failure recorded in this section, and the same +> shape as the first three:** a count taken from one spelling and generalised. The +> first could not see a propagating path; the second asserted a universal negative +> from `head`-truncated output; the third resolved a method name without resolving +> its type; **this one enumerated two of three constructors.** +> +> **It is also the root cause of a touch-table gap.** `testkit/gminor.rs` calls +> *only* `create_versioned`, so it never appeared in any surface count and +> therefore never got a touch row — found by gate 4 failing during execution, +> exactly as an allowlist should. + **`commit` sites** — pin 3's design keeps every one of them unchanged. > **CORRECTED 2026-08-07 in review round 1. The claim this paragraph made was @@ -1215,6 +1282,40 @@ format and container fixtures deliberately exercising arbitrary wire values and Every call site converted by this rung uses one or the other **explicitly**; none may take a value that merely happens to be in scope. +### The real-authority side gets a named constructor. RULED BY THE POST-RATIFICATION AMENDMENT, 2026-08-09. + +**The question this settles**, raised by execution and pressed by review: pin 3b +named the *synthetic* constructor and left the **real-authority** side as "wrap +`epiphany_ops::CURRENT_REDUCTION_ALGORITHM_VERSION`", which is a value, not a +name. Execution introduced a `production_caps()` helper per crate to satisfy +"explicitly" without repeating the wrap 23 times — **unpinned scope**, and in +`epiphany-testkit` it landed as new **public** API. + +**Ruled: the helpers are SANCTIONED, with visibility pinned per crate.** + +| Crate | Visibility | Why | +|---|---|---| +| `epiphany-textproj` | **`pub(crate)`** | A **production** crate. Its five uses are all in-crate, so this rung adds **no public API** to it. `pub` here would be unpinned surface on a shipping crate | +| `epiphany-testkit` | **`pub`** | A test-support crate that exists to be consumed. Its **integration tests and benches are external consumers** (`tests/bundle_reopen.rs` 2 uses, `benches/bundle.rs` 3) and **cannot reach `pub(crate)`**. A capability constructor is precisely what this crate exists to provide | + +**Rejected alternative — direct construction at all 23 sites.** It adds no API, +but repeats the same wrap 23 times, and "explicit" was never the same thing as +"repeated". The named helper *is* explicit: it says which side of pin 3b's split +the site is on, and gate 6a can distinguish the two by name. + +**Consequences, listed rather than left implicit:** + +- The helper is named **`production_caps`** in both crates. Like + `synthetic_for_fixture`, the name is **pinned**, because it is the token that + distinguishes a real-authority site from a fixture one under review. +- **`epiphany-testkit`'s external consumers use it by path** + (`epiphany_testkit::production_caps()`); the crate-internal ones use + `crate::production_caps()`. +- **Touch rows 13 and 14** carry the two crate roots. +- **A `pub(crate)` helper in a production crate is not public API**, so gate 5's + spirit — this rung adds no dependency and no surface `epiphany-ops` must + honour — is preserved for `epiphany-textproj`. + **Pin 4 — the mismatch is a hard error.** ```rust @@ -1344,7 +1445,11 @@ row may not record S16 as open until those land with this rung**; ratification o | 9 | `crates/epiphany-textproj/src/{serialize,project}.rs` | call sites, real authority | | 10 | `spec/core_spec.tex` (+ `.pdf`) | pin 9 | | 11 | `spec/PASS13_CANDIDATES.md` | pin 10 | -| 12 | `crates/epiphany-testkit/tests/requirement_labels.rs` | **conditional** — pin 9, *only if* it mints a new `\label{req:...}`; `CORE_REQUIREMENT_COUNT` (`:15`) then moves 213 → 214. Added in review round 1. If pin 9 mints no label, leave unmodified and say so in the report | +| 12 | `crates/epiphany-testkit/tests/requirement_labels.rs` | **conditional** — pin 9, *only if* it mints a new `\label{req:...}`. **ALL THREE counters move, not one** (amended 2026-08-09): `CORE_REQUIREMENT_COUNT` (`:15`) 213 → 214, **and** `SUITE_REQUIREMENT_COUNT` (`:18`) and `SUITE_LABEL_COUNT` (`:19`) 284 → 285, because the suite totals include `core_spec`'s requirements and its labels. The original instruction named only the first; execution found the other two through **four** failing tests in this file. If pin 9 mints no label, leave unmodified and say so in the report | +| 13 | `crates/epiphany-bundle/src/lib.rs` | **ADDED 2026-08-09.** Pin 3's `BundleCapabilities` is required at `open`/`create`, so **callers in other crates need it re-exported** — 92 converted sites across three crates cannot name a type this crate does not export. Unavoidable, and carried by no row through nineteen rounds | +| 14 | `crates/epiphany-testkit/src/lib.rs` | **ADDED 2026-08-09.** `pub fn production_caps()` — pin 3b's real-authority constructor, `pub` because this crate's integration tests and benches are external consumers | +| 15 | `crates/epiphany-textproj/src/lib.rs` | **ADDED 2026-08-09.** `pub(crate) fn production_caps()` — same constructor, **crate-private** because this is a production crate and all its uses are in-crate | +| 16 | `crates/epiphany-testkit/src/gminor.rs` | **ADDED 2026-08-09.** One `Bundle::create_versioned` site (`:85`). Missing because §0.4 never counted that constructor — see the amendment note there. This file calls **only** `create_versioned`, so no surface count reached it | **Row 12 is conditional, and that is deliberate.** `CLAUDE.md` names this file as a recurring escapee, and it escaped the format-epoch rung's table. Carrying it