Skip to content

Add aarch64 constant-time (f_events) proof for rej_uniform_eta2 - #1389

Closed
jakemas wants to merge 1 commit into
pq-code-package:mainfrom
jakemas:rej-uniform-eta2-ct-fevents
Closed

Add aarch64 constant-time (f_events) proof for rej_uniform_eta2#1389
jakemas wants to merge 1 commit into
pq-code-package:mainfrom
jakemas:rej-uniform-eta2-ct-fevents

Conversation

@jakemas

@jakemas jakemas commented Aug 18, 2026

Copy link
Copy Markdown
Contributor

Resolves #1160

eta4 in progress, will add to this PR

Signed-off-by: Jake Massimo <jakemas@amazon.com>
@jakemas

jakemas commented Aug 18, 2026

Copy link
Copy Markdown
Contributor Author

Superseded by #1390, branched from the upstream repo so full CI (incl. HOL-Light) runs.

@jakemas jakemas closed this Aug 18, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

HOL-Light: prove secret-independence for rej_uniform_eta{2,4}

1 participant