Skip to content

Conversation

@willieyz
Copy link
Contributor

@willieyz willieyz commented Jan 9, 2026

Currently, mldsa-native already uses x86_64 as the architecture identifier for x86 in its existing HOL-Light proofs, and no changes are required in that regard. This commit simply aligns the surrounding scripts and infrastructure to consistently use x86_64 as the architecture name.

  • Adds the related scripts to support dual architectures by introducing an explicit arch parameter in the autogen process.

  • Replaces the arm_or_x86 flag with a unified arch flag in test scripts.

This commit ports the change from
pq-code-package/mlkem-native#1456
to mldsa-native.

Currently, mldsa-native already uses x86_64 as the architecture
identifier for x86 in its existing HOL-Light proofs, and no changes are
required in that regard. This commit simply aligns the surrounding
scripts and infrastructure to consistently use x86_64 as the
architecture name.

- Adds the related scripts to support dual architectures by introducing
  an explicit arch parameter in the autogen process.

- Replaces the arm_or_x86 flag with a unified arch flag in test scripts.

Signed-off-by: willieyz <[email protected]>
@willieyz willieyz force-pushed the consistent_arch_id branch from e111144 to f6e7b6f Compare January 9, 2026 07:25
@mkannwischer mkannwischer self-assigned this Jan 9, 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.

Port: Use consistent architecture identifier in autogen

3 participants