Verify shrtz

[klinashka]

This PR verifies beeu_shrtz. The function takes as input the following parameters:

• p_a : 256-bit unsigned integer.
• p_x : 320-bit unsigned integer.
• p_m : 256-bit unsigned integer, representing the modulus.
• inv_m: 64-bit unsigned integer, s.t. p_m * inv_m = -1 (mod 2^64)

The function updates p_a and p_x as follows:

• It removes at most 63 trailing zeros from p_a.
• It performs Montgomery division on p_x s.t. p_x_post = p_x_pre * 2^(-s) (mod M) , where s is the number of bits removed from p_a.

Additionally, we perform the following modifications in the PR.

• Slightly strengthen the specification of u320_muladd to include bounds on the carry word. The proof does not change.
• Remove an unused existential quantifier from u320_shr.
• Define and prove the specification for u256_shr. The specification closely resembles the one for u320_shr, without the additional carry that is taken as input in u320_shr. The proof is identical to the u320_shr counterpart.