From 1fb7b3a05565e23aa3c1a8ca8a795b9baf24e957 Mon Sep 17 00:00:00 2001 From: "agon (KERN)" <292465531+KERN-Agon@users.noreply.github.com> Date: Thu, 25 Jun 2026 15:03:08 +0200 Subject: [PATCH 1/6] =?UTF-8?q?test(runner):=20array=20`.length`=20oracle?= =?UTF-8?q?=20=E2=80=94=20RED-at-base=203-leg=20spec=20+=20fences?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The discriminating oracle for the array `.length` read slice, authored BEFORE the impl so the runner change is built to this spec. RED-at-base: the certify cases abstain today (the `member` case admits only a caught-error `.message`); they turn green only when the runner reads array length. The fences already pass (abstaining is the correct fail-close at base). - packages/core/tests/runner-array-length.test.ts (new) — direct ReferenceRunner spec: 6 certify cases (count / empty-0 / nested TOP-LEVEL count / arithmetic flow / scalar bind / parenthesized receiver) + 14 fail-close fences (string, ASTRAL string, number, boolean, rebound, array-literal receiver, index-position receiver, chained member, non-`length` member, optional, computed, unbound, and two direct evalPortableValue checks). - packages/python/tests/kern-run-cli-differential.test.ts — 4 `.length` CERT entries (count / empty / nested top-count / arithmetic), every byte verified on real node + python3 via the emitter probe. - packages/cli/tests/run.test.ts — CLI exit-code contract: `.length` happy (count / empty / arithmetic, exit 0) + abstain (string / astral / optional / computed / non-`length` member, exit 2). Module doc updated. Only ARRAY `.length` certifies: a STRING receiver abstains because JS `.length` counts UTF-16 code units while Python `len()` counts code points — `"😀".length` is 2 in JS, 1 in Python (verified). Reference-only — the emitters already lower a portable array `.length` to `len(...)` (Python) / `.length` (TS). ⚔️ Forged by [Agon](https://github.com/KERNlang/agon) Co-Authored-By: agon (KERN) <292465531+KERN-Agon@users.noreply.github.com> --- packages/cli/tests/run.test.ts | 61 ++++++- .../core/tests/runner-array-length.test.ts | 163 ++++++++++++++++++ .../tests/kern-run-cli-differential.test.ts | 13 ++ 3 files changed, 233 insertions(+), 4 deletions(-) create mode 100644 packages/core/tests/runner-array-length.test.ts diff --git a/packages/cli/tests/run.test.ts b/packages/cli/tests/run.test.ts index 2b84082c..37d419d5 100644 --- a/packages/cli/tests/run.test.ts +++ b/packages/cli/tests/run.test.ts @@ -25,10 +25,10 @@ * * Executable surface is exactly what the runner certifies today: print / let / * assign / for / if / while / each / return / portable arithmetic / portable - * array-literal binding / literal in-bounds array index reads. Constructs the - * runner does not yet execute over PRODUCTION IR (branch/try/throw, fmt - * interpolation, whole-array rendering, objects, dynamic array index reads) - * ABSTAIN -> exit 2, by design. + * array-literal binding / literal in-bounds array index reads / array `.length`. + * Constructs the runner does not yet execute over PRODUCTION IR (branch/try/throw, + * fmt interpolation, whole-array rendering, objects, dynamic array index reads, + * string `.length`) ABSTAIN -> exit 2, by design. * * Every expected stdout byte below was verified empirically against the built * runner before this oracle was authored (the `(1/3)*3 != 1` lesson). @@ -234,6 +234,27 @@ describe('kern run — executes a void main and replays stdout (exit 0)', () => expect(r.status).toBe(0); expect(r.stderr).toBe(''); }); + + test('ARRAY LENGTH: reads the element count', () => { + const r = runProgram(['let name=xs value="[1,2,3]"', 'print value="xs.length"']); + expect(r.stdout).toBe('3\n'); + expect(r.status).toBe(0); + expect(r.stderr).toBe(''); + }); + + test('ARRAY LENGTH: an empty array reads 0', () => { + const r = runProgram(['let name=xs value="[]"', 'print value="xs.length"']); + expect(r.stdout).toBe('0\n'); + expect(r.status).toBe(0); + expect(r.stderr).toBe(''); + }); + + test('ARRAY LENGTH: the length value flows into arithmetic', () => { + const r = runProgram(['let name=xs value="[1,2,3]"', 'print value="xs.length - 1"']); + expect(r.stdout).toBe('2\n'); + expect(r.status).toBe(0); + expect(r.stderr).toBe(''); + }); }); // ── FAIL-CLOSE ATOMICITY: abstain produces NO stdout, exit 2 ────────────────── @@ -308,6 +329,38 @@ describe('kern run — abstains atomically on non-portable ops (exit 2, no stdou expect(r.stdout).toBe(''); expect(r.status).toBe(2); }); + + test('STRING `.length` abstains (JS UTF-16 units vs Python code points)', () => { + // ASCII happens to agree, but the runner rule is arrays-only: a string + // receiver fails closed so an astral case can never silently diverge. + const r = runProgram(['let name=s value="\\"hello\\""', 'print value="s.length"']); + expect(r.stdout).toBe(''); + expect(r.status).toBe(2); + }); + + test('ASTRAL string `.length` abstains (the real divergence: JS 2 vs Python 1)', () => { + const r = runProgram(['let name=s value="\\"😀\\""', 'print value="s.length"']); + expect(r.stdout).toBe(''); + expect(r.status).toBe(2); + }); + + test('OPTIONAL `xs?.length` abstains (outside the portable domain)', () => { + const r = runProgram(['let name=xs value="[1,2,3]"', 'print value="xs?.length"']); + expect(r.stdout).toBe(''); + expect(r.status).toBe(2); + }); + + test("COMPUTED `xs['length']` abstains (a string-literal index is not certified)", () => { + const r = runProgram(['let name=xs value="[1,2,3]"', 'print value="xs[\'length\']"']); + expect(r.stdout).toBe(''); + expect(r.status).toBe(2); + }); + + test('a NON-`length` member on an array (`xs.foo`) abstains', () => { + const r = runProgram(['let name=xs value="[1,2,3]"', 'print value="xs.foo"']); + expect(r.stdout).toBe(''); + expect(r.status).toBe(2); + }); }); // ── ENTRY RESOLUTION: deterministic diagnostics, exit 2, no stdout ──────────── diff --git a/packages/core/tests/runner-array-length.test.ts b/packages/core/tests/runner-array-length.test.ts new file mode 100644 index 00000000..d1100e13 --- /dev/null +++ b/packages/core/tests/runner-array-length.test.ts @@ -0,0 +1,163 @@ +/** + * ReferenceRunner — array `.length` read (continues slice-2a/2b array values). + * + * Slice-2a bound array literals + `each`; slice-2b read an element by a literal + * index. This slice lets the ReferenceRunner read an array's ELEMENT COUNT so a + * program can ask how big an array is on its own runtime: + * + * let xs = [1,2,3] → print xs.length → 3 + * + * Scope is the SOUND minimum, mirroring the index slice's receiver fence: + * `.length` certifies ONLY as a NON-optional `.length` member on a BARE + * IDENTIFIER that is bound to a portable array. The result is the array's + * element count — a non-negative safe integer that is byte-identical on all + * three legs: `kern run` (`arr.length`), emitted TS (`arr.length`), emitted + * Python (`len(arr)`). + * + * Only ARRAYS certify. A STRING receiver ABSTAINS even though `len()` reads a + * string too, because JS `.length` counts UTF-16 code units while Python `len()` + * counts code points — `"😀".length` is 2 in JS, 1 in Python (verified on real + * node + python3), so string `.length` is NOT portable. Every other receiver + * (number / boolean / null / object / decimal / caught-error) and every + * non-ident receiver (`[1,2,3].length`, `xs[0].length`, `xs.length.foo`), + * optional (`xs?.length`), computed (`xs['length']`), or non-`length` member + * (`xs.foo`) ABSTAINS. + * + * Reference-only change: an abstaining program is never certified and never + * reaches the emitter differential — the emitters already lower a portable + * array `.length` to `len(...)` (Python) / `.length` (TS), so no codegen change + * is needed. The length VALUE is an ordinary safe integer, so it flows through + * arithmetic / comparison / binding / print with no further hazard. + * + * RED-at-base: `.length` abstains today (the `member` case admits only a + * caught-error `.message`); turns GREEN only when the runner reads array length. + */ + +import { makeEnv, ReferenceRunnerError, referenceRunSequence, registerAllContracts } from '../src/index.js'; +import { evalPortableValue } from '../src/ir/semantics/portable-scalar.js'; +import type { IRNode } from '../src/types.js'; +import type { ValueIR } from '../src/value-ir.js'; + +beforeAll(() => { + registerAllContracts(); +}); + +/** Run a sequence of body statements and return replayed stdout, as `kern run` + * renders it (each `{op:'stdout'}` event + "\n"). */ +function runStdout(nodes: IRNode[]): string { + const trace = referenceRunSequence(nodes, makeEnv()); + return trace.events + .filter((e): e is { op: 'stdout'; text: string } => e.op === 'stdout') + .map((e) => `${e.text}\n`) + .join(''); +} + +function letBind(name: string, value: string): IRNode { + return { type: 'let', props: { name, value } }; +} +function print(expr: string): IRNode { + return { type: 'print', props: { value: expr } }; +} + +// ── CERTIFY: `.length` reads the element count (3-leg portable) ──── +describe('runner array length — element-count reads certify (3-leg portable)', () => { + it('reads the element count of a non-empty array', () => { + expect(runStdout([letBind('xs', '[1,2,3]'), print('xs.length')])).toBe('3\n'); + }); + + it('reads 0 for an empty array (an off-by-one / undefined impl would miss)', () => { + expect(runStdout([letBind('xs', '[]'), print('xs.length')])).toBe('0\n'); + }); + + it('counts TOP-LEVEL elements of a nested array, not leaves', () => { + // A leaf-counting impl would print 5 here; the contract is top-level cardinality. + expect(runStdout([letBind('rows', '[[1,2],[3,4,5]]'), print('rows.length')])).toBe('2\n'); + }); + + it('the length value flows into arithmetic (xs.length - 1)', () => { + expect(runStdout([letBind('xs', '[1,2,3]'), print('xs.length - 1')])).toBe('2\n'); + }); + + it('the length value binds to a scalar and reads back', () => { + expect(runStdout([letBind('xs', '[1,2,3]'), letBind('n', 'xs.length'), print('n')])).toBe('3\n'); + }); + + it('a parenthesized receiver certifies (parens strip to the bare ident)', () => { + // `(xs).length` parses to a member on the bare ident — TS `(xs).length` and + // Python `len(xs)` both read 3, so certifying it is sound. + expect(runStdout([letBind('xs', '[1,2,3]'), print('(xs).length')])).toBe('3\n'); + }); +}); + +// ── FAIL-CLOSE: every non-(array-ident `.length`) form ABSTAINS ─────────────── +describe('runner array length — fail-close fences (abstain, never a value)', () => { + const abstains = (nodes: IRNode[]) => + expect(() => referenceRunSequence(nodes, makeEnv())).toThrow(ReferenceRunnerError); + + it('STRING `.length` abstains (JS UTF-16 units vs Python code points)', () => { + abstains([letBind('s', '"abc"'), print('s.length')]); + }); + + it('ASTRAL string `.length` abstains (the real divergence: JS 2 vs Python 1)', () => { + abstains([letBind('s', '"😀"'), print('s.length')]); + }); + + it('NUMBER receiver `.length` abstains', () => { + abstains([letBind('n', '5'), print('n.length')]); + }); + + it('BOOLEAN receiver `.length` abstains', () => { + abstains([letBind('b', 'true'), print('b.length')]); + }); + + it('a REBOUND ident (array name later holding a scalar) abstains', () => { + // The receiver must be an array AT READ TIME; a scalar binding fails closed. + abstains([letBind('xs', '1'), print('xs.length')]); + }); + + it('ARRAY-LITERAL receiver `[1,2,3].length` abstains (object is not a bare ident)', () => { + abstains([print('[1,2,3].length')]); + }); + + it('INDEX-position receiver `xs[0].length` abstains (object is an index node)', () => { + abstains([letBind('xs', '[[1,2],[3]]'), print('xs[0].length')]); + }); + + it('CHAINED member `xs.length.foo` abstains (object is a member node)', () => { + abstains([letBind('xs', '[1,2,3]'), print('xs.length.foo')]); + }); + + it('a NON-`length` member on an array (`xs.foo`) abstains', () => { + abstains([letBind('xs', '[1,2,3]'), print('xs.foo')]); + }); + + it('OPTIONAL `xs?.length` abstains (outside the portable domain)', () => { + abstains([letBind('xs', '[1,2,3]'), print('xs?.length')]); + }); + + it("COMPUTED `xs['length']` abstains (a string-literal index is not a safe-int literal)", () => { + abstains([letBind('xs', '[1,2,3]'), print("xs['length']")]); + }); + + it('an UNBOUND ident `.length` abstains', () => { + abstains([print('ys.length')]); + }); + + // Direct evaluator checks — pin the helper's array-vs-non-array decision. + it('evalPortableValue returns the count for `.length` on an array binding', () => { + const expr: ValueIR = { + kind: 'member', + object: { kind: 'ident', name: 'xs' }, + property: 'length', + optional: false, + }; + const env = makeEnv({ bindings: new Map([['xs', [10, 20, 30]]]) }); + expect(evalPortableValue(expr, env)).toBe(3); + }); + + it('evalPortableValue abstains on `.length` on a non-array (string) binding', () => { + const expr: ValueIR = { kind: 'member', object: { kind: 'ident', name: 's' }, property: 'length', optional: false }; + const env = makeEnv({ bindings: new Map([['s', 'abc']]) }); + expect(() => evalPortableValue(expr, env)).toThrow(/portable/); + }); +}); diff --git a/packages/python/tests/kern-run-cli-differential.test.ts b/packages/python/tests/kern-run-cli-differential.test.ts index 25ebb54a..5121cf31 100644 --- a/packages/python/tests/kern-run-cli-differential.test.ts +++ b/packages/python/tests/kern-run-cli-differential.test.ts @@ -207,6 +207,19 @@ const CERT: Array<[string, string[], string]> = [ ['let name=xs value="[true,false]"', 'print value="xs[1]"'], 'false\n', ], + // ── array `.length` read: element count is byte-identical 3-leg ────────────── + // `xs.length` lowers to TS `xs.length` and Python `len(xs)`; for an array both + // are the element count. STRING `.length` is NOT certified (JS UTF-16 units vs + // Python code points diverge on astral chars), so it is absent here. + ['array length reads the element count', ['let name=xs value="[1,2,3]"', 'print value="xs.length"'], '3\n'], + ['empty array length is 0', ['let name=xs value="[]"', 'print value="xs.length"'], '0\n'], + [ + // A leaf-counting impl would print 5; the contract is TOP-LEVEL cardinality. + 'nested array length counts top-level elements', + ['let name=xs value="[[1,2],[3,4,5]]"', 'print value="xs.length"'], + '2\n', + ], + ['array length flows into arithmetic', ['let name=xs value="[1,2,3]"', 'print value="xs.length - 1"'], '2\n'], ]; execDescribe('kern run — 3-leg CLI differential (kern-run === ts === py)', () => { From 0532c5f14af3e062a917e23f98bafa24a7fa265e Mon Sep 17 00:00:00 2001 From: "agon (KERN)" <292465531+KERN-Agon@users.noreply.github.com> Date: Thu, 25 Jun 2026 15:36:21 +0200 Subject: [PATCH 2/6] =?UTF-8?q?feat(runner):=20array=20`.length`=20read=20?= =?UTF-8?q?=E2=80=94=20element=20count=20on=20KERN's=20own=20runtime?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The ReferenceRunner — the executor `kern run` uses — now READS an array's ELEMENT COUNT, so a program can ask how big an array is natively: let xs = [1,2,3] -> print xs.length -> 3 This continues the array slices (2a literal binding + each, 2b literal index). An array branch is added to the `member` case of `evalPortableValue`, BEFORE the caught-error `.message` handling and behind the SAME fences: a `.length` read certifies ONLY as a non-optional `.length` on a BARE IDENTIFIER bound to a portable array, and returns the element count — a non-negative safe integer. Everything else throws -> the runner ABSTAINS. Only ARRAYS certify. A STRING `.length` must NOT: JS `.length` counts UTF-16 code units while Python `len()` counts code points, so `"😀".length` is 2 in JS and 1 in Python (verified on real node + python3). `Array.isArray` excludes strings, numbers, booleans, decimals, and caught errors, so every non-array receiver falls through and abstains. Non-ident receivers (`[1,2,3].length`, `xs[0].length`, `xs.length.foo`), optional (`xs?.length`), computed (`xs['length']`), a non-`length` member (`xs.foo`), rebound, and unbound idents all abstain too. Reference-only change: an abstaining program is never certified and never reaches the emitter differential. The emitters ALREADY lower a portable array `.length` to `len(...)` (Python) / `.length` (TS), so no codegen change is needed; the 3-leg differential passes as-authored. The length value is an ordinary safe integer, so it flows through arithmetic / comparison / binding / print with no further hazard. `evalPortableValue` is internal to the ir/semantics runner layer (not re-exported), so `.length` extends only the runner's scalar contexts (print / if / while / fmt / assign), consistently fenced. The slice-2a `.length access abstains (deferred)` fence is updated to assert a STRING `.length` abstains (array `.length` now certifies) — mirroring how slice-2b relaxed slice-2a's in-bounds index fence. Gate: array-length spec 20/20 + array-values 13/13 + array-index 25/25 + runner-entry-import-graph + ir-semantics neighborhood 164/164 + CLI run.test 52/52 + 3-leg differential 23/23 (0 skipped) + biome + docs:contracts:check. Planned with agon brainstorm; built by codex via agon conquer against the RED-at-base oracle; reviewed by the full agon roster. ⚔️ Forged by [Agon](https://github.com/KERNlang/agon) Co-Authored-By: agon (KERN) <292465531+KERN-Agon@users.noreply.github.com> --- .../core/src/ir/semantics/portable-scalar.ts | 23 +++++++++++-------- .../core/tests/runner-array-values.test.ts | 10 +++++--- 2 files changed, 20 insertions(+), 13 deletions(-) diff --git a/packages/core/src/ir/semantics/portable-scalar.ts b/packages/core/src/ir/semantics/portable-scalar.ts index 1e6376de..31e947a4 100644 --- a/packages/core/src/ir/semantics/portable-scalar.ts +++ b/packages/core/src/ir/semantics/portable-scalar.ts @@ -256,20 +256,23 @@ export function evalPortableValue(node: ValueIR, env: SemanticEnv): PortableScal ? evalPortableValue(node.consequent, env) : evalPortableValue(node.alternate, env); case 'member': { - // Error-substrate Slice 1 — the ONLY admitted member read in the portable - // domain is `.message` (a non-optional `.message` on - // an ident resolving to a tagged caught-error value). It returns the - // EVALUATED LITERAL message stored when the explicit `throw new Error("…")` - // was caught — byte-identical to TS `e.message` and Python `str(e)`. - // EVERYTHING else (a different property, an optional `?.`, a non-ident - // object, an ident that is not a caught error) throws → the runner - // ABSTAINS. This is the fail-close fence: `e.name`/`e.stack`/`e` (bare) - // and any non-caught-error member access never produce a one-leg value. + // Member reads are admitted only for the explicit portable slices: + // `.length` and `.message`. Both must be + // non-optional reads on a bare identifier. Everything else throws -> the + // runner ABSTAINS rather than producing a one-leg value. if (node.optional) throw new Error('portable: optional member access is outside the portable scalar domain'); if (node.object.kind !== 'ident') { - throw new Error('portable: member access is only admitted on a caught-error binding'); + throw new Error('portable: member access is only admitted on an array or caught-error binding'); } const obj = getBinding(env, node.object.name); + if (Array.isArray(obj)) { + // Array `.length` is portable; string `.length` is not (JS counts UTF-16 + // code units while Python counts code points), so only arrays pass here. + if (node.property !== 'length') { + throw new Error(`portable: array has no portable property "${node.property}" (only .length is admitted)`); + } + return obj.length; + } if (!isCaughtErrorValue(obj)) { throw new Error(`portable: member access on "${node.object.name}" is outside the portable scalar domain`); } diff --git a/packages/core/tests/runner-array-values.test.ts b/packages/core/tests/runner-array-values.test.ts index a8abb74e..53ab0d7c 100644 --- a/packages/core/tests/runner-array-values.test.ts +++ b/packages/core/tests/runner-array-values.test.ts @@ -22,7 +22,8 @@ * - OUT-OF-BOUNDS / negative / non-integer index access (TS undefined vs Py * IndexError/wraparound/TypeError — not 3-leg portable). In-bounds index * reads now CERTIFY (slice-2b, see runner-array-index.test.ts), - * - `.length`, `assign` to an array binding, methods / spread / concat. + * - `assign` to an array binding, methods / spread / concat. Array `.length` + * now CERTIFIES (see runner-array-length.test.ts); string `.length` abstains. * * Every expected value here was verified empirically on the REAL emitters * (node + python3) before authoring — this is RED-at-base (arrays abstain today) @@ -115,8 +116,11 @@ describe('runner array values — fail-close fences (abstain, never a value)', ( abstains([letArr('xs', '[1,2,3]'), print('xs[5]')]); }); - it('.length access abstains (deferred)', () => { - abstains([letArr('xs', '[1,2,3]'), print('xs.length')]); + it('STRING `.length` abstains (array `.length` now certifies — see runner-array-length.test.ts)', () => { + // Array `.length` reads the element count as of the array-length slice; a + // STRING `.length` stays fenced because JS counts UTF-16 code units while + // Python `len()` counts code points (`"😀".length` is 2 vs 1). + abstains([letArr('s', '"abc"'), print('s.length')]); }); it('a non-integer FLOAT element abstains at binding time', () => { From 4c039cb2c7b077ff914a3e9161cddd2a6320187e Mon Sep 17 00:00:00 2001 From: "agon (KERN)" <292465531+KERN-Agon@users.noreply.github.com> Date: Thu, 25 Jun 2026 15:43:15 +0200 Subject: [PATCH 3/6] =?UTF-8?q?fix(runner):=20array=20`.length`=20review?= =?UTF-8?q?=20fixes=20=E2=80=94=20hasBinding=20diagnostics=20+=20fence=20c?= =?UTF-8?q?overage?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Full-roster agon review (4 engines clean; kimi 2 important + nits). Triaged: - [important 0.90] Member case lacked a hasBinding check (unlike the sibling index case), so an UNBOUND receiver failed with the generic "outside portable scalar domain" instead of a precise "binding not found". Still abstained either way — diagnostics, not soundness — but now consistent with the index case. - [important 0.60] Parenthesized-receiver test "may not match parser" — REFUTED: `parseExpression("(xs).length")` yields a member on a bare ident (verified) and the test is green; it documents real, sound certifying behavior. Kept. - nits adopted: NULL and DECIMAL (tagged-object) receiver fences added, a nested-array TOP-LEVEL-count CLI happy test added, and the direct-helper test renamed from "abstains" to "throws" (abstain is runner-level terminology). Gate: array-length 24/24 + array-values 13/13 + array-index 25/25 + CLI 53/53 + biome. No behavior change to certified output; abstain outcomes unchanged. ⚔️ Forged by [Agon](https://github.com/KERNlang/agon) Co-Authored-By: agon (KERN) <292465531+KERN-Agon@users.noreply.github.com> --- packages/cli/tests/run.test.ts | 7 +++++++ packages/core/src/ir/semantics/portable-scalar.ts | 6 ++++++ packages/core/tests/runner-array-length.test.ts | 12 +++++++++++- 3 files changed, 24 insertions(+), 1 deletion(-) diff --git a/packages/cli/tests/run.test.ts b/packages/cli/tests/run.test.ts index 37d419d5..eef8b61f 100644 --- a/packages/cli/tests/run.test.ts +++ b/packages/cli/tests/run.test.ts @@ -249,6 +249,13 @@ describe('kern run — executes a void main and replays stdout (exit 0)', () => expect(r.stderr).toBe(''); }); + test('ARRAY LENGTH: a nested array counts TOP-LEVEL elements (not leaves)', () => { + const r = runProgram(['let name=xs value="[[1,2],[3,4,5]]"', 'print value="xs.length"']); + expect(r.stdout).toBe('2\n'); + expect(r.status).toBe(0); + expect(r.stderr).toBe(''); + }); + test('ARRAY LENGTH: the length value flows into arithmetic', () => { const r = runProgram(['let name=xs value="[1,2,3]"', 'print value="xs.length - 1"']); expect(r.stdout).toBe('2\n'); diff --git a/packages/core/src/ir/semantics/portable-scalar.ts b/packages/core/src/ir/semantics/portable-scalar.ts index 31e947a4..7902c46a 100644 --- a/packages/core/src/ir/semantics/portable-scalar.ts +++ b/packages/core/src/ir/semantics/portable-scalar.ts @@ -264,6 +264,12 @@ export function evalPortableValue(node: ValueIR, env: SemanticEnv): PortableScal if (node.object.kind !== 'ident') { throw new Error('portable: member access is only admitted on an array or caught-error binding'); } + // Resolve the binding explicitly (mirrors the `index` case) so an UNBOUND + // receiver fails with a precise "binding not found" rather than the generic + // out-of-domain message. Either way the runner abstains; this is diagnostics. + if (!hasBinding(env, node.object.name)) { + throw new Error(`portable: binding "${node.object.name}" not found`); + } const obj = getBinding(env, node.object.name); if (Array.isArray(obj)) { // Array `.length` is portable; string `.length` is not (JS counts UTF-16 diff --git a/packages/core/tests/runner-array-length.test.ts b/packages/core/tests/runner-array-length.test.ts index d1100e13..ad7603ab 100644 --- a/packages/core/tests/runner-array-length.test.ts +++ b/packages/core/tests/runner-array-length.test.ts @@ -110,6 +110,16 @@ describe('runner array length — fail-close fences (abstain, never a value)', ( abstains([letBind('b', 'true'), print('b.length')]); }); + it('NULL receiver `.length` abstains', () => { + abstains([letBind('n', 'null'), print('n.length')]); + }); + + it('DECIMAL (tagged-object) receiver `.length` abstains', () => { + // A non-array, non-caught-error OBJECT receiver — distinct code path from the + // scalar receivers above — must fail closed too. + abstains([letBind('d', 'Decimal.of("1")'), print('d.length')]); + }); + it('a REBOUND ident (array name later holding a scalar) abstains', () => { // The receiver must be an array AT READ TIME; a scalar binding fails closed. abstains([letBind('xs', '1'), print('xs.length')]); @@ -155,7 +165,7 @@ describe('runner array length — fail-close fences (abstain, never a value)', ( expect(evalPortableValue(expr, env)).toBe(3); }); - it('evalPortableValue abstains on `.length` on a non-array (string) binding', () => { + it('evalPortableValue throws on `.length` on a non-array (string) binding', () => { const expr: ValueIR = { kind: 'member', object: { kind: 'ident', name: 's' }, property: 'length', optional: false }; const env = makeEnv({ bindings: new Map([['s', 'abc']]) }); expect(() => evalPortableValue(expr, env)).toThrow(/portable/); From b1de5b01cc4b0c39a7de40859523bf63213e7a38 Mon Sep 17 00:00:00 2001 From: "agon (KERN)" <292465531+KERN-Agon@users.noreply.github.com> Date: Thu, 25 Jun 2026 16:14:10 +0200 Subject: [PATCH 4/6] test(runner): dynamic for-counter index + `.length` for-bound oracle (RED-at-base) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The discriminating 3-leg oracle for the dynamic-index slice, authored BEFORE the impl. RED-at-base: the certify cases abstain today (`for to=xs.length` has no member case in for's evalValue, and the index case rejects idents); they turn green only when the runner gains the `.length` for-bound + for-counter integer provenance. Fences already pass (abstaining is the correct fail-close at base). - packages/core/tests/runner-dynamic-index.test.ts (new) — direct ReferenceRunner spec: 6 certify (headline `for i=0..xs.length: xs[i]`, integer-literal bound, reverse step -1, stepped, empty range, `.length`-bound alone) + 8 fail-close fences (plain let index, THE FLOAT HOLE `let j=4/2; xs[j]`, non-transitive `let j=i`, assign-clears-provenance, arithmetic `xs[i+1]`, OOB atomic, negative counter, `each` binding not provenanced). - packages/python/tests/kern-run-cli-differential.test.ts — 4 `.length`/counter CERT entries (headline, stepped, reverse, `.length`-bound alone), every byte verified on real node + python3 via the emitter probe. - packages/cli/tests/run.test.ts — CLI exit-code contract: dynamic-index happy (headline, reverse, exit 0) + abstain (OOB ATOMIC no-partial-stdout, negative counter, arithmetic-on-counter, non-counter let index, exit 2). Module doc updated. - packages/core/tests/runner-array-index.test.ts — the slice-2b "for-loop variable index abstains (deferred)" fence is updated: a bare for-counter now CERTIFIES (see runner-dynamic-index.test.ts); arithmetic on the counter stays fenced. Mirrors how `.length` relaxed slice-2a's fence. Design: a `for` counter is a GUARANTEED safe integer, so `xs[i]` is byte-identical 3-leg WITHOUT proving arbitrary arithmetic is int-exact — provenance comes from the loop construct, tracked as per-scope binding metadata (set only by `for`, cleared by any reassignment/shadow), not transitive. Reference-only: the emitters already lower `for i --- packages/cli/tests/run.test.ts | 59 +++++- .../core/tests/runner-array-index.test.ts | 13 +- .../core/tests/runner-dynamic-index.test.ts | 168 ++++++++++++++++++ .../tests/kern-run-cli-differential.test.ts | 25 +++ 4 files changed, 257 insertions(+), 8 deletions(-) create mode 100644 packages/core/tests/runner-dynamic-index.test.ts diff --git a/packages/cli/tests/run.test.ts b/packages/cli/tests/run.test.ts index eef8b61f..a9d291a1 100644 --- a/packages/cli/tests/run.test.ts +++ b/packages/cli/tests/run.test.ts @@ -25,10 +25,11 @@ * * Executable surface is exactly what the runner certifies today: print / let / * assign / for / if / while / each / return / portable arithmetic / portable - * array-literal binding / literal in-bounds array index reads / array `.length`. + * array-literal binding / literal in-bounds array index reads / array `.length` + * (value AND as a for-range bound) / for-counter dynamic index reads (`xs[i]`). * Constructs the runner does not yet execute over PRODUCTION IR (branch/try/throw, - * fmt interpolation, whole-array rendering, objects, dynamic array index reads, - * string `.length`) ABSTAIN -> exit 2, by design. + * fmt interpolation, whole-array rendering, objects, NON-counter dynamic index + * reads, arithmetic-on-counter index, string `.length`) ABSTAIN -> exit 2. * * Every expected stdout byte below was verified empirically against the built * runner before this oracle was authored (the `(1/3)*3 != 1` lesson). @@ -262,6 +263,28 @@ describe('kern run — executes a void main and replays stdout (exit 0)', () => expect(r.status).toBe(0); expect(r.stderr).toBe(''); }); + + test('DYNAMIC INDEX: iterate an array by for-counter over its length (headline)', () => { + const r = runProgram([ + 'let name=xs value="[10,20,30]"', + 'for name=i from="0" to="xs.length"', + ' print value="xs[i]"', + ]); + expect(r.stdout).toBe('10\n20\n30\n'); + expect(r.status).toBe(0); + expect(r.stderr).toBe(''); + }); + + test('DYNAMIC INDEX: a reverse for-counter reads back-to-front', () => { + const r = runProgram([ + 'let name=xs value="[10,20,30]"', + 'for name=i from="2" to="-1" step="-1"', + ' print value="xs[i]"', + ]); + expect(r.stdout).toBe('30\n20\n10\n'); + expect(r.status).toBe(0); + expect(r.stderr).toBe(''); + }); }); // ── FAIL-CLOSE ATOMICITY: abstain produces NO stdout, exit 2 ────────────────── @@ -368,6 +391,36 @@ describe('kern run — abstains atomically on non-portable ops (exit 2, no stdou expect(r.stdout).toBe(''); expect(r.status).toBe(2); }); + + test('ATOMICITY: an OUT-OF-BOUNDS for-counter iteration suppresses ALL prior stdout', () => { + // for i in 0..5 over a length-3 array: at i=3 TS reads undefined, Python raises. + // The 10/20/30 from i=0..2 must NOT leak — the whole program abstains. + const r = runProgram(['let name=xs value="[10,20,30]"', 'for name=i from="0" to="5"', ' print value="xs[i]"']); + expect(r.stdout).toBe(''); + expect(r.status).toBe(2); + }); + + test('a NEGATIVE for-counter (reverse past 0) abstains', () => { + const r = runProgram([ + 'let name=xs value="[10,20,30]"', + 'for name=i from="2" to="-2" step="-1"', + ' print value="xs[i]"', + ]); + expect(r.stdout).toBe(''); + expect(r.status).toBe(2); + }); + + test('ARITHMETIC on a for-counter index (`xs[i + 1]`) abstains (out of slice)', () => { + const r = runProgram(['let name=xs value="[10,20,30]"', 'for name=i from="0" to="2"', ' print value="xs[i + 1]"']); + expect(r.stdout).toBe(''); + expect(r.status).toBe(2); + }); + + test('a NON-counter (plain let) index abstains even when in-bounds', () => { + const r = runProgram(['let name=xs value="[10,20,30]"', 'let name=j value="4 / 2"', 'print value="xs[j]"']); + expect(r.stdout).toBe(''); + expect(r.status).toBe(2); + }); }); // ── ENTRY RESOLUTION: deterministic diagnostics, exit 2, no stdout ──────────── diff --git a/packages/core/tests/runner-array-index.test.ts b/packages/core/tests/runner-array-index.test.ts index 05dd10a4..8f4d045b 100644 --- a/packages/core/tests/runner-array-index.test.ts +++ b/packages/core/tests/runner-array-index.test.ts @@ -165,14 +165,17 @@ describe('runner array index — fail-close fences (abstain, never a value)', () abstains([letArr('xs', '[10,20,30]'), print('xs[05]')]); }); - it('an IDENT (bound variable) index abstains (deferred — dynamic indexing)', () => { - // Even in-bounds: a variable can hold a Python float the reference cannot rule - // out by value -> abstain until integer-provenance exists. + it('a plain LET-bound (non-counter) ident index abstains (could be a Python float)', () => { + // Even in-bounds: a plain `let` binding can hold a Python float the reference + // cannot rule out by value -> abstain. A for-COUNTER now certifies via + // integer-provenance (see runner-dynamic-index.test.ts); a plain let does not. abstains([letArr('xs', '[5,6,7]'), letScalar('j', '2'), print('xs[j]')]); }); - it('a for-loop variable index abstains (deferred — dynamic indexing)', () => { - abstains([letArr('xs', '[10,20,30]'), forLoop('i', '0', '3', print('xs[i]'))]); + it('ARITHMETIC on a for-loop counter index abstains (bare counter certifies; `i+1` deferred)', () => { + // `xs[i]` with `i` a for-counter now CERTIFIES (runner-dynamic-index.test.ts); + // arithmetic on the counter stays fenced (overflow / negative-modulo proof). + abstains([letArr('xs', '[10,20,30]'), forLoop('i', '0', '3', print('xs[i + 1]'))]); }); it('INDEX-POSITION nesting `xs[ys[0]]` abstains (a nested index is not a literal)', () => { diff --git a/packages/core/tests/runner-dynamic-index.test.ts b/packages/core/tests/runner-dynamic-index.test.ts new file mode 100644 index 00000000..eaf17a5e --- /dev/null +++ b/packages/core/tests/runner-dynamic-index.test.ts @@ -0,0 +1,168 @@ +/** + * ReferenceRunner — DYNAMIC array index via for-counter integer-provenance + * (continues the array slices 2a bind+each / 2b literal index / `.length`). + * + * Slice 2b read an element only by a BARE safe-integer LITERAL because a + * `let`-bound number index can be a Python float the reference cannot rule out + * by value (`let j = 4 / 2` is 2 in JS/ref but 2.0 in Python → `xs[j]` is xs[2] + * in TS, TypeError in Python). This slice lets the runner read `xs[i]` when `i` + * is a `for` COUNTER, because a `for` counter is a GUARANTEED safe integer (the + * `for` contract enforces `Number.isSafeInteger` on from/to/step and steps by an + * integer), so it is an int on all three legs by construction — the provenance + * comes from the loop, not a value check: + * + * let xs = [10,20,30] + * for i in 0..xs.length: print xs[i] → 10 / 20 / 30 + * + * Two coupled capabilities ship together so the headline works: + * (A) `.length` as a `for` RANGE BOUND (`for i from=0 to=xs.length`), and + * (B) a for-counter as an array INDEX (`xs[i]`). + * + * SCOPE — `xs[i]` certifies ONLY when `i` is a BARE ident that is + * integer-provenanced (currently: the live counter of an enclosing `for`). + * Provenance is per-scope binding metadata, set ONLY by the `for` contract and + * CLEARED by any reassignment/shadowing, so it can never outlive an int value: + * - `let j = 4 / 2; xs[j]` → abstain (a plain let is not provenanced) + * - `for i..: let j = i; xs[j]` → abstain (provenance is NOT transitive) + * - `for i..: assign i = 4/2; xs[i]` → abstain (assign clears provenance) + * - `xs[i + 1]` → abstain (arithmetic on a counter deferred) + * Provenance proves INTEGER-NESS, not in-bounds-ness — the existing runtime + * bounds check still applies, so a reverse loop reaching a NEGATIVE index or a + * range exceeding the array ABSTAINS mid-loop (TS xs[3]=undefined / xs[-1]=undefined + * vs Python IndexError / wraparound — verified on real node + python3), and the + * abstain is ATOMIC (no partial stdout). + * + * Reference-only change: the emitters already lower `for i=0 to xs.length` and + * `xs[i]` correctly (TS `for (…; i < xs.length; …)` + `xs[i]`; Python + * `range(len(xs))` + `xs[i]`), so an abstaining program is never certified and + * never reaches the differential — no codegen change. + * + * RED-at-base: `for to=xs.length` abstains (for's evalValue has no member case) + * and `xs[i]` abstains (the index case rejects idents); both turn GREEN only when + * the runner gains the `.length` bound + counter provenance. + */ + +import { makeEnv, ReferenceRunnerError, referenceRunSequence, registerAllContracts } from '../src/index.js'; +import type { IRNode } from '../src/types.js'; + +beforeAll(() => { + registerAllContracts(); +}); + +/** Run a sequence of body statements and return replayed stdout, as `kern run` + * renders it (each `{op:'stdout'}` event + "\n"). */ +function runStdout(nodes: IRNode[]): string { + const trace = referenceRunSequence(nodes, makeEnv()); + return trace.events + .filter((e): e is { op: 'stdout'; text: string } => e.op === 'stdout') + .map((e) => `${e.text}\n`) + .join(''); +} + +function letBind(name: string, value: string): IRNode { + return { type: 'let', props: { name, value } }; +} +function print(expr: string): IRNode { + return { type: 'print', props: { value: expr } }; +} +function assign(target: string, value: string): IRNode { + return { type: 'assign', props: { target, value } }; +} +/** `for name= from= to= [step=]` with the given body. */ +function forL(props: { name: string; from: string; to: string; step?: string }, ...children: IRNode[]): IRNode { + return { type: 'for', props, children }; +} + +// ── CERTIFY: for-counter index + `.length` bound are 3-leg portable ─────────── +describe('runner dynamic index — for-counter reads certify (3-leg portable)', () => { + it('HEADLINE: iterates an array by index over its `.length`', () => { + expect( + runStdout([letBind('xs', '[10,20,30]'), forL({ name: 'i', from: '0', to: 'xs.length' }, print('xs[i]'))]), + ).toBe('10\n20\n30\n'); + }); + + it('reads by counter over an integer-LITERAL bound', () => { + expect(runStdout([letBind('xs', '[10,20,30]'), forL({ name: 'i', from: '0', to: '3' }, print('xs[i]'))])).toBe( + '10\n20\n30\n', + ); + }); + + it('a REVERSE loop (step -1) reads elements back-to-front', () => { + expect( + runStdout([letBind('xs', '[10,20,30]'), forL({ name: 'i', from: '2', to: '-1', step: '-1' }, print('xs[i]'))]), + ).toBe('30\n20\n10\n'); + }); + + it('a STEPPED loop reads every other element', () => { + expect( + runStdout([ + letBind('xs', '[10,20,30,40,50]'), + forL({ name: 'i', from: '0', to: 'xs.length', step: '2' }, print('xs[i]')), + ]), + ).toBe('10\n30\n50\n'); + }); + + it('an EMPTY range yields no iterations (no output)', () => { + expect(runStdout([letBind('xs', '[10,20,30]'), forL({ name: 'i', from: '0', to: '0' }, print('xs[i]'))])).toBe(''); + }); + + it('`.length` as a for-bound ALONE drives the iteration count (no index)', () => { + // Isolates capability (A): the loop runs `xs.length` times printing the counter. + expect(runStdout([letBind('xs', '[10,20,30]'), forL({ name: 'i', from: '0', to: 'xs.length' }, print('i'))])).toBe( + '0\n1\n2\n', + ); + }); +}); + +// ── FAIL-CLOSE: every non-(provenanced-counter) index ABSTAINS ──────────────── +describe('runner dynamic index — fail-close fences (abstain, never a value)', () => { + const abstains = (nodes: IRNode[]) => + expect(() => referenceRunSequence(nodes, makeEnv())).toThrow(ReferenceRunnerError); + + it('a plain LET-bound number index abstains even when in-bounds (the slice-2b fence holds)', () => { + abstains([letBind('xs', '[10,20,30]'), letBind('j', '2'), print('xs[j]')]); + }); + + it('THE FLOAT HOLE: `let j = 4 / 2; xs[j]` abstains (j is 2.0 in Python)', () => { + // The killer case the provenance gate must keep closed — accepting ANY ident + // index would certify this, then diverge (TS xs[2]=30 vs Python xs[2.0] TypeError). + abstains([letBind('xs', '[10,20,30]'), letBind('j', '4 / 2'), print('xs[j]')]); + }); + + it('provenance is NOT transitive: `for i..: let j = i; xs[j]` abstains', () => { + // `j` copies the counter VALUE but not its provenance, so it fails closed. + abstains([letBind('xs', '[10,20,30]'), forL({ name: 'i', from: '0', to: '3' }, letBind('j', 'i'), print('xs[j]'))]); + }); + + it('ASSIGN to the counter clears provenance: `for i..: assign i = 4/2; xs[i]` abstains', () => { + abstains([ + letBind('xs', '[10,20,30]'), + forL({ name: 'i', from: '0', to: '3' }, assign('i', '4 / 2'), print('xs[i]')), + ]); + }); + + it('ARITHMETIC on the counter abstains: `xs[i + 1]` is out of slice', () => { + abstains([letBind('xs', '[10,20,30]'), forL({ name: 'i', from: '0', to: '2' }, print('xs[i + 1]'))]); + }); + + it('OUT-OF-BOUNDS mid-loop abstains ATOMICALLY (no partial stdout)', () => { + // for i in 0..5 over a length-3 array: at i=3 TS reads undefined, Python raises + // IndexError → the whole program abstains, emitting nothing. + abstains([letBind('xs', '[10,20,30]'), forL({ name: 'i', from: '0', to: '5' }, print('xs[i]'))]); + }); + + it('a NEGATIVE counter (reverse past 0) abstains (TS undefined vs Py wraparound)', () => { + // for i in 2..-2 step -1 reaches i = -1 → divergent index → abstain. + abstains([letBind('xs', '[10,20,30]'), forL({ name: 'i', from: '2', to: '-2', step: '-1' }, print('xs[i]'))]); + }); + + it('an EACH binding is not integer-provenanced: `each x in ys: xs[x]` abstains', () => { + // `each` binds an element value (any type), NOT an int counter — so its binding + // is never provenanced and indexing with it fails closed. + abstains([ + letBind('xs', '[10,20,30]'), + letBind('ys', '[0,1]'), + { type: 'each', props: { name: 'x', in: 'ys' }, children: [print('xs[x]')] }, + ]); + }); +}); diff --git a/packages/python/tests/kern-run-cli-differential.test.ts b/packages/python/tests/kern-run-cli-differential.test.ts index 5121cf31..ef0b698d 100644 --- a/packages/python/tests/kern-run-cli-differential.test.ts +++ b/packages/python/tests/kern-run-cli-differential.test.ts @@ -220,6 +220,31 @@ const CERT: Array<[string, string[], string]> = [ '2\n', ], ['array length flows into arithmetic', ['let name=xs value="[1,2,3]"', 'print value="xs.length - 1"'], '2\n'], + // ── DYNAMIC index via for-counter provenance + `.length` for-bound ─────────── + // A `for` counter is a guaranteed safe integer, so `xs[i]` reads byte-identical + // 3-leg (TS `for(…; i { From e141f2704b77cb5d9b95d992980b8cfee98c0248 Mon Sep 17 00:00:00 2001 From: "agon (KERN)" <292465531+KERN-Agon@users.noreply.github.com> Date: Thu, 25 Jun 2026 16:30:00 +0200 Subject: [PATCH 5/6] feat(runner): dynamic array index via for-counter provenance + `.length` for-bound MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The ReferenceRunner — the executor `kern run` uses — now iterates an array by index on its own runtime, the long-promised headline: let xs = [10,20,30] for i from=0 to=xs.length: print xs[i] -> 10 / 20 / 30 Two coupled capabilities, both REFERENCE-ONLY (the emitters already lower `for i.length` (non-optional, ident object, property `length`, array binding -> element count). `evalIntExpression` already requires Number.isSafeInteger, so the range stays integer-gated. (B) a for-counter as an array INDEX — `xs[i]` certifies when `i` is INTEGER- PROVENANCED. A `for` counter is a guaranteed safe integer (the for-contract enforces Number.isSafeInteger on from/to/step and steps by an integer), so it is an int on all three legs by construction; the provenance comes from the LOOP CONSTRUCT, not a value check — sidestepping the int/float divergence that keeps a plain `let j = 4/2` index abstaining (j is 2.0 in Python). Provenance is per-scope binding metadata on SemanticEnv (`intProvenance: Set`): - `defineIntBinding` (used ONLY by the for-contract for its counter) sets the binding AND marks it; `each` keeps plain `defineBinding`. - `defineBinding` (plain let / redeclare) and `assignBinding` (assign) CLEAR the mark — so `let j = i` is not transitive and `assign i = 4/2` drops provenance. - `isIntProvenanced` resolves the DECLARING scope first, then checks that scope's marker (never a free-floating name match). The index case admits a bare safe-int LITERAL (slice-2b) OR a bare integer-provenanced ident, then applies the SAME runtime bounds check. Provenance proves INTEGER-NESS, not in-bounds-ness: a reverse loop reaching a NEGATIVE index or a range past the array length ABSTAINS mid-loop (TS undefined vs Py IndexError/wraparound), atomically (no partial stdout). Arithmetic on a counter (`xs[i+1]`) stays fenced — provenance proves int-ness, not safe-integer closure. Gate: dynamic-index spec 14/14 + array-index/values/length + for/let/assign/while/ if/try/expr-v1/each + runner-entry-import-graph (core 264/264) + CLI 59/59 + 3-leg differential 27/27 (0 skipped) + biome + docs:contracts:check. Planned with agon brainstorm (6 engines); built by codex via agon conquer against the RED-at-base neighborhood oracle (rescued — codex over-ran into the full `pnpm test` suite and was killed, but the gate-correct impl was complete in the tree); reviewed by the full agon roster. ⚔️ Forged by [Agon](https://github.com/KERNlang/agon) Co-Authored-By: agon (KERN) <292465531+KERN-Agon@users.noreply.github.com> --- packages/core/src/ir/semantics/for.ts | 13 ++++- packages/core/src/ir/semantics/index.ts | 18 ++++++- .../core/src/ir/semantics/portable-scalar.ts | 48 +++++++++++-------- 3 files changed, 57 insertions(+), 22 deletions(-) diff --git a/packages/core/src/ir/semantics/for.ts b/packages/core/src/ir/semantics/for.ts index 77ed973e..0362f4e9 100644 --- a/packages/core/src/ir/semantics/for.ts +++ b/packages/core/src/ir/semantics/for.ts @@ -14,7 +14,7 @@ import type { IRNode } from '../../types.js'; import type { ValueIR } from '../../value-ir.js'; import { childEnv, - defineBinding, + defineIntBinding, getBinding, hasBinding, type NodeContract, @@ -61,6 +61,15 @@ function evalValue(expr: ValueIR, env: SemanticEnv): unknown { if (!hasBinding(env, expr.name)) throw new Error(`for: binding "${expr.name}" not found in env`); return getBinding(env, expr.name); } + case 'member': { + if (expr.optional || expr.object.kind !== 'ident' || expr.property !== 'length') { + throw new Error('for: unsupported member expression in range bound'); + } + if (!hasBinding(env, expr.object.name)) throw new Error(`for: binding "${expr.object.name}" not found in env`); + const array = getBinding(env, expr.object.name); + if (!Array.isArray(array)) throw new Error('for: range bound .length requires an array binding'); + return array.length; + } case 'index': { const target = evalValue(expr.object, env); const index = evalValue(expr.index, env); @@ -105,7 +114,7 @@ function forEffects(ir: IRNode, env: SemanticEnv): Trace { // emitted TS/Python loops. (Previously this forked `new Map(env.bindings)`, // discarding outer mutations: a `sum += i` accumulator returned 0, not 15.) const iterEnv = childEnv(env); - defineBinding(iterEnv, name, i); + defineIntBinding(iterEnv, name, i); const childTrace = referenceRunSequence(children, iterEnv); out.events.push(...childTrace.events); diff --git a/packages/core/src/ir/semantics/index.ts b/packages/core/src/ir/semantics/index.ts index b65bd061..7e49737c 100644 --- a/packages/core/src/ir/semantics/index.ts +++ b/packages/core/src/ir/semantics/index.ts @@ -28,6 +28,7 @@ import type { CompletionRecord, Trace } from './trace.js'; */ export interface SemanticEnv { bindings: Map; + intProvenance?: Set; /** * Enclosing lexical scope, if any. A `let` binds in THIS scope's `bindings`; * reads and `assign` walk up `parent` to the declaring scope (write-through). @@ -55,6 +56,7 @@ export interface SemanticEnv { export function makeEnv(overrides: Partial = {}): SemanticEnv { return { bindings: overrides.bindings ? cloneBindings(overrides.bindings) : new Map(), + intProvenance: overrides.intProvenance ? new Set(overrides.intProvenance) : new Set(), seed: overrides.seed ?? 0, now: overrides.now ?? 0, }; @@ -79,7 +81,7 @@ function cloneBindings(bindings: Map): Map { * mutations to outer bindings write through to where they were declared. */ export function childEnv(parent: SemanticEnv): SemanticEnv { - return { bindings: new Map(), parent, seed: parent.seed, now: parent.now }; + return { bindings: new Map(), intProvenance: new Set(), parent, seed: parent.seed, now: parent.now }; } /** The nearest scope in the chain that declares `name`, or undefined if unbound. */ @@ -108,6 +110,13 @@ export function getBinding(env: SemanticEnv, name: string): unknown { /** Declare `name` in the INNERMOST scope (`let`). Overwrites a same-scope binding. */ export function defineBinding(env: SemanticEnv, name: string, value: unknown): void { env.bindings.set(name, value); + env.intProvenance?.delete(name); +} + +/** Declare `name` in the INNERMOST scope and mark it as a guaranteed safe integer. */ +export function defineIntBinding(env: SemanticEnv, name: string, value: unknown): void { + env.bindings.set(name, value); + (env.intProvenance ??= new Set()).add(name); } /** @@ -119,6 +128,13 @@ export function defineBinding(env: SemanticEnv, name: string, value: unknown): v export function assignBinding(env: SemanticEnv, name: string, value: unknown): void { const scope = declaringScope(env, name) ?? env; scope.bindings.set(name, value); + scope.intProvenance?.delete(name); +} + +/** True iff `name` is declared in a scope that marks it as a guaranteed safe integer. */ +export function isIntProvenanced(env: SemanticEnv, name: string): boolean { + const scope = declaringScope(env, name); + return scope?.intProvenance?.has(name) ?? false; } /** Delete `name` from the INNERMOST scope only (scope teardown). */ diff --git a/packages/core/src/ir/semantics/portable-scalar.ts b/packages/core/src/ir/semantics/portable-scalar.ts index 7902c46a..dfe428bb 100644 --- a/packages/core/src/ir/semantics/portable-scalar.ts +++ b/packages/core/src/ir/semantics/portable-scalar.ts @@ -41,7 +41,7 @@ import { } from '../../decimal/probe-gates.js'; import type { ValueIR } from '../../value-ir.js'; import type { SemanticEnv } from './index.js'; -import { getBinding, hasBinding } from './index.js'; +import { getBinding, hasBinding, isIntProvenanced } from './index.js'; export type PortableScalar = string | number | boolean | null; @@ -290,34 +290,44 @@ export function evalPortableValue(node: ValueIR, env: SemanticEnv): PortableScal return obj.message; } case 'index': { - // Array INDEX read (slice-2b). Certify ONLY an in-bounds, non-negative, - // safe-integer index whose SOURCE is a BARE integer LITERAL, into an - // ident-bound array, returning a PORTABLE SCALAR element. Everything else - // throws -> the runner ABSTAINS. + // Array INDEX read. Certify an in-bounds, non-negative, safe-integer index + // into an ident-bound array, returning a PORTABLE SCALAR element. The index + // SOURCE must be either (slice-2b) a BARE integer LITERAL, or (dynamic-index + // slice) a BARE ident that is INTEGER-PROVENANCED — currently the live + // counter of an enclosing `for`, which the for-contract guarantees is a safe + // integer. Everything else throws -> the runner ABSTAINS. // - // The index is restricted to a literal ({@link isSafeIntegerLiteralIndex}) - // because of TS<->Python divergences verified on real node+python3: + // Why not any ident, and why arithmetic still abstains — TS<->Python + // divergences verified on real node+python3: // - INT vs FLOAT: Python list indices MUST be int — `xs[1.0]`, `xs[4/2]` - // (Python `/` is float), and any ident bound to a float raise TypeError - // in Python while JS + the reference collapse `1.0 === 1` and read xs[1]. + // (Python `/` is float), and any PLAIN-let ident bound to a float raise + // TypeError in Python while JS + the reference collapse `1.0 === 1`. A + // for-counter is exempt because its provenance proves it is an int; a + // plain `let` is NOT provenanced (and `let j = i` is not transitive). // - integer `%` diverges on a negative operand (`5 % -3` is 2 in JS, -1 in - // Python), and `+`/`-`/`*` over safe literals can overflow 2^53 and round - // in JS while Python stays exact — so ARITHMETIC indices abstain. + // Python), and `+`/`-`/`*` over safe values can overflow 2^53 and round + // in JS while Python stays exact — so ARITHMETIC indices (`xs[i+1]`) + // abstain even on a counter (provenance proves int-ness, not closure). // - JS has no int/float distinction and the emitters preserve the source // numeric form, so the reference cannot tell a Python int from a float by - // VALUE — hence the syntactic literal gate, not a value check. - // Idents / nested index-reads abstain (a binding can hold a Python float); - // dynamic indexing is a later slice. Then OOB / NEGATIVE are caught at runtime - // (TS undefined vs Py IndexError / wraparound). Object restricted to an - // array-binding ident, so OBJECT-position nesting (`xs[0][1]`) and string - // index (`s[0]`) abstain; a nested-array element is not a portable scalar, so + // VALUE — hence the syntactic literal / provenance gate, not a value check. + // Provenance proves INTEGER-NESS, not IN-BOUNDS-ness: OOB / NEGATIVE indices + // are caught at runtime below (TS undefined vs Py IndexError / wraparound), + // and the throw propagates atomically. Object restricted to an array-binding + // ident, so OBJECT-position nesting (`xs[0][1]`) and string index (`s[0]`) + // abstain; a nested-array element is not a portable scalar, so // `assertPortableScalar` abstains on it. if (node.optional) throw new Error('portable: optional index access is outside the portable scalar domain'); if (node.object.kind !== 'ident') { throw new Error('portable: index access is only admitted on an array-binding identifier'); } - if (!isSafeIntegerLiteralIndex(node.index)) { - throw new Error('portable: array index must be a bare non-negative safe-integer literal'); + if ( + !isSafeIntegerLiteralIndex(node.index) && + !(node.index.kind === 'ident' && isIntProvenanced(env, node.index.name)) + ) { + throw new Error( + 'portable: array index must be a bare non-negative safe-integer literal or an integer-provenanced loop counter', + ); } if (!hasBinding(env, node.object.name)) { throw new Error(`portable: binding "${node.object.name}" not found`); From 9390591f77845117a4127e8e6908be6cf53fd477 Mon Sep 17 00:00:00 2001 From: "agon (KERN)" <292465531+KERN-Agon@users.noreply.github.com> Date: Thu, 25 Jun 2026 16:41:54 +0200 Subject: [PATCH 6/6] =?UTF-8?q?fix(runner):=20dynamic-index=20review=20fix?= =?UTF-8?q?=20=E2=80=94=20gate=20for-range-bound=20array=20indices?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Full-roster agon review (agy + codex clean; kimi 1 blocking). Triaged: - [BLOCKING 0.90, verified 3-leg] for's LOCAL range evaluator (`evalValue`) admitted an array index by ANY ident — so `for i from=0 to=xs[j]` with a plain `let j=4/2` CERTIFIED in the reference (prints 0..N) but DIVERGES: TS reads xs[2], Python `range(0, xs[2.0])` raises TypeError (confirmed on real node+python3). This was a pre-existing hole in for's evaluator, surfaced now because the slice touches it. FIX: gate the range-bound index with the SAME rule as the body index reader — a bare safe-integer LITERAL (now exported `isSafeIntegerLiteralIndex`) or a bare integer-provenanced ident. Plain-let / arithmetic / float indices abstain; `bounds[0]` literal indices still pass. - [kimi/minimax cluster] documented the per-scope `intProvenance` design on `childEnv` (empty per scope; `declaringScope` finds an outer counter from a nested scope). Kept the field optional + fail-safe `?.` guards — making it required would break full-env literals like `freshDecimalEvalEnv`. - REFUTED: `expr.computed` concern — the `member` IR has no `computed` field (bracket access is the `index` node); double-eval — the index is evaluated once; `xs[i+1]` rejection — by design (deferred, council-confirmed). Added oracle coverage: the blocking `for to=xs[j]` regression fence, an integer-`assign i=1` clears-provenance fence (any reassignment drops the mark), and a NESTED-loop CERT (outer counter resolved across scopes via declaringScope). Gate: dynamic-index spec 17/17 + array neighborhood + for/let/assign 116/116 + CLI 59/59 + 3-leg differential 27/27 (0 skipped) + biome. ⚔️ Forged by [Agon](https://github.com/KERNlang/agon) Co-Authored-By: agon (KERN) <292465531+KERN-Agon@users.noreply.github.com> --- packages/core/src/ir/semantics/for.ts | 16 ++++++++++ packages/core/src/ir/semantics/index.ts | 4 +++ .../core/src/ir/semantics/portable-scalar.ts | 2 +- .../core/tests/runner-dynamic-index.test.ts | 29 +++++++++++++++++++ 4 files changed, 50 insertions(+), 1 deletion(-) diff --git a/packages/core/src/ir/semantics/for.ts b/packages/core/src/ir/semantics/for.ts index 0362f4e9..592c172f 100644 --- a/packages/core/src/ir/semantics/for.ts +++ b/packages/core/src/ir/semantics/for.ts @@ -17,11 +17,13 @@ import { defineIntBinding, getBinding, hasBinding, + isIntProvenanced, type NodeContract, type NodeFixture, registerContract, type SemanticEnv, } from './index.js'; +import { isSafeIntegerLiteralIndex } from './portable-scalar.js'; import { referenceRunSequence } from './reference-runner.js'; import { emptyTrace, type Trace } from './trace.js'; @@ -71,6 +73,20 @@ function evalValue(expr: ValueIR, env: SemanticEnv): unknown { return array.length; } case 'index': { + // A range-bound array index must be PORTABLE for 3-leg parity, the SAME gate + // as the body index reader (portable-scalar): a bare safe-integer LITERAL or + // a bare integer-provenanced ident (a for-counter). A plain `let` ident can + // be a Python float (`let j = 4/2` is 2.0), so `for to=xs[j]` would read + // xs[2] in JS/ref but raise TypeError in Python (`range(0, xs[2.0])`) — it + // must abstain. (`bounds[0]` literal indices still pass.) + if ( + !isSafeIntegerLiteralIndex(expr.index) && + !(expr.index.kind === 'ident' && isIntProvenanced(env, expr.index.name)) + ) { + throw new Error( + 'for: range-bound array index must be a safe-integer literal or an integer-provenanced loop counter', + ); + } const target = evalValue(expr.object, env); const index = evalValue(expr.index, env); if (Array.isArray(target) && typeof index === 'number') return target[index]; diff --git a/packages/core/src/ir/semantics/index.ts b/packages/core/src/ir/semantics/index.ts index 7e49737c..bed2a09f 100644 --- a/packages/core/src/ir/semantics/index.ts +++ b/packages/core/src/ir/semantics/index.ts @@ -81,6 +81,10 @@ function cloneBindings(bindings: Map): Map { * mutations to outer bindings write through to where they were declared. */ export function childEnv(parent: SemanticEnv): SemanticEnv { + // `intProvenance` is PER-SCOPE binding metadata (which names declared in THIS + // scope are guaranteed safe integers). A child starts EMPTY — it does not clone + // the parent's set; `isIntProvenanced` walks `declaringScope` first, so a + // counter declared in an outer scope is still found from a nested scope. return { bindings: new Map(), intProvenance: new Set(), parent, seed: parent.seed, now: parent.now }; } diff --git a/packages/core/src/ir/semantics/portable-scalar.ts b/packages/core/src/ir/semantics/portable-scalar.ts index dfe428bb..0e5a6472 100644 --- a/packages/core/src/ir/semantics/portable-scalar.ts +++ b/packages/core/src/ir/semantics/portable-scalar.ts @@ -217,7 +217,7 @@ export function sameType(a: PortableScalar, b: PortableScalar): boolean { * index-reads are excluded too (they can resolve to a Python float). So a computed * or variable index ABSTAINS; dynamic indexing is deferred to a slice that proves * exact integer arithmetic (e.g. BigInt-checked) or carries integer provenance. */ -function isSafeIntegerLiteralIndex(node: ValueIR): boolean { +export function isSafeIntegerLiteralIndex(node: ValueIR): boolean { if (node.kind !== 'numLit' || node.bigint) return false; if (!/^[0-9]+$/.test(node.raw)) return false; const n = Number(node.raw); diff --git a/packages/core/tests/runner-dynamic-index.test.ts b/packages/core/tests/runner-dynamic-index.test.ts index eaf17a5e..0326b628 100644 --- a/packages/core/tests/runner-dynamic-index.test.ts +++ b/packages/core/tests/runner-dynamic-index.test.ts @@ -112,6 +112,17 @@ describe('runner dynamic index — for-counter reads certify (3-leg portable)', '0\n1\n2\n', ); }); + + it('a NESTED loop resolves the OUTER counter across scopes (declaringScope provenance)', () => { + // `xs[i]` is read in the INNER loop's scope while `i` is the OUTER counter — + // isIntProvenanced must walk to the declaring scope to find i's mark. + expect( + runStdout([ + letBind('xs', '[10,20,30]'), + forL({ name: 'i', from: '0', to: 'xs.length' }, forL({ name: 'k', from: '0', to: '1' }, print('xs[i]'))), + ]), + ).toBe('10\n20\n30\n'); + }); }); // ── FAIL-CLOSE: every non-(provenanced-counter) index ABSTAINS ──────────────── @@ -141,6 +152,24 @@ describe('runner dynamic index — fail-close fences (abstain, never a value)', ]); }); + it('ANY assign to the counter clears provenance, even an integer (`assign i = 1`)', () => { + // Provenance is minted by the loop, not re-derived from the assigned value — + // so even an integer reassignment drops it (the binding is no longer the + // construct-guaranteed counter). Fail-safe over-rejection. + abstains([letBind('xs', '[10,20,30]'), forL({ name: 'i', from: '0', to: '3' }, assign('i', '1'), print('xs[i]'))]); + }); + + it('a for-RANGE bound indexed by a plain let `for to=xs[j]` abstains (j could be a Python float)', () => { + // The blocking review finding: for's range evaluator must apply the SAME index + // gate as the body — `let j = 4/2` is 2.0 in Python, so `range(0, xs[2.0])` + // raises TypeError while JS/ref read xs[2]. Verified divergent on node+python3. + abstains([ + letBind('xs', '[3,4,5]'), + letBind('j', '4 / 2'), + forL({ name: 'i', from: '0', to: 'xs[j]' }, print('i')), + ]); + }); + it('ARITHMETIC on the counter abstains: `xs[i + 1]` is out of slice', () => { abstains([letBind('xs', '[10,20,30]'), forL({ name: 'i', from: '0', to: '2' }, print('xs[i + 1]'))]); });