Remove unused spec for mld_montgomery_reduce, add bounds reasoning

[hanno-becker]

Context:

We previously had two specifications for mld_montgomery_reduce:

• A 'weak' one where the output upper bound matches the input upper bound of mld_reduce32().
• A 'strong' one where the output interval is (-Q,Q), exclusively.

Both contracts were combined into one in a somewhat ad-hoc way (the 'weak' version being encoded as pre- and post-conditions as usual, the 'strong' version being stated as an implication in the post-condition).

The combined contract was used in the CBMC proofs of

• mld_poly_pointwise_montgomery
• mld_polyvecl_pointwise_acc_montgomery

There are two more functions which rely on mld_montgomery_reduce, namely

• mld_fqmul
• mld_fqscale

Observations:

• The 'weak' contract of mld_montgomery_reduce is not needed: In the context of mld_poly_pointwise_montgomery and mld_polyvecl_pointwise_acc_montgomery, the strong version applies.
• The 'strong' version also applies in the context of mld_fqmul and mld_fqscale.

Accordingly, this commit removes the 'weak' version and re-formulates the 'strong' version in traditional pre/post condition form.

The commit also removes the macro wrapper around the input bound, which I find difficult to read. It's easier to understand if the bound is explicit.

The 'strong' version only applies to mld_fqscale because of the recent modification of the iNTT output bound from 3/4*Q to Q. Otherwise, an even stronger spec would have been needed. At present, one can even remove mld_fqscale and just call mld_fqmul directly, but this commit does not do this.

The commit also takes the opportunity to add some pen-and-paper bounds reasoning for mld_montgomery_reduce.

• Resolves Reason about bounds of mld_fqmul and mld_fqscale #602

[mkannwischer]

Thanks @hanno-becker - very welcome simplification. How about we eliminate the larger bound from the documentation altogether?

[jammychiou1]

Thank you @hanno-becker for your work! Very useful result for me to reference from the asm bound comments :D

Only two nits remaining now. Please see the comments.

[jammychiou1]

LGTM. Thank you for your hard work Hanno!

[jakemas]

Thanks Hanno!