Show HN: Formally verified 3D CSG: Trust 93 lines spec, not 1000 lines AI code

https://github.com/godotengine/godot-proposals/issues/9711

Many performant implementations have a separate layer that tries to use floats to decide inequalities and fall back to higher precision when floats are not sufficient. As I understand, this layer can be separated from the geometrical predicates we need (what I mean by predicate is for example deciding which side of a plane a point is), so we could formalize that arithmetic layer separately using axioms on floating point numbers and then plug it in the existing code. I think we could do that and still provide exact outputs and prove the same spec we have right now and the performance should increase a lot, since most of the computations right now is computing all these predicates exactly.

I would not say numerical stability is the one enemy of CSG. See the special cases https://github.com/schildep/verified-3d-mesh-intersection#sp... and bugs in an alternative C++ implementation that also used exact rationals mentioned in https://github.com/schildep/verified-3d-mesh-intersection#co....

Also note that many implementations don’t even try to treat special geometrical cases correctly (for example they „cheat“ by using something called simulation of simplicity which provides some guarantees against some bugs, but at the expense of not treating the cases exactly correctly which can lead to artifacts).

In the 93 lines I assumed a reviewer already trusts that the kernel of the Lean proof assistants is correct. We have to trust somethings.

As far as I know manifold is not verified software, but it does promise that manifold inputs become manifold outputs.

I wonder how manifold will break in that condition or would it snap to the nearest manifold.

https://github.com/schildep/verified-3d-mesh-intersection#wh...

One complication: For union the spec would look a little bit different than for intersection. I defined the solid associated to a mesh in a way that does not include the surface of the mesh itself. That works for the intersection. For union we would have:

solidWithSurface (meshUnion M₁ M₂) = solidWithSurface M₁ ∪ solidWithSurface M₂

I think it would not be hard to reduce the implementation and the proof of correctness to the intersection: There are some tricks which you can do like flipping the orientation of a mesh and putting a large cube that contains both meshes around it and then intersect these. (Hopefully the implementation would not actually do this, but this construction could be used in the proof.)

So you can have the strange situation of proof that the Lean code is correct, but no way of proving that the running machine code corresponds with the same program.

There is also the problem of knowing whether the microprocessor works according to its spec, and I don't think we have anything public about modern multi core processors about that.

To get the feel of this it might help to start with a simpler example: If you declare a function in ordinary old Java with return type int, the Java compiler will complain unless every path through that function returns either an int or something that can be converted to it (or throws). Lean is similar but uses a much more powerful type system called dependent types, which gives you extreme control over the values that are permitted in a type: For example, in Lean it's possible to define a type that consists of just the even integers, or even just the prime numbers. If you define such a PrimeNumber type, and then declare a function that returns a PrimeNumber, the Lean compiler will complain if the function could ever return a number that is not prime. IOW, if your function compiles with no errors, it is proven to always return a prime number.

I expect that OP's code defines a function named something like intersect(), and which takes 2 arguments of a type named something like Mesh, and returns not simply another Mesh but in fact a more complicated type: specifically, a Mesh that is somehow constrained to be a sub-mesh of each of the first and second arguments. Since mesh intersection is deterministic, I expect that this more complicated type will turn out to be inhabited by just a single value (mesh) -- similar to a type FortyTwo whose only value value is the integer 42. (I'm assuming here that a mesh can only be represented in one canonical way; this might not be true.) Then, Lean will complain at compile time if there exists any conceivable pair of input meshes for which the function would construct the wrong intersection.

You can go a very long way using discrete math though. I'm pretty sure it's doable to implement, say, a 3D slicer (to prepare layers/paths for 3D printing I mean) without using any floating point operation.

P.S: FWIW I was coding intros and demos using 3D effects on the Commodore Amiga and then on 386 PCs without using the 387 (the FP co-processor of the 386, when present). I'm not saying it's useful to play games in 4K: what I'm saying is that there are certainly applications where formally verified algos using integer math do make sense.

Blender used to struggle with boolean operations, though. Seems to have got much better some time in the last couple of years, but without knowing any of the backstory I don't know if they've bodged it into shape or would benefit from something proven.

Other than that you can also read introductory material for set theory. There the meaning of all of the unicode symbols you can see in the spec should be explained.