You might find it interesting that I am working on AI-driven decomp of a PS1 game not by matching bytes but by having agents produce C code and test code. Agents submit a C proposal to the harness, the harness compiles their C proposal for the original function, then the test suite provided by the implementer runs against the original machine code and the compiled C code version. The line and branch coverage of both must be 100% and given identical inputs and starting RAM, the function return value and RAM state and RAM/MMIO read write sequence must be identical. This is done with a small MIPS simulator which can run all the tests extremely fast.
The reason I’m finding this is much faster than a traditional decomp is that while it’d be nice for the bytes to match, finding the perfect blend of compiler version, compiler args, permitting variables etc to try and find the perfect register assignments, etc is all very time consuming. My ultimate goal is not a byte for byte match, that’s just one way to ensure correctness. I’ve found agents are much faster and effective at reading the original assembly and understanding what’s going on then writing semantically equivalent C.
That's a great approach, I think byte matching is just popular because it's extremely easy to test in the end: are the bytes the same? While your approach requires putting far more trust into the tests.
I was just looking at this yesterday. Apparently Voyager 1 architecture, ISA, etc are well known but Voyager 2 is still denied via FOIA on grounds of copyright.
Voyager 1 and Voyager 2 are identical, as are their computers. JPL's Voyager documentation is the property of Caltech, not NASA, and are thus not available via FOIA. People have gotten copies of selected documentation by requesting them from libraries that have copies of the original documents on file.
Would they be different? They launched 16 days apart. I always assumed they were mostly the same core hardware. hm... rereading the wikipedia pages now...
I never really "got" sim tower growing up, I liked sim city but bounced off tower. It only clicked years later when I read that it was an elevator simulator that got fleshed out a bit, Knowing this I enjoy it quite a bit more today than younger me who I guess was expecting a vertical simcity.
> People don't usually remember the average amount of time they wait. They fixate on those times when the elevator took FOREVER, the p90 case.
I would always get a chuckle out of seeing some poor soul waiting 3 hours to go down a few floors after work, only because I failed to add stairs to the lobby.
I wish there were more games like this. It’s such a simple premise but so satisfyingly difficult after each level. And it even has a bit of randomish failure which makes for even more challenge.
If you buy the adorable monochrome console called the "Playdate" https://play.date it comes with a bunch of games included, including a cute elevator game where you help penguins to different floors while controlling the elevators yourself using the crank:
https://play.date/games/flipper-lifter/
That's the guy who created Infiniminer, which was essentially 3D multiplayer Motherlode (a game everyone was playing at school lunch and I never figured out why) and inspired Minecraft.
Wow, I just came here to comment that I've always wondered if a game where you have to program an elevator scheduler would be any fun. I thought surely no-one's thought to make that before, too! Glad to be proven wrong.
This seems like very cool work. I'm sorry if I missed it: I'm still not sure how we go from verified proof (Great!) to an implementation (by LLM or by Human) which you're sure actually conforms to the proof? How do we know that the implementation maps precisely to the description within the proof?
Both the implementation and the proof are written in Lean.
In the files I reference here https://github.com/schildep/verified-3d-mesh-intersection#mi...
there are theorems about the function that does the mesh intersection computation.
The implementation is in the CSG/Impl folder. The proof is in the CSG/Proof folder. They are imported and tied together in the human reviewed file. Lean checks that these theorems in the human reviewed file are proven via the proofs.
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 the microprocessor works according to its spec, and I don't think we have anything public about modern multi core processors about that.
Still, this is not a bad situation overall. If you are forced to trust the C compiler to correctly compile C, and the hardware to correctly implement the instructions in the documentation, well, you're already forced to trust both of those every day.
So this doesn't give you an absolute proof of correctness. But it does substantially reduce the size of the problem, which is now limited to (1) verifying that you actually proved what you think you did, and (2) all the stuff you were normally trusting anyway. (Some of the stuff you were trust anyway is broken, of course.) But this is a smaller problem than trusting 1,000 lines of highly-optimized CSG code written by a model we don't actually understand.
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 under worst-case conditions.
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.
I haven't actually used Lean or other proof assistants, so take this with a grain of salt, but I think the basic idea is to use (complicated) function argument and return types to "encode" the spec, and rely on the compiler's typechecking to detect spec violations.
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.
I view the temperature issue almost entirely as a copper problem. Every interface where you use CATx cables will have this issue; It's always extremely hot. For 10Gbps+ SFP and faster fiber is always the answer because those have very little thermal issues. The "only" issue is very few residential places have fiber cabling etc.
Friend shared this site with me like 10+ years ago, I've been using this knot ever since. Kind of amazing it's so generally unknown given how good it is.
Great job. I have spent a lot of time working on fluid simulations (I still am). Glad to see more people still mesmerized. If you’re interested, this rabbit hole goes very deep.
I mean if you're writing a ray tracer and the reflected light has more intensity than the light sources, then that's not desired. You can have the same sort of thing going on with a fluid simulation.
One of the nice aspects of Stable Fluids is that you don't need to iterate the pressure correction terms to convergence. Just run a fixed number of Jacobi or Gauss-Seidel sweeps and keep performance consistent. The only drawback of this is some mass loss in areas, which for the present purposes is acceptable.
I should add that this is a major "tell" for detecting when an app uses the Stable Fluids method: obvious mass loss (and very viscous, energy-dissipating flow).
Sure, but conservation in ray tracing is also a goal that not everyone has and isn’t required for teaching or games or making pretty & even plausible images. There are plenty of situations in both ray tracing and fluid simulation where conservation is not desirable.
Having written a slightly more involved version of this recently myself I think you did a great job of keeping this compact while still readable. This style of library requires some design for sure.
Supporting higher order derivatives was also something I considered, but it’s basically never needed in production models from what I’ve seen.
The reason I’m finding this is much faster than a traditional decomp is that while it’d be nice for the bytes to match, finding the perfect blend of compiler version, compiler args, permitting variables etc to try and find the perfect register assignments, etc is all very time consuming. My ultimate goal is not a byte for byte match, that’s just one way to ensure correctness. I’ve found agents are much faster and effective at reading the original assembly and understanding what’s going on then writing semantically equivalent C.
reply