Phase 0 follow-up: CI/required asserts Idris 2 0.8.0, checker pin bumped to post-ratification trope-checker, schema re-vendored, AFFIRMATION accuracy (haec)

.github/workflows/ci.yml

@@ -77,8 +77,8 @@ jobs:
           ver="$(idris2 --version)"
           echo "idris2 --version -> ${ver}"
           case "$ver" in
-            *"0.7.0"*) ;;
-            *) echo "::error::expected Idris 2 0.7.0, got: ${ver}"; exit 1 ;;
+            *"0.8.0"*) ;;
+            *) echo "::error::expected Idris 2 0.8.0, got: ${ver}"; exit 1 ;;
           esac
           idris2 --typecheck abi.ipkg
 

.github/workflows/governance.yml

@@ -21,4 +21,4 @@ concurrency:
 
 jobs:
   governance:
-    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd
+    uses: metadatastician/standards/.github/workflows/governance-reusable.yml@857ff096af11451841fb10488fed1438523973a1

.github/workflows/hypatia-scan.yml

@@ -1,4 +1,4 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
@@ -20,4 +20,4 @@
 
 jobs:
   scan:
-    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd
+    uses: metadatastician/standards/.github/workflows/hypatia-scan-reusable.yml@857ff096af11451841fb10488fed1438523973a1

.github/workflows/mirror.yml

@@ -12,5 +12,15 @@ permissions:
   contents: read
 jobs:
   mirror:
-    uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd
-    secrets: inherit
+    uses: metadatastician/standards/.github/workflows/mirror-reusable.yml@857ff096af11451841fb10488fed1438523973a1
+    secrets:
+      GITLAB_SSH_KEY: ${{ secrets.GITLAB_SSH_KEY }}
+      BITBUCKET_SSH_KEY: ${{ secrets.BITBUCKET_SSH_KEY }}
+      CODEBERG_SSH_KEY: ${{ secrets.CODEBERG_SSH_KEY }}
+      SOURCEHUT_SSH_KEY: ${{ secrets.SOURCEHUT_SSH_KEY }}
+      DISROOT_SSH_KEY: ${{ secrets.DISROOT_SSH_KEY }}
+      GITEA_SSH_KEY: ${{ secrets.GITEA_SSH_KEY }}
+      RADICLE_KEY: ${{ secrets.RADICLE_KEY }}
+      R2_ACCESS_KEY_ID: ${{ secrets.R2_ACCESS_KEY_ID }}
+      R2_SECRET_ACCESS_KEY: ${{ secrets.R2_SECRET_ACCESS_KEY }}
+      R2_AGE_RECIPIENT: ${{ secrets.R2_AGE_RECIPIENT }}

.github/workflows/scorecard.yml

@@ -1,4 +1,4 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
 # This workflow is managed by gh actions-lock.
@@ -27,4 +27,4 @@
       contents: read
       security-events: write
       id-token: write
-    uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd
+    uses: metadatastician/standards/.github/workflows/scorecard-reusable.yml@857ff096af11451841fb10488fed1438523973a1

.github/workflows/secret-scanner.yml

@@ -15,5 +15,4 @@ permissions:
   contents: read
 jobs:
   scan:
-    uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd
-    secrets: inherit
+    uses: metadatastician/standards/.github/workflows/secret-scanner-reusable.yml@857ff096af11451841fb10488fed1438523973a1

.github/workflows/trope-check.yml

@@ -42,7 +42,7 @@ jobs:
         uses: actions/checkout@v7.0.1
         with:
           repository: hyperpolymath/trope-checker
-          ref: 69221ad6bec0c9286cb5c917edfad281e7e0089e # main @ 2026-07-28
+          ref: 4ecba4f1862aec144ec940b1d8a93ddabd1cb591 # main @ 2026-11-02 (after Phase 0 #107 and #109)
           path: trope-checker
 
       # The pinned idris2-pack image is minimal and ships no jq, which both the

AFFIRMATION.adoc

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = AFFIRMATION — Haec
-:revdate: 2026-10-27
+:revdate: 2026-11-04
 
 A dated, ground-truthed honesty snapshot. This is the brief's "STATUS" for Haec:
 what exists, what is verified, what is deferred — stated plainly, no overclaim.
@@ -34,16 +34,50 @@ and its examples lower to IR the checker accepts.
 == As of 2026-10-27
 
 *Ground truth (run here, UTC 07:49, haec `e9bee39`):*
-`TROPECHECK_REQUIRED=1 TROPECHECK_BIN=/path/to/tropecheck-rs bash tests/check-examples.sh` (the path is a placeholder for the built fast core) → the three examples
-(`faithful-record`, `survey-collapse`, `station-average`) lower to well-formed Trope
-IR; the vendored `design/trope-ir.schema.json` matches the canonical checker schema;
-all three round-trip through the checker to the verdict each states —
+`TROPECHECK_REQUIRED=1 TROPECHECK_BIN=/path/to/tropecheck-rs bash tests/check-examples.sh` (the path is a placeholder for the built fast core) → the three checked-in
+example IR documents (`faithful-record`, `survey-collapse`, `station-average`;
+lowered by hand — there is no compiler, and the script checks these documents, it
+does not produce them) are well-formed Trope IR; the vendored
+`design/trope-ir.schema.json` matched the canonical checker schema at that checker
+revision; all three round-trip through the checker to the verdict each states —
 `faithful-record` `p-sufficient`, `survey-collapse` `p-insufficient` with witness
-`e_collapse/fate.quality`, `station-average` `p-sufficient`. "examples: all lower to
-valid Trope IR." The checker was the Rust fast core built from trope-checker
-`44020f9` (`main` 216f23b plus the two Phase 0 spec/CI patches, which do not touch
-`src/rust`).
+`e_collapse/fate.quality`, `station-average` `p-sufficient`. The script's closing
+line reads "examples: all lower to valid Trope IR" (its wording; see above). The
+checker was the Rust fast core built from trope-checker `44020f9` (`main` 216f23b
+plus the two Phase 0 spec/CI patches, which do not touch `src/rust`).
 
 *Still true, stated once:* no compiler, no LSP, no runtime; the O2 lowering
 obligations in `design/elaboration.adoc` are stated, not discharged; no proofs of
 our own.
+
+== As of 2026-11-04
+
+*Ground truth (run here, haec `6b36491` plus the changes that land with this
+entry):* the same command, with the fast core built from trope-checker `4ecba4f`
+(`main` after Phase 0 landed there via #107, plus the decoder fixes of #109) and
+`design/trope-ir.schema.json` re-vendored from that revision → ok ×7 (three
+well-formed documents, schema match, three round-trips to the stated verdicts,
+witness `e_collapse/fate.quality` unchanged), exit 0. Before the re-vendoring the
+same run failed the drift guard ("vendored IR schema has drifted …", exit 1): the
+canonical schema changed shape between `69221ad6` and `4ecba4f` (explicit `type`
+annotations and a `tau` pass-through; the required fields are unchanged), which is
+what the guard exists to catch. `tests/check-examples.sh` now also fails under
+`TROPECHECK_REQUIRED=1` when the canonical schema is absent, so CI cannot pass
+with the guard silently skipped.
+
+*NOT RUN here, attested by CI:* the Idris2 reference-checker path that
+`.github/workflows/trope-check.yml` takes (no Idris 2 in this session). That
+workflow, now pinned to trope-checker `4ecba4f`, ran on this change: job
+`examples-lower-to-valid-ir` of
+https://github.com/hyperpolymath/haec/actions/runs/41928694567 — success,
+2026-11-04T22:51:37Z (the Idris2 reference checker built at `4ecba4f` gives the
+same three verdicts and witness). `CI / required` now asserts Idris 2 0.8.0, the
+version the digest-pinned image ships (it asserted 0.7.0 and was red on `main`
+from 2026-10-21; haec #83): in run 41928694928 the Idris step passes
+(`idris2 --version -> Idris 2, version 0.8.0-6ca00e72e`, `abi.ipkg` typechecks,
+the Zig FFI tests pass) and the job then fails in its last step on the
+root-shape allowlist (`.machine_readable/root-allow.txt`, the owner-only half
+of #83), so that check stays red for a reason this entry does not claim to fix.
+
+*Still true, stated once:* no compiler, no LSP, no runtime; O2 obligations stated,
+not discharged; no proofs of our own.