CBMC: Refine bounds for input and output of base multiplication#906

Draft

hanno-becker wants to merge 9 commits intomainfrom

Commits on Oct 13, 2025

Switch mlk_polyvec and mlk_polymat to struct wrappers

hanno-becker
authored and
rod-chapman
committed
CBMC: Refine bounds for input and output of base multiplication

hanno-becker
authored and
rod-chapman
committed
Use --arrays-uf-always here to improve proof speed.
rod-chapman
committed
Fix merge conflicts and complete rebase again main branch.
rod-chapman
committed
Use C90 comments /* */ not C99 // style.
rod-chapman
committed
Update component testing code for new type signatures.
rod-chapman
committed
Re-generate auto-generated files to meet lint requirements.
rod-chapman
committed
Update post-condition on native implementions of
rod-chapman
committed
Update master copies of AArch64 arithmetic back-end specs.
rod-chapman
committed