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-04 20:03:40 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
proof-aware-crypto-tooling-.../scripts/build_curriculum_notebooks.py
mrwulf 65772b3d2e warden hardening round: policy engine, ledger rotation, MCP UX, treasury LIVE, ops docs 
Tier 2:
- request_signature decomposed into named gates (latch, freshness,
  intent, policy, signer, firewall)
- ledger: O(1) tail-read appends under a dedicated lock file (survives
  rotation rename); hash-chained segment rotation at policy
  ledger.rotate_at; verify-ledger walks all segments to genesis;
  archive tampering detected (tested)
- docs/threat-model.md (attacker matrix 1-9, proven-vs-trusted, design
  invariants) + docs/runbook-latch.md (diagnose-first recovery)
- lecture 10: executable corrupt-a-member exercise (capsule pin catches
  one appended byte), honest note on what the pin does NOT stop

Lightweight policy engine (POLICY_DENIED wired):
- policy.json: per-request/per-day amount ceilings, counterparty
  allow/deny lists, per-identity overrides; rules make their intent
  fields mandatory; daily sums from the ledger
-

Agent UX:
- signed refusal receipts travel inside MCP errors (receipt +
  receipt_path in structuredContent)
- airgap over MCP: request_signature signer=airgap + request_id,
  new airgap_pending tool; park -> list -> device answers -> complete
  (tested end-to-end)
- all 8 tools carry readOnly/destructive annotations
- sliding-window rate limiter per tool class (custody/verify/liveness);
  RATE_LIMITED refusal code; surface control, not ledgered

warden-treasury LIVE:
- treasury.py: stdlib base58, compact-u16, legacy+v0 wire parsing;
  every required signature quorum-verified over exact message bytes;
  completeness gap named in every verdict; RPC fetch uses response as
  bytes only
-
- live-quorum test: synthetic Solana tx signed with wallet key ->
  authentic via 4 proven forks; flipped byte -> not authentic

100 tests green (was 85).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-07 13:38:42 +02:00

2352 lines
116 KiB
Python
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

from __future__ import annotations
import json
from pathlib import Path
from textwrap import dedent
ROOT = Path(__file__).resolve().parents[1]
NOTEBOOK_DIR = ROOT / "notebooks"
def md(source: str) -> dict:
return {
"cell_type": "markdown",
"metadata": {},
"source": _lines(source),
}
def code(source: str) -> dict:
return {
"cell_type": "code",
"execution_count": None,
"metadata": {},
"outputs": [],
"source": _lines(source),
}
def _lines(text: str) -> list[str]:
stripped = dedent(text).strip("\n")
if not stripped:
return []
return [line + "\n" for line in stripped.splitlines()]
def notebook(cells: list[dict]) -> dict:
return {
"cells": cells,
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3",
},
"language_info": {
"name": "python",
"pygments_lexer": "ipython3",
},
},
"nbformat": 4,
"nbformat_minor": 5,
}
COURSE = {
"00_course_map.ipynb": notebook(
[
md(
"""
# PACTA Curriculum: From Zero to Hero
This curriculum teaches proof-aware cryptographic tooling from first principles to a research-grade professional workflow. It is designed for undergraduate students who know some programming and discrete math, but have not yet worked with formal verification, Lean, certificate transparency, or autonomous-agent risk gates.
The practical anchor is PACTA: Proof-Aware Crypto Tooling Agent. The goal is not to build a trading bot. The goal is to teach an agent, and the engineer supervising it, to ask:
> Does this theorem cover the exact code path that will protect funds?
The course takes that question seriously. Every notebook connects theory to a runnable artifact in this repository.
"""
),
md(
"""
## Learning Objectives
By the end of the sequence, a strong student should be able to:
- Explain why cryptographic implementation proofs have theorem boundaries.
- Distinguish formal proof evidence from tests, audits, marketing claims, and operational controls.
- Read a PACTA claim card and understand its guarantees, preconditions, exclusions, trusted base, and risk level.
- Reproduce a local Lean replay or diagnose why local replay is unavailable.
- Perform a proof hygiene scan and explain why `sorry`, local axioms, and trivial theorem targets are dangerous.
- Explain how a third-party proof-checking provider changes the trusted base.
- Implement and verify RFC 9162-style Merkle inclusion and consistency proofs.
- Explain why Signed Tree Heads need accountable signatures, why Ed25519 is useful here, and why ML-DSA requires a real backend.
- Design policy gates that convert verification evidence into consequences.
- Read R4 four-tier apex evidence, name its residual blockers, and write a research plan toward R5 production assurance.
"""
),
md(
"""
## Prerequisites
Recommended background:
- Python basics: functions, dictionaries, lists, files, subprocesses.
- Discrete math: modular arithmetic, induction, trees, hashes.
- Basic cryptography vocabulary: public keys, signatures, hashes, finite fields.
- Basic command-line usage on macOS or Linux.
Not required at the start:
- Lean.
- Rust internals.
- Elliptic curve implementation expertise.
- Certificate transparency expertise.
"""
),
code(
"""
from pathlib import Path
import sys
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
print(repo_root)
print((repo_root / "README.md").exists())
"""
),
md(
"""
## Course Map
1. `01_threat_model_and_truth_boundary.ipynb`
Learn the product problem, the security boundary, and the difference between verified arithmetic and verified wallets.
2. `02_claim_cards_and_risk_model.ipynb`
Study PACTA claim cards, risk levels R0-R5, and how claim serialization supports machine decisions.
3. `03_lean_replay_and_axiom_audit.ipynb`
Learn how local Lean replay works, why PACTA avoids transpilation, and what an axiom audit proves.
4. `04_proof_hygiene_and_boundaries.ipynb`
Learn to scan proof artifacts for `sorry`, local `axiom`, trivial theorem statements, and missing manifest coverage.
5. `05_third_party_attestation_provider.ipynb`
Learn how a proof-checking service can transform hard local verification into provider trust.
6. `06_merkle_transparency_logs.ipynb`, then the MIRRORED PAIR
`06a_provider_build_the_log.ipynb` / `06b_agent_verify_inclusion.ipynb`
The trust architecture has exactly two domains - ONE provider
who builds and signs the authenticated structure (and pays the
Lean bill), MANY agents who verify inclusion proofs in
milliseconds. The course mirrors that split structurally: 6a is
written entirely in the provider's voice, 6b entirely in the
agent's. If you cannot say which notebook a step belongs to,
you have not understood the step.
Build the Merkle accumulator intuition behind inclusion proofs, consistency proofs, and Signed Tree Heads.
7. `07_agent_consequences.ipynb`
Connect evidence to action: build a lower-layer Rust capsule only when policy gates pass.
8. `08_capstone_research_program.ipynb`
Design a PhD-level roadmap for closing the gaps from R4 toward R5.
9. `09_dogfood_verified_crypto.ipynb`
Eat your own dogfood: run the agent's own signature checks through the proven code path, and hold the post-quantum line honestly.
## The Ratchet Rule
This course follows the same didactic contract as its companion book (*Verifying Cryptography with Lean 4*): **every load-bearing idea is worked at least twice** - once at napkin scale (trees of three leaves, toy claim cards you can score in your head) and once at real scale (the shipped R4 claim cards, real receipts, the real proven-path verifier), with nothing hidden in between. The napkin run teaches the moves; the real-size run proves the moves are the whole story. If a step ever feels like a leap, back up one cell: the smaller rung is there.
"""
),
md(
"""
## Assessment Model
Each notebook contains:
- A lecture section for concepts.
- A lab section with runnable code.
- Checkpoints that force precise answers.
- Exercises for mastery.
- Research prompts for advanced students.
The capstone asks students to produce a defensible assurance case, not a slogan.
"""
),
md(
"""
## References
- RFC 9162, Certificate Transparency Version 2.0: https://datatracker.ietf.org/doc/html/rfc9162
- RFC 8032, Edwards-Curve Digital Signature Algorithm: https://datatracker.ietf.org/doc/html/rfc8032
- NIST FIPS 204, Module-Lattice-Based Digital Signature Standard: https://csrc.nist.gov/pubs/fips/204/final
- PACTA README: `../README.md`
"""
),
]
),
"01_threat_model_and_truth_boundary.ipynb": notebook(
[
md(
"""
# Lecture 1: Threat Model and Truth Boundary
The motivating system is an autonomous economic agent that may move stablecoins. It faces two broad attack classes:
1. Psychological or game-theoretic attacks that trick the agent into harmful financial actions.
2. Implementation attacks against the cryptographic and tooling stack that protects keys, signatures, proofs, and policy gates.
PACTA focuses on the second class. It does not decide trades, call RPC endpoints, manage custody, or build wallets. It evaluates formal-verification-enhanced tooling and decides whether a constrained component can be used in a funds-protecting path.
"""
),
md(
"""
## Learning Objectives
- Define a threat model for proof-aware cryptographic tooling.
- Explain why lower-layer arithmetic proofs do not imply wallet safety.
- State the strongest current Ed25519-family claim in theorem-boundary language.
- List common exclusions that remain outside the proof artifact.
- Explain why an autonomous agent needs consequences, not just reports.
"""
),
md(
"""
## The Core Truth Boundary
The strongest current Ed25519-family claim in this project is approximately:
For selected curve25519-dalek / Solana-Ed25519-family Rust code paths already transpiled into Lean, the verified repositories contain Lean-checked certificates for field arithmetic over `F_p`, `p = 2^255 - 19`, and complete twisted Edwards point-operation laws, under explicit invariants and backend constraints.
That is valuable. And since 2026-07-06 the corpus goes much further: all four ed25519 repositories carry a FOUR-TIER signature apex, button-enforced per fork, up to the full lift - the extracted verifier accepts iff the signature's R decompresses to a valid on-curve point equal to [k](-A)+[s]B. What it is still NOT: a wallet proof, a proof of SHA-512, a proof of the wire parsers (their outcomes are hypotheses), a signing-side proof, or a proof of all Solana transaction behavior. Naming both lists - what is proven and what is not - is the entire discipline of this course.
"""
),
md(
"""
## Proven or High-Value Evidence
A clean R3-style Ed25519 arithmetic result may cover:
- FieldElement51 arithmetic over `F_p` through denotation.
- Panic and overflow freedom under limb-bound preconditions.
- Complete Edwards point operations under `ExtValid` and `OnCurveExt`.
- Implementation laws through denotation.
- Axiom audit expected to show only standard Lean axioms: `propext`, `Classical.choice`, `Quot.sound`.
The exact theorem names matter. In the current target repos, important certificates include:
- `CurveFieldProofs.fieldImplementation`
- `CurveFieldProofs.edwardsImplementation`
"""
),
md(
"""
## Explicit Exclusions
Do not let a lower-layer theorem leak into claims about:
- Full EdDSA signature verification.
- Complete Scalar52 arithmetic unless separately proven.
- SHA-512.
- Encoding, decoding, and canonicality unless separately proven.
- Rust compiler correctness.
- Charon/Aeneas translation faithfulness.
- Side-channel resistance.
- SIMD, AVX, hardware, zkVM, accelerator, or syscall paths.
- Wallet policy, transaction construction, RPC, chain, oracle, market, or LLM decision safety.
A professional assurance case is often mostly about preventing evidence from being overextended.
"""
),
code(
"""
from pathlib import Path
import sys
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
from pacta.config import load_config
config = load_config(repo_root / "examples" / "repos.yaml")
for repo in config.repos:
print(f"{repo.name:32} kind={repo.kind:13} backend={repo.verified_backend}")
if repo.backend_warning:
print(f" backend warning: {repo.backend_warning}")
if repo.known_status:
print(f" known status: {repo.known_status}")
"""
),
md(
"""
## Consequences
PACTA turns evaluation into operational consequences:
- If evidence is R0/R1/R2, do not build or consume lower-layer crypto capsules.
- If evidence is R3, a constrained lower-layer component capsule may be built.
- If evidence is below R4, wallet demo construction is refused.
- If a third-party attestation is required but not trusted, the score falls to R0.
- If a transparency receipt is required but invalid or absent, the score falls to R0.
This makes verification a gate, not a decorative badge.
"""
),
md(
"""
## Checkpoint Questions
1. Why does a proof of field arithmetic not prove transaction construction?
2. What would have to be proven before full EdDSA verification could plausibly reach R4?
3. Why is "the proof failed to replay locally" different from "the theorem is false"?
4. Why should a zkVM accelerator path be excluded unless the repo proves otherwise?
"""
),
md(
"""
## Exercises
- Pick one configured repository from `examples/repos.yaml`. Write three precise claims that PACTA may make about it and three claims PACTA must refuse.
- Rewrite the sentence "this is verified Ed25519" into a theorem-boundary statement that a security reviewer would accept.
- Create a table mapping each exclusion above to the attack class it leaves open.
"""
),
]
),
"02_claim_cards_and_risk_model.ipynb": notebook(
[
md(
"""
# Lecture 2: Claim Cards and the R0-R5 Risk Model
A claim card is a machine-readable assurance artifact. It records what was checked, what theorem names were involved, what axioms were observed, what exclusions remain, what trusted base is assumed, and what risk score follows.
A claim card is not a marketing page. It is a structured input to policy.
"""
),
md(
"""
## Learning Objectives
- Read the claim card schema.
- Explain risk levels R0 through R5.
- Generate an offline fixture claim card.
- Understand why R3 can authorize lower-layer library use but not wallet construction.
- Identify blockers and deployment constraints in a claim card.
"""
),
md(
"""
## Risk Levels
- `R0`: Unknown or untrusted. No usable evidence.
- `R1`: Tests, audits, or informal claims only.
- `R2`: Formal model exists, but incomplete, weakly tied to production code, or major proof gaps remain.
- `R3`: A specific lower-layer implementation artifact is Lean-checked for a specific backend and theorem boundary.
- `R4`: End-to-end primitive proof covers public API, parsing/encoding, scalar arithmetic, hashing interface, signature equation, rejection rules, and implementation boundary.
- `R5`: R4 plus reproducible production builds, compiler/build assurance, side-channel analysis, hardware/KMS/MPC integration, and operational controls.
Ed25519 field plus Edwards arithmetic alone reaches R3. Since the corpus completed its four-tier signature apex (2026-07-06), the FULL configured certificate set - arithmetic, scalars, encoding/decoding, and the four apex tiers, each with its axiom cone pinned to the fork's documented boundary - reaches **R4**, always with explicit residual blockers (the SHA-512 oracle, hypothesis-parametric wire parses, translation faithfulness, and the missing side-channel/build assurance that gates R5).
"""
),
code(
"""
from pathlib import Path
import sys
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
from pacta.claims import build_claim_card
from pacta.config import load_config
config = load_config(repo_root / "examples" / "repos.yaml")
repo = config.repo_named("dalek-ed25519-verified")
card = build_claim_card(repo, repo_root / "repos" / repo.name, offline_fixture=True)
print(card["component"])
print(card["risk"]["level"])
print(card["risk"]["rationale"])
print(card["certificates"][0])
"""
),
code(
"""
important_fields = [
"component",
"repo_url",
"repo_commit",
"verification_dir",
"kind",
"verified_backend",
"certificates",
"guarantees",
"preconditions",
"exclusions",
"trusted_base",
"evidence",
"risk",
]
for field in important_fields:
print(field, "=>", type(card.get(field)).__name__)
"""
),
md(
"""
## Reading a Certificate Entry
A certificate entry contains:
- `name`: theorem or aggregate certificate name.
- `status`: `proven`, `missing`, `failed`, or `unknown`.
- `axiom_status`: `clean`, `dirty`, or `not_checked`.
- `observed_axioms`: axioms reported by Lean.
- `expected_axioms`: allowed standard axioms for this profile.
A clean result requires more than a theorem name. It requires a successful replay or trusted attestation, the RIGHT axiom set per certificate (standard-three below the apex, the fork's documented boundary at the apex tiers - deviation in either direction is dirty), and no policy-blocking exclusions.
### The ratchet, run both ways
First the napkin: a two-certificate card you can score in your head. Then the real thing: the shipped R4 fixture with sixteen certificates and per-tier boundary axioms.
"""
),
code(
"""
# NAPKIN: an arithmetic-only card. Two certificates, standard axioms.
from pacta.risk import score_claim_card
napkin_card = {
"kind": "ed25519",
"certificates": [
{"name": "CurveFieldProofs.fieldImplementation", "status": "proven", "axiom_status": "clean"},
{"name": "CurveFieldProofs.edwardsImplementation", "status": "proven", "axiom_status": "clean"},
],
"exclusions": ["full EdDSA signature verification"],
"meta": {"r4_requirements": []},
}
napkin = score_claim_card(napkin_card)
print(napkin.level, "-", napkin.rationale)
"""
),
code(
"""
# REAL: the shipped R4 fixture - sixteen certificates, apex tiers carrying
# the dalek fork's documented boundary axioms. Same scoring function.
from pacta.yamlio import load_data
real_card = load_data(repo_root / "examples" / "dalek-ed25519.claims.yaml")
real = score_claim_card(real_card)
print(real.level)
print(real.rationale[:180], "...")
print("residual blockers:")
for blocker in real.blockers:
print(" -", blocker)
apex = [c for c in real_card["certificates"] if c["name"].endswith("_decompress")][0]
print("full-lift tier expects:", apex["expected_axioms"])
"""
),
code(
"""
for cert in card["certificates"]:
print(f"{cert['name']}: {cert['status']} / {cert['axiom_status']}")
print(" observed:", cert["observed_axioms"])
print(" expected:", cert["expected_axioms"])
"""
),
md(
"""
## Deployment Constraints
Deployment constraints are where many assurance cases become honest. For Ed25519 arithmetic, constraints include:
- Use exact pinned source or reviewed diff.
- Use verified serial/u64 backend only.
- Disable accelerator/syscall/hardware/SIMD paths unless separately certified.
- Do not treat this as full EdDSA verification.
- Keep key custody behind HSM/MPC/policy firewall until signing stack proof coverage improves.
- Use ordinary tests/fuzzing at encoding/API/transaction boundaries.
"""
),
code(
"""
for constraint in card["risk"]["deployment_constraints"]:
print("-", constraint)
"""
),
md(
"""
## Exercises
- Change the generated card in memory so one certificate is `missing`. Rescore it and explain the change.
- Write a short policy that allows `build-library` at R3 but denies `build-wallet-demo` below R4.
- Compare the trusted base for local replay versus third-party attestation.
"""
),
code(
"""
from copy import deepcopy
from pacta.risk import score_claim_card
weaker = deepcopy(card)
weaker["certificates"][0]["status"] = "missing"
weaker["certificates"][0]["axiom_status"] = "not_checked"
assessment = score_claim_card(weaker)
print(assessment.level)
print(assessment.rationale)
print(assessment.blockers)
"""
),
]
),
"03_lean_replay_and_axiom_audit.ipynb": notebook(
[
md(
"""
# Lecture 3: Lean Replay and Axiom Audit
The verified repositories already contain Lean artifacts. PACTA does not run Charon, Aeneas, extraction, or Rust-to-Lean regeneration. It treats shipped Lean files as the verification artifact and focuses on replaying and inspecting them.
"""
),
md(
"""
## Learning Objectives
- Explain the difference between transpilation and proof replay.
- Understand how PACTA discovers Lean files and manifests.
- Build a portable Lean invocation without Linux-only shell helpers.
- Explain `#print axioms` and why axiom sets matter.
- Diagnose missing Lean/lake or missing pinned Aeneas environments.
"""
),
md(
"""
## Why Not Run Charon/Aeneas?
The corpus policy is strict:
- The transpilation work is finished in the verified repos.
- Re-running extraction could create a different artifact and confuse the trust story.
- The current task is to interpret, replay, summarize, and score the existing Lean proof artifacts.
For a production assurance case, translation faithfulness remains part of the trusted base unless separately proven.
"""
),
code(
"""
from pathlib import Path
import sys
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
from pacta.manifest import discover_layout
fixture = repo_root / "tests" / "fixtures" / "mini-ed25519-verified"
layout = discover_layout(fixture, "verification")
print("verification_dir:", layout.verification_dir)
print("files:")
for path in layout.compile_order:
print(" ", path.relative_to(fixture))
print("warnings:", layout.warnings)
"""
),
md(
"""
## Portable Lean Invocation
PACTA avoids repository `check.sh` scripts because those may assume Linux-only tools like `free`, `taskset`, or GNU `timeout`. Instead it uses Python `subprocess.run(..., timeout=...)` and constructs a Lean environment where `verification/gen` and `verification` are visible through `LEAN_PATH`.
If a pinned Aeneas Lean project is needed, PACTA can source a configured environment script and run `lake env lean`. It still does not run extraction.
"""
),
code(
"""
from pacta.lean import LeanTools, build_lean_invocation
tools = LeanTools(lean="/usr/bin/lean", lake="/usr/bin/lake")
example_file = layout.compile_order[0]
print(build_lean_invocation(example_file, tools, use_lake_env=True, output_path=example_file.with_suffix(".olean")))
"""
),
md(
"""
## Axiom Audit
A theorem can compile while depending on unexpected axioms. For the Ed25519 arithmetic profiles, the expected axiom set is usually:
- `propext`
- `Classical.choice`
- `Quot.sound`
PACTA generates a temporary Lean file with imports such as:
```lean
import Proofs.FieldMain
import Proofs.EdMain
#print axioms CurveFieldProofs.fieldImplementation
#print axioms CurveFieldProofs.edwardsImplementation
```
It then parses Lean output and marks the result clean only when observed axioms match the expected set.
"""
),
code(
"""
from pacta.lean import parse_axiom_output
output = \"\"\"'CurveFieldProofs.fieldImplementation' depends on axioms:
[propext, Classical.choice, Quot.sound]
'CurveFieldProofs.edwardsImplementation' depends on axioms:
[propext, Classical.choice, Quot.sound]
\"\"\"
parsed = parse_axiom_output(
output,
[
"CurveFieldProofs.fieldImplementation",
"CurveFieldProofs.edwardsImplementation",
],
)
print(parsed)
"""
),
md(
"""
## Local Replay Failure Modes
Important distinctions:
- Missing `lean`: local verifier capability unavailable.
- Missing `lake`: local project environment may be unavailable.
- Missing Aeneas Lean project: local replay unavailable for repos that depend on it.
- Lean file fails: proof replay failed in this environment.
- Axiom set dirty: theorem depends on unexpected assumptions.
These are not the same. A professional report must state which one happened.
"""
),
md(
"""
## Exercises
- Run `pacta doctor --config examples/repos.yaml --repo-name dalek-ed25519-verified` and classify the result.
- Create a fake axiom output with an extra axiom. Parse it and explain why the result should be dirty.
- Explain why a replay runner should not silently fall back from failure to an offline fixture.
"""
),
]
),
"04_proof_hygiene_and_boundaries.ipynb": notebook(
[
md(
"""
# Lecture 4: Proof Hygiene and Boundaries
Proof hygiene is the discipline of checking whether formal artifacts have obvious escape hatches or misleading theorem surfaces. It does not replace proof checking. It catches common ways a proof corpus can look stronger than it is.
"""
),
md(
"""
## Learning Objectives
- Detect `sorry`, local `axiom`, trivial theorem targets, and suspicious `by trivial`.
- Understand why comments should not be treated as fatal proof failures.
- Explain why manifest coverage matters.
- Distinguish a hygiene warning from a replay failure.
- Write precise boundary language for proof reports.
"""
),
md(
"""
## Patterns PACTA Scans For
- `sorry`
- `axiom` declarations under `Proofs/`
- theorem targets such as `: True :=`
- suspicious `by trivial` in spec/certificate/root files
- `native_decide` as advisory unless dependency-cone analysis is stronger
- missing certificate names
- proof files not included in a manifest when a manifest exists
A simple scanner may over-warn. It must not over-claim.
"""
),
code(
"""
from pathlib import Path
import sys
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
from pacta.audit import scan_hygiene
from pacta.manifest import discover_layout
fixture = repo_root / "tests" / "fixtures" / "mini-ed25519-verified"
layout = discover_layout(fixture, "verification")
issues = scan_hygiene(layout, ["CurveFieldProofs.fieldImplementation"])
print("issues:", issues)
"""
),
md(
"""
## Why `sorry` Is Serious
In Lean, `sorry` can stand in for a proof. Depending on settings, it may allow a theorem to exist without its proof being completed. In a verification-evidence pipeline, unresolved `sorry` must block high-confidence claims.
The lesson is not "never prototype with placeholders." The lesson is "never ship assurance claims that hide placeholders."
"""
),
md(
"""
## Why Local Axioms Are Serious
A local axiom can assert the result directly. For example:
```lean
axiom fieldImplementation : CorrectFieldImplementation
```
That may be useful for bootstrapping a model, but it is not proof evidence for implementation correctness. PACTA flags local axioms under `Proofs/` because they may collapse the intended theorem into an assumption.
"""
),
md(
"""
## Trivial Theorems and Spec Drift
A theorem target like `: True := by trivial` proves exactly nothing about cryptographic code. A more subtle failure is spec drift: the theorem proves a property, but not the property the system needs.
Professional review asks two questions:
1. Is the proof complete?
2. Is the theorem the right theorem?
"""
),
code(
"""
# A tiny reviewer helper: classify theorem statements by obvious risk.
examples = {
"good_shape": "theorem add_denote ... : denote (add x y) = x + y := ...",
"trivial_target": "theorem certificate : True := by trivial",
"placeholder": "theorem hard_part : P := by sorry",
}
for name, text in examples.items():
flags = []
if "sorry" in text:
flags.append("placeholder proof")
if ": True :=" in text:
flags.append("trivial target")
if "by trivial" in text:
flags.append("trivial proof tactic")
print(name, flags or ["needs semantic review"])
"""
),
md(
"""
## Exercises
- Add a temporary Lean file under a scratch fixture with a theorem `: True := by trivial`. Run the scanner and inspect the issue.
- Explain why the same word in a comment should not be fatal by itself.
- Write a one-page checklist for reviewing a new `*-verified` repository before assigning any risk score above R2.
"""
),
]
),
"05_third_party_attestation_provider.ipynb": notebook(
[
md(
"""
# Lecture 5: Third-Party Proof-Checking Attestations
Local proof replay can be operationally cumbersome. A specialized provider can run the Lean/Aeneas environment in a controlled setup and publish a signed attestation. This transforms trust in local compilation into trust in a provider, its environment, its signing key custody, and its transparency log.
"""
),
md(
"""
## Learning Objectives
- Explain the trust transformation from local replay to provider attestation.
- Read a provider attestation.
- Verify an Ed25519 attestation signature.
- Understand why untrusted attestations must score R0.
- Distinguish a provider signature from transparency-log accountability.
"""
),
md(
"""
## Attestation Contents
A useful attestation records:
- provider identity,
- issue time,
- subject component, repo URL, repo commit, verification dir, kind, backend,
- Lean and lake versions,
- check log and axiom log locations,
- certificate names, statuses, observed axioms, expected axioms,
- provider signature metadata.
The agent must verify both content and trust policy. A valid signature from an untrusted provider is not enough.
"""
),
code(
"""
from pathlib import Path
import sys
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
from pacta.attestation import load_attestation
attestation_path = repo_root / "examples" / "dalek-ed25519.attestation.yaml"
raw = load_attestation(attestation_path)
print(raw.keys())
print(raw["provider"])
print(raw["subject"])
print(raw["certificates"][0])
"""
),
md(
"""
## Trust Policy
PACTA requires an explicit `--trust-attestation-provider` value. If the attestation provider does not match, the attestation is rejected.
Real attestations should be signed. The included example fixture is unsigned and requires `--allow-unsigned-attestation`, which is suitable only for demos and tests.
"""
),
code(
"""
from pacta.attestation import validate_attestation
from pacta.config import RepoConfig
repo = RepoConfig(
name="dalek-ed25519-verified",
url="https://github.com/saymrwulf/dalek-ed25519-verified.git",
kind="ed25519",
verified_backend="serial/u64",
certificates=[
"CurveFieldProofs.fieldImplementation",
"CurveFieldProofs.edwardsImplementation",
],
)
trusted = validate_attestation(
raw,
repo,
path=attestation_path,
trusted_provider="example-proof-checker.invalid",
allow_unsigned=True,
)
untrusted = validate_attestation(raw, repo, path=attestation_path)
print("trusted accepted:", trusted.accepted)
print("untrusted accepted:", untrusted.accepted)
print("untrusted diagnostics:", untrusted.diagnostics)
"""
),
md(
"""
## Provider Threat Model
A proof-checking provider can be valuable, but it introduces new risks:
- It may sign an incorrect result.
- Its environment may be stale or compromised.
- Its signing key may be stolen.
- It may equivocate by showing different results to different agents.
- It may lose log history.
This is why transparency logging matters. A signature says "this provider signed this." A transparency receipt says "this signed result is included in an append-only public structure at this tree head."
"""
),
md(
"""
## Real evidence, checked in this cell
Everything above used schema fixtures. The repository now ships REAL provider evidence under `evidence/`: signed attestations from a guarded Lean replay of all four verified repositories (~30 minutes of kernel re-checking per fork), each recording the repo commit, the machine-protection block, and all sixteen certificates with their observed axiom cones. Read one and re-derive its verdicts locally - never trust the provider's own labels:
"""
),
code(
"""
from pacta.attestation import load_attestation, _normalize_certificate
from pacta.config import load_config
from pacta.profiles import get_profile
from pacta.signing import verify_attestation_signature_detailed
config = load_config(repo_root / "examples" / "repos.yaml")
repo = config.repo_named("dalek-ed25519-verified")
profile = get_profile("ed25519", repo)
att = load_attestation(repo_root / "evidence" / "dalek-ed25519.attestation.yaml")
ok, error, backend = verify_attestation_signature_detailed(att, repo_root / "evidence" / "provider.ed25519.pub")
print("signature valid:", ok, "| verified on backend:", backend)
print("subject commit:", att["subject"]["repo_commit"][:12])
print("machine protection:", att["machine_protection"]["lean_guard"].rsplit("/", 2)[-1])
rederived = [_normalize_certificate(cert, profile) for cert in att["certificates"]]
clean = sum(1 for cert in rederived if cert["status"] == "proven" and cert["axiom_status"] == "clean")
print(f"re-derived locally: {clean}/{len(rederived)} proven with boundary-exact cones")
apex = [cert for cert in rederived if cert["name"].endswith("_decompress")][0]
print("full-lift tier observed cone:", apex["observed_axioms"])
"""
),
md(
"""
## Exercises
- Draw the trusted base for local replay and provider attestation. Mark what changes.
- Explain why a provider attestation must include repo commit, not only repo name.
- Design a monitoring rule that would detect if the provider changes the result for the same commit.
"""
),
]
),
"06_merkle_transparency_logs.ipynb": notebook(
[
md(
"""
# Lecture 6: Merkle Transparency Logs
Transparency logs make signed statements auditable. PACTA uses an RFC 9162-style Merkle accumulator over signed proof-check attestations. A provider signs the tree head, and an agent verifies an inclusion proof before acting on the attestation.
"""
),
md(
"""
## Learning Objectives
- Implement leaf and node hashing with domain separation.
- Compute a Merkle root.
- Generate and verify inclusion proofs.
- Generate and verify consistency proofs.
- Explain Signed Tree Heads and signature policy.
- Explain why ML-DSA must fail closed when unavailable.
"""
),
md(
"""
## RFC 9162 Hash Shape
PACTA follows the Certificate Transparency hash structure:
- Empty tree hash: `SHA256("")`
- Leaf hash: `SHA256(0x00 || leaf_input)`
- Node hash: `SHA256(0x01 || left || right)`
The prefix bytes prevent a leaf value from being confused with an internal node value.
"""
),
code(
"""
from pathlib import Path
import sys
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
from pacta.transparency import (
leaf_hash,
node_hash,
merkle_root,
inclusion_proof,
verify_inclusion,
consistency_proof,
verify_consistency,
)
leaves = [f"attestation-{i}".encode() for i in range(1, 6)]
root = merkle_root(leaves)
print(root.hex())
"""
),
code(
"""
for index, leaf in enumerate(leaves):
proof = inclusion_proof(leaves, index)
ok = verify_inclusion(leaf, index, len(leaves), proof, root)
print(index, ok, [node.hex()[:12] for node in proof])
"""
),
md(
"""
## Consistency Proofs
An inclusion proof answers: "Is this leaf in this tree?"
A consistency proof answers: "Is the newer tree an append-only extension of the older tree?"
Both are needed for a monitored transparency system. Inclusion is enough for one agent to bind one attestation to one signed tree head. Consistency lets monitors detect equivocation or tree rewrites across time.
"""
),
code(
"""
old_size = 3
old_root = merkle_root(leaves[:old_size])
new_root = merkle_root(leaves)
proof = consistency_proof(leaves, old_size)
print("old:", old_root.hex())
print("new:", new_root.hex())
print("proof:", [node.hex()[:12] for node in proof])
print("consistent:", verify_consistency(old_size, len(leaves), old_root, new_root, proof))
"""
),
md(
"""
## Signed Tree Heads
A Signed Tree Head records:
- log ID,
- tree size,
- timestamp,
- root hash,
- hash algorithm,
- signatures.
PACTA signs the canonical JSON STH payload with Ed25519 through OpenSSL. It also records an ML-DSA-65 slot. On this host, if no real ML-DSA backend is present, the slot is `unavailable`.
Policy matters:
- `require-signatures ed25519`: verify Ed25519 and allow ML-DSA to be unavailable.
- `require-signatures both`: require Ed25519 and ML-DSA verified. If ML-DSA is unavailable, fail closed.
"""
),
code(
"""
from pacta.postquantum import detect_ml_dsa
capability = detect_ml_dsa()
print(capability.available)
print(capability.backend)
print(capability.reason)
"""
),
md(
"""
## Why Ed25519 and ML-DSA Together?
Ed25519 is useful because it is widely deployed, fast, and directly relevant to the Ed25519 proof corpus. That creates a deliberate "eat your own dogfood" loop: the proof-checking ecosystem signs evidence using a primitive whose implementation family is under formal scrutiny.
ML-DSA adds post-quantum robustness for the accumulator signature layer. But it must be a real signature, not an aspirational label. If a host lacks ML-DSA, the correct result is an explicit blocker.
"""
),
md(
"""
## Two domains, two notebooks - by design
Everything above is the shared VOCABULARY. The system itself has
exactly two roles, and the next two notebooks separate them on
purpose: **6a - the provider** (a singleton: builds every leaf via
Lean replay, builds the tree, signs the root with the merkleized
library, and Merkle-verifies its own signing library's leaf before
signing), and **6b - the agent** (one of many: the provider's
public key, the evidence files, ~25 lines of hashing, and nothing
else - explicitly NO Lean). Keep the mirror in mind as you drill
the primitives below; each drill belongs to one side.
## Split Views: why a receipt is not enough
Everything above verifies ONE receipt against ONE signed tree head. A malicious provider can maintain TWO trees - one shown to you, one shown to the world - and both views verify perfectly in isolation. This is EQUIVOCATION, and the defense is memory: pin every tree head you accept, and demand that every later tree head be CONSISTENT with your pin (same size -> same root; larger size -> a verified consistency proof from your pinned size; smaller size -> rollback, reject forever).
pacta implements this as a local STH pin store. Run the whole attack and its detection, napkin-size:
"""
),
code(
"""
# NAPKIN: pin a 2-leaf view, then let the log grow honestly - and then
# let a SPLIT VIEW present a different root at the pinned size.
import tempfile
from pathlib import Path as _P
from pacta.sthstore import check_sth_against_store
from pacta.transparency import consistency_proof, merkle_root, proof_to_hex
honest = [b"attestation-A", b"attestation-B", b"attestation-C"]
evil = [b"attestation-A", b"attestation-EVIL", b"attestation-C"]
with tempfile.TemporaryDirectory() as tmp:
store = _P(tmp) / "sth-store.json"
sth = lambda size, leaves: {
"log_id": "demo-log", "tree_size": size,
"root_hash": merkle_root(leaves[:size]).hex(),
"timestamp": "2026-07-06T00:00:00Z",
}
print("pin: ", check_sth_against_store(sth(2, honest), store).diagnostics[0])
grown = check_sth_against_store(
sth(3, honest), store,
consistency_proof_hex=proof_to_hex(consistency_proof(honest, 2)),
)
print("grow: ", grown.diagnostics[0])
attack = check_sth_against_store(sth(3, evil), store)
print("attack ok?", attack.ok)
print("verdict: ", attack.diagnostics[0][:120], "...")
"""
),
md(
"""
At real scale the same check runs on every `pacta receipt-verify --sth-store ...` and `pacta agent --sth-store ...` invocation; receipts embed a consistency anchor from the previous tree size, the provider serves proofs from arbitrary pinned sizes (`pacta_provider log-consistency --from-size N`), and `pacta_provider log-audit` is the monitor's self-check. A freshness policy (`--max-sth-age-seconds`) closes the stale-root hole: an old-but-valid tree head could hide later entries.
### The real thing
The `evidence/` directory holds four REAL receipts from the shipped transparency log (tree size 8 - the first four leaves honestly record a failed audit run; read `evidence/README.md`). Verify all four cryptographically and watch a fresh pin store handle them:
"""
),
code(
"""
import tempfile
from pathlib import Path as _P
from pacta.sthstore import check_sth_against_store
from pacta.transparency import verify_receipt
from pacta.yamlio import load_data as _load
log_key = repo_root / "evidence" / "provider.ed25519.pub"
with tempfile.TemporaryDirectory() as tmp:
store = _P(tmp) / "pins.json"
for fork in ["dalek", "anza", "risc0", "betrusted"]:
att = _load(repo_root / "evidence" / f"{fork}-ed25519.attestation.yaml")
receipt = _load(repo_root / "evidence" / f"{fork}-ed25519.receipt.yaml")
result = verify_receipt(att, receipt, log_key)
pin = check_sth_against_store(receipt["sth"], store, consistency_from=receipt.get("consistency"))
print(f"{fork}: receipt accepted={result.accepted} backend={result.signatures.get('ed25519_backend')} pin={pin.action}")
"""
),
md(
"""
## Exercises
- Tamper with one leaf and show that inclusion verification fails.
- Explain why the tree head signature must cover tree size as well as root hash.
- Napkin, then real: run the split-view drill above; then initialize a real provider log (`pacta_provider log-init`), append two attestations, and verify the second receipt with `--sth-store` - watch the pin advance with a verified consistency proof.
- Why must the consistency anchor's ROOT (not just its size) be checked against the pin? Construct the lie that a size-only check would miss.
- Write a policy for when an autonomous agent should require `both` signatures.
- Research checkpoint: compare PACTA's pin store to production Certificate Transparency monitor/gossip requirements - what does gossip add that a single pin store cannot?
"""
),
]
),
"06a_provider_build_the_log.ipynb": notebook(
[
md(
"""
# Lecture 6a: THE PROVIDER'S SIDE - Building the Authenticated Structure
> **DOMAIN BANNER - read this first.** In this notebook YOU ARE THE
> PROVIDER. There is exactly **one** of you per log. You hold the
> signing key. You own a Lean toolchain and hours of compute. You
> carry the append-only obligations. Nothing in this notebook is
> ever executed by an agent - and that asymmetry is not an
> implementation detail, it is the entire design (see the
> justification at the end).
The provider's job, end to end: **verify -> leaf -> tree -> sign ->
self-check**. Only the first step involves Lean; everything after
is hashing and one signature.
"""
),
md(
"""
## Learning Objectives
- Build the full authenticated data structure from real attestations: leaves, tree, Signed Tree Head.
- Place the Lean verification correctly: it is the LEAF-MAKING step, the only expensive one, and it never travels to the agent.
- Sign the root with the merkleized library and run the provider's own inclusion self-check ("the provider eats its own dogfood").
- Justify the singleton/many split as a design decision.
"""
),
md(
"""
## Step 1 - Verify (the expensive step, done ONCE)
The leaf content is a signed **attestation**: the outcome of replaying
every Lean proof of one repository under lean-guard (~30 minutes of
kernel re-checking per fork on the reference machine). This notebook
does NOT re-run that - the shipped `evidence/` attestations ARE that
step's output. What matters architecturally: **the Lean cost lives
here and only here.** No agent ever pays it again.
"""
),
code(
"""
from pathlib import Path
import sys
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
sys.path.insert(0, str(repo_root / "provider" / "src"))
from pacta.yamlio import load_data
attestations = {
fork: load_data(repo_root / "evidence" / f"{fork}-ed25519.attestation.yaml")
for fork in ["dalek", "anza", "risc0", "betrusted"]
}
for fork, att in attestations.items():
certs = att["certificates"]
clean = sum(1 for c in certs if c["status"] == "proven" and c["axiom_status"] == "clean")
print(f"{fork}: {clean}/{len(certs)} proven | commit {att['subject']['repo_commit'][:8]} | guard: {att['machine_protection']['lean_guard'].rsplit('/',1)[-1]}")
"""
),
md(
"""
## Steps 2+3 - Leaf and tree (cheap, mechanical)
Each attestation is wrapped, canonically serialized, and hashed with
the RFC 9162 leaf prefix `0x00`; pairs of nodes hash with prefix
`0x01`. Build a REAL provider log in a scratch directory - you are
the provider, so mint your own key first:
"""
),
code(
"""
import tempfile
from pacta.signing import generate_ed25519_keypair
from pacta_provider.transparency_log import TransparencyLog
state = Path(tempfile.mkdtemp(prefix="provider-lecture-"))
generate_ed25519_keypair(state / "provider.key", state / "provider.pub")
log = TransparencyLog(state / "log")
log.init("lecture-provider", state / "provider.pub")
receipts = {}
for fork, att in attestations.items():
att_path = state / f"{fork}.attestation.yaml"
from pacta.yamlio import dump_data
dump_data(att, att_path)
receipts[fork] = log.append_attestation(att_path, state / "provider.key", state / "provider.pub")
print("tree size:", receipts["betrusted"]["tree_size"])
print("root:", receipts["betrusted"]["sth"]["root_hash"][:32], "…")
"""
),
md(
"""
## Steps 4+5 - Sign the root, then CHECK YOURSELF
The tree head is signed with the **merkleized library itself** (when
the dogfood binary is built): the Ed25519 code that signs this root
is the same pinned dalek source whose proof attestation is a leaf of
this very tree. Before signing, the provider runs the SAME Merkle
inclusion verification an agent would run - on its own signing
library's leaf, against the tree it is about to sign - and embeds
the verdict in the signature block. A root signature that names the
leaf vouching for the code that produced it:
"""
),
code(
"""
import json
sth = receipts["betrusted"]["sth"]
ed = sth["signatures"]["ed25519"]
print("signing backend:", ed.get("signing_backend"))
print(json.dumps(ed.get("signing_provenance", {"note": "dogfood binary not built on this host - OpenSSL fallback, provenance omitted"}), indent=1))
"""
),
md(
"""
## The structure you just built, drawn from your own log
"""
),
code(
"""
from pacta.transparency import leaf_hash, merkle_root, node_hash
def svg_merkle(leaf_hashes, highlight=None, title="", domain="PROVIDER: builds every box below", color="#1e7f4f"):
n = len(leaf_hashes)
width, lh, lv = 980, 108, 92
levels = []
level = [bytes.fromhex(h) if isinstance(h, str) else h for h in leaf_hashes]
levels.append(level)
while len(level) > 1:
nxt = []
for i in range(0, len(level) - 1, 2):
nxt.append(node_hash(level[i], level[i + 1]))
if len(level) % 2:
nxt.append(level[-1])
levels.append(nxt)
level = nxt
height = 130 + lv * len(levels) + 60
out = [f'<svg xmlns="http://www.w3.org/2000/svg" width="{width}" height="{height}" font-family="monospace" font-size="11">']
out.append(f'<rect x="4" y="4" width="{width-8}" height="{height-8}" fill="none" stroke="{color}" stroke-width="2" rx="8"/>')
out.append(f'<text x="16" y="24" fill="{color}" font-size="13" font-weight="bold">{domain}</text>')
out.append(f'<text x="16" y="42" fill="#555">{title}</text>')
pos = {}
for li, lvl in enumerate(levels):
y = height - 70 - li * lv
span = width / (len(lvl) + 1)
for i, node in enumerate(lvl):
x = span * (i + 1)
pos[(li, i)] = (x, y)
hl = highlight and li == 0 and i == highlight[0]
sib = highlight and (li, i) in highlight[1]
fill = "#fdf0da" if sib else ("#e2f2e9" if hl else "#f4f4f6")
stroke = "#a86a10" if sib else ("#1e7f4f" if hl else "#999")
out.append(f'<rect x="{x-52}" y="{y-16}" width="104" height="32" fill="{fill}" stroke="{stroke}" stroke-width="{2 if (hl or sib) else 1}" rx="4"/>')
label = ("leaf %d" % i) if li == 0 else ("root" if li == len(levels) - 1 else "node")
out.append(f'<text x="{x}" y="{y-3}" text-anchor="middle" fill="#333">{label}</text>')
out.append(f'<text x="{x}" y="{y+11}" text-anchor="middle" fill="#777">{node.hex()[:10]}…</text>')
if li > 0:
for ci in (2 * i, 2 * i + 1):
if (li - 1, ci) in pos:
cx, cy = pos[(li - 1, ci)]
out.append(f'<line x1="{x}" y1="{y+16}" x2="{cx}" y2="{cy-16}" stroke="#bbb"/>')
rx, ry = pos[(len(levels) - 1, 0)]
out.append(f'<rect x="{rx-135}" y="{ry-62}" width="270" height="30" fill="#eef" stroke="#3b4d8f" rx="4"/>')
out.append(f'<text x="{rx}" y="{ry-42}" text-anchor="middle" fill="#3b4d8f">Signed Tree Head: Ed25519(root) via merkleized library</text>')
out.append(f'<line x1="{rx}" y1="{ry-32}" x2="{rx}" y2="{ry-16}" stroke="#3b4d8f"/>')
out.append("</svg>")
return "".join(out)
entries = log.entries()
leaf_hexes = [leaf_hash(e.leaf_bytes()).hex() for e in entries]
svg = svg_merkle(leaf_hexes, title=f"your lecture log: {len(entries)} attestation leaves, root {merkle_root([e.leaf_bytes() for e in entries]).hex()[:16]}…")
try:
from IPython.display import SVG, display
display(SVG(svg))
except Exception:
print(svg[:200], "… (open in a notebook to render)")
"""
),
md(
"""
## Why a singleton? The design justification
| | Provider (this notebook) | Agent (next notebook) |
|---|---|---|
| How many | **exactly one** per log | unbounded |
| Owns | the signing key, the Lean toolchain, the full log | the provider's PUBLIC key, a pin file |
| Pays | hours of kernel time per repo, ONCE | milliseconds per check, forever |
| Obligations | append-only, sign every head, serve proofs, self-verify | pin every head, demand consistency |
| Can be wrong? | detectably: signatures + pins make lies attributable | fails closed |
The asymmetry is the product. If agents had to run Lean, the service
would add nothing; if the provider's claims weren't pinned and
signed, trust would be a rumor. Every artifact in this course lives
on exactly one side of this table - and the split between this
notebook and the next MIRRORS it on purpose: if you cannot say
which notebook a step belongs to, you have not understood the step.
## Exercises
- Append a fifth attestation (edit one field of a copy) and watch the root change; which internal nodes changed and which did not? Explain from the tree shape.
- The self-inclusion check ran against the tree BEFORE your key existed in any leaf. What does `signing_provenance.self_inclusion` say, and why is recording that honest?
- Cost accounting: with 4 repos x 30 minutes of Lean and N agents x 5 ms of verification, at what N does the provider model beat every-agent-verifies-locally? (Hint: N=1.)
- Design question: what breaks if there are TWO providers with one key? With two keys and one log?
"""
),
]
),
"06b_agent_verify_inclusion.ipynb": notebook(
[
md(
"""
# Lecture 6b: THE AGENT'S SIDE - Verifying Inclusion (one of many)
> **DOMAIN BANNER - read this first.** In this notebook YOU ARE AN
> AGENT. There are **many** of you. You possess exactly three
> things: the provider's public key, the evidence files, and about
> forty lines of hashing code. You do NOT possess Lean, a proof
> toolchain, or the provider's private key - and you never will
> need them. Everything below runs in milliseconds. If a cell in
> this notebook needed Lean, the design would have failed.
This is **Merkle proof verification, not Lean verification** - the
agent checks WHERE a statement sits, never re-derives WHY it is true.
"""
),
md(
"""
## Learning Objectives
- Implement the complete inclusion verifier from scratch - hashlib only, no pacta imports for the core.
- Verify a REAL receipt against the REAL signed tree head.
- See the inclusion path in the picture of the real 8-leaf log.
- Read the provider's self-check ("dogfood in both directions") from the signature block and say what it does and does not prove.
"""
),
md(
"""
## The whole verifier, from scratch
To make the cost asymmetry unmistakable, here is the ENTIRE core of
what an agent must implement - RFC 9162 inclusion verification in
~25 lines of standard-library Python. Read every line; this is all
the cryptographic machinery your trust rests on (plus one Ed25519
signature check):
"""
),
code(
"""
import hashlib
def leaf_hash(data: bytes) -> bytes:
return hashlib.sha256(b"\\x00" + data).digest()
def node_hash(left: bytes, right: bytes) -> bytes:
return hashlib.sha256(b"\\x01" + left + right).digest()
def verify_inclusion(leaf: bytes, index: int, size: int, proof: list, root: bytes) -> bool:
if index >= size:
return False
fn, sn = index, size - 1
node = leaf_hash(leaf)
for sibling in proof:
if sn == 0:
return False
if fn % 2 == 1 or fn == sn:
node = node_hash(sibling, node)
if fn % 2 == 0:
while fn % 2 == 0 and fn != 0:
fn //= 2
sn //= 2
else:
node = node_hash(node, sibling)
fn //= 2
sn //= 2
return sn == 0 and node == root
print("the agent's entire Merkle toolbox: 3 functions,", "no imports beyond hashlib")
"""
),
md(
"""
## Apply it to the REAL receipt
"""
),
code(
"""
import json
from pathlib import Path
import sys
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
from pacta.yamlio import load_data
from pacta.signing import canonical_json
att = load_data(repo_root / "evidence" / "dalek-ed25519.attestation.yaml")
receipt = load_data(repo_root / "evidence" / "dalek-ed25519.receipt.yaml")
leaf_bytes = canonical_json({"schema_version": 1, "type": "pacta.transparency.attestation_leaf.v1", "attestation": att})
proof = [bytes.fromhex(h) for h in receipt["inclusion_proof"]]
root = bytes.fromhex(receipt["sth"]["root_hash"])
ok = verify_inclusion(leaf_bytes, receipt["leaf_index"], receipt["tree_size"], proof, root)
print(f"leaf {receipt['leaf_index']} of {receipt['tree_size']}, {len(proof)} siblings -> inclusion:", ok)
assert ok
"""
),
md(
"""
## One signature check completes the chain
Inclusion binds the attestation to a root; the signature binds the
root to the provider. Note what the AGENT learns from the signature
block's `signing_provenance`: the provider signed this root with the
merkleized library and Merkle-verified that library's own leaf first
- dogfood in both directions. The agent still re-checks inclusion
itself (above); the provenance is the provider's discipline made
visible, not a substitute for the agent's check.
"""
),
code(
"""
from pacta.transparency import verify_signed_tree_head
from pacta.sthstore import check_sth_against_store
import tempfile
ok, diagnostics, statuses = verify_signed_tree_head(receipt["sth"], repo_root / "evidence" / "provider.ed25519.pub")
print("STH signature:", statuses.get("ed25519"), "| verified on backend:", statuses.get("ed25519_backend"))
print("provider's own discipline, as recorded in the signature block:")
print(json.dumps(receipt["sth"]["signatures"]["ed25519"].get("signing_provenance", {}), indent=1))
with tempfile.TemporaryDirectory() as tmp:
pin = check_sth_against_store(receipt["sth"], Path(tmp) / "pins.json")
print("pin store:", pin.action)
"""
),
md(
"""
## The picture: where your leaf sits in the real log
"""
),
code(
"""
# reconstruct the on-path node hashes from the receipt alone - the
# agent never needs the other leaves, only the siblings.
def svg_inclusion(receipt, width=980):
size, index = receipt["tree_size"], receipt["leaf_index"]
proof = receipt["inclusion_proof"]
rows = [f'<svg xmlns="http://www.w3.org/2000/svg" width="{width}" height="330" font-family="monospace" font-size="11">']
rows.append(f'<rect x="4" y="4" width="{width-8}" height="322" fill="none" stroke="#3b4d8f" stroke-width="2" rx="8"/>')
rows.append('<text x="16" y="24" fill="#3b4d8f" font-size="13" font-weight="bold">AGENT: verifies only the highlighted path - everything grey is somebody else&apos;s data</text>')
span = width / (size + 1)
for i in range(size):
x = span * (i + 1)
me = i == index
fill = "#e2f2e9" if me else "#f4f4f6"
stroke = "#1e7f4f" if me else "#bbb"
rows.append(f'<rect x="{x-42}" y="250" width="84" height="30" fill="{fill}" stroke="{stroke}" stroke-width="{2 if me else 1}" rx="4"/>')
label = "YOUR leaf" if me else f"leaf {i}"
rows.append(f'<text x="{x}" y="269" text-anchor="middle" fill="{stroke}">{label}</text>')
node = leaf_hash(leaf_bytes)
y = 250
x = span * (index + 1)
for depth, sib in enumerate(proof):
ny = y - 60
nx = x # visual simplification: path rises vertically
rows.append(f'<rect x="{nx-52}" y="{ny-16}" width="104" height="30" fill="#fdf0da" stroke="#a86a10" rx="4"/>')
rows.append(f'<text x="{nx}" y="{ny+3}" text-anchor="middle" fill="#a86a10">sibling {depth}: {sib[:10]}…</text>')
rows.append(f'<line x1="{x}" y1="{y-16 if depth else 250}" x2="{nx}" y2="{ny+14}" stroke="#a86a10"/>')
y = ny
rows.append(f'<rect x="{x-135}" y="{y-70}" width="270" height="30" fill="#eef" stroke="#3b4d8f" rx="4"/>')
rows.append(f'<text x="{x}" y="{y-50}" text-anchor="middle" fill="#3b4d8f">signed root {receipt["sth"]["root_hash"][:14]}… (dogfood-signed)</text>')
rows.append(f'<line x1="{x}" y1="{y-16}" x2="{x}" y2="{y-40}" stroke="#3b4d8f"/>')
rows.append("</svg>")
return "".join(rows)
svg = svg_inclusion(receipt)
try:
from IPython.display import SVG, display
display(SVG(svg))
except Exception:
print("(open in a notebook to render the figure)")
print(f"cost of everything in this notebook: ~{receipt['tree_size'].bit_length()} hashes + 1 signature check - milliseconds.")
"""
),
md(
"""
## Transports: files, git, and the online service
Everything you verified above arrived as FILES - and that is a
feature: receipts are self-contained, so transport never carries
trust. The same log has two more faces. The GIT MIRROR
(`lean-transparency-log` on GitHub and on the provider's Forgejo)
publishes every leaf and every signed head - all cloners see the
same heads, which makes every cloner a WITNESS
(`pacta witness-audit` recomputes every prefix root from the
published leaves; run `python3 verify.py --all` in a clone for the
no-install version). The ONLINE SERVICE
(`ltl.zkdefi.org`) adds live endpoints: fetch
fresh evidence (`pacta log-fetch`), advance your pin with an
online consistency proof (`pacta sth-refresh`). The verification
you do afterwards is IDENTICAL in all three transports - this
notebook's ~25 lines never change.
## Convinced - of what, exactly?
After these cells pass, the agent knows: *the provider whose key I
pinned states that the Lean proofs of repository X at commit Y check
out with exactly the documented assumptions, and that statement is
irrevocably part of the log every other agent sees.* The agent then
clones commit Y (the git hash IS the content hash) and builds it -
compiler and build remain declared trusted base until R5. Where a
claim lives (this notebook) and why it is true (the provider's Lean
replay, lecture 6a) never blur.
## Exercises
- Flip one byte of the leaf and re-run: which of the ~25 lines catches it?
- Flip one byte of the ROOT instead: what fails now, inclusion or the signature?
- Your entire verifier fits in one cell. List everything it does NOT check (freshness? consistency with your previous pin? provider honesty about Lean?) and name the lecture that closes each gap.
- The provenance block says the provider checked itself. Why must the agent still run its own inclusion check rather than trust that field?
"""
),
]
),
"07_agent_consequences.ipynb": notebook(
[
md(
"""
# Lecture 7: Agent Consequences
An evidence interpreter is incomplete if nothing changes after evaluation. PACTA has a small consequence engine: it can build a lower-layer Rust decision capsule when evidence satisfies policy, and it refuses wallet construction when coverage is insufficient.
"""
),
md(
"""
## Learning Objectives
- Explain how risk levels map to actions.
- Run a dry-run agent action.
- Understand the generated Rust capsule.
- Explain why R3 permits lower-layer use but denies wallet demos.
- Run the gate both ways: a partial (arithmetic-only) card is denied; the full four-tier card is allowed.
- Connect transparency receipts to build authorization.
"""
),
md(
"""
## Action Policy
Current actions:
- `build-library`: default threshold R3. Produces a proof-gated component capsule.
- `build-wallet-demo`: threshold R4. Writes a denial artifact below R4 - and since the corpus completed its four-tier apex, R4 evidence EXISTS, so this gate can now legitimately open. Watch it swing both ways below.
This is deliberately conservative. The theorem boundary for Ed25519 field plus Edwards arithmetic is valuable, but it does not cover key custody, encoding, hashing, scalar arithmetic completeness, signature verification, transaction construction, or market decisions.
"""
),
code(
"""
from pathlib import Path
import sys
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
from pacta.agent import run_agent_action
from pacta.claims import build_claim_card
from pacta.config import load_config
repo = load_config(repo_root / "examples" / "repos.yaml").repo_named("dalek-ed25519-verified")
card = build_claim_card(repo, repo_root / "repos" / repo.name, offline_fixture=True)
library_decision = run_agent_action(card, "build-library", repo_root / "artifacts-notebook", dry_run=True)
wallet_decision = run_agent_action(card, "build-wallet-demo", repo_root / "artifacts-notebook", dry_run=True)
print(library_decision.to_dict())
print(wallet_decision.to_dict())
"""
),
code(
"""
# NAPKIN: an arithmetic-only card faces the wallet gate - DENIED.
from pathlib import Path
import sys, tempfile
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
from pacta.agent import run_agent_action
from pacta.risk import score_claim_card
partial = {
"component": "napkin-arithmetic-only",
"kind": "ed25519",
"certificates": [
{"name": "CurveFieldProofs.fieldImplementation", "status": "proven", "axiom_status": "clean"},
{"name": "CurveFieldProofs.edwardsImplementation", "status": "proven", "axiom_status": "clean"},
],
"exclusions": ["full EdDSA signature verification"],
"meta": {"r4_requirements": []},
}
partial["risk"] = score_claim_card(partial).to_dict()
with tempfile.TemporaryDirectory() as tmp:
decision = run_agent_action(partial, "build-wallet-demo", tmp, dry_run=True)
print("allowed:", decision.allowed, "at", decision.risk_level)
print(decision.rationale)
"""
),
code(
"""
# REAL: the shipped four-tier R4 card faces the same gate - ALLOWED
# (a demo scaffold only; the residual blockers ride along in the card).
from pacta.yamlio import load_data
full = load_data(repo_root / "examples" / "dalek-ed25519.claims.yaml")
with tempfile.TemporaryDirectory() as tmp:
decision = run_agent_action(full, "build-wallet-demo", tmp, dry_run=True)
print("allowed:", decision.allowed, "at", decision.risk_level)
print(decision.rationale)
"""
),
md(
"""
## The Rust Capsule
The generated capsule is not cryptographic code. It is a consumable policy artifact. It embeds the claim card and exposes constants such as:
- component,
- repo URL,
- kind,
- verified backend,
- risk level,
- evidence mode,
- attestation provider,
- deployment constraints.
Downstream automation can import this crate and check `allowed_for_lower_layer_crypto()` before enabling a code path.
"""
),
code(
"""
from pacta.artifact import _lib_rs
print(_lib_rs(card).splitlines()[:24])
"""
),
md(
"""
## Receipt-Required Builds
The strongest dogfood path in this prototype is:
1. Provider replays Lean and signs attestation.
2. Provider appends attestation to a Merkle transparency log.
3. Provider emits an inclusion receipt with Signed Tree Head.
4. Agent verifies provider signature, receipt inclusion proof, and STH signature.
5. Agent builds only if risk and transparency policy pass.
This transforms "I read a report" into "I accepted a logged, signed proof-check result and acted within its theorem boundary."
"""
),
md(
"""
## Command-Line Lab
Run these from the repository root after generating a provider attestation:
```bash
pacta receipt-verify \\
--attestation provider/out/dalek-ed25519.attestation.yaml \\
--receipt provider/out/dalek-ed25519.receipt.yaml \\
--log-public-key provider/state/local-provider/provider.ed25519.pub
pacta agent \\
--config examples/repos.yaml \\
--repo-name dalek-ed25519-verified \\
--repo repos/dalek-ed25519-verified \\
--attestation provider/out/dalek-ed25519.attestation.yaml \\
--trust-attestation-provider local-pacta-provider \\
--attestation-public-key provider/state/local-provider/provider.ed25519.pub \\
--transparency-receipt provider/out/dalek-ed25519.receipt.yaml \\
--transparency-log-public-key provider/state/local-provider/provider.ed25519.pub \\
--require-transparency-receipt \\
--action build-library
```
"""
),
md(
"""
## Exercises
- Modify a claim card to R2 and show that `build-library` is refused.
- Explain why a denial artifact is useful for auditability.
- Design a policy where an agent requires `both` Ed25519 and ML-DSA signatures for production deployment but allows Ed25519-only in a local lab.
- Write a downstream Rust pseudo-code snippet that imports the generated capsule before enabling a code path.
"""
),
]
),
"09_dogfood_verified_crypto.ipynb": notebook(
[
md(
"""
# Lecture 9: Eat Your Own Dogfood - Verified Crypto in the Agent's Own Loop
Every lecture so far had the agent consume EVIDENCE about a verified Ed25519 implementation while checking that evidence's signatures with OpenSSL - an unverified implementation of the very primitive the evidence is about. That is a defensible bootstrap, but it leaves an ironic gap. This lecture closes it: pacta can build a verifier binary from the PINNED, PROVEN source workspace - the exact commit the dalek certificates pin, serial backend pinned exactly as the verified extraction pins it - and route its own signature checks through it.
"""
),
md(
"""
## Learning Objectives
- State precisely which parts of the dogfood verifier are certificate-covered and which are its trusted base.
- Extract a raw Ed25519 key from an OpenSSL PEM by hand (napkin) and mechanically (real).
- Demonstrate backend dispatch and the fail-closed `--require-verified-verifier` policy.
- Defend the hybrid post-quantum posture: one proven-classical signature plus one required-but-honest ML-DSA slot.
"""
),
md(
"""
## What "verified" means here - the honest ledger
The binary calls `ed25519_dalek::VerifyingKey::verify` in the pinned workspace. The certificates cover `verify_sha512`, the extraction-refactored image of that same path (the delta is the documented hash-wrapper refactor in the pinned source). Certificate-covered: field arithmetic, the group law, scalars, encoding/decoding, constructive decompression, and the four-tier acceptance criterion. Trusted base: SHA-512 (an oracle in the theorems - the proofs hold for whatever bytes it produces), roughly fifteen lines of wire glue, rustc, and the extraction pipeline. The provenance sidecar written at build time records the source commit, the backend cfg, and this exact coverage note - the dogfood claim is itself a claim card.
"""
),
md(
"""
## Napkin: read a PEM with your eyes
An OpenSSL Ed25519 public key PEM is a base64-wrapped DER SubjectPublicKeyInfo (RFC 8410), and for this one algorithm the DER is FIXED: twelve prefix bytes `302a300506032b6570032100`, then the raw 32-byte key. Decode one by hand:
"""
),
code(
"""
from pathlib import Path
import base64, subprocess, sys, tempfile
repo_root = Path.cwd()
if not (repo_root / "src" / "pacta").exists():
repo_root = repo_root.parent
sys.path.insert(0, str(repo_root / "src"))
from pacta.signing import generate_ed25519_keypair
tmp = Path(tempfile.mkdtemp(prefix="dogfood-lecture-"))
generate_ed25519_keypair(tmp / "k.key", tmp / "k.pub")
pem = (tmp / "k.pub").read_text()
print(pem)
body = "".join(line for line in pem.splitlines() if "-----" not in line)
der = base64.b64decode(body)
print("DER length:", len(der), "(should be 12 + 32 = 44)")
print("prefix: ", der[:12].hex(), "(the fixed Ed25519 SPKI header)")
print("raw key: ", der[12:].hex())
"""
),
code(
"""
# REAL: the same extraction, mechanically, with validation - and the
# dispatch that prefers the proven-path binary when it exists.
from pacta.dogfood import locate_verifier, pem_public_key_to_raw
from pacta.signing import sign_payload_ed25519, verify_payload_ed25519_detailed
raw = pem_public_key_to_raw(tmp / "k.pub")
assert raw == der[12:]
print("mechanical extraction matches the napkin:", raw.hex()[:16], "...")
payload = b"the agent checks its own evidence"
signature = sign_payload_ed25519(payload, tmp / "k.key")
ok, error, backend = verify_payload_ed25519_detailed(payload, signature, tmp / "k.pub")
print("valid:", ok, "| backend:", backend)
binary = locate_verifier()
print("dogfood binary:", binary or "not built (OpenSSL fallback in effect - a recorded downgrade)")
"""
),
md(
"""
Build the proven-path verifier once per machine (it needs a local checkout of the pinned source workspace and cargo):
```bash
pacta dogfood-build --source ~/GitClone/FormalVerification/sources/curve25519-dalek-source
pacta dogfood-status
```
With the binary in place, every receipt and attestation check reports `ed25519_backend: verified-dalek-serial`, and policies can DEMAND it:
```bash
pacta receipt-verify ... --require-verified-verifier # fails closed on OpenSSL fallback
pacta agent ... --require-verified-verifier ...
```
"""
),
md(
"""
## Dogfood in BOTH directions
Since this lecture was first written the loop closed on the
provider's side too: the binary gained a `sign` mode, so the
transparency log's tree heads are now SIGNED by the merkleized
library - and before every signature the provider runs the same
Merkle inclusion check an agent runs, on its own signing library's
leaf, against the very tree it is about to sign. The verdict is
embedded in the signature block (`signing_provenance`: backend,
library commit, leaf index, `self_inclusion: verified`,
certificates 16/16). Lectures 6a/6b walk both sides of this.
Honesty note unchanged: the library's VERIFY path is
certificate-covered; the signing path is declared trusted base -
but it is the attested artifact, not an un-attested third
implementation.
## The post-quantum line, held honestly
The dogfood loop deliberately does NOT extend to ML-DSA. There is no formally verified ML-DSA implementation in this corpus, and pretending otherwise would poison the whole posture. The hybrid strategy is therefore asymmetric on purpose:
- **Ed25519 (classical): proven path.** The signature everyone can check today runs on certificate-covered code.
- **ML-DSA-65 (post-quantum): required, honest, unavailable-until-real.** The tree-head slot exists in every signed structure; `--require-signatures both` fails CLOSED on hosts without a real FIPS 204 backend; and when a real backend lands, the policy flips on without a schema change.
A migration strategy that records "we cannot do this yet" as a deployment blocker is strictly stronger than one that ships a placeholder. Blockers get fixed; placeholders get trusted.
"""
),
code(
"""
from pacta.postquantum import detect_ml_dsa
capability = detect_ml_dsa()
print("ml-dsa available:", capability.available)
print("reason:", capability.reason)
print("slot as recorded in every STH:", capability.to_signature_slot())
"""
),
md(
"""
## Exercises
- Flip one byte of a signature and verify through both backends; confirm both reject and that the BACKEND that rejected is recorded.
- The dogfood binary's trusted base includes rustc. The certificates' trusted base includes Charon/Aeneas. Draw the two trust diagrams side by side; which assumptions are shared?
- Napkin, then real: decode a second PEM by hand; then corrupt its DER prefix and confirm `pem_public_key_to_raw` rejects it.
- Policy design: when should an agent REFUSE to fall back to OpenSSL? Write the deployment rule and its recovery path.
- Research checkpoint: what would a proof-carrying SHA-512 change about the coverage note in the provenance sidecar?
"""
),
]
),
"08_capstone_research_program.ipynb": notebook(
[
md(
"""
# Lecture 8: Capstone Research Program
The final goal is not to memorize PACTA commands. The goal is to think like a research engineer who can build an assurance case for autonomous agents that protect funds.
"""
),
md(
"""
## Learning Objectives
- Design a complete assurance roadmap from R3 to R4/R5.
- Identify proof gaps and operational gaps separately.
- Propose theorem milestones for Ed25519, Pallas/Pasta, and wallet integration.
- Design transparency-log monitoring and provider accountability.
- Write a PhD-quality research proposal with measurable deliverables.
"""
),
md(
"""
## R4, achieved - read it like an auditor
When this course was first drafted, R4 was the roadmap. The corpus then delivered it (2026-07-06): scalar arithmetic, encoding/decoding canonicality, constructive decompression, and the four-tier signature apex, every certificate's axiom cone pinned to its documented boundary by each repository's own check script. The composition lesson stands: the hard part was never one theorem - it was composing coverage without smuggling assumptions, which is why the apex tiers are hypothesis-parametric (parser outcomes stay hypotheses) and why the boundary is enforced per certificate, in both directions.
Your first capstone exercise is therefore no longer "design R4" but "audit R4": take the shipped claim card, list what each of the four tiers states, and name the exact residual trusted base. Then design the discharge plan:
- byte-level specs for the wire parsers and legacy filters (turn the parse hypotheses into theorems),
- a verified SHA-512 or a proof-carrying hash oracle (shrink the boundary),
- signing-side coverage (nonce derivation, signer correctness),
- the production-path mapping per fork (anza's default verify() is NOT the verified path - what would it take to cover it?).
"""
),
md(
"""
## From R4 to R5
R5 adds production assurance:
- reproducible production builds,
- compiler and build-system assurance,
- side-channel analysis,
- hardware/KMS/MPC integration,
- key custody policy,
- operational controls,
- monitoring and incident response,
- transparency-log monitors and consistency checks.
R5 is where formal methods meet systems security.
"""
),
md(
"""
## Research Milestone Template
For each milestone, write:
- Claim: exact theorem-boundary statement.
- Artifact: repository, commit, file paths, theorem names.
- Replay: how to reproduce compilation and axiom audit.
- Exclusions: what remains out of scope.
- Trusted base: tools, compiler, translation, provider, log, hardware.
- Risk impact: how the milestone changes R-level classification.
- Failure modes: what invalidates the evidence.
"""
),
code(
"""
milestone = {
"claim": "Scalar52 arithmetic correctness for selected serial/u64 code paths.",
"artifact": ["repo commit", "Lean files", "aggregate theorem name"],
"replay": ["portable Lean check", "#print axioms", "manifest coverage"],
"exclusions": ["SHA-512", "encoding", "side channels", "compiler correctness"],
"risk_impact": "May reduce one blocker toward R4 but does not by itself prove EdDSA.",
}
for key, value in milestone.items():
print(key, "=>", value)
"""
),
md(
"""
## Capstone Project Options
1. Ed25519 R4 Roadmap
Build a theorem dependency map from field arithmetic to full signature verification. Identify every missing certificate and propose an order of attack.
2. Pallas/Pasta Foundation Audit
Determine whether shipped Pallas/Pasta certificates prove add, mul, reduce, square, invert, and aggregate field implementation. Assign R2/R3 with rationale.
3. Transparency Provider Hardening
Extend the provider with external monitors, persistent checkpoints, log consistency verification between checkpoints, and real ML-DSA signing when a backend is available.
4. Agent Policy Language
Design a small declarative policy language that maps claim cards and transparency receipts to allowed actions.
5. Translation Faithfulness Research
Study how to connect Rust source, transpiled Lean, and compiled artifacts with a defensible trusted base.
"""
),
md(
"""
## PhD-Level Evaluation Rubric
A top submission should:
- Make claims that are precise enough to be wrong.
- Separate proof gaps from engineering gaps.
- Include runnable reproduction steps.
- Include negative tests and failure-mode demonstrations.
- Use transparency receipts or equivalent accountability for third-party evidence.
- Avoid marketing language.
- State exactly what would invalidate the result.
- Produce an artifact another researcher can inspect.
"""
),
md(
"""
## Final Exercises
- Write a two-page assurance case for using an R3 Ed25519 arithmetic capsule in a non-wallet lower-layer library.
- Write a denial memo explaining why the same evidence must not authorize a wallet.
- Design a monitoring protocol for PACTA transparency logs, including consistency checks and alert conditions.
- Propose a real ML-DSA integration plan that names the backend, key format, signature format, test vectors, and failure policy.
- Pick one theorem boundary and write the strongest claim you can defend without exaggeration.
"""
),
]
),
"10_verified_custody_wallet.ipynb": notebook(
[
md(
"""
# Lecture 10: The Verified-Custody Wallet (warden)
Everything so far *decided* which cryptographic code to trust.
This lecture *acts* on the decision: we build a custody boundary
out of the four proven curve25519-dalek forks and use it to
guard signatures - inbound and outbound.
The one idea: **inbound acceptance requires a unanimous quorum of
provably-equivalent verifiers, and every outbound signature must
pass the same quorum before it is released.**
We keep the course's ratchet rule: every load-bearing idea runs
twice - napkin scale by hand, then real scale against the live
system - and both are executable here.
"""
),
md(
"""
## Learning Objectives
- Explain why a *unanimous* quorum of provably-equivalent
verifiers turns disagreement into evidence of a fault, and why
majority voting would hide exactly that fault.
- Classify a quorum divergence as a documented semantic edge
(note) versus unexplained (tamper -> latch).
- Describe the outbound signing firewall as verify-after-sign
with a proven verifier, and state warden's honest asymmetry
(verify custody-grade, sign trusted base).
- Recompute a custody card's inclusion proof as a counterparty -
trust by recomputation, not by assertion.
"""
),
md(
"""
## Why a quorum, when one proof would do?
Each member is *proven* to decide the same predicate,
`accept(A,m,R,s) ⇔ decompress(R) = [k](−A) + [s]B`. So on the
proven domain they cannot disagree about *meaning*. Classic
N-version programming hopes independent code won't share a bug;
we do not hope - we know the semantics coincide, so a runtime
disagreement is not opinion, it is **evidence of a fault**: a
corrupted build, a memory error, or tampering. The quorum turns
"the verifiers differed" into an alarm with a theorem behind it.
"""
),
md(
"""
## Napkin scale: a 3-of-3 quorum with toy verifiers
Forget real curves for a moment. Model three verifiers as
functions and watch the boundary logic: unanimity accepts,
any disagreement fails closed and is classified.
"""
),
code(
"""
def toy_quorum(verdicts):
kinds = set(verdicts.values())
if kinds == {"accept"}:
return "unanimous-accept", True
if kinds == {"reject"}:
return "unanimous-reject", False
return "divergence -> FAIL CLOSED + incident", False
print(toy_quorum({"dalek": "accept", "anza": "accept", "risc0": "accept"}))
print(toy_quorum({"dalek": "reject", "anza": "reject", "risc0": "reject"}))
print(toy_quorum({"dalek": "accept", "anza": "reject", "risc0": "accept"}))
"""
),
md(
"""
The third line is the whole point: a lone dissenter does not get
out-voted. Acceptance needs *everyone*; anything else is a
refusal plus a recorded incident. Majority voting would hide
exactly the fault we most want to see.
"""
),
md(
"""
## The divergence taxonomy
The forks are *allowed* to differ on documented degenerate
inputs (anza rejects `A = 0` and a legacy excluded-small-order-R
list). We still fail closed; the taxonomy only grades the alarm:
- **semantic-edge** - they differ AND a documented edge flag
applies (small-order R, non-canonical s, zero key): severity
*note*.
- **unexplained** - they differ with no documented reason, or a
member errored: severity *tamper* -> custody **latches**.
"""
),
code(
"""
import sys, pathlib
for parent in [pathlib.Path.cwd(), *pathlib.Path.cwd().parents]:
if (parent / "src" / "pacta").exists():
sys.path.insert(0, str(parent / "src")); ROOT = parent; break
from pacta.quorum import semantic_edge_flags, SMALL_ORDER_ENCODINGS
small_order_R = sorted(SMALL_ORDER_ENCODINGS)[0]
print("edge flags for a small-order R:",
semantic_edge_flags(b"\\x02" * 32, small_order_R + b"\\x00" * 32))
print("edge flags for an ordinary sig:",
semantic_edge_flags(b"\\x02" * 32, b"\\x01" * 64))
"""
),
md(
"""
A divergence on the first input is a documented edge (note); a
divergence on the second has no excuse (tamper). Same fail-closed
verdict, very different alarm.
"""
),
md(
"""
## Real scale: the four proven forks, if built
If you have run `pacta wallet build-quorum`, the next cell drives
the **real** four-fork quorum: sign a payload with the dogfood
(attested) signer, then watch all four proven verifiers agree on
accept, and on reject for a flipped byte. If the binaries are not
built, we say so and skip - honestly, the way the wallet itself
fails closed.
"""
),
code(
"""
from pacta.quorum import load_quorum, binary_path
built = [b for b in ("dalek", "anza", "risc0", "betrusted") if binary_path(b).exists()]
if len(built) < 2:
print("quorum not built (need >=2). Run: pacta wallet build-quorum --sources-root <...>")
else:
import tempfile, os
from pacta.dogfood import locate_verifier, pem_public_key_to_raw, sign_payload_dogfood
from pacta.signing import generate_ed25519_keypair
v = locate_verifier()
if v is None:
print("dogfood signer not built; run pacta dogfood-build")
else:
d = tempfile.mkdtemp()
key, pub = os.path.join(d, "k.pem"), os.path.join(d, "k.pub")
generate_ed25519_keypair(key, pub)
payload = b"curriculum lecture 10 payload"
sig = sign_payload_dogfood(payload, key, v)
pk = pem_public_key_to_raw(pub)
q = load_quorum(min_members=2)
print("members:", sorted(q.members))
good = q.verify(payload, sig, pk)
print("valid signature ->", good.classification, "accepted =", good.accepted)
bad = q.verify(payload, bytes([sig[0] ^ 0xFF]) + sig[1:], pk)
print("one flipped byte ->", bad.classification, "accepted =", bad.accepted)
"""
),
md(
"""
## The signing firewall: verify-after-sign, but proven
Outbound is `intent -> sign -> firewall -> release`. The fresh
signature faces the same quorum; only unanimity releases it. A
rejected self-signature is *quarantined, never returned*, and
custody latches. This is the textbook fault-injection
countermeasure - verify a signer's output before trusting it -
with the verifier upgraded to machine-checked code.
Note the honest asymmetry: the *verify* paths are certificate-
covered (custody-grade), but the *signing* step is trusted base -
the attested artifact, not a third implementation. The firewall
is exactly how we fence that weaker edge.
"""
),
md(
"""
## Two voices, one boundary (the domain split, again)
Lecture 06 split provider and agent. warden inherits the split:
- **The operator voice** seals the capsule: it runs the R4 gate,
pins the attested source commits, and stores the transparency-
log receipts that authorized each member.
- **The counterparty (agent) voice** never trusts the operator's
adjectives. It reads the *custody card* and recomputes the
inclusion proofs itself - trust by recomputation.
The next cell is the counterparty side: given a card, verify a
member's inclusion proof with nothing but stdlib hashing.
"""
),
code(
"""
# Counterparty-side check of ONE member's inclusion proof.
# (Works whenever you have a wallet + its fetched evidence; here
# we show the primitive the card relies on.)
from pacta.transparency import verify_inclusion, leaf_bytes_for_attestation
import json, glob
ev = sorted(glob.glob(str(ROOT / "examples" / "wallet-evidence" / "*.attestation.json")))
if not ev:
print("no bundled evidence; fetch with `pacta log-fetch` to try live")
else:
att = json.load(open(ev[0]))
rec = json.load(open(ev[0].replace(".attestation.", ".receipt.")))
ok = verify_inclusion(
leaf_bytes_for_attestation(att),
rec["leaf_index"], rec["tree_size"],
[bytes.fromhex(h) for h in rec["inclusion_proof"]],
bytes.fromhex(rec["sth"]["root_hash"]),
)
print(f"{att['subject']['component']}: inclusion recomputes ->", ok)
print("The counterparty believed no adjective; it recomputed a Merkle root.")
"""
),
md(
"""
## Corrupt a member, watch the pin catch it (executable)
The wallet seals each member's SHA-256 into its capsule. The
next cell stages a COPY of a real member binary in a temp
directory, "seals" its hash the way the capsule does, appends
one byte (a supply-chain attack in miniature), and re-checks.
Nothing on your machine is modified.
"""
),
code(
"""
import hashlib, shutil, tempfile, pathlib
from pacta.quorum import binary_path
member = binary_path("dalek")
if not member.exists():
print("quorum not built; run pacta wallet build-quorum first")
else:
stage = pathlib.Path(tempfile.mkdtemp()) / member.name
shutil.copy2(member, stage)
sealed = hashlib.sha256(stage.read_bytes()).hexdigest() # capsule pin
print("sealed :", sealed[:24], "...")
with stage.open("ab") as f:
f.write(b"\\x00") # the attack
current = hashlib.sha256(stage.read_bytes()).hexdigest()
print("current:", current[:24], "...")
if current != sealed:
print("PIN CAUGHT IT: wallet.quorum() would refuse to assemble ->")
print(" 'quorum member dalek binary hash changed since the capsule was sealed'")
else:
print("impossible: SHA-256 collision")
"""
),
md(
"""
One appended byte and the wallet refuses to even *assemble* the
quorum - before any verification runs. Note what this control
is and is not: it stops binary substitution *between* wallet
sessions; an attacker with live root outranks it (see
docs/threat-model.md, attacker #7 - that is what the choir and
the airgap profiles are for).
"""
),
md(
"""
## Exercises
- Change `toy_quorum` to majority voting and write two sentences
on exactly which attack that lets through.
- Extend the corrupt-a-member cell: corrupt the capsule JSON
itself instead of the binary. What catches that, and when?
(Hint: nothing does until the ledger genesis is compared -
write down the exact trust statement the capsule hash in the
genesis entry provides.)
- The signing path is trusted base. Write the strongest *true*
sentence you can about warden's outbound safety, and the
strongest *false* one a marketer would write - and name the
word that makes the second one false.
- Design `warden-treasury`: which member re-verifies Solana
transactions, and what exactly the RPC provider is still
trusted for after you do.
"""
),
]
),
}
README = """# 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,
- the mirrored provider/agent domain split (6a: one provider builds and dogfood-signs the log; 6b: many agents verify inclusion in ~25 lines, no Lean),
- 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,
- the verified-custody wallet (warden): a quorum boundary of four proven forks, the signing firewall, and the agent-native MCP surface,
- 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.
"""
def main() -> None:
NOTEBOOK_DIR.mkdir(parents=True, exist_ok=True)
for name, data in COURSE.items():
path = NOTEBOOK_DIR / name
path.write_text(json.dumps(data, indent=2, sort_keys=False) + "\n", encoding="utf-8")
(NOTEBOOK_DIR / "README.md").write_text(README, encoding="utf-8")
if __name__ == "__main__":
main()
Reference in a new issue View git blame Copy permalink