✓
Passing This code compiles and runs correctly.
Code
// NEGATIVE: carry an OWNED obligation into a for(0..N) and consume it inside.
// SOUNDNESS: for(0..N) may run 0 times (then the <owned!> obligation is never
// discharged -> leak) OR >1 times (then the second iteration consumes a handle
// that was already discharged on the first -> use-after-discharge). The
// per-iteration count is not provable, so an in-loop consume of a singly-owned
// obligation MUST be rejected.
// Grammar grounded against 330_015_scope_for_loop_outer (for under a branch)
// and 330_072_obligation_transfer_through_loop (<owned!>/<!owned> markers).
const std = @import("std");
const Handle = struct { n: i32 };
~tor make {} -> *Handle<owned!>
~proc make|zig {
const h = std.heap.page_allocator.create(Handle) catch unreachable;
h.* = .{ .n = 0 };
return h;
}
~tor consume { h: *Handle<!owned> }
~proc consume|zig {
std.heap.page_allocator.destroy(h);
}
~make(): h0 |> for(0..3)
! each _ |> consume(h: h0) // consumes the single owned handle every iteration
| done |> _
Backend must reject with:
CONTAINS error[KORU032]
CONTAINS Cannot discharge outer-scope resource
CONTAINS @scope boundaryFlows
flow ~make click a branch to expand · @labels scroll to their anchor
make