Add functional correctness proofs for AArch64-optimized NTT and invNTT in HOL Light#662

Merged

hanno-becker merged 6 commits intomainfrom hol_light

Jan 28, 2025

+2,410-2

Commits on Jan 28, 2025

nix: Package hol_light into a nix derivation

potsrevennil
authored and
hanno-becker
committed
nix: Package s2n_bignum into nix derivation

potsrevennil
authored and
hanno-becker
committed
remove tutorial targets for s2n-bignum Makefile

potsrevennil
authored and
hanno-becker
committed
move hol_light proof under the proofs folder

potsrevennil
authored and
hanno-becker
committed
CI: add job for simple hol_light check

potsrevennil
authored and
hanno-becker
committed
HOL-Light: Run NTT and invNTT proof in CI
hanno-becker
committed