proof-aware-crypto-tooling-agent/notebooks/03_lean_replay_and_axiom_audit.ipynb

{
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "# Lecture 3: Lean Replay and Axiom Audit\n",
        "\n",
        "The verified repositories already contain Lean artifacts. PACTA does not run Charon, Aeneas, extraction, or Rust-to-Lean regeneration. It treats shipped Lean files as the verification artifact and focuses on replaying and inspecting them.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Learning Objectives\n",
        "\n",
        "- Explain the difference between transpilation and proof replay.\n",
        "- Understand how PACTA discovers Lean files and manifests.\n",
        "- Build a portable Lean invocation without Linux-only shell helpers.\n",
        "- Explain `#print axioms` and why axiom sets matter.\n",
        "- Diagnose missing Lean/lake or missing pinned Aeneas environments.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Why Not Run Charon/Aeneas?\n",
        "\n",
        "The corpus policy is strict:\n",
        "\n",
        "- The transpilation work is finished in the verified repos.\n",
        "- Re-running extraction could create a different artifact and confuse the trust story.\n",
        "- The current task is to interpret, replay, summarize, and score the existing Lean proof artifacts.\n",
        "\n",
        "For a production assurance case, translation faithfulness remains part of the trusted base unless separately proven.\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.manifest import discover_layout\n",
        "\n",
        "fixture = repo_root / \"tests\" / \"fixtures\" / \"mini-ed25519-verified\"\n",
        "layout = discover_layout(fixture, \"verification\")\n",
        "print(\"verification_dir:\", layout.verification_dir)\n",
        "print(\"files:\")\n",
        "for path in layout.compile_order:\n",
        "    print(\" \", path.relative_to(fixture))\n",
        "print(\"warnings:\", layout.warnings)\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Portable Lean Invocation\n",
        "\n",
        "PACTA avoids repository `check.sh` scripts because those may assume Linux-only tools like `free`, `taskset`, or GNU `timeout`. Instead it uses Python `subprocess.run(..., timeout=...)` and constructs a Lean environment where `verification/gen` and `verification` are visible through `LEAN_PATH`.\n",
        "\n",
        "If a pinned Aeneas Lean project is needed, PACTA can source a configured environment script and run `lake env lean`. It still does not run extraction.\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "from pacta.lean import LeanTools, build_lean_invocation\n",
        "\n",
        "tools = LeanTools(lean=\"/usr/bin/lean\", lake=\"/usr/bin/lake\")\n",
        "example_file = layout.compile_order[0]\n",
        "print(build_lean_invocation(example_file, tools, use_lake_env=True, output_path=example_file.with_suffix(\".olean\")))\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Axiom Audit\n",
        "\n",
        "A theorem can compile while depending on unexpected axioms. For the Ed25519 arithmetic profiles, the expected axiom set is usually:\n",
        "\n",
        "- `propext`\n",
        "- `Classical.choice`\n",
        "- `Quot.sound`\n",
        "\n",
        "PACTA generates a temporary Lean file with imports such as:\n",
        "\n",
        "```lean\n",
        "import Proofs.FieldMain\n",
        "import Proofs.EdMain\n",
        "#print axioms CurveFieldProofs.fieldImplementation\n",
        "#print axioms CurveFieldProofs.edwardsImplementation\n",
        "```\n",
        "\n",
        "It then parses Lean output and marks the result clean only when observed axioms match the expected set.\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "from pacta.lean import parse_axiom_output\n",
        "\n",
        "output = \"\"\"'CurveFieldProofs.fieldImplementation' depends on axioms:\n",
        "[propext, Classical.choice, Quot.sound]\n",
        "'CurveFieldProofs.edwardsImplementation' depends on axioms:\n",
        "[propext, Classical.choice, Quot.sound]\n",
        "\"\"\"\n",
        "parsed = parse_axiom_output(\n",
        "    output,\n",
        "    [\n",
        "        \"CurveFieldProofs.fieldImplementation\",\n",
        "        \"CurveFieldProofs.edwardsImplementation\",\n",
        "    ],\n",
        ")\n",
        "print(parsed)\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Local Replay Failure Modes\n",
        "\n",
        "Important distinctions:\n",
        "\n",
        "- Missing `lean`: local verifier capability unavailable.\n",
        "- Missing `lake`: local project environment may be unavailable.\n",
        "- Missing Aeneas Lean project: local replay unavailable for repos that depend on it.\n",
        "- Lean file fails: proof replay failed in this environment.\n",
        "- Axiom set dirty: theorem depends on unexpected assumptions.\n",
        "\n",
        "These are not the same. A professional report must state which one happened.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Exercises\n",
        "\n",
        "- Run `pacta doctor --config examples/repos.yaml --repo-name dalek-ed25519-verified` and classify the result.\n",
        "- Create a fake axiom output with an extra axiom. Parse it and explain why the result should be dirty.\n",
        "- Explain why a replay runner should not silently fall back from failure to an offline fixture.\n"
      ]
    }
  ],
  "metadata": {
    "kernelspec": {
      "display_name": "Python 3",
      "language": "python",
      "name": "python3"
    },
    "language_info": {
      "name": "python",
      "pygments_lexer": "ipython3"
    }
  },
  "nbformat": 4,
  "nbformat_minor": 5
}