The trust boundary

A guarantee you cannot delimit is a slogan. This page is the delimitation: what is proven, what is assumed, which running code the proofs depend on, and what remains your discipline as an operator or user. It embeds the machine-readable assurance catalog generated from the Lean assurance case, so the claims here cannot drift from the proofs.

What is proven

The assurance case is organized by guarantee, not by module: each guarantee names an apex theorem and the keystone DAG that discharges it, and every name is #assert_axioms-pinned — the Lean build fails unless the theorem's full axiom set is exactly the kernel triple.

A AUTHORITY

Every state change is justified by an unforgeable, non-amplified, fresh token chain.

apex: authority_guarantee · 19 axiom pins

floor: ed25519 (signature on the handoff), HMAC (caveat-chain tags), Poseidon2-CR (in-circuit cap-root openings). No trusted "this was authorized" premise survives.

B CONSERVATION

Per asset, the resource sum is IDENTICALLY ZERO — on every reachable state, always.

apex: conservation_guarantee · 23 axiom pins

floor: NONE beyond integer arithmetic. Conservation is a kernel theorem; the only crypto that touches it is Pedersen (DLog) IF values are committed rather than cleartext, and the case proves committed = cleartext via Spec.committed_iff_cleartext. DEPLOYMENT CORRESPONDENCE (named, not closed — the theorem's hypothesis vs the running node): reachable_total_zero quantifies over states reachable from a VALUE-EMPTY genesis (GenesisState: bal ≡ 0; live cells may pre-exist, value may not). Two deployed paths are TODAY outside that hypothesis, and this case does not claim them: 1. **Devnet genesis seeding** — node/src/genesis.rs mints the faucet (1,000,000) and demo agents (alice/bob/carol) with positive balances and NO issuer well carrying −supply, so the deployed genesis is not value-empty in the model's sense. The W1-faithful fix is to seed via issuer-moves from a genesis issuer cell (then genesis Σ=0 holds by construction). 2. **The legacy atomic-path fee epilogue** — turn/src/executor/atomic.rs (the fee deduct in execute_atomic) debits atomic_turn.fee from the agent with no crediting move: a burn OUTSIDE the issuer-move discipline (DREGG3 staged item: fees become moves to wells). Until both are reshaped, conservation_guarantee is a theorem about the kernel the node RUNS (execFullTurnA — every committed transaction preserves Σ exactly) but the deployed CHAIN's Σ is offset by its genesis seed and decremented by legacy fees. Reported here so the spec SAYS what it covers; the closure lane is the genesis/fee reshape, not a caveat to carry.

C INTEGRITY

A receipt binds the WHOLE post-state; a tampered input is rejected.

apex: integrity_guarantee · 24 axiom pins

floor: Poseidon2-permutation-CR (the recStateCommit/cellCommit/stateCommit injectivity portals reduce to it; the MMR discharge rests on the SAME Poseidon2SpongeCR). A second pre-image would be the only way to forge a receipt for a different state; that is exactly the CR assumption.

D FRESHNESS

No replay / double-spend; a committed spend's nullifier was fresh; revocation at finality.

apex: freshness_guarantee · 12 axiom pins

floor: Poseidon2-CR (the nullifier-set sorted-tree root openings). PostGSTProgress for the revocation-at-finality leg (consensus terminates after GST). KNOWN RESIDUAL (named, out-of-model): the node's MCP gateway binds biscuit-cap temporal caveats to the live attested consensus height (node/src/mcp.rs McpCapContext.block_height) — the height-expiry leg is real — but consults NO revocation registry for MCP-issued biscuit caps (the gateway's own doc names this). An MCP cap dies only by expiry caveat, never by explicit revocation, until a revocation feed is wired. That path is OUTSIDE this guarantee's statement; it is listed here so the case says so rather than implying coverage.

E UNFOOLABILITY

A light client verifying a Q-chain learns A–D for the WHOLE history; re-witnessing nothing.

apex: unfoolability_guarantee · 22 axiom pins

floor: FRI / STARK soundness (EngineSound.recursive_sound, the ONE recursion obligation), Poseidon2-CR (recStateCommit binds the seam roots), ed25519 (strand-block signatures), PostGSTProgress (a FINALIZED — not merely valid — chain, via the finality-cert leg).

R THE RUNNING ENTRY (A∧B∧C hold over what the node actually runs)

The five guarantees above are stated over the abstract kernel: the List Auth attenuation lattice (A), the multi-asset ledger recTransferBal (B), the Argus term IR (C/D), the aggregation fold (E). The honest question ember keeps pressing is: *do those guarantees hold over the executor the deployed node INVOKES* — execFullForestG, the body behind the dregg_exec_full_forest_auth FFI export (Exec.FFI), the one produce_via_lean / lean_shadow call? They do, and this section proves it in ONE statement rather than leaving it as a reader's inference.

apex: running_entry_sound · 8 axiom pins

floor: unchanged from A–C.

6 guarantees, 108 #assert_axioms pins, generated from Dregg2/AssuranceCase.lean. Every pinned theorem rests on the Lean kernel triple {propext, Classical.choice, Quot.sound} and nothing else.

Guarantee R deserves emphasis: it states A, B, and C over execFullForestG — the executor body the deployed node invokes through FFI — not over an abstract model. "The proofs are about the thing that runs" is itself a theorem (running_entry_sound), not a deployment note.

What is assumed

Every guarantee above is unconditional modulo these carriers, which enter as Prop-portals (hypotheses and typeclass fields), never as axioms:

Poseidon2-permutation collision-resistance — the arithmetization-friendly hash; the sponge/Merkle/state-commitment/MMR collision-resistance is reduced to permutation-CR (Crypto.Poseidon2*, Crypto.Merkle, the recStateCommit injectivity portal, the receipt-index Lightclient.MMR.mroot_binds_position, and the sorted-set/queue Apps.QueueRoot.RootCR/LenBindCR and identity-keyset Apps.PreRotation.KeySetCR carriers — every one a named CR Prop over a Poseidon2/BLAKE3 image, NOT an axiom).
BLAKE3 collision-resistance — the out-of-circuit content/transcript hash.
ed25519 EUF-CMA — turn / strand-block signature unforgeability.
HMAC (PRF/MAC) unforgeability — macaroon caveat-chain tags (Authority.CaveatChain).
AEAD confidentiality+integrity — sealed-value / disclosure payloads.
Discrete-log hardness — Pedersen value commitments (Crypto.Pedersen).
FRI / the STARK soundness chain — a verifying proof attests its statement; the one recursion obligation RecursiveAggregation.EngineSound.recursive_sound.
PostGSTProgress — the network is eventually synchronous (after GST); the consensus LIVENESS carrier (World.gst_liveness, derived from a DLS88/HotStuff Pacemaker).

The assumption floor (8 carriers), generated from Dregg2/AssuranceCase.lean. These enter as Prop-portals (typeclass fields / hypotheses), never as axioms; no other assumption is load-bearing anywhere in the case.

Which running code the proofs depend on

The verified semantics live in metatheory/Dregg2/ and execute through the dregg_exec_full_forest_auth FFI export. Around that core, a soundness claim additionally depends on the correctness of a specific, named set of Rust components (the survey is docs/DREGGRS-SEGREGATION.md):

the bridge — dregg-lean-ffi's marshalling between wire types and the Lean kernel's types;
the node's admission gates — the points where the node consults the verified verdict (production, finality, handoff, admission);
the verifiers — verifier and lightclient, the standalone and succinct proof checkers;
the canonical codecs — types, whose encodings define what is signed and committed;
the token cryptography — macaroon / token (HMAC caveat chains, biscuit verification) and commit / trace (token-proof Merkle and Datalog semantics);
consensus safety — blocklace, with finality gated on the verified rule.

Transport, storage, and networking (wire, net, persist) are deliberately outside the boundary: commitments catch tampering below them, so they need to be available, not correct.

What is operator and user discipline

Key custody. The SDK and cipherclerk are client-local: keys and witness data stay on your device, which means your device's security is yours. A compromised device holds your authority.
What programs cannot see. The constraint grammar has stated expressibility limits (quoted from source in the ontology catalog); rules outside them are SDK and operational discipline, and an app's documentation must say which of its rules are which.
Disclosure choices. The dial (rung 3) gives you projections of Q; choosing what to reveal to whom is a policy you set, not a property the system can choose for you.

Present limitations

Stated plainly, as facts about the present system:

The host-context seam. Some wire-effect families are executed by host Rust whose verdicts are cross-checked against the Lean kernel turn-by-turn rather than produced by it. For those families, that Rust is in the trust base; the node reports the exact split live at /api/node/producer.
Composition security is not machine-checked end-to-end. The per-guarantee theorems are; a universal-composability statement for the whole protocol stack is not yet a Lean artifact.
The circuit graduation and the rotation are in progress. The Lean-emitted descriptor prover is authoritative for a named set of graduated turn shapes; every other shape falls back — logged, never silent — to a hand-written AIR that enforces the same bindings but is test-attested, not theorem-attested. Graduating the remainder, and binding the cell heap's heap_root in-circuit per turn, ride the one VK/commitment epoch (the "rotation"); the heap is kernel-bound and scheme-pinned today, not yet per-turn circuit-committed.

Grounding

metatheory/Dregg2/AssuranceCase.lean — the assurance case this page embeds; Dregg2/Claims.lean is the corpus-wide per-keystone pin net behind it.
docs/DREGGRS-SEGREGATION.md — the crate-by-crate trust survey.
site/tools/gen-ontology-catalog.js — the generator whose drift check fails the site build if any embedded fact here goes stale.

Touch it: ask a live node for its producer split (curl localhost:8420/api/node/producer), and open any proof badge in the explorer — the tier it shows is computed from this same assurance catalog.

← 6 · Userspace · back to the ladder ↑