[siracozmen01]

Problem

A program reading or writing one of a fixed run at an index worked out while running, where the run is inside one of another run at an index written down, inside an element of an array, was refused by the verifier as a fault in the compiler (#253). With struct S { tag: i32; xs: [i32; 4] }, struct Box { ss: [S; 2] }, boxes holding one Box of S(1, [1, 2, 3, 4]) and S(2, [5, 6, 7, 8]), and j worked out while running as 2,

io.print("{boxes[0].ss[1].xs[j]}")
boxes[0].ss[1].xs[j] = 9
io.print("{boxes[0].ss[1].xs[2]}")

was refused under every build and switch with

error[K0411]: `o.main`: `load.at` at 102 reads layout 0 at 24 bytes into what an address is at, which has no such field there

and, without the read, "store.elem.run at 96 reads 4 of layout 0 at 24 bytes into an element that has no such run there". It now prints 7 and then 9. A run of runs with its first index written down is the same case: with struct B { tag: i32; grid: [[i32; 3]; 2] }, reading bs[0].grid[1][j] was refused at 16 bytes.

The compiler writes the right offset. The verifier asks run_holds whether a run of four i32 sits 24 bytes into a Box, and run_holds looked into the fields of a struct but not into one of a fixed run: it found ss, a run of two, and answered no. field_of, which the same reads ask when no index is worked out while running, already looks into one of a run.

Change

• src/verify.c: run_holds asks the one of a fixed run that the offset falls in, when the offset is inside the run, as field_of does. Each of them is laid out alike, so which one it is does not matter.
• tools/check-verifier.sh: the program it changes carries outers[k].ins[1].xs[j] read and written, and four new cases change the byte offset of that load.at and store.elem.run to where the verifier has to refuse them with K0411. At 20 bytes in, the second Inner's tag, no run is. At 44, where the xs of a third Inner would be, the run's place in one Inner is a run, and only the outer run's length says it is past the end of the 40 bytes an Outer has.
• test/regress/runinrun.kest: reads, =, +=, *= in a loop and a bool written, into a run inside the second of two structs in an element, with the struct's other fields and the other element read back; and a run of runs read and written with its first index written down.

A program refused before now runs, so this takes !. Nothing the verifier accepted before changes, and no instruction the compiler writes changes. No version moves.

Verification

• test/regress/runinrun.kest is refused with K0411 by a kest built from main (d692b17). With this src/verify.c linked into the same build in its place, it answers 0, and compiled to C it answers 0; the program above prints 7 and 9, and the bs[0].grid[1][j] read prints 6.
• tools/check-verifier.sh on this branch: "27 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 main's library its program does not build: the verifier refuses inside with K0411, as it does the program above.
• Against a copy of this branch's library with offset < whole->byte_size taken out of run_holds, the check fails with "a run read past the last of the run it is in was held" and "a run written past the last of the run it is in was held": at 44 bytes, 44 % 20 is 4, the xs of an Inner, so only the bound refuses them.
• Light compile check of src/verify.c with clang-20, clang-format in the CI image, and kest fmt of the new program.
• Through heavy.sh, on a dev build of this branch (on d692b17) before the verifier cases were added: 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 among them, which runs the new program under both builds, the heap walked at every allocation, KEST_PLAIN, KEST_NOOPT and compiled to C. The cases change only the check, which was run on its own against the same build, above.
• The full gate runs in CI.

Closes #253

BREAKING CHANGE: a program reading or writing one of a fixed run at an index worked out while running, where the run is inside one of another run at an index written down, inside an element of an array, was refused with K0411 and now compiles and runs.

[siracozmen01]

Review at 2fd786d: changes needed (1). Read, not run.

1. The "past the last" refusal case cannot fail on the bound it is meant to guard.
   • In the check's program, Inner is tag: i32 plus xs: [i32; 4]: 20 bytes, with xs at 4. Outer is 40 bytes.
   • The case sets the load.at offset to 40. With offset < whole->byte_size removed from the new branch, 40 % 20 = 0 lands on the second Inner's tag. The struct walk finds no run there and refuses anyway, so the case passes with or without the bound.
   • The offset that tests the bound is 44. With the bound, 44 < 40 fails and it is refused. Without it, 44 % 20 = 4 lands on xs, the base case accepts a run of four i32 4 bytes into a third Inner, and the read runs 4 to 20 bytes past the 40-byte element.
   • So the bound is what keeps the widened walk inside the element, and 44 (for load.at, and the same for store.elem.run if you want both) is the case that pins it.

The widened walk itself is right. Read against field_of and the existing branches:

• No straddling. The new branch hands offset % element->byte_size to the element's own type. Every way run_holds answers true from there ends at the base case: a fixed run of exactly count elements of step bytes, with offset < step, found as a member or element inside that one element. So the run it accepts lies wholly inside one element of the outer run, and offset < whole->byte_size keeps that element inside the whole.
• No padding. The base case still asks field_of(element, offset, field), and field_of's struct walk takes a member only when offset lies within [byte_offset, byte_offset + size). An offset in padding between members, or at the end of an element, matches no member and is refused.
• No new over-acceptance from the existing struct branch, which has no upper bound on offset. It recurses with offset - byte_offset into a member whose own branches are bounded (offset < step, and now offset < byte_size).
• The 20-byte cases (the tag, for both load.at and store.elem.run) do test the walk: 20 % 20 = 0 lands on tag, so the widened walk refuses only because nothing there is a run.

Not verified: whether the verifier docs list K0411's cases in a way that now needs the nested run named. The message text is unchanged, and I cannot search the tree. A search for K0411 in docs/ would settle it.

The ! and footer are as the body explains. The new regress file is confirmed as new.

[siracozmen01]

Delta 2fd786d..b2c2272: ready. The finding is fixed. Read, not run.

• The past-the-last cases are at 44 now, for both load.at and store.elem.run. 44 % 20 = 4 lands on xs, so only offset < whole->byte_size refuses them. The session reports that removing the bound in a copy fails exactly these two cases, so the bound is pinned for reads and writes. The two tag cases at 20 still test that the widened walk finds no run on tag.
• The comment over the cases names both points. src/verify.c and the regress file are unchanged since 2fd786d.
• docs/internals/verifier.md lists the passes and no K0411 cases, so the docs owe nothing here.