CBMC: Add proofs for native backend functions#768

Merged

mkannwischer merged 13 commits intomainfrom

Dec 12, 2025

Commits on Dec 12, 2025

CBMC: Add proofs on top of native functions (poly_ntt_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions (poly_invntt_tomont_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions (rej_uniform_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions (rej_eta_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions (poly_decompose_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions (mld_poly_caddq_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions (poly_use_hint_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions (poly_chknorm_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions (polyz_unpack_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions (mld_poly_pointwise_montgomery_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions(polyvecl_pointwise_acc_montgomery_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions (keccakf1600_permute_native)

willieyz
authored and
mkannwischer
committed
CBMC: Add proofs on top of native functions (keccakf1600x4_permute_native)

willieyz
authored and
mkannwischer
committed