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.
229 lines
10 KiB
Text
229 lines
10 KiB
Text
{
|
|
"cells": [
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"# Lecture 11: The Customer's-Eye View \u2014 You Hold the Ruler\n",
|
|
"\n",
|
|
"Every earlier lecture looked at the log from the *operator's*\n",
|
|
"side: replaying proofs, signing attestations, building the\n",
|
|
"tree. This one flips the telescope. You are now a customer \u2014 an\n",
|
|
"agent, a wallet, a developer \u2014 who wants to trust one of the\n",
|
|
"four verified Ed25519 forks and has no theorem prover, no Lean,\n",
|
|
"no desire to spend hours re-checking anything. What actually\n",
|
|
"happens on your side? The answer reframes the whole system, and\n",
|
|
"it is the most intuitive on-ramp to it.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Learning Objectives\n",
|
|
"\n",
|
|
"- Separate the three roles that a verification touches:\n",
|
|
" *measurement* (operator), *publication* (the log), and\n",
|
|
" *judgment* (you) \u2014 and see that only the last is yours.\n",
|
|
"- Understand the \"allowed axioms\" list as a **requirements\n",
|
|
" card** you own, can read, and could write yourself.\n",
|
|
"- Explain why a self-written card meeting the supply *exactly*\n",
|
|
" is engineered, not coincidental.\n",
|
|
"- State the three honest outcomes when your card is stricter\n",
|
|
" than the supply: relax (itemized), walk away, or grow the\n",
|
|
" supply.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## The card is a requirements card \u2014 and ideally you write it\n",
|
|
"\n",
|
|
"The list of axioms a certificate is *allowed* to rest on is not\n",
|
|
"handed to you by the operator at verification time. It ships\n",
|
|
"inside your own tooling (the ed25519 profile), on your disk,\n",
|
|
"versioned by you. A maximally paranoid customer ignores the\n",
|
|
"shipped copy and writes the card from first principles:\n",
|
|
"\n",
|
|
"> *\"I accept Lean's three foundational axioms, because that is\n",
|
|
"> what the proof kernel's logic IS. For the signature-tier\n",
|
|
"> theorems I accept named placeholders for SHA-512 and the wire\n",
|
|
"> format, because RFC 8032 tells me those parts exist and I can\n",
|
|
"> see they are declared, not smuggled. Nothing else.\"*\n",
|
|
"\n",
|
|
"That is a wish-list: the assumptions you are willing to live\n",
|
|
"under. Call it your ruler.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"import sys, pathlib\n",
|
|
"for parent in [pathlib.Path.cwd(), *pathlib.Path.cwd().parents]:\n",
|
|
" if (parent / \"src\" / \"pacta\").exists():\n",
|
|
" sys.path.insert(0, str(parent / \"src\")); break\n",
|
|
"\n",
|
|
"# A customer writes their OWN card, from first principles - no\n",
|
|
"# peeking at the operator. Lean's three, plus named oracle slots.\n",
|
|
"my_card = {\n",
|
|
" \"foundational\": {\"propext\", \"Classical.choice\", \"Quot.sound\"},\n",
|
|
" \"apex_oracle_allowed\": {\n",
|
|
" \"sha2.Sha512\", \"verifying.sha512_new\",\n",
|
|
" \"verifying.sha512_update\", \"verifying.sha512_finalize_bytes\",\n",
|
|
" \"ed25519.Signature\", \"ed25519.Signature.to_bytes\",\n",
|
|
" \"signature.error.Error\", \"signature.error.Error.new\",\n",
|
|
" },\n",
|
|
"}\n",
|
|
"print(\"my requirements card:\", sum(len(v) for v in my_card.values()), \"named assumptions\")\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Wish meets supply \u2014 and it is no accident\n",
|
|
"\n",
|
|
"Now compare your self-written card against what the four forks\n",
|
|
"actually declare. They match. That convergence is *engineered*:\n",
|
|
"the supply was deliberately shrunk \u2014 every axiom made to justify\n",
|
|
"its existence \u2014 so that any reasonable person's independently\n",
|
|
"written card lands on the same minimal list. When the wish meets\n",
|
|
"the supply exactly, it is because the supplier spent months\n",
|
|
"making the supply as small as honesty allows.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"from pacta.profiles.ed25519 import APEX_BOUNDARIES\n",
|
|
"\n",
|
|
"# The supply: the apex-tier certificate's documented, allowed\n",
|
|
"# axiom cone for the upstream fork - the exact set the strongest\n",
|
|
"# theorem is permitted to rest on, nothing more, nothing less.\n",
|
|
"supply = set(APEX_BOUNDARIES[\"dalek-wrappers\"])\n",
|
|
"wish = my_card[\"foundational\"] | my_card[\"apex_oracle_allowed\"]\n",
|
|
"print(\"supply == my wish:\", supply == wish)\n",
|
|
"print(\"axioms in supply my card did not anticipate:\", (supply - wish) or \"none\")\n",
|
|
"print(\"axioms my card wanted that are absent:\", (wish - supply) or \"none\")\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## The three roles, kept apart\n",
|
|
"\n",
|
|
"It is tempting to say \"the inclusion proof proves the Lean proof\n",
|
|
"is about my card.\" It does not, and the precision matters:\n",
|
|
"\n",
|
|
"| role | who | what it establishes |\n",
|
|
"|---|---|---|\n",
|
|
"| measurement | operator's kernel run | \"this theorem rests on exactly these named axioms\" (recorded verbatim in the attestation) |\n",
|
|
"| publication | the transparency log | \"this measurement is in the permanent record, shown identically to everyone\" (the inclusion proof + signed head) |\n",
|
|
"| judgment | **you** | \"these observed axioms are inside my allowed card\" (re-derived locally, every time) |\n",
|
|
"\n",
|
|
"Only judgment is yours, and it is the only step that involves an\n",
|
|
"opinion. The operator is trusted to *copy down what the kernel\n",
|
|
"printed* \u2014 never to interpret it.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## If you are happy \u2014 you are already finished\n",
|
|
"\n",
|
|
"If your card covers the observed cone, verification is: check\n",
|
|
"one signature, walk ~4 hashes to the signed root, compare cones\n",
|
|
"to your card. Milliseconds, standard library, no Lean. Done.\n",
|
|
"\n",
|
|
"## If you are NOT happy \u2014 there is nothing to negotiate\n",
|
|
"\n",
|
|
"Suppose your card is stricter: *\"I require SHA-512 itself\n",
|
|
"proven, not an oracle.\"* The system has no sales pitch for you.\n",
|
|
"Its entire answer is an **itemized** statement of the gap:\n",
|
|
"*not in supply; SHA-512-proven is the R5 frontier; here is the\n",
|
|
"exact list of what you would be accepting if you proceed\n",
|
|
"anyway.* Your decision is never \"lower my standards\" in the\n",
|
|
"abstract \u2014 it is a named line item: *SHA-512 as oracle: yes/no.*\n",
|
|
"Informed compromise, not diffuse trust.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "code",
|
|
"execution_count": null,
|
|
"metadata": {},
|
|
"outputs": [],
|
|
"source": [
|
|
"# The honest gap, itemized. A stricter customer wants no hash oracle.\n",
|
|
"strict_card = my_card[\"foundational\"] # foundational ONLY, no oracle slots\n",
|
|
"gap = supply - strict_card\n",
|
|
"print(\"this customer must explicitly accept, or walk away:\")\n",
|
|
"for ax in sorted(gap):\n",
|
|
" print(\" -\", ax)\n",
|
|
"print()\n",
|
|
"print(\"verdict for the strict card:\", \"PASSES\" if supply <= strict_card else \"REFUSED (gap above)\")\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## The third option: grow the supply\n",
|
|
"\n",
|
|
"The gap between anyone's dream card and today's supply is a\n",
|
|
"to-do list, not a wall. Prove SHA-512, certify the wire\n",
|
|
"parsers, and the new certificates enter the same log \u2014 and\n",
|
|
"stricter cards start passing. The log is additive in exactly\n",
|
|
"the way requirements are.\n",
|
|
"\n",
|
|
"**So: you hold the ruler. If your ruler is stricter than our\n",
|
|
"supply, your ruler is our roadmap.** That is the quiet\n",
|
|
"invitation built into the whole design.\n"
|
|
]
|
|
},
|
|
{
|
|
"cell_type": "markdown",
|
|
"metadata": {},
|
|
"source": [
|
|
"## Exercises\n",
|
|
"\n",
|
|
"- Write your own requirements card for the *foundational*\n",
|
|
" (non-signature) certificates from scratch. Those certificates\n",
|
|
" are expected to carry exactly Lean's three standard axioms\n",
|
|
" (`propext`, `Classical.choice`, `Quot.sound`) and nothing\n",
|
|
" else - did your card guess exactly those three?\n",
|
|
"- A vendor's attestation says `status: proven`. Explain in two\n",
|
|
" sentences why your tooling ignores that field entirely, and\n",
|
|
" what it looks at instead.\n",
|
|
"- You require reproducible builds. Is that a card you can write\n",
|
|
" today and have pass? Name the tier that gap belongs to, and\n",
|
|
" what would have to enter the log to close it.\n",
|
|
"- Argue both sides: is \"wish meets supply exactly\" a strength\n",
|
|
" (minimal, auditable) or a weakness (the same author wrote the\n",
|
|
" card and the supply)? What single action by a customer\n",
|
|
" settles the argument in their favor?\n"
|
|
]
|
|
}
|
|
],
|
|
"metadata": {
|
|
"kernelspec": {
|
|
"display_name": "Python 3",
|
|
"language": "python",
|
|
"name": "python3"
|
|
},
|
|
"language_info": {
|
|
"name": "python",
|
|
"pygments_lexer": "ipython3"
|
|
}
|
|
},
|
|
"nbformat": 4,
|
|
"nbformat_minor": 5
|
|
}
|