https://github.com/pq-code-package/mlkem-native/pull/1634 extended the HOL-Light tooling to make it easier to run proofs cross-platform. Task: - Add a job to CI that tests this new feature aarch64->x86_64 and x86_64->aarch64 using one of the cheap HOL-Light proofs.
#1634 extended the HOL-Light tooling to make it easier to run proofs cross-platform.
Task: