CBMC: Add proof and contract for mldsa_shake128_stream_init

[jakemas]

Resolves #141

[hanno-becker]

One unnecessary use of memory_no_alias in the preconditions.

[jakemas]

One unnecessary use of memory_no_alias in the preconditions.

I see, you are correct. When I remove this precondition I get an issue with CBMC overflow detection:

VERIFICATION FAILED

[MLD_65_ref_mldsa_shake128_stream_init.overflow.1] line 15 arithmetic overflow on unsigned to unsigned type conversion in (uint8_t)nonce: FAILURE

[hanno-becker]

@jakemas Yes, CBMC does not like implicit truncation. You need to explicitly mask: t[0] = nonce & 0xFF

Have a look at https://github.com/pq-code-package/mlkem-native/blob/main/mlkem/compress.c#L101 where the same thing happened during compression in mlkem-native.

[jakemas]

@jakemas Yes, CBMC does not like implicit truncation. You need to explicitly mask: t[0] = nonce & 0xFF

Have a look at https://github.com/pq-code-package/mlkem-native/blob/main/mlkem/compress.c#L101 where the same thing happened during compression in mlkem-native.

Got it! Thanks!

[hanno-becker]

Function arguments T foo[N] must be declared as T* foo in the harness, not as T foo[N]. Otherwise, the function will only be considered for valid foo, even if it does not have a precondition for foo.

@jakemas Can you please check existing harnesses to ensure we are not doing this elsewhere? We should never allocate an array in a harness.

[hanno-becker]

Thanks @jakemas!