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