Skip to content

Commit 2218100

Browse files
compiler+harness: string-wall cleanup + affine-parity String-arg support (+ float-wall finding) (#592)
Two related "finish & connect the string wall" changes on one branch. ## 1. String-wall cleanup (compiler) `gen_binop`'s `OpConcat -> I32Add (* Placeholder *)` was a latent landmine — it would *silently sum two string pointers* if ever reached. It is provably unreachable (string `++` → `ExprStringConcat` / the 8a guard; list `++` → its own arm; compound-assign maps only `+= -= *= /=`), so it is now a loud `failwith` guard. `proposals/EVIDENCE-stringwall-slices9-10.adoc` consolidates the eq (slice 9) + relational (slice 10) lowerings and records the wall complete. ## 2. affine-parity String-argument support (harness) Extends the differential-parity harness to pass **String** args: after instantiation it grows linear memory by one page and writes args as `[len:i32 LE][utf8]` (matching the compiler's string layout), passing them by pointer; the oracle still receives the JS string. Adds a `{ strings: [...] }` arg-spec form. Float args already pass through as wasm f64 via `{ values: [...] }`. This **connects the string-wall compiler fixes to the migration harness**. The demo (`examples/string_float_demo`) proves slice-9 `==` against a literal **and** slice-9 + slice-10 comparing two *runtime-provided* strings pointer-vs-pointer — **22/22**. No regression on int-only configs (DeviceType / VmState / Maths / NetworkZones unchanged). ## Finding: the "float wall" `Float` binops type-check but codegen emits **i32** instructions on f64 operands (`band_of` fails wasm validation: `i32.lt_s ... found f64`). Never surfaced because the 94-brain corpus is all-Int (×1000 milli-units). The harness is already ready for float-input brains; the float-codegen fix is the unblocker. See `proposals/EVIDENCE-float-wall-finding.adoc`. https://claude.ai/code/session_01WoKhFQePiRsAj7aqnxbG8s --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent c3ebe69 commit 2218100

6 files changed

Lines changed: 289 additions & 14 deletions

File tree

lib/codegen.ml

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -439,7 +439,15 @@ let gen_binop (op : binary_op) : instr =
439439
| OpBitXor -> I32Xor
440440
| OpShl -> I32Shl
441441
| OpShr -> I32ShrS
442-
| OpConcat -> I32Add (* Placeholder *)
442+
| OpConcat ->
443+
(* Unreachable: `++` never reaches [gen_binop]. String `++` is lowered by
444+
the [ExprStringConcat] arm (slice 8b) or rejected by the slice-8a guard;
445+
list `++` is lowered by its own [ExprBinary (_, OpConcat, _)] arm; and
446+
compound-assign only maps `+= -= *= /=`. The former placeholder returned
447+
[I32Add], which would have *silently* summed two pointers if ever
448+
reached — fail loudly instead so a regression surfaces immediately. *)
449+
failwith "gen_binop: OpConcat must be lowered via ExprStringConcat or the \
450+
list-concat arm, never through gen_binop"
443451

444452
(** Generate code for unary operation *)
445453
let gen_unop (op : unary_op) : instr result =
Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
// SPDX-License-Identifier: AGPL-3.0-or-later
2+
// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= Finding: the "float wall" — Float arith/compare codegen emits i32 ops (2026-06-14)
4+
:toc: macro
5+
6+
== Summary
7+
8+
`Float`-typed binary operations (`+`, `-`, `*`, `/`, `<`, `<=`, `>`, `>=`, `==`)
9+
*type-check* but the wasm backend lowers them with **integer** instructions on
10+
f64 operands, producing a module that fails WebAssembly validation. This is the
11+
float analogue of the string wall (slices 8b/9/10): the type checker dispatches
12+
`Float` correctly, but `gen_binop` returns only the i32 instruction family.
13+
14+
== Reproduction
15+
16+
[source]
17+
----
18+
pub fn band_of(x: Float) -> Int {
19+
if x < 10.0 { 0 } else { if x < 100.0 { 1 } else { 2 } }
20+
}
21+
----
22+
23+
[source]
24+
----
25+
$ main.exe compile band_of.affine -o band_of.wasm # compiles
26+
$ # instantiation fails:
27+
WebAssembly.instantiate(): Compiling function failed:
28+
i32.lt_s[1] expected type i32, found f64.const of type f64
29+
----
30+
31+
`codegen.ml gen_binop` maps `OpLt -> I32LtS`, `OpAdd -> I32Add`, etc., with no
32+
`Float` path; the `ExprBinary` lowering applies it to f64 operands.
33+
34+
== Why it has never surfaced
35+
36+
The entire idaptik migration corpus (94 brains) is `Int(...)->Int`: every float
37+
quantity is carried as a x1000 milli-unit / permille integer, precisely because
38+
float codegen does not work and the parity harness passes integer args. So no
39+
shipped artefact exercises float binops, and the gap stayed latent.
40+
41+
== Shape of the fix (the float wall)
42+
43+
The same type-channel pattern that closed the string wall applies. Either:
44+
45+
* *Type-directed elaboration* (mirrors slices 8b/9/10): `synth` records
46+
`Float`-typed binop nodes; an elaboration rewrites them to dedicated
47+
`ExprFloatBinary` / `ExprFloatRel` nodes; codegen lowers those to the f64
48+
instruction family (`F64Add`, `F64Lt`, …). Most faithful to the established
49+
pattern.
50+
* *Operand-type threading at codegen*: give the `ExprBinary` lowering the
51+
synthesised operand type so it can pick the i32 vs f64 instruction directly.
52+
Smaller surface but introduces a type channel into codegen that does not yet
53+
exist there.
54+
55+
*Scope correction (2026-06-14, after investigation).* This is bigger than "add
56+
a binop arm". The f64 *instructions* all exist in `lib/wasm.ml` (`F64Add`,
57+
`F64Lt`, …; `F64Const` is already emitted for float literals), but the codegen's
58+
*value model is i32-only*, so the fix needs f64 value-type tracking end to end:
59+
60+
. *Params* — `codegen.ml` `TopFn` lowers `ft_params = List.map (fun _ -> I32)
61+
fd.fd_params` (line ~2995). A `Float` param is declared `i32`, so an f64 arg
62+
cannot even arrive. Lower each param from its annotation via the existing
63+
`TyCon "Float" -> F64` mapping (line ~170).
64+
. *Results* — `ft_results = [I32]` (line ~2996). Lower from `fd.fd_ret_ty` so a
65+
`Float`-returning fn declares an `f64` result.
66+
. *Locals* — `alloc_local` (line ~181) tracks only `(name, idx)`; the function's
67+
locals are emitted all-`i32`. Binding a float value (`let y = x + 1.0`) would
68+
`LocalSet` an f64 into an i32 slot → validation failure. Locals must carry a
69+
`val_type`, threaded through `alloc_local` and the locals-emission.
70+
. *Binop dispatch* — the `ExprFloatBinary` elaboration (mirrors slices 8b/9/10):
71+
`synth` records `Float`-typed binop nodes (three sites: the arith branch's
72+
`Float` case, the `comparison` branch's `Float` case, and the `==`/`!=` else
73+
branch when operands are `Float`); elaboration rewrites to `ExprFloatBinary`;
74+
codegen lowers to the f64 family (arith → f64 value; comparison → i32 bool).
75+
76+
Items 1–2 are small; item 3 (typed locals) is the load-bearing change and the
77+
main validation-risk surface; item 4 is the string-wall pattern again. A
78+
*narrow first slice* (params + returns + comparisons + stack-flowing arith,
79+
erroring on float `let`-bindings until typed locals land) makes `Float -> Int`
80+
classifiers like `band_of` compile without item 3, but is partial.
81+
82+
== Harness readiness
83+
84+
`proposals/nextgen-evangelist/affine-parity` already accepts Float arguments
85+
(non-integer values in a `{ values: [...] }` spec pass through as wasm f64; the
86+
result is read as i32). The moment float binop codegen lands, float-input brains
87+
(physics thresholds, geometry classifications, the ~12 float-domain modules
88+
marked `NO_NEW_BRAINS` in cluster C13/C14 purely for the integer-only ABI)
89+
become compilable and parity-testable with no further harness work.
Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
// SPDX-License-Identifier: AGPL-3.0-or-later
2+
// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
= String-wall slices 9–10 + completion capstone (2026-06-14)
4+
:toc: macro
5+
6+
toc::[]
7+
8+
== Context
9+
10+
The "string wall" is the family of `String`-typed operations that the wasm
11+
backend lowered to integer ops on the underlying `[len: i32][utf8 bytes]`
12+
*pointer* rather than on the string's bytes. A `String` value is an i32 pointer
13+
into linear memory, so any pointer-level integer op gives a wrong answer for two
14+
equal-valued strings that live at distinct heap addresses (e.g. a literal vs a
15+
string built at runtime).
16+
17+
Slices 1–7 established the byte-level string primitives (length, indexing,
18+
byte-scan helpers, `startsWith`/`contains`, the WASI `env_at`/`arg_at` string
19+
builders). Slice 8 split into 8a (a *sound-rejection guard* that loudly refused
20+
the syntactically-obvious string `++` cases codegen could not yet lower) and 8b
21+
(the type-directed `ExprStringConcat` lowering). This document records slices
22+
9 (equality) and 10 (relational) — which complete the wall — and the final
23+
hardening.
24+
25+
== The type-channel pattern (shared by 8b / 9 / 10)
26+
27+
Codegen is type-blind; it cannot tell from `a == b` whether `a` is `Int` or
28+
`String`. The fix routes the decision through the type checker, which *does*
29+
know:
30+
31+
1. *`Typecheck.synth`* records the physical AST node (`List.memq` identity) of
32+
every `String`-typed operator occurrence into a site list
33+
(`string_concat_sites` / `string_eq_sites` / `string_rel_sites`).
34+
2. *`Typecheck.elaborate_string_concat`* (run on the wasm-codegen path only)
35+
walks the program once and rewrites each recorded `ExprBinary` node into a
36+
dedicated AST node.
37+
3. *Codegen* lowers the dedicated node with a real byte-level routine.
38+
39+
This keeps the interpreter and non-wasm backends untouched (they never run the
40+
elaboration and handle the original `ExprBinary` directly), and it is
41+
*complete* — variable-to-variable cases are covered because the recording is
42+
type-directed, not syntactic.
43+
44+
== Slice 9 — `==` / `!=` (`ExprStringEq`)
45+
46+
* Equality is polymorphic (`type_of_binop` gives `'a -> 'a -> Bool`), so a
47+
`String` `==` lands in `synth`'s general `else` branch; recorded there when
48+
`repr lhs_ty = TCon "String"`.
49+
* `ExprStringEq (expr, expr, bool)` — the `bool` is `true` for `!=`.
50+
* Lowering: length guard, then a byte loop bounded by the (equal) length; `!=`
51+
negates with `I32Eqz`. The loop runs only after lengths match, so it never
52+
reads past either string.
53+
54+
== Slice 10 — `<` / `<=` / `>` / `>=` (`ExprStringRel`)
55+
56+
* Relational ops land in `synth`'s `comparison` branch (which already returns
57+
`Bool` for `String` per #458); recorded there.
58+
* `ExprStringRel (expr, expr, binary_op)` carries the operator (always one of
59+
`OpLt`/`OpLe`/`OpGt`/`OpGe`).
60+
* Lowering: byte-wise *lexicographic* compare — compare the common prefix
61+
unsigned (`I32LtU`/`I32GtU`), and on a tie the shorter string is smaller; the
62+
result `cmp ∈ {-1,0,1}` maps onto `cmp <signed-op> 0`. The loop is bounded at
63+
`min(len_a, len_b)` (via `Select`), so it never reads out of bounds.
64+
65+
== Final hardening
66+
67+
`gen_binop`'s `| OpConcat -> I32Add (* Placeholder *)` arm — a latent landmine
68+
that would have silently summed two pointers — is now a `failwith` guard. It is
69+
provably unreachable (string `++` → `ExprStringConcat`/8a-guard; list `++` →
70+
its own arm; compound-assign maps only `+= -= *= /=`), so the change is pure
71+
defensive hardening: a regression that ever routed `++` through `gen_binop`
72+
surfaces as a loud failure instead of a wrong answer.
73+
74+
== Verification
75+
76+
* `test/e2e/fixtures/string_eq.affine`, `string_rel.affine` + the slice-9 /
77+
slice-10 cases in `test/test_e2e.ml` (compile-after-elaboration).
78+
* Value checks (out-of-band, via Deno): equality and lexicographic ordering
79+
verified across decisive-byte, prefix-ordering, empty-string, equality, and
80+
built-vs-literal cases.
81+
* No regression: tens of thousands of `Int`-`==`/relational parity cases across
82+
the idaptik migration corpus pass unchanged (only `String` operands are
83+
recorded for elaboration; `Int`/`Bool`/`Float` are untouched).
84+
85+
== Status
86+
87+
*The string wall is complete.* `++`, `==`/`!=`, and `<`/`<=`/`>`/`>=` all lower
88+
correctly on the wasm target. The remaining string surface (interpolation,
89+
`format`, richer stdlib string functions) is additive, not a correctness wall.
90+
91+
NOTE: the parity harness passes integer arguments only, so brains compiled for
92+
it remain `Int(...)->Int`; exercising these string ops with real `String`-input
93+
consumers needs the string/float test-harness extension (separate work item).
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
// SPDX-License-Identifier: AGPL-3.0-or-later
2+
// SPDX-FileCopyrightText: 2025-2026 hyperpolymath
3+
//
4+
// Demo for affine-parity String argument support. `classify` exercises slice-9
5+
// String `==` against a literal; `str_cmp` exercises slice-9 + slice-10
6+
// comparing two RUNTIME-PROVIDED strings (pointer vs pointer) — the strongest
7+
// check that value (not pointer) comparison holds for JS-supplied strings.
8+
// (A Float case is omitted: float `<`/arithmetic codegen still emits i32 ops —
9+
// a separate "float wall" the harness is ready for once codegen is fixed.)
10+
11+
pub fn classify(s: String) -> Int {
12+
if s == "scan" { 1 } else { if s == "exit" { 2 } else { 0 } }
13+
}
14+
15+
pub fn str_cmp(a: String, b: String) -> Int {
16+
if a < b { -1 } else { if a == b { 0 } else { 1 } }
17+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
export default {
3+
affine: "string_float_demo.affine",
4+
cases: [
5+
{ export: "classify", args: [{ strings: ["scan", "exit", "foo", "sca", "scann", ""] }],
6+
oracle: (s) => (s === "scan" ? 1 : s === "exit" ? 2 : 0) },
7+
{ export: "str_cmp", args: [{ strings: ["a", "ab", "b", ""] }, { strings: ["a", "ab", "b", ""] }],
8+
oracle: (a, b) => (a < b ? -1 : a === b ? 0 : 1) },
9+
],
10+
};

proposals/nextgen-evangelist/affine-parity/parity.mjs

Lines changed: 71 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -17,15 +17,24 @@
1717
// which oracle.
1818
//
1919
//## ABI SCOPE (read this)
20-
// This runner handles the **scalar i32 ABI** only: every argument is an i32 and
21-
// every result is an i32. That is exactly the boundary the DESIGN-VISION
22-
// prescribes ("they pass primitives across the wasm boundary") and it covers
23-
// pure-integer co-processors such as SecurityRank. Array/string parameters use
24-
// a different convention -- `[len:i32 LE][utf8 bytes]` written into linear
25-
// memory plus an exported `__affine_alloc` -- and are a deliberate follow-on,
26-
// NOT implemented here. Exports taking [Int]/String params therefore can only be
27-
// invoked here in their nullary form (e.g. Kernel_IO's `main`, whose array
28-
// arguments are inlined inside the .affine source).
20+
// This runner handles i32 results over i32 / f64 / String arguments:
21+
// * i32 args -- swept as integer ranges/values (the original scalar ABI),
22+
// * f64 args -- any non-integer values in a `{ values: [...] }` spec are
23+
// passed through verbatim as wasm f64 (args are not coerced),
24+
// * String args -- written into linear memory as `[len:i32 LE][utf8 bytes]`
25+
// and passed BY POINTER (an i32). The string layout matches
26+
// the compiler's (codegen `gen_literal`). The oracle still
27+
// receives the original JS string, not the pointer.
28+
// Every result is read back as an i32 (`| 0`).
29+
//
30+
// String scratch memory: after instantiation the runner grows the module's
31+
// linear memory by one page (64 KiB) and writes string args into that fresh
32+
// page (reset before each call). Because the page sits above all of the
33+
// module's data and bump-heap base, a read-only string consumer (the common
34+
// case -- a classifier that reads its String arg and returns an Int) never
35+
// collides with it. A module that *allocates heavily during the call* before
36+
// reading its String arg could in principle reach the scratch page; such cases
37+
// should size their sweeps modestly or write a bespoke driver.
2938
//
3039
//## CONFIG SHAPE
3140
// A config is a `.mjs` module with a default export:
@@ -126,11 +135,44 @@ function expandArgSpec(spec, paramIndex) {
126135
return out;
127136
}
128137
if (spec && Array.isArray(spec.values)) return spec.values.slice();
138+
if (spec && Array.isArray(spec.strings)) return spec.strings.slice();
129139
throw new Error(
130-
`arg spec #${paramIndex} must be a number, a [lo,hi] range, or { values: [...] }`,
140+
`arg spec #${paramIndex} must be a number, a [lo,hi] range, { values: [...] }, or { strings: [...] }`,
131141
);
132142
}
133143

144+
// Build a writer for String args. Grows the module's linear memory by one page
145+
// and bump-allocates `[len:i32 LE][utf8]` strings into it, 4-byte aligned, so
146+
// each is a valid AffineScript string the wasm can read by pointer. Returns
147+
// null when the module exports no memory (then String args are a usage error).
148+
function makeStringWriter(memory) {
149+
if (!(memory instanceof WebAssembly.Memory)) return null;
150+
const oldPages = memory.grow(1); // fresh page above all module data + heap
151+
const base = oldPages * 65536;
152+
const enc = new TextEncoder();
153+
let bump = base;
154+
return {
155+
reset() {
156+
bump = base;
157+
},
158+
write(s) {
159+
const u = enc.encode(s);
160+
const need = 4 + u.length;
161+
// Grow if a long string would overrun the scratch page.
162+
if (bump + need > memory.buffer.byteLength) {
163+
memory.grow(Math.ceil(need / 65536) + 1);
164+
}
165+
const ptr = bump;
166+
const dv = new DataView(memory.buffer); // re-read: grow detaches the buffer
167+
dv.setInt32(ptr, u.length, true);
168+
new Uint8Array(memory.buffer, ptr + 4, u.length).set(u);
169+
bump = ptr + need;
170+
bump += (4 - (bump & 3)) & 3; // 4-byte align the next string
171+
return ptr;
172+
},
173+
};
174+
}
175+
134176
// Cartesian product of a list of value-lists. [] -> [[]] (the single empty tuple).
135177
function cartesian(lists) {
136178
return lists.reduce(
@@ -141,7 +183,7 @@ function cartesian(lists) {
141183

142184
// Run a single case (one export + its arg sweep + its oracle). Returns
143185
// { name, total, pass, failures: [{args, got, want}] }.
144-
function runCase(exports, kase, idx) {
186+
function runCase(exports, kase, idx, stringWriter) {
145187
const name = kase.name || kase.export || `case#${idx}`;
146188
const fn = exports[kase.export];
147189
if (typeof fn !== "function") {
@@ -159,7 +201,22 @@ function runCase(exports, kase, idx) {
159201
let pass = 0;
160202
const failures = [];
161203
for (const tuple of tuples) {
162-
const got = fn(...tuple) | 0; // normalise to i32
204+
// String args are written into scratch linear memory as [len][utf8] and
205+
// passed by pointer; the oracle still sees the original JS string. i32 /
206+
// f64 args pass through unchanged.
207+
let wasmArgs = tuple;
208+
if (tuple.some((v) => typeof v === "string")) {
209+
if (!stringWriter) {
210+
throw new Error(
211+
`case "${name}" passes a String arg but the module exports no "memory"`,
212+
);
213+
}
214+
stringWriter.reset();
215+
wasmArgs = tuple.map((v) =>
216+
typeof v === "string" ? stringWriter.write(v) : v
217+
);
218+
}
219+
const got = fn(...wasmArgs) | 0; // normalise result to i32
163220
const want = kase.oracle(...tuple) | 0;
164221
if (got === want) {
165222
pass++;
@@ -206,12 +263,13 @@ export async function runParity(configPath, { verbose = false } = {}) {
206263
}
207264

208265
const exports = await instantiate(outPath);
266+
const stringWriter = makeStringWriter(exports.memory);
209267

210268
let grandTotal = 0;
211269
let grandPass = 0;
212270
const results = [];
213271
cfg.cases.forEach((kase, i) => {
214-
const r = runCase(exports, kase, i);
272+
const r = runCase(exports, kase, i, stringWriter);
215273
results.push(r);
216274
grandTotal += r.total;
217275
grandPass += r.pass;

0 commit comments

Comments
 (0)