✓
Passing This code compiles and runs correctly.
Code
// NEGATIVE: a single re-issued <owned!> handle is consumed TWICE on the same
// back-edge path (use-after-discharge). The `again` branch issues one <owned!>
// (`v`); routing it into BOTH a disposing consume AND @loop consumes the same
// obligation twice. Linearity is one-issue/one-consume, so this MUST be rejected.
// Grammar grounded against 330_072_obligation_transfer_through_loop (transfer
// shape, <!owned> consume marker) 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;
}
~tor step { h: *Handle<!owned> }
| again *Handle<owned!>
| stop *Handle<owned!>
~proc step|zig {
h.n += 1;
if (h.n < 3) {
return .{ .again = h };
}
return .{ .stop = h };
}
// A consuming/disposing leaf.
~tor drop { h: *Handle<!owned> }
~proc drop|zig {
std.heap.page_allocator.destroy(h);
}
~tor spin { h: *Handle<!owned> } -> *Handle<owned!>
~spin = #loop step(h)
| again v |> drop(h: v) |> @loop(h: v) // consumes v twice -> double consume
| stop r -> r
~make(): h0 |> spin(h: h0): hf |> drop(h: hf)
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