[siracozmen01]

Problem

A program writing one of a run of runs at an index worked out while running was refused as a fault in the compiler, in a local and inside an element of an array (#249), and so was a program writing one of a run in a local at such an index with an operator or into a field of one (#251). With

let grid: [[i32; 3]; 2] = [[1, 2, 3], [4, 5, 6]]
let xs: [i32; 3] = [1, 2, 3]
let ps: [P; 2] = [P(1, 2), P(3, 4)]
let i = 1
let j = i + 1
grid[i][j] = 9
xs[i] += 5
ps[i].y = 9
io.print("{grid[1][2]} {xs[1]} {ps[1].y}")

(struct P { x: i32; y: i32 }), each of the three writes was refused under every build and switch with

error[K0505]: this assigns to something that is not a place, which the checker allowed

and the program now prints 9 7 9. grid[i][2] = 9, -=, *= and /=, and boards[k].grid[i][j] = 9 inside an element were refused the same way. A run in a local could be written at a running index only with = and only whole: store.slots wrote as many slots as one of the run is wide, the compiler had no way to keep the index for a read and then a write, and a run of runs at a running first index was no place at all. Inside an element, the change for #245 held one run's index apart, not two.

Change

• src/compile.c: run_way finds the place a write reaches through runs at indexes worked out while running: what holds the outermost run, a local's slots or an element's bytes, and how far into one of the innermost run the place is, through fields and indexes written down after the last running index. A run of runs is reached as one run of what the innermost holds, at one index worked out from all of them, outermost first, in the order they were written. Where more than one index is worked out while running, each is held to its own count first, so a refusal names the index that was outside and its own count. In a local, =, +=, -=, *= and /= all go through it, and a read before a write keeps the index in a slot of its own, since each takes it. A place of any other shape compiles exactly as before.
• src/value.h, src/value.c, src/vm.c, src/verify.c, src/lower.c, src/emitc.c: load.slots and store.slots take how many slots of one of the run they read or write, which is fewer than the stride for a field of one; the verifier holds them to the slots they can reach with it. One instruction, in.run, holds the index at the top to a count and leaves it, refusing with the K0604 sentence a run gets ("index 3 is outside 3 of them"), in the machine and in a body compiled to C. It reaches neither the heap nor the host.
• src/ir.h, src/ir.c: the operation in.run beside them, and a RUN place says how many slots of one it reaches.
• src/verify.c: all_a_run answers whether all of a fixed run is a run of count things step bytes wide, read through runs of runs as one run of what the innermost holds, which is how store.elem.run reaches one inside an element; run_holds asks it first. Each of the outer run's has to be all of a run of the inner. A run found inside one of them, which run_holds finds since fix(verifier)!: find a run inside one of a run at a running index #254, is not enough: eight i32 from the xs of an Inner would step on into the next one's tag.
• test/regress/runofruns.kest: in a local, = and every operator into a run of runs at two running indexes and at a running first index, += and -= into a run, a field of one written and added to, a whole struct written, a run of runs of bool, of structs and three deep inside a struct, with an index written down in the middle, and a run of vec2 added to. Inside an element, the same shapes, writes in a loop, and a write whose right-hand side pushes 64 elements onto the array being written.
• examples/rows.kest: check 16 writes a run of runs of cells at two indexes worked out while running, which is what has the gate's declarations step see in.run run. What it prints is the same.
• tools/check-commands.sh: K0604 for the first index past its run and the second past its own, in a local; the second past its own with += inside an element; += into a run past its end; and a field written past the end of a run.
• tools/check-verifier.sh: the program it changes carries manys[k].grid[i][j] = 9, and one more case moves that store.elem.run to 36 bytes into a Many, the xs of the first Inner of nest: [[Inner; 3]; 2], where the verifier has to refuse it with K0411. first_with can be asked for the first instruction in one function, since the first store.elem.run in the module is inside's.
• tools/check-c.sh: the second index past its own run, in a local and inside an element, in a body compiled to C, has to be refused with the machine's own K0604 line, byte for byte.
• docs/internals/compiler.md: 226 instructions, and how a run of runs is reached.

A program refused before now runs, so this takes !. A program that compiled before compiles to the same instructions, with load.slots and store.slots each two bytes wider for the new operand. No version moves: neither the ABI, the JSON a command writes, nor what a deterministic program that ran before observes changes.

A run inside one of a run written at two running indexes, with a field between them (ss[i].xs[j] = 9), is still refused; that is #252. A run inside one of a run at an index written down, inside an element (bs[k].grid[1][j]), was #253, fixed by #254, which this is built on.

Verification

• The example above, test/regress/runofruns.kest, and the new K0604 programs are refused with K0505 by a kest built from main (d692b17). On this branch the example prints 9 7 9, and the program answers 0 under kest and kest-debug, each with nothing, KEST_PLAIN=1, KEST_NOOPT=1 and KEST_WALK_EVERY=1, and compiled to C. kest emit writes it with 54 in.run.
• In the example, kest emit writes grid[i][j] = 9 as in.run 2, mul.i by 3, in.run 3, add.i and store.slots +0 1 of 6; xs[i] += 5 as store.k, load2, load.slots +6 1 of 3, add.i.narrow.c and store.slots +6 1 of 3; and ps[i].y = 9 as store.slots +10 2 of 2 1 of each.
• The new tests against two changed copies. With in.run in src/vm.c doing nothing, the three run-of-runs K0604 rows fail: the first index past its run is said as "index 6 is outside 6 of them", and the second index past its own writes into the next row and answers. With the kest_run_at line taken out of in.run in src/emitc.c, the C check fails both ways: the body compiled to C says nothing and answers. The rows for xs[i] += and ps[i].y = past the end are load.slots and store.slots refusing, and pass under both.
• tools/check-verifier.sh says "28 way(s) a chunk can name what it has not got, move the stack wrong or read a slot as what it does not hold, each refused, and the program as it was compiled held". Against a copy of this branch's library whose run_holds asks the whole of itself about the inner run, as this change first did, it fails with "a run of runs written where a run of them holds a shorter run was held".
• Light compile checks of every touched file with clang-20, clang-format in the CI image, and kest fmt of both Kest files.
• Through heavy.sh, on a dev build of this branch (on b95fbf3): examples/embed, examples/embed-debug and examples/embed-debug with KEST_WALK_EVERY=1 pass, ctest --preset dev -j4 passes all 21 tests and tools/check-costs.sh passes. tools/check-c.sh over every Kest file of examples, lib and bench passes, saying "a run of runs written past its second run, in a local and in an element, refused in C with the machine's line".
• The full gate runs in CI.

Closes #249
Closes #251

BREAKING CHANGE: a program writing one of a run of runs at an index worked out while running, in a local or inside an element of an array, or writing one of a run in a local at such an index with an operator or into a field of one, was refused with K0505 and now compiles and runs.

[siracozmen01]

Review at ae63f28: ready. No findings. Read, not run. I read verify.c, vm.c, emitc.c, value.c/h, ir and lower in full in the diff. compile.c's 235 lines I read for the places it builds, not every line.

all_a_run, against every caller:

• It is reached only through run_holds (verify.c:1381), whose callers are element_run (1415) and the in-place read at 1920. run_holds itself recurses through struct members (1388) and, since #254, through one element of a fixed run (1398). So every path that accepts a run now ends in all_a_run.
• all_a_run accepts only a fixed run that is all of the run: exactly count elements of step bytes with the field at offset < step. Or it accepts a fixed run of c0 elements whose element is itself all of a run of count / c0.
  • Because it recurses only into a FIXED element, never into a struct, and requires count % c0 == 0 at each level, the flattened run covers the whole outer run with no gap.
  • A fixed run's elements are laid out back to back at element->byte_size, which the base case pins to count' × step.
• The combined case is refused on every route.
  • Many.nest ([Inner; 2], Inner {tag, xs: [i32; 4]}) read as 8 i32: 8 % 2 = 0 recurses into Inner, a struct, so false.
  • The #254 branch goes into one Inner and then xs: all_a_run([i32; 4], 4, 8) recurses into i32, not FIXED, so false.
  • So nothing steps from an xs into the next tag. The offset-36 case pins it.
• constant_run_holds is the constants' own check and is not touched.

VM and C backend, same addresses:

• load.slots and store.slots now carry width beside stride. The VM copies width slots at base + index × stride (vm.c:5193-5233). The C backend writes f[slot + k + which × stride] for k < slots (emitc.c:1644-1699). Those are the same slots.
• The bounds agree everywhere: base + (count - 1) × stride + width in the VM's own_slots, the verifier's reach (verify.c:724) and emitc's mark_frame (467-471). Each is guarded by count > 0 or comes after IN_RUN, so count - 1 cannot underflow.
• in.run holds one index to its own count on both sides: the VM's IN_RUN(top[-1].integer, count), and C's kest_run_at(rt, x.integer, count). It leaves the value in place, and the verifier only asks for a number on top. So each index of a run of runs is checked against its own bound before the combined index is checked against the whole.
• The verifier's slot kinds for both ops iterate k < width across rows at stride, matching the copies.