Port: Hoist default C backend into separate functions

[willieyz]

• Resolves: Port: Hoist default C backend into separate functions #732

• Purpose: This porting aims to separate the native backend functions into two distinct sets:

  • Fallback C backend functions
  • Native backend functions
    This work is based on the runtime-dispatch changes introduced in PR #607.

• Steps:

  • For each function improved by runtime dispatch in PR #607.:
    • Separate a additional fallback C backend function from the original implementation.
    • Add a CBMC proof for the C backend function.
    • Update the existing original implementation's CBMC USE_FUNCTION_CONTRACTS with the C backend function.

• Tests:

  • Run all test scripts with all argument variations under both static ON and static OFF configurations.
  • Run all examples: tests examples.
  • Run all relevant CBMC proofs for each modified or newly added function.

• The following is the checking table for fallback C backend and native backend:

Original	Native	C backend
mld_poly_ntt	mld_ntt_native	mld_poly_ntt_c
mld_poly_invntt_tomont	mld_intt_native	mld_poly_invntt_tomont_c
mld_polymat_permute_bitrev_to_custom	mld_poly_permute_bitrev_to_custom	((void)mat); /* Nothing to do */
mld_rej_uniform	mld_rej_uniform_native	mld_rej_uniform_c
mld_rej_eta	mld_rej_uniform_eta2_native mld_rej_uniform_eta4_native	mld_rej_eta_c
mld_poly_decompose	mld_poly_decompose_32_native mld_poly_decompose_88_native	mld_poly_decompose_c
mld_poly_caddq	mld_poly_caddq_native	mld_poly_caddq_c
mld_poly_use_hint	mld_poly_use_hint_32_native mld_poly_use_hint_88_native	mld_poly_use_hint_c
mld_poly_chknorm	mld_poly_chknorm_native	mld_poly_chknorm_c
mld_polyz_unpack	mld_polyz_unpack_17_native mld_polyz_unpack_19_native	mld_polyz_unpack_c
mld_poly_pointwise_montgomery	mld_poly_pointwise_montgomery_native	mld_poly_pointwise_montgomery_c
mld_polyvecl_pointwise_acc_montgomery	mld_polyvecl_pointwise_acc_montgomery_l4_native mld_polyvecl_pointwise_acc_montgomery_l5_native mld_polyvecl_pointwise_acc_montgomery_l7_native	mld_polyvecl_pointwise_acc_montgomery_c
mld_keccakf1600_permute	mld_keccak_f1600_x1_native	mld_keccakf1600_permute_c
mld_keccakf1600x4_permute	mld_keccak_f1600_x2_v84a_asm * 2 mld_keccak_f1600_x4_scalar_v8a_hybrid_asm mld_keccak_f1600_x4_scalar_v8a_v84a_hybrid_asm	mld_keccakf1600_permute * 4

[mkannwischer]

Thanks @willieyz. This looks very good!
Two small comments.

[mkannwischer]

Thanks @willieyz. This looks excellent!
I only found one extra new line that you could still remove.

[mkannwischer]

Thanks for the changes @willieyz. LGTM.

@hanno-becker, WDYT?

[hanno-becker]

This cast business is not very nice. I wonder if we should modify the native API to streamline this. Not an issue for this PR.

[mkannwischer]

mlkem-native has

    ret = mlk_polyvec_basemul_acc_montgomery_cached_k2_native(
        r->coeffs, (const int16_t *)a, (const int16_t *)b,
        (const int16_t *)b_cache);

Is that better?

[hanno-becker]

LGTM, thank you @willieyz !