022 disconnect before commit

✓ Passing Passing: the compiler rejects this program as expected.

Code

// PIN: disconnect (outer resource) is called BEFORE commit (inner resource
// that requires the outer connection). This violates LIFO resource ordering:
// Rust would drop inner before outer; every DB library commits before
// disconnecting. After disconnect(conn: c), c is discharged (<connected!>
// consumed). commit(tx, conn: c) then reads c as <connected> — use-after-discharge.
//
// Legal order (330_027/input.kz): commit(tx) |> disconnect(conn: c)
// This test inverts that order.
//
// Grounding:
//   - flow structure:            330_027/input.kz
//   - connect/query/disconnect:  ./db.kz (this dir's fixture)
//   - commit requiring conn:     ./db.kz (conn: *Connection<connected>)
//   - disconnect consuming conn: ./db.kz (pub tor disconnect { conn: *Connection<!connected> })
~import app/db

~app/db:connect(url: "postgres://localhost/test"): c |> app/db:query(conn: c): tx |> app/db:disconnect(conn: c) |> app/db:commit(tx, conn: c)

input.kz

Supporting 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", .{});
}

db.kz

Actual compiler output

error[KORU030]: Use-after-discharge: binding 'c' was already discharged and cannot be used
  --> tests/regression/300_ADVANCED_FEATURES/335_OBLIGATION_STRESS/335_022_disconnect_before_commit/input.kz:17:0

❌ Compiler coordination error: Phantom semantic validation failed
   (set KORU_BACKEND_TRACE=1 for the backend return trace)

Must contain:

Use-after-discharge

Flows

flow ~connect click a branch to expand · @labels scroll to their anchor

connect (url: "postgres://localhost/test")

Test Configuration

MUST_ERROR

← 021 instance no explicit free 023 disconnect before rollback →