See https://github.com/solson/miri/issues/532#issuecomment-442552764: If my analysis is correct,
async fn violates Stacked Borrows, but that's just a silly mistake that went unnoticed only because mutable references implicitly coerce to shared references.
a.k.a. why my ACA model did not treat mutable references as "asserting" (i.e. popping the stack) until they are used to some degree.
of course, that approach has the disadvantage of forcing a tree instead of a stack.
it's somewhat weird to see that the examples that violate this are clearly mistakes, rather than being just dubious unsafe code.
(I expected it to be mainly dubious unsafe code that just uses &mut as intermediates).