pub fn eval_choreography_dry(p: &SpatialProgram) -> Result<Trace, ChoreoFault>Expand description
A token-only run: every choreography check (reservations, pushes, waits, semaphore protocol, multicast landing, accumulator protocol, store coverage) with no arithmetic — the certificate’s dry run, every trip at its greatest count.