Phase 0: make the status surfaces true (trope-checker)

.github/workflows/proofs.yml

@@ -53,16 +53,23 @@
         run: |
           set -euo pipefail
           fail=0
-          for f in verification/proofs/lean4/grade-boundary/GradeBoundary.lean \
-                   verification/proofs/lean4/grade-factorisation/GradeFactorisation.lean; do
+          # Every Lean source, not only the two v0.1 files: the ratified-carrier
+          # results (GradeRatified, L4Monotonicity, TierTwoComplete, EffectAtoms,
+          # GradeFactorisationR) are what the current spec cites.
+          for f in $(git ls-files 'verification/proofs/lean4/*.lean' 'verification/proofs/lean4/*/*.lean'); do
             if [ ! -f "$f" ]; then
               echo "::error::gated file is missing: $f"; fail=1; continue
             fi
             echo "--- gating $f ---"
-            if grep -nE '(:=|by|;|<;>|=>|\|)[[:space:]]*(sorry|admit)\b|\bnative_decide\b' "$f"; then
+            # Comment-aware and token-based: strip -- and /- -/ comments first
+            # (tests/lib/strip-proof-comments.awk; line numbers preserved), then match
+            # the bare tokens, so `:= by` with an indented `sorry` on the NEXT line is
+            # caught while the honest "sorry-free" prose in comments is not.
+            stripped=$(awk -f tests/lib/strip-proof-comments.awk "$f")
+            if grep -nE '(^|[^[:alnum:]_.])(sorry|admit)([^[:alnum:]_]|$)|\bnative_decide\b' <<<"$stripped"; then
               echo "::error file=$f::forbidden Lean tactic (sorry/admit/native_decide)"; fail=1
             fi
-            if grep -nE '^[[:space:]]*axiom\b' "$f"; then
+            if grep -nE '^[[:space:]]*axiom\b' <<<"$stripped"; then
               echo "::error file=$f::user axiom declared"; fail=1
             fi
           done
@@ -73,41 +80,49 @@
   # so this is a real check of postulate-freedom and not a word-grep (a grep would
   # false-positive on the honest "postulate-free" prose in the comments).
   #
-  # NOTE ON THE VERSION PIN: theorem-b.agda-lib is developed against Agda 2.8.0
-  # (ADR 0003). The runner's packaged Agda is older. The version is printed, not
-  # asserted, because asserting a version the runner cannot supply produces a
-  # permanently-red gate rather than a signal — and the substantive guarantee here
-  # comes from --safe --without-K, which holds across versions. Verified locally
-  # under 2.6.4.3: All.agda and Smoke.agda both typecheck, exit 0.
+  # TOOLCHAIN: pinned release artefacts, not the runner's apt. ubuntu-latest is
+  # 24.04, whose agda-stdlib is 1.7.3; Theorem B imports Data.Product.Base, which
+  # exists from stdlib 2.0, so `apt-get install agda agda-stdlib` there fails at
+  # scope checking (exit 42) — reproduced 2026-10-13. The job now fetches the
+  # Agda 2.7.0.1 release binary and the stdlib v2.0 source archive, verifies
+  # both SHA-256 sums, and registers the stdlib under the name the .agda-lib
+  # depends on. Verified 2026-10-13 with exactly these artefacts: All.agda and
+  # Smoke.agda typecheck under --safe --without-K, exit 0 (~100 s). A checksum
+  # mismatch fails loudly rather than silently testing a different stdlib.
   agda-theorem-b:
     name: "Agda Theorem B (--safe --without-K)"
     runs-on: ubuntu-latest
     timeout-minutes: 30
     steps:
       - uses: actions/checkout@v7.0.1
-      - name: Install Agda and register the standard library
+      - name: Install Agda 2.7.0.1 and agda-stdlib 2.0 (pinned, checksummed)
         shell: bash
+        env:
+          AGDA_URL: https://github.com/agda/agda/releases/download/v2.7.0.1/Agda-v2.7.0.1-linux.tar.xz
+          AGDA_SHA256: 975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a
+          STDLIB_URL: https://github.com/agda/agda-stdlib/archive/refs/tags/v2.0.tar.gz
+          STDLIB_SHA256: 14eecb83d62495f701e1eb03ffba59a2f767491f728a8ab8c8bb9243331399d8
         run: |
           set -euo pipefail
-          sudo apt-get update -qq
-          sudo apt-get install -y -qq --no-install-recommends agda agda-stdlib
-          echo "agda --version -> $(agda --version | head -1)"
-          echo "ratified pin (ADR 0003) is Agda 2.8.0; --safe --without-K is the substantive check"
-
-          # Installing the package is not enough: Agda only sees a library that is
-          # listed in its `libraries` file, and a fresh runner has none. WHICH path
-          # that file lives at is VERSION-DEPENDENT (~/.agda vs ~/.config/agda), so
-          # point AGDA_DIR at a directory we control rather than guessing, and
-          # resolve the .agda-lib from the package rather than hardcoding it.
-          lib="$(dpkg -L agda-stdlib | grep -m1 'standard-library\.agda-lib$' || true)"
-          if [ -z "$lib" ]; then
-            echo "::error::agda-stdlib is installed but standard-library.agda-lib was not found"
-            exit 1
-          fi
-          mkdir -p "${RUNNER_TEMP}/agda"
-          echo "$lib" > "${RUNNER_TEMP}/agda/libraries"
-          echo "AGDA_DIR=${RUNNER_TEMP}/agda" >> "$GITHUB_ENV"
-          echo "registered standard-library at: $lib"
+          mkdir -p "${RUNNER_TEMP}/agda-toolchain" && cd "${RUNNER_TEMP}/agda-toolchain"
+          curl -sSL -o agda.tar.xz "$AGDA_URL"
+          echo "$AGDA_SHA256  agda.tar.xz" | sha256sum -c -
+          curl -sSL -o stdlib.tar.gz "$STDLIB_URL"
+          echo "$STDLIB_SHA256  stdlib.tar.gz" | sha256sum -c -
+          tar -xJf agda.tar.xz && tar -xzf stdlib.tar.gz
+          # theorem-b.agda-lib depends on `standard-library`; the 2.0 archive names
+          # itself `standard-library-2.0`, so register a lib file under the depended-on name.
+          printf 'name: standard-library\ninclude: src\nflags:\n  --warning=noUnsupportedIndexedMatch\n' \
+            > agda-stdlib-2.0/standard-library.agda-lib
+          mkdir -p "${RUNNER_TEMP}/agda-dir"
+          echo "$PWD/agda-stdlib-2.0/standard-library.agda-lib" > "${RUNNER_TEMP}/agda-dir/libraries"
+          {
+            echo "AGDA_DIR=${RUNNER_TEMP}/agda-dir"
+            echo "Agda_datadir=$PWD/Agda-v2.7.0.1/data"
+            echo "LC_ALL=C.UTF-8"
+          } >> "$GITHUB_ENV"
+          echo "$PWD/Agda-v2.7.0.1/bin" >> "$GITHUB_PATH"
+          "$PWD/Agda-v2.7.0.1/bin/agda" --version
       - name: Typecheck Theorem B
         shell: bash
         working-directory: verification/proofs/agda/theorem-b

AFFIRMATION.adoc

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = AFFIRMATION — trope-checker
-:revdate: 2026-06-24
+:revdate: 2026-10-27
 
 A dated, ground-truthed honesty snapshot (the README/EXPLAINME/AFFIRMATION trio).
 This is the brief's "STATUS" deliverable: what is proved, what is stubbed-and-named,
@@ -78,3 +78,64 @@ Documentation gaps OPEN-B/B′ (`Falsified`/`Misbound` absent from v0.1 §3.1/§
 proved-vs-missing picture: `verification/proofs/INTEGRATION-REPORT.adoc`.
 
 — Authored by the build agent under owner direction; signed in git history.
+
+== As of 2026-10-27 — Phase 0 re-run on the ratified world
+
+*Anchor.* Branch `claude/new-session-snuoro` at `444e4cf` (`main` 216f23b + the v0.2
+consolidation + the `proofs.yml` pin), 2026-10-27T07:56Z, in an Ubuntu 24.04 cloud
+container. Toolchain: Agda 2.7.0.1 + agda-stdlib 2.0 (tag `v2.0`, commit `2b8fff1`);
+Idris2 0.8.0 (built from tag `v0.8.0` on Chez Scheme 9.5.8); rustc 1.97.0; just 1.40.0.
+
+*Ground truth (commands run here):*
+
+* `idris2 --typecheck verification/proofs/idris2/trope.ipkg` → exit 0; 8 modules, all
+  `%default total`; no `believe_me` / `assert_total` / `postulate` in
+  `verification/proofs/idris2` or `src/idris2`.
+* `just trope-build && bash tests/conformance/run.sh` → the reference `tropecheck`
+  builds; *13* verdict cases pass with the expected witness edge and coordinate; *9*
+  schema-invalid documents are rejected at the named slot; "conformance: all pass".
+* `just trope-rust` → `tropecheck-rs` builds; the same 13 + 9 pass — the Rust fast core
+  and the Idris2 reference agree over the whole corpus.
+* `just build-agda` → `agda --safe --without-K All.agda` and `Smoke.agda` exit 0
+  (77 s and 5 s cold; 12 s together with cached interfaces).
+* `just build-lean` → *NOT RUN here*: `lake` is not installed and the Lean toolchain
+  and Mathlib cache hosts were unreachable from this container. The
+  `lean-source-honesty` regexes of `proofs.yml` were run by hand over all 8 tracked
+  `.lean` files: no `sorry` / `admit` / `native_decide`, no user `axiom`. On this
+  branch the `proofs.yml` `lean-build` job (run 40472568287, 2026-10-27T08:18Z) built
+  both packages — `lake build` "Build completed successfully", one axiom line per
+  theorem — and then failed in lean-action's optional `nanoda` step (its lean4export
+  does not compile under the v4.16.0 toolchain), exactly as on `main`; that step, not
+  the build, is why the job is red.
+
+*Proved* (machine-checked; names in `docs/status/PROOF-STATUS.adoc`): L1–L6 on the
+ratified carrier, L4 in full (`fateL4MonoR/L`, `bondComposeMono`, `mergeComposeMono`);
+the decidable retention preorder; the Veridicality Derivation and Honest Generation;
+C1–C3 (`GradeR.conical`, `gradeR_leftCancel_iff`, `TierTwoComplete`,
+`fate-tier-meet-hom-fails`); O1-carrier (`atom_factorization`, stated on the v0.1 `Grade` — finding 4); the sighted tropical
+factorisation (`piR_sighted`); Theorem B Targets 1, 2, 4 and the β/let case of 3
+(`cut-preserves-grade`, `β-app`, `β-let`); grade soundness for exact lowering,
+T-Sub and verdict soundness (`soundFromExact`, `subSound`, `verdictSound`). *Open*
+(`spec/calculus.adoc §10`): CO-1 mechanisation (the `fix` case; designed, not
+mechanised), O1-coord, O2, O3, O5 mechanisation, O6.
+
+*Four findings.* (1) Ubuntu 24.04's apt pair (Agda 2.6.3, agda-stdlib 1.7.3) cannot
+typecheck Theorem B: `agda --safe --without-K All.agda` exits 42, `Data.Product.Base`
+not found — stdlib ≥ 2.0 is required, which is why `proofs.yml` now pins Agda 2.7.0.1
++ stdlib 2.0 by checksum (reproduced here, 58 s). (2) The 2026-06-22 entry's "10/10"
+and "8 schema-invalid" were stale: the corpus is 13 + 9. Also observed: `just
+proof-check-all` is red for reasons that predate this pass (per-file `idris2 --check`
+and `agda --safe` from the repo root cannot resolve module names; the ABI/Types Idris2
+mint templates do not typecheck) — recorded as an issue, not fixed here; the gates
+that mean something are `just check`, `just build-agda`, `just trope-rust` and
+`verify-all`. (3) The CI axiom audit shows `Trope.nine_families` (`EffectAtoms.lean`),
+`FateA.Q_add_left_cancel` and `FateA.atten_cancel_on_normalForms` (`GradeRatified.lean`)
+depend on `Classical.choice` as well as `propext`/`Quot.sound`; the "`propext`/`Quot.sound`
+only" wording in spec §9.3, PROOF-STATUS and the proofs README overclaimed and now reads
+"no `sorryAx`, no user axiom". `GradeBoundary.lean`'s own footer had said so all along. (4) `EffectAtoms.lean` imports
+`GradeBoundary`, so the atom factorisation cited for O1-carrier is a theorem about the
+v0.1 `Grade`; no `GradeR` restatement exists. The factorisation is componentwise and
+should transfer, but that is an argument, not a proof — recorded in PROOF-STATUS (Open)
+and left for the owner where `spec/calculus.adoc §6/§10` cite it as ratified-carrier.
+
+— Run by the Phase 0 agent; the owner signs on landing.

CHANGELOG.adoc

@@ -10,6 +10,26 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 ==== Changed
 
+* *Spec v0.2 consolidation (2026-10-13).* `+docs(spec)+`: consolidate the calculus
+at v0.2 — nine effects with the atom table, ratified carrier inline (A1–A3), L6
+commutativity and the cancellation structure as laws, the tropical factorisation
+recorded as sighted, §7 restated as greatest post-fixed point with T-Fix-Decl, O5
+defined and O6 (ceiling verdict) opened, prover roles per ADR 0005.
+`+spec/calculus-v0.2-draft.adoc+` folded in and removed; README and
+INTEGRATION-REPORT aligned.
+* *Phase 0 — status surfaces made true (2026-10-27).*
+`+docs/status/PROOF-STATUS.adoc+` rewritten to the ratified carrier (one proved
+table citing only existing lemma names; open list = spec §10; history collapsed);
+`+docs/status/ROADMAP.adoc+` ships v0.2; `+AFFIRMATION.adoc+` gains a 2026-10-27
+entry from re-run checks (13 + 9 conformance on both checkers, Agda green, Lean
+NOT RUN in that session); the `+fix+` footer of
+`+verification/proofs/agda/theorem-b/TB/Reduction.agda+` names the designed CO-1
+model and records O4 as resolved.
+* *`+proofs.yml+`* pins Agda 2.7.0.1 + agda-stdlib 2.0 by SHA-256 (the runner's apt
+pair fails at `+Data.Product.Base+`); the Lean honesty gate and `+verify-all+` cover
+every tracked `+.lean+` file and are comment-aware and token-based (a `+sorry+` on the
+line after `+:= by+` is caught; "sorry-free" prose in comments is not).
+
 * *IR 0.2 — A3 `+Attenuated(0)+` ingest normalization (R-2026-07-07-03,
 ADR 0004, #28).* Both checkers (Idris2 reference, Rust fast-core)
 rewrite `+Attenuated(0)+` to `+Present+` at the IR ingest boundary,
@@ -25,6 +45,12 @@ fault. New conformance fixtures prove `+Atten(0)+` ≡ `+Present+`
 
 ==== Added
 
+* *ADR 0005* (`+docs/decisions/0005-v0.2-consolidation-o5-and-prover-roles.adoc+`,
+Proposed): spec v0.2 normative; O5 adopted from the workbench proposal of
+2026-07-17; O6 opened; prover roles (Agda kernel, Idris2 reference, Lean
+provenance, Rust fast core); templates removed; the carrier-as-parameter question
+(D6) recorded, not decided.
+
 * *Grade-algebra ground truth (Lean 4 + Mathlib).*
 `+verification/proofs/lean4/grade-boundary/+`: a sorry-free, axiom-clean
 (`+propext+`/`+Quot.sound+` only) formalisation of the honest/deceptive
@@ -75,3 +101,11 @@ prose.
 central open problem.
 * `+.gitignore+` now excludes `+.lake/+` (Lean build artifacts +
 vendored Mathlib clones).
+
+==== Removed
+
+* The never-instantiated prover templates `+verification/proofs/coq/TypeSafety.v+`,
+`+verification/proofs/tlaplus/StateMachine.tla+` and
+`+verification/proofs/agda/Properties.agda+`, with their tree and recipe references
+(`+proof-check-all+` no longer runs the Coq recipe; `+proof-status+` reports three
+provers).

Justfile

@@ -140,15 +140,9 @@ test-smoke:
     @echo "Smoke test..."
     # TODO: Add basic sanity checks
 
-# Run end-to-end tests (full pipeline: build → run → verify)
+# Run end-to-end conformance tests (build first with `just trope-build`).
 e2e:
-    @echo "Running E2E tests..."
-    # TODO: Replace with your E2E test command. Examples:
-    #   bash tests/e2e.sh                    # Shell-based E2E
-    #   npx playwright test                  # Browser E2E
-    #   mix test test/integration/e2e_test.exs  # Elixir E2E
-    #   cargo test --test end_to_end         # Rust E2E
-    @echo "E2E tests passed!"
+    bash tests/e2e.sh
 
 # Run aspect tests (cross-cutting concern validation)
 aspect:

README.adoc

@@ -45,8 +45,10 @@ an existing language could emit the same IR and be checked by the same checker.
   (calculus O2), discharged per front-end, not here.
 . *Veridicality is declared and propagated, not checked.* Detecting that a value
   claimed faithful is in fact false needs a ground-truth oracle the checker does
-  not have (calculus O5). The checker guarantees only that deception does not
-  compose away and that deceptive grades fail every honest floor.
+  not have — and cannot have: veridicality is undecidable relative to the IR
+  (calculus §10-O5, Remark O5-a). The checker guarantees only that deception does
+  not compose away and that deceptive grades fail every honest floor; a deployment
+  MAY bind an external oracle under the O5-1..3 conditions.
 
 == Deploy variant: prevent (R-2026-06-22)
 
@@ -62,8 +64,7 @@ rejects them at validation, naming the offending coordinate. The alternative
 [cols="1,3",options="header"]
 |===
 | Path | What lives there
-| `spec/calculus.adoc`        | The normative calculus (source of truth, `:revnumber: 0.1`).
-| `spec/calculus-v0.2-draft.adoc` | v0.2 *draft addendum*: the proved grade-algebra obligations `R-2026-06-23-01..04` (non-commutative product monoid; conicality; three-tier cancellation boundary; `Dropped`/`Total` honest). Does not edit v0.1.
+| `spec/calculus.adoc`        | The normative calculus (source of truth, `:revnumber: 0.2` — consolidated 2026-10-13: ratified carrier, nine effects, O5 defined, O6 opened).
 | `spec/trope-ir.adoc`        | The normative IR spec: nodes, edges, grade algebra, verdict.
 | `schemas/trope-ir.schema.json` | The Trope IR JSON Schema — the trust boundary (prevent profile).
 | `src/idris2/`               | The executable checker (Idris2): JSON parser + IR decoder + checker, reusing the verified core; plus `Main` → the `tropecheck` binary.
@@ -142,15 +143,23 @@ https://github.com/hyperpolymath/trope-checker/tree/8f58d2409227b065fed01a898c02
 
 == Status
 
-Alpha. The schema, executable checker, and conformance suite are green; the
-verified core typechecks with no axioms behind its claimed lemmas. The grade-algebra
-*honest/deceptive cancellation boundary* is now proved in Lean (sorry-free,
-axiom-clean) and its metatheory developed in Agda (Theorem B). Grade soundness (the
-full `g ⊑ ρ` theorem) and the *operational model for `fix`/routing* (the central open
-problem, CO-1, gated by O4) remain the named open problems in
-`docs/status/PROOF-STATUS.adoc`; see `verification/proofs/INTEGRATION-REPORT.adoc` for
-the full proved-vs-missing picture. A Rust fast-core is drafted in `src/rust/`
-(dep-free, validated against the Idris2 reference via the conformance corpus).
+Alpha. The IR schema, the executable checker and the conformance suite are green,
+and the verified developments carry no `sorryAx` and no user axiom behind their
+claimed lemmas (the Lean results rest on the standard library's `propext`/`Quot.sound`,
+and `Classical.choice` in three theorems). On the ratified carrier (ADR 0004, R-2026-07-07) the grade algebra is a commutative
+monoid with the three deceptive bottoms as two-sided zeros; L1–L6, conicality, the
+cancellation boundary (left-cancellative iff ε), the Honest Generation and
+Veridicality theorems, the atom factorisation (O1's carrier half — stated on the v0.1 `Grade`,
+not yet restated on `GradeR`) and a veridicality-sighted tropical factorisation are proved across Agda, Idris2 and
+Lean; Theorem B gives grade-exact substitution and β/let subject reduction. The
+named open problems are *CO-1* — the operational model for `fix` is designed
+(`spec/notes/2026-07-07-co1-operational-model.adoc`) and awaits mechanisation,
+which is what stands between the exact-lowering soundness already proved and
+full grade soundness — plus O2 (per producer), O3, O5's mechanisation, O6 and
+O1-coord, all listed in `spec/calculus.adoc §10` with their status. Ground truth:
+`AFFIRMATION.adoc`; the proved-vs-open table: `docs/status/PROOF-STATUS.adoc`. The
+Rust fast core in `src/rust/` (dependency-free) agrees with the Idris2 reference
+over the conformance corpus.
 
 == Licence