10.3. Specifying step boundaries: rely/guarantee🔗

Laurel chooses rely/guarantee contracts for coroutines. This is a general form that enables modular verification. Each coroutine can be annotated with a rely R and a guarantee G, where R is a two-state predicate describing every environment step while the coroutine is suspended, and G is a two-state predicate describing the coroutine's own step. Each coroutine's guarantee is what its peers are entitled to assume as their rely, which is what makes per-coroutine verification compose into a whole-program argument.