proof-aware-crypto-tooling-agent/notebooks/01_threat_model_and_truth_boundary.ipynb

{
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "# Lecture 1: Threat Model and Truth Boundary\n",
        "\n",
        "The motivating system is an autonomous economic agent that may move stablecoins. It faces two broad attack classes:\n",
        "\n",
        "1. Psychological or game-theoretic attacks that trick the agent into harmful financial actions.\n",
        "2. Implementation attacks against the cryptographic and tooling stack that protects keys, signatures, proofs, and policy gates.\n",
        "\n",
        "PACTA focuses on the second class. It does not decide trades, call RPC endpoints, manage custody, or build wallets. It evaluates formal-verification-enhanced tooling and decides whether a constrained component can be used in a funds-protecting path.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Learning Objectives\n",
        "\n",
        "- Define a threat model for proof-aware cryptographic tooling.\n",
        "- Explain why lower-layer arithmetic proofs do not imply wallet safety.\n",
        "- State the strongest current Ed25519-family claim in theorem-boundary language.\n",
        "- List common exclusions that remain outside the proof artifact.\n",
        "- Explain why an autonomous agent needs consequences, not just reports.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## The Core Truth Boundary\n",
        "\n",
        "The strongest current Ed25519-family claim in this project is approximately:\n",
        "\n",
        "For selected curve25519-dalek / Solana-Ed25519-family Rust code paths already transpiled into Lean, the verified repositories contain Lean-checked certificates for field arithmetic over `F_p`, `p = 2^255 - 19`, and complete twisted Edwards point-operation laws, under explicit invariants and backend constraints.\n",
        "\n",
        "That is valuable. And since 2026-07-06 the corpus goes much further: all four ed25519 repositories carry a FOUR-TIER signature apex, button-enforced per fork, up to the full lift - the extracted verifier accepts iff the signature's R decompresses to a valid on-curve point equal to [k](-A)+[s]B. What it is still NOT: a wallet proof, a proof of SHA-512, a proof of the wire parsers (their outcomes are hypotheses), a signing-side proof, or a proof of all Solana transaction behavior. Naming both lists - what is proven and what is not - is the entire discipline of this course.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Proven or High-Value Evidence\n",
        "\n",
        "A clean R3-style Ed25519 arithmetic result may cover:\n",
        "\n",
        "- FieldElement51 arithmetic over `F_p` through denotation.\n",
        "- Panic and overflow freedom under limb-bound preconditions.\n",
        "- Complete Edwards point operations under `ExtValid` and `OnCurveExt`.\n",
        "- Implementation laws through denotation.\n",
        "- Axiom audit expected to show only standard Lean axioms: `propext`, `Classical.choice`, `Quot.sound`.\n",
        "\n",
        "The exact theorem names matter. In the current target repos, important certificates include:\n",
        "\n",
        "- `CurveFieldProofs.fieldImplementation`\n",
        "- `CurveFieldProofs.edwardsImplementation`\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Explicit Exclusions\n",
        "\n",
        "Do not let a lower-layer theorem leak into claims about:\n",
        "\n",
        "- Full EdDSA signature verification.\n",
        "- Complete Scalar52 arithmetic unless separately proven.\n",
        "- SHA-512.\n",
        "- Encoding, decoding, and canonicality unless separately proven.\n",
        "- Rust compiler correctness.\n",
        "- Charon/Aeneas translation faithfulness.\n",
        "- Side-channel resistance.\n",
        "- SIMD, AVX, hardware, zkVM, accelerator, or syscall paths.\n",
        "- Wallet policy, transaction construction, RPC, chain, oracle, market, or LLM decision safety.\n",
        "\n",
        "A professional assurance case is often mostly about preventing evidence from being overextended.\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",
        "from pacta.config import load_config\n",
        "\n",
        "config = load_config(repo_root / \"examples\" / \"repos.yaml\")\n",
        "for repo in config.repos:\n",
        "    print(f\"{repo.name:32} kind={repo.kind:13} backend={repo.verified_backend}\")\n",
        "    if repo.backend_warning:\n",
        "        print(f\"  backend warning: {repo.backend_warning}\")\n",
        "    if repo.known_status:\n",
        "        print(f\"  known status: {repo.known_status}\")\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Consequences\n",
        "\n",
        "PACTA turns evaluation into operational consequences:\n",
        "\n",
        "- If evidence is R0/R1/R2, do not build or consume lower-layer crypto capsules.\n",
        "- If evidence is R3, a constrained lower-layer component capsule may be built.\n",
        "- If evidence is below R4, wallet demo construction is refused.\n",
        "- If a third-party attestation is required but not trusted, the score falls to R0.\n",
        "- If a transparency receipt is required but invalid or absent, the score falls to R0.\n",
        "\n",
        "This makes verification a gate, not a decorative badge.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Checkpoint Questions\n",
        "\n",
        "1. Why does a proof of field arithmetic not prove transaction construction?\n",
        "2. What would have to be proven before full EdDSA verification could plausibly reach R4?\n",
        "3. Why is \"the proof failed to replay locally\" different from \"the theorem is false\"?\n",
        "4. Why should a zkVM accelerator path be excluded unless the repo proves otherwise?\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Exercises\n",
        "\n",
        "- Pick one configured repository from `examples/repos.yaml`. Write three precise claims that PACTA may make about it and three claims PACTA must refuse.\n",
        "- Rewrite the sentence \"this is verified Ed25519\" into a theorem-boundary statement that a security reviewer would accept.\n",
        "- Create a table mapping each exclusion above to the attack class it leaves open.\n"
      ]
    }
  ],
  "metadata": {
    "kernelspec": {
      "display_name": "Python 3",
      "language": "python",
      "name": "python3"
    },
    "language_info": {
      "name": "python",
      "pygments_lexer": "ipython3"
    }
  },
  "nbformat": 4,
  "nbformat_minor": 5
}