CBMC: Consider combining `polyz_unpack_{17,19}_native_aarch64` into one proof

[mkannwischer]

There is no good reason to have those two proofs separate. We can combine them as was done for use_hint in #1037.

When native functions depend on the parameter set, we have different functions for each parameter set, e.g.,

polyz_unpack_17_native
polyz_unpack_19_native

When writing the CBMC proofs for those, there are two options:
A) The CBMC proof is specific to the parameter set and is skipped for other parameter set:

# polyz_unpack_17 is only used with ML-DSA-44
ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
CHECK_FUNCTION_CONTRACTS=mld_polyz_unpack_17_native
USE_FUNCTION_CONTRACTS = mld_polyz_unpack_17_asm
else
CHECK_FUNCTION_CONTRACTS=
USE_FUNCTION_CONTRACTS =
endif

B) The CBMC proof is for all parameter sets:

ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
    CHECK_FUNCTION_CONTRACTS=mld_polyvecl_pointwise_acc_montgomery_l4_native
    USE_FUNCTION_CONTRACTS=mld_polyvecl_pointwise_acc_montgomery_l4_asm
else ifeq ($(MLD_CONFIG_PARAMETER_SET),65)
    CHECK_FUNCTION_CONTRACTS=mld_polyvecl_pointwise_acc_montgomery_l5_native
    USE_FUNCTION_CONTRACTS=mld_polyvecl_pointwise_acc_montgomery_l5_asm
else ifeq ($(MLD_CONFIG_PARAMETER_SET),87)
    CHECK_FUNCTION_CONTRACTS=mld_polyvecl_pointwise_acc_montgomery_l7_native
    USE_FUNCTION_CONTRACTS=mld_polyvecl_pointwise_acc_montgomery_l7_asm
endif

Both approaches are currently used. I think we should pick one of the two and change the other proofs accordingly.

[jakemas]

Nice, I'm glad you liked this format!

[mkannwischer]

Thinking about this more, I think this needs more discussion.
The same would apply to the polyvec_basemul_acc_montgomery_cached_k{2,3,4}_native proofs in mlkem-native.

I think we should pick one of the two approaches and consolidate all proofs in mlkem-native and mldsa-native.

This has relatively low priority for me.