Make the `ref` implementation accepted by the safety checker

[vbgl]

The changes in this PR and the changes to the safety checker enabling annotations (https://github.com/jasmin-lang/jasmin/pull/362) make the safety analysis of the keypair function go through.

Quick measurements show that these changes have no impact on the run-time performance (this REF version is already quite slow).

I’ve no clue about what impact they may have about the correctness proofs.

[vbgl]

I may have a different workaround for NTT: tweak the safety checker (https://github.com/jasmin-lang/jasmin/pull/384) rather than changing the analyzed program.

[vbgl]

With small fixes & improvements to the safety checker (https://github.com/jasmin-lang/jasmin/pull/384, https://github.com/jasmin-lang/jasmin/pull/387), the three main entrypoints of the ref implementations can be verified for safety with the changes made in this PR:

• in gen-matrix , an early exit has been removed; this will impact the proof, but should be doable;
• in the same procedure, an array is now explicitly initialized; this increases the code size, but the run-time effect of this change should not be a concern;
• the rejection-sampling loop is annotated with #no_termination_check, meaning that it is not the duty of the automatic checker to prove termination (note that this loop almost surely terminates);
• a few loop guards are made tighter: this is a syntactic change that allows the widening heuristic to make better guesses;
• a few loops are annotated with #bounded, to tell the analyzer to unroll them: this is required for loops that initialize arrays.

Beware that safety analysis is costly. Witnesses report about 6h of computation for keypair and nearly 16h for decaps, encaps being somewhere in between.