Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 6 commits into from
Jan 28, 2025

HOL-Light: Run NTT and invNTT proof in CI

a1b8105
Select commit
Loading
Failed to load commit list.
Merged

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

HOL-Light: Run NTT and invNTT proof in CI
a1b8105
Select commit
Loading
Failed to load commit list.
DCO-2 / DCO succeeded Jan 28, 2025 in 1s

Check passed!

All commits are signed off, the check passed.

Summary


Sha Message Pass or fail reason
🟢 af3652b nix: Package hol_light into a nix derivation Valid sign-off found
🟢 2d795ad nix: Package s2n_bignum into nix derivation Valid sign-off found
🟢 876a48e remove tutorial targets for s2n-bignum Makefile Valid sign-off found
🟢 24cb962 move hol_light proof under the proofs folder Valid sign-off found
🟢 af94e22 CI: add job for simple hol_light check Valid sign-off found
🟢 a1b8105 HOL-Light: Run NTT and invNTT proof in CI Valid sign-off found