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

add proof-aware crypto curriculum notebooks

Browse source
This commit is contained in:
saymrwulf 2026-07-03 14:42:59 +02:00
parent 0461d2f997
commit 5da353b31e
14 changed files with 2869 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
AGENTS.md
View file

@ -18,3 +18,4 @@ Guidance for future Codex runs in this repository:
- Keep the Merkle log RFC 9162-style unless a new standard is deliberately adopted and documented. Do not replace it with an ad hoc hash chain.
- Do not pretend ML-DSA exists. If no real ML-DSA backend is available, record the signature slot as unavailable and fail closed for policies that require both Ed25519 and ML-DSA.
- Provider private keys and transparency log state belong under ignored `provider/state/` or `provider/out/` paths. Do not commit local trust state.
- Curriculum notebooks are generated by `scripts/build_curriculum_notebooks.py`. Update the generator, regenerate `notebooks/`, and keep notebook code cells output-free.

16
README.md
View file

@ -46,6 +46,22 @@ pacta agent --claims claims.yaml --action build-wallet-demo
pacta agent --config examples/repos.yaml --repo-name dalek-ed25519-verified --attestation examples/dalek-ed25519.attestation.yaml --trust-attestation-provider example-proof-checker.invalid --action build-library
```
## Curriculum Notebooks
The `notebooks/` directory contains a zero-to-hero teaching sequence for undergraduate students moving toward research-grade assurance engineering:
- `00_course_map.ipynb`: course structure, prerequisites, assessment model, references.
- `01_threat_model_and_truth_boundary.ipynb`: threat model, theorem boundaries, exclusions.
- `02_claim_cards_and_risk_model.ipynb`: claim card schema and R0-R5 scoring.
- `03_lean_replay_and_axiom_audit.ipynb`: replay versus transpilation, Lean invocation, axiom audits.
- `04_proof_hygiene_and_boundaries.ipynb`: `sorry`, local axioms, trivial targets, manifest coverage.
- `05_third_party_attestation_provider.ipynb`: provider trust transformation and signed attestations.
- `06_merkle_transparency_logs.ipynb`: RFC 9162-style Merkle proofs, STHs, Ed25519/ML-DSA policy.
- `07_agent_consequences.ipynb`: receipt-gated artifact builds and wallet-denial policy.
- `08_capstone_research_program.ipynb`: research roadmap from R3 toward R4/R5.
The notebooks are committed without execution output. They can be opened in Jupyter, VS Code, or any notebook reader. They import `pacta` directly from this repository and avoid external notebook-only dependencies.
## Consequence Engine
`pacta agent` turns evaluation into an operational consequence.

151
notebooks/00_course_map.ipynb Normal file
View file

@ -0,0 +1,151 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# PACTA Curriculum: From Zero to Hero\n",
"\n",
"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.\n",
"\n",
"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:\n",
"\n",
"> Does this theorem cover the exact code path that will protect funds?\n",
"\n",
"The course takes that question seriously. Every notebook connects theory to a runnable artifact in this repository.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Learning Objectives\n",
"\n",
"By the end of the sequence, a strong student should be able to:\n",
"\n",
"- Explain why cryptographic implementation proofs have theorem boundaries.\n",
"- Distinguish formal proof evidence from tests, audits, marketing claims, and operational controls.\n",
"- Read a PACTA claim card and understand its guarantees, preconditions, exclusions, trusted base, and risk level.\n",
"- Reproduce a local Lean replay or diagnose why local replay is unavailable.\n",
"- Perform a proof hygiene scan and explain why `sorry`, local axioms, and trivial theorem targets are dangerous.\n",
"- Explain how a third-party proof-checking provider changes the trusted base.\n",
"- Implement and verify RFC 9162-style Merkle inclusion and consistency proofs.\n",
"- Explain why Signed Tree Heads need accountable signatures, why Ed25519 is useful here, and why ML-DSA requires a real backend.\n",
"- Design policy gates that convert verification evidence into consequences.\n",
"- Write a research plan for moving from R3 lower-layer arithmetic evidence toward R4/R5 production assurance.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Prerequisites\n",
"\n",
"Recommended background:\n",
"\n",
"- Python basics: functions, dictionaries, lists, files, subprocesses.\n",
"- Discrete math: modular arithmetic, induction, trees, hashes.\n",
"- Basic cryptography vocabulary: public keys, signatures, hashes, finite fields.\n",
"- Basic command-line usage on macOS or Linux.\n",
"\n",
"Not required at the start:\n",
"\n",
"- Lean.\n",
"- Rust internals.\n",
"- Elliptic curve implementation expertise.\n",
"- Certificate transparency expertise.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pathlib import Path\n",
"import sys\n",
"\n",
"repo_root = Path.cwd()\n",
"if not (repo_root / \"src\" / \"pacta\").exists():\n",
" repo_root = repo_root.parent\n",
"sys.path.insert(0, str(repo_root / \"src\"))\n",
"\n",
"print(repo_root)\n",
"print((repo_root / \"README.md\").exists())\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Course Map\n",
"\n",
"1. `01_threat_model_and_truth_boundary.ipynb`\n",
" Learn the product problem, the security boundary, and the difference between verified arithmetic and verified wallets.\n",
"\n",
"2. `02_claim_cards_and_risk_model.ipynb`\n",
" Study PACTA claim cards, risk levels R0-R5, and how claim serialization supports machine decisions.\n",
"\n",
"3. `03_lean_replay_and_axiom_audit.ipynb`\n",
" Learn how local Lean replay works, why PACTA avoids transpilation, and what an axiom audit proves.\n",
"\n",
"4. `04_proof_hygiene_and_boundaries.ipynb`\n",
" Learn to scan proof artifacts for `sorry`, local `axiom`, trivial theorem statements, and missing manifest coverage.\n",
"\n",
"5. `05_third_party_attestation_provider.ipynb`\n",
" Learn how a proof-checking service can transform hard local verification into provider trust.\n",
"\n",
"6. `06_merkle_transparency_logs.ipynb`\n",
" Build the Merkle accumulator intuition behind inclusion proofs, consistency proofs, and Signed Tree Heads.\n",
"\n",
"7. `07_agent_consequences.ipynb`\n",
" Connect evidence to action: build a lower-layer Rust capsule only when policy gates pass.\n",
"\n",
"8. `08_capstone_research_program.ipynb`\n",
" Design a PhD-level roadmap for closing the gaps from R3 toward R4/R5.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Assessment Model\n",
"\n",
"Each notebook contains:\n",
"\n",
"- A lecture section for concepts.\n",
"- A lab section with runnable code.\n",
"- Checkpoints that force precise answers.\n",
"- Exercises for mastery.\n",
"- Research prompts for advanced students.\n",
"\n",
"The capstone asks students to produce a defensible assurance case, not a slogan.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## References\n",
"\n",
"- RFC 9162, Certificate Transparency Version 2.0: https://datatracker.ietf.org/doc/html/rfc9162\n",
"- RFC 8032, Edwards-Curve Digital Signature Algorithm: https://datatracker.ietf.org/doc/html/rfc8032\n",
"- NIST FIPS 204, Module-Lattice-Based Digital Signature Standard: https://csrc.nist.gov/pubs/fips/204/final\n",
"- PACTA README: `../README.md`\n"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"name": "python",
"pygments_lexer": "ipython3"
}
},
"nbformat": 4,
"nbformat_minor": 5
}

163
notebooks/01_threat_model_and_truth_boundary.ipynb Normal file
View file

@ -0,0 +1,163 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Lecture 1: Threat Model and Truth Boundary\n",
"\n",
"The motivating system is an autonomous economic agent that may move stablecoins. It faces two broad attack classes:\n",
"\n",
"1. Psychological or game-theoretic attacks that trick the agent into harmful financial actions.\n",
"2. Implementation attacks against the cryptographic and tooling stack that protects keys, signatures, proofs, and policy gates.\n",
"\n",
"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.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Learning Objectives\n",
"\n",
"- Define a threat model for proof-aware cryptographic tooling.\n",
"- Explain why lower-layer arithmetic proofs do not imply wallet safety.\n",
"- State the strongest current Ed25519-family claim in theorem-boundary language.\n",
"- List common exclusions that remain outside the proof artifact.\n",
"- Explain why an autonomous agent needs consequences, not just reports.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## The Core Truth Boundary\n",
"\n",
"The strongest current Ed25519-family claim in this project is approximately:\n",
"\n",
"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.\n",
"\n",
"That is valuable. It is also not a full wallet proof, not full EdDSA verification, and not a proof of all Solana transaction behavior.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Proven or High-Value Evidence\n",
"\n",
"A clean R3-style Ed25519 arithmetic result may cover:\n",
"\n",
"- FieldElement51 arithmetic over `F_p` through denotation.\n",
"- Panic and overflow freedom under limb-bound preconditions.\n",
"- Complete Edwards point operations under `ExtValid` and `OnCurveExt`.\n",
"- Implementation laws through denotation.\n",
"- Axiom audit expected to show only standard Lean axioms: `propext`, `Classical.choice`, `Quot.sound`.\n",
"\n",
"The exact theorem names matter. In the current target repos, important certificates include:\n",
"\n",
"- `CurveFieldProofs.fieldImplementation`\n",
"- `CurveFieldProofs.edwardsImplementation`\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Explicit Exclusions\n",
"\n",
"Do not let a lower-layer theorem leak into claims about:\n",
"\n",
"- Full EdDSA signature verification.\n",
"- Complete Scalar52 arithmetic unless separately proven.\n",
"- SHA-512.\n",
"- Encoding, decoding, and canonicality unless separately proven.\n",
"- Rust compiler correctness.\n",
"- Charon/Aeneas translation faithfulness.\n",
"- Side-channel resistance.\n",
"- SIMD, AVX, hardware, zkVM, accelerator, or syscall paths.\n",
"- Wallet policy, transaction construction, RPC, chain, oracle, market, or LLM decision safety.\n",
"\n",
"A professional assurance case is often mostly about preventing evidence from being overextended.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pathlib import Path\n",
"import sys\n",
"\n",
"repo_root = Path.cwd()\n",
"if not (repo_root / \"src\" / \"pacta\").exists():\n",
" repo_root = repo_root.parent\n",
"sys.path.insert(0, str(repo_root / \"src\"))\n",
"\n",
"from pacta.config import load_config\n",
"\n",
"config = load_config(repo_root / \"examples\" / \"repos.yaml\")\n",
"for repo in config.repos:\n",
" print(f\"{repo.name:32} kind={repo.kind:13} backend={repo.verified_backend}\")\n",
" if repo.backend_warning:\n",
" print(f\" backend warning: {repo.backend_warning}\")\n",
" if repo.known_status:\n",
" print(f\" known status: {repo.known_status}\")\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Consequences\n",
"\n",
"PACTA turns evaluation into operational consequences:\n",
"\n",
"- If evidence is R0/R1/R2, do not build or consume lower-layer crypto capsules.\n",
"- If evidence is R3, a constrained lower-layer component capsule may be built.\n",
"- If evidence is below R4, wallet demo construction is refused.\n",
"- If a third-party attestation is required but not trusted, the score falls to R0.\n",
"- If a transparency receipt is required but invalid or absent, the score falls to R0.\n",
"\n",
"This makes verification a gate, not a decorative badge.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Checkpoint Questions\n",
"\n",
"1. Why does a proof of field arithmetic not prove transaction construction?\n",
"2. What would have to be proven before full EdDSA verification could plausibly reach R4?\n",
"3. Why is \"the proof failed to replay locally\" different from \"the theorem is false\"?\n",
"4. Why should a zkVM accelerator path be excluded unless the repo proves otherwise?\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Exercises\n",
"\n",
"- Pick one configured repository from `examples/repos.yaml`. Write three precise claims that PACTA may make about it and three claims PACTA must refuse.\n",
"- Rewrite the sentence \"this is verified Ed25519\" into a theorem-boundary statement that a security reviewer would accept.\n",
"- Create a table mapping each exclusion above to the attack class it leaves open.\n"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"name": "python",
"pygments_lexer": "ipython3"
}
},
"nbformat": 4,
"nbformat_minor": 5
}

193
notebooks/02_claim_cards_and_risk_model.ipynb Normal file
View file

@ -0,0 +1,193 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Lecture 2: Claim Cards and the R0-R5 Risk Model\n",
"\n",
"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.\n",
"\n",
"A claim card is not a marketing page. It is a structured input to policy.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Learning Objectives\n",
"\n",
"- Read the claim card schema.\n",
"- Explain risk levels R0 through R5.\n",
"- Generate an offline fixture claim card.\n",
"- Understand why R3 can authorize lower-layer library use but not wallet construction.\n",
"- Identify blockers and deployment constraints in a claim card.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Risk Levels\n",
"\n",
"- `R0`: Unknown or untrusted. No usable evidence.\n",
"- `R1`: Tests, audits, or informal claims only.\n",
"- `R2`: Formal model exists, but incomplete, weakly tied to production code, or major proof gaps remain.\n",
"- `R3`: A specific lower-layer implementation artifact is Lean-checked for a specific backend and theorem boundary.\n",
"- `R4`: End-to-end primitive proof covers public API, parsing/encoding, scalar arithmetic, hashing interface, signature equation, rejection rules, and implementation boundary.\n",
"- `R5`: R4 plus reproducible production builds, compiler/build assurance, side-channel analysis, hardware/KMS/MPC integration, and operational controls.\n",
"\n",
"The expected first milestone for Ed25519 field plus Edwards arithmetic is R3 if certificates compile and the axiom audit is clean.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pathlib import Path\n",
"import sys\n",
"\n",
"repo_root = Path.cwd()\n",
"if not (repo_root / \"src\" / \"pacta\").exists():\n",
" repo_root = repo_root.parent\n",
"sys.path.insert(0, str(repo_root / \"src\"))\n",
"\n",
"from pacta.claims import build_claim_card\n",
"from pacta.config import load_config\n",
"\n",
"config = load_config(repo_root / \"examples\" / \"repos.yaml\")\n",
"repo = config.repo_named(\"dalek-ed25519-verified\")\n",
"card = build_claim_card(repo, repo_root / \"repos\" / repo.name, offline_fixture=True)\n",
"\n",
"print(card[\"component\"])\n",
"print(card[\"risk\"][\"level\"])\n",
"print(card[\"risk\"][\"rationale\"])\n",
"print(card[\"certificates\"][0])\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"important_fields = [\n",
" \"component\",\n",
" \"repo_url\",\n",
" \"repo_commit\",\n",
" \"verification_dir\",\n",
" \"kind\",\n",
" \"verified_backend\",\n",
" \"certificates\",\n",
" \"guarantees\",\n",
" \"preconditions\",\n",
" \"exclusions\",\n",
" \"trusted_base\",\n",
" \"evidence\",\n",
" \"risk\",\n",
"]\n",
"for field in important_fields:\n",
" print(field, \"=>\", type(card.get(field)).__name__)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Reading a Certificate Entry\n",
"\n",
"A certificate entry contains:\n",
"\n",
"- `name`: theorem or aggregate certificate name.\n",
"- `status`: `proven`, `missing`, `failed`, or `unknown`.\n",
"- `axiom_status`: `clean`, `dirty`, or `not_checked`.\n",
"- `observed_axioms`: axioms reported by Lean.\n",
"- `expected_axioms`: allowed standard axioms for this profile.\n",
"\n",
"A clean R3 result requires more than a theorem name. It requires a successful replay or trusted attestation, an expected axiom set, and no policy-blocking exclusions.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"for cert in card[\"certificates\"]:\n",
" print(f\"{cert['name']}: {cert['status']} / {cert['axiom_status']}\")\n",
" print(\" observed:\", cert[\"observed_axioms\"])\n",
" print(\" expected:\", cert[\"expected_axioms\"])\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Deployment Constraints\n",
"\n",
"Deployment constraints are where many assurance cases become honest. For Ed25519 arithmetic, constraints include:\n",
"\n",
"- Use exact pinned source or reviewed diff.\n",
"- Use verified serial/u64 backend only.\n",
"- Disable accelerator/syscall/hardware/SIMD paths unless separately certified.\n",
"- Do not treat this as full EdDSA verification.\n",
"- Keep key custody behind HSM/MPC/policy firewall until signing stack proof coverage improves.\n",
"- Use ordinary tests/fuzzing at encoding/API/transaction boundaries.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"for constraint in card[\"risk\"][\"deployment_constraints\"]:\n",
" print(\"-\", constraint)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Exercises\n",
"\n",
"- Change the generated card in memory so one certificate is `missing`. Rescore it and explain the change.\n",
"- Write a short policy that allows `build-library` at R3 but denies `build-wallet-demo` below R4.\n",
"- Compare the trusted base for local replay versus third-party attestation.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from copy import deepcopy\n",
"from pacta.risk import score_claim_card\n",
"\n",
"weaker = deepcopy(card)\n",
"weaker[\"certificates\"][0][\"status\"] = \"missing\"\n",
"weaker[\"certificates\"][0][\"axiom_status\"] = \"not_checked\"\n",
"assessment = score_claim_card(weaker)\n",
"print(assessment.level)\n",
"print(assessment.rationale)\n",
"print(assessment.blockers)\n"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"name": "python",
"pygments_lexer": "ipython3"
}
},
"nbformat": 4,
"nbformat_minor": 5
}

178
notebooks/03_lean_replay_and_axiom_audit.ipynb Normal file
View file

@ -0,0 +1,178 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Lecture 3: Lean Replay and Axiom Audit\n",
"\n",
"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.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Learning Objectives\n",
"\n",
"- Explain the difference between transpilation and proof replay.\n",
"- Understand how PACTA discovers Lean files and manifests.\n",
"- Build a portable Lean invocation without Linux-only shell helpers.\n",
"- Explain `#print axioms` and why axiom sets matter.\n",
"- Diagnose missing Lean/lake or missing pinned Aeneas environments.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Why Not Run Charon/Aeneas?\n",
"\n",
"The corpus policy is strict:\n",
"\n",
"- The transpilation work is finished in the verified repos.\n",
"- Re-running extraction could create a different artifact and confuse the trust story.\n",
"- The current task is to interpret, replay, summarize, and score the existing Lean proof artifacts.\n",
"\n",
"For a production assurance case, translation faithfulness remains part of the trusted base unless separately proven.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pathlib import Path\n",
"import sys\n",
"\n",
"repo_root = Path.cwd()\n",
"if not (repo_root / \"src\" / \"pacta\").exists():\n",
" repo_root = repo_root.parent\n",
"sys.path.insert(0, str(repo_root / \"src\"))\n",
"\n",
"from pacta.manifest import discover_layout\n",
"\n",
"fixture = repo_root / \"tests\" / \"fixtures\" / \"mini-ed25519-verified\"\n",
"layout = discover_layout(fixture, \"verification\")\n",
"print(\"verification_dir:\", layout.verification_dir)\n",
"print(\"files:\")\n",
"for path in layout.compile_order:\n",
" print(\" \", path.relative_to(fixture))\n",
"print(\"warnings:\", layout.warnings)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Portable Lean Invocation\n",
"\n",
"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`.\n",
"\n",
"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.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pacta.lean import LeanTools, build_lean_invocation\n",
"\n",
"tools = LeanTools(lean=\"/usr/bin/lean\", lake=\"/usr/bin/lake\")\n",
"example_file = layout.compile_order[0]\n",
"print(build_lean_invocation(example_file, tools, use_lake_env=True, output_path=example_file.with_suffix(\".olean\")))\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Axiom Audit\n",
"\n",
"A theorem can compile while depending on unexpected axioms. For the Ed25519 arithmetic profiles, the expected axiom set is usually:\n",
"\n",
"- `propext`\n",
"- `Classical.choice`\n",
"- `Quot.sound`\n",
"\n",
"PACTA generates a temporary Lean file with imports such as:\n",
"\n",
"```lean\n",
"import Proofs.FieldMain\n",
"import Proofs.EdMain\n",
"#print axioms CurveFieldProofs.fieldImplementation\n",
"#print axioms CurveFieldProofs.edwardsImplementation\n",
"```\n",
"\n",
"It then parses Lean output and marks the result clean only when observed axioms match the expected set.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pacta.lean import parse_axiom_output\n",
"\n",
"output = \"\"\"'CurveFieldProofs.fieldImplementation' depends on axioms:\n",
"[propext, Classical.choice, Quot.sound]\n",
"'CurveFieldProofs.edwardsImplementation' depends on axioms:\n",
"[propext, Classical.choice, Quot.sound]\n",
"\"\"\"\n",
"parsed = parse_axiom_output(\n",
" output,\n",
" [\n",
" \"CurveFieldProofs.fieldImplementation\",\n",
" \"CurveFieldProofs.edwardsImplementation\",\n",
" ],\n",
")\n",
"print(parsed)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Local Replay Failure Modes\n",
"\n",
"Important distinctions:\n",
"\n",
"- Missing `lean`: local verifier capability unavailable.\n",
"- Missing `lake`: local project environment may be unavailable.\n",
"- Missing Aeneas Lean project: local replay unavailable for repos that depend on it.\n",
"- Lean file fails: proof replay failed in this environment.\n",
"- Axiom set dirty: theorem depends on unexpected assumptions.\n",
"\n",
"These are not the same. A professional report must state which one happened.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Exercises\n",
"\n",
"- Run `pacta doctor --config examples/repos.yaml --repo-name dalek-ed25519-verified` and classify the result.\n",
"- Create a fake axiom output with an extra axiom. Parse it and explain why the result should be dirty.\n",
"- Explain why a replay runner should not silently fall back from failure to an offline fixture.\n"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"name": "python",
"pygments_lexer": "ipython3"
}
},
"nbformat": 4,
"nbformat_minor": 5
}

154
notebooks/04_proof_hygiene_and_boundaries.ipynb Normal file
View file

@ -0,0 +1,154 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Lecture 4: Proof Hygiene and Boundaries\n",
"\n",
"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.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Learning Objectives\n",
"\n",
"- Detect `sorry`, local `axiom`, trivial theorem targets, and suspicious `by trivial`.\n",
"- Understand why comments should not be treated as fatal proof failures.\n",
"- Explain why manifest coverage matters.\n",
"- Distinguish a hygiene warning from a replay failure.\n",
"- Write precise boundary language for proof reports.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Patterns PACTA Scans For\n",
"\n",
"- `sorry`\n",
"- `axiom` declarations under `Proofs/`\n",
"- theorem targets such as `: True :=`\n",
"- suspicious `by trivial` in spec/certificate/root files\n",
"- `native_decide` as advisory unless dependency-cone analysis is stronger\n",
"- missing certificate names\n",
"- proof files not included in a manifest when a manifest exists\n",
"\n",
"A simple scanner may over-warn. It must not over-claim.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pathlib import Path\n",
"import sys\n",
"\n",
"repo_root = Path.cwd()\n",
"if not (repo_root / \"src\" / \"pacta\").exists():\n",
" repo_root = repo_root.parent\n",
"sys.path.insert(0, str(repo_root / \"src\"))\n",
"\n",
"from pacta.audit import scan_hygiene\n",
"from pacta.manifest import discover_layout\n",
"\n",
"fixture = repo_root / \"tests\" / \"fixtures\" / \"mini-ed25519-verified\"\n",
"layout = discover_layout(fixture, \"verification\")\n",
"issues = scan_hygiene(layout, [\"CurveFieldProofs.fieldImplementation\"])\n",
"print(\"issues:\", issues)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Why `sorry` Is Serious\n",
"\n",
"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.\n",
"\n",
"The lesson is not \"never prototype with placeholders.\" The lesson is \"never ship assurance claims that hide placeholders.\"\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Why Local Axioms Are Serious\n",
"\n",
"A local axiom can assert the result directly. For example:\n",
"\n",
"```lean\n",
"axiom fieldImplementation : CorrectFieldImplementation\n",
"```\n",
"\n",
"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.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Trivial Theorems and Spec Drift\n",
"\n",
"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.\n",
"\n",
"Professional review asks two questions:\n",
"\n",
"1. Is the proof complete?\n",
"2. Is the theorem the right theorem?\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"# A tiny reviewer helper: classify theorem statements by obvious risk.\n",
"examples = {\n",
" \"good_shape\": \"theorem add_denote ... : denote (add x y) = x + y := ...\",\n",
" \"trivial_target\": \"theorem certificate : True := by trivial\",\n",
" \"placeholder\": \"theorem hard_part : P := by sorry\",\n",
"}\n",
"\n",
"for name, text in examples.items():\n",
" flags = []\n",
" if \"sorry\" in text:\n",
" flags.append(\"placeholder proof\")\n",
" if \": True :=\" in text:\n",
" flags.append(\"trivial target\")\n",
" if \"by trivial\" in text:\n",
" flags.append(\"trivial proof tactic\")\n",
" print(name, flags or [\"needs semantic review\"])\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Exercises\n",
"\n",
"- Add a temporary Lean file under a scratch fixture with a theorem `: True := by trivial`. Run the scanner and inspect the issue.\n",
"- Explain why the same word in a comment should not be fatal by itself.\n",
"- Write a one-page checklist for reviewing a new `*-verified` repository before assigning any risk score above R2.\n"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"name": "python",
"pygments_lexer": "ipython3"
}
},
"nbformat": 4,
"nbformat_minor": 5
}

154
notebooks/05_third_party_attestation_provider.ipynb Normal file
View file

@ -0,0 +1,154 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Lecture 5: Third-Party Proof-Checking Attestations\n",
"\n",
"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.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Learning Objectives\n",
"\n",
"- Explain the trust transformation from local replay to provider attestation.\n",
"- Read a provider attestation.\n",
"- Verify an Ed25519 attestation signature.\n",
"- Understand why untrusted attestations must score R0.\n",
"- Distinguish a provider signature from transparency-log accountability.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Attestation Contents\n",
"\n",
"A useful attestation records:\n",
"\n",
"- provider identity,\n",
"- issue time,\n",
"- subject component, repo URL, repo commit, verification dir, kind, backend,\n",
"- Lean and lake versions,\n",
"- check log and axiom log locations,\n",
"- certificate names, statuses, observed axioms, expected axioms,\n",
"- provider signature metadata.\n",
"\n",
"The agent must verify both content and trust policy. A valid signature from an untrusted provider is not enough.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pathlib import Path\n",
"import sys\n",
"\n",
"repo_root = Path.cwd()\n",
"if not (repo_root / \"src\" / \"pacta\").exists():\n",
" repo_root = repo_root.parent\n",
"sys.path.insert(0, str(repo_root / \"src\"))\n",
"\n",
"from pacta.attestation import load_attestation\n",
"\n",
"attestation_path = repo_root / \"examples\" / \"dalek-ed25519.attestation.yaml\"\n",
"raw = load_attestation(attestation_path)\n",
"print(raw.keys())\n",
"print(raw[\"provider\"])\n",
"print(raw[\"subject\"])\n",
"print(raw[\"certificates\"][0])\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Trust Policy\n",
"\n",
"PACTA requires an explicit `--trust-attestation-provider` value. If the attestation provider does not match, the attestation is rejected.\n",
"\n",
"Real attestations should be signed. The included example fixture is unsigned and requires `--allow-unsigned-attestation`, which is suitable only for demos and tests.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pacta.attestation import validate_attestation\n",
"from pacta.config import RepoConfig\n",
"\n",
"repo = RepoConfig(\n",
" name=\"dalek-ed25519-verified\",\n",
" url=\"https://github.com/saymrwulf/dalek-ed25519-verified.git\",\n",
" kind=\"ed25519\",\n",
" verified_backend=\"serial/u64\",\n",
" certificates=[\n",
" \"CurveFieldProofs.fieldImplementation\",\n",
" \"CurveFieldProofs.edwardsImplementation\",\n",
" ],\n",
")\n",
"\n",
"trusted = validate_attestation(\n",
" raw,\n",
" repo,\n",
" path=attestation_path,\n",
" trusted_provider=\"example-proof-checker.invalid\",\n",
" allow_unsigned=True,\n",
")\n",
"untrusted = validate_attestation(raw, repo, path=attestation_path)\n",
"print(\"trusted accepted:\", trusted.accepted)\n",
"print(\"untrusted accepted:\", untrusted.accepted)\n",
"print(\"untrusted diagnostics:\", untrusted.diagnostics)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Provider Threat Model\n",
"\n",
"A proof-checking provider can be valuable, but it introduces new risks:\n",
"\n",
"- It may sign an incorrect result.\n",
"- Its environment may be stale or compromised.\n",
"- Its signing key may be stolen.\n",
"- It may equivocate by showing different results to different agents.\n",
"- It may lose log history.\n",
"\n",
"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.\"\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Exercises\n",
"\n",
"- Draw the trusted base for local replay and provider attestation. Mark what changes.\n",
"- Explain why a provider attestation must include repo commit, not only repo name.\n",
"- Design a monitoring rule that would detect if the provider changes the result for the same commit.\n"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"name": "python",
"pygments_lexer": "ipython3"
}
},
"nbformat": 4,
"nbformat_minor": 5
}

185
notebooks/06_merkle_transparency_logs.ipynb Normal file
View file

@ -0,0 +1,185 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Lecture 6: Merkle Transparency Logs\n",
"\n",
"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.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Learning Objectives\n",
"\n",
"- Implement leaf and node hashing with domain separation.\n",
"- Compute a Merkle root.\n",
"- Generate and verify inclusion proofs.\n",
"- Generate and verify consistency proofs.\n",
"- Explain Signed Tree Heads and signature policy.\n",
"- Explain why ML-DSA must fail closed when unavailable.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## RFC 9162 Hash Shape\n",
"\n",
"PACTA follows the Certificate Transparency hash structure:\n",
"\n",
"- Empty tree hash: `SHA256(\"\")`\n",
"- Leaf hash: `SHA256(0x00 || leaf_input)`\n",
"- Node hash: `SHA256(0x01 || left || right)`\n",
"\n",
"The prefix bytes prevent a leaf value from being confused with an internal node value.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pathlib import Path\n",
"import sys\n",
"\n",
"repo_root = Path.cwd()\n",
"if not (repo_root / \"src\" / \"pacta\").exists():\n",
" repo_root = repo_root.parent\n",
"sys.path.insert(0, str(repo_root / \"src\"))\n",
"\n",
"from pacta.transparency import (\n",
" leaf_hash,\n",
" node_hash,\n",
" merkle_root,\n",
" inclusion_proof,\n",
" verify_inclusion,\n",
" consistency_proof,\n",
" verify_consistency,\n",
")\n",
"\n",
"leaves = [f\"attestation-{i}\".encode() for i in range(1, 6)]\n",
"root = merkle_root(leaves)\n",
"print(root.hex())\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"for index, leaf in enumerate(leaves):\n",
" proof = inclusion_proof(leaves, index)\n",
" ok = verify_inclusion(leaf, index, len(leaves), proof, root)\n",
" print(index, ok, [node.hex()[:12] for node in proof])\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Consistency Proofs\n",
"\n",
"An inclusion proof answers: \"Is this leaf in this tree?\"\n",
"\n",
"A consistency proof answers: \"Is the newer tree an append-only extension of the older tree?\"\n",
"\n",
"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.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"old_size = 3\n",
"old_root = merkle_root(leaves[:old_size])\n",
"new_root = merkle_root(leaves)\n",
"proof = consistency_proof(leaves, old_size)\n",
"print(\"old:\", old_root.hex())\n",
"print(\"new:\", new_root.hex())\n",
"print(\"proof:\", [node.hex()[:12] for node in proof])\n",
"print(\"consistent:\", verify_consistency(old_size, len(leaves), old_root, new_root, proof))\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Signed Tree Heads\n",
"\n",
"A Signed Tree Head records:\n",
"\n",
"- log ID,\n",
"- tree size,\n",
"- timestamp,\n",
"- root hash,\n",
"- hash algorithm,\n",
"- signatures.\n",
"\n",
"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`.\n",
"\n",
"Policy matters:\n",
"\n",
"- `require-signatures ed25519`: verify Ed25519 and allow ML-DSA to be unavailable.\n",
"- `require-signatures both`: require Ed25519 and ML-DSA verified. If ML-DSA is unavailable, fail closed.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pacta.postquantum import detect_ml_dsa\n",
"\n",
"capability = detect_ml_dsa()\n",
"print(capability.available)\n",
"print(capability.backend)\n",
"print(capability.reason)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Why Ed25519 and ML-DSA Together?\n",
"\n",
"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.\n",
"\n",
"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.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Exercises\n",
"\n",
"- Tamper with one leaf and show that inclusion verification fails.\n",
"- Explain why the tree head signature must cover tree size as well as root hash.\n",
"- Write a policy for when an autonomous agent should require `both` signatures.\n",
"- Research checkpoint: compare PACTA's local prototype to production Certificate Transparency monitor/gossip requirements.\n"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"name": "python",
"pygments_lexer": "ipython3"
}
},
"nbformat": 4,
"nbformat_minor": 5
}

168
notebooks/07_agent_consequences.ipynb Normal file
View file

@ -0,0 +1,168 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Lecture 7: Agent Consequences\n",
"\n",
"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.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Learning Objectives\n",
"\n",
"- Explain how risk levels map to actions.\n",
"- Run a dry-run agent action.\n",
"- Understand the generated Rust capsule.\n",
"- Explain why R3 permits lower-layer use but denies wallet demos.\n",
"- Connect transparency receipts to build authorization.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Action Policy\n",
"\n",
"Current actions:\n",
"\n",
"- `build-library`: default threshold R3. Produces a proof-gated component capsule.\n",
"- `build-wallet-demo`: threshold R4. Writes a denial artifact below R4.\n",
"\n",
"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.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pathlib import Path\n",
"import sys\n",
"\n",
"repo_root = Path.cwd()\n",
"if not (repo_root / \"src\" / \"pacta\").exists():\n",
" repo_root = repo_root.parent\n",
"sys.path.insert(0, str(repo_root / \"src\"))\n",
"\n",
"from pacta.agent import run_agent_action\n",
"from pacta.claims import build_claim_card\n",
"from pacta.config import load_config\n",
"\n",
"repo = load_config(repo_root / \"examples\" / \"repos.yaml\").repo_named(\"dalek-ed25519-verified\")\n",
"card = build_claim_card(repo, repo_root / \"repos\" / repo.name, offline_fixture=True)\n",
"\n",
"library_decision = run_agent_action(card, \"build-library\", repo_root / \"artifacts-notebook\", dry_run=True)\n",
"wallet_decision = run_agent_action(card, \"build-wallet-demo\", repo_root / \"artifacts-notebook\", dry_run=True)\n",
"print(library_decision.to_dict())\n",
"print(wallet_decision.to_dict())\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## The Rust Capsule\n",
"\n",
"The generated capsule is not cryptographic code. It is a consumable policy artifact. It embeds the claim card and exposes constants such as:\n",
"\n",
"- component,\n",
"- repo URL,\n",
"- kind,\n",
"- verified backend,\n",
"- risk level,\n",
"- evidence mode,\n",
"- attestation provider,\n",
"- deployment constraints.\n",
"\n",
"Downstream automation can import this crate and check `allowed_for_lower_layer_crypto()` before enabling a code path.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"from pacta.artifact import _lib_rs\n",
"\n",
"print(_lib_rs(card).splitlines()[:24])\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Receipt-Required Builds\n",
"\n",
"The strongest dogfood path in this prototype is:\n",
"\n",
"1. Provider replays Lean and signs attestation.\n",
"2. Provider appends attestation to a Merkle transparency log.\n",
"3. Provider emits an inclusion receipt with Signed Tree Head.\n",
"4. Agent verifies provider signature, receipt inclusion proof, and STH signature.\n",
"5. Agent builds only if risk and transparency policy pass.\n",
"\n",
"This transforms \"I read a report\" into \"I accepted a logged, signed proof-check result and acted within its theorem boundary.\"\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Command-Line Lab\n",
"\n",
"Run these from the repository root after generating a provider attestation:\n",
"\n",
"```bash\n",
"pacta receipt-verify \\\n",
" --attestation provider/out/dalek-ed25519.attestation.yaml \\\n",
" --receipt provider/out/dalek-ed25519.receipt.yaml \\\n",
" --log-public-key provider/state/local-provider/provider.ed25519.pub\n",
"\n",
"pacta agent \\\n",
" --config examples/repos.yaml \\\n",
" --repo-name dalek-ed25519-verified \\\n",
" --repo repos/dalek-ed25519-verified \\\n",
" --attestation provider/out/dalek-ed25519.attestation.yaml \\\n",
" --trust-attestation-provider local-pacta-provider \\\n",
" --attestation-public-key provider/state/local-provider/provider.ed25519.pub \\\n",
" --transparency-receipt provider/out/dalek-ed25519.receipt.yaml \\\n",
" --transparency-log-public-key provider/state/local-provider/provider.ed25519.pub \\\n",
" --require-transparency-receipt \\\n",
" --action build-library\n",
"```\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Exercises\n",
"\n",
"- Modify a claim card to R2 and show that `build-library` is refused.\n",
"- Explain why a denial artifact is useful for auditability.\n",
"- Design a policy where an agent requires `both` Ed25519 and ML-DSA signatures for production deployment but allows Ed25519-only in a local lab.\n",
"- Write a downstream Rust pseudo-code snippet that imports the generated capsule before enabling a code path.\n"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"name": "python",
"pygments_lexer": "ipython3"
}
},
"nbformat": 4,
"nbformat_minor": 5
}

166
notebooks/08_capstone_research_program.ipynb Normal file
View file

@ -0,0 +1,166 @@
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Lecture 8: Capstone Research Program\n",
"\n",
"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.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Learning Objectives\n",
"\n",
"- Design a complete assurance roadmap from R3 to R4/R5.\n",
"- Identify proof gaps and operational gaps separately.\n",
"- Propose theorem milestones for Ed25519, Pallas/Pasta, and wallet integration.\n",
"- Design transparency-log monitoring and provider accountability.\n",
"- Write a PhD-quality research proposal with measurable deliverables.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## From R3 to R4\n",
"\n",
"R3 is lower-layer implementation evidence. Moving toward R4 requires end-to-end primitive coverage:\n",
"\n",
"- public API boundary,\n",
"- parsing and encoding,\n",
"- canonicality and rejection rules,\n",
"- scalar arithmetic,\n",
"- hash interface,\n",
"- signature equation,\n",
"- implementation boundary,\n",
"- connection from theorem names to actual deployed code paths.\n",
"\n",
"The hard part is not one theorem. The hard part is composing theorem coverage without smuggling in unreviewed assumptions.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## From R4 to R5\n",
"\n",
"R5 adds production assurance:\n",
"\n",
"- reproducible production builds,\n",
"- compiler and build-system assurance,\n",
"- side-channel analysis,\n",
"- hardware/KMS/MPC integration,\n",
"- key custody policy,\n",
"- operational controls,\n",
"- monitoring and incident response,\n",
"- transparency-log monitors and consistency checks.\n",
"\n",
"R5 is where formal methods meet systems security.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Research Milestone Template\n",
"\n",
"For each milestone, write:\n",
"\n",
"- Claim: exact theorem-boundary statement.\n",
"- Artifact: repository, commit, file paths, theorem names.\n",
"- Replay: how to reproduce compilation and axiom audit.\n",
"- Exclusions: what remains out of scope.\n",
"- Trusted base: tools, compiler, translation, provider, log, hardware.\n",
"- Risk impact: how the milestone changes R-level classification.\n",
"- Failure modes: what invalidates the evidence.\n"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"milestone = {\n",
" \"claim\": \"Scalar52 arithmetic correctness for selected serial/u64 code paths.\",\n",
" \"artifact\": [\"repo commit\", \"Lean files\", \"aggregate theorem name\"],\n",
" \"replay\": [\"portable Lean check\", \"#print axioms\", \"manifest coverage\"],\n",
" \"exclusions\": [\"SHA-512\", \"encoding\", \"side channels\", \"compiler correctness\"],\n",
" \"risk_impact\": \"May reduce one blocker toward R4 but does not by itself prove EdDSA.\",\n",
"}\n",
"for key, value in milestone.items():\n",
" print(key, \"=>\", value)\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Capstone Project Options\n",
"\n",
"1. Ed25519 R4 Roadmap\n",
" Build a theorem dependency map from field arithmetic to full signature verification. Identify every missing certificate and propose an order of attack.\n",
"\n",
"2. Pallas/Pasta Foundation Audit\n",
" Determine whether shipped Pallas/Pasta certificates prove add, mul, reduce, square, invert, and aggregate field implementation. Assign R2/R3 with rationale.\n",
"\n",
"3. Transparency Provider Hardening\n",
" Extend the provider with external monitors, persistent checkpoints, log consistency verification between checkpoints, and real ML-DSA signing when a backend is available.\n",
"\n",
"4. Agent Policy Language\n",
" Design a small declarative policy language that maps claim cards and transparency receipts to allowed actions.\n",
"\n",
"5. Translation Faithfulness Research\n",
" Study how to connect Rust source, transpiled Lean, and compiled artifacts with a defensible trusted base.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## PhD-Level Evaluation Rubric\n",
"\n",
"A top submission should:\n",
"\n",
"- Make claims that are precise enough to be wrong.\n",
"- Separate proof gaps from engineering gaps.\n",
"- Include runnable reproduction steps.\n",
"- Include negative tests and failure-mode demonstrations.\n",
"- Use transparency receipts or equivalent accountability for third-party evidence.\n",
"- Avoid marketing language.\n",
"- State exactly what would invalidate the result.\n",
"- Produce an artifact another researcher can inspect.\n"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Final Exercises\n",
"\n",
"- Write a two-page assurance case for using an R3 Ed25519 arithmetic capsule in a non-wallet lower-layer library.\n",
"- Write a denial memo explaining why the same evidence must not authorize a wallet.\n",
"- Design a monitoring protocol for PACTA transparency logs, including consistency checks and alert conditions.\n",
"- Propose a real ML-DSA integration plan that names the backend, key format, signature format, test vectors, and failure policy.\n",
"- Pick one theorem boundary and write the strongest claim you can defend without exaggeration.\n"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"name": "python",
"pygments_lexer": "ipython3"
}
},
"nbformat": 4,
"nbformat_minor": 5
}

18
notebooks/README.md Normal file
View file

@ -0,0 +1,18 @@
# 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,
- research roadmaps from R3 evidence toward R4/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.

1277
scripts/build_curriculum_notebooks.py Normal file
View file

File diff suppressed because it is too large Load diff

45
tests/test_curriculum_notebooks.py Normal file
View file

@ -0,0 +1,45 @@
import json
from pathlib import Path
EXPECTED_NOTEBOOKS = [
"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",
"07_agent_consequences.ipynb",
"08_capstone_research_program.ipynb",
]
def test_curriculum_notebooks_are_valid_and_output_free():
root = Path(__file__).resolve().parents[1]
notebook_dir = root / "notebooks"
assert sorted(path.name for path in notebook_dir.glob("*.ipynb")) == EXPECTED_NOTEBOOKS
for name in EXPECTED_NOTEBOOKS:
notebook = json.loads((notebook_dir / name).read_text(encoding="utf-8"))
assert notebook["nbformat"] == 4
assert notebook["nbformat_minor"] >= 5
assert notebook["cells"]
combined = "\n".join(
"".join(cell.get("source", []))
for cell in notebook["cells"]
if cell.get("cell_type") == "markdown"
)
assert "Learning Objectives" in combined
if name != "00_course_map.ipynb":
assert "Exercises" in combined
assert "# Lecture" in combined
for cell in notebook["cells"]:
if cell.get("cell_type") == "code":
assert cell.get("execution_count") is None
assert cell.get("outputs") == []
def test_notebook_readme_points_to_course_map():
readme = (Path(__file__).resolve().parents[1] / "notebooks" / "README.md").read_text(encoding="utf-8")
assert "00_course_map.ipynb" in readme
assert "zero-to-hero" in readme