mrwulf
c848a490ff
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>
5.6 KiB
Trusted base
What you must believe for the theorems in this repository to transfer to the running Rust code. Everything else is machine-checked.
-
Lean 4 kernel (v4.30.0-rc2) and its three foundational axioms
[propext, Classical.choice, Quot.sound]. Every certificate is#print axioms-audited against exactly this list. -
mathlib (prebuilt oleans fetched by
lake exe cache get). -
Charon + Aeneas (pinned
9dd7f23c/bf13c42e): the translation from Rust MIR to the Lean model is assumed faithful. The generatedgen/files are never edited (comments only); proofs are stated ABOUT them. -
External-function models (
gen/*/FunsExternal.lean): Rust items that Aeneas cannot translate (constant-timesubtleprimitives, iterator plumbing, formatting) are axiomatized as opaque symbols. The axiom audit proves none of these axioms enters the dependency cone of any certificate, except where a model is explicitly listed below. -
The signature-apex boundary (signature layer only): FOUR apex-tier certificates —
CurveFieldProofs.verify_accepts_iff(byte apex: accepted iff compress([s]·B − [k]·A) = R byte-for-byte),verify_accepts_iff_point(half-lift: R is the canonical encoding of the recomputed point),verify_accepts_iff_point_eq(point equation: canonically-encoded Q accepted iff Q equals the recomputed point), andverify_accepts_iff_decompress(full lift: R decompresses to a valid on-curve point that equals the recomputed point) — are each#print axioms-audited by check.sh Phase 3b against EXACTLY the standard three plus this documented set, and the build fails on any deviation:ed25519.Signature(wire-format type), the single SHA-512 oracleverifying.sha512_hash3(semanticallySha512(R ‖ A ‖ msg)),ed25519.Signature.to_bytes, andsignature.error.Error/Error.new(opaque error type). The hash is an oracle with no algebraic properties assumed — the theorems hold for whatever bytes it produces; the SHA-512 implementation itself is NOT verified. Zero curve, scalar, or backend axioms are in any of the four cones. The constructive decompress theorem underneath the full lift (decompress_of_canonical) carries the standard three axioms ONLY. -
Compilation of Rust to machine code (rustc backend) is out of scope, as is side-channel behaviour (timing, speculation). The proofs are about functional correctness at the MIR/LLBC level.
-
What the axiom gate binds, and what it does not.
check.shPhase 2b reads every compiledProofs/*.oleanand fails the build if any declaration there is an axiom. It asks the kernel rather than parsing source text, because the source-text check in Phase 1 is evadable four ways — an indentedaxiom,@[simp] axiom,unsafe axiom, andaxiomwith the name on the following line all compile and all miss its pattern. Membership self-derives from the filesystem, soScalar*andAxiomCheckare covered as well, and the count of compiled modules must equal the count of shipped sources, so a deleted.oleancannot make the scan pass vacuously.selftest-axgate.shattacks the shipping gate rather than a copy of it, and was itself negative-tested by removing the gate's error. The residue you must still supply yourself: this binds declarations, not statements. Nothing in the button establishes that a certificate's theorem says what its name — or this document — suggests it says. A theorem gutted to a tautology with the same axiom cone would pass every phase. Reading the statements remains a human act. -
What the statement binding covers.
check.shPhase 3c compilesProofs/Audit.lean, which emits a canonical block containing the policy constants, every certificate's fully-elaborated statement (pp.all, so implicit arguments, instances and universe levels are all visible), and the fully-elaborated body of every specification constant transitively reachable from those statements. The SHA-256 of that block is pinned incheck.shand the block itself is committed asAUDIT-MANIFEST.txt, so a mismatch is diffed rather than merely reported. This is what makes a certificate gutted to a tautology of the same axiom cone fail, and what makes a reference definition redefined to BE the extracted code fail — two attacks that move no cone at all. Phase 0b separately pins the bytes of every extracted-model file undergen/, with membership derived from the filesystem so a new model file fails closed.The residue you must still supply yourself. Three things, stated plainly because a reader would otherwise assume them:
· A digest binds identity, not meaning. The audit proves the statements are the ones that were reviewed. Whether those statements say something worth believing about ed25519 is a question only a human reading them answers.
AUDIT-MANIFEST.txtis committed precisely so that reading is possible without re-running anything.· An author can rotate the pins. Editing a statement and refreshing the digest in the same commit passes every phase. The defence is that both changes are visible in the diff, reviewed at the pinned commit — not that the script prevents it. No harness audits its own author.
· Phase 0b pins the model; it does not verify the translation. That the bytes under
gen/are the reviewed bytes says nothing about whether Charon and Aeneas translated the Rust faithfully. That assumption is item 3 above and is unchanged.