49b77e3b45
## Alive2 proofs | Reduction | Shift | Cmp | Sources | Proof | |-----------|-------|----------|---------|-------| | add | lshr | == 0 | 2 | [proof](https://alive2.llvm.org/ce/z/f44vco) | | add | lshr | == 8 | 2 | [proof](https://alive2.llvm.org/ce/z/Ks_nea) | | add | ashr | == 0 | 2 | [proof](https://alive2.llvm.org/ce/z/ZsXJ5k) | | add | ashr | == -8 | 2 | [proof](https://alive2.llvm.org/ce/z/HZfans) | | add | lshr | == 0 | 3 | [proof](https://alive2.llvm.org/ce/z/x-dEdz) | | add | lshr | == 12 | 3 | [proof](https://alive2.llvm.org/ce/z/sfNvhr) | These proofs are not very exhaustive, but somewhat show that it works for addition. Apart from the fact that we use multiple vectors, the proofs from the previous changes generally apply here as well because we effectively match on reductions of size M x N.