Overflow checking #3027

This is a follow up to #3014.

This MR implements overflow checking of all arithmetic operations in code by opening a new goal where the absence of overflows has to be proven.

Furthermore, it deduplicates and rearranges a lot of rules.

There are some todos where I was unsure, if you know an answer to any of them please add a comment.