CBMC: Add proofs for native backend functions

[willieyz]

• Related CBMC: Add proofs atop of native functions #350

• This commit adds CBMC proofs for 14 native backend functions across arithmetic and FIPS-202 operations:
  Arithmetic Backend:

CBMC Proof	Native Functions
poly_ntt_native	mld_ntt_native
poly_invntt_tomont_native	mld_intt_native
Skip	mld_poly_permute_bitrev_to_custom
rej_uniform_native	mld_rej_uniform_native
rej_eta_native	mld_rej_uniform_eta2_native mld_rej_uniform_eta4_native
poly_decompose_native	mld_poly_decompose_32_native mld_poly_decompose_88_native
poly_caddq_native	mld_poly_caddq_native
poly_use_hint_native	mld_poly_use_hint_32_native mld_poly_use_hint_88_native
poly_chknorm_native	mld_poly_chknorm_native
polyz_unpack_native	mld_polyz_unpack_17_native mld_polyz_unpack_19_native
poly_pointwise_montgomery_native	mld_poly_pointwise_montgomery_native
polyvecl_pointwise_acc_montgomery_native	mld_polyvecl_pointwise_acc_montgomery_l4_native mld_polyvecl_pointwise_acc_montgomery_l5_native mld_polyvecl_pointwise_acc_montgomery_l7_native
keccakf1600_permute_native	mld_keccak_f1600_x1_native
keccakf1600x4_permute_native	mld_keccak_f1600_x4_native

• This PR adds CBMC proofs for all native backend functions except one. We temporarily skip mld_poly_permute_bitrev_to_custom because its proof times out during CBMC ML-DSA-44 checking. Have already asked for help from @mkannwischer and @rod-chapman, and we will open a separate pull request: #770 , to address this issue.

• Each proof reuses the harness and add contracts that reference from the corresponding C implementation, verifying that native backends satisfy the same specifications. Proofs use a corresponding mock backend (dummy_backend.h, dummy_backend_fips202_x1, dummy_backend_fips202_x4).

• This PR made follwoing changes

  • Added proof harnesses and Makefiles in proofs/cbmc/ for all native functions
  • Introduced array_unchanged contract pattern in cbmc.h for fallback verification
  • Added MLD_NTT_BOUND and MLD_INTT_BOUND constant in api.h.
  • Refactored mld_polymat_permute_bitrev_to_custom from double to single loop for proof tractability

• Test steps:

  • make clean & MLD_CONFIG_PARAMETER_SET=44/65/87 make result checking the contract itself.
  • tests cbmc -p "parrent_proof", this will check the parrent proof, for examples: tests cbmc -p poly_ntt will check poly_ntt, poly_ntt_c, poly_ntt_native with 3 security level.

| Status  | Count |
|---------|-------|
| Success | 3     |

| Proof           | Status  | Duration (in s) |
|-----------------|---------|-----------------|
| poly_ntt        | Success | 3               |
| poly_ntt_c      | Success | 2               |
| poly_ntt_native | Success | 3               |

[mkannwischer]

Thanks @willieyz for this PR.

Since the CBMC proof for polymat_permute_bitrev_to_custom_native is blowing up for ML-DSA-44, could you move just that to a new PR so we can investigate there?
Then we can already review+merge all the other commits.

[mkannwischer]

Thanks @willieyz. Looking fairly good. Here are some comments what still needs to be adjusted. The decompose contracts are wrong and are a serious soundness issue - the other comments are minor.

The contract for mld_poly_chknorm_native is rather ugly - we should consider simplifying that vastly, but that can be a follow up.

Please remove the TODOs also for mld_poly_use_hint_88_native and mld_poly_use_hint_32_native.

[willieyz]

Thanks @willieyz. Looking fairly good. Here are some comments what still needs to be adjusted. The decompose contracts are wrong and are a serious soundness issue - the other comments are minor.

The contract for mld_poly_chknorm_native is rather ugly - we should consider simplifying that vastly, but that can be a follow up.

Please remove the TODOs also for mld_poly_use_hint_88_native and mld_poly_use_hint_32_native.

Hello, @mkannwischer , thank you for your review!
I had fixed all issue according to your comment, also ,I will create a issue #773 following up the mld_poly_chknorm_native contract refactor problem,
Thank you for helping me improve this PR, thanks!

[mkannwischer]

Thanks for the changes @willieyz - I just rechecked everything. LGTM now.

@hanno-becker, could you also take a look please?

[rod-chapman]

News: CBMC team have proposed a fix for CBMC that helps with this issue. This is currently on a branch of the CBMC repo awaiting review.

For mldsa-native, I still have to re-structure the code of polymat_permite_bitrev_to_custom() to use a nested loop, so that the code structure matches the data structure.

With that change, AND the new CBMC, the proofs looks OK.

I have the code change - shall I commit and push it here?

[mkannwischer]

News: CBMC team have proposed a fix for CBMC that helps with this issue. This is currently on a branch of the CBMC repo awaiting review.

For mldsa-native, I still have to re-structure the code of polymat_permite_bitrev_to_custom() to use a nested loop, so that the code structure matches the data structure.

With that change, AND the new CBMC, the proofs looks OK.

I have the code change - shall I commit and push it here?

Awesome news. Thanks @rod-chapman for following up.
Please experiment in #770. Once everything works fine we can pull it over here.

[rod-chapman]

I have pushed the refactored polymat_permute_bitrev_to_custom() on the cbmc-native2 branch on PR#770. With the new wavefront of CBMC, proofs go through OK. I will push CBMC team to prioritize review and a new tagged release.