diff --git a/proposals/MIGRATION-PLAN.adoc b/proposals/MIGRATION-PLAN.adoc index 5d204de..0bab98c 100644 --- a/proposals/MIGRATION-PLAN.adoc +++ b/proposals/MIGRATION-PLAN.adoc @@ -194,10 +194,41 @@ Heuristic: | C7 | DONE | Player cluster complete (2026-06-05): two scoped agents (5 verify + 3 float-re-decompose) + parent re-verification. *8 kernels* — CriticalRoll, PlayerAttributes, QCertifications, SkillRank, SkillAbilities, QPrograms, JessicaLoadout, JessicaBackground. *Four gates green (every gate re-run by parent):* 8/8 compile, *4348/4348 parity* (independent oracles), *6 echo-boundary LOSSLESS proofs* across 4 kernels (QCertifications, SkillRank, JessicaLoadout×3, JessicaBackground — agda re-typechecked by parent, exit 0); the other 4 transform/classifier kernels G3-n/a, 8/8 assail-clean. 3 kernels (CriticalRoll/PlayerAttributes/QPrograms) hit the Float→wasm wall (`min_float`/`max_float`/`trunc`) and were re-decomposed Int-native (milli-unit convention, floats host-side) per the C6 `*Int` pattern; parity caught + fixed an off-by-100 in PlayerAttributes. Evidence: `migrated/EVIDENCE-C7.adoc`. NEXT: C2 wave 2. | C2 wave 2a | DONE | Scalar multiply/divide (2026-06-05, Opus). `Mul`/`Div` turned out to be pure *scalar* value-transforms (not memory ops), so they need *no* array ABI — split out of "wave 2" and landed now. *1 kernel* `VmMulDiv` (11 exports) under `proposals/idaptik/migrated/`. Brain = the reversible ancilla multiply (`c := c + a*b`, inverse `c := c - a*b`) + the quotient/remainder divide whose dividend is reconstructable (`q*b + r == a` for all b incl. 0); the intentional-flaw in-place/simple variants migrated as value transforms with no rt==id claim. *Four gates green:* 1/1 compile, *3322/3322 parity* (incl. mul reversibility roundtrip + div reconstruction), G3 n/a (numeric transform), 1/1 assail-clean. *2 new i32 ABI facts:* (a) JS `a*b` loses precision >2^53 → oracle must use `Math.imul` to match `i32.mul`; (b) `i32.div_s` TRAPS on `b==0` and `INT_MIN/-1` (ReScript wraps the latter) → brain guards both (nested-`if`, avoiding the unverified `&&` codegen path) so the wasm is total. Evidence: `migrated/EVIDENCE-C2-wave2a.adoc`. NEXT: C2 wave 2b. | C2 wave 2b | DONE | Memory/stack/port/control opcodes (2026-06-05, Opus). *The "needs an array/linear-memory ABI" premise was WRONG and re-decomposition overturned it:* reading the sources, the VM's memory/stack/port buffers are not arrays in the brain — `VmState.res` stores every one as string-keyed dict slots (`_mem:N`, `_s:N`, `_pin:port`), i.e. host-side STATE (senses). The integer brains are all scalar. *4 kernels* `VmMemory` (LOAD/STORE), `VmStack` (PUSH/POP), `VmPort` (RECV/SEND), `VmControl` (IF_POS/IF_ZERO/LOOP) covering *9 opcodes*. *Four gates green:* 4/4 compile, *1568/1568 parity* (incl. load/store/sp/recv/send round-trips), G3 n/a (transforms/predicates), 4/4 assail-clean. No-kernel senses (classified, not migrated): Call (orchestration), CoprocessorCall (tombstone — never implemented), State/VmState/VM/SubroutineRegistry/VmStateCoprocessor/InstructionCoprocessor (state containers / bridges). Evidence: `migrated/EVIDENCE-C2-wave2b.adoc`. *No array ABI was required* (the blocker was a triage-bucket artefact). *Cluster C2 COMPLETE.* NEXT: C3. -| C3..C12 | TODO | Remaining MIGRATABLE-NOW clusters per `migration-map.json`: C3 (17), C5 (11), C9 (16), C10 (21), C11 (10), C12 (43). Established scalar/enum/predicate recipe. The unary-`~` codegen bug is a candidate Phase-F compiler fix; the string wall (52 non-test .res) + effect wall (110) remain the genuine compiler gates for the STRING-/EFFECT-GATED kernels. +| C3 | DONE | Coprocessor wiring layer (2026-06-05, Opus) — *classified, no new brains to extract.* C3's 17 `src/shared/` files are the host-side bridge layer that exposes C1's already-migrated wasm brains to the game engine. Verified de-dup (by constant, not name): the integer cores C3 needs (`compute_gate`/`data_limit_for_domain` 513/16/259/1024, `max_concurrent_compute` 10, `is_transient` 503/504/429, policy table, DeviceType/GameEvent ordinals) are *all* already migrated + 4-gate-verified in C1. The 12 `*Coprocessor.res` are pure-FFI passthrough (0 logic lines); `Kernel_Compute`/`RetryPolicy` (src/shared) are async/float wrappers over C1 brains; `DeviceType`/`GameEvent` add string-gated ops (string wall, Phase F). No 4-gate run (nothing new to verify). Bridges stay host-side as the essential wasm-loading glue (ADDITIVE, FeaturePacks-flagged); their ReScript→glue fate is a Phase-Ω cutover decision. Evidence: `migrated/EVIDENCE-C3.adoc`. NEXT: C5. +| C5..C12 | TODO | Remaining leaf-brain clusters per `migration-map.json`: *C5 (11, engine coprocessors — maths/random/navigation/resize/audio-state)* and *C11 (10, "pure integer presentation state" — font scaling/keyboard-nav/popup logic)* are the highest brain-yield; C9 (16, game-loop/AffineTEA/VeriSim types — mixed) and C10 (21, utils/tools/companions/narrative/proven — mixed); C12 (43, render-glue screens/PixiJS bindings — senses-heavy, migrated last). Established scalar/enum/predicate recipe. Genuine compiler gates remain: string wall (52 non-test .res), effect wall (110); unary-`~` codegen bug is a candidate Phase-F fix. | F+ | TODO | Compiler walls (string backend, then effects). | Ω | TODO (access-gated) | Cutover + ReScript extinction. |=== *Resume rule:* read the highest non-DONE row + `migration-map.json`; continue from its "Notes". + +[IMPORTANT] +==== +*Completion-drive directive (user-authorised 2026-06-05).* The owner authorised +driving the migratable corpus to completion *autonomously* — do NOT stop to +re-ask at each cluster boundary. Standing plan for the resuming agent: + +. Drive the MIGRATABLE-NOW clusters in this order, each via the full 4-gate + recipe, staged under `proposals/idaptik/migrated/`, one PR per cluster, + squash-merged when the gates are green (CI on this repo is non-gating; the + authoritative gates are the parity/assail/agda runs done locally): + *C5 → C11 → C9 → C10 → C12.* Classify senses/string-gated/effect-gated files + honestly (like C3) rather than forcing a migration. +. Then attack the two compiler walls *in this repo* (in scope): the string + backend, then effect codegen — each unblocks its STRING-/EFFECT-GATED kernels. +. Update this Ledger + `migration-map.json` after every cluster (repo-as-memory; + compaction-proof). + +*Git hygiene (learned 2026-06-05):* base each cluster's work on the *dev-branch +tip* (`origin/claude/cool-keller-gr5sl`), NOT on `origin/main`'s squash SHA — +the remote dev branch is force-push-protected, so basing on it keeps pushes +fast-forward and avoids the post-squash-merge divergence that nags the +commit-identity hook. Rebase onto `origin/main` only if main has advanced beyond +the staged content. + +*The one gate I cannot clear myself:* Phase Ω cutover (apply staged units to +idaptik + delete the `.res` shadows) needs idaptik *write-access*. Until the +owner opens that, "migrated" = "staged + 4-gate-verified", and true CLEAR +(ReScript→0) waits on access. Everything up to that line is drivable here. +==== diff --git a/proposals/idaptik/migrated/EVIDENCE-C3.adoc b/proposals/idaptik/migrated/EVIDENCE-C3.adoc new file mode 100644 index 0000000..52156af --- /dev/null +++ b/proposals/idaptik/migrated/EVIDENCE-C3.adoc @@ -0,0 +1,78 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += Cluster C3 (src/shared coprocessor wiring) — classification (captured 2026-06-05) +:toc: macro + +[IMPORTANT] +==== +*C3 is a wiring/senses cluster with NO new integer brains to extract.* Unlike a +leaf-kernel cluster, C3 is the coprocessor *bridge layer* — the host-side glue +that exposes the already-migrated C1 wasm brains to the game engine. Every +integer core C3 needs is already migrated and four-gate-verified in cluster C1. +There is therefore no 4-gate run for C3: there is nothing new to compile, +parity-test, or prove. This document records the file-by-file classification +that establishes that, with the cross-reference to C1's verified brains. The +de-dup was verified by comparing the actual constants, not just file names. +==== + +toc::[] + +== Why there are no new brains (verified, not assumed) + +`src/shared/` and `shared/src/` are two different directories. C1 migrated the +`shared/src/` integer cores; C3's `src/shared/` files carry the *same* integer +logic behind a game-facing senses surface. The cores were confirmed identical by +value: + +[cols="2,3,3",options="header"] +|=== +| Brain | `shared/src` (C1 source) | C1 staged kernel (verified) +| compute data limits | Vector/Neural/Audio→513, Maths/Physics→16, Tensor→259, _→1024 | `Kernel_Compute.data_limit_for_domain` — identical (513/16/259/1024) +| compute concurrency cap | `maxConcurrentCompute = 10` | `Kernel_Compute.max_concurrent_compute() = 10` +| compute preflight ladder | 504 (saturated) / 413 (payload) / 404 (no backend) | `Kernel_Compute.compute_gate(domain, active_calls, data_len, has_backend)` +| retry transient class | `status == 503 \|\| 504 \|\| 429` | `RetryPolicy.is_transient` — identical +| retry policy table | default/fast/patient (retries, baseMs, factor) | `RetryPolicy.policy_max_retries` / `policy_base_delay_ms` / `policy_backoff_factor_pct` +|=== + +C1 gates for these: `Kernel_Compute` 736/736 parity, `RetryPolicy` 124/124 +parity, both assail-clean (see `EVIDENCE.adoc`). C3 adds no integer logic on top. + +== File-by-file classification (17 files) + +[cols="3,2,3",options="header"] +|=== +| File | Class | Disposition +| `KernelCoprocessor.res` | FFI bridge | 0 logic lines; `@module external` to `KernelCoprocessorBridge.js` + thin wrappers. Loads `kernel.wasm` (C1's brain), exposes dispatch as Int. *Senses.* +| `CoprocessorComputeCoprocessor.res` | FFI bridge | 0 logic lines. Exposes the compute brain. *Senses.* +| `CoprocessorCoreCoprocessor.res` | FFI bridge | 0 logic lines. *Senses.* +| `CoprocessorIOCoprocessor.res` | FFI bridge | 0 logic lines. *Senses.* +| `CoprocessorSecurityCoprocessor.res` | FFI bridge | 0 logic lines. *Senses.* +| `DiagnosticsCoprocessor.res` | FFI bridge | 0 logic lines. Wraps C1 `Diagnostics`. *Senses.* +| `DLCLoaderCoprocessor.res` | FFI bridge | 0 logic lines. *Senses.* +| `InventoryCoprocessor.res` | FFI bridge | 0 logic lines. *Senses.* +| `PuzzleFormatCoprocessor.res` | FFI bridge | 0 logic lines. Wraps C1 `PuzzleFormat`. *Senses.* +| `ResourceAccountingCoprocessor.res` | FFI bridge | 0 logic lines. *Senses.* +| `RetryPolicyCoprocessor.res` | FFI bridge | 0 logic lines. Wraps C1 `RetryPolicy`. *Senses.* +| `UmsLevelLoaderCoprocessor.res` | FFI bridge | 0 logic lines. *Senses.* +| `Coprocessor_Backends.res` | registry | Backend-registration table; host-side dispatch state. *Senses.* +| `Kernel_Compute.res` | async wrapper | `promise` dispatch + string messages over the C1 `compute_gate` brain. Async/string = *senses*; brain already in C1. +| `RetryPolicy.res` | async/float wrapper | `setTimeout` + `Promise` + float backoff over the C1 `is_transient` + policy-table brain. Effect/float = *senses*; brain already in C1. +| `DeviceType.res` | types + string ops | Game-side device taxonomy (defenceFlags, deviceInfo); `portName`/`fromString` are string-gated. Ordinal encoding already in C1 `DeviceType` (39/39). *Senses / string-gated.* +| `GameEvent.res` | types + string ops | Cross-component event union; `toTag` is string serialisation (string-gated). `alertLevel` ordinal already in C1 `GameEvent`. *Senses / string-gated.* +|=== + +== Disposition + +* *Brain extraction:* COMPLETE for C3 — nothing to extract; the integer cores + live in C1's verified wasm. +* *The bridges stay host-side* as the essential wasm-loading glue (the + AffineScript→wasm FFI exemption). They are ADDITIVE by design (callable behind + a FeaturePacks flag; the pure-ReScript path remains until cutover). Their + eventual ReScript→(JS glue / thin .affine) fate is a *Phase Ω cutover* wiring + decision, not a brain migration. +* *String-gated remnants* (`DeviceType.portName`/`fromString`, `GameEvent.toTag`) + fall to the *string wall* (Phase F) like every other STRING-GATED surface. + +*Cluster C3 status: DONE (wiring layer — no new kernels).* NEXT high-yield +leaf-brain clusters: C5 (engine coprocessors — maths/random/navigation) and C11 +("pure integer presentation state"). diff --git a/proposals/idaptik/migration-map.json b/proposals/idaptik/migration-map.json index b0427d0..bf35a55 100644 --- a/proposals/idaptik/migration-map.json +++ b/proposals/idaptik/migration-map.json @@ -153,7 +153,16 @@ "id": "C3", "name": "src/shared coprocessor wiring", "description": "Coprocessor bridge layer in src/shared \u2014 wrappers exposing kernels to the game engine. Depends on C1.", - "status": "TODO", + "status": "DONE", + "done": { + "date": "2026-06-05", + "phase": "G", + "verdict": "NO_NEW_BRAINS \u2014 wiring/senses cluster", + "note": "All 17 files are host-side senses exposing C1's already-migrated wasm brains. 12 *Coprocessor.res are pure-FFI passthrough (0 logic lines). Kernel_Compute/RetryPolicy (src/shared) are async/float wrappers over C1 brains (compute_gate, is_transient + policy table). DeviceType/GameEvent add string-gated ops (string wall). De-dup verified by constant: compute limits 513/16/259/1024, concurrency 10, is_transient 503/504/429 all match C1 staged kernels exactly.", + "no_4gate": "nothing new to compile/parity/prove; the integer cores are C1-verified (Kernel_Compute 736/736, RetryPolicy 124/124)", + "bridges_disposition": "stay host-side as essential wasm-loading glue (ADDITIVE, FeaturePacks-flagged); ReScript->glue is a Phase-Omega cutover decision, not a brain migration", + "evidence": "proposals/idaptik/migrated/EVIDENCE-C3.adoc" + }, "files": [ "src/shared/CoprocessorComputeCoprocessor.res", "src/shared/CoprocessorCoreCoprocessor.res",