Function certify_choreography 

pub fn certify_choreography(
    p: &SpatialProgram,
) -> Result<ChoreographyCertificate, CertifyFault>