5.2. Execution path: state-machine linearization🔗

The default path (CoroutineElaboration.lean) compiles a coroutine body into a state-machine lookup table indexed by a $pc field on a generated <c>State composite, with resume and has_next instance procedures. Linearization assigns each straight-line fragment of the body a $pc label and rewrites control flow into transitions between labels: a yield stamps the resume target and returns to the scheduler (a suspend), while ordinary sequencing falls through to the next label (a transition). resume dispatches on $pc; has_next is $pc != END. This form is convenient for concrete execution but reasons through the heap and $pc at every step, which is why the verification path bypasses it.