Sheet 02 — anatomy
A certificate is worth exactly as much as the thing that computes it. If a
caller can write sound: true into a field, the field is marketing. So the
kernel's certificate is a computed verdict, and the struct that carries it
says so on its first line.
/// The kernel's COMPUTED verdict on a solid — never written by the caller. /// `is_sound()` is the honest "this is a real, closed, manufacturable solid" /// gate: a valid B-Rep that is watertight and manifold.
Soundness is a conjunction of nine independent predicates. That choice is the whole design. An OR, or a score, or a weighted heuristic would let a part pass while carrying a defect that one of the checks could see perfectly well — and the entire value of the certificate is that it cannot be talked around.
Each conjunct exists because it catches a defect class the others structurally cannot. This is not asserted in the abstract; it is documented field by field, at the field.
Rosherapub fn is_sound(&self) -> bool {
self.brep_valid
&& self.watertight
&& self.manifold
&& self.oriented
&& self.self_intersection_free
&& self.construction_consistent.is_sound()
&& self.eyes_consistent.is_sound()
&& self.tessellation.clean
&& self.mesh_quality.clean
}
oriented can. Every conjunct earns its place by
being the sole witness to some failure.
model_debris_orphan_faces existed, orphan faces left behind by a broken
boolean carried solid_id: None, and their boundary-edge errors leaked into
every part's brep_valid verdict. One bad operation could make an
untouched part report unsound. The fix was to attribute debris at model scope — visible,
loud, and not charged to a part that did nothing wrong.
/// A label is an ANNOTATION, not a geometric /// feature, so an `Inconsistent` verdict does /// NOT affect `is_sound()` — it is its own /// honest flag the agent/frontend can surface /// (stale labels rendered amber).
The discipline of exclusion
A certificate that gates on everything it measures is as dishonest as one that gates on nothing — it fails parts for reasons that are not defects, and the people receiving it learn to ignore it. Five things are measured and deliberately kept out of the AND.
Four are simple counts backing a boolean that is gated: the Euler
characteristic, boundary edges, non-manifold edges, inconsistent directed edges. They are
diagnostics, not verdicts. If watertight is false you want to know it was
four boundary edges and not four hundred.
The other two exclusions are substantive, and each encodes a judgement about what a certificate is for. A stale label means an annotation no longer holds — the geometry is untouched, and failing the solid would be a category error. Model debris means orphan faces exist somewhere in the model; real, worth surfacing, and specifically not this part's fault.
The same discipline recurs one level down. mesh_quality measures four
things and gates on two.
// `clean` (which gates `is_sound`) keys ONLY on the true mesh-TOPOLOGY // defects — a facet that bridges across a periodic lateral // (`boundary_crossing`) or folds far off the surface (`normal_deviation`). // Both are 0 on a clean part. Aspect ratio and min-angle are SHAPE-quality // readouts …, NOT gates: a faithful tessellation routinely carries aspect ~150- // 290 slivers …, so gating on them would flag every real part. They are the // OPTIMISATION ORACLE — the number to drive down — not a soundness bar.
A sliver triangle with an aspect ratio of 290 is ugly. It is not a lie. Keeping it out of the gate is what lets the gate mean something when it does fire — and the number stays on the certificate as the thing to improve.
There was a period where a solid whose mesh dimensions failed certified as
sound: false, errors: [] — a verdict with no actionable content. Every failing
gated dimension now synthesises a typed entry, so the certificate always names the
dimension that sank it.
Mechanism
Names are marketing until you read the implementation. Four of the nine are derived from a single welded-mesh pass at chord 0.1 with a weld epsilon of 1e-6: vertices are quantised onto a grid, degenerate triangles are dropped rather than counted, and a directed-edge multiset is accumulated over every surviving triangle.
From that one structure: an edge is boundary exactly when its undirected incidence is one; non-manifold when it exceeds two; the mesh is oriented when no directed edge is traversed more than once; and the Euler characteristic is V − E + F over referenced welded vertices.
| Invariant | Actually performed | Density |
|---|---|---|
| brep_valid | Scoped validation; errors owned by other solids or by orphan topology are filtered out | mesh-independent |
| watertight | Zero mesh edges with undirected incidence 1 | chord 0.1 |
| manifold | Zero mesh edges with incidence > 2 | chord 0.1 |
| oriented | Zero directed edges traversed more than once | chord 0.1 |
| self_intersection_free | Spatial-hash broad phase, exact AABB reject, triangle–triangle narrow phase | chord 0.5 |
| construction_consistent | Every profile point inside the solid's bbox, expanded by max(1% diagonal, tol) | bbox |
| eyes_consistent | Every recognised feature resolves to a live face of the expected surface type | topological |
| tessellation.clean | No degenerate facets; stored and analytic normals agree with winding | display |
| mesh_quality.clean | No periodic boundary-crossing facets; normal deviation under 40° | display |
This is the part a competitor would leave out, which is precisely why it belongs here. In four places the implementation is narrower than the field name suggests, and anyone relying on this certificate should know exactly where.
Orientation is local. The check finds directed edges traversed twice — two facets winding the same way across a shared edge. A mesh in which every facet is uniformly inverted has no repeated directed edge and passes. Outward-ness is not tested.
Self-intersection is gross. It runs on an audit tessellation at chord 0.5 — coarser than the watertightness pass — on the reasoning that gross self-overlap is visible at low density. The broad phase is exact; the approximation is in the density. A shallow self-intersection below that resolution is not detected.
Boundary conformance is u-only. Facets are tested for bridging across a periodic seam only on surfaces that declare a u-period. A torus's second period is not tested; a planar face contributes zero crossings by construction.
Construction consistency is a bounding box. It catches a sketch that has drifted or been orphaned — the case it was built for. It does not verify that the profile still generates the solid.
eyes_consistent is the only reconcile-family check inside the gate, and it
resolves ambiguity against itself: a live face whose surface type cannot be resolved is
treated as inconsistent, not as passing. Its expected-surface map is coarse —
holes and bosses expect cylinders, fillets expect tori, chamfers expect planes — so a
variable-radius fillet reads as inconsistent. That is the intended direction of error.
Some is always current as of the last mutation. Model-debris count is the
exception: it is re-stamped on every return, even from cache, because a debris note that
outlived the debris would be a lie.
/// SOUNDNESS CONTRACT — the verdict must NEVER /// claim `sound: true` it has not actually /// verified. This runs SYNCHRONOUSLY, under the /// model write lock, on EVERY create/loft/ /// boolean/etc., so it must be both TRUSTWORTHY /// and FAST.
sound: true from only the cheap checks — so a
self-intersecting solid was certified sound on every build. The code's own verdict on
that period: "That defeats the moat: a verdict that asserts soundness it never
checked." The resolution was to make the full check fast, not to drop it.
The chokepoint
The certificate is computed inside the same write guard that performed the mutation, at fifteen call sites — every primitive, boolean, blend, transform, extrude, revolve, loft and import. There is no path that mutates geometry and returns without passing through it.
The codebase puts the cost at roughly 44 ms on a 19.8k-triangle part in release, and judges that acceptable on the hot path. That is the trade being made explicitly: every operation pays a fixed verification tax so that no operation can lie.
Callers may opt out per request with "fast": true, which returns only the
lightweight perception block. The default — absent flag, or "fast": false — is
the full certificate. One endpoint refuses the opt-out entirely:
STEP import hard-codes full verification, on the grounds that a STEP file
is untrusted external input.
A second, render-based check views the solid from fourteen viewpoints — distributed by Fibonacci-sphere sampling for even coverage — and reconciles what it sees against what the kernel claims, face by face. It is genuinely independent, and when it runs it is honest about coverage rather than guessing at occlusion.
It is also advisory, and does not gate the mutation. It runs off the
write lock on an owned snapshot, capped at two concurrent, and under burst it is skipped
entirely and left pending. The source says so three separate times, including
"Advisory severity. Never affects is_sound. Gating lives in the
certificate."
The distinction is worth stating plainly because the two things share a name. The render-free feature check is synchronous and gating. The fourteen-viewpoint render is asynchronous and advisory. Anyone who tells you their kernel renders every mutation from fourteen angles before accepting it is describing something we deliberately did not build: it would put a render in front of every write.
The second certificate
A constraint sketch has a different honesty problem. An under-constrained sketch is not broken — it is a legal, useful intermediate state that every draughtsman works in. So the sketch certificate deliberately does not gate on degrees of freedom.
/// The single can't-lie predicate: a sketch is SOUND when its constraint
/// system is satisfiable, its geometry is valid, and it does not
/// self-intersect. DOF freedom and open profiles are reported, not failed.
pub fn is_sound(&self) -> bool {
self.constraint_consistent && self.entities_valid && self.self_intersection_free
}
Degrees of freedom are accounted structurally — points contribute two, circles three, arcs five, splines 2n — and constraints subtract what they remove. Constraints referencing unsupported entities are excluded from the tally rather than counted, which is what keeps the arithmetic honest rather than merely tidy.
Conflicts, however, override the count. Two independent detectors run: a numerical rank diagnosis, and a static-pair check. They are unioned, because the numerical pass can miss — a line direction collapsing to zero vacuously satisfies both parallel and perpendicular. The codebase's note on this is that solvers of the DCM and OCCT class need both, and so do we.
When a sketch over-constrains, the certificate does not say "over-constrained". It returns a minimal conflicting constraint set — the specific constraints that cannot hold together, each with its type and residual, ascending by id.
Minimisation uses QuickXplain (Junker, AAAI-04), which finds a size-k core among n candidates in O(k·log(n/k)) oracle calls. The oracle is an isolated re-solve under exactly that subset. A false negative can only enlarge the witness; it can never fabricate satisfiability.
minimal flag. It is true when QuickXplain completed or
the conflict is a static pair. It is false when the oracle-call cap of 128 was exceeded or
the re-solve could not reproduce the rank diagnosis — in which case the honest
un-minimised conflict set is returned rather than a smaller set that was never proven.
pub struct ConflictWitness {
pub kind: WitnessKind,
pub constraints: Vec<WitnessConstraint>,
pub minimal: bool,
pub oracle_calls: usize,
}
//! The "kernel cannot lie" thesis says a mould //! that breaks a downstream feature must surface //! as a *typed verdict*, never a silent bad or //! partial model … a **re-measured** `is_sound()` //! verdict recomputed from the resulting B-Rep — //! never asserted.
RebuildCertificate::is_sound() is a
getter over a stored boolean. The re-measurement happened at construction. It is still
measured rather than asserted — but it is measured then, not at the moment you
ask.
The third certificate
History here is event-sourced: an edit to an earlier operation is a new event appended to the timeline, never a mutation of the original. Replaying it can break something downstream — a fillet whose edge no longer exists, a boolean whose operand changed shape.
The rebuild certificate is the account of that. Every feature gets a status: rebuilt, unaffected, failed with a reason, dangling with the missing entity, blocked by an earlier break, or stale — the honest arm for document-level events like drawings that have no geometric replay and therefore reflect an older part without being broken.
The global verdict is true only when every feature rebuilt or was unaffected, no reference dangled, and the resulting B-Rep validates on re-measurement. Otherwise the mould is refused and the certificate names the first break.