diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index f5d7501..4d98297 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -6,9 +6,9 @@ @state(version="2.0"): phase: "implementation" -next_action: "User roadmap — only (4) CONSOLIDATE remains. (1) gap-fill DONE (#49 fn/type/agent dup-detect; #46 import/locale/choreography). (2) L10 rung 3b STATIC half DONE (#50, branch l10-rung3b-static); rung-3b RUNTIME half (evaluator Holding/Spent replay) still a follow-on. (3) PROOF SUITE: verified 35/37 passing locally (full runner: idris2+agda+Rocq9), manifest labels refreshed to all-37-passing this branch; M2(mathcomp)+E1(Coquelicot) CI-only by github-only network. Optional leftovers: trace{} standalone-statement parse gap; M5/M1 were stale-labelled not actually missing. CONSOLIDATE = sweep docs/AFFIRMATION/status to the verified state, fold the open branches." -last_action: "Roadmap item 3 — PROOF SUITE GREEN verified + manifest status refresh (branch claude/proof-suite-status-refresh). Ran the FULL canonical-proof-suite-runner with the local toolchain (idris2 0.8 + agda 2.6.3 + Rocq 9.0, now awk-portable via #47): Summary 35/37 passing, 2 regressed. CRUCIAL finding: M5-yoneda.agda is NOT a stub — it's a complete 386-line self-contained Yoneda formalization that COMPILES runner-style (my earlier 'agda 0/1' was the same path/module-name trap as idris — must cd into dir + basename); likewise ~20 'not-started'-labelled rocq entries (M6-M14,S6-S10,E6-E11) actually compile+define their symbol. So the suite was far greener than the labels. Refreshed 21 not-started + 1 in-progress(M1) -> passing (verified); M2(mathcomp)+E1(Coquelicot ndim) kept prior CI-canonical passing (network-blocked locally). Did NOT regenerate REPORT/sidecars (would show M2/E1 locally-regressed; nightly CI regenerates canonical). Manifest balanced 500/500, 37 entries all passing, revision-log entry added. Prior this session: rung-3b static (#50), #49 fn/type/agent dup, #48 docs, #47 awk fix, Rocq9 local, #46/#45." -updated: 2026-06-19T21:45:00Z +next_action: "Roadmap (1)-(4) ALL DONE. Next substantive work = the L10 rung-3b RUNTIME half, which is blocked behind a prerequisite the user chose: BUILD MUTABLE AGENT STATE FIRST. Today an agent handler gets a COPY of state (run_agent_handler in eval.rs: env.set(name, val.clone())) with NO write-back, and there is no state-assignment statement — so a runtime residue cell has nowhere to persist across handlers. Step A: add a state-assignment statement (additive ControlStmt variant, e.g. `set = ` / ` := `) + evaluator write-back into AgentInstance.state; spec+grammar(pest<->ebnf)+tests in lockstep. Step B: explicit `residue ` agent-member cell (user's chosen design, refining the static half's implicit agent_residue_names presence-set) + runtime snapshot-on-`reversible as` / restore-on-`reverse` with Holding/Spent (Idris takeForReverse:Maybe is the model). This closes the once-only discipline the static half could only check by presence." +last_action: "Roadmap item (4) CONSOLIDATE — swept AFFIRMATION.adoc, the status doc, and the next-Claude handover prompt to the verified merged state at 214a08f (branch claude/consolidate-l10-rung3b-proofsuite). #50 (rung-3b static) merged to main via admin-merge; all four recent feature branches (#49/#50/#51 + earlier) deleted on origin, no open PRs, no dangling branches. Renamed docs/status/must-intend-wish-2026-06-19.adoc -> -2026-06-20.adoc and updated both xrefs (AFFIRMATION + handover). Row sweeps: gap-fill intend -> done (imports+locales+choreographies+functions+types+agents); L10 rung-3b -> static done / runtime is the named follow-on (needs mutable state first); proof-suite labels reconciled to 35/37-verified, last 2 (M2 mathcomp + E1 Coquelicot) CI-canonical. CHANGELOG [Unreleased] already current — not touched. Prior this session: rung-3b static (#50, merged), #51 proof-suite refresh (merged), #49 fn/type/agent dup (merged), #48 docs, #47 awk fix, Rocq9 local, #46/#45." +updated: 2026-06-20T00:18:53Z @blockers: - id: proof-debt diff --git a/.machine_readable/session-log.txt b/.machine_readable/session-log.txt index 5f0ee6b..17965a2 100644 --- a/.machine_readable/session-log.txt +++ b/.machine_readable/session-log.txt @@ -46,3 +46,5 @@ [2026-06-19 23:57:43] Roadmap item 3 — PROOF SUITE GREEN + manifest status refresh (branch claude/proof-suite-status-refresh off main c9a9e92). Ran full canonical-proof-suite-runner with local toolchain (idris2 0.8 + agda 2.6.3 + Rocq 9.0; runner awk-portable since #47): Summary 35/37 passing, 2 regressed. KEY: M5-yoneda.agda is a COMPLETE 386-line self-contained Yoneda proof that compiles runner-style — my earlier agda 0/1 was the path/module-name trap (run from repo-root vs cd-into-dir+basename, same as idris). ~20 not-started-labelled rocq entries (M6-M14/S6-S10/E6-E11) also compile+define-symbol. Refreshed 21 not-started + 1 in-progress(M1) -> passing (sed, verified by the runner pass); M2(mathcomp) + E1(Coquelicot ndim port) kept prior CI-canonical passing (their dep sources gitlab.inria.fr/erratique.ch are 403 in this github-only env). Did NOT commit the runner-regenerated REPORT/STATUS/sidecars (they show M2/E1 as locally-regressed; nightly CI regenerates the canonical evidence with full toolchain) — reverted them. Manifest now 37/37 passing, parens 500/500 balanced, 37 entries parse, revision-log entry added, last-manifest-update bumped to 2026-06-19. Only roadmap item (4) CONSOLIDATE remains; rung-3b RUNTIME half is a separate follow-on. Pushing -> draft PR. [2026-06-19 23:49:09] Roadmap item 2 — L10 RUNG 3b STATIC HALF (branch claude/l10-rung3b-static off pre-#49 main). Design (chosen autonomously per user "just drive"): IMPLICIT per-agent scope, static-half-first. check_agent_decl now collects agent_residue_names (all handlers reversible-as bindings, recursive collector mirroring collect_linear_lets) BEFORE the handler loop; the per-handler named_residues isolation stays (intra-body 3a linear discipline). take_named_residue changed Result<(),String> -> 3-way enum ResidueTake{Took,AlreadySpent,NotPresent}; ReverseNamed arm: Took=ok(3a consume), AlreadySpent=in-body double-reverse error, NotPresent=ok IFF agent_residue_names.contains(target) [cross-handler presence, rung 3b] else reverse-without-residue. Key correctness: AlreadySpent (in-body double) NOT masked by agent-presence; cross-FUNCTION still rejected (functions dont populate the set); cross-handler once-only deferred to RUNTIME (firing order unknown, takeForReverse:Maybe). Verified via CLI: r1 cross-handler OK, r2 undeclared->error, r3 in-body-double->error. 3 typechecker tests + examples/cross_handler_reversibility.007 (parse+check+RUN all pass). 900 oo7-core lib pass; fmt+clippy clean. Docs lockstep: spec TYPE-SYSTEM-SPEC new 11b.6, docs/echo-residue-integration.adoc (rung-3b static landed / runtime-half still open), CHANGELOG. REMAINING: 3b runtime half (evaluator replay); roadmap (3) full suite green [write M5 agda], (4) consolidate. Pushing -> draft PR. + +[2026-06-20 00:18:53] Roadmap item 4 — CONSOLIDATE (branch claude/consolidate-l10-rung3b-proofsuite off main 214a08f). #50 (L10 rung-3b static half) merged to main via admin-merge (sha 214a08f); webhook confirmed merged + auto-unsubscribed. State verified: no open PRs, all recent feature branches (#46/#48/#49/#50/#51 + earlier) deleted on origin, no dangling work. Swept the three governance docs to the verified merged state: (1) AFFIRMATION.adoc re-affirmed at 214a08f / 2026-06-20 — L10 now "done (static)" incl. rung-3b cross-handler-by-presence, the "I do NOT affirm" list reduced to the single runtime follow-on (mutable state) + the 2 CI-only proofs; (2) docs/status/must-intend-wish-2026-06-19.adoc renamed -> -2026-06-20.adoc (both xrefs updated), gap-fill intend -> done (imports+locales+choreographies+functions+types+agents), rung-3b row -> static done/runtime follow-on, proof-suite reconciled to 35/37-verified; (3) docs/handover/NEXT-CLAUDE-PROMPT.md regenerated at 214a08f — open-work list now leads with "build mutable agent state" (the user-chosen prerequisite) then the explicit `residue ` cell runtime half, fixed last-3->last-2 proof count, added the static->explicit-cell "evolution not reopen" note. CHANGELOG [Unreleased] already current (rung-3b static, fn/type/agent dup, just gate, proof gating all present) — not touched. STATE.a2ml next_action set to the mutable-state build (Step A: state-assignment ControlStmt + eval write-back into AgentInstance.state; Step B: explicit residue cell + snapshot/restore Holding/Spent). Docs-only consolidation; no code/proof changes, so no build delta to verify. diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 93509a0..5674b7e 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -9,8 +9,8 @@ | Field | Value | Repository | `hyperpolymath/007` -| Affirmed at | 2026-06-19T21:43:26Z (UTC) -| Commit affirmed | `2c52cf639cce81538970a3121af4c3a118d09f3e` (branch `main`) +| Affirmed at | 2026-06-20T00:18:53Z (UTC) +| Commit affirmed | `214a08f678c9554b31e2912de8bc36d9b1190c70` (branch `main`) | Scope | 007 language + canonical proof suite + RSR contractile state | Method | Local verification (`just gate`, the prover suite, the A2ML/K9 validators) | Affirmed by | Agent session (Claude Code), pending maintainer counter-signature @@ -43,11 +43,15 @@ verified: . *Harvard architecture.* Data and control languages are separated; the invariant is gated by `just verify-harvard` and the EBNF↔Pest grammar guard. . *Kategoria type safety L1–L10.* Levels L1–L9 are enforced in the type - checker. *Layer 10 (reversibility)* is now integrated into the type system: - `reversible`/`irreversible`/`reverse` are no longer checked identically — a - `reverse` requires a live `Linear>` echo residue, and the named form - `reversible as ` / `reverse ` binds and consumes a residue at - most once (phases 1–3a, mechanised in `proofs/idris2/EchoResidue*.idr`). + checker. *Layer 10 (reversibility)* is integrated into the type system at the + *static* level: `reversible`/`irreversible`/`reverse` are no longer checked + identically — a `reverse` requires a live `Linear>` echo residue, the + named form `reversible as ` / `reverse ` binds and consumes a + residue at most once, and (rung 3b static, #50) a cross-handler `reverse + ` type-checks by presence of the binding somewhere in the same agent + (phases 1–3a + rung 3b static, mechanised in + `proofs/idris2/EchoResidue*.idr`). The *runtime* replay is the one remaining + follow-on (see below). . *Honest proof discipline.* No proof-bypass escape hatches (unsafe coercions, totality overrides, holes, unproven assumptions); proofs are `--safe`/total. Enforced by the `bust` contractile and the canonical-proof-suite banned-scan. @@ -57,32 +61,41 @@ verified: The machine-checked D-gate is *partially* met and honestly labelled `in_progress`: 35 of 37 canonical proofs compile under a locally-installed -Rocq 9 (plus all Idris2/Agda entries), and the suite runner is now POSIX-awk -portable so it runs locally as well as in CI. +Rocq 9 (plus all Idris2/Agda entries), the manifest labels were swept to that +verified state (#51 — the prior `not-started` labels were a labelling lag, not +missing proofs; M5-yoneda is a complete 386-line Agda proof, and ~20 Rocq +entries already compiled), and the suite runner is now POSIX-awk portable so it +runs locally as well as in CI. The last 2 (mathcomp M2 / Coquelicot E1) remain +CI-canonical because their dependency sources are network-walled locally. == I do NOT affirm — what is open or blocked In the interest of honesty, the following are *not* affirmed as done: -* *L10 rung 3b* (cross-handler residues carried through agent state) is - `declared`, not built. It is irreducibly partly runtime. -* *Duplicate-definition coverage* extends to imports, locales, and - choreographies only; functions/types/agents still silently last-win on - redefinition. -* *Full proof suite green* — several canonical entries are `not-started`. +* *L10 rung 3b runtime* — the *static* half is built and merged (#50: + cross-handler `reverse ` type-checks by presence), but the *runtime* + replay (an evaluator actually executing the reversal log across handler + firings, the `Holding`/`Spent` `takeForReverse : Maybe` semantics) is not. + It is blocked behind a prerequisite: 007 has no *mutable agent state* yet — + handlers receive a copy of agent state with no write-back — so there is + nowhere for a residue cell to persist across handlers at runtime. Building + mutable agent state is the agreed next step before the runtime half. +* *Full proof suite green* — 35/37 verified locally; the last 2 (mathcomp / + Coquelicot) are verified in CI only, by network policy, not by lack of + effort. * *Two environmental blocks*, owner-side, not correctness: ** GitHub Actions billing — cloud CI is rejected before running; PRs this period were admin-merged through red CI after local verification. ** A github-only network policy blocks `gitlab.inria.fr` / `erratique.ch` / - `coq.inria.fr`, so the last 3 proofs' dependency sources (mathcomp ⇒ - hierarchy-builder ⇒ coq-elpi ⇒ elpi ⇒ menhir + cmdliner; Coquelicot) + `coq.inria.fr`, so the last 2 proofs' dependency sources (mathcomp M2 ⇒ + hierarchy-builder ⇒ coq-elpi ⇒ elpi ⇒ menhir + cmdliner; Coquelicot E1) cannot be fetched locally. These proofs are verified in CI instead. * *Echidna* (high-assurance interface verification) does not exist — it is a named ecosystem placeholder with no spec. == Evidence -* Detailed tier-by-tier status: `docs/status/must-intend-wish-2026-06-19.adoc`. +* Detailed tier-by-tier status: `docs/status/must-intend-wish-2026-06-20.adoc`. * Machine-readable project state: `.machine_readable/6a2/STATE.a2ml`. * Session ledger: `.machine_readable/session-log.txt`. * Local gate: `just gate` (green at the affirmed commit, all 9 stages). @@ -92,8 +105,8 @@ In the interest of honesty, the following are *not* affirmed as done: ____ I affirm that, to the best of this session's verification, the statements above -are an honest account of the repository at commit `2c52cf6` on -2026-06-19T21:43:26Z. Hard invariants labelled *done* were checked locally; +are an honest account of the repository at commit `214a08f` on +2026-06-20T00:18:53Z. Hard invariants labelled *done* were checked locally; items labelled *in_progress*, *declared*, or *blocked* are not claimed as complete. ____ @@ -102,7 +115,7 @@ ____ |=== | Signatory | Detail -| Agent | Claude Code session, 2026-06-19 +| Agent | Claude Code session, 2026-06-20 | Maintainer | Jonathan D.A. Jewell (hyperpolymath) — _counter-signature pending_ | Verification basis | local `just gate` + prover suite (cloud CI billing-blocked) |=== diff --git a/docs/handover/NEXT-CLAUDE-PROMPT.md b/docs/handover/NEXT-CLAUDE-PROMPT.md index 1056623..c8227df 100644 --- a/docs/handover/NEXT-CLAUDE-PROMPT.md +++ b/docs/handover/NEXT-CLAUDE-PROMPT.md @@ -4,7 +4,7 @@ # Prompt for the next Claude working on `hyperpolymath/007` > Copy everything below the line into the next session. It is written to be -> pasted as-is. Generated 2026-06-19T21:43:26Z at commit `2c52cf6`. +> pasted as-is. Generated 2026-06-20T00:18:53Z at commit `214a08f`. --- @@ -14,37 +14,57 @@ with a 10-level Kategoria type system). Read these first, in order: 1. `.machine_readable/6a2/STATE.a2ml` — `last_action` / `next_action`. 2. `AFFIRMATION.adoc` (repo root) — the honest current standing. -3. `docs/status/must-intend-wish-2026-06-19.adoc` — tier-by-tier status. +3. `docs/status/must-intend-wish-2026-06-20.adoc` — tier-by-tier status. 4. `.machine_readable/session-log.txt` — the running session ledger (append a new entry when you finish a unit of work). ## Where the work stands - **Layer 10 (reversibility / echo-types in the type system)** is the spine of - recent work. Phases 1→2→3a are merged: `reverse` requires a live - `Linear>` residue; `reversible as ` / `reverse ` bind and - consume a named residue at most once. Mechanised in + recent work. Phases 1→2→3a **and rung 3b static** are merged: `reverse` + requires a live `Linear>` residue; `reversible as ` / + `reverse ` bind and consume a named residue at most once; and a + cross-handler `reverse ` now type-checks by **presence** of the binding + in the same agent (`agent_residue_names` + the 3-way `ResidueTake` + `Took`/`AlreadySpent`/`NotPresent` in `typechecker.rs`). Mechanised in `proofs/idris2/EchoResidue.idr` + `EchoResidueLinear.idr`. -- **Typecheck gap-fill**: `gather_declarations` used to silently skip several - decls. Now there's duplicate-detection for **imports** (`DuplicateImport`) - and **locales/choreographies** (`DuplicateDefinition`) — see - `check_import_bindings` / `check_duplicate_definitions` in `typechecker.rs`. +- **Typecheck gap-fill is DONE.** `gather_declarations` used to silently skip + several decls. Duplicate-detection now covers **imports** (`DuplicateImport`) + *and* **locales / choreographies / functions / types / agents** + (`DuplicateDefinition`) — see `check_import_bindings` / + `check_duplicate_definitions` in `typechecker.rs`. Within-kind and per + top-level decl, so an `agent Name(...)` reference in a `supervisor children:` + list is correctly not a duplicate. - **`just gate`** is the one-command local CI (rustfmt, clippy, test, grammar-check, verify-harvard, e2e, idris2 proofs, a2ml, assail). Use it. -- **Canonical proof suite**: 35/37 compile under a locally-installed Rocq 9; - the runner is now POSIX-awk portable. +- **Canonical proof suite**: 35/37 compile under a locally-installed Rocq 9 and + the manifest is labelled to that verified state; the runner is POSIX-awk + portable. The last 2 (mathcomp / Coquelicot) are CI-canonical by network + policy. ## The open work (pick up here) -1. **L10 rung 3b** — cross-handler residues through agent **state** (a - `reversible` in `on receive` replayed by `reverse` in `on error`). This is - the last reversibility rung and is **partly runtime**: it needs a residue - cell in agent state + evaluator `Holding`/`Spent` semantics (the Idris - `takeForReverse : Maybe` models it). Do the *static* half first (the - "static core first" pattern that worked for 3a), then the runtime half. -2. **Extend duplicate-detection** to functions / types / agents (they still - last-win on redefinition). Same additive pattern as `DuplicateDefinition`. -3. **Proof suite** — drive `not-started` entries toward `passing`. +1. **Mutable agent state** — the agreed *prerequisite* for the L10 rung 3b + runtime half. Today an agent handler receives a **copy** of agent state and + there is **no write-back** (`run_agent_handler` in `eval.rs` binds the state + field with `env.set(name, val.clone())` and never persists changes), and + there is no state-assignment statement at all. The runtime residue cell has + nowhere to live across handler firings. So: add a state-assignment statement + (e.g. `set = ` / ` := `, an additive + `ControlStmt` variant so the compiler enumerates the match sites) and an + evaluator write-back into `AgentInstance.state`. Tests + spec + grammar + (`grammar.pest` ↔ `spec/grammar.ebnf`) in lockstep. +2. **L10 rung 3b runtime half** (after #1). The user's design choice is an + **explicit state cell**: a `residue ` agent member (a declared cell), + refining the static half's implicit presence-set. Then the runtime semantics + = snapshot the residue on `reversible as `, restore/replay it on + `reverse `, with `Holding`/`Spent` transitions (the Idris + `takeForReverse : Maybe` is the model). This closes the *once-only* + discipline that the static half could only check *by presence* (handler + firing order is not statically known). +3. **Proof suite** — 35/37 are verified locally and labelled `passing`. The + last 2 (mathcomp M2 / Coquelicot E1) are CI-canonical; nothing to do locally + on them unless the network policy changes. ## Critical environment knowledge (hard-won — saves you hours) @@ -55,8 +75,8 @@ with a 10-level Kategoria type system). Read these first, in order: - **Network is github-only.** `opam.ocaml.org`, `coq.inria.fr`, `gitlab.inria.fr`, `erratique.ch` all return 403. Rocq 9 was installed by pointing opam at the **github mirror** of opam-repository, and `coq-released` - is `github.com/coq/opam-coq-archive`. The last 3 proofs (mathcomp + - Coquelicot) are walled because their transitive sources (menhir on gitlab, + is `github.com/coq/opam-coq-archive`. The last 2 proofs (mathcomp M2 + + Coquelicot E1) are walled because their transitive sources (menhir on gitlab, cmdliner on erratique.ch) are not on github — leave them to CI. - A locally-built **Rocq 9 switch lives at `OPAMROOT=/root/.opam3`, switch `rocq9`**. To use it: `export OPAMROOT=/root/.opam3 && eval "$(opam env --root=/root/.opam3 --switch=rocq9)"`. idris2 is on `/root/.idris2/bin`. @@ -87,4 +107,10 @@ with a 10-level Kategoria type system). Read these first, in order: per-body affine cells — the static mirror of `ResidueCell`). - The runner awk-portability fix (`\s` → `[[:space:]]`, merged). - The Rocq-9-local-install conclusion: 35/37 is the achievable local number; - the last 3 are CI-only by network policy, not by lack of effort. + the last 2 are CI-only by network policy, not by lack of effort. + +Note (not a reopen, an *evolution*): rung 3b's static half checks cross-handler +residues by **presence** (`agent_residue_names`, an implicit per-agent set). +The planned runtime work deliberately *refines* this into an **explicit +`residue ` agent-member cell** — that is the agreed design, not a +contradiction of the merged static half. diff --git a/docs/status/must-intend-wish-2026-06-19.adoc b/docs/status/must-intend-wish-2026-06-20.adoc similarity index 60% rename from docs/status/must-intend-wish-2026-06-19.adoc rename to docs/status/must-intend-wish-2026-06-20.adoc index d68947f..be3fc5b 100644 --- a/docs/status/must-intend-wish-2026-06-19.adoc +++ b/docs/status/must-intend-wish-2026-06-20.adoc @@ -3,8 +3,8 @@ = Status — Musts, Intends, Wishes (Echidna + 007 language) :toc: left :sectnums: -:revdate: 2026-06-19T21:43:26Z -:commit: 2c52cf6 +:revdate: 2026-06-20T00:00:00Z +:commit: 214a08f [abstract] == Abstract @@ -23,7 +23,11 @@ NOTE: The repo's `Mustfile.a2ml` / `Intentfile.a2ml` are still the generic RSR-template-repo boilerplate (repo-hygiene gates + template wishes), so the *language-level* rows below are synthesised from the actual project state (`.machine_readable/6a2/STATE.a2ml`, the typechecker, the canonical proof -suite) plus the 2026-06-19 session. They are a report, not a gate. +suite) plus the 2026-06-19/20 session. They are a report, not a gate. This +revision is the *consolidation* sweep: #49 (fn/type/agent duplicate detection), +#50 (L10 rung 3b static half), and #51 (proof-suite status refresh) are now +merged to `main` at `214a08f`, and the rows below are swept to that verified +state. == Echidna — high-assurance interface verification @@ -53,27 +57,31 @@ verifies against, which repo) before a real status can exist. | Must | Harvard architecture (data/control bus separation) | done | Enforced — `just verify-harvard` + grammar guard (EBNF↔Pest) | Must | Kategoria type-safety levels L1–L9 | done | Enforced in the typechecker -| Must | L10 reversibility = echo-types in the type system | done (intra-body) | Phases 1→2→3a merged (#34/#41/#42): `reverse` needs a live `Linear>` residue; named residues bind/consume once +| Must | L10 reversibility = echo-types in the type system | done (static) | Phases 1→2→3a + rung 3b static merged (#34/#41/#42/#50): `reverse` needs a live `Linear>` residue; named residues bind/consume once; cross-handler `reverse ` type-checks by presence. Runtime replay is the remaining follow-on | Must | No proof-bypass escape hatches (unsafe coercions / holes / totality overrides); `--safe`/total proofs | done | `bust` contractile + suite banned-scan; zero violations -| Must | Every canonical claim machine-checked (D-gate) | in_progress | 35/37 rocq compile + all idris2/agda; suite runner now POSIX-portable (#47) +| Must | Every canonical claim machine-checked (D-gate) | in_progress | 35/37 verified locally (Rocq 9 + all idris2/agda); manifest labels refreshed to the verified state (#51); last 2 (mathcomp / Coquelicot) are CI-canonical (network-walled locally); runner POSIX-portable (#47) | Must | Repo / RSR hygiene (LICENSE, signed commits, contractiles, 6a2) | done | Per `Mustfile.a2ml`; A2ML + K9 validate clean -| Intend | L10 *rung 3b* — cross-handler residues via agent state | declared | The one remaining reversibility rung; partly RUNTIME (`takeForReverse : Maybe`) — not started -| Intend | Parser/typecheck gap-fill for silently-skipped decls | in_progress | Duplicate detection for imports + locales + choreographies (#46); functions/types/agents still last-wins on redefinition +| Intend | L10 *rung 3b* — cross-handler residues via agent state | in_progress | Static half DONE (#50): cross-handler `reverse ` type-checks by presence, in-body double-`reverse` still rejected. RUNTIME half (Holding/Spent replay, `takeForReverse : Maybe`) is the follow-on — it needs *mutable agent state* first (handlers currently receive a state copy with no write-back) +| Intend | Parser/typecheck gap-fill for silently-skipped decls | done | Duplicate detection now covers imports + locales + choreographies (#46) *and* functions + types + agents (#49); agent-references in `supervisor children:` correctly excluded | Intend | One-command, billing-independent local gate | done | `just gate` (#45) — 9 stages incl. the A2ML + assail tooling installed this session -| Intend | Full canonical proof suite green (all 37 entries) | in_progress | Several entries `not-started`; gated nightly in CI +| Intend | Full canonical proof suite green (all 37 entries) | in_progress | 35/37 verified locally and labelled `passing`; the stale `not-started` labels were a labelling lag, not missing proofs (#51 swept 21 entries + M5-yoneda to verified). Last 2 (mathcomp M2 / Coquelicot E1) remain CI-canonical | Intend | Restore GitHub Actions billing so cloud CI runs | blocked | Owner-side; every PR this session was admin-merged through red CI -| Wish (near) | Full proof suite runnable *locally* | in_progress | Rocq 9 installed → 35/37 local; last 3 (mathcomp / Coquelicot) walled by the github-only network policy +| Wish (near) | Full proof suite runnable *locally* | in_progress | Rocq 9 installed → 35/37 local; last 2 (mathcomp / Coquelicot) walled by the github-only network policy | Wish (mid) | Ordinal track → Bachmann–Howard; Pillar E paper | declared | Lives in `echo-types`; not touched this session | Wish (far) | Echidna interface verification wired into 007 | declared | Depends on Echidna existing (above) |=== *Bottom line (007 language):* the *musts are essentially met* — Harvard -invariant, L1–L10 type safety, total/safe proofs, and repo compliance all -hold. The live frontier is the *intends*: L10 rung 3b (the last reversibility -piece, partly runtime) and continued typecheck gap-fill. The 2026-06-19 -session advanced both a must (L10 fully into the type system) and several -intends (the local gate, three duplicate-detection passes, local proof -execution via a self-installed Rocq 9). +invariant, L1–L10 type safety (now including L10 rung 3b *static*), total/safe +proofs, and repo compliance all hold. The typecheck gap-fill intend is +*closed* (duplicate detection across imports, locales, choreographies, +functions, types, and agents). The live frontier is a single, well-scoped +follow-on: the *runtime* half of L10 rung 3b — replaying a reversal log across +handlers — which is blocked behind 007 not yet having *mutable agent state* +(handlers receive a state copy with no write-back). The 2026-06-19/20 session +advanced a must (L10 cross-handler static) and closed several intends (the +local gate, the full duplicate-detection sweep, local proof execution via a +self-installed Rocq 9), then consolidated #49/#50/#51 to `main`. == The one red thing @@ -81,8 +89,9 @@ Across both scopes the only red is *environmental, not correctness*: * *GitHub Actions billing* — owner-side; cloud CI is rejected before it runs. * *github-only network policy* — blocks `gitlab.inria.fr` / `erratique.ch` / - `coq.inria.fr`, which is why the last 3 proofs' dependency sources (mathcomp - via hierarchy-builder/coq-elpi/elpi → menhir + cmdliner; Coquelicot) cannot - be fetched locally. They ARE verified in CI, which has unrestricted network. + `coq.inria.fr`, which is why the last 2 proofs' dependency sources (mathcomp + M2 via hierarchy-builder/coq-elpi/elpi → menhir + cmdliner; Coquelicot E1) + cannot be fetched locally. They ARE verified in CI, which has unrestricted + network. Everything mergeable has been verified locally and is green.