Principled Rewriting of ONNX Operators for Reluctant Solvers