HOL-Light/x86: Add output bound to specification of mulcache_compute #1440
Description
The HOL-Light specification of mulcache_compute is missing the absolute output bound MLKEM_Q in its spec, making it to weak for the frontend.
{{ message }}
The HOL-Light specification of mulcache_compute is missing the absolute output bound MLKEM_Q in its spec, making it to weak for the frontend.