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": [
        "## R4, achieved - read it like an auditor\n",
        "\n",
        "When this course was first drafted, R4 was the roadmap. The corpus then delivered it (2026-07-06): scalar arithmetic, encoding/decoding canonicality, constructive decompression, and the four-tier signature apex, every certificate's axiom cone pinned to its documented boundary by each repository's own check script. The composition lesson stands: the hard part was never one theorem - it was composing coverage without smuggling assumptions, which is why the apex tiers are hypothesis-parametric (parser outcomes stay hypotheses) and why the boundary is enforced per certificate, in both directions.\n",
        "\n",
        "Your first capstone exercise is therefore no longer \"design R4\" but \"audit R4\": take the shipped claim card, list what each of the four tiers states, and name the exact residual trusted base. Then design the discharge plan:\n",
        "\n",
        "- byte-level specs for the wire parsers and legacy filters (turn the parse hypotheses into theorems),\n",
        "- a verified SHA-512 or a proof-carrying hash oracle (shrink the boundary),\n",
        "- signing-side coverage (nonce derivation, signer correctness),\n",
        "- the production-path mapping per fork (anza's default verify() is NOT the verified path - what would it take to cover it?).\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
}