Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

github.com

Post reply on HN
Print view View original

51–57 of 57 posts

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

#51

Post by angry_octet »

kens wrote: post #48
angry_octet wrote: post #24

Earlier quoted context omitted.

The code generation for Lean is not AFAIK verified in any way. It uses C as a portable assembler, and uses too many fancy C constructs to be compiled by CompCert C, which is the only fully verified compiler. 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 th…

It's kind of hopeless to try to prove that a microprocessor works according to spec, since you're dealing with physical objects in the real world. For instance, early versions of Intel's 386 processor had a 32-bit multiply problem that only showed up in some chips under particular combinations of temperature, voltage, and frequency, probably due to a transistor that wasn't large enough to provide an electrical margin…

Chip makers would disagree. They use tools that simulate at the electrical circuit level for just such problems, and using massive amounts of testing and inspection to statistically bound variations in chip geometry caused by process variation.

It is the quantum effects that occur at tiny geometries that make this hard, but every chip you buy has passed extensive variation.

To account for individual variation and random glitches there are other techniques, like triple modular redundancy or lockstep processors. Or for less stringent software, just computing it twice in different cores and memory blocks.

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

#53

Post by guyomes »

permute wrote: post #2

Note that the claims are about the kernel that computes the mesh intersection, not the web demo: While the kernel is formally verified, the UI and glue code (that call the kernel) are not. I once hit a bug that looked like there were holes in the resulting mesh: I found that it was an overflow in the glue code (now fixed) that converts the exact rationals coordinates of the output mesh, for which we prove the specifi…

> I found that it was an overflow in the glue code (now fixed) that converts the exact rationals coordinates of the output mesh, for which we prove the specification, to floats

Preserving the topology of mesh intersections while rounding the coordinates is a hard problem. In particular, it is only in 2020 that an algorithm was found that handles all the cases [1]. In practice, an efficient algorithm for that was published last year [2].

[1]: https://doi.org/10.1007/s00454-020-00202-2 https://hal.science/hal-02549290/file/DCG.pdf

[2]: https://doi.org/10.1111/cgf.70197 https://hal.science/hal-05242294/file/Snap-SGP-revised.pdf

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

#56

Post by elalish »

iFire wrote: post #5
iFire wrote: post #3

How does it compare against https://github.com/elalish/manifold in performance and zero corruption? I spent a lot of time making elalish/manifold work in Godot Engine and it is now a method in Blender too. https://manifoldcad.org If it helps, feel free to use the apache2 licensed unit tests that were generated in manifold development https://github.com/elalish/manifold/tree/master/test

> Why we cannot have manifold output meshes in general 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...

The difference is that my Manifold library uses a different definition of what constitutes a manifold mesh: https://github.com/elalish/manifold/wiki/Manifold-Library#ma.... By being a purely topological definition, there is no implicit assumption that vertices with the same coordinates are connected. As such we can still generate a 2-manifold even in the "impossible" cases.

The more important difference though, is that our library can still handle epsilon-valid self-intersecting meshes, rather than just reporting an error. This is critical in practice because meshes are stored, transported, and transformed in floating-point, so even the formally-proven non-self-intersecting results of the library under discussion will not necessarily be valid input for it anymore after a round-trip through a file format or a rotation.

Still, these are details. I think the real contribution here is demonstrating a new approach to formally verifying software even for notoriously difficult problems. I believe that concept is really important, as the general state of software reliability tells me that the state of the art in testing software is desperately lacking. I think formal verification may well be one of the most important aspects of computer science research in the nearish term.

Post reply on HN