diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index a176cb2..205d588 100644 --- a/.github/workflows/pages.yml +++ b/.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' diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml new file mode 100644 index 0000000..e786971 --- /dev/null +++ b/.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 diff --git a/.github/workflows/session-ir.yml b/.github/workflows/session-ir.yml new file mode 100644 index 0000000..0b780d0 --- /dev/null +++ b/.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 diff --git a/.github/workflows/sonarqube.yml b/.github/workflows/sonarqube.yml index 7c45959..d65d08b 100644 --- a/.github/workflows/sonarqube.yml +++ b/.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 }} diff --git a/.gitignore b/.gitignore index afbe851..350f5f8 100644 --- a/.gitignore +++ b/.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 diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index ecad9dc..dbd9992 100644 --- a/docs/EXPLAINME.adoc +++ b/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 diff --git a/docs/recon/A1-ACTIONS-RUNBOOK.adoc b/docs/recon/A1-ACTIONS-RUNBOOK.adoc new file mode 100644 index 0000000..1ff05e3 --- /dev/null +++ b/docs/recon/A1-ACTIONS-RUNBOOK.adoc @@ -0,0 +1,250 @@ +// SPDX-License-Identifier: CC-BY-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += A1 runbook — make Actions start jobs +:toc: +:icons: font + +*Date:* 2026-10-04 · *Owner:* repository owner (this is the one thing an agent +cannot do from inside the repository) · *Blocks:* every other item in Tranche A + +== 1. What is already established (measured, not assumed) + +[cols="2,3",options="header"] +|=== +| Observation | Evidence + +| Job-start failures are total, not partial +| Last 100 runs: 96 `startup_failure`, 3 `failure`, 1 `success`. Only *4* runs had any + job at all — the four Dependabot "Update" workflows. + +| It reproduces on the current branch, right now +| The push of `d5caaca` created run `37236457077` ("Push email notification", event + `push`, 2026-10-04T21:31:42Z) → `conclusion: startup_failure`, `jobs: 0`. + +| The workflow files themselves are not the problem +| All 37 workflows report `state: active`. The new ones pass the local gates: SPDX header + in the leading comment block, top-level `permissions:`, and + `node scripts/check-action-pinning.js` → *exit 0*. + +| The local gate passes +| `bash scripts/check.sh --runnable-only` → exit 0 (Session IR 14/14, kill-test audit, + repo shape; proof stages correctly `BLOCKED`, not skipped). +|=== + +*Diagnosis:* a failure at job start, at repository level, affecting every workflow +including ones whose only action is `actions/checkout`. That is the signature of an +allow-list in `selected` mode with an empty pattern set — the same defect as +choreographic-programming#16, where `selected` carried zero patterns and so blocked +*every* action, `actions/checkout` included. + +*What is still unknown:* the posture itself. `GET /repos/{owner}/{repo}/actions/permissions` +returns **403** to this session's token, so the value cannot be read from inside the +repository. That is why A1 is owner-routed. + +== 2. Reading the posture — two routes + +=== 2.1 Route A — the settings page (no token, no scopes) + +Open https://github.com/hyperpolymath/occupancy-types/settings/actions and read the +*Actions permissions* section. It is three radio buttons: + +[cols="1,3",options="header"] +|=== +| Radio | What it means here +| *Allow all actions and reusable workflows* | Posture is fine (case A in §3) — the outage + is something else, so do not change anything. +| *Allow select actions and reusable workflows* | Case B. Read the list underneath: if it + is empty, or omits `actions/*`, that is the defect. +| *Disable actions* | Case C. Actions are off for the repository. +|=== + +This route needs no token at all, and it is the recommended one: no scopes, nothing to +refresh, and the same page is where the fix is applied. + +=== 2.2 Route B — the API + +[IMPORTANT] +==== +*Scope correction (2026-10-04).* An earlier revision of this document said +`gh auth refresh -s admin:repo_hook`. **That was wrong.** `admin:repo_hook` governs +webhooks, not Actions settings. Per GitHub's REST documentation for the repository-level +Actions permissions endpoints: + +* classic PAT / OAuth token → the *`repo`* scope; +* fine-grained PAT → *"Administration"* repository permissions (read to GET, write to PUT). + +(Worth knowing: the *organisation*-level equivalents need `admin:org`/Administration org +permissions. Those are not what this repository needs — `hyperpolymath` is a user account, +so the repository-level setting is authoritative.) +==== + +First, see what your current credential can do: + +[source,bash] +---- +gh auth status +---- + +If the scopes listed do not include `repo` (or an equivalent fine-grained grant): + +[source,bash] +---- +# Works when gh was authenticated via the browser (OAuth): +gh auth refresh -s repo +---- + +[NOTE] +==== +`gh auth refresh` expands scopes by opening a browser, which only works for +*OAuth/browser* logins. If your stored credential is a **personal access token** (the +`gh auth login --with-token` case), `gh` cannot add scopes to it — refreshing will fail. +In that case make a new classic PAT at https://github.com/settings/tokens with the +*`repo`* scope (add `workflow` too, since it governs workflow files) and either log in +with it or use it for one call: + +[source,bash] +---- +gh auth login --with-token < token.txt +GH_TOKEN=ghp_xxx gh api repos/hyperpolymath/occupancy-types/actions/permissions --jq . +---- +==== + +Then run this **exactly as written**: + +[source,bash] +---- +gh api repos/hyperpolymath/occupancy-types/actions/permissions --jq . + +# If the above prints allowed_actions: "selected", list the patterns: +gh api repos/hyperpolymath/occupancy-types/actions/permissions/selected-actions --jq . +---- + +Paste the output. Everything below follows from which of the three cases it is. + +[IMPORTANT] +==== +*The `repos/` prefix is not optional.* `gh api occupancy-types/actions/permissions` +(no `repos/`) returns *HTTP 404 Not Found* — there is no such route, so the 404 says +nothing about permissions. Verified directly on 2026-10-04: + +[cols="1,1",options="header"] +|=== +| Command | Result +| `gh api occupancy-types/actions/permissions` | `404 Not Found` (bad route) +| `gh api repos/hyperpolymath/occupancy-types/actions/permissions` | route exists +|=== + +Two other statuses and what they mean: + +* *`403 Resource not accessible by integration`* — an **App/integration** token. Such + tokens can never read this endpoint, no matter the scope. This session's token is one + of those, which is why the value had to be requested rather than fetched. A normal + user login is not affected. +* *`403` with a message about scopes* (on a user token) — the token lacks the `repo` + scope. Fix per §2.2: `gh auth refresh -s repo`, or a new classic PAT with `repo`. +==== + +== 3. Read the result + +[cols="1,3,3",options="header"] +|=== +| Case | Output looks like | What it means + +| *A* +| `"enabled": true, "allowed_actions": "all"` +| Posture is *not* the cause. The outage is elsewhere (runner availability, billing, + or a disabled-actions flag at another level). Do not apply the PUT in §4 — it would + change nothing and muddy the evidence. Report the output and we re-diagnose. + +| *B* +| `"enabled": true, "allowed_actions": "selected"`, and the selected-actions list is + *empty* (or omits `actions/*`) +| This is the defect. Every action is blocked, including GitHub-owned + `actions/checkout`, which is why `jobs: 0` on every run. Apply §4. + +| *C* +| `"enabled": false` +| Actions are disabled for the repository. Apply §5 first, then §4 if it also reads + `selected`. +|=== + +== 4. The fix for case B — allow actions + +Two options; the first is one command and matches what the rest of the estate runs. + +[source,bash] +---- +# Option 1 (recommended): allow all actions +gh api -X PUT repos/hyperpolymath/occupancy-types/actions/permissions \ + -f enabled=true -f allowed_actions=all +---- + +[source,bash] +---- +# Option 2 (tighter): allow GitHub-owned actions + the pinned third parties this repo uses +gh api -X PUT repos/hyperpolymath/occupancy-types/actions/permissions \ + -f enabled=true -f allowed_actions=selected \ + -F github_owned_allowed=true \ + -F verified_allowed=false \ + -f 'patterns_allowed[]=actions/*' \ + -f 'patterns_allowed[]=github/codeql-action/*' \ + -f 'patterns_allowed[]=dependabot/fetch-metadata@*' \ + -f 'patterns_allowed[]=erlef/setup-beam@*' \ + -f 'patterns_allowed[]=haskell-actions/setup@*' \ + -f 'patterns_allowed[]=oven-sh/setup-bun@*' \ + -f 'patterns_allowed[]=SonarSource/sonarqube-scan-action@*' \ + -f 'patterns_allowed[]=hyperpolymath/standards/.github/workflows/*' +---- + +Option 2 is stricter but brittle: every new action needs a new pattern, and a missing +pattern fails as `jobs: 0` — the exact failure being fixed. *Option 1 is recommended* +precisely because it removes a silent-failure mode rather than narrowing it. + +== 5. The fix for case C — enable Actions + +[source,bash] +---- +gh api -X PUT repos/hyperpolymath/occupancy-types/actions/permissions -f enabled=true +---- + +== 6. Positive control — prove it worked + +Do not trust the badge; count jobs. A workflow that starts is the only evidence a +workflow can start. + +[source,bash] +---- +# Trigger a run (empty commit is enough and changes no content) +git commit --allow-empty -m "chore: A1 positive control" && git push + +# Then, after ~30s: +gh api "repos/hyperpolymath/occupancy-types/actions/runs?per_page=5" \ + --jq '.workflow_runs[] | "\(.id)\t\(.name)\t\(.conclusion)"' + +# R1: how many of the last 20 runs actually executed a job? +for id in $(gh api "repos/hyperpolymath/occupancy-types/actions/runs?per_page=20" \ + --jq '.workflow_runs[].id'); do + printf "%s\t%s\n" "$id" \ + "$(gh api "repos/hyperpolymath/occupancy-types/actions/runs/$id/jobs" --jq '.total_count')" +done +---- + +*A1 is closed when:* the newest `Session IR (R0-B)` and `Proofs (R0-B Occ, R1 stackcert)` +runs show `total_count >= 1` and a conclusion other than `startup_failure`. + +Both new workflows are `workflow_dispatch`, so they can also be started by hand — +useful for the control, since it avoids waiting on a path filter: + +[source,bash] +---- +gh workflow run session-ir.yml -R hyperpolymath/occupancy-types +gh workflow run proofs.yml -R hyperpolymath/occupancy-types +---- + +== 7. Note on scope + +`hyperpolymath` is a user account, so the repository-level setting is authoritative; +there is no organisation policy above it that could override the change. (If this were +an org-owned repo, an org-level allow-list would win, and the fix would have to be +applied there instead — worth checking if the outputs above look right but runs still +show `jobs: 0`.) diff --git a/docs/recon/COORDINATED-PLAN-2026-10-04.adoc b/docs/recon/COORDINATED-PLAN-2026-10-04.adoc new file mode 100644 index 0000000..0d90d8e --- /dev/null +++ b/docs/recon/COORDINATED-PLAN-2026-10-04.adoc @@ -0,0 +1,367 @@ += Coordinated plan — the seven repos, 2026-10-04 + +_Companion to:_ `docs/recon/TYPE-FAMILY-POSITION-2026-10-04.adoc` (the position) and +the follower-notes working copy (consumer outreach; kept out of the public repo until the messages are sent). +_Scope:_ `echo-types`, `epistemic-types`, `residual-evidence-types`, `choreographic-types`, +`tropical-types`, `occupancy-types`, `absolute-zero`, the `nextgen-typing` hub and the satellites. + +''' + +== 1. The governing idea + +The recon found one asymmetry that should drive the whole plan: + +[quote] +____ +**Most of the estate's claims are already true and already fenced — but a large fraction are +not _machine-enforced_.** Proof work that exists on disk is unreceipted (no CI lane, no +toolchain run, no issue), while several workflows that appear to gate it die at startup. +____ + +So the plan is not "do more research". It is, in order: _(W1) make what exists checkable_, +_(W2) convert the five cross-family arrows from proposed to checked_, **(W3) time-box the two +open keystones*, _(W4) run the occupancy rungs through their own kill gates_, *(W5) build +consumers so the work has external standing**. Research ambition is capped deliberately: the +plan's job is to make the boundary between _established_ and _open_ impossible to misread. + +=== Principles (non-negotiable, because they are the estate's credibility) + +. _Receipts over claims._ A result is [RAN] (command + output), [CI] (run id + commit), [DOC] + (dated author run), or it is _not established_. Upgrading [DOC]→[CI] is the cheapest work in + the estate and the highest value. +. _Blocked ≠ retracted._ Blocked items carry the exact command that would unblock them. + Retractions are recorded with the counterexample. Both ledgers already exist — keep using them. +. _Separation before capability._ Every family's identity rests on matched-negatives or + no-go results. A new capability claim without a separation is a naming exercise. +. _Kill criteria are pre-written and honoured._ occupancy-types §3 has them per rung; + absolute-zero warns that a too-clean composition result is probably wrong. Obey the ledgers, + not the momentum. +. _No arrow as dependency._ The type-family map's dashed arrows are obligations, not imports. + The one deliberate exception (occupancy's "no cross-kernel imports") stays. + +''' + +== 2. Workstreams + +=== W1 — Make the receipts real (highest leverage, mostly mechanical) + +[cols="1,1,1,1,1",options="header"] +|=== +| # | Task | Repo | Owner | Closes with + +| W1.1 | Read the Actions posture; if `selected`/short, PUT the canon allow-list; re-run the gates | occupancy-types | _owner-only_ | a push where Secret Scanner + Governance + a checker job _start and pass_ (issue #6) + +| W1.2 | Wire the Session IR manifest as a CI job (`PYTHONPATH=src python3 -m session_ir test …`, 14/14 today) | occupancy-types | automatable | green job on `main`; regression visible + +| W1.3 | Build `verification/proofs/` in CI (XP‑1 currently unenforced) | nextgen-typing | automatable | green job; issue #57 + +| W1.4 | Extend Isabelle `ROOT` to all 9 theories + add the Isabelle job | tropical-types | needs Isabelle | PROOF-STATUS's "CI-gated" claim becomes true; issue #57 + +| W1.5 | Lane `experimental/echo-additive` + the 4 bit-narrowing modules | echo-types | automatable | modules in `All.agda`/a lane or archived; issues #320/#321 + +| W1.6 | Pin the Agda toolchain (drop unpinned `apt-get agda`) | echo-types | automatable | pinned version in workflow; issue #322 + +| W1.7 | Make CI mirror the local all-provers gate (or say so loudly in CI + README) | absolute-zero | author | issue #161 closed or scoped honestly + +| W1.8 | _Estate-wide: treat `STARTUP_FAILURE` as failure for required checks_ (§6.2) | all | owner (settings) | no PR can merge with zero CI signal; echo-types#330 + +| W1.9 | File the missing issue(s) for repos with dead CI and no tracker entry | occupancy-types | done (issue #6) | — + +| W1.10 | Remove tracked `__pycache__` (7 files) + ignore rule | occupancy-types | _done this session_ | clean tree + +|=== + +_Why first:_ W1 costs days, converts a large body of [DOC] into [CI], and — critically — +W1.8 and W1.1 also _unblock_ every future automated check. Right now a green badge in this +estate is not evidence that anything ran. + +=== W2 — Mature the interfaces (the five arrows) + +The hub's `TYPE-CONNECTIONS.adoc` lists what each connection needs. Current state, from the +recon: Echo→Residual and Epistemic→Residual cover _Milestone 1 only_; Echo→Choreographic and +Epistemic→Choreographic have _no proof_; Tropical→Choreographic needs a grading semantics. + +[cols="1,1,1,1",options="header"] +|=== +| # | Task | Repo | Closes with + +| W2.1 | Comparisons 2.0: do composition (`compose-claims`) and revision (`survives-retraction`, `revise`) transport beyond `Echo.Echo` / `SoundWarrant`? | residual-evidence-types | a checked answer either way — _"no, a richer interface is needed"_ is a publishable result + +| W2.2 | _Cost vs state as a separation_: exhibit a composition where the HWM grade and the cost grade cannot be identified | occupancy + tropical | a witness pair + a no-identification theorem (cheap, falsifiable, cross-family) + +| W2.3 | Projection model + correspondence theorem for the echo loss-grade on a projection | echo ↔ choreographic | a stated projection with a proved commuting square (two-event case first) + +| W2.4 | `K-CUT-WARRANT` statement with side conditions (`SoundWarrant` receiver-local) — _state it precisely before proving it_ | epistemic ↔ choreographic | a written statement + its side conditions, reviewed + +| W2.5 | Grading semantics for bounds under interaction (declared algebra, not a port) | tropical ↔ choreographic | a semantics + a projection theorem, or a documented negative + +| W2.6 | Reconcile the choreographic "echo loss-grade" vocabulary with the shared glossary (index ≠ measure ≠ grade) | choreographic + hub | README/glossary agreement; hub roadmap item closed + +| W2.7 | Refresh stale STATE files against their own PROOF-STATUS | residual-evidence, tropical, absolute-zero | a state file that does not contradict the receipts + +|=== + +_W2.2 is the sleeper._ The estate's central architectural claim is that cost and state are +different axes; both halves already exist in separate repos; and the claim is a _separation_, +which means it is cheap to make and cheap to falsify. If it fails, that is important news for +occupancy's thesis. It should be done early. + +=== W3 — Keystones, time-boxed and pre-falsified + +[cols="1,1,1,1,1",options="header"] +|=== +| # | Task | Repo | Time box | Kill / honest outcome + +| W3.1 | Two-event K-CUT-LOSS square under `Independent₂` | choreographic | 1–2 sessions | if `Independent₂` needs hypotheses that trivialise it, record that + +| W3.2 | A _second, non-degenerate_ projection pattern | choreographic | after W3.1 | if degeneracy is incidental, K-CUT gains standing; if essential, the assembly hypothesis narrows honestly + +| W3.3 | Bachmann–Howard `ψ₀(Ω_ω)` fidelity (Lane 3, retired from echo-types) | echo-types | multi-session frontier | remains OPEN by D-2026-06-14; the 2 Fidelity postulates are the only ones in the tree + +| W3.4 | OND-6 conditional composition | absolute-zero | research-grade, last | the roadmap already warns a too-clean positive result has dropped a term + +| W3.5 | Kernel-certificate / guardrail re-check after any W3.3 movement | echo-types | per change | `Smoke.agda` + `All.agda` + guardrails green + +|=== + +_Rule for W3:_ nothing here is allowed to block W1/W2, and every item ships a written negative +outcome. Lane 3 was already retired once from echo-types for outgrowing the project — that +precedent is the model. + +=== W4 — Run the occupancy rungs through their own gates + +[cols="1,1,1,1",options="header"] +|=== +| # | Task | Blocked on | Then + +| W4.1 | Idris 2 Occupancy spike: `idris2 --check Occ.idr` + `Demo.idr` + 4 rejection controls; answer the kill question (constant grades tolerable _and tight_?) | `idris2` installed | R0‑B Piece 2 closes or the kill criterion fires + +| W4.2 | stackcert: `lean StackcertCore.lean`, `#print axioms cert_sound`, fixture run + 4 negative controls | `lean`/`lake` installed | replaces the CONJECTURE with a pasted axiom footprint + +| W4.3 | Zephyr painted-stack HWM fixture on `qemu_cortex_m3` | `west` + QEMU + Zephyr SDK | R1's ground-truth protocol can run: measured ≤ certified + +| W4.4 | R2 static pools + affine/linear handles, T1 coherence theorem | W4.1–W4.3 | _project gate_: no external consumer + no theorem beyond restatement ⇒ archive with a ledger entry + +| W4.5 | Phase‑2 "protocol cut = reclaim" (live memory = f(protocol shape)) | R2 | compositional advantage demonstrated, or kill + +|=== + +_This is the only workstream with a project-level stop written into it._ Treat W4.4 as the +real decision point and do not let it drift into R3/R4/R5 by inertia. + +=== W5 — Consumers and external standing + +[cols="1,1,1",options="header"] +|=== +| # | Task | Closes with + +| W5.1 | Sign + re-anchor the per-repo AFFIRMATIONs at main (nextgen-typing#69) | dated, GPG-signed receipts at current SHAs + +| W5.2 | Register occupancy-types in the hub's type map (question, boundary, connections) — hub#118 | map row + vocabulary fence + +| W5.3 | Re-cite the residual receipts and give Echo→Residual / Epistemic→Residual acceptance criteria (hub#115) | guide updated with acceptance criteria + +| W5.4 | Mirror the general `EchoAggregation` into EchoTypes.jl (echo-types#280) | finite-domain falsifier covers the general law + +| W5.5 | Clear the Pillar E offline half: packaging, DOI, submission | paper submitted (author-driven) + +| W5.6 | absolute-zero artifact-evaluation package (one-command container) | reviewer can reproduce `ALL-PROVERS-GREEN` + +| W5.7 | Follower outreach (see the companion notes file) | replies → real consumers; keeps the estate honest about who actually uses this + +| W5.8 | A public artefact over the outreach: "what a projection/receipt/bound problem looks like, four worked examples" | citable, reaches the same audience without 269 DMs + +|=== + +''' + +== 3. Dependencies + +[source] +---- +W1.8 (treat STARTUP_FAILURE as failure) ──► makes every other gate trustworthy +W1.1 (occupancy Actions posture) ──► W1.2, W4.* receipts +toolchains (idris2 / lean / zephyr) ──► W4.1 ─► W4.2/W4.3 ─► W4.4 (project gate) +W2.1 (interfaces beyond M1) ──► W2.3, W2.4, W2.5 (three of five arrows) +W2.2 (cost vs state separation) ──► independent; strengthens or breaks occupancy's thesis +W3.* (keystones) ──► must NOT block anything in W1/W2 +W5.1/W5.2 (receipts + registration) ──► prerequisite for W5.5, W5.7 credibility +---- + +Two structural notes: _(a)_ W1.8 is a single settings decision with estate-wide leverage — +it belongs in the first hour. _(b)_ The three arrows that depend on W2.1 mean the residual +repo's next question is worth more than its apparent size: it is the hinge for half the map. + +''' + +== 4. Sequence + +_Horizon 1 — this week (all mechanical, no research):_ W1.8, W1.1, W1.2, W1.3, W1.10 (done), +W1.4, W1.6, W1.7; W2.7 (state files); W5.1, W5.2. +*Outcome: every existing proof claim that can be receipted is receipted; no green badge is +false.* + +_Horizon 2 — the quarter (interfaces + the rungs that can run now):_ W2.1, W2.2, W2.6; +W4.1, W4.2, W4.3; W3.1, W3.2; W1.5. +*Outcome: the five arrows either checked or honestly narrowed; occupancy past R1 with ground +truth; K-CUT either advanced one non-degenerate step or falsified at the two-event scale.* + +_Horizon 3 — beyond (research + external):_ W3.3, W3.4; W4.4 decision, then R3–R5; W2.3–W2.5; +W5.4–W5.6; W5.7/W5.8. +*Outcome: external standing, or an honest narrowing — the estate's own decision policy on the +identity claim (echo-types' roadmap: *"if it is refuted, narrow honestly… or stop the identity +claim and retain the suite as Agda exposition"_)._ + +''' + +== 5. What this plan refuses to do + +* _No cross-kernel imports._ occupancy's ULTRAPLAN §1.2 is permanent: not dependent on K-CUT, + Echo, epistemic or secret types. The map is vocabulary, not a build graph. +* _No new surface language before a certificate checker has a user_ (occupancy non-goal). +* _No capability claim without a separation_ (echo-types' gate discipline). +* _No "one more prover" for absolute-zero before CI mirrors the gate it already has._ +* _No 269-message outreach._ Narrow, falsifiable, per-person hints only — the alternative is + noise with a reputational bill. +* _No treating a conceptual arrow as a dependency, an equivalence, or a theorem._ + +''' + +== 6. Measurement discipline — how to read a pass rate + +*Added 2026-10-04, after the recon. Every figure below was measured that day from the Actions +API — never from a badge.* + +=== 6.1 Two ratios, never one + +A single "pass rate" is ambiguous in a way that flatters a broken pipeline: a run that never +executed is still a run, so 96 non-executions read as "96% failing" — and when the gate that +never starts is the one that would have failed, a disarmed repo can read _green_. Split it: + +[cols="1,1,1,1",options="header"] +|=== +| Ratio | Definition | Measured 2026-10-04 | Target + +| _R1 · executed / required_ | required checks that produced at least one job | _~0/100_ in occupancy-types; _≈100%_ in the five repos whose proof jobs run | _100%_ + +| _R2 · passed / executed_ | executed checks ending in success | _≈100%_ in every proof lane measured — epistemic 21/21, residual 39/39, tropical Lean 13/13, absolute-zero Proofs 5/5, echo-types green at HEAD | _100%_ for proof lanes; _no threshold_ for tightness (6.4) + +|=== + +The occupancy-types figure in full: of the last 100 runs, 96 `startup_failure`, 3 `failure`, +1 `success` — and _exactly 4 runs had any job at all_, all four being dependency-graph +"Update" workflows (pip, hex, npm_and_yarn, github_actions). No gate in that repository has +ever executed a single job. + +_Rule: report R1 before R2._ A pass rate quoted without its execution rate is not a +measurement — and a "100% pass" over 0 executed checks is precisely what a dead pipeline looks +like. + +=== 6.2 Green must mean executed + +A green tick is evidence only if a job ran. Enforce three things: + +* _`STARTUP_FAILURE` counts as failure_ for every required context, and so does a required + context that reports no jobs (W1.8; the recommendation in echo-types#330). +* _Every receipt names a run id and a commit._ `[CI]` in the estate's tagging means "a job + started and passed", never "a workflow is listed". +* _Prefer a revoked badge to a stale one._ A repo whose gates cannot run should say so in the + README rather than display workflow badges that no longer execute — the badge is the single + most misleading artefact in a disarmed pipeline. + +=== 6.3 Proof lanes carry zero flake tolerance + +Proof checking is deterministic: same toolchain, same inputs, same verdict. There is no +legitimate "sometimes" for `agda All.agda`. A proof lane's expectation is _100%_, and any +deviation is a bug in the pipeline or the environment — never noise to budget for. + +What the estate's own record shows (last 100 runs per repo, 2026-10-04): every prover red in the +window had a cause — + +* _real breakage_ — echo-types' Agda lane on 2026-09-27 (`39a7a99c`) and 2026-09-30 + (`f11031f2`), the "Typecheck full suite" step failing: main was genuinely broken, then fixed. + The cold-check step (`--ignore-interfaces`, no cache) failed in the same runs; +* _supersede_ — a concurrency `cancel` (absolute-zero `Proofs` `27d879f5`; echo-types Agda + `36919959218`); +* _infrastructure_ — the `startup_failure` family. + +_No case of the same commit passing and failing at random was found._ That distinction is the +point: _flakiness_ trains a team to re-run until green and is the thing to hunt; a +red-with-a-cause is a bug report carrying a file and a line number, and it is the system working. + +The one real drift risk is the environment, and it is documented: echo-types#322 — +`agda.yml` performs an unpinned `apt-get install -y agda`, so *the prover under the proofs can +change without a commit*. Pin the toolchain (W1.6) and keep the guardrails already in place: +`--safe --without-K`, the postulate/escape greps, the `Smoke.agda` pins, the kernel certificate. + +=== 6.4 Tightness is a distribution, not a gate + +Keep the asymmetry ULTRAPLAN §6 already states: + +* _Soundness_ — _"measured ≤ certified on every run. Violation = stop + ledger entry"_ → + _100%, zero tolerance_. This is a correctness property, not a benchmark. +* _Tightness_ — _"certified/measured per unit; report distribution"_ → _not pass/fail_. + +Do not turn tightness into a threshold. A limit loose enough never to fire is decoration; one +tight enough to fire on measurement noise teaches everyone to ignore red — exactly the failure +mode 6.3 exists to prevent. Report the distribution, watch it move, and act on trends with a +named cause. + +Also note the current state: _nothing has been measured yet._ The Zephyr painted-stack fixture +(W4.3) is still a fixture request, so R1 ground truth does not exist. "Benchmarks occasionally +drift" is not the situation; "no benchmark has ever run" is. + +Retries are permitted for genuinely non-deterministic infrastructure — package/action downloads, +superseded runs, cancelled fuzz batches — and are _never_ permitted to produce a green verdict +on a claim that was not checked. Blocked ≠ retracted; blocked ≠ passed. + +=== 6.5 Three kinds of red, three responses + +[cols="1,1,1",options="header"] +|=== +| Kind | Signature | Response + +| _Real breakage_ | job ran; a named step failed | Fix or revert; the run id goes in the ledger entry + +| _Environment / infrastructure_ | job never started, or a dependency fetch failed | Fix the cause (pin, allow-list, retry policy) and file it; never re-run to green + +| _Supersede / cancel_ | `cancelled`; a newer run exists on the same ref | Nothing — but confirm a later run executed + +|=== + +=== 6.6 Recompute it + +[source,bash] +---- +# R1/R2 inputs for a repo — conclusions, from the API, not badges +gh api "repos/hyperpolymath/occupancy-types/actions/runs?per_page=100" \ + --jq '[.workflow_runs[].conclusion] | group_by(.) | map({(.[0]): length}) | add' + +# R1 precisely: did a run actually execute any job? +gh api "repos/hyperpolymath/occupancy-types/actions/runs//jobs" --jq '.total_count' +---- + +''' + +== 7. How to tell whether the plan worked + +*Measure everything below with §6's ratios: _R1 before R2_, and green-means-executed.* + +Falsifiable, in order of cheapness: + +. _`STARTUP_FAILURE` cannot masquerade as green_ in any estate repo (W1.8). Check: force a + failing workflow and confirm it blocks; check that a required context that never starts + reports failure. +. _Every "[DOC] verified" line in PROOF-STATUS has a corresponding green run id_, or is + explicitly marked as not CI-covered. Check: grep the PROOF-STATUS files against the Actions + API. +. _The cost/state separation is settled either way_ (W2.2) — a witness + no-identification + theorem, or a documented collision that narrows occupancy's thesis. +. _K-CUT is either non-degenerate-advancing or honestly narrowed_ to what a two-event square + can support (W3.1/W3.2), with the degenerate case's status written down. +. _At least one external consumer_ exists for one artefact (W5.5–W5.8), or the R2 project + gate fires and occupancy is archived with a ledger entry — which is a _success_ under its + own rules. +. _No state file contradicts its repo's receipts_ (W2.7). This is the cheapest measure of + estate coherence, and today three fail it. + diff --git a/docs/recon/TYPE-FAMILY-POSITION-2026-10-04.adoc b/docs/recon/TYPE-FAMILY-POSITION-2026-10-04.adoc new file mode 100644 index 0000000..d1dd2ea --- /dev/null +++ b/docs/recon/TYPE-FAMILY-POSITION-2026-10-04.adoc @@ -0,0 +1,711 @@ += Type-family position — deep recon + +_Date of recon:_ 2026-10-04 · _Prepared in:_ `occupancy-types` @ `arena/01a1087c-occupancy-types` +_Scope:_ `echo-types`, `epistemic-types`, `residual-evidence-types`, `choreographic-types`, +`tropical-types`, `occupancy-types`, `absolute-zero`, plus the coordination hub +`nextgen-typing` and the satellite repos. + +''' + +== 0. How to read this, and how much to trust it + +The estate is unusually well instrumented for honesty — AFFIRMATIONs, PROOF-STATUS +receipts, retraction ledgers, kill criteria, blocked-item registers. This document tries +to hold to that same standard, so every claim below is tagged with _how we know it_: + +[cols="1,1",options="header"] +|=== +| Tag | Meaning + +| _[RAN]_ | I ran the command in this session and saw the result. First-hand. + +| _[CI]_ | A hosted CI job on the recorded commit passed; run id/URL given. + +| _[DOC]_ | The claim is the repo's own recorded status (PROOF-STATUS / AFFIRMATION / STATE / README), reproduced by an author in a stated environment, _not_ re-run by me and not covered by a CI receipt in this recon. + +| _[ISSUE]_ | The claim comes from a filed issue (i.e. a known, acknowledged defect or task). + +| _[INFER]_ | My inference from file evidence; stated plainly as such. + +|=== + +_Calibration — what this session could and could not do._ This sandbox has +`python3` and `git` only. It has _no_ `agda`, `lean`/`lake`, `idris2`, `coqc`, +`isabelle`, `mizar`, `z3`, `just`, `bun`, or Rust toolchain. Therefore: + +* Every Agda / Lean / Isabelle / Coq result is _[DOC]_ or _[CI]_ — I did _not_ + re-typecheck any proof. Where a hosted run exists, I cite the run id. +* The one proof-adjacent thing I could re-run was `occupancy-types`' Session IR gate — it + passed 14/14 _[RAN]_. +* Repo trees, docs, roadmap text, ledger entries, workflow contents, CI conclusions, + issue text and commit signatures were all read directly from clones and the GitHub API. +* CI conclusions were read from the API, not inferred from READMEs or badges. + +_Anchor pins_ (HEAD at recon time; all commits GPG-verified _[API]_): + +[cols="1,1,1",options="header"] +|=== +| Repo | HEAD | Date + +| echo-types | `da140cc26f` | 2026-10-03 + +| epistemic-types | `eb810d4ee7` | 2026-10-04 + +| residual-evidence-types | `62d7490754` | 2026-10-02 + +| choreographic-types | `71ba51d3b8` | 2026-10-03 + +| tropical-types | `ad7bfdfd56` | 2026-10-03 + +| occupancy-types | `2e276c365f` | 2026-10-04 + +| absolute-zero | `5f27136835` | 2026-10-02 + +| nextgen-typing | `70df154951` | 2026-10-01 + +| EchoTypes.jl | `a0ac9131f7` | 2026-10-01 + +| EpistemicTypes.jl | `6ab3fb4a01` | 2026-10-01 + +| ResidualEvidenceTypes.jl | `abe97d5c99` | 2026-10-01 + +| secret-types | `aed3f1cc2d` | 2026-10-04 + +|=== + +=== The three-tier vocabulary used throughout + +* _There (established)_ — a machine-checked artefact exists _and_ it is either + receipted by a current CI run or reproducible by a named local command; the claim is + fenced by an explicit written boundary. +* _Nearly there_ — the artefact exists in the tree but one link is missing: no CI lane, + no toolchain run, an unwired module, a stale state file, or a theorem that is true but + degenerate relative to the claim it is cited for. +* _Within reach_ — the repo's own next step, already specified in a roadmap, ledger + entry, or open issue, needing no new research — only work. Everything beyond this line + is named as _open research_ rather than aspiration. + +''' + +== 1. The estate map (as it stands) + +The five research families and their owning repos, with questions and boundaries exactly +as `nextgen-typing`'s shared guide states them _[DOC: TYPE-CONNECTIONS.adoc]_: + +[cols="1,1,1",options="header"] +|=== +| Family | Question | Fence (what it is _not_) + +| _echo-types_ | Which possible origins lie over an output after a transformation? `Echo f y = Σ (x : A), f x ≡ y` | An output need not identify its origin; a numeric residue measure does not determine residue structure + +| _epistemic-types_ | From which standpoint is a claim available, with what evidence? `E κ A` | Having evidence ≠ proof of the claim; belief/knowledge/sound warrant have different interfaces + +| _tropical-types_ | How do declared resource bounds compose? | The algebra must be stated; a bound is neither a probability nor an Echo residue identity + +| _residual-evidence-types_ | Which worlds satisfy an observation _and_ its evidence constraints? | Constructing a candidate does not recover the world; real-world soundness needs the actual-world premise + +| _choreographic-types_ | What happens to distinctions, bounds and warrants under projection to participants? | A causal-order cut is not Gentzen cut-elimination, nor causal identification; the general K-CUT is open + +|=== + +Neighbours in the same map but _out of the type family proper_: + +* _occupancy-types_ (this repo) — _state_ resource grades (HWM monoid, non-commutative), + deliberately separated from tropical _cost_ grades; session/protocol frontier reclamation. +* _absolute-zero_ — CNO (certified null _effect_) and OND (certified null _disclosure_); + a multi-prover effort with an Echo bridge module. Not one of the five families; connected + to them (and proposed for a map row in absolute-zero#175 _[ISSUE]_). +* _secret-types_ — new (created 2026-09-27), specification-stage only. Owner ruling + 2026-10-04: this is the home for secret types; `epistemic-types` adds no Secret API; + epistemic-types#29 closed, #32 transfer pending GitHub issue-write access _[DOC: STATE.a2ml]_. +* _nextgen-typing_ — the coordination hub: shared glossary, ownership routing, the + cross-project proof. It hosts no family code. + +_Vocabulary fences that are load-bearing and currently holding_ (worth stating because +they are the estate's main defence against concept collapse): + +[quote] +____ +cost grade ≠ occupancy (HWM) grade ≠ echo index ≠ residue measure ≠ warrant ≠ residual +____ + +The guide is explicit that the five families are **complementary questions, not ranks of +type-system strength**, and that dashed arrows in the map assert *conceptual use or a +proposed research task* — not dependency, equivalence, or a checked bridge +_[DOC: TYPE-CONNECTIONS.adoc]_. + +''' + +== 2. Per-repo deep recon + +=== 2.1 `echo-types` — the most developed family member + +_What it is._ Constructive Agda formalisation of proof-relevant fibres as witnesses of +structured (non-total) information loss. 209 `.agda` files under `proofs/` _[RAN: file count]_; +the verified closure (`proofs/agda/All.agda`) is described as ≈200 modules and +_postulate-free_. + +_There (established)._ +* The Agda suite typechecks under `--safe --without-K`, and the _hosted Agda job is green_ + on current main: run `37152181722` @ `da140cc2`, 2026-10-03 _[CI]_. +* A canonical-identity spine landed 2026-05-27: `EchoTotalCompletion` (`A ≃ Σ B (Echo f)`), + the (equivalence, projection) factorisation, no-section results, four-axis loss/residue + taxonomies, and audience modules _[DOC: PROOF-STATUS, README]_. +* _Matched-negative separation proofs_ — where the identity claim does its real work: + Echo is not distinguished by Shannon entropy; the LL `!A := 1` shallow-encoding gap; + equal measure ⇏ equal Echo (`Echo.Separation.NotResourceInstance`) _[DOC]_. +* An ordinal/Buchholz track with a sound carrier: doubled-ladder well-foundedness, + Brouwer `ω^^_`/`ε₀`, and a real Buchholz notation order with well-foundedness _[DOC]_. +* Retraction discipline: R-2026-05-18 narrowed four headline claims (graded comonad → + thin-poset reindexing modality; universal property → funext-relative pointwise mediator; + model-independence → carrier-parametricity; conservativity metatheorem → postulate-free + build that is _evidence for_, not proof of) _[DOC: AFFIRMATION, roadmap]_. +* A cross-project proof `EchoTyping.agda` (XP-1: pipeline information-loss = echo fibres, + spanning echo-types ↔ affinescript ↔ typed-wasm) lives in `nextgen-typing` _[DOC]_. + +_Nearly there._ +* _Identity gates are at PROVISIONAL / PASSED-narrowed, none STABLE-ESTABLISHED_ + (Gate 1 PROVISIONAL, Gate 2 PASSED (narrowed), Gate 3 PROVISIONAL) _[DOC: roadmap]_. +* _WFS, not OFS_: diagonal lifts and uniqueness-up-to-iso exist, but unique diagonal + fills are unproved; the module name `EchoOrthogonalFactorizationSystem` overstates the + target (renaming pending) _[DOC: README caution block]_. +* _Lane 1 (type-theoretic standing) is IN-REPO CLOSED, EXTERNALLY OPEN_ — the paper is a + living draft; the offline half (submission, DOI, packaging) is author-driven _[DOC]_. +* `experimental/echo-additive` (7 modules incl. the `Grade` dioid) is _in no CI lane_ + _[ISSUE #321]_; 4 bit-narrowing modules are similarly unlaned _[ISSUE #320]_. +* Doc/toolchain debts: `README.adoc` still carries RSR `+{{PLACEHOLDER}}+` template material + while `README.md` is canonical _[RAN: file read]_; `agda.yml` installs an unpinned + `apt-get agda` _[ISSUE #322]_; governance red on `CONTRIBUTING`/gitleaks + _[ISSUE #323]_; CodeQL startup-failure _[ISSUE #269]_. + +_Within reach._ Rename to honesty (`EchoWeakFactorizationSystem`); wire the unlaned +experimental modules into CI; clear the packaging/DOI half of Pillar E; refresh +`README.adoc` out of template state. + +_Open research (not reachable by wiring)._ Bachmann–Howard `ψ₀(Ω_ω)` order-type fidelity +(D-2026-06-14, _OPEN_ — `ε₀ ≪ Γ₀ ≪ …`); the two quarantined postulates in +`Ordinal/Buchholz/Fidelity.agda`; the `∥_∥` image truncation (cannot be built under +`--safe --without-K` without HITs — present only in a `--cubical` island); the unbudgeted +global `wf-<ᵇʳᶠ` (walled: the native order is ordinally unsound, with a documented +counterexample). + +''' + +=== 2.2 `epistemic-types` — small, self-contained, genuinely green + +_What it is._ A minimal-of-design Agda prototype for standpoint-indexed modalities, +separating knowledge (factive) from belief (non-factive) and warrant from sound proof. +The base modality is deliberately _not_ a monad or comonad. + +_There (established)._ +* The **whole library type-checks under `--safe` with zero postulates and no standard + library** (`--no-libraries`, only `Agda.Builtin.*`), and the **hosted `Proof Safety` job + is green on the current HEAD*: run `37187387026` @ `eb810d4e`, 2026-10-04 *[CI]**. +* Module inventory is concrete: 17 modules listed in STATE, including `Base`, `Warrant`, + `Access`, `ProofTransport`, `ReadConsistency`, `EchoBridge`, `SurrealBridge`, and an + Applications layer _[DOC]_. +* The _Applications layer (2026-09-27)_ is a real worked result, not a demo: + `QCriterion.qBound-≤-Q` over an arbitrary `OrderedGroup`; `RapidNJSkip` generating a + warrant from a skip certificate with `skip-known` proved; `IntegerModel` discharging the + arithmetic budget; a rejection fixture for an unchecked check _[DOC: PROOF-STATUS]_. +* Explicit non-claims are recorded: no ℚ instance, no rescaling transport, no row-insertion + update, no cross-iteration bound reuse _[DOC]_. +* Concrete Echo adapter: `SurrealBridge` relaxes a proved upper bound on a residue measure + along the access order while preserving the retained value; the `daySurrealAccess` + instance is explicitly a set-sized fragment, _not_ the Conway proper class _[DOC]_. +* `ReadConsistency` was corrected so `ReadView` entails equality with indexed store + contents; the older version-only relabelling and free `Sync` witness were _removed_ + _[DOC]_. + +_Nearly there._ +* STATE calls it `prototype` / `experimental` at _35% completion_, last-updated + 2026-10-04 — i.e. the repo itself does not claim maturity _[DOC: STATE.a2ml]_. +* The Applications obligations are named but unmet (rational instance, rescaling + transport, row-insertion invariants). +* The proof-transport soundness story is qualified ("holder-dependent transfer is + explicitly qualified") _[DOC]_. + +_Within reach._ Close the named Applications obligations; settle the secret-types +handover (epistemic-types#32 transfer is blocked on GitHub issue-write access — an +_administrative_ blocker, not a technical one) _[DOC/ISSUE]_. + +_Open research._ Whether `bind`/`extract` structure is wanted at all (currently a +deliberate "future commitment, not a hidden assumption"); the soundness map from evidence +to claim meaning under a standpoint index. + +''' + +=== 2.3 `residual-evidence-types` — newest, fastest-moving, and the only family with a machine-checked _correspondence_ + +_What it is._ Evidence-indexed residual types: which worlds are compatible with an +observation _and_ its declared evidence constraints, and what holds for all of them. +Founded 2026-09-09 from imported Windows-Downloads material (assessment + a standalone +HTML/JS explorer), with _all core work newly written in-repo_. + +_There (established)._ +* _Milestone 1_ — presence without identification (`u+n=2`, `n≤1` establishes `u≠0` + while `(1,1)` and `(2,0)` still disagree), evidence-refined fibre round trips, + conditional actual-world soundness, claim transport under refinement; three invalid + modules must be rejected by Agda _[DOC]_. +* _Milestone 2_ — contexts of assumptions with thinnings, dependency-preserving + composition and coarsening, constructive revision and retraction, **a certified finite + checker proved equivalent to the explorer by `refl` over all 546 configurations** + (`Correspondence.checker-matches-explorer`), and nine expected-rejection controls + _[DOC]_. +* _Both sibling interfaces are actually imported_ — Echo's fibre packaging round-trips, + and Epistemic's `SoundWarrant` requiring explicit actual-world premises — pinned to + sibling heads (`echo-types` `9c4b72b5`, `epistemic-types` `dd948fbd` for M1) _[DOC]_. +* Hosted _`Agda proofs` job green_ on the current HEAD: run `36949121242` @ `62d74907`, + 2026-10-02, and a prior receipt run `36740394802` @ `befdf964` _[CI/DOC]_. +* The repo is scrupulous about the limit: the correspondence certifies the *finite checker + against the explorer*, _not_ the ℕ core against the explorer _[DOC]_. + +_Nearly there._ +* `STATE.a2ml` (last-updated 2026-09-09) is _stale_: it still lists composition, + revision/retraction, the certified checker and the explorer correspondence as _pending_ + — all of which Milestone 2 landed _[RAN: file read vs PROOF-STATUS]_. +* The two sibling comparisons cover _Milestone 1 only_; whether composition/revision need + an interface beyond `Echo.Echo` and `SoundWarrant` is the explicitly open question + _[DOC]_. +* A separate "starter archive" named in the imported assessment has _not been recovered_ + and the repo does not pretend otherwise _[DOC]_. +* Codeac status has been pending on main since 2026-09-24 _[ISSUE #11]_. + +_Within reach._ Refresh STATE; run comparisons 2.0 (post-M1 interfaces); the explorer's +signed −6..6 model is already the certified finite object, so further finite-model checks +are cheap. + +_Open research._ Causal specialisation and probability adapters — both explicitly require +models and obligations of their own _[DOC]_. + +''' + +=== 2.4 `choreographic-types` — a pre-registration, and it says so + +_What it is._ The assembly hypothesis: grade a global choreography with echo _loss-grades_ +and epistemic _standpoint-warrants_, project to participants, and ask whether grading and +transport commute with projection across a consistent frontier (a _cut_). The keystone is +_K-CUT_, split into K-CUT-LOSS (equality) and K-CUT-WARRANT (bound, under a `SoundWarrant` +side-condition). + +_There (established)._ +* _The specification and its fences._ The pre-registration (2026-10-03) states that + K-CUT-LOSS and K-CUT-WARRANT remain _OPEN_, that `SoundWarrant` is an *assumed + receiver-local side-condition*, and that the application Agda file **"contains postulates, + not proofs"_ and is not imported by any build _[DOC: docs/pre-registration.adoc]**. +* `CITATION.cff` no longer claims a completed Agda formalisation; integrity checks now fail + such claims on description-mirroring surfaces _[DOC]_. Issue #15 records that the + README/description still overstate _[ISSUE]_. +* CI's two substantive checks — `Secret Scanner` and `Documentation Integrity` — are both + green _[CI]_. There is _no prover workflow at all_, by design at this stage. + +_Nearly there._ +* The _degenerate base case exists and is real_, but it is a sibling's theorem: + `characteristic/RoleGraded.choreo-grade-commute` in `echo-types` — two actions (role + transport × grade degradation) commuting on one Echo-indexed family, satisfying the + "same data" test that struck down the earlier N3 nominee _[DOC/RAN: file read]_. + It is a _single-static-edge integration theorem_, not K-CUT. echo-types' own audit + _declined to adopt it as nominee N5_ on the grounds that its only non-trivial cell is + already credited elsewhere (adoption would be cosmetic) _[DOC: N5Falsifier, IntegrationAudit]_. +* The smallest concrete target is specified: a two-event K-CUT-LOSS commuting square under + an `Independent₂` witness, with the witness required to carry disjoint read/write + footprints, phase safety and a deterministic tie policy _[DOC]_. +* A vocabulary obligation is open: the choreographic README's phrase "echo loss-grade" + conflicts with the estate's separation of echo index / residue measure / resource grade; + reconciling it is a _coordination task_ in the hub roadmap _[DOC: TYPE-CONNECTIONS]_. + +_Within reach._ Wire the existing `rapidnj-two-thread.agda` postulates into a real +minimal proof of the two-event square; land the `Independent₂` witness; reconcile the +vocabulary with the shared glossary. None of that requires solving K-CUT. + +_Open research._ K-CUT in general (both fragments) — the repo's own honest position is +that the general result is open and only degenerate single-static-edge cases exist. + +''' + +=== 2.5 `tropical-types` — dual-formalised, one half verified, one half CI-gated-by-claim + +_What it is._ Max-plus / min-max algebra applied to resource-aware typing: compositional +worst-case bounds for latency, stack use and adversarial round counts, plus a reusable +resource-grade axis for downstream languages. _Note the prover split_: this family is +_Lean 4 + Isabelle/HOL_, not Agda. + +_There (established)._ +* _Lean 4 — verified and CI-gated._ `lake build` green, no Mathlib, toolchain pinned in + `lean-toolchain` (`v4.13.0`); hosted _`Lean` job green_ on current main: run + `37116071270` @ `ad7bfdfd`, 2026-10-03 _[CI]_. PROOF-STATUS records a clean rebuild of + _20/20 targets_ including `TropicalSessionTypes.lean` (max-plus session grading), + `TropicalAdapterPath.lean` (min-max bottleneck transport + the `hub_ceiling` no-go), + the `Resource/Algebra` interface with a _parametric transport theorem_, and concrete + instances (MaxPlus, MinPlus, MinMax, Linear, Affine) _[DOC]_. +* The two twins are related by an order-reversing involution proved as a **lattice + anti-isomorphism** and explicitly _not_ a semiring homomorphism — a structural fact, + stated as such _[DOC]_. +* `Resource/EchoBridge.lean` is an _echo-free residue-measure bridge_ (no dependency on + the echo-types Agda kernel; the relationship is at design level) _[DOC]_. + +_Nearly there._ +* _The Isabelle half is not verified in the recon sense._ Nine `.thy` theories exist and + the session is meant to be CI-gated by `just isabelle-build` + `just check-sorry`, but + _no workflow mentions Isabelle_; `ROOT` lists _5 of 9_ theories; PROOF-STATUS itself + says the Isabelle side was _"NOT re-verified in this environment"_ _[DOC]_. +* Issue #57 states the contradictions directly: the claim is CI-gated but nothing gates it, + ROOT covers 5 of 9, and STATE says GREEN and RED for the same theory _[ISSUE]_. +* The `CI context contract` job is red on recent commits (required-status-check drift); + it is the repo's own guard for `docs/CI-CONTEXTS.adoc` and it fails for that documented + reason — a CI-hygiene red, not a proof red _[CI]_. +* The no-go theorem `hub_ceiling` refutes Protocol Squisher's universal-interoperability + claim — real, but it is a _no-go_, not a capability _[DOC]_. + +_Within reach._ Extend `ROOT` to all nine theories; add the Isabelle job; delete the +residual Deno test files (Deno is banned estate-wide _[ISSUE #58]_); SHA-pin the two +tagged `actions/checkout` uses _[ISSUE #59]_. + +_Open research._ The Buchholz-collapsing ladder (Rungs 2–N, 0% per STATE); tropical time +series (Diehl–Ebrahimi-Fard–Tapia); a probabilistic extension; a Lean tactic for automated +grade calculation. + +''' + +=== 2.6 `occupancy-types` (this repo) — pre-registered, locally reproducible, CI-disarmed + +_What it is._ Stepwise resource-bounding types: deterministic memory first, network +second. The organising claim is that _cost and state are different axes_: cost composes +with `+` in sequence and `max` across alternatives (tropical), while _state_ resources +(pools, buffers, credits, FDs) compose by the _non-commutative high-water-mark monoid_ +`(p₁,n₁)·(p₂,n₂) = (max(p₁, n₁+p₂), n₁+n₂)`. Buffer = memory, and the **protocol frontier +is the reclamation point**. The whole thing is pre-registered in `ULTRAPLAN.md` with +per-rung kill criteria and a decision log (D1–D7). + +_There (established)._ +* _R0-B, Phase 1 — Session IR checker: TESTED. I re-ran it in this session:_ + `PYTHONPATH=src python3 -m session_ir test examples/session_ir/manifest.json` → + _14/14 PASS_, exit 0 _[RAN]_. Seven accept cases with measured steps ≤ certified + bound (including a strict case: certify 5 / measure 4, and a tight case: 6/6) and seven + expected-rejection controls each pinning an error class (double-send, use-after-drop, + protocol mismatch, close-before-End, double-free, leak, alias) _[RAN]_. +* The operational model exists and its Phase-0 kill test is _mechanically audited_ + (four sentences, banned word absent) _[DOC: EXPLAINME C3]_. +* The honesty apparatus is real and already in use: `docs/EXPLAINME.adoc` classifies every + claim as TESTED / UNVERIFIED / CONJECTURE, and `docs/retraction-ledger.adoc` records + blocked rungs (with exact unblocking commands) separately from retractions — with **zero + retractions so far* and three blocked items *[RAN: file read]**. +* The estate placement is correct and deliberate: registered against the cost/state + vocabulary split, with "not echo, not warrant, not residue" written into the plan + _[DOC: ULTRAPLAN §5]_. + +_Nearly there (blocked, not disproved)._ +* _Idris 2 Occupancy spike — UNVERIFIED._ `src/occ/Occ.idr`, `Demo.idr` (static peak = K + = 2 producer/consumer) and four rejection controls exist; no `idris2` on the work + environment's PATH _[DOC/RAN: toolchain check]_. The kill question (are constant grades + tolerable _and tight_?) is answered only provisionally, and the repo labels the answer + CONJECTURE. +* _R1 stackcert — UNVERIFIED._ `src/stackcert/StackcertCore.lean` with the target theorem + `cert_sound`, plus fixtures generated by real `gcc -fcallgraph-info=su -fstack-usage` + _[DOC]_, but no `lean` locally and no `#print axioms` footprint pasted. The expected + empty axiom list is _explicitly marked CONJECTURE until pasted_ _[DOC: EXPLAINME C5]_. +* _Ground truth — BLOCKED._ Zephyr painted-stack HWM on `qemu_cortex_m3` is a **fixture + request**; nothing is measured until it runs. The plan's own rule is "measured ≤ certified + on every run, violation = stop" — so R1 cannot be _closed_ without this _[DOC]_. +* _CI is comprehensively non-functional._ 96 of the last 100 workflow runs on this repo + concluded `startup_failure`, including on `main` pushes by the owner actor; _every_ + gate — Rust CI, Dogfood, Static Analysis, Invisible Character Detection, K9, Secret + Scanner — dies before starting a job _[CI/API]_. The estate has two _documented_ + mechanisms that produce exactly this signature: (a) an Actions allow-list posture of + `selected` with _0 patterns_, which kills any workflow whose step references a + non-allow-listed action, `jobs=0` (choreographic-types#16, with a produced mutant + proof); (b) an actor gate refusing workflow triggering for a given actor + (echo-types#330). The precise gate for _this_ repo is _not established_ from here, and + unlike its siblings this repo carries _no open issue_ about it (it has no open issues + at all). Consequence: _none of this repo's checks are currently machine-enforced_; + the local gates are the only source of truth. +* `README.adoc` is still RSR template material (self-declared in-file) _[RAN]_. + +_Within reach (needs a toolchain or a settings change, not research)._ Install +`idris2` → run the spike and its four controls; install `lean`/`lake` → run stackcert and +paste `#print axioms cert_sound`; obtain the Zephyr fixture; fix the Actions settings +(owner-only PUT) and file the missing issue for this repo; refresh `README.adoc` from the +template. + +_Open research (the actual rungs)._ R2 static pools + affine/linear handles with the T1 +coherence theorem (project gate after R2); R3 binary session channels with HWM buffer +grades; R4 network-calculus curves over ℕ/ℤ without reals; R5 multiparty projection and the +projection/grade commutation question; Phase 5 host-tool contract. The pre-written kill +criteria are, correctly, part of the design: R2 archives the project if there is no external +consumer for certificates and no theorem beyond restatement. + +''' + +=== 2.7 `absolute-zero` — the most _concretely_ verified repo in the estate + +_What it is._ Two co-equal pillars — _CNO_ (a program that provably does nothing to the +world) and _OND_ (a program whose observable trace is constant over its secret input, +relative to a declared observation model `O`). The pillars are logically independent (a +proved theorem) and joined by a _coupling dial_ that is explicitly _framing, not theorem_. + +_There (established)._ +* _A single gate reproduces everything locally_: `proofs/verify-all-provers.sh` → + `ALL-PROVERS-GREEN` across _Coq, Agda, Lean 4 (+Mathlib), Z3, Isabelle/HOL, Mizar_, plus + the _Idris 2 ABI_, with an absent prover treated as _failure, never skip_ (since + 2026-09-23), Z3 verdicts checked against `; expect sat|unsat`, and a Coq + `Print Assumptions` audit with its own control _[DOC: PROOF-STATUS]_. A gate self-test + proves the gate turns red for each absent/failing prover and each verdict/audit mutant + (16 cases, run in CI) _[DOC]_. +* _CI Proofs job green_ on current main: run `37077637092` @ `5f271368`, 2026-10-02 + _[CI]_. The workflow runs the lightweight provers (Coq 14/14 theories, Agda CNO+OND, + Z3 CNO+OND, Mathlib-free Lean core with an `AxiomAudit`); the heavy provers are covered + only by the local container gate — and the workflow says so in its own header **[RAN: + workflow read]**. +* _OND-1..5 and OND-7 are landed_ — proved in Coq with _zero axioms_ (every theorem + `Closed under the global context`), mirrored in Lean 4, Agda and Z3 _[DOC]_. +* _CNO axiom discharge 98 → a small classified remainder_, with the pathological cases + found and fixed rather than hidden: `no_cloning` and `Cconj_Cexp` were _provably false_ + and removed; `eta_equivalence` was _false as stated_ (counterexample `f = LVar 5`) and + replaced by an honestly guarded theorem _[DOC]_. Remaining axioms are tagged either + `METAL-BOUNDARY` (genuine physics: `kB>0`, `temperature>0`, Second Law, Landauer) or + _class-A_ (true, provable in principle, listed with blockers — 4 items) _[DOC]_. +* An _Echo bridge exists in Agda_ (`EchoBridgeCNO.agda`): `EchoRel` instantiated + against real `CNO.Program`/`CNO.eval` with `CNO.state-eq` _[RAN: file read]_. +* Roadmap restraint is explicit: the long-horizon "universal CNO standard" is quarantined + in an appendix as _aspirational and unfunded_, "a direction of travel, not a + commitment with a date" _[DOC]_. + +_Nearly there._ +* _OND-6_ (conditional composition) is _open by design_ — the research capstone. The + roadmap warns, correctly, that if composition appears to hold as cleanly as for CNOs the + result has almost certainly dropped a term _[DOC]_. +* _CI is weaker than the local gate_ and the repo knows it: for a time Isabelle and Mizar + printed "skipped" while the gate said GREEN; that is fixed in the local gate, but + absolute-zero#161 records that the `Proofs` workflow still has a `paths:` filter, + `z3 … || true`, and no assumption check _[ISSUE]_. +* _Documentation drift_: `ROADMAP.adoc` (last updated 2026-07-07) still lists as pending + the Idris ABI repair and "make CI truthful: run Coq+Agda+Rust", both since superseded by + `PROOF-STATUS` and the current workflow _[RAN: file comparison]_. +* 73 of 182 Coq theorems rest on axioms and 38 `Axiom`/`Parameter` declarations use four + tag forms (unify grammar, generate census) _[ISSUE #171]_; 2 Idris2 postulates in + `src/abi/Layout.idr` remain _[ISSUE #27]_; Scorecard has 5 high alerts _[ISSUE #170]_. + +_Within reach._ Make CI mirror the local all-provers gate (fix #161); unify the axiom tag +grammar and publish the census (#171); port the Coq filesystem model to Lean so the +`FilesystemCNO` law axioms become theorems (#167); refresh the roadmap against PROOF-STATUS; +the artifact-evaluation one-command container. + +_Open research._ OND-6 conditional composition; the 4 class-A Coq items +(`CNOT_gate_unitary`, `unitary_inverse_property`, `fidelity_bound` need a finite-dim/tensor +model; `y_not_cno` needs a coinductive/step-indexed β non-termination argument); the paper. + +''' + +== 3. The hub, the satellites, and the name-collisions + +=== 3.1 `nextgen-typing` (coordination) — the map is the artefact + +* Hosts the shared glossary, ownership routing and the _XP-1 cross-project proof_ + (`verification/proofs/agda/EchoTyping.agda`, `--safe --without-K`, spanning echo-types ↔ + affinescript ↔ typed-wasm) _[DOC]_. +* _But nothing runs it_: nextgen-typing#57 records that no CI job runs + `just proof-check-all` _[ISSUE]_. The estate's only cross-project proof is therefore + unenforced. +* Open coordination tasks relevant to the family: *#118* register `occupancy-types` in + the type map + cost/state vocabulary split + boundary notes (this repo is not yet + registered); *#115* re-cite the residual receipt and give the Echo→Residual / + Epistemic→Residual obligations acceptance criteria; *#69* verify and GPG-sign the + per-repo AFFIRMATIONs in-env; *#117/#121* two pre-existing CI reds. +* The hub's own readiness self-assessment is _Grade C_ ("dogfooded, CI passing"), and its + stated path to Grade B is _external adoption_ — 6+ diverse external targets _[DOC]_. + That is the estate's own statement that the gap between "internally coherent" and + "externally established" is a _consumption_ gap, not a proof gap. + +=== 3.2 Satellites + +[cols="1,1,1",options="header"] +|=== +| Repo | Role | Position + +| _EchoTypes.jl_ | Executable finite-domain shadow of Echo's Tier-1/2 spine | Explicitly _not a proof_; can falsify, cannot prove; honestly scoped under R-2026-05-18 — does _not_ replay the retracted surface or the funext-qualified clauses _[DOC]_ + +| _EpistemicTypes.jl_ | The strongest _consumer story_ in the estate: per-row receipts (standpoint, warrant, projection, SHA-256 seal) and an epistemic status per taxonomy call | README-level claim; not re-verified here _[DOC]_ + +| _ResidualEvidenceTypes.jl_ | Julia companion to the residual work | Young (created 2026-09-30), 4 commits since 2026-09-01 _[API]_ + +| _secret-types_ | New home for confidentiality-labelled flow + audited declassification | Specification-stage; no checker or runtime _[DOC]_ + +|=== + +_Name-collision warning (worth keeping straight):_ `ZeroProb.jl` (measure-zero events) and +`zerostep` (a VAE dataset normaliser) are _not_ members of this family; they are adjacent +by name only. Likewise `katagoria` (historical name) resolves to `ideas-to-alphas` and is +_not_ `kategoria`; `tropical-resource-typing` resolves to `tropical-types` **[DOC: +nextgen-typing naming note 2026-09-09]**. + +=== 3.3 The consumer chain (the "near zone beyond" that matters) + +[source] +---- +katagoria → typell (kernel) → typed-wasm (target) → PanLL (environment) → affinescript / ephapax / phronesis +---- + +The estate's own fence is firm: **a conceptual arrow in the map does not establish that any +family is integrated into these projects* *[DOC: TYPE-CONNECTIONS]**. Integration that +_has_ happened is recorded in echo-types' bridge ledger: `EchoTyping.agda` in +nextgen-typing, `PhronesisEcho.agda` in phronesis, a machine-checked `EchoBridge.agda` in +nextgen-languages/kitchenspeak, and a Rust application example in invariant-path _[DOC]_. + +''' + +== 4. The cross-cutting position — what is safe to say + +=== 4.1 What the estate can claim today, without hedging + +. _Five of the seven repos have a green proof job on their current main_: + echo-types (Agda, `37152181722`), epistemic-types (Proof Safety, `37187387026`), + residual-evidence-types (Agda proofs, `36949121242`), absolute-zero (Proofs, + `37077637092`), and tropical-types' _Lean_ half (`37116071270`) — with tropical's + Isabelle half unverified by its own admission. The two without one are + choreographic-types (deliberately: no prover workflow exists yet) and occupancy-types + (whose CI is disarmed, below). +. _The honesty apparatus is real, not decorative._ Retractions actually happened and are + load-bearing (echo-types R-2026-05-18); false axioms were actually found and removed + (absolute-zero: 3 latent-unsound axioms); stale claims are actually corrected + (epistemic-types removed the free `Sync` witness; choreographic-types retired its + CITATION claim). Ledger entries separate _blocked_ from _retracted_. +. _The separations are the substance._ Each family earns its identity by + matched-negatives (Echo vs entropy/LL/resource-instance), by conditionality (Epistemic: + warrant ≠ sound proof), by no-go (Tropical: `hub_ceiling`), or by proved _non-_ + composition (absolute-zero OND-5). +. _The estate's own claims are unusually well fenced._ Where something is degenerate, + provisional, gated, or unverified, there is usually a document saying so — frequently + more conservative than the README. + +=== 4.2 What the estate must not claim today + +* _No external validation yet._ echo-types' Lane 1 is _in-repo closed, externally open_; + nextgen-typing's path to Grade B is external adoption; nothing here is submitted, + accepted, or DOI-minted. +* _No general K-CUT._ Only degenerate single-static-edge base cases exist, and the + strongest of those has been declined as a gate nominee _by its own repo_, for good reason. +* _No established cross-prover equivalence._ tropical-types says the Lean and Isabelle + developments intend to agree but equivalence is not mechanically established; each + prover checks its own development. +* _No established bridge by arrow._ The five family connections in the map are + obligations, not results (Echo→Choreographic and Epistemic→Choreographic have _no_ proof; + Echo→Residual and Epistemic→Residual cover Milestone 1 only; Tropical→Choreographic needs + a grading semantics + projection theorem). +* _No "six provers in CI" for absolute-zero._ Six provers are green _via the local gate_; + CI covers the lightweight subset, and the local gate has not been run here. + +=== 4.3 The one systemic blocker with the highest leverage + +_The CI estate is partially disarmed, and the pattern is already diagnosed._ + +* _occupancy-types_: 96/100 recent runs `startup_failure`; every gate dead; no issue filed + for this repo _[CI/API]_. +* _choreographic-types#16_ documents mechanism (a): Actions allow-list `selected` with + _0 patterns_ → any third-party action dies at startup, `jobs=0`, with a produced mutant + proof on residual-evidence-types (same head, one `uses:` step toggled, `startup_failure` + ⇄ green). Fix is an _owner-only PUT_ of the canon payload. The repo explicitly notes + this is _silent_ until the first third-party action. +* _echo-types#330_ documents mechanism (b): an actor gate refusing workflow triggering for + `arena-ai-coding-agent`, so PRs can merge with _zero_ CI signal. Its recommended + mitigation — treat `STARTUP_FAILURE` as failure for required checks — is generally + applicable. +* _echo-types#324_ / _tropical-types#59_ record allow-list/count and pinning drift. + +Practical consequence for planning: **for these repos, a green badge is not evidence until +the underlying workflow actually started.** The recon above therefore cites run ids, not +badges. The coordinated plan's §6 turns this into a measurement rule (two ratios, R1 before R2, +green-means-executed) — see `COORDINATED-PLAN-2026-10-04.adoc`. + +=== 4.4 Planned already (named, in-tree, not speculation) + +[cols="1,1",options="header"] +|=== +| Where | Named next step + +| nextgen-typing | register `occupancy-types` in the type map (#118); reconcile the choreographic "echo loss-grade" vocabulary; re-cite residual receipts (#115); sign AFFIRMATIONs (#69); build `verification/proofs` in CI (#57) + +| echo-types | Gate re-assessment at each tag; rename the WFS module; land unlaned experimental modules (#320/#321); Pillar E offline half + +| epistemic-types | Applications obligations (ℚ/rescaling/row-insertion); secret-types #32 transfer + +| residual-evidence-types | Comparisons 2.0 beyond M1 interfaces; refresh STATE; causal specialisation as its own model + +| choreographic-types | Two-event K-CUT-LOSS square under `Independent₂`; vocabulary reconciliation + +| tropical-types | ROOT → 9 theories + Isabelle job (#57); Deno removal (#58); SHA pins (#59) + +| occupancy-types | Idris spike run; stackcert run + `#print axioms`; Zephyr fixture; Actions settings; then the R2 project gate + +| absolute-zero | CI mirrors the local gate (#161); axiom tag census (#171); filesystem model → Lean (#167); the paper + +|=== + +=== 4.5 The near zone beyond (what the estate is one or two steps from) + +. _Interfaces, not just imports._ residual-evidence-types already _imports_ + `Echo.Echo` and `SoundWarrant` and proved round trips. The question it asks itself — does + composition/revision need a richer interface than `Echo.Echo`/`SoundWarrant`? — is + answerable now, and its answer would settle three of the five map obligations. +. _Turn proofs on._ Wiring the existing proofs into CI (nextgen #57, tropical #57, + occupancy's settings) converts several [DOC] claims into [CI] claims at near-zero + research cost. +. _Two K-CUT-LOSS squares._ The two-event square is specified at the level where it can + be proved today; a second, non-degenerate pattern would test whether the + single-static-edge degeneracy is essential or incidental — the cheapest experiment that + could falsify the assembly hypothesis early. +. _Cost vs state as a testable separation._ `occupancy-types` claims the HWM monoid is a + _different_ axis from tropical cost, with witnesses; the estate already has both halves + in place (tropical-types' algebra; occupancy's session IR). A small composition whose + HWM grade and cost grade cannot be identified would be the cleanest possible + cross-family result — and it is a _separation_, so it is falsifiable cheaply. +. _A consumer._ Every family's honest bottleneck is the same one the hub names: nobody + outside the estate is consuming this yet. `EpistemicTypes.jl` (per-row classifier + receipts) and occupancy's session IR (certificates over measured bounds) are the two + most consumer-shaped artefacts in the estate. + +''' + +== 5. One-table position summary + +[cols="1,1,1,1,1",options="header"] +|=== +| Repo | Established (receipt) | Nearly there | Within reach | Open research + +| _echo-types_ | Agda suite green under `--safe --without-K` (`37152181722`); 209 `.agda` files; separations; retraction-disciplined | Gates provisional; WFS-not-OFS naming; unlaned modules; `README.adoc` template drift | Rename; lane the modules; packaging/DOI | Buchholz `ψ₀(Ω_ω)`; 2 Fidelity postulates; truncation under −K + +| _epistemic-types_ | Whole library green, zero postulates, no stdlib (`37187387026`); RapidNJ Q-criterion warrants | 35% prototype; applications obligations unmet | Close named obligations; secret-types transfer | Monad/comonad structure; evidence→claim soundness + +| _residual-evidence-types_ | M1+M2 checked; 9 rejections; 546-config correspondence by `refl`; both sibling interfaces imported (`36949121242`) | STATE stale; comparisons cover M1 only | Refresh STATE; comparisons 2.0 | Causal specialisation; probability adapters + +| _choreographic-types_ | Specification + fences; docs integrity green; the _reason_ it exists is one theorem | Degenerate base case (real, sibling-side, declined as a gate nominee) | Two-event square; `Independent₂`; vocabulary fix | K-CUT-LOSS / K-CUT-WARRANT general case + +| _tropical-types_ | Lean green, 20/20, no Mathlib (`37116071270`); `hub_ceiling` no-go; parametric transport | Isabelle 9 theories, ROOT 5/9, _no CI job_; `CI context contract` red | ROOT→9; Isabelle job; Deno removal; SHA pins | Buchholz ladder; time series; probabilistic extension + +| _occupancy-types_ | Session IR 14/14 _[RAN]_; operational model; ledger with blocked ≠ retracted | Idris spike + stackcert + Zephyr fixture all UNVERIFIED; _CI 96/100 startup_failure_ | Install toolchains; run; paste `#print axioms`; fix Actions; file the issue | R2–R5 rungs; cost/state separation as a theorem + +| _absolute-zero_ | Six provers + Idris green _locally_; CI Proofs green (`37077637092`); OND-1..5,7 zero-axiom; 98→classified axioms; 3 unsound axioms fixed | OND-6 open by design; CI narrower than the local gate; roadmap drift | #161, #171, #167; roadmap refresh; artifact package | OND-6; 4 class-A Coq items; the paper + +|=== + +''' + +== 6. Method and limits of this recon + +* Read: full repo trees (shallow clones at the pins above), all top-level status documents + (README, PROOF-STATUS, AFFIRMATION, ROADMAP, ULTRAPLAN, EXPLAINME, STATE.a2ml, + pre-registration, retraction ledger), the hub's TYPE-CONNECTIONS guide and roadmap, and + the workflow files. +* Queried: GitHub Actions run history and conclusions per repo (not badges), open issues + and key issue bodies, commit dates, signatures and HEAD SHAs, toolchain availability + locally. +* Ran: the only proof-adjacent gate runnable without a prover toolchain — + `occupancy-types`' Session IR manifest (14/14). Everything else in this document that is + not marked _[RAN]_ rests on _[CI]_, _[DOC]_ or _[ISSUE]_ evidence as tagged. +* Not done: no Agda/Lean/Isabelle/Coq/Mizar/Z3 re-run; no `just check` anywhere; no + evaluation of proof _quality_ beyond what the repos' own guardrails (postulate/escape + greps, kernel certificates, axiom audits) enforce; no attempt to resolve the + occupancy-types Actions gate (owner-only API surface). +* Everything above is dated 2026-10-04 and pinned by the SHAs in §0. Move the SHAs and it + becomes a draft until re-run — which is exactly the estate's own rule for AFFIRMATIONs, + and a good rule for this document too. + diff --git a/docs/recon/ULTRA-PLAN-2026-10-04.adoc b/docs/recon/ULTRA-PLAN-2026-10-04.adoc new file mode 100644 index 0000000..8fce7d9 --- /dev/null +++ b/docs/recon/ULTRA-PLAN-2026-10-04.adoc @@ -0,0 +1,254 @@ +// SPDX-License-Identifier: CC-BY-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += Ultra-plan — the rest of the work +:toc: macro +:toclevels: 3 +:icons: font + +*Date:* 2026-10-04 · *Base commit:* `2e276c3` + this session's branch +· *Companions:* `TYPE-FAMILY-POSITION-2026-10-04.adoc` (what is true), +`COORDINATED-PLAN-2026-10-04.adoc` (workstreams W1–W5 and §6 measurement discipline) + +toc::[] + +== 0. What changed today (receipts, not intentions) + +[cols="1,3",options="header"] +|=== +| Change | Evidence + +| Gate re-run locally, still green +| `bash scripts/check.sh --runnable-only` → *exit 0*; session-IR 14/14; kill-test audit + PASS; repo-shape PASS; stages 4–5 correctly *BLOCKED* (never a silent skip). + +| *Defect found and fixed:* R1 had **no `lakefile.toml` and no `lean-toolchain`** +| `tests/run_stackcert.sh` stage 2 runs `lake build` and stage 3 `lake exe stackcert` + — neither could ever have passed. The harness reported "toolchain absent", which was + true but hid a second, permanent blocker. Added `src/stackcert/lakefile.toml` + (libs `StackcertCore`, `Parsers`; exe `stackcert` rooted at `Main`) and + `src/stackcert/lean-toolchain` (`leanprover/lean4:v4.15.0`). + +| Both blocked rungs now have a *CI execution path* +| Added `.github/workflows/proofs.yml`: `stackcert` (Lean 4.15.0 via elan, strict) and + `occ-idris` (Idris 2 v0.7.0 built over Chez Scheme; *advisory* until its first green + run). Only `actions/checkout` is used — no third-party action, so the allow-list + posture (issue #6) cannot kill these jobs at startup. + +| Markdown-gate regression I had introduced, fixed +| The three recon documents were `.md` under `docs/`, which the estate rule forbids. + `TYPE-FAMILY-POSITION` and `COORDINATED-PLAN` converted to AsciiDoc; the follower + notes moved *out of the public repo* (unsent drafts about named people) and remain a + working copy. `bash scripts/check-no-md-in-docs.sh .` → PASS. + +| Sandbox limits measured, not assumed +| Only `github.com`, `api.github.com` and `pypi.org` are reachable here; + `release-assets.githubusercontent.com` / `elan.lean-lang.org` / `deb.debian.org` are + not. So Lean/Idris cannot be fetched *here* — but GitHub runners can. + +| *Pre-existing defect found:* the action-pinning gate is already red on `main` +| `node scripts/check-action-pinning.js` → exit 1: + `.github/workflows/pages.yml:37` (`haskell-actions/setup@v2.12.1`) and + `.github/workflows/sonarqube.yml:67` (`SonarSource/sonarqube-scan-action@v8.3.0`) + resolve through neither an inline SHA nor `actions.lock`. Both my new workflows + pass the gate. Fix: pin the two refs to SHAs, or run `gh actions-lock`. + +| *Gate fixed:* the action-pinning gate now exits 0 for the first time +| `node scripts/check-action-pinning.js` → *exit 0*, "all action refs are pinned". + (Two refs were unpinned on `main` since they were introduced; see A8.) +|=== + +| The outage reproduces on this branch, in the current hour +| The push of `d5caaca` created run `37236457077` ("Push email notification", 21:31:42Z) + → `startup_failure`, `jobs: 0`. All 37 workflows report `state: active`. So the workflow + *files* are fine (they also pass the SPDX, permissions and pinning gates); jobs die at + start. Signature matches choreographic#16: `selected` with an empty pattern set, which + blocks GitHub-owned `actions/checkout` too. +|=== + +*Correction to an earlier reading:* `scripts/check-lock-sync.sh` is **not** defective. +It aborts here with `FATAL: no awk supporting 3-argument match() (need gawk)` — which is a +clear message and exit 1. Its behaviour is right; the sandbox simply lacks `gawk`. Any +runner that must execute it needs `gawk` installed. + +=== What this means for planning + +The estate's blockers split cleanly into three kinds, and only the third needs the +author: + +. *Scaffolding* (no lakefile, no lock, no lane) — fixable in-repo, today. +. *Execution* (toolchain absent) — fixable by CI, once workflows can start. +. *Authority* (Actions settings, credentials, priority) — owner-only. + +The rest of this plan is ordered along that split. Nothing below asks the author to do +work an agent or a CI job can do first. + +== 1. The rule for the rest of the work + +[quote] +____ +*No outreach until the house is closed.* The follower notes do not go out while this +repository's own gates cannot run, while a rung it claims is unverified, or while a +state file contradicts its receipts. Advice about verification, sent from a repository +that cannot verify, is the fastest way to lose the audience it is addressed to. +____ + +Corollary: W5.7/W5.8 (outreach) are *gated tasks*. They open when Tranche A is closed — +not before, and not "in parallel because they are independent". + +== 2. Owner routing + +[cols="1,2,3",options="header"] +|=== +| Route | Meaning | Typical tasks + +| *AGENT* | In-repo, no toolchain, no credentials | docs, workflows, ledgers, conversion, checks +| *CI* | Runs on GitHub runners; needs an execution path to exist | stackcert, Occ spike, session-IR lane +| *OWNER* | Needs repository settings, credentials, or a decision | Actions allow-list PUT, priority calls, repo access +| *HOST* | Needs a machine with toolchains (his laptop, devcontainer, guix shell) | local confirmation runs, Zephyr fixture +|=== + +== 3. Tranche A — close the house (this week) + +*A is closed when every item below has a receipt.* All of A is agent/owner work; none of +it is research. + +[cols="1,2,1,3",options="header"] +|=== +| ID | Task | Route | Acceptance + +| A1 | Read the Actions posture; if `selected` with a short list, PUT the canon payload + (issue #6) — see the dedicated `A1-ACTIONS-RUNBOOK.adoc` | *OWNER* | a push where + `Session IR` and `Proofs` *start* (`total_count >= 1`, conclusion ≠ `startup_failure`). + *This is the only item blocking Tranche A; everything else in A waits on it.* +| A2 | Wire the session-IR lane into CI | *AGENT*→*CI* — **done in-repo, dormant until A1** | + `.github/workflows/session-ir.yml` committed: the 14 pinned fixtures + kill-test audit + + repo-shape gates, on the runner's system `python3` (pure stdlib). Cannot *execute* until A1. +| A8 | Pin the two unpinned action refs — **done** | *AGENT* | `node scripts/check-action-pinning.js` + → *exit 0*. `haskell-actions/setup@v2.12.1` → `0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d` + and `SonarSource/sonarqube-scan-action@v8.3.0` → `d209202bc7d53ff1cc128f7f907dac145c9d6ae9`, + each with the tag kept as a trailing comment +| A9 | Ensure `gawk` is present wherever `scripts/check-lock-sync.sh` runs | *AGENT* | the script + runs instead of aborting; it already fails correctly (exit 1, clear message) +| A3 | First green `proofs.yml` run | *CI* | `R1 stackcert (Lean 4)` green; its log carries + the `#print axioms` line, pasted into `docs/EXPLAINME.adoc` C5 +| A4 | First `occ-idris` run | *CI* | advisory job green, then `continue-on-error` removed + and the CONJECTURE in EXPLAINME C4 becomes a pasted result +| A5 | Treat `STARTUP_FAILURE` as failure for required checks (estate-wide) | *OWNER* | a + required context that never starts cannot show green (echo-types#330) +| A6 | Re-run `bash scripts/check.sh` (full mode) on a host with both toolchains | *HOST* | + stages 4–5 report PASS, not BLOCKED; ledger updated +| A7 | Ground truth: Zephyr painted-stack fixture | *HOST* | measured ≤ certified recorded + per ULTRAPLAN §6, or the rung's kill criterion fires +|=== + +== 4. Tranche B — receipts and interfaces + +[cols="1,2,1,3",options="header"] +|=== +| ID | Task | Route | Acceptance + +| B1 | Refresh stale state files against their own receipts (residual-evidence, tropical, + absolute-zero) | *AGENT* | no state file contradicts a PROOF-STATUS line +| B2 | Comparisons 2.0 in residual-evidence-types: do composition and revision transport + beyond `Echo.Echo` / `SoundWarrant`? | *AGENT*→*CI* | a checked yes or no — *"a richer + interface is needed"* is a result, not a failure +| B3 | *Cost-vs-state separation*: a composition where the HWM grade and the cost grade + cannot be identified | *AGENT* | a witness pair + a no-identification statement, or a + documented collision that narrows occupancy's thesis +| B4 | Register occupancy-types in the hub's type map (hub#118) | *AGENT* | map row with + question, boundary and the cost/state vocabulary fence +| B5 | Build `verification/proofs` in CI (hub#57) | *AGENT* | XP-1 green in CI, not just on + a laptop +| B6 | Reconcile the choreographic "echo loss-grade" vocabulary with the shared glossary | *AGENT* | README/glossary agreement +|=== + +== 5. Tranche C — rungs and keystones (research, time-boxed) + +[cols="1,2,1,3",options="header"] +|=== +| ID | Task | Route | Kill / honest outcome + +| C1 | Two-event K-CUT-LOSS square under `Independent₂` | *AGENT* | if `Independent₂` needs + hypotheses that trivialise the square, record that as the finding +| C2 | A second, non-degenerate projection pattern | *AGENT* | if degeneracy is essential + rather than incidental, the assembly hypothesis narrows explicitly +| C3 | R2 static pools + affine/linear handles, T1 coherence | *HOST* | **project gate**: + no external consumer and no theorem beyond restatement ⇒ archive with a ledger entry +| C4 | Bachmann–Howard `ψ₀(Ω_ω)` | *AGENT* | remains OPEN by D-2026-06-14; the two Fidelity + postulates are the only ones in the tree and stay quarantined +| C5 | OND-6 conditional composition | *AGENT* | a too-clean positive result is the warning + sign (absolute-zero ROADMAP); treat with suspicion +|=== + +== 6. Tranche D — external standing + +[cols="1,2,1,3",options="header"] +|=== +| ID | Task | Route | Acceptance + +| D1 | Sign and re-anchor the per-repo AFFIRMATIONs at main (hub#69) | *OWNER*+*AGENT* | + dated, GPG-signed, SHA-pinned receipts +| D2 | Pillar E offline half (packaging, DOI, submission) | *OWNER* | submitted +| D3 | absolute-zero artifact-evaluation container | *AGENT* | reviewer reproduces + `ALL-PROVERS-GREEN` with one command +| D4 | Follower notes — send | *OWNER* | *gated on Tranche A closed* (§1) +| D5 | Public write-up: "what a projection/receipt/bound problem looks like, four worked + examples" | *AGENT* | citable artefact; reaches the same audience without 269 messages +|=== + +== 7. What I need from you + +Short, explicit, and each one is a decision or a credential — nothing else: + +. *The Actions posture for this repository* (A1) — the one item nothing else can + route around. Either paste the output of the command below, *or* just read the + three radio buttons at + https://github.com/hyperpolymath/occupancy-types/settings/actions (Actions + permissions) and tell me which one is selected — the UI route needs no token + and no scopes. ++ +[source,bash] +---- +gh api repos/hyperpolymath/occupancy-types/actions/permissions --jq . +# and, if it reads "selected": +gh api repos/hyperpolymath/occupancy-types/actions/permissions/selected-actions --jq . +---- ++ +It returns 403 to me (an App token, which cannot read this endpoint at any scope), so +this cannot be read from inside the repository. Note the `repos/` prefix is required — +without it the call returns *404 Not Found*, which is a bad route, not a permissions +answer. `A1-ACTIONS-RUNBOOK.adoc` maps all three possible outputs to their fix and gives +the positive control (count jobs, do not read badges). +. *Scope of my hands* (all tranches). This session can only push + `arena/01a1087c-occupancy-types` on this repository. For the other repos I can produce + ready-to-apply patches, or issue bodies, or nothing — your call which. +. *Priority* (next session). Which tranche leads: A (close the house), B (receipts and + interfaces), C (rungs and keystones), or D (standing)? +. *Toolchain route* (A3/A4/A6). CI (needs A1 first), your machine + (`bash tests/run_stackcert.sh`, then paste the `#print axioms` line), or the + devcontainer in this repo — all three are fine; they just need picking. + +Answers to these unblock every row above; nothing else in the plan is waiting on you. + +== 8. Stop rules + +* *A rung that cannot run is BLOCKED, never OK.* `scripts/check.sh` already enforces this + (fixture request, exit 2 semantics); do not "fix" a blocked stage by softening it. +* *Kill criteria fire on schedule.* R2's project gate (occupancy ULTRAPLAN §1.3/§4) is a + real stop, not a milestone: no external consumer + no theorem beyond restatement ⇒ + archive with a ledger entry. +* *No capability claim without a separation* (echo-types' gate discipline). +* *Outreach waits.* See §1. + +== 9. Decision-log additions + +[cols="2,2,3",options="header"] +|=== +| Decision | Choice | Why / revisit + +| Where toolchain-dependent rungs run | *CI*, not the authoring sandbox | Release-asset hosts are unreachable from the sandbox (measured 2026-10-04); runners can fetch them. Revisit if a local toolchain appears. +| Workflow style for new jobs | `actions/checkout` only; toolchains installed in `run:` steps | The allow-list posture can kill any third-party action at startup with `jobs=0` (issue #6). Revisit when the posture is fixed. +| Recon documents | AsciiDoc under `docs/`; follower drafts outside the public repo | Estate markdown rule; unsent drafts about named people are not publishable material. +| Outreach gating | Tranche A closed first | Credibility: advice about verification from a repo that cannot verify is self-defeating. +| stackcert build definition | `lakefile.toml` + pinned `lean-toolchain` committed | The harness's `lake build` / `lake exe` steps require them; without them the rung was permanently unpassable. +|=== diff --git a/docs/retraction-ledger.adoc b/docs/retraction-ledger.adoc index 99ad764..7efb882 100644 --- a/docs/retraction-ledger.adoc +++ b/docs/retraction-ledger.adoc @@ -31,16 +31,39 @@ requested). Blocked ≠ retracted: no claim has been withdrawn. | 2026-09-27 | Idris 2 spike unverified (no `idris2` on PATH in the work environment) | `idris2 --check Occ.idr` from `src/occ/`; `./check-rejections.sh` for the - four expected-rejection controls (see `src/occ/README.adoc`) + four expected-rejection controls (see `src/occ/README.adoc`). *CI path added + 2026-10-04:* `occ-idris` job in `.github/workflows/proofs.yml` + (Idris 2 v0.7.0 over Chez Scheme, advisory until its first green run). | R0-B Piece 2 | 2026-09-27 | stackcert core unverified (no `lean`/`lake` on PATH) | `lake build && lake exe stackcert …` from `src/stackcert/`; `lean StackcertCore.lean` then `#print axioms cert_sound` (see - `src/stackcert/README.adoc`) + `src/stackcert/README.adoc`). *CI path added 2026-10-04:* `stackcert` job in + `.github/workflows/proofs.yml` (Lean 4.15.0 via elan). | R1 Piece 3 +| 2026-10-04 +| *Two blockers were stacked behind one message*: R1's `lake build` / + `lake exe stackcert` steps had **no `lakefile.toml` and no `lean-toolchain` + anywhere in the repository**, so the rung could not have passed even with a + Lean install. The harness's "toolchain absent" report (exit 2) was accurate + but incomplete. +| Fixed in-repo: added `src/stackcert/lakefile.toml` (libs `StackcertCore`, + `Parsers`; exe `stackcert` rooted at `Main`) and + `src/stackcert/lean-toolchain` (`leanprover/lean4:v4.15.0`). Remaining + blocker is the toolchain only, resolved by the `proofs.yml` job. +| R1 Piece 3 + +| 2026-10-04 +| Session IR — the estate's only fully-green rung (14/14 locally) — had *no CI + lane at all*, so its most credible result carried no clickable receipt. +| Added `.github/workflows/session-ir.yml`: checker on the 14 pinned fixtures + + kill-test audit + repo-shape gates, on any runner's system `python3` (the + module is pure standard library). +| R0-B Phase 1 + | 2026-09-27 | Zephyr ground-truth fixture absent (no `west`/QEMU/Zephyr SDK; fixture request issued — see `src/stackcert/README.adoc` §Fixture request) diff --git a/src/session_ir/__pycache__/__init__.cpython-311.pyc b/src/session_ir/__pycache__/__init__.cpython-311.pyc deleted file mode 100644 index d699973..0000000 Binary files a/src/session_ir/__pycache__/__init__.cpython-311.pyc and /dev/null differ diff --git a/src/session_ir/__pycache__/__main__.cpython-311.pyc b/src/session_ir/__pycache__/__main__.cpython-311.pyc deleted file mode 100644 index af10570..0000000 Binary files a/src/session_ir/__pycache__/__main__.cpython-311.pyc and /dev/null differ diff --git a/src/session_ir/__pycache__/checker.cpython-311.pyc b/src/session_ir/__pycache__/checker.cpython-311.pyc deleted file mode 100644 index 324d31b..0000000 Binary files a/src/session_ir/__pycache__/checker.cpython-311.pyc and /dev/null differ diff --git a/src/session_ir/__pycache__/cli.cpython-311.pyc b/src/session_ir/__pycache__/cli.cpython-311.pyc deleted file mode 100644 index 243eca5..0000000 Binary files a/src/session_ir/__pycache__/cli.cpython-311.pyc and /dev/null differ diff --git a/src/session_ir/__pycache__/machine.cpython-311.pyc b/src/session_ir/__pycache__/machine.cpython-311.pyc deleted file mode 100644 index 355d5d8..0000000 Binary files a/src/session_ir/__pycache__/machine.cpython-311.pyc and /dev/null differ diff --git a/src/session_ir/__pycache__/parser.cpython-311.pyc b/src/session_ir/__pycache__/parser.cpython-311.pyc deleted file mode 100644 index 955afca..0000000 Binary files a/src/session_ir/__pycache__/parser.cpython-311.pyc and /dev/null differ diff --git a/src/session_ir/__pycache__/syntax.cpython-311.pyc b/src/session_ir/__pycache__/syntax.cpython-311.pyc deleted file mode 100644 index 373b592..0000000 Binary files a/src/session_ir/__pycache__/syntax.cpython-311.pyc and /dev/null differ diff --git a/src/stackcert/lakefile.toml b/src/stackcert/lakefile.toml new file mode 100644 index 0000000..e916c17 --- /dev/null +++ b/src/stackcert/lakefile.toml @@ -0,0 +1,30 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Lake build definition for the stackcert R1 artefacts. +# +# WHY THIS FILE EXISTS: ULTRAPLAN R1 declares stackcert's verification command +# as `bash tests/run_stackcert.sh`, whose stage 2 runs `lake build` and stage 3 +# runs `lake exe stackcert`. Neither could have succeeded without a lake +# definition, so the harness's "toolchain absent" report was two blockers +# stacked: missing build scaffolding *and* an absent toolchain. This file +# supplies the first. The second is a toolchain/CI concern, not a proof claim, +# and is handled by .github/workflows/proofs.yml. +# +# The verified/UNVERIFIED split is unchanged by this file (see README.adoc): +# StackcertCore — the verified core (zero imports, no Mathlib, no holes) +# Parsers, Main — the I/O and CLI layer, explicitly outside cert_sound + +name = "stackcert" +version = "0.1.0" +defaultTargets = ["stackcert"] + +[[lean_lib]] +name = "StackcertCore" + +[[lean_lib]] +name = "Parsers" + +[[lean_exe]] +name = "stackcert" +root = "Main" diff --git a/src/stackcert/lean-toolchain b/src/stackcert/lean-toolchain new file mode 100644 index 0000000..d0eb99f --- /dev/null +++ b/src/stackcert/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.15.0