025 stale tx after commit

✓ Passing This code compiles and runs correctly.

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")
| connected c |> app/db:query(conn: c, sql: "SELECT * FROM users")
    | started tx |> app/db:commit(tx) |> app/db:rollback(tx) |> app/db:disconnect(conn: c)

input.kz

Must contain:

Use-after-discharge

Error Verification

Actual Compiler Output

error[KORU030]: Use-after-discharge: binding 'tx' was already discharged and cannot be used
  --> phantom_semantic_check:13:0

❌ Compiler coordination error: Phantom semantic validation failed
error: CompilerCoordinationFailed
/Users/larsde/src/koru/tests/regression/300_ADVANCED_FEATURES/335_OBLIGATION_STRESS/335_025_stale_tx_after_commit/backend.zig:94:13: 0x10310e3b3 in emit (backend)
            return error.CompilerCoordinationFailed;
            ^
/Users/larsde/src/koru/tests/regression/300_ADVANCED_FEATURES/335_OBLIGATION_STRESS/335_025_stale_tx_after_commit/backend.zig:190:28: 0x10310f09f in main (backend)
    const generated_code = try RuntimeEmitter.emit(compile_allocator, final_ast);
                           ^

Imported 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 event connect { url: []const u8 }
| connected *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 .{ .connected = c };
}

~pub event query { conn: *Connection<connected>, sql: []const u8 }
| started *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 .{ .started = t };
}

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

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

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

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

~pub event disconnect { conn: *Connection<!connected> }

~proc disconnect|zig {
    std.debug.print("Disconnecting\n", .{});
}

db.kz

Test Configuration

MUST_FAIL

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