5. Concurrency🔗

Coroutines are lowered along one of two paths, selected by the LaurelTranslateOptions.verifyCoroutine flag. The default path elaborates each coroutine into an executable state machine; the opt-in verification path generates verification conditions directly from the coroutine body under rely/guarantee. The two paths live in CoroutineElaboration.lean and YieldElim.lean respectively. CoroutineElaboration runs before LiftInstanceProcedures (it emits instance calls that pass must lift); the coroutine-lowering pass YieldElim runs later, just before HeapParameterization.

1. 5.1. Verification path: YieldElim
2. 5.2. Execution path: state-machine linearization
3. 5.3. Contract representation
4. 5.4. Exception lowering