✓
Passing Passing: the compiler rejects this program as expected.
Code
// PIN: after `std/string:take(s)` consumes the <view!> binding `s` and
// produces a new <instance!> binding `owned`, the old binding `s` is stale.
// Using `s` in a subsequent call is use-after-discharge: the view! obligation
// was consumed by take, and `s` no longer has a valid phantom state.
//
// The transition take: *String<!view> → | instance *String<instance!>
// is the ATS/Mezzo "transfer" move: ownership moves to a new name.
// The old name is invalid from that point forward.
//
// Grounding:
// - take consuming <!view>: koru_std/string.kz:74
// - take producing instance!: koru_std/string.kz:75
// - from-page/take flow shape: 610_002_string_ownership/input.kz:5-11
// - use-after-discharge shape: 610_005_reject_use_after_free/input.kz:6 (free then len)
import std/string
std/string:from-page(text: "hello")
| ok s |> std/string:take(s): owned |> std/string:len(s): _ |> std/string:free(s: owned)
| err _ |> _
Actual compiler output
error[KORU030]: Use-after-discharge: binding 's' was already discharged and cannot be used
--> tests/regression/300_ADVANCED_FEATURES/335_OBLIGATION_STRESS/335_024_stale_view_after_take/input.k:18:0
❌ Compiler coordination error: Phantom semantic validation failed
(set KORU_BACKEND_TRACE=1 for the backend return trace)Must contain:
Use-after-dischargeFlows
flow ~from-page click a branch to expand · @labels scroll to their anchor
from-page (text: "hello")
Test Configuration
MUST_ERROR