docs(remediation): promote two first-class principles to the charter; dispatch RM-02 round 3
Mos ruled both open questions and promoted the pattern to the charter. PRINCIPLE 1 — the anchor must live outside the audited party's authority. You cannot fix "the author controls X" by deriving X from something the author also controls; deriving only MOVES the control point. Third independent arrival of one conclusion, each reached while shipping something else and each from a different direction: the manifest certifying its own tree (D-19), the sandbox evaluating code that enters before the boundary exists (D-25), and now the registry seam derived from a path the author also places (D-45). Three impossibility-derivations of the same conclusion is the strongest architectural evidence this mission has produced, and it is what forces Builds 1-2 rather than making them a preference. PRINCIPLE 2 — no universally-quantified check may pass over an empty set. "All registered cases ran" is vacuously true when there are none. Non-emptiness and anchoring are preconditions asserted before the quantified check runs, not properties hoped for after. The identical vacuity appeared twice at two levels — seam=HEAD emptied the commit range, an emptied manifest emptied the registry population — and the first was fixed as an instance, so it returned one level up. Corollary, same disease: a clause written for the instance that produced it is not a clause. Q1 ruled: the merge-base anchor IS in scope for f10-coder in this PR. It is git-computable against main, which the author does not control, so reordering or splitting within the branch cannot move it — an existing non-author-controlled reference, no new infrastructure. RM-60's execution boundary is a sibling under the same principle but a different mechanism (where gate-verify runs, not what the anchor is) and stays with Mos and Jason. Honesty required in both directions: the merge-base anchors to main, whose integrity rests on the merge discipline this registry enforces — a bootstrap, sound against an author who cannot rewrite main and NOT sound against an attacker who can, with that residual bound to the Builds 1-2 dependency rather than implied. Q2 ruled: state the empty-set principle as a general clause now, and generalize the D-38/D-40 criteria the same way — quantify over the population instead of relabeling the originating instances. Round 3 dispatched to f10-coder: merge-base anchor plus delayed-introduction must-fail; empty-set precondition as a general clause with an emptied-registry must-fail; generalized clauses bound across the gate inventory; each red-first. Number.isInteger accepting zero/negative/unsafe pipeline numbers banked as a non-blocking follow-up. Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>
This commit is contained in:
co-authored by
Claude Opus 5
parent
09875143c0
commit
4520d2f672
@@ -117,6 +117,51 @@ gate/program; the LLM handles only genuine judgment.
|
||||
> not yet a hypothesis. Where the answer is consequential, **reproduce** rather than accept — two
|
||||
> independent runs beat one confident report.
|
||||
|
||||
### First-class principle — the anchor must live outside the audited party's authority
|
||||
|
||||
> **You cannot fix "the author controls X" by deriving X from something the author ALSO controls.**
|
||||
> Deriving merely **moves** the control point; it does not remove it.
|
||||
>
|
||||
> Promoted to the charter by Mos (2026-08-01) on the **THIRD INDEPENDENT ARRIVAL** of the same
|
||||
> conclusion, each reached while trying to ship something else, each from a different direction:
|
||||
>
|
||||
> | arrival | the audited party controls… | found as |
|
||||
> | ----------------- | ------------------------------------------------------------------- | -------- |
|
||||
> | manifest | the tree that certifies its own generated state (same-UID, CWE-345) | **D-19** |
|
||||
> | sandbox | the code that enters the sandbox, before the boundary exists | **D-25** |
|
||||
> | **registry seam** | **WHEN the tracked path is introduced, hence the derived boundary** | **D-45** |
|
||||
>
|
||||
> Round 1 the value was an author-settable **field**, so it was **derived**. Round 2 the derivation
|
||||
> depended on **when the author introduces the path**. Same authority, new costume. **Three
|
||||
> impossibility-derivations of one conclusion is not a coincidence to note — it is the strongest
|
||||
> architectural evidence this mission has produced**, and it is precisely what **forces Builds 1–2**
|
||||
> rather than making them a preference.
|
||||
>
|
||||
> **Operationally:** anchor to a reference the audited party cannot move. A git **merge-base against
|
||||
> `main`** is such a reference for a PR author (they own their branch; they do not own `main`).
|
||||
> **State the bootstrap in BOTH directions (D-19):** that anchor is sound against an author who cannot
|
||||
> rewrite `main` — the threat in scope — and **NOT** sound against an attacker who can. **That residual
|
||||
> is what Builds 1–2 close, and it must be recorded as a tracked dependency, never implied.**
|
||||
|
||||
### First-class principle — no universally-quantified check may pass over an empty set
|
||||
|
||||
> **"All registered cases ran" is VACUOUSLY TRUE when there are no registered cases.**
|
||||
> **Non-emptiness and anchoring are PRECONDITIONS asserted before the quantified check runs — not
|
||||
> properties hoped for after it.**
|
||||
>
|
||||
> Promoted by Mos (2026-08-01) after the identical vacuity appeared **twice, at two different levels**:
|
||||
> `activationCommit = HEAD` emptied the **commit range** (D-44), and an emptied manifest — `criteria`,
|
||||
> `gates`, `proseClaims`, `compatibilityScenarios` all `[]` — emptied the **registry population**
|
||||
> (D-46), each yielding **exit 0**. The first was fixed **as an instance**; the principle was never
|
||||
> extracted, **so it returned one level up.**
|
||||
>
|
||||
> **Delete every gate and every criterion TOGETHER and no remaining reference complains — because every
|
||||
> reference went with them.** A check that quantifies over a population must actually **range** over it,
|
||||
> and that population must be **provably complete and non-empty**.
|
||||
>
|
||||
> **Corollary (same disease):** a clause written for the instance that produced it is not a clause.
|
||||
> **Do not relabel the originating instances as the general clauses** — quantify over the population.
|
||||
|
||||
### First-class principle — redundant observation on evidence-bearing steps
|
||||
|
||||
> **Two observers of the same evidence, disagreeing, catch what neither catches alone.** Apply redundancy
|
||||
|
||||
Reference in New Issue
Block a user