mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-04 20:03:40 +00:00
mrwulf
19d25458e8
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>
|
||
|---|---|---|
| .. | ||
| 00_course_map.ipynb | ||
| 01_threat_model_and_truth_boundary.ipynb | ||
| 02_claim_cards_and_risk_model.ipynb | ||
| 03_lean_replay_and_axiom_audit.ipynb | ||
| 04_proof_hygiene_and_boundaries.ipynb | ||
| 05_third_party_attestation_provider.ipynb | ||
| 06_merkle_transparency_logs.ipynb | ||
| 06a_provider_build_the_log.ipynb | ||
| 06b_agent_verify_inclusion.ipynb | ||
| 07_agent_consequences.ipynb | ||
| 08_capstone_research_program.ipynb | ||
| 09_dogfood_verified_crypto.ipynb | ||
| README.md | ||
PACTA Curriculum Notebooks
This directory contains a zero-to-hero teaching sequence for proof-aware cryptographic tooling.
Start with 00_course_map.ipynb, then proceed in order. The notebooks are intentionally output-free in git. Run them from the repository root or from this directory; each notebook locates the repo root and imports pacta from src/.
The course teaches:
- theorem-boundary thinking,
- claim cards and residual risk,
- Lean replay and axiom audit concepts,
- proof hygiene,
- third-party proof-check provider trust,
- RFC 9162-style Merkle transparency logs,
- receipt-gated agent consequences (including the R4 wallet gate, now reachable),
- split-view defense: STH pinning, consistency enforcement, freshness, monitoring,
- dogfood verified cryptography and the honest hybrid post-quantum posture,
- research roadmaps from R4 evidence toward R5 assurance.
This curriculum is not financial advice, not a trading bot, and not a wallet-building guide. It is a training path for engineers and researchers who need to evaluate formal-verification-enhanced cryptographic tooling without overclaiming.