saymrwulf/proof-aware-crypto-tooling-agent
1
0
Fork 0
mirror of https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git synced 2026-09-03 19:53:43 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

cockpit: the lab manual — a study-club course in six chairs (/manual)

Browse source 
Operator asked for a real big fat user manual: read on one monitor with
the deck on the other, worked like a lab from beginning to end, with
highest didactical skill — the goal being to educate ONE person in ALL
roles, as if to BECOME each role. Shipped as a full course:

- docs/warden-lab-manual.md (canonical, ~7100 words): 8 sessions +
  capstone. Fixed didactic ritual per role-session: why the role exists
  -> the mind of the role -> concepts -> LAB (numbered machine exercises
  with checkpoint rails) -> never-list with whys + thought experiment ->
  handoff artifact -> self-test -> recap card. Notation: do / checkpoint
  / write / optional. Capstone 'incident day': one incident walked
  through all six chairs producing seven written artifacts; graduation
  session maps the path to a real wallet; Appendix A command reference
  by chair, Appendix B full self-test answers.
- Session 4's tamper drill: copy the demo wallet, flip one character of
  ledger history, watch verify-ledger AND a second cockpit catch it.
  Every checkpoint in the manual was executed by the author before
  commit: status fields, intact-chain exit 0, tampered-chain 'entry 0:
  hash mismatch / BROKEN' exit 1, CUSTODY EVIDENCE BROKEN banner.
- src/pacta/mdlite.py: deliberately small stdlib Markdown renderer
  (headings/anchors+TOC, bold/italic/code with placeholder stashing,
  fences, lists, quotes, tables, links); tested against the real manual
  for zero artifact leaks.
- /manual route with syllabus TOC; manual typography (checkpoint boxes,
  session borders); nav tab, deck wizard cross-link, cli hint.

Suite 142 -> 144 green; read-only sweep covers /manual.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-21 17:26:09 +02:00
parent 15421ac4d0
commit 1d712a884a
8 changed files with 1265 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
docs/cockpit.md
View file

@ -143,7 +143,8 @@ separate, explicitly reviewed milestone.
| **Incidents** (`/incidents`) | *What has ever gone wrong?* Incident records and signed refusal receipts, verbatim, newest first — with the page explaining why empty is the good state | `incidents/*.json`, `receipts/*.json` | | **Incidents** (`/incidents`) | *What has ever gone wrong?* Incident records and signed refusal receipts, verbatim, newest first — with the page explaining why empty is the good state | `incidents/*.json`, `receipts/*.json` |
| **Inspect** (`/inspect`) | *Can I check a receipt myself?* Paste an attestation + transparency receipt + log public key; the verdict, per-signature results, and diagnostics come verbatim from the deployed verifier | `pacta.transparency.verify_receipt` | | **Inspect** (`/inspect`) | *Can I check a receipt myself?* Paste an attestation + transparency receipt + log public key; the verdict, per-signature results, and diagnostics come verbatim from the deployed verifier | `pacta.transparency.verify_receipt` |
| **Estate map** (`/estate`) | *Where does this wallet sit in the whole endeavour?* Every repo, service, mirror, loop — with RUNTIME on every entity (always-on / on-demand / not-running / static) | rendering of ESTATE.md's model (drift-guarded by test) | | **Estate map** (`/estate`) | *Where does this wallet sit in the whole endeavour?* Every repo, service, mirror, loop — with RUNTIME on every entity (always-on / on-demand / not-running / static) | rendering of ESTATE.md's model (drift-guarded by test) |
| **Guide** (`/guide`) | *What does any of this mean?* The manual: plain-language explanations, color code, tour, full glossary, honest limits — static, no live data | — | | **Guide** (`/guide`) | *What does any of this mean?* The reference: plain-language explanations, color code, tour, full glossary, honest limits — static, no live data | — |
| **Lab manual** (`/manual`) | *Teach me every role.* The full study-club course ([docs/warden-lab-manual.md](warden-lab-manual.md), canonical Markdown rendered live): eight sessions + capstone, one chair per role — labs with checkpoints, a safe tamper drill, self-tests with answers, graduation path to a real wallet. Built for two monitors: manual on one, deck on the other. | `mdlite` over the committed file |
Every panel also states what it does **not** prove (e.g. the quorum Every panel also states what it does **not** prove (e.g. the quorum
table says binary hashes are pinned but source-to-binary correspondence table says binary hashes are pinned but source-to-binary correspondence

992
docs/warden-lab-manual.md Normal file
View file

@ -0,0 +1,992 @@
# The warden lab manual — one person, six roles
*A study-club course in verified custody. You will not read about the roles —
you will sit in each chair, do each job with your own hands on a live (and
harmless) wallet, and only leave a chair when you can say what that role
does, why it exists, and what it must never do.*
---
## How to use this manual
**Two monitors.** Put this manual on one screen. On the other, start the
cockpit and keep it open for the whole course:
```
cd proof-aware-crypto-tooling-agent
PYTHONPATH=src:provider/src python3 -m pacta wallet cockpit --demo
```
The command prints two things you need:
1. the **demo wallet path** (something like `/tmp/warden-DEMO-xxxxxxxx/wallet`), and
2. the address `http://127.0.0.1:8471` with its `/deck` and `/guide` pointers.
Open **http://127.0.0.1:8471/deck** on the second monitor. For the terminal
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'
export W=/tmp/warden-DEMO-xxxxxxxx/wallet # <- your printed demo path
```
**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
later, just start `--demo` again and re-export `W`.
**Notation.** Four marks carry the whole manual:
- **▶ Do** — an action at the machine (deck pane, page, or terminal).
- **✔ Checkpoint** — what you must be seeing before you continue. If you do
not see it, stop and re-do the step; checkpoints are the course's rails.
- **✎ Write** — answer in your own words, on paper or in a scratch file.
Writing is not optional; it is how the role gets into your hands.
- **⌂ Optional** — needs internet, or goes beyond the demo. Skip freely.
**The two rules of the lab.**
1. Everything in the cockpit is **read-only** — you cannot break custody from
a browser, so click with total freedom.
2. When we *deliberately* break things (and we will — that is Session 4's
best moment), we break **copies**, never originals. The demo wallet is
custody-inert anyway; the discipline is the point.
> ✔ **Checkpoint.** Your second monitor shows the deck: six colored panes and
> the wizard rail. Your second terminal answers `pacta --help` without an
> error. If both are true, you are ready.
---
## Session 0 — the world you are entering
**Goal of this session:** hold the whole system in your head at low
resolution, so every later session has a place to hang its detail.
### 0.1 The one idea
warden is a prototype custody wallet built on a single idea: **no single
program is trusted.** Before this wallet trusts a piece of cryptography, four
verifier programs — each built from a *different*, formally verified codebase
— must independently agree. If they ever disagree, the wallet freezes itself
and writes down what happened. Every decision leaves a tamper-evident trace.
Why so paranoid? Because in custody, the failure mode is not a crash — it is
a *quiet lie*: a verifier that says "valid" when it should say "invalid," a
history that has been edited, a green light nobody actually checked. Every
mechanism you will meet in this course exists to make a quiet lie either
impossible or loud.
### 0.2 The estate in five minutes
warden does not float alone. It is the custody corner of a larger estate:
- **Four verified forks** (`dalek`, `anza`, `risc0`, `betrusted`
`-ed25519-verified`): four independent Ed25519 implementations, each with
machine-checked proofs (in the Lean 4 proof assistant) that the code
matches the mathematics, each fork from a different upstream lineage.
- **The Lean Transparency Log** (LTL, live at `ltl.zkdefi.org`): a public,
append-only log. Each entry is a signed statement — *"this repository, at
this exact commit, was verified with this exact toolchain, with this
result"* — recorded so it can never be quietly edited or denied.
- **pacta** (this repository): the tooling that verifies, grades, and
consumes that evidence — and warden, the wallet that stakes custody on it.
- **The public faces**: the log's API, the paper, the blog, the mirror.
You will meet all of these from inside the cockpit. You do not need to
memorize the estate — that is the Architect's chair, Session 6, and there is
a live map.
### 0.3 The three laws of the cockpit
Everything you look at for the rest of the course obeys three laws. Learn
them now; test them all course long:
1. **The design law — it renders evidence, it never asserts it.** Every panel
is recomputed from the wallet's files at the moment the page loads, by the
same functions the wallet itself uses. Every panel ends with a dashed
*provenance line* naming the function and timestamp that produced it.
What cannot be recomputed shows a red FAILED TO VERIFY — never a stale
green, never a neutral gray.
2. **The UX law — it never leaves a human in the dark.** Verdicts come in
words before colors; every panel has a "How to read this panel" expander;
every term links to the glossary.
3. **The crew law — roles are distinct and cooperate through handoffs.** Six
roles run this estate. The one who proposes never approves; the one who
verifies never proposes; the one who watches never overrides the bench.
You are about to become all six — *one at a time*.
### LAB 0
1. ▶ On the deck, read each pane's header: name and italic question. Say each
role's question out loud (yes, out loud — it works).
2. ▶ Click **← Bridge** in the deck's top bar. Read the verdict banner and
the strip of chips under it.
3. ▶ Find the **"If this happens, who acts"** dispatch table. ✎ Copy the
two-column skeleton (event → station) onto paper. This is your course map:
each row is a session.
4. ▶ Return to the deck (the STATIONS row of tabs, or your browser's back).
> ✔ **Checkpoint.** The bridge said **CUSTODY HEALTHY** in words, the chips
> said `4 pinned` and `chain verified`, and your paper holds a seven-row
> dispatch table.
### Self-test 0 *(answers in Appendix B)*
1. What is the one idea warden is built on, in one sentence?
2. Why does the cockpit refuse to show a "neutral gray" state?
3. Name the six roles without looking.
---
## Session 1 — the Newcomer: learning to read evidence
**You are becoming:** the person who reads evidence correctly and whose
confusion is a diagnostic instrument, not an embarrassment.
### 1.1 Why this role exists
Every other role assumes a skill nobody is born with: reading a security
surface *without trusting it*. The Newcomer chair is where that skill is
built. It is also the estate's quality sensor: veterans stop seeing gaps;
fresh eyes find them. That is why the Newcomer's report — "this page confused
me" — is treated as a bug report about the page, never about the reader.
### 1.2 The mind of the Newcomer
Adopt these three postures for this session (and keep them forever):
- **Verdict first.** On any page, read the words at the top before any
numbers. If you read nothing else, read the verdict.
- **Provenance always.** Before believing a panel, glance at its dashed
footer: *what function recomputed this, and when?* No footer, no belief.
- **Ask the page.** Every panel has a "How to read this panel" expander and
little `?` marks. Using them is the skill, not a failure of it.
### 1.3 Concepts: the reading system
- **Colors mean one thing each.** Green = re-checked just now and passed.
Amber = waiting, or needs attention. Red = failed, or *could not be
checked*. That last part matters: the cockpit treats "I don't know" as red,
because in custody, unverified and broken deserve the same caution.
- **The provenance line is the anti-cache.** It names the exact function
(e.g. `Wallet.verify_ledger()`) and the UTC second of recomputation.
- **FAILED TO VERIFY is honesty, not breakage.** It means: this panel refused
to guess.
### LAB 1
1. ▶ Open the **Guide** (INSTRUMENTS row). Read it fully once — ten minutes,
no skimming. It is the reference the rest of the course leans on.
2. ▶ Open **Posture**. Read only the verdict banner and each panel's *first
sentence*. ✎ In one line each: what do the latch, ledger, quorum, signing
rules, and recorded-history panels answer?
3. ▶ The recompute proof: note the timestamp in the Ledger panel's provenance
line. Reload the page. Compare.
4. ▶ Open one `?` mark (any panel) and follow it to the glossary and back.
5. ▶ On the deck, run wizard steps 1–3 if you have not already (the wizard is
this session's condensed twin).
> ✔ **Checkpoint.** The provenance timestamp *changed* when you reloaded —
> you watched the ledger's full hash chain being re-verified for you,
> live, both times. That is the design law observed with your own eyes.
### What the Newcomer never does
- Never pretends to understand. Every other chair once sat here.
- Never assumes a confusing page is their fault — they report it.
*Thought experiment:* if newcomers politely stayed quiet, which of the three
laws would rot first, and who would notice — and when?
### Handoff
The Newcomer **delivers** confusion reports to the Architect and Operator,
and **receives** the guide, the demo, and patient answers. ✎ Write one real
confusion report from your Lab 1 (there is always one). Keep it — you will
deliver it in Session 6.
### Self-test 1
1. A panel shows green. What two things did the cockpit do before showing it?
2. What is the difference between red-failed and red-could-not-check, and why
does the cockpit refuse to distinguish them visually?
3. Where do you look first on any page?
> **Recap card — NEWCOMER.** Question: *what is all this?* Reads verdict
> first, provenance always. Confusion = instrument. Never silent, never
> ashamed. Delivers: fresh eyes.
---
## Session 2 — the Proposer: asking precisely
**You are becoming:** the origin of every signature — the one who asks, and
who lives with written answers.
### 2.1 Why this role exists
Somebody has to want something signed; in production that is the financial
agent. The danger of the asking role is scope creep: the asker who also
approves, or who "just quickly" adjusts policy to fit their own request, has
dismantled the whole trust story alone. So the estate gives asking its own
chair with hard walls — and in exchange, the Proposer gets something rare:
**every "no" arrives in writing, with instructions.**
### 2.2 The mind of the Proposer
- **Precision or nothing.** A proposal is the exact bytes to be signed, named
by their SHA-256 fingerprint. "Roughly this transaction" does not exist.
- **A refusal is a to-do list.** Not an insult, not a negotiation opening —
a machine-readable statement of what rule fired and what would satisfy it.
- **I ask; I never approve.** Even when — especially when — I am sure.
### 2.3 Concepts
- **The payload fingerprint.** SHA-256 of the exact bytes to sign. The
offline signer signs those bytes and nothing else; both sides of the
air gap can compare fingerprints before anything happens. Every later
dispute is settled by this hash.
- **The front door.** Proposals enter through the wallet's agent-native MCP
surface — the `request_signature` tool on `pacta wallet mcp`. There is
deliberately no cozier side entrance.
- **The refusal receipt.** `code` (which rule fired), `missing` (the exact
unmet precondition), `remediation` (what would make the same request
succeed). Machine-readable so an agent — or you — can correct and retry
without guessing.
- **Queue states.** *awaiting device* = parked in the outbox, the offline
signer has not answered; *answered* = a response file arrived in the inbox.
### LAB 2
1. ▶ In the **amber Proposer pane** (or the full station page), find the
queue. One request sits *awaiting device*. ✎ Note the first 12 characters
of its payload fingerprint.
2. ▶ Watch a fingerprint being born. In your second terminal:
```
printf 'pay 5 to bob' > /tmp/payload.demo
sha256sum /tmp/payload.demo
```
Change one character (`5` → `6`) and hash again. ✎ How much of the
fingerprint changed? What does that mean for "roughly this transaction"?
3. ▶ From the Proposer station's instrument links, open **Incidents** and
read the demo refusal receipt. ✎ Fill this sentence from its fields: *"My
request was refused under rule ________ because ________ was missing; it
would succeed if I ________."*
4. ▶ Read the Proposer station's Duties top to bottom — every command shown
is the real CLI. (⌂ The JSON-RPC lines for driving `request_signature` by
hand are in `WALLET.md` — worth a look, not required.)
> ✔ **Checkpoint.** Your two hashes differ completely (an avalanche — one
> character flipped roughly half the bits), and your refusal sentence reads:
> rule `POLICY_DENIED`, missing *allowlisted destination*, succeed after
> *adding the destination to the policy allowlist*.
### What the Proposer never does — and why
- **Never approves or verifies their own proposal.** Self-approval is the
single cheapest attack on any custody system: no cryptography needs to be
broken, only one person's honesty. The wall is load-bearing.
- **Never touches the air-gap device or its folders.** The walk belongs to
the Operator; splitting request-maker from request-carrier means collusion,
not error, is required for abuse.
- **Never edits `policy.json` to fit their own request.** Policy changes are
the Operator's deliberate act — and the ledger records them permanently.
### Handoff
Delivers: fingerprinted requests → the signing firewall; escalations after
repeated refusals → the Operator. Receives: a signature, or a refusal
receipt ← the wallet. ✎ Draft a two-line escalation note for the demo
refusal, addressed to the Operator. Keep it for the capstone.
### Self-test 2
1. Why is the payload fingerprint the thing both sides of the air gap
compare, rather than a human-readable description?
2. Name the three fields of a refusal receipt and each one's job.
3. Your request keeps being refused and you are *certain* it is fine. List
your legal moves.
> **Recap card — PROPOSER.** Question: *how do I ask?* Exact bytes,
> fingerprinted. Refusals are instructions. Asks through the front door;
> never approves, never carries, never bends policy.
---
## Session 3 — the Quorum bench: four seats, one answer each
**You are becoming:** one seat of four — a verifier whose entire value is
that its judgment is nobody else's.
### 3.1 Why this role exists
One verifier — however carefully built — is one bug, one backdoor, one
compromised build machine away from a quiet lie. warden's answer is not "be
more careful"; it is **independence multiplied**: four verifier programs,
each built from a *different* formally verified Ed25519 codebase from a
different upstream lineage. For a wrong verdict to pass, the same lie would
have to exist independently in all four — not one mistake, but a coordinated
miracle.
### 3.2 The mind of a seat
- **My verdict is mine alone.** Built from my sources, computed by my
binary. I do not preview, harmonize, or average with the other seats.
- **Dissent is my job working.** If I say INVALID while three say OK, I have
either caught the failure of the century or found a bug in myself — both
are exactly what four seats exist to surface. Custody freezes; humans look.
- **My independence is my hygiene.** A shared toolchain, cache, or patch
with another seat is a shared bug: four seats that secretly agree because
they are one seat protect nothing.
### 3.3 Concepts
- **Unanimity or latch.** All members must independently accept, or custody
freezes. Not majority — a 3-of-4 design would trade the estate's whole
premise (catch the quiet lie) for availability. Here, one honest dissenter
outvotes three comfortable agreements — by design.
- **Pinning.** The custody capsule stores each member binary's SHA-256. On
use, the file on disk is re-hashed and compared: a swapped or modified
binary fails and is rejected. Pinning proves the file is *unchanged* —
and, honestly, nothing more.
- **Evidence grades R0–R5.** This estate's scale for formal evidence:
R0 = no usable evidence … R4 = machine-checked proofs covering the full
documented boundary … R5 would add reproducible builds and side-channel
assurance. **Nothing holds R5 yet**, so pinning cannot prove a binary was
honestly *built* from its attested sources. The capsule requires R4 of
every member, and the gap to R5 is stated everywhere it matters — an
honest system states its own boundary.
- **The capsule.** The wallet's founding document: members, pins, policy.
Its own SHA-256 is anchored in the ledger's first entry — so even the list
of who is trusted cannot be quietly swapped.
### LAB 3
1. ▶ **Indigo Quorum pane** (or full Posture): the bench roster. ✎ For each
of the four seats: backend name, the repo it is built from, and the first
8 characters of its binary fingerprint. Write all four — the act of
copying fingerprints by hand is the point.
2. ▶ Open the roster's "How to read this panel" expander and read the
*evidence grade* bullet. ✎ In one line: what exactly would R5 add, and
what attack does its absence leave open?
3. ▶ In the terminal:
```
pacta wallet status --wallet "$W"
```
✎ Find the members and the capsule hash in the output. Does the capsule
hash's first 24 hex match what the cockpit's quorum panel shows?
4. ▶ Open **Incidents** and read the demo divergence: `risc0` answered
INVALID where three answered OK. ✎ As the risc0 seat, write two sentences
defending your dissent to the Operator *without apologizing*.
> ✔ **Checkpoint.** Four seats on paper with four distinct fingerprints; the
> CLI's capsule hash matches the cockpit's; your dissent defense states what
> you observed and refuses to guess at what the others did.
### What the bench never does — and why
- **Never proposes.** The bench judges evidence; the moment it originates
spends, judge and party have merged.
- **Never harmonizes before answering.** Pre-agreement converts four
independent measurements into one measurement with four signatures.
- **Never clears a latch its own dissent caused.** You are a witness to your
own alarm, not its judge.
*Thought experiment:* an attacker can fully compromise the build of exactly
one seat. Walk through what happens on the next verification — and what the
attacker would have needed instead for the lie to go through.
### Handoff
Delivers: unanimous admits, or a latch-tripping dissent → the wallet;
divergence incidents → the Operator. Receives: component evidence ← the
wallet's inbound boundary; rebuilt pinned sources ← the Architect's forks.
### Self-test 3
1. Why unanimity instead of 3-of-4 majority — what is being traded for what?
2. What does a pinned fingerprint prove, and what does it *not* prove? Name
the grade that would close the gap.
3. Your seat dissents and custody freezes trading for a day. Was this a
success or a failure? For whom?
> **Recap card — QUORUM SEAT.** Question: *would I stake custody on this?*
> One seat, one codebase, one verdict. Unanimity or latch. Independence is
> hygiene; dissent is the job working; never proposes, never averages.
---
## Session 4 — the Operator: watching, and the day something breaks
**You are becoming:** the person who watches the pulses, holds the brakes,
and writes the permanent notes — the calm in the estate.
### 4.1 Why this role exists
Every guarantee you have met so far is *checkable* — but checkable is
worthless if nobody checks. An unwatched log, an unprobed service, an
unverified ledger are safe only on paper. The Operator is the estate's
standing answer to "who actually looks?" — and, when the latch trips, the
one chair with the authority (and the obligation) to run the recovery by the
book.
### 4.2 The mind of the Operator
- **Liveness is not honesty.** My probes tell me something *answered* — not
that it told the truth. Truth is the Cryptographer's replay; I check
pulses, daily, on demand, never on autopilot.
- **Procedures over improvisation.** When the latch trips, I open the
runbook. Excitement is for people without checklists.
- **Permanent notes.** My unlatch decision goes into the ledger with a
written root cause, forever. If I cannot write the cause, I am not done
investigating.
### 4.3 Concepts
- **The liveness board.** On-demand probes: HTTP GET on each public service
(status, observed facts, latency), `git` checks on each local working copy
(present, HEAD, clean/dirty). It runs only when you press **Probe now** —
the cockpit never phones home on an ordinary page load.
- **The latch lifecycle.** Trips on quorum divergence or suspected tampering
→ all outbound signing refused (with receipts) → investigation per
`docs/runbook-latch.md` → root cause fixed → `pacta wallet unlatch` with a
mandatory note, recorded permanently.
- **Append-only ethics.** The transparency log's operator side has four
absolute nevers: never force-push the log repo, never edit or delete under
`entries/`, never re-sign a published head, never backdate. An append-only
log that gets "corrected" once is not append-only — it is marketing.
- **Advancing the pin.** `pacta sth-refresh` fetches the log's newest signed
head, verifies its signature *and its consistency with the previously
pinned tree size*, then advances the local pin — the defense against a log
that shows different histories to different people (split view) or rolls
back.
### LAB 4
1. ▶ **Green Operator pane**: press **Probe now**. ✎ Record: the log head's
`tree_size` and root prefix; the slowest probe's latency; any repo marked
*dirty* (uncommitted changes) — dirty is amber, not red: alive, but with
local work in progress.
2. ▶ Daily wallet checks, from the terminal:
```
pacta wallet status --wallet "$W"
pacta wallet verify-ledger --wallet "$W"
```
✎ What did verify-ledger actually recompute? (The Ledger panel's
explainer has the exact answer.)
3. ▶ **The tamper drill.** You will now watch the system catch history
editing — on a **copy**:
```
cp -r "$W" /tmp/tamper-lab-wallet
sed -i 's/genesis/gene-sis/' /tmp/tamper-lab-wallet/ledger.jsonl
pacta wallet verify-ledger --wallet /tmp/tamper-lab-wallet
```
One character of history changed. ✔ The verifier reports the chain broken
at the first entry — loudly, non-zero exit.
4. ▶ Now see it as the crew would: point a *second* cockpit at the corpse:
```
pacta wallet cockpit --wallet /tmp/tamper-lab-wallet --port 8481
```
Open `http://127.0.0.1:8481/posture`. Read the banner. Then stop that
server (Ctrl-C) and destroy the evidence of your crime:
```
rm -rf /tmp/tamper-lab-wallet /tmp/payload.demo
```
5. ▶ Read the Operator station's Duties 2 and 3 (`sth-refresh`,
`witness-audit`) — these are the same watching, aimed at the public log.
(⌂ With internet and a clone of `lean-transparency-log`, run
`pacta witness-audit --published-dir <clone>` and watch every historical
head re-verified.)
> ✔ **Checkpoint.** The tampered copy produced (a) a failing
> `verify-ledger` naming the broken entry and (b) a cockpit banner reading
> **CUSTODY EVIDENCE BROKEN** with the ledger panel red. You edited one
> character of one file, and two independent surfaces caught it instantly.
> *That* is what a hash chain buys.
### What the Operator never does — and why
- **Never unlatches without a written root cause.** The CLI refuses an empty
note; the ledger keeps it forever. An unexplained unlatch is a future
incident with a head start.
- **Never rewrites history** — the four log nevers above. The log's entire
value is that this never happened, not that it rarely happens.
- **Never overrides the bench.** A divergence gets investigation, not a
fifth vote.
- **Never signs or proposes.** The brakes and the pen live in different
chairs.
### Handoff
Delivers: unlatch decisions with permanent notes → the ledger; outage and
repair notes → the Architect. Receives: incidents ← wallet and bench;
escalations ← the Proposer (you are holding one from Session 2 — file it
mentally under "capstone").
### Self-test 4
1. Alive and honest — whose job is each, and with which tools?
2. Recite the four log nevers. Which one would be the *most* tempting on a
bad day, and why is it still absolute?
3. In the tamper drill, why did changing bytes in entry 1 break the chain at
entry 1 rather than at the newest entry?
> **Recap card — OPERATOR.** Question: *is everything running, and is
> custody unfrozen?* Probes on demand; verifies the chain daily; runs the
> runbook when the latch trips; writes permanent notes; never rewrites,
> never overrides, never signs.
---
## Session 5 — the Cryptographer: recompute everything
**You are becoming:** the person who accepts nothing they did not recompute
— and who knows *exactly* where each guarantee stops.
### 5.1 Why this role exists
Everything in this estate ultimately reduces to a claim someone could check.
The Cryptographer is the someone. Without this chair, "verifiable" quietly
degrades into "verified by nobody" — and the estate becomes exactly the
kind of trust-me system it was built to replace.
### 5.2 The mind of the Cryptographer
- **Recompute, don't trust.** A green light I did not recompute is a rumor —
including the cockpit's own green lights.
- **Boundaries are sacred.** "Verified" means precisely what the certificate
says — never one theorem more. Stretching a claim past its boundary is not
enthusiasm, it is a false claim.
- **The log is not an oracle.** It is an accountability ledger: it makes
claims permanent and attributable, not true. A lie recorded in the log is
still a lie — permanently on the record, and catchable by replay.
### 5.3 Concepts
- **Attestation.** A signed statement: repository X, at exact commit C, was
verified with exact toolchain T, with result R (every certificate, every
axiom listed). It names its own evidence precisely enough to replay.
- **Transparency receipt.** Proof that the attestation is recorded in the
public log: an *inclusion proof* (a short chain of hashes showing the
leaf is under the log's signed root) plus the *signed tree head*. Verify
both and you know: this exact statement is permanently in the public
record — the operator can never unsay, edit, or deny it.
- **What the log guarantees — and what it does not.** The Merkle machinery
guarantees inclusion, append-only history, and transferable evidence of
equivocation (two conflicting signed heads at the same size, in one log
context, convict the key holder). It does **not** referee truth: a leaf's
*content* can be false, and only independent replay — off-protocol work
with the proof assistant — catches that. The design's honest slogan:
cheap to claim, impossible to unsay, catchable forever.
- **Claim boundaries you must be able to recite.** The Ed25519 proofs treat
SHA-512 as an opaque function (its correctness is assumed, not proven);
reproducible builds are out of scope (the R4/R5 gap); the mechanized
results cover the accumulator model as stated in the paper, with a
published ledger of what is *not* proven. Where the mathematics stops,
the certificate says so.
### LAB 5
1. ▶ **Purple Cryptographer pane**: click **Load the sample evidence**, then
**Verify (read-only)**. Do not just admire the green: ✎ copy out the
diagnostics list and annotate each line with what check it was
(signature? inclusion? hash equality? freshness?). Use the panel's
explainers.
2. ▶ Break it, three ways. After each, restore (reload the sample) before
the next:
- delete one character from the **receipt** box → verify;
- delete one character from the **attestation** box → verify;
- delete one character from the **public key** box → verify.
✎ For each: what failed, and *at which layer*? Notice the error surfaces
are different — a verifier that fails identically for every cause is a
verifier you cannot debug.
3. ▶ Boundary recitation, closed-book: ✎ write the three claim boundaries
from 5.3 from memory. Check yourself against the guide's "What this
cockpit cannot tell you."
4. ⌂ **The full replay** (internet + a clone):
```
pacta log-fetch --url https://ltl.zkdefi.org --component dalek-ed25519-verified
git clone https://zkdefi.org/saymrwulf/lean-transparency-log
cd lean-transparency-log && python3 verify.py --all && python3 verify_selftest.py
```
`verify.py --all` re-checks every leaf, every signed head, every receipt,
offline, fail-closed — and `verify_selftest.py` then attacks the verifier
itself with corrupted inputs to prove it *would* fail if lied to.
✎ Why does shipping the self-test beside the verifier matter?
> ✔ **Checkpoint.** One ACCEPTED verdict whose every diagnostic line you can
> name; three different refusals you caused on purpose and can tell apart;
> three boundaries recited without looking.
### What the Cryptographer never does — and why
- **Never accepts an unrecomputed green** — the chair exists to be the
recomputation.
- **Never extends a claim past its boundary.** The estate's credibility is
the sum of its stated limits; one stretched claim spends all of it.
- **Never treats the log as a truth oracle.** Permanence is not truth;
replay is truth's only entrance.
### Handoff
Delivers: audit verdicts → Operator and Proposer; boundary corrections →
the Architect (docs and map). Receives: artifacts to audit ← anyone; fresh
evidence ← the live log.
### Self-test 5
1. An attestation verifies perfectly: signatures good, inclusion proven,
head signed. List everything this does — and does not — tell you.
2. What is equivocation evidence, and why is it the one misbehavior directly
attributable to the log operator?
3. Why did the three sabotages in Lab 5 fail *differently*, and why is that
a feature?
> **Recap card — CRYPTOGRAPHER.** Question: *does the evidence prove what it
> claims?* Recomputes everything, everywhere, including the cockpit. Knows
> each boundary by heart. Log = permanent, not true; replay decides. Never
> stretches, never trusts, never tires.
---
## Session 6 — the Architect: the map and the territory
**You are becoming:** the person who keeps the whole estate tellable — every
repo, service, mirror, and loop — and who guards what may be said in public.
### 6.1 Why this role exists
The estate is many repositories, services, mirrors, and two self-referential
loops. No head holds that reliably — and an estate nobody can hold is an
estate where drift, duplication, and quiet inconsistency breed. The
Architect's answer is a *map that is recomputed, never remembered* — and a
tripwire that screams when the map forks from itself.
### 6.2 The mind of the Architect
- **The map is recomputed, never remembered.** If I "know" the estate from
memory, I know last month's estate.
- **Two renderings of one model need a tripwire.** Anything that exists
twice will drift; the only question is whether the drift is caught.
- **Public is a one-way door.** A name published once is published forever.
Public documents list only entities whose existence is already public or
must be public for trust.
### 6.3 Concepts
- **The estate map.** Five lanes of custody (upstream sources → verified
subjects → machinery and operator-held → published faces → consumers),
with every entity carrying its *runtime* (always-on / on-demand /
not-running / static) and mutability class.
- **The two loops** — the estate's hardest furniture, each tellable in one
breath:
- **Loop 1, the dogfood signer:** the log's own signing machinery uses an
Ed25519 implementation that is itself verified and attested *inside the
log it signs* (leaf 8). The tool guards the evidence; the evidence
covers the tool.
- **Loop 2, the self-attesting mechanization:** entry 13 of the log is the
kernel-checked mechanization of the very soundness arguments the log's
accumulator relies on. The proofs about the machinery live inside the
ledger the machinery protects — scoped honestly, with a published list
of what is *not* proven.
- **The drift tripwire.** The map exists twice (committed `ESTATE.md`; the
cockpit's estate view). A name-level comparison runs live on the Architect
station and in the test suite; if the renderings disagree, the suite fails.
- **The generated-file lesson** (a true war story): a published verifier
once got hardened at its destination while the *template that generates
it* kept the old, weaker code — a time bomb where the next publish would
have silently un-fixed it. It was caught in an audit and now has its own
tripwire test. The Architect's rule ever since: **when you fix a
generated file, find and fix its generator in the same change.**
### LAB 6
1. ▶ **Slate Architect pane**: read the **drift tripwire** result. Then open
the **Estate map** (instrument link). Click the transparency-log card and
read its dossier. ✎ Which lane is it in, what is its runtime, what is its
mutability?
2. ▶ Find warden/pacta on the map. ✎ Which entities *consume* the log's
evidence, per the map's edges?
3. ▶ Trace Loop 2 on the map until you can tell it in one breath. ✎ Write
both loops, one sentence each, closed-book.
4. ▶ Close the map. ✎ Draw the five lanes from memory — boxes and arrows,
ninety seconds, ugly is fine. Reopen and compare. What did you misplace?
5. ▶ Deliver the Newcomer's confusion report from Session 1 (you kept it):
decide *as the Architect* — is it a page bug, a glossary gap, or a map
gap? ✎ Write the one-line disposition.
> ✔ **Checkpoint.** The tripwire says the renderings agree; both loops exist
> as single sentences in your handwriting; the confusion report has a
> disposition.
### What the Architect never does — and why
- **Never names private infrastructure in public artifacts.** Existence
disclosure is irreversible and someone else's risk to accept, not yours.
- **Never fixes a generated file without its generator** — the war story
above is why this is a never and not a tip.
- **Never redraws the map from memory.** Memory is where drift lives.
### Handoff
Delivers: the updated, drift-guarded map → everyone. Receives: outage and
repair notes ← the Operator; boundary corrections ← the Cryptographer;
confusion reports ← the Newcomer.
### Self-test 6
1. Tell both loops, one sentence each.
2. Why is "runtime" (always-on / on-demand / static) a property the *map*
must carry, rather than something people just know?
3. A teammate fixed a bug directly in a published, generated file and
pushed. What do you do, in order?
> **Recap card — ARCHITECT.** Question: *does the map match the territory?*
> Five lanes, two loops, runtime on everything. Tripwires over trust;
> generators with their outputs; public is forever. Never draws from memory.
---
## Session 7 — Capstone: the incident day
*One person, six chairs, one incident, no AI. You will walk a single event
through every role, producing each role's real artifact. Do this with the
deck open — move your eyes to each pane as you take its chair. If you run a
study club (see Session 8), this is the session to run as a group, one chair
per person.*
**The scenario.** A routine component re-verification comes through the
wallet's inbound boundary. Seat `risc0` answers INVALID; `dalek`, `anza`,
`betrusted` answer OK. The latch trips. (This is exactly the incident your
demo wallet carries — the deck is your set dressing.)
Work the stations **in this order**, writing each artifact (✎) before
moving to the next chair. Do not blend chairs — that is the whole exam:
1. **The wallet speaks first** (no chair): an incident file exists; the
latch is on; every signing request now gets a refusal receipt citing
`CUSTODY_LATCHED`. ▶ Find all three facts in the cockpit (incidents
list; latch panel wording; refusal-code explainer).
2. **Proposer.** Your pending payment just got refused. ✎ Artifact 1: the
escalation note to the Operator — request id, payload fingerprint,
refusal code, and the sentence "awaiting custody recovery; will resubmit
unchanged." (No pressure on anyone to hurry — note that restraint; it is
the role.)
3. **Operator.** Open the runbook mentally: freeze confirmed, incident read.
✎ Artifact 2: the investigation plan — three numbered checks you will
run, in order, and who you will hear from before any unlatch (the bench
and the cryptographer). *Hint: your Session 4 daily checks are two of the
three.*
4. **Quorum seat (risc0).** ✎ Artifact 3: the dissent defense — what your
seat observed, refusal to speculate about other seats, and the one thing
that would change your verdict (a re-run on your rebuilt, re-pinned
binary).
5. **Cryptographer.** ✎ Artifact 4: the audit verdict — what you recomputed
(the payload against each seat's verifier, the members' pins, the
evidence receipts), what you found (in this scenario's story: the risc0
seat's binary was faulty *at sealing time* — its pin verified, meaning
unchanged since sealing, which is exactly why pin-checking could not
catch it; a rebuild from the pinned proven sources produced a differing,
correct binary), and the boundary sentence: "this attributes the
divergence; it does not prove the other three correct — their pins
verified, and unchanged-since-sealing is all a pin ever proves."
6. **Operator again.** Root cause in hand (stale seat binary; rebuilt and
re-pinned by the bench). ✎ Artifact 5: the permanent unlatch note —
cause, fix, evidence checked, date. One paragraph you would sign with
your name, knowing the ledger keeps it forever.
7. **Architect.** ✎ Artifact 6: the map disposition — does anything on the
estate map change? (A seat was rebuilt and re-pinned: the capsule's pin
set changed, which is a re-sealing event the wallet's dossier must
reflect — and the incident is now permanent recorded history. One line
each.)
8. **Newcomer** (yes, last chair): reread all six artifacts as someone who
joined today. ✎ Artifact 7: the one place the paper trail would confuse a
fresh reader, and the one-line fix.
> ✔ **Checkpoint — the debrief.** Lay the seven artifacts in a row. Notice
> three things. *Every handoff is written* — nothing moved by hallway
> conversation. *No chair did another chair's job* — the proposer never
> argued innocence, the bench never touched the latch, the operator never
> re-verified crypto. And *the system was never trusted to be fine* — it
> was recomputed fine, at every step. That is the crew law, lived once,
> end to end.
---
## Session 8 — Graduation: toward the real thing
### 8.1 What changes with a real wallet
The demo you have been flying is custody-inert: fake members, throwaway
keys. The real path — read it now, walk it when you mean it:
1. **Build the quorum from the pinned proven sources:**
`pacta wallet build-quorum --sources-root <fork-checkouts>` — four real
verifier binaries, four real fingerprints.
2. **Fetch real evidence** for every member from the live log:
`pacta log-fetch --url https://ltl.zkdefi.org --component <each>`.
3. **Seal the wallet — the R4 gate in executable form:**
`pacta wallet init --wallet <dir> --evidence <dir> --log-public-key
log.pub --trusted-provider <name>` — it *refuses* to seal below
end-to-end evidence coverage. A wallet that cannot prove its bench is a
wallet that does not open.
4. **Write policy before you need it:** `pacta wallet policy --wallet <dir>
--init-template`, then edit limits and allowlists while nothing is at
stake.
5. **Decide the air-gap story** (which machine holds the key, who walks the
files) — and only then let value near it.
### 8.2 Running this as a study club
The capstone was built for a table of people: one chair each, artifacts
passed as real handoffs, the deck on a shared screen. Rotate chairs and
re-run it — the incident reads completely differently from inside another
role, and *that* discovery is the club's graduation. (One person plus an AI
agent works too: the agent takes the chairs you are not sitting in — but it
must obey the same law you learned: one chair at a time, handoffs in
writing.)
### 8.3 Where this manual ends
- The **paper** — the transparency model, the accountability games, and the
honest limits, with full rigor: linked from the estate map's log dossier
and at `ltl.zkdefi.org/paper`.
- The **blog** (`blog.zkdefi.org`) — the narrative pieces, including what
the log does and does not promise.
- **`WALLET.md`** and **`docs/`** in this repository — the wallet's
reference documentation, threat model, runbooks, product lineup.
- The **curriculum repository** (`verifying-crypto-with-lean`) — if Session
5 left you wanting the mathematics itself, that is its course.
You came in as one person. You leave as a crew that happens to share a
body — and you know which chair you are sitting in at every moment.
---
## Appendix A — command reference by chair
*All read-only against the demo wallet except where marked ⚠ (mutates
wallet state — real operations, operator's deliberate acts).*
| Chair | Command | What it does |
|---|---|---|
| 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 | `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 |
| Operator | `pacta wallet verify-ledger --wallet DIR` | recompute the full hash chain |
| Operator | `pacta sth-refresh --url URL --sth-store F --log-public-key K` | advance the log pin (split-view defense) |
| Operator | `pacta witness-audit --published-dir DIR` | re-verify a log clone's entire history |
| Operator ⚠ | `pacta wallet unlatch --wallet DIR --note "cause"` | clear the latch; note recorded forever |
| Cryptographer | `pacta receipt-verify --attestation A --receipt R --log-public-key K` | verify one receipt (add `--sth-store`, `--max-sth-age-seconds`, `--require-verified-verifier` to harden) |
| Cryptographer | `pacta log-fetch --url URL --component C` | fetch + locally verify fresh evidence |
| Cryptographer | `python3 verify.py --all` (in a log clone) | replay the whole log offline |
| Architect | `python3 scripts/mini_pytest.py` | run the suite, incl. the drift tripwire |
## Appendix B — self-test answers
**0.1** No single program is trusted: four independently built, formally
verified verifiers must unanimously agree before the wallet trusts a
component; disagreement freezes custody and is recorded.
**0.2** Gray would mean "status unknown, presumed fine." In custody,
unverified must look as alarming as broken — so unknown renders red
(FAILED TO VERIFY), never neutral.
**0.3** Newcomer, Proposer, Quorum bench, Operator, Cryptographer,
Architect.
**1.1** It recomputed the underlying fact from the wallet's files at
request time, and it stamped a provenance line naming the function and
timestamp that did it.
**1.2** Red-failed = a check ran and failed; red-could-not-check = the check
could not run. Visually identical on purpose: both must stop you, and a
distinction would invite "it's probably just the checker."
**1.3** The verdict, in words, at the top.
**2.1** The fingerprint commits to the exact bytes; a description can match
many byte strings (and can be argued about later). Both sides hash
independently and compare — no trust in transcription needed.
**2.2** `code` = which rule fired; `missing` = the precise unmet
precondition; `remediation` = what would make the same request succeed.
**2.3** Read the receipt and remediate; resubmit unchanged if the receipt
says the block is temporary (e.g. latch); escalate in writing to the
Operator. Not on the list, ever: self-approve, touch the device, edit
policy.
**3.1** Unanimity trades availability (any seat can halt custody) for the
guarantee that a single honest seat defeats a quiet lie. Majority would
keep trading through exactly the event the system exists to catch.
**3.2** Pinning proves the binary on disk is byte-identical to the one
sealed in the capsule. It does not prove the binary was honestly built from
the attested sources — that is the reproducible-builds gap, closed only at
grade R5 (which nothing holds yet, and the estate says so).
**3.3** A success of the mechanism (the lie or fault did not pass), whatever
it cost in downtime. For the seat: the job working. For the estate: the
premium it agreed to pay.
**4.1** Alive = Operator, with probes (HTTP GET, git checks). Honest =
Cryptographer, with recomputation (receipt-verify, offline replay).
**4.2** Never force-push, never edit/delete under `entries/`, never re-sign
a published head, never backdate. The tempting one is re-signing "to fix a
mistake" — and it is absolute because one corrected head destroys the only
thing the log sells: that this never happens.
**4.3** Because every entry contains the hash of the previous one, the
chain is checked from genesis forward; the first entry whose stored link
fails to recompute is where verification stops and reports. The tamper was
*in* entry 1, so the chain broke *at* entry 1.
**5.1** It tells you: this exact statement is permanently recorded in the
log under a validly signed head, and the artifacts are internally
consistent. It does not tell you: that the statement's content is true
(replay decides that), that the verification it describes was competent, or
anything beyond the certificate's stated boundary.
**5.2** Two conflicting signed tree heads at the same tree size, in one log
context. Only the operator's key can produce signed heads, so two
conflicting ones are transferable proof of double-speak, attributable to
the key holder — no interpretation needed.
**5.3** Each sabotage hit a different layer (log signature chain,
attestation content hash, key parsing), and the verifier reports the layer
that failed. Distinct failures mean a debuggable verifier — and are
themselves evidence the checks are real and separate, not one theatrical
boolean.
**6.1** Loop 1: the log's signing machinery runs on an Ed25519
implementation that is itself verified and attested inside the log it
signs (leaf 8). Loop 2: entry 13 is the kernel-checked mechanization of
the accumulator arguments the log itself relies on — the proofs about the
machinery live in the ledger the machinery protects.
**6.2** Because "what is running" is invisible from any single machine and
rots fastest in memory; carrying runtime on the map makes staleness a
checkable property instead of folklore.
**6.3** (1) Check whether the generator still produces the old file — if
so, the fix is a time bomb. (2) Fix the generator, regenerate, verify
byte-identity with the intended output. (3) Add the tripwire test that
fails on generator/output drift. (4) Only then consider the incident
closed — and write the note.
## Appendix C — glossary and further reading
Every term this manual uses — capsule, seat, pin, grade, ledger, latch,
incident, refusal receipt, air gap, attestation, receipt, provenance,
station — is defined in plain language in the cockpit's **Guide**
(`/guide`), which is the manual's companion reference. The estate map
(`/estate`) is the territory's picture; `ESTATE.md` is its committed twin;
the paper and blog (Session 8.3) are the deep end. Go sit in a chair.

5
src/pacta/cli.py
View file

@ -693,8 +693,9 @@ def cmd_wallet_cockpit(args: argparse.Namespace) -> int:
server = serve(wallet_dir, host=args.host, port=args.port) server = serve(wallet_dir, host=args.host, port=args.port)
host, port = server.server_address[0], server.server_address[1] host, port = server.server_address[0], server.server_address[1]
print(f"warden cockpit (READ-ONLY) on http://{host}:{port} - Ctrl-C to stop") print(f"warden cockpit (READ-ONLY) on http://{host}:{port} - Ctrl-C to stop")
print(f" the deck: http://{host}:{port}/deck - all six roles live, guided by the wizard") print(f" the deck: http://{host}:{port}/deck - all six roles live, guided by the wizard")
print(f" the guide: http://{host}:{port}/guide - every term explained") print(f" the course: http://{host}:{port}/manual - the lab manual: become every role")
print(f" the guide: http://{host}:{port}/guide - every term explained")
try: try:
server.serve_forever() server.serve_forever()
except KeyboardInterrupt: except KeyboardInterrupt:

4
src/pacta/deck.py
View file

@ -245,6 +245,10 @@ def render_deck(wallet_dir: str) -> str:
"<p class='muted' style='margin-top:.8rem;font-size:.74rem'>Pane " "<p class='muted' style='margin-top:.8rem;font-size:.74rem'>Pane "
"controls, tmux-style: ⟳ reload · ⤢ zoom one pane · ↗ open the full " "controls, tmux-style: ⟳ reload · ⤢ zoom one pane · ↗ open the full "
"station page. Your step is remembered for this browser session.</p>" "station page. Your step is remembered for this browser session.</p>"
"<p class='muted' style='font-size:.74rem'>Want the whole course, not "
"just the tour? <a href='/manual' target='_top'>Open the lab "
"manual</a> — sessions, drills, self-tests, capstone. Built to sit "
"on one monitor while this deck flies on the other.</p>"
"</aside></div>" "</aside></div>"
"<script>" "<script>"
"(function(){" "(function(){"

162
src/pacta/mdlite.py Normal file
View file

@ -0,0 +1,162 @@
"""mdlite - a deliberately small Markdown renderer (stdlib only).
Renders exactly the subset the lab manual uses: ATX headings (# ## ###),
paragraphs, **bold**, *italic*, `code`, fenced code blocks, unordered and
ordered lists, blockquotes, tables, horizontal rules, and [links](...).
Text is HTML-escaped first; code spans are protected from inline rules.
Why not a library: the cockpit is standard-library-only by law, and a
small renderer whose whole grammar fits on one screen is auditable in a
way a dependency is not. The test suite renders the real manual through
this and asserts no raw Markdown artifacts leak into the HTML.
"""
from __future__ import annotations
import html
import re
def _slug(text: str) -> str:
return re.sub(r"[^a-z0-9]+", "-", text.lower()).strip("-") or "section"
def _inline(text: str) -> str:
"""Inline rules over an already HTML-escaped string.
Code spans are stashed as placeholder tokens first, so bold/italic/link
rules can span across them (e.g. **never edits `policy.json` alone**)
while code content itself stays untouched by those rules."""
codes: list[str] = []
def stash(m: re.Match[str]) -> str:
codes.append(m.group(1))
return f"\x00{len(codes) - 1}\x00"
text = re.sub(r"`([^`]+)`", stash, text)
text = re.sub(r"\*\*([^*]+)\*\*", r"<strong>\1</strong>", text)
text = re.sub(r"(?<![*\w])\*([^*\n]+)\*(?![*\w])", r"<em>\1</em>", text)
text = re.sub(r"\[([^\]]+)\]\(([^)\s]+)\)", r'<a href="\2">\1</a>', text)
for idx, code in enumerate(codes):
text = text.replace(f"\x00{idx}\x00", f"<code>{code}</code>")
return text
def render(md: str) -> tuple[str, list[tuple[int, str, str]]]:
"""Render markdown -> (html, toc) where toc = [(level, text, anchor)]."""
lines = md.splitlines()
out: list[str] = []
toc: list[tuple[int, str, str]] = []
seen_slugs: dict[str, int] = {}
para: list[str] = []
i = 0
def flush_para() -> None:
if para:
out.append(f"<p>{_inline(html.escape(' '.join(para)))}</p>")
para.clear()
while i < len(lines):
line = lines[i]
stripped = line.strip()
# fenced code block
if stripped.startswith("```"):
flush_para()
i += 1
code: list[str] = []
while i < len(lines) and not lines[i].strip().startswith("```"):
code.append(lines[i])
i += 1
i += 1 # closing fence
out.append(f"<pre class='cmd'>{html.escape(chr(10).join(code))}</pre>")
continue
# heading
m = re.match(r"^(#{1,4})\s+(.*)$", stripped)
if m:
flush_para()
level = len(m.group(1))
text = m.group(2).strip()
base = _slug(re.sub(r"[*`\[\]()]", "", text))
n = seen_slugs.get(base, 0)
seen_slugs[base] = n + 1
anchor = base if n == 0 else f"{base}-{n}"
if level in (2, 3):
toc.append((level, re.sub(r"[*`]", "", text), anchor))
out.append(f"<h{level} id='{anchor}'>{_inline(html.escape(text))}</h{level}>")
i += 1
continue
# horizontal rule
if re.match(r"^-{3,}$", stripped):
flush_para()
out.append("<hr>")
i += 1
continue
# blockquote
if stripped.startswith(">"):
flush_para()
quote: list[str] = []
while i < len(lines) and lines[i].strip().startswith(">"):
quote.append(lines[i].strip().lstrip(">").strip())
i += 1
out.append("<blockquote><p>"
+ _inline(html.escape(" ".join(q for q in quote if q)))
+ "</p></blockquote>")
continue
# table
if stripped.startswith("|") and i + 1 < len(lines) and \
re.match(r"^\|[\s:|-]+\|$", lines[i + 1].strip()):
flush_para()
def cells(row: str) -> list[str]:
return [c.strip() for c in row.strip().strip("|").split("|")]
head = cells(stripped)
i += 2
rows: list[list[str]] = []
while i < len(lines) and lines[i].strip().startswith("|"):
rows.append(cells(lines[i].strip()))
i += 1
thead = "".join(f"<th>{_inline(html.escape(c))}</th>" for c in head)
body = "".join(
"<tr>" + "".join(f"<td>{_inline(html.escape(c))}</td>" for c in r)
+ "</tr>" for r in rows)
out.append(f"<div class='tablewrap'><table><tr>{thead}</tr>{body}</table></div>")
continue
# lists (one level)
m_ul = re.match(r"^[-*]\s+(.*)$", stripped)
m_ol = re.match(r"^\d+[.)]\s+(.*)$", stripped)
if m_ul or m_ol:
flush_para()
tag = "ul" if m_ul else "ol"
items: list[str] = []
while i < len(lines):
s = lines[i].strip()
m2 = re.match(r"^[-*]\s+(.*)$", s) if tag == "ul" else \
re.match(r"^\d+[.)]\s+(.*)$", s)
if m2:
items.append(m2.group(1))
i += 1
elif s and not re.match(r"^([-*]|\d+[.)])\s", s) and \
lines[i].startswith((" ", "\t")) and items:
items[-1] += " " + s # continuation line
i += 1
else:
break
lis = "".join(f"<li>{_inline(html.escape(item))}</li>" for item in items)
out.append(f"<{tag}>{lis}</{tag}>")
continue
# blank line ends a paragraph
if not stripped:
flush_para()
i += 1
continue
para.append(stripped)
i += 1
flush_para()
return "".join(out), toc

18
src/pacta/uikit.py
View file

@ -85,6 +85,24 @@ STYLE = """
.muted{color:var(--ink2);font-size:.85rem} .muted{color:var(--ink2);font-size:.85rem}
.mono{font-family:ui-monospace,monospace} .mono{font-family:ui-monospace,monospace}
.breakany{overflow-wrap:anywhere} .breakany{overflow-wrap:anywhere}
/* lab manual */
.toc ol{margin:.3rem 0;padding-left:1.4rem;columns:2;column-gap:2rem}
@media(max-width:44rem){.toc ol{columns:1}}
.toc li{font-size:.88rem;margin:.15rem 0;break-inside:avoid}
.manual{background:#fff;border:1px solid var(--line);border-radius:8px;
padding:1.2rem 1.6rem;margin:.7rem 0;font-size:.94rem}
.manual h1{font-size:1.45rem;margin:.4rem 0 .2rem}
.manual h2{font-size:1.2rem;margin:2.2rem 0 .5rem;padding-top:1.1rem;
border-top:2px solid var(--accentbg)}
.manual h3{font-size:1rem;margin:1.3rem 0 .3rem}
.manual h4{font-size:.92rem;margin:1rem 0 .25rem}
.manual blockquote{margin:.9rem 0;padding:.65rem .9rem;border-left:4px solid var(--ok);
background:var(--okbg);border-radius:0 6px 6px 0;font-size:.9rem}
.manual blockquote p{margin:0}
.manual hr{border:0;border-top:2px solid var(--accentbg);margin:1.6rem 0}
.manual li{margin:.25rem 0}
.manual em{color:var(--ink)}
.manual pre.cmd{margin:.6rem 0}
/* bridge */ /* bridge */
.strip{display:flex;gap:.45rem;flex-wrap:wrap;margin:.8rem 0} .strip{display:flex;gap:.45rem;flex-wrap:wrap;margin:.8rem 0}
.chip{border:1px solid var(--line);background:#fff;border-radius:8px; .chip{border:1px solid var(--line);background:#fff;border-radius:8px;

48
src/pacta/walletui.py
View file

@ -57,6 +57,7 @@ from typing import Any, Callable
from .attestation import load_attestation from .attestation import load_attestation
from .deck import render_deck from .deck import render_deck
from .liveness import collect_liveness, render_liveness from .liveness import collect_liveness, render_liveness
from .mdlite import render as render_markdown
from .stations import STATION_BY_ID, STATIONS, render_bridge, render_station from .stations import STATION_BY_ID, STATIONS, render_bridge, render_station
from .transparency import load_receipt, verify_receipt from .transparency import load_receipt, verify_receipt
from .uikit import (STYLE, esc as _esc, explain as _explain, from .uikit import (STYLE, esc as _esc, explain as _explain,
@ -184,6 +185,7 @@ _INSTRUMENT_TABS = [
("/inspect", "Inspect", "check a receipt yourself"), ("/inspect", "Inspect", "check a receipt yourself"),
("/estate", "Estate map", "the territory, drawn"), ("/estate", "Estate map", "the territory, drawn"),
("/guide", "Guide", "every term, explained"), ("/guide", "Guide", "every term, explained"),
("/manual", "Lab manual", "the full course, chair by chair"),
] ]
_LEADS: dict[str, str] = { _LEADS: dict[str, str] = {
@ -212,8 +214,14 @@ _LEADS: dict[str, str] = {
'own verifier on them, on your machine, without writing anything to the ' 'own verifier on them, on your machine, without writing anything to the '
'wallet. Use it to check evidence somebody handed you before trusting it.'), 'wallet. Use it to check evidence somebody handed you before trusting it.'),
"/guide": ('Plain-language explanations for everything this cockpit shows. Nothing on ' "/guide": ('Plain-language explanations for everything this cockpit shows. Nothing on '
'this page is live data — this is the manual. The Bridge and the stations ' 'this page is live data — this is the reference. The Bridge and the stations '
'are the working surfaces; the instruments are the shared evidence.'), 'are the working surfaces; the instruments are the shared evidence. For the '
'full course, open the <a href="/manual">Lab manual</a>.'),
"/manual": ('The full course: put this page on one monitor and the '
'<a href="/deck">deck</a> on the other, then work it like a lab — session '
'by session, chair by chair, from Newcomer to graduation. The table of '
'contents below is your syllabus; your place is wherever your last '
'checkpoint passed.'),
} }
for _s in STATIONS: for _s in STATIONS:
_LEADS[f"/station/{_s['id']}"] = _s["lead"] _LEADS[f"/station/{_s['id']}"] = _s["lead"]
@ -698,7 +706,39 @@ def _render_drift_panel() -> str:
# --------------------------------------------------------------------------- # ---------------------------------------------------------------------------
# guide instrument - the manual # lab manual instrument - the course, rendered from its canonical Markdown
# ---------------------------------------------------------------------------
def render_manual() -> str:
"""The lab manual: docs/warden-lab-manual.md rendered with a syllabus.
The Markdown file in the repository is canonical (readable on the
mirror, diffable, committed); this route renders it so the course can
sit on one monitor while the deck flies on the other."""
def read() -> str:
path = Path(__file__).resolve().parents[2] / "docs" / "warden-lab-manual.md"
return path.read_text(encoding="utf-8")
coll = collect("docs/warden-lab-manual.md (canonical file, rendered live)", read)
if not coll["ok"]:
return _failed_panel("Lab manual", coll["via"], coll["error"])
body, toc = render_markdown(coll["data"])
toc_items = "".join(
f'<li class="toc{level}"><a href="#{anchor}">{_esc(text)}</a></li>'
for level, text, anchor in toc if level == 2)
return (
"<div class='panel toc'><h2 style='margin-top:0'>Syllabus</h2>"
f"<ol>{toc_items}</ol>"
"<p class='muted'>Sessions build on each other; the capstone assumes "
"all six chairs. Answers to every self-test are in Appendix B — "
"attempt first, then check. Marks: ▶ do · ✔ checkpoint · ✎ write · "
"⌂ optional.</p></div>"
f"<div class='manual'>{body}</div>"
f"{_provenance(coll['via'])}"
)
# ---------------------------------------------------------------------------
# guide instrument - the reference
# --------------------------------------------------------------------------- # ---------------------------------------------------------------------------
def render_guide() -> str: def render_guide() -> str:
@ -1027,6 +1067,8 @@ def make_handler(wallet_dir: Path):
note + render_inspect(None, defaults)) note + render_inspect(None, defaults))
elif route == "/guide": elif route == "/guide":
page("guide", "/guide", render_guide()) page("guide", "/guide", render_guide())
elif route == "/manual":
page("lab manual", "/manual", render_manual())
elif route == "/estate": elif route == "/estate":
from .estateview import ESTATE_HTML from .estateview import ESTATE_HTML
self._send(ESTATE_HTML + _ESTATE_BACK_CHIP) self._send(ESTATE_HTML + _ESTATE_BACK_CHIP)

40
tests/test_walletui.py
View file

@ -179,7 +179,7 @@ def test_server_routes_and_read_only_guarantee(tmp_path):
thread.start() thread.start()
try: try:
routes = ("/", "/posture", "/queue", "/incidents", "/inspect", "/guide", routes = ("/", "/posture", "/queue", "/incidents", "/inspect", "/guide",
"/deck", "/station/proposer", "/station/quorum", "/manual", "/deck", "/station/proposer", "/station/quorum",
"/station/operator", "/station/operator?probe=1", "/station/operator", "/station/operator?probe=1",
"/station/operator?pane=1", "/station/cryptographer", "/station/operator?pane=1", "/station/cryptographer",
"/station/architect", "/station/newcomer") "/station/architect", "/station/newcomer")
@ -466,6 +466,44 @@ def test_inspect_sample_prefill(tmp_path):
thread.join(timeout=5) thread.join(timeout=5)
def test_manual_is_a_complete_course(tmp_path):
"""The lab manual: a full study-club course — every role gets a session,
every session has a lab with checkpoints and a self-test, the capstone
crosses all chairs, and the answers exist."""
wallet = _seal_wallet(tmp_path)
server, thread, port = _serve(wallet.dir)
try:
status, body = _get(port, "/manual")
assert status == 200
assert "Syllabus" in body # the TOC
for session in ("the world you are entering", "the Newcomer",
"the Proposer", "the Quorum bench", "the Operator",
"the Cryptographer", "the Architect",
"Capstone: the incident day", "Graduation"):
assert session in body, f"manual lost session: {session}"
assert body.count("Checkpoint") >= 8, "labs lost their checkpoints"
assert body.count("Self-test") >= 6, "sessions lost their self-tests"
assert "Appendix B" in body and "self-test answers" in body.lower()
assert "tamper drill" in body.lower() # the hands-on heart of Session 4
assert "Recap card" in body
finally:
server.shutdown()
thread.join(timeout=5)
def test_manual_markdown_renders_cleanly(tmp_path):
"""mdlite over the real manual: no raw Markdown artifacts may leak."""
from pacta.mdlite import render as render_markdown
md = (Path("docs") / "warden-lab-manual.md").read_text(encoding="utf-8")
html_out, toc = render_markdown(md)
for artifact in ("```", "](", "\n## ", "> ✔"):
assert artifact not in html_out, f"raw markdown leaked: {artifact!r}"
assert html_out.count("**") == 0, "unrendered bold markers leaked"
assert len(toc) >= 10 # sessions + appendices reach the syllabus
assert "<pre class='cmd'>" in html_out # command blocks rendered
assert "<blockquote>" in html_out # checkpoints rendered
def test_operator_probe_is_explicit_and_live(tmp_path): def test_operator_probe_is_explicit_and_live(tmp_path):
"""The liveness board never phones home on an ordinary page load; probes """The liveness board never phones home on an ordinary page load; probes
run only on the operator's explicit demand, then show per-target rows.""" run only on the operator's explicit demand, then show per-target rows."""