Struct PlacementCertificate 

pub struct PlacementCertificate { /* private fields */ }

A machine-checkable certificate that a placed mapping grid computes its datapath spec for every bounded assignment. It carries the refuted CNF (¬(grid ≡ datapath)) and the propagation-redundancy + RUP refutation of it. It is self-contained: recheck needs nothing but the certificate.

Implementations

impl PlacementCertificate

pub fn recheck(&self) -> bool

Re-verify the certificate INDEPENDENTLY. Trusts only the small PR/RUP checker — not the prover, placer, or emitter that produced it. This is the audit a third party runs to confirm our place-and-route without re-deriving anything: it replays the refutation against the original CNF and returns whether every step is redundancy-sound and the empty clause is reached.

pub fn len(&self) -> usize

The number of refutation steps carried — the size of the shipped proof.

pub fn is_empty(&self) -> bool

pub fn num_vars(&self) -> usize

The number of Boolean variables in the refuted obligation.

pub fn digest(&self) -> u64

A stable 64-bit digest of the whole certificate — the refuted CNF and every refutation step, witnesses included (FNV-1a over the literal codes) — so a summary that travels without the object is bound to it: a dropped step, a changed clause or a different obligation is a different digest.

pub fn with_last_step_removed(&self) -> Self

A tampered copy: the final refutation step is dropped, so the empty clause is no longer derived. Used to prove the checker is load-bearing — recheck on the result must return false.

Trait Implementations

impl Clone for PlacementCertificate

fn clone(&self) -> PlacementCertificate

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for PlacementCertificate

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.