From 62c2134d9cf38e4a59178003bb946b23fa58ad59 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:14:21 +0000 Subject: [PATCH 1/3] =?UTF-8?q?docs(status):=20STATE-OF-THE-STACK=20?= =?UTF-8?q?=E2=80=94=20one=20row=20per=20repo,=20ground-truthed?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong: no single surface said what each of the five repos is, what exists, which obligations it owns, and which command verifies the row; the status words were scattered across five READMEs of different ages. What changed: docs/status/STATE-OF-THE-STACK.adoc (CC-BY-SA-4.0) with one table (repo · status · what exists · obligations it owns · proof/test citations · ground-truth command · last verified), the five-repo map paragraph, and a Known gaps list (A2ML still in haec/hermeneia/vocarium; vocarium's checker pin 69221ad6; this repo's stuck Pages run and cancelled Secret scan; Lean not run in the Phase 0 session). Linked from README "Where to go next". What I ran (2026-10-27, the dates in the table): bash tests/check-vocabulary.sh (nine effects consistent); the trope-checker, haec and hermeneia commands cited in each row were run in the same session and are recorded in those repos' AFFIRMATION entries of this date. What I did not run: vocarium's zig build test and gate (no Zig executable permitted in the session) — the row says so and points at CI. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- README.adoc | 2 + docs/status/STATE-OF-THE-STACK.adoc | 96 +++++++++++++++++++++++++++++ 2 files changed, 98 insertions(+) create mode 100644 docs/status/STATE-OF-THE-STACK.adoc diff --git a/README.adoc b/README.adoc index f3989c2..267e0f2 100644 --- a/README.adoc +++ b/README.adoc @@ -200,6 +200,8 @@ https://github.com/hyperpolymath/trope-particularity-workbench/tree/b18eb67dcf10 * https://hyperpolymath.github.io/trope-particularity-workbench/[the trainer] (source: `assets/particularity-trainer.html`) — drill until you can name the move from the test. * `docs/background.adoc` — why the vocabulary is compatible with the metaphysics it borrows from. +* `docs/status/STATE-OF-THE-STACK.adoc` — one table, one row per repo: status, what exists, + the obligations it owns, proof/test citations, and the ground-truth command that verifies it. * `docs/status/RESEARCH-PROGRAMME.adoc` — the prioritised, trope-stack-wide programme of work (what is worth doing next in the field, and who might fund it). * `docs/theory/computing/trope-theory-and-neural-representation.adoc` — a position paper diff --git a/docs/status/STATE-OF-THE-STACK.adoc b/docs/status/STATE-OF-THE-STACK.adoc new file mode 100644 index 0000000..ed0c8c3 --- /dev/null +++ b/docs/status/STATE-OF-THE-STACK.adoc @@ -0,0 +1,96 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += State of the trope stack — 2026-10-27 +:toc: macro + +One table, one row per repository: what each one is, what exists, which open +obligations it owns, where its proofs and tests are, and the command that +verifies the row. "Last verified" is the date the command in that row was run +and the result observed; a row that could not be run says so and names the CI +run that attests it instead. + +toc::[] + +== The table + +[cols="1,1,3,2,2,2,1",options="header"] +|=== +| Repo | Status | What exists | Obligations it owns | Proof / test citations | Ground-truth command | Last verified + +| trope-particularity-workbench +| specification +| The nine effects (`vocabulary/`), the particularity trainer, the pipeline map, +the research programme, the O5 proposal (adopted upstream into +`trope-checker/spec/calculus.adoc §10`, ADR 0005 pending ratification). +| O1-coord metaphysical adequacy (WP-5). +| `tests/check-vocabulary.sh` (nine effects consistent across vocabulary, trainer, +map, README). +| `bash tests/check-vocabulary.sh` +| 2026-10-27 + +| trope-checker +| alpha +| Spec v0.2 (one normative document on the ratified carrier), Trope IR 0.2 + +JSON schema, Idris2 reference checker + Rust fast core, Agda kernel (Theorem B), +Lean provenance developments, conformance suite. +| CO-1 mechanisation; O3; O5 and O6 mechanisation; O2 for its own fixtures only. +| `docs/status/PROOF-STATUS.adoc` (proved table / open list), `AFFIRMATION.adoc` +2026-10-27 entry: 13 verdict + 9 schema-invalid conformance cases pass on both +checkers; `All.agda`/`Smoke.agda` under `--safe --without-K` exit 0. +| `just check`, `just build-agda`, `just trope-rust`; `just build-lean` (needs lake ++ Mathlib; CI `proofs.yml`) +| 2026-10-27 (Lean: CI) + +| haec +| design +| Grammar (`design/grammar.ebnf`), elaboration table with per-construct O2 +obligations, three example program/IR pairs that round-trip through the checker. +| O2 lowering correctness for its constructs. +| `AFFIRMATION.adoc` 2026-10-27: 3 well-formed, schema matches canonical, 3 +round-trips to the stated verdicts. +| `TROPECHECK_BIN= bash tests/check-examples.sh` +| 2026-10-27 + +| hermeneia +| implementation (M1) +| `invoke` end to end against the checker; the other six vokes parse and are +refused as unimplemented; `show loss` refused (needs the checker's loss vector); +stub store. +| None of the calculus's; O2 as a producer, once it emits IR from a real store. +| `AFFIRMATION.adoc` 2026-10-27: `cargo test --workspace` 39 pass; e2e slice 7 +pass (`src/hermeneia-cli/tests/slice.rs`). +| `cargo test --workspace`; `HERMENEIA_TROPECHECK= cargo test -p +hermeneia-cli --features e2e --test slice` +| 2026-10-27 + +| vocarium +| M1 invoke slice +| `voc` store engine (pure Zig, ADR-0002 wire-not-link): JSONL replay, warrant +door, `voc invoke` emitting Trope IR 0.2; the use-relativity gate. M2 +StoreProvider adapter pending. +| None of the calculus's; O2 as a producer; O5-2 attestations are its warrants. +| `AFFIRMATION.adoc` 2026-10-27 (NOT RUN in that session; CI `vocarium-ci.yml` +runs `zig build test` and the gate on every push). +| `zig build test`; `TROPECHECK_BIN= bash tests/e2e/invoke_slice.sh` +| CI (see PR) +|=== + +== The five-repo map + +Vocabulary track: trope-particularity-workbench → haec → trope-checker (verdict). +Store/query track: haec → vocarium → hermeneia → trope-checker (verdict). +trope-checker depends on nothing (HC-1); the workbench depends on nothing; +vocarium and hermeneia meet at the M2 StoreProvider adapter (vocarium ADR-0002: +wire, do not link). + +== Known gaps + +* A2ML machine-readable files are still present in haec, hermeneia and vocarium + (retired in this repo and in trope-checker); retirement is written up as an + issue per repo, not done in Phase 0. +* vocarium's gate pins checker commit `69221ad6`, which predates the spec v0.2 + consolidation; the pin is to be bumped once Phase 0 lands upstream (issue). +* This repo's GitHub Pages (trainer) run has been queued since 2026-10-06 and a + Secret scan run was cancelled; both are repository settings, owner-only. +* `trope-checker`'s `just build-lean` was not run in the Phase 0 session (no + Lean toolchain reachable there); its `proofs.yml` CI job is the attestation. From d2f41a7669d0aaf1bf11987a32c670cd68dd305f Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:14:21 +0000 Subject: [PATCH 2/3] docs(programme): three provers, WP-2 delivered, O6 on the spine, caveat retired MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit What was wrong: RESEARCH-PROGRAMME described a "four-prover verification stack"; WP-2 (define O5) was still open although O5 is defined in the checker's spec §10 since 2026-10-13; the security-facing obligation O6 was absent from the spine; the References caveat said the checker's status files describe the pre-07-07 world, which Phase 0 has fixed. The O5 note carried no adoption status. What changed: "three-prover (Agda, Idris2, Lean) verification stack plus a Rust fast core"; WP-2 gains a Status line (delivered; mechanisation remains); one sentence adds O6 (ceiling verdict) to the spine; the caveat becomes "Current as of 2026-10-27"; :revnumber: 0.3, :revdate: 2026-10-27. The O5 note's Status section opens with "Adopted into trope-checker spec §10 on 2026-10-13 (ADR 0005, pending owner ratification)". "gated by O4" does not occur in the file (checked). What I ran: grep -n "four-prover\|gated by O4\|Caveat" docs/status/RESEARCH-PROGRAMME.adoc -> no hits. What I did not run: n/a. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- docs/status/RESEARCH-PROGRAMME.adoc | 24 +++++++++++++------ .../defining-o5-veridicality-oracle.adoc | 2 ++ 2 files changed, 19 insertions(+), 7 deletions(-) diff --git a/docs/status/RESEARCH-PROGRAMME.adoc b/docs/status/RESEARCH-PROGRAMME.adoc index cc6d60a..bcde4fd 100644 --- a/docs/status/RESEARCH-PROGRAMME.adoc +++ b/docs/status/RESEARCH-PROGRAMME.adoc @@ -1,8 +1,8 @@ // SPDX-FileCopyrightText: © 2026 Jonathan D.A. Jewell (hyperpolymath) // SPDX-License-Identifier: CC-BY-SA-4.0 = A Programme of Work for Trope Theory -:revnumber: 0.2 (draft for review; synced to ratified calculus R-2026-07-07 / ADR 0004) -:revdate: 2026-07-16 +:revnumber: 0.3 (draft for review; synced to calculus v0.2 and ADR 0005, Proposed) +:revdate: 2026-10-27 :toc: macro :sectnums: :sectnumlevels: 3 @@ -33,7 +33,8 @@ This estate has started to build that missing dynamics: residual, a use-model, two verdicts), grounded in Williams/Campbell (`docs/background.adoc`). Status: *specification*. * `trope-checker` — the *graded calculus*, the Trope IR (the trust boundary), and a - four-prover verification stack. Status: *alpha, conformance-green*. + three-prover (Agda, Idris2, Lean) verification stack plus a Rust fast core. Status: + *alpha, conformance-green*. * `haec` (front-end language, *design*), `vocarium` (store, *M1 invoke slice; M2 adapter pending*), `hermeneia` (query, *implementation*). @@ -81,6 +82,11 @@ each companion document refers back to it. | Ask whether provenance-enrichment relocates or dissolves the regress (WP-1). |=== +Security-facing, and new at calculus v0.2: *O6*, the ceiling verdict +(`trope-checker/spec/calculus.adoc §10`) — the privacy direction, that no more than a +declared ceiling is retained, which the `Withheld`/`Severed` distinction exists to serve — +is the dual of the sufficiency verdict and sits on this spine as an open obligation. + == How to read the work packages Priority is triage, not chronology: @@ -146,6 +152,11 @@ provide, and the checker's exact relationship to it), or a proof that veridicali *not* checkable relative to the IR — with the README/AFFIRMATION references updated to match. +*Status.* Delivered: O5 is defined in `trope-checker/spec/calculus.adoc §10` (ADR 0005, +ratification pending), adopted on 2026-10-13 from +`../theory/formalisms/defining-o5-veridicality-oracle.adoc` unchanged in substance; what +remains is its mechanisation (O5-1 as a side condition on an `Oracle`-indexed verdict). + *Closes.* *O5* (define-or-refute). *Funder fit.* EPSRC / UKRI (formal methods); ARIA _Mathematics for Safe AI_. @@ -315,10 +326,9 @@ for work not yet done, and should be read as such. and atoms), and the ratified-carrier proofs (`L4Monotonicity.lean`, `EffectAtoms.lean`, `TierTwoComplete.lean`, `GradeRatified.lean`, `GradeFactorisationR.lean`). - *Caveat:* `trope-checker/docs/status/{ROADMAP,PROOF-STATUS}.adoc`, - `AFFIRMATION.adoc`, and `INTEGRATION-REPORT.adoc` were not updated in the - ratification wave and still describe the pre-07-07 world — prefer ADR 0004 and the - spec where they disagree. + *Current as of 2026-10-27:* `trope-checker/docs/status/{ROADMAP,PROOF-STATUS}.adoc` and + `AFFIRMATION.adoc` were rewritten to the ratified world in Phase 0; + `INTEGRATION-REPORT.adoc` is kept as the historical record under a header note. * Founding grounding: `trope-particularity-workbench/docs/background.adoc`. * Companion documents: `../theory/computing/trope-theory-and-neural-representation.adoc`, `../whitepapers/outreach/baffled-couch-potatoes.adoc`, diff --git a/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc b/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc index a4eabf5..a89b967 100644 --- a/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc +++ b/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc @@ -97,6 +97,8 @@ right slots, which is evidence the definition carves at a real joint: world-access vouched (O5-1) and left an attestation (O5-2). == Status and next step +*Adopted into trope-checker spec §10 on 2026-10-13 (ADR 0005, pending owner ratification).* + This note is the WP-2 deliverable in its *define* branch (the *refute* branch — that no useful oracle interface exists — is answered by the constructions above existing). From 734a9c6337517d32c8e4436f42f2ec7c02da6c2b Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:32:28 +0000 Subject: [PATCH 3/3] docs: cite the CI runs, shell-safe placeholders, O5 status reconciled, README link What was wrong (review findings on #77): STATE-OF-THE-STACK said "CI" for the Lean and vocarium rows without naming a run; its commands used ``, which Bash reads as redirection; RESEARCH-PROGRAMME's first-quarter sentence still said "WP-2 (define O5)" although the Status line says delivered; the O5 note's new status line sat above prose that still says O5 was never written down; the README bullet was monospace text, not a link. What changed: the Lean cell cites proofs.yml run 40472568287 (lake build succeeded; job red only in nanoda, trope-checker #104) and the vocarium cell cites vocarium-ci.yml run 40472451463 (invoke-slice gate success, 2026-10-27T08:17Z), with the workflow's real triggers; placeholders are `/path/to/tropecheck-rs`; the first-quarter sentence reads "WP-2's remainder (ratify ADR 0005, mechanise O5-1)"; the O5 note opens its Status section with a dated update that marks its proposal language historical and the spec normative; the README bullet is a link: macro. What I ran: n/a (prose). What I did not run: n/a. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31 --- README.adoc | 2 +- docs/status/RESEARCH-PROGRAMME.adoc | 2 +- docs/status/STATE-OF-THE-STACK.adoc | 14 ++++++++------ .../defining-o5-veridicality-oracle.adoc | 6 +++++- 4 files changed, 15 insertions(+), 9 deletions(-) diff --git a/README.adoc b/README.adoc index 267e0f2..e3a9a40 100644 --- a/README.adoc +++ b/README.adoc @@ -200,7 +200,7 @@ https://github.com/hyperpolymath/trope-particularity-workbench/tree/b18eb67dcf10 * https://hyperpolymath.github.io/trope-particularity-workbench/[the trainer] (source: `assets/particularity-trainer.html`) — drill until you can name the move from the test. * `docs/background.adoc` — why the vocabulary is compatible with the metaphysics it borrows from. -* `docs/status/STATE-OF-THE-STACK.adoc` — one table, one row per repo: status, what exists, +* link:docs/status/STATE-OF-THE-STACK.adoc[State of the trope stack] — one table, one row per repo: status, what exists, the obligations it owns, proof/test citations, and the ground-truth command that verifies it. * `docs/status/RESEARCH-PROGRAMME.adoc` — the prioritised, trope-stack-wide programme of work (what is worth doing next in the field, and who might fund it). diff --git a/docs/status/RESEARCH-PROGRAMME.adoc b/docs/status/RESEARCH-PROGRAMME.adoc index bcde4fd..f9724b8 100644 --- a/docs/status/RESEARCH-PROGRAMME.adoc +++ b/docs/status/RESEARCH-PROGRAMME.adoc @@ -300,7 +300,7 @@ the funding memo. | *Essay + ORCID/DOI first* | WP-8's low-cost items unblock every funding application immediately. |=== -A pragmatic first quarter: WP-2 (define O5) and WP-8's cheap items (ORCID, DOI, +A pragmatic first quarter: WP-2's remainder (ratify ADR 0005, mechanise O5-1) and WP-8's cheap items (ORCID, DOI, corrected citation, the essay) are low-effort and unblock both honesty and funding; WP-1 and WP-4 are the two papers most likely to attract a grant; WP-5 is the time-critical foundational one. diff --git a/docs/status/STATE-OF-THE-STACK.adoc b/docs/status/STATE-OF-THE-STACK.adoc index ed0c8c3..8e59c73 100644 --- a/docs/status/STATE-OF-THE-STACK.adoc +++ b/docs/status/STATE-OF-THE-STACK.adoc @@ -39,7 +39,9 @@ Lean provenance developments, conformance suite. checkers; `All.agda`/`Smoke.agda` under `--safe --without-K` exit 0. | `just check`, `just build-agda`, `just trope-rust`; `just build-lean` (needs lake + Mathlib; CI `proofs.yml`) -| 2026-10-27 (Lean: CI) +| 2026-10-27; Lean: `proofs.yml` run 40472568287 (2026-10-27T08:18Z) — `lake build` +succeeded for both packages, the job is red only in lean-action's `nanoda` step +(trope-checker #104) | haec | design @@ -48,7 +50,7 @@ obligations, three example program/IR pairs that round-trip through the checker. | O2 lowering correctness for its constructs. | `AFFIRMATION.adoc` 2026-10-27: 3 well-formed, schema matches canonical, 3 round-trips to the stated verdicts. -| `TROPECHECK_BIN= bash tests/check-examples.sh` +| `TROPECHECK_BIN=/path/to/tropecheck-rs bash tests/check-examples.sh` | 2026-10-27 | hermeneia @@ -59,7 +61,7 @@ stub store. | None of the calculus's; O2 as a producer, once it emits IR from a real store. | `AFFIRMATION.adoc` 2026-10-27: `cargo test --workspace` 39 pass; e2e slice 7 pass (`src/hermeneia-cli/tests/slice.rs`). -| `cargo test --workspace`; `HERMENEIA_TROPECHECK= cargo test -p +| `cargo test --workspace`; `HERMENEIA_TROPECHECK=/path/to/tropecheck-rs cargo test -p hermeneia-cli --features e2e --test slice` | 2026-10-27 @@ -70,9 +72,9 @@ door, `voc invoke` emitting Trope IR 0.2; the use-relativity gate. M2 StoreProvider adapter pending. | None of the calculus's; O2 as a producer; O5-2 attestations are its warrants. | `AFFIRMATION.adoc` 2026-10-27 (NOT RUN in that session; CI `vocarium-ci.yml` -runs `zig build test` and the gate on every push). -| `zig build test`; `TROPECHECK_BIN= bash tests/e2e/invoke_slice.sh` -| CI (see PR) +runs `zig build test` and the gate on pushes to `main`, pull requests and dispatch). +| `zig build test`; `TROPECHECK_BIN=/path/to/tropecheck-rs bash tests/e2e/invoke_slice.sh` +| CI run 40472451463, job "invoke-slice gate": success, 2026-10-27T08:17Z (vocarium #42) |=== == The five-repo map diff --git a/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc b/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc index a89b967..ce5c57a 100644 --- a/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc +++ b/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc @@ -97,7 +97,11 @@ right slots, which is evidence the definition carves at a real joint: world-access vouched (O5-1) and left an attestation (O5-2). == Status and next step -*Adopted into trope-checker spec §10 on 2026-10-13 (ADR 0005, pending owner ratification).* +*Status update, 2026-10-27.* The text below was written when `spec/calculus.adoc §10` +stopped at O4. Since the consolidation of 2026-10-13 that section carries O5, adopted +from this note unchanged in substance (trope-checker ADR 0005, *Proposed*); owner +ratification is pending, so the "proposal" and "never written down" language below is +historical — the normative text is now the spec's, and this note is its derivation. This note is the WP-2 deliverable in its *define* branch (the *refute* branch — that no