[Merged by Bors] - fix: Data/Bitvec change definition of ofInt to the ring homomorphism

[ChrisHughes24]

---

After discussion with colleagues, we agreed that this was probably the more usual definition of ofInt.

[semorrison]

Sorry this has been sitting here unreviewed. I can't really tell why this change is being made. Perhaps you could incorporate more of that discussion into comments?

(But please, other reviewers, don't let my ignorance get in the way if you're inclined to merge.)

[tobiasgrosser]

Thank you @semorrison. As part of our effort to model compiler IRs as they arise in LLVM and MLIR, @bollu, @goens, and @ChrisHughes24 started to model bit-vector arithmetic. Aiming to contribute to the lean community where sensible, we want to explore in which way our requirements are compatible with mathlib. Truncating to the least significant bits (instead of preserving the sign but) is what programming languages typically do and also matches our own modeling efforts for LLVM/MLIR as well as the lean-smt people. We once again discussed this internally and feel this is a genuine correction to mathlib and the old code just required this correction.

Some CS details: in our work we obtained peephole rewrite test cases from the Alive project that are generic over the bitwidth and contain constants such as 1. Even though the value 1 is a common constant in many test cases, it is not in the set of values represented by a 1-bit vector when interpreted as 2's complement, which is just {0, -1}. Hence, we need to convert the bitwidth-generic value 1 into a 1-bit value. The new implementation that this PR introduces coincides with the conversion LLVM/MLIR chose for the very reason that it is more convenient for mathematicians, as it increases consistency across different bitwidths.

[digama0]

The new definition is definitely more sensible than the old one.

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style

[tobiasgrosser]

Thank you @digama0