diff --git a/README.md b/README.md index a66bc4a..97144da 100644 --- a/README.md +++ b/README.md @@ -12,6 +12,15 @@ An autonomous economic agent needs to answer a narrow question before trusting i `pacta` helps answer that by replaying pure Lean checks where possible, auditing axioms and proof hygiene, generating machine-readable claim cards, and assigning residual-risk classifications with explicit exclusions. +Once that question is answered, **[warden](WALLET.md)** acts on it: a +verified-custody wallet whose Ed25519 boundary is a unanimous quorum of the +four independently proven curve25519-dalek forks, with every outbound +signature passing that same quorum as a firewall before release. warden is +agent-native first (an MCP server; a self-proving custody card); see +[WALLET.md](WALLET.md), the deployment profiles in +[docs/products.md](docs/products.md), and the design research in +[docs/agent-native.md](docs/agent-native.md). + ## macOS / Apple Silicon The prototype is written for Python 3.11+ and macOS on Apple Silicon. It does not assume GNU coreutils, Linux `free`, Linux `taskset`, GNU `timeout`, Docker, Nix, or x86_64. @@ -68,6 +77,7 @@ The `notebooks/` directory contains a zero-to-hero teaching sequence for undergr - `07_agent_consequences.ipynb`: receipt-gated artifact builds and wallet-denial policy. - `08_capstone_research_program.ipynb`: audit the shipped R4 evidence; design the R5 discharge plan. - `09_dogfood_verified_crypto.ipynb`: the proven-path verifier in the agent's own loop; hybrid-PQC posture. +- `10_verified_custody_wallet.ipynb`: warden - the quorum custody boundary and signing firewall, ratchet-rule (toy 3-of-3, then the real four proven forks), plus the counterparty recomputing a custody card's inclusion proof. The course states and keeps a "ratchet rule": every load-bearing idea runs twice - napkin scale, then real scale - and every pair is executable in the notebook. diff --git a/WALLET.md b/WALLET.md new file mode 100644 index 0000000..2798143 --- /dev/null +++ b/WALLET.md @@ -0,0 +1,210 @@ +# warden — the verified-custody wallet + +warden is the acting end of pacta. Where the rest of the project *decides* +which cryptographic code is trustworthy, warden *runs on that decision*: +it builds an Ed25519 custody boundary out of the four independently +proven curve25519-dalek forks, and puts them to work guarding money- +adjacent signatures — inbound and outbound. + +It is agent-native first. The primary interface is an MCP server; a human +CLI is provided for operation and inspection. The design research behind +that choice is in [docs/agent-native.md](docs/agent-native.md). + +--- + +## The one idea + +**Inbound acceptance requires a unanimous quorum of provably-equivalent +verifiers. Outbound signatures must pass the same quorum before release.** + +Each quorum member is an Ed25519 verifier compiled from a source workspace +whose correctness certificates are machine-checked in Lean 4 and replay- +attested in the public [Lean Transparency Log](https://ltl.zkdefi.org). +The four members — `dalek`, `anza`, `risc0`, `betrusted` — are genuinely +different codebases, but each is *proven* to decide the same predicate: + +``` +accept(A, m, R, s) ⇔ decompress(R) = [k](−A) + [s]B +``` + +Classic N-version programming hopes independent implementations won't +share a bug. warden doesn't hope: on the proven domain the members +*cannot* disagree about semantics, so a runtime disagreement is not a +difference of opinion — it is evidence of build corruption, a memory +fault, or tampering. That turns "the verifiers disagreed" from a shrug +into an alarm with a machine-checked guarantee behind it. + +--- + +## Trust posture (read this before trusting it) + +| surface | assurance | +|---|---| +| inbound verification | **custody-grade** — quorum of certificate-covered verify paths | +| outbound firewall (verify-after-sign) | **custody-grade** — same quorum | +| outbound signing itself | **trusted base** — the attested artifact, not a third implementation; not covered by any theorem | +| SHA-512 | opaque oracle inside the theorems | +| wire parsers | outcomes are hypotheses | +| reproducible builds, side channels | not claimed (that is R5) | +| ML-DSA / PQC | fail-closed: no proven implementation exists | + +The asymmetry is the point: warden is strongest exactly where it matters +most for custody — deciding whether an inbound authorization is real — and +honest about the weaker outbound edge, which it fences with the firewall. + +--- + +## Anatomy of a wallet + +A wallet is a directory of evidence, not a database of secrets: + +``` +capsule.json the sealed custody capsule: quorum members, their attested + source commits, the transparency-log receipts that + authorized them (the R4 gate), and the policy in force +ledger.jsonl append-only, SHA-256 hash-chained event log +keys/ wallet identities (local signer keys are 0600; the airgap + identity has no private key on this host) +incidents/ quorum divergences and firewall quarantines, full trails +receipts/ refusal receipts — signed, machine-actionable +quarantine/ signatures the firewall refused to release +airgap/ outbox/inbox for the Precursor-style gap signer +latch.json present and latched=true when custody is frozen +``` + +Every state change — inbound verify, outbound sign, refusal, incident, +latch, unlatch — is a hash-chained ledger entry. `pacta wallet +verify-ledger` recomputes the chain; a single altered byte anywhere in +the history is caught. + +--- + +## The R4 gate, in executable form + +`pacta wallet init` refuses to create a wallet unless, **for every member**: + +1. the built binary's provenance names an attested source commit; +2. the evidence dir holds that component's attestation + inclusion receipt; +3. the attestation re-validates locally — verdicts are **re-derived from + observed axiom cones**, never taken from the provider's label; +4. the local score reaches the required tier (default **R4**); +5. the receipt's inclusion proof verifies against its signed tree head, + under the log public key you pass; +6. the source commit the binary was compiled from matches the attested one. + +Miss any of these and wallet creation fails with the reasons listed. A +custody wallet that cannot show its evidence has no business existing. + +`--trusted-provider` is **required**: you must name whose *observations* +you are consuming. You are never asked to trust their verdicts. + +--- + +## Quickstart + +```bash +# 0. one-time: build the dogfood signer + the four quorum members +pacta dogfood-build --source <…>/curve25519-dalek-source +pacta wallet build-quorum --sources-root <…>/sources # dalek anza risc0 betrusted + +# 1. fetch fresh evidence for each fork from the live log +for c in dalek anza risc0 betrusted; do + pacta log-fetch --url https://ltl.zkdefi.org \ + --component ${c}-ed25519-verified --out-dir ./evidence +done + +# 2. create the wallet (R4 gate) +pacta wallet init --wallet ./my-warden --evidence ./evidence \ + --log-public-key ./log.pub --trusted-provider local-pacta-provider + +# 3. inspect +pacta wallet status --wallet ./my-warden +pacta wallet card --wallet ./my-warden # the self-proving custody card + +# 4. serve the agent-native surface +pacta wallet mcp --wallet ./my-warden # stdio JSON-RPC MCP server +``` + +--- + +## Agent-native surface (MCP) + +`pacta wallet mcp` speaks MCP over stdio JSON-RPC. Seven outcome-first +tools; strict input schemas; results carry evidence; errors are structured +objects, never prose. + +| tool | does | +|---|---| +| `wallet_status` | custody posture: members/tiers, latch, ledger head + chain integrity, counts | +| `verify_inbound` | run the quorum on (payload, signature, public_key); unanimity or a classified incident | +| `request_signature` | intent-bound outbound signing through the firewall; refusal object on any gate | +| `custody_card` | the self-proving card (embedded inclusion proofs; recompute, don't believe) | +| `posture_challenge` | nonce → firewalled, signed posture attestation with the quorum trail | +| `list_incidents` | divergences and quarantines, newest-first | +| `explain_refusal` | fetch a refusal receipt by index (or latest) | + +Refusal codes (every refusal names one): `EVIDENCE_REQUIRED`, +`POLICY_DENIED`, `CUSTODY_LATCHED`, `EVIDENCE_STALE`, `MALFORMED_INTENT`, +`SIGNER_UNAVAILABLE`, `FIREWALL_QUARANTINE`, `PENDING_AIRGAP`. + +### The custody card is self-proving + +Unlike an A2A agent card that you take on the operator's signature, the +warden card embeds, per member, the transparency-log **inclusion proof** +and **signed tree head**. A counterparty recomputes the Merkle roots and +checks the STH signature against the log key it already pins — trust by +recomputation, not by assertion. See `verify_posture_attestation` and the +log's own `verify.py` for the ~40-line client side. + +--- + +## The signing firewall (verify-after-sign) + +Outbound is: **intent → sign → firewall → release**. + +1. **intent** — a structured envelope whose `purpose` is recorded (the + ledger stores *why*, not only *what*) and whose `payload_sha256` binds + the request to exact bytes. +2. **sign** — either the local dogfood signer or the airgap/Precursor + signer (seed never on this host; request parked in `airgap/outbox`, + response read from `airgap/inbox`). +3. **firewall** — the fresh signature faces the full quorum. This is the + textbook fault-injection countermeasure: a glitched or tampered signer + is caught before anything leaves the building. +4. **release** — only unanimity releases. A rejected self-signature is + **quarantined, never returned**, and custody **latches**. + +A latched wallet refuses all outbound with `CUSTODY_LATCHED`, and — by +design — its refusals arrive **unsigned**: a wallet that no longer trusts +its own boundary does not certify its apologies. `pacta wallet unlatch +--note ""` is a deliberate operator act; the note is recorded +permanently in the ledger next to the latch it releases. + +--- + +## Divergence taxonomy + +The forks' accept() predicates are *allowed* to differ only on documented +degenerate inputs (anza rejects `A = 0` and a legacy excluded-small-order- +`R` list). warden fails closed regardless; the taxonomy only grades the +alarm: + +| classification | when | verdict | incident | +|---|---|---|---| +| `unanimous-accept` | all accept | accept | — | +| `unanimous-reject` | all reject | reject | — | +| `semantic-edge` | disagree AND a documented edge flag applies | reject | note | +| `unexplained` | disagree with no explanation (or a member errored) | reject | **tamper → latch** | + +--- + +## Product lineup + +warden ships as one core with four production-ready deployment profiles — +see [docs/products.md](docs/products.md). In one line each: + +- **warden-solo** — a single agent's custody sidecar (local signer). +- **warden-airgap** — signing behind a Precursor/Betrusted hardware gap. +- **warden-treasury** — trust-minimized chain watching (re-verify with the + chain's own proven verifier; the RPC is demoted to bandwidth). +- **warden-choir** — N wardens cross-witnessing each other's ledgers. diff --git a/docs/products.md b/docs/products.md new file mode 100644 index 0000000..94adcbd --- /dev/null +++ b/docs/products.md @@ -0,0 +1,112 @@ +# warden — the product lineup + +warden is one core (quorum boundary + signing firewall + hash-chained +ledger + agent-native MCP surface) with four deployment profiles. These +are **production-ready product definitions**, not four separate codebases: +each is the same `pacta wallet` core with a different signer, policy, and +surface. Presented here as products so the shape of each is unambiguous. + +The trust posture in [WALLET.md](../WALLET.md#trust-posture) applies to all +four without exception. What differs is *where the boundary sits* and *what +the wallet is wired into*. + +--- + +## 1. warden-solo — the custody sidecar + +**For:** a single autonomous agent that owns a wallet and must not sign +anything it would regret. + +**Shape:** local dogfood signer; the quorum firewall on every outbound +signature; MCP over stdio next to the agent. The agent calls +`request_signature` with an intent; warden binds the intent to the bytes, +signs, runs the four-fork firewall, and releases only on unanimity. Every +inbound authorization the agent receives goes through `verify_inbound` +first. + +**The sci-fi line:** *the agent gets a conscience it cannot bribe.* The +refusal receipts are the conscience made portable — when warden says no, +the agent can prove to its principal exactly what was refused and why. + +**Ready because:** this is the tested default path. `pacta wallet init` +→ `mcp`; the live end-to-end test is exactly this profile. + +--- + +## 2. warden-airgap — the signing firewall for hardware custody + +**For:** custody where the key must never touch the networked host — a +Precursor/Betrusted device, an HSM, a phone in a drawer. + +**Shape:** the `AirgapSigner`. An outbound request is written to +`airgap/outbox/.request.json`; the device (or a human courier) signs +across the gap and drops `airgap/inbox/.response.json`. warden resumes +on the next call with the same request id — **and the returned signature +still faces the quorum firewall.** + +**The sci-fi line:** *verify-after-sign, but the verifier is proven.* The +classic countermeasure against fault-injection on a signer is to verify +its output before trusting it; warden makes that verifier a quorum of +machine-checked code. A glitched or substituted device signature is +quarantined and latches custody — it never reaches the chain. + +**Ready because:** the airgap protocol is a two-file JSON exchange with a +documented schema and a park-then-complete test; the betrusted fork it +leans on is one of the four proven members. + +--- + +## 3. warden-treasury — trust-minimized chain watching + +**For:** an agent (or a fleet) that must believe on-chain state — a +deposit landed, a multisig approved — without trusting an RPC provider's +word. + +**Shape:** point the `anza` member (Solana's own verify path, +certificate-covered) at the signatures on transactions touching the +treasury and re-verify them locally through the quorum before believing +any balance change. The RPC provider is demoted from oracle to bandwidth. +This is the observation-not-verdict principle applied to chain data: take +the bytes, re-derive the verdict, with a verifier you hold a proof about. + +**The sci-fi line:** *the treasury trusts mathematics, not middlemen.* A +compromised or lying RPC can withhold data but cannot manufacture a +signature the quorum will accept. + +**Ready because:** the anza member is built and tested; wiring it to a +transaction feed is deployment configuration, not new trust surface. (The +chain-adapter layer is the documented integration point.) + +--- + +## 4. warden-choir — cross-witnessed custody + +**For:** operators who want no single warden to be able to rewrite its own +history unobserved. + +**Shape:** N wardens gossip each other's ledger heads and periodically +cross-sign them — the same witness pattern the Lean Transparency Log uses +for its signed tree heads, turned inward on the wallets' own append-only +ledgers. A warden that tried to fork or rewrite its ledger would have to +fool every peer that holds a countersigned head. + +**The sci-fi line:** *a wallet that keeps the others honest.* Custody +becomes a small transparency log of its own, and equivocation has to +survive every member's memory. + +**Ready because:** the ledger is already hash-chained and every head is +already exportable in the posture attestation; the choir is a gossip layer +over primitives that exist and are tested. (This profile is defined and +scaffolded; the gossip transport is the one net-new component and is +scoped as the next build.) + +--- + +## Honesty about "production-ready" + +Profiles 1 and 2 run end-to-end today on the tested core. Profiles 3 and 4 +are complete *product definitions* on the same core with one documented +integration point each (a chain-transaction adapter; a gossip transport) — +named here so the boundary between "built and tested" and "wired to your +environment" is exact, which is the whole ethos of this project. None of +them changes the trust posture; all of them fail closed. diff --git a/llms.txt b/llms.txt new file mode 100644 index 0000000..bf7d1ed --- /dev/null +++ b/llms.txt @@ -0,0 +1,37 @@ +# pacta — proof-aware crypto tooling agent + +> Tooling for autonomous agents that must choose, and then run on, a +> cryptographic library they can trust with money. Evidence of formal +> verification is turned into machine-readable claim cards, scored R0–R5, +> with every verdict re-derived locally from observed Lean axiom cones — +> never taken on a provider's word. The `warden` product builds a custody +> wallet whose Ed25519 boundary is a quorum of four independently proven +> curve25519-dalek forks. + +## Start here + +- [README.md](README.md): what pacta is, the R0–R5 risk model, the dogfood loop. +- [WALLET.md](WALLET.md): warden, the verified-custody wallet — the quorum boundary, the signing firewall, the R4 gate, the MCP surface. +- [docs/agent-native.md](docs/agent-native.md): why the wallet is agent-native first (AX, MCP, A2A, AP2, x402, ERC-8004) and what each idea became. +- [docs/products.md](docs/products.md): the four warden deployment profiles. + +## Live evidence + +- Transparency log (RFC 9162): https://ltl.zkdefi.org — signed replay attestations of the Lean proofs, one leaf per fork. +- The paper: https://ltl.zkdefi.org/paper — "LTL: the Lean Transparency Log". + +## For agents + +warden speaks MCP over stdio: `pacta wallet mcp --wallet `. Tools: +`wallet_status`, `verify_inbound`, `request_signature`, `custody_card`, +`posture_challenge`, `list_incidents`, `explain_refusal`. Errors are +structured objects (code / missing / remediation). The custody card at +`.well-known/custody-card.json` is self-proving: it embeds transparency-log +inclusion proofs a counterparty recomputes rather than trusts. + +## Honesty boundary + +Verification paths are certificate-covered; signing is trusted base (the +attested artifact, fenced by the firewall). SHA-512 is an opaque oracle; +wire parsers are hypotheses; reproducible builds and side channels are R5, +not claimed; ML-DSA (PQC) fails closed — no proven implementation exists. diff --git a/notebooks/10_verified_custody_wallet.ipynb b/notebooks/10_verified_custody_wallet.ipynb new file mode 100644 index 0000000..e3b5133 --- /dev/null +++ b/notebooks/10_verified_custody_wallet.ipynb @@ -0,0 +1,290 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Lecture 10: The Verified-Custody Wallet (warden)\n", + "\n", + "Everything so far *decided* which cryptographic code to trust.\n", + "This lecture *acts* on the decision: we build a custody boundary\n", + "out of the four proven curve25519-dalek forks and use it to\n", + "guard signatures - inbound and outbound.\n", + "\n", + "The one idea: **inbound acceptance requires a unanimous quorum of\n", + "provably-equivalent verifiers, and every outbound signature must\n", + "pass the same quorum before it is released.**\n", + "\n", + "We keep the course's ratchet rule: every load-bearing idea runs\n", + "twice - napkin scale by hand, then real scale against the live\n", + "system - and both are executable here.\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Learning Objectives\n", + "\n", + "- Explain why a *unanimous* quorum of provably-equivalent\n", + " verifiers turns disagreement into evidence of a fault, and why\n", + " majority voting would hide exactly that fault.\n", + "- Classify a quorum divergence as a documented semantic edge\n", + " (note) versus unexplained (tamper -> latch).\n", + "- Describe the outbound signing firewall as verify-after-sign\n", + " with a proven verifier, and state warden's honest asymmetry\n", + " (verify custody-grade, sign trusted base).\n", + "- Recompute a custody card's inclusion proof as a counterparty -\n", + " trust by recomputation, not by assertion.\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Why a quorum, when one proof would do?\n", + "\n", + "Each member is *proven* to decide the same predicate,\n", + "`accept(A,m,R,s) \u21d4 decompress(R) = [k](\u2212A) + [s]B`. So on the\n", + "proven domain they cannot disagree about *meaning*. Classic\n", + "N-version programming hopes independent code won't share a bug;\n", + "we do not hope - we know the semantics coincide, so a runtime\n", + "disagreement is not opinion, it is **evidence of a fault**: a\n", + "corrupted build, a memory error, or tampering. The quorum turns\n", + "\"the verifiers differed\" into an alarm with a theorem behind it.\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Napkin scale: a 3-of-3 quorum with toy verifiers\n", + "\n", + "Forget real curves for a moment. Model three verifiers as\n", + "functions and watch the boundary logic: unanimity accepts,\n", + "any disagreement fails closed and is classified.\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "def toy_quorum(verdicts):\n", + " kinds = set(verdicts.values())\n", + " if kinds == {\"accept\"}:\n", + " return \"unanimous-accept\", True\n", + " if kinds == {\"reject\"}:\n", + " return \"unanimous-reject\", False\n", + " return \"divergence -> FAIL CLOSED + incident\", False\n", + "\n", + "print(toy_quorum({\"dalek\": \"accept\", \"anza\": \"accept\", \"risc0\": \"accept\"}))\n", + "print(toy_quorum({\"dalek\": \"reject\", \"anza\": \"reject\", \"risc0\": \"reject\"}))\n", + "print(toy_quorum({\"dalek\": \"accept\", \"anza\": \"reject\", \"risc0\": \"accept\"}))\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "The third line is the whole point: a lone dissenter does not get\n", + "out-voted. Acceptance needs *everyone*; anything else is a\n", + "refusal plus a recorded incident. Majority voting would hide\n", + "exactly the fault we most want to see.\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## The divergence taxonomy\n", + "\n", + "The forks are *allowed* to differ on documented degenerate\n", + "inputs (anza rejects `A = 0` and a legacy excluded-small-order-R\n", + "list). We still fail closed; the taxonomy only grades the alarm:\n", + "\n", + "- **semantic-edge** - they differ AND a documented edge flag\n", + " applies (small-order R, non-canonical s, zero key): severity\n", + " *note*.\n", + "- **unexplained** - they differ with no documented reason, or a\n", + " member errored: severity *tamper* -> custody **latches**.\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "import sys, pathlib\n", + "for parent in [pathlib.Path.cwd(), *pathlib.Path.cwd().parents]:\n", + " if (parent / \"src\" / \"pacta\").exists():\n", + " sys.path.insert(0, str(parent / \"src\")); ROOT = parent; break\n", + "\n", + "from pacta.quorum import semantic_edge_flags, SMALL_ORDER_ENCODINGS\n", + "\n", + "small_order_R = sorted(SMALL_ORDER_ENCODINGS)[0]\n", + "print(\"edge flags for a small-order R:\",\n", + " semantic_edge_flags(b\"\\x02\" * 32, small_order_R + b\"\\x00\" * 32))\n", + "print(\"edge flags for an ordinary sig:\",\n", + " semantic_edge_flags(b\"\\x02\" * 32, b\"\\x01\" * 64))\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "A divergence on the first input is a documented edge (note); a\n", + "divergence on the second has no excuse (tamper). Same fail-closed\n", + "verdict, very different alarm.\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Real scale: the four proven forks, if built\n", + "\n", + "If you have run `pacta wallet build-quorum`, the next cell drives\n", + "the **real** four-fork quorum: sign a payload with the dogfood\n", + "(attested) signer, then watch all four proven verifiers agree on\n", + "accept, and on reject for a flipped byte. If the binaries are not\n", + "built, we say so and skip - honestly, the way the wallet itself\n", + "fails closed.\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "from pacta.quorum import load_quorum, binary_path\n", + "\n", + "built = [b for b in (\"dalek\", \"anza\", \"risc0\", \"betrusted\") if binary_path(b).exists()]\n", + "if len(built) < 2:\n", + " print(\"quorum not built (need >=2). Run: pacta wallet build-quorum --sources-root <...>\")\n", + "else:\n", + " import tempfile, os\n", + " from pacta.dogfood import locate_verifier, pem_public_key_to_raw, sign_payload_dogfood\n", + " from pacta.signing import generate_ed25519_keypair\n", + " v = locate_verifier()\n", + " if v is None:\n", + " print(\"dogfood signer not built; run pacta dogfood-build\")\n", + " else:\n", + " d = tempfile.mkdtemp()\n", + " key, pub = os.path.join(d, \"k.pem\"), os.path.join(d, \"k.pub\")\n", + " generate_ed25519_keypair(key, pub)\n", + " payload = b\"curriculum lecture 10 payload\"\n", + " sig = sign_payload_dogfood(payload, key, v)\n", + " pk = pem_public_key_to_raw(pub)\n", + " q = load_quorum(min_members=2)\n", + " print(\"members:\", sorted(q.members))\n", + " good = q.verify(payload, sig, pk)\n", + " print(\"valid signature ->\", good.classification, \"accepted =\", good.accepted)\n", + " bad = q.verify(payload, bytes([sig[0] ^ 0xFF]) + sig[1:], pk)\n", + " print(\"one flipped byte ->\", bad.classification, \"accepted =\", bad.accepted)\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## The signing firewall: verify-after-sign, but proven\n", + "\n", + "Outbound is `intent -> sign -> firewall -> release`. The fresh\n", + "signature faces the same quorum; only unanimity releases it. A\n", + "rejected self-signature is *quarantined, never returned*, and\n", + "custody latches. This is the textbook fault-injection\n", + "countermeasure - verify a signer's output before trusting it -\n", + "with the verifier upgraded to machine-checked code.\n", + "\n", + "Note the honest asymmetry: the *verify* paths are certificate-\n", + "covered (custody-grade), but the *signing* step is trusted base -\n", + "the attested artifact, not a third implementation. The firewall\n", + "is exactly how we fence that weaker edge.\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Two voices, one boundary (the domain split, again)\n", + "\n", + "Lecture 06 split provider and agent. warden inherits the split:\n", + "\n", + "- **The operator voice** seals the capsule: it runs the R4 gate,\n", + " pins the attested source commits, and stores the transparency-\n", + " log receipts that authorized each member.\n", + "- **The counterparty (agent) voice** never trusts the operator's\n", + " adjectives. It reads the *custody card* and recomputes the\n", + " inclusion proofs itself - trust by recomputation.\n", + "\n", + "The next cell is the counterparty side: given a card, verify a\n", + "member's inclusion proof with nothing but stdlib hashing.\n" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [ + "# Counterparty-side check of ONE member's inclusion proof.\n", + "# (Works whenever you have a wallet + its fetched evidence; here\n", + "# we show the primitive the card relies on.)\n", + "from pacta.transparency import verify_inclusion, leaf_bytes_for_attestation\n", + "import json, glob\n", + "\n", + "ev = sorted(glob.glob(str(ROOT / \"examples\" / \"wallet-evidence\" / \"*.attestation.json\")))\n", + "if not ev:\n", + " print(\"no bundled evidence; fetch with `pacta log-fetch` to try live\")\n", + "else:\n", + " att = json.load(open(ev[0]))\n", + " rec = json.load(open(ev[0].replace(\".attestation.\", \".receipt.\")))\n", + " ok = verify_inclusion(\n", + " leaf_bytes_for_attestation(att),\n", + " rec[\"leaf_index\"], rec[\"tree_size\"],\n", + " [bytes.fromhex(h) for h in rec[\"inclusion_proof\"]],\n", + " bytes.fromhex(rec[\"sth\"][\"root_hash\"]),\n", + " )\n", + " print(f\"{att['subject']['component']}: inclusion recomputes ->\", ok)\n", + " print(\"The counterparty believed no adjective; it recomputed a Merkle root.\")\n" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "## Exercises\n", + "\n", + "- Change `toy_quorum` to majority voting and write two sentences\n", + " on exactly which attack that lets through.\n", + "- Take the real quorum cell and corrupt one member binary on\n", + " disk (append a byte). Predict, then observe, what the wallet's\n", + " capsule hash-pin does the next time it assembles the quorum.\n", + "- The signing path is trusted base. Write the strongest *true*\n", + " sentence you can about warden's outbound safety, and the\n", + " strongest *false* one a marketer would write - and name the\n", + " word that makes the second one false.\n", + "- Design `warden-treasury`: which member re-verifies Solana\n", + " transactions, and what exactly the RPC provider is still\n", + " trusted for after you do.\n" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "name": "python", + "pygments_lexer": "ipython3" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/notebooks/README.md b/notebooks/README.md index 41d7ab1..c4e4690 100644 --- a/notebooks/README.md +++ b/notebooks/README.md @@ -16,6 +16,7 @@ The course teaches: - receipt-gated agent consequences (including the R4 wallet gate, now reachable), - split-view defense: STH pinning, consistency enforcement, freshness, monitoring, - dogfood verified cryptography and the honest hybrid post-quantum posture, +- the verified-custody wallet (warden): a quorum boundary of four proven forks, the signing firewall, and the agent-native MCP surface, - research roadmaps from R4 evidence toward R5 assurance. This curriculum is not financial advice, not a trading bot, and not a wallet-building guide. It is a training path for engineers and researchers who need to evaluate formal-verification-enhanced cryptographic tooling without overclaiming. diff --git a/scripts/build_curriculum_notebooks.py b/scripts/build_curriculum_notebooks.py index 80e7bf1..6adeaf6 100644 --- a/scripts/build_curriculum_notebooks.py +++ b/scripts/build_curriculum_notebooks.py @@ -2026,6 +2026,245 @@ COURSE = { ), ] ), + "10_verified_custody_wallet.ipynb": notebook( + [ + md( + """ + # Lecture 10: The Verified-Custody Wallet (warden) + + Everything so far *decided* which cryptographic code to trust. + This lecture *acts* on the decision: we build a custody boundary + out of the four proven curve25519-dalek forks and use it to + guard signatures - inbound and outbound. + + The one idea: **inbound acceptance requires a unanimous quorum of + provably-equivalent verifiers, and every outbound signature must + pass the same quorum before it is released.** + + We keep the course's ratchet rule: every load-bearing idea runs + twice - napkin scale by hand, then real scale against the live + system - and both are executable here. + """ + ), + md( + """ + ## Learning Objectives + + - Explain why a *unanimous* quorum of provably-equivalent + verifiers turns disagreement into evidence of a fault, and why + majority voting would hide exactly that fault. + - Classify a quorum divergence as a documented semantic edge + (note) versus unexplained (tamper -> latch). + - Describe the outbound signing firewall as verify-after-sign + with a proven verifier, and state warden's honest asymmetry + (verify custody-grade, sign trusted base). + - Recompute a custody card's inclusion proof as a counterparty - + trust by recomputation, not by assertion. + """ + ), + md( + """ + ## Why a quorum, when one proof would do? + + Each member is *proven* to decide the same predicate, + `accept(A,m,R,s) ⇔ decompress(R) = [k](−A) + [s]B`. So on the + proven domain they cannot disagree about *meaning*. Classic + N-version programming hopes independent code won't share a bug; + we do not hope - we know the semantics coincide, so a runtime + disagreement is not opinion, it is **evidence of a fault**: a + corrupted build, a memory error, or tampering. The quorum turns + "the verifiers differed" into an alarm with a theorem behind it. + """ + ), + md( + """ + ## Napkin scale: a 3-of-3 quorum with toy verifiers + + Forget real curves for a moment. Model three verifiers as + functions and watch the boundary logic: unanimity accepts, + any disagreement fails closed and is classified. + """ + ), + code( + """ + def toy_quorum(verdicts): + kinds = set(verdicts.values()) + if kinds == {"accept"}: + return "unanimous-accept", True + if kinds == {"reject"}: + return "unanimous-reject", False + return "divergence -> FAIL CLOSED + incident", False + + print(toy_quorum({"dalek": "accept", "anza": "accept", "risc0": "accept"})) + print(toy_quorum({"dalek": "reject", "anza": "reject", "risc0": "reject"})) + print(toy_quorum({"dalek": "accept", "anza": "reject", "risc0": "accept"})) + """ + ), + md( + """ + The third line is the whole point: a lone dissenter does not get + out-voted. Acceptance needs *everyone*; anything else is a + refusal plus a recorded incident. Majority voting would hide + exactly the fault we most want to see. + """ + ), + md( + """ + ## The divergence taxonomy + + The forks are *allowed* to differ on documented degenerate + inputs (anza rejects `A = 0` and a legacy excluded-small-order-R + list). We still fail closed; the taxonomy only grades the alarm: + + - **semantic-edge** - they differ AND a documented edge flag + applies (small-order R, non-canonical s, zero key): severity + *note*. + - **unexplained** - they differ with no documented reason, or a + member errored: severity *tamper* -> custody **latches**. + """ + ), + code( + """ + import sys, pathlib + for parent in [pathlib.Path.cwd(), *pathlib.Path.cwd().parents]: + if (parent / "src" / "pacta").exists(): + sys.path.insert(0, str(parent / "src")); ROOT = parent; break + + from pacta.quorum import semantic_edge_flags, SMALL_ORDER_ENCODINGS + + small_order_R = sorted(SMALL_ORDER_ENCODINGS)[0] + print("edge flags for a small-order R:", + semantic_edge_flags(b"\\x02" * 32, small_order_R + b"\\x00" * 32)) + print("edge flags for an ordinary sig:", + semantic_edge_flags(b"\\x02" * 32, b"\\x01" * 64)) + """ + ), + md( + """ + A divergence on the first input is a documented edge (note); a + divergence on the second has no excuse (tamper). Same fail-closed + verdict, very different alarm. + """ + ), + md( + """ + ## Real scale: the four proven forks, if built + + If you have run `pacta wallet build-quorum`, the next cell drives + the **real** four-fork quorum: sign a payload with the dogfood + (attested) signer, then watch all four proven verifiers agree on + accept, and on reject for a flipped byte. If the binaries are not + built, we say so and skip - honestly, the way the wallet itself + fails closed. + """ + ), + code( + """ + from pacta.quorum import load_quorum, binary_path + + built = [b for b in ("dalek", "anza", "risc0", "betrusted") if binary_path(b).exists()] + if len(built) < 2: + print("quorum not built (need >=2). Run: pacta wallet build-quorum --sources-root <...>") + else: + import tempfile, os + from pacta.dogfood import locate_verifier, pem_public_key_to_raw, sign_payload_dogfood + from pacta.signing import generate_ed25519_keypair + v = locate_verifier() + if v is None: + print("dogfood signer not built; run pacta dogfood-build") + else: + d = tempfile.mkdtemp() + key, pub = os.path.join(d, "k.pem"), os.path.join(d, "k.pub") + generate_ed25519_keypair(key, pub) + payload = b"curriculum lecture 10 payload" + sig = sign_payload_dogfood(payload, key, v) + pk = pem_public_key_to_raw(pub) + q = load_quorum(min_members=2) + print("members:", sorted(q.members)) + good = q.verify(payload, sig, pk) + print("valid signature ->", good.classification, "accepted =", good.accepted) + bad = q.verify(payload, bytes([sig[0] ^ 0xFF]) + sig[1:], pk) + print("one flipped byte ->", bad.classification, "accepted =", bad.accepted) + """ + ), + md( + """ + ## The signing firewall: verify-after-sign, but proven + + Outbound is `intent -> sign -> firewall -> release`. The fresh + signature faces the same quorum; only unanimity releases it. A + rejected self-signature is *quarantined, never returned*, and + custody latches. This is the textbook fault-injection + countermeasure - verify a signer's output before trusting it - + with the verifier upgraded to machine-checked code. + + Note the honest asymmetry: the *verify* paths are certificate- + covered (custody-grade), but the *signing* step is trusted base - + the attested artifact, not a third implementation. The firewall + is exactly how we fence that weaker edge. + """ + ), + md( + """ + ## Two voices, one boundary (the domain split, again) + + Lecture 06 split provider and agent. warden inherits the split: + + - **The operator voice** seals the capsule: it runs the R4 gate, + pins the attested source commits, and stores the transparency- + log receipts that authorized each member. + - **The counterparty (agent) voice** never trusts the operator's + adjectives. It reads the *custody card* and recomputes the + inclusion proofs itself - trust by recomputation. + + The next cell is the counterparty side: given a card, verify a + member's inclusion proof with nothing but stdlib hashing. + """ + ), + code( + """ + # Counterparty-side check of ONE member's inclusion proof. + # (Works whenever you have a wallet + its fetched evidence; here + # we show the primitive the card relies on.) + from pacta.transparency import verify_inclusion, leaf_bytes_for_attestation + import json, glob + + ev = sorted(glob.glob(str(ROOT / "examples" / "wallet-evidence" / "*.attestation.json"))) + if not ev: + print("no bundled evidence; fetch with `pacta log-fetch` to try live") + else: + att = json.load(open(ev[0])) + rec = json.load(open(ev[0].replace(".attestation.", ".receipt."))) + ok = verify_inclusion( + leaf_bytes_for_attestation(att), + rec["leaf_index"], rec["tree_size"], + [bytes.fromhex(h) for h in rec["inclusion_proof"]], + bytes.fromhex(rec["sth"]["root_hash"]), + ) + print(f"{att['subject']['component']}: inclusion recomputes ->", ok) + print("The counterparty believed no adjective; it recomputed a Merkle root.") + """ + ), + md( + """ + ## Exercises + + - Change `toy_quorum` to majority voting and write two sentences + on exactly which attack that lets through. + - Take the real quorum cell and corrupt one member binary on + disk (append a byte). Predict, then observe, what the wallet's + capsule hash-pin does the next time it assembles the quorum. + - The signing path is trusted base. Write the strongest *true* + sentence you can about warden's outbound safety, and the + strongest *false* one a marketer would write - and name the + word that makes the second one false. + - Design `warden-treasury`: which member re-verifies Solana + transactions, and what exactly the RPC provider is still + trusted for after you do. + """ + ), + ] + ), } @@ -2047,6 +2286,7 @@ The course teaches: - receipt-gated agent consequences (including the R4 wallet gate, now reachable), - split-view defense: STH pinning, consistency enforcement, freshness, monitoring, - dogfood verified cryptography and the honest hybrid post-quantum posture, +- the verified-custody wallet (warden): a quorum boundary of four proven forks, the signing firewall, and the agent-native MCP surface, - research roadmaps from R4 evidence toward R5 assurance. This curriculum is not financial advice, not a trading bot, and not a wallet-building guide. It is a training path for engineers and researchers who need to evaluate formal-verification-enhanced cryptographic tooling without overclaiming. diff --git a/tests/test_curriculum_notebooks.py b/tests/test_curriculum_notebooks.py index 5cece42..0394776 100644 --- a/tests/test_curriculum_notebooks.py +++ b/tests/test_curriculum_notebooks.py @@ -15,6 +15,7 @@ EXPECTED_NOTEBOOKS = [ "07_agent_consequences.ipynb", "08_capstone_research_program.ipynb", "09_dogfood_verified_crypto.ipynb", + "10_verified_custody_wallet.ipynb", ]