Spec math mode #3014

This MR implements the spec math modes discussed in a recent KaKeY meeting. See here for a reference. Furthermore, safe math is implemented using the wd checker, this mode generates additional in bounds checks when doing a wd proof and is otherwise treated like the bigint mode.

The code overflow behaviour remains unchanged and is to be overhauled in a later MR. This MR only includes the changes to specification translation.

Tests do exists here. All other tests are green and only minor changes to the specification of the existing examples were necessary.

@unp1 @mulbrich