✓
Passing This code compiles and runs correctly.
Code
// NEGATIVE: a label-fold consumes an OUTER-issued obligation each iteration with
// NO compensating reissue on the back-edge. `step` consumes the outer handle
// (<!owned>) but does NOT re-issue an <owned!>; the back-edge re-feeds the SAME
// outer binding `h0`, which was already discharged on the prior iteration. With
// no reissue, every back-edge is a use-after-discharge, and a 0-iteration run
// leaks the outer obligation. MUST be rejected.
// Grammar grounded against 330_017_scope_label_loop (@loop re-feeding an outer
// binding), 330_072_obligation_transfer_through_loop (<owned!>/<!owned> markers),
// and 210_123 (#loop / @loop fold form).
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;
}
// Consumes <!owned> but re-issues nothing (branch payloads are plain i32).
~tor step { h: *Handle<!owned> }
| again i32
| stop i32
~proc step|zig {
h.n += 1;
if (h.n < 3) {
return .{ .again = h.n };
}
return .{ .stop = h.n };
}
~tor report { n: i32 }
~proc report|zig {
std.debug.print("n={}\n", .{n});
}
~tor spin { h: *Handle<!owned> } -> i32
~spin = #loop step(h)
| again _ |> @loop(h) // re-feeds already-consumed h -> use-after-discharge, no reissue
| stop r -> r
~make(): h0 |> spin(h: h0): f |> report(n: f)
Must fail at runtime with:
CONTAINS error[KORU030]
CONTAINS Use-after-dischargeFlows
subflow ~spin click a branch to expand · @labels scroll to their anchor
#loop step (h)
flow ~make click a branch to expand · @labels scroll to their anchor
make