mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-03 19:53:43 +00:00
mrwulf
1086a3ba02
The 14-notebook course predated the post-quantum campaign entirely (coherence findings 10, 11). Now, authored in the GENERATOR and regenerated (AGENTS.md rule): - notebook 06: new section 'The second signature that actually shipped: SLH-DSA' — the deterministic co-signature since tree size 14, chosen because the log attests its own parameter set's verify path (leaf 18, 11 certs); absent-not-failed for older heads; determinism as an audit primitive; verify-only always. Plus a runnable keygen/sign/verify/ re-sign-byte-equality demo (honest skip below OpenSSL 3.5) and the --slhdsa-public-key consumer flag in the policy list. - notebook 09: the 'post-quantum line' is now three-legged — Ed25519 proven-verify dogfood, SLH-DSA shipped-and-attested, ML-DSA required- but-honest-unavailable — with the closing point that a slot stops being aspirational the day its verify path enters the log; stale 16/16 provenance count -> 44/44 (leaf 13 re-attestation). - notebook 07: policy exercise extended with the co-signature question; 00 course map goal updated; README course listing for 06/09. - GENERATOR DRIFT REPAIRED in passing: notebook 10's cockpit cell had been added to the .ipynb but never backported to the generator — regeneration would have silently dropped it; the cell is now IN the generator and round-trips (19 cells, content identical). Suite 157 green.
222 lines
9 KiB
Text
222 lines
9 KiB
Text
{
|
|
"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",
|
|
"- Run the gate both ways: a partial (arithmetic-only) card is denied; the full four-tier card is allowed.\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 - 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.\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": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"# NAPKIN: an arithmetic-only card faces the wallet gate - DENIED.\n",
|
|
"from pathlib import Path\n",
|
|
"import sys, tempfile\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.risk import score_claim_card\n",
|
|
"\n",
|
|
"partial = {\n",
|
|
" \"component\": \"napkin-arithmetic-only\",\n",
|
|
" \"kind\": \"ed25519\",\n",
|
|
" \"certificates\": [\n",
|
|
" {\"name\": \"CurveFieldProofs.fieldImplementation\", \"status\": \"proven\", \"axiom_status\": \"clean\"},\n",
|
|
" {\"name\": \"CurveFieldProofs.edwardsImplementation\", \"status\": \"proven\", \"axiom_status\": \"clean\"},\n",
|
|
" ],\n",
|
|
" \"exclusions\": [\"full EdDSA signature verification\"],\n",
|
|
" \"meta\": {\"r4_requirements\": []},\n",
|
|
"}\n",
|
|
"partial[\"risk\"] = score_claim_card(partial).to_dict()\n",
|
|
"with tempfile.TemporaryDirectory() as tmp:\n",
|
|
" decision = run_agent_action(partial, \"build-wallet-demo\", tmp, dry_run=True)\n",
|
|
" print(\"allowed:\", decision.allowed, \"at\", decision.risk_level)\n",
|
|
" print(decision.rationale)\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"# REAL: the shipped four-tier R4 card faces the same gate - ALLOWED\n",
|
|
"# (a demo scaffold only; the residual blockers ride along in the card).\n",
|
|
"from pacta.yamlio import load_data\n",
|
|
"\n",
|
|
"full = load_data(repo_root / \"examples\" / \"dalek-ed25519.claims.yaml\")\n",
|
|
"with tempfile.TemporaryDirectory() as tmp:\n",
|
|
" decision = run_agent_action(full, \"build-wallet-demo\", tmp, dry_run=True)\n",
|
|
" print(\"allowed:\", decision.allowed, \"at\", decision.risk_level)\n",
|
|
" print(decision.rationale)\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",
|
|
"- Extend it: when should the agent also require the SLH-DSA co-signature, given that heads before tree size 14 legitimately lack it?\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
|
|
}
|