proof-aware-crypto-tooling-agent/notebooks/08_capstone_research_program.ipynb

{
  "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
}