proof-aware-crypto-tooling-agent/notebooks/04_proof_hygiene_and_boundaries.ipynb

{
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "# Lecture 4: Proof Hygiene and Boundaries\n",
        "\n",
        "Proof hygiene is the discipline of checking whether formal artifacts have obvious escape hatches or misleading theorem surfaces. It does not replace proof checking. It catches common ways a proof corpus can look stronger than it is.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Learning Objectives\n",
        "\n",
        "- Detect `sorry`, local `axiom`, trivial theorem targets, and suspicious `by trivial`.\n",
        "- Understand why comments should not be treated as fatal proof failures.\n",
        "- Explain why manifest coverage matters.\n",
        "- Distinguish a hygiene warning from a replay failure.\n",
        "- Write precise boundary language for proof reports.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Patterns PACTA Scans For\n",
        "\n",
        "- `sorry`\n",
        "- `axiom` declarations under `Proofs/`\n",
        "- theorem targets such as `: True :=`\n",
        "- suspicious `by trivial` in spec/certificate/root files\n",
        "- `native_decide` as advisory unless dependency-cone analysis is stronger\n",
        "- missing certificate names\n",
        "- proof files not included in a manifest when a manifest exists\n",
        "\n",
        "A simple scanner may over-warn. It must not over-claim.\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.audit import scan_hygiene\n",
        "from pacta.manifest import discover_layout\n",
        "\n",
        "fixture = repo_root / \"tests\" / \"fixtures\" / \"mini-ed25519-verified\"\n",
        "layout = discover_layout(fixture, \"verification\")\n",
        "issues = scan_hygiene(layout, [\"CurveFieldProofs.fieldImplementation\"])\n",
        "print(\"issues:\", issues)\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Why `sorry` Is Serious\n",
        "\n",
        "In Lean, `sorry` can stand in for a proof. Depending on settings, it may allow a theorem to exist without its proof being completed. In a verification-evidence pipeline, unresolved `sorry` must block high-confidence claims.\n",
        "\n",
        "The lesson is not \"never prototype with placeholders.\" The lesson is \"never ship assurance claims that hide placeholders.\"\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Why Local Axioms Are Serious\n",
        "\n",
        "A local axiom can assert the result directly. For example:\n",
        "\n",
        "```lean\n",
        "axiom fieldImplementation : CorrectFieldImplementation\n",
        "```\n",
        "\n",
        "That may be useful for bootstrapping a model, but it is not proof evidence for implementation correctness. PACTA flags local axioms under `Proofs/` because they may collapse the intended theorem into an assumption.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Trivial Theorems and Spec Drift\n",
        "\n",
        "A theorem target like `: True := by trivial` proves exactly nothing about cryptographic code. A more subtle failure is spec drift: the theorem proves a property, but not the property the system needs.\n",
        "\n",
        "Professional review asks two questions:\n",
        "\n",
        "1. Is the proof complete?\n",
        "2. Is the theorem the right theorem?\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "# A tiny reviewer helper: classify theorem statements by obvious risk.\n",
        "examples = {\n",
        "    \"good_shape\": \"theorem add_denote ... : denote (add x y) = x + y := ...\",\n",
        "    \"trivial_target\": \"theorem certificate : True := by trivial\",\n",
        "    \"placeholder\": \"theorem hard_part : P := by sorry\",\n",
        "}\n",
        "\n",
        "for name, text in examples.items():\n",
        "    flags = []\n",
        "    if \"sorry\" in text:\n",
        "        flags.append(\"placeholder proof\")\n",
        "    if \": True :=\" in text:\n",
        "        flags.append(\"trivial target\")\n",
        "    if \"by trivial\" in text:\n",
        "        flags.append(\"trivial proof tactic\")\n",
        "    print(name, flags or [\"needs semantic review\"])\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Exercises\n",
        "\n",
        "- Add a temporary Lean file under a scratch fixture with a theorem `: True := by trivial`. Run the scanner and inspect the issue.\n",
        "- Explain why the same word in a comment should not be fatal by itself.\n",
        "- Write a one-page checklist for reviewing a new `*-verified` repository before assigning any risk score above R2.\n"
      ]
    }
  ],
  "metadata": {
    "kernelspec": {
      "display_name": "Python 3",
      "language": "python",
      "name": "python3"
    },
    "language_info": {
      "name": "python",
      "pygments_lexer": "ipython3"
    }
  },
  "nbformat": 4,
  "nbformat_minor": 5
}