logicaffeine_compile/spatial/passes/
verify.rs

1//! `verify` — attach the choreography certificate, or refuse.
2
3use super::SpatialReject;
4use crate::spatial::certificate::{certify_choreography, CertifyFault};
5use crate::spatial::ir::*;
6use crate::spatial::target::SpatialTarget;
7
8pub fn verify(
9    p: &SpatialProgram,
10    _target: &SpatialTarget,
11) -> Result<SpatialProgram, SpatialReject> {
12    if p.certificate.is_some() {
13        return Ok(p.clone());
14    }
15    if p.schedule.is_none() {
16        return Err(SpatialReject::WrongPhase {
17            pass: "verify",
18            expected: "Scheduled",
19            found: p.phase(),
20        });
21    }
22    p.validate()?;
23    match certify_choreography(p) {
24        Ok(cert) => {
25            let mut q = p.clone();
26            q.certificate = Some(cert);
27            Ok(q)
28        }
29        Err(CertifyFault::Invalid(v)) => Err(SpatialReject::Invalid(v)),
30        Err(CertifyFault::Eval(f)) => Err(SpatialReject::Unverified(f)),
31        Err(other) => Err(SpatialReject::Unverified(
32            crate::spatial::eval::ChoreoFault::Unsupported(format!("{other:?}")),
33        )),
34    }
35}

logicaffeine_compile/spatial/passes/verify.rs

logicaffeine_compile/spatial/passes/
verify.rs