docs: coherence + portability audit — clean-clone bootstrap proven

Audit question: is the documentation coherent, and is the app portable
to a fresh machine (macOS) with proper isolation? Findings and fixes:

- README never mentioned the cockpit/deck/lab manual (three rounds of UI
  evolution invisible at the front door). Added: human-surface section
  with the one command, expanded Install (editable-from-clone is the
  supported mode — repo files are part of the product; zero-install
  PYTHONPATH=src alternative; fresh-machine skip behavior), macOS
  openssl/LibreSSL Ed25519 prerequisite with a one-line self-check,
  wallet commands in the command list.
- The lab manual violated the repo's own macOS law (AGENTS.md): GNU
  sha256sum -> shasum -a 256; GNU sed -i -> portable python3 -c
  one-liner (executed and output-matched before shipping: entry 0 hash
  mismatch, BROKEN, exit 1).
- Fresh-clone bootstrap was actually tested end to end in a scratch
  clone: zero-install suite 130 passed / 0 failed / 14 skipped after
  fixing the one unguarded test (test_ledger_is_hash_chained now skips
  like its siblings when the dogfood binary is absent - capability gap,
  not failure); venv + pip install -e . -> pacta console script serves
  bridge/deck/manual/sample-prefill/drift-tripwire with no PYTHONPATH.
- PYTHONPATH incantations simplified: cockpit needs src only (provider
  never imported by src/pacta); manual + cockpit.md updated.
- threat-model.md: cockpit attack-surface note (no mutating routes,
  no auth because nothing to operate, localhost-only disclosure risk,
  probe-only network I/O, fake-cockpit = host-compromise boundary).
- products.md: cockpit named as the shared human surface of all four
  profiles. AGENTS.md: doc-portability law + the cockpit's three laws
  added to the standing guidance.

Suite 144 green here; 130/0/14 on a bare clone.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-21 18:00:08 +02:00
parent 1d712a884a
commit 37429335e6
7 changed files with 92 additions and 6 deletions

View file

@ -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 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. - 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. - 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. - Prefer explicit theorem-boundary language over marketing language.
- Update tests with every behavior change. - Update tests with every behavior change.
- Do not silently lower risk ratings. A lower score must explain the failed or missing evidence. - Do not silently lower risk ratings. A lower score must explain the failed or missing evidence.

View file

@ -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/products.md](docs/products.md), and the design research in
[docs/agent-native.md](docs/agent-native.md). [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 ## 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. 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. 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 ## Tests
@ -39,18 +67,38 @@ python3 scripts/mini_pytest.py # dependency-free fallback runner (same suite)
## Install ## 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 ```bash
git clone <this repo> && cd proof-aware-crypto-tooling-agent
python3 -m venv .venv python3 -m venv .venv
. .venv/bin/activate . .venv/bin/activate
python -m pip install -e ".[dev]" 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. PyYAML is optional. Without it, `pacta` can still read the included simple YAML examples and JSON-compatible `.yaml` files.
## Commands ## Commands
```bash ```bash
python -m pacta --help 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 scan --config examples/repos.yaml
pacta doctor --config examples/repos.yaml --repo-name dalek-ed25519-verified 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 pacta claims --config examples/repos.yaml --repo-name dalek-ed25519-verified --offline-fixture --out claims.yaml

View file

@ -159,8 +159,9 @@ pacta wallet cockpit --wallet ~/my-wallet # 127.0.0.1:8471
pacta wallet cockpit --wallet ~/my-wallet --port 9000 pacta wallet cockpit --wallet ~/my-wallet --port 9000
``` ```
(Uninstalled, from the repo root: (Installed per the README — venv + `pip install -e .` — the plain `pacta`
`PYTHONPATH=src:provider/src python3 -m pacta wallet cockpit --demo`.) 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; The server binds localhost by default and is not meant to be exposed;
there is no authentication because there is nothing to operate. there is no authentication because there is nothing to operate.

View file

@ -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 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. 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 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 four without exception. What differs is *where the boundary sits* and *what
the wallet is wired into*. the wallet is wired into*.

View file

@ -33,6 +33,27 @@ lying (firewall); an attacker who fully owns the host owns the wallet.**
- **Deliberately absent**: reproducible builds, side-channel hardening - **Deliberately absent**: reproducible builds, side-channel hardening
(R5 frontier); ML-DSA (fail-closed — no proven implementation exists). (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 ## Design invariants the controls enforce
1. **Unanimity or nothing**: no majority voting; any divergence fails 1. **Unanimity or nothing**: no majority voting; any divergence fails

View file

@ -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): 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 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 **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 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 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 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 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 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 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 --demo` | seal + serve a throwaway demo wallet |
| any | `pacta wallet cockpit --wallet DIR` | serve the cockpit over a wallet | | any | `pacta wallet cockpit --wallet DIR` | serve the cockpit over a wallet |
| any | `pacta wallet status --wallet DIR` | custody posture (capsule, latch, ledger) | | 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 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 | | 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 | | Quorum | `pacta wallet build-quorum --sources-root DIR` | rebuild members from pinned proven sources |

View file

@ -79,6 +79,10 @@ def _payload_intent(payload: bytes) -> dict:
def test_ledger_is_hash_chained(tmp_path): 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") wallet = _seal_wallet(tmp_path, {"a": "accept", "b": "accept"}, tmp_path / "state")
payload = b"hello" payload = b"hello"
wallet.request_signature(_payload_intent(payload), payload, state_dir=wallet._test_state_dir) wallet.request_signature(_payload_intent(payload), payload, state_dir=wallet._test_state_dir)