025 stale tx after commit

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

Code

// PIN: after `commit(tx)` discharges the <transaction!> obligation, binding `tx`
// is stale — its phantom state was consumed. Using `tx` in a subsequent call
// (rollback) is use-after-discharge. This is the database analogue of
// 330_007_use_after_disposal: a binding used after its obligation is discharged.
//
// Grounding:
//   - legal flow:             330_027/input.kz:4-9 (commit OR rollback, then disconnect)
//   - commit consuming <!tx>: ./db.kz:40 (pub event commit { tx: *Transaction<!transaction> })
//   - use-after pattern:      330_007/input.kz:3 (close then use-file with same binding)
import app/db

app/db:connect(url: "postgres://localhost/test"): c |> app/db:query(conn: c, sql: "SELECT * FROM users"): tx |> app/db:commit(tx) |> app/db:rollback(tx) |> app/db:disconnect(conn: c)

input.k

Supporting Files

// Library module: db (copy of 330_027/db.kz)
// Database operations with layered cleanup obligations
//
// Pattern: connect → query → (commit OR rollback) → disconnect
//
// Grounding: 330_027_db_transaction_pattern/db.kz verbatim

const std = @import("std");

const Connection = struct {
    id: i32,
};

const Transaction = struct {
    conn: *Connection,
};

~pub tor connect { url: string } -> *Connection<connected!>

~proc connect|zig {
    std.debug.print("Connecting to: {s}\n", .{url});
    const allocator = std.heap.page_allocator;
    const c = allocator.create(Connection) catch unreachable;
    c.* = Connection{ .id = 1 };
    return c;
}

~pub tor query { conn: *Connection<connected>, sql: string } -> *Transaction<transaction!>

~proc query|zig {
    std.debug.print("Query: {s}\n", .{sql});
    const allocator = std.heap.page_allocator;
    const t = allocator.create(Transaction) catch unreachable;
    t.* = Transaction{ .conn = conn };
    return t;
}

~pub tor commit { tx: *Transaction<!transaction> }

~proc commit|zig {
    std.debug.print("Committing transaction\n", .{});
}

~pub tor rollback { tx: *Transaction<!transaction> }

~proc rollback|zig {
    std.debug.print("Rolling back transaction\n", .{});
}

~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 'tx' was already discharged and cannot be used
  --> tests/regression/300_ADVANCED_FEATURES/335_OBLIGATION_STRESS/335_025_stale_tx_after_commit/input.k:12: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

← 024 stale view after take 040 subflow drops obligation on input →