✓
Passing This code compiles and runs correctly.
Code
// PINS: the sweep's own cursor indexes the grid WITHOUT the index floor.
//
// std/grid:sweep(cells) ! sweep c |> std/grid:stored { c.v: c.v + 1 }
//
// The loop the sweep emits constructs the index from `0..__koru_size`, so the
// `__koru_at` call the shared lowering wraps around it re-proves a fact the
// transform already holds. The cursor rides the lowering as a TRUSTED index
// — the same widening + cast, spelled through `__koru_intcast` so no
// `llvm.assume` reaches the vectorizer — with the failure edge gone.
//
// Two directions are pinned, in post.sh: `__koru_at` never receives the
// cursor, and the SAME program's ordinary `cells[i]` under `for` keeps the
// floor — trusted is a property of the name's provenance, not a widening of
// `unsafe(bounds)`.
//
// The value oracle: cells starts [0,10,20,0], the sweep adds 1 to every
// visited cell, the for-loop sums: 1 + 11 + 21 + 1 = 34.
import std/io
import std/grid
std/grid:new(cells, size: 4) { v: 0[i64] }
std/grid:stored { cells[1].v: 10 }
std/grid:stored { cells[2].v: 20 }
std/grid:sweep(cells)
! sweep c |> std/grid:stored { c.v: c.v + 1 }
capture { sum: 0[i64] }
! as s |> for(0..4)
! each i |> captured { sum: s.sum + cells[i].v }
| captured r |> std/io:print.ln("{{ r.sum:d }}")
Actual
34
Expected output
34
Flows
flow ~new click a branch to expand · @labels scroll to their anchor
new (cells, size: 4, source: v: 0[i64])
flow ~stored click a branch to expand · @labels scroll to their anchor
stored (source: cells[1].v: 10)
flow ~stored click a branch to expand · @labels scroll to their anchor
stored (source: cells[2].v: 20)
flow ~sweep click a branch to expand · @labels scroll to their anchor
sweep (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: the sweep cursor is emitted TRUSTED — the widening + __koru_intcast
# spelling, never __koru_at — while an ordinary `cells[i]` under `for` in the
# same program keeps the floor.
set -e
# 1. No cursor ever goes through the floor.
if grep -q "__koru_at(__koru_gi" output_emitted.zig; then
echo "FAIL: sweep cursor still routed through __koru_at"
exit 1
fi
# 2. The trusted spelling (widen, then the vectorizer-safe cast) is emitted
# for cursor reads.
grep -q "__koru_intcast(usize, main_module.__KoruGridT_cells.__koru_wide(__koru_gi" output_emitted.zig || {
echo "FAIL: trusted cursor spelling (__koru_intcast + __koru_wide) not found on a cursor read"
exit 1
}
# 3. A cursor-addressed write lands unchecked too — the write unit's own
# parameter is trusted when the site's index is the cursor.
grep -q ")[[:space:]]*__koru_intcast(usize, main_module.__KoruGridT_cells.__koru_wide(__koru_gwx" output_emitted.zig \
|| grep -q "__koru_intcast(usize, main_module.__KoruGridT_cells.__koru_wide(__koru_gwx" output_emitted.zig || {
echo "FAIL: cursor-addressed write unit still carries the floor"
exit 1
}
# 4. The floor still exists for an index nobody proved: `cells[i]` under the
# ordinary `for` must route through `__koru_at`.
grep -q "__koru_at(i)" output_emitted.zig || {
echo "FAIL: unproven index lost the floor — trusted widened beyond the cursor"
exit 1
}