Hacker News Reader

Comment by j2kun | Hacker News Reader

Functional equivalence here, of course, depends on the completeness of the test suite, where byte-identical compiled artifacts does not.

(For example, your approach would not necessarily catch all the same overflow behaviors; the OP expressly claimed that "replicating all bugs" was also important, and many bugs are caused by certain overflow behaviors)

View on HN

> catch all the same overflow behaviors

So you're looking not just for functional but also dysfunctional equivalence %)

no, thats still functional here. the bugs have to be the same, such that speed runs could still run correctly

I'm going to start using that term :)

Byte exact seems only of interest to preserve known bugs etc for cheats/shortcuts/etc.

That may be true, but I hate it when people repeat the false idea that functional equivalence requires only a test suite that has full branch/line coverage. Call me triggered :)

That said, I would probably follow this same approach if I were to do this, but with extensive randomized testing as well.

You can do the process in stages. Do the first decompilation mechanically (no LLM), use a SMT solver to show it builds to an equivalent binary to the original, and then use LLM to clean up the code into something idiomatic with the benefit of a correct binary built with the new toolchain. This helps when you want to port across languages or toolchains, and helps protect against toolchain bugs.

In my project I've been practicing a similar loop as you describe: an agent writes code, SMT solver checks against a spec. A few things I observed:

1. Solver is great at the bugs tests miss (overflow, off-by-one, empty inputs...), its output can be used by the agent to fix it.

2. Solver struggles where you'd assume: loops, non-linear arithmetic and pointer aliasing blow up solve time, floating point is painful.

So your step 2 would cover some of it well, but since the game code is a lot of floating point, SMT would probably have a hard time (get stuck/timeout).

It depends, the way I set the problem up I define equivalence as Z3 finds a solution within an rlimit of 8M, anything that fails gets machinery added to subdivide or reduce the problem (e.g. assume an index is in the bounds of the buffer it's associated with and add a bounds check). Floating point will in many cases require software emulation but I think that's unavoidable. That might be less of an issue if source and destination are both fairly conformant to IEEE 754 and use modern sizes.

For anything with recorded replays or multiplayer you need to preserve known and unknown bugs for compatibility reasons, not just for cheating.

Or a speedrunning community

Reply on news.ycombinator.com