diff --git a/AGENTS.md b/AGENTS.md index 45a1d68..6e7d7e2 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -6,6 +6,8 @@ Guidance for future Codex runs in this repository: - Do not regenerate Lean from Rust. Treat shipped Lean files in verified repos as the artifact. - Do not claim end-to-end verification unless theorem coverage actually exists. - Keep macOS and Apple Silicon portability. Do not rely on GNU `timeout`, `free`, `taskset`, Docker, Nix, or x86_64 assumptions. +- The same portability law applies to DOCUMENTATION: commands printed in docs, the cockpit, and the lab manual must run on macOS (BSD userland: `shasum -a 256` not `sha256sum`; no GNU `sed -i` form; prefer portable `python3 -c` one-liners), and every printed command must be executed once before it ships. +- The cockpit's three laws are load-bearing: renders-evidence-never-asserts (provenance lines, loud FAILED TO VERIFY), never-leave-a-human-in-the-dark (verdict in words, explainers, glossary links), and distinct-roles-with-handoffs (stations never melt). All three are test-enforced; keep them so. - Prefer explicit theorem-boundary language over marketing language. - Update tests with every behavior change. - Do not silently lower risk ratings. A lower score must explain the failed or missing evidence. diff --git a/README.md b/README.md index 9df2b9b..212531e 100644 --- a/README.md +++ b/README.md @@ -24,10 +24,38 @@ agent-native first (an MCP server; a self-proving custody card); see [docs/products.md](docs/products.md), and the design research in [docs/agent-native.md](docs/agent-native.md). +For humans, warden ships the **custody cockpit** — a local, read-only web +UI organized as a bridge of six role stations (proposer, quorum bench, +operator, cryptographer, architect, newcomer) over shared evidence +instruments, with a tmux-style deck showing every station live in +parallel and a color-guided wizard. It explains itself; no prior warden +knowledge is assumed. One command, no wallet needed: + +```bash +pacta wallet cockpit --demo # → http://127.0.0.1:8471/deck +``` + +The full course lives beside it: [docs/warden-lab-manual.md](docs/warden-lab-manual.md) +(served at `/manual`) — a study-club lab that teaches every role hands-on. +Docs: [docs/cockpit.md](docs/cockpit.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. +One system prerequisite for the wallet features (key generation and +signing, including `cockpit --demo`): an `openssl` on PATH that supports +Ed25519. Stock macOS ships LibreSSL as `/usr/bin/openssl`, and older +LibreSSL versions lack the Ed25519 key commands — self-check with: + +```bash +openssl genpkey -algorithm ed25519 | head -1 # must print a PEM header, not an error +``` + +If it errors, `brew install openssl@3` and put it first on PATH (e.g. +`export PATH="$(brew --prefix openssl@3)/bin:$PATH"`). `git` on PATH is +needed only for the cockpit's liveness board repo probes. + Lean tooling is detected with `shutil.which("lean")` and `shutil.which("lake")`. If neither is available, `pacta` reports clear diagnostics and still supports offline claim-card generation and static hygiene scans. ## Tests @@ -39,18 +67,38 @@ python3 scripts/mini_pytest.py # dependency-free fallback runner (same suite) ## Install +Runtime dependencies: **none** — the tool is Python 3.11+ standard +library. The supported install is an **editable install from a clone**: +the repo's own files (estate map, lab manual, sample evidence) are part +of the product and are resolved relative to the checkout. + ```bash +git clone && cd proof-aware-crypto-tooling-agent python3 -m venv .venv . .venv/bin/activate python -m pip install -e ".[dev]" +pacta wallet cockpit --demo # smoke-test the human surface ``` +Zero-install alternative (no venv, no pip, straight from the clone): + +```bash +python3 scripts/mini_pytest.py # dependency-free suite +PYTHONPATH=src python3 -m pacta wallet cockpit --demo +``` + +On a fresh machine with no Lean toolchain and no locally built dogfood +binary, the suite passes with a handful of clearly labeled skips — +capability gaps skip, they never fail silently. + PyYAML is optional. Without it, `pacta` can still read the included simple YAML examples and JSON-compatible `.yaml` files. ## Commands ```bash python -m pacta --help +pacta wallet cockpit --demo # the human surface: bridge, deck, lab manual +pacta wallet status --wallet DIR # custody posture from the CLI pacta scan --config examples/repos.yaml pacta doctor --config examples/repos.yaml --repo-name dalek-ed25519-verified pacta claims --config examples/repos.yaml --repo-name dalek-ed25519-verified --offline-fixture --out claims.yaml diff --git a/docs/cockpit.md b/docs/cockpit.md index 1fb8cde..91dd745 100644 --- a/docs/cockpit.md +++ b/docs/cockpit.md @@ -159,8 +159,9 @@ pacta wallet cockpit --wallet ~/my-wallet # 127.0.0.1:8471 pacta wallet cockpit --wallet ~/my-wallet --port 9000 ``` -(Uninstalled, from the repo root: -`PYTHONPATH=src:provider/src python3 -m pacta wallet cockpit --demo`.) +(Installed per the README — venv + `pip install -e .` — the plain `pacta` +command works. Zero-install, from the repo root: +`PYTHONPATH=src python3 -m pacta wallet cockpit --demo`.) The server binds localhost by default and is not meant to be exposed; there is no authentication because there is nothing to operate. diff --git a/docs/products.md b/docs/products.md index 37939bb..1bc2fd8 100644 --- a/docs/products.md +++ b/docs/products.md @@ -6,6 +6,11 @@ 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. +Every profile also ships the same human surface: the **custody cockpit** +(`pacta wallet cockpit`) — local, read-only, six role stations over live +evidence instruments, with the deck, the guide, and the lab manual. See +[docs/cockpit.md](cockpit.md). + 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*. diff --git a/docs/threat-model.md b/docs/threat-model.md index 631a15c..cff5029 100644 --- a/docs/threat-model.md +++ b/docs/threat-model.md @@ -33,6 +33,27 @@ lying (firewall); an attacker who fully owns the host owns the wallet.** - **Deliberately absent**: reproducible builds, side-channel hardening (R5 frontier); ML-DSA (fail-closed — no proven implementation exists). +## The cockpit surface (attack surface note) + +The custody cockpit (`pacta wallet cockpit`) adds a localhost-bound, +read-only HTTP surface. Its threat posture, stated plainly: + +- **No mutating routes exist.** It cannot approve, sign, unlatch, or edit + custody state; the test suite asserts byte-level wallet-directory + identity across a full request sweep including POST. Custody-mutating + acts are only ever printed as CLI commands for the human. +- **No authentication because there is nothing to operate** — but it binds + `127.0.0.1` by default and must not be exposed: it *reads* wallet state, + so exposure is an information-disclosure risk (posture, incidents, + member fingerprints), not a custody-control risk. +- **It phones home never by default.** Outbound traffic happens only when + the operator explicitly presses «Probe now» (liveness GETs) — page loads + perform no network I/O. +- An attacker who can serve the operator a *fake* cockpit (host compromise, + attacker #7) can lie to the human — which is the standing host-compromise + boundary above, not a new one; the CLI (`pacta wallet status`, + `verify-ledger`) remains the independent second surface. + ## Design invariants the controls enforce 1. **Unanimity or nothing**: no majority voting; any divergence fails diff --git a/docs/warden-lab-manual.md b/docs/warden-lab-manual.md index 203b057..31b951f 100644 --- a/docs/warden-lab-manual.md +++ b/docs/warden-lab-manual.md @@ -27,10 +27,14 @@ exercises, open a *second* terminal in the same repo directory and set up two things once (the server keeps running in the first terminal): ``` -alias pacta='PYTHONPATH=src:provider/src python3 -m pacta' +alias pacta='PYTHONPATH=src python3 -m pacta' export W=/tmp/warden-DEMO-xxxxxxxx/wallet # <- your printed demo path ``` +(If you installed per the README — venv plus `pip install -e .` — skip the +alias: plain `pacta` already works. The alias is the zero-install path +straight from a clone; both are equivalent for this course.) + **Time.** The course is eight sessions plus a capstone: roughly four to six hours total. Every session is self-contained — stopping after any session and resuming tomorrow is fine. The demo wallet is throwaway: if you come back @@ -267,7 +271,7 @@ chair with hard walls — and in exchange, the Proposer gets something rare: ``` printf 'pay 5 to bob' > /tmp/payload.demo -sha256sum /tmp/payload.demo +shasum -a 256 /tmp/payload.demo # GNU/Linux equivalent: sha256sum ``` Change one character (`5` → `6`) and hash again. ✎ How much of the @@ -487,7 +491,8 @@ pacta wallet verify-ledger --wallet "$W" ``` cp -r "$W" /tmp/tamper-lab-wallet -sed -i 's/genesis/gene-sis/' /tmp/tamper-lab-wallet/ledger.jsonl +python3 -c "p='/tmp/tamper-lab-wallet/ledger.jsonl'; s=open(p).read(); \ +open(p,'w').write(s.replace('genesis','gene-sis'))" pacta wallet verify-ledger --wallet /tmp/tamper-lab-wallet ``` @@ -889,7 +894,7 @@ wallet state — real operations, operator's deliberate acts).* | any | `pacta wallet cockpit --demo` | seal + serve a throwaway demo wallet | | any | `pacta wallet cockpit --wallet DIR` | serve the cockpit over a wallet | | any | `pacta wallet status --wallet DIR` | custody posture (capsule, latch, ledger) | -| Proposer | `sha256sum payload.bin` | the payload fingerprint, born | +| Proposer | `shasum -a 256 payload.bin` | the payload fingerprint, born | | Proposer | `pacta wallet mcp --wallet DIR` | the front door (then `request_signature`) | | Proposer | `pacta wallet treasury-verify --wallet DIR --tx-file f` | quorum-verify a transaction's signatures | | Quorum | `pacta wallet build-quorum --sources-root DIR` | rebuild members from pinned proven sources | diff --git a/tests/test_wallet.py b/tests/test_wallet.py index d31fd5f..0d86a54 100644 --- a/tests/test_wallet.py +++ b/tests/test_wallet.py @@ -79,6 +79,10 @@ def _payload_intent(payload: bytes) -> dict: def test_ledger_is_hash_chained(tmp_path): + from pacta.dogfood import locate_verifier + + if locate_verifier() is None: + pytest.skip("dogfood signer not built") wallet = _seal_wallet(tmp_path, {"a": "accept", "b": "accept"}, tmp_path / "state") payload = b"hello" wallet.request_signature(_payload_intent(payload), payload, state_dir=wallet._test_state_dir)