celld ack after fence

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

Code

input.k

Actual compiler output

error[KORU030]: Use-after-discharge: binding 'l' was already discharged and cannot be used
  --> tests/regression/830_THE_WORLD/847_celld_ack_after_fence/input.k:76:8

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

Must fail at runtime with:

CONTAINS Use-after-discharge

Flows

flow ~new click a branch to expand · @labels scroll to their anchor
new (own, capacity: 1, source: epoch: 0[i64], etag: 0[i64])
flow ~new click a branch to expand · @labels scroll to their anchor
new (st, capacity: 1, source: pos: 0[i64], synced: 0[i64])
subflow ~cas.claim click a branch to expand · @labels scroll to their anchor
if (guard == own.etag)
subflow ~cas.release click a branch to expand · @labels scroll to their anchor
print.ln (expr: " release {{ lease:s }} — clean handoff")
subflow ~node.fence click a branch to expand · @labels scroll to their anchor
print.ln (expr: " SELF-FENCE {{ lease:s }} — lease not renewed within TTL")
subflow ~node.renew click a branch to expand · @labels scroll to their anchor
print.ln (expr: " renew {{ lease:s }}")
subflow ~cell.write click a branch to expand · @labels scroll to their anchor
if (own.epoch > 0)
subflow ~replica.sync click a branch to expand · @labels scroll to their anchor
if (upto <= st.pos)
subflow ~gate.ack click a branch to expand · @labels scroll to their anchor
print.ln (expr: " ack {{ r:s }} — durable through {{ proof:d }}")
subflow ~gate.fail click a branch to expand · @labels scroll to their anchor
print.ln (expr: " fail {{ r:s }} — {{ why:s }}")
subflow ~served click a branch to expand · @labels scroll to their anchor
cell.write (lease, data)
flow ~cas.claim click a branch to expand · @labels scroll to their anchor
cas.claim (node: "node-a", guard: 0)

Test Configuration

MUST_ERROR