celld forged lease

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

Code

// The World in Koru — entry 8, negative twin two of 838_celld_lease_race.
// Doorway: celld's losing node — the one whose conditional PUT came back 412.
// Over there `cas_owner` returns `CasOutcome::Rejected` and it is up to the
// caller to honour it; the write path is an ordinary function and nothing in
// the type of a cell name says "you may not call this." Correctness rests on
// the caller checking the outcome.
//
// Here the losing branch simply has no token in it, and a lease cannot be
// conjured from a bare string. The check is not something the caller remembers
// to do — there is no spelling of the forgery that type-checks.
import std/io
import std/store

std/store:new(own, capacity: 1) { epoch: 0[i64], etag: 0[i64] }

pub tor cas.claim { node: string, guard: i64 }
| applied string<lease!>
| rejected

cas.claim = if(guard == own.etag)
| then |> std/store:stored { own.etag: own.etag + 1, own.epoch: own.epoch + 1 } => applied node
| else => rejected

pub tor cell.write { lease: string<lease>, cell: string, data: string }
cell.write = std/io:print.ln("  {{ lease:s }}  write e{{ own.epoch:d }} {{ cell:s }} <- {{ data:s }}")

pub tor cas.release { lease: string<!lease> }
cas.release = std/io:print.ln("  {{ lease:s }}  release")

// node-b lost the CAS. It tries to write anyway, forging a lease from a string.
std/store:stored { own.etag: 1 }
cas.claim(node: "node-b", guard: 0)
| applied l |> cell.write(lease: l, cell: "room-42", data: "legitimate")
| rejected |> cell.write(lease: "node-b", cell: "room-42", data: "forged")

input.k

Actual compiler output

error[KORU030]: Phantom state mismatch: argument 'lease' has no tracked phantom state, but this event requires state '<lease>'.
  --> tests/regression/830_THE_WORLD/840_celld_forged_lease/input.k:34:0

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

Must fail at runtime with:

CONTAINS has no tracked phantom state

Flows

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

new (own, capacity: 1, source: epoch: 0[i64], etag: 0[i64])

subflow ~cas.claim click a branch to expand · @labels scroll to their anchor

if (guard == own.etag)

subflow ~cell.write click a branch to expand · @labels scroll to their anchor

print.ln (expr: " {{ lease:s }} write e{{ own.epoch:d }} {{ cell:s }} <- {{ data:s }}")

celld forged lease

Code

Actual compiler output

Must fail at runtime with:

Flows

Test Configuration