google/heir

Investigate if/how "Verifying Peephole Rewriting In SSA Compiler IRs" can be used in HEIR

Opened this issue · 1 comments

AlexanderViand-Intel commented

As some of you might be aware a group of researchers around Prof. Tobias Grosser from the University of Edinburgh/Cambridge University have been using (an earlier version of) our polynomial dialect as an example for their work on verifying MLIR in LEAN .

I'm happy to report that their paper1 has been accepted at ITP 2024 and is now available: https://doi.org/10.4230/LIPIcs.ITP.2024.9 or https://arxiv.org/abs/2407.03685 🎉

While this is already a cool result in itself, the natural question would be to see if we can somehow make use of this in HEIR (or MLIR, if it concerns up streamed polynomial things). For example, I wonder if something like this could have helped us catch #749 and/or might be useful as we go into more advanced modular arithmetic optimizations and transitions between poly and mod arith. The paper also implements reasoning about bit vectors, so there's a good chance it could capture such lowerings/rewrites.

Footnotes

  1. Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, and Tobias Grosser.
    Verifying Peephole Rewriting in SSA Compiler IRs.
    In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
    https://doi.org/10.4230/LIPIcs.ITP.2024.9 ↩

AlexanderViand-Intel commented

Adding examples of issues/bugs that motivate why formal verification might be interesting for polynomial->arith lowerings:

  • PR #731 needed some fixing before merging, because I was not aware of arith restrictions on remui/remsi, meaning that we cannot fit, e.g., numbers modulo $2^{31}-1$ into i31 (artificial example) and need an extra bit to ensure things work as expected when lowered to LLVM.
  • PR #928 fixes an issue where "the current implementation would have incorrect behaviour if the arith.sub resulted in a negative signed number that was then interpreted as an unsigned int with arith.remui" which "is fixed by adding the modulus to the result before applying remui such that the range after sub shifts from (-mod, mod) -> [0, mod)"
  • Issue #990 is another example of pre-‘mod_artih’ code not correctly handling lowering modular arithmetic to ‘arith’
  • PR #998 fixes an issue with bit-widths not being correct for reduce (technically during the review of PR #927 this was already noticed, but the fixes didn't make it in there, exposing this bug)
  • ❤️2