diff --git a/docs/practice/AI-CONVENTIONS.adoc b/docs/practice/AI-CONVENTIONS.adoc index f988ee8..d606550 100644 --- a/docs/practice/AI-CONVENTIONS.adoc +++ b/docs/practice/AI-CONVENTIONS.adoc @@ -12,7 +12,7 @@ Per-tool config files (.cursorrules, .clinerules, etc.) reference this document. ## Session Startup 1. Read `0-AI-MANIFEST.a2ml` FIRST (mandatory gatekeeper). -2. Read `.machine_readable/descriptiles/STATE.a2ml` for current status and blockers. +2. Read `docs/status/JOURNAL.adoc` for the current phase, blockers and next action. It governs over the journal sections of `.machine_readable/descriptiles/STATE.a2ml`, which stays only until its consumers are rewired. 3. Read `.machine_readable/descriptiles/anchors/ANCHOR.a2ml` for canonical authority boundaries. 4. Read `.machine_readable/policies/MAINTENANCE-AXES.a2ml` for maintenance/audit sequencing. 5. Read `.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml` for baseline controls. @@ -80,7 +80,8 @@ Use `just` (Justfile) for all build, test, lint, and format tasks. - `0-AI-MANIFEST.a2ml` -- universal AI entry point - `.machine_readable/descriptiles/AGENTIC.a2ml` -- agent permissions and constraints -- `.machine_readable/descriptiles/STATE.a2ml` -- current project state +- `docs/status/JOURNAL.adoc` -- thin session journal: phase, blockers, last and next action +- `.machine_readable/descriptiles/STATE.a2ml` -- legacy project state (kept until its consumers are rewired) - `.machine_readable/descriptiles/anchors/ANCHOR.a2ml` -- canonical authority and policy boundary - `.machine_readable/policies/MAINTENANCE-AXES.a2ml` -- canonical axis sequencing and audit requirements - `.machine_readable/policies/MAINTENANCE-CHECKLIST.a2ml` -- baseline maintenance checklist policy diff --git a/docs/status/JOURNAL.adoc b/docs/status/JOURNAL.adoc new file mode 100644 index 0000000..a9e5f02 --- /dev/null +++ b/docs/status/JOURNAL.adoc @@ -0,0 +1,83 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += systemet — thin session journal +:updated: 2026-11-10 + +What the next agent or human needs to resume work, and nothing that can be +derived. This is the STATE v2 thin journal +(`1-formats/templates/STATE.a2ml.v2.spec.adoc` in `standards`: phase, blockers, +last action, next action), written as AsciiDoc because A2ML is retired. + +Where this file and the journal sections of +`.machine_readable/descriptiles/STATE.a2ml` disagree, **this file governs** +(`state-v1-decision`, option B, ruled 2026-11-10). `STATE.a2ml` stays only +until the checks and scripts that still require it are rewired. + +Kept elsewhere, on purpose: milestones in `ROADMAP.adoc`, history in the git +log, evidence and the completion census in `PROOF-STATUS.adoc`, task lists in +the GitHub issues. + +phase:: +implementation. The mechanized core is in place: the L2 grade algebras (ET-4, +ET-5) and L1 conversion for the β-fragment of the core calculus (ET-1, ET-2). +The η extension, the gates beyond L2, tropes and TEA erasure (ET-14) are open. +Census, with its denominator: 2 of 15 ET obligations done and 2 in progress +(`docs/status/PROOF-STATUS.adoc`). + +last_action:: +Finished the wager experiment in Cubical Agda: stages 5 to 7 and the final +verdict (#89, 2026-11-10). W does not hold as written. It holds for the +fragment with 2 additions: trope states with an index, and, for a whole +program, a grade algebra in which the grade 𝟙 is unrestricted. + +next_action:: +Land the η-long normalizer `nfE` (issue #32). It is blocked on an `adjWkv` +weakening-exchange lemma (`docs/status/PROOF-STATUS.adoc`). + +session_marker:: +next_action taken from PROOF-STATUS (open items) and STATE v1 (2026-07-29); +owner to confirm it is still the intended next step. + +updated:: +2026-11-10 + +== Blockers + +[cols="2,5,3,2",options="header"] +|=== +| id | description | waiting_on | since + +| `wager-owner-decisions` +| Two decisions are with the owner: the class of the kinding judgement (R1), + and the class of the extension of Stage 6, part 2 (R23, R24). The verdict + gives the facts for each answer and does not decide + (`verification/proofs/agda/Wager/VERDICT.adoc`, which also holds draft ADR + text that is not filed). +| owner +| 2026-11-10 + +| `et-16-further-adr` +| ET-14 (TEA erasure) is OPEN, a research target. ET-16, the L0 observation + interface, is adopted narrowly and is specified, with mechanization not + started (ADR-0002). The broader claim, that lowering preserves L1 conversion, + is unadopted and needs its own ADR. +| owner (a further ADR) +| 2026-07-27 (ADR-0002) + +| `state-archive-rewire` +| `STATE.a2ml` cannot be archived yet. `openssf-compliance.yml`, the Must + invariant, `scripts/validate-template.sh`, the e2e template test and the + arrival-pack generator still require it. +| rewiring those consumers (several are derived from the estate canon) +| 2026-11-10 +|=== + +== Provenance + +* `phase` comes from `docs/status/PROOF-STATUS.adoc` (summary table and the + ET-1/ET-2 rows). +* `last_action` and the `wager-owner-decisions` blocker come from the merge + commit of #89 and `Wager/VERDICT.adoc` (R1, R23, R24 checked there). +* `et-16-further-adr` comes from `docs/theory/OBLIGATIONS.adoc` (ET-14, ET-16). +* `next_action` is in `PROOF-STATUS.adoc`; that it is the *intended* next step + is carried from STATE v1 and not re-verified. diff --git a/systemet_chora.deed b/systemet_chora.deed index c06b3bc..d3c74fb 100644 --- a/systemet_chora.deed +++ b/systemet_chora.deed @@ -14,11 +14,11 @@ ;; per state-v1-decision.adoc, OPTION B [RULED 2026-11-10, owner] ;; Carried: [position] maturity -> (maturity :level ...); ;; [metadata] status "active" dedupes into (status :phase active). -;; NOT carried (journal / derivable; they go to the archive -;; surface, never the deed): [route-to-mvp], [blockers-and-issues], -;; [critical-next-actions], [maintenance-status], -;; completion-percentage. [position] phase "implementation" has -;; no home under B (see the (status) comment below). +;; NOT carried (journal / derivable, never the deed): milestones +;; stay in docs/status/ROADMAP.adoc; blockers, the next action and +;; the free-text [position] phase "implementation" go to the thin +;; journal, docs/status/JOURNAL.adoc; [maintenance-status] and +;; completion-percentage are derivable and dropped. ;; 0-AI-MANIFEST.a2ml (root) -> (manifest)(agent)(policy)(work) ;; per ai-manifest-decision.adoc, OPTION A [RULED 2026-11-10, owner] ;; Agent seen-set: open, flag-any-unknown (the spec's default; the @@ -61,11 +61,10 @@ ; CLADE.a2ml carries no [status] section, so :phase comes from STATE v1 ; [metadata] status = "active", which dedupes into this clause under ; state-v1-decision option B (one lifecycle truth, in the registry surface). - ; QUESTION FOR THE OWNER: STATE's separate [position] phase = "implementation" - ; uses a different vocabulary (design | implementation | testing | maintenance - ; | archived) from this closed lifecycle enum (reserved incubating active - ; dormant | merged superseded archived extinct), and maturity has its own - ; clause. Option B gives it no home, so it is preserved only in the archive. + ; STATE's separate [position] phase = "implementation" is a development-stage + ; label in a different vocabulary (design | implementation | testing | + ; maintenance | archived) from this closed lifecycle enum, so it is not written + ; here. It lives in the journal's free-text phase (docs/status/JOURNAL.adoc). (status :phase active :since "2026-06-28" :present #t