A more rigorous way to verify rendering correctness

[kmatzen]

Sinter has two independent implementations of every SDF operation and nothing checks that they agree:

• src/worker/sdf/evaluate.ts — the CPU evaluator, used for meshing and therefore for everything you export
• src/worker/sdf/codegen.ts — GLSL generation, used for the ray-marched viewport

The viewport is what users judge the model by; the CPU path is what ends up in the printer. A divergence between them means the STL doesn't match what was on screen, and today nothing would catch that.

What existing tests cover

codegen.test.ts asserts on the text of generated GLSL — that it contains sdBox, that NaN got sanitized. That confirms codegen emits plausible-looking source, not that the source computes the right distance. evaluate.test.ts checks CPU distances at hand-picked points (center is inside, outside is positive). Both are reasonable smoke tests. Neither compares the two paths, and neither would notice if a GLSL operator drifted from its CPU counterpart.

Proposals, roughly in order of value per effort

1. Differential testing, CPU vs. GPU. The highest-value item. Compile the generated GLSL, evaluate it over a sampled point set in a headless WebGL context, and assert it agrees with evaluateSDF within a tolerance. Catches operator drift directly. The work is mostly harness: getting WebGL running headless in CI (headless-gl, or Playwright with a real context — Playwright is already a dependency), and picking a tolerance that tolerates mediump/highp differences without going slack enough to hide real bugs. Sampling should be biased toward surfaces, where disagreement matters and where both implementations are least stable.

2. Property-based tests over random trees. Generate random node trees and assert properties that hold for any correct SDF, independent of both implementations:

• Lipschitz bound — |f(a) - f(b)| <= |a - b| for a true distance field. Sphere tracing depends on this; violating it causes the overshoot artifacts that look like holes in thin walls.
• Boolean algebra — union(a,b) == union(b,a), intersect(a,a) == a, subtract(a, empty) == a.
• Transform invariance — translating a shape by t and evaluating at p equals evaluating the untransformed shape at p - t.
• Sign agreement — CPU and GPU may differ slightly in magnitude but must never disagree on inside vs. outside away from the surface.

fast-check fits the existing Vitest setup. This finds cases nobody thought to hand-write, which is where these bugs live.

3. Golden-image tests for the viewport. Playwright is already set up. Render a fixed set of models at a fixed camera and compare against committed reference images with a perceptual diff. Catches shader regressions that value-level tests miss — normals, lighting, the hasWarn highlight path. Brittle across GPUs and driver versions, so it needs a generous threshold and probably a pinned CI runner; more of a change-detector than a correctness proof.

4. Meshing invariants. dualContour should produce a watertight manifold: every edge shared by exactly two triangles, consistent winding, no degenerate triangles. These are checkable on the output without a reference implementation, and a non-manifold mesh is a print failure. Partially covered in dualContour.test.ts; worth making exhaustive since #26 (thin-wall warning) depends on mesh validity.

On formal methods specifically

TLA+ was the right tool for the WorkerBridge protocol (see specs/, #50) because that was a concurrency problem with a small discrete state space. It is the wrong tool here. Rendering correctness is numeric and geometric — floating-point tolerance, sampling density, continuous space — none of which TLC can model usefully.

The rigorous options for this class of problem are differential and property-based testing (above), or an SMT-backed check of specific algebraic identities in codegen via something like Z3 over floating-point theory. The latter is a real option for a bounded question — "does the generated GLSL for smoothUnion compute the same function as the CPU version, for all inputs in range" — but it is a much larger undertaking than #1 and #2, and I would want those in place first to see whether they leave anything uncovered.

Suggested order: 1 and 2 together (they share a tree generator), then 4, then 3 if viewport regressions turn out to be a recurring problem in practice.