Skip to main content

certify_external_placement

Function certify_external_placement 

Source
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.