2 commits

Author	SHA1	Message	Date
mrwulf	b3f4ee0d33	verification: pin the harness, the audit drivers and the policy files (P1-c) ... Every gate this repository has was executed by scripts that nothing pinned. Round-5 review of the companion SLH-DSA repository stubbed the compiler wrapper alone and its button printed ALL GREEN in 3.6 seconds over deliberately destroyed proofs; flipping two guards in the audit driver disabled every check with the digest byte-identical. Depth of checking is worth nothing if the thing doing the checking is unbound — and every gate added this week made that gap more valuable to an attacker, not less. Phase 0c requires every harness file to match HARNESS.sha256. Two design points carry the weight: - WHICH files must be pinned is POLICY and lives in check.sh, never in the map being consulted. If the required set were read from the pin file, deleting an entry would silently un-pin that file. It is instead derived from the filesystem, so a deleted entry is a set mismatch and a build failure. That is the exact defect SLH-DSA round-6 found, closed here by construction. - Membership self-derives from the executable bit: anything this script can shell out to must be pinned, so a NEW script fails closed until someone pins it deliberately. Load-bearing files that are not executable — the audit driver, the committed manifests, the policy tables — cannot be discovered that way and are listed explicitly. lean-guard is inside the set, which finally makes the standing "lean-guard stays hash-pinned" rule a property of the repository rather than a convention. selftest-harness.sh replays five cases, each asserting a specific diagnostic: an edited lean-guard, a new unpinned executable, a deleted pin entry, a missing pin file, and a positive control. It was itself negative-tested — with the hash comparison removed it goes red on exactly that case while cheerfully reporting "10 harness files match their pins". TRUSTED-BASE.md states the limit at equal length to the claim: pinning a harness from inside that harness is circular, and an author who edits a script and refreshes its pin in the same commit passes every phase. What the pin changes is that the edit can no longer be SILENT — it must appear in the diff at the commit being reviewed. A green button says "this is the apparatus that was reviewed", never "this apparatus is trustworthy". Also fixed, found by this sweep: both self-tests compared the working tree against its starting state with `diff <(echo "$VAR") <(command)`, which is asymmetric — for a clean tree the variable is empty and `echo` emits a blank line the command does not. It reported a difference precisely when nothing was wrong, and only surfaced once P1-a was committed and Proofs/ became clean. Both now compare as strings. Verified green: 20 runs across the four ed25519 repositories (four buttons, four harness self-tests, four axiom-gate self-tests, four binding self-tests, four scalar buttons), zero red. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-07-29 20:12:58 +02:00
mrwulf	21f80d29eb	verification: bind the statements, the specifications, and the model (P1-a) ... Phases 3/3b establish what each certificate RESTS ON. Neither says what it SAYS, nor what it is ABOUT. A certificate gutted to a tautology of the same axiom cone passes both; so does one whose reference definition has been redefined to BE the extracted code, at which point the theorem reads `loop = loop` and every cone is byte-identical. Phase 3c closes that. Proofs/Audit.lean emits a canonical block holding the policy constants, every certificate's fully-elaborated statement (pp.all, so implicit arguments, instances and universe levels are visible), and the body of every specification constant transitively reachable from those statements. Its SHA-256 is pinned in check.sh and the block itself is committed as AUDIT-MANIFEST.txt, so a mismatch is DIFFED, not merely reported. 31 certificates, 68 specification constants per repository. Two tiers, not one. These forks have an arithmetic tier that must stay oracle-free and an apex tier carrying this fork's hash and wire-format axioms, and the apex boundary genuinely differs per fork (dalek 8 extra names, anza 4, risc0 and betrusted 5). One shared constant would have widened the arithmetic tier to accept hash oracles, which is the most valuable property these repos have. Each auditor is generated from its own repository's policy. Phase 0b pins the extracted model. This was not a precaution: risc0 and betrusted were observed emitting BYTE-IDENTICAL audit-manifest digests (6c821b8e…) while shipping demonstrably different extracted models, their point-doubling routines differing in operation order. A statement names an extracted function; it does not contain that function's body. Binding statements is not binding the subject. Membership derives from the filesystem, so a new model file fails closed. selftest-statements.sh attacks both phases with ten cases, each asserting a specific diagnostic: an edited model body, an unlisted model file, a widened policy, a hand-edited committed block, a certificate dropped from the auditor WITH the digest refreshed to match, and a gutted statement whose cone is unchanged. It lifts the phases out of check.sh at run time, so it attacks the shipping gate rather than a copy. Two bugs found and fixed during that testing, both mine: Phase 3c read `$0` after `cd "$AENEAS_LEAN"`, and $0 is the caller's relative path; and the axgate self-test compared the tree against a pristine checkout rather than against how it found it. A third expectation was wrong rather than the code — widening the apex boundary is caught by the exact-cone requirement before the digest ever runs, which is a stronger rejection, and the test now says so. All sixteen runs green at these commits: four main buttons, four axgate self-tests, four binding self-tests, four scalar buttons. TRUSTED-BASE.md records what this binds and, at equal length, what it does not: a digest binds identity, not meaning; an author can rotate the pins in one commit and is caught by review, not by the script; and pinning the model says nothing about whether Charon and Aeneas translated the Rust faithfully. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-07-29 00:38:19 +02:00