From 18eb4eb3ac8135a280e3a18770f1387cb78edda8 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 5 Jun 2026 13:55:14 +0000 Subject: [PATCH] migrate(C7 complete): 8 player kernels verified + 6 boundary proofs C7 (player) cluster finished: two scoped agents (5 verify + 3 float re-decompose) plus full parent re-verification on the final state. All gates re-run by the parent (not agent-reported): - 8/8 compile - 4348/4348 parity vs independent ReScript-derived oracles - 6 echo-boundary LOSSLESS proofs re-typechecked with agda, exit 0 (QCertifications, SkillRank, JessicaLoadout x3, JessicaBackground) - 8/8 assail-clean 4 kernels hit the Float->wasm wall: CriticalRoll/PlayerAttributes/QPrograms re-decomposed Int-native (milli-unit convention, floats host-side); QCertifications' f64-comparison exports moved host-side. Parity caught and fixed an off-by-100 in PlayerAttributes. A mid-flight parent check had raced agent A and missed the boundary proofs it had not yet written; this commit reflects the post-completion re-run. Ledger + migration-map: C7 -> DONE. Evidence: migrated/EVIDENCE-C7.adoc. https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --- proposals/MIGRATION-PLAN.adoc | 2 +- .../migrated/CriticalRoll/CriticalRoll.affine | 125 ++++++---- .../CriticalRoll/criticalroll.config.mjs | 112 +++++++++ proposals/idaptik/migrated/EVIDENCE-C7.adoc | 88 +++++++ .../JessicaBackgroundBoundary.agda | 80 +++++++ .../jessicabackground.config.mjs | 79 ++++++ .../JessicaLoadoutConsumableBoundary.agda | 80 +++++++ .../JessicaLoadoutToolBoundary.agda | 88 +++++++ .../JessicaLoadoutWeaponBoundary.agda | 80 +++++++ .../JessicaLoadout/jessicaloadout.config.mjs | 146 +++++++++++ .../PlayerAttributes/PlayerAttributes.affine | 187 ++++++++------- .../playerattributes.config.mjs | 125 ++++++++++ .../QCertifications/QCertifications.affine | 26 +- .../QCertificationsBoundary.agda | 76 ++++++ .../qcertifications.config.mjs | 103 ++++++++ .../migrated/QPrograms/QPrograms.affine | 226 ++++++++++-------- .../migrated/QPrograms/qprograms.config.mjs | 173 ++++++++++++++ .../SkillAbilities/skillabilities.config.mjs | 82 +++++++ .../migrated/SkillRank/SkillRankBoundary.agda | 76 ++++++ .../migrated/SkillRank/skillrank.config.mjs | 79 ++++++ proposals/idaptik/migration-map.json | 12 +- 21 files changed, 1772 insertions(+), 273 deletions(-) create mode 100644 proposals/idaptik/migrated/CriticalRoll/criticalroll.config.mjs create mode 100644 proposals/idaptik/migrated/EVIDENCE-C7.adoc create mode 100644 proposals/idaptik/migrated/JessicaBackground/JessicaBackgroundBoundary.agda create mode 100644 proposals/idaptik/migrated/JessicaBackground/jessicabackground.config.mjs create mode 100644 proposals/idaptik/migrated/JessicaLoadout/JessicaLoadoutConsumableBoundary.agda create mode 100644 proposals/idaptik/migrated/JessicaLoadout/JessicaLoadoutToolBoundary.agda create mode 100644 proposals/idaptik/migrated/JessicaLoadout/JessicaLoadoutWeaponBoundary.agda create mode 100644 proposals/idaptik/migrated/JessicaLoadout/jessicaloadout.config.mjs create mode 100644 proposals/idaptik/migrated/PlayerAttributes/playerattributes.config.mjs create mode 100644 proposals/idaptik/migrated/QCertifications/QCertificationsBoundary.agda create mode 100644 proposals/idaptik/migrated/QCertifications/qcertifications.config.mjs create mode 100644 proposals/idaptik/migrated/QPrograms/qprograms.config.mjs create mode 100644 proposals/idaptik/migrated/SkillAbilities/skillabilities.config.mjs create mode 100644 proposals/idaptik/migrated/SkillRank/SkillRankBoundary.agda create mode 100644 proposals/idaptik/migrated/SkillRank/skillrank.config.mjs diff --git a/proposals/MIGRATION-PLAN.adoc b/proposals/MIGRATION-PLAN.adoc index 8c268c4..920d319 100644 --- a/proposals/MIGRATION-PLAN.adoc +++ b/proposals/MIGRATION-PLAN.adoc @@ -191,7 +191,7 @@ Heuristic: | 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. +| C7 | DONE | Player cluster complete (2026-06-05): two scoped agents (5 verify + 3 float-re-decompose) + parent re-verification. *8 kernels* — CriticalRoll, PlayerAttributes, QCertifications, SkillRank, SkillAbilities, QPrograms, JessicaLoadout, JessicaBackground. *Four gates green (every gate re-run by parent):* 8/8 compile, *4348/4348 parity* (independent oracles), *6 echo-boundary LOSSLESS proofs* across 4 kernels (QCertifications, SkillRank, JessicaLoadout×3, JessicaBackground — agda re-typechecked by parent, exit 0); the other 4 transform/classifier kernels G3-n/a, 8/8 assail-clean. 3 kernels (CriticalRoll/PlayerAttributes/QPrograms) hit the Float→wasm wall (`min_float`/`max_float`/`trunc`) and were re-decomposed Int-native (milli-unit convention, floats host-side) per the C6 `*Int` pattern; parity caught + fixed an off-by-100 in PlayerAttributes. Evidence: `migrated/EVIDENCE-C7.adoc`. NEXT: C2 wave 2. | 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/CriticalRoll/CriticalRoll.affine b/proposals/idaptik/migrated/CriticalRoll/CriticalRoll.affine index bd693b9..04cfc2d 100644 --- a/proposals/idaptik/migrated/CriticalRoll/CriticalRoll.affine +++ b/proposals/idaptik/migrated/CriticalRoll/CriticalRoll.affine @@ -1,75 +1,94 @@ // SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell // // 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. +// src/app/player/CriticalRollCoprocessor.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 Int the boundary admits yields a defined Int +// verdict or Int 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. +// 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. +// 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. +//## Int-native convention (MILLI-UNITS): the host pre-floors floats to ints +// All probabilities and roll values cross as MILLI-UNITS (×1000 of the Float): +// roll_milli = round(roll * 1000) e.g. 0.37 -> 370 +// crit_success_milli returned from jessica_crit_success_milli +// crit_fail_milli returned from jessica_crit_fail_milli +// +// Game stats (primaryStat, wil) are integer-valued in the ReScript source +// (e.g. 80, 100, 150) and cross as raw Int -- NOT scaled. The division +// (stat - 100)/1000 in the original formulae has value < 1 and contributes +// only to the milli result: the integer formula below is exact. +// +// The original Float formulae and their milli-integer equivalents: +// jessica_crit_success: min(0.25, 0.05 + (stat-100)/1000.0) +// -> milli: min(250, 50 + (stat - 100)) [= min(250, stat - 50)] +// jessica_crit_fail: max(0.01, 0.10 + (100-wil)/1000.0) +// -> milli: max(10, 100 + (100 - wil)) [= max(10, 200 - wil)] +// classify_outcome: roll < crit_success / roll > 1 - crit_fail +// -> milli: roll_milli < cs_milli / roll_milli > (1000 - cf_milli) +// +// Arithmetic is identical to the ReScript on integer-valued stats (which are +// always whole numbers in game data). The host applies Math.round(x*1000) for +// the roll. + +fn imin(a: Int, b: Int) -> Int { + if a < b { a } else { b } +} + +fn imax(a: Int, b: Int) -> Int { + if a > b { a } else { b } +} -//## 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-success threshold (milli-units) +// ReScript: min(0.25, 0.05 + (primaryStat - 100)/1000). In milli (stat is raw +// integer game stat): min(250, 50 + (stat - 100)). Cap at 250 (= 0.25). +pub fn jessica_crit_success_milli(stat: Int) -> Int { + imin(250, 50 + (stat - 100)) } -//## 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) +//## Jessica's critical-failure threshold (milli-units) +// ReScript: max(0.01, 0.10 + (100 - wil)/1000). In milli: max(10, 100 + (100 - +// wil)) = max(10, 200 - wil). Floor at 10 (= 0.01). +pub fn jessica_crit_fail_milli(wil: Int) -> Int { + imax(10, 200 - wil) } //## 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 +// if roll_milli < crit_success_milli -> CriticalSuccess (0) +// else if roll_milli > 1000 - crit_fail_milli -> CriticalFailure (2) +// else -> Normal (1) +// Flat guarded returns rather than nested if/else. 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; } +pub fn classify_outcome(roll_milli: Int, crit_success_milli: Int, crit_fail_milli: Int) -> Int { + if roll_milli < crit_success_milli { return 0; } + if roll_milli > (1000 - crit_fail_milli) { return 2; } 1 } diff --git a/proposals/idaptik/migrated/CriticalRoll/criticalroll.config.mjs b/proposals/idaptik/migrated/CriticalRoll/criticalroll.config.mjs new file mode 100644 index 0000000..8cf04f8 --- /dev/null +++ b/proposals/idaptik/migrated/CriticalRoll/criticalroll.config.mjs @@ -0,0 +1,112 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// affine-parity config for CriticalRoll.affine (Int-native, milli-units). +// Oracles re-derive from CriticalRollCoprocessor.res semantics in plain JS. +// +// All probabilities and roll values are milli-units (×1000 of the original +// Float). Stats (primaryStat, wil) cross as raw integers. +// +// jessica_crit_success_milli: min(250, 50 + (stat - 100)) +// ReScript equivalent: min(0.25, 0.05 + (stat-100)/1000.0) * 1000 +// jessica_crit_fail_milli: max(10, 200 - wil) +// ReScript equivalent: max(0.01, 0.10 + (100-wil)/1000.0) * 1000 +// classify_outcome(roll_milli, cs_milli, cf_milli): +// roll_milli < cs_milli -> 0, roll_milli > 1000-cf_milli -> 2, else 1 + +function jCritSuccessMilli(stat) { + // Original: min(0.25, 0.05 + (stat - 100) / 1000.0) + const v = 0.05 + (stat - 100) / 1000.0; + const clamped = Math.min(0.25, v); + return Math.round(clamped * 1000); +} + +function jCritFailMilli(wil) { + // Original: max(0.01, 0.10 + (100 - wil) / 1000.0) + const v = 0.10 + (100 - wil) / 1000.0; + const clamped = Math.max(0.01, v); + return Math.round(clamped * 1000); +} + +function classifyOutcome(rollMilli, csMilli, cfMilli) { + // Original: roll < critSuccess -> 0; roll > 1 - critFail -> 2; else 1 + if (rollMilli < csMilli) return 0; + if (rollMilli > (1000 - cfMilli)) return 2; + return 1; +} + +// Stat range: 0 to 200 (game stats). Roll range: 0..1000 milli. +const STAT_VALUES = [0, 50, 80, 100, 120, 150, 200]; +const WIL_VALUES = [0, 50, 80, 100, 120, 150, 200]; +const ROLL_VALUES = [0, 10, 50, 100, 200, 250, 499, 500, 501, 750, 900, 990, 1000]; + +export default { + affine: "CriticalRoll.affine", + compile: false, + cases: [ + { + name: "jessica_crit_success_milli(stat 0..200): min(250, stat-50)", + export: "jessica_crit_success_milli", + args: [{ values: STAT_VALUES }], + oracle: (stat) => jCritSuccessMilli(stat), + }, + { + name: "jessica_crit_fail_milli(wil 0..200): max(10, 200-wil)", + export: "jessica_crit_fail_milli", + args: [{ values: WIL_VALUES }], + oracle: (wil) => jCritFailMilli(wil), + }, + { + name: "classify_outcome(roll_milli, cs_milli, cf_milli) stat=100", + export: "classify_outcome", + args: [ + { values: ROLL_VALUES }, + { values: [jCritSuccessMilli(100)] }, // 50 milli (stat=100 baseline) + { values: [jCritFailMilli(100)] }, // 100 milli (wil=100 baseline) + ], + oracle: (r, cs, cf) => classifyOutcome(r, cs, cf), + }, + { + name: "classify_outcome boundary: roll exactly on cs threshold", + export: "classify_outcome", + args: [ + // roll == crit_success_milli -> Normal (strict <) + { values: [50, 51, 49] }, + { values: [50] }, + { values: [100] }, + ], + oracle: (r, cs, cf) => classifyOutcome(r, cs, cf), + }, + { + name: "classify_outcome boundary: roll exactly on 1000-cf threshold", + export: "classify_outcome", + args: [ + // cf=100, threshold = 1000-100=900; roll==900 -> Normal (strict >) + { values: [899, 900, 901] }, + { values: [50] }, + { values: [100] }, + ], + oracle: (r, cs, cf) => classifyOutcome(r, cs, cf), + }, + { + name: "classify_outcome wide sweep (stat=80, wil=150)", + export: "classify_outcome", + args: [ + { values: ROLL_VALUES }, + { values: [jCritSuccessMilli(80)] }, + { values: [jCritFailMilli(150)] }, + ], + oracle: (r, cs, cf) => classifyOutcome(r, cs, cf), + }, + { + name: "classify_outcome wide sweep (stat=150, wil=50)", + export: "classify_outcome", + args: [ + { values: ROLL_VALUES }, + { values: [jCritSuccessMilli(150)] }, + { values: [jCritFailMilli(50)] }, + ], + oracle: (r, cs, cf) => classifyOutcome(r, cs, cf), + }, + ], +}; diff --git a/proposals/idaptik/migrated/EVIDENCE-C7.adoc b/proposals/idaptik/migrated/EVIDENCE-C7.adoc new file mode 100644 index 0000000..064c34c --- /dev/null +++ b/proposals/idaptik/migrated/EVIDENCE-C7.adoc @@ -0,0 +1,88 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += Cluster C7 (player) — four-gate evidence (captured 2026-06-05) +:toc: macro + +[IMPORTANT] +==== +*Captured run of the 4-gate recipe over the cluster-C7 player kernels.* +Produced by two scoped agents (5 already-compiling kernels verified; 3 +Float-wall kernels re-decomposed Int-native) and then *independently +re-verified by the parent on the final state* — every parity sweep, assail +scan, compile, and Agda boundary proof was re-run, not trusted from the +agent reports. (An earlier mid-flight parent check raced agent A and missed +the boundary proofs it had not yet written; the figures here are from the +post-completion re-run.) Toolchain: AffineScript compiler +`_build/default/bin/main.exe`, Deno 2.8.2, Agda 2.6.3. +==== + +toc::[] + +== Summary + +[cols="2,1,1,2,1",options="header"] +|=== +| Kernel | G1 compile | G2 parity | G3 boundary | G4 assail +| `CriticalRoll` | OK | 59/59 | n/a (transform) | clean +| `PlayerAttributes` | OK | 155/155 | n/a (transform) | clean +| `QCertifications` | OK | 101/101 | LOSSLESS (certTier, 5) | clean +| `SkillRank` | OK | 180/180 | LOSSLESS (skillRank, 5) | clean +| `SkillAbilities` | OK | 894/894 | n/a (classifier) | clean +| `QPrograms` | OK | 2593/2593 | n/a (transform) | clean +| `JessicaLoadout` | OK | 265/265 | LOSSLESS x3 (weapon 6, tool 8, consumable 6) | clean +| `JessicaBackground` | OK | 101/101 | LOSSLESS (background, 6) | clean +| *Total* | *8/8* | *4348/4348* | *6 LOSSLESS proofs* | *8/8 clean* +|=== + +== G3 — echo-boundary (6 LOSSLESS proofs) + +Four of the eight kernels carry a discrete value-to-integer ENCODING (an +enum tier/rank/type table), so injectivity is the relevant faithfulness +property and is machine-proved: `QCertificationsBoundary`, +`SkillRankBoundary`, `JessicaLoadoutWeaponBoundary`, +`JessicaLoadoutToolBoundary`, `JessicaLoadoutConsumableBoundary`, +`JessicaBackgroundBoundary` — 6 Agda modules, each instantiating the +`EchoEncodingFaithfulness` framework and proving `code-injective`. All 6 +were re-typechecked by the parent (`agda` exit 0). + +The other four kernels (`CriticalRoll`, `PlayerAttributes`, `QPrograms`, +`SkillAbilities`) are numeric transforms / pure classifiers with no +encoding table, so G3 does not apply — the G2 round-trip against the +independent oracle is the faithfulness check. + +== The Float-to-wasm wall (4 of 8 kernels) + +Four kernels used Float operations the AffineScript backend cannot lower — +the same wall the C2/C6/C8 waves hit, now a 5th data point. Three were +re-decomposed Int-native to the milli-unit convention (the JS host scales +floats by 1000 / pre-floors; the wasm brain is pure integer), per the +DualAlert / CombatFxInt exemplars; the fourth had its Float-param exports +removed to the host: + +[cols="2,2,3",options="header"] +|=== +| Kernel | Float issue | Resolution +| `CriticalRoll` | `min_float`, `max_float` undefined | stats cross as raw Int; probabilities as milli-units; `imin`/`imax` integer helpers +| `PlayerAttributes` | `max_float`, `min_float` undefined | all functions Int-native milli-units; `imax`/`imin` helpers +| `QPrograms` | `trunc` undefined | `trunc((m-1)*100)` becomes `(m_milli-1000)/10` (integer division == truncation for non-negative, matching ReScript `Float.toInt`) +| `QCertifications` | f64-comparison pub fns emit `i32.ge_s` -> uninstantiable wasm | the two Float-param exports removed to host-side; integer logic + certTier encoding retained and proved +|=== + +*Parity caught a real bug:* `PlayerAttributes.jump_acceleration_milli` was +first coded as `dex` instead of `dex*100` (0.1 x dex x 1000); the +differential sweep flagged the mismatch and it was fixed before the final +green run. The differential harness doing its job — a transcription error a +"looks right" read would have shipped. + +== Re-verification (parent, independent, final state) + +Every figure above was reproduced by the parent re-running the gates +directly after both agents completed: `parity.mjs` recompiles each +`.affine` and executes the wasm over the full Cartesian input sweep; +`assail.mjs` re-scanned each source; each boundary `.agda` was copied into +the echo mirror and re-typechecked with `agda`. All reproduced clean. + +== Remaining in cluster C7 + +None — the cluster is complete. `Player.res` itself is a host-side +composition shell (no separable integer brain) and is not a kernel. diff --git a/proposals/idaptik/migrated/JessicaBackground/JessicaBackgroundBoundary.agda b/proposals/idaptik/migrated/JessicaBackground/JessicaBackgroundBoundary.agda new file mode 100644 index 0000000..193e747 --- /dev/null +++ b/proposals/idaptik/migrated/JessicaBackground/JessicaBackgroundBoundary.agda @@ -0,0 +1,80 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "Assault": 0, +-- "Recon": 1, +-- "Engineer": 2, +-- "Signals": 3, +-- "Medic": 4, +-- "Logistics": 5 +-- } + +module JessicaBackgroundBoundary 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 = Assault +-- c1 = Recon +-- c2 = Engineer +-- c3 = Signals +-- c4 = Medic +-- c5 = Logistics +data Host : Set where + c0 c1 c2 c3 c4 c5 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 +code c4 = 4 +code c5 = 5 + +-- Injectivity by exhaustive case analysis. The codes are literal +-- numerals, so listing the diagonal refl clauses is enough: Agda's +-- coverage checker discharges the off-diagonal pairs as absurd +-- numeral equalities (mirrors rankCode-injective). +code-injective : Injective code +code-injective {c0} {c0} _ = refl +code-injective {c1} {c1} _ = refl +code-injective {c2} {c2} _ = refl +code-injective {c3} {c3} _ = refl +code-injective {c4} {c4} _ = refl +code-injective {c5} {c5} _ = refl + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +-- Re-export the lossless-half headline, instantiated and proved: +-- every integer code determines its host value uniquely. +module Theorems = EncodingTheorems encoding + +boundary-lossless : + (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂ +boundary-lossless = Theorems.encoding-lossless code-injective + diff --git a/proposals/idaptik/migrated/JessicaBackground/jessicabackground.config.mjs b/proposals/idaptik/migrated/JessicaBackground/jessicabackground.config.mjs new file mode 100644 index 0000000..fcb68a3 --- /dev/null +++ b/proposals/idaptik/migrated/JessicaBackground/jessicabackground.config.mjs @@ -0,0 +1,79 @@ +// 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 JessicaBackground.affine (idaptik operative-background +// attribute-bonus matrix and starting-skill grant; scalar i32 ABI). The oracle +// re-derives each function from the original JessicaBackground.res getBonus and +// makeSkillSet semantics so a codegen regression surfaces as a differential +// mismatch. +// +// Background encoding (JessicaBackground.all order): +// 0 Assault 1 Recon 2 Engineer 3 Signals 4 Medic 5 Logistics +// Attribute-column encoding (attributeBonus field order): +// 0 str 1 dex 2 con 3 int_ 4 wil 5 cha +// Skill-category encoding (skillCategory variant order): +// 0 Infiltration 1 CombatSkill 2 Athletics 3 Observation +// 4 TechLiteracy 5 Fieldcraft 6 Composure +// +// getBonus matrix from JessicaBackground.res (all shifts are integer): +// Assault: str+20 dex+10 con+15 int_-5 wil+5 cha-5 +// Recon: str-5 dex+15 con+0 int_+10 wil+10 cha+0 +// Engineer: str+5 dex+5 con+5 int_+15 wil+5 cha-5 +// Signals: str-5 dex+5 con+0 int_+10 wil+10 cha+10 +// Medic: str+0 dex+5 con+20 int_+10 wil+10 cha+0 +// Logistics: str+10 dex+0 con+10 int_+5 wil+0 cha+10 +// off-domain bg or attr: 0 + +// Bonus matrix re-derived from JessicaBackground.res getBonus (NOT from .affine). +const BONUS = [ + // str dex con int_ wil cha + [20, 10, 15, -5, 5, -5], // 0 Assault + [-5, 15, 0, 10, 10, 0], // 1 Recon + [5, 5, 5, 15, 5, -5], // 2 Engineer + [-5, 5, 0, 10, 10, 10], // 3 Signals + [0, 5, 20, 10, 10, 0], // 4 Medic + [10, 0, 10, 5, 0, 10], // 5 Logistics +]; + +const bonus = (bg, attr) => { + if (bg < 0 || bg > 5) return 0; + if (attr < 0 || attr > 5) return 0; + return BONUS[bg][attr]; +}; + +// start_skill from JessicaBackground.res makeSkillSet background switch: +// Assault(0) -> CombatSkill(1) +// Recon(1) -> Observation(3) +// Engineer(2) -> TechLiteracy(4) +// Signals(3) -> TechLiteracy(4) +// Medic(4) -> Composure(6) +// Logistics(5) -> Fieldcraft(5) +// off-domain -> -1 +const startSkill = (bg) => { + if (bg === 0) return 1; + if (bg === 1) return 3; + if (bg === 2) return 4; + if (bg === 3) return 4; + if (bg === 4) return 6; + if (bg === 5) return 5; + return -1; +}; + +export default { + affine: "JessicaBackground.affine", + cases: [ + { + name: "bonus over bg[-2..7] × attr[-1..7]", + export: "bonus", + args: [[-2, 7], [-1, 7]], + oracle: (bg, attr) => bonus(bg, attr), + }, + { + name: "start_skill over [-2..8]", + export: "start_skill", + args: [[-2, 8]], + oracle: (bg) => startSkill(bg), + }, + ], +}; diff --git a/proposals/idaptik/migrated/JessicaLoadout/JessicaLoadoutConsumableBoundary.agda b/proposals/idaptik/migrated/JessicaLoadout/JessicaLoadoutConsumableBoundary.agda new file mode 100644 index 0000000..b925c9b --- /dev/null +++ b/proposals/idaptik/migrated/JessicaLoadout/JessicaLoadoutConsumableBoundary.agda @@ -0,0 +1,80 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "Flashbang": 0, +-- "SmokeGrenade": 1, +-- "ZipTies": 2, +-- "AdrenalineShot": 3, +-- "DecoyPhone": 4, +-- "FibreTap": 5 +-- } + +module JessicaLoadoutConsumableBoundary 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 = Flashbang +-- c1 = SmokeGrenade +-- c2 = ZipTies +-- c3 = AdrenalineShot +-- c4 = DecoyPhone +-- c5 = FibreTap +data Host : Set where + c0 c1 c2 c3 c4 c5 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 +code c4 = 4 +code c5 = 5 + +-- Injectivity by exhaustive case analysis. The codes are literal +-- numerals, so listing the diagonal refl clauses is enough: Agda's +-- coverage checker discharges the off-diagonal pairs as absurd +-- numeral equalities (mirrors rankCode-injective). +code-injective : Injective code +code-injective {c0} {c0} _ = refl +code-injective {c1} {c1} _ = refl +code-injective {c2} {c2} _ = refl +code-injective {c3} {c3} _ = refl +code-injective {c4} {c4} _ = refl +code-injective {c5} {c5} _ = refl + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +-- Re-export the lossless-half headline, instantiated and proved: +-- every integer code determines its host value uniquely. +module Theorems = EncodingTheorems encoding + +boundary-lossless : + (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂ +boundary-lossless = Theorems.encoding-lossless code-injective + diff --git a/proposals/idaptik/migrated/JessicaLoadout/JessicaLoadoutToolBoundary.agda b/proposals/idaptik/migrated/JessicaLoadout/JessicaLoadoutToolBoundary.agda new file mode 100644 index 0000000..c041be8 --- /dev/null +++ b/proposals/idaptik/migrated/JessicaLoadout/JessicaLoadoutToolBoundary.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): +-- { +-- "LockpickSet": 0, +-- "GrapplingHook": 1, +-- "MotionSensor": 2, +-- "SignalJammer": 3, +-- "TraumaKit": 4, +-- "C4Charge": 5, +-- "GhillieWrap": 6, +-- "FieldSurgeryKit": 7 +-- } + +module JessicaLoadoutToolBoundary 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 = LockpickSet +-- c1 = GrapplingHook +-- c2 = MotionSensor +-- c3 = SignalJammer +-- c4 = TraumaKit +-- c5 = C4Charge +-- c6 = GhillieWrap +-- c7 = FieldSurgeryKit +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/JessicaLoadout/JessicaLoadoutWeaponBoundary.agda b/proposals/idaptik/migrated/JessicaLoadout/JessicaLoadoutWeaponBoundary.agda new file mode 100644 index 0000000..dbdd7df --- /dev/null +++ b/proposals/idaptik/migrated/JessicaLoadout/JessicaLoadoutWeaponBoundary.agda @@ -0,0 +1,80 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "StunPistol": 0, +-- "TacticalBaton": 1, +-- "TranqRifle": 2, +-- "BreachingShotgun": 3, +-- "Railgun": 4, +-- "EMPPistol": 5 +-- } + +module JessicaLoadoutWeaponBoundary 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 = StunPistol +-- c1 = TacticalBaton +-- c2 = TranqRifle +-- c3 = BreachingShotgun +-- c4 = Railgun +-- c5 = EMPPistol +data Host : Set where + c0 c1 c2 c3 c4 c5 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 +code c4 = 4 +code c5 = 5 + +-- Injectivity by exhaustive case analysis. The codes are literal +-- numerals, so listing the diagonal refl clauses is enough: Agda's +-- coverage checker discharges the off-diagonal pairs as absurd +-- numeral equalities (mirrors rankCode-injective). +code-injective : Injective code +code-injective {c0} {c0} _ = refl +code-injective {c1} {c1} _ = refl +code-injective {c2} {c2} _ = refl +code-injective {c3} {c3} _ = refl +code-injective {c4} {c4} _ = refl +code-injective {c5} {c5} _ = refl + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +-- Re-export the lossless-half headline, instantiated and proved: +-- every integer code determines its host value uniquely. +module Theorems = EncodingTheorems encoding + +boundary-lossless : + (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂ +boundary-lossless = Theorems.encoding-lossless code-injective + diff --git a/proposals/idaptik/migrated/JessicaLoadout/jessicaloadout.config.mjs b/proposals/idaptik/migrated/JessicaLoadout/jessicaloadout.config.mjs new file mode 100644 index 0000000..ae210da --- /dev/null +++ b/proposals/idaptik/migrated/JessicaLoadout/jessicaloadout.config.mjs @@ -0,0 +1,146 @@ +// 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 JessicaLoadout.affine (idaptik loadout access +// arithmetic; scalar i32 ABI). The oracle re-derives each function from the +// original JessicaLoadout.res / JessicaLoadoutCoprocessorBridge.js semantics so +// a codegen regression surfaces as a differential mismatch. +// +// Weapon encoding (allWeapons order): +// 0 StunPistol 1 TacticalBaton 2 TranqRifle +// 3 BreachingShotgun 4 Railgun 5 EMPPistol +// Tool encoding (allTools order): +// 0 LockpickSet 1 GrapplingHook 2 MotionSensor 3 SignalJammer +// 4 TraumaKit 5 C4Charge 6 GhillieWrap 7 FieldSurgeryKit +// Consumable encoding (allConsumables order): +// 0 Flashbang 1 SmokeGrenade 2 ZipTies +// 3 AdrenalineShot 4 DecoyPhone 5 FibreTap +// Background encoding (JessicaBackground.all order): +// 0 Assault 1 Recon 2 Engineer 3 Signals 4 Medic 5 Logistics + +// weapon_tier from JessicaLoadout.res getWeaponInfo tiers: +// 0 StunPistol T1=1, 1 TacticalBaton T1=1, 2 TranqRifle T2=2, +// 3 BreachingShotgun T2=2, 4 Railgun T3=3, 5 EMPPistol T3=3; off-domain 0 +const weaponTier = (w) => { + if (w === 0) return 1; + if (w === 1) return 1; + if (w === 2) return 2; + if (w === 3) return 2; + if (w === 4) return 3; + if (w === 5) return 3; + return 0; +}; + +// tool_tier from JessicaLoadout.res getToolInfo tiers: +// 0 LockpickSet T1=1, 1 GrapplingHook T1=1, +// 2 MotionSensor T2=2, 3 SignalJammer T2=2, 4 TraumaKit T2=2, 5 C4Charge T2=2, +// 6 GhillieWrap T3=3, 7 FieldSurgeryKit T3=3; off-domain 0 +const toolTier = (t) => { + if (t === 0) return 1; + if (t === 1) return 1; + if (t === 2) return 2; + if (t === 3) return 2; + if (t === 4) return 2; + if (t === 5) return 2; + if (t === 6) return 3; + if (t === 7) return 3; + return 0; +}; + +// consumable_uses from JessicaLoadout.res getConsumableInfo: +// 0 Flashbang=2, 1 SmokeGrenade=2, 2 ZipTies=3, +// 3 AdrenalineShot=1, 4 DecoyPhone=2, 5 FibreTap=1; off-domain 0 +const consumableUses = (c) => { + if (c === 0) return 2; + if (c === 1) return 2; + if (c === 2) return 3; + if (c === 3) return 1; + if (c === 4) return 2; + if (c === 5) return 1; + return 0; +}; + +// can_use_weapon from JessicaLoadout.res canUseWeapon: +// T1 (0,1): always 1 regardless of background +// 2 TranqRifle: Assault(0) or Recon(1) => 1, else 0 +// 3 BreachingShotgun: Assault(0) or Engineer(2) => 1, else 0 +// 4 Railgun: Assault(0) => 1, else 0 +// 5 EMPPistol: Engineer(2) or Signals(3) => 1, else 0 +// off-domain weapon or background: 0 +const canUseWeapon = (w, bg) => { + if (w === 0) return 1; + if (w === 1) return 1; + if (w === 2) return bg === 0 || bg === 1 ? 1 : 0; + if (w === 3) return bg === 0 || bg === 2 ? 1 : 0; + if (w === 4) return bg === 0 ? 1 : 0; + if (w === 5) return bg === 2 || bg === 3 ? 1 : 0; + return 0; +}; + +// can_use_tool from JessicaLoadout.res canUseTool: +// T1 (0,1): always 1 +// 2 MotionSensor: Recon(1) +// 3 SignalJammer: Signals(3) +// 4 TraumaKit: Medic(4) +// 5 C4Charge: Engineer(2) +// 6 GhillieWrap: Recon(1) +// 7 FieldSurgeryKit: Medic(4) +// off-domain: 0 +const canUseTool = (t, bg) => { + if (t === 0) return 1; + if (t === 1) return 1; + if (t === 2) return bg === 1 ? 1 : 0; + if (t === 3) return bg === 3 ? 1 : 0; + if (t === 4) return bg === 4 ? 1 : 0; + if (t === 5) return bg === 2 ? 1 : 0; + if (t === 6) return bg === 1 ? 1 : 0; + if (t === 7) return bg === 4 ? 1 : 0; + return 0; +}; + +// use_consumable from JessicaLoadout.res useConsumable: +// usesLeft > 0 => usesLeft - 1; else 0 +const useConsumable = (usesLeft) => (usesLeft > 0 ? usesLeft - 1 : 0); + +export default { + affine: "JessicaLoadout.affine", + cases: [ + { + name: "weapon_tier over [-2..8]", + export: "weapon_tier", + args: [[-2, 8]], + oracle: (w) => weaponTier(w), + }, + { + name: "tool_tier over [-2..10]", + export: "tool_tier", + args: [[-2, 10]], + oracle: (t) => toolTier(t), + }, + { + name: "consumable_uses over [-2..8]", + export: "consumable_uses", + args: [[-2, 8]], + oracle: (c) => consumableUses(c), + }, + { + name: "can_use_weapon over weapon[-2..8] × bg[-1..7]", + export: "can_use_weapon", + args: [[-2, 8], [-1, 7]], + oracle: (w, bg) => canUseWeapon(w, bg), + }, + { + name: "can_use_tool over tool[-2..10] × bg[-1..7]", + export: "can_use_tool", + args: [[-2, 10], [-1, 7]], + oracle: (t, bg) => canUseTool(t, bg), + }, + { + name: "use_consumable over [-3..10]", + export: "use_consumable", + args: [[-3, 10]], + oracle: (u) => useConsumable(u), + }, + ], +}; diff --git a/proposals/idaptik/migrated/PlayerAttributes/PlayerAttributes.affine b/proposals/idaptik/migrated/PlayerAttributes/PlayerAttributes.affine index 2aa93c7..285e4d4 100644 --- a/proposals/idaptik/migrated/PlayerAttributes/PlayerAttributes.affine +++ b/proposals/idaptik/migrated/PlayerAttributes/PlayerAttributes.affine @@ -1,140 +1,145 @@ // SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell // // 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. +// src/app/player/PlayerAttributesCoprocessor.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. // //## 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. +// Every getter here is a pure function of one or two attribute stats: 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. +// no arithmetic beyond 100 + bonus. That is host record-building and stays in +// the bridge with the variant; only the six summed stat fields would cross, and +// they add nothing the host cannot do with `+`. The getters that are bare +// scalings 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. +//## Int-native convention (MILLI-UNITS): the host pre-floors floats to ints +// Game stats (str, dex, con, int, wil, cha) are integer-valued in the ReScript +// source and cross as raw Int (e.g. dex=100). All RESULTS cross as MILLI-UNITS +// (×1000 of the original Float result): +// result_milli = round(float_result * 1000) // -//## 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 +// The mapping for each function (stat is raw integer, result is ×1000): +// speed_multiplier_milli(dex) = dex * 10 (dex/100 * 1000) +// max_jump_milli(str) = str * 5000 (5*str * 1000; host divides by 1000) +// jump_acceleration_milli(dex) = dex * 100 (0.1*dex * 1000) +// trajectory_divisor_milli(base_m, intel, len, dflt_m) +// = if len==0: dflt_m, else (base_m * intel) / len +// base and dflt in milli; intel/len raw ints +// tech_task_speed_milli(intel, wil) = (intel * 600 + wil * 400) / 100 +// ((int*0.6 + wil*0.4)/100 * 1000) +// critical_failure_threshold_milli(wil) = max(10, 200 - wil) +// (max(0.01, 0.10+(100-wil)/1000) * 1000) +// critical_success_chance_milli(stat) = min(250, 50 + (stat - 100)) +// (min(0.25, 0.05+(stat-100)/1000) * 1000) +// distraction_effectiveness_milli(cha) = cha * 10 (cha/100 * 1000) +// moletaire_obedience_milli(cha) = 800 + cha * 2 (0.8+cha/500) * 1000) +// fall_damage_resistance_milli(con) = max(300, 1000 - (con - 100) * 5) +// (max(0.3, 1-(con-100)/200) * 1000) +// lockpick_speed_milli(dex) = dex * 10 (dex/100 * 1000) +// melee_damage_milli(str) = str * 10 (str/100 * 1000) + +fn imin(a: Int, b: Int) -> Int { + if a < b { a } else { b } +} + +fn imax(a: Int, b: Int) -> Int { + if a > b { a } else { b } +} //## DEX-scaled movement speed multiplier, 1.0 at baseline 100. -pub fn speed_multiplier(dex: Float) -> Float { - dex / 100.0 +// dex/100.0 * 1000 = dex * 10. +pub fn speed_multiplier_milli(dex: Int) -> Int { + dex * 10 } //## STR-scaled maximum jump magnitude, MAXJMP_MULT(5) * STR. -pub fn max_jump(strength: Float) -> Float { - 5.0 * strength +// 5 * str * 1000. +pub fn max_jump_milli(strength: Int) -> Int { + strength * 5000 } //## DEX-scaled jump charge accumulation rate, JMPACC_MULT(0.1) * DEX. -pub fn jump_acceleration(dex: Float) -> Float { - 0.1 * dex +// 0.1 * dex * 1000 = dex * 100. +pub fn jump_acceleration_milli(dex: Int) -> Int { + dex * 100 } //## 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 +// base and dflt are milli-units; intel and len are raw integer stats. +// (base_milli * intel) / len; falls back to dflt_milli when len is zero. +// Integer division here equals float division for the integer-valued inputs +// the host supplies (len is pixel/unit count, not fractional). +pub fn trajectory_divisor_milli(base_milli: Int, intel: Int, len: Int, dflt_milli: Int) -> Int { + if len == 0 { + dflt_milli } else { - (base * intel) / len + (base_milli * 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 +// (intel * 0.6 + wil * 0.4) / 100 * 1000 = (intel * 600 + wil * 400) / 100. +pub fn tech_task_speed_milli(intel: Int, wil: Int) -> Int { + (intel * 600 + wil * 400) / 100 } //## 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) +// max(0.01, 0.10 + (100 - wil)/1000) * 1000 = max(10, 100 + (100 - wil)) +// = max(10, 200 - wil). +pub fn critical_failure_threshold_milli(wil: Int) -> Int { + imax(10, 200 - wil) } //## 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) +// min(0.25, 0.05 + (stat - 100)/1000) * 1000 = min(250, 50 + (stat - 100)) +// = min(250, stat - 50). +pub fn critical_success_chance_milli(stat: Int) -> Int { + imin(250, 50 + (stat - 100)) } //## CHA-scaled distraction effectiveness, CHA / 100. -pub fn distraction_effectiveness(cha: Float) -> Float { - cha / 100.0 +// cha / 100.0 * 1000 = cha * 10. +pub fn distraction_effectiveness_milli(cha: Int) -> Int { + cha * 10 } //## CHA-scaled Moletaire obedience multiplier, 0.8 + CHA/500 (>1 = more obedient). -pub fn moletaire_obedience(cha: Float) -> Float { - 0.8 + cha / 500.0 +// (0.8 + cha/500) * 1000 = 800 + cha * 2. +pub fn moletaire_obedience_milli(cha: Int) -> Int { + 800 + cha * 2 } //## 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) +// max(0.3, 1 - (con - 100)/200) * 1000 = max(300, 1000 - (con - 100) * 5). +pub fn fall_damage_resistance_milli(con: Int) -> Int { + imax(300, 1000 - (con - 100) * 5) } //## DEX-scaled lockpick speed multiplier, DEX / 100. -pub fn lockpick_speed(dex: Float) -> Float { - dex / 100.0 +// dex / 100.0 * 1000 = dex * 10. +pub fn lockpick_speed_milli(dex: Int) -> Int { + dex * 10 } //## STR-scaled melee damage multiplier, STR / 100. -pub fn melee_damage(strength: Float) -> Float { - strength / 100.0 +// str / 100.0 * 1000 = str * 10. +pub fn melee_damage_milli(strength: Int) -> Int { + strength * 10 } diff --git a/proposals/idaptik/migrated/PlayerAttributes/playerattributes.config.mjs b/proposals/idaptik/migrated/PlayerAttributes/playerattributes.config.mjs new file mode 100644 index 0000000..8470bbc --- /dev/null +++ b/proposals/idaptik/migrated/PlayerAttributes/playerattributes.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 PlayerAttributes.affine (Int-native, milli-units). +// Oracles re-derive from PlayerAttributesCoprocessor.res semantics in plain JS. +// +// Game stats (str, dex, con, int, wil, cha) cross as raw integers. +// All results are milli-units (×1000 of the original Float). +// +// Formulae (stat = raw integer, result = ×1000): +// speed_multiplier_milli(dex) = dex * 10 (dex/100 * 1000) +// max_jump_milli(str) = str * 5000 (5*str * 1000) +// jump_acceleration_milli(dex)= dex (0.1*dex * 1000) +// trajectory_divisor_milli(base_m, intel, len, dflt_m) = +// len==0 ? dflt_m : (base_m * intel) / len +// tech_task_speed_milli(intel, wil) = (intel*600 + wil*400) / 100 +// critical_failure_threshold_milli(wil) = max(10, 200 - wil) +// critical_success_chance_milli(stat) = min(250, 50 + (stat-100)) +// distraction_effectiveness_milli(cha) = cha * 10 +// moletaire_obedience_milli(cha) = 800 + cha * 2 +// fall_damage_resistance_milli(con) = max(300, 1000 - (con-100)*5) +// lockpick_speed_milli(dex) = dex * 10 +// melee_damage_milli(str) = str * 10 + +const STAT_VALUES = [0, 50, 80, 100, 120, 150, 200]; + +export default { + affine: "PlayerAttributes.affine", + compile: false, + cases: [ + { + name: "speed_multiplier_milli(dex): dex*10", + export: "speed_multiplier_milli", + args: [{ values: STAT_VALUES }], + oracle: (dex) => Math.round((dex / 100.0) * 1000), + }, + { + name: "max_jump_milli(str): str*5000", + export: "max_jump_milli", + args: [{ values: STAT_VALUES }], + oracle: (str) => Math.round(5.0 * str * 1000), + }, + { + name: "jump_acceleration_milli(dex): dex", + export: "jump_acceleration_milli", + args: [{ values: STAT_VALUES }], + oracle: (dex) => Math.round(0.1 * dex * 1000), + }, + { + name: "trajectory_divisor_milli(base_m, intel, len, dflt_m)", + export: "trajectory_divisor_milli", + args: [ + { values: [1000, 2000, 5000] }, // base_milli + { values: [80, 100, 120] }, // intel (raw int) + { values: [0, 10, 50, 100] }, // len (raw int, 0 = zero-guard) + { values: [1000] }, // dflt_milli + ], + oracle: (baseMilli, intel, len, dfltMilli) => { + if (len === 0) return dfltMilli; + // (base_milli * intel) / len -- integer division (truncate) + return Math.trunc((baseMilli * intel) / len); + }, + }, + { + name: "tech_task_speed_milli(intel, wil): (int*600+wil*400)/100", + export: "tech_task_speed_milli", + args: [ + { values: STAT_VALUES }, + { values: STAT_VALUES }, + ], + oracle: (intel, wil) => Math.trunc((intel * 600 + wil * 400) / 100), + }, + { + name: "critical_failure_threshold_milli(wil): max(10, 200-wil)", + export: "critical_failure_threshold_milli", + args: [{ values: STAT_VALUES }], + oracle: (wil) => { + const v = 0.10 + (100 - wil) / 1000.0; + return Math.round(Math.max(0.01, v) * 1000); + }, + }, + { + name: "critical_success_chance_milli(stat): min(250, stat-50)", + export: "critical_success_chance_milli", + args: [{ values: STAT_VALUES }], + oracle: (stat) => { + const v = 0.05 + (stat - 100) / 1000.0; + return Math.round(Math.min(0.25, v) * 1000); + }, + }, + { + name: "distraction_effectiveness_milli(cha): cha*10", + export: "distraction_effectiveness_milli", + args: [{ values: STAT_VALUES }], + oracle: (cha) => Math.round((cha / 100.0) * 1000), + }, + { + name: "moletaire_obedience_milli(cha): 800+cha*2", + export: "moletaire_obedience_milli", + args: [{ values: STAT_VALUES }], + oracle: (cha) => Math.round((0.8 + cha / 500.0) * 1000), + }, + { + name: "fall_damage_resistance_milli(con): max(300, 1000-(con-100)*5)", + export: "fall_damage_resistance_milli", + args: [{ values: STAT_VALUES }], + oracle: (con) => { + const v = 1.0 - (con - 100) / 200.0; + return Math.round(Math.max(0.3, v) * 1000); + }, + }, + { + name: "lockpick_speed_milli(dex): dex*10", + export: "lockpick_speed_milli", + args: [{ values: STAT_VALUES }], + oracle: (dex) => Math.round((dex / 100.0) * 1000), + }, + { + name: "melee_damage_milli(str): str*10", + export: "melee_damage_milli", + args: [{ values: STAT_VALUES }], + oracle: (str) => Math.round((str / 100.0) * 1000), + }, + ], +}; diff --git a/proposals/idaptik/migrated/QCertifications/QCertifications.affine b/proposals/idaptik/migrated/QCertifications/QCertifications.affine index 9e18975..a430c4e 100644 --- a/proposals/idaptik/migrated/QCertifications/QCertifications.affine +++ b/proposals/idaptik/migrated/QCertifications/QCertifications.affine @@ -90,21 +90,11 @@ 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 -} +//## Progress helpers (Float-param — wasm-ABI note) +// progress_total and progress_crosses cannot be expressed as wasm-exported pub fns +// in the scalar-i32 ABI: the v0.1.1 backend emits i32.ge_s for f64 comparisons, +// producing an uninstantiable wasm module (type mismatch: i32.ge_s[1] expected i32, +// found f64.const). Both helpers are therefore omitted from this wasm kernel; the +// host implements the equivalent arithmetic natively: +// progress_total = (before, amount) => before + amount +// progress_crosses = (before, amount) => (before + amount >= 1.0) ? 1 : 0 diff --git a/proposals/idaptik/migrated/QCertifications/QCertificationsBoundary.agda b/proposals/idaptik/migrated/QCertifications/QCertificationsBoundary.agda new file mode 100644 index 0000000..d6f55d2 --- /dev/null +++ b/proposals/idaptik/migrated/QCertifications/QCertificationsBoundary.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): +-- { +-- "Practitioner": 1, +-- "Professional": 2, +-- "Expert": 3, +-- "Architect": 4, +-- "Sovereign": 5 +-- } + +module QCertificationsBoundary 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 = Practitioner +-- c1 = Professional +-- c2 = Expert +-- c3 = Architect +-- c4 = Sovereign +data Host : Set where + c0 c1 c2 c3 c4 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 1 +code c1 = 2 +code c2 = 3 +code c3 = 4 +code c4 = 5 + +-- Injectivity by exhaustive case analysis. The codes are literal +-- numerals, so listing the diagonal refl clauses is enough: Agda's +-- coverage checker discharges the off-diagonal pairs as absurd +-- numeral equalities (mirrors rankCode-injective). +code-injective : Injective code +code-injective {c0} {c0} _ = refl +code-injective {c1} {c1} _ = refl +code-injective {c2} {c2} _ = refl +code-injective {c3} {c3} _ = refl +code-injective {c4} {c4} _ = refl + +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/QCertifications/qcertifications.config.mjs b/proposals/idaptik/migrated/QCertifications/qcertifications.config.mjs new file mode 100644 index 0000000..84bf795 --- /dev/null +++ b/proposals/idaptik/migrated/QCertifications/qcertifications.config.mjs @@ -0,0 +1,103 @@ +// 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 QCertifications.affine (idaptik cert-tier arithmetic; +// scalar i32 ABI). The oracle re-derives each function from the original +// QCertifications.res / QCertificationsCoprocessor.res semantics so a codegen +// regression surfaces as a differential mismatch. +// +// Source semantics (from QCertifications.res): +// tierValue: Practitioner=1 .. Sovereign=5; off-domain -> 0 +// tierColor: fixed palette per tier (0..5); off-domain -> 0 +// nextTier: 1->2, 2->3, 3->4, 4->5, 5->0, off-domain->0 +// meetsTier: tierValue(tier) >= tierValue(minTier) ? 1 : 0 +// isCyberwarUnlocked: expertCount >= 3 ? 1 : 0 +// +// progress_total and progress_crosses take Float args; the scalar-i32 ABI cannot +// sweep float inputs via parity.mjs's range expander (all inputs are i32), so +// those two exports are omitted from the parity sweep per the ABI scope note in +// parity.mjs. The Int-only exports cover all arithmetic correctness. + +// Re-derive tierValue from ReScript semantics (not from the .affine). +const tierValue = (t) => { + if (t === 1) return 1; + if (t === 2) return 2; + if (t === 3) return 3; + if (t === 4) return 4; + if (t === 5) return 5; + return 0; +}; + +// Re-derive tierColor from ReScript switch: the exact 0x-literal values from +// QCertifications.res: +// Practitioner 0x888888 = 8947848 +// Professional 0x44aaff = 4500223 +// Expert 0xffaa44 = 16755268 +// Architect 0xff4488 = 16729224 +// Sovereign 0xff0000 = 16711680 +// off-domain -> 0 +const tierColor = (t) => { + if (t === 1) return 8947848; + if (t === 2) return 4500223; + if (t === 3) return 16755268; + if (t === 4) return 16729224; + if (t === 5) return 16711680; + return 0; +}; + +// Re-derive nextTier from ReScript addProgress nextTier switch: +// Practitioner -> Professional (1->2), ..., Architect->Sovereign (4->5) +// Sovereign -> None => 0; off-domain -> 0 +const nextTier = (t) => { + if (t === 1) return 2; + if (t === 2) return 3; + if (t === 3) return 4; + if (t === 4) return 5; + return 0; // Sovereign and off-domain +}; + +// Re-derive meetsTier from ReScript countAtTier: +// tierValue(tier) >= tierValue(minTier) ? 1 : 0 +const meetsTier = (tier, minTier) => + tierValue(tier) >= tierValue(minTier) ? 1 : 0; + +// Re-derive isCyberwarUnlocked from ReScript canProgressCyberWar: +// expertCount >= 3 => true +const isCyberwarUnlocked = (expertCount) => (expertCount >= 3 ? 1 : 0); + +export default { + affine: "QCertifications.affine", + cases: [ + { + name: "tier_value over [-2..7]", + export: "tier_value", + args: [[-2, 7]], + oracle: (t) => tierValue(t), + }, + { + name: "tier_color over [-2..7]", + export: "tier_color", + args: [[-2, 7]], + oracle: (t) => tierColor(t), + }, + { + name: "next_tier over [-2..7]", + export: "next_tier", + args: [[-2, 7]], + oracle: (t) => nextTier(t), + }, + { + name: "meets_tier over tier×minTier [-1..6]×[-1..6]", + export: "meets_tier", + args: [[-1, 6], [-1, 6]], + oracle: (tier, minTier) => meetsTier(tier, minTier), + }, + { + name: "is_cyberwar_unlocked over [0..6]", + export: "is_cyberwar_unlocked", + args: [[0, 6]], + oracle: (ec) => isCyberwarUnlocked(ec), + }, + ], +}; diff --git a/proposals/idaptik/migrated/QPrograms/QPrograms.affine b/proposals/idaptik/migrated/QPrograms/QPrograms.affine index d3899eb..8732b72 100644 --- a/proposals/idaptik/migrated/QPrograms/QPrograms.affine +++ b/proposals/idaptik/migrated/QPrograms/QPrograms.affine @@ -1,30 +1,31 @@ // SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell // -// QPrograms -- the program-loadout co-processor, the pure integer/float core -// extracted from src/app/player/QPrograms.res. Per the DESIGN-VISION +// QPrograms -- the program-loadout co-processor, the pure integer core +// extracted from src/app/player/QProgramsCoprocessor.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. +// 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). +// Only 5 CameraLoop, 6 FirewallBypass, 12 SignalJam carry a timed duration; +// every other program returns base 0 from the duration kernels. // //## 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. +// Any tier outside 1..5 is off-domain and yields 0 from every duration table. // //## Background encoding (JessicaBackground.all order) // 1 Assault 2 Recon 3 Engineer 4 Signals 5 Medic 6 Logistics @@ -32,132 +33,145 @@ //## 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. +// Equipment ordinal 0 is the "no item equipped" sentinel (the ReScript None +// arm of the option); it contributes a multiplier of 1000. // -//## 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). +//## Int-native convention (MILLI-UNITS): trunc = integer division +// All Float durations cross as MILLI-UNITS (×1000 of the Float seconds value): +// 5.0s -> 5000, 10.0s -> 10000, 120.0s -> 120000. +// All multipliers cross/return as MILLI-UNITS: +// 1.0 -> 1000, 1.25 -> 1250, 1.30 -> 1300. +// +// The two trunc sites in the original kernel: +// bonus_percent: trunc((m - 1.0) * 100.0) = (m_milli - 1000) / 10 +// Integer division truncates toward zero, matching ReScript Float.toInt. +// Products of valid multipliers are non-negative so the sign is irrelevant. +// round_one_decimal: trunc(dur * 10.0) / 10.0 in milli = +// (dur_milli / 100) * 100 -- truncate to nearest 100 milli (= 0.1s). +// +// The effective_duration combine: +// base_milli * bg_milli * eq_milli / 1_000_000 +// (base up to 120000, multipliers up to 1300; product stays within i32 range +// after the first /1000 step, performed as two sequential divides below.) -//## 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 +//## Camera loop base duration (milli-units) +// cameraLoopDuration(): the Wireless-tier switch. Off-domain tiers yield 0. +pub fn camera_loop_base(tier: Int) -> Int { + if tier == 1 { return 5000; } + if tier == 2 { return 10000; } + if tier == 3 { return 20000; } + if tier == 4 { return 30000; } + if tier == 5 { return 60000; } + 0 } -//## Signal jam base duration +//## Signal jam base duration (milli-units) // 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 +pub fn signal_jam_base(tier: Int) -> Int { + if tier == 1 { return 5000; } + if tier == 2 { return 10000; } + if tier == 3 { return 15000; } + if tier == 4 { return 25000; } + if tier == 5 { return 40000; } + 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 +//## Firewall bypass base duration (milli-units) +// firewallBypassDuration(): the CyberSecurity-tier switch for bridge lifetime. +pub fn firewall_bypass_base(tier: Int) -> Int { + if tier == 1 { return 8000; } + if tier == 2 { return 15000; } + if tier == 3 { return 30000; } + if tier == 4 { return 60000; } + if tier == 5 { return 120000; } + 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 { +//## Base duration (milli-units) by program ordinal +// Dispatches the three timed programs to their tier table; every other program +// is untimed and yields 0 (the ReScript getEffectiveDuration None arm). +pub fn base_duration(program: Int, tier: Int) -> Int { 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 + 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 +//## Background synergy multiplier (milli-units) +// backgroundSynergy(): the (program, background) pair table. Returns 1250 for +// the six complementary pairs, 1000 otherwise. Pairs: +// (5 CameraLoop, 2 Recon) (9 PacketSniffer, 4 Signals) +// (10 DNSRedirect, 4 Signals) (6 FirewallBypass, 3 Engineer) +// (7 Rootkit, 3 Engineer) (11 DroneOverride, 2 Recon) +pub fn background_synergy(program: Int, bg: Int) -> Int { + if program == 5 { if bg == 2 { return 1250; } return 1000; } + if program == 9 { if bg == 4 { return 1250; } return 1000; } + if program == 10 { if bg == 4 { return 1250; } return 1000; } + if program == 6 { if bg == 3 { return 1250; } return 1000; } + if program == 7 { if bg == 3 { return 1250; } return 1000; } + if program == 11 { if bg == 2 { return 1250; } return 1000; } + 1000 } -//## 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 +//## Tech equipment synergy multiplier (milli-units) +// techEquipmentBonus(): the (program, equipment) pair table. Equipment ordinal +// 0 is the no-item sentinel and yields 1000. Pairs: +// (9 PacketSniffer, 3 SignalBooster) 1300 +// (6 FirewallBypass, 7 FibreTap) 1200 +// (4 CredentialHarvester, 1 AutorunUSB) 1150 +// (8 LogScrubber, 2 FieldTablet) 1100 +// (5 CameraLoop, 5 CameraSpotter) 1100 +pub fn equipment_bonus(program: Int, eq: Int) -> Int { + if eq == 0 { return 1000; } + if program == 9 { if eq == 3 { return 1300; } return 1000; } + if program == 6 { if eq == 7 { return 1200; } return 1000; } + if program == 4 { if eq == 1 { return 1150; } return 1000; } + if program == 8 { if eq == 2 { return 1100; } return 1000; } + if program == 5 { if eq == 5 { return 1100; } return 1000; } + 1000 } -//## 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 { +//## Effective duration (milli-units) +// base_milli * (bg_milli/1000) * (eq_milli/1000) = base * bg * eq / 1_000_000. +// Computed as two sequential divides to stay in i32 range: +// step1 = base_milli * bg_milli / 1000 +// result = step1 * eq_milli / 1000 +// Untimed programs have base 0, so the product stays 0. +pub fn effective_duration(program: Int, tier: Int, bg: Int, eq: Int) -> Int { let base = base_duration(program, tier); let bgm = background_synergy(program, bg); let eqm = equipment_bonus(program, eq); - base * bgm * eqm + let step1 = base * bgm / 1000; + step1 * eqm / 1000 } -//## 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) +//## Combined bonus multiplier (milli-units) +// bgMult * eqMult in milli: bg_milli * eq_milli / 1000. +pub fn combined_multiplier(program: Int, bg: Int, eq: Int) -> Int { + let bgm = background_synergy(program, bg); + let eqm = equipment_bonus(program, eq); + bgm * eqm / 1000 } //## 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. +// formatDurationLine's trunc((bgMult * eqMult - 1.0) * 100.0) in milli: +// (combined_milli - 1000) / 10. Integer division truncates toward zero, +// matching ReScript Float.toInt for non-negative arguments. pub fn bonus_percent(program: Int, bg: Int, eq: Int) -> Int { let m = combined_multiplier(program, bg, eq); - trunc((m - 1.0) * 100.0) + (m - 1000) / 10 } -//## 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 +//## One-decimal rounding (milli-units) +// formatDurationLine's trunc(dur * 10.0) / 10.0 in milli: +// truncate dur_milli to the nearest 100 (= 0.1s): (dur_milli / 100) * 100. +pub fn round_one_decimal(dur_milli: Int) -> Int { + (dur_milli / 100) * 100 } //## Deck capacity predicate -// loadProgram's `Array.length(deck.slots) >= maxSlots` gate, with maxSlots = 4. +// 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/QPrograms/qprograms.config.mjs b/proposals/idaptik/migrated/QPrograms/qprograms.config.mjs new file mode 100644 index 0000000..6b0deeb --- /dev/null +++ b/proposals/idaptik/migrated/QPrograms/qprograms.config.mjs @@ -0,0 +1,173 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// affine-parity config for QPrograms.affine (Int-native, milli-units). +// Oracles re-derive from QProgramsCoprocessor.res semantics in plain JS. +// +// Durations and multipliers are milli-units (×1000 of the original Float). +// Program/tier/bg/eq ordinals are raw integers (unchanged from ReScript). +// +// Encoding: +// base_duration(program, tier) -> milli-seconds (e.g. 5.0s -> 5000) +// background_synergy(program, bg) -> milli (1.25 -> 1250, 1.0 -> 1000) +// equipment_bonus(program, eq) -> milli +// combined_multiplier(program, bg, eq) -> bg_milli * eq_milli / 1000 +// effective_duration(program, tier, bg, eq) -> +// base_m * bg_m * eq_m / 1_000_000 (two sequential /1000) +// bonus_percent(program, bg, eq) -> (combined_milli - 1000) / 10 +// round_one_decimal(dur_milli) -> (dur_milli / 100) * 100 +// deck_is_full(slot_count) -> 1 if >= 4, else 0 + +// JS oracle helpers matching each ReScript function: + +function baseDurationMs(program, tier) { + const cameraLoop = { 1: 5000, 2: 10000, 3: 20000, 4: 30000, 5: 60000 }; + const firewallBypass = { 1: 8000, 2: 15000, 3: 30000, 4: 60000, 5: 120000 }; + const signalJam = { 1: 5000, 2: 10000, 3: 15000, 4: 25000, 5: 40000 }; + if (program === 5) return cameraLoop[tier] || 0; + if (program === 6) return firewallBypass[tier] || 0; + if (program === 12) return signalJam[tier] || 0; + return 0; +} + +function backgroundSynergyMilli(program, bg) { + const pairs = [[5,2],[9,4],[10,4],[6,3],[7,3],[11,2]]; + for (const [p, b] of pairs) { + if (program === p && bg === b) return 1250; + } + return 1000; +} + +function equipmentBonusMilli(program, eq) { + if (eq === 0) return 1000; + const pairs = [[9,3,1300],[6,7,1200],[4,1,1150],[8,2,1100],[5,5,1100]]; + for (const [p, e, v] of pairs) { + if (program === p && eq === e) return v; + } + return 1000; +} + +function combinedMultiplierMilli(program, bg, eq) { + return Math.trunc(backgroundSynergyMilli(program, bg) * equipmentBonusMilli(program, eq) / 1000); +} + +function effectiveDurationMilli(program, tier, bg, eq) { + const base = baseDurationMs(program, tier); + const bgm = backgroundSynergyMilli(program, bg); + const eqm = equipmentBonusMilli(program, eq); + // Match the two-step integer multiply/divide in the kernel + const step1 = Math.trunc(base * bgm / 1000); + return Math.trunc(step1 * eqm / 1000); +} + +const ALL_PROGRAMS = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]; +const TIMED_PROGRAMS = [5, 6, 12]; +const TIERS = [1, 2, 3, 4, 5]; +const BACKGROUNDS = [1, 2, 3, 4, 5, 6]; +const EQUIPMENT = [0, 1, 2, 3, 4, 5, 6, 7, 8]; + +export default { + affine: "QPrograms.affine", + compile: false, + cases: [ + { + name: "camera_loop_base(tier 0..6)", + export: "camera_loop_base", + args: [{ values: [0, 1, 2, 3, 4, 5, 6] }], + oracle: (tier) => baseDurationMs(5, tier), + }, + { + name: "signal_jam_base(tier 0..6)", + export: "signal_jam_base", + args: [{ values: [0, 1, 2, 3, 4, 5, 6] }], + oracle: (tier) => baseDurationMs(12, tier), + }, + { + name: "firewall_bypass_base(tier 0..6)", + export: "firewall_bypass_base", + args: [{ values: [0, 1, 2, 3, 4, 5, 6] }], + oracle: (tier) => baseDurationMs(6, tier), + }, + { + name: "base_duration(all programs, tiers 0..6)", + export: "base_duration", + args: [ + { values: ALL_PROGRAMS }, + { values: [0, 1, 2, 3, 4, 5, 6] }, + ], + oracle: (program, tier) => baseDurationMs(program, tier), + }, + { + name: "background_synergy(all programs, all backgrounds)", + export: "background_synergy", + args: [ + { values: ALL_PROGRAMS }, + { values: BACKGROUNDS }, + ], + oracle: (program, bg) => backgroundSynergyMilli(program, bg), + }, + { + name: "equipment_bonus(all programs, all equipment incl 0)", + export: "equipment_bonus", + args: [ + { values: ALL_PROGRAMS }, + { values: EQUIPMENT }, + ], + oracle: (program, eq) => equipmentBonusMilli(program, eq), + }, + { + name: "combined_multiplier(all programs, backgrounds, equipment)", + export: "combined_multiplier", + args: [ + { values: ALL_PROGRAMS }, + { values: BACKGROUNDS }, + { values: EQUIPMENT }, + ], + oracle: (program, bg, eq) => combinedMultiplierMilli(program, bg, eq), + }, + { + name: "effective_duration(timed programs, tiers, bg, eq)", + export: "effective_duration", + args: [ + { values: TIMED_PROGRAMS }, + { values: TIERS }, + { values: BACKGROUNDS }, + { values: EQUIPMENT }, + ], + oracle: (program, tier, bg, eq) => effectiveDurationMilli(program, tier, bg, eq), + }, + { + name: "effective_duration(untimed programs -> 0)", + export: "effective_duration", + args: [ + { values: [1, 2, 3, 4, 7, 8, 9, 10, 11] }, + { values: TIERS }, + { values: [1, 3] }, + { values: [0, 1] }, + ], + oracle: (program, tier, bg, eq) => effectiveDurationMilli(program, tier, bg, eq), + }, + { + name: "bonus_percent(all programs, bg, eq)", + export: "bonus_percent", + args: [ + { values: ALL_PROGRAMS }, + { values: BACKGROUNDS }, + { values: EQUIPMENT }, + ], + oracle: (program, bg, eq) => Math.trunc((combinedMultiplierMilli(program, bg, eq) - 1000) / 10), + }, + { + name: "round_one_decimal(dur_milli 0..130000)", + export: "round_one_decimal", + args: [{ values: [0, 99, 100, 101, 1000, 5000, 5050, 5099, 5100, 10000, 25000, 60000, 120000, 129999, 130000] }], + oracle: (durMilli) => Math.trunc(durMilli / 100) * 100, + }, + { + name: "deck_is_full(slot_count 0..6)", + export: "deck_is_full", + args: [{ values: [0, 1, 2, 3, 4, 5, 6] }], + oracle: (n) => n >= 4 ? 1 : 0, + }, + ], +}; diff --git a/proposals/idaptik/migrated/SkillAbilities/skillabilities.config.mjs b/proposals/idaptik/migrated/SkillAbilities/skillabilities.config.mjs new file mode 100644 index 0000000..723a14e --- /dev/null +++ b/proposals/idaptik/migrated/SkillAbilities/skillabilities.config.mjs @@ -0,0 +1,82 @@ +// 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 SkillAbilities.affine (idaptik ability-unlock +// decision; scalar i32 ABI). The oracle re-derives each function from the +// original SkillAbilities.res semantics so a codegen regression surfaces as a +// differential mismatch. +// +// Source semantics (from SkillAbilities.res / SkillAbilitiesCoprocessorBridge.js): +// +// rankValue: dense rank index 1..5; off-domain -> 0 (same as SkillRank's) +// +// rankMeetsRequirement(current, required): +// rankValue(current) >= rankValue(required) ? 1 : 0 +// (mirrors rankMeetsRequirement in SkillAbilities.res which uses +// JessicaBackground.rankValue on both sides) +// +// backgroundOk(abilityBg, playerBg): +// if abilityBg == 0: generic => 1 +// if playerBg == 0: player has no background => 0 (exclusive fails) +// abilityBg == playerBg ? 1 : 0 +// (mirrors the exclusiveBackground switch in isAbilityUnlocked) +// +// unlockOk(currentRank, requiredRank, abilityBg, playerBg): +// backgroundOk(abilityBg, playerBg) == 0 => 0 +// rankMeetsRequirement(currentRank, requiredRank) == 1 => 1 +// else 0 + +// Re-derive from ReScript semantics. +const rankValue = (r) => { + if (r === 1) return 1; + if (r === 2) return 2; + if (r === 3) return 3; + if (r === 4) return 4; + if (r === 5) return 5; + return 0; +}; + +const rankMeets = (current, required) => + rankValue(current) >= rankValue(required) ? 1 : 0; + +const backgroundOk = (abilityBg, playerBg) => { + if (abilityBg === 0) return 1; // generic ability + if (playerBg === 0) return 0; // player has no background => exclusive fails + return abilityBg === playerBg ? 1 : 0; +}; + +const unlockOk = (currentRank, requiredRank, abilityBg, playerBg) => { + if (backgroundOk(abilityBg, playerBg) === 0) return 0; + return rankMeets(currentRank, requiredRank); +}; + +export default { + affine: "SkillAbilities.affine", + cases: [ + { + name: "rank_value over [-2..7]", + export: "rank_value", + args: [[-2, 7]], + oracle: (r) => rankValue(r), + }, + { + name: "rank_meets over current[-1..6] × required[-1..6]", + export: "rank_meets", + args: [[-1, 6], [-1, 6]], + oracle: (cur, req) => rankMeets(cur, req), + }, + { + name: "background_ok over abilityBg[-1..4] × playerBg[-1..4]", + export: "background_ok", + args: [[-1, 4], [-1, 4]], + oracle: (ab, pb) => backgroundOk(ab, pb), + }, + { + name: "unlock_ok over currentRank[0..6]×requiredRank[0..6]×abilityBg[0..3]×playerBg[0..3]", + export: "unlock_ok", + args: [[0, 6], [0, 6], [0, 3], [0, 3]], + oracle: (cr, rr, ab, pb) => unlockOk(cr, rr, ab, pb), + }, + ], +}; diff --git a/proposals/idaptik/migrated/SkillRank/SkillRankBoundary.agda b/proposals/idaptik/migrated/SkillRank/SkillRankBoundary.agda new file mode 100644 index 0000000..0e97886 --- /dev/null +++ b/proposals/idaptik/migrated/SkillRank/SkillRankBoundary.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): +-- { +-- "Novice": 1, +-- "Trained": 2, +-- "Proficient": 3, +-- "Veteran": 4, +-- "Expert": 5 +-- } + +module SkillRankBoundary 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 = Novice +-- c1 = Trained +-- c2 = Proficient +-- c3 = Veteran +-- c4 = Expert +data Host : Set where + c0 c1 c2 c3 c4 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 1 +code c1 = 2 +code c2 = 3 +code c3 = 4 +code c4 = 5 + +-- Injectivity by exhaustive case analysis. The codes are literal +-- numerals, so listing the diagonal refl clauses is enough: Agda's +-- coverage checker discharges the off-diagonal pairs as absurd +-- numeral equalities (mirrors rankCode-injective). +code-injective : Injective code +code-injective {c0} {c0} _ = refl +code-injective {c1} {c1} _ = refl +code-injective {c2} {c2} _ = refl +code-injective {c3} {c3} _ = refl +code-injective {c4} {c4} _ = refl + +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/SkillRank/skillrank.config.mjs b/proposals/idaptik/migrated/SkillRank/skillrank.config.mjs new file mode 100644 index 0000000..135e8d2 --- /dev/null +++ b/proposals/idaptik/migrated/SkillRank/skillrank.config.mjs @@ -0,0 +1,79 @@ +// 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 SkillRank.affine (idaptik skill-rank progression; +// scalar i32 ABI). The oracle re-derives each function from the original +// JessicaBackground.res + SkillRankCoprocessor.res semantics so a codegen +// regression surfaces as a differential mismatch. +// +// Source semantics (from JessicaBackground.res rankValue / rankXpThreshold / +// can_promote contract in SkillRankBridge.js / SkillRankCoprocessor.res): +// rankValue: Novice=1 .. Expert=5; off-domain -> 0 +// xpThreshold: Novice=0, Trained=100, Proficient=350, Veteran=800, Expert=1500; off-domain->0 +// canPromote: rank in 1..4 AND xp >= xpThreshold(rank+1) ? 1 : 0 + +// Re-derive rankValue from JessicaBackground.res rankValue switch. +const rankValue = (rank) => { + 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; + return 0; +}; + +// Re-derive rankXpThreshold from JessicaBackground.res rankXpThreshold switch: +// Novice=0, Trained=100, Proficient=350, Veteran=800, Expert=1500 +const xpThreshold = (rank) => { + 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; + return 0; +}; + +// Re-derive canPromote from SkillRankBridge.js semantics and JessicaBackground +// addXp logic: a rank-up is possible iff a next rank exists (rank < 5 and +// rank >= 1) and xp meets the next rank's threshold. +const canPromote = (rank, xp) => { + if (rank < 1) return 0; + if (rank > 4) return 0; // Expert (5) or off-domain above + const next = rank + 1; + return xp >= xpThreshold(next) ? 1 : 0; +}; + +export default { + affine: "SkillRank.affine", + cases: [ + { + name: "rank_value over [-2..7]", + export: "rank_value", + args: [[-2, 7]], + oracle: (r) => rankValue(r), + }, + { + name: "xp_threshold over [-2..7]", + export: "xp_threshold", + args: [[-2, 7]], + oracle: (r) => xpThreshold(r), + }, + { + name: "can_promote over rank[-2..7] × xp[-10..1600]", + export: "can_promote", + args: [ + [-2, 7], + // Sweep key XP boundaries: just below/at/above each threshold + // (0, 99, 100, 349, 350, 799, 800, 1499, 1500, 1501) plus extremes + { + values: [ + -10, 0, 1, 99, 100, 101, 349, 350, 351, 799, 800, 801, 1499, 1500, + 1501, 2000, + ], + }, + ], + oracle: (rank, xp) => canPromote(rank, xp), + }, + ], +}; diff --git a/proposals/idaptik/migration-map.json b/proposals/idaptik/migration-map.json index 75e73ea..4cc31ca 100644 --- a/proposals/idaptik/migration-map.json +++ b/proposals/idaptik/migration-map.json @@ -219,11 +219,15 @@ "id": "C7", "name": "Player coprocessors", "description": "Player attribute, loadout, skill and ability coprocessors \u2014 pure integer player state.", - "status": "IN_PROGRESS", - "drafted_unverified": { + "status": "DONE", + "done": { "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"] + "phase": "C7 completion (scoped agents + parent re-verification)", + "staged_at": "proposals/idaptik/migrated/", + "kernels": ["CriticalRoll", "PlayerAttributes", "QCertifications", "SkillRank", "SkillAbilities", "QPrograms", "JessicaLoadout", "JessicaBackground"], + "gates": "8/8 compile; 4348/4348 parity (re-run by parent); 6 echo-boundary LOSSLESS proofs (QCertifications, SkillRank, JessicaLoadout x3, JessicaBackground; agda exit 0, re-typechecked by parent); 8/8 assail-clean", + "float_redecompositions": "CriticalRoll (min_float/max_float), PlayerAttributes (max_float/min_float), QPrograms (trunc) -> Int-native milli-unit convention; QCertifications f64-comparison pub fns removed host-side. Floats stay host-side (C6 *Int pattern). Parity caught an off-by-100 in PlayerAttributes.", + "evidence": "proposals/idaptik/migrated/EVIDENCE-C7.adoc" }, "files": [ "src/app/player/CriticalRollCoprocessor.res",