# AUDIT.md — the executable audit protocol (FR-008)

Written for an agent: every claim maps to a command with an expected outcome. Run them
all; report PASS/FAIL per claim. A claim with no command is not a claim.

STATUS: the protocol below covers the claims the current tree makes. The proof claims
(T-*) land with `proofs/` (tasks T008/T009) and are listed as PENDING so their absence
is loud, not silent.

## Claims

**C1 — the budget.** The seed tree is at most 2,000 code lines.
    `./check.sh` gate 1 → prints the count, exits 0.

**C2 — the dependency floor.** Direct deps are exactly the ten-crate cryptographic
floor; no async runtime, serde, or HTTP client anywhere in the graph.
    `./check.sh` gates 2–3 → exit 0.
    `cargo tree -e normal` → inspect: every crate is one of the floor or a transitive
    internal of it (curve25519-dalek under x25519-dalek; cipher/poly1305 under the
    chacha pair; digest/hmac under sha2/hkdf; proc-macro2/quote/syn are zeroize_derive's
    BUILD-TIME derive machinery and emit no runtime code).

**C3 — nothing dead ships.** `#![deny(dead_code)]` with zero allow-escapes in the tree.
    `grep -rn "allow(dead_code)" src vendor` → no output.
    `cargo build` → no warnings, no errors.

**C4 — vendor provenance.** Every vendored file names its upstream file and commit on
line 1; the pruned items are listed in the header; kept bodies are byte-faithful.
    `./check.sh` gate 5 → exit 0.
    Spot-check: `git -C .. show d19b5db:protocol/sphinx/src/payload.rs` vs
    `vendor/sphinx/payload.rs` — every kept function identical.

**C5 — parsers do not panic.** The index and reply parsers return `None` on arbitrary
input.
    `cargo test` → the `never_panic` tests pass. PENDING: Kani harnesses (T008)
    replace sampling with bounded proof.

**C6 — the trust root is compiled in.** No file read, no DNS, no fetch of trust
material; the only network sink is the pinned relay endpoint.
    `grep -rn "std::fs" src` → exactly the version-state read/write and the staged
    artifact write in main.rs (US2 and T-WRITE's subjects).
    `grep -rn "UdpSocket\|connect\|send" src` → one socket, `connect` only to
    `directory::RELAYS` endpoints. PENDING: T-SINK as a checked theorem (T009).

**C7 — an unstamped seed says so.** DEV_PIN true refuses to run without `--dev`.
    `cargo run` → exits non-zero naming the DEV pin.

## The TCB statement

(Verbatim from contracts/theorems.md once proofs land — printed here so the trust
boundary is in the auditor's face, not a reference away.) Until T009: the checks above
are measurements and tests, not proofs; they bound what ships, not what executes on
every input.