✓
Passing This code compiles and runs correctly.
Code
// PINS: `std/grid:for(lo..hi, g) ! each i |> ...` — a bounded loop the GRID
// owns, so the index's proof is established once at the door and the body
// rides a trusted cursor.
//
// std/grid:for(0..8, cells)
// ! each i |> std/grid:stored { cells[i].v: i * 2 }
//
// The driver emits ONE check before the loop (`lo >= 0`, `hi <= size`,
// `lo <= hi`) and renames the binding to the minted cursor
// `__koru_gi_<grid>_L<line>` — a name that carries WHICH grid the range was
// proven against. Reads AND writes of the proven grid at the bare cursor
// drop the `__koru_at` floor; everything else keeps it.
//
// post.sh pins all four directions in the emitted Zig:
// cells[i] read/write -> __koru_intcast (trusted)
// cells[i+1] read -> __koru_at (not the bare cursor)
// dst[i] write -> __koru_at (proof was for cells)
// dst[k] read -> __koru_at (ordinary for, unproven)
//
// The value oracle: cells[i]=2i over 0..8; dst[i]=cells[i]+cells[i+1] over
// 0..7 = [2,6,10,14,18,22,26], dst[7]=0; sum=98.
import std/io
import std/grid
std/grid:new(cells, size: 8) { v: 0[i64] }
std/grid:new(dst, size: 8) { w: 0[i64] }
std/grid:for(0..8, cells)
! each i |> std/grid:stored { cells[i].v: i * 2 }
| done |> std/io:print.ln("written")
std/grid:for(0..7, cells)
! each i |> std/grid:stored { dst[i].w: cells[i].v + cells[i + 1].v }
capture { sum: 0[i64] }
! as s |> for(0..8)
! each k |> captured { sum: s.sum + dst[k].w }
| captured r |> std/io:print.ln("{{ r.sum:d }}")
Actual
written
98
Expected output
written
98
Flows
flow ~new click a branch to expand · @labels scroll to their anchor
new (cells, size: 8, source: v: 0[i64])
flow ~new click a branch to expand · @labels scroll to their anchor
new (dst, size: 8, source: w: 0[i64])
flow ~for click a branch to expand · @labels scroll to their anchor
for (0..8, cells)
flow ~for click a branch to expand · @labels scroll to their anchor
for (0..7, cells)
flow ~capture click a branch to expand · @labels scroll to their anchor
capture (source: sum: 0[i64])
Test Configuration
MUST_RUN LANGUAGES: zig
Post-validation Script:
#!/bin/bash
# Pin: a grid:for cursor is trusted only on the grid it was proven for —
# minted as `__koru_gi_<grid>_L<line>` — while every other index keeps the
# floor, and the range check is emitted ONCE before the loop.
set -e
# 1. The bare cursor on the PROVEN grid never crosses the floor.
if grep -qE "__koru_at\(__koru_gi_cells_L[0-9]+\)" output_emitted.zig; then
echo "FAIL: cursor on its own grid still routed through __koru_at"
exit 1
fi
# 2. Trusted spelling on the proven grid (read in a value position and the
# write lvalue).
grep -qE "__koru_intcast\(usize, main_module\.__KoruGridT_cells\.__koru_wide\(__koru_gi_cells_L[0-9]+\)\)" output_emitted.zig || {
echo "FAIL: trusted cursor spelling not found on a proven-grid access"
exit 1
}
grep -qE "__koru_intcast\(usize, main_module\.__KoruGridT_cells\.__koru_wide\(__koru_gwx" output_emitted.zig || {
echo "FAIL: cursor-addressed write on the proven grid still carries the floor"
exit 1
}
# 3. `cells[i+1]` is not the bare cursor — the floor stays.
grep -qE "__koru_at\(__koru_gi_cells_L[0-9]+ \+ 1\)" output_emitted.zig || {
echo "FAIL: an unproven offset index lost the floor"
exit 1
}
# 4. `dst[i]` writes to a grid the proof does not name — floor stays.
grep -q "__koru_at(__koru_gwx" output_emitted.zig || {
echo "FAIL: a write to a grid outside the proof went unchecked"
exit 1
}
# 5. An ordinary `for` index keeps the floor — trusted is the cursor's
# provenance, not a property of counting.
grep -q "__koru_at(k)" output_emitted.zig || {
echo "FAIL: unproven index lost the floor — trusted widened beyond the cursor"
exit 1
}
# 6. The door check: one compare before the loop, panic on the outside.
grep -qE "if \(__koru_forlo_L[0-9]+ < 0 or __koru_forhi_L[0-9]+ > @as\(i64, @intCast\(main_module\.__KoruGridT_cells\.__koru_size\)\) or __koru_forlo_L[0-9]+ > __koru_forhi_L[0-9]+\) @panic" output_emitted.zig || {
echo "FAIL: the hoisted range check is missing from the emitted driver"
exit 1
}