From 3fda93bc6bff33b9d16ced1bac96df07b9bc5b7d Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Tue, 11 Aug 2026 20:52:34 +0200 Subject: [PATCH] P13-S26 amendment 4 EXECUTED: section 8.4's M27 sentence corrected Section 8.4's M27 entry said M27 varies which clause is chosen. It now says each of M22-M26 presupposes that selection succeeded and M27 attacks whether selection is permitted at all. M25 is what varies which clause is chosen; a correct implementation rejects M27 before selecting any clause. Section 8.6 is untouched and verified so with a zero-context diff: its sentence appears in the staged diff only as hunk context, never as an addition or a deletion. It says M27 was the step no mutation had reached, which is true, and an earlier draft of amendment 4 would have rewritten it. Contract-only, three hunks: the replaced sentence, section 9's landed status literal, and section 9's historical marker naming amendment 4. No annex edit -- its record that the correction was open as of bff7be0 remains true. Baseline unchanged at 43 suites, 1586 passing; this commit changes prose only. Section 9.6's gate observed, all items: one path staged; within section 8.4's M27 entry the old sentence absent and the replacement present exactly once; section 8.6 unchanged under zero context; within section 9's slice the landed literal and an amendment-4-specific marker present; diff check clean. One nuance in the ratified gate rationale is worth recording rather than patching, since section 9 is frozen. Item 2 argues the scope is mandatory because a file-wide form is unsatisfiable, section 9.1 quoting the old sentence and 9.3 the replacement. Measured: under a normalising reader -- blockquote prefixes stripped, whitespace collapsed, which is how every guard in this repository reads .tex -- file-wide is indeed 1 and 2, and unsatisfiable. Under raw exact matching against the source's own line wrapping it is 0 and 1, and would pass. Section 9.6 does not say which reader it means. The scoping is right under either, and item 4's scope is mandatory under both, the file carrying eleven copies of the landed literal. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x --- spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md b/spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md index c6e34a3..833aa89 100644 --- a/spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md +++ b/spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md @@ -2474,9 +2474,9 @@ implementation asserts exactly one `\MUST{}` in the block, finds two, and **fails** before clause selection begins. An implementation that silently takes the **first** occurrence selects the original normative sentence as its clause — which still contains `ordering`, `bounds`, `same region` and `\MUST{}` — and -**passes every clause assertion**. Nothing in M22–M26 separates those two: they -all vary the *contents* of the clause, and this one varies which clause is -chosen. +**passes every clause assertion**. Nothing in M22–M26 separates those two: each +of them presupposes that selection succeeded, and this one attacks whether +selection is permitted at all. *Must fail:* test 3, **alone**. @@ -2537,11 +2537,15 @@ step 1 and, until this round, the only step no mutation reached. ## §9. AMENDMENT 4 — §8'S CHARACTERIZATION OF M27 -STATUS: RATIFIED; DISPATCHED to correct §8's M27 characterization. +STATUS: LANDED by this commit. -**Ratified 2026-08-11 on the authority of the repository owner**, the last -review pass returning zero findings. Amendment 3 is ratified at `7c8a30d` and -executed at `bff7be0`; **this amendment does not reopen it**, changes no +> **DATED HISTORICAL RECORD — amendment 4 is ratified and executed. §9's +> findings, its taxonomy and §9.5's dispositions are an account of what was +> found and decided on 2026-08-11, and state no current condition.** + +**Ratified 2026-08-11 at `a347a03` on the authority of the repository owner**, +the last review pass returning zero findings. Amendment 3 is ratified at +`7c8a30d` and executed at `bff7be0`; **this amendment does not reopen it**, changes no selector rule, no mutation, no radius and no lifecycle transition. It corrects **one explanatory sentence**, and nothing else. The replacement is executed, not edited; a further defect is its own amendment with its own review round.