Audit: are the zero-to-hero notebooks current and macOS-runnable, and
does the README present the new teaching surfaces and CLI well?
Verified by execution: all 14 notebooks run headlessly cell-by-cell,
offline, pure-Python (zero shell magics), degrading gracefully where
Lean/built binaries are absent — before AND after these edits. That is
also the macOS answer: no GNU userland is touched by any cell.
Gaps found and closed:
- README's notebook list stopped at 10; notebook 11 (the customer's
eye view) now listed.
- No notebook knew the cockpit era existed. Three pointer cells added:
00 (course map: the three-track teaching stack — notebooks = code
track, lab manual = role track, guide = reference), 10 (see the
wallet you built through the cockpit; --demo and --wallet forms),
11 (the Inspect instrument is this notebook's recomputation, живой).
- README: cockpit command block now shows --demo, --wallet, --port/
--host variants; curriculum section names the teaching stack and the
notebooks' offline/runnable contract.
Suite 144 green.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The trust architecture has exactly two roles and the curriculum now
mirrors that split structurally - the conceptual burden is the design,
stated as such to the student:
- 06a THE PROVIDER'S SIDE (singleton). Domain banner in the provider's
voice. The full build pipeline run live in a scratch log made from
the REAL attestations: verify (Lean replay = the leaf-making step,
the only expensive one - the shipped evidence IS its output) -> leaf
(0x00 domain separation) -> tree -> STH signed via the MERKLEIZED
LIBRARY -> the self-inclusion check embedded in the signature block.
A generated SVG draws the student's own tree: leaves, internal
nodes, root, and the signature box, framed in the provider's domain
color. Closes with the singleton-vs-many justification table
(key/cost/obligation asymmetry) and exercises.
- 06b THE AGENT'S SIDE (one of many). Domain banner in the agent's
voice: you own the public key, the evidence files, ~25 lines of
hashing - and explicitly NO Lean. The COMPLETE RFC 9162 inclusion
verifier is implemented from scratch in one cell (hashlib only, no
pacta imports for the core) and run against the REAL dalek receipt
(leaf 4 of 8, three siblings, dogfood-signed root); then the STH
signature, the provider's signing_provenance read and interpreted
(why the agent still re-checks inclusion itself), the pin store, and
an SVG of the real log with the agent's path highlighted against the
grey leaves it never needs. Cost line: ~4 hashes + 1 signature.
- Lecture 06 now routes students into the pair and states the mirror
rule ("if you cannot say which notebook a step belongs to, you have
not understood the step"); lecture 09 records that dogfood now runs
in BOTH directions; course map + README updated.
Every cell of 06a/06b/09 executed against the real evidence before
commit (SVGs render in Jupyter, fail soft in plain exec). One
generation bug found and fixed: a single-backslash \\x00 in the
generator produced a literal NUL byte in a cell. 50/50 tests green
with the notebook inventory at twelve.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The notebooks now carry the same didactic contract as the companion book
(the "ratchet rule", stated in the course map): every load-bearing idea
runs twice - napkin scale, then real scale - and every pair is EXECUTABLE
in the notebook, not narrated.
- Lecture 1: the truth boundary updated to the proven four-tier apex,
with the what-is-still-NOT-proven list (SHA-512, parsers, signing,
wallets) given equal weight.
- Lecture 2: napkin/real scoring pair - a two-certificate toy card
scored in your head, then the shipped sixteen-certificate R4 fixture
through the same function, residual blockers and per-tier boundary
axioms printed.
- Lecture 6: new split-view section. A runnable equivocation drill:
pin a two-leaf view, grow it honestly with a consistency proof, then
present a forged same-size root and watch the pin store name the
attack. Real-scale pointers to --sth-store, log-consistency,
log-audit, and the freshness policy; a new exercise asks students to
construct the lie a size-only anchor check would miss.
- Lecture 7: the wallet gate now swings BOTH ways on real evidence -
a partial card denied at R3, the shipped R4 card allowed - both
runnable.
- Lecture 8 capstone: "design R4" became "audit R4": read the shipped
card like an auditor, then design the R5 discharge plan (parser
specs, verified SHA-512, signing-side, per-fork production-path
mapping).
- NEW Lecture 9, "Eat Your Own Dogfood": the honest coverage ledger of
the proven-path verifier; a napkin PEM decode (the fixed 12-byte
Ed25519 SPKI prefix, read with your eyes) paired with the mechanical
extraction; live backend dispatch; the fail-closed
--require-verified-verifier policy; and the hybrid-PQC section -
proven-classical Ed25519 plus a required-but-honest ML-DSA slot
("blockers get fixed; placeholders get trusted").
Every code cell of the changed notebooks was executed end-to-end before
committing (outputs stripped per house rules). 49/49 tests green with
the notebook inventory updated.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
