What's "wrong" with matching decompilation as an oracle for provably correct source code for a given binary?
Also, my decompilation project's goal was a remaster in the spirit of REDRIVER2, with bugfixes, new features, quality of life improvements and a PC port. The end result would not have been matching or even functionally equivalent anyways.