ci: repin standards to 9bdf864 with the fork-PR publisher; proofs: gate holes, totality and import cone, ledgers to PROOF-POLICY

.github/workflows/actions.lock

@@ -21,34 +21,36 @@ workflows:
     '.github/workflows/dogfood-gate.yml':
         - 'actions/checkout@v7.0.1'
         - 'hyperpolymath/deed-ecosystem@main'
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/e2e.yml':
         - 'actions/checkout@v7.0.1'
         - 'dtolnay/rust-toolchain@v1'
         - 'goto-bus-stop/setup-zig@v2.2.1'
         - 'swatinem/rust-cache@v2.9.3'
+    '.github/workflows/fork-governance-publish.yml':
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/fork-governance.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/governance.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/hypatia-scan.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/instant-sync.yml':
         - 'peter-evans/repository-dispatch@v4.0.1'
     '.github/workflows/label-triage.yml': []
     '.github/workflows/labels.yml': []
     '.github/workflows/main-estate-audit.yml':
         - 'hyperpolymath/cicd-suite@4f5404281dd7092fa77cc18daec7237c4f1ee4ac'
     '.github/workflows/mirror.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/push-email-notify.yml':
         - 'hyperpolymath/smtp-notify-action@v0.5.0'
     '.github/workflows/rust-ci.yml':
         - 'metadatastician/standards@412a7031577112b31ee287cc6060179d638d6500'
     '.github/workflows/scorecard.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
     '.github/workflows/secret-scanner.yml':
-        - 'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6'
+        - 'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
 dependencies:
     'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9':
         ref: 'v6.1.0'
@@ -183,9 +185,14 @@ dependencies:
         commit: 'sha1-c1c9fa07992a02c1fd3d67a0dc1b08cccb852aef'
         owner_id: 6759885
         repo_id: 1352485172
-    'metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6':
-        ref: 'e064539116c2dcfdf282a4749dbd58c69961c7e6'
-        commit: 'sha1-e064539116c2dcfdf282a4749dbd58c69961c7e6'
+    'metadatastician/standards@412a7031577112b31ee287cc6060179d638d6500':
+        ref: '412a7031577112b31ee287cc6060179d638d6500'
+        commit: 'sha1-412a7031577112b31ee287cc6060179d638d6500'
+        owner_id: 297579217
+        repo_id: 1116521501
+    'metadatastician/standards@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5':
+        ref: '9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
+        commit: 'sha1-9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5'
         owner_id: 297579217
         repo_id: 1116521501
         uses:
@@ -201,11 +208,6 @@ dependencies:
             - 'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e'
             - 'oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6'
             - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555'
-    'metadatastician/standards@412a7031577112b31ee287cc6060179d638d6500':
-        ref: '412a7031577112b31ee287cc6060179d638d6500'
-        commit: 'sha1-412a7031577112b31ee287cc6060179d638d6500'
-        owner_id: 297579217
-        repo_id: 1116521501
     'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e':
         ref: 'v2.5.0'
         commit: 'sha1-fa7117db83c52d787ae5a89f350999701505d78e'

.github/workflows/build-validation.yml

@@ -44,6 +44,39 @@ jobs:
       - name: Build Panel Contract Compiler
         run: cargo build --locked --release --manifest-path tools/pcc/Cargo.toml
 
+  # Provenance model (docs/models/Provenance.tla, a PROOF-POLICY §4
+  # exception recorded in PROOF-NEEDS.adoc): TLC checks that a chain
+  # verifies only if it is the genuine one while either signing key is
+  # uncompromised, and must find the forgery when both are.
+  #
+  # PROOF-POLICY §6 deviation (also recorded in PROOF-NEEDS.adoc, state
+  # open): PanLL has no Guix manifest or proof container that provides TLC,
+  # so the official tla2tools.jar release asset is fetched and checked
+  # against the SHA-256 recorded here; the script asserts the TLC version
+  # it ran.  Java is the runner image's.
+  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 TLA+ tools v1.7.4 (pinned by digest)
+        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 -
+          java -version
+
+      - name: Model-check the provenance binding (both ways)
+        run: bash scripts/check-provenance-model.sh "$RUNNER_TEMP/tla2tools.jar"
+
   # panel-clades ABI: every PanelClades.ABI module typechecks against
   # 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,
@@ -62,6 +95,11 @@ jobs:
         with:
           persist-credentials: false
 
+      # The source scans check-abi.sh relies on, tested both ways; needs no
+      # Idris2, so it fails fast before the 8-minute toolchain build.
+      - name: ABI scan regression tests
+        run: bash panel-clades/tests/scan/test-abi-scan.sh
+
       - name: Install Chez Scheme and GMP
         run: |
           sudo apt-get update -qq

.github/workflows/dogfood-gate.yml

@@ -14,7 +14,7 @@
     branches: [main, master]
 
 permissions:
   actions: read
   contents: read
 
 jobs:
@@ -74,7 +74,7 @@
   k9-conformance:
     name: K9-DEED conformance (push)
     if: github.event_name == 'push'
-    uses: metadatastician/standards/.github/workflows/k9-conformance.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/k9-conformance.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     permissions:
       contents: read
       pull-requests: read

.github/workflows/fork-governance-publish.yml

@@ -0,0 +1,181 @@
+# This workflow is managed by gh actions-lock.
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+# fork-governance-publish.yml — post the Fork governance comment on pull
+# requests from forks.
+#
+# On a fork PR GitHub gives the "Fork governance" run a read-only token, so
+# its verdict job uploads the rendered comment as an artifact instead of
+# posting it. This workflow runs after every "Fork governance" run, from the
+# default branch's copy with this repository's token, and posts that comment
+# as escaped, explicitly untrusted text. It skips same-repository runs,
+# which post their own comment. It takes effect once merged to main.
+#
+# Publisher vendored from metadatastician/standards at
+# 9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5, with safe artifact rendering.
+# Preserve the shared comment marker and publisher stamp protocol.
+name: Fork governance publish
+
+# workflow_run, deliberately: it is the only way to write a comment for a
+# fork PR. Nothing from the fork runs here. This job checks out no code,
+# reads the artifact as data, and posts only to the open PR whose head is
+# the commit the run built.
+on:
+  workflow_run:
+    workflows: ["Fork governance"]
+    types: [completed]
+
+permissions:
+  contents: read
+
+jobs:
+  publish:
+    name: Publish the fork governance summary (fork PR)
+    # Only a completed pull_request run from a fork has anything to publish;
+    # every other run posted its own comment.
+    if: >-
+      ${{ github.event_name == 'workflow_run'
+          && github.event.workflow_run.event == 'pull_request'
+          && github.event.workflow_run.head_repository.full_name != github.repository }}
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    # One publisher at a time per fork branch, so the read-compare-write of
+    # the comment below never interleaves with another publisher's.
+    concurrency:
+      group: fork-governance-publish-${{ github.event.workflow_run.head_repository.full_name }}-${{ github.event.workflow_run.head_branch }}
+      cancel-in-progress: false
+    permissions:
+      actions: read
+      pull-requests: write
+    steps:
+      - name: Download the rendered comment
+        id: download
+        continue-on-error: true
+        uses: actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333 # v8.0.2
+        with:
+          name: fork-governance-comment
+          path: ${{ runner.temp }}/fork-governance-comment
+          run-id: ${{ github.event.workflow_run.id }}
+          github-token: ${{ github.token }}
+
+      # A run may leave no artifact only when it was replaced: a newer attempt
+      # of the same run, or a newer push to the fork branch (a newer run at a
+      # different commit; a push re-runs every pull request from the branch,
+      # so each one gets its own successor). Anything else is a missing report
+      # and fails here, including a run cancelled by hand with no successor.
+      - name: Fail on a missing comment
+        if: ${{ steps.download.outcome != 'success' }}
+        env:
+          GH_TOKEN: ${{ github.token }}
+          RUN_ID: ${{ github.event.workflow_run.id }}
+          RUN_ATTEMPT: ${{ github.event.workflow_run.run_attempt }}
+          WORKFLOW_ID: ${{ github.event.workflow_run.workflow_id }}
+          RUN_HEAD_SHA: ${{ github.event.workflow_run.head_sha }}
+          RUN_HEAD_REPO: ${{ github.event.workflow_run.head_repository.full_name }}
+          RUN_HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
+          RUN_CONCLUSION: ${{ github.event.workflow_run.conclusion }}
+          RUN_URL: ${{ github.event.workflow_run.html_url }}
+        run: |
+          set -euo pipefail
+          pushed=$(gh api -X GET "repos/$GITHUB_REPOSITORY/actions/workflows/$WORKFLOW_ID/runs" \
+              -f event=pull_request -f branch="$RUN_HEAD_BRANCH" -f per_page=100 \
+            | jq --arg repo "$RUN_HEAD_REPO" --arg sha "$RUN_HEAD_SHA" --argjson id "$RUN_ID" \
+                '[.workflow_runs[] | select(.head_repository.full_name == $repo and .id > $id and .head_sha != $sha)] | length')
+          attempt=$(gh api "repos/$GITHUB_REPOSITORY/actions/runs/$RUN_ID" --jq '.run_attempt')
+          if [ "$pushed" -gt 0 ] || [ "$attempt" -gt "$RUN_ATTEMPT" ]; then
+            echo "$RUN_URL left no comment, but a newer push or attempt replaced it; that run publishes."
+            exit 0
+          fi
+          echo "::error::$RUN_URL ($RUN_CONCLUSION) uploaded no fork-governance-comment artifact and nothing replaced it, so its pull request has no governance comment"
+          exit 1
+
+      - name: Publish the comment
+        if: ${{ steps.download.outcome == 'success' }}
+        env:
+          GH_TOKEN: ${{ github.token }}
+          GRID_AUTHOR: github-actions[bot]
+          RUN_ID: ${{ github.event.workflow_run.id }}
+          RUN_ATTEMPT: ${{ github.event.workflow_run.run_attempt }}
+          RUN_HEAD_SHA: ${{ github.event.workflow_run.head_sha }}
+          RUN_HEAD_REPO: ${{ github.event.workflow_run.head_repository.full_name }}
+          RUN_HEAD_BRANCH: ${{ github.event.workflow_run.head_branch }}
+          RUN_URL: ${{ github.event.workflow_run.html_url }}
+        run: |
+          set -euo pipefail
+          dir="$RUNNER_TEMP/fork-governance-comment"
+          body="$dir/body.md"
+          meta="$dir/meta.json"
+          [ -f "$body" ] && [ -f "$meta" ] || { echo "::error::artifact is missing body.md or meta.json"; exit 1; }
+
+          pr=$(jq -r '.pr_number // ""' "$meta")
+          if ! [[ "$pr" =~ ^[1-9][0-9]{0,9}$ ]]; then
+            echo "::error::artifact pr_number is not a pull request number"; exit 1
+          fi
+
+          # The pull request must be this run's own: open, at the commit the
+          # run built, from the fork and branch the run came from (header).
+          # Captured first, so a failed lookup fails the step under `set -e`
+          # instead of reading as "not open".
+          pr_info=$(gh api "repos/$GITHUB_REPOSITORY/pulls/$pr" \
+            --jq '[.state, .head.sha, (.head.repo.full_name // "-"), .head.ref] | join(" ")')
+          # A git ref cannot contain whitespace, so the branch is the last field.
+          read -r pr_state pr_sha pr_repo pr_branch <<< "$pr_info"
+          if [ "$pr_state" != open ]; then
+            echo "Pull request #$pr is $pr_state; nothing to publish."; exit 0
+          fi
+          if [ "$pr_sha" != "$RUN_HEAD_SHA" ]; then
+            echo "Pull request #$pr has moved past $RUN_HEAD_SHA; its newer run publishes."; exit 0
+          fi
+          if [ "$pr_repo" != "$RUN_HEAD_REPO" ] || [ "$pr_branch" != "$RUN_HEAD_BRANCH" ]; then
+            echo "::error::artifact names #$pr, which is not from $RUN_HEAD_REPO:$RUN_HEAD_BRANCH"; exit 1
+          fi
+
+          if ! head -n 1 "$body" | grep -q '^<!-- fork-governance-verdict:'; then
+            echo "::error::body does not start with the fork-governance marker"; exit 1
+          fi
+          # The run stamp is the comment's last line, written here and never by
+          # the fork, so the last stamp in a comment is always the publisher's.
+          {
+            # Fixed trusted framing; artifact bytes are text, never Markdown/HTML.
+            printf '<!-- fork-governance-verdict: untrusted-fork-report -->\n'
+            printf '## Untrusted fork governance report\n\n'
+            printf 'The following text was supplied by the fork. It is not a verified bot verdict. Consult the lane checks for results.\n\n'
+            printf '<pre>\n'
+            jq -Rrs '@html' "$body"
+            printf '</pre>\n'
+            printf '\n<sub>Rendered by the fork pull request run %s and published by fork-governance-publish.</sub>\n' "$RUN_URL"
+            printf '<!-- fork-governance-publish-run: %s.%s -->\n' "$RUN_ID" "$RUN_ATTEMPT"
+          } > "$dir/published.md"
+          # GitHub's limit is 65536 characters, not bytes; the glyphs are
+          # multibyte, so count characters.
+          if [ "$(LC_ALL=C.UTF-8 wc -m < "$dir/published.md")" -gt 65000 ]; then
+            echo "::error::body exceeds the 65000-character comment limit"; exit 1
+          fi
+
+          existing=$(gh api --paginate --slurp "repos/$GITHUB_REPOSITORY/issues/$pr/comments" \
+            | jq -c --arg a "$GRID_AUTHOR" \
+                '[.[][] | select((.user.login // "") == $a and ((.body // "") | contains("<!-- fork-governance-verdict:")))]
+                 | last // {} | {id: (.id // ""), body: (.body // "")}')
+          comment_id=$(jq -r '.id' <<< "$existing")
+          # Runs for one pull request can finish out of order (a re-run, or a
+          # close and reopen). Never replace a comment a newer run published:
+          # compare this run's id, then attempt, with the comment's last stamp.
+          stamp=$(jq -r '.body' <<< "$existing" \
+            | sed -n 's/^<!-- fork-governance-publish-run: \([0-9]*\)\.\([0-9]*\) -->$/\1 \2/p' | tail -n 1)
+          if [ -n "$stamp" ]; then
+            read -r prev_id prev_attempt <<< "$stamp"
+            if [ "$prev_id" -gt "$RUN_ID" ] || { [ "$prev_id" -eq "$RUN_ID" ] && [ "$prev_attempt" -gt "$RUN_ATTEMPT" ]; }; then
+              echo "#$pr already carries the comment from newer run $prev_id.$prev_attempt; leaving it."; exit 0
+            fi
+          fi
+
+          jq -n --rawfile body "$dir/published.md" '{body: $body}' > "$dir/comment.json"
+          if [ -n "$comment_id" ]; then
+            gh api -X PATCH "repos/$GITHUB_REPOSITORY/issues/comments/$comment_id" \
+              --input "$dir/comment.json" >/dev/null
+            echo "updated the fork governance comment on #$pr ($comment_id)"
+          else
+            gh api -X POST "repos/$GITHUB_REPOSITORY/issues/$pr/comments" \
+              --input "$dir/comment.json" >/dev/null
+            echo "posted the fork governance comment on #$pr"
+          fi

.github/workflows/fork-governance.yml

@@ -29,15 +29,15 @@ permissions:
 jobs:
   deed:
     name: DEED syntax
-    uses: metadatastician/standards/.github/workflows/deed-conformance.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/deed-conformance.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     permissions:
       contents: read
     with:
       require-files: false
 
   k9:
     name: K9-DEED conformance
-    uses: metadatastician/standards/.github/workflows/k9-conformance.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/k9-conformance.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     permissions:
       contents: read
       pull-requests: read
@@ -47,7 +47,7 @@ jobs:
 
   hypatia:
     name: Hypatia verdict grid
-    uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     permissions:
       actions: read
       contents: read
@@ -59,7 +59,7 @@ jobs:
     name: Post the fork governance summary
     needs: [deed, k9, hypatia]
     if: ${{ always() && github.event_name == 'pull_request' }}
-    uses: metadatastician/standards/.github/workflows/fork-governance-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/fork-governance-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     permissions:
       contents: read
       actions: read
@@ -72,4 +72,4 @@ jobs:
       hypatia-result: ${{ needs.hypatia.result }}
       hypatia-verdict: ${{ needs.hypatia.outputs.verdict }}
       hypatia-advisory: ${{ needs.hypatia.outputs.advisory }}
-      canon-ref: e064539116c2dcfdf282a4749dbd58c69961c7e6
+      canon-ref: 9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5

.github/workflows/governance.yml

@@ -33,6 +33,6 @@ permissions:
 
 jobs:
   governance:
-    uses: metadatastician/standards/.github/workflows/governance-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/governance-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     secrets:
       HYPATIA_SCAN_PAT: ${{ secrets.HYPATIA_SCAN_PAT }}

.github/workflows/hypatia-scan.yml

@@ -34,6 +34,6 @@ jobs:
       actions: read
       contents: read
       security-events: write
-    uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     secrets:
       HYPATIA_SCAN_PAT: ${{ secrets.HYPATIA_SCAN_PAT }}

.github/workflows/mirror.yml

@@ -16,7 +16,7 @@ jobs:
     # A manual dispatch from a feature branch has no local main ref to push.
     # Mirror only the canonical branch, as the push trigger already requires.
     if: github.ref == 'refs/heads/main'
-    uses: metadatastician/standards/.github/workflows/mirror-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/mirror-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5
     secrets:
       GITLAB_SSH_KEY: ${{ secrets.GITLAB_SSH_KEY }}
       CODEBERG_SSH_KEY: ${{ secrets.CODEBERG_SSH_KEY }}

.github/workflows/scorecard.yml

@@ -16,4 +16,4 @@ jobs:
       contents: read
       security-events: write
       id-token: write
-    uses: metadatastician/standards/.github/workflows/scorecard-reusable.yml@e064539116c2dcfdf282a4749dbd58c69961c7e6
+    uses: metadatastician/standards/.github/workflows/scorecard-reusable.yml@9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5