x86_64: Replace rej_uniform_eta2/eta4 intrinsics with hand-written assembly#1187
Closed
jakemas wants to merge 1 commit into
Closed
x86_64: Replace rej_uniform_eta2/eta4 intrinsics with hand-written assembly#1187jakemas wants to merge 1 commit into
jakemas wants to merge 1 commit into
Conversation
…sembly Add hand-written x86_64 AVX2 assembly for rej_uniform_eta2 and rej_uniform_eta4, following the rej_uniform approach in pq-code-package#1014: the table is passed as a parameter and all constants are built from immediates (no .rodata), enabling future HOL-Light verification. Wire eta4 to the new asm in meta.h, add the asm entry points and contracts in arith_native_x86_64.h, register the bytecode dump targets in autogen and the Makefile, and add a poly_uniform_eta_4x component benchmark. Signed-off-by: jake massimo <jakemas@amazon.com>
Contributor
Author
|
Superseded by a branch pushed directly to the upstream repo so CI runs (fork PRs skip the self-hosted/EC2 test+bench jobs). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Draft — opened while the HOL-Light proofs are still in progress.
Replaces the AVX2 intrinsics implementations of
rej_uniform_eta2andrej_uniform_eta4with hand-written x86_64 assembly, following the same approach as #1014:.rodata), enabling future HOL-Light formal verification.__contract__annotations on the asm entry points (CBMC), to be kept in sync with the HOL-Light specs.scripts/autogenand the x86_64 HOL-LightMakefileregister the eta2/eta4 bytecode dump targets.poly_uniform_eta_4xcomponent benchmark.Scope of this draft
This draft contains assembly + build/bytecode infrastructure only. It intentionally excludes the HOL-Light
.mlproofs, which are still being developed. The proofs will be added before this is marked ready for review.Notes / TODO before ready-for-review
meta.hcurrently wires only eta4 to the new asm; eta2 asm is in place butmld_rej_uniform_eta2_nativestill calls the intrinsic — wire it once verified.