iter kernel-extension-mechanics.tidy: architect drift items — present-state + plugin-migration aftermath

Audit Step 3 fix path. Architect drift review at milestone close
surfaced 8 items (3 high, 4 medium, 1 low). Resolved 7 inline as
mechanical text rewrites + 2 source-rustdoc cleanups; the 1 low
(cycle-avoidance pattern documentation in design ledger) is
deferred — architect flagged it "Note, do not push" because the
pattern is implementation mechanism, not language semantics,
and is already documented in the load-bearing place
(`crates/ailang-kernel-stub/src/lib.rs //!`).

CLAUDE.md (2 sites):
  - Lead paragraph: "this file carries [...] in-tree skill system"
    → reframe to "this file carries [...] orchestrator discipline
    (the skill system itself lives in the ~/dev/skills/ plugin
    and is wired in via .claude/dev-cycle-profile.yml)".
  - Code-layout table: new row for `crates/ailang-kernel-stub/`
    documenting the zero-dep leaf design, the parse-hop location
    in `ailang-surface`, and the planned retirement at raw-buf
    landing.

design/INDEX.md (2 sites):
  - Project-ecosystem "Skills" bullet: in-tree `skills/` path +
    `skills/README.md` reference → `~/dev/skills/` plugin +
    in-tree per-project profile. Also added `docwriter` and
    `boss` to the enumerated skill list (8 in total) for
    completeness.
  - kernel-extensions row 111: added stub-retirement plan to the
    annotation so the spine names the future state, not just the
    in-tree reader of `lib.rs //!`.

design/models/0007-kernel-extensions.md (3 sites):
  - § "Migration policy" subsection: 4 bullets transitioned
    forward → present-state per honesty-rule. References to
    `loader.rs:98-108` / `workspace.rs:308-311, 467, 2655` as
    if hardcoded paths still existed → described as past state
    that has been replaced by the generic flag-filter. Codegen-
    intercept-migration bullet kept forward-looking because the
    `try_emit_primitive_instance_body` migration is *actually*
    still pending (deferred to Series milestone per spec
    § Out-of-scope).
  - § "Feature-acceptance argument": "the bounded push-only
    mutation surface — gated by the `Series` effect" — internal
    contradiction with three earlier statements that "Series
    carries no separate algebraic effect; mutation is mode-
    tracked, not effect-tracked". Re-framed to "gated by
    uniqueness mode-tracking on the owned `Series` value (not by
    an algebraic effect; see §"Coexistence" below)".
  - § "Coexistence" "Algebraic effects" bullet: "Reused
    unchanged. The `Series` effect is a new name" — same
    contradiction. Re-framed to "Not extended by Series.
    Mutation discipline lives in the uniqueness/mode system; the
    algebraic-effects set is unchanged".

Source rustdoc (2 sites):
  - `crates/ailang-core/tests/design_index_pin.rs:117` comment
    "skills/**/SKILL.md" → "any in-tree project-discipline
    document (e.g. CLAUDE.md)" — the allowlist comment now
    matches what the test actually does (no allowlist enforced
    in code; any existing path passes).
  - `crates/ailang-core/tests/design_schema_drift.rs:419`
    rustdoc: "RED until `skills/implement` mini-mode adds it"
    → "RED until the `implement` skill (mini-mode dispatch)
    adds it" — same skill, post-plugin-migration framing.

Architect items not addressed in this tidy:
  - 0007 § "The plugin contract (consolidated)" forward-intent
    reference to `try_emit_primitive_instance_body` migration —
    architect flagged as edge-case-acceptable per the explicit
    STATUS carve-out (the migration IS still pending). No
    change.
  - Cycle-avoidance pattern documentation (low): deferred per
    architect recommendation.

Tests green (664/0); workspace_pin module-count assertion picked
up from a844de3 carries through.

design/INDEX.md

@@ -46,12 +46,13 @@ evolving in lockstep with the language:
   `merge-prose`, etc., preferably with `--json` for machine consumption.
 - **Examples** (`examples/`): canonical `.ail.json` programs. They are
   specification anchors, not demos — the E2E suite hangs off them.
-- **Skills** (`skills/`): specialised disciplines
+- **Skills** (`~/dev/skills/` plugin, wired in via
+  `.claude/dev-cycle-profile.yml`): specialised disciplines
   (`brainstorm`, `planner`, `implement`, `audit`, `debug`,
-  `fieldtest`) plus the agent rosters they dispatch
-  (`skills/<name>/agents/`). They form the project's own
-  development methodology and are versioned with the codebase.
-  See `skills/README.md`.
+  `fieldtest`, `docwriter`, `boss`) plus the agent rosters
+  they dispatch. They form the project's development
+  methodology; the plugin is versioned separately, the
+  per-project profile is in-tree.
 - **Design ledger** (`design/`): `design/INDEX.md` (this file — the
   sole addressable spine for canonical state), `design/contracts/`
   (test-linked invariants), `design/models/` (onboarding
@@ -108,4 +109,4 @@ is the default.
 | authoring-surface | onboarding / evolves | design/models/0001-authoring-surface.md |
 | prose-projection  | onboarding / evolves | design/models/0006-prose-projection.md |
 | pipeline          | onboarding / evolves | design/models/0003-pipeline.md |
-| kernel-extensions | onboarding / evolves (mechanisms milestone closed 2026-05-28; raw-buf and series milestones pending) | design/models/0007-kernel-extensions.md |
+| kernel-extensions | onboarding / evolves (mechanisms milestone closed 2026-05-28; ratified end-to-end by the `ailang-kernel-stub` fixture, planned for retirement when raw-buf lands a real second consumer; raw-buf and series milestones pending) | design/models/0007-kernel-extensions.md |

design/models/0007-kernel-extensions.md

@@ -517,9 +517,11 @@ summary: LLM authors naturally reach for a bounded ring buffer
 for streaming workloads (clause 1 — the SMA worked example
 above is the evidence); the type structurally eliminates a class
 of off-by-one and warmup-handling bugs (clause 2); the bounded
-push-only mutation surface — gated by the `Series` effect — does
-not reintroduce the iterated-mutable-state bug class that the
-`mut`/`var`/`assign` removal addressed (clause 3 — see
+push-only mutation surface — gated by uniqueness mode-tracking
+on the owned `Series` value (not by an algebraic effect; see
+§"Coexistence" below) — does not reintroduce the iterated-
+mutable-state bug class that the `mut`/`var`/`assign` removal
+addressed (clause 3 — see
 `docs/specs/0052-kernel-extension-mechanics.md`'s clause-3
 discussion).
 
@@ -537,36 +539,41 @@ strictly better than an existing one for the use case it covers,
 the existing one is retired or repositioned, not preserved
 in parallel for compatibility.**
 
-Concrete consequences for the prep milestone:
+Concrete state after the mechanisms milestone closed (2026-05-28):
 
 - Type-scoped namespacing makes `<module>.<TypeOrFn>` non-canonical
-  for type-associated operations. Existing examples and fixtures
-  using `std_maybe.from_maybe`, `std_pair.from_pair`, etc., are
-  rewritten to type-scoped form. Hash pins are refreshed in
-  lockstep — each test crate (`crates/ailang-core/tests/hash_pin.rs`,
-  `crates/ailang-surface/tests/prelude_module_hash_pin.rs`, and
-  any other hash-pin file the prep recon enumerates) is walked,
-  per the "hash-pin blast-radius audit" practice.
+  for type-associated operations. The example and fixture corpus
+  has been rewritten from `std_maybe.from_maybe`,
+  `std_pair.from_pair`, etc., to type-scoped form. The hash-pin
+  blast-radius audit at prep.1 plan time enumerated the affected
+  pin files; only `crates/ailang-surface/tests/prelude_module_hash_pin.rs`
+  needed refresh in this milestone (at prep.3, when prelude
+  gained `(kernel)`).
 
-- The existing `BareCrossModuleTypeRef` /
+- The pre-existing `BareCrossModuleTypeRef` /
   `BadCrossModuleTypeRef` diagnostics are repurposed: what they
   considered "bad" before (a bare type ref to a foreign module's
-  type) becomes "bad" still, but the *correct* form is now
-  type-scoped (when feasible) rather than module-qualified.
+  type) is still bad when the type is not in scope, but the
+  *correct* form is now type-scoped (when feasible) rather than
+  module-qualified.
 
-- The prelude module gains `kernel: true`. The hardcoded
-  prelude-name paths in `crates/ailang-surface/src/loader.rs:98-108`
-  and `crates/ailang-core/src/workspace.rs:308-311, 467, 2655`
-  migrate to the generic flag-driven mechanism. Consumer-
-  observable behaviour for prelude is unchanged (the 12 free
-  fns remain callable bare); the code path no longer hardcodes
-  any module name as special.
+- The prelude module carries `kernel: true`. The previously
+  hardcoded prelude-name paths in `crates/ailang-surface/src/loader.rs`
+  (the `&["prelude"]` literal) and the matching reservation +
+  contract docs in `crates/ailang-core/src/workspace.rs` have
+  been replaced by a generic `modules.values().filter(|m| m.kernel)`
+  derivation. Consumer-observable behaviour for prelude is
+  unchanged (the 12 free fns remain callable bare in every
+  consumer — `crates/ail/tests/prelude_free_fns.rs` is the
+  regression pin); the code path no longer hardcodes any module
+  name as special.
 
-- Codegen intercepts: the existing `try_emit_primitive_instance_body`
-  hardcoded list is migrated into the plugin registry as part
-  of the Series milestone — when there is the first real
-  external consumer, the mechanism graduates from "hardcoded
-  for one case" to "registry for many cases".
+- Codegen intercepts: the pre-existing `try_emit_primitive_instance_body`
+  hardcoded list is **not yet** migrated into a plugin registry —
+  that migration is deferred to the Series milestone, when there
+  is the first real external consumer and the mechanism can
+  graduate from "hardcoded for one case" to "registry for many
+  cases". Single-consumer registries are premature mechanism.
 
 The reason migration cost is not a decision driver: there is
 nothing to break externally, and rewrites inside the workspace
@@ -589,10 +596,10 @@ here so the spec can quote the position:
   via the instance) and a `Series.dump` free-fn def (accessed
   via type-scope). Both mechanisms remain.
 
-- **Algebraic effects.** Reused unchanged. The `Series` effect
-  is a new name in the flat effect-set; the `(do effect/op
-  args)` syntax is the existing one (`io/print_str` is the
-  precedent).
+- **Algebraic effects.** Not extended by Series. Mutation
+  discipline lives in the uniqueness/mode system (see
+  `(own Series)` in caller signatures); the algebraic-effects
+  set is unchanged.
 
 - **RC + uniqueness.** Series values are RC-managed like any
   heap value; drop is via a kernel-supplied `@ailang_series_drop`.