{
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "# Lecture 5: Third-Party Proof-Checking Attestations\n",
        "\n",
        "Local proof replay can be operationally cumbersome. A specialized provider can run the Lean/Aeneas environment in a controlled setup and publish a signed attestation. This transforms trust in local compilation into trust in a provider, its environment, its signing key custody, and its transparency log.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Learning Objectives\n",
        "\n",
        "- Explain the trust transformation from local replay to provider attestation.\n",
        "- Read a provider attestation.\n",
        "- Verify an Ed25519 attestation signature.\n",
        "- Understand why untrusted attestations must score R0.\n",
        "- Distinguish a provider signature from transparency-log accountability.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Attestation Contents\n",
        "\n",
        "A useful attestation records:\n",
        "\n",
        "- provider identity,\n",
        "- issue time,\n",
        "- subject component, repo URL, repo commit, verification dir, kind, backend,\n",
        "- Lean and lake versions,\n",
        "- check log and axiom log locations,\n",
        "- certificate names, statuses, observed axioms, expected axioms,\n",
        "- provider signature metadata.\n",
        "\n",
        "The agent must verify both content and trust policy. A valid signature from an untrusted provider is not enough.\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.attestation import load_attestation\n",
        "\n",
        "attestation_path = repo_root / \"examples\" / \"dalek-ed25519.attestation.yaml\"\n",
        "raw = load_attestation(attestation_path)\n",
        "print(raw.keys())\n",
        "print(raw[\"provider\"])\n",
        "print(raw[\"subject\"])\n",
        "print(raw[\"certificates\"][0])\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Trust Policy\n",
        "\n",
        "PACTA requires an explicit `--trust-attestation-provider` value. If the attestation provider does not match, the attestation is rejected.\n",
        "\n",
        "Real attestations should be signed. The included example fixture is unsigned and requires `--allow-unsigned-attestation`, which is suitable only for demos and tests.\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "from pacta.attestation import validate_attestation\n",
        "from pacta.config import RepoConfig\n",
        "\n",
        "repo = RepoConfig(\n",
        "    name=\"dalek-ed25519-verified\",\n",
        "    url=\"https://github.com/saymrwulf/dalek-ed25519-verified.git\",\n",
        "    kind=\"ed25519\",\n",
        "    verified_backend=\"serial/u64\",\n",
        "    certificates=[\n",
        "        \"CurveFieldProofs.fieldImplementation\",\n",
        "        \"CurveFieldProofs.edwardsImplementation\",\n",
        "    ],\n",
        ")\n",
        "\n",
        "trusted = validate_attestation(\n",
        "    raw,\n",
        "    repo,\n",
        "    path=attestation_path,\n",
        "    trusted_provider=\"example-proof-checker.invalid\",\n",
        "    allow_unsigned=True,\n",
        ")\n",
        "untrusted = validate_attestation(raw, repo, path=attestation_path)\n",
        "print(\"trusted accepted:\", trusted.accepted)\n",
        "print(\"untrusted accepted:\", untrusted.accepted)\n",
        "print(\"untrusted diagnostics:\", untrusted.diagnostics)\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Provider Threat Model\n",
        "\n",
        "A proof-checking provider can be valuable, but it introduces new risks:\n",
        "\n",
        "- It may sign an incorrect result.\n",
        "- Its environment may be stale or compromised.\n",
        "- Its signing key may be stolen.\n",
        "- It may equivocate by showing different results to different agents.\n",
        "- It may lose log history.\n",
        "\n",
        "This is why transparency logging matters. A signature says \"this provider signed this.\" A transparency receipt says \"this signed result is included in an append-only public structure at this tree head.\"\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Real evidence, checked in this cell\n",
        "\n",
        "Everything above used schema fixtures. The repository now ships REAL provider evidence under `evidence/`: signed attestations from a guarded Lean replay of all four verified repositories (~30 minutes of kernel re-checking per fork), each recording the repo commit, the machine-protection block, and all sixteen certificates with their observed axiom cones. Read one and re-derive its verdicts locally - never trust the provider's own labels:\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "from pacta.attestation import load_attestation, _normalize_certificate\n",
        "from pacta.config import load_config\n",
        "from pacta.profiles import get_profile\n",
        "from pacta.signing import verify_attestation_signature_detailed\n",
        "\n",
        "config = load_config(repo_root / \"examples\" / \"repos.yaml\")\n",
        "repo = config.repo_named(\"dalek-ed25519-verified\")\n",
        "profile = get_profile(\"ed25519\", repo)\n",
        "att = load_attestation(repo_root / \"evidence\" / \"dalek-ed25519.attestation.yaml\")\n",
        "\n",
        "ok, error, backend = verify_attestation_signature_detailed(att, repo_root / \"evidence\" / \"provider.ed25519.pub\")\n",
        "print(\"signature valid:\", ok, \"| verified on backend:\", backend)\n",
        "print(\"subject commit:\", att[\"subject\"][\"repo_commit\"][:12])\n",
        "print(\"machine protection:\", att[\"machine_protection\"][\"lean_guard\"].rsplit(\"/\", 2)[-1])\n",
        "\n",
        "rederived = [_normalize_certificate(cert, profile) for cert in att[\"certificates\"]]\n",
        "clean = sum(1 for cert in rederived if cert[\"status\"] == \"proven\" and cert[\"axiom_status\"] == \"clean\")\n",
        "print(f\"re-derived locally: {clean}/{len(rederived)} proven with boundary-exact cones\")\n",
        "apex = [cert for cert in rederived if cert[\"name\"].endswith(\"_decompress\")][0]\n",
        "print(\"full-lift tier observed cone:\", apex[\"observed_axioms\"])\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Exercises\n",
        "\n",
        "- Draw the trusted base for local replay and provider attestation. Mark what changes.\n",
        "- Explain why a provider attestation must include repo commit, not only repo name.\n",
        "- Design a monitoring rule that would detect if the provider changes the result for the same commit.\n"
      ]
    }
  ],
  "metadata": {
    "kernelspec": {
      "display_name": "Python 3",
      "language": "python",
      "name": "python3"
    },
    "language_info": {
      "name": "python",
      "pygments_lexer": "ipython3"
    }
  },
  "nbformat": 4,
  "nbformat_minor": 5
}