# Contract: the theorem set (FR-009) What "provably does what it says" means here, exactly. Each theorem is stated over the Lean model extracted from the seed's Rust (Aeneas/Charon, pinned at plan time), named so AUDIT.md can map it to its `lake build` target. The list is closed: a safety claim not theoremized below is either given a theorem or not made. ## T-PARSE — parsers are total and exact For the index parser and the reply parser (the seed's only two input grammars): 1. No input causes a panic or non-termination (totality over arbitrary bytes). 2. `parse (emit x) = some x` for every well-formed value (round-trip). 3. `parse b = some x → emit x = b` up to the contract's canonical form — the parser accepts EXACTLY the grammar in contracts/, nothing else (no parser differential to hide in). ## T-WRITE — nothing unverified reaches the disk Every trace of the seed model that performs the final artifact write contains, earlier in the trace, a successful `ed25519_verify(release_key, index_bytes) = true` AND `sha256(artifact) = index.entry.digest` AND the per-piece `blake3` checks for every piece composing the artifact. (The staging path is modeled; only the final rename is the guarded effect.) ## T-SINK — one network sink, pinned The model's effect signature contains exactly one send target: the UDP endpoint chosen from the compiled-in relay table. No trace sends bytes anywhere else; no trace reads any name-resolution or configuration source. This is the structural no-fallback property (049 T011's ancestor) as a checked theorem. ## T-ROLLBACK — version monotonicity is enforced Any trace that accepts index version `v` after having durably recorded `v' > v` terminates in the refusal path, not the fetch path; and the stale-seed horizon gate cannot be passed without the explicit override input. ## T-BOUND — the seed is finite Retries per piece ≤ 3; total requests bounded by `piece_count + retries`; every loop in the model carries a decreasing measure (Lean totality makes this structural, but the bound VALUES are asserted so the theorem breaks if a constant drifts). ## T-FORMAT — the packet is the format The sphinx packet and SURB the model constructs satisfy a Lean specification of the wire layout (sizes, field offsets, layer count = 3) written from contracts/seed-fetch.md and the sphinx constants — proving the seed implements the format. Explicitly NOT proved: that Sphinx-the-design provides anonymity (literature, axiom), or that the crypto crates implement their primitives correctly (axiomatized opaque specs; they are FR-002's audited-elsewhere floor). ## The TCB statement (printed verbatim in AUDIT.md) These theorems are checked by the Lean kernel and hold of the EXTRACTED MODEL. Trusted: the Aeneas/Charon translation's faithfulness to the Rust semantics, the Lean 4 kernel, the axiomatized crypto specifications, rustc at the pinned toolchain, and the machine that runs it all. Kani's harnesses cross-check T-PARSE clause 1 against the untranslated Rust to shrink the translation's share of that trust. Reproducible builds of the seed binary (spec Assumptions) are the remaining bridge from "the audited source" to "the bytes on disk", and ride the release-process feature.