[siracozmen01]

Problem

A program writing one of a fixed run inside an element of an array, at an index worked out while running, was refused as a fault in the compiler, whichever field the run was (#245). With struct Row { count: [i32; 3] }, rows holding Row([10, 20, 30]) and at worked out while running as 1,

rows[0].count[at] = 99
rows[0].count[at - 1] += 5
io.print("{rows[0].count[0]} {rows[0].count[1]} {rows[0].count[2]}")

was refused under every build and switch with

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

once for each write, and now prints 15 99 30. Only a run held in a local could be written at such an index. A write into an element is held apart as the array and its index until the moment it is written, so that what the right-hand side does to the array (growing it most of all) cannot leave the write an address into a block that moved; store.elem and load.elem carry the run's place as a byte offset fixed in the instruction, so there was no way to hold the run's index apart too.

Change

• src/value.h, src/value.c: two instructions, load.elem.run and store.elem.run, each load.elem and store.elem with the run's index as the third thing under the value and the run's stride and count beside the offset and layout. Neither reaches the heap.
• src/vm.c: both ask what the handle is and whether the element's index is in the array, as load.elem and store.elem do, and whether the run's index is one of the run, with the same K0604 sentence a run in a local gets ("index 3 is outside 3 of them"). The address is worked out when the instruction runs.
• src/verify.c: element_run holds the offset, layout, stride and count to a run the element's layout has there (run_holds, which load.at already uses).
• src/compile.c: run_in_element finds such a run under the place written, with fields of one of the run after it (rows[k].cells[at].hp = 44), and the assignment holds the run's index apart above the element's. =, +=, -=, *= and /= all go through it. A place not of that shape compiles exactly as before.
• src/lower.c, src/ir.h: an element place with a count is lowered to the two instructions, and never fused.
• src/emitc.c: a body compiled to C asks kest_run_at about the run's index, which is the machine's own sentence, and steps into the run after the element is found.
• test/regress/runwrite.kest: =, += and -= into runs of i32 and bool after the first field and as the first field, a field of one of a run of structs and a whole struct written into one, a run inside a struct inside the element, writes in a loop, and a write whose right-hand side pushes 64 rows onto the array being written.
• examples/rows.kest: checks 14 and 15 write a cell's field through a handle with both indexes worked out while running, which is what has the gate's declarations step see both instructions run. What it prints is the same.
• tools/check-commands.sh: a run's index past the run is refused with K0604 written with =, with +=, and with /= by nought. The last tells the read's check apart from the write's: without it, the read goes past the run and the division is refused first, with K0601.
• tools/check-c.sh: the same = and /= by nought in a body compiled to C have to be refused with the machine's own K0604 line, byte for byte.
• docs/internals/compiler.md: 225 instructions, and what an element place holds.

A program refused before now runs, so this takes !. A program that compiled before compiles to the same instructions. No version moves: neither the ABI, the JSON a command writes, nor what a deterministic program that ran before observes changes.

A run of runs written at two indexes worked out while running (grid[i][j] = 9) is still refused, in a local as well as in an element; that is #249.

Verification

• The example above is refused with two K0505 and test/regress/runwrite.kest with eleven by a kest built from 66caeab, whose src/compile.c, src/lower.c and src/emitc.c are main's (ca6f9c2). On this branch the example prints 15 99 30, and the program answers 0 under kest and kest-debug, each with nothing, KEST_PLAIN=1, KEST_NOOPT=1 and KEST_WALK_EVERY=1. kest emit writes it with 19 load.elem.run and store.elem.run.
• *= and /= by hand: [10, 20, 30] with count[1] *= 3 and count[2] /= 4 prints 10 60 7 under kest-debug, with and without KEST_NOOPT=1.
• The write whose right-hand side grows the array is read back right under kest-debug's sanitizers: the place is worked out after the 64 pushes.
• The new tests against two changed copies. With IN_RUN taken out of load.elem.run in src/vm.c, the /= row says error[K0601]: division by zero and fails, and so does the C check, because the machine's line is no longer the same. With the kest_run_at block taken out of write_elem in src/emitc.c, the C check fails both ways: the = says nothing and answers, and the /= says K0601. The += row passes under both, because the write's check says the same sentence after the read; it is there for the compound path.
• Through heavy.sh, after the tests were added (8e588a1): tables, commands, backend and declarations pass, backend saying "a run inside an element written and divided into past its end, refused in C with the machine's line".
• Light compile checks of every touched file with clang-20 and gcc-14, and clang-format in the CI image. kest fmt of both Kest files.
• Through heavy.sh, on a dev build of this branch (on ca6f9c2): examples/embed, examples/embed-debug and examples/embed-debug with KEST_WALK_EVERY=1 pass, and ctest --preset dev -j4 passes all 21 tests: regressions runs the new program under both builds, the heap walked at every allocation, KEST_PLAIN, KEST_NOOPT and compiled to C; gate runs examples/rows.kest every way and holds it to the same output; declarations sees both instructions run; commands has the new K0604. A first run without the example failed declarations with "nothing emits load.elem.run, so no example has run it", which is why examples/rows.kest writes one.
• The full gate runs in CI.

Closes #245

BREAKING CHANGE: a program writing one of a fixed run inside an element of an array at an index worked out while running was refused with K0505 and now compiles and runs.

[siracozmen01]

Review of 88738d8: changes needed (1). Read, not run. Checks were still pending apart from docs, gate and title, which pass.

1. The run-index refusal is tested on one of its four paths.

The new check-commands.sh row writes rows[0].count[i] = 9 with i 3 and runs it with kest run, which is the machine's store.elem.run. Three paths have no test that fails if their check goes:

• the machine's load.elem.run (IN_RUN, vm.c), which a += reaches first;
• both instructions compiled to C (the kest_run_at block in write_elem).

runwrite.kest stays in range throughout. A mutant that drops IN_RUN from KEST_OP_LOAD_ELEM_RUN, or the place->count > 0 block from write_elem, passes everything here, and the load then reads past the run: past the element for a run at its end. One more row, such as rows[0].count[i] += 9, covers the machine's load. A refusal of the same program compiled to C, wherever the suite runs K0604 cases through the C backend, covers kest_run_at.

What checks out

• The same three indexes in the same order, with the same sentence:
  • The machine checks HOLD (the handle), then IN_ARRAY (the element), then IN_RUN (the run). IN_RUN says "index %lld is outside %u of them" under K0604.
  • write_elem does the handle and element test inline, falls back to kest_elem_at, which is the machine's own answer, and then calls kest_run_at, which says the same K0604 sentence (vm.c:9761-9772).
  • The run check is emitted on all three element paths (guarded, in bounds and plain), so a walk that proves the element in bounds still checks the run index.
• The address is taken after the right-hand side. The assignment pushes the handle, the element's index and the run's index, then computes the value, and only store.elem.run (vm.c) or the C block at the PUT forms bytes + index * stride + offset + within * stride. For +=, load.elem.run leaves the place in place, and the store forms the address again. runwrite.kest's last write, whose right-hand side pushes 64 rows, exercises this.
• Stack effects:
  • kest_op_stack gives load.elem.run 3 in and 3 plus the layout out, and store.elem.run 3 plus the layout in and nothing out.
  • verify.c checks a number at the top and the next, an array third, element_run (run_holds on the element's layout, with the offset pointing at the field in the first of the run, which is what in_the_run writes: the run's start plus inside), and kept_in for the store. Then it drops slots + 3.
• Lowering: read_place and write_place return for count > 0 before any fused path. A consuming read and take_address of such a place fault rather than lower to load.elem or elem.addr.
• Docs: compiler.md's 225 instructions is the table plus two, and the new sentence describes the element place.
• ! with the footer is right at 0.x, since a refused program now runs. The body's code block lines (rows[0]..., io.print(...)) are not commit headers, and the title check passes.

[siracozmen01]

Delta review at 8e588a1: ready. CI was pending when I read it (title passes), so this assumes it goes green. Read, not run.

The delta touches only tests. Comparing the trees of 88738d8 and 8e588a1, the only change at the root is tools/. Within it, only tools/check-commands.sh and tools/check-c.sh change. src/ and test/ are the same trees.

My point had two parts, and the new rows cover both:

• The VM's read check (IN_RUN in load.elem.run): the /= row divides by z = 0. With the read check, the read past the run is refused first with K0604 index 3 is outside 3 of them. Without it, the read goes on and the division is refused with K0601, so the row fails. The += row cannot tell the two apart, since the write's check says the same sentence, and the body says so. It is there for the compound path, which is fine.
• The C backend's check (kest_run_at): check-c.sh compiles = 9 and /= nought with at = len(rows) + 2 and nought = len(rows) - 1, values found at run time, so the C compiler cannot fold them. Each must print an error line containing K0604 and index 3 is outside 3 of them, and that line must equal kest run's byte for byte. A missing write check makes = print nothing. A missing check anywhere before the division makes /= print K0601. Either way the C check fails, which matches the two mutants in the body.
• A build or compile failure counts as wrong too, so a C backend that cannot compile the program does not pass silently. $runpast_said is added to the summary line.

The body's Verification describes the three rows, the C check and both mutants as the scripts and the reported runs show them. No line in the body starts at column 0 with a name and (.