Arena/01a1087c occupancy types

.github/workflows/pages.yml

@@ -34,7 +34,7 @@ jobs:
           path: .casket-ssg
 
       - name: Setup GHCup
-        uses: haskell-actions/setup@v2.12.1
+        uses: haskell-actions/setup@0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d # v2.12.1
         with:
           ghc-version: '9.8.2'
           cabal-version: '3.10'

.github/workflows/proofs.yml

@@ -0,0 +1,97 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+#
+# proofs.yml — the R0-B / R1 proof rungs that cannot run in the authoring
+# environment.
+#
+# WHY THIS WORKFLOW EXISTS: both rungs were recorded BLOCKED in
+# docs/retraction-ledger.adoc because the authoring machine has no `idris2`
+# and no `lean`/`lake`, and cannot fetch toolchain binaries (release-asset
+# hosts unreachable).  GitHub runners *can* fetch them, so the rungs are
+# verified here rather than reported as proved by nobody.
+#
+#   stackcert — Lean 4, toolchain pinned by src/stackcert/lean-toolchain.
+#               `bash tests/run_stackcert.sh` = core `#print axioms cert_sound`
+#               + `lake build` + positive fixture + four negative controls.
+#   occ-idris — Idris 2 v0.7.0 built from source over Chez Scheme.
+#               `bash src/occ/check-rejections.sh` = the accepts compile and
+#               the four expected-rejection controls are rejected.
+#
+# NO THIRD-PARTY ACTIONS by design: only actions/checkout (GitHub-owned),
+# because this repository's Actions allow-list posture is under investigation
+# (issue #6) and a step referencing a non-allow-listed action dies at startup
+# with jobs=0 — a gate that cannot start must not be trusted to say "green".
+name: Proofs (R0-B Occ, R1 stackcert)
+
+on:
+  workflow_dispatch:
+  push:
+    branches: [main, master]
+    paths:
+      - 'src/stackcert/**'
+      - 'src/occ/**'
+      - 'tests/run_stackcert.sh'
+      - '.github/workflows/proofs.yml'
+  pull_request:
+    paths:
+      - 'src/stackcert/**'
+      - 'src/occ/**'
+      - 'tests/run_stackcert.sh'
+      - '.github/workflows/proofs.yml'
+
+# Estate guardrail: cancel superseded runs on the same ref.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  stackcert:
+    name: R1 stackcert (Lean 4)
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@v7.0.1
+      - name: Install elan (toolchain resolves from src/stackcert/lean-toolchain)
+        run: |
+          set -euo pipefail
+          curl -sSfL https://elan.lean-lang.org/elan-init.sh | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Run the stackcert harness (core + build + fixture + 4 controls)
+        run: |
+          set -euo pipefail
+          export PATH="$HOME/.elan/bin:$PATH"
+          bash tests/run_stackcert.sh
+
+  occ-idris:
+    name: R0-B Occ spike (Idris 2, advisory)
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    # Advisory until the first green run: this rung has never executed
+    # anywhere, so a red result is information (bad toolchain assumptions,
+    # or a real error in the spike) rather than a regression to block on.
+    # Remove this flag once the job has passed on main — see
+    # docs/retraction-ledger.adoc §Blocked.
+    continue-on-error: true
+    steps:
+      - uses: actions/checkout@v7.0.1
+      - name: Install Chez Scheme (Idris 2 backend)
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq
+          sudo apt-get install -y -qq chezscheme build-essential
+      - name: Build Idris 2 v0.7.0 from source
+        run: |
+          set -euo pipefail
+          git clone --depth 1 --branch v0.7.0 https://github.com/idris-lang/Idris2.git "$RUNNER_TEMP/Idris2"
+          make -C "$RUNNER_TEMP/Idris2" bootstrap SCHEME=chezscheme
+          make -C "$RUNNER_TEMP/Idris2" install PREFIX="$HOME/.idris2"
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+      - name: Occ spike — accepts compile, four controls rejected
+        run: |
+          set -euo pipefail
+          export PATH="$HOME/.idris2/bin:$PATH"
+          idris2 --version
+          bash src/occ/check-rejections.sh

.github/workflows/session-ir.yml

@@ -0,0 +1,80 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
+#
+# session-ir.yml — CI lane for the R0-B Session IR rung (ULTRAPLAN Phase 1).
+#
+# WHY THIS WORKFLOW EXISTS: the Session IR checker is the estate's only
+# fully-green, fully-runnable rung — `bash scripts/check.sh` passes 14/14
+# locally — and it was the ONLY rung with no CI lane at all. That combination
+# is the worst of both worlds: a result that is genuinely reproducible is
+# attested by nothing a reader can click, and the repository's most credible
+# claim is the one with no receipt.
+#
+# The module is pure standard library (json, sys, typing, dataclasses — no
+# third-party imports), so it runs on any runner's system python3. That is
+# deliberate: fewer moving parts, and no toolchain to fetch.
+#
+# The lane runs the SAME command as `scripts/check.sh` stage 1, including the
+# kill-test audit and the repo-shape gates, which are the other two stages
+# that can execute without a prover. Proof stages (Idris, Lean) are out of
+# scope here — see .github/workflows/proofs.yml.
+name: Session IR (R0-B)
+
+on:
+  workflow_dispatch:
+  push:
+    branches: [main, master]
+    paths:
+      - 'src/session_ir/**'
+      - 'examples/session_ir/**'
+      - 'scripts/check*.sh'
+      - 'docs/OPERATIONAL-MODEL.md'
+      - '.github/workflows/session-ir.yml'
+  pull_request:
+    paths:
+      - 'src/session_ir/**'
+      - 'examples/session_ir/**'
+      - 'scripts/check*.sh'
+      - 'docs/OPERATIONAL-MODEL.md'
+      - '.github/workflows/session-ir.yml'
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  session-ir:
+    name: R0-B Session IR (checker + kill-test + repo shape)
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@v7.0.1
+
+      - name: Session IR checker on the 14 pinned fixtures
+        # 7 accepts (judgment, measured steps <= grade, peak live bytes) and
+        # 7 rejects (each pinning its exact error code). A reject fixture that
+        # starts being ACCEPTED is a regression, not a tolerance question.
+        run: |
+          set -euo pipefail
+          PYTHONPATH=src python3 -m session_ir test examples/session_ir/manifest.json
+
+      - name: Repo shape gates and kill-test audit
+        # The runnable slice of scripts/check.sh: root allowlist, docs .md
+        # policy, and the Phase 0 kill-test block (four sentences, banned word
+        # absent). Proof stages are excluded by design (see proofs.yml).
+        run: |
+          set -euo pipefail
+          bash scripts/check-root-shape.sh .
+          bash scripts/check-no-md-in-docs.sh .
+          bash scripts/check.sh --runnable-only 2>&1 | grep -E '^(PASS|FAIL|BLOCKED)' || true
+          # --runnable-only exits 0 with proofs BLOCKED; assert the three
+          # runnable stages actually PASSED, and that nothing FAILed.
+          out="$(bash scripts/check.sh --runnable-only 2>&1)"
+          echo "$out"
+          echo "$out" | grep -q '^FAIL' && exit 1
+          echo "$out" | grep -q 'PASS: session-ir examples' || exit 1
+          echo "$out" | grep -q 'PASS: kill-test audit' || exit 1
+          echo "$out" | grep -q 'PASS: root allowlist' || exit 1

.github/workflows/sonarqube.yml

@@ -64,6 +64,6 @@ jobs:
 
       - name: SonarQube Scan
         if: steps.cfg.outputs.configured == 'true'
-        uses: SonarSource/sonarqube-scan-action@v8.3.0
+        uses: SonarSource/sonarqube-scan-action@d209202bc7d53ff1cc128f7f907dac145c9d6ae9 # v8.3.0
         env:
           SONAR_TOKEN: ${{ secrets.SONAR_TOKEN }}

.gitignore

@@ -144,3 +144,8 @@ verification/proofs/coq/.*.aux
 # Agda compiled proof artifacts
 verification/proofs/agda/*.agdai
 
+
+# Python bytecode (was tracked inadvertently; see docs/recon/TYPE-FAMILY-POSITION-2026-10-04.md)
+__pycache__/
+*.py[cod]
+*.pyo

docs/EXPLAINME.adoc

@@ -59,6 +59,11 @@ Status: *UNVERIFIED* (no `idris2` in the work environment).
   (CONJECTURE: constant grades tolerable and tight on this example).
 * Commands: `cd src/occ && idris2 --check Occ.idr && idris2 --check Demo.idr`;
   `bash src/occ/check-rejections.sh`.
+* *CI path (added 2026-10-04):* the `occ-idris` job in
+  `.github/workflows/proofs.yml` builds Idris 2 v0.7.0 over Chez Scheme and
+  runs the same script. It is `continue-on-error: true` *because this rung has
+  never executed anywhere* — a red result is information, not a regression.
+  Remove that flag after the first green run on `main`.
 
 == C5. stackcert `check` is sound: accepted certificates bound every call path
 
@@ -74,6 +79,18 @@ Status: *UNVERIFIED* (no `lean` in the work environment).
 * Commands: `bash tests/run_stackcert.sh` (core + fixture + four negative
   controls: decremented bound, undeclared recursion, unresolved indirect,
   undeclared cycle).
+* *CI path (added 2026-10-04):* the `stackcert` job in
+  `.github/workflows/proofs.yml` installs elan and runs the same harness.
+  Until 2026-10-04 the harness could not have passed even with Lean installed:
+  the repository carried no `lakefile.toml` and no `lean-toolchain`, so
+  `lake build` and `lake exe stackcert` had nothing to act on. Both are now
+  committed, and the version is pinned rather than floating (compare
+  echo-types#322, where an unpinned `apt-get install agda` lets the prover
+  under the proofs change without a commit).
+* *When the run is green,* paste the job's `#print axioms` output verbatim in
+  place of the expectation above, and record the run id. Not before: a
+  predicted footprint is a conjecture, and the point of this repository is
+  that conjectures are labelled.
 
 == C6. Fixtures are real compiler output