5.1. Verification path: YieldElim🔗

YieldElim (enabled by verifyCoroutine := true) verifies each coroutine as a straight-line procedure, so the verifier never reasons about a dispatch loop. It rewrites every yield in the body into an inline block

assert ⋀guarantees;
snapshot $old_heap;   // = $heap, pre-havoc (for the rely's old)
havocHeap();          // the environment acts (a havoc)
assume ⋀relies;
snapshot $old_heap    // = $heap, post-havoc (start of the next step)

and clears the coroutine's relies/guarantees clauses, turning it into a regular procedure. The assert discharges the coroutine's own step guarantee; the havocHeap() call (a bodiless opaque modifies * preamble procedure) models the environment acting while suspended; the assume grants the rely about that environment step. havocHeap's monotonic-counter postcondition records that the environment step allocates but never deallocates, so a post-yield allocation cannot alias a pre-yield reference.

Both clause families are two-state, and each relates a prior heap to the current $heap. A single reassigned snapshot $old_heap serves both sides, since a coroutine step is linear:

• A guarantee's old(...) — spelled oldGuarantee(...) in body asserts and loop invariants — reads $old_heap while it holds the start of the current step (procedure entry, or the post-havoc heap after the previous yield).

• A rely's old(...) — spelled oldRelies(...) — reads $old_heap after the pre-havoc reassignment, so an assumed rely is R($old_heap, $heap) = "what the environment did across this step".

Both are emitted as a labeled Old (some $old_heap), which heap parameterization evaluates against $old_heap; heap-param also declares the $old_heap local (seeded to the entry heap) and lowers each Snapshot to $old_heap := $heap. The per-yield asserts cover each resume → yield step; a separate pass step (addExitGuarantees) asserts the guarantee on every path out of the body (before each return and at the body end), covering the final resume → halt segment that the caller also observes.

YieldElim runs before HeapParameterization: it never touches $heap directly, emitting Snapshot/labeled-Old/havocHeap() for heap-param to lower. Resolution is disabled across that gap, so those transient artifacts reach heap-param untouched. YieldElim also handles the caller-side dual (the coroutineRelyHeap step): it threads a per-instance $h1_co snapshot through resume callers and adds the $h_rely_old parameter to the generated resume procedures. Unlike the body rewrite, this caller-side step runs regardless of verifyCoroutine, since the default elaboration path also emits the oldRelies/oldGuarantees markers it lowers.