From af747e6a835fbf4f012b76472897128685b82409 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 4 Jun 2026 20:31:24 +0000 Subject: [PATCH 1/6] =?UTF-8?q?proposals(nextgen-evangelist):=20seed=20the?= =?UTF-8?q?=20evangelist=20toolkit=20=E2=80=94=205=20trialed=20components?= =?UTF-8?q?=20+=20orchestrator?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A nextgen-languages-evangelist that automates the AffineScript-migration pipeline (triage -> weak-points -> boundary-proof -> parity), composing five components, each trialed host-native this session: - echo-boundary (#1/#2): encoding table -> lossless/controlled-loss verdict + GENERATED, agda-typechecked EchoEncodingFaithfulness proof (exit 0). - affine-parity (#2/#3): generic differential-parity runner; SecurityRank 78/78, Kernel_IO main()=6. - affine-migratability (#4): .res triage; reproduces Compute=MIGRATABLE, IO=STRING-GATED, Quantum=EFFECT-GATED. - affine-assail (#5): .affine weak-point scanner; flags SecurityRank's clamp (PA-AFF-001) at HIGH. Reference impl for the panic-attack gap. - deno-esm-spike (#3): proves the .affine -> Deno-ESM TypeScript-0 path WORKS (5/5 driver checks, zero TS). - evangelist: orchestrator; emits one readiness report (verified end-to-end). Trial components are Deno (runnable now under the github-only firewall; hypatia-allow pragma'd); production target is Rust/AffineScript per policy. https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --- proposals/nextgen-evangelist/README.adoc | 148 ++++++ .../affine-assail/README.adoc | 197 ++++++++ .../affine-assail/assail.mjs | 349 +++++++++++++ .../affine-assail/fixtures/weakpoints.affine | 45 ++ .../affine-migratability/README.adoc | 235 +++++++++ .../affine-migratability/migratability.mjs | 348 +++++++++++++ .../affine-parity/README.adoc | 199 ++++++++ .../affine-parity/SecurityRank.affine | 63 +++ .../affine-parity/kernel_io.config.mjs | 32 ++ .../affine-parity/parity.mjs | 263 ++++++++++ .../affine-parity/securityrank.config.mjs | 43 ++ .../deno-esm-spike/README.adoc | 161 ++++++ .../deno-esm-spike/driver.mjs | 40 ++ .../deno-esm-spike/sample.affine | 28 ++ .../deno-esm-spike/sample.js | 463 +++++++++++++++++ .../echo-boundary/README.adoc | 203 ++++++++ .../echo-boundary/boundary.mjs | 468 ++++++++++++++++++ .../samples/BoundaryControlledLoss.agda | 83 ++++ .../samples/BoundaryLossless.agda | 72 +++ .../nextgen-evangelist/evangelist/README.adoc | 62 +++ .../evangelist/evangelist.mjs | 144 ++++++ 21 files changed, 3646 insertions(+) create mode 100644 proposals/nextgen-evangelist/README.adoc create mode 100644 proposals/nextgen-evangelist/affine-assail/README.adoc create mode 100644 proposals/nextgen-evangelist/affine-assail/assail.mjs create mode 100644 proposals/nextgen-evangelist/affine-assail/fixtures/weakpoints.affine create mode 100644 proposals/nextgen-evangelist/affine-migratability/README.adoc create mode 100644 proposals/nextgen-evangelist/affine-migratability/migratability.mjs create mode 100644 proposals/nextgen-evangelist/affine-parity/README.adoc create mode 100644 proposals/nextgen-evangelist/affine-parity/SecurityRank.affine create mode 100644 proposals/nextgen-evangelist/affine-parity/kernel_io.config.mjs create mode 100644 proposals/nextgen-evangelist/affine-parity/parity.mjs create mode 100644 proposals/nextgen-evangelist/affine-parity/securityrank.config.mjs create mode 100644 proposals/nextgen-evangelist/deno-esm-spike/README.adoc create mode 100644 proposals/nextgen-evangelist/deno-esm-spike/driver.mjs create mode 100644 proposals/nextgen-evangelist/deno-esm-spike/sample.affine create mode 100644 proposals/nextgen-evangelist/deno-esm-spike/sample.js create mode 100644 proposals/nextgen-evangelist/echo-boundary/README.adoc create mode 100644 proposals/nextgen-evangelist/echo-boundary/boundary.mjs create mode 100644 proposals/nextgen-evangelist/echo-boundary/samples/BoundaryControlledLoss.agda create mode 100644 proposals/nextgen-evangelist/echo-boundary/samples/BoundaryLossless.agda create mode 100644 proposals/nextgen-evangelist/evangelist/README.adoc create mode 100644 proposals/nextgen-evangelist/evangelist/evangelist.mjs diff --git a/proposals/nextgen-evangelist/README.adoc b/proposals/nextgen-evangelist/README.adoc new file mode 100644 index 00000000..460b03f2 --- /dev/null +++ b/proposals/nextgen-evangelist/README.adoc @@ -0,0 +1,148 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += nextgen-languages-evangelist — component seed (trialed here) +:toc: macro + +[IMPORTANT] +==== +*Status: SEED / PROPOSAL — all six pieces built and trialed end-to-end this +session.* A *nextgen-languages-evangelist* is a toolkit that automates the +AffineScript-migration pipeline this session ran by hand. Every component +here was *run and verified in this environment* (evidence captured below +and in each subdir) against the real github-only network policy. Staged in +the affinescript repo for review; eventual home is a dedicated evangelist +repo (or under `hyperpolymath/nextgen-languages`). + +*Two decisions flagged for the owner* (defaulted, not blocking): (1) the +trial components are **Deno** scripts so they run immediately under the +firewall — the *production* CLI should be **Rust or AffineScript** per +estate policy; (2) the eventual **home repo** is the owner's call. +==== + +toc::[] + +== What an "evangelist" is + +A tool (and ultimately an agent) that *finds, validates, demonstrates, and +advances* next-gen-language adoption across the estate. It automates the +pipeline a human/agent otherwise runs by hand for every kernel: + +---- +.res kernel + │ ① triage (migratable now? gated on which compiler wall?) + ▼ +re-decomposed .affine + │ ② weak-points (silent clamps? unguarded decoders? unbounded scans?) + │ ③ boundary-proof (is the host->int encoding lossless, or a declared clamp?) + │ ④ parity (does the wasm match an independent oracle?) + ▼ +guide-linked readiness report +---- + +== Component map (each maps to a roadmap ask 1-5) — all TRIALED + +[cols="1,1,3,2",options="header"] +|=== +| Component | Ask | What it does | Trial result (this session) + +| `echo-boundary/` +| #1 #2 +| Reads an encoding table, decides lossless (injective) vs controlled + loss (clamp/collision), GENERATES the matching `EchoEncodingFaithfulness` + Agda instance, and typechecks it. The `@boundary` obligation as a + runnable, machine-checked check. +| ✅ `{Open:0..Strong:3}` -> *LOSSLESS*; `+{OOB:0}` -> *CONTROLLED LOSS*; both generated modules **agda exit 0** (`--safe --without-K`). + +| `affine-parity/` +| #2 #3 +| Config-driven differential-parity runner: compile `.affine` host-native, + instantiate the wasm, sweep exported `pub fn`s against an independent + oracle, report N/N (scalar i32 ABI). +| ✅ SecurityRank **78/78 pass**; Kernel_IO `main()` **= 6**; wrong-oracle negative check exits 1. + +| `affine-migratability/` +| #4 +| Scans a `.res` kernel for the two compiler walls + re-decomposition + signals; verdict MIGRATABLE NOW / STRING-GATED / EFFECT-GATED. +| ✅ Reproduced the triage 3/3: Compute=MIGRATABLE, IO=STRING-GATED, Quantum=EFFECT-GATED. + +| `affine-assail/` +| #5 +| Weak-point scanner for `.affine` (PA-AFF-001 undeclared clamp-sentinel, + PA-AFF-002 unguarded boundary decoder, PA-AFF-003 unbounded scan) — the + reference impl for the panic-attack gap (Finding 7). +| ✅ Flags SecurityRank's `Invalid(v) => …{0}else{3}` clamp at HIGH (exit 1); Kernel_IO decoder + scans, no false positives on in-band arms. + +| `deno-esm-spike/` +| #3 +| Compiles a `.affine` with `--deno-esm` and runs it under Deno — proving + the TypeScript-0 harness path. +| ✅ **WORKS** — real ESM named exports (`export function add…`), 5/5 driver checks, zero TS. Caveat: ~440-line host-shim prelude; struct/`extern fn` lowering not yet trialed. + +| `evangelist/` +| all +| Orchestrator: walks a tree, runs ①+② automatically and ③+④ via a + manifest, emits one readiness report. +| ✅ End-to-end on the demo target (report below). +|=== + +== Verified end-to-end (the orchestrator output) + +`deno run -A evangelist/evangelist.mjs /tmp/evangelist-demo manifest.json` +(demo target = the three idaptik kernels + `SecurityRank.affine` + +`Kernel_IO.affine`) produced: + +---- +# Next-gen readiness report +Target: /tmp/evangelist-demo | 3 .res, 2 .affine + +① ReScript migratability (.res) + Kernel_Quantum.res | EFFECT-GATED + Kernel_IO.res | STRING-GATED + Kernel_Compute.res | MIGRATABLE NOW + +② AffineScript weak points (.affine) + Kernel_IO.affine | 5 — PA-AFF-003, PA-AFF-002 + SecurityRank.affine | 1 — PA-AFF-001 + +③ Boundary faithfulness proofs (echo-boundary) + SecurityRank | LOSSLESS (generated Agda, exit 0) + +④ Differential parity (affine-parity) + SecurityRank | 78/78 pass +---- + +== The consistency the toolkit surfaces + +`affine-assail` flags SecurityRank's clamp (PA-AFF-001), while +`echo-boundary` reports the in-band table `{Open:0..Strong:3}` as LOSSLESS +*and* the same table **with** the clamp (`+{OOB:0}`) as CONTROLLED LOSS. +That is not a contradiction — it is the whole point: the toolkit *flags* +the undeclared clamp and *lets you discharge it*, either by certifying the +lossless band or by declaring the controlled loss (the `@boundary` +obligation from `proposals/toolchain/` Finding 2). Flag -> certify, in one +pipeline. + +== Trial-here principle + +No component is "done" until it *runs and is verified in this environment*. +Each subdir captures the exact command + output that proves it works, +against the same github-only firewall the estate CI runs under (agda, the +host-native `affinescript` binary, deno — no registries). + +== What's next (production) + +* Re-author the orchestrator + tools as a Rust or AffineScript CLI (policy). +* JSON/SARIF output for CI; a real manifest schema; `groove`-style kernel + auto-discovery instead of a directory walk. +* Trial `--deno-esm` struct->`export class` + `extern fn` lowering before + parity harnesses are migrated off TypeScript wholesale. +* Promote `affine-assail`'s rules into a real panic-attack AffineScript + analyzer (closes Finding 7). + +== Provenance + +Seeded in the 2026-06-04 AffineScript co-development session, extending the +verified migration + proof + guide work (PRs #531, #532) toward a reusable +evangelist toolkit. Built by a five-agent fan-out + an orchestrator; +every component trialed here. diff --git a/proposals/nextgen-evangelist/affine-assail/README.adoc b/proposals/nextgen-evangelist/affine-assail/README.adoc new file mode 100644 index 00000000..9ec4a2b2 --- /dev/null +++ b/proposals/nextgen-evangelist/affine-assail/README.adoc @@ -0,0 +1,197 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += affine-assail — a weak-point scanner for AffineScript (.affine) +:toc: macro + +[IMPORTANT] +==== +*Status: REFERENCE IMPL / PROPOSAL — TRIALED, GREEN.* This directory is the +*working reference implementation* for the *panic-attack AffineScript gap*: +panic-attack scans 49 languages but not `.affine`. nextgen-languages-evangelist +roadmap ask #5. + +It is a *Deno* trial script (plain JavaScript `.mjs`, NOT TypeScript) so it +runs immediately under the firewall. The *production* analyzer should be the +Rust pass inside `panic-attack` (`src/assail/`), learning the three rules this +script demonstrates against real migrated kernels. +==== + +toc::[] + +== What it flags + +Three `.affine`-specific weak points, each with a stable rule id paralleling +panic-attack's `PA0xx` codes: + +[cols="1,2,1,4"] +|=== +| Rule | Name | Severity | What it catches + +| `PA-AFF-001` +| undeclared clamp-sentinel *(the key rule)* +| high +| A `match` arm or `if/else` mapping a catch-all / out-of-band / `Invalid` + case to a *literal integer* in-band code (`Invalid(v) => if v < 0 { 0 } else + { 3 }`, or `_ => 0`). These collapse out-of-band input onto an in-band code. + +| `PA-AFF-002` +| unguarded boundary decoder +| medium / low +| A `pub fn` whose params include `[Int]`/`Int` and whose body indexes/scans + (`nth(`, subscript, `get(`) — a boundary decoder. *Medium* by default; + *lowered to low* when a length/bounds guard is detected in the body + (heuristic). + +| `PA-AFF-003` +| unbounded scan +| info +| `for in ` over an array-typed parameter. Informational/perf: O(n) + over caller-supplied length; reviewer confirms n is bounded. +|=== + +The PA-AFF-001 message points the author at the sibling `echo-boundary/` +proposal: _"out-of-band collapses to in-band code N; declare a clamp or prove +injective via echo-boundary."_ + +== Design notes (honest) + +* *Line-oriented heuristic, no full parse.* A tool in the panic-attack family + must run standalone on partial / non-compiling sources, exactly like its + other 49 analyzers. This scanner therefore matches *shapes*, not a typed AST. + The migrated kernels write flat single-line arms (per the AffineScript + "flat guarded returns" style the parser prefers), which suits this approach. +* *Trailing `//` comments are stripped* before matching, so comment prose never + triggers a rule. Block comments don't exist in the canonical face; `//` + inside a string literal is an accepted known limitation. +* *Guarded vs unguarded* (PA-AFF-002) is a genuine heuristic: presence of a + `len`/`length`/`array_len`/`path_len` token or an `if ... < / <= / > / >= / + ==` comparison in the body lowers severity. It does NOT prove the guard + covers *every* index — the message says so. +* *Exit code:* 1 if any *high*-severity finding (CI-gate friendly), else 0. + +== Usage + +---- +deno run --allow-read assail.mjs # human + JSON summary +deno run --allow-read assail.mjs --json # JSON object only +---- + +== Trial 1 — SecurityRank.affine (MUST flag the clamp) — PASS + +Target: `/home/user/idaptik/vm/coprocessor/SecurityRank.affine`. The +load-bearing line is 48: `Invalid(v) => { if v < 0 { 0 } else { 3 } }`. + +---- +$ deno run --allow-read assail.mjs /home/user/idaptik/vm/coprocessor/SecurityRank.affine +affine-assail: scanning /home/user/idaptik/vm/coprocessor/SecurityRank.affine + + [HIGH] PA-AFF-001 /home/user/idaptik/vm/coprocessor/SecurityRank.affine:48 + Invalid(v) => { if v < 0 { 0 } else { 3 } } + -> out-of-band collapses to in-band code 0; declare a clamp or prove injective via echo-boundary (proposals/nextgen-evangelist/echo-boundary). + + 1 finding(s): 1 high. + +JSON summary: +{"file":"/home/user/idaptik/vm/coprocessor/SecurityRank.affine","findings":[{"rule":"PA-AFF-001","severity":"high","line":48,"snippet":"Invalid(v) => { if v < 0 { 0 } else { 3 } }","detail":"out-of-band collapses to in-band code 0; declare a clamp or prove injective via echo-boundary (proposals/nextgen-evangelist/echo-boundary)."}]} +exit=1 +---- + +*Result: the required clamp-sentinel is flagged HIGH at line 48.* Note the +*absence* of false positives: `rank_of`'s in-band arms (`Open => 0`, `Weak => +1`, …) and `level_of`'s `if level == N { return Variant }` guarded returns are +correctly NOT flagged — only the out-of-band `Invalid(v) =>` arm fires. The two +`pub fn`s (`rank_security_level`, `passes_min_security`) take `Int` but call +`rank_of`/`level_of` rather than indexing, so PA-AFF-002 correctly stays quiet. + +== Trial 2 — Kernel_IO.affine (the in_sandbox decoder + scans) — PASS + +Target: `/tmp/idaptik-migration/Kernel_IO.affine`. + +---- +$ deno run --allow-read assail.mjs /tmp/idaptik-migration/Kernel_IO.affine +affine-assail: scanning /tmp/idaptik-migration/Kernel_IO.affine + + [INFO] PA-AFF-003 /tmp/idaptik-migration/Kernel_IO.affine:34 + for x in xs { n = n + 1; } + -> scans array parameter 'xs' — O(n) over caller-supplied length; confirm n is bounded. + + [INFO] PA-AFF-003 /tmp/idaptik-migration/Kernel_IO.affine:45 + for b in data { + -> scans array parameter 'data' — O(n) over caller-supplied length; confirm n is bounded. + + [INFO] PA-AFF-003 /tmp/idaptik-migration/Kernel_IO.affine:59 + for x in xs { + -> scans array parameter 'xs' — O(n) over caller-supplied length; confirm n is bounded. + + [INFO] PA-AFF-003 /tmp/idaptik-migration/Kernel_IO.affine:71 + for r in root { + -> scans array parameter 'root' — O(n) over caller-supplied length; confirm n is bounded. + + [LOW] PA-AFF-002 /tmp/idaptik-migration/Kernel_IO.affine:82 + pub fn in_sandbox(data: [Int], root: [Int]) -> Int { + -> pub fn 'in_sandbox' decodes numeric boundary input and indexes/scans (a length/bounds guard was detected; severity lowered to low — confirm it covers every index). + + 5 finding(s): 1 low, 4 info. +---- +(exit=0 — no high-severity finding) + +*Result: the `in_sandbox` boundary decoder is flagged (PA-AFF-002, lowered to +LOW because the body has guards: `if pl < rl`, `if pl == rl`), and all four +array-parameter scans are flagged informational (PA-AFF-003).* This is the +honest verdict — `in_sandbox` genuinely does bounds-guard its `nth(data, rl)` +read, so LOW is correct, but it is still surfaced so a reviewer can confirm the +guard covers every index. + +== Trial 3 — synthetic fixture (the shapes the real kernels don't cover) — PASS + +`fixtures/weakpoints.affine` is a hand-written fixture exercising the wildcard +`_ => N` arm, the brace-less `Invalid(v) => N` arm, and a *genuinely +unguarded* decoder (to show PA-AFF-002 at MEDIUM, contrasting Kernel_IO's LOW). + +---- +$ deno run --allow-read assail.mjs fixtures/weakpoints.affine +affine-assail: scanning fixtures/weakpoints.affine + + [HIGH] PA-AFF-001 fixtures/weakpoints.affine:17 + _ => 0 + -> out-of-band collapses to in-band code 0; declare a clamp or prove injective via echo-boundary (proposals/nextgen-evangelist/echo-boundary). + + [HIGH] PA-AFF-001 fixtures/weakpoints.affine:26 + Invalid(v) => 3 + -> out-of-band collapses to in-band code 3; declare a clamp or prove injective via echo-boundary (proposals/nextgen-evangelist/echo-boundary). + + [MEDIUM] PA-AFF-002 fixtures/weakpoints.affine:33 + pub fn first_byte(data: [Int]) -> Int { + -> pub fn 'first_byte' decodes numeric boundary input and indexes/scans with NO obvious length/bounds guard; a malformed [Int]/Int can read out of range. + + [INFO] PA-AFF-003 fixtures/weakpoints.affine:40 + for x in xs { + -> scans array parameter 'xs' — O(n) over caller-supplied length; confirm n is bounded. + + 4 finding(s): 2 high, 1 medium, 1 info. +---- +(exit=1 — two high-severity findings) + +*Result: both clamp-sentinel shapes flag HIGH; the unguarded `first_byte` +decoder flags MEDIUM (vs Kernel_IO's guarded LOW), confirming the +guarded/unguarded heuristic discriminates as intended.* + +== Files + +[cols="1,3"] +|=== +| `assail.mjs` | The scanner (Deno, plain JavaScript). +| `fixtures/weakpoints.affine` | Synthetic fixture covering shapes the two real kernels don't. +|=== + +== Hand-off to panic-attack (production) + +The Rust port in `panic-attack` (`src/assail/analyzer.rs` + +`src/assail/patterns.rs`) should add an AffineScript analyzer with these three +patterns. PA-AFF-001 is the novel, high-value one — it is the type-system-aware +analogue of panic-attack's existing `InputBoundary` (PA024) / `MutationGap` +(PA025) family, specialised to the AffineScript "out-of-band variant collapses +to an in-band integer" idiom that the ReScript->AffineScript migration produces +when a variant is re-decomposed onto a closed integer band. The fix the message +recommends — a *declared clamp* or an *injectivity proof via `echo-boundary`* — +ties the finding to the sibling proposal. diff --git a/proposals/nextgen-evangelist/affine-assail/assail.mjs b/proposals/nextgen-evangelist/affine-assail/assail.mjs new file mode 100644 index 00000000..fd245618 --- /dev/null +++ b/proposals/nextgen-evangelist/affine-assail/assail.mjs @@ -0,0 +1,349 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// assail.mjs -- a weak-point scanner for AffineScript (.affine) source. +// +// This is the *working reference implementation* for the panic-attack +// AffineScript gap (panic-attack scans 49 languages but not .affine). +// nextgen-languages-evangelist roadmap ask #5. It demonstrates, against real +// migrated kernels, the three .affine-specific weak points the production +// Rust analyzer should learn: +// +// PA-AFF-001 undeclared clamp-sentinel (high) -- the key rule +// PA-AFF-002 unguarded boundary decoder (low/med) -- heuristic +// PA-AFF-003 unbounded scan (info) -- perf/informational +// +// It is deliberately a line-oriented heuristic scanner (no full AffineScript +// parse): a tool in this family must run standalone, including on partial / +// non-compiling sources, exactly like panic-attack's other 49 analyzers. +// +// Usage: +// deno run --allow-read assail.mjs [--json] +// +// Output: human-readable findings, then a JSON summary +// { file, findings: [ { rule, severity, line, snippet } ] } +// (with --json, ONLY the JSON object is printed, for pipeline integration.) + +// --------------------------------------------------------------------------- +// Rule catalogue +// --------------------------------------------------------------------------- + +const RULES = { + CLAMP_SENTINEL: { + id: "PA-AFF-001", + name: "undeclared-clamp-sentinel", + severity: "high", + }, + BOUNDARY_DECODER: { + id: "PA-AFF-002", + name: "unguarded-boundary-decoder", + severity: "medium", // lowered to "low" when guards are detected + }, + UNBOUNDED_SCAN: { + id: "PA-AFF-003", + name: "unbounded-scan", + severity: "info", + }, +}; + +const ECHO_BOUNDARY_HINT = + "out-of-band collapses to in-band code N; declare a clamp or prove " + + "injective via echo-boundary (proposals/nextgen-evangelist/echo-boundary)."; + +// --------------------------------------------------------------------------- +// Lightweight source helpers +// --------------------------------------------------------------------------- + +// Strip a trailing line comment (// ...) so comment text never triggers a +// rule. We do NOT strip block comments (AffineScript canonical face has none); +// `//` inside a string literal is rare in these integer kernels, accepted as +// a known heuristic limitation. +function stripLineComment(line) { + const idx = line.indexOf("//"); + return idx === -1 ? line : line.slice(0, idx); +} + +function trimSnippet(line) { + return line.trim(); +} + +// Does a string contain a bare integer literal as a "result" token? Matches a +// standalone integer (optionally negative) that is the value of an arm/branch, +// e.g. `=> 0`, `{ 0 }`, `else { 3 }`, `return 3;`. Returns the literal text or +// null. +function extractIntResult(text) { + // Common result positions: after `=>`, inside `{ N }`, after `return`, + // after `else`/`then`. Capture the first standalone integer. + const patterns = [ + /=>\s*(-?\d+)\b/, // match arm: Invalid(v) => 0 + /\breturn\s+(-?\d+)\b/, // return 0 + /\{\s*(-?\d+)\s*\}/, // braces: { 0 } + /\belse\s+(-?\d+)\b/, // else 0 (brace-less) + /\bthen\s+(-?\d+)\b/, // then 0 (pseudocode-ish) + ]; + for (const re of patterns) { + const m = text.match(re); + if (m) return m[1]; + } + return null; +} + +// Catch-all / out-of-band arm heads we care about. `_` is the wildcard; +// `Invalid`, `Unknown`, `Other`, `Err`, `None` are the conventional +// out-of-band / sentinel constructor names seen across the migrated kernels. +const OUT_OF_BAND_HEAD = + /(^|[\s|(])(_|Invalid|Unknown|Other|OutOfBand|Err|None|Default)\b/; + +// An array-typed parameter list mention: `[Int]`, `[Float]`, `[Byte]` etc. +const ARRAY_PARAM = /\[\s*(Int|Float|Byte|Bool|Char|String)\s*\]/; +// A scalar Int/Float param. +const SCALAR_NUM_PARAM = /\b(a|b|x|y|z|i|j|k|n|m|level|threshold|idx|index)\s*:\s*(Int|Float)\b/; + +// Indexing / scanning operations in a body. +const INDEX_OP = /\bnth\s*\(|\bget\s*\(|\bindex\s*\(|\[\s*[A-Za-z_][A-Za-z0-9_]*\s*\]|\.\s*at\s*\(/; + +// A bounds/length guard somewhere in a function body. +const GUARD = + /\b(len|length|array_len|path_len|count|size)\b|\bif\b[^/\n]*\b(<|<=|>|>=|==)\b/; + +// --------------------------------------------------------------------------- +// Rule: PA-AFF-001 undeclared clamp-sentinel +// --------------------------------------------------------------------------- +// Flags a `match` arm OR an `if/else` that maps a catch-all / out-of-band / +// Invalid case to a *literal integer* in-band code. These collapse out-of-band +// input onto an in-band code without a declared clamp or an injectivity proof. +// +// Two shapes, both on a single line (the migrated kernels write flat arms): +// (a) match arm: Invalid(v) => { if v < 0 { 0 } else { 3 } } +// _ => 0 +// (b) brace-less: Invalid(v) => 3 +function scanClampSentinel(lines) { + const findings = []; + for (let i = 0; i < lines.length; i++) { + const raw = lines[i]; + const code = stripLineComment(raw); + if (!code.trim()) continue; + + // Must look like a match arm or a guarded mapping: needs `=>` (arm) and an + // out-of-band head before it. + const armIdx = code.indexOf("=>"); + if (armIdx === -1) continue; + + const head = code.slice(0, armIdx); + if (!OUT_OF_BAND_HEAD.test(head)) continue; + + const body = code.slice(armIdx); + const lit = extractIntResult(body); + if (lit === null) continue; + + findings.push({ + rule: RULES.CLAMP_SENTINEL.id, + severity: RULES.CLAMP_SENTINEL.severity, + line: i + 1, + snippet: trimSnippet(raw), + detail: ECHO_BOUNDARY_HINT.replace("N", lit), + }); + } + return findings; +} + +// --------------------------------------------------------------------------- +// Rule: PA-AFF-002 unguarded boundary decoder +// --------------------------------------------------------------------------- +// A `pub fn` whose params include `[Int]`/`Int` and whose body indexes/scans +// (nth(, subscript, get(...)) — a boundary decoder. Severity medium; lowered to +// low when a length/bounds guard is detected in the same body. (Heuristic.) +function scanBoundaryDecoder(lines) { + const findings = []; + for (let i = 0; i < lines.length; i++) { + const code = stripLineComment(lines[i]); + const m = code.match(/\bpub\s+fn\s+([A-Za-z_][A-Za-z0-9_]*)\s*\(([^)]*)\)/); + if (!m) continue; + + const params = m[2]; + const takesNumericInput = + ARRAY_PARAM.test(params) || SCALAR_NUM_PARAM.test(params) || /:\s*Int\b/.test(params); + if (!takesNumericInput) continue; + + // Gather the function body: from this line to the matching end of the + // brace block (best-effort brace counting starting at the `{`). + const { bodyText, endLine } = collectBody(lines, i); + if (!INDEX_OP.test(bodyText)) continue; + + const hasGuard = GUARD.test(bodyText); + findings.push({ + rule: RULES.BOUNDARY_DECODER.id, + severity: hasGuard ? "low" : "medium", + line: i + 1, + snippet: trimSnippet(lines[i]), + detail: + `pub fn '${m[1]}' decodes numeric boundary input and indexes/scans` + + (hasGuard + ? " (a length/bounds guard was detected; severity lowered to low — confirm it covers every index)." + : " with NO obvious length/bounds guard; a malformed [Int]/Int can read out of range."), + }); + // Skip ahead past the body to avoid re-matching nested `pub fn` (there are + // none nested in practice, but keep the scan O(n)). + i = Math.max(i, endLine - 1); + } + return findings; +} + +// Collect a brace-delimited body starting at the line containing the fn's +// opening `{`. Returns the concatenated body text and the (1-based-exclusive) +// end line index. Falls back to a 30-line window if braces don't balance. +function collectBody(lines, startLine) { + let depth = 0; + let started = false; + const parts = []; + let end = startLine; + for (let j = startLine; j < lines.length && j < startLine + 200; j++) { + const code = stripLineComment(lines[j]); + parts.push(code); + for (const ch of code) { + if (ch === "{") { + depth += 1; + started = true; + } else if (ch === "}") { + depth -= 1; + } + } + end = j + 1; + if (started && depth <= 0) break; + } + return { bodyText: parts.join("\n"), endLine: end }; +} + +// --------------------------------------------------------------------------- +// Rule: PA-AFF-003 unbounded scan +// --------------------------------------------------------------------------- +// `for in ` loops over an array-typed parameter. Informational/perf: +// in pure-integer kernels these are O(n) passes; flagged so a reviewer can +// confirm n is bounded (e.g. fixed-length protocol payloads) rather than +// attacker-controlled unboundedly. +function scanUnboundedScan(lines) { + const findings = []; + + // First, collect array-typed parameter names from all fn signatures so we can + // tell "loops over a param" from "loops over a local". + const arrayParams = new Set(); + for (const line of lines) { + const code = stripLineComment(line); + const sig = code.match(/\bfn\s+[A-Za-z_][A-Za-z0-9_]*\s*\(([^)]*)\)/); + if (!sig) continue; + // Each param is `name: Type`; keep those with an array type. + for (const part of sig[1].split(",")) { + const pm = part.match(/([A-Za-z_][A-Za-z0-9_]*)\s*:\s*(\[[^\]]*\])/); + if (pm) arrayParams.add(pm[1]); + } + } + + for (let i = 0; i < lines.length; i++) { + const code = stripLineComment(lines[i]); + const fm = code.match(/\bfor\s+[A-Za-z_][A-Za-z0-9_]*\s+in\s+([A-Za-z_][A-Za-z0-9_]*)\b/); + if (!fm) continue; + const coll = fm[1]; + const overParam = arrayParams.has(coll); + findings.push({ + rule: RULES.UNBOUNDED_SCAN.id, + severity: RULES.UNBOUNDED_SCAN.severity, + line: i + 1, + snippet: trimSnippet(lines[i]), + detail: overParam + ? `scans array parameter '${coll}' — O(n) over caller-supplied length; confirm n is bounded.` + : `scans '${coll}' — O(n) loop; informational.`, + }); + } + return findings; +} + +// --------------------------------------------------------------------------- +// Driver +// --------------------------------------------------------------------------- + +function analyze(source) { + const lines = source.split("\n"); + const findings = [ + ...scanClampSentinel(lines), + ...scanBoundaryDecoder(lines), + ...scanUnboundedScan(lines), + ]; + // Stable order: by line, then by rule id. + findings.sort((a, b) => a.line - b.line || a.rule.localeCompare(b.rule)); + return findings; +} + +const SEVERITY_RANK = { high: 0, medium: 1, low: 2, info: 3 }; + +function printHuman(file, findings) { + console.log(`affine-assail: scanning ${file}`); + console.log(""); + if (findings.length === 0) { + console.log(" no weak points found."); + } else { + for (const f of findings) { + console.log(` [${f.severity.toUpperCase()}] ${f.rule} ${file}:${f.line}`); + console.log(` ${f.snippet}`); + console.log(` -> ${f.detail}`); + console.log(""); + } + } + // Tally by severity. + const tally = {}; + for (const f of findings) tally[f.severity] = (tally[f.severity] || 0) + 1; + const order = Object.keys(tally).sort( + (a, b) => SEVERITY_RANK[a] - SEVERITY_RANK[b], + ); + const summary = order.map((s) => `${tally[s]} ${s}`).join(", "); + console.log(` ${findings.length} finding(s)${summary ? ": " + summary : ""}.`); + console.log(""); +} + +function main() { + const args = Deno.args.slice(); + const jsonOnly = args.includes("--json"); + const positional = args.filter((a) => !a.startsWith("--")); + + if (positional.length !== 1) { + console.error("usage: deno run --allow-read assail.mjs [--json]"); + Deno.exit(2); + } + + const file = positional[0]; + let source; + try { + source = Deno.readTextFileSync(file); + } catch (e) { + console.error(`affine-assail: cannot read ${file}: ${e.message}`); + Deno.exit(2); + } + + // The JSON summary: drop the human-only `detail` field's verbosity? No — + // keep `detail` too; it is useful for pipeline consumers. The spec's minimal + // shape is {rule, severity, line, snippet}; we include those plus detail. + const findings = analyze(source); + const jsonSummary = { + file, + findings: findings.map((f) => ({ + rule: f.rule, + severity: f.severity, + line: f.line, + snippet: f.snippet, + detail: f.detail, + })), + }; + + if (jsonOnly) { + console.log(JSON.stringify(jsonSummary, null, 2)); + } else { + printHuman(file, findings); + console.log("JSON summary:"); + console.log(JSON.stringify(jsonSummary)); + } + + // Exit code: 1 if any high-severity finding, else 0 (CI-gate friendly). + const anyHigh = findings.some((f) => f.severity === "high"); + Deno.exit(anyHigh ? 1 : 0); +} + +main(); diff --git a/proposals/nextgen-evangelist/affine-assail/fixtures/weakpoints.affine b/proposals/nextgen-evangelist/affine-assail/fixtures/weakpoints.affine new file mode 100644 index 00000000..f738fc11 --- /dev/null +++ b/proposals/nextgen-evangelist/affine-assail/fixtures/weakpoints.affine @@ -0,0 +1,45 @@ +// SPDX-License-Identifier: MPL-2.0 +// +// weakpoints.affine -- a SYNTHETIC fixture (not migrated source) exercising +// the shapes the two real kernels don't cover, so affine-assail's full reach +// is demonstrated honestly in one place: +// - a wildcard `_ => N` clamp-sentinel arm, +// - a brace-less `Invalid(v) => N` clamp-sentinel arm, +// - a genuinely UNGUARDED boundary decoder (severity medium, no length check). + +enum Tag { A, B, Invalid(Int) } + +// Wildcard catch-all collapsing to an in-band literal: PA-AFF-001. +fn classify(t: Int) -> Int { + match t { + 0 => 1, + 1 => 2, + _ => 0 + } +} + +// Brace-less out-of-band arm collapsing to a literal: PA-AFF-001. +fn rank(tag: Tag) -> Int { + match tag { + A => 0, + B => 1, + Invalid(v) => 3 + } +} + +// Unguarded boundary decoder: pub fn over [Int], indexes via nth(, NO length +// guard anywhere -> PA-AFF-002 at MEDIUM. (Contrast Kernel_IO.in_sandbox, which +// has guards and is lowered to LOW.) +pub fn first_byte(data: [Int]) -> Int { + nth(data, 0) +} + +fn nth(xs: [Int], k: Int) -> Int { + let mut out = 0; + let mut i = 0; + for x in xs { + out = if i == k { x } else { out }; + i = i + 1; + } + out +} diff --git a/proposals/nextgen-evangelist/affine-migratability/README.adoc b/proposals/nextgen-evangelist/affine-migratability/README.adoc new file mode 100644 index 00000000..64143b5f --- /dev/null +++ b/proposals/nextgen-evangelist/affine-migratability/README.adoc @@ -0,0 +1,235 @@ +// SPDX-License-Identifier: MPL-2.0 += affine-migratability +:toc: macro +:toclevels: 2 + +A linter that triages whether a ReScript `.res` kernel can be migrated to +AffineScript-wasm *today*, or is blocked on a specific AffineScript compiler +wall. Roadmap ask #4 of the *nextgen-languages-evangelist*. It automates the +by-hand triage of the idaptik ReScript->AffineScript migration campaign. + +toc::[] + +== What it does + +`migratability.mjs` takes one or more `.res` files, line-scans for the two +known AffineScript compiler walls plus the re-decomposition signals, and +prints a verdict per file with the offending patterns and line numbers. It +also emits a machine-readable JSON summary for an orchestrator to consume. + +=== The two compiler walls + +[cols="1,3a",options="header"] +|=== +| Wall | What it detects + +| `STRING-GATED` +| The *variable-string backend gap*: string-introspection ops the current +AffineScript codegen cannot lower over a runtime string value. +`String.fromCharCode`, `String.length`, `String.startsWith`, +`String.endsWith`, `String.slice`, `String.get`, `String.charCodeAt`, +`String.indexOf`, and string subscripting (`s[i]`). + +*Not* flagged: plain `++` concatenation and string *literals* — those are +fine today. + +| `EFFECT-GATED` +| The *effect-codegen wall*: ambient effects and module-level mutable state +with no effect-tracked lowering yet. `Date.now`, `Js.Date`, `Console.log`, +`Math.random`, and *module-level* mutable state — a top-level +`let x = Dict.make()` or `let x = ref(...)` (a binding *not* nested inside a +function body). +|=== + +=== Re-decomposition signals (non-blocking) + +These are migratable, but not 1:1 — they require re-decomposition rather than +transliteration, per the migration-playbook. They do *not* block migration; +they are reported as `re-decompose` notes: + +* `promise<` / `Promise.resolve` — incidental async. +* service-locator globals `getDeviceState` / `getState(` — hidden-state reads. + +=== Verdict logic + +[source] +---- +if (any STRING-GATED wall) -> STRING-GATED +elif (any EFFECT-GATED wall) -> EFFECT-GATED +else -> MIGRATABLE NOW (+ any re-decompose notes) +---- + +Process exit code: `0` when every input is `MIGRATABLE NOW`, `1` when any +input is walled, `2` on a usage / IO error. Re-decompose notes alone never +fail the run. + +== Usage + +[source,bash] +---- +# human-readable report (one block per file) +deno run --allow-read migratability.mjs [ ...] + +# JSON summary only (for the orchestrator) +deno run --allow-read migratability.mjs --json +---- + +The JSON summary shape (the contract for the orchestrator): + +[source,json] +---- +{ + "file": "", + "verdict": "STRING-GATED | EFFECT-GATED | MIGRATABLE NOW", + "walls": [ { "kind", "label", "line", "snippet" }, ... ], + "notes": [ { "label", "line", "snippet" }, ... ] +} +---- + +When more than one file is passed with `--json`, the output is a JSON array of +these objects. + +== Detection notes / known limitations + +* *Comment-aware.* Line comments (`//`) and block comments (`+/* */+`) are + stripped before scanning, so a pattern that appears only in prose does not + count as a real wall. +* *`@val external` bindings are skipped for effect calls.* A line such as + `@val external dateNow: unit => float = "Date.now"` *declares* a name; the + effect is carried by the *use* (`dateNow()`). The literal `"Date.now"` on + the binding line is therefore not counted. (This is exactly why + `Kernel_Quantum.res` is judged `EFFECT-GATED` by its module-level + `Dict.make()` + `Console.log`, not by the `"Date.now"` binding string.) +* *Module-level vs function-local mutable state* is decided by column: a + top-level `let` starts at column 0, a function-local `let` is indented + inside its enclosing `let f = (...) => {`. So `Kernel_IO.res`'s in-function + `ref("")` / `ref(false)` are correctly *not* treated as effect walls. +* *String subscript vs array subscript.* ReScript uses the same `ident[i]` + syntax for string and array access, so an array subscript like `arr[2]` + would also match the string-subscript rule. In practice the idaptik kernels + use `Array.get(...)` for arrays, so this does not misfire on them; treat a + lone string-subscript hit as a prompt to confirm the element type. Array + *literals* (`[1, 2, 3]`) are not matched (no leading identifier). + +== Trials (captured) + +Run on the three real idaptik kernels. All three reproduce the known by-hand +triage. + +=== Trial 1 — `Kernel_Compute.res` -> MIGRATABLE NOW + +Command: + +[source,bash] +---- +deno run --allow-read migratability.mjs --json \ + /home/user/idaptik/shared/src/Kernel_Compute.res +---- + +Output: + +[source,json] +---- +{ + "file": "/home/user/idaptik/shared/src/Kernel_Compute.res", + "verdict": "MIGRATABLE NOW", + "walls": [], + "notes": [ + { "label": "promise type (incidental async)", "line": 63, "snippet": "promise<" }, + { "label": "service-locator: getDeviceState", "line": 64, "snippet": "getDeviceState" }, + { "label": "Promise.resolve (incidental async)", "line": 68, "snippet": "Promise.resolve" }, + { "label": "Promise.resolve (incidental async)", "line": 83, "snippet": "Promise.resolve" }, + { "label": "Promise.resolve (incidental async)", "line": 97, "snippet": "Promise.resolve" } + ] +} +---- + +Matches the triage: no walls, re-decompose notes for Promise + the +`getDeviceState` service-locator. This kernel was in fact the migrated +exemplar this session. + +=== Trial 2 — `Kernel_IO.res` -> STRING-GATED + +Command: + +[source,bash] +---- +deno run --allow-read migratability.mjs --json \ + /home/user/idaptik/shared/src/Kernel_IO.res +---- + +Output: + +[source,json] +---- +{ + "file": "/home/user/idaptik/shared/src/Kernel_IO.res", + "verdict": "STRING-GATED", + "walls": [ + { "kind": "STRING-GATED", "label": "String.fromCharCode", "line": 47, "snippet": "String.fromCharCode" }, + { "kind": "STRING-GATED", "label": "String.length", "line": 61, "snippet": "String.length" }, + { "kind": "STRING-GATED", "label": "String.startsWith", "line": 63, "snippet": "String.startsWith" } + ], + "notes": [ + { "label": "promise type (incidental async)", "line": 80, "snippet": "promise<" }, + { "label": "Promise.resolve (incidental async)", "line": 88, "snippet": "Promise.resolve" } + ] +} +---- + +Matches the triage: `String.startsWith` / `String.length` / +`String.fromCharCode`. Note the in-function `ref("")` / `ref(false)` on lines +40-41 are correctly *not* flagged as effect walls (they are nested inside +`decodePathForCheck`). Exit code `1` (walled). + +=== Trial 3 — `Kernel_Quantum.res` -> EFFECT-GATED + +Command: + +[source,bash] +---- +deno run --allow-read migratability.mjs --json \ + /home/user/idaptik/shared/src/Kernel_Quantum.res +---- + +Output: + +[source,json] +---- +{ + "file": "/home/user/idaptik/shared/src/Kernel_Quantum.res", + "verdict": "EFFECT-GATED", + "walls": [ + { "kind": "EFFECT-GATED", "label": "module-level mutable state (Dict.make())", "line": 37, + "snippet": "let lastQuantumOp: Dict.t = Dict.make()" }, + { "kind": "EFFECT-GATED", "label": "Console.log", "line": 99, "snippet": "Console.log" } + ], + "notes": [ + { "label": "promise type (incidental async)", "line": 62, "snippet": "promise<" }, + { "label": "service-locator: getDeviceState", "line": 63, "snippet": "getDeviceState" }, + { "label": "Promise.resolve (incidental async)", "line": 68, "snippet": "Promise.resolve" }, + { "label": "Promise.resolve (incidental async)", "line": 85, "snippet": "Promise.resolve" }, + { "label": "Promise.resolve (incidental async)", "line": 108, "snippet": "Promise.resolve" }, + { "label": "Promise.resolve (incidental async)", "line": 120, "snippet": "Promise.resolve" } + ] +} +---- + +Matches the triage: module-level `Dict.make()` (`lastQuantumOp`, line 37) and +`Console.log` (line 99). The `@val external dateNow ... = "Date.now"` binding +on line 44 is correctly *not* counted as an effect site (it is a binding, not +a use); the verdict stands on the module-level `Dict` + `Console.log`. Exit +code `1` (walled). + +=== Trial summary + +[cols="2,1,3",options="header"] +|=== +| Kernel | Verdict | Decided by + +| `Kernel_Compute.res` | `MIGRATABLE NOW` | no walls (Promise + getDeviceState re-decompose notes only) +| `Kernel_IO.res` | `STRING-GATED` | `String.fromCharCode` / `String.length` / `String.startsWith` +| `Kernel_Quantum.res` | `EFFECT-GATED` | module-level `Dict.make()` + `Console.log` +|=== + +All three reproduce the known by-hand triage. diff --git a/proposals/nextgen-evangelist/affine-migratability/migratability.mjs b/proposals/nextgen-evangelist/affine-migratability/migratability.mjs new file mode 100644 index 00000000..61a9fb88 --- /dev/null +++ b/proposals/nextgen-evangelist/affine-migratability/migratability.mjs @@ -0,0 +1,348 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-migratability — triage whether a ReScript `.res` kernel can be +// migrated to AffineScript-wasm today, or is blocked on a specific compiler +// wall. Roadmap ask #4 of the nextgen-languages-evangelist. +// +// Two known AffineScript compiler walls are detected: +// STRING-GATED — the variable-string backend gap (string introspection +// ops that the current codegen cannot lower). +// EFFECT-GATED — the effect-codegen wall (ambient effects + module-level +// mutable state that has no effect-tracked lowering yet). +// +// Plus re-decomposition signals: patterns that are migratable, but not 1:1. +// They do NOT block migration — they are reported as "re-decompose" notes. +// +// Verdict precedence: STRING-GATED > EFFECT-GATED > MIGRATABLE NOW. +// +// Usage: +// deno run --allow-read migratability.mjs [ ...] +// deno run --allow-read migratability.mjs --json +// +// Exit code: 0 if all inputs are MIGRATABLE NOW, 1 if any are walled, +// 2 on usage / IO error. (Re-decompose notes alone do NOT fail.) + +// --------------------------------------------------------------------------- +// Detection rules +// --------------------------------------------------------------------------- +// +// Each rule is { wall, label, test } where `test(line)` returns either null +// (no match) or the matched substring. A line may match several rules. + +// --- STRING-GATED: variable-string backend gap ----------------------------- +// Plain `++` concatenation and string *literals* are FINE and intentionally +// not listed here. +const STRING_RULES = [ + ["String.fromCharCode", /String\.fromCharCode\b/], + ["String.length", /String\.length\b/], + ["String.startsWith", /String\.startsWith\b/], + ["String.endsWith", /String\.endsWith\b/], + ["String.slice", /String\.slice\b/], + ["String.get", /String\.get\b/], + ["String.charCodeAt", /String\.charCodeAt\b/], + ["String.indexOf", /String\.indexOf\b/], + // String subscripting, e.g. `s[i]` / `path[0]`. Heuristic: an identifier + // immediately followed by `[ ]`. We bias toward names that look + // string-ish OR an index that is plainly numeric/identifier, while skipping + // obvious array-of-int literals like `[1, 2, 3]`. + ["string subscript", /\b[A-Za-z_][A-Za-z0-9_']*\[[A-Za-z0-9_'. ]+\]/], +]; + +// --- EFFECT-GATED: effect-codegen wall ------------------------------------- +// Ambient-effect calls. Module-level mutable state is handled separately +// (it needs column/scope awareness, not just a per-line regex). +const EFFECT_RULES = [ + ["Date.now", /\bDate\.now\b/], + ["Js.Date", /\bJs\.Date\b/], + ["Console.log", /\bConsole\.log\b/], + ["Math.random", /\bMath\.random\b/], +]; + +// --- re-decomposition signals (non-blocking) ------------------------------- +const REDECOMPOSE_RULES = [ + ["promise type (incidental async)", /\bpromise {`. +// +// So: a line that begins with `let ` (no leading whitespace) and whose RHS +// (text after the first `=`) contains a mutable allocator. + +const MUT_ALLOCATORS = [ + ["Dict.make()", /Dict\.make\(\)/], + ["ref(...)", /\bref\(/], +]; + +function detectModuleLevelMutable(line) { + // Must be a top-level `let` (column 0, exactly one `let ` at the start). + if (!/^let\s/.test(line)) return null; + const eq = line.indexOf("="); + if (eq === -1) return null; + const rhs = line.slice(eq + 1); + for (const [label, re] of MUT_ALLOCATORS) { + const m = rhs.match(re); + if (m) return { label, snippet: m[0] }; + } + return null; +} + +// --------------------------------------------------------------------------- +// Comment stripping +// --------------------------------------------------------------------------- +// +// We do not want a pattern that only appears in a comment (e.g. an `@val +// external` doc, or prose mentioning `Date.now`) to count as a real wall. +// We strip line comments (`//...`) before scanning. Block comments (`/* */`) +// are rare in ReScript and handled with a simple stateful pass. String +// literals are deliberately NOT stripped: an `@val external` BINDING whose +// payload string is `"Date.now"` is a genuine effect site only when called, +// and the call (`dateNow()`) is what carries the effect — but to stay +// conservative and avoid false-negatives we keep literal text out of the +// scan for the literal-only `@val external ... = "Date.now"` shape, since +// that line is a binding, not a use. See `isExternalBinding`. + +function isExternalBinding(line) { + // `@val external foo: ... = "..."` — a binding line, not a use site. + return /@(val|scope|send|get|set|new|module)\b/.test(line) && + /\bexternal\b/.test(line); +} + +// Strip `//` line comments outside of string literals. Good enough for +// ReScript: we walk the line tracking double-quote string state. +function stripLineComment(line) { + let inStr = false; + for (let i = 0; i < line.length - 1; i++) { + const c = line[i]; + if (c === '"' && line[i - 1] !== "\\") inStr = !inStr; + if (!inStr && c === "/" && line[i + 1] === "/") { + return line.slice(0, i); + } + } + return line; +} + +// --------------------------------------------------------------------------- +// Scanner +// --------------------------------------------------------------------------- + +function scan(source, file) { + const rawLines = source.split(/\r?\n/); + + const walls = []; // { kind, label, line, snippet } + const notes = []; // { label, line, snippet } + + let inBlockComment = false; + + rawLines.forEach((raw, idx) => { + const lineNo = idx + 1; + + // --- block comment handling --- + let line = raw; + if (inBlockComment) { + const end = line.indexOf("*/"); + if (end === -1) return; // whole line is inside a block comment + line = line.slice(end + 2); + inBlockComment = false; + } + const open = line.indexOf("/*"); + if (open !== -1) { + const close = line.indexOf("*/", open + 2); + if (close === -1) { + line = line.slice(0, open); + inBlockComment = true; + } else { + line = line.slice(0, open) + " " + line.slice(close + 2); + } + } + + // --- line comment handling --- + line = stripLineComment(line); + if (line.trim() === "") return; + + const externalBinding = isExternalBinding(line); + + // --- STRING-GATED --- + for (const [label, re] of STRING_RULES) { + const m = line.match(re); + if (m) { + walls.push({ kind: "STRING-GATED", label, line: lineNo, snippet: m[0] }); + } + } + + // --- EFFECT-GATED: ambient calls --- + // Skip pure `@val external ... = "..."` binding lines: they declare a + // name, the effect is carried by the *use* of that name elsewhere. + if (!externalBinding) { + for (const [label, re] of EFFECT_RULES) { + const m = line.match(re); + if (m) { + walls.push({ kind: "EFFECT-GATED", label, line: lineNo, snippet: m[0] }); + } + } + } + + // --- EFFECT-GATED: module-level mutable state --- + const mut = detectModuleLevelMutable(line); + if (mut) { + walls.push({ + kind: "EFFECT-GATED", + label: `module-level mutable state (${mut.label})`, + line: lineNo, + snippet: line.trim(), + }); + } + + // --- re-decomposition notes (non-blocking) --- + for (const [label, re] of REDECOMPOSE_RULES) { + const m = line.match(re); + if (m) { + notes.push({ label, line: lineNo, snippet: m[0] }); + } + } + }); + + // --- verdict precedence --- + const stringWalls = walls.filter((w) => w.kind === "STRING-GATED"); + const effectWalls = walls.filter((w) => w.kind === "EFFECT-GATED"); + + let verdict; + if (stringWalls.length > 0) verdict = "STRING-GATED"; + else if (effectWalls.length > 0) verdict = "EFFECT-GATED"; + else verdict = "MIGRATABLE NOW"; + + return { file, verdict, walls, notes, stringWalls, effectWalls }; +} + +// --------------------------------------------------------------------------- +// Reporting +// --------------------------------------------------------------------------- + +function basename(p) { + const parts = p.split("/"); + return parts[parts.length - 1]; +} + +function printHuman(result) { + const { file, verdict, walls, notes } = result; + const tag = verdict === "MIGRATABLE NOW" ? "[OK]" : "[WALL]"; + console.log(`${tag} ${basename(file)} -> ${verdict}`); + console.log(` ${file}`); + + if (walls.length > 0) { + // The deciding walls first, grouped by kind. + const deciding = verdict === "STRING-GATED" ? "STRING-GATED" : "EFFECT-GATED"; + const decidingWalls = walls.filter((w) => w.kind === deciding); + console.log(` walls (${deciding}):`); + for (const w of decidingWalls) { + console.log(` ${file}:${w.line} ${w.label} -> ${w.snippet}`); + } + // Any other-kind walls that exist but did not decide the verdict. + const other = walls.filter((w) => w.kind !== deciding); + if (other.length > 0) { + console.log(` also flagged (${other[0].kind}):`); + for (const w of other) { + console.log(` ${file}:${w.line} ${w.label} -> ${w.snippet}`); + } + } + } + + if (notes.length > 0) { + console.log(" re-decompose notes (non-blocking):"); + for (const n of notes) { + console.log(` ${file}:${n.line} ${n.label} -> ${n.snippet}`); + } + } +} + +function summaryJSON(result) { + return { + file: result.file, + verdict: result.verdict, + walls: result.walls.map((w) => ({ + kind: w.kind, + label: w.label, + line: w.line, + snippet: w.snippet, + })), + notes: result.notes.map((n) => ({ + label: n.label, + line: n.line, + snippet: n.snippet, + })), + }; +} + +// --------------------------------------------------------------------------- +// CLI +// --------------------------------------------------------------------------- + +function usage() { + console.error( + "usage: deno run --allow-read migratability.mjs [--json] [ ...]", + ); +} + +async function main() { + const args = [...Deno.args]; + let jsonOnly = false; + const files = []; + for (const a of args) { + if (a === "--json") jsonOnly = true; + else if (a === "-h" || a === "--help") { + usage(); + Deno.exit(0); + } else files.push(a); + } + + if (files.length === 0) { + usage(); + Deno.exit(2); + } + + const results = []; + for (const file of files) { + let source; + try { + source = await Deno.readTextFile(file); + } catch (e) { + console.error(`error: cannot read ${file}: ${e.message}`); + Deno.exit(2); + } + results.push(scan(source, file)); + } + + if (jsonOnly) { + const out = results.length === 1 + ? summaryJSON(results[0]) + : results.map(summaryJSON); + console.log(JSON.stringify(out, null, 2)); + } else { + results.forEach((r, i) => { + if (i > 0) console.log(""); + printHuman(r); + console.log(" summary: " + JSON.stringify(summaryJSON(r))); + }); + } + + const anyWalled = results.some((r) => r.verdict !== "MIGRATABLE NOW"); + Deno.exit(anyWalled ? 1 : 0); +} + +// Exported for testing / orchestrator embedding. +export { scan, summaryJSON }; + +if (import.meta.main) { + await main(); +} diff --git a/proposals/nextgen-evangelist/affine-parity/README.adoc b/proposals/nextgen-evangelist/affine-parity/README.adoc new file mode 100644 index 00000000..40aa2778 --- /dev/null +++ b/proposals/nextgen-evangelist/affine-parity/README.adoc @@ -0,0 +1,199 @@ +// SPDX-License-Identifier: MPL-2.0 += affine-parity -- a generic differential-parity harness runner for AffineScript wasm +:toc: macro +:toclevels: 2 + +A config-driven runner that generalises the one-off "compile + instantiate + +sweep + compare to a JS oracle" harnesses written by hand during the +AffineScript co-development sessions. It is roadmap asks #2/#3 of the +*nextgen-languages-evangelist*. + +Given a config it: + +. compiles the `.affine` source *host-native* by calling the prebuilt + compiler binary directly (no `dune`, to dodge the build lock); +. instantiates the resulting wasm (scalar i32 ABI; WASI stubbed); +. calls each exported `pub fn` over a sweep of inputs; +. compares every result against an *independent* JS oracle; +. reports `N/N pass` and exits `1` on any mismatch. + +toc::[] + +== ABI scope (read this) + +This runner handles the *scalar i32 ABI* only: every argument is an `i32` and +every result is an `i32`. That is exactly the boundary the `DESIGN-VISION` +prescribes ("AffineScript is the brain, JS/Pixi the senses; they pass +*primitives* across the wasm boundary") and it covers pure-integer +co-processors such as `SecurityRank`. + +Array/string parameters use a *different* convention -- +`[len:i32 LE][utf8/bytes]` written into linear memory plus an exported +`__affine_alloc` -- and are a deliberate *follow-on*, NOT implemented here. +Exports taking `[Int]` / `String` parameters can therefore only be invoked here +in their nullary form (e.g. `Kernel_IO`'s `main`, whose array arguments are +inlined inside the `.affine` source). See the limitation note at the end. + +== Requirements + +* `deno` on `PATH`. +* The prebuilt AffineScript compiler at + `/home/user/affinescript/_build/default/bin/main.exe` + (the path is a constant at the top of `parity.mjs`). + +== Usage + +[source,console] +---- +deno run --allow-read --allow-run parity.mjs +deno run --allow-read --allow-run parity.mjs --verbose +---- + +Exit codes: `0` = all cases pass, `1` = a mismatch / compile / load error, +`2` = bad invocation. + +== Config shape + +A config is a `.mjs` module with a default export: + +[source,js] +---- +export default { + affine: "SecurityRank.affine", // path, resolved relative to the config file + // out: "SecurityRank.wasm", // optional wasm output path + // compile: true, // optional; default true. false = reuse an existing wasm + cases: [ + { + name: "rank_security_level over [-5..8]", // optional label + export: "rank_security_level", // the wasm export to call + args: [ [-5, 8] ], // one entry per parameter + oracle: (level) => /* expected i32 */, // independent expected-value fn + }, + // ... + ], +}; +---- + +Each entry in `args` is one of: + +* an inclusive integer range `[lo, hi]` -- swept `lo..hi`; +* an explicit value list `{ values: [a, b, c] }` -- swept verbatim; +* a single number -- a fixed scalar (1-element sweep). + +The runner takes the *Cartesian product* across all parameters. A nullary export +uses `args: []` and is called once. Results are normalised to i32 (`| 0`) on +both sides before comparison. + +Relative paths (`affine`, `out`) resolve against the *config file's* directory, +so a config can sit next to its `.affine`/`.wasm`. + +== Files in this directory + +[cols="1,3"] +|=== +| `parity.mjs` | the runner (plain JavaScript / Deno; scalar i32 ABI) +| `securityrank.config.mjs` | trial 1 config (two cases, 78 inputs) +| `kernel_io.config.mjs` | trial 2 config (one nullary case) +| `SecurityRank.affine` | local copy of the idaptik co-processor under test +| `SecurityRank.wasm` / `Kernel_IO.wasm` | compiler output (regenerated each run) +|=== + +`Kernel_IO.affine` itself is read from `/tmp/idaptik-migration/Kernel_IO.affine` +(referenced by absolute path in `kernel_io.config.mjs`); it was not copied into +this directory. + +== Captured trials + +=== Setup -- copy + compile + +[source,console] +---- +$ cp /home/user/idaptik/vm/coprocessor/SecurityRank.affine ./SecurityRank.affine + +$ /home/user/affinescript/_build/default/bin/main.exe compile ./SecurityRank.affine -o ./SecurityRank.wasm +Compiled ./SecurityRank.affine -> ./SecurityRank.wasm (WASM) +# exit=0 + +$ /home/user/affinescript/_build/default/bin/main.exe compile /tmp/idaptik-migration/Kernel_IO.affine -o ./Kernel_IO.wasm +Compiled /tmp/idaptik-migration/Kernel_IO.affine -> ./Kernel_IO.wasm (WASM) +# exit=0 +---- + +Export/import surface confirmed (both import only +`wasi_snapshot_preview1.fd_write`; the runner stubs the whole WASI namespace so +modules pulling in extra wasi names via `_start` still instantiate): + +---- +SecurityRank.wasm EXPORTS= memory, rank_security_level, passes_min_security +Kernel_IO.wasm EXPORTS= memory, in_sandbox, main, _start +---- + +=== Trial 1 -- SecurityRank (78/78 pass) + +`rank_security_level(level)` over `level` in `[-5..8]` (14 inputs), oracle +`lv => lv===0?0:lv===1?1:lv===2?2:lv===3?3:(lv<0?0:3)`; and +`passes_min_security(dl, th)` over `dl, th` in `[-2..5]^2` (64 inputs), oracle +`(dl, th) => oracleRank(dl) >= oracleRank(th) ? 1 : 0`. 14 + 64 = 78. + +[source,console] +---- +$ deno run --allow-read --allow-run parity.mjs securityrank.config.mjs + [PASS] rank_security_level over [-5..8]: 14/14 + [PASS] passes_min_security over [-2..5]^2: 64/64 + +78/78 pass +# exit=0 +---- + +*Result: 78/78 pass, exit 0.* (Matches the expected 78/78.) + +=== Trial 2 -- Kernel_IO (`main()` === 6) + +`Kernel_IO`'s `in_sandbox` takes two `[Int]` parameters (the array ABI this +runner does not yet marshal), so it cannot be swept here. Instead the harness +drives the module's nullary self-check `main()`, which runs six inlined sandbox +scenarios and returns the count that passed -- 6 when all green. Oracle: the +constant `6`. + +[source,console] +---- +$ deno run --allow-read --allow-run parity.mjs kernel_io.config.mjs + [PASS] main() self-check returns 6: 1/1 + +1/1 pass +# exit=0 +---- + +*Result: `main()` === 6, 1/1 pass, exit 0.* +(`/tmp/idaptik-migration/Kernel_IO.affine` was present, so case 2 was not +skipped.) + +=== Negative check -- a wrong oracle exits 1 + +To show the mismatch path is real (not a runner that always reports green), a +deliberately-wrong oracle (`() => 99`) against `rank_security_level`: + +[source,console] +---- + [FAIL] deliberately wrong oracle: 0/14 + args=(-5) got=0 want=99 + args=(-4) got=0 want=99 + ... and 4 more + +0/14 pass <-- MISMATCH +# exit=1 +---- + +Per-input failures are reported (first 10, then a count), and the process exits +`1`. + +== Known limitation + +The runner currently marshals only the *scalar i32 ABI* (i32 args -> i32 +result), which is the primitives-across-the-boundary contract pure-integer +co-processors use. Exports with `[Int]` / `String` parameters need the +`[len:i32 LE][utf8 bytes]`-into-linear-memory convention plus the exported +`__affine_alloc` allocator; marshalling those (write args into `memory`, pass +pointers, read back any array result) is a clean follow-on but is *not* +implemented here -- which is why `Kernel_IO` is exercised through its nullary +`main()` rather than by sweeping `in_sandbox` directly. diff --git a/proposals/nextgen-evangelist/affine-parity/SecurityRank.affine b/proposals/nextgen-evangelist/affine-parity/SecurityRank.affine new file mode 100644 index 00000000..b57a4fb1 --- /dev/null +++ b/proposals/nextgen-evangelist/affine-parity/SecurityRank.affine @@ -0,0 +1,63 @@ +// SPDX-License-Identifier: AGPL-3.0-or-later +// +// SecurityRank -- the device security-level ranking co-processor, the pure +// integer core extracted from DeviceRegistry.byMinSecurityLevel. Per the +// DESIGN-VISION ("AffineScript is the brain, JS/Pixi the senses; they pass +// primitives across the wasm boundary"), the JS host keeps the dict of devices +// and their string IP keys; AffineScript owns only the ordering arithmetic. +// +// The ReScript original folds a securityLevel variant through a four-arm rank +// switch (Open < Weak < Medium < Strong) and keeps a device iff its rank is at +// least the threshold's. We re-decompose that variant as the canonical 0..3 +// integer encoding the switch already produces, so the rank function is a clamp +// onto that closed band and the filter predicate is a single comparison. No +// strings, no floats, no effects cross the boundary; the encoding IS the rank. +// +//## Security-level encoding (the header contract for the JS host) +// level variant rank +// 0 Open 0 +// 1 Weak 1 +// 2 Medium 2 +// 3 Strong 3 +// Any input outside 0..3 is clamped to the nearest valid rank, so a malformed +// host level can never invert the ordering. + +enum Level { Open, Weak, Medium, Strong, Invalid(Int) } + +// Decode a host integer into a level variant. The trailing Invalid arm carries +// the offending value so the nullary variants ahead of it tag correctly and so +// the clamp can recover a defined rank. Flat guarded returns avoid the deep +// if/else expression nesting the parser dislikes. +fn level_of(level: Int) -> Level { + if level == 0 { return Open; } + if level == 1 { return Weak; } + if level == 2 { return Medium; } + if level == 3 { return Strong; } + Invalid(level) +} + +// Map a level variant to its ordinal rank. Out-of-band inputs clamp: anything +// below Open becomes 0, anything above Strong becomes 3, preserving the total +// order Open < Weak < Medium < Strong. +fn rank_of(l: Level) -> Int { + match l { + Open => 0, + Weak => 1, + Medium => 2, + Strong => 3, + Invalid(v) => { if v < 0 { 0 } else { 3 } } + } +} + +// Rank a security level, clamping the 0..3 encoding. Identity on valid input. +pub fn rank_security_level(level: Int) -> Int { + rank_of(level_of(level)) +} + +// The filter predicate of byMinSecurityLevel: keep a device iff its security +// rank meets or exceeds the threshold. Returns 1 to keep, 0 to drop. +pub fn passes_min_security(device_level: Int, threshold: Int) -> Int { + let dr = rank_of(level_of(device_level)); + let tr = rank_of(level_of(threshold)); + if dr >= tr { 1 } else { 0 } +} diff --git a/proposals/nextgen-evangelist/affine-parity/kernel_io.config.mjs b/proposals/nextgen-evangelist/affine-parity/kernel_io.config.mjs new file mode 100644 index 00000000..72ff1e60 --- /dev/null +++ b/proposals/nextgen-evangelist/affine-parity/kernel_io.config.mjs @@ -0,0 +1,32 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-parity config for Kernel_IO.affine (idaptik pure-integer device +// sandbox check). +// +// Kernel_IO's interesting export, `in_sandbox(data: [Int], root: [Int])`, takes +// two Int-array parameters -- the array ABI ([len:i32 LE][utf8/bytes] + an +// exported __affine_alloc) which THIS runner does not yet marshal (it handles +// the scalar i32 ABI only; see the ABI SCOPE note in parity.mjs). So we cannot +// sweep in_sandbox from here. +// +// What we CAN do, staying inside the scalar ABI, is exercise the module's own +// self-checking entry point `main()`. It runs six inlined sandbox scenarios +// (exact root IN, root+"/file" IN, other-device OUT, /etc/passwd OUT, empty IN, +// "/sandbox/dev10" prefix-without-separator OUT) and returns the count that +// passed -- 6 when all green. A nullary export, so the oracle is the constant 6. +// +// This proves the harness drives a nullary i32-returning export and that the +// re-decomposed array logic (inlined in main) computes correctly end to end. + +export default { + affine: "/tmp/idaptik-migration/Kernel_IO.affine", + cases: [ + { + name: "main() self-check returns 6", + export: "main", + args: [], // nullary + oracle: () => 6, + }, + ], +}; diff --git a/proposals/nextgen-evangelist/affine-parity/parity.mjs b/proposals/nextgen-evangelist/affine-parity/parity.mjs new file mode 100644 index 00000000..c957370f --- /dev/null +++ b/proposals/nextgen-evangelist/affine-parity/parity.mjs @@ -0,0 +1,263 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-parity -- a generic differential-parity harness runner for AffineScript +// wasm. Roadmap asks #2/#3 of the nextgen-languages-evangelist. +// +// Given a config, it: +// 1. compiles the `.affine` source host-native (via the prebuilt compiler), +// 2. instantiates the resulting wasm (scalar i32 ABI; wasi stubbed), +// 3. calls each exported `pub fn` over a sweep of inputs, +// 4. compares every result against an independent JS oracle, +// 5. reports "N/N pass" and exits 1 on any mismatch. +// +// It is the config-driven generalisation of the one-off harnesses written by +// hand this session: instead of bespoke `deno eval` per module, you hand it a +// config describing which exports to sweep, over which input ranges, against +// which oracle. +// +//## ABI SCOPE (read this) +// This runner handles the **scalar i32 ABI** only: every argument is an i32 and +// every result is an i32. That is exactly the boundary the DESIGN-VISION +// prescribes ("they pass primitives across the wasm boundary") and it covers +// pure-integer co-processors such as SecurityRank. Array/string parameters use +// a different convention -- `[len:i32 LE][utf8 bytes]` written into linear +// memory plus an exported `__affine_alloc` -- and are a deliberate follow-on, +// NOT implemented here. Exports taking [Int]/String params therefore can only be +// invoked here in their nullary form (e.g. Kernel_IO's `main`, whose array +// arguments are inlined inside the .affine source). +// +//## CONFIG SHAPE +// A config is a `.mjs` module with a default export: +// +// export default { +// affine: "SecurityRank.affine", // path, resolved relative to cfg +// // optional: out: "SecurityRank.wasm", // wasm output path +// // optional: compile: true, // default true; false = reuse wasm +// cases: [ +// { +// export: "rank_security_level", // wasm export to call +// args: [ [-5, 8] ], // one [lo,hi] inclusive range / arg +// oracle: (level) => (...), // independent expected-value fn +// // optional: name: "..." // label for the report +// }, +// ... +// ], +// }; +// +// `args` is a list, one entry per function parameter. Each entry is either: +// * an inclusive integer range `[lo, hi]` -> swept lo..hi, OR +// * an explicit array of values `{ values: [..] }` -> swept verbatim, OR +// * a single number -> a fixed scalar (1-element sweep). +// The runner takes the Cartesian product across all parameters. A nullary export +// (no params) uses `args: []` and is called once. +// +// Usage: +// deno run --allow-read --allow-run parity.mjs +// deno run --allow-read --allow-run parity.mjs --verbose +// +// Exit codes: 0 = all cases pass, 1 = a mismatch / compile / load error, +// 2 = bad invocation. + +const COMPILER = "/home/user/affinescript/_build/default/bin/main.exe"; + +// A WASI shim: every import returns 0 and does nothing. The scalar-i32 pub fns +// never actually drive I/O at runtime, but the module imports fd_write (and the +// `_start`/wasi surface may reference more), so a permissive stub keeps +// instantiation total regardless of which wasi names a given module pulls in. +function makeWasiImports() { + const stub = new Proxy( + {}, + { get: () => () => 0 }, + ); + return { wasi_snapshot_preview1: stub }; +} + +// Resolve a path that may be relative to the config file's directory. +function resolveFrom(baseDir, p) { + if (p.startsWith("/")) return p; + return `${baseDir}/${p}`; +} + +// Compile -> by calling the prebuilt compiler binary directly +// (no dune, to dodge the build lock). Returns the path to the produced wasm. +async function compileAffine(affinePath, outPath) { + const cmd = new Deno.Command(COMPILER, { + args: ["compile", affinePath, "-o", outPath], + stdout: "piped", + stderr: "piped", + }); + const { code, stdout, stderr } = await cmd.output(); + const out = new TextDecoder().decode(stdout).trim(); + const err = new TextDecoder().decode(stderr).trim(); + if (code !== 0) { + throw new Error( + `compile failed (exit ${code})\n cmd: ${COMPILER} compile ${affinePath} -o ${outPath}\n stdout: ${out}\n stderr: ${err}`, + ); + } + return { outPath, log: out || err }; +} + +// Instantiate a wasm file under the WASI stub; return the exports object. +async function instantiate(wasmPath) { + const bytes = await Deno.readFile(wasmPath); + const { instance } = await WebAssembly.instantiate(bytes, makeWasiImports()); + return instance.exports; +} + +// Expand one parameter spec into the concrete list of values it sweeps. +function expandArgSpec(spec, paramIndex) { + if (typeof spec === "number") return [spec]; + if (Array.isArray(spec)) { + if (spec.length !== 2) { + throw new Error( + `arg spec #${paramIndex} as a range must be [lo, hi]; got [${spec}]`, + ); + } + const [lo, hi] = spec; + if (!Number.isInteger(lo) || !Number.isInteger(hi)) { + throw new Error(`arg spec #${paramIndex} range bounds must be integers`); + } + if (hi < lo) { + throw new Error(`arg spec #${paramIndex} range hi(${hi}) < lo(${lo})`); + } + const out = []; + for (let v = lo; v <= hi; v++) out.push(v); + return out; + } + if (spec && Array.isArray(spec.values)) return spec.values.slice(); + throw new Error( + `arg spec #${paramIndex} must be a number, a [lo,hi] range, or { values: [...] }`, + ); +} + +// Cartesian product of a list of value-lists. [] -> [[]] (the single empty tuple). +function cartesian(lists) { + return lists.reduce( + (acc, list) => acc.flatMap((tuple) => list.map((v) => [...tuple, v])), + [[]], + ); +} + +// Run a single case (one export + its arg sweep + its oracle). Returns +// { name, total, pass, failures: [{args, got, want}] }. +function runCase(exports, kase, idx) { + const name = kase.name || kase.export || `case#${idx}`; + const fn = exports[kase.export]; + if (typeof fn !== "function") { + throw new Error( + `export "${kase.export}" not found or not a function (case "${name}")`, + ); + } + if (typeof kase.oracle !== "function") { + throw new Error(`case "${name}" has no oracle function`); + } + const argSpecs = kase.args || []; + const perParam = argSpecs.map((s, i) => expandArgSpec(s, i)); + const tuples = cartesian(perParam); + + let pass = 0; + const failures = []; + for (const tuple of tuples) { + const got = fn(...tuple) | 0; // normalise to i32 + const want = kase.oracle(...tuple) | 0; + if (got === want) { + pass++; + } else { + failures.push({ args: tuple, got, want }); + } + } + return { name, total: tuples.length, pass, failures }; +} + +async function loadConfig(configPath) { + const abs = configPath.startsWith("/") + ? configPath + : `${Deno.cwd()}/${configPath}`; + const mod = await import(`file://${abs}`); + const cfg = mod.default; + if (!cfg || typeof cfg !== "object") { + throw new Error(`config "${configPath}" must have a default-export object`); + } + if (!cfg.affine) throw new Error(`config "${configPath}" missing "affine"`); + if (!Array.isArray(cfg.cases) || cfg.cases.length === 0) { + throw new Error(`config "${configPath}" needs a non-empty "cases" array`); + } + // baseDir = directory of the config file, for resolving relative paths. + const baseDir = abs.slice(0, abs.lastIndexOf("/")) || "."; + return { cfg, baseDir, configPath }; +} + +export async function runParity(configPath, { verbose = false } = {}) { + const { cfg, baseDir } = await loadConfig(configPath); + + const affinePath = resolveFrom(baseDir, cfg.affine); + const outPath = resolveFrom( + baseDir, + cfg.out || cfg.affine.replace(/\.affine$/, ".wasm"), + ); + + const doCompile = cfg.compile !== false; + if (doCompile) { + const { log } = await compileAffine(affinePath, outPath); + if (verbose && log) console.log(`[compile] ${log}`); + } else if (verbose) { + console.log(`[compile] skipped; reusing ${outPath}`); + } + + const exports = await instantiate(outPath); + + let grandTotal = 0; + let grandPass = 0; + const results = []; + cfg.cases.forEach((kase, i) => { + const r = runCase(exports, kase, i); + results.push(r); + grandTotal += r.total; + grandPass += r.pass; + }); + + // Report. + for (const r of results) { + const ok = r.pass === r.total; + const tag = ok ? "PASS" : "FAIL"; + console.log(` [${tag}] ${r.name}: ${r.pass}/${r.total}`); + if (!ok) { + const show = r.failures.slice(0, 10); + for (const f of show) { + console.log( + ` args=(${f.args.join(", ")}) got=${f.got} want=${f.want}`, + ); + } + if (r.failures.length > show.length) { + console.log(` ... and ${r.failures.length - show.length} more`); + } + } else if (verbose) { + for (let i = 0; i < Math.min(r.total, 0); i++) { /* no-op */ } + } + } + + const allPass = grandPass === grandTotal; + console.log(""); + console.log(`${grandPass}/${grandTotal} pass${allPass ? "" : " <-- MISMATCH"}`); + return { grandPass, grandTotal, allPass, results }; +} + +if (import.meta.main) { + const args = Deno.args.slice(); + const verbose = args.includes("--verbose"); + const positional = args.filter((a) => !a.startsWith("--")); + if (positional.length !== 1) { + console.error( + "usage: deno run --allow-read --allow-run parity.mjs [--verbose]", + ); + Deno.exit(2); + } + try { + const { allPass } = await runParity(positional[0], { verbose }); + Deno.exit(allPass ? 0 : 1); + } catch (e) { + console.error(`affine-parity error: ${e.message}`); + Deno.exit(1); + } +} diff --git a/proposals/nextgen-evangelist/affine-parity/securityrank.config.mjs b/proposals/nextgen-evangelist/affine-parity/securityrank.config.mjs new file mode 100644 index 00000000..05dd7e1a --- /dev/null +++ b/proposals/nextgen-evangelist/affine-parity/securityrank.config.mjs @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// affine-parity config for SecurityRank.affine (idaptik device-security +// ranking co-processor; scalar i32 ABI). +// +// Two parity cases: +// 1. rank_security_level(level) over level in [-5..8] -> 14 inputs +// 2. passes_min_security(device_level, threshold) over [-2..5]^2 -> 64 inputs +// Total: 78 inputs. Expect 78/78 pass. +// +//## The oracle (independent of the .affine) +// The .affine clamps a host integer onto the closed 0..3 rank band: +// level rank +// 0 0 (Open) +// 1 1 (Weak) +// 2 2 (Medium) +// 3 3 (Strong) +// <0 0 (clamp down -- Invalid below Open) +// >3 3 (clamp up -- Invalid above Strong) +// We re-derive that here in plain JS rather than reusing any AffineScript code, +// so a regression in the compiler/codegen surfaces as a differential mismatch. +const oracleRank = (lv) => + lv === 0 ? 0 : lv === 1 ? 1 : lv === 2 ? 2 : lv === 3 ? 3 : (lv < 0 ? 0 : 3); + +export default { + affine: "SecurityRank.affine", + cases: [ + { + name: "rank_security_level over [-5..8]", + export: "rank_security_level", + args: [[-5, 8]], + oracle: (level) => oracleRank(level), + }, + { + name: "passes_min_security over [-2..5]^2", + export: "passes_min_security", + args: [[-2, 5], [-2, 5]], + // keep a device iff its rank >= the threshold's rank + oracle: (dl, th) => (oracleRank(dl) >= oracleRank(th) ? 1 : 0), + }, + ], +}; diff --git a/proposals/nextgen-evangelist/deno-esm-spike/README.adoc b/proposals/nextgen-evangelist/deno-esm-spike/README.adoc new file mode 100644 index 00000000..480372bc --- /dev/null +++ b/proposals/nextgen-evangelist/deno-esm-spike/README.adoc @@ -0,0 +1,161 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += deno-esm-spike — proving the AffineScript -> Deno-ESM -> TypeScript-0 path +:toc: macro + +[IMPORTANT] +==== +*Status: SPIKE / PROPOSAL — TRIALED, GREEN.* This directory is a trial of +*nextgen-languages-evangelist roadmap ask #3*: can an AffineScript source be +compiled to a Deno ES module and run under Deno, so that *parity / scan +harnesses could be authored in AffineScript instead of TypeScript* (the +"TypeScript-0" goal)? + +*Verdict: WORKS.* The `--deno-esm` backend (issue #122) emits real ESM +named exports that import cleanly from a plain `.mjs` Deno driver and are +directly callable. All five driver checks pass; exit 0; zero TypeScript. +==== + +toc::[] + +== What this proves (and why it matters for TS-0) + +The evangelist's parity harness (sibling `affine-parity/`) and any future +scan/test harness need to *call AffineScript-compiled code from a script*. +The estate language policy bans new TypeScript and prefers AffineScript. If +AffineScript compiles to an importable ES module, those harnesses can be +written in AffineScript (compiled to `.js`) + a thin `.mjs` glue driver, +with *no TypeScript anywhere* in the loop. + +This spike is the minimal end-to-end demonstration of that path. + +== Files + +[cols="1,3"] +|=== +| `sample.affine` | Minimal AffineScript: two `pub fn`s (`add`, `clamp_band`), pure integer arithmetic, no `extern`/host calls — so the only thing under test is the *export shape*. +| `sample.js` | Generated by the compiler with `--deno-esm`. A drop-in ES module (committed here as the captured trial artefact). +| `driver.mjs` | Plain-JavaScript (`.mjs`, NOT TypeScript) Deno consumer: `import { add, clamp_band } from "./sample.js"` then asserts five results. +|=== + +== Step 0 — confirm the invocation (the flag is real) + +`compile --help` documents the flag exactly: + +---- +$ /home/user/affinescript/_build/default/bin/main.exe compile --help +... +OPTIONS + --deno-esm + Emit a standalone Deno/Node ES module directly from the AST (issue + #122): `export class` for struct+impl, `export` for public + fns/consts, and `extern fn` lowered to direct host calls + (Deno.*Sync / JSON / WebAssembly). No wasm, no require, no handle + table — the output is a drop-in importable ESM. A `.deno.js` + output extension selects this backend implicitly. +... +---- + +So the invocation is `compile --deno-esm -o .js .affine` (or simply +name the output `.deno.js` to select the backend implicitly). + +== Step 1 — compile the sample with --deno-esm + +---- +$ /home/user/affinescript/_build/default/bin/main.exe compile --deno-esm -o sample.js sample.affine +Compiled sample.affine -> sample.js (Deno-ESM) +exit=0 +---- + +== Step 2 — what the generated `.js` looks like + +The file is ~453 lines: an inlined AffineScript Deno-ESM runtime prelude +(Option/Result constructors, `print`/`println`, and a large bank of host +shims for Deno FS, pixi.js, motion, sqlite, http, json, etc. — all unused +by this pure sample but always emitted), followed by the actual exports. The +load-bearing tail is the exports themselves: + +[source,javascript] +---- +// Generated by AffineScript compiler (Deno-ESM target, issue #122) +// SPDX-License-Identifier: MPL-2.0 +// ---- AffineScript Deno-ESM runtime ---- +const Some = (value) => ({ tag: "Some", value }); +const None = { tag: "None" }; +const Ok = (value) => ({ tag: "Ok", value }); +const Err = (error) => ({ tag: "Err", error }); +const Unit = null; +const print = (s) => { Deno.stdout.writeSync(new TextEncoder().encode(String(s))); }; +const println = (s) => { console.log(String(s)); }; +// ... (~440 lines of host shims for FS/pixi/motion/sqlite/http/json) ... +// ---- end runtime ---- + +export function add(a, b) { + return (a + b); +} + +export function clamp_band(x) { + return ((x < 0) ? (() => { return 0; })() : (() => { return ((x > 3) ? (() => { return 3; })() : (() => { return x; })()); })()); +} +---- + +Observations, honestly: + +* The exports are *real ESM named exports* (`export function add`), not a + default-export blob, not a wasm handle table — exactly the "drop-in + importable ESM" the `--help` text promises. +* `if/else` lowers to an IIFE-per-branch ternary + (`(cond ? (() => {...})() : (() => {...})())`). Verbose, but semantically + correct and fully callable (the driver exercises both branches of + `clamp_band`). +* The runtime prelude is emitted unconditionally (all host shims, even + when the sample uses none). Cosmetic only — it does not affect the export + contract — but a future size-conscious iteration could tree-shake it. + +== Step 3 — run it under Deno + +[source] +---- +$ deno run ./driver.mjs +deno-esm-spike driver: importing AffineScript-compiled ESM + typeof add = function + typeof clamp_band = function + ok add(2, 3): 5 + ok add(-4, 4): 0 + ok clamp_band(-7) [below band]: 0 + ok clamp_band(2) [in band]: 2 + ok clamp_band(99) [above band]: 3 + +result: 5 passed, 0 failed +exit=0 +---- + +(Runs identically with or without `--allow-read`; the module read is implicit +in Deno's module loader, and the sample needs no further permissions.) + +`deno --version` at trial time: `deno 2.8.2 (stable) / typescript 6.0.3`. + +== Verdict + +*WORKS — the TS-0 path is open.* An AffineScript source compiles via +`--deno-esm` to a drop-in ES module whose `pub fn`s become callable named +exports, importable from a plain `.mjs` Deno driver, returning correct values +across both arms of a branch. No TypeScript was authored or needed at any +step. + +*Implication for the evangelist:* parity and scan harnesses (sibling +`affine-parity/`, `affine-assail/`) can be rewritten with their *logic in +AffineScript* (compiled to `.js`) and only a thin `.mjs` runner — satisfying +the estate "no new TypeScript" policy end to end. + +*Known rough edges (non-blocking, flagged for the roadmap):* + +. The runtime prelude (~440 lines of host shims) is always emitted, even for + a pure module that calls none of it. Tree-shaking / on-demand emission + would shrink artefacts. +. `if/else` -> IIFE-ternary is correct but verbose; a future codegen pass + could emit flat `if` statements for statement-position branches. +. Only pure integer fns were trialed here. Struct/`impl` -> `export class` + and `extern fn` -> host-call lowering are documented by `--help` but NOT + exercised by this spike — a follow-up spike should confirm those export + shapes too before the harness migration relies on them. diff --git a/proposals/nextgen-evangelist/deno-esm-spike/driver.mjs b/proposals/nextgen-evangelist/deno-esm-spike/driver.mjs new file mode 100644 index 00000000..2aaffd88 --- /dev/null +++ b/proposals/nextgen-evangelist/deno-esm-spike/driver.mjs @@ -0,0 +1,40 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// +// driver.mjs -- the Deno-side consumer for the deno-esm-spike. Imports the +// AffineScript-compiled ES module (sample.js) and calls its exports, proving +// the TypeScript-0 path (roadmap ask #3): a parity / scan harness like this +// could be authored in AffineScript-compiled JS instead of hand-written TS. +// +// Run: deno run ./driver.mjs + +import { add, clamp_band } from "./sample.js"; + +let pass = 0; +let fail = 0; + +function check(label, got, want) { + const ok = got === want; + if (ok) { + pass += 1; + console.log(` ok ${label}: ${got}`); + } else { + fail += 1; + console.log(` FAIL ${label}: got ${got}, want ${want}`); + } +} + +console.log("deno-esm-spike driver: importing AffineScript-compiled ESM"); +console.log(` typeof add = ${typeof add}`); +console.log(` typeof clamp_band = ${typeof clamp_band}`); + +check("add(2, 3)", add(2, 3), 5); +check("add(-4, 4)", add(-4, 4), 0); +check("clamp_band(-7) [below band]", clamp_band(-7), 0); +check("clamp_band(2) [in band]", clamp_band(2), 2); +check("clamp_band(99) [above band]", clamp_band(99), 3); + +console.log(`\nresult: ${pass} passed, ${fail} failed`); +if (fail > 0) { + Deno.exit(1); +} diff --git a/proposals/nextgen-evangelist/deno-esm-spike/sample.affine b/proposals/nextgen-evangelist/deno-esm-spike/sample.affine new file mode 100644 index 00000000..960dad04 --- /dev/null +++ b/proposals/nextgen-evangelist/deno-esm-spike/sample.affine @@ -0,0 +1,28 @@ +// SPDX-License-Identifier: MPL-2.0 +// +// sample.affine -- minimal AffineScript source for the deno-esm-spike. Proves +// the AffineScript -> Deno-ESM -> TypeScript-0 path (roadmap ask #3): if a +// trivial pure module compiles to a runnable, importable Deno ES module, then +// parity / scan harnesses can be authored in AffineScript instead of TypeScript. +// +// Two public surfaces, both pure integer arithmetic (no extern, no host calls), +// so the only thing under test is the ESM *export shape*, not the host glue: +// - add : the canonical "does the export work" probe. +// - clamp_band : a tiny clamp onto 0..3, mirroring SecurityRank's band, so the +// driver exercises a branch too. + +pub fn add(a: Int, b: Int) -> Int { + a + b +} + +pub fn clamp_band(x: Int) -> Int { + if x < 0 { + 0 + } else { + if x > 3 { + 3 + } else { + x + } + } +} diff --git a/proposals/nextgen-evangelist/deno-esm-spike/sample.js b/proposals/nextgen-evangelist/deno-esm-spike/sample.js new file mode 100644 index 00000000..7b4b300e --- /dev/null +++ b/proposals/nextgen-evangelist/deno-esm-spike/sample.js @@ -0,0 +1,463 @@ +// Generated by AffineScript compiler (Deno-ESM target, issue #122) +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// SPDX-License-Identifier: MPL-2.0 +// ---- AffineScript Deno-ESM runtime ---- +const Some = (value) => ({ tag: "Some", value }); +const None = { tag: "None" }; +const Ok = (value) => ({ tag: "Ok", value }); +const Err = (error) => ({ tag: "Err", error }); +const Unit = null; +const print = (s) => { Deno.stdout.writeSync(new TextEncoder().encode(String(s))); }; +const println = (s) => { console.log(String(s)); }; +// ---- Deno host shims (extern fn lowering targets, issue #122) ---- +// Kept tiny + inlined so emitted modules are genuinely drop-in (no extra +// package to publish or resolve). The same surface is mirrored, for +// standalone `deno test`, by packages/affine-deno/mod.js. +const __as_ensureDir = (p) => { + try { Deno.mkdirSync(p, { recursive: true }); } + catch (e) { if (!(e instanceof Deno.errors.AlreadyExists)) throw e; } +}; +const __as_pathJoin = (a, b) => { + if (a.length === 0) return b; + const sep = a.endsWith("/") || a.endsWith("\\") ? "" : "/"; + return a + sep + b; +}; +const __as_readDirNames = (p) => { + const names = []; + for (const entry of Deno.readDirSync(p)) { + if (entry.isFile) names.push(entry.name); + } + return names; +}; +const __as_isNotFound = (e) => (e instanceof Deno.errors.NotFound); +const __as_walkRecursive = (root) => { + const out = []; + const rec = (dir) => { + for (const entry of Deno.readDirSync(dir)) { + const full = (dir.endsWith("/") ? dir : dir + "/") + entry.name; + if (entry.isFile) out.push(full); + else if (entry.isDirectory) rec(full); + } + }; + rec(root); + return out; +}; +const __as_regexMatch = (s, pat) => new RegExp(pat).test(String(s)); +const __as_wasmInstance = (bytes) => + new WebAssembly.Instance(new WebAssembly.Module(bytes)).exports; +const __as_wasmCall = (exports, name, args) => Number(exports[name](...(args || []))); +// ---- WasmValue (Deno.affine #455 — Tier 1 #5, Option B) ---- +// Opaque tagged value crossing the AS/JS boundary as `{ kind, v }`. +// `kind` is one of "i32" | "i64" | "f32" | "f64". The `v` payload is +// `BigInt` for i64 (preserves precision beyond 2^53), `Number` otherwise. +const __as_wv_i32 = (n) => ({ kind: "i32", v: (Number(n) | 0) }); +const __as_wv_i64 = (n) => ({ kind: "i64", v: BigInt(n) }); +const __as_wv_f32 = (f) => ({ kind: "f32", v: Math.fround(Number(f)) }); +const __as_wv_f64 = (f) => ({ kind: "f64", v: Number(f) }); +const __as_wv_as_int = (v) => { + if (v == null) return 0; + if (typeof v.v === "bigint") { + // i64: truncate to safe-integer Number; caller's responsibility for + // precision-sensitive paths (use wv_kind to detect). + return Number(v.v); + } + // i32 / f32 / f64: truncate toward zero per AS Int semantics. + return (Number(v.v) | 0); +}; +const __as_wv_as_float = (v) => { + if (v == null) return 0; + return typeof v.v === "bigint" ? Number(v.v) : Number(v.v); +}; +const __as_wv_kind = (v) => (v && typeof v.kind === "string") ? v.kind : ""; +const __as_wasm_export_call = (exports, name, args) => { + // Unmarshal AS-side [WasmValue] to raw JS scalars for the wasm call. + const rawArgs = (args || []).map((wv) => { + if (wv == null) return 0; + // i64 payload is BigInt; wasm i64 imports accept BigInt directly. + return wv.v; + }); + const result = exports[name](...rawArgs); + // Wrap return as f64 (lossless for any numeric; callers expecting i32/i64 + // can rebuild via wv_i32(wv_as_int(result)) or inspect wv_kind). + if (typeof result === "bigint") { + return { kind: "i64", v: result }; + } + return { kind: "f64", v: Number(result) }; +}; +// ---- motion (bindings #4): consumer-provided import ---- +// Host JS environment must expose globalThis.__as_motion (the motion +// library or a compatible mock). Tests set it in the harness before +// importing the generated module; production consumers typically do +// `import * as m from "motion"; globalThis.__as_motion = m;` once at +// module-init time. The AffineScript-side externs (stdlib/Motion.affine) +// don't see this indirection — they call __as_motion* helpers directly. +const __as_motionAnimate = (target, keyframes, options) => + globalThis.__as_motion.animate(target, keyframes, options); +const __as_motionAwait = (controls) => + Promise.resolve(controls).then(() => 0); +const __as_motionCancel = (controls) => { + if (controls && typeof controls.cancel === "function") controls.cancel(); + return 0; +}; +// `animateMini` / `tween` / `spring` / `ease` — bindings #4 follow-up +// surface. Each helper resolves the host method on globalThis.__as_motion +// at call time so a mock that only stubs a subset still works for the +// rest (the smoke harness exercises every variant). +const __as_motionAnimateMini = (target, keyframes, options) => + globalThis.__as_motion.animateMini(target, keyframes, options); +const __as_motionTween = (target, from, to, options) => + globalThis.__as_motion.tween(target, from, to, options); +const __as_motionSpring = (target, keyframes, springConfig) => + globalThis.__as_motion.spring(target, keyframes, springConfig); +const __as_motionEase = (name) => + globalThis.__as_motion.ease(name); +// ---- pixi.js (bindings #1): consumer-provided import ---- +// Host JS environment exposes globalThis.__as_pixi (the PIXI namespace +// from `import * as PIXI from "pixi.js"`). Tests set it in the harness +// before importing the generated module. +const __as_pixiAppInit = async (options) => { + const app = new globalThis.__as_pixi.Application(); + await app.init(options); + return app; +}; +const __as_pixiAppCanvas = (app) => app.canvas; +const __as_pixiAppStage = (app) => app.stage; +const __as_pixiAppTicker = (app) => app.ticker; +const __as_pixiAppDestroy = (app) => { app.destroy(); return 0; }; +const __as_pixiContainerNew = () => new globalThis.__as_pixi.Container(); +const __as_pixiContainerAddChild = (p, c) => { p.addChild(c); return 0; }; +const __as_pixiContainerRemoveChild = (p, c) => { p.removeChild(c); return 0; }; +const __as_pixiContainerSetPosition = (c, x, y) => { c.x = x; c.y = y; return 0; }; +const __as_pixiContainerSetScale = (c, x, y) => { c.scale.set(x, y); return 0; }; +const __as_pixiContainerSetPivot = (c, x, y) => { c.pivot.set(x, y); return 0; }; +const __as_pixiContainerSetRotation = (c, rad) => { c.rotation = rad; return 0; }; +const __as_pixiContainerSetAlpha = (c, a) => { c.alpha = a; return 0; }; +const __as_pixiContainerSetZIndex = (c, z) => { c.zIndex = z; return 0; }; +const __as_pixiContainerSetSortableChildren = (c, v) => { c.sortableChildren = v; return 0; }; +const __as_pixiContainerSetEventMode = (c, mode) => { c.eventMode = mode; return 0; }; +const __as_pixiContainerSetCursor = (c, cursor) => { c.cursor = cursor; return 0; }; +const __as_pixiContainerSetVisible = (c, v) => { c.visible = v; return 0; }; +const __as_pixiContainerOn = (c, event, handler) => { c.on(event, handler); return 0; }; +const __as_pixiContainerOff = (c, event, handler) => { c.off(event, handler); return 0; }; +const __as_pixiContainerDestroy = (c) => { c.destroy(); return 0; }; +const __as_pixiSpriteFrom = (t) => new globalThis.__as_pixi.Sprite(t); +const __as_pixiSpriteSetAnchor = (s, x, y) => { s.anchor.set(x, y); return 0; }; +// Upcasts are identity — PIXI's class hierarchy makes Sprite/Graphics/ +// Text actual Container subclasses, so the JS object is the same. +const __as_pixiSpriteAsContainer = (s) => s; +const __as_pixiTextureFromUrl = (url) => globalThis.__as_pixi.Texture.from(url); +const __as_pixiGraphicsNew = () => new globalThis.__as_pixi.Graphics(); +const __as_pixiGraphicsRect = (g, x, y, w, h) => { g.rect(x, y, w, h); return 0; }; +const __as_pixiGraphicsFill = (g, color) => { g.fill({ color }); return 0; }; +const __as_pixiGraphicsClear = (g) => { g.clear(); return 0; }; +const __as_pixiGraphicsAsContainer = (g) => g; +const __as_pixiTextNew = (options) => new globalThis.__as_pixi.Text(options); +const __as_pixiTextSetText = (t, content) => { t.text = content; return 0; }; +const __as_pixiTextAsContainer = (t) => t; +const __as_pixiTickerAdd = (t, cb) => { t.add(cb); return 0; }; +const __as_pixiTickerStart = (t) => { t.start(); return 0; }; +const __as_pixiTickerStop = (t) => { t.stop(); return 0; }; +// ---- @pixi/ui (bindings #3): consumer-provided import ---- +// Host JS environment exposes globalThis.__as_pixi_ui (the namespace +// from `import * as PixiUI from "@pixi/ui"`). Tests set it in the +// harness before importing the generated module; production +// consumers typically do once at module-init time. The +// AffineScript-side externs (stdlib/PixiUI.affine) don't see this +// indirection — they call __as_pixiUi* helpers directly. +// +// Upcasts to Container are identity — @pixi/ui's Button / +// FancyButton / Slider / Switch are all real PIXI.Container +// subclasses, so the JS object is the same. +const __as_pixiUiButtonNew = (options) => new globalThis.__as_pixi_ui.Button(options); +const __as_pixiUiButtonOnPress = (b, cb) => { b.onPress.connect(cb); return 0; }; +const __as_pixiUiButtonAsContainer = (b) => b; +const __as_pixiUiFancyButtonNew = (options) => new globalThis.__as_pixi_ui.FancyButton(options); +const __as_pixiUiFancyButtonAsContainer = (b) => b; +const __as_pixiUiSliderNew = (options) => new globalThis.__as_pixi_ui.Slider(options); +const __as_pixiUiSliderOnUpdate = (s, cb) => { s.onUpdate.connect(cb); return 0; }; +const __as_pixiUiSliderAsContainer = (s) => s; +const __as_pixiUiSwitchNew = (options) => new globalThis.__as_pixi_ui.Switch(options); +const __as_pixiUiSwitchOnChange = (sw, cb) => { sw.onChange.connect(cb); return 0; }; +const __as_pixiUiSwitchAsContainer = (sw) => sw; +// ---- @pixi/sound (bindings #2): consumer-provided import ---- +// Host JS environment exposes globalThis.__as_pixi_sound (the `Sound` +// named export from `@pixi/sound`). Tests set it in the harness before +// importing the generated module; production consumers typically do +// `import { Sound } from "@pixi/sound"; globalThis.__as_pixi_sound = Sound;` +// once at module-init time. The AffineScript-side externs +// (stdlib/PixiSound.affine) don't see this indirection — they call +// __as_pixiSound* helpers directly. +const __as_pixiSoundFrom = (url) => globalThis.__as_pixi_sound.from(url); +const __as_pixiSoundPlay = (s) => { s.play(); return 0; }; +const __as_pixiSoundStop = (s) => { s.stop(); return 0; }; +const __as_pixiSoundPause = (s) => { s.pause(); return 0; }; +const __as_pixiSoundResume = (s) => { s.resume(); return 0; }; +const __as_pixiSoundSetVolume = (s, vol) => { s.volume = vol; return 0; }; +const __as_pixiSoundSetLoop = (s, loop) => { s.loop = loop; return 0; }; +// ---- Ipc (bindings #9): web-platform MessageChannel/MessagePort ---- +// Uses standard web globals (MessageChannel, structuredClone) — no +// consumer-side init required. Available unmodified in Deno, Node 16+, +// browsers, and Web Workers. +const __as_messageChannelNew = () => new MessageChannel(); +const __as_messageChannelPort1 = (ch) => ch.port1; +const __as_messageChannelPort2 = (ch) => ch.port2; +const __as_messagePortPostMessage = (p, data) => { p.postMessage(data); return 0; }; +const __as_messagePortOnMessage = (p, handler) => { p.onmessage = handler; return 0; }; +const __as_messagePortStart = (p) => { p.start(); return 0; }; +const __as_messagePortClose = (p) => { p.close(); return 0; }; +const __as_targetPostMessage = (t, msg) => { t.postMessage(msg); return 0; }; +const __as_structuredCloneValue = (v) => structuredClone(v); +// ---- Canvas (bindings #8): HTML5 Canvas 2D rendering context ---- +// `canvas` arg is the consumer-supplied HTMLCanvasElement; helpers +// dispatch directly to the standard CanvasRenderingContext2D +// methods. Available unmodified in browsers, jsdom-under-Deno, +// idaptik's WebView host, and any DOM emulator. +const __as_canvasGetContext2D = (canvas) => canvas.getContext("2d"); +const __as_canvasFillStyle = (ctx, color) => { ctx.fillStyle = color; return 0; }; +const __as_canvasStrokeStyle = (ctx, color) => { ctx.strokeStyle = color; return 0; }; +const __as_canvasLineWidth = (ctx, w) => { ctx.lineWidth = w; return 0; }; +const __as_canvasGlobalAlpha = (ctx, a) => { ctx.globalAlpha = a; return 0; }; +const __as_canvasFillRect = (ctx, x, y, w, h) => { ctx.fillRect(x, y, w, h); return 0; }; +const __as_canvasStrokeRect = (ctx, x, y, w, h) => { ctx.strokeRect(x, y, w, h); return 0; }; +const __as_canvasClearRect = (ctx, x, y, w, h) => { ctx.clearRect(x, y, w, h); return 0; }; +const __as_canvasBeginPath = (ctx) => { ctx.beginPath(); return 0; }; +const __as_canvasClosePath = (ctx) => { ctx.closePath(); return 0; }; +const __as_canvasMoveTo = (ctx, x, y) => { ctx.moveTo(x, y); return 0; }; +const __as_canvasLineTo = (ctx, x, y) => { ctx.lineTo(x, y); return 0; }; +const __as_canvasArc = (ctx, x, y, r, s, e) => { ctx.arc(x, y, r, s, e); return 0; }; +const __as_canvasFill = (ctx) => { ctx.fill(); return 0; }; +const __as_canvasStroke = (ctx) => { ctx.stroke(); return 0; }; +const __as_canvasSave = (ctx) => { ctx.save(); return 0; }; +const __as_canvasRestore = (ctx) => { ctx.restore(); return 0; }; +const __as_canvasTranslate = (ctx, x, y) => { ctx.translate(x, y); return 0; }; +const __as_canvasRotate = (ctx, rad) => { ctx.rotate(rad); return 0; }; +const __as_canvasScale = (ctx, x, y) => { ctx.scale(x, y); return 0; }; +const __as_canvasFont = (ctx, font) => { ctx.font = font; return 0; }; +const __as_canvasTextAlign = (ctx, align) => { ctx.textAlign = align; return 0; }; +const __as_canvasTextBaseline = (ctx, baseline) => { ctx.textBaseline = baseline; return 0; }; +const __as_canvasFillText = (ctx, text, x, y) => { ctx.fillText(text, x, y); return 0; }; +const __as_canvasStrokeText = (ctx, text, x, y) => { ctx.strokeText(text, x, y); return 0; }; +const __as_canvasMeasureText = (ctx, text) => ctx.measureText(text); +const __as_canvasDrawImage = (ctx, img, x, y) => { ctx.drawImage(img, x, y); return 0; }; +const __as_canvasDrawImageScaled = (ctx, img, x, y, w, h) => { ctx.drawImage(img, x, y, w, h); return 0; }; +// `++` is overloaded (string concat / array concat); `a + b` would +// stringify arrays. Dispatch on shape so stdlib/string.affine's +// `result ++ [x]` and `a ++ b` are both correct. +const __as_concat = (a, b) => Array.isArray(a) ? a.concat(b) : (a + b); +// Honest host/runtime primitives underpinning the AffineScript-level +// stdlib/string.affine (its is_empty/starts_with/ends_with/split/join/ +// replace/... are real AffineScript on top of these). +const __as_strSub = (s, start, n) => String(s).slice(start, start + n); +const __as_strGet = (s, i) => String(s)[i]; +const __as_strFind = (s, n) => String(s).indexOf(n); +const __as_charToInt = (c) => String(c).codePointAt(0); +const __as_intToChar = (n) => String.fromCodePoint(n); +const __as_strCharCodeAt = (s, i) => (i >= 0 && i < s.length ? s.charCodeAt(i) : -1); +const __as_strFromCharCode = (n) => String.fromCharCode(n & 0xff); +const __as_parseInt = (s) => { + const n = parseInt(String(s), 10); + return Number.isNaN(n) ? None : Some(n); +}; +const __as_parseFloat = (s) => { + const n = parseFloat(String(s)); + return Number.isNaN(n) ? None : Some(n); +}; +const __as_show = (v) => (typeof v === "string" ? v : JSON.stringify(v)); +// ---- Http (issue #160): portable fetch round-trip ---- +// `headers` crosses the boundary as an AffineScript [(String, String)] +// assoc list == JS array of [name, value] pairs. `body` is an +// AffineScript Option == { tag: "Some", value } | { tag: "None" }. +// The result is the `Response` record shape { status, headers, body }. +const __as_httpHeadersToObject = (pairs) => { + const o = {}; + for (const kv of (pairs || [])) o[kv[0]] = kv[1]; + return o; +}; +const __as_httpHeadersFromResponse = (res) => { + const out = []; + res.headers.forEach((value, key) => out.push([key, value])); + return out; +}; +// ---- hpm-json-rsr Zig FFI shims (stdlib/json.affine v0.3) ---- +// `HpmJsonValue` is opaque to AffineScript; on Deno-ESM it's just the +// underlying JS value from JSON.parse. The shims mirror the sentinel +// conventions of the Zig exports so the AffineScript-side wrappers +// (`to_json`, `parse`) behave identically across backends. +const __as_hpmJsonParse = (s) => { + try { return Some(JSON.parse(String(s))); } catch (_e) { return None; } +}; +const __as_hpmJsonFree = (_v) => 0; +const __as_hpmJsonType = (v) => { + if (v === null || v === undefined) return 0; + if (typeof v === "boolean") return 1; + if (typeof v === "number") return Number.isInteger(v) ? 2 : 3; + if (typeof v === "string") return 4; + if (Array.isArray(v)) return 5; + if (typeof v === "object") return 6; + return -1; +}; +const __as_hpmJsonBool = (v) => (typeof v === "boolean" ? (v ? 1 : 0) : -1); +const __as_hpmJsonInt = (v) => + (typeof v === "number" ? Math.trunc(v) : Number.MIN_SAFE_INTEGER); +const __as_hpmJsonFloat = (v) => (typeof v === "number" ? v : NaN); +const __as_hpmJsonString = (v) => (typeof v === "string" ? v : ""); +const __as_hpmJsonObjectGet = (v, k) => { + if (v === null || typeof v !== "object" || Array.isArray(v)) return None; + return Object.prototype.hasOwnProperty.call(v, String(k)) + ? Some(v[String(k)]) : None; +}; +const __as_hpmJsonArrayLen = (v) => (Array.isArray(v) ? v.length : 0); +const __as_hpmJsonArrayGet = (v, i) => { + if (!Array.isArray(v)) return None; + const idx = Number(i); + return (idx >= 0 && idx < v.length) ? Some(v[idx]) : None; +}; +const __as_hpmJsonEscapeString = (s) => { + let out = ""; + const src = String(s); + for (let i = 0; i < src.length; i++) { + const c = src.charCodeAt(i); + if (c === 0x22) out += "\\\""; + else if (c === 0x5c) out += "\\\\"; + else if (c === 0x0a) out += "\\n"; + else if (c === 0x0d) out += "\\r"; + else if (c === 0x09) out += "\\t"; + else if (c === 0x08) out += "\\b"; + else if (c === 0x0c) out += "\\f"; + else if (c < 0x20) out += "\\u00" + c.toString(16).padStart(2, "0"); + else out += src[i]; + } + return out; +}; +// ---- Sqlite (db-theory #1a / stdlib/Sqlite.affine): SQL via host adapter ---- +// Host JS environment must expose globalThis.__as_sqlite, a namespace +// implementing the small adapter contract below. Consumers init once +// (Deno): +// import * as s from "jsr:@db/sqlite"; +// globalThis.__as_sqlite = { +// open: (p) => new s.Database(p), +// close: (db) => db.close(), +// execute: (db, sql) => db.exec(sql), +// query: (db, sql, params) => db.prepare(sql).all(...params), +// queryOne: (db, sql, params) => db.prepare(sql).get(...params), +// queryInt: (db, sql, params) => db.prepare(sql).value(...params), +// }; +// or (Node + better-sqlite3): adapt the same shape. The smoke harness +// installs an in-memory mock that implements the same contract. +// +// Parameter marshalling is intentionally simple: the AffineScript side +// hands the adapter a JSON-encoded `params` string (`"[]"` for none); +// rows + single-row results come back as JSON strings for caller-side +// decoding via `json::parse`. This matches the existing 6-extern +// stdlib/Sqlite.affine surface; richer typed bindings (prepared +// statements, schema introspection, bulk I/O) land in db-theory #1b. +const __as_dbOpen = (path) => globalThis.__as_sqlite.open(path); +const __as_dbClose = (h) => { globalThis.__as_sqlite.close(h); return 0; }; +const __as_dbExecute = (h, sql) => { globalThis.__as_sqlite.execute(h, sql); return 0; }; +const __as_dbQuery = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const rows = globalThis.__as_sqlite.query(h, sql, params); + return JSON.stringify(rows); +}; +const __as_dbQueryOne = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const row = globalThis.__as_sqlite.queryOne(h, sql, params); + return JSON.stringify(row); +}; +const __as_dbQueryInt = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const v = globalThis.__as_sqlite.queryInt(h, sql, params); + return Number(v) | 0; +}; +// ---- Sqlite prepared statements (db-theory #1b) ---- +// Layered on top of the convenience surface above. The host adapter +// gains nine extra methods (`prepare`, `bindInt`, `bindText`, `bindNull`, +// `step`, `columnCount`, `columnInt`, `columnText`, `reset`, `finalize`); +// the smoke harness's mock implements them, and both `jsr:@db/sqlite` +// and `better-sqlite3` provide direct one-line wrappers (each library +// already exposes a `prepare()` + iterator-style step + typed column +// accessors). Bind-index convention is sqlite3's 1-indexed; column-index +// convention is 0-indexed (matches both adapter libraries). +const __as_dbPrepare = (h, sql) => globalThis.__as_sqlite.prepare(h, sql); +const __as_dbBindInt = (s, idx, v) => { globalThis.__as_sqlite.bindInt(s, idx, v); return 0; }; +const __as_dbBindText = (s, idx, v) => { globalThis.__as_sqlite.bindText(s, idx, v); return 0; }; +const __as_dbBindNull = (s, idx) => { globalThis.__as_sqlite.bindNull(s, idx); return 0; }; +const __as_dbStep = (s) => (globalThis.__as_sqlite.step(s) ? 1 : 0); +const __as_dbColumnCount = (s) => Number(globalThis.__as_sqlite.columnCount(s)) | 0; +const __as_dbColumnInt = (s, idx) => { + const v = globalThis.__as_sqlite.columnInt(s, idx); + return v == null ? 0 : (Number(v) | 0); +}; +const __as_dbColumnText = (s, idx) => { + const v = globalThis.__as_sqlite.columnText(s, idx); + return v == null ? "" : String(v); +}; +const __as_dbReset = (s) => { globalThis.__as_sqlite.reset(s); return 0; }; +const __as_dbFinalize = (s) => { globalThis.__as_sqlite.finalize(s); return 0; }; +// ---- Sqlite schema introspection + bulk I/O + error inspection (db-theory #1c) ---- +// Five more adapter methods (`schemaTables`, `schemaColumns`, +// `tableExists`, `importCsv`, `exportCsv`, `lastError`); each +// real-world adapter (jsr:@db/sqlite, better-sqlite3) backs them with +// a one-liner over `PRAGMA table_info` / a `Database.prepare()` +// iterator / a `fs.writeFileSync(..., csv)` call. +const __as_dbSchemaTables = (h) => String(globalThis.__as_sqlite.schemaTables(h)); +const __as_dbSchemaColumns = (h, table) => String(globalThis.__as_sqlite.schemaColumns(h, table)); +const __as_dbTableExists = (h, table) => Boolean(globalThis.__as_sqlite.tableExists(h, table)); +const __as_dbImportCsv = (h, table, path, hasHeader) => + Number(globalThis.__as_sqlite.importCsv(h, table, path, Boolean(hasHeader))) | 0; +const __as_dbExportCsv = (h, sql, paramsJson, path) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + return Number(globalThis.__as_sqlite.exportCsv(h, sql, params, path)) | 0; +}; +const __as_dbLastError = (h) => { + const v = globalThis.__as_sqlite.lastError(h); + return v == null ? "" : String(v); +}; +// ---- Sqlite transactions (db-theory #2) ---- +// `Tx` is an opaque handle; the host adapter is required to +// invalidate it on `commit` / `rollback` so that subsequent calls +// throw a host-side `Error` (the affine type system's +// at-most-one-use guarantee is enforced statically on the AS side; +// this host invariant catches FFI-side aliasing bugs in tests). +const __as_txBegin = (h) => globalThis.__as_sqlite.txBegin(h); +const __as_txCommit = (t) => { globalThis.__as_sqlite.txCommit(t); return 0; }; +const __as_txRollback = (t) => { globalThis.__as_sqlite.txRollback(t); return 0; }; +const __as_txSavepoint = (t, n) => { globalThis.__as_sqlite.txSavepoint(t, n); return 0; }; +const __as_txRelease = (t, n) => { globalThis.__as_sqlite.txRelease(t, n); return 0; }; +const __as_txRollbackTo = (t, n) => { globalThis.__as_sqlite.txRollbackTo(t, n); return 0; }; +const __as_txDb = (t) => globalThis.__as_sqlite.txDb(t); +const __as_txIsLive = (t) => (globalThis.__as_sqlite.txIsLive(t) ? 1 : 0); +// ---- Sqlite aggregation (db-theory #3 / stdlib/Aggregate.affine) ---- +// Each scalar aggregator delegates to a host adapter method that runs +// the SQL, expects a single-row result, and unwraps column 0. `groupBy` +// / `groupCount` return JSON strings (caller parses). +const __as_dbCount = (h, sql, params) => Number(globalThis.__as_sqlite.aggCount(h, sql, params)) | 0; +const __as_dbSum = (h, sql, params) => Number(globalThis.__as_sqlite.aggSum(h, sql, params)) | 0; +const __as_dbMinInt = (h, sql, params) => Number(globalThis.__as_sqlite.aggMinInt(h, sql, params)) | 0; +const __as_dbMaxInt = (h, sql, params) => Number(globalThis.__as_sqlite.aggMaxInt(h, sql, params)) | 0; +const __as_dbAvg = (h, sql, params) => Number(globalThis.__as_sqlite.aggAvg(h, sql, params)); +const __as_dbGroupBy = (h, sql, params) => String(globalThis.__as_sqlite.groupBy(h, sql, params)); +const __as_dbGroupCount = (h, table, keyCol) => String(globalThis.__as_sqlite.groupCount(h, table, keyCol)); +const __as_httpFetch = async (url, method, headers, bodyOpt) => { + const init = { method, headers: __as_httpHeadersToObject(headers) }; + if (bodyOpt && bodyOpt.tag === "Some") init.body = bodyOpt.value; + // `globalThis.fetch` explicitly: the stdlib `Http.fetch` compiles to a + // module-level `function fetch`, which would otherwise shadow the host. + const res = await globalThis.fetch(url, init); + const text = await res.text(); + return { + status: res.status, + headers: __as_httpHeadersFromResponse(res), + body: text, + }; +}; +// ---- end runtime ---- + +export function add(a, b) { + return (a + b); +} + +export function clamp_band(x) { + return ((x < 0) ? (() => { return 0; })() : (() => { return ((x > 3) ? (() => { return 3; })() : (() => { return x; })()); })()); +} + diff --git a/proposals/nextgen-evangelist/echo-boundary/README.adoc b/proposals/nextgen-evangelist/echo-boundary/README.adoc new file mode 100644 index 00000000..5d41a402 --- /dev/null +++ b/proposals/nextgen-evangelist/echo-boundary/README.adoc @@ -0,0 +1,203 @@ +// SPDX-License-Identifier: MPL-2.0 += echo-boundary +:toc: macro +:icons: font + +A runnable tool that turns the AffineScript `@boundary` *encoding-faithfulness +obligation* into a *machine-checked* check. + +toc::[] + +== What it is + +When a host-side enumerated / stringly-typed value (a 4-element security rank +`Open/Weak/Medium/Strong`, a device-port name, ...) is encoded to an integer +and a pure integer kernel (e.g. a wasm kernel) computes on that integer, the +migration slogan is *"the integer IS the host value."* That slogan is exactly +an encode-faithfulness question on the encoder `enc : Source -> Code`: + +* *Lossless* iff the codes are pairwise distinct (the encoder is injective). + Then the integer faithfully names the host value -- every code determines its + source uniquely. +* *Controlled loss* iff two distinct names map to the same code (a collision / + clamp). Then *no section* exists: there is no pure `decode : Code -> Source` + recovering the host value from the integer. The lost distinction is named and + localised at the colliding code -- the classic "default a bad input to 0 / + `Open`" clamp bug. + +`echo-boundary` reads an *encoding table* (`{name: integer-code}`), decides the +verdict, then *generates a self-contained Agda module that proves that verdict* +by reusing the existing `EchoEncodingFaithfulness` framework, and *typechecks +it*. `agda` exit 0 means the verdict is certified, not merely asserted. + +The generated modules copy the SHAPE of the framework's worked +`Rank`/`rankCode`/`rankCode-injective` instance: + +* *Lossless* -> `data Host`, `code : Host -> ℕ`, a diagonal `refl`-per-constructor + `code-injective` (Agda's coverage discharges the off-diagonal absurd numeral + cases), an `Encoding` record, and the re-exported `encoding-lossless` headline. +* *Controlled loss* -> the enum + code fn, the two colliding constructors + exhibited as data, and `encoding-collision⇒no-section` invoked to obtain the + certified no-section (controlled-loss) witness. + +== Requirements + +* `deno` on PATH (the tool is plain JavaScript -- TypeScript is banned + estate-wide). +* `agda` (2.6.3 here) with `standard-library` on the library path. +* The echo *mirror* repo at `/tmp/mirror-boundary` (override with `--mirror`), + containing `proofs/agda/EchoEncodingFaithfulness.agda` and its dependencies. + The generated module is written into `proofs/agda/.agda` and typechecked + from there so it can `open import` the framework. + +== Usage + +[source,sh] +---- +# Table on argv: +deno run --allow-read --allow-write --allow-run --allow-env \ + boundary.mjs '{"Open":0,"Weak":1,"Medium":2,"Strong":3}' + +# Table (with a clamp spec) on stdin: +echo '{"table":{"Open":0,"Weak":1,"Medium":2,"Strong":3},"clamp":{"OOB":0}}' \ + | deno run --allow-read --allow-write --allow-run --allow-env boundary.mjs +---- + +Input forms: + +* *Bare table*: `{"Open":0,"Weak":1,"Medium":2,"Strong":3}`. +* *With clamp*: `{"table":{...},"clamp":{"OOB":0}}`. The `clamp` entries are + merged into the table; an out-of-band name (`OOB`) that shares a code with a + valid name is the canonical clamp bug. (Clamp vs. table is purely a + presentation distinction -- the faithfulness logic treats every entry + uniformly, so a collision between two ordinary table names is detected too.) + +Flags: + +[cols="1,3"] +|=== +| `--name ` | generated Agda module name (default `BoundaryLossless` / + `BoundaryControlledLoss`) +| `--mirror ` | echo mirror repo (default `/tmp/mirror-boundary`) +| `--out ` | also write the generated `.agda` to this path +| `--no-check` | generate only; do not invoke `agda` +| `--help` | usage +|=== + +Exit code: `0` if the verdict's proof typechecks, `1` if `agda` rejects the +generated module, `2` on bad input, `3` if `agda` could not be run. + +== Trial runs (captured) + +Both trials were run on 2026-06-04 against the mirror at `/tmp/mirror-boundary` +(Agda 2.6.3, stdlib 2.3). The generated, verified modules are saved under +`samples/`. + +=== Trial 1 -- SecurityRank table -> LOSSLESS + +Command: + +[source,sh] +---- +deno run --allow-read --allow-write --allow-run --allow-env \ + boundary.mjs '{"Open":0,"Weak":1,"Medium":2,"Strong":3}' --name BoundaryLossless +---- + +Output: + +---- +verdict: LOSSLESS + names: 4 + codes: 0, 1, 2, 3 + module: BoundaryLossless + agda: exit 0 (wrote /tmp/mirror-boundary/proofs/agda/BoundaryLossless.agda) + PROOF HOLDS: encoder injective -> boundary is lossless (the integer IS the host value). +---- + +Independent re-typecheck of the generated module: + +[source,sh] +---- +cd /tmp/mirror-boundary && LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/BoundaryLossless.agda +# AGDA_EXIT=0 +---- + +Generated module: `samples/BoundaryLossless.agda`. The headline proved is +`boundary-lossless : (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂` +(every integer code determines its host value uniquely), via the framework's +`encoding-lossless` and a diagonal `code-injective`. + +=== Trial 2 -- clamping table that collides -> CONTROLLED LOSS + +Command (input on stdin): + +[source,sh] +---- +echo '{"table":{"Open":0,"Weak":1,"Medium":2,"Strong":3},"clamp":{"OOB":0}}' \ + | deno run --allow-read --allow-write --allow-run --allow-env \ + boundary.mjs --name BoundaryControlledLoss +---- + +Output: + +---- +verdict: CONTROLLED LOSS + names: 5 + codes: 0, 1, 2, 3 + collision at code 0: "Open" and "OOB" + module: BoundaryControlledLoss + agda: exit 0 (wrote /tmp/mirror-boundary/proofs/agda/BoundaryControlledLoss.agda) + PROOF HOLDS: code collision -> no section -> controlled loss is certified. +---- + +Independent re-typecheck of the generated module: + +[source,sh] +---- +cd /tmp/mirror-boundary && LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/BoundaryControlledLoss.agda +# AGDA_EXIT=0 +---- + +Generated module: `samples/BoundaryControlledLoss.agda`. The clamp value `OOB` +collides with `Open` on the sentinel code `0`; the headline proved is +`boundary-controlled-loss : ¬ Σ (ℕ → Host) (λ decode → ∀ x → decode (code x) ≡ x)` +(no integer-to-host recovery type-checks), via the framework's +`encoding-collision⇒no-section`. + +== Files + +[cols="1,3"] +|=== +| `boundary.mjs` | the tool (Deno / plain JavaScript) +| `README.adoc` | this file +| `samples/BoundaryLossless.agda` | generated + verified lossless proof (Trial 1) +| `samples/BoundaryControlledLoss.agda` | generated + verified controlled-loss proof (Trial 2) +|=== + +== Scope / honest bounds + +This is a *type-level* faithfulness check, inheriting the +`EchoEncodingFaithfulness` `NotProved-*` discipline: + +* It certifies the encoder *table* is injective (lossless) or has a localised + collision (controlled loss). It says *nothing* about whether the deployed + runtime bit-for-bit implements that encoder -- that is the differential-parity + harness's job. +* `Code` is modelled as Agda `ℕ`. A real fixed-width integer type could + re-introduce collisions (overflow / truncation) that a `ℕ` model never sees, + so a lossless verdict is about the *table as given*, not about any particular + integer width. + +== Implementation note (Agda generation) + +The lossless injectivity proof uses the *finite-enum diagonal form* -- one +`code-injective {cN} {cN} _ = refl` clause per constructor, exactly as the +framework's `rankCode-injective` does. This is sound *because* every `code` +clause maps its constructor to a literal `ℕ` numeral, so Agda's coverage checker +discharges every off-diagonal pair as an absurd numeral equality (e.g. `0 ≡ 1`) +without the generator having to enumerate them. A fully general +`Injective`-for-arbitrary-codomain proof is *not* attempted; the diagonal form +is both what the framework uses and what is robust to generate for any finite +table. No generation obstruction was hit -- both verdict shapes typecheck +straight off the framework's worked instances, including non-clamp collisions +(two ordinary table names sharing a code) and clamp collisions alike. diff --git a/proposals/nextgen-evangelist/echo-boundary/boundary.mjs b/proposals/nextgen-evangelist/echo-boundary/boundary.mjs new file mode 100644 index 00000000..407a20cc --- /dev/null +++ b/proposals/nextgen-evangelist/echo-boundary/boundary.mjs @@ -0,0 +1,468 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// +// echo-boundary: turn the @boundary encoding-faithfulness obligation into +// a machine-checked check. Given an encoding table (host name -> integer +// code), decide whether the boundary is LOSSLESS (the codes are pairwise +// distinct, so the integer faithfully names the host value) or CONTROLLED +// LOSS (two distinct names collide on one code, e.g. a clamp/sentinel), +// then GENERATE a self-contained Agda module that PROVES that verdict by +// reusing the existing EchoEncodingFaithfulness framework, and TYPECHECK +// it (agda exit 0 = the verdict is certified). +// +// This is a Deno tool. Run as plain JavaScript (TypeScript is banned +// estate-wide). No network access is used. +// +// deno run --allow-read --allow-write --allow-run --allow-env \ +// boundary.mjs '{"Open":0,"Weak":1,"Medium":2,"Strong":3}' +// +// echo '{"table":{"Open":0,"Weak":1,"Medium":2,"Strong":3},"clamp":{"OOB":0}}' \ +// | deno run --allow-read --allow-write --allow-run --allow-env boundary.mjs +// +// Flags: +// --name name of the generated Agda module (default auto) +// --mirror path to the echo mirror repo +// (default /tmp/mirror-boundary) +// --out also write the generated .agda to this path +// --no-check generate only; do not invoke agda +// --help + +// --------------------------------------------------------------------------- +// Argument / input handling +// --------------------------------------------------------------------------- + +function parseArgs(argv) { + const opts = { + name: null, + mirror: "/tmp/mirror-boundary", + out: null, + check: true, + json: null, + }; + const positional = []; + for (let i = 0; i < argv.length; i++) { + const a = argv[i]; + if (a === "--help" || a === "-h") { + opts.help = true; + } else if (a === "--no-check") { + opts.check = false; + } else if (a === "--name") { + opts.name = argv[++i]; + } else if (a === "--mirror") { + opts.mirror = argv[++i]; + } else if (a === "--out") { + opts.out = argv[++i]; + } else { + positional.push(a); + } + } + if (positional.length > 0) opts.json = positional.join(" "); + return opts; +} + +async function readStdin() { + const chunks = []; + const buf = new Uint8Array(4096); + while (true) { + const n = await Deno.stdin.read(buf); + if (n === null) break; + chunks.push(buf.slice(0, n)); + } + const total = chunks.reduce((s, c) => s + c.length, 0); + const out = new Uint8Array(total); + let off = 0; + for (const c of chunks) { + out.set(c, off); + off += c.length; + } + return new TextDecoder().decode(out).trim(); +} + +const HELP = `echo-boundary — machine-check the @boundary encoding-faithfulness obligation + +USAGE + boundary.mjs '' table on argv + echo '' | boundary.mjs table on stdin + +INPUT + Bare table: {"Open":0,"Weak":1,"Medium":2,"Strong":3} + With clamp: {"table":{...},"clamp":{"OOB":0}} + (clamp entries are merged into the table; an OOB name that + shares a code with a valid name is the canonical clamp bug) + +VERDICT + LOSSLESS codes pairwise distinct (encoder injective) + CONTROLLED LOSS two distinct names share a code (collision / clamp) + +For each verdict a self-contained Agda module is generated against the +EchoEncodingFaithfulness framework and typechecked (agda exit 0 = certified). + +FLAGS + --name generated Agda module name (default auto) + --mirror echo mirror repo (default /tmp/mirror-boundary) + --out also write the generated .agda here + --no-check generate only, skip agda + --help +`; + +// --------------------------------------------------------------------------- +// Table normalisation +// --------------------------------------------------------------------------- + +// Accept either a bare {name: code} object or {table:{...}, clamp:{...}}. +// Returns an ordered array of {name, code, oob} entries. `oob` marks entries +// that arrived via the clamp spec (purely informational for the report; the +// faithfulness logic treats every entry uniformly). +function normalizeTable(raw) { + let table; + let clamp = {}; + if (raw && typeof raw === "object" && !Array.isArray(raw) && + Object.prototype.hasOwnProperty.call(raw, "table")) { + table = raw.table; + clamp = raw.clamp || {}; + } else { + table = raw; + } + if (!table || typeof table !== "object" || Array.isArray(table)) { + throw new Error("table must be a JSON object of {name: integer-code}"); + } + const entries = []; + const seenNames = new Set(); + for (const [name, code] of Object.entries(table)) { + checkEntry(name, code, seenNames); + entries.push({ name, code, oob: false }); + } + for (const [name, code] of Object.entries(clamp)) { + checkEntry(name, code, seenNames); + entries.push({ name, code, oob: true }); + } + if (entries.length === 0) throw new Error("table is empty"); + return entries; +} + +function checkEntry(name, code, seenNames) { + if (seenNames.has(name)) { + // JSON objects can't have duplicate keys after parse, but a clamp name + // could shadow a table name; that's a genuine spec error. + throw new Error(`duplicate name in table: ${JSON.stringify(name)}`); + } + seenNames.add(name); + if (typeof code !== "number" || !Number.isInteger(code)) { + throw new Error(`code for ${JSON.stringify(name)} must be an integer`); + } + if (code < 0) { + throw new Error( + `code for ${JSON.stringify(name)} is negative (${code}); ` + + `codes are encoded as Agda ℕ literals, so must be ≥ 0`, + ); + } +} + +// --------------------------------------------------------------------------- +// Verdict +// --------------------------------------------------------------------------- + +// Lossless iff codes pairwise distinct. Otherwise find a witnessing +// collision: the first two distinct names sharing one code. +function decide(entries) { + const byCode = new Map(); + for (const e of entries) { + if (!byCode.has(e.code)) byCode.set(e.code, []); + byCode.get(e.code).push(e); + } + for (const [code, group] of byCode) { + if (group.length >= 2) { + return { + lossless: false, + collision: { code, a: group[0], b: group[1], group }, + }; + } + } + return { lossless: true, collision: null }; +} + +// --------------------------------------------------------------------------- +// Agda identifier safety +// --------------------------------------------------------------------------- + +// Map each entry to a guaranteed-safe Agda constructor name. We use indexed +// `cN` constructors rather than the host names directly, which sidesteps every +// hazard at once: Agda keywords (`open`, `data`, `where`, ...), names with +// spaces / punctuation / non-ASCII, and names that collide after sanitisation. +// The original host name is preserved in a comment on each constructor. +function assignCtors(entries) { + return entries.map((e, i) => ({ ...e, ctor: `c${i}` })); +} + +function moduleNameFor(entries, verdict, explicit) { + if (explicit) return explicit; + return verdict.lossless ? "BoundaryLossless" : "BoundaryControlledLoss"; +} + +// Escape a host name for safe inclusion inside an Agda line comment. +function commentSafe(s) { + return String(s).replace(/[\r\n]/g, " "); +} + +// --------------------------------------------------------------------------- +// Agda code generation +// --------------------------------------------------------------------------- + +const GEN_HEADER = (modName, srcJson) => + `{-# 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): +${srcJson.split("\n").map((l) => "-- " + l).join("\n")} + +module ${modName} 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 (¬_) +`; + +function genEnum(modName, entries) { + const ctorList = entries.map((e) => e.ctor).join(" "); + const lines = []; + lines.push("-- The host-side enumerated value (one constructor per table name)."); + for (const e of entries) { + lines.push(`-- ${e.ctor} = ${commentSafe(e.name)}` + + (e.oob ? " (out-of-band / clamp entry)" : "")); + } + lines.push(`data Host : Set where`); + lines.push(` ${ctorList} : Host`); + return lines.join("\n"); +} + +function genCode(entries) { + const lines = []; + lines.push("-- The integer code the pure kernel computes on."); + lines.push("code : Host → ℕ"); + // Align the arrows for readability. + const w = Math.max(...entries.map((e) => e.ctor.length)); + for (const e of entries) { + lines.push(`code ${e.ctor.padEnd(w)} = ${e.code}`); + } + return lines.join("\n"); +} + +// Lossless: diagonal-only injectivity (exactly like rankCode-injective). +// This is sound BECAUSE every `code` clause maps to a literal ℕ numeral, so +// Agda's coverage checker discharges every off-diagonal pair as an absurd +// numeral equality (e.g. 0 ≡ 1) without us listing it. See the note in +// EchoEncodingFaithfulness.agda lines ~369-371. We emit only the diagonal. +function genLosslessProof(modName, entries) { + const w = Math.max(...entries.map((e) => e.ctor.length)); + const lines = []; + lines.push("-- Injectivity by exhaustive case analysis. The codes are literal"); + lines.push("-- numerals, so listing the diagonal refl clauses is enough: Agda's"); + lines.push("-- coverage checker discharges the off-diagonal pairs as absurd"); + lines.push("-- numeral equalities (mirrors rankCode-injective)."); + lines.push("code-injective : Injective code"); + for (const e of entries) { + const pat = `{${e.ctor}}`.padEnd(w + 2); + lines.push(`code-injective ${pat} ${pat} _ = refl`); + } + lines.push(""); + lines.push("encoding : Encoding"); + lines.push("encoding = record"); + lines.push(" { Source = Host"); + lines.push(" ; Code = ℕ"); + lines.push(" ; enc = code"); + lines.push(" }"); + lines.push(""); + lines.push("-- Re-export the lossless-half headline, instantiated and proved:"); + lines.push("-- every integer code determines its host value uniquely."); + lines.push("module Theorems = EncodingTheorems encoding"); + lines.push(""); + lines.push("boundary-lossless :"); + lines.push(" (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂"); + lines.push("boundary-lossless = Theorems.encoding-lossless code-injective"); + return lines.join("\n"); +} + +// Controlled loss: exhibit the two colliding constructors and invoke +// encoding-collision⇒no-section (exactly like clamp-sentinel-no-section). +function genLossyProof(modName, entries, collision) { + const a = collision.a; + const b = collision.b; + const lines = []; + lines.push("encoding : Encoding"); + lines.push("encoding = record"); + lines.push(" { Source = Host"); + lines.push(" ; Code = ℕ"); + lines.push(" ; enc = code"); + lines.push(" }"); + lines.push(""); + lines.push("module Theorems = EncodingTheorems encoding"); + lines.push(""); + lines.push(`-- The collision, as data: two distinct host values collapse onto the`); + lines.push(`-- same code ${collision.code}.`); + lines.push(`-- ${a.ctor} = ${commentSafe(a.name)}` + + (a.oob ? " (out-of-band / clamp)" : "")); + lines.push(`-- ${b.ctor} = ${commentSafe(b.name)}` + + (b.oob ? " (out-of-band / clamp)" : "")); + lines.push(`-- Distinctness is constructor disjointness; the shared code is refl.`); + lines.push(`${a.ctor}≢${b.ctor} : ${a.ctor} ≢ ${b.ctor}`); + lines.push(`${a.ctor}≢${b.ctor} ()`); + lines.push(""); + lines.push(`collision : ${a.ctor} ≢ ${b.ctor} × code ${a.ctor} ≡ code ${b.ctor}`); + lines.push(`collision = ${a.ctor}≢${b.ctor} , refl`); + lines.push(""); + lines.push("-- THE VERDICT, certified: the boundary exhibits controlled loss."); + lines.push("-- The colliding fibre admits NO section -- there is no pure"); + lines.push("-- decode : ℕ → Host recovering the host value from its code,"); + lines.push("-- because two distinct host values share one code. The lost"); + lines.push(`-- distinction is named and localised at code ${collision.code}.`); + lines.push("boundary-controlled-loss :"); + lines.push(" ¬ Σ (ℕ → Host) (λ decode → ∀ x → decode (code x) ≡ x)"); + lines.push("boundary-controlled-loss ="); + lines.push(" Theorems.encoding-collision⇒no-section"); + lines.push(` ${a.ctor} ${b.ctor}`); + lines.push(` ${a.ctor}≢${b.ctor}`); + lines.push(" refl"); + return lines.join("\n"); +} + +function generateAgda(modName, entries, verdict, srcJson) { + const parts = [ + GEN_HEADER(modName, srcJson), + genEnum(modName, entries), + genCode(entries), + verdict.lossless + ? genLosslessProof(modName, entries) + : genLossyProof(modName, entries, verdict.collision), + "", + ]; + return parts.join("\n\n"); +} + +// --------------------------------------------------------------------------- +// Typecheck driver +// --------------------------------------------------------------------------- + +async function typecheck(mirror, modName, source) { + const agdaDir = `${mirror}/proofs/agda`; + const modPath = `${agdaDir}/${modName}.agda`; + await Deno.writeTextFile(modPath, source); + const cmd = new Deno.Command("agda", { + args: ["-i", "proofs/agda", `proofs/agda/${modName}.agda`], + cwd: mirror, + env: { LC_ALL: "C.UTF-8" }, + stdout: "piped", + stderr: "piped", + }); + const { code, stdout, stderr } = await cmd.output(); + const out = new TextDecoder().decode(stdout) + + new TextDecoder().decode(stderr); + return { exit: code, output: out.trim(), modPath }; +} + +// --------------------------------------------------------------------------- +// Main +// --------------------------------------------------------------------------- + +async function main() { + const opts = parseArgs(Deno.args); + if (opts.help) { + console.log(HELP); + return 0; + } + let jsonText = opts.json; + if (!jsonText) jsonText = await readStdin(); + if (!jsonText) { + console.error("error: no input table (pass JSON on argv or stdin; --help)"); + return 2; + } + + let raw; + try { + raw = JSON.parse(jsonText); + } catch (e) { + console.error(`error: input is not valid JSON: ${e.message}`); + return 2; + } + + let entries; + try { + entries = normalizeTable(raw); + } catch (e) { + console.error(`error: ${e.message}`); + return 2; + } + + entries = assignCtors(entries); + const verdict = decide(entries); + const modName = moduleNameFor(entries, verdict, opts.name); + + // Pretty-print the normalised table back for the generated-module banner. + const tableForBanner = {}; + for (const e of entries) tableForBanner[e.name] = e.code; + const srcJson = JSON.stringify(tableForBanner, null, 2); + + const source = generateAgda(modName, entries, verdict, srcJson); + + // Report the verdict to the human. + const label = verdict.lossless ? "LOSSLESS" : "CONTROLLED LOSS"; + console.log(`verdict: ${label}`); + console.log(` names: ${entries.length}`); + console.log(` codes: ${[...new Set(entries.map((e) => e.code))].sort((a, b) => a - b).join(", ")}`); + if (!verdict.lossless) { + const c = verdict.collision; + console.log(` collision at code ${c.code}: ${JSON.stringify(c.a.name)} and ${JSON.stringify(c.b.name)}`); + } + console.log(` module: ${modName}`); + + if (opts.out) { + await Deno.writeTextFile(opts.out, source); + console.log(` wrote: ${opts.out}`); + } + + if (!opts.check) { + if (!opts.out) { + // Still surface the generated source on stdout when not checking. + console.log("\n----- generated Agda -----"); + console.log(source); + } + return 0; + } + + // Typecheck. + let tc; + try { + tc = await typecheck(opts.mirror, modName, source); + } catch (e) { + console.error(`error: could not run agda: ${e.message}`); + return 3; + } + console.log(` agda: exit ${tc.exit} (wrote ${tc.modPath})`); + if (tc.exit === 0) { + console.log(verdict.lossless + ? " PROOF HOLDS: encoder injective -> boundary is lossless (the integer IS the host value)." + : " PROOF HOLDS: code collision -> no section -> controlled loss is certified."); + } else { + console.log(" PROOF FAILED to typecheck; agda output:"); + console.log(tc.output); + } + return tc.exit === 0 ? 0 : 1; +} + +if (import.meta.main) { + Deno.exit(await main()); +} diff --git a/proposals/nextgen-evangelist/echo-boundary/samples/BoundaryControlledLoss.agda b/proposals/nextgen-evangelist/echo-boundary/samples/BoundaryControlledLoss.agda new file mode 100644 index 00000000..854261e5 --- /dev/null +++ b/proposals/nextgen-evangelist/echo-boundary/samples/BoundaryControlledLoss.agda @@ -0,0 +1,83 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "Open": 0, +-- "Weak": 1, +-- "Medium": 2, +-- "Strong": 3, +-- "OOB": 0 +-- } + +module BoundaryControlledLoss where + +open import Echo using (Echo) +open import EchoImageFactorization using (Injective) +open import EchoEncodingFaithfulness using (Encoding; module EncodingTheorems) + +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl) +open import Relation.Nullary using (¬_) + + +-- The host-side enumerated value (one constructor per table name). +-- c0 = Open +-- c1 = Weak +-- c2 = Medium +-- c3 = Strong +-- c4 = OOB (out-of-band / clamp entry) +data Host : Set where + c0 c1 c2 c3 c4 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 +code c4 = 0 + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +module Theorems = EncodingTheorems encoding + +-- The collision, as data: two distinct host values collapse onto the +-- same code 0. +-- c0 = Open +-- c4 = OOB (out-of-band / clamp) +-- Distinctness is constructor disjointness; the shared code is refl. +c0≢c4 : c0 ≢ c4 +c0≢c4 () + +collision : c0 ≢ c4 × code c0 ≡ code c4 +collision = c0≢c4 , refl + +-- THE VERDICT, certified: the boundary exhibits controlled loss. +-- The colliding fibre admits NO section -- there is no pure +-- decode : ℕ → Host recovering the host value from its code, +-- because two distinct host values share one code. The lost +-- distinction is named and localised at code 0. +boundary-controlled-loss : + ¬ Σ (ℕ → Host) (λ decode → ∀ x → decode (code x) ≡ x) +boundary-controlled-loss = + Theorems.encoding-collision⇒no-section + c0 c4 + c0≢c4 + refl + diff --git a/proposals/nextgen-evangelist/echo-boundary/samples/BoundaryLossless.agda b/proposals/nextgen-evangelist/echo-boundary/samples/BoundaryLossless.agda new file mode 100644 index 00000000..0db1bf17 --- /dev/null +++ b/proposals/nextgen-evangelist/echo-boundary/samples/BoundaryLossless.agda @@ -0,0 +1,72 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- GENERATED by echo-boundary (boundary.mjs). Do not edit by hand. +-- +-- This module certifies an @boundary encoding-faithfulness verdict for a +-- concrete host-value -> integer-code table, by reusing the +-- EchoEncodingFaithfulness framework. It follows the SHAPE of that module's +-- worked Rank / rankCode / rankCode-injective instance. +-- +-- Source table (host name -> code): +-- { +-- "Open": 0, +-- "Weak": 1, +-- "Medium": 2, +-- "Strong": 3 +-- } + +module BoundaryLossless where + +open import Echo using (Echo) +open import EchoImageFactorization using (Injective) +open import EchoEncodingFaithfulness using (Encoding; module EncodingTheorems) + +open import Data.Nat.Base using (ℕ) +open import Data.Product.Base using (Σ; _,_; _×_; proj₁) +open import Relation.Binary.PropositionalEquality + using (_≡_; _≢_; refl) +open import Relation.Nullary using (¬_) + + +-- The host-side enumerated value (one constructor per table name). +-- c0 = Open +-- c1 = Weak +-- c2 = Medium +-- c3 = Strong +data Host : Set where + c0 c1 c2 c3 : Host + +-- The integer code the pure kernel computes on. +code : Host → ℕ +code c0 = 0 +code c1 = 1 +code c2 = 2 +code c3 = 3 + +-- Injectivity by exhaustive case analysis. The codes are literal +-- numerals, so listing the diagonal refl clauses is enough: Agda's +-- coverage checker discharges the off-diagonal pairs as absurd +-- numeral equalities (mirrors rankCode-injective). +code-injective : Injective code +code-injective {c0} {c0} _ = refl +code-injective {c1} {c1} _ = refl +code-injective {c2} {c2} _ = refl +code-injective {c3} {c3} _ = refl + +encoding : Encoding +encoding = record + { Source = Host + ; Code = ℕ + ; enc = code + } + +-- Re-export the lossless-half headline, instantiated and proved: +-- every integer code determines its host value uniquely. +module Theorems = EncodingTheorems encoding + +boundary-lossless : + (i : ℕ) (e₁ e₂ : Echo code i) → proj₁ e₁ ≡ proj₁ e₂ +boundary-lossless = Theorems.encoding-lossless code-injective + diff --git a/proposals/nextgen-evangelist/evangelist/README.adoc b/proposals/nextgen-evangelist/evangelist/README.adoc new file mode 100644 index 00000000..448ed43c --- /dev/null +++ b/proposals/nextgen-evangelist/evangelist/README.adoc @@ -0,0 +1,62 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += evangelist — the orchestrator +:toc: macro + +The thin top layer of the nextgen-languages-evangelist. It walks a target +tree and composes the four component tools into one *next-gen readiness +report*. + +== Pipeline + +[cols="1,1,2",options="header"] +|=== +| Step | Component | On +| ① migratability triage | `affine-migratability` | every `.res` +| ② weak-point scan | `affine-assail` | every `.affine` +| ③ boundary faithfulness proof | `echo-boundary` | manifest tables (emits machine-checked Agda) +| ④ differential parity | `affine-parity` | manifest configs (wasm vs oracle) +|=== + +Steps ① and ② are fully automatic (the tools take a file path). Steps ③ +and ④ need a small `manifest.json` because a proof table / parity oracle +cannot be inferred from source alone. + +== Run it + +[source,console] +---- +# automatic triage + weak-point scan over a tree: +$ deno run -A evangelist.mjs /tmp/evangelist-demo + +# add proofs + parity via a manifest: +$ deno run -A evangelist.mjs /tmp/evangelist-demo manifest.json +---- + +`manifest.json` shape: + +[source,json] +---- +{ + "boundary": [{ "name": "SecurityRank", + "table": {"Open":0,"Weak":1,"Medium":2,"Strong":3} }], + "parity": [{ "name": "SecurityRank", + "config": "../affine-parity/securityrank.config.mjs" }] +} +---- + +== Status + +*Verified end-to-end this session.* The orchestrator composes the four +trialed component tools and produced a full readiness report on the demo +target — the captured output is in the parent `README.adoc` +("Verified end-to-end"). Per-component evidence lives in each sibling +subdir. + +== Design note (production) + +This trial orchestrator is Deno/JS for immediate runnability under the +github-only firewall. The production evangelist should be a Rust or +AffineScript CLI per estate policy, and would gain: a real manifest +schema, JSON/SARIF output for CI, and a `groove`-style auto-discovery of +kernels rather than a directory walk. diff --git a/proposals/nextgen-evangelist/evangelist/evangelist.mjs b/proposals/nextgen-evangelist/evangelist/evangelist.mjs new file mode 100644 index 00000000..a2b18288 --- /dev/null +++ b/proposals/nextgen-evangelist/evangelist/evangelist.mjs @@ -0,0 +1,144 @@ +// SPDX-License-Identifier: MPL-2.0 +// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell +// +// evangelist.mjs -- the nextgen-languages-evangelist orchestrator. +// +// Walks a target tree and runs the component tools to produce one +// "next-gen readiness report": +// * every .res -> affine-migratability (migratable now? which wall?) +// * every .affine -> affine-assail (weak points: clamps, decoders) +// * (optional manifest) per .affine -> echo-boundary (proof) + affine-parity (parity) +// +// Trial-here principle: this composes the *verified* component tools; run it +// on a small target and read the report. No registries (github-only firewall): +// it shells out to `deno` running the sibling component .mjs files only. +// +// Usage: +// deno run -A evangelist.mjs [manifest.json] +// +// manifest.json (optional) lets the proof/parity steps run (they need a table +// / oracle that can't be inferred from source): +// { +// "boundary": [{ "name": "SecurityRank", "table": {"Open":0,"Weak":1,"Medium":2,"Strong":3} }], +// "parity": [{ "name": "SecurityRank", "config": "../affine-parity/securityrank.config.mjs" }] +// } + +const HERE = new URL(".", import.meta.url).pathname; +const COMP = { + migratability: HERE + "../affine-migratability/migratability.mjs", + assail: HERE + "../affine-assail/assail.mjs", + boundary: HERE + "../echo-boundary/boundary.mjs", + parity: HERE + "../affine-parity/parity.mjs", +}; +const SKIP_DIRS = new Set(["node_modules", ".git", "lib", "_build", ".deno"]); + +async function run(cmd, args) { + try { + const p = new Deno.Command(cmd, { args, stdout: "piped", stderr: "piped" }); + const { code, stdout, stderr } = await p.output(); + return { code, out: new TextDecoder().decode(stdout), err: new TextDecoder().decode(stderr) }; + } catch (e) { + return { code: 127, out: "", err: String(e) }; + } +} + +// Tolerant: pull the last line that parses as a JSON object, else null. +function lastJson(s) { + const lines = (s || "").trim().split("\n"); + for (let i = lines.length - 1; i >= 0; i--) { + const t = lines[i].trim(); + if (t.startsWith("{")) { try { return JSON.parse(t); } catch { /* keep looking */ } } + } + return null; +} + +async function* walk(dir) { + let entries; + try { entries = Deno.readDir(dir); } catch { return; } + for await (const e of entries) { + const p = `${dir}/${e.name}`; + if (e.isDirectory) { if (!SKIP_DIRS.has(e.name)) yield* walk(p); } + else yield p; + } +} + +const target = Deno.args[0]; +if (!target) { console.error("usage: deno run -A evangelist.mjs [manifest.json]"); Deno.exit(2); } +const manifest = Deno.args[1] ? JSON.parse(await Deno.readTextFile(Deno.args[1])) : {}; + +const resFiles = [], affFiles = []; +for await (const f of walk(target)) { + if (f.endsWith(".res")) resFiles.push(f); + else if (f.endsWith(".affine")) affFiles.push(f); +} + +const report = []; +report.push(`# Next-gen readiness report`); +report.push(``); +report.push(`Target: \`${target}\` | ${resFiles.length} .res, ${affFiles.length} .affine`); +report.push(``); + +// 1. Migratability triage of every ReScript kernel. +report.push(`## ① ReScript migratability (.res)`); +report.push(``); +report.push(`| file | verdict | walls |`); +report.push(`|---|---|---|`); +for (const f of resFiles) { + const r = await run("deno", ["run", "-A", COMP.migratability, f]); + const j = lastJson(r.out); + const tok = (r.out.match(/STRING-GATED|EFFECT-GATED|MIGRATABLE NOW/) || [])[0]; + const verdict = j?.verdict ?? tok ?? (r.code === 0 ? "ran" : `err(${r.code})`); + const walls = (j?.walls?.length ? j.walls : (j?.notes ?? [])).join("; "); + report.push(`| \`${f.replace(target, ".")}\` | ${verdict} | ${walls} |`); +} +report.push(``); + +// 2. Weak-point scan of every AffineScript core. +report.push(`## ② AffineScript weak points (.affine)`); +report.push(``); +report.push(`| file | findings |`); +report.push(`|---|---|`); +for (const f of affFiles) { + const r = await run("deno", ["run", "-A", COMP.assail, f]); + const j = lastJson(r.out); + const n = j?.findings?.length ?? (r.code === 0 ? 0 : "?"); + const kinds = j?.findings ? [...new Set(j.findings.map((x) => x.rule))].join(", ") : ""; + report.push(`| \`${f.replace(target, ".")}\` | ${n}${kinds ? " — " + kinds : ""} |`); +} +report.push(``); + +// 3. Boundary proofs (manifest-driven; these emit machine-checked Agda). +if (manifest.boundary?.length) { + report.push(`## ③ Boundary faithfulness proofs (echo-boundary)`); + report.push(``); + report.push(`| encoding | verdict |`); + report.push(`|---|---|`); + for (const b of manifest.boundary) { + const r = await run("deno", ["run", "-A", COMP.boundary, JSON.stringify({ table: b.table, clamp: b.clamp })]); + const j = lastJson(r.out); + const tok = (r.out.match(/CONTROLLED LOSS|LOSSLESS/) || [])[0]; + const verdict = j?.verdict ?? tok ?? (r.code === 0 ? "checked" : `err(${r.code})`); + report.push(`| ${b.name} | ${verdict} |`); + } + report.push(``); +} + +// 4. Differential parity (manifest-driven configs). +if (manifest.parity?.length) { + report.push(`## ④ Differential parity (affine-parity)`); + report.push(``); + report.push(`| kernel | result |`); + report.push(`|---|---|`); + for (const p of manifest.parity) { + const r = await run("deno", ["run", "-A", COMP.parity, p.config]); + const all = [...r.out.matchAll(/(\d+\/\d+)\s*pass/g)]; + const m = all.length ? `${all[all.length - 1][1]} pass` : (r.code === 0 ? "pass" : `err(${r.code})`); + report.push(`| ${p.name} | ${m} |`); + } + report.push(``); +} + +report.push(`---`); +report.push(`_Generated by the nextgen-languages-evangelist orchestrator._`); +console.log(report.join("\n")); From 869a0b3b01fc83dfb2c0653bd44949c0c5e575d2 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 4 Jun 2026 20:38:43 +0000 Subject: [PATCH 2/6] fix(nextgen-evangelist): least-privilege deno perms + drop generated sample.js Address #533 review findings: - Hypatia js_deno_all_perms (CWE-250): the orchestrator spawned sub-tools with `deno run -A` (all perms). Replaced with --allow-read --allow-run --allow-write (the union the tools need); usage docs updated to --allow-read --allow-run. - Semgrep detect-non-literal-regexp on deno-esm-spike/sample.js: that file is GENERATED --deno-esm output whose prelude uses new RegExp(). Generated code is not hand-edited; dropped sample.js + gitignored it, documented regeneration, and recorded the prelude-RegExp as a codegen finding. Orchestrator re-verified green end-to-end with the new flags. https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --- proposals/nextgen-evangelist/README.adoc | 2 +- .../deno-esm-spike/.gitignore | 4 + .../deno-esm-spike/README.adoc | 9 +- .../deno-esm-spike/sample.js | 463 ------------------ .../nextgen-evangelist/evangelist/README.adoc | 4 +- .../evangelist/evangelist.mjs | 12 +- 6 files changed, 21 insertions(+), 473 deletions(-) create mode 100644 proposals/nextgen-evangelist/deno-esm-spike/.gitignore delete mode 100644 proposals/nextgen-evangelist/deno-esm-spike/sample.js diff --git a/proposals/nextgen-evangelist/README.adoc b/proposals/nextgen-evangelist/README.adoc index 460b03f2..1f4b9c70 100644 --- a/proposals/nextgen-evangelist/README.adoc +++ b/proposals/nextgen-evangelist/README.adoc @@ -88,7 +88,7 @@ guide-linked readiness report == Verified end-to-end (the orchestrator output) -`deno run -A evangelist/evangelist.mjs /tmp/evangelist-demo manifest.json` +`deno run --allow-read --allow-run evangelist/evangelist.mjs /tmp/evangelist-demo manifest.json` (demo target = the three idaptik kernels + `SecurityRank.affine` + `Kernel_IO.affine`) produced: diff --git a/proposals/nextgen-evangelist/deno-esm-spike/.gitignore b/proposals/nextgen-evangelist/deno-esm-spike/.gitignore new file mode 100644 index 00000000..c200ec10 --- /dev/null +++ b/proposals/nextgen-evangelist/deno-esm-spike/.gitignore @@ -0,0 +1,4 @@ +# Generated AffineScript -> Deno-ESM output (regenerate via README Step 1). +# Not committed: compiler output; its prelude tripped a Semgrep non-literal-RegExp +# (ReDoS) finding -- a codegen concern, not source. +sample.js diff --git a/proposals/nextgen-evangelist/deno-esm-spike/README.adoc b/proposals/nextgen-evangelist/deno-esm-spike/README.adoc index 480372bc..5c58da68 100644 --- a/proposals/nextgen-evangelist/deno-esm-spike/README.adoc +++ b/proposals/nextgen-evangelist/deno-esm-spike/README.adoc @@ -34,7 +34,7 @@ This spike is the minimal end-to-end demonstration of that path. [cols="1,3"] |=== | `sample.affine` | Minimal AffineScript: two `pub fn`s (`add`, `clamp_band`), pure integer arithmetic, no `extern`/host calls — so the only thing under test is the *export shape*. -| `sample.js` | Generated by the compiler with `--deno-esm`. A drop-in ES module (committed here as the captured trial artefact). +| `sample.js` | Generated by `--deno-esm` (Step 1). *Not committed* (gitignored): it is compiler output, and its prelude tripped a Semgrep non-literal-RegExp finding. Regenerate it before running the driver. | `driver.mjs` | Plain-JavaScript (`.mjs`, NOT TypeScript) Deno consumer: `import { add, clamp_band } from "./sample.js"` then asserts five results. |=== @@ -116,6 +116,8 @@ Observations, honestly: [source] ---- +$ # sample.js is gitignored compiler output -- regenerate it first (Step 1): +$ /home/user/affinescript/_build/default/bin/main.exe compile --deno-esm -o sample.js sample.affine $ deno run ./driver.mjs deno-esm-spike driver: importing AffineScript-compiled ESM typeof add = function @@ -159,3 +161,8 @@ the estate "no new TypeScript" policy end to end. and `extern fn` -> host-call lowering are documented by `--help` but NOT exercised by this spike — a follow-up spike should confirm those export shapes too before the harness migration relies on them. +. The generated runtime prelude calls `new RegExp()`, which + Semgrep flags as a potential ReDoS (`detect-non-literal-regexp`). Because + this is *generated* code, the fix belongs in the AffineScript codegen + (hardcode the prelude's regexes, or omit the unused shim) — which is also + why `sample.js` is gitignored here rather than committed. diff --git a/proposals/nextgen-evangelist/deno-esm-spike/sample.js b/proposals/nextgen-evangelist/deno-esm-spike/sample.js deleted file mode 100644 index 7b4b300e..00000000 --- a/proposals/nextgen-evangelist/deno-esm-spike/sample.js +++ /dev/null @@ -1,463 +0,0 @@ -// Generated by AffineScript compiler (Deno-ESM target, issue #122) -// hypatia: allow cicd_rules/javascript_detected -- Deno trial component for nextgen-evangelist; production target is Rust/AffineScript (see proposals/nextgen-evangelist/README.adoc) -// SPDX-License-Identifier: MPL-2.0 -// ---- AffineScript Deno-ESM runtime ---- -const Some = (value) => ({ tag: "Some", value }); -const None = { tag: "None" }; -const Ok = (value) => ({ tag: "Ok", value }); -const Err = (error) => ({ tag: "Err", error }); -const Unit = null; -const print = (s) => { Deno.stdout.writeSync(new TextEncoder().encode(String(s))); }; -const println = (s) => { console.log(String(s)); }; -// ---- Deno host shims (extern fn lowering targets, issue #122) ---- -// Kept tiny + inlined so emitted modules are genuinely drop-in (no extra -// package to publish or resolve). The same surface is mirrored, for -// standalone `deno test`, by packages/affine-deno/mod.js. -const __as_ensureDir = (p) => { - try { Deno.mkdirSync(p, { recursive: true }); } - catch (e) { if (!(e instanceof Deno.errors.AlreadyExists)) throw e; } -}; -const __as_pathJoin = (a, b) => { - if (a.length === 0) return b; - const sep = a.endsWith("/") || a.endsWith("\\") ? "" : "/"; - return a + sep + b; -}; -const __as_readDirNames = (p) => { - const names = []; - for (const entry of Deno.readDirSync(p)) { - if (entry.isFile) names.push(entry.name); - } - return names; -}; -const __as_isNotFound = (e) => (e instanceof Deno.errors.NotFound); -const __as_walkRecursive = (root) => { - const out = []; - const rec = (dir) => { - for (const entry of Deno.readDirSync(dir)) { - const full = (dir.endsWith("/") ? dir : dir + "/") + entry.name; - if (entry.isFile) out.push(full); - else if (entry.isDirectory) rec(full); - } - }; - rec(root); - return out; -}; -const __as_regexMatch = (s, pat) => new RegExp(pat).test(String(s)); -const __as_wasmInstance = (bytes) => - new WebAssembly.Instance(new WebAssembly.Module(bytes)).exports; -const __as_wasmCall = (exports, name, args) => Number(exports[name](...(args || []))); -// ---- WasmValue (Deno.affine #455 — Tier 1 #5, Option B) ---- -// Opaque tagged value crossing the AS/JS boundary as `{ kind, v }`. -// `kind` is one of "i32" | "i64" | "f32" | "f64". The `v` payload is -// `BigInt` for i64 (preserves precision beyond 2^53), `Number` otherwise. -const __as_wv_i32 = (n) => ({ kind: "i32", v: (Number(n) | 0) }); -const __as_wv_i64 = (n) => ({ kind: "i64", v: BigInt(n) }); -const __as_wv_f32 = (f) => ({ kind: "f32", v: Math.fround(Number(f)) }); -const __as_wv_f64 = (f) => ({ kind: "f64", v: Number(f) }); -const __as_wv_as_int = (v) => { - if (v == null) return 0; - if (typeof v.v === "bigint") { - // i64: truncate to safe-integer Number; caller's responsibility for - // precision-sensitive paths (use wv_kind to detect). - return Number(v.v); - } - // i32 / f32 / f64: truncate toward zero per AS Int semantics. - return (Number(v.v) | 0); -}; -const __as_wv_as_float = (v) => { - if (v == null) return 0; - return typeof v.v === "bigint" ? Number(v.v) : Number(v.v); -}; -const __as_wv_kind = (v) => (v && typeof v.kind === "string") ? v.kind : ""; -const __as_wasm_export_call = (exports, name, args) => { - // Unmarshal AS-side [WasmValue] to raw JS scalars for the wasm call. - const rawArgs = (args || []).map((wv) => { - if (wv == null) return 0; - // i64 payload is BigInt; wasm i64 imports accept BigInt directly. - return wv.v; - }); - const result = exports[name](...rawArgs); - // Wrap return as f64 (lossless for any numeric; callers expecting i32/i64 - // can rebuild via wv_i32(wv_as_int(result)) or inspect wv_kind). - if (typeof result === "bigint") { - return { kind: "i64", v: result }; - } - return { kind: "f64", v: Number(result) }; -}; -// ---- motion (bindings #4): consumer-provided import ---- -// Host JS environment must expose globalThis.__as_motion (the motion -// library or a compatible mock). Tests set it in the harness before -// importing the generated module; production consumers typically do -// `import * as m from "motion"; globalThis.__as_motion = m;` once at -// module-init time. The AffineScript-side externs (stdlib/Motion.affine) -// don't see this indirection — they call __as_motion* helpers directly. -const __as_motionAnimate = (target, keyframes, options) => - globalThis.__as_motion.animate(target, keyframes, options); -const __as_motionAwait = (controls) => - Promise.resolve(controls).then(() => 0); -const __as_motionCancel = (controls) => { - if (controls && typeof controls.cancel === "function") controls.cancel(); - return 0; -}; -// `animateMini` / `tween` / `spring` / `ease` — bindings #4 follow-up -// surface. Each helper resolves the host method on globalThis.__as_motion -// at call time so a mock that only stubs a subset still works for the -// rest (the smoke harness exercises every variant). -const __as_motionAnimateMini = (target, keyframes, options) => - globalThis.__as_motion.animateMini(target, keyframes, options); -const __as_motionTween = (target, from, to, options) => - globalThis.__as_motion.tween(target, from, to, options); -const __as_motionSpring = (target, keyframes, springConfig) => - globalThis.__as_motion.spring(target, keyframes, springConfig); -const __as_motionEase = (name) => - globalThis.__as_motion.ease(name); -// ---- pixi.js (bindings #1): consumer-provided import ---- -// Host JS environment exposes globalThis.__as_pixi (the PIXI namespace -// from `import * as PIXI from "pixi.js"`). Tests set it in the harness -// before importing the generated module. -const __as_pixiAppInit = async (options) => { - const app = new globalThis.__as_pixi.Application(); - await app.init(options); - return app; -}; -const __as_pixiAppCanvas = (app) => app.canvas; -const __as_pixiAppStage = (app) => app.stage; -const __as_pixiAppTicker = (app) => app.ticker; -const __as_pixiAppDestroy = (app) => { app.destroy(); return 0; }; -const __as_pixiContainerNew = () => new globalThis.__as_pixi.Container(); -const __as_pixiContainerAddChild = (p, c) => { p.addChild(c); return 0; }; -const __as_pixiContainerRemoveChild = (p, c) => { p.removeChild(c); return 0; }; -const __as_pixiContainerSetPosition = (c, x, y) => { c.x = x; c.y = y; return 0; }; -const __as_pixiContainerSetScale = (c, x, y) => { c.scale.set(x, y); return 0; }; -const __as_pixiContainerSetPivot = (c, x, y) => { c.pivot.set(x, y); return 0; }; -const __as_pixiContainerSetRotation = (c, rad) => { c.rotation = rad; return 0; }; -const __as_pixiContainerSetAlpha = (c, a) => { c.alpha = a; return 0; }; -const __as_pixiContainerSetZIndex = (c, z) => { c.zIndex = z; return 0; }; -const __as_pixiContainerSetSortableChildren = (c, v) => { c.sortableChildren = v; return 0; }; -const __as_pixiContainerSetEventMode = (c, mode) => { c.eventMode = mode; return 0; }; -const __as_pixiContainerSetCursor = (c, cursor) => { c.cursor = cursor; return 0; }; -const __as_pixiContainerSetVisible = (c, v) => { c.visible = v; return 0; }; -const __as_pixiContainerOn = (c, event, handler) => { c.on(event, handler); return 0; }; -const __as_pixiContainerOff = (c, event, handler) => { c.off(event, handler); return 0; }; -const __as_pixiContainerDestroy = (c) => { c.destroy(); return 0; }; -const __as_pixiSpriteFrom = (t) => new globalThis.__as_pixi.Sprite(t); -const __as_pixiSpriteSetAnchor = (s, x, y) => { s.anchor.set(x, y); return 0; }; -// Upcasts are identity — PIXI's class hierarchy makes Sprite/Graphics/ -// Text actual Container subclasses, so the JS object is the same. -const __as_pixiSpriteAsContainer = (s) => s; -const __as_pixiTextureFromUrl = (url) => globalThis.__as_pixi.Texture.from(url); -const __as_pixiGraphicsNew = () => new globalThis.__as_pixi.Graphics(); -const __as_pixiGraphicsRect = (g, x, y, w, h) => { g.rect(x, y, w, h); return 0; }; -const __as_pixiGraphicsFill = (g, color) => { g.fill({ color }); return 0; }; -const __as_pixiGraphicsClear = (g) => { g.clear(); return 0; }; -const __as_pixiGraphicsAsContainer = (g) => g; -const __as_pixiTextNew = (options) => new globalThis.__as_pixi.Text(options); -const __as_pixiTextSetText = (t, content) => { t.text = content; return 0; }; -const __as_pixiTextAsContainer = (t) => t; -const __as_pixiTickerAdd = (t, cb) => { t.add(cb); return 0; }; -const __as_pixiTickerStart = (t) => { t.start(); return 0; }; -const __as_pixiTickerStop = (t) => { t.stop(); return 0; }; -// ---- @pixi/ui (bindings #3): consumer-provided import ---- -// Host JS environment exposes globalThis.__as_pixi_ui (the namespace -// from `import * as PixiUI from "@pixi/ui"`). Tests set it in the -// harness before importing the generated module; production -// consumers typically do once at module-init time. The -// AffineScript-side externs (stdlib/PixiUI.affine) don't see this -// indirection — they call __as_pixiUi* helpers directly. -// -// Upcasts to Container are identity — @pixi/ui's Button / -// FancyButton / Slider / Switch are all real PIXI.Container -// subclasses, so the JS object is the same. -const __as_pixiUiButtonNew = (options) => new globalThis.__as_pixi_ui.Button(options); -const __as_pixiUiButtonOnPress = (b, cb) => { b.onPress.connect(cb); return 0; }; -const __as_pixiUiButtonAsContainer = (b) => b; -const __as_pixiUiFancyButtonNew = (options) => new globalThis.__as_pixi_ui.FancyButton(options); -const __as_pixiUiFancyButtonAsContainer = (b) => b; -const __as_pixiUiSliderNew = (options) => new globalThis.__as_pixi_ui.Slider(options); -const __as_pixiUiSliderOnUpdate = (s, cb) => { s.onUpdate.connect(cb); return 0; }; -const __as_pixiUiSliderAsContainer = (s) => s; -const __as_pixiUiSwitchNew = (options) => new globalThis.__as_pixi_ui.Switch(options); -const __as_pixiUiSwitchOnChange = (sw, cb) => { sw.onChange.connect(cb); return 0; }; -const __as_pixiUiSwitchAsContainer = (sw) => sw; -// ---- @pixi/sound (bindings #2): consumer-provided import ---- -// Host JS environment exposes globalThis.__as_pixi_sound (the `Sound` -// named export from `@pixi/sound`). Tests set it in the harness before -// importing the generated module; production consumers typically do -// `import { Sound } from "@pixi/sound"; globalThis.__as_pixi_sound = Sound;` -// once at module-init time. The AffineScript-side externs -// (stdlib/PixiSound.affine) don't see this indirection — they call -// __as_pixiSound* helpers directly. -const __as_pixiSoundFrom = (url) => globalThis.__as_pixi_sound.from(url); -const __as_pixiSoundPlay = (s) => { s.play(); return 0; }; -const __as_pixiSoundStop = (s) => { s.stop(); return 0; }; -const __as_pixiSoundPause = (s) => { s.pause(); return 0; }; -const __as_pixiSoundResume = (s) => { s.resume(); return 0; }; -const __as_pixiSoundSetVolume = (s, vol) => { s.volume = vol; return 0; }; -const __as_pixiSoundSetLoop = (s, loop) => { s.loop = loop; return 0; }; -// ---- Ipc (bindings #9): web-platform MessageChannel/MessagePort ---- -// Uses standard web globals (MessageChannel, structuredClone) — no -// consumer-side init required. Available unmodified in Deno, Node 16+, -// browsers, and Web Workers. -const __as_messageChannelNew = () => new MessageChannel(); -const __as_messageChannelPort1 = (ch) => ch.port1; -const __as_messageChannelPort2 = (ch) => ch.port2; -const __as_messagePortPostMessage = (p, data) => { p.postMessage(data); return 0; }; -const __as_messagePortOnMessage = (p, handler) => { p.onmessage = handler; return 0; }; -const __as_messagePortStart = (p) => { p.start(); return 0; }; -const __as_messagePortClose = (p) => { p.close(); return 0; }; -const __as_targetPostMessage = (t, msg) => { t.postMessage(msg); return 0; }; -const __as_structuredCloneValue = (v) => structuredClone(v); -// ---- Canvas (bindings #8): HTML5 Canvas 2D rendering context ---- -// `canvas` arg is the consumer-supplied HTMLCanvasElement; helpers -// dispatch directly to the standard CanvasRenderingContext2D -// methods. Available unmodified in browsers, jsdom-under-Deno, -// idaptik's WebView host, and any DOM emulator. -const __as_canvasGetContext2D = (canvas) => canvas.getContext("2d"); -const __as_canvasFillStyle = (ctx, color) => { ctx.fillStyle = color; return 0; }; -const __as_canvasStrokeStyle = (ctx, color) => { ctx.strokeStyle = color; return 0; }; -const __as_canvasLineWidth = (ctx, w) => { ctx.lineWidth = w; return 0; }; -const __as_canvasGlobalAlpha = (ctx, a) => { ctx.globalAlpha = a; return 0; }; -const __as_canvasFillRect = (ctx, x, y, w, h) => { ctx.fillRect(x, y, w, h); return 0; }; -const __as_canvasStrokeRect = (ctx, x, y, w, h) => { ctx.strokeRect(x, y, w, h); return 0; }; -const __as_canvasClearRect = (ctx, x, y, w, h) => { ctx.clearRect(x, y, w, h); return 0; }; -const __as_canvasBeginPath = (ctx) => { ctx.beginPath(); return 0; }; -const __as_canvasClosePath = (ctx) => { ctx.closePath(); return 0; }; -const __as_canvasMoveTo = (ctx, x, y) => { ctx.moveTo(x, y); return 0; }; -const __as_canvasLineTo = (ctx, x, y) => { ctx.lineTo(x, y); return 0; }; -const __as_canvasArc = (ctx, x, y, r, s, e) => { ctx.arc(x, y, r, s, e); return 0; }; -const __as_canvasFill = (ctx) => { ctx.fill(); return 0; }; -const __as_canvasStroke = (ctx) => { ctx.stroke(); return 0; }; -const __as_canvasSave = (ctx) => { ctx.save(); return 0; }; -const __as_canvasRestore = (ctx) => { ctx.restore(); return 0; }; -const __as_canvasTranslate = (ctx, x, y) => { ctx.translate(x, y); return 0; }; -const __as_canvasRotate = (ctx, rad) => { ctx.rotate(rad); return 0; }; -const __as_canvasScale = (ctx, x, y) => { ctx.scale(x, y); return 0; }; -const __as_canvasFont = (ctx, font) => { ctx.font = font; return 0; }; -const __as_canvasTextAlign = (ctx, align) => { ctx.textAlign = align; return 0; }; -const __as_canvasTextBaseline = (ctx, baseline) => { ctx.textBaseline = baseline; return 0; }; -const __as_canvasFillText = (ctx, text, x, y) => { ctx.fillText(text, x, y); return 0; }; -const __as_canvasStrokeText = (ctx, text, x, y) => { ctx.strokeText(text, x, y); return 0; }; -const __as_canvasMeasureText = (ctx, text) => ctx.measureText(text); -const __as_canvasDrawImage = (ctx, img, x, y) => { ctx.drawImage(img, x, y); return 0; }; -const __as_canvasDrawImageScaled = (ctx, img, x, y, w, h) => { ctx.drawImage(img, x, y, w, h); return 0; }; -// `++` is overloaded (string concat / array concat); `a + b` would -// stringify arrays. Dispatch on shape so stdlib/string.affine's -// `result ++ [x]` and `a ++ b` are both correct. -const __as_concat = (a, b) => Array.isArray(a) ? a.concat(b) : (a + b); -// Honest host/runtime primitives underpinning the AffineScript-level -// stdlib/string.affine (its is_empty/starts_with/ends_with/split/join/ -// replace/... are real AffineScript on top of these). -const __as_strSub = (s, start, n) => String(s).slice(start, start + n); -const __as_strGet = (s, i) => String(s)[i]; -const __as_strFind = (s, n) => String(s).indexOf(n); -const __as_charToInt = (c) => String(c).codePointAt(0); -const __as_intToChar = (n) => String.fromCodePoint(n); -const __as_strCharCodeAt = (s, i) => (i >= 0 && i < s.length ? s.charCodeAt(i) : -1); -const __as_strFromCharCode = (n) => String.fromCharCode(n & 0xff); -const __as_parseInt = (s) => { - const n = parseInt(String(s), 10); - return Number.isNaN(n) ? None : Some(n); -}; -const __as_parseFloat = (s) => { - const n = parseFloat(String(s)); - return Number.isNaN(n) ? None : Some(n); -}; -const __as_show = (v) => (typeof v === "string" ? v : JSON.stringify(v)); -// ---- Http (issue #160): portable fetch round-trip ---- -// `headers` crosses the boundary as an AffineScript [(String, String)] -// assoc list == JS array of [name, value] pairs. `body` is an -// AffineScript Option == { tag: "Some", value } | { tag: "None" }. -// The result is the `Response` record shape { status, headers, body }. -const __as_httpHeadersToObject = (pairs) => { - const o = {}; - for (const kv of (pairs || [])) o[kv[0]] = kv[1]; - return o; -}; -const __as_httpHeadersFromResponse = (res) => { - const out = []; - res.headers.forEach((value, key) => out.push([key, value])); - return out; -}; -// ---- hpm-json-rsr Zig FFI shims (stdlib/json.affine v0.3) ---- -// `HpmJsonValue` is opaque to AffineScript; on Deno-ESM it's just the -// underlying JS value from JSON.parse. The shims mirror the sentinel -// conventions of the Zig exports so the AffineScript-side wrappers -// (`to_json`, `parse`) behave identically across backends. -const __as_hpmJsonParse = (s) => { - try { return Some(JSON.parse(String(s))); } catch (_e) { return None; } -}; -const __as_hpmJsonFree = (_v) => 0; -const __as_hpmJsonType = (v) => { - if (v === null || v === undefined) return 0; - if (typeof v === "boolean") return 1; - if (typeof v === "number") return Number.isInteger(v) ? 2 : 3; - if (typeof v === "string") return 4; - if (Array.isArray(v)) return 5; - if (typeof v === "object") return 6; - return -1; -}; -const __as_hpmJsonBool = (v) => (typeof v === "boolean" ? (v ? 1 : 0) : -1); -const __as_hpmJsonInt = (v) => - (typeof v === "number" ? Math.trunc(v) : Number.MIN_SAFE_INTEGER); -const __as_hpmJsonFloat = (v) => (typeof v === "number" ? v : NaN); -const __as_hpmJsonString = (v) => (typeof v === "string" ? v : ""); -const __as_hpmJsonObjectGet = (v, k) => { - if (v === null || typeof v !== "object" || Array.isArray(v)) return None; - return Object.prototype.hasOwnProperty.call(v, String(k)) - ? Some(v[String(k)]) : None; -}; -const __as_hpmJsonArrayLen = (v) => (Array.isArray(v) ? v.length : 0); -const __as_hpmJsonArrayGet = (v, i) => { - if (!Array.isArray(v)) return None; - const idx = Number(i); - return (idx >= 0 && idx < v.length) ? Some(v[idx]) : None; -}; -const __as_hpmJsonEscapeString = (s) => { - let out = ""; - const src = String(s); - for (let i = 0; i < src.length; i++) { - const c = src.charCodeAt(i); - if (c === 0x22) out += "\\\""; - else if (c === 0x5c) out += "\\\\"; - else if (c === 0x0a) out += "\\n"; - else if (c === 0x0d) out += "\\r"; - else if (c === 0x09) out += "\\t"; - else if (c === 0x08) out += "\\b"; - else if (c === 0x0c) out += "\\f"; - else if (c < 0x20) out += "\\u00" + c.toString(16).padStart(2, "0"); - else out += src[i]; - } - return out; -}; -// ---- Sqlite (db-theory #1a / stdlib/Sqlite.affine): SQL via host adapter ---- -// Host JS environment must expose globalThis.__as_sqlite, a namespace -// implementing the small adapter contract below. Consumers init once -// (Deno): -// import * as s from "jsr:@db/sqlite"; -// globalThis.__as_sqlite = { -// open: (p) => new s.Database(p), -// close: (db) => db.close(), -// execute: (db, sql) => db.exec(sql), -// query: (db, sql, params) => db.prepare(sql).all(...params), -// queryOne: (db, sql, params) => db.prepare(sql).get(...params), -// queryInt: (db, sql, params) => db.prepare(sql).value(...params), -// }; -// or (Node + better-sqlite3): adapt the same shape. The smoke harness -// installs an in-memory mock that implements the same contract. -// -// Parameter marshalling is intentionally simple: the AffineScript side -// hands the adapter a JSON-encoded `params` string (`"[]"` for none); -// rows + single-row results come back as JSON strings for caller-side -// decoding via `json::parse`. This matches the existing 6-extern -// stdlib/Sqlite.affine surface; richer typed bindings (prepared -// statements, schema introspection, bulk I/O) land in db-theory #1b. -const __as_dbOpen = (path) => globalThis.__as_sqlite.open(path); -const __as_dbClose = (h) => { globalThis.__as_sqlite.close(h); return 0; }; -const __as_dbExecute = (h, sql) => { globalThis.__as_sqlite.execute(h, sql); return 0; }; -const __as_dbQuery = (h, sql, paramsJson) => { - const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); - const rows = globalThis.__as_sqlite.query(h, sql, params); - return JSON.stringify(rows); -}; -const __as_dbQueryOne = (h, sql, paramsJson) => { - const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); - const row = globalThis.__as_sqlite.queryOne(h, sql, params); - return JSON.stringify(row); -}; -const __as_dbQueryInt = (h, sql, paramsJson) => { - const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); - const v = globalThis.__as_sqlite.queryInt(h, sql, params); - return Number(v) | 0; -}; -// ---- Sqlite prepared statements (db-theory #1b) ---- -// Layered on top of the convenience surface above. The host adapter -// gains nine extra methods (`prepare`, `bindInt`, `bindText`, `bindNull`, -// `step`, `columnCount`, `columnInt`, `columnText`, `reset`, `finalize`); -// the smoke harness's mock implements them, and both `jsr:@db/sqlite` -// and `better-sqlite3` provide direct one-line wrappers (each library -// already exposes a `prepare()` + iterator-style step + typed column -// accessors). Bind-index convention is sqlite3's 1-indexed; column-index -// convention is 0-indexed (matches both adapter libraries). -const __as_dbPrepare = (h, sql) => globalThis.__as_sqlite.prepare(h, sql); -const __as_dbBindInt = (s, idx, v) => { globalThis.__as_sqlite.bindInt(s, idx, v); return 0; }; -const __as_dbBindText = (s, idx, v) => { globalThis.__as_sqlite.bindText(s, idx, v); return 0; }; -const __as_dbBindNull = (s, idx) => { globalThis.__as_sqlite.bindNull(s, idx); return 0; }; -const __as_dbStep = (s) => (globalThis.__as_sqlite.step(s) ? 1 : 0); -const __as_dbColumnCount = (s) => Number(globalThis.__as_sqlite.columnCount(s)) | 0; -const __as_dbColumnInt = (s, idx) => { - const v = globalThis.__as_sqlite.columnInt(s, idx); - return v == null ? 0 : (Number(v) | 0); -}; -const __as_dbColumnText = (s, idx) => { - const v = globalThis.__as_sqlite.columnText(s, idx); - return v == null ? "" : String(v); -}; -const __as_dbReset = (s) => { globalThis.__as_sqlite.reset(s); return 0; }; -const __as_dbFinalize = (s) => { globalThis.__as_sqlite.finalize(s); return 0; }; -// ---- Sqlite schema introspection + bulk I/O + error inspection (db-theory #1c) ---- -// Five more adapter methods (`schemaTables`, `schemaColumns`, -// `tableExists`, `importCsv`, `exportCsv`, `lastError`); each -// real-world adapter (jsr:@db/sqlite, better-sqlite3) backs them with -// a one-liner over `PRAGMA table_info` / a `Database.prepare()` -// iterator / a `fs.writeFileSync(..., csv)` call. -const __as_dbSchemaTables = (h) => String(globalThis.__as_sqlite.schemaTables(h)); -const __as_dbSchemaColumns = (h, table) => String(globalThis.__as_sqlite.schemaColumns(h, table)); -const __as_dbTableExists = (h, table) => Boolean(globalThis.__as_sqlite.tableExists(h, table)); -const __as_dbImportCsv = (h, table, path, hasHeader) => - Number(globalThis.__as_sqlite.importCsv(h, table, path, Boolean(hasHeader))) | 0; -const __as_dbExportCsv = (h, sql, paramsJson, path) => { - const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); - return Number(globalThis.__as_sqlite.exportCsv(h, sql, params, path)) | 0; -}; -const __as_dbLastError = (h) => { - const v = globalThis.__as_sqlite.lastError(h); - return v == null ? "" : String(v); -}; -// ---- Sqlite transactions (db-theory #2) ---- -// `Tx` is an opaque handle; the host adapter is required to -// invalidate it on `commit` / `rollback` so that subsequent calls -// throw a host-side `Error` (the affine type system's -// at-most-one-use guarantee is enforced statically on the AS side; -// this host invariant catches FFI-side aliasing bugs in tests). -const __as_txBegin = (h) => globalThis.__as_sqlite.txBegin(h); -const __as_txCommit = (t) => { globalThis.__as_sqlite.txCommit(t); return 0; }; -const __as_txRollback = (t) => { globalThis.__as_sqlite.txRollback(t); return 0; }; -const __as_txSavepoint = (t, n) => { globalThis.__as_sqlite.txSavepoint(t, n); return 0; }; -const __as_txRelease = (t, n) => { globalThis.__as_sqlite.txRelease(t, n); return 0; }; -const __as_txRollbackTo = (t, n) => { globalThis.__as_sqlite.txRollbackTo(t, n); return 0; }; -const __as_txDb = (t) => globalThis.__as_sqlite.txDb(t); -const __as_txIsLive = (t) => (globalThis.__as_sqlite.txIsLive(t) ? 1 : 0); -// ---- Sqlite aggregation (db-theory #3 / stdlib/Aggregate.affine) ---- -// Each scalar aggregator delegates to a host adapter method that runs -// the SQL, expects a single-row result, and unwraps column 0. `groupBy` -// / `groupCount` return JSON strings (caller parses). -const __as_dbCount = (h, sql, params) => Number(globalThis.__as_sqlite.aggCount(h, sql, params)) | 0; -const __as_dbSum = (h, sql, params) => Number(globalThis.__as_sqlite.aggSum(h, sql, params)) | 0; -const __as_dbMinInt = (h, sql, params) => Number(globalThis.__as_sqlite.aggMinInt(h, sql, params)) | 0; -const __as_dbMaxInt = (h, sql, params) => Number(globalThis.__as_sqlite.aggMaxInt(h, sql, params)) | 0; -const __as_dbAvg = (h, sql, params) => Number(globalThis.__as_sqlite.aggAvg(h, sql, params)); -const __as_dbGroupBy = (h, sql, params) => String(globalThis.__as_sqlite.groupBy(h, sql, params)); -const __as_dbGroupCount = (h, table, keyCol) => String(globalThis.__as_sqlite.groupCount(h, table, keyCol)); -const __as_httpFetch = async (url, method, headers, bodyOpt) => { - const init = { method, headers: __as_httpHeadersToObject(headers) }; - if (bodyOpt && bodyOpt.tag === "Some") init.body = bodyOpt.value; - // `globalThis.fetch` explicitly: the stdlib `Http.fetch` compiles to a - // module-level `function fetch`, which would otherwise shadow the host. - const res = await globalThis.fetch(url, init); - const text = await res.text(); - return { - status: res.status, - headers: __as_httpHeadersFromResponse(res), - body: text, - }; -}; -// ---- end runtime ---- - -export function add(a, b) { - return (a + b); -} - -export function clamp_band(x) { - return ((x < 0) ? (() => { return 0; })() : (() => { return ((x > 3) ? (() => { return 3; })() : (() => { return x; })()); })()); -} - diff --git a/proposals/nextgen-evangelist/evangelist/README.adoc b/proposals/nextgen-evangelist/evangelist/README.adoc index 448ed43c..935eb68f 100644 --- a/proposals/nextgen-evangelist/evangelist/README.adoc +++ b/proposals/nextgen-evangelist/evangelist/README.adoc @@ -27,10 +27,10 @@ cannot be inferred from source alone. [source,console] ---- # automatic triage + weak-point scan over a tree: -$ deno run -A evangelist.mjs /tmp/evangelist-demo +$ deno run --allow-read --allow-run evangelist.mjs /tmp/evangelist-demo # add proofs + parity via a manifest: -$ deno run -A evangelist.mjs /tmp/evangelist-demo manifest.json +$ deno run --allow-read --allow-run evangelist.mjs /tmp/evangelist-demo manifest.json ---- `manifest.json` shape: diff --git a/proposals/nextgen-evangelist/evangelist/evangelist.mjs b/proposals/nextgen-evangelist/evangelist/evangelist.mjs index a2b18288..a297f6d8 100644 --- a/proposals/nextgen-evangelist/evangelist/evangelist.mjs +++ b/proposals/nextgen-evangelist/evangelist/evangelist.mjs @@ -15,7 +15,7 @@ // it shells out to `deno` running the sibling component .mjs files only. // // Usage: -// deno run -A evangelist.mjs [manifest.json] +// deno run --allow-read --allow-run evangelist.mjs [manifest.json] // // manifest.json (optional) lets the proof/parity steps run (they need a table // / oracle that can't be inferred from source): @@ -64,7 +64,7 @@ async function* walk(dir) { } const target = Deno.args[0]; -if (!target) { console.error("usage: deno run -A evangelist.mjs [manifest.json]"); Deno.exit(2); } +if (!target) { console.error("usage: deno run --allow-read --allow-run evangelist.mjs [manifest.json]"); Deno.exit(2); } const manifest = Deno.args[1] ? JSON.parse(await Deno.readTextFile(Deno.args[1])) : {}; const resFiles = [], affFiles = []; @@ -85,7 +85,7 @@ report.push(``); report.push(`| file | verdict | walls |`); report.push(`|---|---|---|`); for (const f of resFiles) { - const r = await run("deno", ["run", "-A", COMP.migratability, f]); + const r = await run("deno", ["run", "--allow-read", "--allow-run", "--allow-write", COMP.migratability, f]); const j = lastJson(r.out); const tok = (r.out.match(/STRING-GATED|EFFECT-GATED|MIGRATABLE NOW/) || [])[0]; const verdict = j?.verdict ?? tok ?? (r.code === 0 ? "ran" : `err(${r.code})`); @@ -100,7 +100,7 @@ report.push(``); report.push(`| file | findings |`); report.push(`|---|---|`); for (const f of affFiles) { - const r = await run("deno", ["run", "-A", COMP.assail, f]); + const r = await run("deno", ["run", "--allow-read", "--allow-run", "--allow-write", COMP.assail, f]); const j = lastJson(r.out); const n = j?.findings?.length ?? (r.code === 0 ? 0 : "?"); const kinds = j?.findings ? [...new Set(j.findings.map((x) => x.rule))].join(", ") : ""; @@ -115,7 +115,7 @@ if (manifest.boundary?.length) { report.push(`| encoding | verdict |`); report.push(`|---|---|`); for (const b of manifest.boundary) { - const r = await run("deno", ["run", "-A", COMP.boundary, JSON.stringify({ table: b.table, clamp: b.clamp })]); + const r = await run("deno", ["run", "--allow-read", "--allow-run", "--allow-write", COMP.boundary, JSON.stringify({ table: b.table, clamp: b.clamp })]); const j = lastJson(r.out); const tok = (r.out.match(/CONTROLLED LOSS|LOSSLESS/) || [])[0]; const verdict = j?.verdict ?? tok ?? (r.code === 0 ? "checked" : `err(${r.code})`); @@ -131,7 +131,7 @@ if (manifest.parity?.length) { report.push(`| kernel | result |`); report.push(`|---|---|`); for (const p of manifest.parity) { - const r = await run("deno", ["run", "-A", COMP.parity, p.config]); + const r = await run("deno", ["run", "--allow-read", "--allow-run", "--allow-write", COMP.parity, p.config]); const all = [...r.out.matchAll(/(\d+\/\d+)\s*pass/g)]; const m = all.length ? `${all[all.length - 1][1]} pass` : (r.code === 0 ? "pass" : `err(${r.code})`); report.push(`| ${p.name} | ${m} |`); From 89fa719322e540f0d232fb84e699ab3fc4810b44 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 4 Jun 2026 21:36:40 +0000 Subject: [PATCH 3/6] proposals(idaptik): server-authoritative-determinism architecture note + diagram Why ReScript->AffineScript->wasm unlocks deterministic rollback netcode (the same vm.wasm on client + server), grounded with the multiplayer migratability tally, gamer-facing examples, and a language matrix (not Elixir-specific). Threads, grounded in the named repos: - SNIFS (github/hyperpolymath/snifs) = Safe NIFs (wasm-in-BEAM via wasmex) IS the safe server-side embedding, not a threat to it. - Burble data channel (protobuf) as a partial P2P string-offload around the AS string gap (non-authoritative comms only). - three-runtime debugging concrete anchor (cross-runtime causal replay by tick). Includes server-authoritative-determinism.svg. https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --- .../idaptik/multiplayer-determinism.adoc | 244 ++++++++++++++++++ .../server-authoritative-determinism.svg | 95 +++++++ 2 files changed, 339 insertions(+) create mode 100644 proposals/idaptik/multiplayer-determinism.adoc create mode 100644 proposals/idaptik/server-authoritative-determinism.svg diff --git a/proposals/idaptik/multiplayer-determinism.adoc b/proposals/idaptik/multiplayer-determinism.adoc new file mode 100644 index 00000000..941b3f3b --- /dev/null +++ b/proposals/idaptik/multiplayer-determinism.adoc @@ -0,0 +1,244 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += Server-authoritative determinism — the same wasm on both sides +:toc: macro + +[IMPORTANT] +==== +*Status: ARCHITECTURE NOTE / PROPOSAL.* Analysis of why the +ReScript→AffineScript→wasm migration *unlocks* a class of multiplayer +netcode that ReScript→JS made impractical, why it is not Elixir-specific, +and the open threads it raises (Burble string-offload, safe-NIF embedding, +three-runtime debugging). Staged in affinescript (MPL); subject is idaptik +(AGPL). A companion SVG (`server-authoritative-determinism.svg`) renders +the two diagrams below. +==== + +toc::[] + +== The thesis in one line + +The *server's* simulation is the single source of truth (authoritative); +every machine runs the *same deterministic* simulation; so a client can +*predict ahead* of the server and, when it guesses wrong, *rewind and +replay* to land exactly on the server's result — no drift, no cheating, no +laggy feel. + +Three legs: **authority** (server decides), **prediction** (client +simulates locally so input feels instant), **determinism** (same inputs + +same start state → bit-identical result everywhere). Determinism is the +load-bearing leg — and AffineScript→wasm makes it nearly free. + +== Diagram 1 — same binary, both sides + +---- + ┌──────────── CLIENT (browser) ───────────┐ ┌──────────── SERVER (Elixir / OTP) ──────────┐ + │ my input ─▶ [ vm.wasm ] ─▶ predict ─▶ Pixi│ │ collect ALL inputs ─▶ [ vm.wasm ] ─▶ step │ + │ ▲ │ │ (authoritative) via wasmex │ + │ rollback + replay │ │ per-entity GenServer + OTP supervision │ + └───────────────────────────┬───────────────┘ └───────────────┬─────────────────────────────┘ + │ inputs (tick, player, bits) │ + └──────────────▶ Phoenix Channel ◀─────┘ + authoritative state / hash @ tick T + ╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌╌ + the IDENTICAL AffineScript-compiled vm.wasm runs in BOTH boxes +---- + +Only *inputs* cross client→server (tiny), and *authoritative state (or a +hash)* crosses server→client. Determinism is what lets you ship inputs +instead of whole world-states. + +== Diagram 2 — predict → confirm → reconcile + +---- +ticks → 8 9 10 11 12 13 14 ← client's predicted "now" +CLIENT: [C] [C] [C] [P] [P] [P] [P] C = confirmed P = predicted (my inputs only) + ▲ +SERVER confirms tick 11 — but it includes PLAYER B's input the client never predicted + │ + ▼ predicted@11 ≠ authoritative@11 → MISMATCH + │ + RECONCILE: 1. rewind to 10 (last confirmed) + 2. re-apply now-known inputs (mine + B's) for 11..14 + 3. replay forward → corrected "now" @14 + (determinism ⇒ this lands exactly on the server's result) +---- + +If the prediction was right (the common case) the compare matches and the +player never notices. Mispredictions cost a one-frame correction, not a +stall. + +== Diagram 3 — why ReScript couldn't, and what the real requirement is + +---- + CLASSIC netcode (brittle) AFFINESCRIPT → wasm (by construction) + ───────────────────────── ───────────────────────────────────── + client sim server sim client server + (JS / ReScript) (rewritten in Elixir) [ vm.wasm ] ===== [ vm.wasm ] + └─ must match BIT-FOR-BIT, by hand same bytes → same result, always + float rounding / map order / overflow compile ONCE, run both places + → silent divergence → DESYNC (browser + Elixir via wasmex/wasmtime NIF) +---- + +In the classic world you maintain *two* implementations that must agree to +the last bit forever; one float-rounding difference between V8 and the BEAM +and you desync. AffineScript compiles to one `vm.wasm` you run in both +places, so "the two sims match" is true *by construction*. + +== Every gamer knows this (the examples) + +[cols="1,2a",options="header"] +|=== +| What gamers say | The concept it is + +| *"GGPO / rollback netcode is so good"* (Guilty Gear Strive, Skullgirls, Street Fighter 6) +| This *is* predict + rollback + replay. It feels like magic *because* the + sim is deterministic — the praised netcode is literally this mechanism. + +| *"I SHOT him, he was behind the wall!"* (CS, Valorant, Apex — peeker's advantage) +| Prediction vs authority under latency: you acted on your predicted frame; + the server's authoritative timeline disagreed. The eternal complaint is + the reconciliation gap made visible. + +| *Rubber-banding / teleporting players* +| Reconciliation snapping a client to the authoritative position after a + misprediction (or packet loss). The "warp" is the correction. + +| *"This guy's on wifi"* (Smash Ultimate desync/lag jokes — "why is my Falco teleporting") +| Latency + weak determinism = the experience you are trying to *kill*. + Delay-based, non-deterministic netcode is the thing gamers mock. + +| *Dark Souls backstab / "phantom hit" desyncs* (P2P, no authoritative host) +| The horror of *no authority + weak determinism*: two peers each think + they're right, neither can reconcile. This is the architecture you are + *avoiding*. +|=== + +The punchline: determinism + same-binary + reversibility is the recipe +behind the netcode gamers *praise* (GGPO rollback) and whose *absence* is +the netcode they *mock* (delay-based, P2P backstab desync, wifi Falco). + +== Is this Elixir-specific? (no) + +It is a *determinism + shared-artifact* property, not an Elixir property. +The requirement is: **a deterministic simulation that the same artifact can +run on both the client and the authoritative host.** + +[cols="2,1,3a",options="header"] +|=== +| Stack | Works? | Why +| ReScript → JS + Elixir | ✗ | JS float/GC nondeterminism; and you can't run the *same artifact* server-side — you'd reimplement the sim in Elixir (the two-sims problem). +| *AffineScript → wasm* + Elixir | ✓✓ | Deterministic integer wasm both sides + affine no-aliasing + *reversible* VM (rollback = step backward). +| Rust → wasm + Elixir | ✓ | Rust is deterministic; same wasm both sides (Rust-native also works server-side via a Rustler NIF). A very common, strong combo. +| C/C++/Zig → wasm + any host | ✓ | Deterministic if you avoid float / UB / map-order. wasm is the shared artifact. +| "Elixir sim on both sides" | ✗ (browser) | BEAM doesn't run in the browser; Gleam→JS puts you back on JS-client nondeterminism. +|=== + +**wasm is the lingua franca** that makes "same binary both sides" possible. +Elixir's role is just a *great authoritative host* (per-entity processes, +OTP supervision, `wasmex` to embed the module) — swap Elixir for a +Rust/Go server and the determinism story is unchanged. So: *Rust+Elixir, +Rust+Rust, AffineScript+Elixir* all work; *ReScript+anything* doesn't, +because it can't give you the shared deterministic artifact. + +== Honest caveats + +* The synced sim must be **pure**: no wall-clock, unseeded RNG, or host + effects in the stepped path (exactly the effect-codegen wall — networking + and time stay *outside* the VM). AffineScript *enforces* this rather than + hoping for it. +* The VM's I/O ports must be **fed identically** server-side (the server's + wasm consumes recorded inputs, it does not make live host calls). +* `wasmex`/`wasmtime` is real but you **batch ticks** across the NIF + boundary to amortise call overhead, and validate under load. +* Determinism removes *desync*, not *latency* — you still need input-delay / + a rollback window. + +== Open threads (raised, not yet resolved) + +=== T1 — Burble's data channel to offload the string gap + +CONFIRMED from `github.com/hyperpolymath/burble`: a *media plane* (WebRTC +RTP/SRTP voice), an Elixir/OTP *control plane* (auth, rooms, presence, +signaling), a P2P *data channel* (the burble proof-spec: a "bidirectional +AI agent data channel" exchanging JSON over the same connection as voice), +and a *Protobuf-defined wire protocol* shared by server and clients. (Your +three-channel framing — voice/chat, an LLM channel, an "rtsm" real-time +state channel — maps onto media-plane + two uses of the data channel; the +exact `rtsm` name isn't in the public ARCHITECTURE.adoc I could read.) + +Idea: route the game's *stringy* comms (chat, names, AI/LLM text) over +Burble's data channel so the AffineScript sim never touches them — routing +strings *around* the AS string-gap, not through it. + +* *Strong fit:* the data channel is **Protobuf**, not ad-hoc string + parsing — structured, length-delimited, integer-tagged. That is exactly + the shape AffineScript likes at a boundary; the AS sim can read protobuf + field tags/ints without needing variable-string ops. +* *Works for:* non-authoritative peer strings (chat, voice, the LLM + channel). Brain/senses: AS = integer brain on Phoenix; Burble data + channel = peer string/voice senses. +* *Does NOT replace the authoritative path:* game-*affecting* strings must + still traverse Phoenix→Elixir→wasm (authority + determinism), not a P2P + side-channel. +* *Integration cost is real:* Burble needs signaling/discovery (its Elixir + control plane, or Groove); adding it as a game dependency is a second + transport. Verdict: a good *partial* offload for the comms layer, the + protobuf wire is a bonus — but not a substitute for the variable-string + backend on the authoritative path. + +=== T2 — "snifs instead of nifs": it doesn't dismantle this — it IS the server side + +CONFIRMED from `github.com/hyperpolymath/snifs`: *SNIFS = Safe NIFs* — +native (Zig) code compiled to WebAssembly and run via `wasmex`/`wasmtime`, +so guest faults (out-of-bounds, overflow, divide-by-zero, crashes) become +`{:error, reason}` tuples instead of taking down the BEAM. Tagline: +"WebAssembly sandboxing provides genuine crash isolation for BEAM NIFs." + +This is not a threat to server-authoritative determinism — *it is the +recommended way to do the server side of it.* The diagram's "server-side +`vm.wasm` via wasmex" literally IS a SNIF. So: + +* *Determinism is unaffected:* it comes from the *wasm module being + identical both sides*. SNIFS runs that same wasm; the computation is + bit-identical. +* *SNIFS improves the architecture:* a runaway or faulting authoritative + tick yields `{:error}` (the entity's GenServer rejects/rolls back that + input) instead of crashing the lobby — exactly the OTP-shaped recovery + you want. Raw-NIF embedding gives determinism but not containment; SNIFS + gives both. +* *A convergence worth naming:* the determinism argument *wants* wasm on + the server (the same-binary property); SNIFS *independently* wants wasm + on the server (crash isolation). Same choice, two reasons. SNIFS is the + production substrate for "vm.wasm via wasmex." + +Net: use SNIFs, not raw NIFs — *same determinism, crash-contained +authority*. Far from dismantling it, SNIFS is the piece that makes the +server side safe to ship. + +=== T3 — three-runtime debugging (concrete anchor) + +A desync spans three runtimes. Concrete bug: *"Player A sees the door open; +Player B sees it closed."* The door bit lives in the AS-wasm VM; the input +was marshalled by the JS host; relayed/authorised by Elixir. Suspects: + +. *AS↔JS ABI* — A's input mis-marshalled (wrong integer crossed the wasm boundary). +. *JS↔Elixir codec* — schema drift (a field dropped in JSON). +. *Elixir ordering* — input applied at the wrong tick. +. *determinism break* — B's wasm ≠ A's wasm (shouldn't happen with the same binary). + +One symptom, three runtimes, four boundaries, *no single stack trace*. The +concrete handle: a **unified trace keyed by `(tick, entityId, traceId)`** +that every runtime emits, so the cross-runtime causal chain can be +reconstructed — and because the VM is *reversible + deterministic*, the +exact desync can be **replayed from recorded inputs** across all three +runtimes (record-and-replay debugging end to end). A generalised +debugging idea is worth testing against this anchor: *does it help +reconstruct/replay the cross-runtime causal chain keyed by tick?* + +== Provenance + +2026-06-04 AffineScript co-development session. Companion: the multiplayer +architecture analysis in `proposals/idaptik/README.adoc` and the migratability +tally of `src/app/multiplayer/*.res` (6 MIGRATABLE NOW / 5 EFFECT-GATED / +2 STRING-GATED) that empirically confirms the brain/senses cleavage. diff --git a/proposals/idaptik/server-authoritative-determinism.svg b/proposals/idaptik/server-authoritative-determinism.svg new file mode 100644 index 00000000..affc1590 --- /dev/null +++ b/proposals/idaptik/server-authoritative-determinism.svg @@ -0,0 +1,95 @@ + + + Server-Authoritative Determinism + one compiled vm.wasm runs on the client AND the authoritative server + + + ① Same binary, both sides + + + + CLIENT — browser + + vm.wasm + predict locally (instant) + → Pixi render + rewind ◀ replay on mismatch + + + + SERVER — Elixir / OTP + + vm.wasm + authoritative step (via SNIFS / wasmex) + per-entity GenServer + supervision + orders all players' inputs + + + + + + + inputs + + state/hash + Phoenix + Channel + + + + + + IDENTICAL compiled module — determinism for free + + + + + + ② Predict → Confirm → Reconcile + + + + + rewind to tick 10 + + + + + 8 + 9 + 10 + + 11 + 12 + 13 + 14 + + confirmed + predicted (my inputs only) + + + + ticks + + + ✱ MISMATCH + + + + + server confirms 11 — incl. Player B's input + + + + + replay 11…14 with known inputs → corrected "now" + + + determinism ⇒ replay lands exactly on the server's result (no drift) + reversible VM ⇒ rewind = run the instructions backward (no stored snapshots) + affine types ⇒ no hidden aliasing to silently desync shared state + + ReScript→JS can't: float/GC nondeterminism + no way to run the same artifact server-side. + Works with anything giving a deterministic, embeddable artifact both sides: AffineScript→wasm, Rust→wasm, … + hyperpolymath / idaptik · AffineScript co-development 2026-06-04 + From ad907824d08dbe6b34aca9b48b55c5501c8d73ec Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 4 Jun 2026 21:38:34 +0000 Subject: [PATCH 4/6] =?UTF-8?q?proposals(idaptik):=20SNIFS=20=3D=20'Safer?= =?UTF-8?q?=20NIFs'=20(comparative,=20not=20absolute)=20=E2=80=94=20honest?= =?UTF-8?q?-bounds=20naming?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --- proposals/idaptik/multiplayer-determinism.adoc | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/proposals/idaptik/multiplayer-determinism.adoc b/proposals/idaptik/multiplayer-determinism.adoc index 941b3f3b..be54265d 100644 --- a/proposals/idaptik/multiplayer-determinism.adoc +++ b/proposals/idaptik/multiplayer-determinism.adoc @@ -189,11 +189,14 @@ strings *around* the AS string-gap, not through it. === T2 — "snifs instead of nifs": it doesn't dismantle this — it IS the server side -CONFIRMED from `github.com/hyperpolymath/snifs`: *SNIFS = Safe NIFs* — -native (Zig) code compiled to WebAssembly and run via `wasmex`/`wasmtime`, +CONFIRMED from `github.com/hyperpolymath/snifs`: *SNIFS = Safer NIFs* +(the owner's preferred framing — a *comparative* claim that survives a +single sandbox-escape counterexample, where the absolute "safe" would not; +the `SNIFS` acronym is unchanged — Safer Native Implemented Functions). +Native (Zig) code compiled to WebAssembly and run via `wasmex`/`wasmtime`, so guest faults (out-of-bounds, overflow, divide-by-zero, crashes) become -`{:error, reason}` tuples instead of taking down the BEAM. Tagline: -"WebAssembly sandboxing provides genuine crash isolation for BEAM NIFs." +`{:error, reason}` tuples instead of taking down the BEAM — crash +*containment*, not a perfect security boundary. This is not a threat to server-authoritative determinism — *it is the recommended way to do the server side of it.* The diagram's "server-side From e7c83bf02027da091c33e7eaf05f0af710b42252 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 5 Jun 2026 00:21:36 +0000 Subject: [PATCH 5/6] proposals: compaction-phased migration plan (durable spine + ledger) Organises the ReScript->AffineScript->wasm migration by context-compaction boundary; each phase ends at a verified checkpoint and updates the ledger so the plan survives compaction (repo = memory). Standing gates + the two compiler walls + the 4-gate per-kernel recipe captured. https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --- proposals/MIGRATION-PLAN.adoc | 172 ++++++++++++++++++++++++++++++++++ 1 file changed, 172 insertions(+) create mode 100644 proposals/MIGRATION-PLAN.adoc diff --git a/proposals/MIGRATION-PLAN.adoc b/proposals/MIGRATION-PLAN.adoc new file mode 100644 index 00000000..d207e836 --- /dev/null +++ b/proposals/MIGRATION-PLAN.adoc @@ -0,0 +1,172 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell += Migration plan — organised by compaction boundary +:toc: macro + +[IMPORTANT] +==== +*This file is the durable spine of the ReScript -> AffineScript -> wasm +migration.* It is written to survive context compaction: the repo is the +memory, not the model's window. Each PHASE below ends at a *committed, +verified checkpoint* and updates the *Ledger* at the bottom. After any +compaction, the resuming agent reads (1) this file's Ledger and (2) the +latest `proposals/idaptik/migration-map.json`, and continues — it does not +rely on the auto-summary. + +Cadence: roughly one PHASE per context window ("to compact"). Each PHASE = +goal + deliverables + a green checkpoint + a one-line handoff. The arc runs +until "CLEAR": the migratable corpus is exhausted, the two compiler walls +are down, and the cutover has retired the ReScript shadows. +==== + +toc::[] + +== Standing gates (re-check every phase) + +* *Decision gate 1 — production language.* The evangelist tools + harnesses + are Deno trials today; production should be Rust or AffineScript (owner's + call). Until decided: keep the Deno trials, do NOT re-author. Blocks only + the "harden the tooling" sub-tasks, not the migration. +* *Decision gate 2 — evangelist home repo* (dedicated repo vs under + `nextgen-languages`). Cosmetic; blocks nothing. +* *Access gate — idaptik write-access.* Current rule: writes land in + affinescript only; everything idaptik-bound is *staged as applyable + units* under `proposals/idaptik/`. The actual *apply* + *cutover* steps + (Phases C+ "apply", Phase Ω) need either idaptik opened for writes or the + owner accepting the staged patches. Until then, "migrated" means + "verified + staged + applyable", not "applied". + +== The two walls (what ultimately gates "CLEAR") + +. *Variable-string backend* — `String.length` / indexing / `startsWith` / + `fromCharCode` cannot lower to wasm yet. Gates every STRING-GATED kernel + (e.g. `Kernel_IO`, `DeviceType`, i18n). Lives in *this* repo's compiler, + so it is attackable here. +. *Effect codegen* — module-level mutable state / `Date.now` / `Console.log` + cannot lower ("references an unbound binding"). Gates every EFFECT-GATED + kernel (e.g. `Kernel_Quantum`). Also a compiler task. + +Until a wall falls, its kernels stay staged with the honest +"compiler-gated, not effort-gated" label. + +== Phases + +=== PHASE A — now -> compact 1 : consolidate + make the plan durable +Goal: a clean baseline that compaction can't lose. + +* Write this file + the Ledger (done by creating it). +* Settle PR #533 (evangelist toolkit): CI green; leave as draft for owner + review (merge on owner word). +* Fold the three architecture artefacts (`multiplayer-determinism.adoc`, + `state-vs-digest.svg`, `game-vs-deepspace.svg`) into the determinism doc + as a captured "latency regimes" appendix. +* Record the standing gates above. + +*Checkpoint:* plan + ledger committed & pushed; staged work coherent. +*Handoff:* "Read §Ledger; next is PHASE B (full-corpus triage)." + +=== PHASE B — compact 1 -> 2 : broad sweep (the master worklist) +Goal: know the whole backlog, prioritised. + +* Run `affine-migratability` over all ~571 idaptik `.res`; bucket by area + (`src/app`, `shared/src`, `vm`, `src/app/multiplayer`, …) x verdict + (MIGRATABLE-NOW / STRING-GATED / EFFECT-GATED) x shape (pure-integer core + / binding shim / render-glue). +* Emit `proposals/idaptik/migration-map.adoc` (human) + + `migration-map.json` (machine, the resumable worklist) + the headline %. +* Order the MIGRATABLE-NOW set into clusters: leaf pure-integer cores + first, then up the dependency tree. + +*Checkpoint:* full triage committed; backlog + order fixed. +*Handoff:* "worklist = migration-map.json; cluster 1 = ; PHASE C." + +=== PHASE C — compact 2 -> 3 : deep wave 1 (first clean cluster, end-to-end) +Goal: migrate + verify the first batch via the 4-gate recipe. + +The *recipe* (every kernel, every wave): +. re-decompose `.res` -> `.affine` (NOT transliterate — collapse incidental + Promise/async, thread service-locator state as params, enum the options, + hand-ladder int rendering, keep wire bytes identical); +. `affinescript compile` -> wasm (gate 1: builds); +. `affine-parity` oracle-vs-wasm sweep green (gate 2: parity); +. `echo-boundary` proves each host-boundary encoding LOSSLESS or + declared-clamp (gate 3: faithful); +. `affine-assail` clean — no undeclared clamp / unguarded decoder (gate 4). + +* Apply recipe to cluster 1 (~6-10 pure-integer cores). Stage each under + `proposals/idaptik/migrated//` with `.affine` + harness + evidence. + +*Checkpoint:* cluster 1 four-gate-green + staged. Ledger % updated. +*Handoff:* "cluster 1 done (list); cluster 2 next; recipe in §Phase C." + +=== PHASE D — compact 3 -> 4 : deep wave 2 + the TS-0 harness path +Goal: more kernels + start retiring the 17.6k LOC of TS harness. + +* Cluster 2 of MIGRATABLE-NOW (same recipe). +* Trial `--deno-esm` struct -> `export class` + `extern fn` lowering; + re-author ONE parity harness in AffineScript -> Deno-ESM; prove it + reproduces the TS harness's verdict. TS-0-for-harnesses becomes real. + +*Checkpoint:* cluster 2 green + the AffineScript-authored harness PoC. + +=== PHASE E — compact 4 -> 5 : the multiplayer determinism spine (wasmex + SNIFS) +Goal: make server-authoritative determinism concrete before the big +multiplayer-client migration. + +* `vm.affine` reversible counter; run the *identical* wasm in Deno (client) + and under SNIFS/`wasmex` in a one-file Elixir (server); demonstrate + identical step, reverse (rollback), and the per-tick *hash tripwire* + catching an injected desync. + +*Checkpoint:* same-binary-both-sides PoC + hash-tripwire demo verified. + +=== PHASE F — compact 5 -> 6 : attack wall 1, slice 1 (variable-string backend) +Goal: stop documenting the wall; start removing it (compiler work, in scope). + +* Implement `String.length` + string indexing end-to-end in the compiler + (lexer/typer/codegen) on the `[len:i32 LE][utf8]` read-side ABI, with + tests; demonstrate a previously STRING-GATED kernel now builds + + parity-greens. + +*Checkpoint:* first string primitive lands (compiler PR) + one string-kernel +unblocked. + +=== PHASES G..N — compact -> compact : the repeating grind +Each window, in order: +. migrate the next cluster the latest compiler capability unblocked (recipe); +. advance the next wall-slice (`startsWith` -> `fromCharCode`; then the + effect-codegen slices for `Date.now`/log/module-state); +. re-run the evangelist readiness map (the % climbs; gated counts fall); +. update the Ledger. + +Repeat until the MIGRATABLE set is exhausted and both walls are down — at +which point `Kernel_IO` (string) and `Kernel_Quantum` (effect) finally fall. + +=== PHASE Ω — -> CLEAR : cutover + extinction (the goodbye) +Goal: flip the switches, delete the shadows. (Gated on idaptik write-access; +until then each cutover is a staged applyable bundle for sign-off.) + +* Per area, once all cores are parity-green + bindings wired: enable the + `FeaturePacks` flag, delete the `.res` shadows, drop the TS harnesses, + remove the lone `.py` holdout; re-run the census (ReScript -> 0 in that + area). +* Final census target: ReScript 0 in migrated areas, AffineScript primary, + TypeScript 0, Python 0; agreed-keep set (Elixir/Zig/Idris2/Julia) intact. + +*CLEAR* = migratable corpus migrated + applied, walls down, shadows retired. + +== Ledger (each phase updates this; the resume point lives here) + +[cols="1,1,3",options="header"] +|=== +| Phase | State | Notes +| Pre | DONE | #531 echo proof (merged); #532 migration practice + guide + proposals (merged); #533 evangelist toolkit (draft, CI green). +| A | IN PROGRESS | This plan written. Architecture docs staged (determinism + 2 SVGs). Pending: fold SVGs into determinism doc as appendix; settle #533 on owner word. +| B | TODO | Full-corpus triage -> migration-map.{adoc,json}. +| C+ | TODO | Deep waves via the 4-gate recipe. +| F+ | TODO | Compiler walls (string backend, then effects). +| Ω | TODO (access-gated) | Cutover + ReScript extinction. +|=== + +*Resume rule:* read the highest non-DONE row + `migration-map.json`; +continue from its "Notes". From 4e3a9207bc8ee16d56cd0f14a5fb5ffea545b5df Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 5 Jun 2026 00:25:51 +0000 Subject: [PATCH 6/6] =?UTF-8?q?plan:=20close=20Phase=20A=20=E2=80=94=20mod?= =?UTF-8?q?el-per-phase=20guide=20+=20determinism=20latency-regimes=20appe?= =?UTF-8?q?ndix?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds a model-per-phase table (Opus/Sonnet/Haiku heuristic) to the migration plan, folds the verify-don't-transfer + game-vs-deep-space explainers and the two SVGs into the determinism doc as an appendix, ticks the ledger (A=DONE, next=PHASE B). https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --- proposals/MIGRATION-PLAN.adoc | 27 +++++++++++++++- .../idaptik/multiplayer-determinism.adoc | 31 +++++++++++++++++++ 2 files changed, 57 insertions(+), 1 deletion(-) diff --git a/proposals/MIGRATION-PLAN.adoc b/proposals/MIGRATION-PLAN.adoc index d207e836..95cc313b 100644 --- a/proposals/MIGRATION-PLAN.adoc +++ b/proposals/MIGRATION-PLAN.adoc @@ -155,13 +155,38 @@ until then each cutover is a staged applyable bundle for sign-off.) *CLEAR* = migratable corpus migrated + applied, walls down, shadows retired. +== Model per phase (advise at each compact) + +Heuristic: + +* *Opus* — re-decomposition design, compiler-internals (the walls), + novel cross-runtime integration, cutover review. Anywhere a wrong or + subtle call is expensive. ("Fast" Opus when you want that reasoning with + quicker output.) +* *Sonnet* — known-pattern multi-file grinding: the triage sweep, the rote + waves once the recipe is set, the mechanical cutover apply. +* *Haiku* — pure mechanical sub-steps (bulk tool runs, boilerplate, status + checks). Rarely a whole phase. + +[cols="1,1,3",options="header"] +|=== +| Phase | Model | Why +| A consolidate/plan | Opus | synthesis + architecture +| B broad triage | *Sonnet* | run one tool over ~571 files, bucket + prioritise; systematic, low-novelty +| C/D deep waves | *Opus* for the re-decomposition; Sonnet once rote | re-decompose is subtle (a transliteration is rejected); the 4 gates are mechanical +| E wasmex/SNIFS PoC | *Opus* | novel Elixir+wasm+Deno integration + determinism reasoning +| F + walls (compiler) | *Opus* | real OCaml compiler engineering (lexer/typer/codegen/ABI), correctness-critical +| G..N grind | alternate: *Sonnet* (migrate) / *Opus* (wall-slice) | per window +| Ω cutover | *Sonnet* to execute, *Opus* to sign off the diff | high-stakes deletes; mechanical apply +|=== + == Ledger (each phase updates this; the resume point lives here) [cols="1,1,3",options="header"] |=== | Phase | State | Notes | Pre | DONE | #531 echo proof (merged); #532 migration practice + guide + proposals (merged); #533 evangelist toolkit (draft, CI green). -| A | IN PROGRESS | This plan written. Architecture docs staged (determinism + 2 SVGs). Pending: fold SVGs into determinism doc as appendix; settle #533 on owner word. +| A | DONE | Plan + model-per-phase guidance written; determinism doc gained a latency-regimes appendix (verify-don't-transfer + game-vs-deep-space + the 2 SVGs); #533 green (draft, owner to merge). NEXT: PHASE B. | B | TODO | Full-corpus triage -> migration-map.{adoc,json}. | C+ | TODO | Deep waves via the 4-gate recipe. | F+ | TODO | Compiler walls (string backend, then effects). diff --git a/proposals/idaptik/multiplayer-determinism.adoc b/proposals/idaptik/multiplayer-determinism.adoc index be54265d..e689a6f9 100644 --- a/proposals/idaptik/multiplayer-determinism.adoc +++ b/proposals/idaptik/multiplayer-determinism.adoc @@ -239,6 +239,37 @@ runtimes (record-and-replay debugging end to end). A generalised debugging idea is worth testing against this anchor: *does it help reconstruct/replay the cross-runtime causal chain keyed by tick?* +== Appendix — latency regimes (captured from the 2026-06-04 discussion) + +Two companion diagrams are staged beside this note: +`state-vs-digest.svg` (state transfer O(state) vs agreement-by-digest ~O(1)) +and `game-vs-deepspace.svg` (game netcode vs deep-space link). + +=== Verify, don't transfer (the hash tripwire, restated) +Under shared determinism the state is *redundant* — both sides reconstruct +it from the same inputs — so the only non-redundant thing worth sending is +one bit: "do we agree?" A per-tick state hash carries exactly that ("look at +the moon — is it there?" "yes"). Three honest caveats: (1) it is a *detector, +not a corrector* — on mismatch you fall back to replay from the input log, so +keep the log; (2) it is agreement *with overwhelming probability*, not proof +(use a wide collision-resistant hash); (3) granularity — one hash finds +*that* you diverged; a *Merkle tree of per-entity hashes* finds *where* in +log n; reversibility finds *when* by reverse-bisection. Localisation in +space (Merkle) x time (reversible step), both logarithmic. + +=== The flip across latency regimes +*Cheap round-trips* (game, ~ms) reward sending LESS — a fingerprint, ask +"agree?", reconcile on the rare mismatch. *Ruinous round-trips* (deep space, +light-seconds to light-minutes) forbid asking at all, so they send MORE: +forward error correction (Reed-Solomon / Turbo / LDPC, CCSDS), store-and- +forward relays (Delay-Tolerant Networking; Queqiao is CNSA's Chang'e relay +at Earth-Moon L2 — not ESA), and autonomy + a ground "digital twin" checked +offline. echo-types (a PROOF of recoverability) is the static cousin of +channel coding (a coding-theory GUARANTEE of correctability): same goal — +know the data survives the crossing — different layer. IDApTIK lives at the +millisecond end where verification wins; a probe lives at the light-minute +end where redundancy wins. + == Provenance 2026-06-04 AffineScript co-development session. Companion: the multiplayer