✓
Passing This code compiles and runs correctly.
Code
// PINS: `std/grid:walk { s: inp.b, 2, d: enc.c, 3 }` — a RESLICING window
// walk over borrowed columns. The driver emits
//
// var s = __koru_grid_inp.b[0..];
// var d = __koru_grid_enc.c[0..];
// while (s.len >= 2 and d.len >= 3) {
// __grid_walkbody_L<line>_event.handler(.{ .s = s, .d = d });
// s = s[2..];
// d = d[3..];
// }
// __grid_walktail_L<line>_event.handler(.{ .s = s, .d = d });
//
// Each labeled arg names a cursor and the positional after it is its
// stride. The bound is proven once at the loop head (`s.len >= n`) —
// inside, every `s[k]`/`d[k]` is a raw slice access with no per-access
// floor. This is the loop shape LLVM auto-vectorizes: moving base
// pointers plus fixed-offset reads and writes, the same shape Goose's
// slice-window loops emit. The `| tail` arm runs once with the leftover
// window (s.len < n here) — the remainder is the program's to write,
// never silently dropped.
//
// Value oracle: inp = [1..7] u8, stride 2 -> 3 full pairs + 1 leftover;
// enc stride 3: d[0]=s[0]+1, d[1]=s[1]+1, d[2]=s[0]+s[1] per pair;
// tail writes d[0] = s[0] + 100 (the leftover byte, readable).
// enc = [2,3,3, 4,5,7, 6,7,11, 107]; sum = 155.
import std/io
import std/grid
std/grid:new(inp, size: 7) { b: 0[u8] }
std/grid:new(enc, size: 10) { c: 0[u8] }
for(0..7)
! each i |> std/grid:stored { inp[i].b: @as(u8, @intCast(i + 1)) }
std/grid:walk { s: inp.b, 2, d: enc.c, 3 }
! each |> std/grid:stored { d[0]: s[0] + 1, d[1]: s[1] + 1, d[2]: s[0] + s[1] }
| tail |> std/grid:stored { d[0]: s[0] + 100 }
| done |> std/io:print.ln("sum={{ enc[0].c + enc[1].c + enc[2].c + enc[3].c + enc[4].c + enc[5].c + enc[6].c + enc[7].c + enc[8].c + enc[9].c:d }} last={{ enc[9].c:d }}")
Actual
sum=155 last=107
Expected output
sum=155 last=107
Flows
flow ~new click a branch to expand · @labels scroll to their anchor
new (inp, size: 7, source: b: 0[u8])
flow ~new click a branch to expand · @labels scroll to their anchor
new (enc, size: 10, source: c: 0[u8])
flow ~for click a branch to expand · @labels scroll to their anchor
for (0..7)
flow ~walk click a branch to expand · @labels scroll to their anchor
walk (source: s: inp.b, 2, d: enc.c, 3)
Test Configuration
MUST_RUN
Post-validation Script:
#!/bin/sh
# A walk emits a reslicing driver: two `var` cursors off the columns, a
# counted `for (0..__koru_walktrips)` whose trip count is min(len/stride) —
# the proof the body's raw s[k]/d[k] accesses lean on, in a form LLVM can
# unroll — then `s = s[(n)..]` / `d = d[(m)..]` reslices and a tail call.
# NO __koru_at anywhere on the walked columns — the borrow's contract carries.
EMIT=$(ls output_emitted.zig 2>/dev/null || ls emitted.zig 2>/dev/null)
grep -q "var s: \[\]u8 = main_module.__koru_grid_inp.b\[0..\];" "$EMIT" || { echo "src cursor missing"; exit 1; }
grep -q "var d: \[\]u8 = main_module.__koru_grid_enc.c\[0..\];" "$EMIT" || { echo "dst cursor missing"; exit 1; }
grep -q "__koru_walktrips = @min(__koru_walktrips, d.len / (3));" "$EMIT" || { echo "trip count missing"; exit 1; }
grep -q "for (0..__koru_walktrips) |_| {" "$EMIT" || { echo "counted walk loop missing"; exit 1; }
grep -q "s = s\[(2)..\];" "$EMIT" || { echo "src reslice missing"; exit 1; }
grep -q "d = d\[(3)..\];" "$EMIT" || { echo "dst reslice missing"; exit 1; }
grep -q "__grid_walktail_" "$EMIT" || { echo "tail call missing"; exit 1; }
grep -q "__koru_gs0: \[\]u8" "$EMIT" || { echo "cursor not threaded to write unit"; exit 1; }
# No floor inside the walk's own driver proc — from the cursor decls to
# `return;` there may be no __koru_at at all (other sites, like the fill
# loop's ordinary stored, keep the floor they deserve).
awk '/var s: \[\]u8 = __koru_grid_inp|var s: \[\]u8 = main_module.__koru_grid_inp/{f=1} f&&/__koru_at/{bad=1} f&&/^ return;/{f=0} END{exit bad}' "$EMIT" || { echo "walk driver still pays the floor"; exit 1; }
exit 0