✓
Passing Passing: the compiler rejects this program as expected.
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
Actual compiler output
error[KORU032]: Cannot discharge outer-scope resource 'h0' inside @scope boundary. Handle outside the scope or escape via branch constructor.
--> tests/regression/300_ADVANCED_FEATURES/330_PHANTOM_TYPES/330_077_reject_carry_consume_in_for/input.kz:25:4
❌ Compiler coordination error: Auto-discharge failed (multiple disposal options or no disposal event)
(set KORU_BACKEND_TRACE=1 for the backend return trace)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
Test Configuration
MUST_ERROR