diff --git a/README.adoc b/README.adoc index f3989c2..e3a9a40 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. +* 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). * `docs/theory/computing/trope-theory-and-neural-representation.adoc` — a position paper diff --git a/docs/status/RESEARCH-PROGRAMME.adoc b/docs/status/RESEARCH-PROGRAMME.adoc index cc6d60a..f9724b8 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_. @@ -289,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. @@ -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/status/STATE-OF-THE-STACK.adoc b/docs/status/STATE-OF-THE-STACK.adoc new file mode 100644 index 0000000..8e59c73 --- /dev/null +++ b/docs/status/STATE-OF-THE-STACK.adoc @@ -0,0 +1,98 @@ +// 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: `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 +| 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=/path/to/tropecheck-rs 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=/path/to/tropecheck-rs 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 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 + +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. diff --git a/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc b/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc index a4eabf5..ce5c57a 100644 --- a/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc +++ b/docs/theory/formalisms/defining-o5-veridicality-oracle.adoc @@ -97,6 +97,12 @@ 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 +*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 useful oracle interface exists — is answered by the constructions above existing).