pub fn certify_external_placement(
placement: &Grid,
source: &[FabricOp],
result: usize,
width: u32,
) -> Option<PlacementCertificate>Expand description
Import-and-certify — the SDK-facing seam. Certify a placement PRODUCED BY AN EXTERNAL TOOL (e.g. the
SambaFlow place-and-route) against the English source datapath: lower the external placement grid and
the source spec to the same bounded fragment, then prove they agree for every input and keep the
re-checkable witness. Returns None (fail-closed) if the placement is NOT equivalent to the source, or the
obligation escapes the propositional fragment. We need nothing from the vendor but the placed grid — no
config format, no trust in their placer: the certificate stands on its own via
PlacementCertificate::recheck. This is how a vendor mapping earns a proof it computes the intended
program.