022 disconnect before commit

✗ Failing This test is currently failing.

Failed: frontend

Failure Output

error[PARSE005]: redundant explicit label 'tx:' — the value 'tx' already puns to 'tx'
  --> tests/regression/300_ADVANCED_FEATURES/335_OBLIGATION_STRESS/335_022_disconnect_before_commit/input.kz:19:1
    |
 19 |     | started tx |> app/db:disconnect(conn: c) |> app/db:commit(tx: tx, conn: c)
    | ^
  hint: drop the label: write 'tx' instead of 'tx: tx'

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:7): commit(tx) |> disconnect(conn: c)
// This test inverts that order.
//
// Grounding:
//   - flow structure:            330_027/input.kz:4-8
//   - connect/query/disconnect:  ./db.kz (this dir's fixture)
//   - commit requiring conn:     ./db.kz:45 (conn: *Connection<connected>)
//   - disconnect consuming conn: ./db.kz:59 (~pub event disconnect { conn: *Connection<!connected> })
~import app/db

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

input.kz

Must contain:

Use-after-discharge

Error Verification

Actual Compiler Output

error[PARSE005]: redundant explicit label 'tx:' — the value 'tx' already puns to 'tx'
  --> tests/regression/300_ADVANCED_FEATURES/335_OBLIGATION_STRESS/335_022_disconnect_before_commit/input.kz:19:1
    |
 19 |     | started tx |> app/db:disconnect(conn: c) |> app/db:commit(tx: tx, conn: c)
    | ^
  hint: drop the label: write 'tx' instead of 'tx: tx'

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:
//   - struct field phantom pattern: 330_027/db.kz:11-13 (Connection struct)
//   - event with non-consuming phantom req: 330_027/db.kz:34 (query takes conn: *Connection<connected>)
//   - obligation consume marker <!state>: 330_027/db.kz:46 (commit consumes <!transaction>)
//   - disconnect consuming <!connected>: 330_027/db.kz:60

const std = @import("std");

const Connection = struct {
    id: i32,
};

const Transaction = struct {
    id: i32,
};

~pub event connect { url: []const u8 }
| connected *Connection<connected!>

~proc connect|zig {
    const c = std.heap.page_allocator.create(Connection) catch unreachable;
    c.* = Connection{ .id = 1 };
    return .{ .connected = c };
}

~pub event query { conn: *Connection<connected> }
| started *Transaction<transaction!>

~proc query|zig {
    const t = std.heap.page_allocator.create(Transaction) catch unreachable;
    t.* = Transaction{ .id = 1 };
    return .{ .started = t };
}

// commit requires conn in <connected> (non-consuming read) and consumes tx
~pub event 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 event 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 event disconnect { conn: *Connection<!connected> }

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

db.kz

Test Configuration

MUST_FAIL

← 021 instance no explicit free 023 disconnect before rollback →