fix(proofs): reconcile the proof ledger with PROOF-POLICY; make the gates check what they claim

.github/workflows/build-validation.yml

@@ -48,7 +48,10 @@ jobs:
   # typed-wasm's grade kernel at its pin, and the expected rejections are
   # refused.  Idris2 publishes no binaries, so 0.8.0 is built from source,
   # fetched by the commit its v0.8.0 tag names (a tag can move; the SHA
-  # cannot).
+  # cannot).  Deviation (PROOF-POLICY §6): built from upstream source, not a
+  # Guix manifest or container (PanLL has neither for proof tools yet);
+  # the commit is asserted here and check-abi.sh asserts version 0.8.0.
+  # State: open.
   panel-clades-abi:
     runs-on: ubuntu-latest
     timeout-minutes: 40
@@ -84,3 +87,32 @@ jobs:
 
       - name: panel-clades ABI
         run: bash panel-clades/scripts/check-abi.sh
+
+  # Provenance adversary model (PROOF-POLICY §4 exception, TESTED within the
+  # bounds in docs/models/Provenance.cfg), checked both ways by
+  # docs/models/check-models.sh. Deviation (PROOF-POLICY §6): TLC is fetched
+  # from the tlaplus/tlaplus v1.7.4 release, not a Guix manifest or
+  # container (PanLL has neither for proof tools yet); the script asserts
+  # the jar's SHA-256 and TLC 2.19 and fails on any mismatch. State: open.
+  provenance-model:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    permissions:
+      contents: read
+    env:
+      TLA2TOOLS_URL: https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
+      TLA2TOOLS_SHA256: 936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Fetch TLC 2.19 (tla2tools v1.7.4)
+        run: |
+          curl -fsSL --proto '=https' --proto-redir '=https' --tlsv1.2 --retry 3 \
+            -o "$RUNNER_TEMP/tla2tools.jar" "$TLA2TOOLS_URL"
+          echo "$TLA2TOOLS_SHA256  $RUNNER_TEMP/tla2tools.jar" | sha256sum -c -
+
+      - name: Model-check docs/models/Provenance.tla
+        run: bash docs/models/check-models.sh "$RUNNER_TEMP/tla2tools.jar"

CHANGELOG.adoc

@@ -9,6 +9,23 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === https://github.com/hyperpolymath/panll/compare/v0.1.0...HEAD[Unreleased]
 
+==== Fixed (2026-11-09 — proof ledger reconciled with the estate proof policy)
+
+* *The Idris2 proof gate now covers the whole import cone.*
+`panel-clades/scripts/scan-escape-hatches.sh` fails on escape hatches,
+holes (`?name`, which `idris2 --build` accepts), `partial`/`covering` and a
+missing `%default total`, in PanelClades and in typed-wasm's kernel at its
+pin. Before, holes were not checked and the kernel was not scanned.
+* *The provenance TLA+ model checks something.* Its `Sign` action let any
+party sign any payload, so `Binding` held by definition. It now models a
+leaked author key, spliced chains and an honest witness, and CI
+(`provenance-model`) checks it both ways: a forgery must be found without
+the witness check, and a verified state must be reachable.
+* `PROOF-NEEDS.adoc` uses PROOF-POLICY's status tokens, records the import
+cone, the §4 exception and the §6 toolchain deviations, states that PanLL's
+provenance profile is narrower than Exhibit B, and corrects two overclaims
+(`decDivides` is a semi-decision; the struct-size bound needs `align >= 1`).
+
 ==== Removed (2026-11-05)
 
 * *The PCC ReScript scanner (`tools/pcc/src/rescript_scanner.rs`) is