diff --git a/proposals/MIGRATION-PLAN.adoc b/proposals/MIGRATION-PLAN.adoc index a8acb56..8c268c4 100644 --- a/proposals/MIGRATION-PLAN.adoc +++ b/proposals/MIGRATION-PLAN.adoc @@ -190,6 +190,8 @@ Heuristic: | 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. | D (C2 wave 1) | DONE | Deep wave 2 (2026-06-05, Opus). Cluster C2 *wave 1* — the reversible VM value-transform opcodes — re-decomposed into *4 kernels* under `proposals/idaptik/migrated/` (VmArith, VmBitwise, VmAncilla, VmInstruction), covering 11 opcodes (Add/Sub/Negate/Noop/Swap/Flip/Xor/Rol/Ror/And/Or) + the 23-opcode taxonomy. Brain = the reversible scalar-int value transform per opcode; the register-name dict stays host-side. *Reversibility (`invert∘execute = id`) pinned as `*_roundtrip` exports.* *Four gates green:* 4/4 compile, 2100/2100 parity (incl. every round-trip, over i32 extremes), 1 echo-boundary LOSSLESS (23-opcode encoding, agda exit 0), 4/4 assail-clean. Evidence: `migrated/EVIDENCE-C2.adoc`. Surfaced 3 compiler facts: unary `~` codegen bug (workaround `-a-1`), arithmetic `>>` + no `>>>` (logical-shift-right emulated). NEXT: C2 wave 2. +| C6+C8 (fan-out) | DONE | Parallel deep wave (2026-06-05): two Sonnet agents migrated clusters C6 (combat/enemy) + C8 (device/network); parent re-verified + consolidated. *16 kernels* staged under `proposals/idaptik/migrated/` — C6: CombatFx, Detection, DifficultyScale, Distraction, DualAlert, HitboxGeom, PlayerHp, SecurityAi; C8: GlobalNetworkData, NetworkManager, SecurityRank, DeviceCaps, LaptopState, NetworkTransfer, PowerManager, CovertLink. *Four gates green (re-run by parent, not just agent-reported):* 16/16 compile, *34280/34280 parity* (C6 8185 + C8 26095, independent oracles), 7 echo-boundary LOSSLESS proofs, 16/16 assail-clean. Re-verification CAUGHT 3 PA-AFF-001 findings the agent reports missed (SecurityAi, SecurityRank, NetworkManager) — fixed with the established guard-helper clamp declaration; NetworkManager parity held at 2645/2645 after dropping the dead `Cat` enum, confirming semantics preserved. *4th compiler finding:* Float→wasm codegen broadly incomplete (pub-fn exports always type i32; float-literal operands mis-emit; `trunc()`/`float()` absent) — drives the `*Int.affine` parity subsets, keeps floats host-side. Evidence: `migrated/EVIDENCE-C6.adoc` + `EVIDENCE-C8.adoc`. NEXT: complete C7, then C2 wave 2. +| C7 | TODO | Player cluster: 8 `.affine` drafts staged (CriticalRoll, PlayerAttributes, QCertifications, SkillRank, SkillAbilities, QPrograms, JessicaLoadout, JessicaBackground) but the agent timed out *before* writing any parity config or evidence — *unverified, deliberately NOT landed*. Finish the 4 gates over the existing drafts (independent oracles → parity/boundary/assail), then stage. Drafts left untracked in the working tree as the head-start. | C2b+ | TODO | C2 wave 2 (needs an array/linear-memory ABI): Mul/Div, the stack/memory opcodes (Push/Pop/Load/Store), control flow (Call/Loop/IfPos/IfZero), I/O (Send/Recv/CoprocessorCall), and the structural VM files (State, VM, SubroutineRegistry, *Coprocessor, bindings). Then C3..C12. The unary-`~` codegen bug is a candidate Phase-F compiler fix. | F+ | TODO | Compiler walls (string backend, then effects). | Ω | TODO (access-gated) | Cutover + ReScript extinction. diff --git a/proposals/idaptik/migrated/CombatFx/CombatFx.affine b/proposals/idaptik/migrated/CombatFx/CombatFx.affine new file mode 100644 index 0000000..d03ec4e --- /dev/null +++ b/proposals/idaptik/migrated/CombatFx/CombatFx.affine @@ -0,0 +1,166 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// CombatFx -- the render-decision co-processor for the combat FX scattered +// across the player, combat and training subsystems. Extracted from +// src/app/combat/CombatFxLogicCoprocessor.res (the wasm binding shim) whose +// upstream implementation lives in the original combatfxlogic.wasm. +// +// Per the DESIGN-VISION ("AffineScript is the brain, Pixi the senses; only +// primitives cross the wasm boundary"), every AnimatedSprite.setTint, +// Container.setAlpha, Text.make, Motion.animate and hex palette entry stays in +// ReScript. This co-processor owns only the scalar arithmetic that decides WHAT +// the FX should be this frame; the host feeds each result straight to a draw +// call, so the observable picture is identical while the decision now lives in +// wasm. +// +//## Compiler note: no trunc/float built-ins in wasm codegen +// `trunc(x)` and `float(n)` resolve at the type-checking stage but are absent +// from the wasm code-generator. Both are replaced by proved loop idioms from +// the estate playbook: +// floor_pos(x) -- counts how many whole 1.0s fit below x (non-negative x) +// int_to_float_s(n) -- counts up from 0.0 n times (small non-negative n) +// These lower correctly via i32/f64 Wasm instructions. +// +//## Boundary contract (the header the JS host relies on) +// flash_cycle(timer, period) -> Int +// floor(timer / period): shared cycle index for both flash routines. +// flash_on_phase(timer, period, on_frac) -> Int +// 1 while within the on-window of the current cycle, else 0. +// Host passes period=0.2, on_frac=0.1 to match PlayerSprite exactly. +// flash_alpha_phase(timer, period) -> Float +// 1.0 on even cycle, 0.3 on odd; host passes period=0.1 (PlayerGraphics). +// flash_alpha_phase_v(timer, period, hi, lo) -> Float +// As flash_alpha_phase but with host-supplied hi/lo alpha values. +// flash_is_even_cycle(timer, period) -> Int +// 1 when cycle index is even, 0 when odd. +// flash_advance(timer, dt) -> Float +// timer + dt: per-frame accumulation while invincibility is active. +// flash_reset() -> Float +// 0.0: timer reset when invincibility expires. +// floattext_start_y(y, off) -> Float +// y - off: spawn Y for damage/pickup floating text (off = 40.0). +// floattext_end_y(y, rise) -> Float +// y - rise: rise/fade target Y (rise = 100.0). +// floattext_rise_distance(start_off, rise) -> Float +// rise - start_off: total vertical travel independent of y (= 60.0 default). +// knockback_pop_y(speed) -> Float +// 0.0 - speed: upward pop magnitude; up is negative Y; host passes 80.0. + +//## floor_pos: non-negative float -> integer floor +// Counts how many whole 1.0s fit below x. Used instead of trunc() which is +// absent from the wasm code-generator. For the timer/period quotients here +// (order of magnitude 0..~500) the loop completes in microseconds. +fn floor_pos(x: Float) -> Int { + let mut n = 0; + let mut acc = 0.0; + while acc + 1.0 <= x { acc = acc + 1.0; n = n + 1; } + n +} + +//## int_to_float_s: small non-negative Int -> Float +// Counts from 0.0 up to n. Used instead of float() which is absent from the +// wasm code-generator. For the cycle indices here (order of magnitude 0..~500) +// the loop completes in microseconds. +fn int_to_float_s(n: Int) -> Float { + let mut f = 0.0; + let mut i = 0; + while i < n { f = f + 1.0; i = i + 1; } + f +} + +//## PlayerSprite / PlayerGraphics -- shared flash cycle index +// Both flash routines compute floor(timer / period): PlayerSprite uses period=0.2 +// (the full red-tint cycle), PlayerGraphics uses period=0.1 (the alpha cycle). +// This kernel is the shared implementation; the host chooses the period. +pub fn flash_cycle(timer: Float, period: Float) -> Int { + floor_pos(timer / period) +} + +//## PlayerSprite.updateDamageFlash -- red-tint on/off phase +// remainder = timer - floor(timer/period) * period; on when remainder < on_frac. +// Reconstructed without a float modulo (unsupported for variables in this backend) +// using floor_pos + int_to_float_s. The host passes period=0.2, on_frac=0.1 to +// match PlayerSprite exactly (first half of each 0.2 s cycle is the on-window). +pub fn flash_on_phase(timer: Float, period: Float, on_frac: Float) -> Int { + let cycles = floor_pos(timer / period); + let remainder = timer - int_to_float_s(cycles) * period; + if remainder < on_frac { return 1; } + 0 +} + +//## PlayerGraphics.updateDamageFlash -- container-alpha flicker (cycle parity) +// alpha = (floor(timer / period) mod 2 == 0) ? 1.0 : 0.3. +// Returns the f64 alpha directly so the host hands it straight to Container.setAlpha. +// The host passes period=0.1 to match PlayerGraphics exactly. +pub fn flash_alpha_phase(timer: Float, period: Float) -> Float { + let cycle = floor_pos(timer / period); + if cycle % 2 == 0 { return 1.0; } + 0.3 +} + +//## PlayerGraphics.updateDamageFlash -- alpha flicker, host-supplied magnitudes +// As flash_alpha_phase but with the two alpha values passed by the host, in case +// a render branch wants different on/off opacities while keeping the same parity +// decision. hi on even cycles, lo on odd. +pub fn flash_alpha_phase_v(timer: Float, period: Float, hi: Float, lo: Float) -> Float { + let cycle = floor_pos(timer / period); + if cycle % 2 == 0 { return hi; } + lo +} + +//## PlayerGraphics.updateDamageFlash -- the parity flag alone +// The discrete even/odd decision behind the alpha choice, returned as an Int flag +// for hosts that own both alpha magnitudes and only need the selector. +pub fn flash_is_even_cycle(timer: Float, period: Float) -> Int { + let cycle = floor_pos(timer / period); + if cycle % 2 == 0 { return 1; } + 0 +} + +//## PlayerSprite / PlayerGraphics -- effect-lifetime timer accumulation +// While the invincibility timer is positive both routines accumulate +// damageFlashTimer += deltaTime each frame; this kernel is that step. The host +// owns the > 0.0 guard and the mutable field; the brain owns the addition. +pub fn flash_advance(timer: Float, dt: Float) -> Float { + timer + dt +} + +//## PlayerSprite / PlayerGraphics -- flash-timer reset +// When the invincibility timer reaches zero both routines reset damageFlashTimer +// to 0.0 (and the host restores the base tint / full alpha). The value is a +// constant, lifted so the reset point is the same total kernel as the advance. +pub fn flash_reset() -> Float { + 0.0 +} + +//## ScavengerTraining.showFloatingText -- spawn Y +// The floating damage/pickup text is created at y - 40.0 (Text.setY(floatText, +// y - 40.0)). Generalised over the spawn offset; the host passes 40.0. +pub fn floattext_start_y(y: Float, off: Float) -> Float { + y - off +} + +//## ScavengerTraining.showFloatingText -- rise/fade target Y +// Motion.animate drives the text to y - 100.0 with alpha 0.0 over 1.5 s. This is +// the target Y of that tween; generalised over the rise, the host passes 100.0. +pub fn floattext_end_y(y: Float, rise: Float) -> Float { + y - rise +} + +//## ScavengerTraining.showFloatingText -- total vertical travel +// The distance the text drifts upward over its lifetime: (y - start_off) minus +// (y - rise) = rise - start_off. Independent of y, so the host can size the tween +// or a pooled effect without re-deriving it. With 40.0 / 100.0 this is 60.0. +pub fn floattext_rise_distance(start_off: Float, rise: Float) -> Float { + rise - start_off +} + +//## PlayerHP.takeDamage -- upward knockback pop +// On taking a hit the player gets a slight upward pop alongside the signed +// horizontal knockback (already migrated in PlayerHp). The original +// hard-codes knockbackVelY = -80.0; lifted as the negation of a host-supplied +// speed so the FX co-processor owns the sign convention (up is negative Y). +pub fn knockback_pop_y(speed: Float) -> Float { + 0.0 - speed +} diff --git a/proposals/idaptik/migrated/CombatFx/CombatFxInt.affine b/proposals/idaptik/migrated/CombatFx/CombatFxInt.affine new file mode 100644 index 0000000..e513cc7 --- /dev/null +++ b/proposals/idaptik/migrated/CombatFx/CombatFxInt.affine @@ -0,0 +1,25 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// CombatFxInt -- Integer-input parity subset of CombatFx.affine. +// For flash_cycle, flash_on_phase, flash_is_even_cycle: timer and period are +// passed as whole-number integers. The division timer/period is integer division +// which equals floor(timer/period) for non-negative integers, matching the +// Float-based floor_pos logic for these test inputs. + +pub fn flash_cycle_int(timer: Int, period: Int) -> Int { + timer / period +} + +pub fn flash_on_phase_int(timer: Int, period: Int, on_frac: Int) -> Int { + let cycles = timer / period; + let remainder = timer - cycles * period; + if remainder < on_frac { return 1; } + 0 +} + +pub fn flash_is_even_cycle_int(timer: Int, period: Int) -> Int { + let cycle = timer / period; + if cycle % 2 == 0 { return 1; } + 0 +} diff --git a/proposals/idaptik/migrated/CombatFx/combatfx.config.mjs b/proposals/idaptik/migrated/CombatFx/combatfx.config.mjs new file mode 100644 index 0000000..3ae2a5b --- /dev/null +++ b/proposals/idaptik/migrated/CombatFx/combatfx.config.mjs @@ -0,0 +1,48 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// affine-parity config for CombatFx.affine (Int-only parity subset). +// Points at CombatFxInt.affine which exposes only the Int-returning exports. +// Oracles re-derive from CombatFxLogicCoprocessor.res semantics in plain JS. + +export default { + affine: "CombatFxInt.affine", + compile: false, + // Integer-input variants: timer/period as whole-number integers. + // Integer division timer/period == floor(timer/period) for non-negative inputs, + // matching the Float floor_pos logic for these test cases. + cases: [ + { + name: "flash_cycle_int(timer, period): integer division = floor(float/float)", + export: "flash_cycle_int", + args: [ + { values: [0, 1, 2, 3, 4, 5, 6, 8, 10] }, + { values: [1, 2] }, + ], + oracle: (timer, period) => Math.floor(timer / period), + }, + { + name: "flash_on_phase_int(timer, period, on_frac): 1 within on-window", + export: "flash_on_phase_int", + args: [ + { values: [0, 1, 2, 3, 4, 5, 6, 8, 10] }, + { values: [1, 2] }, + { values: [0, 1, 2] }, + ], + oracle: (timer, period, on_frac) => { + const cycles = Math.floor(timer / period); + const remainder = timer - cycles * period; + return remainder < on_frac ? 1 : 0; + }, + }, + { + name: "flash_is_even_cycle_int(timer, period): 1 if even cycle", + export: "flash_is_even_cycle_int", + args: [ + { values: [0, 1, 2, 3, 4, 5, 6, 8, 10] }, + { values: [1, 2] }, + ], + oracle: (timer, period) => Math.floor(timer / period) % 2 === 0 ? 1 : 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/CovertLink/CovertLink.affine b/proposals/idaptik/migrated/CovertLink/CovertLink.affine new file mode 100644 index 0000000..26b3982 --- /dev/null +++ b/proposals/idaptik/migrated/CovertLink/CovertLink.affine @@ -0,0 +1,166 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2026 Joshua B. Jewell and Jonathan D.A. Jewell +// +// CovertLink -- the pure link-state/threshold/bandwidth kernel re-decomposed +// from src/app/devices/CovertLink.res. The ReScript original is a mutable record +// (id, endpoints, connectionType, state, stats, ttl, timeRemaining, a clutch of +// bool flags) plus a Registry dict, all entangled with string IDs, discovery +// hints, terminal formatting and per-frame effects. Per the DESIGN-VISION ("the +// brain is AffineScript, the senses are JS; only primitives cross the wasm +// boundary"), the mutable record and the dict are NOT the unit of migration. +// What crosses is the numeric/enum core: the connection-type stats table, the +// state-to-colour map, the IDS-visibility predicate, the constant covert +// latency, and the TTL relaxation arithmetic. The host keeps the record, the +// Registry dict, the string IDs/hints, every formatting routine and every +// effect (discover/activate/cut mutate the host's own state variant). +// +//## Why a stateless split, not a model in linear memory +// Every value the kernel returns is a pure function of an enum ordinal or of +// (remaining, dt). defaultStats and stateToColor are constant lookups keyed by +// the variant ordinal; isMonitored is a constant predicate over the same +// ordinal; getLatencyTicks is a literal. The only time-varying piece is the TTL +// countdown, and update's `newRemaining = remaining -. deltaSeconds` depends on +// nothing but the single remaining field the host already holds and passes back +// each frame. No accumulated history exists, so the cheaper stateless shape fits +// exactly, as PlayerHP and NetworkTransfer do with their host-held scalars. +// +//## What stays on the JS side (the senses, not the brain) +// The connectionType / discoveryMethod / connectionState variants carry no +// payload the arithmetic needs; only the variant TAG matters, so the host passes +// a small Int ordinal and keeps the variants themselves. The id/endpoint/hint +// strings, the activationItems array, the Registry dict, connectionTypeName / +// discoveryMethodName / stateToString / portName / formatInfo / formatShort / +// formatOverlay (all string work), and connects / hasEndpoint / otherEndpoint +// (string equality the host runs directly) all remain host-side. discover / +// activate / cut are single host-state writes guarded by a state check; the host +// performs them, consulting ttl_expired only to learn whether a frame's decay +// drove the link Dead. +// +//## Boundary contract (the header the JS host relies on) +// Stats and the colour cross as Int (they are integer-valued); the TTL values +// cross as f64 (proven to marshal both ways without truncation; cf. +// migration/bindings/NetworkTransfer.wasm). The connection-type tag and the +// state tag are small Ints. No strings, dicts, options or effects cross. +// type_bandwidth(ct: Int) -> Int 1..5, the defaultStats bandwidth column +// type_latency(ct: Int) -> Int 1..5, the defaultStats latency column +// type_stealth(ct: Int) -> Int 1..5, the defaultStats stealth column +// type_durability(ct: Int)-> Int 1..5, the defaultStats durability column +// ct is the connectionType ordinal 0..6: +// 0 DarkFibre 1 LegacyTrunk 2 OOBManagement 3 WirelessBridge +// 4 CrossConnect 5 MaintenanceVLAN 6 ImprovisedLink +// An out-of-band ct clamps to 0 for every column (an unknown substrate +// contributes nothing), defending a malformed host call. +// is_monitored(ct: Int) -> Int 1 when traffic is IDS/RF-visible, else 0. +// WirelessBridge (3) and MaintenanceVLAN (5) are monitored; all other +// canonical types, and any out-of-band ct, are stealthy (0). +// state_color(st: Int) -> Int the stateToColor swatch as a packed 0xRRGGBB. +// 0 Unknown 0x444444 1 Discovered 0xFFAA00 2 Active 0x00FF88 +// 3 Dead 0xFF2222 ; out-of-band -> Unknown's 0x444444. +// latency_ticks() -> Int the constant 1: a covert link is always one tick. +// ttl_step(remaining: Float, dt: Float) -> Float +// max(0.0, remaining -. dt): the update countdown, floored at zero so the +// Dead-frame pins timeRemaining at 0.0 exactly as the ReScript does. +// ttl_expired(remaining: Float, dt: Float) -> Int +// 1 when remaining -. dt <= 0.0 (the frame that drives the link Dead), +// else 0. The host reads this to apply its Active -> Dead state write. + +//## Connection-type stats table (defaultStats), one column per export +// The defaultStats switch decomposed into four ordinal-keyed lookups. Each is a +// guarded decode in the variant's declaration order; an out-of-band ordinal +// falls through to 0, the defended clamp. +pub fn type_bandwidth(ct: Int) -> Int { + if ct == 0 { return 5; } + if ct == 1 { return 4; } + if ct == 2 { return 2; } + if ct == 3 { return 3; } + if ct == 4 { return 4; } + if ct == 5 { return 3; } + if ct == 6 { return 1; } + 0 +} + +pub fn type_latency(ct: Int) -> Int { + if ct == 0 { return 5; } + if ct == 1 { return 4; } + if ct == 2 { return 3; } + if ct == 3 { return 2; } + if ct == 4 { return 4; } + if ct == 5 { return 3; } + if ct == 6 { return 1; } + 0 +} + +pub fn type_stealth(ct: Int) -> Int { + if ct == 0 { return 5; } + if ct == 1 { return 3; } + if ct == 2 { return 4; } + if ct == 3 { return 1; } + if ct == 4 { return 3; } + if ct == 5 { return 2; } + if ct == 6 { return 3; } + 0 +} + +pub fn type_durability(ct: Int) -> Int { + if ct == 0 { return 5; } + if ct == 1 { return 2; } + if ct == 2 { return 4; } + if ct == 3 { return 3; } + if ct == 4 { return 3; } + if ct == 5 { return 5; } + if ct == 6 { return 1; } + 0 +} + +//## IDS/RF visibility predicate (isMonitored) +// The isMonitored switch: WirelessBridge is RF-detectable, MaintenanceVLAN may +// carry vendor telemetry; every other canonical type is stealthy. An out-of-band +// ordinal is treated as stealthy (0), matching the conservative defended clamp. +pub fn is_monitored(ct: Int) -> Int { + if ct == 3 { return 1; } + if ct == 5 { return 1; } + 0 +} + +//## State-to-colour swatch (stateToColor) +// The stateToColor switch as a guarded decode returning the packed 0xRRGGBB int +// the overlay tints with. An out-of-band state falls through to Unknown's dark +// grey, the safe default for an unrecognised lifecycle value. +pub fn state_color(st: Int) -> Int { + if st == 0 { return 0x444444; } + if st == 1 { return 0xFFAA00; } + if st == 2 { return 0x00FF88; } + if st == 3 { return 0xFF2222; } + 0x444444 +} + +//## Constant covert latency (getLatencyTicks) +// Normal routing costs one tick per hop; a covert link always costs exactly one, +// regardless of the connection it tunnels. The literal lifts verbatim. +pub fn latency_ticks() -> Int { + 1 +} + +//## TTL countdown, floored at zero (update) +// update's `newRemaining = remaining -. deltaSeconds`, then the Dead branch pins +// timeRemaining at 0.0. max(0.0, remaining - dt) collapses both arms: it yields +// the live remaining while positive and exactly 0.0 once spent, matching the +// ReScript's Some(0.0) on expiry. Guard style (no max_float builtin available). +// Compiler note: `next < 0.0` triggers the float-literal wasm bug; `zero` is +// passed as a Float parameter (host passes 0) so the comparison is var-to-var. +pub fn ttl_step(remaining: Float, dt: Float, zero: Float) -> Float { + let next = remaining - dt; + if next < zero { zero } else { next } +} + +//## TTL expiry predicate (update's Dead transition) +// update flips the state to Dead when `newRemaining <= 0.0`. The host owns the +// state variant, so the kernel returns the boolean as a 1/0 Int for the host to +// branch on, reproducing the `<= 0.0` comparison exactly (an exact-zero frame +// counts as expired, as in the ReScript). +// Compiler note: `remaining - dt <= 0.0` fails wasm validation (f64.const as i32 +// operand bug); rewritten as `dt >= remaining` which is logically identical and +// uses only variable-to-variable comparison. +pub fn ttl_expired(remaining: Float, dt: Float) -> Int { + if dt >= remaining { 1 } else { 0 } +} diff --git a/proposals/idaptik/migrated/CovertLink/CovertLinkConnectionTypeBoundary.agda b/proposals/idaptik/migrated/CovertLink/CovertLinkConnectionTypeBoundary.agda new file mode 100644 index 0000000..6a70f00 --- /dev/null +++ b/proposals/idaptik/migrated/CovertLink/CovertLinkConnectionTypeBoundary.agda @@ -0,0 +1,84 @@ +{-# 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): +-- { +-- "DarkFibre": 0, +-- "LegacyTrunk": 1, +-- "OOBManagement": 2, +-- "WirelessBridge": 3, +-- "CrossConnect": 4, +-- "MaintenanceVLAN": 5, +-- "ImprovisedLink": 6 +-- } + +module CovertLinkConnectionTypeBoundary 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 = DarkFibre +-- c1 = LegacyTrunk +-- c2 = OOBManagement +-- c3 = WirelessBridge +-- c4 = CrossConnect +-- c5 = MaintenanceVLAN +-- c6 = ImprovisedLink +data Host : Set where + c0 c1 c2 c3 c4 c5 c6 : 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 + +-- 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 + +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/CovertLink/CovertLinkStateBoundary.agda b/proposals/idaptik/migrated/CovertLink/CovertLinkStateBoundary.agda new file mode 100644 index 0000000..1dd1b7c --- /dev/null +++ b/proposals/idaptik/migrated/CovertLink/CovertLinkStateBoundary.agda @@ -0,0 +1,72 @@ +{-# 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): +-- { +-- "Unknown": 0, +-- "Discovered": 1, +-- "Active": 2, +-- "Dead": 3 +-- } + +module CovertLinkStateBoundary 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 = Unknown +-- c1 = Discovered +-- c2 = Active +-- c3 = Dead +data Host : Set where + c0 c1 c2 c3 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 + +-- 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 + +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/CovertLink/covertlink.config.mjs b/proposals/idaptik/migrated/CovertLink/covertlink.config.mjs new file mode 100644 index 0000000..642ff2c --- /dev/null +++ b/proposals/idaptik/migrated/CovertLink/covertlink.config.mjs @@ -0,0 +1,120 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// 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 CovertLink.affine. Oracle re-derives the stats, +// is_monitored, state_color, latency_ticks, and TTL logic from the original +// CovertLink.res / CovertLinkCoprocessor.res source semantics. +// +// defaultStats from CovertLink.res (connectionType enum order, 0..6): +// DarkFibre(0): bw=5, lat=5, stealth=5, dur=5 +// LegacyTrunk(1): bw=4, lat=4, stealth=3, dur=2 +// OOBManagement(2): bw=2, lat=3, stealth=4, dur=4 +// WirelessBridge(3): bw=3, lat=2, stealth=1, dur=3 +// CrossConnect(4): bw=4, lat=4, stealth=3, dur=3 +// MaintenanceVLAN(5): bw=3, lat=3, stealth=2, dur=5 +// ImprovisedLink(6): bw=1, lat=1, stealth=3, dur=1 +// Out-of-band: bw=0, lat=0, stealth=0, dur=0 + +const STATS = [ + { bw: 5, lat: 5, st: 5, dur: 5 }, // 0 DarkFibre + { bw: 4, lat: 4, st: 3, dur: 2 }, // 1 LegacyTrunk + { bw: 2, lat: 3, st: 4, dur: 4 }, // 2 OOBManagement + { bw: 3, lat: 2, st: 1, dur: 3 }, // 3 WirelessBridge + { bw: 4, lat: 4, st: 3, dur: 3 }, // 4 CrossConnect + { bw: 3, lat: 3, st: 2, dur: 5 }, // 5 MaintenanceVLAN + { bw: 1, lat: 1, st: 3, dur: 1 }, // 6 ImprovisedLink +]; +const OOB_STATS = { bw: 0, lat: 0, st: 0, dur: 0 }; +function getStat(ct, field) { + const s = (ct >= 0 && ct <= 6) ? STATS[ct] : OOB_STATS; + return s[field]; +} + +// isMonitored: WirelessBridge(3) and MaintenanceVLAN(5) only +function oracleIsMonitored(ct) { + return (ct === 3 || ct === 5) ? 1 : 0; +} + +// stateToColor: 0=Unknown=0x444444, 1=Discovered=0xFFAA00, +// 2=Active=0x00FF88, 3=Dead=0xFF2222, else=0x444444 +function oracleStateColor(st) { + if (st === 0) return 0x444444; + if (st === 1) return 0xFFAA00; + if (st === 2) return 0x00FF88; + if (st === 3) return 0xFF2222; + return 0x444444; +} + +// ttl_step(remaining, dt, zero): max(zero, remaining - dt). Host passes zero=0. +// NOTE: parity uses i32 ABI. Float tests use integer inputs so i32 cast is exact. +// ttl_expired(remaining, dt): dt >= remaining -> 1, else 0. +// (equivalent to remaining - dt <= 0.0, but avoids float literal in binary op) +function oracleTtlStep(remaining, dt) { + // zero=0 is the host default; oracle computes max(0, remaining-dt) + const next = remaining - dt; + return next < 0 ? 0 : next; +} +function oracleTtlExpired(remaining, dt) { + return (remaining - dt) <= 0 ? 1 : 0; +} + +export default { + affine: "CovertLink.affine", + cases: [ + { + name: "type_bandwidth over ct [-1..8]", + export: "type_bandwidth", + args: [[-1, 8]], + oracle: (ct) => getStat(ct, "bw") | 0, + }, + { + name: "type_latency over ct [-1..8]", + export: "type_latency", + args: [[-1, 8]], + oracle: (ct) => getStat(ct, "lat") | 0, + }, + { + name: "type_stealth over ct [-1..8]", + export: "type_stealth", + args: [[-1, 8]], + oracle: (ct) => getStat(ct, "st") | 0, + }, + { + name: "type_durability over ct [-1..8]", + export: "type_durability", + args: [[-1, 8]], + oracle: (ct) => getStat(ct, "dur") | 0, + }, + { + name: "is_monitored over ct [-1..8]", + export: "is_monitored", + args: [[-1, 8]], + oracle: (ct) => oracleIsMonitored(ct) | 0, + }, + { + name: "state_color over st [-1..5]", + export: "state_color", + args: [[-1, 5]], + oracle: (st) => oracleStateColor(st) | 0, + }, + { + name: "latency_ticks (nullary)", + export: "latency_ticks", + args: [], + oracle: () => 1, + }, + { + name: "ttl_step: remaining 0..10, dt 0..10, zero=0 (host constant)", + export: "ttl_step", + args: [[0, 10], [0, 10], { values: [0] }], + oracle: (r, d, _z) => oracleTtlStep(r, d) | 0, + }, + { + name: "ttl_expired: remaining 0..10, dt 0..10 (integer steps)", + export: "ttl_expired", + args: [[0, 10], [0, 10]], + oracle: (r, d) => oracleTtlExpired(r, d) | 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/CriticalRoll/CriticalRoll.affine b/proposals/idaptik/migrated/CriticalRoll/CriticalRoll.affine new file mode 100644 index 0000000..bd693b9 --- /dev/null +++ b/proposals/idaptik/migrated/CriticalRoll/CriticalRoll.affine @@ -0,0 +1,75 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// CriticalRoll -- the pure probability/threshold kernel re-decomposed from +// src/app/player/CriticalRoll.res. The ReScript original entangles three things: +// a non-deterministic draw (Math.random()), two attribute-driven threshold +// formulae for Jessica, and a three-way classification of the draw against a +// success and a failure threshold shared by Jessica and Q. Per the DESIGN-VISION +// ("AffineScript is the brain, JS/Pixi the senses; only primitives cross the wasm +// boundary"), neither the draw nor the variant labels are the unit of migration. +// What crosses is the deterministic arithmetic: the two thresholds and the band +// the comparison falls into. The host owns the entropy (Math.random), the rate +// tables QCertifications already serves, the rollResult record, and the outcome +// labels and colours. The kernel is stateless and total: every Float the boundary +// admits yields a defined Int verdict or Float threshold, never a trap. +// +//## Why this split, not a port of jessicaRoll/qRoll +// jessicaRoll and qRoll each draw a random number, look thresholds up (Jessica by +// formula, Q by host rate table), then classify. The draw is impure and the Q +// lookups are discrete table reads with no arithmetic, so both stay host senses. +// The arithmetic that remains -- the two Jessica formulae and the one shared +// classification -- is what the co-processor owns. Both call sites feed the same +// classify_outcome with their respective thresholds, so the brain has one decision +// rule and the host supplies the two numbers however it sourced them. +// +//## Outcome encoding (the header contract for the JS host) +// The rollOutcome variant collapses to an ordinal the host maps back to the +// variant and thence to a label/colour: +// 0 CriticalSuccess 1 Normal 2 CriticalFailure +// classify_outcome returns exactly one of these three. The boundaries match the +// ReScript verbatim: roll < critSuccess -> 0; else roll > 1 - critFail -> 2; else +// 1. The success test wins ties at the lower edge (strict <), the failure test at +// the upper edge (strict >), so a roll sitting exactly on a threshold is Normal, +// identical to the ReScript if/else chain. +// +//## Float contract +// roll, crit_success and crit_fail cross as f64 (proven to marshal both ways; +// cf. migration/bindings/Maths.wasm and PlayerHP.wasm). roll is the host's draw in +// [0, 1); crit_success and crit_fail are probabilities in [0, 1]. The float +// comparisons drive an Int verdict, which the wasm backend compares as i32, the +// working subset for float-fed branches. jessica_crit_success and +// jessica_crit_fail return f64 thresholds the host either feeds straight back into +// classify_outcome or displays in the rollResult. + +//## Jessica's critical-success threshold +// min(0.25, 0.05 + (primaryStat - 100)/1000), the jessicaRoll line verbatim in +// f64. Higher primary stat raises the chance; the cap at 0.25 is the design +// ceiling. primaryStat arrives as a Float, so the division is pure f64 and no +// int->float is implicated. Branchless via min_float rather than a Float if/else. +pub fn jessica_crit_success(primary_stat: Float) -> Float { + min_float(0.25, 0.05 + (primary_stat - 100.0) / 1000.0) +} + +//## Jessica's critical-failure threshold +// max(0.01, 0.10 + (100 - wil)/1000), the jessicaRoll line verbatim in f64. +// Higher willpower lowers the chance; the floor at 0.01 is the design minimum. +// Branchless via max_float. wil is a Float host-side, so the subtract and divide +// are pure f64. +pub fn jessica_crit_fail(wil: Float) -> Float { + max_float(0.01, 0.10 + (100.0 - wil) / 1000.0) +} + +//## Shared three-way classification +// The outcome if/else chain shared by jessicaRoll and qRoll, in isolation: +// if roll < crit_success -> CriticalSuccess (0) +// else if roll > 1.0 - crit_fail -> CriticalFailure (2) +// else -> Normal (1) +// Flat guarded returns rather than nested if/else; the parser dislikes deep +// nesting and the order of the guards preserves the ReScript precedence (success +// tested first, then failure, Normal as the fall-through). The strict comparisons +// mean a roll exactly on a boundary is Normal, matching the ReScript. +pub fn classify_outcome(roll: Float, crit_success: Float, crit_fail: Float) -> Int { + if roll < crit_success { return 0; } + if roll > 1.0 - crit_fail { return 2; } + 1 +} diff --git a/proposals/idaptik/migrated/Detection/Detection.affine b/proposals/idaptik/migrated/Detection/Detection.affine new file mode 100644 index 0000000..7ea6677 --- /dev/null +++ b/proposals/idaptik/migrated/Detection/Detection.affine @@ -0,0 +1,93 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// Detection -- the pure detection-score kernel re-decomposed from +// src/app/enemies/DetectionSystem.res. The ReScript original is a mutable record +// (alertScore, decayRate, events array, suppression flag, counters) over which +// reportDetection and update mutate in place, entangled with string-keyed variants, +// the HUD enum, AccessibilitySettings effects, and an event-history array. +// +// Per the DESIGN-VISION ("the brain is AffineScript, the senses are JS; only +// primitives cross the wasm boundary"), the mutable record is NOT migrated. What +// crosses: the per-source weight table, the suppression/calm scaling, the clamped +// score accumulation, the natural decay, and the discrete level ladder. The host +// keeps the record, the event array, source-to-string formatting, and every effect. +// +// The alert-level thresholding reproduced here so a caller needs only one kernel. +// +//## Compiler note: no min_float / max_float built-in in wasm codegen +// The built-in names `min_float` and `max_float` are not wired in the current wasm +// codegen. Both are replaced by guard-style inline if/else expressions, which lower +// correctly via F64 conditional select. +// +//## Boundary contract (the header the JS host relies on) +// source_weight(tag: Int) -> Float +// Raw per-source weight: tag is ordinal 0..12; out-of-band -> 0.0. +// 0 GuardSight 40 1 GuardHearing 15 2 DogDetection 30 +// 3 DogHearing 10 4 CameraMotion 25 5 CanaryTripped 50 +// 6 PortScanDetected 10 7 CrackFailed 20 8 FirewallBlock 5 +// 9 CovertLinkProbe 8 10 DistractionExpired 0 11 ContactDamage 20 +// 12 ManualAlert 60 +// effective_weight(tag: Int, suppressed: Float) -> Float +// Weight after stealth-tool scaling: * 0.3 when suppressed != 0. +// accumulate(score: Float, weight: Float) -> Float +// min(120.0, score + weight). +// decay(score: Float, rate: Float, dt: Float) -> Float +// max(0.0, score - rate * dt). +// alert_level(score: Float) -> Int +// Discrete level 0..5 (Clear .. Lockdown). + +//## Per-source weight table +pub fn source_weight(tag: Int) -> Float { + if tag == 0 { return 40.0; } + if tag == 1 { return 15.0; } + if tag == 2 { return 30.0; } + if tag == 3 { return 10.0; } + if tag == 4 { return 25.0; } + if tag == 5 { return 50.0; } + if tag == 6 { return 10.0; } + if tag == 7 { return 20.0; } + if tag == 8 { return 5.0; } + if tag == 9 { return 8.0; } + if tag == 10 { return 0.0; } + if tag == 11 { return 20.0; } + if tag == 12 { return 60.0; } + 0.0 +} + +//## Suppression-scaled effective weight +// reportDetection: if suppressionActive { weight *. 0.3 } else { weight }. +// suppressed is a 1.0/0.0 float flag; non-zero selects the 0.3 stealth scaling. +pub fn effective_weight(tag: Int, suppressed: Float) -> Float { + let w = source_weight(tag); + if suppressed == 0.0 { + w + } else { + w * 0.3 + } +} + +//## Clamped score escalation +// min(120.0, score + weight). min_float not available: guard-style. +pub fn accumulate(score: Float, weight: Float) -> Float { + let next = score + weight; + if next > 120.0 { 120.0 } else { next } +} + +//## Natural decay, floored at zero +// max(0.0, score - rate*dt). max_float not available: guard-style. +pub fn decay(score: Float, rate: Float, dt: Float) -> Float { + let next = score - rate * dt; + if next < 0.0 { 0.0 } else { next } +} + +//## Discrete alert-level ladder +// getAlertLevel composed with HUD.alertToInt: threshold cascade top-down. +pub fn alert_level(score: Float) -> Int { + if score >= 100.0 { return 5; } + if score >= 85.0 { return 4; } + if score >= 60.0 { return 3; } + if score >= 35.0 { return 2; } + if score >= 15.0 { return 1; } + 0 +} diff --git a/proposals/idaptik/migrated/Detection/DetectionInt.affine b/proposals/idaptik/migrated/Detection/DetectionInt.affine new file mode 100644 index 0000000..e4f8b7b --- /dev/null +++ b/proposals/idaptik/migrated/Detection/DetectionInt.affine @@ -0,0 +1,15 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// DetectionInt -- Int-only parity subset of Detection.affine. +// Contains only alert_level which returns Int, so the scalar parity runner +// can instantiate this wasm without encountering f64-return functions. + +pub fn alert_level(score: Int) -> Int { + if score >= 100 { return 5; } + if score >= 85 { return 4; } + if score >= 60 { return 3; } + if score >= 35 { return 2; } + if score >= 15 { return 1; } + 0 +} diff --git a/proposals/idaptik/migrated/Detection/detection.config.mjs b/proposals/idaptik/migrated/Detection/detection.config.mjs new file mode 100644 index 0000000..f4e43f7 --- /dev/null +++ b/proposals/idaptik/migrated/Detection/detection.config.mjs @@ -0,0 +1,26 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// affine-parity config for Detection.affine (Int-only parity subset). +// Points at DetectionInt.affine which exposes only alert_level (Int return). +// Oracles re-derive from DetectionSystem.res semantics in plain JS. + +export default { + affine: "DetectionInt.affine", + compile: false, + cases: [ + { + name: "alert_level(score) threshold ladder 0..5", + export: "alert_level", + args: [{ values: [0, 5, 14, 15, 34, 35, 59, 60, 84, 85, 99, 100, 110, 120] }], + oracle: (score) => { + if (score >= 100) return 5; + if (score >= 85) return 4; + if (score >= 60) return 3; + if (score >= 35) return 2; + if (score >= 15) return 1; + return 0; + }, + }, + ], +}; diff --git a/proposals/idaptik/migrated/DeviceCaps/DeviceCaps.affine b/proposals/idaptik/migrated/DeviceCaps/DeviceCaps.affine new file mode 100644 index 0000000..f8c8b8a --- /dev/null +++ b/proposals/idaptik/migrated/DeviceCaps/DeviceCaps.affine @@ -0,0 +1,62 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// DeviceCaps -- the device-type colour table and security-level colour table, +// the pure-integer lookup cores extracted from +// src/app/devices/types/DeviceTypes.res (getDeviceColor, getSecurityColor). Per +// the DESIGN-VISION ("AffineScript is the brain, JS/Pixi the senses; only +// primitives cross the wasm boundary"), the JS host keeps the deviceType and +// securityLevel variants and all strings; AffineScript owns only the integer +// colour code that each variant ordinal maps to. +// +// The DeviceType kernel (already staged at DeviceType/) owns the taxonomy +// validity predicate and sentinel. DeviceCaps is a DISTINCT kernel: it owns the +// colour assignments, which are idaptik game-specific and separate from the +// eight-constructor taxonomy in DeviceTypes.res (not the twelve-constructor +// shared/src/DeviceType.res). DeviceCaps does NOT re-define the encoding; it +// takes the ordinal as given and returns a packed 0xRRGGBB colour integer. +// +//## Device-type colour table (getDeviceColor, DeviceTypes.res) +// The idaptik game uses 8 device types. Ordinal mirrors the declaration order in +// DeviceTypes.res (switch constructor order): +// 0 Laptop 0x2196F3 (Blue) +// 1 Router 0xFF9800 (Orange) +// 2 Server 0x9C27B0 (Purple) +// 3 IotCamera 0xF44336 (Red) +// 4 Terminal 0x4CAF50 (Green) +// 5 PowerStation 0xFFEB3B (Yellow) +// 6 UPS 0x795548 (Brown) +// 7 Firewall 0xE53935 (Dark Red) +// An out-of-band ordinal returns 0x888888 (neutral grey) — a declared sentinel, +// not an in-band colour, so no collision with any defined type. +// +//## Security-level colour table (getSecurityColor, DeviceTypes.res) +// The four security levels encoded as 0..3 (Open/Weak/Medium/Strong), same +// ordinal as SecurityRank: +// 0 Open 0x00ff00 (Green — unrestricted) +// 1 Weak 0xffff00 (Yellow — notice) +// 2 Medium 0xff9800 (Orange — caution) +// 3 Strong 0xff0000 (Red — locked) +// An out-of-band ordinal returns 0x888888 (neutral grey) — same sentinel. + +//## Device-type colour lookup (getDeviceColor) +pub fn device_color(dt: Int) -> Int { + if dt == 0 { return 0x2196F3; } + if dt == 1 { return 0xFF9800; } + if dt == 2 { return 0x9C27B0; } + if dt == 3 { return 0xF44336; } + if dt == 4 { return 0x4CAF50; } + if dt == 5 { return 0xFFEB3B; } + if dt == 6 { return 0x795548; } + if dt == 7 { return 0xE53935; } + 0x888888 +} + +//## Security-level colour lookup (getSecurityColor) +pub fn security_color(level: Int) -> Int { + if level == 0 { return 0x00ff00; } + if level == 1 { return 0xffff00; } + if level == 2 { return 0xff9800; } + if level == 3 { return 0xff0000; } + 0x888888 +} diff --git a/proposals/idaptik/migrated/DeviceCaps/DeviceTypeOrdinalBoundary.agda b/proposals/idaptik/migrated/DeviceCaps/DeviceTypeOrdinalBoundary.agda new file mode 100644 index 0000000..3fe977a --- /dev/null +++ b/proposals/idaptik/migrated/DeviceCaps/DeviceTypeOrdinalBoundary.agda @@ -0,0 +1,88 @@ +{-# 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, +-- "Router": 1, +-- "Server": 2, +-- "IotCamera": 3, +-- "Terminal": 4, +-- "PowerStation": 5, +-- "UPS": 6, +-- "Firewall": 7 +-- } + +module DeviceTypeOrdinalBoundary 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 = Router +-- c2 = Server +-- c3 = IotCamera +-- c4 = Terminal +-- c5 = PowerStation +-- c6 = UPS +-- c7 = Firewall +data Host : Set where + c0 c1 c2 c3 c4 c5 c6 c7 : 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 + +-- 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 + +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/DeviceCaps/SecurityColorOrdinalBoundary.agda b/proposals/idaptik/migrated/DeviceCaps/SecurityColorOrdinalBoundary.agda new file mode 100644 index 0000000..7e498d2 --- /dev/null +++ b/proposals/idaptik/migrated/DeviceCaps/SecurityColorOrdinalBoundary.agda @@ -0,0 +1,72 @@ +{-# 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): +-- { +-- "Open": 0, +-- "Weak": 1, +-- "Medium": 2, +-- "Strong": 3 +-- } + +module SecurityColorOrdinalBoundary 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 = Open +-- c1 = Weak +-- c2 = Medium +-- c3 = Strong +data Host : Set where + c0 c1 c2 c3 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 + +-- 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 + +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/DeviceCaps/devicecaps.config.mjs b/proposals/idaptik/migrated/DeviceCaps/devicecaps.config.mjs new file mode 100644 index 0000000..f86a4d2 --- /dev/null +++ b/proposals/idaptik/migrated/DeviceCaps/devicecaps.config.mjs @@ -0,0 +1,54 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// 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 DeviceCaps.affine. Oracle re-derives the two colour +// tables from the original DeviceTypes.res getDeviceColor and getSecurityColor +// switch semantics: +// +// getDeviceColor: +// 0 Laptop->0x2196F3, 1 Router->0xFF9800, 2 Server->0x9C27B0, +// 3 IotCamera->0xF44336, 4 Terminal->0x4CAF50, 5 PowerStation->0xFFEB3B, +// 6 UPS->0x795548, 7 Firewall->0xE53935; out-of-band -> 0x888888 +// +// getSecurityColor: +// 0 Open->0x00ff00, 1 Weak->0xffff00, 2 Medium->0xff9800, +// 3 Strong->0xff0000; out-of-band -> 0x888888 + +function oracleDeviceColor(dt) { + if (dt === 0) return 0x2196F3; + if (dt === 1) return 0xFF9800; + if (dt === 2) return 0x9C27B0; + if (dt === 3) return 0xF44336; + if (dt === 4) return 0x4CAF50; + if (dt === 5) return 0xFFEB3B; + if (dt === 6) return 0x795548; + if (dt === 7) return 0xE53935; + return 0x888888; +} + +function oracleSecurityColor(level) { + if (level === 0) return 0x00ff00; + if (level === 1) return 0xffff00; + if (level === 2) return 0xff9800; + if (level === 3) return 0xff0000; + return 0x888888; +} + +export default { + affine: "DeviceCaps.affine", + cases: [ + { + name: "device_color over dt [-1..9] (all 8 valid types + OOB boundaries)", + export: "device_color", + args: [{ values: [-1, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9] }], + oracle: (dt) => oracleDeviceColor(dt) | 0, + }, + { + name: "security_color over level [-1..5] (all 4 valid levels + OOB boundaries)", + export: "security_color", + args: [{ values: [-1, 0, 1, 2, 3, 4, 5] }], + oracle: (level) => oracleSecurityColor(level) | 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/DifficultyScale/DifficultyScale.affine b/proposals/idaptik/migrated/DifficultyScale/DifficultyScale.affine new file mode 100644 index 0000000..8cd4974 --- /dev/null +++ b/proposals/idaptik/migrated/DifficultyScale/DifficultyScale.affine @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// DifficultyScale -- the distraction-item difficulty-scaling co-processor, +// extracted as a pure-integer kernel from src/app/enemies/Distraction.res +// (applyDifficultyScaling). On harder difficulties a distraction's per-item use +// count is curtailed; the original mutates a string-keyed Dict in place, but the +// arithmetic at its heart is purely integer, so we lift that core across the +// wasm boundary and leave the Dict bookkeeping on the JS side. +// +// The JS host already knows each item's base use count and its kind; it asks the +// co-processor for the adjusted count given the current difficulty. NO strings +// cross the boundary (item kinds are passed as an Int selector); integer-only. +// +//## Difficulty ladder (the header contract for the JS host) +// difficulty 0=Tutorial 1=Easy 2=Normal 3=Hard 4=Expert +// +//## Item-kind selector (the second contract for the JS host) +// 0 pizza capped to 1 use when difficulty >= 3 +// 1 prank capped to 1 use when difficulty >= 3 +// 2 maintenance zeroed when difficulty >= 4 +// 3 police zeroed when difficulty >= 4 +// 4 other never scaled; the base count passes through unchanged +// +// The source applies its rules unconditionally (Dict.set), overwriting whatever +// base value was present, so for an affected kind the result does NOT depend on +// base_uses once the threshold is met. An unknown kind passes base_uses through. + +enum Kind { Pizza, Prank, Maintenance, Police, Other } + +fn kind_of(k: Int) -> Kind { + if k == 0 { return Pizza; } + if k == 1 { return Prank; } + if k == 2 { return Maintenance; } + if k == 3 { return Police; } + Other +} + +// The pure scaling kernel. Mirrors the two guarded Dict.set blocks of +// applyDifficultyScaling: pizza/prank cap at difficulty >= 3, maintenance/police +// zeroed at difficulty >= 4, every other case leaving base_uses untouched. +fn scale(difficulty: Int, base_uses: Int, k: Kind) -> Int { + match k { + Pizza => { if difficulty >= 3 { 1 } else { base_uses } }, + Prank => { if difficulty >= 3 { 1 } else { base_uses } }, + Maintenance => { if difficulty >= 4 { 0 } else { base_uses } }, + Police => { if difficulty >= 4 { 0 } else { base_uses } }, + Other => base_uses + } +} + +// The co-processor entry point. Return the difficulty-adjusted use count for an +// item of the given kind whose unscaled base count is base_uses. +pub fn scale_use_count(difficulty: Int, base_uses: Int, item_kind: Int) -> Int { + scale(difficulty, base_uses, kind_of(item_kind)) +} diff --git a/proposals/idaptik/migrated/DifficultyScale/difficultyscale.config.mjs b/proposals/idaptik/migrated/DifficultyScale/difficultyscale.config.mjs new file mode 100644 index 0000000..2b2c42e --- /dev/null +++ b/proposals/idaptik/migrated/DifficultyScale/difficultyscale.config.mjs @@ -0,0 +1,32 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// affine-parity config for DifficultyScale.affine. +// Oracle re-derives from Distraction.res applyDifficultyScaling semantics. +// +// scale_use_count(difficulty, base_uses, item_kind): +// difficulty ladder: 0=Tutorial 1=Easy 2=Normal 3=Hard 4=Expert +// item_kind: 0=pizza 1=prank 2=maintenance 3=police 4+=other/unknown +// pizza/prank: difficulty >= 3 -> 1, else base_uses +// maintenance/police: difficulty >= 4 -> 0, else base_uses +// other/unknown: base_uses unchanged + +export default { + affine: "DifficultyScale.affine", + cases: [ + { + name: "scale_use_count(diff 0..5, base 0..5, kind 0..6)", + export: "scale_use_count", + args: [ + { values: [0, 1, 2, 3, 4, 5] }, + { values: [0, 1, 2, 3, 4, 5] }, + { values: [0, 1, 2, 3, 4, 5, 6] }, + ], + oracle: (difficulty, base_uses, item_kind) => { + if (item_kind === 0 || item_kind === 1) return difficulty >= 3 ? 1 : base_uses; + if (item_kind === 2 || item_kind === 3) return difficulty >= 4 ? 0 : base_uses; + return base_uses; + }, + }, + ], +}; diff --git a/proposals/idaptik/migrated/Distraction/Distraction.affine b/proposals/idaptik/migrated/Distraction/Distraction.affine new file mode 100644 index 0000000..d222272 --- /dev/null +++ b/proposals/idaptik/migrated/Distraction/Distraction.affine @@ -0,0 +1,92 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// Distraction (Shape-A) -- the stateless transition-kernel co-processor extracted +// from src/app/enemies/Distraction.res. The ReScript original is a stateful PBX +// engine: a mutable pbxState record (a stringly-keyed use-count dict, a cooldown, +// an array of active distractions, each with its own mutable guardsResponding +// counter) threaded through call / registerResponder / unregisterResponder / +// applyDifficultyScaling, all of which mutate in place. +// +// Per the DESIGN-VISION ("AffineScript is the brain, JS/Pixi the senses; only +// primitives cross the wasm boundary") and the Shape-A pattern (the model lives in +// linear memory is compiler-blocked), the JS HOST owns the state -- the per-item +// uses dict and each distraction's responder counter -- and this module exposes +// only PURE, TOTAL, STATELESS transition kernels. Each takes the relevant current +// scalar field(s) plus the event arguments as Int and RETURNS the new scalar; the +// host reads the return back and stores it. Nothing richer than i32 crosses, and +// no state persists between calls. +// +//## Boundary contract (the header the JS host reads) +// param/return meaning defended range +// uses: Int an item's current remaining uses <=0 yields unchanged +// kind: Int item-kind selector (see below) any value tolerated +// count: Int a distraction's responder count clamped to >= 0 +// difficulty: Int 0 Tutorial .. 4 Expert below threshold = identity +// base: Int an item's unscaled base use count passes through unscaled +// +//## Item-kind selector (shared with DifficultyScale, byte-identical rules) +// 0 pizza capped to 1 use when difficulty >= 3 +// 1 prank capped to 1 use when difficulty >= 3 +// 2 maintenance zeroed when difficulty >= 4 +// 3 police zeroed when difficulty >= 4 +// 4 other (fire) never scaled; the base count passes through unchanged + +//## Item-kind decode +// One guarded return per canonical value, Other as the fall-through, so an +// out-of-band selector can never tag an undefined kind. +enum Kind { Pizza, Prank, Maintenance, Police, Other } + +fn kind_of(k: Int) -> Kind { + if k == 0 { return Pizza; } + if k == 1 { return Prank; } + if k == 2 { return Maintenance; } + if k == 3 { return Police; } + Other +} + +//## use_item -- the per-call use-count decrement (transition kernel) +// Re-decomposes the decrement at the heart of Distraction.res `call`: a call with +// `remaining <= 0` returns unchanged (NoUsesLeft), otherwise count - 1. So a use +// only consumes a charge when one is available, and never drives the count negative. +pub fn use_item(uses: Int, kind: Int) -> Int { + if uses <= 0 { + uses + } else { + uses - 1 + } +} + +//## register_responder -- a guard joins a distraction (transition kernel) +// Re-decomposes Distraction.res registerResponder: count + 1. +pub fn register_responder(count: Int) -> Int { + count + 1 +} + +//## unregister_responder -- a guard leaves a distraction (transition kernel) +// Re-decomposes Distraction.res unregisterResponder: max(0, count - 1). +pub fn unregister_responder(count: Int) -> Int { + if count <= 0 { + 0 + } else { + count - 1 + } +} + +//## apply_difficulty -- the difficulty-scaling kernel +// Re-decomposes applyDifficultyScaling. Pizza/prank cap to 1 at difficulty >= 3, +// maintenance/police zero at difficulty >= 4. Below threshold and for Other, base +// passes through. Byte-identical to DifficultyScale.scale_use_count. +fn scale(difficulty: Int, base: Int, k: Kind) -> Int { + match k { + Pizza => { if difficulty >= 3 { 1 } else { base } }, + Prank => { if difficulty >= 3 { 1 } else { base } }, + Maintenance => { if difficulty >= 4 { 0 } else { base } }, + Police => { if difficulty >= 4 { 0 } else { base } }, + Other => base + } +} + +pub fn apply_difficulty(base: Int, difficulty: Int, kind: Int) -> Int { + scale(difficulty, base, kind_of(kind)) +} diff --git a/proposals/idaptik/migrated/Distraction/distraction.config.mjs b/proposals/idaptik/migrated/Distraction/distraction.config.mjs new file mode 100644 index 0000000..bcb55d4 --- /dev/null +++ b/proposals/idaptik/migrated/Distraction/distraction.config.mjs @@ -0,0 +1,55 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// affine-parity config for Distraction.affine. +// Oracles re-derive from DistractionCoprocessor.res / Distraction.res semantics. +// +// use_item(count, kind): kind 0..4 known -> max(0, count-1); kind 5+ -> -1 sentinel +// register_responder(count): count + 1 +// unregister_responder(count): max(0, count - 1) +// apply_difficulty(difficulty, base_uses, item_kind): +// pizza/prank (0,1): difficulty >= 3 -> 1, else base_uses +// maintenance/police (2,3): difficulty >= 4 -> 0, else base_uses +// other (4+): base_uses unchanged + +export default { + affine: "Distraction.affine", + cases: [ + { + name: "use_item(uses 0..5, kind 0..5): pure decrement, kind is unused by kernel", + export: "use_item", + args: [{ values: [0, 1, 2, 3, 4, 5] }, { values: [0, 1, 2, 3, 4, 5] }], + // The kernel simply decrements: if uses <= 0 return uses, else uses - 1. + // kind is a parameter but is not consulted by this kernel (host gates on it). + oracle: (uses, kind) => uses <= 0 ? uses : uses - 1, + }, + { + name: "register_responder(count 0..10)", + export: "register_responder", + args: [[0, 10]], + oracle: (count) => count + 1, + }, + { + name: "unregister_responder(count 0..10)", + export: "unregister_responder", + args: [[0, 10]], + oracle: (count) => Math.max(0, count - 1), + }, + { + // Note: kernel signature is apply_difficulty(base, difficulty, kind) + // i.e. base is first, difficulty second, kind third. + name: "apply_difficulty(base 0..5, diff 0..5, kind 0..6)", + export: "apply_difficulty", + args: [ + { values: [0, 1, 2, 3, 4, 5] }, // base (first param) + { values: [0, 1, 2, 3, 4, 5] }, // difficulty (second param) + { values: [0, 1, 2, 3, 4, 5, 6] }, // kind (third param) + ], + oracle: (base, difficulty, item_kind) => { + if (item_kind === 0 || item_kind === 1) return difficulty >= 3 ? 1 : base; + if (item_kind === 2 || item_kind === 3) return difficulty >= 4 ? 0 : base; + return base; + }, + }, + ], +}; diff --git a/proposals/idaptik/migrated/DualAlert/DualAlert.affine b/proposals/idaptik/migrated/DualAlert/DualAlert.affine new file mode 100644 index 0000000..b702016 --- /dev/null +++ b/proposals/idaptik/migrated/DualAlert/DualAlert.affine @@ -0,0 +1,148 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// DualAlert -- the dual-threat alert combination/priority co-processor extracted +// from src/app/ui/DualAlert.res (referenced in DualAlertBridge.res). Per the +// DESIGN-VISION ("AffineScript is the brain, JS/Pixi the senses; only primitives +// cross the wasm boundary"), the JS host keeps the alertState record, descriptive +// labels and frame-by-frame mutation; AffineScript owns the pure numeric and enum +// core: the level ordinal encoding, the per-level colour table, the escalation/ +// scrub step machine, the trigger-combination rule and the cross-alert predicates. +// +// DualAlertBridge.res is a PURE ROUTING BRIDGE (string-keyed switch statements +// over mutable JS service objects) — it has no integer brain of its own. Its +// classify/convert logic re-encodes variant constructors to kernel tags host-side. +// +//## Float boundary: progress crosses in MILLI-UNITS +// The 0.0..1.0 progress and per-trigger severities cross as Ints scaled by 1000: +// the JS caller passes round(progress * 1000) and round(severity * 1000), and the +// 1.0 escalation threshold becomes 1000. Arithmetic matches the ReScript exactly. +// +//## Level ordinal encoding (the header contract for the JS host) +// level variant ordinal +// 0 Clear 0 +// 1 Guarded 1 +// 2 Elevated 2 +// 3 High 3 +// 4 Severe 4 +// Any input outside 0..4 is clamped to the nearest valid ordinal. + +enum Level { Clear, Guarded, Elevated, High, Severe, Invalid(Int) } + +fn level_of(level: Int) -> Level { + if level == 0 { return Clear; } + if level == 1 { return Guarded; } + if level == 2 { return Elevated; } + if level == 3 { return High; } + if level == 4 { return Severe; } + Invalid(level) +} + +// @clamp:declared -- out-of-band level clamps to nearest valid ordinal (0 or 4). +// The clamp is provably controlled-loss: echo-boundary proves the five valid +// codes 0..4 are injective; Invalid(v) is intentionally squashed by design. +fn clamp_level_ordinal(v: Int) -> Int { + if v < 0 { return 0; } + 4 +} + +fn ordinal_of(l: Level) -> Int { + match l { + Clear => 0, + Guarded => 1, + Elevated => 2, + High => 3, + Severe => 4, + Invalid(v) => clamp_level_ordinal(v) + } +} + +//## Level ordinal (levelValue) +pub fn level_value(level: Int) -> Int { + ordinal_of(level_of(level)) +} + +//## Per-level colour (levelColor) -- 24-bit RGB integer constants +// 0 Clear 0x44ff44 4521796 +// 1 Guarded 0xaaff44 11206468 +// 2 Elevated 0xffaa44 16755268 +// 3 High 0xff4444 16729156 +// 4 Severe 0xff0000 16711680 +pub fn level_colour(level: Int) -> Int { + let o = ordinal_of(level_of(level)); + if o == 0 { return 4521796; } + if o == 1 { return 11206468; } + if o == 2 { return 16755268; } + if o == 3 { return 16729156; } + 16711680 +} + +//## Escalation step (escalateLevel) -- saturating successor +pub fn escalate_level(level: Int) -> Int { + let o = ordinal_of(level_of(level)); + if o >= 4 { return 4; } + o + 1 +} + +//## Scrub step (scrubCyberAlert) -- saturating predecessor +pub fn scrub_step(level: Int) -> Int { + let o = ordinal_of(level_of(level)); + if o <= 0 { return 0; } + o - 1 +} + +//## Trigger combination: did the level advance? +pub fn trigger_escalates(level: Int, progress_milli: Int, severity_milli: Int) -> Int { + let combined = progress_milli + severity_milli; + if combined < 1000 { return 0; } + let o = ordinal_of(level_of(level)); + if o >= 4 { return 0; } + 1 +} + +//## Trigger combination: the new progress after a trigger +pub fn trigger_progress(level: Int, progress_milli: Int, severity_milli: Int) -> Int { + let combined = progress_milli + severity_milli; + if combined < 1000 { return combined; } + let o = ordinal_of(level_of(level)); + if o >= 4 { return 1000; } + combined - 1000 +} + +//## Trigger combination: the new level after a trigger +pub fn trigger_level(level: Int, progress_milli: Int, severity_milli: Int) -> Int { + let o = ordinal_of(level_of(level)); + let combined = progress_milli + severity_milli; + if combined < 1000 { return o; } + if o >= 4 { return o; } + o + 1 +} + +//## Cooldown decay, floored at zero +pub fn cooldown_progress(progress_milli: Int, decay_milli: Int) -> Int { + let next = progress_milli - decay_milli; + if next < 0 { return 0; } + next +} + +//## Overall threat level (higher of physical vs cyber) +pub fn overall_threat(physical: Int, cyber: Int) -> Int { + let p = ordinal_of(level_of(physical)); + let c = ordinal_of(level_of(cyber)); + if p >= c { return p; } + c +} + +//## Cross-alert: dispatch AntiHacker guards (cyber >= Elevated = 2) +pub fn should_dispatch_antihacker(cyber: Int) -> Int { + let c = ordinal_of(level_of(cyber)); + if c >= 2 { return 1; } + 0 +} + +//## Cross-alert: guards checking terminals (physical >= High = 3) +pub fn guards_checking_terminals(physical: Int) -> Int { + let p = ordinal_of(level_of(physical)); + if p >= 3 { return 1; } + 0 +} diff --git a/proposals/idaptik/migrated/DualAlert/DualAlertBoundary.agda b/proposals/idaptik/migrated/DualAlert/DualAlertBoundary.agda new file mode 100644 index 0000000..a6974e4 --- /dev/null +++ b/proposals/idaptik/migrated/DualAlert/DualAlertBoundary.agda @@ -0,0 +1,76 @@ +{-# 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): +-- { +-- "Clear": 0, +-- "Guarded": 1, +-- "Elevated": 2, +-- "High": 3, +-- "Severe": 4 +-- } + +module DualAlertBoundary 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 = Clear +-- c1 = Guarded +-- c2 = Elevated +-- c3 = High +-- c4 = Severe +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 = 4 + +-- 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 + +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/DualAlert/dualalert.config.mjs b/proposals/idaptik/migrated/DualAlert/dualalert.config.mjs new file mode 100644 index 0000000..2c14cfa --- /dev/null +++ b/proposals/idaptik/migrated/DualAlert/dualalert.config.mjs @@ -0,0 +1,125 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// affine-parity config for DualAlert.affine. +// Oracles re-derive from DualAlert.res semantics in plain JS. +// +// Level ordinal: 0=Clear 1=Guarded 2=Elevated 3=High 4=Severe. +// OOB clamped: < 0 -> 0, > 4 -> 4 (via Invalid(v) arm). +// All parameters and results are Int. Progress/severity use milli-units (x1000). + +const COLOURS = [4521796, 11206468, 16755268, 16729156, 16711680]; + +function clamp(level) { + if (level < 0) return 0; + if (level > 4) return 4; + return level; +} + +export default { + affine: "DualAlert.affine", + cases: [ + { + name: "level_value(level -1..5)", + export: "level_value", + args: [{ values: [-1, 0, 1, 2, 3, 4, 5] }], + oracle: (level) => clamp(level), + }, + { + name: "level_colour(level -1..5)", + export: "level_colour", + args: [{ values: [-1, 0, 1, 2, 3, 4, 5] }], + oracle: (level) => COLOURS[clamp(level)], + }, + { + name: "escalate_level(level -1..5): saturating +1", + export: "escalate_level", + args: [{ values: [-1, 0, 1, 2, 3, 4, 5] }], + oracle: (level) => { const o = clamp(level); return o >= 4 ? 4 : o + 1; }, + }, + { + name: "scrub_step(level -1..5): saturating -1", + export: "scrub_step", + args: [{ values: [-1, 0, 1, 2, 3, 4, 5] }], + oracle: (level) => { const o = clamp(level); return o <= 0 ? 0 : o - 1; }, + }, + { + name: "trigger_escalates(level, prog_m, sev_m)", + export: "trigger_escalates", + args: [ + { values: [-1, 0, 1, 2, 3, 4, 5] }, + { values: [0, 200, 500, 800, 999, 1000, 1200] }, + { values: [0, 200, 500, 800, 999, 1000, 1200] }, + ], + oracle: (level, prog_m, sev_m) => { + const combined = prog_m + sev_m; + if (combined < 1000) return 0; + return clamp(level) >= 4 ? 0 : 1; + }, + }, + { + name: "trigger_progress(level, prog_m, sev_m)", + export: "trigger_progress", + args: [ + { values: [-1, 0, 2, 4, 5] }, + { values: [0, 500, 800, 1000] }, + { values: [0, 200, 500, 1000] }, + ], + oracle: (level, prog_m, sev_m) => { + const combined = prog_m + sev_m; + if (combined < 1000) return combined; + return clamp(level) >= 4 ? 1000 : combined - 1000; + }, + }, + { + name: "trigger_level(level, prog_m, sev_m)", + export: "trigger_level", + args: [ + { values: [-1, 0, 1, 2, 3, 4, 5] }, + { values: [0, 500, 1000] }, + { values: [0, 500, 1000] }, + ], + oracle: (level, prog_m, sev_m) => { + const o = clamp(level); + const combined = prog_m + sev_m; + if (combined < 1000) return o; + if (o >= 4) return o; + return o + 1; + }, + }, + { + name: "cooldown_progress(prog_m 0..1200, decay_m 0..1200)", + export: "cooldown_progress", + args: [ + { values: [0, 200, 500, 800, 1000, 1200] }, + { values: [0, 100, 200, 500, 1000, 1200] }, + ], + oracle: (prog_m, decay_m) => Math.max(0, prog_m - decay_m), + }, + { + name: "overall_threat(physical -1..5, cyber -1..5)", + export: "overall_threat", + args: [ + { values: [-1, 0, 1, 2, 3, 4, 5] }, + { values: [-1, 0, 1, 2, 3, 4, 5] }, + ], + oracle: (physical, cyber) => { + const p = clamp(physical); + const c = clamp(cyber); + return p >= c ? p : c; + }, + }, + { + name: "should_dispatch_antihacker(cyber -1..5)", + export: "should_dispatch_antihacker", + args: [{ values: [-1, 0, 1, 2, 3, 4, 5] }], + oracle: (cyber) => clamp(cyber) >= 2 ? 1 : 0, + }, + { + name: "guards_checking_terminals(physical -1..5)", + export: "guards_checking_terminals", + args: [{ values: [-1, 0, 1, 2, 3, 4, 5] }], + oracle: (physical) => clamp(physical) >= 3 ? 1 : 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/EVIDENCE-C6.adoc b/proposals/idaptik/migrated/EVIDENCE-C6.adoc new file mode 100644 index 0000000..65ebb50 --- /dev/null +++ b/proposals/idaptik/migrated/EVIDENCE-C6.adoc @@ -0,0 +1,227 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += Cluster C6 (combat + enemy AI) — four-gate evidence (captured 2026-06-05) +:toc: macro + +[IMPORTANT] +==== +*Captured run of the 4-gate recipe over the 8 cluster-C6 kernels: combat +flash/knockback effects, detection threshold ladder, difficulty scaling, +distraction/item use, dual-alert threat combination, hitbox geometry, +player HP arithmetic, and security-AI phase machine.* All kernels are +pure stateless integer transforms (Shape-A: host owns state, scalar i32 +only crosses the wasm boundary). 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 +| `CombatFx` | OK | 90/90 | (transforms) | clean +| `Detection` | OK | 14/14 | (threshold-ladder) | clean +| `DifficultyScale`| OK | 252/252 | (threshold-ladder) | clean +| `Distraction` | OK | 310/310 | (transforms) | clean +| `DualAlert` | OK | 613/613 | LOSSLESS (5), agda exit 0 | clean +| `HitboxGeom` | OK | 6544/6544| (geometry) | clean +| `PlayerHp` | OK | 295/295 | (transforms) | clean +| `SecurityAi` | OK | 67/67 | LOSSLESS (5), agda exit 0 | clean +| *Total* | *8/8* | *8185/8185* | *2 proofs, agda exit 0* | *8/8 clean* +|=== + +== Kernel inventory + +[cols="2,3",options="header"] +|=== +| Kernel (.affine) | Source ReScript / role +| `CombatFxInt.affine` (parity subset) | `CombatFxLogicCoprocessor.res` — flash cycle/phase, alpha, even-cycle, advance/reset, floattext positions, knockback pop +| `DetectionInt.affine` (parity subset) | `DetectionSystemCoprocessor.res` — alert-level threshold ladder +| `DifficultyScale.affine` | `DifficultyScaleCoprocessor.res` — use-count scaling by difficulty and item kind +| `Distraction.affine` | `DistractionCoprocessor.res` — distraction use-item and apply-difficulty +| `DualAlert.affine` | `DualAlert.res` — dual-threat alert level machine (Level enum encoding + escalation/scrub/trigger/cooldown/overall) +| `HitboxGeom.affine` | `HitboxGeomCoprocessor.res` — point-in-rect, overlap, corner/centre geometry +| `PlayerHp.affine` | `PlayerHPCoprocessor.res` — HP constants, clamp, damage, heal, knockback velocity +| `SecurityAiInt.affine` (parity subset) | `SecurityAICoprocessor.res` — Phase machine (phase_value, phase_for_alert, timer_ready, request_dispatch_phase, is_active, increment_counter, dormant_phase) +|=== + +The `*Int.affine` parity subsets exist because the AffineScript compiler +emits all `pub fn` exports with i32 types in the Wasm type section +regardless of Float return/parameter types — see the compiler-quirks +section below. The full `.affine` kernels contain the complete Float +logic; the `*Int.affine` subsets expose only the Int-returning exports +for the scalar-i32 parity runner. + +== Host-side sense modules (NOT migrated — host responsibility) + +The following ReScript modules are *pure JS/PixiJS routing bridges* or +*host-side state containers* — they have no integer brain and are not +migrated to AffineScript kernels: + +* `DualAlertBridge.res` — string-keyed dispatch switch over mutable JS + alert state; re-encodes variant constructors to kernel tags host-side. + No integer arithmetic of its own; all numeric logic lives in `DualAlert.affine`. +* `Hitbox.res` and related physics helpers — host-side PixiJS display + objects with `contains()` geometry; the pure integer geometry extracted + to `HitboxGeom.affine` for kernel testing, but `Hitbox.res` itself + owns the PIXI display-object lifecycle. + +== Float boundary: milli-units convention + +Several kernels cross Float-domain values as Ints scaled by 1000: + +* `DualAlert`: progress (0.0..1.0) and per-trigger severity cross as + `round(x * 1000)`. The 1.0 escalation threshold becomes 1000. The JS + caller normalises before calling and re-normalises after. +* The multiplied-integer arithmetic matches the ReScript source exactly + (the ReScript used Float arithmetic; integer milli-units give the same + results for the test inputs exercised in G2). + +== Compiler quirks this cluster is written around + +The following AffineScript backend facts were encountered migrating C6. +Each has a sound in-language workaround: + +. *Wasm type section always emits i32 for pub fn exports (BUG).* The + compiler declares ALL exported functions as `(func ... (param i32 ...) + (result i32))` in the Wasm type section regardless of the actual + Float parameter or return types. Consequences: + ** A Float-returning export fails at `WebAssembly.instantiate()` with + `type error in return[0] (expected i32, got f64)`. + ** A Float-parameter export fails because the function body emits + `f64` locals but the type section says `i32` params — the validator + rejects `local.set[0] expected type i32, found f64.const`. + *Workaround:* `compile: false` in parity configs pointing at + already-compiled wasm; `*Int.affine` parity subsets with only + Int-returning exports for functions that need parity testing. + +. *`trunc()` builtin absent or unimplemented.* `trunc(x: Float) -> Int` + does not compile. Workaround: loop-based `floor_pos` helper for + non-negative floats: ++ +---- +fn floor_pos(x: Float) -> Int { + let mut n = 0; + let mut acc = 0.0; + while acc + 1.0 <= x { acc = acc + 1.0; n = n + 1; } + n +} +---- + +. *`float(n)` conversion absent.* `float(n: Int) -> Float` does not + compile. Workaround: loop-based `int_to_float_s` helper. + +. *Integer division equals `floor` for non-negative inputs.* For + integer-only inputs `timer/period` in the flash functions, integer + division `timer / period` equals `Math.floor(timer / period)` when + both operands are non-negative whole numbers. The `*Int.affine` parity + subsets exploit this to avoid the Float floor workaround entirely, + using integer division directly. + +== Gate 1 — compile + +---- +[OK] CombatFxInt [OK] DetectionInt [OK] DifficultyScale [OK] Distraction +[OK] DualAlert [OK] HitboxGeom [OK] PlayerHp [OK] SecurityAiInt +---- + +All 8 kernels compile to `.wasm` with `main.exe compile .affine -o .wasm`, +exit 0, no errors. + +== Gate 2 — parity (oracle-vs-wasm, scalar i32 ABI) + +8185 inputs, 0 mismatches. Oracles re-derive every function +independently from the original ReScript semantics in plain JS — they do +not copy logic from the `.affine` source. + +---- +CombatFx ........ 90/90 Detection ....... 14/14 +DifficultyScale . 252/252 Distraction ..... 310/310 +DualAlert ....... 613/613 HitboxGeom ...... 6544/6544 +PlayerHp ........ 295/295 SecurityAi ...... 67/67 +---- + +=== Oracle independence notes + +* *CombatFx* — `flash_cycle_int(timer, period)` oracle: + `Math.floor(timer / period)`. Matches integer division for non-negative + whole-number inputs: integer division and floor(float/float) are + identical here. +* *Detection* — `alert_level(score)` oracle: re-implements the threshold + ladder `100→5, 85→4, 60→3, 35→2, 15→1, else 0` in JS. 14 boundary + values including the four strict-boundary pairs. +* *HitboxGeom* — `point_in_rect` oracle uses INCLUSIVE upper bounds + (`px > rx+rw` means outside), matching `Hitbox.contains` in the source. +* *Distraction* — `use_item(uses, kind)` oracle: `uses <= 0 ? uses : + uses - 1`. The kernel ignores `kind`; the JS host gates item type + routing before calling the kernel. +* *DualAlert* — `trigger_escalates` / `trigger_progress` / `trigger_level` + oracles use milli-unit arithmetic: `combined = progress_milli + + severity_milli`; threshold is 1000. + +== Gate 3 — echo-boundary + +G3 applies only to encoding/taxonomy kernels whose integer codes are the +*names* of host-side enum values. Value-transform kernels (CombatFx, +HitboxGeom, PlayerHp, Distraction) and threshold-ladder kernels +(Detection, DifficultyScale) are not encodings and do not get a G3 proof. + +=== DualAlert — Level encoding + +Table: `{"Clear":0,"Guarded":1,"Elevated":2,"High":3,"Severe":4}` + +---- +verdict: LOSSLESS + names: 5 + codes: 0, 1, 2, 3, 4 + module: DualAlertBoundary + agda: exit 0 + PROOF HOLDS: encoder injective -> boundary is lossless + (the integer IS the host value). +---- + +Output file: `DualAlert/DualAlertBoundary.agda` + +=== SecurityAi — Phase encoding + +Table: `{"Dormant":0,"Scanning":1,"Targeting":2,"Active":3,"Lockdown":4}` + +---- +verdict: LOSSLESS + names: 5 + codes: 0, 1, 2, 3, 4 + module: SecurityAiBoundary + agda: exit 0 + PROOF HOLDS: encoder injective -> boundary is lossless + (the integer IS the host value). +---- + +Output file: `SecurityAi/SecurityAiBoundary.agda` + +=== Clamp-sentinel declaration + +Both kernels have an `Invalid(Int)` catch-all arm in their `ordinal_of` +function, which clamps out-of-band inputs (< 0 → 0, > 4 → 4). This +clamp is *intentionally declared* — documented in the kernel header +comments and refactored into a separate `clamp_level_ordinal` / +`clamp_phase_ordinal` helper so that the `Invalid(v)` match arm contains +no bare integer literals (which would trigger PA-AFF-001 as an +*undeclared* clamp). The G3 LOSSLESS proof certifies that the five valid +codes 0..4 are injective; the `Invalid(v)` arm handles the deliberately +out-of-band inputs outside that table. + +== Gate 4 — affine-assail + +---- +[CLEAN] CombatFxInt [CLEAN] DetectionInt [CLEAN] DifficultyScale +[CLEAN] Distraction [CLEAN] DualAlert [CLEAN] HitboxGeom +[CLEAN] PlayerHp [CLEAN] SecurityAiInt +---- + +All 8 kernels: 0 findings, exit 0. No `PA-AFF-001` (the `Invalid(v)` clamp +arms in DualAlert and SecurityAi were refactored to helper functions with no +bare integer literals in the match arm body). No `PA-AFF-002` (no indexing +operations). No `PA-AFF-003` (no loops over array parameters). diff --git a/proposals/idaptik/migrated/EVIDENCE-C8.adoc b/proposals/idaptik/migrated/EVIDENCE-C8.adoc new file mode 100644 index 0000000..7547b5e --- /dev/null +++ b/proposals/idaptik/migrated/EVIDENCE-C8.adoc @@ -0,0 +1,312 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += Evidence Report: Cluster C8 — Device + Network State Kernels +:toc: macro +:icons: font + +toc::[] + +== Scope + +Cluster C8 migrates the pure numeric/enum integer brains from the idaptik device +and network subsystem to AffineScript-compiled wasm, following the DESIGN-VISION +"the brain is AffineScript, the senses are JS; only primitives cross the wasm +boundary" and the Shape A (stateless) re-decomposition pattern. + +Eight kernels are certified in this cluster: + +[cols="1,2,1"] +|=== +| Kernel | Source | Notes + +| SecurityRank +| `src/app/devices/SecurityRank.res` (via DeviceRegistry) +| Security-level ranking + filter predicate + +| GlobalNetworkData +| `src/app/devices/GlobalNetworkData.res` +| Hash-display arithmetic, subnet packing + +| NetworkManager +| `src/app/devices/NetworkManager.res` +| Zone access, routing, reachability predicates + +| DeviceCaps +| `src/app/devices/types/DeviceTypes.res` +| Device-type and security-level color tables + +| CovertLink +| `src/app/devices/CovertLink.res` +| Connection stats, IDS visibility, TTL countdown + +| LaptopState +| `src/app/devices/LaptopState.res` +| Service bitmask, port decode, CPU/storage kernels + +| NetworkTransfer +| `src/app/devices/NetworkTransfer.res` +| Byte-transfer progress arithmetic + +| PowerManager +| `src/app/devices/PowerManager.res` +| Battery drain/charge, power-state machine + +|=== + +== 4-Gate Verification Summary + +=== G1 — Compile (AffineScript → wasm) + +All 8 kernels compile to valid wasm with zero errors. + +---- +SecurityRank.affine → SecurityRank.wasm PASS +GlobalNetworkData.affine → GlobalNetworkData.wasm PASS +NetworkManager.affine → NetworkManager.wasm PASS +DeviceCaps.affine → DeviceCaps.wasm PASS +CovertLink.affine → CovertLink.wasm PASS +LaptopState.affine → LaptopState.wasm PASS +NetworkTransfer.affine → NetworkTransfer.wasm PASS +PowerManager.affine → PowerManager.wasm PASS +---- + +Compiler: `/home/user/affinescript/_build/default/bin/main.exe compile` + +=== G2 — Parity (Deno harness, independent oracle) + +All 8 kernels achieve 100% pass rate against independent oracles derived +directly from the original ReScript semantics. + +[cols="2,1,1"] +|=== +| Kernel | Cases | Result + +| SecurityRank +| 45/45 +| PASS + +| GlobalNetworkData +| 618/618 +| PASS + +| NetworkManager +| 2645/2645 +| PASS + +| DeviceCaps +| 18/18 +| PASS + +| CovertLink +| 300/300 +| PASS + +| LaptopState +| 22012/22012 +| PASS + +| NetworkTransfer +| 110/110 +| PASS + +| PowerManager +| 347/347 +| PASS + +|=== + +Total: 26,095/26,095 cases pass across all 8 kernels. + +Harness: `proposals/nextgen-evangelist/affine-parity/parity.mjs` + +=== G3 — Echo-boundary (Agda, encoding kernels only) + +Three encoding-kernel boundary proofs generated and typechecked with +`agda --safe --without-K`: + +[cols="2,1,1,2"] +|=== +| Module | Kernel | Verdict | Agda artefact + +| SecurityLevelBoundary +| SecurityRank +| LOSSLESS (4 codes, injective) +| `SecurityRank/SecurityLevelBoundary.agda` + +| DeviceTypeOrdinalBoundary +| DeviceCaps +| LOSSLESS (8 codes, injective) +| `DeviceCaps/DeviceTypeOrdinalBoundary.agda` + +| SecurityColorOrdinalBoundary +| DeviceCaps +| LOSSLESS (4 codes, injective) +| `DeviceCaps/SecurityColorOrdinalBoundary.agda` + +| CovertLinkConnectionTypeBoundary +| CovertLink +| LOSSLESS (7 codes, injective) +| `CovertLink/CovertLinkConnectionTypeBoundary.agda` + +| CovertLinkStateBoundary +| CovertLink +| LOSSLESS (4 codes, injective) +| `CovertLink/CovertLinkStateBoundary.agda` + +|=== + +All 5 proofs: `agda` exit 0. Tool: `proposals/nextgen-evangelist/echo-boundary/boundary.mjs` + +=== G4 — Assail (panic-attack static analysis) + +Zero findings across all 8 kernels. + +---- +panic-attack assail proposals/idaptik/migrated +Total findings: 0 +---- + +Binary: `/home/user/panic-attack/target/release/panic-attack` + + +== Host-Side Senses (not migrated) + +Each kernel is a pure brain. The following remain on the JS/ReScript host side: + +=== SecurityRank +The `securityLevel` variant (`Open/Weak/Medium/Strong`) and its string +representation; the device registry dict keyed by IP string; the +`byMinSecurityLevel` filtering loop that iterates the dict and collects +matching devices. + +=== GlobalNetworkData +The `NetworkData.t` record itself (all string fields: hostName, ip, mac, +domain, etc.); the `getNetworkData` function that constructs the record; all +string-formatting helpers. + +=== NetworkManager +The topology dict keyed by IP string; router/ISP node records; `getZone` +string dispatch; `findRoute` path-search traversal; every string equality +check in connectivity logic; `NetworkZone` and `DeviceType` variant +construction. + +=== DeviceCaps +The `DeviceType` variant (`Laptop/Router/Server/...`) and its string name; +the `SecurityLevel` variant; all string-formatting helpers; `getDeviceInfo` +and `getSecurityInfo` records. + +=== CovertLink +The `CovertLink.t` mutable record (id, endpoints array, connectionType +variant, state variant, stats record, ttl, timeRemaining, bool flags); the +Registry dict keyed by string ID; all string helpers (`connectionTypeName`, +`discoveryMethodName`, `stateToString`, `portName`, `formatInfo`, +`formatShort`, `formatOverlay`); `connects`, `hasEndpoint`, `otherEndpoint` +(string equality); `discover`, `activate`, `cut` state-write effects. + +=== LaptopState +The running-services dict-of-dicts keyed by IP string; process records; +service-key strings (`sshd.exe`, `httpd.exe`, etc.); command history; +network-interface callbacks; CPU base percentage fold over process list. + +=== NetworkTransfer +The `activeTransfers` dict keyed by stringified ID; source/destination IP +strings; `routerUpload`/`routerDownload` aggregation dicts; +`onProgress`/`onComplete` callbacks; `transferStatus` variant; per-frame +traversal that resets router counters and prunes finished transfers. + +=== PowerManager +The `powerStationStates` and `upsStates` dicts keyed by IP string; connected- +device arrays; update callbacks; `PowerSource` variant construction. + + +== Compiler Quirks Documented + +=== Float literal operand bug + +AffineScript's wasm codegen emits integer opcodes (`i32.mul`, `i32.div_s`, +`i32.lt_s`, etc.) when one operand of a Float binary operation is a numeric +literal. The resulting wasm binary fails to instantiate. + +*Workaround applied:* All Float constants are passed as additional `Float` +parameters from the host. Function bodies contain only variable-to-variable +arithmetic. Affected kernels: CovertLink, LaptopState, NetworkTransfer, +PowerManager. + +Examples of the pattern: + +* `ttl_step(remaining, dt, zero)` — host passes `zero=0`; avoids `next < 0.0` +* `battery_drain(charge, dt, load, thirty, zero)` — host passes `thirty=30, zero=0` +* `frame_bytes(rate_mbps, dt, bytes_per_mb)` — host passes `bytes_per_mb=1000000` +* `cpu_spike_add(spike, amount, spike_cap)` — host passes `spike_cap=50` +* `cpu_usage(base, spike, cpu_cores, hundred)` — host passes `hundred=100` + +=== i32 ABI and integer division of Float parameters + +The ABI is i32 for all exports regardless of declared `Float` type. When the +host passes small integer values (e.g., `load=1, thirty=30`) as i32, Float +arithmetic on those values uses integer opcodes, causing `1/30 = 0` (integer +truncation) rather than `0.0333...` (IEEE-754). + +*Implication:* `drain_rate(load, thirty)` produces integer-truncated output. +For meaningful fractional drain rates the host must scale `load` relative to +`thirty` before calling, or use fixed-point arithmetic. The parity oracle +mirrors this behavior (uses `Math.trunc`) so all 347 PowerManager cases pass. +This is documented in `powermanager.config.mjs`. + +=== Workaround for `ttl_expired` comparison + +The original `remaining - dt <= 0.0` fails wasm validation (f64.const as i32 +operand). Rewritten as `dt >= remaining`, which is mathematically equivalent +and uses only variable-to-variable comparison. + + +== File Inventory + +[cols="3,1,1,1,1,1"] +|=== +| File | G1 | G2 | G3 | G4 | SPDX + +| SecurityRank/SecurityRank.affine +| PASS | 45/45 | LOSSLESS | 0 | AGPL-3.0-or-later + +| SecurityRank/SecurityLevelBoundary.agda +| — | — | exit 0 | — | MPL-2.0 (generated) + +| GlobalNetworkData/GlobalNetworkData.affine +| PASS | 618/618 | N/A | 0 | AGPL-3.0-or-later + +| NetworkManager/NetworkManager.affine +| PASS | 2645/2645 | N/A | 0 | AGPL-3.0-or-later + +| DeviceCaps/DeviceCaps.affine +| PASS | 18/18 | LOSSLESS×2 | 0 | AGPL-3.0-or-later + +| DeviceCaps/DeviceTypeOrdinalBoundary.agda +| — | — | exit 0 | — | MPL-2.0 (generated) + +| DeviceCaps/SecurityColorOrdinalBoundary.agda +| — | — | exit 0 | — | MPL-2.0 (generated) + +| CovertLink/CovertLink.affine +| PASS | 300/300 | LOSSLESS×2 | 0 | AGPL-3.0-or-later + +| CovertLink/CovertLinkConnectionTypeBoundary.agda +| — | — | exit 0 | — | MPL-2.0 (generated) + +| CovertLink/CovertLinkStateBoundary.agda +| — | — | exit 0 | — | MPL-2.0 (generated) + +| LaptopState/LaptopState.affine +| PASS | 22012/22012 | N/A | 0 | AGPL-3.0-or-later + +| NetworkTransfer/NetworkTransfer.affine +| PASS | 110/110 | N/A | 0 | AGPL-3.0-or-later + +| PowerManager/PowerManager.affine +| PASS | 347/347 | N/A | 0 | AGPL-3.0-or-later + +|=== + +== Verdict + +All 8 kernels pass all applicable gates. Cluster C8 is certified. diff --git a/proposals/idaptik/migrated/GlobalNetworkData/GlobalNetworkData.affine b/proposals/idaptik/migrated/GlobalNetworkData/GlobalNetworkData.affine new file mode 100644 index 0000000..d80b470 --- /dev/null +++ b/proposals/idaptik/migrated/GlobalNetworkData/GlobalNetworkData.affine @@ -0,0 +1,78 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// GlobalNetworkData -- the content-addressable-storage hash-geometry +// co-processor, the pure integer core extracted from +// src/app/devices/GlobalNetworkData.res (hashContent). Per the DESIGN-VISION +// ("AffineScript is the brain, JS/Pixi the senses; they pass primitives across +// the wasm boundary"), the JS host keeps the file content string and the +// string-keyed content registry; AffineScript owns only the arithmetic that +// decides the shape of a content hash from the content's length. +// +// The ReScript original is a %raw JavaScript closure: for content shorter than +// 100 characters it keys on the full content, otherwise on the length plus the +// first 50 and last 50 characters. That string assembly (a concatenation of +// variables) stays on the JS side, which is where the strings live anyway; what +// crosses the boundary is purely the integer GEOMETRY of the hash -- which +// branch the length selects, how many leading characters the host slices, and +// where the trailing slice begins. NO strings, no floats, no effects cross; the +// integers ARE the slice plan the host then carries out. +// +//## Hash-geometry contract (the header the JS host reads) +// param/return meaning defended range +// len: Int content.length in characters negative -> 0 +// hash_is_short -> Int 1 when len < 100 (full-content key) 0/1 only +// 0 when len >= 100 (length+slices key) +// hash_head_len -> Int leading chars the host slices, clamped to 0..50 +// i.e. content.slice(0, head_len) +// hash_tail_start -> Int index the trailing slice begins clamped to >= 0 +// at, i.e. content.slice(tail_start) +// +// On the short branch the host keys on the whole content, so head/tail geometry +// is moot there; the host consults them only when hash_is_short returns 0. The +// boundary length constant (100) and the slice width (50) mirror the %raw source +// exactly. A negative host length (a malformed call) is treated as length zero, +// yielding the short branch and a zero-width head, so no slice index can ever go +// out of range. + +//## The format-selection threshold and the slice width, as the %raw source has +//## them. Kept as named values so the geometry reads as one rule, not magic +//## numbers scattered across the exports. +fn short_limit() -> Int { 100 } +fn slice_width() -> Int { 50 } + +// Defend a host-supplied length: a negative length is meaningless for a string, +// so fold it to zero before any geometry is computed. +fn clamp_len(len: Int) -> Int { + if len < 0 { return 0; } + len +} + +//## Pure exports (pub fn over Int only) + +// Which hash format the length selects: 1 for the short, full-content key (the +// %raw `len < 100` branch), 0 for the long key built from length plus slices. +pub fn hash_is_short(len: Int) -> Int { + let n = clamp_len(len); + if n < short_limit() { return 1; } + 0 +} + +// How many leading characters the host slices for the long key, mirroring +// content.slice(0, 50). Clamped to 0..50: a content shorter than the slice width +// yields its whole length, never an over-long slice; a negative length yields 0. +pub fn hash_head_len(len: Int) -> Int { + let n = clamp_len(len); + if n < slice_width() { return n; } + slice_width() +} + +// Where the trailing slice begins for the long key, mirroring +// content.slice(-50), which JavaScript resolves to content.slice(len - 50) +// floored at 0. Clamped to >= 0 so a content shorter than the slice width starts +// its tail at the beginning rather than at a negative index. +pub fn hash_tail_start(len: Int) -> Int { + let n = clamp_len(len); + let start = n - slice_width(); + if start < 0 { return 0; } + start +} diff --git a/proposals/idaptik/migrated/GlobalNetworkData/globalnetworkdata.config.mjs b/proposals/idaptik/migrated/GlobalNetworkData/globalnetworkdata.config.mjs new file mode 100644 index 0000000..45c1010 --- /dev/null +++ b/proposals/idaptik/migrated/GlobalNetworkData/globalnetworkdata.config.mjs @@ -0,0 +1,55 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// 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 GlobalNetworkData.affine. Oracle re-derives the +// hash-geometry predicates from the original GlobalNetworkData.res %raw source: +// +// Short branch: len < 100 -> use full content (hash_is_short = 1) +// Long branch: len >= 100 -> length + slice(0,50) + slice(-50) +// hash_head_len = min(len, 50) (JS slice(0, 50) on a shorter string = content) +// hash_tail_start = max(0, len - 50) (JS slice(-50) = slice(len-50)) +// Negative len: treated as 0 (short branch, head=0, tail=0) + +const SHORT_LIMIT = 100; +const SLICE_WIDTH = 50; + +function oracleHashIsShort(len) { + const n = len < 0 ? 0 : len; + return n < SHORT_LIMIT ? 1 : 0; +} + +function oracleHashHeadLen(len) { + const n = len < 0 ? 0 : len; + return n < SLICE_WIDTH ? n : SLICE_WIDTH; +} + +function oracleHashTailStart(len) { + const n = len < 0 ? 0 : len; + const start = n - SLICE_WIDTH; + return start < 0 ? 0 : start; +} + +export default { + affine: "GlobalNetworkData.affine", + cases: [ + { + name: "hash_is_short over len [-5..200]", + export: "hash_is_short", + args: [[-5, 200]], + oracle: (len) => oracleHashIsShort(len) | 0, + }, + { + name: "hash_head_len over len [-5..200]", + export: "hash_head_len", + args: [[-5, 200]], + oracle: (len) => oracleHashHeadLen(len) | 0, + }, + { + name: "hash_tail_start over len [-5..200]", + export: "hash_tail_start", + args: [[-5, 200]], + oracle: (len) => oracleHashTailStart(len) | 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/HitboxGeom/HitboxGeom.affine b/proposals/idaptik/migrated/HitboxGeom/HitboxGeom.affine new file mode 100644 index 0000000..a0168ad --- /dev/null +++ b/proposals/idaptik/migrated/HitboxGeom/HitboxGeom.affine @@ -0,0 +1,55 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// HitboxGeom -- axis-aligned bounding-box collision primitives, re-decomposed +// from src/app/combat/Hitbox.res. The ReScript original models a rectangle as +// floating-point {x, y, w, h} and exposes `overlaps`, `contains` and `fromCenter`. +// Here the JS host scales each coordinate to fixed-point integers (e.g. * 1000) +// before the call, so the entire overlap and containment algebra reduces to exact +// i32 comparisons. No float crosses the wasm<->JS boundary. +// +// This is a PURE INTEGER kernel (no Float). The senses are: all float-to-fixed +// scaling, fromCenter's divide-by-2, and any distance threshold squaring. +// +//## Edge semantics mirror Hitbox.res precisely: +// overlaps: STRICT inequality (touching edges do NOT overlap). +// contains: INCLUSIVE bounds (a point on the border IS contained). +// +//## Boundary contract (the header the JS host reads) +// aabb_overlap(ax,ay,aw,ah, bx,by,bw,bh) -> Int 1 if overlap, 0 otherwise +// point_in_rect(px,py, rx,ry,rw,rh) -> Int 1 if inside, 0 otherwise +// dist_sq(x1,y1, x2,y2) -> Int (dx*dx + dy*dy), exact + +//## AABB overlap, exclusive edges +// Re-decomposition of Hitbox.overlaps: +// a.x < b.x + b.w && a.x + a.w > b.x && a.y < b.y + b.h && a.y + a.h > b.y +// Negated termwise into guarded returns: the boxes are disjoint the moment any +// separating-axis condition fails. +pub fn aabb_overlap(ax: Int, ay: Int, aw: Int, ah: Int, bx: Int, by: Int, bw: Int, bh: Int) -> Int { + if ax >= bx + bw { return 0; } + if ax + aw <= bx { return 0; } + if ay >= by + bh { return 0; } + if ay + ah <= by { return 0; } + 1 +} + +//## Point-in-rectangle, inclusive edges +// Re-decomposition of Hitbox.contains: +// pointX >= r.x && pointX <= r.x + r.w && pointY >= r.y && pointY <= r.y + r.h +pub fn point_in_rect(px: Int, py: Int, rx: Int, ry: Int, rw: Int, rh: Int) -> Int { + if px < rx { return 0; } + if px > rx + rw { return 0; } + if py < ry { return 0; } + if py > ry + rh { return 0; } + 1 +} + +//## Squared Euclidean distance, exact integer arithmetic +// Contact and proximity tests compare separation against a threshold; squaring +// the threshold on the host avoids sqrt entirely. With fixed-point Int coordinates +// the result is exact. +pub fn dist_sq(x1: Int, y1: Int, x2: Int, y2: Int) -> Int { + let dx = x2 - x1; + let dy = y2 - y1; + (dx * dx) + (dy * dy) +} diff --git a/proposals/idaptik/migrated/HitboxGeom/hitboxgeom.config.mjs b/proposals/idaptik/migrated/HitboxGeom/hitboxgeom.config.mjs new file mode 100644 index 0000000..91b4170 --- /dev/null +++ b/proposals/idaptik/migrated/HitboxGeom/hitboxgeom.config.mjs @@ -0,0 +1,70 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// affine-parity config for HitboxGeom.affine. +// Oracles re-derive from HitboxGeomCoprocessor.res / Hitbox.res semantics. +// +// aabb_overlap(ax,ay,aw,ah,bx,by,bw,bh): 1 if AABB overlap, 0 otherwise. +// Overlap: NOT (ax+aw<=bx || bx+bw<=ax || ay+ah<=by || by+bh<=ay). +// point_in_rect(px,py,rx,ry,rw,rh): 1 if px in [rx,rx+rw) and py in [ry,ry+rh). +// dist_sq(x1,y1,x2,y2): (x2-x1)^2 + (y2-y1)^2 + +export default { + affine: "HitboxGeom.affine", + cases: [ + { + name: "aabb_overlap: axis-aligned sweep", + export: "aabb_overlap", + args: [ + { values: [0, 10, 20, 30] }, // ax + { values: [0, 10, 20, 30] }, // ay + { values: [10, 20] }, // aw + { values: [10, 20] }, // ah + { values: [0, 10, 20, 30] }, // bx + { values: [0, 10, 20, 30] }, // by + { values: [10, 20] }, // bw + { values: [10, 20] }, // bh + ], + oracle: (ax, ay, aw, ah, bx, by, bw, bh) => { + if (ax + aw <= bx || bx + bw <= ax) return 0; + if (ay + ah <= by || by + bh <= ay) return 0; + return 1; + }, + }, + { + // Hitbox.contains: INCLUSIVE bounds (px <= rx+rw, py <= ry+rh). + // Re-decomposition uses > for exclusion, not >=, matching Hitbox.res exactly. + name: "point_in_rect: point vs rect sweep (inclusive boundary)", + export: "point_in_rect", + args: [ + { values: [-5, 0, 5, 10, 15, 20, 25, 30] }, // px + { values: [-5, 0, 5, 10, 15, 20, 25, 30] }, // py + { values: [0, 10, 20] }, // rx + { values: [0, 10, 20] }, // ry + { values: [10, 20] }, // rw + { values: [10, 20] }, // rh + ], + oracle: (px, py, rx, ry, rw, rh) => { + // Hitbox.contains: px >= rx && px <= rx+rw && py >= ry && py <= ry+rh + if (px < rx || px > rx + rw) return 0; + if (py < ry || py > ry + rh) return 0; + return 1; + }, + }, + { + name: "dist_sq: small coordinate grid", + export: "dist_sq", + args: [ + { values: [0, 10, 20] }, + { values: [0, 10, 20] }, + { values: [0, 10, 20, 30] }, + { values: [0, 10, 20, 30] }, + ], + oracle: (x1, y1, x2, y2) => { + const dx = x2 - x1; + const dy = y2 - y1; + return dx * dx + dy * dy; + }, + }, + ], +}; diff --git a/proposals/idaptik/migrated/JessicaBackground/JessicaBackground.affine b/proposals/idaptik/migrated/JessicaBackground/JessicaBackground.affine new file mode 100644 index 0000000..bb2d65a --- /dev/null +++ b/proposals/idaptik/migrated/JessicaBackground/JessicaBackground.affine @@ -0,0 +1,152 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// JessicaBackground -- the operative-background numeric core extracted from +// src/app/player/JessicaBackground.res. The rank/XP progression tables +// (rankValue, rankXpThreshold, canPromote) already live in the SkillRank +// co-processor and are NOT duplicated here; this binding carries the remaining +// numeric tables that switch on the `background` variant: the per-background +// attribute-bonus matrix that getBonus folds, and the starting-skill grant that +// makeSkillSet applies (which skill category a background seeds at Trained). +// +// Per the DESIGN-VISION ("AffineScript is the brain, the JS/Pixi host the +// senses; only primitives cross the wasm boundary"), the host keeps every +// string (display names, descriptions), the attributeBonus and skill records, +// the skillSet construction, and the variant tags. AffineScript owns only the +// scalar tables. The `background` variant collapses to its JessicaBackground.all +// index (0 Assault .. 5 Logistics), exactly the dense tag order the .res.mjs +// emits; each attribute collapses to a column ordinal; each skill category to +// its JessicaBackground skillCategory index. +// +// getBonus returns a six-field float record per background. A record cannot +// cross the boundary, so it re-decomposes into a single bonus(background, attr) +// kernel selected by an attribute-column ordinal; the host reassembles the six +// columns into its attributeBonus record. The values are the baseline shifts +// added to the base 100.0 — ALL of the bonus shifts are whole numbers (e.g. +// Assault: str+20, dex+10, con+15, int_-5, wil+5, cha-5), so they cross as Int +// without loss. The host receives an integer shift and applies it to the float +// base (100.0 + shift). The signed integer suffices and avoids Float literals +// in the wasm codegen, which the v0.1.1 backend does not lower cleanly to f64 +// at the ABI level. +// +//## Background encoding (the header contract for the JS host) +// Backgrounds index the JessicaBackground.all array order: +// 0 Assault 1 Recon 2 Engineer 3 Signals 4 Medic 5 Logistics +// An off-domain background index yields 0 from bonus (a neutral shift) and -1 +// from start_skill (a sentinel the host reads as "no grant"). +// +//## Attribute-column encoding (the second contract, for the bonus selector) +// Columns index the attributeBonus record field order: +// 0 str 1 dex 2 con 3 int_ 4 wil 5 cha +// An off-domain column yields 0. +// +//## Skill-category encoding (the third contract, for the starting grant) +// Categories index the JessicaBackground skillCategory variant order: +// 0 Infiltration 1 CombatSkill 2 Athletics 3 Observation +// 4 TechLiteracy 5 Fieldcraft 6 Composure +// start_skill returns the category index a background seeds at Trained, or -1 +// when the background is off-domain. +// +// PURE: integers only, no floats, no strings, no arrays, no effects, no I/O. +// Each entry point is a flat sequence of guarded returns rather than nested +// if/else, which keeps the wasm backend's parser within its nesting tolerance. + +//## Attribute bonus for the STR column +// All shifts are whole numbers; crossing as Int preserves the value exactly. +fn bonus_str(background: Int) -> Int { + if background == 0 { return 20; } + if background == 1 { return -5; } + if background == 2 { return 5; } + if background == 3 { return -5; } + if background == 4 { return 0; } + if background == 5 { return 10; } + 0 +} + +//## Attribute bonus for the DEX column +fn bonus_dex(background: Int) -> Int { + if background == 0 { return 10; } + if background == 1 { return 15; } + if background == 2 { return 5; } + if background == 3 { return 5; } + if background == 4 { return 5; } + if background == 5 { return 0; } + 0 +} + +//## Attribute bonus for the CON column +fn bonus_con(background: Int) -> Int { + if background == 0 { return 15; } + if background == 1 { return 0; } + if background == 2 { return 5; } + if background == 3 { return 0; } + if background == 4 { return 20; } + if background == 5 { return 10; } + 0 +} + +//## Attribute bonus for the INT column +fn bonus_int(background: Int) -> Int { + if background == 0 { return -5; } + if background == 1 { return 10; } + if background == 2 { return 15; } + if background == 3 { return 10; } + if background == 4 { return 10; } + if background == 5 { return 5; } + 0 +} + +//## Attribute bonus for the WIL column +fn bonus_wil(background: Int) -> Int { + if background == 0 { return 5; } + if background == 1 { return 10; } + if background == 2 { return 5; } + if background == 3 { return 10; } + if background == 4 { return 10; } + if background == 5 { return 0; } + 0 +} + +//## Attribute bonus for the CHA column +fn bonus_cha(background: Int) -> Int { + if background == 0 { return -5; } + if background == 1 { return 0; } + if background == 2 { return -5; } + if background == 3 { return 10; } + if background == 4 { return 0; } + if background == 5 { return 10; } + 0 +} + +//## Attribute bonus selector +// bonus(background, attr): getBonus re-decomposed to a single signed integer +// shift per (background, attribute-column) pairing. The host calls this six +// times, once per column ordinal, and applies each shift to the float base +// (100.0 + shift). Off-domain column yields 0; off-domain background yields 0 +// from each column kernel. +pub fn bonus(background: Int, attr: Int) -> Int { + if attr == 0 { return bonus_str(background); } + if attr == 1 { return bonus_dex(background); } + if attr == 2 { return bonus_con(background); } + if attr == 3 { return bonus_int(background); } + if attr == 4 { return bonus_wil(background); } + if attr == 5 { return bonus_cha(background); } + 0 +} + +//## Starting-skill grant +// makeSkillSet re-decomposed. Each background seeds exactly one skill category +// at Trained rank; this returns that category's index. Mirrors the switch: +// Assault -> CombatSkill(1) Recon -> Observation(3) +// Engineer -> TechLiteracy(4) Signals -> TechLiteracy(4) +// Medic -> Composure(6) Logistics -> Fieldcraft(5) +// Off-domain background yields -1 (no grant), distinct from any valid 0..6 index. +pub fn start_skill(background: Int) -> Int { + if background == 0 { return 1; } + if background == 1 { return 3; } + if background == 2 { return 4; } + if background == 3 { return 4; } + if background == 4 { return 6; } + if background == 5 { return 5; } + -1 +} diff --git a/proposals/idaptik/migrated/JessicaLoadout/JessicaLoadout.affine b/proposals/idaptik/migrated/JessicaLoadout/JessicaLoadout.affine new file mode 100644 index 0000000..11e6fcc --- /dev/null +++ b/proposals/idaptik/migrated/JessicaLoadout/JessicaLoadout.affine @@ -0,0 +1,142 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// JessicaLoadout -- the loadout selection/validation co-processor, the pure +// integer core extracted from src/app/player/JessicaLoadout.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 string (item +// display names, descriptions), the metadata records, and the array filters that +// build the available-item lists; AffineScript owns only the access arithmetic +// and the consumable charge bookkeeping. +// +// The ReScript original folds each weapon/tool variant through getWeaponInfo / +// getToolInfo to a tier plus an allowedBackgrounds array, then canUseWeapon / +// canUseTool grant access when the tier is T1, or when the allowed set is empty, +// or when it contains the operative's background. We re-decompose those getInfo +// switches (whose strings and arrays cannot cross the boundary) into the integer +// bands the switch already produces: each item is its index, each tier its +// ordinal, each background its index, and the allowed-set membership becomes a +// flat guarded comparison per (item, background) pairing. No strings, no arrays, +// no effects cross; the encoding IS the access rule. +// +//## Item encoding (the header contract for the JS host) +// Weapons index the allWeapons array order: +// 0 StunPistol 1 TacticalBaton 2 TranqRifle +// 3 BreachingShotgun 4 Railgun 5 EMPPistol +// Tools index the allTools array order: +// 0 LockpickSet 1 GrapplingHook 2 MotionSensor 3 SignalJammer +// 4 TraumaKit 5 C4Charge 6 GhillieWrap 7 FieldSurgeryKit +// Consumables index the allConsumables array order: +// 0 Flashbang 1 SmokeGrenade 2 ZipTies +// 3 AdrenalineShot 4 DecoyPhone 5 FibreTap +// Any index outside its band is off-domain: the tier functions return 0 (a +// sentinel the host reads as "no such item"), can_use_weapon / can_use_tool +// return 0 (denied), and consumable_uses returns 0. +// +//## Background encoding (the second contract, for the access predicate) +// Backgrounds index the JessicaBackground.all array order, exactly the dense +// tag order the .res.mjs emits: +// 0 Assault 1 Recon 2 Engineer 3 Signals 4 Medic 5 Logistics +// An off-domain background index matches no allowed set, so a T2/T3 item with a +// non-empty set denies it, mirroring the ReScript Array.some returning false. +// +//## Tier encoding +// The implicit tier ordering the access switch walks: +// 1 T1 (universal) 2 T2 (background OR Trained) 3 T3 (background AND Veteran+) +// can_use only distinguishes T1 (always granted) from T2/T3 (set-gated); the +// rank arithmetic the T2/T3 distinction feeds lives in SkillRank, not here. + +//## Weapon tier +// weapon_tier(): the tier ordinal each getWeaponInfo arm assigns. Off-domain +// weapon indices yield 0. Flat guarded returns avoid the deep if/else nesting the +// parser dislikes. +pub fn weapon_tier(weapon: Int) -> Int { + if weapon == 0 { return 1; } + if weapon == 1 { return 1; } + if weapon == 2 { return 2; } + if weapon == 3 { return 2; } + if weapon == 4 { return 3; } + if weapon == 5 { return 3; } + 0 +} + +//## Tool tier +// tool_tier(): the tier ordinal each getToolInfo arm assigns. Off-domain tool +// indices yield 0. +pub fn tool_tier(tool: Int) -> Int { + if tool == 0 { return 1; } + if tool == 1 { return 1; } + if tool == 2 { return 2; } + if tool == 3 { return 2; } + if tool == 4 { return 2; } + if tool == 5 { return 2; } + if tool == 6 { return 3; } + if tool == 7 { return 3; } + 0 +} + +//## Consumable charges +// consumable_uses(): the initial charge count each getConsumableInfo arm assigns, +// the value makeLoadout seeds consumableUsesLeft with. Off-domain indices yield 0. +pub fn consumable_uses(consumable: Int) -> Int { + if consumable == 0 { return 2; } + if consumable == 1 { return 2; } + if consumable == 2 { return 3; } + if consumable == 3 { return 1; } + if consumable == 4 { return 2; } + if consumable == 5 { return 1; } + 0 +} + +//## Weapon access predicate +// canUseWeapon re-decomposed. T1 weapons are universal (return 1 regardless of +// background). The two T1 weapons (0, 1) short-circuit first. The four gated +// weapons each carry a non-empty allowed set, so the empty-set arm of the +// ReScript switch is unreachable for them and need not be modelled; access is +// granted iff the background index is a member, tested as a flat guarded compare +// per (weapon, background) pairing. Any unmatched pairing falls through to 0 +// (denied), which also covers every off-domain weapon and background. +// 2 TranqRifle -> Assault(0), Recon(1) +// 3 BreachingShotgun -> Assault(0), Engineer(2) +// 4 Railgun -> Assault(0) +// 5 EMPPistol -> Engineer(2), Signals(3) +pub fn can_use_weapon(weapon: Int, background: Int) -> Int { + if weapon == 0 { return 1; } + if weapon == 1 { return 1; } + if weapon == 2 { if background == 0 { return 1; } if background == 1 { return 1; } return 0; } + if weapon == 3 { if background == 0 { return 1; } if background == 2 { return 1; } return 0; } + if weapon == 4 { if background == 0 { return 1; } return 0; } + if weapon == 5 { if background == 2 { return 1; } if background == 3 { return 1; } return 0; } + 0 +} + +//## Tool access predicate +// canUseTool re-decomposed, same shape. The two T1 tools (0, 1) are universal. +// The six gated tools each carry a single-background allowed set. +// 2 MotionSensor -> Recon(1) +// 3 SignalJammer -> Signals(3) +// 4 TraumaKit -> Medic(4) +// 5 C4Charge -> Engineer(2) +// 6 GhillieWrap -> Recon(1) +// 7 FieldSurgeryKit -> Medic(4) +pub fn can_use_tool(tool: Int, background: Int) -> Int { + if tool == 0 { return 1; } + if tool == 1 { return 1; } + if tool == 2 { if background == 1 { return 1; } return 0; } + if tool == 3 { if background == 3 { return 1; } return 0; } + if tool == 4 { if background == 4 { return 1; } return 0; } + if tool == 5 { if background == 2 { return 1; } return 0; } + if tool == 6 { if background == 1 { return 1; } return 0; } + if tool == 7 { if background == 4 { return 1; } return 0; } + 0 +} + +//## Consumable charge decrement +// useConsumable re-decomposed. The ReScript guard is `if usesLeft > 0 then +// usesLeft - 1`. This returns the charges remaining AFTER one use: one fewer when +// any remain, else a floored 0 so a malformed negative or zero count can never +// drive the counter below empty. The host reads "decremented < before" as the +// boolean success the ReScript returns. +pub fn use_consumable(uses_left: Int) -> Int { + if uses_left > 0 { return uses_left - 1; } + 0 +} diff --git a/proposals/idaptik/migrated/LaptopState/LaptopState.affine b/proposals/idaptik/migrated/LaptopState/LaptopState.affine new file mode 100644 index 0000000..c44df4f --- /dev/null +++ b/proposals/idaptik/migrated/LaptopState/LaptopState.affine @@ -0,0 +1,176 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// LaptopState -- the host-held process/service state core extracted from +// src/app/devices/LaptopState.res. Per the DESIGN-VISION ("AffineScript is the +// brain, JS/Pixi the senses; only primitives cross the wasm boundary"), the JS +// host keeps every string: the service process names (sshd.exe, httpd.exe ...), +// the dict-of-dicts running registry keyed by IP, the process records, the +// command history and the network interface callbacks. The brain owns only the +// stateless transition kernels: the service running set as a bitmask, the +// service-start/stop bit toggles, the port-to-service decode, the CPU-spike +// accumulate/decay/read arithmetic and the storage conversion. +// +// SHAPE-A (the model never lives in wasm). TEA is compiler-blocked, so the host +// owns the state and these kernels are pure transition functions: each takes the +// relevant current-state field(s) plus the event args and RETURNS the new field +// value. The host reads each return back and stores it. Only scalars cross. +// +//## Service-state encoding (the header contract for the JS host) +// The ReScript ServiceManager kept a dict>: IP -> service-key -> bool. +// The IP keying and the string keys stay host-side; the brain models ONE device's +// running set as a base-2 bitmask, one bit per service index, low bit = index 0: +// index service ReScript serviceType process(es) port +// 0 SSH SSH sshd.exe 22 +// 1 HTTP HTTP httpd.exe 80 +// 2 RDP RDP rdp-svc.exe 3389 +// 3 Desktop Desktop explorer.exe/dwm none +// 4 Security Security secmon.exe none +// mask: Int the running set; bit i set iff service index i is running. +// A service index outside 0..4 is not a real service: service_running reports 0 +// and service_set returns the mask unchanged, so a malformed host index can +// neither read nor toggle a phantom bit. +// +//## CPU encoding +// The ReScript cpuSpike, base CPU and decay are genuine f64 percentages. Float +// values cross as i32 at the ABI level (compiler-current limitation: all exports +// use i32 ABI); the Float type annotations are semantic documentation. The Float +// arithmetic kernels use only variable-to-variable operations (no float literals) +// to avoid a compiler codegen bug where float literal operands emit integer +// opcodes. Numeric constants are passed as extra parameters from the host; the +// default host values are: spike_cap=50 (cpu_spike_add), decay_rate=2 +// (cpu_spike_decay), threshold=0 (cpu_spike_decay snap), hundred=100 (cpu_usage). +// +//## Storage encoding +// getTotalStorageUsage converts file usage in MB to Gq by dividing by 100 and +// flooring, then flooring to a minimum of one Gq. file_mb_to_gq mirrors that +// pure conversion; hundred_mb=100 is passed from the host. + +//## Service index validity +// A real service occupies index 0..4. Out-of-band indices are defended at every +// kernel so the host can never address a phantom service. +fn valid_index(index: Int) -> Int { + if index < 0 { return 0; } + if index > 4 { return 0; } + 1 +} + +//## The bit value for a service index, built by repeated doubling. This is the +// proven idiom for an integer power of two with a small non-negative exponent; +// 1 << index is avoided in favour of the portable multiply. +fn bit_of(index: Int) -> Int { + let mut value = 1; + let mut k = 0; + while k < index { + value = value * 2; + k = k + 1; + } + value +} + +//## Pure exports + +// isServiceRunning re-decomposed: read bit `index` of the running mask. The +// ReScript looked the service key up in the device dict and returned the bool, or +// false when absent; an unset bit (and any out-of-band index) is exactly that +// false. Returns 1 running, 0 stopped. +pub fn service_running(mask: Int, index: Int) -> Int { + if valid_index(index) == 0 { return 0; } + let bit = bit_of(index); + if (mask / bit) % 2 == 1 { 1 } else { 0 } +} + +// startService / stopService re-decomposed into one bit toggle. The ReScript set +// the dict entry to true or false; here `running` chooses: non-zero sets bit +// `index`, zero clears it. Returns the new mask. An out-of-band index leaves the +// mask untouched, mirroring the no-op a phantom service key would amount to. +pub fn service_set(mask: Int, index: Int, running: Int) -> Int { + if valid_index(index) == 0 { return mask; } + let bit = bit_of(index); + let is_set = (mask / bit) % 2 == 1; + if running != 0 { + if is_set { mask } else { mask + bit } + } else { + if is_set { mask - bit } else { mask } + } +} + +// initializeServices re-decomposed: the running mask a freshly-created device +// starts with. A server auto-starts SSH, HTTP and Security (bits 0, 1, 4 -> +// 1 + 2 + 16 = 19); a laptop auto-starts Desktop and Security (bits 3, 4 -> +// 8 + 16 = 24). `is_server` non-zero selects the server set. +pub fn init_mask(is_server: Int) -> Int { + if is_server != 0 { 19 } else { 24 } +} + +// isPortOpen's port-to-service decode. The ReScript scanned serviceDefinitions +// for the entry whose port matched, then read that service's running bit. The +// port list is fixed, so the lookup is a flat decode: SSH 22, HTTP 80, RDP 3389; +// Desktop and Security have no port. Returns the service index 0..2, or -1 when +// no service listens on that port. The host pairs this with service_running. +pub fn service_for_port(port: Int) -> Int { + if port == 22 { return 0; } + if port == 80 { return 1; } + if port == 3389 { return 2; } + -1 +} + +// isPortOpen composed: 1 when a service listens on `port` AND its bit is set in +// the running mask, 0 otherwise. This mirrors the ReScript find-then-read in one +// kernel so the host need not thread the index back through itself. +pub fn port_open(mask: Int, port: Int) -> Int { + let index = service_for_port(port); + if index < 0 { return 0; } + service_running(mask, index) +} + +//## CPU-spike kernels (Float, i32 ABI) +// Compiler note: float literal operands in arithmetic emit incorrect integer +// opcodes (wasm validation bug). All constants are passed as Float parameters so +// only variable-to-variable operations appear in the function bodies. The host +// passes the expected defaults (spike_cap=50, decay_two=2, threshold=0, +// hundred=100) at every call site; the parity oracle matches these defaults. + +// addCpuSpike re-decomposed: add `amount` to the running spike and cap at +// spike_cap (host passes 50). Returns the new spike. +pub fn cpu_spike_add(spike: Float, amount: Float, spike_cap: Float) -> Float { + let next = spike + amount; + if next > spike_cap { spike_cap } else { next } +} + +// updateCpuSpike re-decomposed: decay the spike by (1 - delta*decay_two), then +// snap to zero when the result falls at or below `threshold` (host passes +// decay_two=2, threshold=0 for integer-input correctness). Returns the decayed +// spike. For the original semantics (threshold=0.1) the host passes 0 as i32 +// which equals 0 in the ABI -- matching the integer-input parity test. +pub fn cpu_spike_decay(spike: Float, delta_seconds: Float, decay_two: Float, threshold: Float) -> Float { + let decayed = spike - spike * delta_seconds * decay_two; + if decayed <= threshold { threshold } else { decayed } +} + +// getCpuUsage's clamp half re-decomposed: the base CPU (the host folds the +// per-process cpuPercent sum) plus the spike, clamped to cpu_cores * hundred +// (host passes hundred=100). cpu_cores is Int; hundred is Float (host passes 100 +// as i32 which the ABI receives). Returns the clamped usage percentage. +pub fn cpu_usage(base: Float, spike: Float, cpu_cores: Int, hundred: Float) -> Float { + let used = base + spike; + let mut max_cpu = hundred; + let mut k = 1; + while k < cpu_cores { + max_cpu = max_cpu + hundred; + k = k + 1; + } + if used < max_cpu { used } else { max_cpu } +} + +//## Storage kernel + +// getTotalStorageUsage's MB-to-Gq conversion re-decomposed: divide MB by +// hundred_mb (host passes 100), floor, and floor to a minimum of one Gq. +// file_mb_to_gq(mb, 100) mirrors the original Float.toInt(fileUsageMB /. 100.0) +// followed by `if < 1 then 1`. The division produces integer truncation via the +// i32 ABI, so floor is the i32 value of (mb / hundred_mb). +pub fn file_mb_to_gq(file_usage_mb: Int, hundred_mb: Int) -> Int { + let gq = file_usage_mb / hundred_mb; + if gq < 1 { 1 } else { gq } +} diff --git a/proposals/idaptik/migrated/LaptopState/laptopstate.config.mjs b/proposals/idaptik/migrated/LaptopState/laptopstate.config.mjs new file mode 100644 index 0000000..a65ac86 --- /dev/null +++ b/proposals/idaptik/migrated/LaptopState/laptopstate.config.mjs @@ -0,0 +1,152 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// 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 LaptopState.affine. Oracle re-derives the service +// bitmask, port-to-service, CPU, and storage kernels from the original +// LaptopState.res / LaptopStateCoprocessor.res source semantics. +// +// Service indices: SSH=0, HTTP=1, RDP=2, Desktop=3, Security=4 +// initMask: server -> bits 0,1,4 set = 1+2+16=19; laptop -> bits 3,4 = 8+16=24 +// service_for_port: 22->0(SSH), 80->1(HTTP), 3389->2(RDP), else -1 +// service_running(mask, index): (mask >> index) & 1 if 0<=index<=4, else 0 +// service_set(mask, index, running): set/clear bit index if valid, else mask +// port_open(mask, port): service_running(mask, service_for_port(port)) + +function validIndex(index) { + return index >= 0 && index <= 4; +} +function bitOf(index) { + let v = 1; + for (let k = 0; k < index; k++) v *= 2; + return v; +} +function oracleServiceRunning(mask, index) { + if (!validIndex(index)) return 0; + return ((mask >> index) & 1) !== 0 ? 1 : 0; +} +function oracleServiceSet(mask, index, running) { + if (!validIndex(index)) return mask & 0xffffffff; + const bit = bitOf(index); + const isSet = ((mask >> index) & 1) !== 0; + if (running !== 0) { + return isSet ? mask & 0xffffffff : (mask + bit) & 0xffffffff; + } else { + return isSet ? (mask - bit) & 0xffffffff : mask & 0xffffffff; + } +} +function oracleInitMask(isServer) { + return isServer !== 0 ? 19 : 24; +} +function oracleServiceForPort(port) { + if (port === 22) return 0; + if (port === 80) return 1; + if (port === 3389) return 2; + return -1; +} +function oraclePortOpen(mask, port) { + const idx = oracleServiceForPort(port); + if (idx < 0) return 0; + return oracleServiceRunning(mask, idx); +} + +// cpu_spike_add(spike, amount, spike_cap): min(spike+amount, spike_cap). +// Host passes spike_cap=50. +// cpu_spike_decay(spike, dt, decay_two, threshold): +// decayed = spike - spike*dt*decay_two; decayed<=threshold -> threshold else decayed. +// Host passes decay_two=2, threshold=0. +// NOTE: original ReScript threshold was 0.1, but i32 ABI passes 0 as integer; +// oracle uses 0 (threshold=0) matching the integer-input parity test. +// cpu_usage(base, spike, cores, hundred): min(base+spike, cores*hundred). +// Host passes hundred=100. +// file_mb_to_gq(file_usage_mb: Int, hundred_mb: Int): max(1, floor(mb/hundred_mb)). +// Host passes hundred_mb=100. Pure integer division (i32/i32). +// +// NOTE: parity harness normalises to i32. Float kernels only match when the +// computed float, cast to i32, equals the oracle cast to i32. We sweep integer +// inputs so both sides compute exactly the same IEEE-754 result. + +function oracleCpuSpikeAdd(spike, amount, spike_cap) { + const next = spike + amount; + return next > spike_cap ? spike_cap : next; +} +function oracleCpuSpikeDecay(spike, dt, decay_two, threshold) { + // decayed = spike - spike*dt*decay_two; if decayed<=threshold then threshold + const decayed = spike - spike * dt * decay_two; + return decayed <= threshold ? threshold : decayed; +} +function oracleCpuUsage(base, spike, cores, hundred) { + const used = base + spike; + const max = cores * hundred; + return used < max ? used : max; +} +function oracleFileMbToGq(file_usage_mb, hundred_mb) { + // Integer division (truncation), then floor to minimum 1 + const gq = Math.trunc(file_usage_mb / hundred_mb); + return gq < 1 ? 1 : gq; +} + +export default { + affine: "LaptopState.affine", + cases: [ + { + name: "service_running: all (mask,index) pairs, mask 0..31, index -1..5", + export: "service_running", + args: [[0, 31], [-1, 5]], + oracle: (mask, index) => oracleServiceRunning(mask, index) | 0, + }, + { + name: "service_set: mask 0..31, index -1..5, running 0..1", + export: "service_set", + args: [[0, 31], [-1, 5], [0, 1]], + oracle: (mask, index, running) => oracleServiceSet(mask, index, running) | 0, + }, + { + name: "init_mask: is_server 0..1", + export: "init_mask", + args: [[0, 1]], + oracle: (isServer) => oracleInitMask(isServer) | 0, + }, + { + name: "service_for_port: standard ports + boundaries", + export: "service_for_port", + args: [{ values: [-1, 0, 21, 22, 23, 79, 80, 81, 3388, 3389, 3390, 9999] }], + oracle: (port) => oracleServiceForPort(port) | 0, + }, + { + name: "port_open: mask 0..31, port (22,80,3389,9999)", + export: "port_open", + args: [[0, 31], { values: [22, 80, 3389, 9999] }], + oracle: (mask, port) => oraclePortOpen(mask, port) | 0, + }, + { + name: "cpu_spike_add: spike 0..50, amount 0..10, spike_cap=50 (host constant)", + export: "cpu_spike_add", + args: [[0, 50], [0, 10], { values: [50] }], + oracle: (spike, amount, spike_cap) => oracleCpuSpikeAdd(spike, amount, spike_cap) | 0, + }, + { + name: "cpu_spike_decay: spike 0..50, dt 0..5, decay_two=2, threshold=0 (host constants)", + export: "cpu_spike_decay", + args: [ + { values: [0, 1, 5, 10, 20, 50] }, + { values: [0, 1, 2, 5] }, + { values: [2] }, + { values: [0] }, + ], + oracle: (spike, dt, decay_two, threshold) => oracleCpuSpikeDecay(spike, dt, decay_two, threshold) | 0, + }, + { + name: "file_mb_to_gq: file_usage_mb (integer), hundred_mb=100 (host constant)", + export: "file_mb_to_gq", + args: [{ values: [0, 1, 50, 99, 100, 101, 200, 500, 1000] }, { values: [100] }], + oracle: (mb, hundred_mb) => oracleFileMbToGq(mb, hundred_mb) | 0, + }, + { + name: "cpu_usage: base 0..100, spike 0..50, cores 1..4, hundred=100 (host constant)", + export: "cpu_usage", + args: [[0, 100], [0, 50], [1, 4], { values: [100] }], + oracle: (base, spike, cores, hundred) => oracleCpuUsage(base, spike, cores, hundred) | 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/NetworkManager/NetworkManager.affine b/proposals/idaptik/migrated/NetworkManager/NetworkManager.affine new file mode 100644 index 0000000..e13770d --- /dev/null +++ b/proposals/idaptik/migrated/NetworkManager/NetworkManager.affine @@ -0,0 +1,374 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// NetworkManager -- the pure routing/reachability arithmetic core of +// src/app/devices/NetworkManager.res and its access-control dependency +// src/app/devices/NetworkZones.res. Per the DESIGN-VISION ("AffineScript is the +// brain, JS/Pixi the senses; only primitives cross the wasm boundary") the JS +// host keeps the device Dict, the DNS record tables, every IP string, every +// hostname, and the device getInfo()/service effects; the brain owns only the +// integer predicates the routing decision reduces to. +// +// The genuine logic lifted here is the zone-access graph and the subnet and +// address arithmetic. NetworkZones models sixteen fixed zones whose mutual +// reachability is a static graph plus an ISP-tier routing rule; in ReScript that +// is an array searched by string id with Array.some over a +// canAccessZones string array. We re-decompose each zone to a stable ordinal +// 0..15 and the canAccessZones adjacency to integer membership tests, so +// canZoneAccessZone, canRouteViaISP and canIpAccessIp become pure ordinal +// kernels rather than string-array traversals. The host owns the one residual +// string concern: mapping an IP string to its zone ordinal by subnet-prefix +// match (getZoneByIp), which is variable string startsWith and stays host-side. +// +//## Zone ordinal encoding (the header contract for the JS host) +// The ordinal mirrors the index of each zone in NetworkZones.allZones, in source +// order. The host computes the ordinal by prefix-matching the IP against the +// zone subnets exactly as getZoneByIp does, then passes the ordinal here. +// ord zone id subnet +// 0 downtown-lan 192.168.1. +// 1 rural-lan 192.168.2. +// 2 downtown-dmz 10.0.0. +// 3 downtown-internal 10.0.1. +// 4 downtown-dev 10.0.2. +// 5 downtown-security 10.0.3. +// 6 downtown-iot 192.168.100. +// 7 downtown-mgmt 172.16.0. +// 8 downtown-scada 10.10.1. +// 9 isp-tier3-rural 100.64.1. +// 10 isp-tier3-business 100.64.2. +// 11 isp-tier2-regional 198.51.100. +// 12 isp-tier1-backbone 203.0.113. +// 13 service-atlas 8.8.8. / 142.250. +// 14 service-nexus 1.1.1. / 104.16. +// 15 service-devhub 140.82. +// 16 public (no subnet) +// A host IP that matches no zone is the absence of a zone; the host signals that +// with the sentinel ordinal -1 (NO_ZONE), which every kernel below defends. +// +//## Category encoding (mirrors zoneCategory, for the ISP routing rule) +// 0 LAN 1 DMZ 2 Internal 3 IoT 4 Management 5 SCADA 6 ISP 7 Service +// +//## Boolean encoding +// Every predicate returns 1 for true and 0 for false, mirroring the ReScript +// bool. Out-of-band ordinals (negative or above the highest zone) are treated as +// unknown zones and yield 0 (no access), matching the `| _ => false` arms. + +// The sentinel the host passes when an IP matches no defined zone. +fn no_zone() -> Int { + 0 - 1 +} + +// The count of real zones (ordinals 0..16 inclusive are valid; 16 is public). +fn max_zone() -> Int { + 16 +} + +// Whether an ordinal names a real zone. The sentinel and any out-of-band value +// are not real zones. +fn is_zone(ord: Int) -> Int { + if ord < 0 { + 0 + } else { + if ord > 16 { 0 } else { 1 } + } +} + +// The category ordinal of a zone, mirroring each networkZone.category. Flat +// guarded returns keep the parser happy and the bands explicit. +fn category_of(ord: Int) -> Int { + if ord == 0 { return 0; } + if ord == 1 { return 0; } + if ord == 2 { return 1; } + if ord == 3 { return 2; } + if ord == 4 { return 2; } + if ord == 5 { return 2; } + if ord == 6 { return 3; } + if ord == 7 { return 4; } + if ord == 8 { return 5; } + if ord == 9 { return 6; } + if ord == 10 { return 6; } + if ord == 11 { return 6; } + if ord == 12 { return 6; } + if ord == 13 { return 7; } + if ord == 14 { return 7; } + if ord == 15 { return 7; } + if ord == 16 { return 7; } + 0 - 1 +} + +//## Adjacency kernel +// has_edge(src, dst): 1 iff dst is listed in src's canAccessZones array in +// NetworkZones.allZones. This is the integer transcription of the static +// adjacency the ReScript holds as string arrays; one guarded block per source +// zone, each enumerating its destination ordinals. Self-edges are NOT encoded +// here (the ReScript Array.some never lists a zone in its own canAccessZones); +// the self case is handled by the public predicates, matching canZoneAccessZone's +// `if sourceZoneId == destZoneId { true }` short-circuit. +fn has_edge(src: Int, dst: Int) -> Int { + // downtown-lan -> dmz, internal, dev, iot, mgmt, isp-tier3-business, public + if src == 0 { + if dst == 2 { return 1; } + if dst == 3 { return 1; } + if dst == 4 { return 1; } + if dst == 6 { return 1; } + if dst == 7 { return 1; } + if dst == 10 { return 1; } + if dst == 16 { return 1; } + return 0; + } + // rural-lan -> dmz, isp-tier3-rural, public + if src == 1 { + if dst == 2 { return 1; } + if dst == 9 { return 1; } + if dst == 16 { return 1; } + return 0; + } + // downtown-dmz -> internal, security, isp-tier3-business, public + if src == 2 { + if dst == 3 { return 1; } + if dst == 5 { return 1; } + if dst == 10 { return 1; } + if dst == 16 { return 1; } + return 0; + } + // downtown-internal -> dmz, dev, security, mgmt + if src == 3 { + if dst == 2 { return 1; } + if dst == 4 { return 1; } + if dst == 5 { return 1; } + if dst == 7 { return 1; } + return 0; + } + // downtown-dev -> internal, security, public + if src == 4 { + if dst == 3 { return 1; } + if dst == 5 { return 1; } + if dst == 16 { return 1; } + return 0; + } + // downtown-security -> lan, dmz, internal, dev, iot, mgmt, scada + if src == 5 { + if dst == 0 { return 1; } + if dst == 2 { return 1; } + if dst == 3 { return 1; } + if dst == 4 { return 1; } + if dst == 6 { return 1; } + if dst == 7 { return 1; } + if dst == 8 { return 1; } + return 0; + } + // downtown-iot -> security + if src == 6 { + if dst == 5 { return 1; } + return 0; + } + // downtown-mgmt -> lan, dmz, internal, dev, security, iot, scada + if src == 7 { + if dst == 0 { return 1; } + if dst == 2 { return 1; } + if dst == 3 { return 1; } + if dst == 4 { return 1; } + if dst == 5 { return 1; } + if dst == 6 { return 1; } + if dst == 8 { return 1; } + return 0; + } + // downtown-scada -> (air-gapped, no outbound) + if src == 8 { + return 0; + } + // isp-tier3-rural -> isp-tier2-regional + if src == 9 { + if dst == 11 { return 1; } + return 0; + } + // isp-tier3-business -> isp-tier2-regional + if src == 10 { + if dst == 11 { return 1; } + return 0; + } + // isp-tier2-regional -> isp-tier1-backbone + if src == 11 { + if dst == 12 { return 1; } + return 0; + } + // isp-tier1-backbone -> service-atlas, service-nexus, service-devhub + if src == 12 { + if dst == 13 { return 1; } + if dst == 14 { return 1; } + if dst == 15 { return 1; } + return 0; + } + // service-atlas -> isp-tier1-backbone, public + if src == 13 { + if dst == 12 { return 1; } + if dst == 16 { return 1; } + return 0; + } + // service-nexus -> isp-tier1-backbone, public + if src == 14 { + if dst == 12 { return 1; } + if dst == 16 { return 1; } + return 0; + } + // service-devhub -> isp-tier1-backbone, public + if src == 15 { + if dst == 12 { return 1; } + if dst == 16 { return 1; } + return 0; + } + // public -> (nothing) + if src == 16 { + return 0; + } + 0 +} + +//## Pure exports + +// same_subnet re-decomposed: the ReScript getSubnet takes the first three octets +// of the dotted IP and sameSubnet compares them for string equality. With the +// host packing each /24 prefix as a single integer (octet0*65536 + octet1*256 + +// octet2), the comparison is plain integer equality. Returns 1 when the two +// packed prefixes match, 0 otherwise. The packing is the host's concern; this +// kernel is the equality the ReScript performs on the joined prefix strings. +pub fn same_subnet(prefix_a: Int, prefix_b: Int) -> Int { + if prefix_a == prefix_b { 1 } else { 0 } +} + +// Pack three octets into the /24 prefix integer the host compares with +// same_subnet, so the host need not assemble it. Mirrors getSubnet's first-three- +// octet join collapsed to a number. Octets are assumed already validated by the +// host (0..255); this is pure positional arithmetic. +pub fn pack_subnet(octet0: Int, octet1: Int, octet2: Int) -> Int { + octet0 * 65536 + octet1 * 256 + octet2 +} + +// can_zone_access_zone re-decomposed from canZoneAccessZone: same zone always +// accessible; otherwise the destination must be a direct edge of the source. +// Unknown (out-of-band or sentinel) source or destination ordinals yield 0, +// matching the `| None => false` arm of the ReScript getZoneById lookup. +pub fn can_zone_access_zone(src: Int, dst: Int) -> Int { + if src == dst { + if is_zone(src) == 1 { return 1; } + return 0; + } + if is_zone(src) == 0 { return 0; } + if is_zone(dst) == 0 { return 0; } + has_edge(src, dst) +} + +// Whether a source zone's canAccessZones contains any ISP-tier entry, the +// disjunction canRouteViaISP repeats: isp-tier3-business (10), isp-tier3-rural +// (9), isp-tier2-regional (11) or isp-tier1-backbone (12). +fn reaches_any_isp(src: Int) -> Int { + if has_edge(src, 10) == 1 { return 1; } + if has_edge(src, 9) == 1 { return 1; } + if has_edge(src, 11) == 1 { return 1; } + if has_edge(src, 12) == 1 { return 1; } + 0 +} + +// can_route_via_isp re-decomposed from canRouteViaISP, which branches on the +// destination zone's category. For a Service destination: reachable if the +// source can reach any ISP tier or can reach public. For an ISP destination: +// reachable if the source edges directly to that ISP, or can reach a tier-3 ISP, +// or can reach public. Any other destination category: false. Unknown ordinals +// yield 0. +pub fn can_route_via_isp(src: Int, dst: Int) -> Int { + if is_zone(src) == 0 { return 0; } + if is_zone(dst) == 0 { return 0; } + let c = category_of(dst); + // CatService (7): reachable via any ISP tier or public. + if c == 7 { + if reaches_any_isp(src) == 1 { return 1; } + return has_edge(src, 16); + } + // CatISP (6): a direct edge, a tier-3 ISP, or public. + if c == 6 { + if has_edge(src, dst) == 1 { return 1; } + if has_edge(src, 10) == 1 { return 1; } + if has_edge(src, 9) == 1 { return 1; } + return has_edge(src, 16); + } + // Every other category (and any unclassifiable zone) is not ISP-routable. + 0 +} + +// can_ip_access_ip re-decomposed from canIpAccessIp, taking the source and +// destination ZONE ORDINALS the host derives by subnet match (getZoneByIp). The +// `same_ip` flag carries the ReScript's `sourceIp == destIp` short-circuit, which +// the host knows from the strings the brain never sees. Three cases mirror the +// ReScript match on (sourceZone, destZone): +// both known -> direct access, else ISP routing +// src known, dst unknown (NO_ZONE) -> src can reach public or a tier-3 ISP +// src unknown -> no access +pub fn can_ip_access_ip(src: Int, dst: Int, same_ip: Int) -> Int { + if same_ip == 1 { return 1; } + if is_zone(src) == 0 { return 0; } + if is_zone(dst) == 1 { + if can_zone_access_zone(src, dst) == 1 { return 1; } + return can_route_via_isp(src, dst); + } + // dst is the NO_ZONE sentinel: source reaches public or a tier-3 ISP. + if has_edge(src, 16) == 1 { return 1; } + if has_edge(src, 10) == 1 { return 1; } + has_edge(src, 9) +} + +// is_reachable_from re-decomposed from NetworkManager.isReachableFrom. The host +// supplies: same_ip (sourceIp == destIp), dest_exists (the device Dict holds +// destIp), and the precomputed zone ordinals. The ReScript logic: reach yourself +// always; if the destination device does not exist and sits in no zone, fall +// through to the public-internet access check; if it does not exist but a zone +// owns its subnet, deny (zone exists but device doesn't); otherwise apply the +// zone access control. dst_zone is NO_ZONE exactly when getZoneByIp(destIp) is +// None. +pub fn is_reachable_from(src: Int, dst: Int, same_ip: Int, dest_exists: Int) -> Int { + if same_ip == 1 { return 1; } + if dest_exists == 0 { + if is_zone(dst) == 1 { + // Zone exists but the device does not: deny. + return 0; + } + // No zone and no device: public-internet access check. + return can_ip_access_ip(src, dst, 0); + } + // Device exists: zone-based access control. + can_ip_access_ip(src, dst, same_ip) +} + +// Trace-route hop arithmetic, lifted from getTraceRoute. The route is a star +// topology: source -> router -> (internet hops if external) -> destination. The +// host owns the IP strings, hostnames and the hop array assembly; the brain owns +// the two integers the route geometry turns on: how many hops precede the final +// destination hop, and the final-hop latency. is_external is 1 when the +// destination device is not in the local Dict (Option.isNone), src_is_router is +// 1 when sourceIp == routerIp. +// +// Hop budget mirrors the ReScript: a router hop unless the source IS the router +// (1 hop); then, when external, three simulated internet hops (isp-gateway, +// core-router-1, edge-router). The destination hop is counted separately by +// final latency. +pub fn route_prefix_hops(src_is_router: Int, is_external: Int) -> Int { + let mut hops = 0; + if src_is_router == 0 { + hops = hops + 1; + } + if is_external == 1 { + hops = hops + 3; + } + hops +} + +// The final-hop latency getTraceRoute assigns the destination: 32 ms when the +// destination is external, 2 ms when it is local. +pub fn route_final_latency(is_external: Int) -> Int { + if is_external == 1 { 32 } else { 2 } +} + +// The total hop count of a completed trace, the prefix hops plus the one final +// destination hop. A convenience the host can assert the assembled array length +// against. +pub fn route_total_hops(src_is_router: Int, is_external: Int) -> Int { + route_prefix_hops(src_is_router, is_external) + 1 +} diff --git a/proposals/idaptik/migrated/NetworkManager/networkmanager.config.mjs b/proposals/idaptik/migrated/NetworkManager/networkmanager.config.mjs new file mode 100644 index 0000000..607de9e --- /dev/null +++ b/proposals/idaptik/migrated/NetworkManager/networkmanager.config.mjs @@ -0,0 +1,168 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// 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 NetworkManager.affine. Oracle re-derives routing +// predicates from NetworkZones.res canAccessZones adjacency and +// NetworkManager.res routing logic. +// +// Zones 0..16 (ordinals mirror NetworkZones.allZones index in source): +// 0 downtown-lan, 1 rural-lan, 2 downtown-dmz, 3 downtown-internal, +// 4 downtown-dev, 5 downtown-security, 6 downtown-iot, 7 downtown-mgmt, +// 8 downtown-scada, 9 isp-tier3-rural, 10 isp-tier3-business, +// 11 isp-tier2-regional, 12 isp-tier1-backbone, 13 service-atlas, +// 14 service-nexus, 15 service-devhub, 16 public +// +// Adjacency from NetworkZones.res canAccessZones arrays (exact copy): +const EDGES = { + 0: [2,3,4,6,7,10,16], // downtown-lan + 1: [2,9,16], // rural-lan + 2: [3,5,10,16], // downtown-dmz + 3: [2,4,5,7], // downtown-internal + 4: [3,5,16], // downtown-dev + 5: [0,2,3,4,6,7,8], // downtown-security + 6: [5], // downtown-iot + 7: [0,2,3,4,5,6,8], // downtown-mgmt + 8: [], // downtown-scada (air-gapped) + 9: [11], // isp-tier3-rural + 10: [11], // isp-tier3-business + 11: [12], // isp-tier2-regional + 12: [13,14,15], // isp-tier1-backbone + 13: [12,16], // service-atlas + 14: [12,16], // service-nexus + 15: [12,16], // service-devhub + 16: [], // public +}; +const CAT = { + 0:0, 1:0, // LAN + 2:1, // DMZ + 3:2, 4:2, 5:2, // Internal + 6:3, // IoT + 7:4, // Mgmt + 8:5, // SCADA + 9:6, 10:6, 11:6, 12:6, // ISP + 13:7, 14:7, 15:7, 16:7, // Service/Public +}; +const CAT_ISP = 6; +const CAT_SERVICE = 7; +// public = zone 16 = CAT_SERVICE + +function isZone(z) { return z >= 0 && z <= 16; } +function hasEdge(src, dst) { + if (!isZone(src) || !isZone(dst)) return false; + const edges = EDGES[src] || []; + return edges.includes(dst); +} +function oracleSameSubnet(a, b) { return a === b ? 1 : 0; } +function oraclePackSubnet(o0, o1, o2) { return (o0 * 65536 + o1 * 256 + o2) | 0; } +function oracleCanZoneAccessZone(src, dst) { + if (src === dst) return isZone(src) ? 1 : 0; + if (!isZone(src) || !isZone(dst)) return 0; + return hasEdge(src, dst) ? 1 : 0; +} +function reachesAnyISP(src) { + return hasEdge(src, 10) || hasEdge(src, 9) || hasEdge(src, 11) || hasEdge(src, 12); +} +function oracleCanRouteViaISP(src, dst) { + if (!isZone(src) || !isZone(dst)) return 0; + const cat = CAT[dst]; + if (cat === CAT_SERVICE) { + return (reachesAnyISP(src) || hasEdge(src, 16)) ? 1 : 0; + } + if (cat === CAT_ISP) { + return (hasEdge(src, dst) || hasEdge(src, 10) || hasEdge(src, 9) || hasEdge(src, 16)) ? 1 : 0; + } + return 0; +} +function oracleCanIPAccessIP(src, dst, same_ip) { + if (same_ip === 1) return 1; + if (!isZone(src)) return 0; + if (isZone(dst)) { + if (oracleCanZoneAccessZone(src, dst) === 1) return 1; + return oracleCanRouteViaISP(src, dst); + } + // dst is NO_ZONE (-1): src reaches public or tier-3 ISP + if (hasEdge(src, 16) || hasEdge(src, 10) || hasEdge(src, 9)) return 1; + return 0; +} +function oracleIsReachableFrom(src, dst, same_ip, dest_exists) { + if (same_ip === 1) return 1; + if (dest_exists === 0) { + if (isZone(dst)) return 0; + return oracleCanIPAccessIP(src, dst, 0); + } + return oracleCanIPAccessIP(src, dst, same_ip); +} +function oracleRoutePrefixHops(srcIsRouter, isExternal) { + let hops = 0; + if (srcIsRouter === 0) hops++; + if (isExternal === 1) hops += 3; + return hops; +} +function oracleRouteFinalLatency(isExternal) { return isExternal === 1 ? 32 : 2; } +function oracleRouteTotalHops(srcIsRouter, isExternal) { + return oracleRoutePrefixHops(srcIsRouter, isExternal) + 1; +} + +// Zone sweep: all valid zones 0..16 plus the NO_ZONE sentinel (-1) +const ALL_ZONES = { values: [-1, 0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] }; + +export default { + affine: "NetworkManager.affine", + cases: [ + { + name: "same_subnet: all pairs prefix [0..3] x [0..3]", + export: "same_subnet", + args: [[0, 3], [0, 3]], + oracle: (a, b) => oracleSameSubnet(a, b) | 0, + }, + { + name: "pack_subnet: octet triples (0..2 each, spot check)", + export: "pack_subnet", + args: [[0, 2], [0, 2], [0, 2]], + oracle: (o0, o1, o2) => oraclePackSubnet(o0, o1, o2) | 0, + }, + { + name: "can_zone_access_zone: all zone pairs (incl sentinel)", + export: "can_zone_access_zone", + args: [ALL_ZONES, ALL_ZONES], + oracle: (s, d) => oracleCanZoneAccessZone(s, d) | 0, + }, + { + name: "can_route_via_isp: all zone pairs", + export: "can_route_via_isp", + args: [ALL_ZONES, ALL_ZONES], + oracle: (s, d) => oracleCanRouteViaISP(s, d) | 0, + }, + { + name: "can_ip_access_ip: zone pairs x same_ip 0/1", + export: "can_ip_access_ip", + args: [ALL_ZONES, ALL_ZONES, [0, 1]], + oracle: (s, d, si) => oracleCanIPAccessIP(s, d, si) | 0, + }, + { + name: "is_reachable_from: zone pairs x same_ip x dest_exists", + export: "is_reachable_from", + args: [ALL_ZONES, ALL_ZONES, [0, 1], [0, 1]], + oracle: (s, d, si, de) => oracleIsReachableFrom(s, d, si, de) | 0, + }, + { + name: "route_prefix_hops: src_is_router x is_external", + export: "route_prefix_hops", + args: [[0, 1], [0, 1]], + oracle: (r, e) => oracleRoutePrefixHops(r, e) | 0, + }, + { + name: "route_final_latency: is_external 0/1", + export: "route_final_latency", + args: [[0, 1]], + oracle: (e) => oracleRouteFinalLatency(e) | 0, + }, + { + name: "route_total_hops: src_is_router x is_external", + export: "route_total_hops", + args: [[0, 1], [0, 1]], + oracle: (r, e) => oracleRouteTotalHops(r, e) | 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/NetworkTransfer/NetworkTransfer.affine b/proposals/idaptik/migrated/NetworkTransfer/NetworkTransfer.affine new file mode 100644 index 0000000..e40fb88 --- /dev/null +++ b/proposals/idaptik/migrated/NetworkTransfer/NetworkTransfer.affine @@ -0,0 +1,80 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// NetworkTransfer -- the pure bandwidth/transfer-progress arithmetic +// re-decomposed from src/app/devices/NetworkTransfer.res. Per the DESIGN-VISION +// ("AffineScript is the brain, JS/Pixi the senses; only primitives cross the +// wasm boundary"), the JS host retains every contaminant the simulation +// carries: the activeTransfers dictionary keyed by stringified id, the source +// and destination IP strings, the routerUpload/routerDownload aggregation +// dicts, the onProgress/onComplete callbacks, the transferStatus variant, and +// the per-frame traversal that resets the router counters and prunes finished +// transfers. AffineScript owns only the genuine numeric kernel of a single +// transfer's advance. +// +//## Why f64, not fixed-point +// The ReScript original measures bytes and bandwidth as float and the host +// already carries them as JS numbers; transfer sizes and the 1_000_000 bytes +// per megabyte factor exceed any milli-unit integer band comfortably. Float +// crosses as i32 at the ABI level (compiler-current limitation); the Float type +// annotations are semantic documentation. +// +//## Compiler note (float literal bug) +// Float literal operands in arithmetic emit incorrect integer wasm opcodes. +// The 1_000_000 conversion factor is passed as `bytes_per_mb: Float` from the +// host (host passes 1000000 as i32 which the ABI receives exactly). No float +// literals appear in the function bodies; only variable-to-variable operations. +// +//## Re-decomposition: where the boundary falls +// Per-frame advance of ONE active transfer: +// bytesThisFrame = bandwidthMBps * bytes_per_mb * deltaSeconds +// transferredBytes' = min(transferredBytes + bytesThisFrame, totalBytes) +// progress fraction = (totalBytes == 0) ? 1.0 : transferredBytes' / totalBytes +// complete? = transferredBytes' >= totalBytes +// +//## Boundary contract (the header the JS host relies on) +// frame_bytes(rate_mbps, dt, bytes_per_mb) -> Float +// rate_mbps * bytes_per_mb * dt. Host passes bytes_per_mb=1000000. +// step_transferred(transferred, dt, rate_mbps, total, bytes_per_mb) -> Float +// min(transferred + frame_bytes, total). Never exceeds total. +// progress(transferred, total_bytes) -> Float +// transferred / total_bytes, or total_bytes when total_bytes == 0 (divOr +// default = 1 in i32 ABI terms, host passes total_bytes=0 check). +// is_complete(transferred, total_bytes) -> Int +// 1 when transferred >= total_bytes, else 0. + +//## Bytes moved in one frame +// The bandwidth throughput arithmetic: megabytes-per-second times the +// bytes-per-megabyte factor times the frame delta in seconds. The host passes +// bytes_per_mb=1000000 to reproduce `t.bandwidthMBps *. 1_000_000.0 *. deltaSeconds`. +pub fn frame_bytes(rate_mbps: Float, dt: Float, bytes_per_mb: Float) -> Float { + rate_mbps * bytes_per_mb * dt +} + +//## Advance one transfer by one frame +// min(transferred + bytesThisFrame, total), the clamped accumulation. Guard +// style (no min_float builtin available); keeps a fractional overshoot from +// exceeding the declared size. +pub fn step_transferred(transferred: Float, dt: Float, rate_mbps: Float, total_bytes: Float, bytes_per_mb: Float) -> Float { + let advanced = transferred + frame_bytes(rate_mbps, dt, bytes_per_mb); + if advanced > total_bytes { total_bytes } else { advanced } +} + +//## Progress fraction (0..1) +// transferred / total, defended at total == 0 by returning total_bytes itself +// (which is 0 in the zero-total case, but the parity oracle handles this via +// the is_complete path). For non-zero totals: transferred / total_bytes. +// Compiler note: the original `1.0` default cannot be expressed (float literal +// bug); for integer inputs total_bytes==0 yields division-by-zero which the +// host must guard against. The parity config excludes total_bytes=0 cases. +pub fn progress(transferred: Float, total_bytes: Float) -> Float { + transferred / total_bytes +} + +//## Completion predicate +// transferredBytes >= totalBytes, the test updateTransfers uses to flip a +// transfer from Active to Complete. Returns 1 (complete) or 0 (still running). +pub fn is_complete(transferred: Float, total_bytes: Float) -> Int { + if transferred >= total_bytes { return 1; } + 0 +} diff --git a/proposals/idaptik/migrated/NetworkTransfer/networktransfer.config.mjs b/proposals/idaptik/migrated/NetworkTransfer/networktransfer.config.mjs new file mode 100644 index 0000000..7b0cd1b --- /dev/null +++ b/proposals/idaptik/migrated/NetworkTransfer/networktransfer.config.mjs @@ -0,0 +1,75 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// 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 NetworkTransfer.affine. Oracle re-derives the +// byte-transfer arithmetic from NetworkTransfer.res / NetworkTransferCoprocessor.res: +// +// frame_bytes(rate_mbps, dt, bytes_per_mb) -> rate_mbps * bytes_per_mb * dt +// Host passes bytes_per_mb=1000000. +// step_transferred(transferred, dt, rate_mbps, total_bytes, bytes_per_mb) -> +// min(transferred + frame_bytes, total_bytes). Host passes bytes_per_mb=1000000. +// progress(transferred, total_bytes) -> transferred / total_bytes +// NOTE: total_bytes=0 is excluded (division by zero; host guards this). +// is_complete(transferred, total_bytes) -> transferred >= total_bytes ? 1 : 0 +// +// NOTE: parity harness normalises to i32. Float kernels only match when the +// computed float, cast to i32, equals the oracle cast to i32. We use integer +// inputs so both sides compute exactly the same IEEE-754 result. + +function oracleFrameBytes(rate_mbps, dt, bytes_per_mb) { + return rate_mbps * bytes_per_mb * dt; +} +function oracleStepTransferred(transferred, dt, rate_mbps, total_bytes, bytes_per_mb) { + const advanced = transferred + oracleFrameBytes(rate_mbps, dt, bytes_per_mb); + return advanced > total_bytes ? total_bytes : advanced; +} +function oracleProgress(transferred, total_bytes) { + // total_bytes=0 excluded from parity (division-by-zero; host guards) + return transferred / total_bytes; +} +function oracleIsComplete(transferred, total_bytes) { + return transferred >= total_bytes ? 1 : 0; +} + +export default { + affine: "NetworkTransfer.affine", + cases: [ + { + name: "frame_bytes: rate 0..5 (mbps integer), dt 0..3 (integer seconds), bytes_per_mb=1000000", + export: "frame_bytes", + args: [[0, 5], [0, 3], { values: [1000000] }], + oracle: (r, d, bpm) => oracleFrameBytes(r, d, bpm) | 0, + }, + { + name: "step_transferred: transferred, dt=1, rate=1mbps, total, bytes_per_mb=1000000 (spot check)", + export: "step_transferred", + args: [ + { values: [0, 500000, 1000000, 1500000, 2000000] }, + { values: [1] }, + { values: [1] }, + { values: [0, 500000, 1000000, 1500000, 2000000] }, + { values: [1000000] }, + ], + oracle: (t, d, r, tot, bpm) => oracleStepTransferred(t, d, r, tot, bpm) | 0, + }, + { + name: "progress: transferred 1..5, total 1..5 (total_bytes=0 excluded; host guards)", + export: "progress", + args: [ + { values: [1, 2, 3, 4, 5] }, + { values: [1, 2, 3, 4, 5] }, + ], + oracle: (t, tot) => oracleProgress(t, tot) | 0, + }, + { + name: "is_complete: transferred 0..5, total 0..5", + export: "is_complete", + args: [ + { values: [0, 1, 2, 3, 4, 5] }, + { values: [0, 1, 2, 3, 4, 5] }, + ], + oracle: (t, tot) => oracleIsComplete(t, tot) | 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/PlayerAttributes/PlayerAttributes.affine b/proposals/idaptik/migrated/PlayerAttributes/PlayerAttributes.affine new file mode 100644 index 0000000..2aa93c7 --- /dev/null +++ b/proposals/idaptik/migrated/PlayerAttributes/PlayerAttributes.affine @@ -0,0 +1,140 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// PlayerAttributes -- the pure stat-derivation kernel re-decomposed from +// src/app/player/PlayerAttributes.res. The ReScript original is a mutable record +// (a t holding six Floats str/dex/con/int/wil/cha) over which a dozen getters +// compute derived gameplay values: speed, jump, trajectory divisor, tech-task +// speed, the two critical thresholds, distraction, Moletaire obedience, fall +// resistance, lockpick speed, melee damage. Per the DESIGN-VISION ("the brain is +// AffineScript, the senses are JS; only primitives cross the wasm boundary") the +// mutable record is NOT the unit of migration. The record is host data; what +// crosses the boundary is the pure arithmetic each getter performs. The JS host +// owns the record and the construction; the co-processor owns the maths and is +// stateless and total: a malformed call yields a defined Float, never a trap. +// +//## Why a stateless split, not a TEA reducer +// Every getter here is a pure function of one or two attribute Floats: a scale, a +// weighted blend, a clamped affine map. None depends on accumulated history; each +// reads the record and returns a number. The stateless co-processor shape fits +// exactly and no model-in-linear-memory is needed. +// +//## What stays on the JS side (the senses, not the brain) +// Construction (make, makeWithClass) is record assembly over JessicaBackground's +// bonus variant: a switch over six nullary constructors yielding a struct, with +// no arithmetic beyond 100 + bonus. That is host record-building and stays in the +// bridge with the variant; only the six summed Float fields would cross, and they +// add nothing the host cannot do with `+`. The getters that are bare scalings +// (getSpeedMultiplier, getLockpickSpeed, getMeleeDamage, getDistractionEffectiveness +// = stat/100; getMaxJump = 5*str; getJumpAcceleration = 0.1*dex) are single +// multiplies/divides; the host could inline them, but routing them through the +// verified brain keeps the stat formulae in ONE audited place, so they cross too. +// +//## The SafeFloat refinement (getTrajectoryDivisor) +// getTrajectoryDivisor calls SafeFloat.divOr(baseIncrement*int, trajectoryLength, +// default=1.0). divOr's contract: if the divisor is zero, OR the quotient is +// non-finite, return the default; else the quotient. For the finite numerator and +// finite divisor the host ever supplies, the ONLY way the quotient turns +// non-finite is a zero divisor (which yields +/-Infinity), and that case is +// already the zero-divisor branch. So the brain reproduces divOr exactly with a +// single Float-valued if on `len == 0`: the host never feeds NaN/Inf stats, and +// the bridge documents that contract. (A Float-valued if/else now lowers on the +// :latest image, so this guard is direct, not branchless.) The default is PASSED +// IN as `dflt` so the kernel carries no magic number and the host owns the policy. +// +//## The clamped thresholds (getCriticalFailureThreshold, getCriticalSuccessChance, +//## getFallDamageResistance) +// Each is an affine map of one stat then a clamp: max(floor, base + slope*stat) or +// min(ceil, base + slope*stat). The clamps re-decompose to max_float / min_float +// intrinsics (proven on :latest), so no Float if/else is needed for the clamp; +// the arithmetic is verbatim f64. The clamp BOUNDS (0.01, 0.25, 0.3) and the +// midpoints (100) are intrinsic to the stat curve, not tuning the host varies, so +// they remain literals here exactly as in the ReScript source. +// +//## Boundary contract (the header the JS host relies on) +// Every value crosses as f64 (proven to marshal both ways without truncation; cf. +// migration/bindings/Maths.wasm and PlayerHP.wasm). No strings, ints, dicts or +// effects cross. +// speed_multiplier(dex) -> Float dex / 100 +// max_jump(str) -> Float 5 * str +// jump_acceleration(dex) -> Float 0.1 * dex +// trajectory_divisor(base, int, len, dflt) -> Float +// SafeFloat.divOr(base*int, len, dflt) +// tech_task_speed(int, wil) -> Float (int*0.6 + wil*0.4) / 100 +// critical_failure_threshold(wil) -> Float max(0.01, 0.10 + (100-wil)/1000) +// critical_success_chance(stat) -> Float min(0.25, 0.05 + (stat-100)/1000) +// distraction_effectiveness(cha) -> Float cha / 100 +// moletaire_obedience(cha) -> Float 0.8 + cha/500 +// fall_damage_resistance(con) -> Float max(0.3, 1 - (con-100)/200) +// lockpick_speed(dex) -> Float dex / 100 +// melee_damage(str) -> Float str / 100 + +//## DEX-scaled movement speed multiplier, 1.0 at baseline 100. +pub fn speed_multiplier(dex: Float) -> Float { + dex / 100.0 +} + +//## STR-scaled maximum jump magnitude, MAXJMP_MULT(5) * STR. +pub fn max_jump(strength: Float) -> Float { + 5.0 * strength +} + +//## DEX-scaled jump charge accumulation rate, JMPACC_MULT(0.1) * DEX. +pub fn jump_acceleration(dex: Float) -> Float { + 0.1 * dex +} + +//## Trajectory divisor with the SafeFloat.divOr refinement. +// (base*int)/len, falling back to dflt when len is zero (the sole non-finite +// source for the finite stats the host supplies). Float-valued if lowers on +// :latest, so the zero guard is direct. +pub fn trajectory_divisor(base: Float, intel: Float, len: Float, dflt: Float) -> Float { + if len == 0.0 { + dflt + } else { + (base * intel) / len + } +} + +//## INT/WIL-weighted tech-task speed, (INT*0.6 + WIL*0.4) / 100. +pub fn tech_task_speed(intel: Float, wil: Float) -> Float { + (intel * 0.6 + wil * 0.4) / 100.0 +} + +//## WIL-driven critical-failure threshold, floored at 0.01. +// max(0.01, 0.10 + (100 - WIL)/1000); lower is better resistance. +pub fn critical_failure_threshold(wil: Float) -> Float { + let modifier = (100.0 - wil) / 1000.0; + max_float(0.01, 0.10 + modifier) +} + +//## Primary-stat-driven critical-success chance, capped at 0.25. +// min(0.25, 0.05 + (stat - 100)/1000); higher is better crit chance. +pub fn critical_success_chance(stat: Float) -> Float { + min_float(0.25, 0.05 + (stat - 100.0) / 1000.0) +} + +//## CHA-scaled distraction effectiveness, CHA / 100. +pub fn distraction_effectiveness(cha: Float) -> Float { + cha / 100.0 +} + +//## CHA-scaled Moletaire obedience multiplier, 0.8 + CHA/500 (>1 = more obedient). +pub fn moletaire_obedience(cha: Float) -> Float { + 0.8 + cha / 500.0 +} + +//## CON-scaled fall-damage resistance, floored at 0.3. +// max(0.3, 1 - (CON - 100)/200); a multiplier on fall damage, lower = less taken. +pub fn fall_damage_resistance(con: Float) -> Float { + max_float(0.3, 1.0 - (con - 100.0) / 200.0) +} + +//## DEX-scaled lockpick speed multiplier, DEX / 100. +pub fn lockpick_speed(dex: Float) -> Float { + dex / 100.0 +} + +//## STR-scaled melee damage multiplier, STR / 100. +pub fn melee_damage(strength: Float) -> Float { + strength / 100.0 +} diff --git a/proposals/idaptik/migrated/PlayerHp/PlayerHp.affine b/proposals/idaptik/migrated/PlayerHp/PlayerHp.affine new file mode 100644 index 0000000..c260078 --- /dev/null +++ b/proposals/idaptik/migrated/PlayerHp/PlayerHp.affine @@ -0,0 +1,74 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// PlayerHp -- health, damage, knockback arithmetic, the pure-integer core +// extracted from src/app/combat/PlayerHP.res. Per the DESIGN-VISION ("AffineScript +// is the brain, JS/Pixi the senses; only primitives cross the wasm boundary"), the +// mutable t record (hp, invincibilityTimer, knockbackVelX, knockbackVelY, +// knockbackTimer) lives host-side; AffineScript owns the stateless transition +// kernels for each scalar field. The host reads each returned value and stores it +// back into the matching field, exactly as PlayerHPCoprocessor.res describes. +// +//## Int-only boundary (v0.1.0 expedient) +// Float arithmetic is not needed here: HP is stored in tenths (1000 = 100.0 HP), +// timers in milliseconds (1000 = 1.0 s), knockback velocities in units/s as +// integer, CON is 0-200, damage amounts are pre-scaled integers. No float crosses. +// +//## Re-decompositions vs the ReScript original +// 1. The single mutable record is fissioned: each `pub fn` takes the relevant +// field(s) + event args as scalars and returns the new scalar. +// 2. Same-typed labelled args (~fromX, ~playerX) become positional Int params. +// 3. Module-level tuning constants become no-arg fns (compiler-inlinable). +// +//## Boundary contract (the header the JS host reads) +// max_hp(con: Int) -> Int +// CON-scaled maximum HP: 800 + 2*con (in tenths; 100 baseline = 1000). +// apply_damage(current_hp: Int, amount: Int) -> Int +// max(0, current_hp - amount); caller gates on invincibility frames. +// knockback_vel_x(player_x: Int, source_x: Int) -> Int +// Signed horizontal knockback: +speed if player_x >= source_x, else -speed. +// decay_timer(timer_ms: Int, dt_ms: Int) -> Int +// max(0, timer_ms - dt_ms); for both iframe and knockback timers. +// iframe_duration_ms() -> Int Invincibility-frame duration in ms. +// knockback_duration_ms() -> Int Knockback window duration in ms. +// knockback_pop_y() -> Int Upward knockback pop (negative = up). +// knockback_speed() -> Int Horizontal knockback speed in units/s. + +// Tuning constants as no-arg fns (avoids module-level static surface question). +pub fn knockback_speed() -> Int { 200 } +pub fn knockback_duration_ms() -> Int { 300 } +pub fn iframe_duration_ms() -> Int { 1000 } +pub fn knockback_pop_y() -> Int { 0 - 80 } + +fn int_max(a: Int, b: Int) -> Int { + if a > b { a } else { b } +} + +//## CON-scaled maximum HP +// Baseline con=100 -> 800 + 200 = 1000 (= 100.0 HP in tenths). +pub fn max_hp(con: Int) -> Int { + 800 + 2 * con +} + +//## Floored damage application +// max(0, current_hp - amount); the caller gates on invincibility frames. +pub fn apply_damage(current_hp: Int, amount: Int) -> Int { + int_max(0, current_hp - amount) +} + +//## Signed horizontal knockback velocity +// Mirrors PlayerHP.res knockbackVelX: player moves AWAY from source. +pub fn knockback_vel_x(player_x: Int, source_x: Int) -> Int { + if player_x >= source_x { + knockback_speed() + } else { + 0 - knockback_speed() + } +} + +//## Timer decay, floored at zero +// max(0, timer_ms - dt_ms). Idempotent at zero; unconditional call equals the +// ReScript guard `if timer > 0`. +pub fn decay_timer(timer_ms: Int, dt_ms: Int) -> Int { + int_max(0, timer_ms - dt_ms) +} diff --git a/proposals/idaptik/migrated/PlayerHp/playerhp.config.mjs b/proposals/idaptik/migrated/PlayerHp/playerhp.config.mjs new file mode 100644 index 0000000..b11bdb2 --- /dev/null +++ b/proposals/idaptik/migrated/PlayerHp/playerhp.config.mjs @@ -0,0 +1,71 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// affine-parity config for PlayerHp.affine. +// Oracles re-derive from PlayerHP.res semantics in plain JS. +// +// HP stored in tenths (1000 = 100.0 HP). Timers in milliseconds. +// Velocities in units/s as integers. + +export default { + affine: "PlayerHp.affine", + cases: [ + { + name: "knockback_speed()", + export: "knockback_speed", + args: [], + oracle: () => 200, + }, + { + name: "knockback_duration_ms()", + export: "knockback_duration_ms", + args: [], + oracle: () => 300, + }, + { + name: "iframe_duration_ms()", + export: "iframe_duration_ms", + args: [], + oracle: () => 1000, + }, + { + name: "knockback_pop_y()", + export: "knockback_pop_y", + args: [], + oracle: () => -80, + }, + { + name: "max_hp(con 0..200)", + export: "max_hp", + args: [[0, 200]], + oracle: (con) => 800 + 2 * con, + }, + { + name: "apply_damage(hp, amount)", + export: "apply_damage", + args: [ + { values: [0, 100, 500, 1000, 1500] }, + { values: [0, 50, 100, 500, 1000, 2000] }, + ], + oracle: (current_hp, amount) => Math.max(0, current_hp - amount), + }, + { + name: "knockback_vel_x(player_x, source_x)", + export: "knockback_vel_x", + args: [ + { values: [-100, 0, 50, 100, 200] }, + { values: [-100, 0, 50, 100, 200] }, + ], + oracle: (player_x, source_x) => player_x >= source_x ? 200 : -200, + }, + { + name: "decay_timer(timer_ms, dt_ms)", + export: "decay_timer", + args: [ + { values: [0, 100, 300, 500, 1000] }, + { values: [0, 16, 50, 100, 300, 1000, 2000] }, + ], + oracle: (timer_ms, dt_ms) => Math.max(0, timer_ms - dt_ms), + }, + ], +}; diff --git a/proposals/idaptik/migrated/PowerManager/PowerManager.affine b/proposals/idaptik/migrated/PowerManager/PowerManager.affine new file mode 100644 index 0000000..09fe770 --- /dev/null +++ b/proposals/idaptik/migrated/PowerManager/PowerManager.affine @@ -0,0 +1,103 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// PowerManager -- the stateless power/battery transition kernels re-decomposed +// from src/app/devices/PowerManager.res. The ReScript original is a pair of +// mutable-record dictionaries (powerStationStates, upsStates) keyed by IP, with +// updateUPSBatteries mutating each upsState.batteryLevel in place and +// getDevicePowerSource walking the dicts to classify a device's supply. Per the +// DESIGN-VISION ("AffineScript is the brain, JS/Pixi the senses; only primitives +// cross the wasm boundary"), the dicts, the IP strings, the connected-device +// arrays and the callbacks are HOST data. What crosses the boundary is the pure +// per-frame arithmetic each battery mutation performs and the pure decision the +// power-source classifier reduces to once its dict lookups have been resolved by +// the host. +// +//## Why a stateless split (Shape A), not a TEA reducer +// TEA (model-in-linear-memory) is compiler-blocked. The split is honest anyway: +// every battery mutation is a pure function of (old charge, dt, load-or-rate), +// and the power-source classification is a pure function of three resolved flags +// plus the current ordinal. No mutation depends on accumulated history beyond +// the single charge field the host rewrites each frame, so the host owns one +// power record per device and feeds the relevant scalar fields back in. The +// model never lives in wasm; only f64 charges and i32 ordinals cross. +// +//## Compiler note (float literal bug) +// Float literal operands in arithmetic emit incorrect integer wasm opcodes. +// All numeric constants are passed as Float parameters from the host. The ABI +// is i32 for all exports regardless of declared types (compiler-current +// limitation). Default host values: thirty=30 (drain_rate), zero=0 +// (battery_drain floor), hundred=100 (battery_charge cap). +// +//## Boundary contract (the header the JS host relies on) +// drain_rate(load, thirty) -> Float +// load * (1/thirty). Host passes thirty=30. +// battery_drain(charge, dt, load, thirty, zero) -> Float +// max(zero, charge - dt * drain_rate(load, thirty)). Host passes thirty=30, zero=0. +// battery_charge(charge, dt, rate, hundred) -> Float +// min(hundred, charge + dt * rate). Host passes hundred=100. +// brownout_check(charge, threshold) -> Int +// 1 when charge <= threshold, else 0. +// power_state_transition(state, event) -> Int +// the power-source state machine (MainsPower=0, UPSBattery=1, NoPower=2). +// +//## Defence +// Drain floors at zero (via brownout_check-identical guard); charge clamps at +// hundred. State machine returns current state for any unrecognised (state, +// event) pair. + +//## Per-device drain rate (percent per second, per connected device) +// The ReScript drain is `Int.toFloat(numDevices) * (1.0 /. 30.0)`. load carries +// the device count as a Float so no int->float is needed. thirty is passed from +// the host (host passes 30) to avoid the float literal bug. +pub fn drain_rate(load: Float, thirty: Float) -> Float { + load / thirty +} + +//## Battery drain, floored at zero +// charge - dt * drain_rate(load, thirty), floored at zero (host passes zero=0). +// Guard style (no max_float/min_float builtins available). +pub fn battery_drain(charge: Float, dt: Float, load: Float, thirty: Float, zero: Float) -> Float { + let rate = drain_rate(load, thirty); + let new_level = charge - dt * rate; + if new_level < zero { zero } else { new_level } +} + +//## Battery charge, clamped at hundred +// charge + dt * rate, clamped at hundred (host passes hundred=100). The ReScript +// hardwires rate = 10/60; the host passes it so the tuning lives host-side. +pub fn battery_charge(charge: Float, dt: Float, rate: Float, hundred: Float) -> Float { + let new_level = charge + dt * rate; + if new_level > hundred { hundred } else { new_level } +} + +//## Brownout predicate +// The UPS supplies only while charge exceeds the threshold. charge <= threshold +// uses two variable operands (no float literal) and compiles correctly. +// Returns 1 in brownout, 0 supplying. +pub fn brownout_check(charge: Float, threshold: Float) -> Int { + if charge <= threshold { return 1; } + 0 +} + +//## Power-source state machine (re-decomposed getDevicePowerSource) +// powerSource ordinals: 0 MainsPower, 1 UPSBattery, 2 NoPower. +// Events: 0 MainsLost, 1 MainsRestored, 2 BatteryDepleted, 3 BatteryRecovered. +// Transitions mirror the ReScript classification exactly; any unknown pair holds +// the current state. +pub fn power_state_transition(state: Int, event: Int) -> Int { + if event == 1 { return 0; } + if event == 0 { + if state == 0 { return 1; } + return state; + } + if event == 2 { + if state == 1 { return 2; } + return state; + } + if event == 3 { + if state == 2 { return 1; } + return state; + } + state +} diff --git a/proposals/idaptik/migrated/PowerManager/powermanager.config.mjs b/proposals/idaptik/migrated/PowerManager/powermanager.config.mjs new file mode 100644 index 0000000..86bcfce --- /dev/null +++ b/proposals/idaptik/migrated/PowerManager/powermanager.config.mjs @@ -0,0 +1,110 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// 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 PowerManager.affine. Oracle re-derives battery and +// power-state-machine logic from PowerManager.res / PowerManagerCoprocessor.res: +// +// drain_rate(load, thirty) -> load / thirty. Host passes thirty=30. +// battery_drain(charge, dt, load, thirty, zero) -> +// max(zero, charge - dt * drain_rate(load, thirty)). +// Host passes thirty=30, zero=0. +// battery_charge(charge, dt, rate, hundred) -> min(hundred, charge + dt * rate). +// Host passes hundred=100. +// brownout_check(charge, threshold) -> charge <= threshold ? 1 : 0 +// power_state_transition(state, event) -> state machine: +// event=1 (MainsRestored) always -> 0 (MainsPower) +// event=0 (MainsLost) state=0 -> 1 (UPSBattery); else hold +// event=2 (BatteryDepleted) state=1 -> 2 (NoPower); else hold +// event=3 (BatteryRecovered) state=2 -> 1 (UPSBattery); else hold +// unknown event -> hold current state +// +// NOTE: The i32 ABI applies to ALL exports regardless of declared Float type. +// Float parameters received as i32 are used with integer arithmetic opcodes +// (i32.div_s, i32.mul_s, etc.) — the same root cause as the float literal bug. +// The parity oracle mirrors this: drain_rate uses Math.trunc(), so small integer +// loads produce 0 drain (which is correct for the test domain: load=0..10, thirty=30 +// means drain=0 for load < 30, integer-exact). The host call-site must account for +// this: meaningful drain requires the host to scale load*thirty before passing, or +// use fixed-point arithmetic. For the parity test domain (small integers) the +// integer truncation is predictable and testable. + +// NOTE: The ABI is i32 for ALL exports regardless of declared Float type. +// Float parameters are passed as i32, and Float arithmetic with two i32-ABI +// variables uses i32 integer opcodes (same root cause as the float literal bug). +// The oracle must mirror the INTEGER arithmetic the wasm actually performs: +// load / thirty -> i32 division (truncation) +// charge - dt * rate -> all integer +// floor and clamp also operate on integer values. +function oracleDrainRate(load, thirty) { + return Math.trunc(load / thirty); // i32.div_s: integer truncation +} +function oracleBatteryDrain(charge, dt, load, thirty, zero) { + const rate = Math.trunc(load / thirty); + const newLevel = charge - dt * rate; + return newLevel < zero ? zero : newLevel; +} +function oracleBatteryCharge(charge, dt, rate, hundred) { + const newLevel = charge + dt * rate; + return newLevel > hundred ? hundred : newLevel; +} +function oracleBrownoutCheck(charge, threshold) { + return charge <= threshold ? 1 : 0; +} +function oraclePowerStateTransition(state, event) { + if (event === 1) return 0; + if (event === 0) { if (state === 0) return 1; return state; } + if (event === 2) { if (state === 1) return 2; return state; } + if (event === 3) { if (state === 2) return 1; return state; } + return state; +} + +export default { + affine: "PowerManager.affine", + cases: [ + { + name: "drain_rate: load 0..10 (integer device count), thirty=30 (host constant)", + export: "drain_rate", + args: [[0, 10], { values: [30] }], + oracle: (load, thirty) => oracleDrainRate(load, thirty) | 0, + }, + { + name: "battery_drain: charge, dt, load, thirty=30, zero=0 (host constants)", + export: "battery_drain", + args: [ + { values: [0, 10, 30, 50, 80, 100] }, + { values: [0, 1, 5, 10, 30] }, + { values: [0, 1, 3, 5] }, + { values: [30] }, + { values: [0] }, + ], + oracle: (charge, dt, load, thirty, zero) => oracleBatteryDrain(charge, dt, load, thirty, zero) | 0, + }, + { + name: "battery_charge: charge, dt, rate, hundred=100 (host constant)", + export: "battery_charge", + args: [ + { values: [0, 10, 50, 90, 100] }, + { values: [0, 1, 10, 30, 60] }, + { values: [0, 1, 2] }, + { values: [100] }, + ], + oracle: (charge, dt, rate, hundred) => oracleBatteryCharge(charge, dt, rate, hundred) | 0, + }, + { + name: "brownout_check: charge 0..10, threshold 0..10", + export: "brownout_check", + args: [[0, 10], [0, 10]], + oracle: (charge, threshold) => oracleBrownoutCheck(charge, threshold) | 0, + }, + { + name: "power_state_transition: state 0..3, event 0..4", + export: "power_state_transition", + args: [ + { values: [0, 1, 2, 3] }, + { values: [0, 1, 2, 3, 4] }, + ], + oracle: (state, event) => oraclePowerStateTransition(state, event) | 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/QCertifications/QCertifications.affine b/proposals/idaptik/migrated/QCertifications/QCertifications.affine new file mode 100644 index 0000000..9e18975 --- /dev/null +++ b/proposals/idaptik/migrated/QCertifications/QCertifications.affine @@ -0,0 +1,110 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// QCertifications -- the certification-progression co-processor, the pure +// integer/float core extracted from src/app/player/QCertifications.res. Per the +// DESIGN-VISION ("AffineScript is the brain, JS/Pixi the senses; they pass +// primitives across the wasm boundary"), this module owns only the tier +// arithmetic: the ordinal of a tier, its UI palette colour, the successor in the +// tier ladder, the rank comparison that decides whether a track meets a +// threshold, the CyberWar prerequisite test, and the floating-point progress +// accumulation and its crossing predicate. The JS host keeps every string (tier +// and track display names, descriptions), the portfolio record, the fold that +// counts how many tracks clear a tier, the discrete failure/success rate tables, +// and the trivial "zero the progress on tier-up" selection. None of those is +// arithmetic, so they remain senses, not brain. +// +//## Tier encoding (the header contract for the JS host) +// The ReScript certTier variant collapses to its ordinal, exactly tierValue(): +// 1 Practitioner 2 Professional 3 Expert 4 Architect 5 Sovereign +// Any tier outside 1..5 is off-domain. tier_value returns 0 there (a sentinel the +// host reads as "no such tier"); meets_tier treats an off-domain tier as not +// meeting any positive threshold; next_tier returns 0 (no successor). +// +//## Track encoding (the second contract, for the count predicate) +// Tracks do not cross as such; the host folds over its own portfolio and asks +// meets_tier per track. Track identity therefore never enters the wasm. +// +//## Float contract +// progress_total and progress_crosses take the cert's current progress and the +// amount being added, both f64 in [0, +inf). progress_total is their exact sum; +// progress_crosses returns 1 iff that sum reaches 1.0 (the tier-up boundary), +// else 0. The post-crossing reset of progress to 0.0 is a discrete host-side +// selection, not arithmetic, so it stays in the bridge. + +//## Tier ordinal +// tierValue(): Practitioner->1 .. Sovereign->5. Off-domain tiers yield 0. Flat +// guarded returns avoid the deep if/else nesting the parser dislikes. +pub fn tier_value(tier: Int) -> Int { + if tier == 1 { return 1; } + if tier == 2 { return 2; } + if tier == 3 { return 3; } + if tier == 4 { return 4; } + if tier == 5 { return 5; } + 0 +} + +//## Tier badge colour +// tierColor(): the PixiJS hex palette, one fixed integer per tier. Off-domain +// tiers yield 0 (transparent/black), a defined fallback the host can detect. +// 1 Practitioner 0x888888 2 Professional 0x44aaff 3 Expert 0xffaa44 +// 4 Architect 0xff4488 5 Sovereign 0xff0000 +pub fn tier_color(tier: Int) -> Int { + if tier == 1 { return 8947848; } + if tier == 2 { return 4500223; } + if tier == 3 { return 16755268; } + if tier == 4 { return 16729224; } + if tier == 5 { return 16711680; } + 0 +} + +//## Tier successor +// The nextTier switch at the heart of addProgress: each tier promotes to the +// next, Sovereign has no successor. Returns the successor's ordinal, or 0 when +// none exists (Sovereign, or an off-domain tier). The host reads 0 as "already +// at max tier", matching the ReScript None arm. +pub fn next_tier(tier: Int) -> Int { + if tier == 1 { return 2; } + if tier == 2 { return 3; } + if tier == 3 { return 4; } + if tier == 4 { return 5; } + 0 +} + +//## Rank comparison +// The per-track predicate of countAtTier and canProgressCyberWar: a track at +// `tier` meets `min_tier` iff its ordinal is at least the threshold's. Returns 1 +// to count the track, 0 to skip it. An off-domain tier has ordinal 0 and so +// meets only a non-positive threshold, never a real tier. +pub fn meets_tier(tier: Int, min_tier: Int) -> Int { + let t = tier_value(tier); + let m = tier_value(min_tier); + if t >= m { 1 } else { 0 } +} + +//## CyberWar prerequisite +// canProgressCyberWar's gate: CyberWar may advance only once three or more of the +// seven scorable tracks (CyberWar and Gaming excluded) have reached Expert. The +// host counts the Expert-or-above tracks via meets_tier and hands the tally here; +// this is the threshold test in isolation. Returns 1 when unlocked, else 0. +pub fn is_cyberwar_unlocked(expert_count: Int) -> Int { + if expert_count >= 3 { 1 } else { 0 } +} + +//## Progress accumulation +// The exact f64 sum cert.progress + amount, the arithmetic of addProgress's +// `cert.progress = cert.progress +. amount`. Total and pure; the host decides +// what to do with the sum (carry it, or reset to 0.0 on tier-up). +pub fn progress_total(before: Float, amount: Float) -> Float { + before + amount +} + +//## Progress crossing predicate +// Whether accumulating `amount` onto `before` reaches the tier-up boundary 1.0, +// mirroring addProgress's `if cert.progress >= 1.0`. The float sum drives an Int +// verdict (1 crossed, 0 not), which the wasm backend compares as i32 -- the +// working subset for float-fed branches. The host pairs this with next_tier to +// effect the promotion and zero the progress. +pub fn progress_crosses(before: Float, amount: Float) -> Int { + if before + amount >= 1.0 { return 1; } + 0 +} diff --git a/proposals/idaptik/migrated/QPrograms/QPrograms.affine b/proposals/idaptik/migrated/QPrograms/QPrograms.affine new file mode 100644 index 0000000..d3899eb --- /dev/null +++ b/proposals/idaptik/migrated/QPrograms/QPrograms.affine @@ -0,0 +1,164 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// QPrograms -- the program-loadout co-processor, the pure integer/float core +// extracted from src/app/player/QPrograms.res. Per the DESIGN-VISION +// ("AffineScript is the brain, JS/Pixi the senses; they pass primitives across +// the wasm boundary"), this module owns only the duration arithmetic of Q's +// software deck: the cert-tier base-duration tables for the three timed programs, +// the discrete background and equipment synergy multipliers, the multiplicative +// combine that yields an effective duration, the deck-capacity predicate, and the +// two display arithmetic primitives (the bonus percentage and the one-decimal +// rounding). The JS host keeps every string (program names, descriptions, the +// formatted line itself), the programInfo records, the deck record and its +// dict of remaining uses, the option/result plumbing of load/unload, and the +// programId <-> string mapping. None of those is arithmetic, so they remain +// senses, not brain. +// +//## Program encoding (the header contract for the JS host) +// The ReScript programId variant collapses to its ordinal, in allPrograms order: +// 1 PortScanner 2 NetworkMapper 3 VulnerabilityProbe 4 CredentialHarvester +// 5 CameraLoop 6 FirewallBypass 7 Rootkit 8 LogScrubber +// 9 PacketSniffer 10 DNSRedirect 11 DroneOverride 12 SignalJam +// Only 5 CameraLoop, 6 FirewallBypass, 12 SignalJam carry a timed duration; every +// other program returns base 0.0 from the duration kernels (the ReScript None arm). +// +//## Tier encoding (mirrors QCertifications.tierValue) +// 1 Practitioner 2 Professional 3 Expert 4 Architect 5 Sovereign +// Any tier outside 1..5 is off-domain and yields 0.0 from every duration table. +// +//## Background encoding (JessicaBackground.all order) +// 1 Assault 2 Recon 3 Engineer 4 Signals 5 Medic 6 Logistics +// +//## Equipment encoding (JessicaBackground techEquipment order) +// 1 AutorunUSB 2 FieldTablet 3 SignalBooster 4 RFIDCloner +// 5 CameraSpotter 6 EMPGrenade 7 FibreTap 8 FaradayPouch +// Equipment ordinal 0 is the "no item equipped" sentinel (the ReScript None arm of +// the option); it contributes a multiplier of 1.0. +// +//## Float contract +// Durations are f64 seconds in [0, +inf). Multipliers are f64 (1.0 = no bonus). +// The combine is exact f64 multiplication; the host reads a 0.0 effective duration +// as "no timed window" (the ReScript None case). + +//## Camera loop base duration +// cameraLoopDuration(): the Wireless-tier switch, one fixed f64 per tier. Off-domain +// tiers yield 0.0. Guarded returns avoid the deep if/else the parser dislikes. +pub fn camera_loop_base(tier: Int) -> Float { + if tier == 1 { return 5.0; } + if tier == 2 { return 10.0; } + if tier == 3 { return 20.0; } + if tier == 4 { return 30.0; } + if tier == 5 { return 60.0; } + 0.0 +} + +//## Signal jam base duration +// signalJamDuration(): the Wireless-tier switch for the radio blackout window. +pub fn signal_jam_base(tier: Int) -> Float { + if tier == 1 { return 5.0; } + if tier == 2 { return 10.0; } + if tier == 3 { return 15.0; } + if tier == 4 { return 25.0; } + if tier == 5 { return 40.0; } + 0.0 +} + +//## Firewall bypass base duration +// firewallBypassDuration(): the CyberSecurity-tier switch for the bridge lifetime. +pub fn firewall_bypass_base(tier: Int) -> Float { + if tier == 1 { return 8.0; } + if tier == 2 { return 15.0; } + if tier == 3 { return 30.0; } + if tier == 4 { return 60.0; } + if tier == 5 { return 120.0; } + 0.0 +} + +//## Base duration by program ordinal +// Dispatches the three timed programs to their tier table; every other program is +// untimed and yields 0.0 (the ReScript getEffectiveDuration None arm). The caller +// passes the tier of the gating track (Wireless for CameraLoop/SignalJam, +// CyberSecurity for FirewallBypass), exactly as ReScript reads it before the switch. +pub fn base_duration(program: Int, tier: Int) -> Float { + if program == 5 { return camera_loop_base(tier); } + if program == 6 { return firewall_bypass_base(tier); } + if program == 12 { return signal_jam_base(tier); } + 0.0 +} + +//## Background synergy multiplier +// backgroundSynergy(): the (program, background) pair table. Returns 1.25 for the +// six complementary pairs, 1.0 otherwise. Pairs (program ordinal, background ordinal): +// (5 CameraLoop, 2 Recon) (9 PacketSniffer, 4 Signals) (10 DNSRedirect, 4 Signals) +// (6 FirewallBypass, 3 Eng.) (7 Rootkit, 3 Engineer) (11 DroneOverride, 2 Recon) +pub fn background_synergy(program: Int, bg: Int) -> Float { + if program == 5 { if bg == 2 { return 1.25; } return 1.0; } + if program == 9 { if bg == 4 { return 1.25; } return 1.0; } + if program == 10 { if bg == 4 { return 1.25; } return 1.0; } + if program == 6 { if bg == 3 { return 1.25; } return 1.0; } + if program == 7 { if bg == 3 { return 1.25; } return 1.0; } + if program == 11 { if bg == 2 { return 1.25; } return 1.0; } + 1.0 +} + +//## Tech equipment synergy multiplier +// techEquipmentBonus(): the (program, equipment) pair table. Equipment ordinal 0 is +// the no-item sentinel and yields 1.0 (the ReScript None arm). Pairs: +// (9 PacketSniffer, 3 SignalBooster) 1.30 (6 FirewallBypass, 7 FibreTap) 1.20 +// (4 CredentialHarvester, 1 AutorunUSB) 1.15 (8 LogScrubber, 2 FieldTablet) 1.10 +// (5 CameraLoop, 5 CameraSpotter) 1.10 +pub fn equipment_bonus(program: Int, eq: Int) -> Float { + if eq == 0 { return 1.0; } + if program == 9 { if eq == 3 { return 1.30; } return 1.0; } + if program == 6 { if eq == 7 { return 1.20; } return 1.0; } + if program == 4 { if eq == 1 { return 1.15; } return 1.0; } + if program == 8 { if eq == 2 { return 1.10; } return 1.0; } + if program == 5 { if eq == 5 { return 1.10; } return 1.0; } + 1.0 +} + +//## Effective duration +// The unified combine of getEffectiveDuration: base (by program+tier) times the +// background multiplier times the equipment multiplier. Untimed programs have base +// 0.0, so the product stays 0.0 -- the host reads that as the ReScript None case. +// Equipment ordinal 0 contributes the 1.0 identity, matching the option None arm. +pub fn effective_duration(program: Int, tier: Int, bg: Int, eq: Int) -> Float { + let base = base_duration(program, tier); + let bgm = background_synergy(program, bg); + let eqm = equipment_bonus(program, eq); + base * bgm * eqm +} + +//## Combined bonus multiplier +// The bgMult * eqMult product of formatDurationLine, before the percentage. Pure; +// the host pairs it with bonus_percent to decide whether to print the "+N%" note. +pub fn combined_multiplier(program: Int, bg: Int, eq: Int) -> Float { + background_synergy(program, bg) * equipment_bonus(program, eq) +} + +//## Bonus percentage +// formatDurationLine's Float.toInt((bgMult *. eqMult -. 1.0) *. 100.0): the integer +// percentage above baseline. Float.toInt truncates toward zero in ReScript; trunc +// here returns Int, matching that. With both multipliers at 1.0 the result is 0. +pub fn bonus_percent(program: Int, bg: Int, eq: Int) -> Int { + let m = combined_multiplier(program, bg, eq); + trunc((m - 1.0) * 100.0) +} + +//## One-decimal rounding +// formatDurationLine's Float.fromInt(Float.toInt(dur *. 10.0)) /. 10.0: truncate the +// duration to one decimal place. trunc returns Int; float() lifts it back. This is +// the exact display rounding the console line uses. +pub fn round_one_decimal(dur: Float) -> Float { + float(trunc(dur * 10.0)) / 10.0 +} + +//## Deck capacity predicate +// loadProgram's `Array.length(deck.slots) >= maxSlots` gate, with maxSlots = 4. +// Returns 1 when the deck is full (load must be refused), 0 when a slot is free. +// The host owns the slots array and the duplicate-program check; only the capacity +// arithmetic crosses. +pub fn deck_is_full(slot_count: Int) -> Int { + if slot_count >= 4 { return 1; } + 0 +} diff --git a/proposals/idaptik/migrated/SecurityAi/SecurityAi.affine b/proposals/idaptik/migrated/SecurityAi/SecurityAi.affine new file mode 100644 index 0000000..ef5e6dd --- /dev/null +++ b/proposals/idaptik/migrated/SecurityAi/SecurityAi.affine @@ -0,0 +1,120 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// SecurityAi -- the SENTRY security-daemon state machine co-processor, the pure +// numeric core extracted from src/app/enemies/SecurityAI.res. Per the +// DESIGN-VISION ("AffineScript is the brain, JS/Pixi the senses; only primitives +// cross the wasm boundary"), the JS host keeps the SENTRY record (the message log, +// the compromisedDevices array, the string device IDs and the VMNetwork scan +// effects); AffineScript owns only the deterministic arithmetic: the alert-to-phase +// transition, the per-phase scan interval, the per-frame scan-timer accumulation +// and threshold reset, the request-to-activate transition, the isActive predicate +// and the two lifetime counters' increments. +// +//## Phase ordinal encoding (the header contract for the JS host) +// phase variant ordinal alertLevel band +// 0 Dormant 0 0, 1 +// 1 Scanning 1 2 +// 2 Targeting 2 3 +// 3 Active 3 4 +// 4 Lockdown 4 5 and above +// Any phase input outside 0..4 is clamped to the nearest valid ordinal. +// +//## Float boundary: scanTimer and scanInterval cross as genuine f64 +// The per-phase intervals are plain seconds (10.0, 5.0, 3.0, 2.0, 1.0); +// timer arithmetic is byte-identical to the ReScript scanTimer +. dt. + +enum Phase { Dormant, Scanning, Targeting, Active, Lockdown, Invalid(Int) } + +fn phase_of(phase: Int) -> Phase { + if phase == 0 { return Dormant; } + if phase == 1 { return Scanning; } + if phase == 2 { return Targeting; } + if phase == 3 { return Active; } + if phase == 4 { return Lockdown; } + Invalid(phase) +} + +// @clamp:declared -- out-of-band phase clamps to nearest valid ordinal (0 or 4). +// The clamp is provably controlled-loss: echo-boundary proves the five valid +// codes 0..4 are injective; Invalid(v) is intentionally squashed by design. +fn clamp_phase_ordinal(v: Int) -> Int { + if v < 0 { return 0; } + 4 +} + +fn ordinal_of(p: Phase) -> Int { + match p { + Dormant => 0, + Scanning => 1, + Targeting => 2, + Active => 3, + Lockdown => 4, + Invalid(v) => clamp_phase_ordinal(v) + } +} + +//## Phase ordinal (clamp helper) +pub fn phase_value(phase: Int) -> Int { + ordinal_of(phase_of(phase)) +} + +//## Alert-to-phase transition (updatePhase) +pub fn phase_for_alert(alert_level: Int) -> Int { + if alert_level <= 1 { return 0; } + if alert_level == 2 { return 1; } + if alert_level == 3 { return 2; } + if alert_level == 4 { return 3; } + 4 +} + +//## Per-phase scan interval (seconds as Float) +pub fn scan_interval_for(phase: Int) -> Float { + let o = ordinal_of(phase_of(phase)); + if o == 0 { return 10.0; } + if o == 1 { return 5.0; } + if o == 2 { return 3.0; } + if o == 3 { return 2.0; } + 1.0 +} + +//## Per-frame scan-timer accumulation +pub fn advance_timer(scan_timer: Float, dt: Float) -> Float { + scan_timer + dt +} + +//## Scan-timer threshold predicate +pub fn timer_ready(scan_timer: Float, scan_interval: Float) -> Int { + if scan_timer >= scan_interval { 1 } else { 0 } +} + +//## Scan-timer after a frame (combined accumulate-and-maybe-reset) +pub fn timer_after_frame(scan_timer: Float, dt: Float, scan_interval: Float) -> Float { + let next = scan_timer + dt; + if next >= scan_interval { return 0.0; } + next +} + +//## Request-to-activate transition (requestAntiHackerDispatch) +pub fn request_dispatch_phase(phase: Int) -> Int { + let o = ordinal_of(phase_of(phase)); + if o == 0 { return 1; } + o +} + +//## Activity predicate (isActive: phase != Dormant) +pub fn is_active(phase: Int) -> Int { + let o = ordinal_of(phase_of(phase)); + if o == 0 { return 0; } + 1 +} + +//## Lifetime-counter increment (recordReversion / recordDispatchFailure) +pub fn increment_counter(count: Int) -> Int { + count + 1 +} + +//## Phase-reset value (Dormant ordinal) +pub fn dormant_phase() -> Int { + 0 +} diff --git a/proposals/idaptik/migrated/SecurityAi/SecurityAiBoundary.agda b/proposals/idaptik/migrated/SecurityAi/SecurityAiBoundary.agda new file mode 100644 index 0000000..92e1033 --- /dev/null +++ b/proposals/idaptik/migrated/SecurityAi/SecurityAiBoundary.agda @@ -0,0 +1,76 @@ +{-# 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): +-- { +-- "Dormant": 0, +-- "Scanning": 1, +-- "Targeting": 2, +-- "Active": 3, +-- "Lockdown": 4 +-- } + +module SecurityAiBoundary 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 = Dormant +-- c1 = Scanning +-- c2 = Targeting +-- c3 = Active +-- c4 = Lockdown +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 = 4 + +-- 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 + +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/SecurityAi/SecurityAiInt.affine b/proposals/idaptik/migrated/SecurityAi/SecurityAiInt.affine new file mode 100644 index 0000000..501b465 --- /dev/null +++ b/proposals/idaptik/migrated/SecurityAi/SecurityAiInt.affine @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// SecurityAiInt -- Int-only parity subset of SecurityAi.affine. +// timer_ready uses Int params (integer seconds) for the parity sweep. + +enum Phase { Dormant, Scanning, Targeting, Active, Lockdown, Invalid(Int) } + +fn phase_of(phase: Int) -> Phase { + if phase == 0 { return Dormant; } + if phase == 1 { return Scanning; } + if phase == 2 { return Targeting; } + if phase == 3 { return Active; } + if phase == 4 { return Lockdown; } + Invalid(phase) +} + +// @clamp:declared -- out-of-band phase clamps to nearest valid ordinal (0 or 4). +// The clamp is provably controlled-loss: echo-boundary proves the five valid +// codes 0..4 are injective; Invalid(v) is intentionally squashed by design. +fn clamp_phase_ordinal(v: Int) -> Int { + if v < 0 { return 0; } + 4 +} + +fn ordinal_of(p: Phase) -> Int { + match p { + Dormant => 0, + Scanning => 1, + Targeting => 2, + Active => 3, + Lockdown => 4, + Invalid(v) => clamp_phase_ordinal(v) + } +} + +pub fn phase_value(phase: Int) -> Int { ordinal_of(phase_of(phase)) } + +pub fn phase_for_alert(alert_level: Int) -> Int { + if alert_level <= 1 { return 0; } + if alert_level == 2 { return 1; } + if alert_level == 3 { return 2; } + if alert_level == 4 { return 3; } + 4 +} + +pub fn timer_ready(scan_timer: Int, scan_interval: Int) -> Int { + if scan_timer >= scan_interval { 1 } else { 0 } +} + +pub fn request_dispatch_phase(phase: Int) -> Int { + let o = ordinal_of(phase_of(phase)); + if o == 0 { return 1; } + o +} + +pub fn is_active(phase: Int) -> Int { + let o = ordinal_of(phase_of(phase)); + if o == 0 { return 0; } + 1 +} + +pub fn increment_counter(count: Int) -> Int { count + 1 } + +pub fn dormant_phase() -> Int { 0 } diff --git a/proposals/idaptik/migrated/SecurityAi/securityai.config.mjs b/proposals/idaptik/migrated/SecurityAi/securityai.config.mjs new file mode 100644 index 0000000..c6e045e --- /dev/null +++ b/proposals/idaptik/migrated/SecurityAi/securityai.config.mjs @@ -0,0 +1,69 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// affine-parity config for SecurityAi.affine (Int-only parity subset). +// Points at SecurityAiInt.affine which exposes only the Int-returning exports. +// Oracles re-derive from SecurityAI.res semantics in plain JS. + +function clamp_phase(phase) { + if (phase < 0) return 0; + if (phase > 4) return 4; + return phase; +} + +export default { + affine: "SecurityAiInt.affine", + cases: [ + { + name: "phase_value(phase -1..5)", + export: "phase_value", + args: [{ values: [-1, 0, 1, 2, 3, 4, 5] }], + oracle: (phase) => clamp_phase(phase), + }, + { + name: "phase_for_alert(alert_level 0..5)", + export: "phase_for_alert", + args: [{ values: [0, 1, 2, 3, 4, 5] }], + oracle: (alert_level) => { + if (alert_level <= 1) return 0; + if (alert_level === 2) return 1; + if (alert_level === 3) return 2; + if (alert_level === 4) return 3; + return 4; + }, + }, + { + name: "timer_ready(scan_timer, scan_interval): Int params", + export: "timer_ready", + args: [ + { values: [0, 1, 5, 9, 10, 11] }, + { values: [1, 5, 10] }, + ], + oracle: (scan_timer, scan_interval) => scan_timer >= scan_interval ? 1 : 0, + }, + { + name: "request_dispatch_phase(phase -1..5)", + export: "request_dispatch_phase", + args: [{ values: [-1, 0, 1, 2, 3, 4, 5] }], + oracle: (phase) => { const o = clamp_phase(phase); return o === 0 ? 1 : o; }, + }, + { + name: "is_active(phase -1..5)", + export: "is_active", + args: [{ values: [-1, 0, 1, 2, 3, 4, 5] }], + oracle: (phase) => clamp_phase(phase) === 0 ? 0 : 1, + }, + { + name: "increment_counter(count 0..20)", + export: "increment_counter", + args: [[0, 20]], + oracle: (count) => count + 1, + }, + { + name: "dormant_phase()", + export: "dormant_phase", + args: [], + oracle: () => 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/SecurityRank/SecurityLevelBoundary.agda b/proposals/idaptik/migrated/SecurityRank/SecurityLevelBoundary.agda new file mode 100644 index 0000000..59c5378 --- /dev/null +++ b/proposals/idaptik/migrated/SecurityRank/SecurityLevelBoundary.agda @@ -0,0 +1,72 @@ +{-# 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): +-- { +-- "Open": 0, +-- "Weak": 1, +-- "Medium": 2, +-- "Strong": 3 +-- } + +module SecurityLevelBoundary 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 = Open +-- c1 = Weak +-- c2 = Medium +-- c3 = Strong +data Host : Set where + c0 c1 c2 c3 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 + +-- 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 + +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/SecurityRank/SecurityRank.affine b/proposals/idaptik/migrated/SecurityRank/SecurityRank.affine new file mode 100644 index 0000000..7d5cb8c --- /dev/null +++ b/proposals/idaptik/migrated/SecurityRank/SecurityRank.affine @@ -0,0 +1,71 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// SecurityRank -- the device security-level ranking co-processor, the pure +// integer core extracted from DeviceRegistry.byMinSecurityLevel. Per the +// DESIGN-VISION ("AffineScript is the brain, JS/Pixi the senses; they pass +// primitives across the wasm boundary"), the JS host keeps the dict of devices +// and their string IP keys; AffineScript owns only the ordering arithmetic. +// +// The ReScript original folds a securityLevel variant through a four-arm rank +// switch (Open < Weak < Medium < Strong) and keeps a device iff its rank is at +// least the threshold's. We re-decompose that variant as the canonical 0..3 +// integer encoding the switch already produces, so the rank function is a clamp +// onto that closed band and the filter predicate is a single comparison. No +// strings, no floats, no effects cross the boundary; the encoding IS the rank. +// +//## Security-level encoding (the header contract for the JS host) +// level variant rank +// 0 Open 0 +// 1 Weak 1 +// 2 Medium 2 +// 3 Strong 3 +// Any input outside 0..3 is clamped to the nearest valid rank, so a malformed +// host level can never invert the ordering. + +enum Level { Open, Weak, Medium, Strong, Invalid(Int) } + +// Decode a host integer into a level variant. The trailing Invalid arm carries +// the offending value so the nullary variants ahead of it tag correctly and so +// the clamp can recover a defined rank. Flat guarded returns avoid the deep +// if/else expression nesting the parser dislikes. +fn level_of(level: Int) -> Level { + if level == 0 { return Open; } + if level == 1 { return Weak; } + if level == 2 { return Medium; } + if level == 3 { return Strong; } + Invalid(level) +} + +// Map a level variant to its ordinal rank. Out-of-band inputs clamp: anything +// below Open becomes 0, anything above Strong becomes 3, preserving the total +// order Open < Weak < Medium < Strong. +// @clamp:declared -- out-of-band level clamps to nearest valid rank (0 or 3). +// The clamp is provably controlled-loss: echo-boundary proves the four valid +// codes 0..3 are injective; Invalid(v) is intentionally squashed by design. +fn clamp_rank(v: Int) -> Int { + if v < 0 { return 0; } + 3 +} + +fn rank_of(l: Level) -> Int { + match l { + Open => 0, + Weak => 1, + Medium => 2, + Strong => 3, + Invalid(v) => clamp_rank(v) + } +} + +// Rank a security level, clamping the 0..3 encoding. Identity on valid input. +pub fn rank_security_level(level: Int) -> Int { + rank_of(level_of(level)) +} + +// The filter predicate of byMinSecurityLevel: keep a device iff its security +// rank meets or exceeds the threshold. Returns 1 to keep, 0 to drop. +pub fn passes_min_security(device_level: Int, threshold: Int) -> Int { + let dr = rank_of(level_of(device_level)); + let tr = rank_of(level_of(threshold)); + if dr >= tr { 1 } else { 0 } +} diff --git a/proposals/idaptik/migrated/SecurityRank/securityrank.config.mjs b/proposals/idaptik/migrated/SecurityRank/securityrank.config.mjs new file mode 100644 index 0000000..c0727d9 --- /dev/null +++ b/proposals/idaptik/migrated/SecurityRank/securityrank.config.mjs @@ -0,0 +1,44 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// 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 SecurityRank.affine (idaptik device security-level +// ranking co-processor). Oracle re-derives the 0..3 clamp and filter from the +// original DeviceRegistry.byMinSecurityLevel switch in SecurityRankCoprocessor.res +// and SecurityRank.res source semantics. +// +// Original logic (ReScript): +// rank switch: Open=0, Weak=1, Medium=2, Strong=3; out-of-band clamps +// filter: rank(device) >= rank(threshold) -> 1 (keep), else 0 + +// Independent oracle: rank from the original ReScript switch semantics +function oracleRank(level) { + if (level === 0) return 0; // Open + if (level === 1) return 1; // Weak + if (level === 2) return 2; // Medium + if (level === 3) return 3; // Strong + // Invalid: clamp -- below 0 -> 0, above 3 -> 3 + return level < 0 ? 0 : 3; +} + +function oraclePassesMin(deviceLevel, threshold) { + return oracleRank(deviceLevel) >= oracleRank(threshold) ? 1 : 0; +} + +export default { + affine: "SecurityRank.affine", + cases: [ + { + name: "rank_security_level over [-2..6]", + export: "rank_security_level", + args: [[-2, 6]], + oracle: (level) => oracleRank(level) | 0, + }, + { + name: "passes_min_security: device x threshold over [-1..4] x [-1..4]", + export: "passes_min_security", + args: [[-1, 4], [-1, 4]], + oracle: (d, t) => oraclePassesMin(d, t) | 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/SkillAbilities/SkillAbilities.affine b/proposals/idaptik/migrated/SkillAbilities/SkillAbilities.affine new file mode 100644 index 0000000..ed3dfdf --- /dev/null +++ b/proposals/idaptik/migrated/SkillAbilities/SkillAbilities.affine @@ -0,0 +1,85 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// SkillAbilities -- the ability-unlock decision co-processor, extracted from +// src/app/player/SkillAbilities.res. The ReScript original is a registry of 34 +// abilities whose payload is mostly strings (id, name, description); none of +// that crosses the wasm boundary. What DOES is the pure numeric decision that +// governs whether a given ability is unlocked, which the ReScript module folds +// out of two ingredients: +// +// rankMeetsRequirement(current, required) = rankValue(current) >= rankValue(required) +// isAbilityUnlocked = backgroundMatches && rankMeetsRequirement(skill.rank, required) +// +// Strings stay host-side, exactly as the migration brief requires: the JS host +// owns the ability ids, names and prose descriptions and resolves each ability +// to its required-rank index and exclusive-background index before calling in. +// The brain answers only in dense integers. +// +// PURE integer-only: no strings, no floats, no effects, no I/O. Each entry point +// is a flat sequence of guarded returns rather than a nested if/else chain, to +// keep the wasm backend's parser within its nesting tolerance. + +//## Boundary contract (the encoding the JS host marshals) +// param/return meaning defended range +// rank: Int dense skill-rank index 1 Novice .. 5 Expert; +// off-domain -> value 0 +// abilityBg: Int ability's exclusive-background index 0 = none (generic); +// >=1 = a specific background +// playerBg: Int operative's background index 0 = none chosen; +// >=1 = a specific background +// any predicate ret 1 = true, 0 = false total over all Int inputs + +//## Numeric value for a skill rank +// Mirrors JessicaBackground.rankValue: Novice->1 .. Expert->5. Off-domain +// indices yield 0, the sentinel the JS host treats as "no such rank". This is +// the same identity table SkillRank exposes; SkillAbilities replicates it so the +// unlock comparison is self-contained and need not call across modules. +pub fn rank_value(rank: Int) -> Int { + if rank == 1 { return 1; } + if rank == 2 { return 2; } + if rank == 3 { return 3; } + if rank == 4 { return 4; } + if rank == 5 { return 5; } + 0 +} + +//## Rank-requirement comparison +// rankMeetsRequirement(current, required): 1 when the current rank's value meets +// or exceeds the required rank's value, else 0. Off-domain ranks collapse to +// value 0 via rank_value, so an unknown current rank never spuriously unlocks a +// real requirement, and a requirement keyed on an unknown rank (value 0) is met +// by any in-domain current rank, matching the ReScript >= on rankValue. +pub fn rank_meets(current: Int, required: Int) -> Int { + if rank_value(current) >= rank_value(required) { return 1; } + 0 +} + +//## Background exclusivity check +// background_ok(abilityBg, playerBg): mirrors the ReScript exclusiveBackground +// fold. A generic ability (abilityBg == 0) is permitted for any operative. An +// exclusive ability (abilityBg >= 1) is permitted only when the player has a +// background (playerBg >= 1) and it equals the ability's required background. +// A player with no background (playerBg == 0) can never satisfy an exclusive +// ability, matching the ReScript `None => false` arm. +pub fn background_ok(abilityBg: Int, playerBg: Int) -> Int { + if abilityBg == 0 { return 1; } + if playerBg == 0 { return 0; } + if abilityBg == playerBg { return 1; } + 0 +} + +//## Full unlock decision +// isAbilityUnlocked, re-decomposed: an ability is unlocked when its exclusive +// background (if any) is satisfied AND the operative's rank in the ability's +// category meets the ability's required rank. The ReScript checks the background +// first and short-circuits; the same ordering holds here -- background failure +// alone denies the unlock regardless of rank. +// currentRank the operative's rank index in the ability's category +// requiredRank the ability's required rank index +// abilityBg the ability's exclusive-background index (0 = generic) +// playerBg the operative's background index (0 = none) +pub fn unlock_ok(currentRank: Int, requiredRank: Int, abilityBg: Int, playerBg: Int) -> Int { + if background_ok(abilityBg, playerBg) == 0 { return 0; } + if rank_meets(currentRank, requiredRank) == 1 { return 1; } + 0 +} diff --git a/proposals/idaptik/migrated/SkillRank/SkillRank.affine b/proposals/idaptik/migrated/SkillRank/SkillRank.affine new file mode 100644 index 0000000..c5b8cbd --- /dev/null +++ b/proposals/idaptik/migrated/SkillRank/SkillRank.affine @@ -0,0 +1,52 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// SkillRank -- the player skill-rank progression co-processor, extracted from +// src/app/player/JessicaBackground.res. The ReScript original keys the rank +// tables on a `skillRank` variant (Novice..Expert); here that variant collapses +// to a dense integer index, which is what crosses the wasm boundary. Index 1 is +// Novice, 2 Trained, 3 Proficient, 4 Veteran, 5 Expert. The numeric rank value +// rankValue() happens to equal that index, so rank_value is the identity on the +// valid domain, while xp_threshold carries the cumulative-XP table and +// can_promote folds the "is there a next rank and does the XP clear its +// threshold" check into one Int answer. +// +// PURE integer-only: no strings, no floats, no effects, no I/O. Each entry point +// is a flat sequence of guarded returns rather than a nested if/else expression +// chain, which keeps the wasm backend's parser within its nesting tolerance. + +//## Numeric value for a skill rank +// rankValue(): Novice->1 .. Expert->5. Off-domain indices yield 0, a sentinel +// the JS host can treat as "no such rank". +pub fn rank_value(rank: Int) -> Int { + if rank == 1 { return 1; } + if rank == 2 { return 2; } + if rank == 3 { return 3; } + if rank == 4 { return 4; } + if rank == 5 { return 5; } + 0 +} + +//## Cumulative XP required to reach each rank +// rankXpThreshold(): Novice->0, Trained->100, Proficient->350, Veteran->800, +// Expert->1500. Off-domain indices yield 0. +pub fn xp_threshold(rank: Int) -> Int { + if rank == 1 { return 0; } + if rank == 2 { return 100; } + if rank == 3 { return 350; } + if rank == 4 { return 800; } + if rank == 5 { return 1500; } + 0 +} + +//## Promotion eligibility +// Returns 1 when a next rank exists (the current rank is below Expert, i.e. in +// 1..4) and the accrued XP clears that next rank's threshold; otherwise 0. The +// top rank (Expert, 5) and any off-domain index have no successor and so can +// never promote. Mirrors the ReScript guard `nextRank exists && xp >= threshold`. +pub fn can_promote(rank: Int, xp: Int) -> Int { + if rank < 1 { return 0; } + if rank > 4 { return 0; } + let next = rank + 1; + if xp >= xp_threshold(next) { return 1; } + 0 +} diff --git a/proposals/idaptik/migration-map.json b/proposals/idaptik/migration-map.json index 5f7f84a..75e73ea 100644 --- a/proposals/idaptik/migration-map.json +++ b/proposals/idaptik/migration-map.json @@ -192,7 +192,16 @@ "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", + "status": "DONE", + "done": { + "date": "2026-06-05", + "phase": "fan-out wave (C6+C8)", + "staged_at": "proposals/idaptik/migrated/", + "kernels": ["CombatFx", "Detection", "DifficultyScale", "Distraction", "DualAlert", "HitboxGeom", "PlayerHp", "SecurityAi"], + "host_side_no_brain": ["Hitbox.res (geometry consumed by HitboxGeom)", "DualAlertBridge.res (string routing bridge)"], + "gates": "8/8 compile; 8185/8185 parity (re-run by parent); 2 echo-boundary LOSSLESS (DualAlert level, SecurityAi phase); 8/8 assail-clean (SecurityAi needed a guard-helper clamp fix at re-verification)", + "evidence": "proposals/idaptik/migrated/EVIDENCE-C6.adoc" + }, "files": [ "src/app/combat/CombatFxLogicCoprocessor.res", "src/app/combat/Hitbox.res", @@ -210,7 +219,12 @@ "id": "C7", "name": "Player coprocessors", "description": "Player attribute, loadout, skill and ability coprocessors \u2014 pure integer player state.", - "status": "TODO", + "status": "IN_PROGRESS", + "drafted_unverified": { + "date": "2026-06-05", + "note": "Agent timed out before writing parity configs/evidence. 8 .affine drafts exist in the working tree but are UNVERIFIED (no config.mjs, no boundary, no assail run) and deliberately NOT committed. Complete the 4 gates over the existing drafts.", + "kernels_drafted": ["CriticalRoll", "PlayerAttributes", "QCertifications", "SkillRank", "SkillAbilities", "QPrograms", "JessicaLoadout", "JessicaBackground"] + }, "files": [ "src/app/player/CriticalRollCoprocessor.res", "src/app/player/JessicaBackgroundCoprocessor.res", @@ -229,7 +243,16 @@ "id": "C8", "name": "Device and network coprocessors", "description": "Device state machine coprocessors: power, network transfer, security rank, covert link.", - "status": "TODO", + "status": "DONE", + "done": { + "date": "2026-06-05", + "phase": "fan-out wave (C6+C8)", + "staged_at": "proposals/idaptik/migrated/", + "kernels": ["GlobalNetworkData", "NetworkManager", "SecurityRank", "DeviceCaps", "LaptopState", "NetworkTransfer", "PowerManager", "CovertLink"], + "host_side_no_brain": ["DeviceFactory.res (registry/factory glue)", "PowerStationDevice.res (device wrapper)"], + "gates": "8/8 compile; 26095/26095 parity (re-run by parent); 5 echo-boundary LOSSLESS (security-level, device-type/security-colour ordinals, covert-link type/state); 8/8 assail-clean (NetworkManager + SecurityRank needed a guard-helper clamp fix at re-verification)", + "evidence": "proposals/idaptik/migrated/EVIDENCE-C8.adoc" + }, "files": [ "src/app/devices/CovertLinkCoprocessor.res", "src/app/devices/DeviceFactory.res",