Institute infrastructure to formally verify correctness of suitable compiler passes in CI

[j2kun]

https://github.com/google/heir/issues/817 gave an initial exploration of the potential for formal verification of HEIR's low-level mod_arith canonicalization rules. We'd like to extend this to a more comprehensive and tightly integrated system. This PR outlines the work needed for that. We'd like to do this for mod_arith to start, and then move up the stack to polynomial and rns.

• Convert the dialects we'd like to formalize to irdl and the rules to pdll, which would enable automated extraction from HEIR/MLIR to lean-mlir. This will almost certainly require upstream improvements to both irdl and pdll to support missing features.
• Create CI infrastructure that understands when affected dialects/passes are changed, and installs and runs the lean-mlir infra in CI.
• Provide tutorials for contributors on how to work with the formal verification tooling outside of the CI, as well as debugging when verification fails.