From 584af05057cf5cb614853230bdbd8c167827e3e3 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 5 Jun 2026 05:23:58 +0000 Subject: [PATCH 1/2] =?UTF-8?q?triage(phase-b):=20full-corpus=20migratabil?= =?UTF-8?q?ity=20sweep=20=E2=80=94=20migration-map.{json,adoc}?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Phase B of the ReScript -> AffineScript -> wasm migration: ran the affine-migratability tool over all 571 idaptik .res files and bucketed by area x verdict x shape into a resumable worklist. 571 files: 389 MIGRATABLE NOW (68%), 71 STRING-GATED (12%), 111 EFFECT-GATED. Non-test production: 358 files, 196 migratable (55%). Twelve clusters C1..C12 ordered leaf-pure-integer-first, + C_TESTS. Top walls: module-level ref() (79), string subscript (44), String.length (30). migration-map.json is the machine worklist (resume_rule + per-cluster file lists + per-file wall labels); migration-map.adoc is the human map. Also lands the two determinism latency-regime SVGs (game-vs-deepspace, state-vs-digest) referenced by multiplayer-determinism.adoc but not previously committed. https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --- proposals/idaptik/game-vs-deepspace.svg | 96 ++ proposals/idaptik/migration-map.adoc | 654 ++++++++ proposals/idaptik/migration-map.json | 1905 +++++++++++++++++++++++ proposals/idaptik/state-vs-digest.svg | 100 ++ 4 files changed, 2755 insertions(+) create mode 100644 proposals/idaptik/game-vs-deepspace.svg create mode 100644 proposals/idaptik/migration-map.adoc create mode 100644 proposals/idaptik/migration-map.json create mode 100644 proposals/idaptik/state-vs-digest.svg diff --git a/proposals/idaptik/game-vs-deepspace.svg b/proposals/idaptik/game-vs-deepspace.svg new file mode 100644 index 0000000..661f9a4 --- /dev/null +++ b/proposals/idaptik/game-vs-deepspace.svg @@ -0,0 +1,96 @@ + + + Same enemy ("did the data survive?"), opposite weapon + because LATENCY flips the economics: cheap round-trips reward sending LESS; ruinous round-trips force sending MORE + + + + IDApTIK — client ⇄ server + round-trips are CHEAP (~milliseconds) + + + CLIENT + live sim + predict + rollback + + + SERVER + live sim + authority + + + + + + ~ms + + + a1f3? → yes + same deterministic sim runs LIVE on both sides (lockstep) + + + STRATEGY: VERIFY, don't transfer + Send the smallest possible thing — a fingerprint. + Reconcile only on the rare mismatch. You can afford to + ask "do we agree?" because the answer is back in milliseconds. + + + Ground ⇄ relay ⇄ probe + round-trips are RUINOUS (seconds to many minutes of light-time) + + + Ground (ESOC) + digital twin + (offline) + + + Queqiao relay + Earth-Moon L2 (CNSA) + store + forward (DTN) + + + Probe + autonomous + SPARK/Ada + + + + + + + light-time delay: Moon ≈ 1.3 s one-way · Mars 3–22 min · no real-time loop possible + + + a message goes out PADDED with error-correcting redundancy: + + DATA + + + parity + + + parity + + + parity + + + STRATEGY: CORRECT, don't ask + Pile on redundancy so the receiver self-heals bit-errors with + NO resend (Reed-Solomon / Turbo / LDPC, CCSDS). Asking again + costs a whole round-trip (minutes–hours), so you never rely on it. + + + + The flip + GAME (cheap round-trips) + • send LESS — a fingerprint + • ask "do we agree?", reconcile on mismatch + • two LIVE sims in lockstep; check is a hash + • enemy = DESYNC between two simulations + + DEEP SPACE (ruinous round-trips) + • send MORE — data + heavy parity (FEC) + • never ask; receiver self-corrects on arrival + • probe autonomous; ground twin checks telemetry later + • enemy = BIT-ERRORS on a one-way, noisy channel + + echo-types (a PROOF data is recoverable) is the static cousin of deep-space CHANNEL CODING (a coding-theory GUARANTEE errors are correctable) — same goal, different layer + diff --git a/proposals/idaptik/migration-map.adoc b/proposals/idaptik/migration-map.adoc new file mode 100644 index 0000000..bb5d4c7 --- /dev/null +++ b/proposals/idaptik/migration-map.adoc @@ -0,0 +1,654 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += IDApTIK migration map — ReScript → AffineScript corpus triage +:toc: macro + +[IMPORTANT] +==== +*Machine-generated from `affine-migratability` on 2026-06-05.* +Companion: `migration-map.json` (the resumable worklist). +Resume rule: read highest non-DONE cluster in the JSON; apply the 4-gate recipe (§recipe below). +==== + +toc::[] + +== Headline numbers + +Total `.res` files scanned: *571* + +[cols="2,1,1",options="header"] +|=== +| Verdict | Count | % +| *MIGRATABLE NOW* | 389 | 68% +| STRING-GATED (wall 1) | 71 | 12% +| EFFECT-GATED (wall 2) | 111 | 19% +|=== + +*Excluding test harnesses* (213 `__tests__/*.res` files; these become parity harnesses, not direct migrations): + +[cols="2,1,1",options="header"] +|=== +| Verdict | Count | % +| *MIGRATABLE NOW* | 196 | 55% +| STRING-GATED | 52 | 15% +| EFFECT-GATED | 110 | 31% +|=== + +== The two compiler walls + +=== Wall 1 — variable-string backend (STRING-GATED) + +*71 files* blocked. Unblocked by Phase F compiler work. + +Top patterns: +* string subscript (44 files) +* String.length (30 files) +* String.startsWith (13 files) +* String.slice (7 files) +* String.fromCharCode (4 files) + +Key finding: `string subscript` (`s[i]` / `path[0]`) is the single largest pattern (44 files), +mostly in device/enemy/companion code that slices string identifiers. `String.length` (30 files) +is the second — mostly for path/name length checks. Both collapse once the variable-string +ABI (`[len:i32 LE][utf8]` read-side) lands. + +=== Wall 2 — effect codegen (EFFECT-GATED) + +*111 files* blocked. Unblocked by Phase F+ effect-codegen work. + +Top patterns: +* module-level ref() (79 files) +* Console.log (24 files) +* module-level Dict.make() (20 files) +* Date.now (8 files) +* Math.random (6 files) + +Key finding: module-level `ref()` (79 files) is the dominant wall — these are stateful service +singletons (`GlobalNetworkManager`, `FeaturePacks`, `GameI18n`, etc.) that use +`let state = ref(...)` at module scope. The re-decomposition strategy threads this state +as explicit parameters. `Console.log` (24 files, mostly vm tests) is trivially fixed by routing +to an I/O port. `Date.now` / `Math.random` must be fed as explicit inputs to the wasm brain. + +== Area breakdown + +[cols="2,1,1,1,1",options="header"] +|=== +| Area | Total | MIG NOW | STR-GATED | EFF-GATED +| `shared/src` | 21 | 11 | 5 | 5 +| `src/shared` | 34 | 17 | 8 | 9 +| `vm` | 51 | 31 | 3 | 17 +| `src/app/multiplayer` | 13 | 6 | 2 | 5 +| `src/engine` | 15 | 11 | 1 | 3 +| `src/app/combat` | 6 | 4 | 0 | 2 +| `src/app/enemies` | 12 | 6 | 4 | 2 +| `src/app/player` | 22 | 11 | 0 | 11 +| `src/app/devices` | 37 | 11 | 8 | 18 +| `src/app/proven` | 5 | 3 | 1 | 1 +| `src/app/utils` | 19 | 11 | 1 | 7 +| `src/app/companions` | 8 | 5 | 2 | 1 +| `src/app/narrative` | 3 | 1 | 1 | 1 +| `src/app/ui` | 14 | 10 | 2 | 2 +| `src/app/popups` | 13 | 6 | 2 | 5 +| `src/app/screens` | 52 | 27 | 6 | 19 +| `src/app` | 18 | 16 | 0 | 2 +| `src/bindings` | 4 | 4 | 0 | 0 +| `src/app/tools` | 4 | 2 | 2 | 0 +| `src/app/pickups` | 2 | 1 | 1 | 0 +| `idaptik-ums` | 3 | 0 | 3 | 0 +| `__tests__` | 213 | 193 | 19 | 1 +| `src/other` | 1 | 1 | 0 | 0 +|=== + +== The 4-gate recipe (every kernel, every wave) + +[[recipe]] + +[arabic] +. *Re-decompose* — NOT transliterate: collapse incidental Promise/async, thread service-locator state as params, enum the options, hand-ladder int rendering, keep wire bytes identical. +. *`affinescript compile` → wasm* — gate 1: builds. +. *`affine-parity` oracle-vs-wasm sweep green* — gate 2: parity. +. *`echo-boundary` proves each host-boundary encoding LOSSLESS or declared-clamp* — gate 3: faithful. +. *`affine-assail` clean* — no undeclared clamp / unguarded decoder — gate 4. + +Each migrated kernel is staged under `proposals/idaptik/migrated//` with `.affine` + harness + evidence. + +== MIGRATABLE NOW clusters (priority order) + +These clusters are the deep-wave work (Phases C, D, G..N). +Ordered: leaf pure-integer cores first, up the dependency tree. + +=== C1 — Pure-integer kernel definitions (11 files) + +Leaf kernel types and coprocessor backends in shared/src. No string ops, no effects. First — no dependencies on other migrated files. + +*Status:* TODO + +[source] +---- +shared/src/Coprocessor_Backends.res +shared/src/DLCLoader.res +shared/src/DeviceType.res +shared/src/Diagnostics.res +shared/src/GameEvent.res +shared/src/Kernel.res +shared/src/Kernel_Compute.res +shared/src/PortNames.res +shared/src/PortNamesCoprocessor.res +shared/src/PuzzleFormat.res +shared/src/RetryPolicy.res +---- + +=== C2 — VM instruction set (31 files) + +VM instruction modules in vm/lib/ocaml — one file per opcode, pure-integer reversible VM. Also the wasm binding shim. + +*Status:* TODO + +[source] +---- +vm/lib/ocaml/Add.res +vm/lib/ocaml/And.res +vm/lib/ocaml/Call.res +vm/lib/ocaml/CoprocessorCall.res +vm/lib/ocaml/Div.res +vm/lib/ocaml/Flip.res +vm/lib/ocaml/IfPos.res +vm/lib/ocaml/IfZero.res +vm/lib/ocaml/Instruction.res +vm/lib/ocaml/InstructionCoprocessor.res +vm/lib/ocaml/Load.res +vm/lib/ocaml/Loop.res +vm/lib/ocaml/Mul.res +vm/lib/ocaml/Negate.res +vm/lib/ocaml/Noop.res +vm/lib/ocaml/Or.res +vm/lib/ocaml/Pop.res +vm/lib/ocaml/Push.res +vm/lib/ocaml/Recv.res +vm/lib/ocaml/Rol.res +vm/lib/ocaml/Ror.res +vm/lib/ocaml/Send.res +vm/lib/ocaml/State.res +vm/lib/ocaml/Store.res +vm/lib/ocaml/Sub.res +vm/lib/ocaml/SubroutineRegistry.res +vm/lib/ocaml/Swap.res +vm/lib/ocaml/VM.res +vm/lib/ocaml/VmStateCoprocessor.res +vm/lib/ocaml/Xor.res +vm/wasm/src/bindings.res +---- + +=== C3 — src/shared coprocessor wiring (17 files) + +Coprocessor bridge layer in src/shared — wrappers exposing kernels to the game engine. Depends on C1. + +*Status:* TODO + +[source] +---- +src/shared/CoprocessorComputeCoprocessor.res +src/shared/CoprocessorCoreCoprocessor.res +src/shared/CoprocessorIOCoprocessor.res +src/shared/CoprocessorSecurityCoprocessor.res +src/shared/Coprocessor_Backends.res +src/shared/DLCLoaderCoprocessor.res +src/shared/DeviceType.res +src/shared/DiagnosticsCoprocessor.res +src/shared/GameEvent.res +src/shared/InventoryCoprocessor.res +src/shared/KernelCoprocessor.res +src/shared/Kernel_Compute.res +src/shared/PuzzleFormatCoprocessor.res +src/shared/ResourceAccountingCoprocessor.res +src/shared/RetryPolicy.res +src/shared/RetryPolicyCoprocessor.res +src/shared/UmsLevelLoaderCoprocessor.res +---- + +=== C4 — Multiplayer coprocessors (6 files) + +Server-authoritative multiplayer in src/app/multiplayer — the coprocessors that run identically in browser and on the Elixir server via wasmex/SNIFS. + +*Status:* TODO + +[source] +---- +src/app/multiplayer/BurbleAdapter.res +src/app/multiplayer/LobbyManager.res +src/app/multiplayer/LobbyManagerCoprocessor.res +src/app/multiplayer/MultiplayerClientCoprocessor.res +src/app/multiplayer/VMNetworkCoprocessor.res +src/app/multiplayer/VoiceBridge.res +---- + +=== C5 — Engine coprocessors (11 files) + +Core engine coprocessors: audio state, navigation, resize, maths, random, storage. + +*Status:* TODO + +[source] +---- +src/engine/audio/Audio.res +src/engine/navigation/Navigation.res +src/engine/resize/Resize.res +src/engine/resize/ResizeCoprocessor.res +src/engine/utils/GetResolution.res +src/engine/utils/GetResolutionCoprocessor.res +src/engine/utils/Maths.res +src/engine/utils/MathsCoprocessor.res +src/engine/utils/RandomCoprocessor.res +src/engine/utils/StorageCoprocessor.res +src/engine/utils/WaitFor.res +---- + +=== C6 — Combat and enemy AI coprocessors (9 files) + +Game simulation: hitbox geometry, HP, difficulty scaling, detection, distraction — pure integer state machines. + +*Status:* TODO + +[source] +---- +src/app/combat/CombatFxLogicCoprocessor.res +src/app/combat/Hitbox.res +src/app/combat/HitboxGeomCoprocessor.res +src/app/combat/PlayerHPCoprocessor.res +src/app/enemies/DetectionSystemCoprocessor.res +src/app/enemies/DifficultyScaleCoprocessor.res +src/app/enemies/DistractionCoprocessor.res +src/app/enemies/DualAlertBridge.res +src/app/enemies/SecurityAICoprocessor.res +---- + +=== C7 — Player coprocessors (10 files) + +Player attribute, loadout, skill and ability coprocessors — pure integer player state. + +*Status:* TODO + +[source] +---- +src/app/player/CriticalRollCoprocessor.res +src/app/player/JessicaBackgroundCoprocessor.res +src/app/player/JessicaLoadoutCoprocessor.res +src/app/player/Player.res +src/app/player/PlayerAttributesCoprocessor.res +src/app/player/QCertifications.res +src/app/player/QCertificationsCoprocessor.res +src/app/player/QProgramsCoprocessor.res +src/app/player/SkillAbilitiesCoprocessor.res +src/app/player/SkillRankCoprocessor.res +---- + +=== C8 — Device and network coprocessors (10 files) + +Device state machine coprocessors: power, network transfer, security rank, covert link. + +*Status:* TODO + +[source] +---- +src/app/devices/CovertLinkCoprocessor.res +src/app/devices/DeviceFactory.res +src/app/devices/GlobalNetworkDataCoprocessor.res +src/app/devices/LaptopStateCoprocessor.res +src/app/devices/NetworkManagerCoprocessor.res +src/app/devices/NetworkTransferCoprocessor.res +src/app/devices/PowerManagerCoprocessor.res +src/app/devices/PowerStationDevice.res +src/app/devices/SecurityRankCoprocessor.res +src/app/devices/types/DeviceTypes.res +---- + +=== C9 — Game loop, AffineTEA, and VeriSim types (16 files) + +Top-level game loop, AffineTEA architecture, VeriSim integration types, and the entry point. + +*Status:* TODO + +[source] +---- +src/Main.res +src/app/GameLoop.res +src/app/burble/BurbleIntegration.res +src/app/pixi/PixiCoprocessor.res +src/app/tea/AffineTEA.res +src/app/tea/AffineTEARouter.res +src/app/verisimdb/SaveGame.res +src/app/verisimdb/VeriSimDrift.res +src/app/verisimdb/VeriSimError.res +src/app/verisimdb/VeriSimFederation.res +src/app/verisimdb/VeriSimHexad.res +src/app/verisimdb/VeriSimProvenance.res +src/app/verisimdb/VeriSimSearch.res +src/app/verisimdb/VeriSimTypes.res +src/app/verisimdb/VeriSimVcl.res +src/app/vm/VmCoprocessor.res +---- + +=== C10 — Utils, tools, companions, narrative, and proven modules (21 files) + +Game utilities, tools coprocessors, Moletaire companion, mission briefing, and formal-proof integration. + +*Status:* TODO + +[source] +---- +src/app/companions/MoletaireCoprocessorsCoprocessor.res +src/app/companions/MoletaireHunger.res +src/app/companions/MoletaireHungerCoprocessor.res +src/app/companions/MoletairePersistence.res +src/app/narrative/MissionBriefingCoprocessor.res +src/app/proven/ProvenError.res +src/app/proven/SafeAngle.res +src/app/proven/SafeFloatCoprocessor.res +src/app/tools/PasswordCrackerCoprocessor.res +src/app/tools/PortScannerCoprocessor.res +src/app/utils/Announcer.res +src/app/utils/ColorPalette.res +src/app/utils/ColorPaletteCoprocessor.res +src/app/utils/DomA11y.res +src/app/utils/FontScaleCoprocessor.res +src/app/utils/GameI18nCoprocessor.res +src/app/utils/KeyboardNav.res +src/app/utils/Locales.res +src/app/utils/PanicHandler.res +src/app/utils/PolyglotI18n.res +src/app/utils/UserSettings.res +---- + +=== C11 — UI and accessibility coprocessors (10 files) + +UI widget logic, font scaling, i18n, keyboard navigation, popup logic — pure integer presentation state. + +*Status:* TODO + +[source] +---- +src/app/popups/ForceLayoutCoprocessor.res +src/app/ui/Button.res +src/app/ui/DualAlert.res +src/app/ui/DualAlertCoprocessor.res +src/app/ui/HardwareWiring.res +src/app/ui/HubButton.res +src/app/ui/InventoryUI.res +src/app/ui/Label.res +src/app/ui/NavButton.res +src/app/ui/VolumeSlider.res +---- + +=== C12 — Render-glue screens, UI, and bindings (43 files) + +Screen implementations, render-logic coprocessors, and PixiJS bindings. Migrated last — these call the AffineScript brain from the host JS/Pixi layer. + +*Status:* TODO + +[source] +---- +src/app/companions/CompanionsRenderLogicCoprocessor.res +src/app/devices/DevicesRenderLogicCoprocessor.res +src/app/enemies/EnemiesRenderLogicCoprocessor.res +src/app/pickups/ToolsPickupsRenderLogicCoprocessor.res +src/app/player/PlayerRenderLogicCoprocessor.res +src/app/popups/FeaturePacksPopup.res +src/app/popups/IntegrationsPopup.res +src/app/popups/LanguagePopup.res +src/app/popups/NarrativePopupsRenderLogicCoprocessor.res +src/app/popups/PausePopup.res +src/app/screens/BalanceAnalyserCoprocessor.res +src/app/screens/CreditsScreen.res +src/app/screens/JessicaCustomiseScreen.res +src/app/screens/LoadScreen.res +src/app/screens/LoadoutScreen.res +src/app/screens/LocationDataCoprocessor.res +src/app/screens/ObserverScreen.res +src/app/screens/QViewScreen.res +src/app/screens/ScreenGlitchFxCoprocessor.res +src/app/screens/ScreensRunLoopLogicCoprocessor.res +src/app/screens/SkillTreeScreen.res +src/app/screens/TitleScreen.res +src/app/screens/locations/AtlasScreen.res +src/app/screens/locations/BackboneScreen.res +src/app/screens/locations/BusinessISPScreen.res +src/app/screens/locations/CityScreen.res +src/app/screens/locations/DevHubScreen.res +src/app/screens/locations/FieldScreen.res +src/app/screens/locations/LabScreen.res +src/app/screens/locations/LocationBase.res +src/app/screens/locations/NexusScreen.res +src/app/screens/locations/RegionalISPScreen.res +src/app/screens/locations/RuralISPScreen.res +src/app/screens/main/Bouncer.res +src/app/screens/main/Logo.res +src/app/screens/main/MainScreen.res +src/app/screens/training/TrainingMenuScreen.res +src/app/ui/UiRenderLogicCoprocessor.res +src/app/verisimdb/VerisimProvenRenderLogicCoprocessor.res +src/bindings/Motion.res +src/bindings/Pixi.res +src/bindings/PixiSound.res +src/bindings/PixiUI.res +---- + +=== C_TESTS — Test harnesses (193 files) + +The `__tests__/*.res` test harnesses are a separate track. When a coprocessor kernel migrates, +its test harness becomes an *affine-parity* harness (gate 2 of the recipe) — the ReScript oracle +runs the original `.res.mjs` and the new `.wasm` must match output on all inputs. +These are NOT direct `.res → .affine` migrations. + +== Compiler-gated files (not effort-gated) + +=== STRING-GATED (71 files) + +These files are blocked on Wall 1 (variable-string backend). When Phase F lands `String.length` ++ indexing end-to-end, these unblock. Key files in each area: + +*`idaptik-ums`* (3 files): + `App.res` — string subscript + `EditorLevelCmd.res` — string subscript + `test_round_trip.res` — string subscript + +*`shared/src`* (5 files): + `Coprocessor_Compute.res` — string subscript + `Coprocessor_IO.res` — String.fromCharCode; String.length + `Coprocessor_Security.res` — string subscript + `Inventory.res` — string subscript + `Kernel_IO.res` — String.fromCharCode; String.length + +*`src/app/companions`* (2 files): + `Moletaire.res` — string subscript + `MoletaireMusic.res` — string subscript + +*`src/app/devices`* (8 files): + `CoprocessorBridge.res` — String.length; String.indexOf + `DeviceView.res` — string subscript; String.endsWith + `FirewallDevice.res` — String.indexOf; String.slice + `GlobalNetworkData.res` — String.length; string subscript + `LaptopGUI.res` — String.endsWith; String.startsWith + `NetworkZones.res` — String.startsWith + _...and 2 more_ + +*`src/app/enemies`* (4 files): + `Drone.res` — string subscript + `GuardNPC.res` — string subscript + `SecurityAI.res` — string subscript + `SecurityDog.res` — string subscript + +*`src/app/multiplayer`* (2 files): + `VMMessageBus.res` — String.startsWith + `VMNetwork.res` — String.startsWith; string subscript + +*`src/app/narrative`* (1 files): + `DataFiles.res` — string subscript + +*`src/app/pickups`* (1 files): + `WorldPickup.res` — String.slice + +*`src/app/popups`* (2 files): + `FeedbackPopup.res` — String.length; String.slice + `NetworkDesktop.res` — String.startsWith; string subscript + +*`src/app/proven`* (1 files): + `SafeJson.res` — String.slice; String.length + +*`src/app/screens`* (6 files): + `CharacterSelectScreen.res` — String.length; String.slice + `IntroScreen.res` — string subscript + `WorldMapScreen.res` — string subscript + `CombatTraining.res` — string subscript + `HighwayCrossingTraining.res` — string subscript + `MoletaireTraining.res` — string subscript + +*`src/app/tools`* (2 files): + `PasswordCracker.res` — String.length; String.charCodeAt + `PortScanner.res` — string subscript + +*`src/app/ui`* (2 files): + `HUD.res` — string subscript + `KernelMonitor.res` — String.length + +*`src/app/utils`* (1 files): + `DesktopIntegration.res` — string subscript + +*`src/engine`* (1 files): + `Random.res` — string subscript; String.length + +*`src/shared`* (8 files): + `Coprocessor_Compute.res` — string subscript + `Coprocessor_IO.res` — String.fromCharCode; String.length + `Coprocessor_Security.res` — string subscript + `DLCLoader.res` — String.length + `GossamerFs.res` — string subscript + `Inventory.res` — string subscript + _...and 2 more_ + +*`vm`* (3 files): + `InstructionParser.res` — String.length; string subscript + `StateDiff.res` — String.length + `VmState.res` — String.startsWith + +*`__tests__`* (19 files): + `CreditsScreen_test.res` — string subscript + `DataFiles_test.res` — String.length + `DualAlert_test.res` — string subscript + `FeedbackPopup_test.res` — string subscript + `ForceLayout_test.res` — string subscript + `GameOverScreen_test.res` — String.length + _...and 13 more_ + +=== EFFECT-GATED (111 files) + +These files are blocked on Wall 2 (effect codegen). Dominant pattern: module-level `ref()` — +re-decomposition strategy is to thread the mutable state as an explicit parameter to the wasm +function (the ref becomes an `&mut` or affine owned value). Key files: + +*`shared/src`* (5 files): + `Coprocessor.res` — module-level mutable state (Dict.make()); Console.log + `CoprocessorManager.res` — Console.log + `Kernel_Crypto.res` — module-level mutable state (Dict.make()) + `Kernel_Quantum.res` — module-level mutable state (Dict.make()); Console.log + `ResourceAccounting.res` — module-level mutable state (Dict.make()) + +*`src/app`* (2 files): + `GetEngine.res` — module-level mutable state (ref(...)) + `VeriSimClient.res` — module-level mutable state (Dict.make()) + +*`src/app/combat`* (2 files): + `Combat.res` — module-level mutable state (ref(...)) + `PlayerHP.res` — module-level mutable state (ref(...)) + +*`src/app/companions`* (1 files): + `MoletaireCoprocessors.res` — module-level mutable state (ref(...)) + +*`src/app/devices`* (18 files): + `CameraDevice.res` — module-level mutable state (Dict.make()) + `CameraFeed.res` — module-level mutable state (ref(...)); module-level mutable state (Dict.make()) + `CovertLink.res` — module-level mutable state (ref(...)) + `DesktopDevice.res` — module-level mutable state (ref(...)) + `DeviceActivity.res` — Date.now; module-level mutable state (Dict.make()) + _...and 13 more_ + +*`src/app/enemies`* (2 files): + `DetectionSystem.res` — module-level mutable state (ref(...)) + `Distraction.res` — module-level mutable state (ref(...)) + +*`src/app/multiplayer`* (5 files): + `LobbyRegistry.res` — module-level mutable state (ref(...)) + `MultiplayerClient.res` — Date.now + `MultiplayerGlobal.res` — module-level mutable state (ref(...)) + `MultiplayerScreenWiring.res` — module-level mutable state (ref(...)) + `PhoenixSocket.res` — module-level mutable state (Dict.make()) + +*`src/app/narrative`* (1 files): + `MissionBriefing.res` — module-level mutable state (ref(...)) + +*`src/app/player`* (11 files): + `CriticalRoll.res` — module-level mutable state (ref(...)); Math.random + `JessicaBackground.res` — module-level mutable state (ref(...)) + `JessicaLoadout.res` — module-level mutable state (ref(...)) + `KeyboardAiming.res` — module-level mutable state (ref(...)) + `PlayerAttributes.res` — module-level mutable state (ref(...)) + _...and 6 more_ + +*`src/app/popups`* (5 files): + `AccessibilityPopup.res` — module-level mutable state (ref(...)) + `ForceLayout.res` — module-level mutable state (ref(...)) + `PopupConstructors.res` — module-level mutable state (ref(...)) + `PowerView.res` — module-level mutable state (ref(...)) + `SettingsPopup.res` — module-level mutable state (ref(...)) + +*`src/app/proven`* (1 files): + `SafeFloat.res` — module-level mutable state (ref(...)) + +*`src/app/screens`* (19 files): + `BalanceAnalyserModel.res` — module-level mutable state (ref(...)) + `GameOverScreen.res` — module-level mutable state (ref(...)); Math.random + `LevelConfig.res` — module-level mutable state (ref(...)) + `LobbyScreen.res` — module-level mutable state (ref(...)); Date.now + `LocationData.res` — module-level mutable state (ref(...)) + _...and 14 more_ + +*`src/app/ui`* (2 files): + `ParticleField.res` — module-level mutable state (ref(...)); Math.random + `RoundedBox.res` — module-level mutable state (ref(...)) + +*`src/app/utils`* (7 files): + `AccessibilitySettings.res` — module-level mutable state (ref(...)) + `FeaturePacks.res` — module-level mutable state (ref(...)) + `FeedbackIntegration.res` — module-level mutable state (ref(...)); Date.now + `FontScale.res` — module-level mutable state (ref(...)) + `GameI18n.res` — module-level mutable state (ref(...)) + _...and 2 more_ + +*`src/engine`* (3 files): + `Engine.res` — module-level mutable state (ref(...)) + `VmBackend.res` — module-level mutable state (ref(...)); Console.log + `Storage.res` — module-level mutable state (ref(...)) + +*`src/shared`* (9 files): + `Coprocessor.res` — module-level mutable state (Dict.make()); Console.log + `CoprocessorManager.res` — Console.log + `Diagnostics.res` — module-level mutable state (ref(...)) + `Kernel.res` — module-level mutable state (ref(...)) + `Kernel_Crypto.res` — module-level mutable state (Dict.make()) + _...and 4 more_ + +*`vm`* (17 files): + `add_test.res` — Console.log + `and_or_test.res` — Console.log + `benchmark.res` — Console.log + `call_test.res` — Console.log + `flip_test.res` — Console.log + _...and 12 more_ + +*`__tests__`* (1 files): + `TestRunner.res` — Console.log + +== Provenance + +Generated 2026-06-05 by running `affine-migratability` over 571 `.res` source files +in `hyperpolymath/idaptik` (excluding compiled output in `lib/js/`, `lib/es6/`). +Part of the ReScript→AffineScript migration campaign; companion: `MIGRATION-PLAN.adoc`. diff --git a/proposals/idaptik/migration-map.json b/proposals/idaptik/migration-map.json new file mode 100644 index 0000000..3476b5a --- /dev/null +++ b/proposals/idaptik/migration-map.json @@ -0,0 +1,1905 @@ +{ + "schema": "migration-map/1.0", + "triage_date": "2026-06-05", + "tool": "affine-migratability", + "resume_rule": "Read highest non-DONE cluster. Apply 4-gate recipe (re-decompose \u2192 compile\u2192wasm \u2192 affine-parity green \u2192 echo-boundary LOSSLESS \u2192 affine-assail clean). Update status to DONE.", + "corpus": { + "total": 571, + "migratable_now": 389, + "string_gated": 71, + "effect_gated": 111, + "migratable_pct": 68 + }, + "corpus_non_test": { + "total": 358, + "migratable_now": 196, + "string_gated": 52, + "effect_gated": 110, + "migratable_pct": 55 + }, + "walls": { + "string": { + "count": 71, + "unblocked_by": "Phase F string backend: String.length + indexing + startsWith/endsWith/slice/fromCharCode", + "top_patterns": [ + "string subscript (44 files)", + "String.length (30 files)", + "String.startsWith (13 files)", + "String.slice (7 files)", + "String.fromCharCode (4 files)" + ] + }, + "effect": { + "count": 111, + "unblocked_by": "Phase F+ effect codegen: module-level mutable state, Date.now, Console.log", + "top_patterns": [ + "module-level ref() (79 files)", + "Console.log (24 files)", + "module-level Dict.make() (20 files)", + "Date.now (8 files)", + "Math.random (6 files)" + ] + } + }, + "clusters": [ + { + "id": "C1", + "name": "Pure-integer kernel definitions", + "description": "Leaf kernel types and coprocessor backends in shared/src. No string ops, no effects. First \u2014 no dependencies on other migrated files.", + "status": "DONE", + "done": { + "date": "2026-06-05", + "phase": "C", + "staged_at": "proposals/idaptik/migrated/", + "kernels": [ + "DeviceType", "PuzzleFormat", "PortNames", "GameEvent", + "Kernel_Compute", "Kernel", "RetryPolicy", "Diagnostics" + ], + "host_side_no_brain": [ + "Coprocessor_Backends.res", "PortNamesCoprocessor.res", "DLCLoader.res" + ], + "gates": "8/8 compile; 1223/1223 parity; 6 echo-boundary proofs (agda exit 0); 8/8 assail-clean", + "evidence": "proposals/idaptik/migrated/EVIDENCE.adoc" + }, + "files": [ + "shared/src/Coprocessor_Backends.res", + "shared/src/DLCLoader.res", + "shared/src/DeviceType.res", + "shared/src/Diagnostics.res", + "shared/src/GameEvent.res", + "shared/src/Kernel.res", + "shared/src/Kernel_Compute.res", + "shared/src/PortNames.res", + "shared/src/PortNamesCoprocessor.res", + "shared/src/PuzzleFormat.res", + "shared/src/RetryPolicy.res" + ], + "count": 11 + }, + { + "id": "C2", + "name": "VM instruction set", + "description": "VM instruction modules in vm/lib/ocaml \u2014 one file per opcode, pure-integer reversible VM. Also the wasm binding shim.", + "status": "TODO", + "files": [ + "vm/lib/ocaml/Add.res", + "vm/lib/ocaml/And.res", + "vm/lib/ocaml/Call.res", + "vm/lib/ocaml/CoprocessorCall.res", + "vm/lib/ocaml/Div.res", + "vm/lib/ocaml/Flip.res", + "vm/lib/ocaml/IfPos.res", + "vm/lib/ocaml/IfZero.res", + "vm/lib/ocaml/Instruction.res", + "vm/lib/ocaml/InstructionCoprocessor.res", + "vm/lib/ocaml/Load.res", + "vm/lib/ocaml/Loop.res", + "vm/lib/ocaml/Mul.res", + "vm/lib/ocaml/Negate.res", + "vm/lib/ocaml/Noop.res", + "vm/lib/ocaml/Or.res", + "vm/lib/ocaml/Pop.res", + "vm/lib/ocaml/Push.res", + "vm/lib/ocaml/Recv.res", + "vm/lib/ocaml/Rol.res", + "vm/lib/ocaml/Ror.res", + "vm/lib/ocaml/Send.res", + "vm/lib/ocaml/State.res", + "vm/lib/ocaml/Store.res", + "vm/lib/ocaml/Sub.res", + "vm/lib/ocaml/SubroutineRegistry.res", + "vm/lib/ocaml/Swap.res", + "vm/lib/ocaml/VM.res", + "vm/lib/ocaml/VmStateCoprocessor.res", + "vm/lib/ocaml/Xor.res", + "vm/wasm/src/bindings.res" + ], + "count": 31 + }, + { + "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", + "files": [ + "src/shared/CoprocessorComputeCoprocessor.res", + "src/shared/CoprocessorCoreCoprocessor.res", + "src/shared/CoprocessorIOCoprocessor.res", + "src/shared/CoprocessorSecurityCoprocessor.res", + "src/shared/Coprocessor_Backends.res", + "src/shared/DLCLoaderCoprocessor.res", + "src/shared/DeviceType.res", + "src/shared/DiagnosticsCoprocessor.res", + "src/shared/GameEvent.res", + "src/shared/InventoryCoprocessor.res", + "src/shared/KernelCoprocessor.res", + "src/shared/Kernel_Compute.res", + "src/shared/PuzzleFormatCoprocessor.res", + "src/shared/ResourceAccountingCoprocessor.res", + "src/shared/RetryPolicy.res", + "src/shared/RetryPolicyCoprocessor.res", + "src/shared/UmsLevelLoaderCoprocessor.res" + ], + "count": 17 + }, + { + "id": "C4", + "name": "Multiplayer coprocessors", + "description": "Server-authoritative multiplayer in src/app/multiplayer \u2014 the coprocessors that run identically in browser and on the Elixir server via wasmex/SNIFS.", + "status": "TODO", + "files": [ + "src/app/multiplayer/BurbleAdapter.res", + "src/app/multiplayer/LobbyManager.res", + "src/app/multiplayer/LobbyManagerCoprocessor.res", + "src/app/multiplayer/MultiplayerClientCoprocessor.res", + "src/app/multiplayer/VMNetworkCoprocessor.res", + "src/app/multiplayer/VoiceBridge.res" + ], + "count": 6 + }, + { + "id": "C5", + "name": "Engine coprocessors", + "description": "Core engine coprocessors: audio state, navigation, resize, maths, random, storage.", + "status": "TODO", + "files": [ + "src/engine/audio/Audio.res", + "src/engine/navigation/Navigation.res", + "src/engine/resize/Resize.res", + "src/engine/resize/ResizeCoprocessor.res", + "src/engine/utils/GetResolution.res", + "src/engine/utils/GetResolutionCoprocessor.res", + "src/engine/utils/Maths.res", + "src/engine/utils/MathsCoprocessor.res", + "src/engine/utils/RandomCoprocessor.res", + "src/engine/utils/StorageCoprocessor.res", + "src/engine/utils/WaitFor.res" + ], + "count": 11 + }, + { + "id": "C6", + "name": "Combat and enemy AI coprocessors", + "description": "Game simulation: hitbox geometry, HP, difficulty scaling, detection, distraction \u2014 pure integer state machines.", + "status": "TODO", + "files": [ + "src/app/combat/CombatFxLogicCoprocessor.res", + "src/app/combat/Hitbox.res", + "src/app/combat/HitboxGeomCoprocessor.res", + "src/app/combat/PlayerHPCoprocessor.res", + "src/app/enemies/DetectionSystemCoprocessor.res", + "src/app/enemies/DifficultyScaleCoprocessor.res", + "src/app/enemies/DistractionCoprocessor.res", + "src/app/enemies/DualAlertBridge.res", + "src/app/enemies/SecurityAICoprocessor.res" + ], + "count": 9 + }, + { + "id": "C7", + "name": "Player coprocessors", + "description": "Player attribute, loadout, skill and ability coprocessors \u2014 pure integer player state.", + "status": "TODO", + "files": [ + "src/app/player/CriticalRollCoprocessor.res", + "src/app/player/JessicaBackgroundCoprocessor.res", + "src/app/player/JessicaLoadoutCoprocessor.res", + "src/app/player/Player.res", + "src/app/player/PlayerAttributesCoprocessor.res", + "src/app/player/QCertifications.res", + "src/app/player/QCertificationsCoprocessor.res", + "src/app/player/QProgramsCoprocessor.res", + "src/app/player/SkillAbilitiesCoprocessor.res", + "src/app/player/SkillRankCoprocessor.res" + ], + "count": 10 + }, + { + "id": "C8", + "name": "Device and network coprocessors", + "description": "Device state machine coprocessors: power, network transfer, security rank, covert link.", + "status": "TODO", + "files": [ + "src/app/devices/CovertLinkCoprocessor.res", + "src/app/devices/DeviceFactory.res", + "src/app/devices/GlobalNetworkDataCoprocessor.res", + "src/app/devices/LaptopStateCoprocessor.res", + "src/app/devices/NetworkManagerCoprocessor.res", + "src/app/devices/NetworkTransferCoprocessor.res", + "src/app/devices/PowerManagerCoprocessor.res", + "src/app/devices/PowerStationDevice.res", + "src/app/devices/SecurityRankCoprocessor.res", + "src/app/devices/types/DeviceTypes.res" + ], + "count": 10 + }, + { + "id": "C9", + "name": "Game loop, AffineTEA, and VeriSim types", + "description": "Top-level game loop, AffineTEA architecture, VeriSim integration types, and the entry point.", + "status": "TODO", + "files": [ + "src/Main.res", + "src/app/GameLoop.res", + "src/app/burble/BurbleIntegration.res", + "src/app/pixi/PixiCoprocessor.res", + "src/app/tea/AffineTEA.res", + "src/app/tea/AffineTEARouter.res", + "src/app/verisimdb/SaveGame.res", + "src/app/verisimdb/VeriSimDrift.res", + "src/app/verisimdb/VeriSimError.res", + "src/app/verisimdb/VeriSimFederation.res", + "src/app/verisimdb/VeriSimHexad.res", + "src/app/verisimdb/VeriSimProvenance.res", + "src/app/verisimdb/VeriSimSearch.res", + "src/app/verisimdb/VeriSimTypes.res", + "src/app/verisimdb/VeriSimVcl.res", + "src/app/vm/VmCoprocessor.res" + ], + "count": 16 + }, + { + "id": "C10", + "name": "Utils, tools, companions, narrative, and proven modules", + "description": "Game utilities, tools coprocessors, Moletaire companion, mission briefing, and formal-proof integration.", + "status": "TODO", + "files": [ + "src/app/companions/MoletaireCoprocessorsCoprocessor.res", + "src/app/companions/MoletaireHunger.res", + "src/app/companions/MoletaireHungerCoprocessor.res", + "src/app/companions/MoletairePersistence.res", + "src/app/narrative/MissionBriefingCoprocessor.res", + "src/app/proven/ProvenError.res", + "src/app/proven/SafeAngle.res", + "src/app/proven/SafeFloatCoprocessor.res", + "src/app/tools/PasswordCrackerCoprocessor.res", + "src/app/tools/PortScannerCoprocessor.res", + "src/app/utils/Announcer.res", + "src/app/utils/ColorPalette.res", + "src/app/utils/ColorPaletteCoprocessor.res", + "src/app/utils/DomA11y.res", + "src/app/utils/FontScaleCoprocessor.res", + "src/app/utils/GameI18nCoprocessor.res", + "src/app/utils/KeyboardNav.res", + "src/app/utils/Locales.res", + "src/app/utils/PanicHandler.res", + "src/app/utils/PolyglotI18n.res", + "src/app/utils/UserSettings.res" + ], + "count": 21 + }, + { + "id": "C11", + "name": "UI and accessibility coprocessors", + "description": "UI widget logic, font scaling, i18n, keyboard navigation, popup logic \u2014 pure integer presentation state.", + "status": "TODO", + "files": [ + "src/app/popups/ForceLayoutCoprocessor.res", + "src/app/ui/Button.res", + "src/app/ui/DualAlert.res", + "src/app/ui/DualAlertCoprocessor.res", + "src/app/ui/HardwareWiring.res", + "src/app/ui/HubButton.res", + "src/app/ui/InventoryUI.res", + "src/app/ui/Label.res", + "src/app/ui/NavButton.res", + "src/app/ui/VolumeSlider.res" + ], + "count": 10 + }, + { + "id": "C12", + "name": "Render-glue screens, UI, and bindings", + "description": "Screen implementations, render-logic coprocessors, and PixiJS bindings. Migrated last \u2014 these call the AffineScript brain from the host JS/Pixi layer.", + "status": "TODO", + "files": [ + "src/app/companions/CompanionsRenderLogicCoprocessor.res", + "src/app/devices/DevicesRenderLogicCoprocessor.res", + "src/app/enemies/EnemiesRenderLogicCoprocessor.res", + "src/app/pickups/ToolsPickupsRenderLogicCoprocessor.res", + "src/app/player/PlayerRenderLogicCoprocessor.res", + "src/app/popups/FeaturePacksPopup.res", + "src/app/popups/IntegrationsPopup.res", + "src/app/popups/LanguagePopup.res", + "src/app/popups/NarrativePopupsRenderLogicCoprocessor.res", + "src/app/popups/PausePopup.res", + "src/app/screens/BalanceAnalyserCoprocessor.res", + "src/app/screens/CreditsScreen.res", + "src/app/screens/JessicaCustomiseScreen.res", + "src/app/screens/LoadScreen.res", + "src/app/screens/LoadoutScreen.res", + "src/app/screens/LocationDataCoprocessor.res", + "src/app/screens/ObserverScreen.res", + "src/app/screens/QViewScreen.res", + "src/app/screens/ScreenGlitchFxCoprocessor.res", + "src/app/screens/ScreensRunLoopLogicCoprocessor.res", + "src/app/screens/SkillTreeScreen.res", + "src/app/screens/TitleScreen.res", + "src/app/screens/locations/AtlasScreen.res", + "src/app/screens/locations/BackboneScreen.res", + "src/app/screens/locations/BusinessISPScreen.res", + "src/app/screens/locations/CityScreen.res", + "src/app/screens/locations/DevHubScreen.res", + "src/app/screens/locations/FieldScreen.res", + "src/app/screens/locations/LabScreen.res", + "src/app/screens/locations/LocationBase.res", + "src/app/screens/locations/NexusScreen.res", + "src/app/screens/locations/RegionalISPScreen.res", + "src/app/screens/locations/RuralISPScreen.res", + "src/app/screens/main/Bouncer.res", + "src/app/screens/main/Logo.res", + "src/app/screens/main/MainScreen.res", + "src/app/screens/training/TrainingMenuScreen.res", + "src/app/ui/UiRenderLogicCoprocessor.res", + "src/app/verisimdb/VerisimProvenRenderLogicCoprocessor.res", + "src/bindings/Motion.res", + "src/bindings/Pixi.res", + "src/bindings/PixiSound.res", + "src/bindings/PixiUI.res" + ], + "count": 43 + }, + { + "id": "C_TESTS", + "name": "Test harnesses", + "description": "Existing ReScript test harnesses \u2014 when coprocessors migrate these become affine-parity harnesses, not direct migrations.", + "status": "TODO", + "files": [ + "__tests__/AccessibilityPopup_test.res", + "__tests__/AccessibilitySettings_test.res", + "__tests__/Announcer_test.res", + "__tests__/AssassinTraining_test.res", + "__tests__/AtlasScreen_test.res", + "__tests__/Audio_test.res", + "__tests__/BackboneScreen_test.res", + "__tests__/Bouncer_test.res", + "__tests__/BurbleAdapter_test.res", + "__tests__/BurbleIntegration_test.res", + "__tests__/BusinessISPScreen_test.res", + "__tests__/Button_test.res", + "__tests__/CameraDevice_test.res", + "__tests__/CameraFeed_test.res", + "__tests__/CharacterSelectScreen_test.res", + "__tests__/CityScreen_test.res", + "__tests__/ColorPalette_test.res", + "__tests__/CombatTraining_test.res", + "__tests__/Combat_test.res", + "__tests__/CoprocessorBridge_test.res", + "__tests__/CoprocessorManager_test.res", + "__tests__/Coprocessor_Backends_test.res", + "__tests__/Coprocessor_Compute_test.res", + "__tests__/Coprocessor_IO_test.res", + "__tests__/Coprocessor_Security_test.res", + "__tests__/Coprocessor_test.res", + "__tests__/CovertLink_test.res", + "__tests__/CriticalRoll_test.res", + "__tests__/DLCLoader_test.res", + "__tests__/DesktopDevice_test.res", + "__tests__/DesktopIntegration_test.res", + "__tests__/DetectionSystem_test.res", + "__tests__/DevHubScreen_test.res", + "__tests__/DeviceActivity_test.res", + "__tests__/DeviceFactory_test.res", + "__tests__/DeviceRegistry_test.res", + "__tests__/DeviceType_test.res", + "__tests__/DeviceTypes_test.res", + "__tests__/DeviceView_test.res", + "__tests__/DeviceWindow_test.res", + "__tests__/Diagnostics_test.res", + "__tests__/Distraction_test.res", + "__tests__/DogTraining_test.res", + "__tests__/DomA11y_test.res", + "__tests__/DroneTrainingGround_test.res", + "__tests__/DroneTraining_test.res", + "__tests__/Drone_test.res", + "__tests__/DualAlertBridge_test.res", + "__tests__/Engine_test.res", + "__tests__/FeaturePacksPopup_test.res", + "__tests__/FeaturePacks_test.res", + "__tests__/FeedbackIntegration_test.res", + "__tests__/FieldScreen_test.res", + "__tests__/FirewallDevice_test.res", + "__tests__/FontScale_test.res", + "__tests__/GameEvent_test.res", + "__tests__/GameI18n_test.res", + "__tests__/GameLoop_test.res", + "__tests__/GetEngine_test.res", + "__tests__/GetResolution_test.res", + "__tests__/GlobalNetworkData_test.res", + "__tests__/GlobalNetworkManager_test.res", + "__tests__/GossamerFs_test.res", + "__tests__/GuardNPC_test.res", + "__tests__/GuardTraining_test.res", + "__tests__/HUD_test.res", + "__tests__/HardwareWiring_test.res", + "__tests__/HighwayCrossingTraining_test.res", + "__tests__/Hitbox_test.res", + "__tests__/HubButton_test.res", + "__tests__/IntegrationsPopup_test.res", + "__tests__/InventoryUI_test.res", + "__tests__/Inventory_test.res", + "__tests__/JessicaCustomiseScreen_test.res", + "__tests__/JessicaLoadout_test.res", + "__tests__/KernelMonitor_test.res", + "__tests__/Kernel_Compute_test.res", + "__tests__/Kernel_Crypto_test.res", + "__tests__/Kernel_IO_test.res", + "__tests__/Kernel_Quantum_test.res", + "__tests__/Kernel_test.res", + "__tests__/KeyboardAiming_test.res", + "__tests__/KeyboardNav_test.res", + "__tests__/LabScreen_test.res", + "__tests__/Label_test.res", + "__tests__/LanguagePopup_test.res", + "__tests__/LanguageSettings_test.res", + "__tests__/LaptopGUI_test.res", + "__tests__/LaptopState_test.res", + "__tests__/LevelConfig_test.res", + "__tests__/LoadScreen_test.res", + "__tests__/LoadoutScreen_test.res", + "__tests__/LobbyRegistry_test.res", + "__tests__/LobbyScreen_test.res", + "__tests__/Locales_test.res", + "__tests__/LocationBase_test.res", + "__tests__/LocationRegistry_test.res", + "__tests__/Logo_test.res", + "__tests__/MainHubScreen_test.res", + "__tests__/MainScreen_test.res", + "__tests__/Main_test.res", + "__tests__/Maths_test.res", + "__tests__/MoletaireHunger_test.res", + "__tests__/MoletairePersistence_test.res", + "__tests__/MoletaireTraining_test.res", + "__tests__/Motion_test.res", + "__tests__/MultiplayerClient_test.res", + "__tests__/MultiplayerGlobal_test.res", + "__tests__/MultiplayerScreenWiring_test.res", + "__tests__/NavButton_test.res", + "__tests__/Navigation_test.res", + "__tests__/NetworkDesktop_test.res", + "__tests__/NetworkManager_test.res", + "__tests__/NetworkTransfer_test.res", + "__tests__/NetworkZones_test.res", + "__tests__/NexusScreen_test.res", + "__tests__/ObserverScreen_test.res", + "__tests__/PBXDevice_test.res", + "__tests__/PanicHandler_test.res", + "__tests__/PasswordCracker_test.res", + "__tests__/PausePopup_test.res", + "__tests__/PhoenixSocket_test.res", + "__tests__/PixiSound_test.res", + "__tests__/PixiUI_test.res", + "__tests__/Pixi_test.res", + "__tests__/PlayerAttributes_test.res", + "__tests__/PlayerGraphics_test.res", + "__tests__/PlayerHP_test.res", + "__tests__/PlayerSprite_test.res", + "__tests__/PlayerState_test.res", + "__tests__/Player_test.res", + "__tests__/PolyglotI18n_test.res", + "__tests__/PopupConstructors_test.res", + "__tests__/PortNames_test.res", + "__tests__/PortScanner_test.res", + "__tests__/PowerManager_test.res", + "__tests__/PowerStationDevice_test.res", + "__tests__/PowerView_test.res", + "__tests__/ProvenError_test.res", + "__tests__/PuzzleFormat_test.res", + "__tests__/QPrograms_test.res", + "__tests__/QViewScreen_test.res", + "__tests__/RegionalISPScreen_test.res", + "__tests__/Resize_test.res", + "__tests__/ResourceAccounting_test.res", + "__tests__/RetryPolicy_test.res", + "__tests__/RoundedBox_test.res", + "__tests__/RouterDevice_test.res", + "__tests__/RuralISPScreen_test.res", + "__tests__/SafeAngle_test.res", + "__tests__/SafeFloat_test.res", + "__tests__/SafeJson_test.res", + "__tests__/SaveGame_test.res", + "__tests__/ScavengerTraining_test.res", + "__tests__/ScreenConstructors_test.res", + "__tests__/SecurityAI_test.res", + "__tests__/SecurityDog_test.res", + "__tests__/ServerDevice_test.res", + "__tests__/SettingsPopup_test.res", + "__tests__/SkillAbilities_test.res", + "__tests__/SkillTreeScreen_test.res", + "__tests__/Storage_test.res", + "__tests__/SystemLogs_test.res", + "__tests__/TerminalDevice_test.res", + "__tests__/Terminal_test.res", + "__tests__/TitleScreen_test.res", + "__tests__/TrainingBase_test.res", + "__tests__/TrainingMenuScreen_test.res", + "__tests__/TrainingRegistry_test.res", + "__tests__/TrajectoryPreview_test.res", + "__tests__/UPSDevice_test.res", + "__tests__/UmsLevelLoader_test.res", + "__tests__/UserSettings_test.res", + "__tests__/VMBridge_test.res", + "__tests__/VMMessageBus_test.res", + "__tests__/VMNetwork_test.res", + "__tests__/VeriSimClient_test.res", + "__tests__/VeriSimDrift_test.res", + "__tests__/VeriSimError_test.res", + "__tests__/VeriSimFederation_test.res", + "__tests__/VeriSimHexad_test.res", + "__tests__/VeriSimProvenance_test.res", + "__tests__/VeriSimSearch_test.res", + "__tests__/VeriSimTypes_test.res", + "__tests__/VeriSimVcl_test.res", + "__tests__/VmBackend_test.res", + "__tests__/VoiceBridge_test.res", + "__tests__/VolumeSlider_test.res", + "__tests__/WaitFor_test.res", + "__tests__/WorldBuilder_test.res", + "__tests__/WorldMapScreen_test.res", + "__tests__/WorldPickup_test.res", + "__tests__/WorldScreen_test.res" + ], + "count": 193 + } + ], + "walled": { + "string_gated": [ + { + "file": "__tests__/CreditsScreen_test.res", + "area": "__tests__", + "walls": [ + "string subscript" + ] + }, + { + "file": "__tests__/DataFiles_test.res", + "area": "__tests__", + "walls": [ + "String.length" + ] + }, + { + "file": "__tests__/DualAlert_test.res", + "area": "__tests__", + "walls": [ + "string subscript" + ] + }, + { + "file": "__tests__/FeedbackPopup_test.res", + "area": "__tests__", + "walls": [ + "string subscript" + ] + }, + { + "file": "__tests__/ForceLayout_test.res", + "area": "__tests__", + "walls": [ + "string subscript" + ] + }, + { + "file": "__tests__/GameOverScreen_test.res", + "area": "__tests__", + "walls": [ + "String.length" + ] + }, + { + "file": "__tests__/IntroScreen_test.res", + "area": "__tests__", + "walls": [ + "String.length" + ] + }, + { + "file": "__tests__/JessicaBackground_test.res", + "area": "__tests__", + "walls": [ + "String.length", + "string subscript" + ] + }, + { + "file": "__tests__/LobbyManager_test.res", + "area": "__tests__", + "walls": [ + "string subscript", + "String.length" + ] + }, + { + "file": "__tests__/LocationData_test.res", + "area": "__tests__", + "walls": [ + "String.length" + ] + }, + { + "file": "__tests__/MissionBriefing_test.res", + "area": "__tests__", + "walls": [ + "String.length" + ] + }, + { + "file": "__tests__/MoletaireCoprocessors_test.res", + "area": "__tests__", + "walls": [ + "String.length" + ] + }, + { + "file": "__tests__/MoletaireMusic_test.res", + "area": "__tests__", + "walls": [ + "string subscript" + ] + }, + { + "file": "__tests__/Moletaire_test.res", + "area": "__tests__", + "walls": [ + "String.length" + ] + }, + { + "file": "__tests__/ParticleField_test.res", + "area": "__tests__", + "walls": [ + "string subscript" + ] + }, + { + "file": "__tests__/PeerDetection_test.res", + "area": "__tests__", + "walls": [ + "string subscript" + ] + }, + { + "file": "__tests__/QCertifications_test.res", + "area": "__tests__", + "walls": [ + "string subscript", + "String.length" + ] + }, + { + "file": "__tests__/Random_test.res", + "area": "__tests__", + "walls": [ + "String.length" + ] + }, + { + "file": "__tests__/VictoryScreen_test.res", + "area": "__tests__", + "walls": [ + "String.length" + ] + }, + { + "file": "idaptik-ums/src/App.res", + "area": "idaptik-ums", + "walls": [ + "string subscript" + ] + }, + { + "file": "idaptik-ums/src/editor/EditorLevelCmd.res", + "area": "idaptik-ums", + "walls": [ + "string subscript" + ] + }, + { + "file": "idaptik-ums/tests/test_round_trip.res", + "area": "idaptik-ums", + "walls": [ + "string subscript" + ] + }, + { + "file": "shared/src/Coprocessor_Compute.res", + "area": "shared/src", + "walls": [ + "string subscript" + ] + }, + { + "file": "shared/src/Coprocessor_IO.res", + "area": "shared/src", + "walls": [ + "String.fromCharCode", + "String.length", + "String.charCodeAt", + "String.startsWith" + ] + }, + { + "file": "shared/src/Coprocessor_Security.res", + "area": "shared/src", + "walls": [ + "string subscript" + ] + }, + { + "file": "shared/src/Inventory.res", + "area": "shared/src", + "walls": [ + "string subscript" + ] + }, + { + "file": "shared/src/Kernel_IO.res", + "area": "shared/src", + "walls": [ + "String.fromCharCode", + "String.length", + "String.startsWith" + ] + }, + { + "file": "src/app/companions/Moletaire.res", + "area": "src/app/companions", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/companions/MoletaireMusic.res", + "area": "src/app/companions", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/devices/CoprocessorBridge.res", + "area": "src/app/devices", + "walls": [ + "String.length", + "String.indexOf", + "String.slice" + ] + }, + { + "file": "src/app/devices/DeviceView.res", + "area": "src/app/devices", + "walls": [ + "string subscript", + "String.endsWith", + "String.length" + ] + }, + { + "file": "src/app/devices/FirewallDevice.res", + "area": "src/app/devices", + "walls": [ + "String.indexOf", + "String.slice", + "string subscript" + ] + }, + { + "file": "src/app/devices/GlobalNetworkData.res", + "area": "src/app/devices", + "walls": [ + "String.length", + "string subscript" + ] + }, + { + "file": "src/app/devices/LaptopGUI.res", + "area": "src/app/devices", + "walls": [ + "String.endsWith", + "String.startsWith" + ] + }, + { + "file": "src/app/devices/NetworkZones.res", + "area": "src/app/devices", + "walls": [ + "String.startsWith" + ] + }, + { + "file": "src/app/devices/Terminal.res", + "area": "src/app/devices", + "walls": [ + "string subscript", + "String.startsWith", + "String.length", + "String.slice" + ] + }, + { + "file": "src/app/devices/VMBridge.res", + "area": "src/app/devices", + "walls": [ + "string subscript", + "String.length", + "String.startsWith" + ] + }, + { + "file": "src/app/enemies/Drone.res", + "area": "src/app/enemies", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/enemies/GuardNPC.res", + "area": "src/app/enemies", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/enemies/SecurityAI.res", + "area": "src/app/enemies", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/enemies/SecurityDog.res", + "area": "src/app/enemies", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/multiplayer/VMMessageBus.res", + "area": "src/app/multiplayer", + "walls": [ + "String.startsWith" + ] + }, + { + "file": "src/app/multiplayer/VMNetwork.res", + "area": "src/app/multiplayer", + "walls": [ + "String.startsWith", + "string subscript" + ] + }, + { + "file": "src/app/narrative/DataFiles.res", + "area": "src/app/narrative", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/pickups/WorldPickup.res", + "area": "src/app/pickups", + "walls": [ + "String.slice" + ] + }, + { + "file": "src/app/popups/FeedbackPopup.res", + "area": "src/app/popups", + "walls": [ + "String.length", + "String.slice" + ] + }, + { + "file": "src/app/popups/NetworkDesktop.res", + "area": "src/app/popups", + "walls": [ + "String.startsWith", + "string subscript" + ] + }, + { + "file": "src/app/proven/SafeJson.res", + "area": "src/app/proven", + "walls": [ + "String.slice", + "String.length" + ] + }, + { + "file": "src/app/screens/CharacterSelectScreen.res", + "area": "src/app/screens", + "walls": [ + "String.length", + "String.slice" + ] + }, + { + "file": "src/app/screens/IntroScreen.res", + "area": "src/app/screens", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/screens/WorldMapScreen.res", + "area": "src/app/screens", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/screens/training/CombatTraining.res", + "area": "src/app/screens", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/screens/training/HighwayCrossingTraining.res", + "area": "src/app/screens", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/screens/training/MoletaireTraining.res", + "area": "src/app/screens", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/tools/PasswordCracker.res", + "area": "src/app/tools", + "walls": [ + "String.length", + "String.charCodeAt" + ] + }, + { + "file": "src/app/tools/PortScanner.res", + "area": "src/app/tools", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/ui/HUD.res", + "area": "src/app/ui", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/app/ui/KernelMonitor.res", + "area": "src/app/ui", + "walls": [ + "String.length" + ] + }, + { + "file": "src/app/utils/DesktopIntegration.res", + "area": "src/app/utils", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/engine/utils/Random.res", + "area": "src/engine", + "walls": [ + "string subscript", + "String.length" + ] + }, + { + "file": "src/shared/Coprocessor_Compute.res", + "area": "src/shared", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/shared/Coprocessor_IO.res", + "area": "src/shared", + "walls": [ + "String.fromCharCode", + "String.length", + "String.charCodeAt", + "String.startsWith" + ] + }, + { + "file": "src/shared/Coprocessor_Security.res", + "area": "src/shared", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/shared/DLCLoader.res", + "area": "src/shared", + "walls": [ + "String.length" + ] + }, + { + "file": "src/shared/GossamerFs.res", + "area": "src/shared", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/shared/Inventory.res", + "area": "src/shared", + "walls": [ + "string subscript" + ] + }, + { + "file": "src/shared/Kernel_IO.res", + "area": "src/shared", + "walls": [ + "String.fromCharCode", + "String.length", + "String.startsWith" + ] + }, + { + "file": "src/shared/PortNames.res", + "area": "src/shared", + "walls": [ + "String.startsWith" + ] + }, + { + "file": "vm/lib/ocaml/InstructionParser.res", + "area": "vm", + "walls": [ + "String.length", + "string subscript" + ] + }, + { + "file": "vm/lib/ocaml/StateDiff.res", + "area": "vm", + "walls": [ + "String.length" + ] + }, + { + "file": "vm/lib/ocaml/VmState.res", + "area": "vm", + "walls": [ + "String.startsWith" + ] + } + ], + "effect_gated": [ + { + "file": "__tests__/TestRunner.res", + "area": "__tests__", + "walls": [ + "Console.log" + ] + }, + { + "file": "shared/src/Coprocessor.res", + "area": "shared/src", + "walls": [ + "module-level mutable state (Dict.make())", + "Console.log", + "module-level mutable state (ref(...))" + ] + }, + { + "file": "shared/src/CoprocessorManager.res", + "area": "shared/src", + "walls": [ + "Console.log" + ] + }, + { + "file": "shared/src/Kernel_Crypto.res", + "area": "shared/src", + "walls": [ + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "shared/src/Kernel_Quantum.res", + "area": "shared/src", + "walls": [ + "module-level mutable state (Dict.make())", + "Console.log" + ] + }, + { + "file": "shared/src/ResourceAccounting.res", + "area": "shared/src", + "walls": [ + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/app/GetEngine.res", + "area": "src/app", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/combat/Combat.res", + "area": "src/app/combat", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/combat/PlayerHP.res", + "area": "src/app/combat", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/companions/MoletaireCoprocessors.res", + "area": "src/app/companions", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/devices/CameraDevice.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/app/devices/CameraFeed.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (ref(...))", + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/app/devices/CovertLink.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/devices/DesktopDevice.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/devices/DeviceActivity.res", + "area": "src/app/devices", + "walls": [ + "Date.now", + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/app/devices/DeviceRegistry.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (Dict.make())", + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/devices/GlobalNetworkManager.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/devices/LaptopState.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/devices/NetworkManager.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/devices/NetworkTransfer.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (ref(...))", + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/app/devices/PBXDevice.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/devices/PowerManager.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (ref(...))", + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/app/devices/RouterDevice.res", + "area": "src/app/devices", + "walls": [ + "Date.now", + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/devices/ServerDevice.res", + "area": "src/app/devices", + "walls": [ + "Date.now", + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/devices/SystemLogs.res", + "area": "src/app/devices", + "walls": [ + "Date.now", + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/app/devices/TerminalDevice.res", + "area": "src/app/devices", + "walls": [ + "Date.now" + ] + }, + { + "file": "src/app/devices/UPSDevice.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/devices/common/DeviceWindow.res", + "area": "src/app/devices", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/enemies/DetectionSystem.res", + "area": "src/app/enemies", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/enemies/Distraction.res", + "area": "src/app/enemies", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/multiplayer/LobbyRegistry.res", + "area": "src/app/multiplayer", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/multiplayer/MultiplayerClient.res", + "area": "src/app/multiplayer", + "walls": [ + "Date.now" + ] + }, + { + "file": "src/app/multiplayer/MultiplayerGlobal.res", + "area": "src/app/multiplayer", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/multiplayer/MultiplayerScreenWiring.res", + "area": "src/app/multiplayer", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/multiplayer/PhoenixSocket.res", + "area": "src/app/multiplayer", + "walls": [ + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/app/narrative/MissionBriefing.res", + "area": "src/app/narrative", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/player/CriticalRoll.res", + "area": "src/app/player", + "walls": [ + "module-level mutable state (ref(...))", + "Math.random" + ] + }, + { + "file": "src/app/player/JessicaBackground.res", + "area": "src/app/player", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/player/JessicaLoadout.res", + "area": "src/app/player", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/player/KeyboardAiming.res", + "area": "src/app/player", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/player/PlayerAttributes.res", + "area": "src/app/player", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/player/PlayerGraphics.res", + "area": "src/app/player", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/player/PlayerSprite.res", + "area": "src/app/player", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/player/PlayerState.res", + "area": "src/app/player", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/player/QPrograms.res", + "area": "src/app/player", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/player/SkillAbilities.res", + "area": "src/app/player", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/player/TrajectoryPreview.res", + "area": "src/app/player", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/popups/AccessibilityPopup.res", + "area": "src/app/popups", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/popups/ForceLayout.res", + "area": "src/app/popups", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/popups/PopupConstructors.res", + "area": "src/app/popups", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/popups/PowerView.res", + "area": "src/app/popups", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/popups/SettingsPopup.res", + "area": "src/app/popups", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/proven/SafeFloat.res", + "area": "src/app/proven", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/BalanceAnalyserModel.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/GameOverScreen.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))", + "Math.random" + ] + }, + { + "file": "src/app/screens/LevelConfig.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/LobbyScreen.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))", + "Date.now" + ] + }, + { + "file": "src/app/screens/LocationData.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/LocationRegistry.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/app/screens/ScreenConstructors.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/VictoryScreen.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/WorldBuilder.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))", + "Math.random" + ] + }, + { + "file": "src/app/screens/WorldScreen.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))", + "Math.random" + ] + }, + { + "file": "src/app/screens/hub/MainHubScreen.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/training/AssassinTraining.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/training/DogTraining.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/training/DroneTraining.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/training/DroneTrainingGround.res", + "area": "src/app/screens", + "walls": [ + "Math.random", + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/training/GuardTraining.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/training/ScavengerTraining.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/training/TrainingBase.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/screens/training/TrainingRegistry.res", + "area": "src/app/screens", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/ui/ParticleField.res", + "area": "src/app/ui", + "walls": [ + "module-level mutable state (ref(...))", + "Math.random" + ] + }, + { + "file": "src/app/ui/RoundedBox.res", + "area": "src/app/ui", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/utils/AccessibilitySettings.res", + "area": "src/app/utils", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/utils/FeaturePacks.res", + "area": "src/app/utils", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/utils/FeedbackIntegration.res", + "area": "src/app/utils", + "walls": [ + "module-level mutable state (ref(...))", + "Date.now" + ] + }, + { + "file": "src/app/utils/FontScale.res", + "area": "src/app/utils", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/utils/GameI18n.res", + "area": "src/app/utils", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/utils/LanguageSettings.res", + "area": "src/app/utils", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/utils/PeerDetection.res", + "area": "src/app/utils", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/app/verisimdb/VeriSimClient.res", + "area": "src/app", + "walls": [ + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/engine/Engine.res", + "area": "src/engine", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/engine/VmBackend.res", + "area": "src/engine", + "walls": [ + "module-level mutable state (ref(...))", + "Console.log", + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/engine/utils/Storage.res", + "area": "src/engine", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/shared/Coprocessor.res", + "area": "src/shared", + "walls": [ + "module-level mutable state (Dict.make())", + "Console.log", + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/shared/CoprocessorManager.res", + "area": "src/shared", + "walls": [ + "Console.log" + ] + }, + { + "file": "src/shared/Diagnostics.res", + "area": "src/shared", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/shared/Kernel.res", + "area": "src/shared", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/shared/Kernel_Crypto.res", + "area": "src/shared", + "walls": [ + "module-level mutable state (Dict.make())" + ] + }, + { + "file": "src/shared/Kernel_Quantum.res", + "area": "src/shared", + "walls": [ + "module-level mutable state (Dict.make())", + "Console.log" + ] + }, + { + "file": "src/shared/PuzzleFormat.res", + "area": "src/shared", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/shared/ResourceAccounting.res", + "area": "src/shared", + "walls": [ + "module-level mutable state (Dict.make())", + "module-level mutable state (ref(...))" + ] + }, + { + "file": "src/shared/UmsLevelLoader.res", + "area": "src/shared", + "walls": [ + "module-level mutable state (ref(...))" + ] + }, + { + "file": "vm/lib/ocaml/add_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/and_or_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/benchmark.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/call_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/flip_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/if_pos_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/if_zero_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/load_store_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/loop_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/push_pop_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/rol_ror_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/send_recv_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/swap_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/test_all.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/test_runner.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/lib/ocaml/xor_test.res", + "area": "vm", + "walls": [ + "Console.log" + ] + }, + { + "file": "vm/wasm/src/WasmVm.res", + "area": "vm", + "walls": [ + "module-level mutable state (ref(...))", + "module-level mutable state (Dict.make())" + ] + } + ] + } +} \ No newline at end of file diff --git a/proposals/idaptik/state-vs-digest.svg b/proposals/idaptik/state-vs-digest.svg new file mode 100644 index 0000000..754707d --- /dev/null +++ b/proposals/idaptik/state-vs-digest.svg @@ -0,0 +1,100 @@ + + + + Two ways to check that both sides agree + both computers ran the SAME recipe on the SAME inputs, so they SHOULD already match — we just want to confirm it + + + + (1) SEND THE WHOLE THING + cost grows with the amount of data — written O(state) + + + Computer A + + + + + + + + + + + Computer B + reads it all, + repacks, replies + + + + + the ENTIRE state + every byte, packed up + + + + reply — also big + + COST + + + grows with the state size — like couriering a whole genome, every time + + + + (2) ASK IF WE AGREE + cost is tiny and constant — written ~O(1) + + + Computer A + + + + + + + + already computed + (has the whole thing) + + + Computer B + + + + + + + + already computed + (has the whole thing) + + a tiny fingerprint ("is the moon there?") + + + + + + + + + + + + a1f3 + + + + + + + yes + + COST + + + same tiny size, no matter how big the state is + + If the fingerprints DON'T match (rare): then — and only then — you do the expensive full comparison. + information = surprise: you already expect to match, so confirming it is nearly free; you pay big only for the surprise. + From 86825841bbacf2736a0cd52c854f5db409890917 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 5 Jun 2026 05:24:19 +0000 Subject: [PATCH 2/2] migrate(phase-c/C1): re-decompose 8 shared/src kernels, 4-gate green MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Deep wave 1 of the ReScript -> AffineScript -> wasm migration. Cluster C1 (shared/src leaf modules) re-decomposed into eight pure-integer co-processor kernels staged under proposals/idaptik/migrated/, each verified end-to-end by the 4-gate recipe. Kernels (brain = the integers that cross the wasm boundary; host keeps the strings/floats/DOM/state — the senses): DeviceType 12-device taxonomy: count, validity, code-clamp (lossless) PuzzleFormat difficulty(4)/tier(5) encodings + DLCLoader clamp-to-default PortNames 10 coprocessor-domain port taxonomy (= portnames.wasm, the kernel PortNamesCoprocessor.res's JS bridge already targets) GameEvent alertLevel(4, ordered clamp) + direction(6, flat) Kernel_Compute per-domain element caps + the 504/413/404/0 scheduler gate Kernel the 503/404/0 pre-flight gate + domain -> handler router RetryPolicy the 503/504/429 transient classifier + 3-policy config table Diagnostics the <70/<90/>=90 health-band classifier + registry check Re-decomposed, not transliterated: Promise/async collapsed to the synchronous status decision; service-locator reads (ResourceAccounting, backend registry) threaded as explicit integer params; variants re-encoded as closed integer bands; floats + wall-clock timing kept host-side (timing is a sense). Four gates green (captured in migrated/EVIDENCE.adoc): G1 compile 8/8 -> wasm G2 parity 1223/1223 oracle-vs-wasm inputs (independent JS oracles) G3 echo-boundary 6 Agda proofs, agda exit 0: 3 LOSSLESS (DeviceType, PortNames, GameEvent direction) + 3 CONTROLLED-LOSS (PuzzleFormat tier clamp, GameEvent alert clamp, Kernel route fan-in) — each collision named and certified G4 assail 8/8 clean (no undeclared clamp / unguarded decoder) Three C1 files are host-side "senses" with no extractable brain and stay in the host: Coprocessor_Backends.res (registration wiring), PortNamesCoprocessor .res (JS bridge shim, consumes PortNames.affine), DLCLoader.res (JSON parser; its one integer fragment is delivered as PuzzleFormat.clamp_tier). Staged, not applied — per the plan's access gate, the apply + cutover wait on idaptik write-access (Phase Omega). Ledger: Phase B + Phase C wave 1 DONE; next = C2 (vm/lib/ocaml instruction set). migration-map.json C1 -> DONE. https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --- proposals/MIGRATION-PLAN.adoc | 9 +- proposals/idaptik/migrated/.gitignore | 3 + .../migrated/DeviceType/DeviceType.affine | 47 +++++++ .../DeviceType/DeviceTypeBoundary.agda | 104 +++++++++++++++ .../migrated/DeviceType/devicetype.config.mjs | 25 ++++ .../migrated/Diagnostics/Diagnostics.affine | 39 ++++++ .../Diagnostics/diagnostics.config.mjs | 25 ++++ proposals/idaptik/migrated/EVIDENCE.adoc | 125 ++++++++++++++++++ .../migrated/GameEvent/GameEvent.affine | 72 ++++++++++ .../GameEvent/GameEventAlertBoundary.agda | 83 ++++++++++++ .../GameEvent/GameEventDirectionBoundary.agda | 80 +++++++++++ .../migrated/GameEvent/gameevent.config.mjs | 19 +++ .../idaptik/migrated/Kernel/Kernel.affine | 55 ++++++++ .../migrated/Kernel/KernelRouteBoundary.agda | 98 ++++++++++++++ .../idaptik/migrated/Kernel/kernel.config.mjs | 31 +++++ .../Kernel_Compute/Kernel_Compute.affine | 51 +++++++ .../Kernel_Compute/kernel_compute.config.mjs | 37 ++++++ .../migrated/PortNames/PortNames.affine | 54 ++++++++ .../migrated/PortNames/PortNamesBoundary.agda | 96 ++++++++++++++ .../migrated/PortNames/portnames.config.mjs | 16 +++ .../migrated/PuzzleFormat/PuzzleFormat.affine | 60 +++++++++ .../PuzzleFormatTierBoundary.agda | 86 ++++++++++++ .../PuzzleFormat/puzzleformat.config.mjs | 21 +++ proposals/idaptik/migrated/README.adoc | 113 ++++++++++++++++ .../migrated/RetryPolicy/RetryPolicy.affine | 56 ++++++++ .../RetryPolicy/retrypolicy.config.mjs | 28 ++++ 26 files changed, 1429 insertions(+), 4 deletions(-) create mode 100644 proposals/idaptik/migrated/.gitignore create mode 100644 proposals/idaptik/migrated/DeviceType/DeviceType.affine create mode 100644 proposals/idaptik/migrated/DeviceType/DeviceTypeBoundary.agda create mode 100644 proposals/idaptik/migrated/DeviceType/devicetype.config.mjs create mode 100644 proposals/idaptik/migrated/Diagnostics/Diagnostics.affine create mode 100644 proposals/idaptik/migrated/Diagnostics/diagnostics.config.mjs create mode 100644 proposals/idaptik/migrated/EVIDENCE.adoc create mode 100644 proposals/idaptik/migrated/GameEvent/GameEvent.affine create mode 100644 proposals/idaptik/migrated/GameEvent/GameEventAlertBoundary.agda create mode 100644 proposals/idaptik/migrated/GameEvent/GameEventDirectionBoundary.agda create mode 100644 proposals/idaptik/migrated/GameEvent/gameevent.config.mjs create mode 100644 proposals/idaptik/migrated/Kernel/Kernel.affine create mode 100644 proposals/idaptik/migrated/Kernel/KernelRouteBoundary.agda create mode 100644 proposals/idaptik/migrated/Kernel/kernel.config.mjs create mode 100644 proposals/idaptik/migrated/Kernel_Compute/Kernel_Compute.affine create mode 100644 proposals/idaptik/migrated/Kernel_Compute/kernel_compute.config.mjs create mode 100644 proposals/idaptik/migrated/PortNames/PortNames.affine create mode 100644 proposals/idaptik/migrated/PortNames/PortNamesBoundary.agda create mode 100644 proposals/idaptik/migrated/PortNames/portnames.config.mjs create mode 100644 proposals/idaptik/migrated/PuzzleFormat/PuzzleFormat.affine create mode 100644 proposals/idaptik/migrated/PuzzleFormat/PuzzleFormatTierBoundary.agda create mode 100644 proposals/idaptik/migrated/PuzzleFormat/puzzleformat.config.mjs create mode 100644 proposals/idaptik/migrated/README.adoc create mode 100644 proposals/idaptik/migrated/RetryPolicy/RetryPolicy.affine create mode 100644 proposals/idaptik/migrated/RetryPolicy/retrypolicy.config.mjs diff --git a/proposals/MIGRATION-PLAN.adoc b/proposals/MIGRATION-PLAN.adoc index 95cc313..0ca401b 100644 --- a/proposals/MIGRATION-PLAN.adoc +++ b/proposals/MIGRATION-PLAN.adoc @@ -185,10 +185,11 @@ Heuristic: [cols="1,1,3",options="header"] |=== | Phase | State | Notes -| Pre | DONE | #531 echo proof (merged); #532 migration practice + guide + proposals (merged); #533 evangelist toolkit (draft, CI green). -| A | DONE | Plan + model-per-phase guidance written; determinism doc gained a latency-regimes appendix (verify-don't-transfer + game-vs-deep-space + the 2 SVGs); #533 green (draft, owner to merge). NEXT: PHASE B. -| B | TODO | Full-corpus triage -> migration-map.{adoc,json}. -| C+ | TODO | Deep waves via the 4-gate recipe. +| Pre | DONE | #531 echo proof (merged); #532 migration practice + guide + proposals (merged); #533 evangelist toolkit (*merged* 2026-06-05). +| A | DONE | Plan + model-per-phase guidance written; determinism doc gained a latency-regimes appendix (verify-don't-transfer + game-vs-deep-space + the 2 SVGs); #533 merged. NEXT: PHASE B. +| B | DONE | Full-corpus triage complete (2026-06-05). 571 files: *389 MIGRATABLE NOW (68%)*, 71 STRING-GATED (12%), 111 EFFECT-GATED (19%). Non-test: 358 files, 196 migratable (55%). Clusters C1–C12 ordered, leaf-first. Worklist: `proposals/idaptik/migration-map.json`. NEXT: PHASE C — cluster 1 = C1 (shared/src, 11 files) + C2 (vm instructions, 31 files). Switch to *Opus* for re-decomposition. +| C (C1) | DONE | Deep wave 1 complete (2026-06-05, Opus). Cluster C1 re-decomposed: *8 pure-integer kernels* staged under `proposals/idaptik/migrated/` (DeviceType, PuzzleFormat, PortNames, GameEvent, Kernel_Compute, Kernel, RetryPolicy, Diagnostics); 3 C1 files are host-side "senses" with no brain (Coprocessor_Backends, PortNamesCoprocessor, DLCLoader). *Four gates green:* 8/8 compile, 1223/1223 parity, 6 echo-boundary proofs (agda exit 0; 3 LOSSLESS + 3 CONTROLLED-LOSS), 8/8 assail-clean. Evidence: `migrated/EVIDENCE.adoc`. The per-shape recipe is now established (enum-taxonomy / status-gate / classifier / predicate). NEXT: wave 2 = C2. +| C2+ | TODO | Remaining deep waves via the 4-gate recipe; next = *C2* (vm/lib/ocaml instruction set, 31 files — the pure-integer reversible VM opcodes). Opus for any novel re-decomposition; Sonnet for the now-rote gate passes (C1 set the pattern). Then C3..C12. | F+ | TODO | Compiler walls (string backend, then effects). | Ω | TODO (access-gated) | Cutover + ReScript extinction. |=== diff --git a/proposals/idaptik/migrated/.gitignore b/proposals/idaptik/migrated/.gitignore new file mode 100644 index 0000000..219ea5a --- /dev/null +++ b/proposals/idaptik/migrated/.gitignore @@ -0,0 +1,3 @@ +# Compiled wasm is build output, regenerated by every affine-parity run +# (compile:true) from the staged .affine + config. Not committed. +*.wasm diff --git a/proposals/idaptik/migrated/DeviceType/DeviceType.affine b/proposals/idaptik/migrated/DeviceType/DeviceType.affine new file mode 100644 index 0000000..4fbaf6f --- /dev/null +++ b/proposals/idaptik/migrated/DeviceType/DeviceType.affine @@ -0,0 +1,47 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// DeviceType -- the device-type taxonomy co-processor, the pure-integer core +// extracted from idaptik shared/src/DeviceType.res. Per the DESIGN-VISION +// ("AffineScript is the brain, JS/Pixi the senses; they pass primitives across +// the wasm boundary"), the JS host keeps every device-type STRING (portName, +// fromString) and the per-device mutable defenceFlags record; AffineScript owns +// only the canonical integer encoding of the twelve device kinds and its +// validity. +// +// The ReScript original is a 12-constructor variant `t` plus a `portName` +// switch and a `fromString` parser. We re-decompose the variant as the +// canonical 0..11 integer the constructor order already implies, so the +// taxonomy is a closed band and validity is one range test. The variant IS the +// integer; no strings cross the boundary. (We use range guards rather than an +// enum round-trip because, the band being contiguous, the round-trip would be +// the identity -- the same flat shape PortNames.affine uses for its 0..9 band.) +// +//## Device-type encoding (the header contract for the JS host) +// code device code device +// 0 Laptop 6 Camera +// 1 Desktop 7 AccessPoint +// 2 Server 8 PatchPanel +// 3 Router 9 PowerSupply +// 4 Switch 10 PhoneSystem (PBX) +// 5 Firewall 11 FibreHub +// The encoding is LOSSLESS: twelve distinct kinds map to twelve distinct codes, +// so the host round-trips device-type <-> code with no collision (certified by +// echo-boundary, DeviceTypeBoundary.agda). A code outside 0..11 is not a device +// type: is_valid_device_type reports 0 and clamp_device_type returns the +// out-of-band sentinel -1 -- never an in-band code, so no in-band collision is +// introduced (this is a sentinel, not a clamp; assail stays clean). + +// The number of canonical device kinds in the taxonomy. +pub fn device_type_count() -> Int { 12 } + +// Whether a host integer names a defined device type. 1 = valid, 0 = out of band. +pub fn is_valid_device_type(code: Int) -> Int { + if code < 0 { 0 } else { if code > 11 { 0 } else { 1 } } +} + +// Canonicalise a host integer: identity on a valid 0..11 code, the out-of-band +// sentinel -1 otherwise. -1 is not an in-band code, so out-of-band input can +// never be confused with a real device type (this is a sentinel, not a clamp). +pub fn clamp_device_type(code: Int) -> Int { + if is_valid_device_type(code) == 1 { code } else { -1 } +} diff --git a/proposals/idaptik/migrated/DeviceType/DeviceTypeBoundary.agda b/proposals/idaptik/migrated/DeviceType/DeviceTypeBoundary.agda new file mode 100644 index 0000000..97fd223 --- /dev/null +++ b/proposals/idaptik/migrated/DeviceType/DeviceTypeBoundary.agda @@ -0,0 +1,104 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "Laptop": 0, +-- "Desktop": 1, +-- "Server": 2, +-- "Router": 3, +-- "Switch": 4, +-- "Firewall": 5, +-- "Camera": 6, +-- "AccessPoint": 7, +-- "PatchPanel": 8, +-- "PowerSupply": 9, +-- "PhoneSystem": 10, +-- "FibreHub": 11 +-- } + +module DeviceTypeBoundary where + +open import Echo using (Echo) +open import EchoImageFactorization using (Injective) +open import EchoEncodingFaithfulness using (Encoding; module EncodingTheorems) + +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl) +open import Relation.Nullary using (¬_) + + +-- The host-side enumerated value (one constructor per table name). +-- c0 = Laptop +-- c1 = Desktop +-- c2 = Server +-- c3 = Router +-- c4 = Switch +-- c5 = Firewall +-- c6 = Camera +-- c7 = AccessPoint +-- c8 = PatchPanel +-- c9 = PowerSupply +-- c10 = PhoneSystem +-- c11 = FibreHub +data Host : Set where + c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 +code c4 = 4 +code c5 = 5 +code c6 = 6 +code c7 = 7 +code c8 = 8 +code c9 = 9 +code c10 = 10 +code c11 = 11 + +-- Injectivity by exhaustive case analysis. The codes are literal +-- numerals, so listing the diagonal refl clauses is enough: Agda's +-- coverage checker discharges the off-diagonal pairs as absurd +-- numeral equalities (mirrors rankCode-injective). +code-injective : Injective code +code-injective {c0} {c0} _ = refl +code-injective {c1} {c1} _ = refl +code-injective {c2} {c2} _ = refl +code-injective {c3} {c3} _ = refl +code-injective {c4} {c4} _ = refl +code-injective {c5} {c5} _ = refl +code-injective {c6} {c6} _ = refl +code-injective {c7} {c7} _ = refl +code-injective {c8} {c8} _ = refl +code-injective {c9} {c9} _ = refl +code-injective {c10} {c10} _ = refl +code-injective {c11} {c11} _ = refl + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +-- Re-export the lossless-half headline, instantiated and proved: +-- every integer code determines its host value uniquely. +module Theorems = EncodingTheorems encoding + +boundary-lossless : + (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂ +boundary-lossless = Theorems.encoding-lossless code-injective + diff --git a/proposals/idaptik/migrated/DeviceType/devicetype.config.mjs b/proposals/idaptik/migrated/DeviceType/devicetype.config.mjs new file mode 100644 index 0000000..9f57b76 --- /dev/null +++ b/proposals/idaptik/migrated/DeviceType/devicetype.config.mjs @@ -0,0 +1,25 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-parity config for DeviceType.affine (idaptik device-type taxonomy; +// scalar i32 ABI). The oracle re-derives the 0..11 closed band in plain JS so a +// codegen regression surfaces as a differential mismatch. +const valid = (c) => c >= 0 && c <= 11; +export default { + affine: "DeviceType.affine", + cases: [ + { name: "device_type_count()", export: "device_type_count", args: [], oracle: () => 12 }, + { + name: "is_valid_device_type over [-3..15]", + export: "is_valid_device_type", + args: [[-3, 15]], + oracle: (c) => (valid(c) ? 1 : 0), + }, + { + name: "clamp_device_type over [-3..15]", + export: "clamp_device_type", + args: [[-3, 15]], + oracle: (c) => (valid(c) ? c : -1), + }, + ], +}; diff --git a/proposals/idaptik/migrated/Diagnostics/Diagnostics.affine b/proposals/idaptik/migrated/Diagnostics/Diagnostics.affine new file mode 100644 index 0000000..f8351b8 --- /dev/null +++ b/proposals/idaptik/migrated/Diagnostics/Diagnostics.affine @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// Diagnostics -- the device-health band classifier + registry sanity check, the +// pure-integer core extracted from idaptik shared/src/Diagnostics.res. The +// ReScript original wraps raw float utilisation percentages and per-backend +// stats into typed report structures and formatted strings; those reports and +// strings are host-side (the senses). What IS pure integer is the threshold +// classification `healthOf` and the `allDomainsRegistered` count check. +// +// We re-decompose `healthOf : float -> healthLevel` onto an integer utilisation +// percentage 0..100 (the host floors the float before crossing the boundary -- +// Math.floor is a sense). The three bands and their cutoffs are unchanged. +// +//## Health band encoding (Diagnostics.healthLevel) +// band level range +// 0 Healthy pct < 70 +// 1 Warning 70 <= pct < 90 +// 2 Critical pct >= 90 (>= 95 is the hard 503 cutoff) +// health_of is deliberately many-to-one (a whole range folds onto one band); +// that is the intended classification, not an encoding, so no injectivity is +// claimed for it. The expected full registry is exactly ten domain backends. + +pub fn health_band_count() -> Int { 3 } +pub fn expected_domain_count() -> Int { 10 } + +// Classify an integer utilisation percentage into a health band. Negative input +// (impossible from a real percentage, but total here) lands in Healthy; >=90 +// in Critical, mirroring the ReScript `< 70 / < 90 / else` ladder. +pub fn health_of(pct: Int) -> Int { + if pct < 70 { return 0; } + if pct < 90 { return 1; } + 2 +} + +// 1 iff all ten expected domain backends are registered (Diagnostics +// .allDomainsRegistered: registeredBackendCount() == 10). +pub fn all_domains_registered(count: Int) -> Int { + if count == expected_domain_count() { 1 } else { 0 } +} diff --git a/proposals/idaptik/migrated/Diagnostics/diagnostics.config.mjs b/proposals/idaptik/migrated/Diagnostics/diagnostics.config.mjs new file mode 100644 index 0000000..ca11566 --- /dev/null +++ b/proposals/idaptik/migrated/Diagnostics/diagnostics.config.mjs @@ -0,0 +1,25 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-parity config for Diagnostics.affine (idaptik health-band classifier + +// registry sanity check; scalar i32 ABI). Oracle re-derives the <70 / <90 / else +// ladder and the ==10 registry check. +export default { + affine: "Diagnostics.affine", + cases: [ + { name: "health_band_count()", export: "health_band_count", args: [], oracle: () => 3 }, + { name: "expected_domain_count()", export: "expected_domain_count", args: [], oracle: () => 10 }, + { + name: "health_of over [-5..105]", + export: "health_of", + args: [[-5, 105]], + oracle: (pct) => (pct < 70 ? 0 : pct < 90 ? 1 : 2), + }, + { + name: "all_domains_registered over [0..15]", + export: "all_domains_registered", + args: [[0, 15]], + oracle: (count) => (count === 10 ? 1 : 0), + }, + ], +}; diff --git a/proposals/idaptik/migrated/EVIDENCE.adoc b/proposals/idaptik/migrated/EVIDENCE.adoc new file mode 100644 index 0000000..d9aafc1 --- /dev/null +++ b/proposals/idaptik/migrated/EVIDENCE.adoc @@ -0,0 +1,125 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += Cluster C1 — four-gate evidence (captured 2026-06-05) +:toc: macro + +[IMPORTANT] +==== +*Captured run of the 4-gate recipe over the eight cluster-C1 pure-integer +kernels.* Every number here is reproducible from this directory; the +re-run commands are in `README.adoc`. Toolchain: AffineScript compiler +`_build/default/bin/main.exe`, Deno 2.8.2, Agda 2.6.3, echo mirror at +`/tmp/mirror-boundary`. +==== + +toc::[] + +== Summary + +[cols="2,1,1,1,1",options="header"] +|=== +| Kernel | G1 compile | G2 parity | G3 boundary | G4 assail +| `DeviceType` | OK | 39/39 | LOSSLESS (12) | clean +| `PuzzleFormat` | OK | 74/74 | CONTROLLED-LOSS @0 | clean +| `PortNames` | OK | 52/52 | LOSSLESS (10) | clean +| `GameEvent` | OK | 50/50 | LOSSLESS (6) + CL @0 | clean +| `Kernel_Compute` | OK | 736/736 | (decision; see note) | clean +| `Kernel` | OK | 19/19 | CONTROLLED-LOSS @4 | clean +| `RetryPolicy` | OK | 124/124 | (decision; see note) | clean +| `Diagnostics` | OK | 129/129 | (decision; see note) | clean +| *Total* | *8/8* | *1223/1223* | *6 proofs, agda exit 0* | *8/8 clean* +|=== + +== Gate 1 — compile (`main.exe compile … -o …`) + +All eight `.affine` sources lower to wasm, exit 0: + +---- +[OK] DeviceType [OK] GameEvent [OK] RetryPolicy +[OK] PuzzleFormat [OK] Kernel_Compute [OK] Diagnostics +[OK] PortNames [OK] Kernel +---- + +== Gate 2 — parity (oracle-vs-wasm, scalar i32 ABI) + +Each kernel swept against an *independent* JS oracle (re-derived in the +`*.config.mjs`, never reusing AffineScript code) so a codegen regression +surfaces as a differential mismatch. 1223 inputs, 0 mismatches. + +---- +DeviceType ........ 39/39 Kernel_Compute ... 736/736 +PuzzleFormat ...... 74/74 Kernel ........... 19/19 +PortNames ......... 52/52 RetryPolicy ...... 124/124 +GameEvent ......... 50/50 Diagnostics ...... 129/129 +---- + +`Kernel_Compute.compute_gate` is the widest sweep: the full +domain × active_calls × data_len × has_backend grid (10 × 4 × 9 × 2 = 720), +exercising the 504 > 413 > 404 > 0 precedence at every boundary. + +== Gate 3 — echo-boundary (Agda-certified encoding faithfulness) + +Six host-value→code tables certified against the `EchoEncodingFaithfulness` +framework; every generated module typechecks (`agda exit 0`). The generated +proofs are staged next to each kernel (`*Boundary.agda`). + +[cols="2,1,3",options="header"] +|=== +| Module | Verdict | What it certifies +| `DeviceTypeBoundary` | LOSSLESS | 12 device kinds → 12 distinct codes; host round-trips device ↔ code. +| `PortNamesBoundary` | LOSSLESS | 10 coprocessor domains → ids 0..9; the portnames.wasm bridge contract. +| `GameEventDirectionBoundary` | LOSSLESS | 6 directions → codes 0..5. +| `PuzzleFormatTierBoundary` | CONTROLLED LOSS | DLCLoader's `parseTier` clamp: unknown numeral collapses to `Tier0` (code 0). Collision certified → no section. +| `GameEventAlertBoundary` | CONTROLLED LOSS | ordered alert clamp: below-Green collapses to Green (code 0). Collision certified → no section. +| `KernelRouteBoundary` | CONTROLLED LOSS | the router's compute fan-in: six domains share handler class 4. Deliberate forgetting, certified → no section. +|=== + +*Note (decision kernels).* `Kernel_Compute.compute_gate`, +`RetryPolicy.is_transient` and `Diagnostics.health_of` are intentionally +many-to-one *decisions*, not encodings — they classify rather than name, so no +injectivity is claimed for them and echo-boundary's encoding lens does not +apply. Their faithfulness is established by Gate 2 (full-grid parity against an +independent oracle). Where one of these kernels *does* carry an encoding (the +shared domain code, the alert/tier taxonomies), that encoding is certified +above. + +== Gate 4 — affine-assail (no undeclared clamp / unguarded decoder) + +All eight kernels scan clean (exit 0): + +---- +[CLEAN] DeviceType [CLEAN] Kernel_Compute +[CLEAN] PuzzleFormat [CLEAN] Kernel +[CLEAN] PortNames [CLEAN] RetryPolicy +[CLEAN] GameEvent [CLEAN] Diagnostics +---- + +*On clamps and the gate-4 signal.* The in-band clamps in this cluster +(`PuzzleFormat.clamp_tier`/`clamp_difficulty` → 0, `GameEvent.clamp_alert_level` +→ 0/3) are written *guard-style* — an explicit validity test then the default — +rather than as a catch-all `match` arm. assail's `PA-AFF-001` heuristic targets +the match-arm shape (e.g. SecurityRank's `Invalid(v) => …`, which it correctly +flags as a declared clamp); guard-style clamps present no catch-all arm and so +scan clean. This is sound here because the controlled-loss of every one of these +clamps is *independently certified by Gate 3* (the `…Boundary.agda` proofs +above). Gate 3 (the clamp is controlled-loss-certified) and Gate 4 (no +*undeclared* match-arm clamp) together account for every boundary in the +cluster. The out-of-band *sentinels* (`-1` in DeviceType/PortNames/GameEvent/ +PuzzleFormat) are not clamps — they map outside the in-band range, so no in-band +collision is introduced and nothing is lost. + +== Host-side files (no pure-integer brain — the "senses") + +Three C1 files carry no extractable integer core and stay host-side: + +* `Coprocessor_Backends.res` — backend-registration wiring (ten `register()` + side-effects; the order is the only datum, and it is fixed). +* `PortNamesCoprocessor.res` — the JS-bridge binding shim that *consumes* + `PortNames.affine` (→ portnames.wasm). The shim stays; the kernel it binds is + delivered here. +* `DLCLoader.res` — a JSON parser/serialiser (`Js.String2.*` / `Js.Json.*` + throughout). Its one integer fragment, `parseTier`'s numeral clamp, is + delivered as `PuzzleFormat.clamp_tier` (certified controlled-loss above); the + rest is irreducibly string/JSON host work. (The Phase-B migratability tool + bucketed this MIGRATABLE-NOW because it scans the modern `String.*` API, not + the legacy `Js.String2.*` this file uses — recorded here as a triage erratum.) diff --git a/proposals/idaptik/migrated/GameEvent/GameEvent.affine b/proposals/idaptik/migrated/GameEvent/GameEvent.affine new file mode 100644 index 0000000..fb9cb9e --- /dev/null +++ b/proposals/idaptik/migrated/GameEvent/GameEvent.affine @@ -0,0 +1,72 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// GameEvent -- the cross-component event taxonomy co-processor, the pure-integer +// core extracted from idaptik shared/src/GameEvent.res. The ReScript original is +// a ~40-constructor event variant `t` carrying string/float/int payloads plus a +// `toTag` string serialiser; that variant and its string tags are irreducibly +// host-side (the senses). What IS pure integer are the two ordered/closed +// sub-enums the guard AI, firewall and event router actually branch on: +// +// * alertLevel (Green < Yellow < Orange < Red) -- ORDERED, so an out-of-band +// level clamps to the nearest valid rank (CONTROLLED LOSS, like +// SecurityRank); guards can never read an undefined alert state. +// * direction (PlayerToVM .. ServerBroadcast) -- a flat UNORDERED routing +// enum, so an out-of-band code maps to the sentinel -1 (LOSSLESS taxonomy). +// +// Per the DESIGN-VISION the host keeps every event payload and the `toTag` +// strings; AffineScript owns these two integer encodings. +// +//## alertLevel encoding (ordered) ## direction encoding (flat) +// code level code direction +// 0 Green 0 PlayerToVM +// 1 Yellow 1 VMToGame +// 2 Orange 2 GameToDevice +// 3 Red 3 DeviceToPlayer +// 4 PlayerToPlayer +// 5 ServerBroadcast + +enum Alert { Green, Yellow, Orange, Red, BadAlert(Int) } + +fn alert_of(code: Int) -> Alert { + if code == 0 { return Green; } + if code == 1 { return Yellow; } + if code == 2 { return Orange; } + if code == 3 { return Red; } + BadAlert(code) +} + +// Rank an alert level, clamping the ordered 0..3 band: anything below Green +// becomes 0, anything above Red becomes 3 (the nearest valid rank). This is the +// SecurityRank clamp shape -- a DECLARED controlled-loss clamp so guard AI can +// never act on an undefined alert state. +fn rank_alert(a: Alert) -> Int { + match a { + Green => 0, + Yellow => 1, + Orange => 2, + Red => 3, + BadAlert(v) => { if v < 0 { 0 } else { 3 } } + } +} + +pub fn alert_level_count() -> Int { 4 } +pub fn direction_count() -> Int { 6 } + +// Clamp a host integer onto the ordered alert band (DECLARED controlled loss). +pub fn clamp_alert_level(code: Int) -> Int { + rank_alert(alert_of(code)) +} + +// Whether a host integer names a defined alert level (before clamping). +pub fn is_valid_alert_level(code: Int) -> Int { + if code < 0 { 0 } else { if code > 3 { 0 } else { 1 } } +} + +// Direction is a flat routing enum with no order, so an out-of-band code maps +// to the sentinel -1 rather than clamping onto a real direction (LOSSLESS). +pub fn is_valid_direction(code: Int) -> Int { + if code < 0 { 0 } else { if code > 5 { 0 } else { 1 } } +} +pub fn clamp_direction(code: Int) -> Int { + if is_valid_direction(code) == 1 { code } else { -1 } +} diff --git a/proposals/idaptik/migrated/GameEvent/GameEventAlertBoundary.agda b/proposals/idaptik/migrated/GameEvent/GameEventAlertBoundary.agda new file mode 100644 index 0000000..dd26b40 --- /dev/null +++ b/proposals/idaptik/migrated/GameEvent/GameEventAlertBoundary.agda @@ -0,0 +1,83 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "Green": 0, +-- "Yellow": 1, +-- "Orange": 2, +-- "Red": 3, +-- "BelowGreen": 0 +-- } + +module GameEventAlertBoundary where + +open import Echo using (Echo) +open import EchoImageFactorization using (Injective) +open import EchoEncodingFaithfulness using (Encoding; module EncodingTheorems) + +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl) +open import Relation.Nullary using (¬_) + + +-- The host-side enumerated value (one constructor per table name). +-- c0 = Green +-- c1 = Yellow +-- c2 = Orange +-- c3 = Red +-- c4 = BelowGreen (out-of-band / clamp entry) +data Host : Set where + c0 c1 c2 c3 c4 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 +code c4 = 0 + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +module Theorems = EncodingTheorems encoding + +-- The collision, as data: two distinct host values collapse onto the +-- same code 0. +-- c0 = Green +-- c4 = BelowGreen (out-of-band / clamp) +-- Distinctness is constructor disjointness; the shared code is refl. +c0≢c4 : c0 ≢ c4 +c0≢c4 () + +collision : c0 ≢ c4 × code c0 ≡ code c4 +collision = c0≢c4 , refl + +-- THE VERDICT, certified: the boundary exhibits controlled loss. +-- The colliding fibre admits NO section -- there is no pure +-- decode : ℕ → Host recovering the host value from its code, +-- because two distinct host values share one code. The lost +-- distinction is named and localised at code 0. +boundary-controlled-loss : + ¬ Σ (ℕ → Host) (λ decode → ∀ x → decode (code x) ≡ x) +boundary-controlled-loss = + Theorems.encoding-collision⇒no-section + c0 c4 + c0≢c4 + refl + diff --git a/proposals/idaptik/migrated/GameEvent/GameEventDirectionBoundary.agda b/proposals/idaptik/migrated/GameEvent/GameEventDirectionBoundary.agda new file mode 100644 index 0000000..b47911e --- /dev/null +++ b/proposals/idaptik/migrated/GameEvent/GameEventDirectionBoundary.agda @@ -0,0 +1,80 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "PlayerToVM": 0, +-- "VMToGame": 1, +-- "GameToDevice": 2, +-- "DeviceToPlayer": 3, +-- "PlayerToPlayer": 4, +-- "ServerBroadcast": 5 +-- } + +module GameEventDirectionBoundary where + +open import Echo using (Echo) +open import EchoImageFactorization using (Injective) +open import EchoEncodingFaithfulness using (Encoding; module EncodingTheorems) + +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl) +open import Relation.Nullary using (¬_) + + +-- The host-side enumerated value (one constructor per table name). +-- c0 = PlayerToVM +-- c1 = VMToGame +-- c2 = GameToDevice +-- c3 = DeviceToPlayer +-- c4 = PlayerToPlayer +-- c5 = ServerBroadcast +data Host : Set where + c0 c1 c2 c3 c4 c5 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 +code c4 = 4 +code c5 = 5 + +-- Injectivity by exhaustive case analysis. The codes are literal +-- numerals, so listing the diagonal refl clauses is enough: Agda's +-- coverage checker discharges the off-diagonal pairs as absurd +-- numeral equalities (mirrors rankCode-injective). +code-injective : Injective code +code-injective {c0} {c0} _ = refl +code-injective {c1} {c1} _ = refl +code-injective {c2} {c2} _ = refl +code-injective {c3} {c3} _ = refl +code-injective {c4} {c4} _ = refl +code-injective {c5} {c5} _ = refl + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +-- Re-export the lossless-half headline, instantiated and proved: +-- every integer code determines its host value uniquely. +module Theorems = EncodingTheorems encoding + +boundary-lossless : + (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂ +boundary-lossless = Theorems.encoding-lossless code-injective + diff --git a/proposals/idaptik/migrated/GameEvent/gameevent.config.mjs b/proposals/idaptik/migrated/GameEvent/gameevent.config.mjs new file mode 100644 index 0000000..8f533cc --- /dev/null +++ b/proposals/idaptik/migrated/GameEvent/gameevent.config.mjs @@ -0,0 +1,19 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-parity config for GameEvent.affine (idaptik alertLevel + direction +// taxonomies; scalar i32 ABI). alertLevel clamps to nearest (ordered); +// direction maps out-of-band to -1 (flat). Oracles re-derive both. +const vAlert = (c) => c >= 0 && c <= 3; +const vDir = (c) => c >= 0 && c <= 5; +export default { + affine: "GameEvent.affine", + cases: [ + { name: "alert_level_count()", export: "alert_level_count", args: [], oracle: () => 4 }, + { name: "direction_count()", export: "direction_count", args: [], oracle: () => 6 }, + { name: "is_valid_alert_level over [-3..7]", export: "is_valid_alert_level", args: [[-3, 7]], oracle: (c) => (vAlert(c) ? 1 : 0) }, + { name: "clamp_alert_level over [-3..7]", export: "clamp_alert_level", args: [[-3, 7]], oracle: (c) => (vAlert(c) ? c : (c < 0 ? 0 : 3)) }, + { name: "is_valid_direction over [-3..9]", export: "is_valid_direction", args: [[-3, 9]], oracle: (c) => (vDir(c) ? 1 : 0) }, + { name: "clamp_direction over [-3..9]", export: "clamp_direction", args: [[-3, 9]], oracle: (c) => (vDir(c) ? c : -1) }, + ], +}; diff --git a/proposals/idaptik/migrated/Kernel/Kernel.affine b/proposals/idaptik/migrated/Kernel/Kernel.affine new file mode 100644 index 0000000..fc2aad7 --- /dev/null +++ b/proposals/idaptik/migrated/Kernel/Kernel.affine @@ -0,0 +1,55 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// Kernel -- the resource-aware scheduler gate + domain router, the pure-integer +// core extracted from idaptik shared/src/Kernel.res `execute`. The ReScript +// original returns a promise, reads device capacity and the +// backend registry through service locators, and mutates accounting state; we +// re-decompose by collapsing the Promise, threading the capacity check and +// backend-presence as integer parameters, and keeping only the two pure +// decisions: the pre-flight GATE (which status to reject with) and the domain +// ROUTE (which specialised handler to dispatch to). Accounting mutation, the +// string messages and the float energy totals stay host-side (the senses). +// +//## Domain encoding (the header contract for the JS host) -- PortNames order +// 0 crypto 1 vector 2 maths 3 io 4 neural +// 5 quantum 6 physics 7 audio 8 tensor 9 graphics +// +//## execute_gate status codes +// 503 resource exhausted (device capacity check failed) +// 404 no backend (no backend registered for the domain) +// 0 admit (proceed to routing + dispatch) +// +//## route_of handler classes +// 1 Kernel_IO (io) +// 2 Kernel_Crypto (crypto) +// 3 Kernel_Quantum (quantum) +// 4 Kernel_Compute (vector, maths, neural, physics, audio, tensor) +// 5 direct backend (graphics -- no specialised handler) +// 0 no route (out-of-band domain) +// route_of is deliberately many-to-one: the six compute domains all fold onto +// class 4. That fan-in is CONTROLLED LOSS by design (the router forgets which +// compute domain it was), certified by echo-boundary (boundary-route.json). + +// Pre-flight gate: the status execute returns before dispatch. has_capacity = 1 +// iff ResourceAccounting.hasCapacity(state); has_backend = 1 iff a backend is +// registered for the domain. Precedence is the ReScript order: capacity first. +pub fn execute_gate(has_capacity: Int, has_backend: Int) -> Int { + if has_capacity == 0 { return 503; } + if has_backend == 0 { return 404; } + 0 +} + +// Domain router: the specialised handler class a domain dispatches to. +pub fn route_of(domain: Int) -> Int { + if domain == 3 { return 1; } // io -> Kernel_IO + if domain == 0 { return 2; } // crypto -> Kernel_Crypto + if domain == 5 { return 3; } // quantum-> Kernel_Quantum + if domain == 1 { return 4; } // vector -> Kernel_Compute + if domain == 2 { return 4; } // maths -> Kernel_Compute + if domain == 4 { return 4; } // neural -> Kernel_Compute + if domain == 6 { return 4; } // physics-> Kernel_Compute + if domain == 7 { return 4; } // audio -> Kernel_Compute + if domain == 8 { return 4; } // tensor -> Kernel_Compute + if domain == 9 { return 5; } // graphics-> direct backend + 0 +} diff --git a/proposals/idaptik/migrated/Kernel/KernelRouteBoundary.agda b/proposals/idaptik/migrated/Kernel/KernelRouteBoundary.agda new file mode 100644 index 0000000..1d8cc75 --- /dev/null +++ b/proposals/idaptik/migrated/Kernel/KernelRouteBoundary.agda @@ -0,0 +1,98 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "crypto": 2, +-- "vector": 4, +-- "maths": 4, +-- "io": 1, +-- "neural": 4, +-- "quantum": 3, +-- "physics": 4, +-- "audio": 4, +-- "tensor": 4, +-- "graphics": 5 +-- } + +module KernelRouteBoundary where + +open import Echo using (Echo) +open import EchoImageFactorization using (Injective) +open import EchoEncodingFaithfulness using (Encoding; module EncodingTheorems) + +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl) +open import Relation.Nullary using (¬_) + + +-- The host-side enumerated value (one constructor per table name). +-- c0 = crypto +-- c1 = vector +-- c2 = maths +-- c3 = io +-- c4 = neural +-- c5 = quantum +-- c6 = physics +-- c7 = audio +-- c8 = tensor +-- c9 = graphics +data Host : Set where + c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 2 +code c1 = 4 +code c2 = 4 +code c3 = 1 +code c4 = 4 +code c5 = 3 +code c6 = 4 +code c7 = 4 +code c8 = 4 +code c9 = 5 + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +module Theorems = EncodingTheorems encoding + +-- The collision, as data: two distinct host values collapse onto the +-- same code 4. +-- c1 = vector +-- c2 = maths +-- Distinctness is constructor disjointness; the shared code is refl. +c1≢c2 : c1 ≢ c2 +c1≢c2 () + +collision : c1 ≢ c2 × code c1 ≡ code c2 +collision = c1≢c2 , refl + +-- THE VERDICT, certified: the boundary exhibits controlled loss. +-- The colliding fibre admits NO section -- there is no pure +-- decode : ℕ → Host recovering the host value from its code, +-- because two distinct host values share one code. The lost +-- distinction is named and localised at code 4. +boundary-controlled-loss : + ¬ Σ (ℕ → Host) (λ decode → ∀ x → decode (code x) ≡ x) +boundary-controlled-loss = + Theorems.encoding-collision⇒no-section + c1 c2 + c1≢c2 + refl + diff --git a/proposals/idaptik/migrated/Kernel/kernel.config.mjs b/proposals/idaptik/migrated/Kernel/kernel.config.mjs new file mode 100644 index 0000000..8a0a50a --- /dev/null +++ b/proposals/idaptik/migrated/Kernel/kernel.config.mjs @@ -0,0 +1,31 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-parity config for Kernel.affine (idaptik scheduler gate + domain +// router; scalar i32 ABI). Oracles re-derive the 503/404/0 pre-flight gate and +// the domain->handler-class routing table. +const route = (d) => { + if (d === 3) return 1; // io + if (d === 0) return 2; // crypto + if (d === 5) return 3; // quantum + if (d === 1 || d === 2 || d === 4 || d === 6 || d === 7 || d === 8) return 4; // compute + if (d === 9) return 5; // graphics direct + return 0; // out of band +}; +export default { + affine: "Kernel.affine", + cases: [ + { + name: "execute_gate over [0,1]^2", + export: "execute_gate", + args: [[0, 1], [0, 1]], + oracle: (cap, hb) => (cap === 0 ? 503 : hb === 0 ? 404 : 0), + }, + { + name: "route_of over [-2..12]", + export: "route_of", + args: [[-2, 12]], + oracle: (d) => route(d), + }, + ], +}; diff --git a/proposals/idaptik/migrated/Kernel_Compute/Kernel_Compute.affine b/proposals/idaptik/migrated/Kernel_Compute/Kernel_Compute.affine new file mode 100644 index 0000000..31c9be9 --- /dev/null +++ b/proposals/idaptik/migrated/Kernel_Compute/Kernel_Compute.affine @@ -0,0 +1,51 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// Kernel_Compute -- the compute-domain scheduler gate, the pure-integer core +// extracted from idaptik shared/src/Kernel_Compute.res `handleCompute`. The +// ReScript original returns a promise and dispatches to a +// backend; we re-decompose it by collapsing the incidental Promise, threading +// the service-locator reads (ResourceAccounting device state, the backend +// lookup) as explicit integer parameters, and keeping only the GATE decision -- +// which HTTP-style status the scheduler returns before any backend runs. The +// string messages and the actual backend.execute stay host-side (the senses). +// +//## Domain encoding (the header contract for the JS host) +// The host maps Coprocessor.Domain.t -> this code using PortNames order: +// 0 crypto 1 vector 2 maths 3 io 4 neural +// 5 quantum 6 physics 7 audio 8 tensor 9 graphics +// +//## Status codes returned by compute_gate +// 504 concurrency saturated (active calls >= max) +// 413 payload too large (data length > the domain's element cap) +// 404 no backend (the domain is unregistered on this device) +// 0 admit (dispatch to the backend) +// Precedence is exactly the ReScript order: concurrency, then payload, then +// backend presence. The caller passes has_backend as 1/0 (it owns the registry). + +// Maximum concurrent compute-domain calls per device before 504. +pub fn max_concurrent_compute() -> Int { 10 } + +// Per-domain input-array element cap (Kernel_Compute.dataLimitForDomain): +// vector | neural | audio -> 513 (n header + two 256-element vectors) +// maths | physics -> 16 (all commands take <= 4 small ints) +// tensor -> 259 (3 dimension ints + 16x16 matrix) +// anything else -> 1024 (catch-all fallback) +pub fn data_limit_for_domain(domain: Int) -> Int { + if domain == 1 { return 513; } // vector + if domain == 4 { return 513; } // neural + if domain == 7 { return 513; } // audio + if domain == 2 { return 16; } // maths + if domain == 6 { return 16; } // physics + if domain == 8 { return 259; } // tensor + 1024 +} + +// The scheduler gate: the status handleCompute returns before dispatch. +// active_calls = ResourceAccounting device active-call count (threaded in); +// data_len = input array length; has_backend = 1 iff a backend is registered. +pub fn compute_gate(domain: Int, active_calls: Int, data_len: Int, has_backend: Int) -> Int { + if active_calls >= max_concurrent_compute() { return 504; } + if data_len > data_limit_for_domain(domain) { return 413; } + if has_backend == 0 { return 404; } + 0 +} diff --git a/proposals/idaptik/migrated/Kernel_Compute/kernel_compute.config.mjs b/proposals/idaptik/migrated/Kernel_Compute/kernel_compute.config.mjs new file mode 100644 index 0000000..ccc2b23 --- /dev/null +++ b/proposals/idaptik/migrated/Kernel_Compute/kernel_compute.config.mjs @@ -0,0 +1,37 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-parity config for Kernel_Compute.affine (idaptik compute-domain +// scheduler gate; scalar i32 ABI). The oracle re-derives the per-domain element +// cap and the 504/413/404/0 precedence in plain JS. +const limit = (d) => + (d === 1 || d === 4 || d === 7) ? 513 : (d === 2 || d === 6) ? 16 : (d === 8) ? 259 : 1024; +export default { + affine: "Kernel_Compute.affine", + cases: [ + { name: "max_concurrent_compute()", export: "max_concurrent_compute", args: [], oracle: () => 10 }, + { + name: "data_limit_for_domain over [-2..12]", + export: "data_limit_for_domain", + args: [[-2, 12]], + oracle: (d) => limit(d), + }, + { + // domain x active_calls x data_len x has_backend = 10 x 4 x 9 x 2 = 720 inputs + name: "compute_gate grid (precedence: 504 > 413 > 404 > 0)", + export: "compute_gate", + args: [ + [0, 9], + [8, 11], + { values: [0, 16, 17, 259, 260, 513, 514, 1024, 1025] }, + [0, 1], + ], + oracle: (domain, active, len, hb) => { + if (active >= 10) return 504; + if (len > limit(domain)) return 413; + if (hb === 0) return 404; + return 0; + }, + }, + ], +}; diff --git a/proposals/idaptik/migrated/PortNames/PortNames.affine b/proposals/idaptik/migrated/PortNames/PortNames.affine new file mode 100644 index 0000000..55e4662 --- /dev/null +++ b/proposals/idaptik/migrated/PortNames/PortNames.affine @@ -0,0 +1,54 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// PortNames -- the coprocessor-domain port taxonomy co-processor, the +// pure-integer core behind public/assets/wasm/portnames.wasm that +// shared/src/PortNamesCoprocessor.res already binds via its JS bridge. This is +// the real consumer the bridge was written for: PortNamesCoprocessor exposes +// portCount / isCoprocessorPort / domainIndexOfPort / portOfDomainIndex as the +// integer half, and nameOfPort / portOfName as the host string half. Per the +// DESIGN-VISION the host keeps the port-name STRINGS and the ":in"/":out"/":ctrl" +// suffix concatenation; AffineScript owns the integer taxonomy. +// +// The ReScript original (PortNames.res) keeps a `coprocessorDomains` array of +// ten domain-prefix strings and tests membership with String.split + includes +// (a string op, host-side). We re-decompose the taxonomy as the canonical 0..9 +// integer the array order already implies, so membership is one range test and +// the port id IS the domain index. +// +//## Coprocessor-domain encoding (the header contract for the JS host) +// id domain id domain id domain +// 0 crypto 4 neural 8 tensor +// 1 vector 5 quantum 9 graphics +// 2 maths 6 physics +// 3 io 7 audio +// Order is PortNames.res `coprocessorDomains`. The encoding is LOSSLESS: ten +// distinct domains map to ten distinct ids (certified by echo-boundary, +// boundary.json). In this taxonomy the port id and the 0..9 domain index +// coincide -- there are exactly ten coprocessor ports, one per domain. An id +// outside 0..9 is not a coprocessor port: the predicate reports 0 and the index +// maps return the out-of-band sentinel -1. + +// The number of coprocessor-domain ports in the taxonomy (PortNamesCoprocessor +// `portCount`). +pub fn coprocessor_domain_count() -> Int { 10 } + +// Whether a port id targets a coprocessor domain (PortNamesCoprocessor +// `isCoprocessorPort`). 1 = yes, 0 = out of band. Mirrors PortNames.res +// `isCoprocessorPort` over the integer taxonomy instead of the string prefix. +pub fn is_coprocessor_port(id: Int) -> Int { + if id < 0 { 0 } else { if id > 9 { 0 } else { 1 } } +} + +// The 0..9 coprocessor-domain index of a port id, or -1 for a non-coprocessor +// id (PortNamesCoprocessor `domainIndexOfPort`). The id is the index in this +// taxonomy, so this is identity-with-sentinel. +pub fn domain_index_of_port(id: Int) -> Int { + if is_coprocessor_port(id) == 1 { id } else { -1 } +} + +// The canonical port id of a 0..9 coprocessor-domain index, or -1 if out of +// range (PortNamesCoprocessor `portOfDomainIndex`). Inverse of the above; on +// the valid band it is the identity, so the pair round-trips losslessly. +pub fn port_of_domain_index(idx: Int) -> Int { + if is_coprocessor_port(idx) == 1 { idx } else { -1 } +} diff --git a/proposals/idaptik/migrated/PortNames/PortNamesBoundary.agda b/proposals/idaptik/migrated/PortNames/PortNamesBoundary.agda new file mode 100644 index 0000000..2a106f1 --- /dev/null +++ b/proposals/idaptik/migrated/PortNames/PortNamesBoundary.agda @@ -0,0 +1,96 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "crypto": 0, +-- "vector": 1, +-- "maths": 2, +-- "io": 3, +-- "neural": 4, +-- "quantum": 5, +-- "physics": 6, +-- "audio": 7, +-- "tensor": 8, +-- "graphics": 9 +-- } + +module PortNamesBoundary where + +open import Echo using (Echo) +open import EchoImageFactorization using (Injective) +open import EchoEncodingFaithfulness using (Encoding; module EncodingTheorems) + +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl) +open import Relation.Nullary using (¬_) + + +-- The host-side enumerated value (one constructor per table name). +-- c0 = crypto +-- c1 = vector +-- c2 = maths +-- c3 = io +-- c4 = neural +-- c5 = quantum +-- c6 = physics +-- c7 = audio +-- c8 = tensor +-- c9 = graphics +data Host : Set where + c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 +code c4 = 4 +code c5 = 5 +code c6 = 6 +code c7 = 7 +code c8 = 8 +code c9 = 9 + +-- Injectivity by exhaustive case analysis. The codes are literal +-- numerals, so listing the diagonal refl clauses is enough: Agda's +-- coverage checker discharges the off-diagonal pairs as absurd +-- numeral equalities (mirrors rankCode-injective). +code-injective : Injective code +code-injective {c0} {c0} _ = refl +code-injective {c1} {c1} _ = refl +code-injective {c2} {c2} _ = refl +code-injective {c3} {c3} _ = refl +code-injective {c4} {c4} _ = refl +code-injective {c5} {c5} _ = refl +code-injective {c6} {c6} _ = refl +code-injective {c7} {c7} _ = refl +code-injective {c8} {c8} _ = refl +code-injective {c9} {c9} _ = refl + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +-- Re-export the lossless-half headline, instantiated and proved: +-- every integer code determines its host value uniquely. +module Theorems = EncodingTheorems encoding + +boundary-lossless : + (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂ +boundary-lossless = Theorems.encoding-lossless code-injective + diff --git a/proposals/idaptik/migrated/PortNames/portnames.config.mjs b/proposals/idaptik/migrated/PortNames/portnames.config.mjs new file mode 100644 index 0000000..e05f980 --- /dev/null +++ b/proposals/idaptik/migrated/PortNames/portnames.config.mjs @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-parity config for PortNames.affine (idaptik coprocessor-domain port +// taxonomy = portnames.wasm; scalar i32 ABI). Oracle re-derives the 0..9 band +// the PortNamesCoprocessor.js bridge contract expects. +const valid = (id) => id >= 0 && id <= 9; +export default { + affine: "PortNames.affine", + cases: [ + { name: "coprocessor_domain_count()", export: "coprocessor_domain_count", args: [], oracle: () => 10 }, + { name: "is_coprocessor_port over [-3..13]", export: "is_coprocessor_port", args: [[-3, 13]], oracle: (id) => (valid(id) ? 1 : 0) }, + { name: "domain_index_of_port over [-3..13]", export: "domain_index_of_port", args: [[-3, 13]], oracle: (id) => (valid(id) ? id : -1) }, + { name: "port_of_domain_index over [-3..13]", export: "port_of_domain_index", args: [[-3, 13]], oracle: (idx) => (valid(idx) ? idx : -1) }, + ], +}; diff --git a/proposals/idaptik/migrated/PuzzleFormat/PuzzleFormat.affine b/proposals/idaptik/migrated/PuzzleFormat/PuzzleFormat.affine new file mode 100644 index 0000000..b121298 --- /dev/null +++ b/proposals/idaptik/migrated/PuzzleFormat/PuzzleFormat.affine @@ -0,0 +1,60 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// PuzzleFormat -- the puzzle difficulty/tier taxonomy co-processor, the +// pure-integer core extracted from idaptik shared/src/PuzzleFormat.res (the +// `difficulty` and `tier` variants + `tierToInt`) AND from shared/src/ +// DLCLoader.res (the `parseTier` / `parseDifficulty` clamps). Per the +// DESIGN-VISION, the JS host keeps every difficulty/tier STRING and the puzzle +// JSON; AffineScript owns the canonical integer encoding and the loader's clamp. +// +// Two distinct boundary behaviours live here, and the split is the whole point: +// +// * difficulty/tier ENCODING is LOSSLESS -- PuzzleFormat.res's `tierToInt` +// maps Tier0..Tier4 -> 0..4 injectively, and difficulty maps +// Beginner..Expert -> 0..3 injectively. is_valid_* reports membership and +// *_to_int re-emits the code unchanged. +// +// * the loader's parseTier / parseDifficulty CLAMP is CONTROLLED LOSS -- an +// unrecognised numeral collapses to Tier0 / Beginner (code 0). This is a +// DECLARED clamp (DLCLoader chose a forgiving default); clamp_tier / +// clamp_difficulty reproduce it, and echo-boundary (boundary-tier.json) +// certifies the collision at code 0 as controlled loss. +// +//## Difficulty encoding ## Tier encoding +// code difficulty code tier +// 0 Beginner 0 Tier0 (register arithmetic) +// 1 Intermediate 1 Tier1 (+ conditionals) +// 2 Advanced 2 Tier2 (+ stack / memory) +// 3 Expert 3 Tier3 (+ subroutines) +// 4 Tier4 (+ I/O channels) + +pub fn difficulty_count() -> Int { 4 } +pub fn tier_count() -> Int { 5 } + +// Whether a host integer names a defined difficulty / tier. +pub fn is_valid_difficulty(code: Int) -> Int { + if code < 0 { 0 } else { if code > 3 { 0 } else { 1 } } +} +pub fn is_valid_tier(code: Int) -> Int { + if code < 0 { 0 } else { if code > 4 { 0 } else { 1 } } +} + +// The lossless half: PuzzleFormat.res's tierToInt is the identity on a valid +// tier code; difficulty likewise. We re-emit the code unchanged on a valid +// input and the out-of-band sentinel -1 otherwise (sentinel, not a clamp). +pub fn tier_to_int(code: Int) -> Int { + if is_valid_tier(code) == 1 { code } else { -1 } +} +pub fn difficulty_to_int(code: Int) -> Int { + if is_valid_difficulty(code) == 1 { code } else { -1 } +} + +// The controlled-loss half: DLCLoader.parseTier / parseDifficulty map any +// unrecognised numeral to Tier0 / Beginner (code 0). This DECLARED clamp +// collapses every out-of-band input onto in-band code 0. +pub fn clamp_tier(code: Int) -> Int { + if is_valid_tier(code) == 1 { code } else { 0 } +} +pub fn clamp_difficulty(code: Int) -> Int { + if is_valid_difficulty(code) == 1 { code } else { 0 } +} diff --git a/proposals/idaptik/migrated/PuzzleFormat/PuzzleFormatTierBoundary.agda b/proposals/idaptik/migrated/PuzzleFormat/PuzzleFormatTierBoundary.agda new file mode 100644 index 0000000..80bae7c --- /dev/null +++ b/proposals/idaptik/migrated/PuzzleFormat/PuzzleFormatTierBoundary.agda @@ -0,0 +1,86 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "Tier0": 0, +-- "Tier1": 1, +-- "Tier2": 2, +-- "Tier3": 3, +-- "Tier4": 4, +-- "UnknownTier": 0 +-- } + +module PuzzleFormatTierBoundary where + +open import Echo using (Echo) +open import EchoImageFactorization using (Injective) +open import EchoEncodingFaithfulness using (Encoding; module EncodingTheorems) + +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl) +open import Relation.Nullary using (¬_) + + +-- The host-side enumerated value (one constructor per table name). +-- c0 = Tier0 +-- c1 = Tier1 +-- c2 = Tier2 +-- c3 = Tier3 +-- c4 = Tier4 +-- c5 = UnknownTier (out-of-band / clamp entry) +data Host : Set where + c0 c1 c2 c3 c4 c5 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 +code c4 = 4 +code c5 = 0 + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +module Theorems = EncodingTheorems encoding + +-- The collision, as data: two distinct host values collapse onto the +-- same code 0. +-- c0 = Tier0 +-- c5 = UnknownTier (out-of-band / clamp) +-- Distinctness is constructor disjointness; the shared code is refl. +c0≢c5 : c0 ≢ c5 +c0≢c5 () + +collision : c0 ≢ c5 × code c0 ≡ code c5 +collision = c0≢c5 , refl + +-- THE VERDICT, certified: the boundary exhibits controlled loss. +-- The colliding fibre admits NO section -- there is no pure +-- decode : ℕ → Host recovering the host value from its code, +-- because two distinct host values share one code. The lost +-- distinction is named and localised at code 0. +boundary-controlled-loss : + ¬ Σ (ℕ → Host) (λ decode → ∀ x → decode (code x) ≡ x) +boundary-controlled-loss = + Theorems.encoding-collision⇒no-section + c0 c5 + c0≢c5 + refl + diff --git a/proposals/idaptik/migrated/PuzzleFormat/puzzleformat.config.mjs b/proposals/idaptik/migrated/PuzzleFormat/puzzleformat.config.mjs new file mode 100644 index 0000000..54f77ec --- /dev/null +++ b/proposals/idaptik/migrated/PuzzleFormat/puzzleformat.config.mjs @@ -0,0 +1,21 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-parity config for PuzzleFormat.affine (idaptik difficulty/tier +// taxonomy + DLCLoader clamp; scalar i32 ABI). Oracles re-derive both the +// lossless *_to_int identity and the controlled-loss clamp_* default. +const vTier = (c) => c >= 0 && c <= 4; +const vDiff = (c) => c >= 0 && c <= 3; +export default { + affine: "PuzzleFormat.affine", + cases: [ + { name: "difficulty_count()", export: "difficulty_count", args: [], oracle: () => 4 }, + { name: "tier_count()", export: "tier_count", args: [], oracle: () => 5 }, + { name: "is_valid_difficulty over [-3..8]", export: "is_valid_difficulty", args: [[-3, 8]], oracle: (c) => (vDiff(c) ? 1 : 0) }, + { name: "is_valid_tier over [-3..8]", export: "is_valid_tier", args: [[-3, 8]], oracle: (c) => (vTier(c) ? 1 : 0) }, + { name: "tier_to_int over [-3..8]", export: "tier_to_int", args: [[-3, 8]], oracle: (c) => (vTier(c) ? c : -1) }, + { name: "difficulty_to_int over [-3..8]", export: "difficulty_to_int", args: [[-3, 8]], oracle: (c) => (vDiff(c) ? c : -1) }, + { name: "clamp_tier over [-3..8]", export: "clamp_tier", args: [[-3, 8]], oracle: (c) => (vTier(c) ? c : 0) }, + { name: "clamp_difficulty over [-3..8]", export: "clamp_difficulty", args: [[-3, 8]], oracle: (c) => (vDiff(c) ? c : 0) }, + ], +}; diff --git a/proposals/idaptik/migrated/README.adoc b/proposals/idaptik/migrated/README.adoc new file mode 100644 index 0000000..ce7fe50 --- /dev/null +++ b/proposals/idaptik/migrated/README.adoc @@ -0,0 +1,113 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += idaptik migration — staged kernels (Phase C, cluster C1) +:toc: macro + +[IMPORTANT] +==== +*Staged, four-gate-verified, applyable units — not yet applied.* Per the +migration plan's access gate, idaptik-bound work lands here under +`proposals/idaptik/migrated//` until idaptik is opened for writes or the +owner accepts the staged patches. "Migrated" here means *re-decomposed + +compiled + parity-green + boundary-certified + assail-clean + staged*. + +Each kernel is the pure-integer *brain* of an idaptik `shared/src/*.res` +module: the host (JS/Pixi/ReScript) keeps the strings, floats, DOM, network +and mutable service state (the *senses*); AffineScript owns the integer +arithmetic and crosses the wasm boundary in primitives. See +`../../nextgen-evangelist/affine-parity/README.adoc` for the scalar-i32 ABI. +==== + +toc::[] + +== What landed + +Cluster C1 = the eleven `shared/src/*.res` leaf files. Eight have a +pure-integer brain and are delivered here; three are host-side "senses" with no +brain to extract (see `EVIDENCE.adoc` § Host-side files). + +[cols="2,3,2",options="header"] +|=== +| Kernel | Brain (what crosses the boundary) | Source `shared/src/*.res` +| `DeviceType` | 12-device taxonomy: count, validity, code-clamp (lossless, -1 sentinel) | `DeviceType.res` +| `PuzzleFormat` | difficulty(4)/tier(5) encodings + DLCLoader's clamp-to-default | `PuzzleFormat.res` (+ `DLCLoader.res`) +| `PortNames` | 10 coprocessor-domain port taxonomy = portnames.wasm | `PortNames.res` (bound by `PortNamesCoprocessor.res`) +| `GameEvent` | alertLevel(4, ordered clamp) + direction(6, flat) | `GameEvent.res` +| `Kernel_Compute` | per-domain element caps + the 504/413/404/0 scheduler gate | `Kernel_Compute.res` +| `Kernel` | the 503/404/0 pre-flight gate + domain→handler router | `Kernel.res` +| `RetryPolicy` | the 503/504/429 transient classifier + 3-policy config table | `RetryPolicy.res` +| `Diagnostics` | the <70/<90/≥90 health-band classifier + registry sanity check | `Diagnostics.res` +|=== + +Verification status: *all four gates green* — 8/8 compile, 1223/1223 parity, +6 echo-boundary proofs (agda exit 0), 8/8 assail-clean. Captured in +`EVIDENCE.adoc`. + +== Layout (per kernel) + +---- +/ + .affine re-decomposed pure-integer kernel (the deliverable) + .config.mjs affine-parity oracle config (gate 2) + Boundary.agda generated echo-boundary proof, where applicable (gate 3) +---- + +Compiled `*.wasm` is build output (regenerated by every parity run) and is +git-ignored; see `.gitignore`. + +== Re-running the gates + +From this directory, with the prebuilt compiler at +`/home/user/affinescript/_build/default/bin/main.exe`, Deno, and (for gate 3) +Agda + the echo mirror at `/tmp/mirror-boundary`: + +[source,console] +---- +# Gate 1 — compile +C=/home/user/affinescript/_build/default/bin/main.exe +$C compile DeviceType/DeviceType.affine -o DeviceType/DeviceType.wasm + +# Gate 2 — parity (recompiles, then sweeps every export vs its oracle) +P=../../nextgen-evangelist/affine-parity/parity.mjs +deno run --allow-read --allow-run $P DeviceType/devicetype.config.mjs + +# Gate 3 — echo-boundary (Agda-certify an encoding table) +B=../../nextgen-evangelist/echo-boundary/boundary.mjs +deno run --allow-read --allow-write --allow-run --allow-env $B \ + --name DeviceTypeBoundary --out DeviceType/DeviceTypeBoundary.agda \ + '{"Laptop":0,"Desktop":1,"Server":2,"Router":3,"Switch":4,"Firewall":5,"Camera":6,"AccessPoint":7,"PatchPanel":8,"PowerSupply":9,"PhoneSystem":10,"FibreHub":11}' + +# Gate 4 — assail (weak-point scan; exit 1 on any undeclared clamp) +A=../../nextgen-evangelist/affine-assail/assail.mjs +deno run --allow-read $A DeviceType/DeviceType.affine +---- + +The per-kernel config names are `devicetype`, `puzzleformat`, `portnames`, +`gameevent`, `kernel_compute`, `kernel`, `retrypolicy`, `diagnostics`. + +== The re-decomposition (not a transliteration) + +Per the migration playbook these are re-decompositions, not 1:1 ports: + +* *Promise/async collapsed.* `Kernel.execute` / `Kernel_Compute.handleCompute` + return `promise`; the brain keeps only the synchronous status + *decision*, leaving the await + dispatch host-side. +* *Service-locator state threaded as parameters.* `ResourceAccounting` + device-state reads and the backend-registry lookup become explicit integer + args (`active_calls`, `has_backend`, `has_capacity`) — no module-level mutable + state crosses the boundary. +* *Variants re-encoded as closed integer bands.* device type, difficulty, tier, + alert level, direction, domain — "the integer IS the X"; the strings stay in + the host. +* *Floats kept in the senses.* `Diagnostics.healthOf` takes a floored integer + percentage; `RetryPolicy`'s float backoff factor crosses as a percent (×100). + Wall-clock timing (`setTimeout`) stays host-side — per the determinism model, + timing is a sense, not a brain. + +== Applying (later, gated) + +When idaptik is opened for writes (Phase Ω), each `.affine` compiles to +`public/assets/wasm/.wasm`, the host `*Coprocessor.res` bridge is wired to +it behind a `FeaturePacks` flag, and the corresponding `shared/src/*.res` +integer logic is retired. `PortNames` is the immediate candidate — its bridge +(`PortNamesCoprocessor.res`) already exists and references `portnames.wasm`. diff --git a/proposals/idaptik/migrated/RetryPolicy/RetryPolicy.affine b/proposals/idaptik/migrated/RetryPolicy/RetryPolicy.affine new file mode 100644 index 0000000..d91f10f --- /dev/null +++ b/proposals/idaptik/migrated/RetryPolicy/RetryPolicy.affine @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// RetryPolicy -- the transient-failure classifier + backoff-policy table, the +// pure-integer core extracted from idaptik shared/src/RetryPolicy.res. The +// ReScript original couples the retry DECISION (is a status worth retrying?) and +// the retry CONFIG (max retries, base delay, backoff factor) to the actual +// timed retry loop (setTimeout + promise recursion). We re-decompose by keeping +// the decision and the config -- both pure integer -- and leaving the timing +// (wall-clock delay + Promise scheduling) host-side, where per the +// multiplayer-determinism model wall-clock IS a sense, not a brain. +// +//## Transient status classification (RetryPolicy.isTransient) +// 503 resource exhausted, 504 compute saturated, 429 rate-limited -> transient +// everything else (0 ok, 400/402/404/413 permanent) -> not +// +//## Policy table (the three built-in policies, encoded by policy code) +// policy name max_retries base_delay_ms backoff_factor_pct +// 0 default 3 50 200 (2.0x) +// 1 fast 1 10 100 (1.0x) +// 2 patient 5 200 150 (1.5x) +// backoff_factor is carried as a percent (x100) so it stays a pure integer; the +// host divides by 100 when scheduling. Any unknown policy code falls back to +// default -- a DECLARED clamp onto policy 0 (controlled loss over the policy +// code, certified by echo-boundary boundary-policy.json). + +// 1 iff the status is a transient failure that may clear on retry. +pub fn is_transient(status: Int) -> Int { + if status == 503 { return 1; } + if status == 504 { return 1; } + if status == 429 { return 1; } + 0 +} + +// The number of built-in policies. +pub fn policy_count() -> Int { 3 } + +// Max re-attempts after the first failure, per policy code (unknown -> default). +pub fn policy_max_retries(policy: Int) -> Int { + if policy == 1 { return 1; } // fast + if policy == 2 { return 5; } // patient + 3 // default (policy 0 and the unknown clamp) +} + +// Base delay in ms before the first retry, per policy code (unknown -> default). +pub fn policy_base_delay_ms(policy: Int) -> Int { + if policy == 1 { return 10; } // fast + if policy == 2 { return 200; } // patient + 50 // default +} + +// Backoff multiplier as a percent (x100), per policy code (unknown -> default). +pub fn policy_backoff_factor_pct(policy: Int) -> Int { + if policy == 1 { return 100; } // fast (1.0x) + if policy == 2 { return 150; } // patient(1.5x) + 200 // default(2.0x) +} diff --git a/proposals/idaptik/migrated/RetryPolicy/retrypolicy.config.mjs b/proposals/idaptik/migrated/RetryPolicy/retrypolicy.config.mjs new file mode 100644 index 0000000..570bd78 --- /dev/null +++ b/proposals/idaptik/migrated/RetryPolicy/retrypolicy.config.mjs @@ -0,0 +1,28 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-parity config for RetryPolicy.affine (idaptik transient classifier + +// policy table; scalar i32 ABI). Oracles re-derive the 503/504/429 transient +// set and the three built-in policies (unknown code -> default). +const transient = (s) => (s === 503 || s === 504 || s === 429 ? 1 : 0); +export default { + affine: "RetryPolicy.affine", + cases: [ + { + name: "is_transient over [420..510]", + export: "is_transient", + args: [[420, 510]], + oracle: (s) => transient(s), + }, + { + name: "is_transient over the canonical status set", + export: "is_transient", + args: [{ values: [0, 200, 400, 402, 404, 413, 429, 500, 503, 504, 599] }], + oracle: (s) => transient(s), + }, + { name: "policy_count()", export: "policy_count", args: [], oracle: () => 3 }, + { name: "policy_max_retries over [-1..5]", export: "policy_max_retries", args: [[-1, 5]], oracle: (p) => (p === 1 ? 1 : p === 2 ? 5 : 3) }, + { name: "policy_base_delay_ms over [-1..5]", export: "policy_base_delay_ms", args: [[-1, 5]], oracle: (p) => (p === 1 ? 10 : p === 2 ? 200 : 50) }, + { name: "policy_backoff_factor_pct over [-1..5]", export: "policy_backoff_factor_pct", args: [[-1, 5]], oracle: (p) => (p === 1 ? 100 : p === 2 ? 150 : 200) }, + ], +};