HOL Light proofs infrastructure for x86 and basemul proof #1323
Conversation
dkostic
force-pushed
the
hol-x86-poly-basemul
branch
5 times, most recently
from
8155685 to
52cc0bd
Compare
Signed-off-by: Dusan Kostic <[email protected]>
dkostic
force-pushed
the
hol-x86-poly-basemul
branch
from
52cc0bd to
d32e305
Compare
hanno-becker
left a comment
hanno-becker
left a comment
There was a problem hiding this comment.
Looking really good @dkostic, thank you.
Could you clean up x86/proofs/mlkem_specs.ml? This has at least mentions of Arm and mldsa in it.
the reason it has mentions of Arm and ML-DSA is because I copied the whole script from s2n-bignum (https://github.com/awslabs/s2n-bignum/blob/main/common/mlkem_mldsa.ml). There, we tried to minimize duplication and consolidate all definitions and theorems that are common to ML-KEM and ML-DSA for x86 and Arm into a single file. I think we should follow the same approach here. We should aim to have a single mlkem_specs.ml file that can be shared between Arm and x86. I'd be fine with removing the ML-DSA parts but I think ideally we'd keep the file identical to the one in s2n-bignum. |
Signed-off-by: Dusan Kostic <[email protected]>
| if platform.machine().lower() in ["arm64", "aarch64"]: | ||
| arm_or_x86 = "arm" | ||
| elif platform.machine().lower() in ["x86_64"]: | ||
| arm_or_x86 = "x86" |
There was a problem hiding this comment.
We should allow cross-checking of proofs, but this can be a follow-up
There was a problem hiding this comment.
LGTM, many thanks @dkostic for the work. There are some follow-up issues we need to address, but they should not block the PR.
.github/workflows/hol_light.yml
Outdated
| # TODO: fix the interactive mode to work for both x86 and arm. | ||
| # hol_light_interactive_x86_64: | ||
| # name: HOL-Light interactive shell test | ||
| # runs-on: pqcp-x64 | ||
| # needs: [ hol_light_bytecode_x86_64 ] | ||
| # if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork | ||
| # steps: | ||
| # - uses: actions/checkout@08c6903cd8c0fde910a37f88322edcfb5dd907a8 # v5.0.0 | ||
| # with: | ||
| # fetch-depth: 0 | ||
| # - uses: ./.github/actions/setup-shell | ||
| # with: | ||
| # gh_token: ${{ secrets.GITHUB_TOKEN }} | ||
| # nix-shell: 'hol_light' | ||
| # script: | | ||
| # make -C proofs/hol_light/x86 mlkem/mlkem_poly_basemul_acc_montgomery_cached_k2.o | ||
| # echo 'needs "proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml";;' | hol.sh |
There was a problem hiding this comment.
What's the issue here?
| needs "arm/proofs/base.ml";; | ||
|
|
||
| needs "proofs/mlkem_specs.ml";; | ||
| needs "../common/mlkem_specs.ml";; |
There was a problem hiding this comment.
Why do we not need to prefix all object file paths below with arm resp. x86_64?
hanno-becker
left a comment
hanno-becker
left a comment
There was a problem hiding this comment.
Apologies, I got some late questions about relative file paths and why the CI disables the interactive x86 HOL-Light shell test (may be related).
Signed-off-by: Dusan Kostic <[email protected]>
Signed-off-by: Dusan Kostic <[email protected]>
dkostic
force-pushed
the
hol-x86-poly-basemul
branch
from
df0b7fa to
3cc281e
Compare
No description provided.