docs: truth pass across human, machine, and wiki documentation + DEBT register

.gitignore

@@ -80,3 +80,6 @@ CoqMakefile.conf
 *.pem
 *.key
 .venv/
+
+# Claude Code session worktrees (untracked second checkouts of this repo)
+.claude/worktrees/

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -4,15 +4,17 @@
 # ECOSYSTEM.a2ml — My Lang ecosystem position
 [metadata]
 version = "1.1"
-last-updated = "2026-06-02"
+last-updated = "2026-08-07"
 
 [project]
 name = "My Lang"
 purpose = """
 Multi-dialect programming language with Quantitative Type Theory (QTT) semantic
 core. Combines affine/linear type discipline, echo-type loss modelling, formal
-mechanised proofs, and AI-adjacent effect tracking. Four dialects: solo, duet,
-ensemble, me.
+mechanised proofs, and AI-adjacent effect tracking. Dialects are NESTED
+conservative extensions — solo ⊂ duet ⊂ ensemble — plus `me`, an agent-generated
+PROJECTION over that hierarchy rather than a fourth dialect. Only solo is
+authoritative in f0.
 """
 role = "flagship-language-experiment"
 licence = "MPL-2.0"
@@ -72,11 +74,11 @@ projects = [
 reference = "proofs/ALIGNMENT-PLAN.md"
 gaps-closed = [
   "G1-partial: mechanised QTT solo-core scaffold on dual Coq + Idris2 tracks (F1.0 done)",
+  "G1-remainder: F1.1 small-step semantics, F1.3 progress, F1.4 preservation + ht_subst + affine_pres — all machine-checked and axiom-free on the Coq track (closed 2026-06-14)",
+  "G2: mechanised operational semantics constructors present on both tracks (F1.1)",
+  "G3: proof CI leg live — .github/workflows/proofs.yml with per-rung Print-Assumptions gates (F5, closed 2026-06-14)",
+  "G5: coqc + idris2 --build both run in CI (same workflow)",
 ]
 gaps-open = [
-  "G1-remainder: F1.1–F1.4 (small-step semantics, progress/preservation proofs)",
-  "G2: no mechanised operational semantics constructors yet",
-  "G3: proof CI leg absent (Phase F5)",
   "G4: paper-proof topic parity (quantitative-types doc, row-polymorphism, Hoare semantics, categorical semantics, complexity analysis)",
-  "G5: no coqc/idris2 CI leg",
 ]

.machine_readable/6a2/STATE.a2ml

@@ -5,7 +5,7 @@
 [metadata]
 project = "my-lang"
 version = "0.2.0"                                # matches Cargo.toml [workspace.package]
-last-updated = "2026-07-27"
+last-updated = "2026-08-07"
 status = "active"
 session = "CI/CD + supply-chain close-out (PRs #143/#146/#147): codeql-action repointed off a NONEXISTENT SHA; all 15 Hypatia findings triaged (8 fixed at source incl. a self-referential critical, 7 baselined to 2026-10-27 under issue #145); unsafe_block ruled unsatisfiable and scoped-exempted; GitHub Pages un-stuck (workflow was disabled_manually) and LIVE; ARCHITECTURE.md + Justfile de-boilerplated. main FULLY GREEN — 2026-07-27"
 prior-session = "Coq solo-core: R2–R5b (SEMIRING functor / affine_pres / Tropical / usage-walk checker / aff_type_dec) + M1 me→solo elaboration + structure climb S1.0–S3c.3-msg (session-π: subject reduction, fidelity, progress, duet-by-projection, n-party projection totality, static n-party config, label-union merge, union-projection, n-ary located operational semantics, head-coupled message subject reduction = first earned n-party safety half) + E4 residue-measure SEAM (Coq mirror) — all axiom-free, CI-gated — 2026-06-14"
@@ -44,7 +44,7 @@ qtt-semiring-idris2 = "locally-checked"
 solo-syntax-contexts-typing = "machine-checked"
 operational-semantics = "machine-checked"      # F1.1 — CBV step/Step committed both tracks
 progress = "machine-checked"                    # F1.3 — Coq Qed (axiom-free), CI Print Assumptions closed; Idris total/hole-free
-preservation = "machine-checked"                # F1.4 — Coq Qed (axiom-free, ht_subst), CI-gated; Idris ?todo_preservation deliberately open (D1 option A)
+preservation = "machine-checked"                # F1.4 — Coq Qed (axiom-free, ht_subst), CI-gated. CORRECTION 2026-08-07: the Idris ?todo_preservation hole was DISCHARGED 2026-06-21 (#108) — zero ?todo holes remain in proofs/verification/idris/. proofs/STATUS.md still grades the Idris track locally-checked (its CI job runs idris2 --build with NO hole assertion — DEBT.md P-2).
 resource-algebra-functor = "machine-checked"   # R2 — SoloCoreF over Module Type SEMIRING; Include Linear3 = R0 axiom-free
 affine-pres = "machine-checked"                 # R3 — distinct affine budget-preservation over ORDERED_SEMIRING qle
 tropical-instance = "machine-checked"           # R4 — SoloCoreF Tropical, infinite min-plus carrier, axiom-free
@@ -89,7 +89,8 @@ milestones = [
   { id = "S3c.1", description = "Union-projection proj_u/projectable_u_wf + keystone existence theorem projection_total_u + one-directional monotonicity bridge projectable_wf_implies_u (on keystone merge_forces_eq: plain merge is the identity-meet); SEPARATE proj_u added ALONGSIDE proj (canonical proj byte-identical, NOT re-pointed); projection-EXISTENCE only, non-vacuity g_union3 in union-projectable minus plain-projectable; axiom-free", status = "done", date = "2026-06-14" },
   { id = "S3c.2", description = "n-ary LOCATED operational semantics: nstep (located mirror of fused cstep; one comm ra_set-updates exactly the two roles) + ra_set + global gstep + nstar/gstar closures + functional wf_assignment_f (wf_assignment_to_f keeps S3b green); 3-party ring run 0->1->2->0 witnessed both sides (ring_runs_to_end, g_ring_gsteps); ADEQUACY-only, nstep_breaks_wf_at_fixed_G PROVES no fixed-G subject reduction; axiom-free", status = "done", date = "2026-06-14" },
   { id = "S3c.3-msg", description = "Head-coupled message subject reduction nstep_sr_msg_head (the FIRST EARNED n-party safety half): the head communication sanctioned by GMsg p q t G' carries wf_assignment_f from G to its continuation G' (3-way located role split; same v:t sender ships = receiver substitutes via pty_subst0); coupled corollary nstep_gstep_sr_msg_head; earned-safety headline sr_earns_safety_across_step (same ra_ring1 S3c.2 refuted at fixed g is wf at stepped g); run-ahead fence SELF-WITNESSED (runahead_breaks_head_coupling). Design-panel-validated + independently adversary-verified (sound-and-honest). HEAD message fragment, preservation only; axiom-free", status = "done", date = "2026-06-14" },
-  { id = "S3c.3-choice/perm + S3c.4", description = "remaining n-party safety: select/branch SR (S3c.3-choice, couple NStep_Sel with a choice-gstep), run-ahead/permutation SR (S3c.3-perm, needs gstep-with-swap relation), n-party progress (S3c.4 = coherence ⇒ safety, research-hard — fence; wf_assignment ra -> deadlock-free is FALSE)", status = "pending", note = "S3c.0/.1/.2/.3-msg landed; the message-HEAD safety half is earned; choice/permutation/progress remain, solo" },
+  { id = "S3c.3-choice", description = "head-coupled select/branch subject reduction — the CHOICE analogue of nstep_sr_choice_head; couples NStep_Sel with a choice-gstep to the selected continuation Gl = gbget l bs", status = "done", date = "2026-08-07", note = "CORRECTION 2026-08-07: recorded as pending here while .github/workflows/proofs.yml:319-343 already gates nstep_sr_choice_head / nstep_gstep_sr_choice_head / proj_br_selected / proj_uninv_selected / wf_ra_choice3 / choice3_head_fires_end_to_end as axiom-free. The CI was ahead of this file; re-verify the landing date against git history." },
+  { id = "S3c.3-perm + S3c.4", description = "remaining n-party safety: run-ahead/permutation SR (S3c.3-perm, needs gstep-with-swap relation), n-party progress (S3c.4 = coherence ⇒ safety, research-hard — fence; wf_assignment ra -> deadlock-free is FALSE)", status = "pending", note = "S3c.0/.1/.2/.3-msg/.3-choice landed; permutation SR and n-party progress remain, solo" },
   { id = "E4", description = "Echo residue-measure SEAM (Coq mirror): RESIDUE_MEASURE + EchoTraceTropical + echo_measure_not_injective; full measure-independence upstream-cited", status = "done", date = "2026-06-14" },
   { id = "F2", description = "Effects metatheory mechanised", status = "pending" },
   { id = "F3", description = "Memory model mechanised", status = "pending" },
@@ -148,10 +149,10 @@ idris2 = "built from source in CI — see proofs.yml"
 task-runner = "just (Justfile); parse-verified 2026-07-27"
 
 [maintenance-status]
-last-run-utc = "2026-07-27T18:15:00Z"
-last-result = "pass"
-main-commit = "8636e15"
-main-board = "FULLY GREEN — every workflow on main succeeds or is deliberately skipped"
+last-run-utc = "2026-08-07T07:56:37Z"
+last-result = "mixed — see main-board"
+main-commit = "e68bb3d"
+main-board = "MIXED — the six standards-reusable wrappers parse again after the lockfile work (#152/#153), but dependabot bumps #155/#157 restaked 7 of 15 workflows: CodeQL + OSSF Scorecard startup_failure, Governance red on its own actions-lock --verify-local step. Repaired in PR #158. Lockfile regeneration is a RECURRING obligation on every action bump — see DEBT.md I-1."
 ci-governance = "pass"                 # incl. Validate Hypatia Baseline, green for the first time since >=2026-07-22
 ci-security-scan = "pass"              # Hypatia Security Scan + Secret Scanner + CodeQL + Scorecard
 ci-rust-tests = "pass"                 # Coverage (llvm-cov, floor 40%)

CONTRIBUTING.md

@@ -1,122 +1,179 @@
-<!-- SPDX-License-Identifier: MPL-2.0-or-later -->
+<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
 <!-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
-<!--
-SPDX-License-Identifier: CC-BY-SA-4.0
-Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--->
-# Clone the repository
+<!-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
+# Contributing to my-lang
+
+Thanks for your interest. my-lang is an early-alpha research language: an
+affine / Quantitative-Type-Theory core whose metatheory is mechanised in Coq
+and Idris2, with a Rust compiler that is being brought into correspondence
+with those proofs.
+
+That last part shapes everything below. **Changes to typing rules are proof
+obligations, not just code changes.** See [Proof-affecting changes](#proof-affecting-changes).
+
+## Getting set up
+
+```sh
+# Clone
 git clone https://github.com/hyperpolymath/my-lang.git
 cd my-lang
 
-# Using Nix (recommended for reproducibility)
-nix develop
+# Initialise submodules (proof tracks and vendored specs)
+just init
 
-# Or using toolbox/distrobox
-toolbox create my-lang-dev
-toolbox enter my-lang-dev
-# Install dependencies manually
-
-# Verify setup
-just check   # or: cargo check / mix compile / etc.
-just test    # Run test suite
+# Verify the toolchain works
+just check      # fmt-check + lint + test
+just test       # unit + conformance tests (excludes my-llvm)
 ```
 
-### Repository Structure
-```
-my-lang/
-├── src/                 # Source code (Perimeter 1-2)
-├── lib/                 # Library code (Perimeter 1-2)
-├── extensions/          # Extensions (Perimeter 2)
-├── plugins/             # Plugins (Perimeter 2)
-├── tools/               # Tooling (Perimeter 2)
-├── docs/                # Documentation (Perimeter 3)
-│   ├── architecture/    # ADRs, specs (Perimeter 2)
-│   └── proposals/       # RFCs (Perimeter 3)
-├── examples/            # Examples (Perimeter 3)
-├── spec/                # Spec tests (Perimeter 3)
-├── tests/               # Test suite (Perimeter 2-3)
-├── .well-known/         # Protocol files (Perimeter 1-3)
-├── .github/             # GitHub config (Perimeter 1)
-│   ├── ISSUE_TEMPLATE/
-│   └── workflows/
-├── CHANGELOG.md
-├── CODE_OF_CONDUCT.md
-├── CONTRIBUTING.md      # This file
-├── GOVERNANCE.md
-├── LICENSE
-├── MAINTAINERS.md
-├── README.adoc
-├── SECURITY.md
-├── flake.nix            # Nix flake (Perimeter 1)
-└── Justfile             # Task runner (Perimeter 1)
-```
+You need a stable Rust toolchain. The LLVM back end (`my-llvm`) additionally
+needs **system LLVM 21**, which is why the default `build`/`test` recipes
+exclude it — use `just build-all` / `just test-all` when you have it.
 
----
+Proof work additionally needs **Coq/Rocq** and/or **Idris2**:
 
-## How to Contribute
+```sh
+just proofs        # both tracks
+just proofs-coq    # the authoritative track
+just proofs-idris  # the Idris2 twin
+```
 
-### Reporting Bugs
+Run `just --list` for the full recipe set.
 
-**Before reporting**:
-1. Search existing issues
-2. Check if it's already fixed in `main`
-3. Determine which perimeter the bug affects
+## Repository structure
 
-**When reporting**:
+```
+my-lang/
+├── crates/            # the Cargo workspace — all live compiler code
+│   ├── my-lang/       #   core: lexer, parser, checker, interpreter, stdlib
+│   ├── my-parser/     #   standalone parser
+│   ├── my-qtt/        #   QTT kernel — the port of the verified Coq checker
+│   ├── my-hir/  my-mir/  my-llvm/    # lowering pipeline → native
+│   ├── my-cli/        #   the `my` binary
+│   ├── my-fmt/ my-lint/ my-lsp/ my-dap/ my-debug/ my-pkg/ my-test/
+│   └── my-ai/         #   AI-assist surface (mock operations — see DEBT.md)
+├── proofs/            # mechanised metatheory (Coq + Idris2) + STATUS.md
+├── dialects/          # dialect definitions (solo, duet)
+├── docs/              # design notes, ADRs, and the in-tree wiki
+├── spec/  conformance/  tests/  fuzz/    # specification and test surfaces
+├── examples/          # sample programs
+├── .machine_readable/ # machine-facing state, contractiles, service metadata
+└── Justfile           # task runner — the golden path
+```
 
-Use the [bug report template](.github/ISSUE_TEMPLATE/bug_report.md) and include:
+Note: the root `src/`, `lib/` and `tests/` trees are **orphaned** — not
+referenced by any crate. They are tracked as debt in [`DEBT.md`](DEBT.md);
+do not add to them.
 
-- Clear, descriptive title
-- Environment details (OS, versions, toolchain)
-- Steps to reproduce
-- Expected vs actual behaviour
-- Logs, screenshots, or minimal reproduction
+## How to contribute
 
-### Suggesting Features
+### Reporting bugs
 
-**Before suggesting**:
-1. Check the [roadmap](ROADMAP.md) if available
-2. Search existing issues and discussions
-3. Consider which perimeter the feature belongs to
+Search existing issues first, then use the
+[bug report template](.github/ISSUE_TEMPLATE/bug_report.md). Include the
+environment, steps to reproduce, expected vs actual behaviour, and a minimal
+reproduction where possible.
 
-**When suggesting**:
+For a miscompilation or a type-checker soundness bug, say so explicitly — those
+are triaged ahead of everything else, and may indicate a divergence between the
+implementation and the mechanised specification.
 
-Use the [feature request template](.github/ISSUE_TEMPLATE/feature_request.md) and include:
+### Suggesting features
 
-- Problem statement (what pain point does this solve?)
-- Proposed solution
-- Alternatives considered
-- Which perimeter this affects
+Check [`ROADMAP.adoc`](ROADMAP.adoc) and
+[`proofs/STATUS.md`](proofs/STATUS.md) first — a surprising amount of "missing"
+functionality is deliberately fenced pending a proof. Then use the
+[feature request template](.github/ISSUE_TEMPLATE/feature_request.md).
 
-### Your First Contribution
+### Good first contributions
 
-Look for issues labelled:
+- [`good first issue`](https://github.com/hyperpolymath/my-lang/labels/good%20first%20issue)
+- [`help wanted`](https://github.com/hyperpolymath/my-lang/labels/help%20wanted)
+- [`documentation`](https://github.com/hyperpolymath/my-lang/labels/documentation)
 
-- [`good first issue`](https://github.com/hyperpolymath/my-lang/labels/good%20first%20issue) — Simple Perimeter 3 tasks
-- [`help wanted`](https://github.com/hyperpolymath/my-lang/labels/help%20wanted) — Community help needed
-- [`documentation`](https://github.com/hyperpolymath/my-lang/labels/documentation) — Docs improvements
-- [`perimeter-3`](https://github.com/hyperpolymath/my-lang/labels/perimeter-3) — Community sandbox scope
+Documentation accuracy fixes are especially welcome — see [`DEBT.md`](DEBT.md)
+for a catalogue of known-stale pages.
 
----
+## Development workflow
 
-## Development Workflow
+### Branches
 
-### Branch Naming
 ```
-docs/short-description       # Documentation (P3)
-test/what-added              # Test additions (P3)
-feat/short-description       # New features (P2)
-fix/issue-number-description # Bug fixes (P2)
-refactor/what-changed        # Code improvements (P2)
-security/what-fixed          # Security fixes (P1-2)
+docs/short-description        # documentation
+test/what-added               # test additions
+feat/short-description        # new features
+fix/issue-number-description  # bug fixes
+refactor/what-changed         # internal improvements
+security/what-fixed           # security fixes
+proof/what-proved             # mechanised proof work
 ```
 
-### Commit Messages
+### Commits
 
 We follow [Conventional Commits](https://www.conventionalcommits.org/):
+
 ```
 <type>(<scope>): <description>
 
 [optional body]
 
 [optional footer]
+```
+
+**Commits must be cryptographically signed.** The `main` branch ruleset
+enforces `required_signatures`, so unsigned commits are rejected at push time:
+
+```sh
+git config --global commit.gpgsign true
+git config --global user.signingkey <your-key-id>
+```
+
+SSH signing works too (`gpg.format = ssh`). A linear history is also enforced —
+rebase rather than merge.
+
+### Pull requests
+
+1. Branch from `main`.
+2. Keep the change focused; unrelated cleanups belong in their own PR.
+3. Run `just check` before pushing.
+4. Update `CHANGELOG.md` under `[Unreleased]`.
+5. If you touched documentation claims, make sure they are still true — this
+   repository has an explicit honesty discipline (below).
+
+CI gates include governance/licence checks, the Hypatia neurosymbolic scanner,
+secret scanning, CodeQL, and both proof tracks. A red proof gate blocks merge.
+
+## Proof-affecting changes
+
+If your change touches the typing rules, usage/quantity discipline, the QTT
+kernel (`crates/my-qtt/`), or anything in `proofs/`:
+
+- [`proofs/STATUS.md`](proofs/STATUS.md) is **the single authoritative record**
+  of what is proved. If your change makes it inaccurate, update it in the same
+  PR.
+- Use its status vocabulary precisely: *machine-checked*, *locally-checked*,
+  *conformance-checked*, *proved-on-paper*, *statement-only*,
+  *definitions-only*, *absent*.
+- **No proof hole is ever described as proved.** A `statement-only` theorem is
+  an obligation, not a result.
+- The Coq trusted base carries no `Admitted`/`Axiom`; soundness results are
+  asserted axiom-free via `Print Assumptions` in CI. Keep it that way.
+
+## Documentation standards
+
+- Prose is `CC-BY-SA-4.0`; code is `MPL-2.0`. Every file carries **exactly
+  one** `SPDX-License-Identifier` on its first line.
+- Don't document unimplemented behaviour as if it ships. If you must describe
+  intended design, mark it explicitly as planned and record it in
+  [`DEBT.md`](DEBT.md).
+- Prefer fixing a stale claim to adding a new page.
+
+## Code of conduct
+
+Participation is governed by [`CODE_OF_CONDUCT.md`](CODE_OF_CONDUCT.md).
+
+## Licence
+
+By contributing you agree that your contributions are licensed under
+**MPL-2.0** (code) or **CC-BY-SA-4.0** (documentation), matching the file you
+are editing. See [`LICENSE`](LICENSE).