5. Scaling Up: Advanced Features and Capstones

This chapter is framed explicitly as "the toolkit doesn't change, only its ergonomics do". It is also the one part of the tutorial explicitly designed to be enterable cold: a reader who already knows separation logic/Iris (or who's willing to take Parts 1–4's core assertions on faith) should be able to start here directly. That's a deliberate tradeoff against the "one example grows across the whole tutorial" pitch from the introduction — resolved by keeping backreferences to specific earlier subsections rather than re-teaching them. Each section opens with a one-line "Assumes" pointer naming exactly what's carried over from earlier parts.

• 5a. Capstone: Fork/Join — no new mechanism, just Parts 1–4's whole toolkit, applied once, start to finish, including the first attempt that doesn't work.
• 5b. Atomic Contracts — Capstone: The Ticket Lock
• 5c. Iterated Separating Conjunctions — Capstone: A Shelf of Counters
• 5d. Automation Features