Function decomposes_by_section 

pub fn decomposes_by_section(p: &SpatialProgram) -> bool

Does this choreography’s liveness proof decompose into one proof per section?

The precondition section_ranges checks, exposed so a caller — and the lock that probes it — can see which form a certificate will take and why, instead of inferring it from the certificate’s size.