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

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.