Skip to content

native: Unify asm backend symbol naming #1663

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.

Sign up for GitHub

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

Merged
mkannwischer merged 5 commits into from
Apr 24, 2026
Merged

native: Unify asm backend symbol naming #1663

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
9bf9fcf
bench: call _native wrappers instead of raw _asm
mkannwischer Apr 23, 2026
181a465
native: Unify asm backend symbol naming
mkannwischer Apr 23, 2026
101f214
hol_light: Unify asm and proof filenames with exported symbols
mkannwischer Apr 23, 2026
ee72a51
bench: Gate native component bench per-function and cover full native…
mkannwischer Apr 23, 2026
295530e
CI: Disable RISE riscv runner (apt install failing)
mkannwischer Apr 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 6 additions & 4 deletions .github/workflows/base.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,9 +34,10 @@ jobs:
name: 'aarch64'
- runner: ubuntu-latest
name: 'x86_64'
# TODO: RISE riscv runner currently fails during apt install — re-enable once fixed.
# via https://riseproject-dev.github.io/riscv-runner/
- runner: ubuntu-24.04-riscv
name: 'riscv'
# - runner: ubuntu-24.04-riscv
# name: 'riscv'
- runner: macos-latest
name: 'macos (aarch64)'
- runner: macos-15-intel
Expand Down Expand Up @@ -71,9 +72,10 @@ jobs:
name: 'aarch64'
- runner: ubuntu-latest
name: 'x86_64'
# TODO: RISE riscv runner currently fails during apt install — re-enable once fixed.
# via https://riseproject-dev.github.io/riscv-runner/
- runner: ubuntu-24.04-riscv
name: 'riscv'
# - runner: ubuntu-24.04-riscv
# name: 'riscv'
acvp-version: [v1.1.0.39, v1.1.0.40, v1.1.0.41]
exclude:
- {external: true,
Expand Down
80 changes: 40 additions & 40 deletions .github/workflows/hol_light.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,44 +70,44 @@ jobs:
gh_token: ${{ secrets.GITHUB_TOKEN }}
nix-shell: 'hol_light'
script: |
make -C proofs/hol_light/aarch64 mlkem/mlkem_poly_tobytes.o
echo 'needs "aarch64/proofs/mlkem_poly_tobytes.ml";;' | hol.sh
make -C proofs/hol_light/aarch64 mlkem/poly_tobytes_aarch64_asm.o
echo 'needs "aarch64/proofs/poly_tobytes_aarch64_asm.ml";;' | hol.sh
hol_light_proofs:
needs: [ hol_light_bytecode ]
strategy:
fail-fast: false
matrix:
proof:
# Dependencies on {name}.{S,ml} are implicit
- name: mlkem_ntt
- name: ntt_aarch64_asm
needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
- name: mlkem_intt
- name: intt_aarch64_asm
needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
- name: mlkem_poly_tomont
- name: poly_tomont_aarch64_asm
needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
- name: mlkem_poly_mulcache_compute
- name: poly_mulcache_compute_aarch64_asm
needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_zetas.ml"]
- name: mlkem_poly_reduce
- name: poly_reduce_aarch64_asm
needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
- name: mlkem_poly_basemul_acc_montgomery_cached_k2
- name: polyvec_basemul_acc_montgomery_cached_k2_aarch64_asm
needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
- name: mlkem_poly_basemul_acc_montgomery_cached_k3
- name: polyvec_basemul_acc_montgomery_cached_k3_aarch64_asm
needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
- name: mlkem_poly_basemul_acc_montgomery_cached_k4
- name: polyvec_basemul_acc_montgomery_cached_k4_aarch64_asm
needs: ["mlkem_specs.ml", "mlkem_utils.ml"]
- name: mlkem_poly_tobytes
- name: poly_tobytes_aarch64_asm
needs: ["mlkem_specs.ml", "mlkem_utils.ml" ]
- name: mlkem_rej_uniform
- name: rej_uniform_aarch64_asm
needs: ["mlkem_specs.ml", "mlkem_utils.ml", "mlkem_rej_uniform_table.ml"]
- name: keccak_f1600_x1_scalar
- name: keccak_f1600_x1_scalar_aarch64_asm
needs: ["keccak_specs.ml"]
- name: keccak_f1600_x1_v84a
- name: keccak_f1600_x1_v84a_aarch64_asm
needs: ["keccak_specs.ml"]
- name: keccak_f1600_x2_v84a
- name: keccak_f1600_x2_v84a_aarch64_asm
needs: ["keccak_specs.ml"]
- name: keccak_f1600_x4_v8a_v84a_scalar
- name: keccak_f1600_x4_v8a_v84a_scalar_hybrid_aarch64_asm
needs: ["keccak_specs.ml"]
- name: keccak_f1600_x4_v8a_scalar
- name: keccak_f1600_x4_v8a_scalar_hybrid_aarch64_asm
needs: ["keccak_specs.ml"]
name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S
runs-on: pqcp-arm64
Expand Down Expand Up @@ -178,56 +178,56 @@ jobs:
gh_token: ${{ secrets.GITHUB_TOKEN }}
nix-shell: 'hol_light'
script: |
make -C proofs/hol_light/x86_64 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o
echo 'needs "x86_64/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml";;' | hol.sh
make -C proofs/hol_light/x86_64 mlkem/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.o
echo 'needs "x86_64/proofs/polyvec_basemul_acc_montgomery_cached_k2_avx2_asm.ml";;' | hol.sh
hol_light_proofs_x86_64:
needs: [ hol_light_bytecode_x86_64 ]
strategy:
fail-fast: false
matrix:
proof:
# Dependencies on {name}.{S,ml} are implicit
- name: mlkem_ntt
- name: ntt_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_zetas.ml"]
- name: mlkem_intt
- name: intt_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_zetas.ml"]
- name: mlkem_poly_basemul_acc_montgomery_cached_k2
- name: polyvec_basemul_acc_montgomery_cached_k2_avx2_asm
needs: ["mlkem_specs.ml"]
- name: mlkem_poly_basemul_acc_montgomery_cached_k3
- name: polyvec_basemul_acc_montgomery_cached_k3_avx2_asm
needs: ["mlkem_specs.ml"]
- name: mlkem_poly_basemul_acc_montgomery_cached_k4
- name: polyvec_basemul_acc_montgomery_cached_k4_avx2_asm
needs: ["mlkem_specs.ml"]
- name: mlkem_reduce
- name: reduce_avx2_asm
needs: ["mlkem_specs.ml"]
- name: mlkem_tobytes
- name: ntttobytes_avx2_asm
needs: ["mlkem_specs.ml"]
- name: mlkem_rej_uniform
- name: rej_uniform_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_rej_uniform_table.ml"]
- name: mlkem_frombytes
- name: nttfrombytes_avx2_asm
needs: ["mlkem_specs.ml"]
- name: mlkem_tomont
- name: tomont_avx2_asm
needs: ["mlkem_specs.ml"]
- name: mlkem_unpack
- name: nttunpack_avx2_asm
needs: ["mlkem_specs.ml"]
- name: mlkem_mulcache_compute
- name: poly_mulcache_compute_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_zetas.ml"]
- name: mlkem_poly_compress_d4
- name: poly_compress_d4_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
- name: mlkem_poly_decompress_d4
- name: poly_decompress_d4_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
- name: mlkem_poly_compress_d5
- name: poly_compress_d5_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
- name: mlkem_poly_decompress_d5
- name: poly_decompress_d5_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
- name: mlkem_poly_compress_d10
- name: poly_compress_d10_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
- name: mlkem_poly_decompress_d10
- name: poly_decompress_d10_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
- name: mlkem_poly_compress_d11
- name: poly_compress_d11_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
- name: mlkem_poly_decompress_d11
- name: poly_decompress_d11_avx2_asm
needs: ["mlkem_specs.ml", "mlkem_compress_consts.ml"]
- name: keccak_f1600_x4_avx2
- name: keccak_f1600_x4_avx2_asm
needs: ["keccak_utils.ml", "keccak_spec.ml", "keccak_f1600_x4_avx2_constants.ml", "keccak_constants.ml"]
name: x86_64 HOL Light proof for ${{ matrix.proof.name }}.S
runs-on: pqcp-x64
Expand Down
Loading
Loading