Module pnr_certificate 

Proof-carrying place-and-route.

A dataflow compiler that only reports a mapping — the way a spatial-architecture toolchain validates a placement with performance counters — asks you to TRUST that the placed grid computes the intended datapath. We instead SHIP A CERTIFICATE: a machine-checkable refutation that the placed grid equals its datapath specification for every bounded input. The recipient (e.g. the silicon vendor) re-verifies it with PlacementCertificate::recheck, trusting only the tiny PR/RUP checker in logicaffeine_proof::pr — never our prover, our placer, or our word. That is the difference between “we validated it” and “here is the proof; check it yourself.”

The obligation is the same grid ≡ datapath biconditional the SAT-certified placer already discharges; here we keep the witness (the propagation-redundancy + RUP steps) instead of discarding it, so the certificate travels with the emitted RTL.

Structs

PlacementCertificate

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.

Enums

CertifyRefusal

Why a mapping earned no certificate. The three answers are genuinely different — “we cannot express this obligation”, “we will not pay to materialise it”, and “it is not true” — and a caller that prints Uncertified { reason } must not collapse them into one sentence.

Constants

GATE_BUDGET_NODES

How large a SHARED GATE DAG the certificate path will pay to refute.

Functions

certify_external_placement

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.

certify_gates

Certify a placement whose grid and datapath are ALREADY blasted into the shared gate DAG — the path that never materialises a ProofExpr tree, and therefore the only one that can certify a reconvergent datapath (a multiply chain’s tree is exponentially larger than its circuit). Fail-closed exactly like certify_mapping: a grid that is not equivalent to its spec earns no certificate.

certify_gates_bounded

certify_gates with the refusal NAMED, against the production GATE_BUDGET_NODES.

certify_gates_within

certify_gates_bounded against an EXPLICIT gate ceiling — the seam a lock shrinks to prove the budget is live code and not a constant nobody reads.

certify_mapping

Emit a proof-carrying certificate that the placed grid equals the datapath spec for every bounded input, by refuting ¬(grid ≡ datapath) and KEEPING the checkable refutation. Fail-closed: returns None when the equivalence does not actually hold (a wrong mapping earns no certificate) or the obligation leaves the propositional fragment (bit-blast the datapath first). A returned certificate is guaranteed recheck-valid by construction — the underlying prover only hands back a refutation it has already PR/RUP-verified.

certify_mapping_bounded

certify_mapping with the refusal NAMED. The obligation is PRICED in the shared gate DAG before any ProofExpr is materialised, so an encoding too big to hold fails as a typed refusal in milliseconds instead of walking the allocator off a cliff.

certify_mapping_within

certify_mapping_bounded against an EXPLICIT bit-blast ceiling — the seam a lock shrinks to prove the budget is live code and not a constant nobody reads.