Feat/runner dynamic index#477
Merged
Merged
Conversation
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>
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>
…fence coverage
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>
…(RED-at-base) 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<xs.length`+`xs[i]` (TS) / `range(len(xs))`+`xs[i]` (Python). ⚔️ Forged by [Agon](https://github.com/KERNlang/agon) Co-Authored-By: agon (KERN) <292465531+KERN-Agon@users.noreply.github.com>
…th` for-bound
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<xs.length`+`xs[i]` on TS and `range(len(xs))`+`xs[i]` on Python):
(A) `.length` as a `for` RANGE BOUND — for.ts's local range evaluator gains a
`member` case admitting ONLY `<arrayIdent>.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>
…dices 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>
cukas
force-pushed
the
feat/runner-dynamic-index
branch
from
135b337 to
9390591
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Why
How
Checklist
tsc -bpassespnpm testpassespnpm test:kernpassespnpm lintpasseskern review packages/ --recursivechecked