proof-aware-crypto-tooling-agent/notebooks/11_the_customers_eye_view.ipynb

{
  "cells": [
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "# Lecture 11: The Customer's-Eye View \u2014 You Hold the Ruler\n",
        "\n",
        "Every earlier lecture looked at the log from the *operator's*\n",
        "side: replaying proofs, signing attestations, building the\n",
        "tree. This one flips the telescope. You are now a customer \u2014 an\n",
        "agent, a wallet, a developer \u2014 who wants to trust one of the\n",
        "four verified Ed25519 forks and has no theorem prover, no Lean,\n",
        "no desire to spend hours re-checking anything. What actually\n",
        "happens on your side? The answer reframes the whole system, and\n",
        "it is the most intuitive on-ramp to it.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Learning Objectives\n",
        "\n",
        "- Separate the three roles that a verification touches:\n",
        "  *measurement* (operator), *publication* (the log), and\n",
        "  *judgment* (you) \u2014 and see that only the last is yours.\n",
        "- Understand the \"allowed axioms\" list as a **requirements\n",
        "  card** you own, can read, and could write yourself.\n",
        "- Explain why a self-written card meeting the supply *exactly*\n",
        "  is engineered, not coincidental.\n",
        "- State the three honest outcomes when your card is stricter\n",
        "  than the supply: relax (itemized), walk away, or grow the\n",
        "  supply.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## The card is a requirements card \u2014 and ideally you write it\n",
        "\n",
        "The list of axioms a certificate is *allowed* to rest on is not\n",
        "handed to you by the operator at verification time. It ships\n",
        "inside your own tooling (the ed25519 profile), on your disk,\n",
        "versioned by you. A maximally paranoid customer ignores the\n",
        "shipped copy and writes the card from first principles:\n",
        "\n",
        "> *\"I accept Lean's three foundational axioms, because that is\n",
        "> what the proof kernel's logic IS. For the signature-tier\n",
        "> theorems I accept named placeholders for SHA-512 and the wire\n",
        "> format, because RFC 8032 tells me those parts exist and I can\n",
        "> see they are declared, not smuggled. Nothing else.\"*\n",
        "\n",
        "That is a wish-list: the assumptions you are willing to live\n",
        "under. Call it your ruler.\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "import sys, pathlib\n",
        "for parent in [pathlib.Path.cwd(), *pathlib.Path.cwd().parents]:\n",
        "    if (parent / \"src\" / \"pacta\").exists():\n",
        "        sys.path.insert(0, str(parent / \"src\")); break\n",
        "\n",
        "# A customer writes their OWN card, from first principles - no\n",
        "# peeking at the operator. Lean's three, plus named oracle slots.\n",
        "my_card = {\n",
        "    \"foundational\": {\"propext\", \"Classical.choice\", \"Quot.sound\"},\n",
        "    \"apex_oracle_allowed\": {\n",
        "        \"sha2.Sha512\", \"verifying.sha512_new\",\n",
        "        \"verifying.sha512_update\", \"verifying.sha512_finalize_bytes\",\n",
        "        \"ed25519.Signature\", \"ed25519.Signature.to_bytes\",\n",
        "        \"signature.error.Error\", \"signature.error.Error.new\",\n",
        "    },\n",
        "}\n",
        "print(\"my requirements card:\", sum(len(v) for v in my_card.values()), \"named assumptions\")\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Wish meets supply \u2014 and it is no accident\n",
        "\n",
        "Now compare your self-written card against what the four forks\n",
        "actually declare. They match. That convergence is *engineered*:\n",
        "the supply was deliberately shrunk \u2014 every axiom made to justify\n",
        "its existence \u2014 so that any reasonable person's independently\n",
        "written card lands on the same minimal list. When the wish meets\n",
        "the supply exactly, it is because the supplier spent months\n",
        "making the supply as small as honesty allows.\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "from pacta.profiles.ed25519 import APEX_BOUNDARIES\n",
        "\n",
        "# The supply: the apex-tier certificate's documented, allowed\n",
        "# axiom cone for the upstream fork - the exact set the strongest\n",
        "# theorem is permitted to rest on, nothing more, nothing less.\n",
        "supply = set(APEX_BOUNDARIES[\"dalek-wrappers\"])\n",
        "wish = my_card[\"foundational\"] | my_card[\"apex_oracle_allowed\"]\n",
        "print(\"supply == my wish:\", supply == wish)\n",
        "print(\"axioms in supply my card did not anticipate:\", (supply - wish) or \"none\")\n",
        "print(\"axioms my card wanted that are absent:\", (wish - supply) or \"none\")\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## The three roles, kept apart\n",
        "\n",
        "It is tempting to say \"the inclusion proof proves the Lean proof\n",
        "is about my card.\" It does not, and the precision matters:\n",
        "\n",
        "| role | who | what it establishes |\n",
        "|---|---|---|\n",
        "| measurement | operator's kernel run | \"this theorem rests on exactly these named axioms\" (recorded verbatim in the attestation) |\n",
        "| publication | the transparency log | \"this measurement is in the permanent record, shown identically to everyone\" (the inclusion proof + signed head) |\n",
        "| judgment | **you** | \"these observed axioms are inside my allowed card\" (re-derived locally, every time) |\n",
        "\n",
        "Only judgment is yours, and it is the only step that involves an\n",
        "opinion. The operator is trusted to *copy down what the kernel\n",
        "printed* \u2014 never to interpret it.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## If you are happy \u2014 you are already finished\n",
        "\n",
        "If your card covers the observed cone, verification is: check\n",
        "one signature, walk ~4 hashes to the signed root, compare cones\n",
        "to your card. Milliseconds, standard library, no Lean. Done.\n",
        "\n",
        "## If you are NOT happy \u2014 there is nothing to negotiate\n",
        "\n",
        "Suppose your card is stricter: *\"I require SHA-512 itself\n",
        "proven, not an oracle.\"* The system has no sales pitch for you.\n",
        "Its entire answer is an **itemized** statement of the gap:\n",
        "*not in supply; SHA-512-proven is the R5 frontier; here is the\n",
        "exact list of what you would be accepting if you proceed\n",
        "anyway.* Your decision is never \"lower my standards\" in the\n",
        "abstract \u2014 it is a named line item: *SHA-512 as oracle: yes/no.*\n",
        "Informed compromise, not diffuse trust.\n"
      ]
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {},
      "outputs": [],
      "source": [
        "# The honest gap, itemized. A stricter customer wants no hash oracle.\n",
        "strict_card = my_card[\"foundational\"]  # foundational ONLY, no oracle slots\n",
        "gap = supply - strict_card\n",
        "print(\"this customer must explicitly accept, or walk away:\")\n",
        "for ax in sorted(gap):\n",
        "    print(\"  -\", ax)\n",
        "print()\n",
        "print(\"verdict for the strict card:\", \"PASSES\" if supply <= strict_card else \"REFUSED (gap above)\")\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## The third option: grow the supply\n",
        "\n",
        "The gap between anyone's dream card and today's supply is a\n",
        "to-do list, not a wall. Prove SHA-512, certify the wire\n",
        "parsers, and the new certificates enter the same log \u2014 and\n",
        "stricter cards start passing. The log is additive in exactly\n",
        "the way requirements are.\n",
        "\n",
        "**So: you hold the ruler. If your ruler is stricter than our\n",
        "supply, your ruler is our roadmap.** That is the quiet\n",
        "invitation built into the whole design.\n"
      ]
    },
    {
      "cell_type": "markdown",
      "metadata": {},
      "source": [
        "## Exercises\n",
        "\n",
        "- Write your own requirements card for the *foundational*\n",
        "  (non-signature) certificates from scratch. Those certificates\n",
        "  are expected to carry exactly Lean's three standard axioms\n",
        "  (`propext`, `Classical.choice`, `Quot.sound`) and nothing\n",
        "  else - did your card guess exactly those three?\n",
        "- A vendor's attestation says `status: proven`. Explain in two\n",
        "  sentences why your tooling ignores that field entirely, and\n",
        "  what it looks at instead.\n",
        "- You require reproducible builds. Is that a card you can write\n",
        "  today and have pass? Name the tier that gap belongs to, and\n",
        "  what would have to enter the log to close it.\n",
        "- Argue both sides: is \"wish meets supply exactly\" a strength\n",
        "  (minimal, auditable) or a weakness (the same author wrote the\n",
        "  card and the supply)? What single action by a customer\n",
        "  settles the argument in their favor?\n"
      ]
    }
  ],
  "metadata": {
    "kernelspec": {
      "display_name": "Python 3",
      "language": "python",
      "name": "python3"
    },
    "language_info": {
      "name": "python",
      "pygments_lexer": "ipython3"
    }
  },
  "nbformat": 4,
  "nbformat_minor": 5
}