✓
Passing This code compiles and runs correctly.
Code
// PIN: on the failure path, disconnect is called before rollback — same
// LIFO violation as 335_022 but on the error branch. The rule is symmetric:
// both commit AND rollback require the connection still live (conn: <connected>).
// Disconnecting first in the error path is as wrong as in the happy path.
//
// Legal order (330_027/input.kz): rollback(tx) |> disconnect(conn: c)
// This test inverts that order.
//
// Grounding:
// - error-branch rollback pattern: 330_027/input.kz (| else |> rollback(tx) |> disconnect)
// - rollback requiring conn: ./db.kz (conn: *Connection<connected>)
// - disconnect consuming conn: ./db.kz (pub tor disconnect { conn: *Connection<!connected> })
~import app/db
~import std/control
const error_occurred = true;
~app/db:connect(url: "postgres://localhost/test"): c |> app/db:query(conn: c): tx |> if(error_occurred)
| then |> app/db:disconnect(conn: c) |> app/db:rollback(tx, conn: c)
| else |> app/db:commit(tx, conn: c) |> app/db:disconnect(conn: c)
Must contain:
Use-after-dischargeFlows
flow ~connect click a branch to expand · @labels scroll to their anchor
connect (url: "postgres://localhost/test")
Imported Files
// Library: DB with explicit commit-needs-connection constraint.
//
// connect → query → (commit | rollback) → disconnect
//
// commit and rollback both require conn: *Connection<connected> (not consuming
// it — phantom annotation <connected> without ! means "must be in this state,
// but don't consume the obligation"). This encodes the real-world invariant:
// committing a transaction requires the connection to still be open.
//
// Grounding: 330_027/db.kz — same lifecycle, bare-return spellings.
const std = @import("std");
const Connection = struct {
id: i32,
};
const Transaction = struct {
id: i32,
};
~pub tor connect { url: string } -> *Connection<connected!>
~proc connect|zig {
const c = std.heap.page_allocator.create(Connection) catch unreachable;
c.* = Connection{ .id = 1 };
return c;
}
~pub tor query { conn: *Connection<connected> } -> *Transaction<transaction!>
~proc query|zig {
const t = std.heap.page_allocator.create(Transaction) catch unreachable;
t.* = Transaction{ .id = 1 };
return t;
}
// commit requires conn in <connected> (non-consuming read) and consumes tx
~pub tor commit { tx: *Transaction<!transaction>, conn: *Connection<connected> }
~proc commit|zig {
std.debug.print("Committing\n", .{});
}
// rollback requires conn in <connected> (non-consuming read) and consumes tx
~pub tor rollback { tx: *Transaction<!transaction>, conn: *Connection<connected> }
~proc rollback|zig {
std.debug.print("Rolling back\n", .{});
}
// disconnect consumes connected! — after this conn is dead
~pub tor disconnect { conn: *Connection<!connected> }
~proc disconnect|zig {
std.debug.print("Disconnecting\n", .{});
}