Skip to content

Commit

Permalink
Merge pull request #716 from pq-code-package/hol_light_mac
Browse files Browse the repository at this point in the history 
HOL-Light: Add support for MacOS
  • Loading branch information
@hanno-becker
hanno-becker authored Jan 29, 2025
2 parents 3dc9642 + dfb3166 commit 3da5027
Show file tree
Hide file tree
Showing 2 changed files with 26 additions and 0 deletions.
14 changes: 14 additions & 0 deletions proofs/hol_light/arm/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,11 +69,25 @@ OBJ = mlkem/mlkem_ntt.o mlkem/mlkem_intt.o
# According to
# https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms,
# x18 should not be used for Apple platforms. Check this using grep.
ifneq ($(OSTYPE_RESULT),Darwin)
$(OBJ): %.o : %.S
$(Q)[ -d $(@D) ] || mkdir -p $(@D)
cat $< | $(PREPROCESS) | $(SPLIT) | grep -v -E '^\s+.quad\s+0x[0-9a-f]+$$' | $(ASSEMBLE) -o $@ -
$(OBJDUMP) $@ | ( ( ! grep --ignore-case -E 'w18|[^0]x18' ) || ( rm $@ ; exit 1 ) )
cat $< | $(PREPROCESS) | $(SPLIT) | $(ASSEMBLE) -o $@ -
else
$(OBJ): %.o : %.S
@if ! (which gobjcopy >/dev/null); then \
echo "gobjcopy not found. Consider installing it via 'brew install binutils', and put its parent directory (typically `/opt/homebrew/opt/binutils/bin`) in your PATH.";\
exit 1; \
fi
$(Q)[ -d $(@D) ] || mkdir -p $(@D)
cat $< | $(PREPROCESS) | $(SPLIT) | grep -v -E '^\s+.quad\s+0x[0-9a-f]+$$' | $(ASSEMBLE) -o $@ -
$(OBJDUMP) $@ | ( ( ! grep --ignore-case -E 'w18|[^0]x18' ) || ( rm $@ ; exit 1 ) )
cat $< | $(PREPROCESS) | $(SPLIT) | $(ASSEMBLE) -o $@ -
# On Darwin, we need to explicitly convert Mach-O to ELF
gobjcopy -I mach-o-arm64 -O elf64-littleaarch64 $@ $@
endif

clean:; rm -f */*.o */*/*.o */*.correct */*.native

Expand Down
12 changes: 12 additions & 0 deletions proofs/hol_light/arm/README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,18 @@ make -C proofs/hol_light/arm

will build and run the proofs. Note that this make take hours even on powerful machines.

### macOS (AArch64)

If you want run the proofs from an AArch64 Apple machine, you need to manually install `gobjcopy` via

```
brew install binutils
```

and put its parent directory (typically `/opt/homebrew/opt/binutils/bin`) into your `PATH`.
This is needed to convert Mach-O object files to ELF (if you know a way to install a suitable version
of `objcopy` through `nix`, please let us know!).

## What is covered?

At present, this directory contains functional correctness proofs for the following functions:
Expand Down

18 comments on commit 3da5027

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Arm Cortex-A76 (Raspberry Pi 5) benchmarks

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 29045 cycles 29044 cycles 1.00
ML-KEM-512 encaps 34921 cycles 34919 cycles 1.00
ML-KEM-512 decaps 45433 cycles 45430 cycles 1.00
ML-KEM-768 keypair 49259 cycles 49260 cycles 1.00
ML-KEM-768 encaps 55568 cycles 55570 cycles 1.00
ML-KEM-768 decaps 70409 cycles 70407 cycles 1.00
ML-KEM-1024 keypair 71975 cycles 71976 cycles 1.00
ML-KEM-1024 encaps 80724 cycles 80729 cycles 1.00
ML-KEM-1024 decaps 100531 cycles 100536 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Intel Xeon 4th gen (c7i)

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 9315 cycles 9322 cycles 1.00
ML-KEM-512 encaps 10787 cycles 10791 cycles 1.00
ML-KEM-512 decaps 14961 cycles 14879 cycles 1.01
ML-KEM-768 keypair 16115 cycles 16110 cycles 1.00
ML-KEM-768 encaps 17332 cycles 17328 cycles 1.00
ML-KEM-768 decaps 22965 cycles 22971 cycles 1.00
ML-KEM-1024 keypair 21803 cycles 21807 cycles 1.00
ML-KEM-1024 encaps 23560 cycles 23551 cycles 1.00
ML-KEM-1024 decaps 31223 cycles 31213 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AMD EPYC 3rd gen (c6a)

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 16979 cycles 16963 cycles 1.00
ML-KEM-512 encaps 18633 cycles 18638 cycles 1.00
ML-KEM-512 decaps 23951 cycles 23952 cycles 1.00
ML-KEM-768 keypair 28803 cycles 28897 cycles 1.00
ML-KEM-768 encaps 29937 cycles 29934 cycles 1.00
ML-KEM-768 decaps 37646 cycles 37633 cycles 1.00
ML-KEM-1024 keypair 42019 cycles 42144 cycles 1.00
ML-KEM-1024 encaps 44392 cycles 44254 cycles 1.00
ML-KEM-1024 decaps 54455 cycles 54692 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Intel Xeon 4th gen (c7i) (no-opt)

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 28806 cycles 28793 cycles 1.00
ML-KEM-512 encaps 34812 cycles 34819 cycles 1.00
ML-KEM-512 decaps 44945 cycles 44962 cycles 1.00
ML-KEM-768 keypair 48310 cycles 48491 cycles 1.00
ML-KEM-768 encaps 58560 cycles 58558 cycles 1.00
ML-KEM-768 decaps 71973 cycles 72121 cycles 1.00
ML-KEM-1024 keypair 71752 cycles 71744 cycles 1.00
ML-KEM-1024 encaps 86081 cycles 86145 cycles 1.00
ML-KEM-1024 decaps 103543 cycles 103558 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AMD EPYC 4th gen (c7a)

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 11584 cycles 11577 cycles 1.00
ML-KEM-512 encaps 13050 cycles 13033 cycles 1.00
ML-KEM-512 decaps 17963 cycles 17949 cycles 1.00
ML-KEM-768 keypair 19525 cycles 19635 cycles 0.99
ML-KEM-768 encaps 20532 cycles 20577 cycles 1.00
ML-KEM-768 decaps 27659 cycles 27635 cycles 1.00
ML-KEM-1024 keypair 26176 cycles 26223 cycles 1.00
ML-KEM-1024 encaps 28215 cycles 28249 cycles 1.00
ML-KEM-1024 decaps 37490 cycles 37534 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Intel Xeon 3rd gen (c6i)

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 15795 cycles 15779 cycles 1.00
ML-KEM-512 encaps 17842 cycles 17843 cycles 1.00
ML-KEM-512 decaps 24391 cycles 24358 cycles 1.00
ML-KEM-768 keypair 27062 cycles 27053 cycles 1.00
ML-KEM-768 encaps 28682 cycles 28661 cycles 1.00
ML-KEM-768 decaps 38133 cycles 38119 cycles 1.00
ML-KEM-1024 keypair 36590 cycles 36575 cycles 1.00
ML-KEM-1024 encaps 39506 cycles 39488 cycles 1.00
ML-KEM-1024 decaps 51977 cycles 51951 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AMD EPYC 3rd gen (c6a) (no-opt)

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 39689 cycles 39696 cycles 1.00
ML-KEM-512 encaps 48335 cycles 48393 cycles 1.00
ML-KEM-512 decaps 62954 cycles 63017 cycles 1.00
ML-KEM-768 keypair 65551 cycles 65547 cycles 1.00
ML-KEM-768 encaps 77182 cycles 77185 cycles 1.00
ML-KEM-768 decaps 96272 cycles 96276 cycles 1.00
ML-KEM-1024 keypair 98080 cycles 98056 cycles 1.00
ML-KEM-1024 encaps 112490 cycles 112583 cycles 1.00
ML-KEM-1024 decaps 136569 cycles 137084 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AMD EPYC 4th gen (c7a) (no-opt)

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 37758 cycles 37785 cycles 1.00
ML-KEM-512 encaps 44407 cycles 44424 cycles 1.00
ML-KEM-512 decaps 58613 cycles 58614 cycles 1.00
ML-KEM-768 keypair 61363 cycles 61433 cycles 1.00
ML-KEM-768 encaps 69953 cycles 70047 cycles 1.00
ML-KEM-768 decaps 88862 cycles 89231 cycles 1.00
ML-KEM-1024 keypair 88849 cycles 88826 cycles 1.00
ML-KEM-1024 encaps 101003 cycles 101176 cycles 1.00
ML-KEM-1024 decaps 123410 cycles 123493 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton4

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 18120 cycles 18124 cycles 1.00
ML-KEM-512 encaps 21277 cycles 21280 cycles 1.00
ML-KEM-512 decaps 27915 cycles 27915 cycles 1
ML-KEM-768 keypair 30579 cycles 30584 cycles 1.00
ML-KEM-768 encaps 33623 cycles 33621 cycles 1.00
ML-KEM-768 decaps 43183 cycles 43181 cycles 1.00
ML-KEM-1024 keypair 44186 cycles 44190 cycles 1.00
ML-KEM-1024 encaps 49653 cycles 49652 cycles 1.00
ML-KEM-1024 decaps 62636 cycles 62638 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Intel Xeon 3rd gen (c6i) (no-opt)

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 47136 cycles 47172 cycles 1.00
ML-KEM-512 encaps 56379 cycles 56388 cycles 1.00
ML-KEM-512 decaps 72643 cycles 72631 cycles 1.00
ML-KEM-768 keypair 78077 cycles 77979 cycles 1.00
ML-KEM-768 encaps 89842 cycles 89785 cycles 1.00
ML-KEM-768 decaps 111228 cycles 111101 cycles 1.00
ML-KEM-1024 keypair 114929 cycles 115046 cycles 1.00
ML-KEM-1024 encaps 130411 cycles 130352 cycles 1.00
ML-KEM-1024 decaps 157665 cycles 157863 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton3

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 18956 cycles 18956 cycles 1
ML-KEM-512 encaps 22522 cycles 22521 cycles 1.00
ML-KEM-512 decaps 29631 cycles 29631 cycles 1
ML-KEM-768 keypair 32347 cycles 32343 cycles 1.00
ML-KEM-768 encaps 35920 cycles 35917 cycles 1.00
ML-KEM-768 decaps 46301 cycles 46302 cycles 1.00
ML-KEM-1024 keypair 46670 cycles 46668 cycles 1.00
ML-KEM-1024 encaps 52534 cycles 52528 cycles 1.00
ML-KEM-1024 decaps 66315 cycles 66312 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton4 (no-opt)

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 37937 cycles 37939 cycles 1.00
ML-KEM-512 encaps 43315 cycles 43313 cycles 1.00
ML-KEM-512 decaps 55544 cycles 55545 cycles 1.00
ML-KEM-768 keypair 63142 cycles 63144 cycles 1.00
ML-KEM-768 encaps 70606 cycles 70605 cycles 1.00
ML-KEM-768 decaps 86946 cycles 86945 cycles 1.00
ML-KEM-1024 keypair 94526 cycles 94525 cycles 1.00
ML-KEM-1024 encaps 105293 cycles 105293 cycles 1
ML-KEM-1024 decaps 126582 cycles 126582 cycles 1

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton2

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 29047 cycles 29045 cycles 1.00
ML-KEM-512 encaps 34950 cycles 34950 cycles 1
ML-KEM-512 decaps 45448 cycles 45444 cycles 1.00
ML-KEM-768 keypair 49244 cycles 49244 cycles 1
ML-KEM-768 encaps 55557 cycles 55555 cycles 1.00
ML-KEM-768 decaps 70417 cycles 70408 cycles 1.00
ML-KEM-1024 keypair 71975 cycles 71971 cycles 1.00
ML-KEM-1024 encaps 80757 cycles 80753 cycles 1.00
ML-KEM-1024 decaps 100441 cycles 100437 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton3 (no-opt)

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 39352 cycles 39346 cycles 1.00
ML-KEM-512 encaps 45276 cycles 45274 cycles 1.00
ML-KEM-512 decaps 57148 cycles 57142 cycles 1.00
ML-KEM-768 keypair 65873 cycles 65866 cycles 1.00
ML-KEM-768 encaps 73874 cycles 73883 cycles 1.00
ML-KEM-768 decaps 89846 cycles 89852 cycles 1.00
ML-KEM-1024 keypair 99011 cycles 99001 cycles 1.00
ML-KEM-1024 encaps 109989 cycles 109983 cycles 1.00
ML-KEM-1024 decaps 130877 cycles 130860 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Arm Cortex-A55 (Snapdragon 888) benchmarks

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 58244 cycles 58238 cycles 1.00
ML-KEM-512 encaps 65719 cycles 65650 cycles 1.00
ML-KEM-512 decaps 84440 cycles 84458 cycles 1.00
ML-KEM-768 keypair 98779 cycles 98763 cycles 1.00
ML-KEM-768 encaps 110143 cycles 110184 cycles 1.00
ML-KEM-768 decaps 136627 cycles 136303 cycles 1.00
ML-KEM-1024 keypair 150202 cycles 150097 cycles 1.00
ML-KEM-1024 encaps 166372 cycles 165912 cycles 1.00
ML-KEM-1024 decaps 203008 cycles 202018 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Graviton2 (no-opt)

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 61372 cycles 61376 cycles 1.00
ML-KEM-512 encaps 69993 cycles 69997 cycles 1.00
ML-KEM-512 decaps 88961 cycles 88962 cycles 1.00
ML-KEM-768 keypair 102041 cycles 102056 cycles 1.00
ML-KEM-768 encaps 114172 cycles 114152 cycles 1.00
ML-KEM-768 decaps 139516 cycles 139501 cycles 1.00
ML-KEM-1024 keypair 154590 cycles 154590 cycles 1
ML-KEM-1024 encaps 170445 cycles 170334 cycles 1.00
ML-KEM-1024 decaps 202602 cycles 202511 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Arm Cortex-A72 (Raspberry Pi 4) benchmarks

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 51584 cycles 51590 cycles 1.00
ML-KEM-512 encaps 59449 cycles 60136 cycles 0.99
ML-KEM-512 decaps 75928 cycles 75769 cycles 1.00
ML-KEM-768 keypair 89026 cycles 88608 cycles 1.00
ML-KEM-768 encaps 96759 cycles 96818 cycles 1.00
ML-KEM-768 decaps 119591 cycles 120138 cycles 1.00
ML-KEM-1024 keypair 131399 cycles 131788 cycles 1.00
ML-KEM-1024 encaps 145863 cycles 145353 cycles 1.00
ML-KEM-1024 decaps 175824 cycles 175673 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

@oqs-bot
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Bananapi bpi-f3 benchmarks

Benchmark suite Current: 3da5027 Previous: 3dc9642 Ratio
ML-KEM-512 keypair 331322 cycles 331334 cycles 1.00
ML-KEM-512 encaps 439889 cycles 439896 cycles 1.00
ML-KEM-512 decaps 588401 cycles 588436 cycles 1.00
ML-KEM-768 keypair 548649 cycles 548599 cycles 1.00
ML-KEM-768 encaps 688357 cycles 688259 cycles 1.00
ML-KEM-768 decaps 880460 cycles 880050 cycles 1.00
ML-KEM-1024 keypair 814746 cycles 814706 cycles 1.00
ML-KEM-1024 encaps 988815 cycles 988517 cycles 1.00
ML-KEM-1024 decaps 1222508 cycles 1222676 cycles 1.00

This comment was automatically generated by workflow using github-action-benchmark.

Please sign in to comment.