proof-aware-crypto-tooling-agent/notebooks/00_course_map.ipynb

{
  "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, why ML-DSA requires a real backend, and how the shipped SLH-DSA co-signature differs from both.\n",
        "- Design policy gates that convert verification evidence into consequences.\n",
        "- Read R4 four-tier apex evidence, name its residual blockers, and write a research plan toward 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`, then the MIRRORED PAIR\n",
        "   `06a_provider_build_the_log.ipynb` / `06b_agent_verify_inclusion.ipynb`\n",
        "\n",
        "   The trust architecture has exactly two domains - ONE provider\n",
        "   who builds and signs the authenticated structure (and pays the\n",
        "   Lean bill), MANY agents who verify inclusion proofs in\n",
        "   milliseconds. The course mirrors that split structurally: 6a is\n",
        "   written entirely in the provider's voice, 6b entirely in the\n",
        "   agent's. If you cannot say which notebook a step belongs to,\n",
        "   you have not understood the step.\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 R4 toward R5.\n",
        "\n",
        "9. `09_dogfood_verified_crypto.ipynb`\n",
        "\n",
        "   Eat your own dogfood: run the agent's own signature checks through the proven code path, and hold the post-quantum line honestly.\n",
        "\n",
        "## The Ratchet Rule\n",
        "\n",
        "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.\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
}