From 4964ba1b4aae8abb42fa7eac34eb3c0e11126523 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 13 Nov 2023 20:43:50 -0800 Subject: [PATCH] Provide standalone binaries Fixes #1724 Note that we keep the non-unified binaries (and use them to build generated files) to avoid OOMs on Coq's CI. It's unfortunate that compilation is so slow here, taking almost an hour on my machine just to extract and compile the various binaries.
Timing Diff

``` Time | Peak Mem | File Name ---------------------------------------------------------------------------------- 53m02.47s | 2463008 ko | Total Time / Peak Mem ---------------------------------------------------------------------------------- 2m21.70s | 2462928 ko | ExtractionOCaml/fiat_crypto 2m19.85s | 2463008 ko | ExtractionOCaml/bedrock2_fiat_crypto 1m53.82s | 1863716 ko | ExtractionOCaml/solinas_reduction 1m36.75s | 2462904 ko | ExtractionOCaml/with_bedrock2_fiat_crypto 1m33.30s | 2316820 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml 1m30.98s | 2300660 ko | ExtractionOCaml/fiat_crypto.ml 1m30.25s | 2075840 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery 1m26.51s | 2074640 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery 1m25.26s | 1829432 ko | ExtractionOCaml/word_by_word_montgomery 1m22.38s | 1780504 ko | ExtractionOCaml/bedrock2_unsaturated_solinas 1m20.72s | 2147524 ko | ExtractionOCaml/bedrock2_solinas_reduction 1m20.62s | 2336764 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml 1m18.57s | 1416332 ko | ExtractionOCaml/with_bedrock2_base_conversion 1m16.74s | 1469000 ko | ExtractionOCaml/bedrock2_dettman_multiplication 1m14.80s | 1780196 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas 1m14.67s | 1415232 ko | ExtractionOCaml/base_conversion 1m08.91s | 1416276 ko | ExtractionOCaml/bedrock2_base_conversion 1m08.90s | 1415436 ko | ExtractionOCaml/dettman_multiplication 1m07.90s | 1415368 ko | ExtractionOCaml/saturated_solinas 1m07.63s | 1525784 ko | ExtractionOCaml/unsaturated_solinas 1m07.23s | 1449720 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication 1m07.09s | 1447196 ko | ExtractionOCaml/with_bedrock2_saturated_solinas 1m07.02s | 1439752 ko | ExtractionOCaml/bedrock2_saturated_solinas 1m06.29s | 1448860 ko | ExtractionOCaml/with_bedrock2_solinas_reduction 1m05.35s | 2190452 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml 1m03.87s | 2137192 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml 1m01.18s | 2137308 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml 0m58.53s | 2057100 ko | ExtractionOCaml/solinas_reduction.ml 0m56.27s | 2063328 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml 0m55.76s | 1836424 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml 0m55.38s | 2030208 ko | ExtractionOCaml/word_by_word_montgomery.ml 0m52.90s | 1413320 ko | ExtractionOCaml/perf_unsaturated_solinas 0m51.44s | 2063536 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml 0m51.16s | 1950720 ko | ExtractionOCaml/bedrock2_base_conversion.ml 0m50.96s | 1989736 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml 0m49.61s | 1936244 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml 0m49.39s | 1936412 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml 0m49.38s | 1753040 ko | ExtractionOCaml/perf_unsaturated_solinas.ml 0m48.72s | 1938204 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml 0m48.29s | 1952524 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml 0m48.16s | 1938444 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml 0m47.28s | 1962520 ko | ExtractionOCaml/unsaturated_solinas.ml 0m46.15s | 1823484 ko | ExtractionOCaml/base_conversion.ml 0m42.74s | 1413036 ko | ExtractionOCaml/perf_word_by_word_montgomery 0m41.95s | 1882704 ko | ExtractionOCaml/dettman_multiplication.ml 0m38.36s | 1846056 ko | ExtractionOCaml/saturated_solinas.ml 0m04.57s | 1035968 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo 0m00.93s | 106556 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi 0m00.90s | 102844 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi 0m00.89s | 103608 ko | ExtractionOCaml/dettman_multiplication.cmi 0m00.87s | 105352 ko | ExtractionOCaml/unsaturated_solinas.cmi 0m00.84s | 102728 ko | ExtractionOCaml/fiat_crypto.cmi 0m00.83s | 103608 ko | ExtractionOCaml/saturated_solinas.cmi 0m00.83s | 103844 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi 0m00.81s | 102720 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi 0m00.80s | 103684 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi 0m00.76s | 102640 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi 0m00.76s | 107620 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi 0m00.75s | 102300 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi 0m00.75s | 103592 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi 0m00.75s | 102900 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi 0m00.74s | 102780 ko | ExtractionOCaml/bedrock2_base_conversion.cmi 0m00.72s | 103088 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi 0m00.71s | 105644 ko | ExtractionOCaml/word_by_word_montgomery.cmi 0m00.70s | 103272 ko | ExtractionOCaml/base_conversion.cmi 0m00.69s | 103100 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi 0m00.67s | 102580 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi 0m00.67s | 103236 ko | ExtractionOCaml/solinas_reduction.cmi 0m00.42s | 58808 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi 0m00.39s | 60084 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi ```

--- .github/workflows/coq-alpine.yml | 62 ++++++------- .github/workflows/coq-debian.yml | 72 +++++++--------- .github/workflows/coq-docker.yml | 73 +++++++--------- .github/workflows/coq-macos.yml | 57 ++++++------ .github/workflows/coq-opam-package.yml | 9 +- .github/workflows/coq-windows.yml | 64 +++++--------- Makefile.config | 36 ++++++-- Makefile.standalone | 46 ++++++++-- README.md | 56 +++++++----- src/CLI.v | 86 ++++++++++++++++++- src/ExtractionHaskell/bedrock2_fiat_crypto.v | 5 ++ src/ExtractionHaskell/fiat_crypto.v | 4 + .../with_bedrock2_fiat_crypto.v | 5 ++ src/ExtractionOCaml/bedrock2_fiat_crypto.v | 4 + src/ExtractionOCaml/fiat_crypto.v | 3 + .../with_bedrock2_fiat_crypto.v | 4 + src/StandaloneDebuggingExamples.v | 10 +-- src/StandaloneHaskellMain.v | 5 ++ src/StandaloneOCamlMain.v | 5 ++ src/Util/Arg.v | 23 +++-- 20 files changed, 385 insertions(+), 244 deletions(-) create mode 100644 src/ExtractionHaskell/bedrock2_fiat_crypto.v create mode 100644 src/ExtractionHaskell/fiat_crypto.v create mode 100644 src/ExtractionHaskell/with_bedrock2_fiat_crypto.v create mode 100644 src/ExtractionOCaml/bedrock2_fiat_crypto.v create mode 100644 src/ExtractionOCaml/fiat_crypto.v create mode 100644 src/ExtractionOCaml/with_bedrock2_fiat_crypto.v diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml index e38f1d3540f..d4842335813 100644 --- a/.github/workflows/coq-alpine.yml +++ b/.github/workflows/coq-alpine.yml @@ -65,14 +65,14 @@ jobs: name: generated-files-${{ matrix.alpine }} path: generated-files.tgz if: ${{ failure() }} - - name: package-standalone-ocaml + - name: install-standalone-unified-ocaml shell: alpine.sh {0} - run: make package-standalone-ocaml + run: make install-standalone-unified-ocaml BINDIR=dist - name: upload standalone files uses: actions/upload-artifact@v3 with: name: standalone-${{ matrix.alpine }} - path: standalone.tar.gz + path: dist/fiat_crypto - name: upload OCaml files uses: actions/upload-artifact@v3 with: @@ -112,32 +112,25 @@ jobs: uses: actions/download-artifact@v3 with: name: standalone-${{ matrix.alpine }} - path: dist-${{ matrix.alpine }}/ + path: dist/ - name: List files - run: find dist-edge - - name: Rename files - run: | - mkdir dist - mv dist-${{ matrix.alpine }}/standalone.tar.gz dist/fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz - find dist - tar -tvf dist/fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz - - name: Unpack files - run: | - cd dist - tar -xzvf fiat-crypto-alpine-${{ matrix.alpine }}.tar.gz - ls -la . + run: find dist + - run: chmod +x dist/fiat_crypto - name: Test files (host) run: | cd dist - for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do - echo "::group::file $prog" - file $prog - echo "::endgroup::" - echo "::group::ldd $prog" - ldd $prog || true - echo "::endgroup::" + echo "::group::file fiat_crypto" + file fiat_crypto + echo "::endgroup::" + echo "::group::ldd fiat_crypto" + ldd fiat_crypto || true + echo "::endgroup::" + echo "::group::fiat_crypto" + ./fiat_crypto -h + echo "::endgroup::" + for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do echo "::group::$prog" - ./$prog -h + ./fiat_crypto $prog -h echo "::endgroup::" done - uses: jirutka/setup-alpine@v1 @@ -148,9 +141,12 @@ jobs: shell: alpine.sh {0} run: | cd dist - for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do + echo "::group::fiat_crypto" + ./fiat_crypto -h + echo "::endgroup::" + for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do echo "::group::$prog" - ./$prog -h + ./fiat_crypto $prog -h echo "::endgroup::" done @@ -168,21 +164,19 @@ jobs: uses: actions/download-artifact@v3 with: name: standalone-edge - path: dist-edge/ + path: dist/ - name: List files - run: find dist-edge + run: find dist - name: Unpack files run: | - mkdir dist echo "::group::find arch" - ( cd dist-edge && tar -xzvf standalone.tar.gz ) - arch="$(etc/ci/find-arch.sh dist-edge/word_by_word_montgomery "unknown")" + arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Linux_${arch}.tar.gz" + fname="Fiat-Cryptography_${tag}_Linux_${arch}" echo "$fname" - mv dist-edge/standalone.tar.gz "dist/$fname" + mv dist/fiat_crypto "dist/$fname" find dist - tar -tvf "dist/$fname" + file "dist/$fname" - name: Upload artifacts to GitHub Release env: GITHUB_TOKEN: ${{ github.token }} diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml index 7fb9976e99f..59e8f442a37 100644 --- a/.github/workflows/coq-debian.yml +++ b/.github/workflows/coq-debian.yml @@ -57,14 +57,14 @@ jobs: name: generated-files-${{ matrix.env.DEBIAN }} path: generated-files.tgz if: ${{ failure() }} - - name: package-standalone-ocaml + - name: install-standalone-unified-ocaml shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh package-standalone-ocaml + run: etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist - name: upload standalone files uses: actions/upload-artifact@v3 with: name: standalone-${{ matrix.env.DEBIAN }} - path: standalone.tar.gz + path: dist/fiat_crypto - name: upload OCaml files uses: actions/upload-artifact@v3 with: @@ -103,32 +103,24 @@ jobs: uses: actions/download-artifact@v3 with: name: standalone-${{ matrix.debian }} - path: dist-${{ matrix.debian }}/ + path: dist/ - name: List files - run: find dist-${{ matrix.debian }} - - name: Rename files - run: | - mkdir dist - mv dist-${{ matrix.debian }}/standalone.tar.gz dist/fiat-crypto-${{ matrix.debian }}.tar.gz - find dist - tar -tvf dist/fiat-crypto-${{ matrix.debian }}.tar.gz - - name: Unpack Files - run: | - cd dist - tar -xzvf fiat-crypto-${{ matrix.debian }}.tar.gz - ls -la . + run: find dist - name: Test files (host) run: | cd dist - for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do - echo "::group::file $prog" - file $prog - echo "::endgroup::" - echo "::group::ldd $prog" - ldd $prog - echo "::endgroup::" + echo "::group::file fiat_crypto" + file fiat_crypto + echo "::endgroup::" + echo "::group::ldd fiat_crypto" + ldd fiat_crypto + echo "::endgroup::" + echo "::group::fiat_crypto" + ./fiat_crypto -h + echo "::endgroup::" + for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do echo "::group::$prog" - ./$prog -h + ./fiat_crypto $prog -h echo "::endgroup::" done - name: setup Debian chroot @@ -137,15 +129,18 @@ jobs: shell: in-debian-chroot.sh {0} run: | cd dist - for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do - echo "::group::file $prog" - file $prog - echo "::endgroup::" - echo "::group::ldd $prog" - ldd $prog - echo "::endgroup::" + echo "::group::file fiat_crypto" + file fiat_crypto + echo "::endgroup::" + echo "::group::ldd fiat_crypto" + ldd fiat_crypto + echo "::endgroup::" + echo "::group::fiat_crypto" + ./fiat_crypto -h + echo "::endgroup::" + for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do echo "::group::$prog" - ./$prog -h + ./fiat_crypto $prog -h echo "::endgroup::" done @@ -163,21 +158,20 @@ jobs: uses: actions/download-artifact@v3 with: name: standalone-sid - path: dist-sid/ + path: dist/ - name: List files - run: find dist-sid + run: find dist + - run: chmod +x dist/fiat_crypto - name: Unpack files run: | mkdir dist echo "::group::find arch" - ( cd dist-sid && tar -xzvf standalone.tar.gz ) - arch="$(etc/ci/find-arch.sh dist-sid/word_by_word_montgomery "unknown")" + arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Linux_debian_sid_${arch}.tar.gz" + fname="Fiat-Cryptography_${tag}_Linux_debian_sid_${arch}" echo "$fname" - mv dist-sid/standalone.tar.gz "dist/$fname" + mv dist/fiat_crypto "dist/$fname" find dist - tar -tvf "dist/$fname" # - name: Upload artifacts to GitHub Release # env: # GITHUB_TOKEN: ${{ github.token }} diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml index 735e23f8986..1471c96f26b 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq-docker.yml @@ -68,13 +68,13 @@ jobs: name: generated-files-${{ matrix.env.COQ_VERSION }} path: generated-files.tgz if: ${{ failure() }} - - name: package-standalone-ocaml - run: etc/ci/github-actions-make.sh -f Makefile.standalone package-standalone-ocaml + - name: install-standalone-unified-ocaml + run: make -f Makefile.standalone install-standalone-unified-ocaml BINDIR=dist - name: upload standalone files uses: actions/upload-artifact@v3 with: name: standalone-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }} - path: standalone.tar.gz + path: dist/fiat_crypto - name: upload OCaml files uses: actions/upload-artifact@v3 with: @@ -151,32 +151,25 @@ jobs: uses: actions/download-artifact@v3 with: name: standalone-docker-coq-${{ matrix.docker-coq-version }} - path: dist-docker-coq-${{ matrix.docker-coq-version }}/ + path: dist/ - name: List files - run: find dist-docker-coq-${{ matrix.docker-coq-version }} - - name: Rename files - run: | - mkdir dist - mv dist-docker-coq-${{ matrix.docker-coq-version }}/standalone.tar.gz dist/fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz - find dist - tar -tvf dist/fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz - - name: Unpack Files - run: | - cd dist - tar -xzvf fiat-crypto-docker-coq-${{ matrix.docker-coq-version }}.tar.gz - ls -la . + run: find dist + - run: chmod +x dist/fiat_crypto - name: Test files (host) run: | cd dist - for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do - echo "::group::file $prog" - file $prog - echo "::endgroup::" - echo "::group::ldd $prog" - ldd $prog - echo "::endgroup::" + echo "::group::file fiat_crypto" + file fiat_crypto + echo "::endgroup::" + echo "::group::ldd fiat_crypto" + ldd fiat_crypto + echo "::endgroup::" + echo "::group::fiat_crypto" + ./fiat_crypto -h + echo "::endgroup::" + for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do echo "::group::$prog" - ./$prog -h + ./fiat_crypto $prog -h echo "::endgroup::" done - name: Test files (container) @@ -190,15 +183,18 @@ jobs: sudo apt-get install -y file echo "::endgroup::" cd dist - for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do - echo "::group::file $prog" - file $prog - echo "::endgroup::" - echo "::group::ldd $prog" - ldd $prog - echo "::endgroup::" + echo "::group::file fiat_crypto" + file fiat_crypto + echo "::endgroup::" + echo "::group::ldd fiat_crypto" + ldd fiat_crypto + echo "::endgroup::" + echo "::group::fiat_crypto" + ./fiat_crypto -h + echo "::endgroup::" + for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do echo "::group::$prog" - ./$prog -h + ./fiat_crypto $prog -h echo "::endgroup::" done @@ -216,21 +212,18 @@ jobs: uses: actions/download-artifact@v3 with: name: standalone-docker-coq-dev - path: dist-docker-coq-dev/ + path: dist/ - name: List files - run: find dist-docker-coq-dev + run: find dist - name: Unpack files run: | - mkdir dist echo "::group::find arch" - ( cd dist-docker-coq-dev && tar -xzvf standalone.tar.gz ) - arch="$(etc/ci/find-arch.sh dist-docker-coq-dev/word_by_word_montgomery "unknown")" + arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Linux_docker_dev_${arch}.tar.gz" + fname="Fiat-Cryptography_${tag}_Linux_docker_dev_${arch}" echo "$fname" - mv dist-docker-coq-dev/standalone.tar.gz "dist/$fname" + mv dist/fiat_crypto "dist/$fname" find dist - tar -tvf "dist/$fname" # - name: Upload artifacts to GitHub Release # env: # GITHUB_TOKEN: ${{ github.token }} diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml index 51ea39d7f30..eede0748906 100644 --- a/.github/workflows/coq-macos.yml +++ b/.github/workflows/coq-macos.yml @@ -65,10 +65,10 @@ jobs: eval $(opam env) etc/ci/github-actions-make.sh -j2 all - - name: package standalone files + - name: install-standalone-unified-ocaml run: | eval $(opam env) - etc/ci/github-actions-make.sh package-standalone-ocaml + etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist - name: only-test-amd64-files-lite run: | @@ -84,7 +84,7 @@ jobs: uses: actions/upload-artifact@v3 with: name: standalone-macos - path: standalone.tar.gz + path: dist/fiat_crypto - name: display timing info run: cat time-of-build-pretty.log - name: display per-line timing info @@ -110,35 +110,28 @@ jobs: uses: actions/download-artifact@v3 with: name: standalone-macos - path: dist-macos/ + path: dist/ - name: List files - run: find dist-macos - - name: Rename files - run: | - mkdir dist - mv dist-macos/standalone.tar.gz dist/fiat-crypto-macos.tar.gz - find dist - tar -tvf dist/fiat-crypto-macos.tar.gz - - name: Unpack Files - run: | - cd dist - tar -xzvf fiat-crypto-macos.tar.gz - ls -la . + run: find dist + - run: chmod +x dist/fiat_crypto - name: Test files run: | cd dist - for prog in word_by_word_montgomery unsaturated_solinas saturated_solinas base_conversion; do - echo "::group::file $prog" - file $prog - echo "::endgroup::" - echo "::group::otool -L $prog" - otool -L $prog - echo "::endgroup::" - echo "::group::lipo -info $prog" - lipo -info $prog - echo "::endgroup::" + echo "::group::file fiat_crypto" + file fiat_crypto + echo "::endgroup::" + echo "::group::otool -L fiat_crypto" + otool -L fiat_crypto + echo "::endgroup::" + echo "::group::lipo -info fiat_crypto" + lipo -info fiat_crypto + echo "::endgroup::" + echo "::group::fiat_crypto" + ./fiat_crypto -h + echo "::endgroup::" + for prog in word-by-word-montgomery unsaturated-solinas saturated-solinas base-conversion; do echo "::group::$prog" - ./$prog -h + ./fiat_crypto $prog -h echo "::endgroup::" done @@ -156,20 +149,18 @@ jobs: uses: actions/download-artifact@v3 with: name: standalone-macos - path: dist-macos/ + path: dist/ - name: List files run: find dist-macos - name: Unpack files run: | mkdir dist - ( cd dist-macos && tar -xzvf standalone.tar.gz ) - arch="$(etc/ci/find-arch.sh dist-macos/word_by_word_montgomery)" + arch="$(etc/ci/find-arch.sh dist/fiat_crypto)" tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_macOS_${arch}.tar.gz" + fname="Fiat-Cryptography_${tag}_macOS_${arch}" echo "$fname" - mv dist-macos/standalone.tar.gz "dist/$fname" + mv dist/fiat_crypto "dist/$fname" find dist - tar -tvf "dist/$fname" - name: Upload artifacts to GitHub Release env: GITHUB_TOKEN: ${{ github.token }} diff --git a/.github/workflows/coq-opam-package.yml b/.github/workflows/coq-opam-package.yml index 3e756250311..0f9df7e6b66 100644 --- a/.github/workflows/coq-opam-package.yml +++ b/.github/workflows/coq-opam-package.yml @@ -165,7 +165,8 @@ jobs: if: ${{ always() && runner.os == 'Windows' }} - run: opam list - - run: opam exec -- word_by_word_montgomery -h - - run: opam exec -- unsaturated_solinas -h - - run: opam exec -- saturated_solinas -h - - run: opam exec -- base_conversion -h + - run: opam exec -- fiat_crypto -h + - run: opam exec -- fiat_crypto word-by-word-montgomery -h + - run: opam exec -- fiat_crypto unsaturated-solinas -h + - run: opam exec -- fiat_crypto saturated-solinas -h + - run: opam exec -- fiat_crypto base-conversion -h diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml index de811eabae4..6f3bc4a18fd 100644 --- a/.github/workflows/coq-windows.yml +++ b/.github/workflows/coq-windows.yml @@ -72,9 +72,9 @@ jobs: run: | %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} standalone-ocaml' shell: cmd - - name: package-standalone-ocaml + - name: install-standalone-unified-ocaml run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh package-standalone-ocaml PACKAGE=standalone.zip PACKAGE_CMD=zip' + %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist' shell: cmd - name: coq run: | @@ -101,7 +101,7 @@ jobs: uses: actions/upload-artifact@v3 with: name: standalone-windows - path: standalone.zip + path: dist/fiat_crypto.exe - name: display timing info run: type time-of-build-pretty.log shell: cmd @@ -130,43 +130,26 @@ jobs: uses: actions/download-artifact@v3 with: name: standalone-windows - path: dist-windows/ + path: dist/ - name: List files - run: Get-ChildItem dist-windows -Name - - name: Rename files - run: | - New-Item -ItemType Directory -Path dist - Move-Item dist-windows/standalone.zip dist/fiat-crypto-windows.zip - Get-ChildItem dist -Name - - name: Unpack files - run: | - Expand-Archive -Path dist/fiat-crypto-windows.zip -DestinationPath dist - Get-ChildItem dist - - run: .\dist\word_by_word_montgomery.exe -h - - run: .\dist\unsaturated_solinas.exe -h - - run: .\dist\saturated_solinas.exe -h - - run: .\dist\base_conversion.exe -h + run: Get-ChildItem dist -Name + - run: .\dist\fiat_crypto.exe -h + - run: .\dist\fiat_crypto.exe word-by-word-montgomery -h + - run: .\dist\fiat_crypto.exe unsaturated-solinas -h + - run: .\dist\fiat_crypto.exe saturated-solinas -h + - run: .\dist\fiat_crypto.exe base-conversion -h - name: Set up MSVC Environment for dumpbin uses: ilammy/msvc-dev-cmd@v1 - name: Check Executable Dependencies run: | - $executables = @( - ".\dist\word_by_word_montgomery.exe", - ".\dist\unsaturated_solinas.exe", - ".\dist\saturated_solinas.exe", - ".\dist\base_conversion.exe" - ) - - foreach ($prog in $executables) { - Write-Host "::group::File Info - $prog" - Get-Item $prog | Format-List - dumpbin.exe /headers $prog - Write-Host "::endgroup::" + Write-Host "::group::File Info - fiat_crypto" + Get-Item .\dist\fiat_crypto.exe | Format-List + dumpbin.exe /headers .\dist\fiat_crypto.exe + Write-Host "::endgroup::" - Write-Host "::group::DLL Dependencies - $prog" - dumpbin.exe /dependents $prog - Write-Host "::endgroup::" - } + Write-Host "::group::DLL Dependencies - fiat_crypto" + dumpbin.exe /dependents .\dist\fiat_crypto.exe + Write-Host "::endgroup::" publish-standalone: runs-on: ubuntu-latest @@ -182,20 +165,17 @@ jobs: uses: actions/download-artifact@v3 with: name: standalone-windows - path: dist-windows/ + path: dist/ - name: List files - run: find dist-windows + run: find dist - name: Unpack files run: | - mkdir dist - ( cd dist-windows && unzip standalone.zip ) - arch="$(etc/ci/find-arch.sh dist-windows/word_by_word_montgomery "x86_64")" + arch="$(etc/ci/find-arch.sh dist/fiat_crypto.exe "x86_64")" tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Windows_${arch}.zip" + fname="Fiat-Cryptography_${tag}_Windows_${arch}.exe" echo "$fname" - mv dist-windows/standalone.zip "dist/$fname" + mv dist/fiat_crypto.exe "dist/$fname" find dist - unzip -l "dist/$fname" - name: Upload artifacts to GitHub Release env: GITHUB_TOKEN: ${{ github.token }} diff --git a/Makefile.config b/Makefile.config index c559c61740e..afed0c3954a 100644 --- a/Makefile.config +++ b/Makefile.config @@ -50,16 +50,34 @@ else if_SKIP_BEDROCK2 = $(1) endif -BASE_STANDALONE := unsaturated_solinas saturated_solinas dettman_multiplication word_by_word_montgomery base_conversion solinas_reduction -BEDROCK2_STANDALONE := $(addprefix bedrock2_,$(BASE_STANDALONE)) $(addprefix with_bedrock2_,$(BASE_STANDALONE)) -STANDALONE := $(BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_STANDALONE) $(WITH_BEDROCK2_STANDALONE)) +UNIFIED_BASE_STANDALONE := fiat_crypto +SEPARATE_BASE_STANDALONE := unsaturated_solinas saturated_solinas dettman_multiplication word_by_word_montgomery base_conversion solinas_reduction +BASE_STANDALONE := $(SEPARATE_BASE_STANDALONE) $(UNIFIED_STANDALONE) +BEDROCK2_UNIFIED_STANDALONE := $(addprefix bedrock2_,$(UNIFIED_BASE_STANDALONE)) $(addprefix with_bedrock2_,$(UNIFIED_BASE_STANDALONE)) +BEDROCK2_SEPARATE_STANDALONE := $(addprefix bedrock2_,$(SEPARATE_BASE_STANDALONE)) $(addprefix with_bedrock2_,$(SEPARATE_BASE_STANDALONE)) +BEDROCK2_STANDALONE := $(BEDROCK2_UNIFIED_STANDALONE) $(BEDROCK2_SEPARATE_STANDALONE) +UNIFIED_STANDALONE := $(UNIFIED_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_UNIFIED_STANDALONE) $(WITH_BEDROCK2_UNIFIED_STANDALONE)) +SEPARATE_STANDALONE := $(SEPARATE_BASE_STANDALONE) $(call if_SKIP_BEDROCK2,,$(BEDROCK2_SEPARATE_STANDALONE) $(WITH_BEDROCK2_SEPARATE_STANDALONE)) +STANDALONE := $(UNIFIED_STANDALONE) $(SEPARATE_STANDALONE) PERF_STANDALONE := perf_unsaturated_solinas perf_word_by_word_montgomery -STANDALONE_OCAML := $(STANDALONE) $(PERF_STANDALONE) -STANDALONE_HASKELL := $(STANDALONE) +UNIFIED_STANDALONE_OCAML := $(UNIFIED_STANDALONE) +SEPARATE_STANDALONE_OCAML := $(SEPARATE_STANDALONE) $(PERF_STANDALONE) +STANDALONE_OCAML := $(UNIFIED_STANDALONE_OCAML) $(SEPARATE_STANDALONE_OCAML) +UNIFIED_STANDALONE_HASKELL := $(UNIFIED_STANDALONE) +SEPARATE_STANDALONE_HASKELL := $(SEPARATE_STANDALONE) +STANDALONE_HASKELL := $(UNIFIED_STANDALONE_HASKELL) $(SEPARATE_STANDALONE_HASKELL) -OCAML_BINARIES := $(BASE_STANDALONE:%=src/ExtractionOCaml/%) -HASKELL_BINARIES := $(BASE_STANDALONE:%=src/ExtractionHaskell/%) +UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/%) +SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/%) +OCAML_BINARIES := $(UNIFIED_OCAML_BINARIES) $(SEPARATE_OCAML_BINARIES) +UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/%) +SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/%) +HASKELL_BINARIES := $(UNIFIED_HASKELL_BINARIES) $(SEPARATE_HASKELL_BINARIES) -WITH_BEDROCK2_OCAML_BINARIES := $(BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%) -WITH_BEDROCK2_HASKELL_BINARIES := $(BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%) +WITH_BEDROCK2_UNIFIED_OCAML_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%) +WITH_BEDROCK2_SEPARATE_OCAML_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionOCaml/with_bedrock2_%) +WITH_BEDROCK2_OCAML_BINARIES := $(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES) $(WITH_BEDROCK2_SEPARATE_OCAML_BINARIES) +WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES := $(UNIFIED_BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%) +WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES := $(SEPARATE_BASE_STANDALONE:%=src/ExtractionHaskell/with_bedrock2_%) +WITH_BEDROCK2_HASKELL_BINARIES := $(WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES) $(WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES) diff --git a/Makefile.standalone b/Makefile.standalone index 2175966a598..a5f2fcd754a 100644 --- a/Makefile.standalone +++ b/Makefile.standalone @@ -32,10 +32,18 @@ ENSURE_STACK_LIMIT := . etc/ensure_stack_limit.sh || true .PHONY: \ perf-standalone \ + standalone-unified install-standalone-unified install-standalone-unified \ + standalone-separate install-standalone-separate uninstall-standalone-separate \ standalone install-standalone uninstall-standalone \ + standalone-unified-ocaml install-standalone-unified-ocaml uninstall-standalone-unified-ocaml \ + standalone-separate-ocaml install-standalone-separate-ocaml uninstall-standalone-separate-ocaml \ standalone-ocaml install-standalone-ocaml uninstall-standalone-ocaml \ + standalone-unified-haskell install-standalone-unified-haskell uninstall-standalone-unified-haskell \ + standalone-separate-haskell install-standalone-separate-haskell uninstall-standalone-separate-haskell \ standalone-haskell install-standalone-haskell uninstall-standalone-haskell \ package-standalone package-standalone-ocaml package-standalone-haskell \ + package-standalone-unified package-standalone-unified-ocaml package-standalone-unified-haskell \ + package-standalone-separate package-standalone-separate-ocaml package-standalone-separate-haskell \ # # pass -w -20 to disable the unused argument warning @@ -55,19 +63,33 @@ $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%) : % : %.hs $(HIDE)$(TIMER) $(GHC) $(GHCFLAGS) -o $@ $< standalone: standalone-haskell standalone-ocaml +standalone-unified: standalone-unified-haskell standalone-unified-ocaml +standalone-separate: standalone-separate-haskell standalone-separate-ocaml perf-standalone: $(PERF_STANDALONE:%=src/ExtractionOCaml/%) -standalone-ocaml: $(STANDALONE_OCAML:%=src/ExtractionOCaml/%) -standalone-haskell: $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%) - +standalone-ocaml: standalone-unified-ocaml standalone-separate-ocaml +standalone-unified-ocaml: $(UNIFIED_STANDALONE_OCAML:%=src/ExtractionOCaml/%) +standalone-separate-ocaml: $(SEPARATE_STANDALONE_OCAML:%=src/ExtractionOCaml/%) +standalone-haskell: standalone-unified-haskell standalone-separate-haskell +standalone-unified-haskell: $(UNIFIED_STANDALONE_HASKELL:%=src/ExtractionHaskell/%) +standalone-separate-haskell: $(SEPARATE_STANDALONE_HASKELL:%=src/ExtractionHaskell/%) +# FIXME HERE uninstall-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES) +uninstall-standalone-unified-ocaml: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES) +uninstall-standalone-separate-ocaml: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES) uninstall-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES) +uninstall-standalone-unified-haskell: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES) +uninstall-standalone-separate-haskell: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES) ifeq ($(SKIP_BEDROCK2),1) install-standalone-ocaml: FILESTOINSTALL=$(OCAML_BINARIES) +install-standalone-unified-ocaml: FILESTOINSTALL=$(UNIFIED_OCAML_BINARIES) +install-standalone-separate-ocaml: FILESTOINSTALL=$(SEPARATE_OCAML_BINARIES) install-standalone-haskell: FILESTOINSTALL=$(HASKELL_BINARIES) +install-standalone-unified-haskell: FILESTOINSTALL=$(UNIFIED_HASKELL_BINARIES) +install-standalone-separate-haskell: FILESTOINSTALL=$(SEPARATE_HASKELL_BINARIES) -install-standalone-ocaml install-standalone-haskell: +install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell: $(HIDE)code=0; for f in $(FILESTOINSTALL); do\ if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ done; exit $$code @@ -78,9 +100,13 @@ install-standalone-ocaml install-standalone-haskell: done else install-standalone-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_OCAML_BINARIES) +install-standalone-unified-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_OCAML_BINARIES) +install-standalone-separate-ocaml: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_OCAML_BINARIES) install-standalone-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_HASKELL_BINARIES) +install-standalone-unified-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_UNIFIED_HASKELL_BINARIES) +install-standalone-separate-haskell: FILESTOINSTALL=$(WITH_BEDROCK2_SEPARATE_HASKELL_BINARIES) -install-standalone-ocaml install-standalone-haskell: +install-standalone-ocaml install-standalone-unified-ocaml install-standalone-separate-ocaml install-standalone-haskell install-standalone-unified-haskell install-standalone-separate-haskell: $(HIDE)code=0; for f in $(FILESTOINSTALL); do\ if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ done; exit $$code @@ -94,7 +120,7 @@ install-standalone-ocaml install-standalone-haskell: done endif -uninstall-standalone-ocaml uninstall-standalone-haskell: +uninstall-standalone-ocaml uninstall-standalone-unified-ocaml uninstall-standalone-separate-ocaml uninstall-standalone-haskell uninstall-standalone-unified-haskell uninstall-standalone-separate-haskell: $(HIDE)for f in $(FILESTOINSTALL); do \ instf="$(BINDIR)/`basename $$f`" &&\ rm -f "$$instf" &&\ @@ -102,11 +128,17 @@ uninstall-standalone-ocaml uninstall-standalone-haskell: done install-standalone: install-standalone-ocaml # install-standalone-haskell +install-standalone-unified: install-standalone-unified-ocaml # install-standalone-unified-haskell +install-standalone-separate: install-standalone-separate-ocaml # install-standalone-separate-haskell uninstall-standalone: uninstall-standalone-ocaml # uninstall-standalone-haskell +uninstall-standalone-unified: uninstall-standalone-unified-ocaml # uninstall-standalone-unified-haskell +uninstall-standalone-separate: uninstall-standalone-separate-ocaml # uninstall-standalone-separate-haskell package-standalone: package-standalone-ocaml # package-standalone-haskell +package-standalone-unified: package-standalone-unified-ocaml # package-standalone-unified-haskell +package-standalone-separate: package-standalone-separate-ocaml # package-standalone-separate-haskell -package-standalone-ocaml package-standalone-haskell : package-standalone-% : +package-standalone-ocaml package-standalone-unified-ocaml package-standalone-separate-ocaml package-standalone-haskell package-standalone-unified-haskell package-standalone-separate-haskell : package-standalone-% : $(SHOW)'PACKAGE STANDALONE $*' $(HIDE)rm -f "$(PACKAGE)" +$(HIDE)standalonedir="$$(TMPDIR="$$(pwd)" $(MKTEMP_D))"; \ diff --git a/README.md b/README.md index 2b49c30652b..3fc5b28980a 100644 --- a/README.md +++ b/README.md @@ -52,9 +52,9 @@ Then run: You can check out [our CI](https://github.com/mit-plv/fiat-crypto/actions?query=branch%3Amaster+workflow%3A%22CI+%28Coq%29%22) to see how long the build should take; as of the last update to this line in the README, it takes about 1h10m to run `make -j2` on Coq 8.11.1. -If you want to build only the command-line binaries used for generating code, you can save a bit of time by making only the `standalone-ocaml` target with +If you want to build only the command-line binaries used for generating code, you can save a bit of time by making only the `standalone-unified-ocaml` target with - make standalone-ocaml + make standalone-unified-ocaml Usage (Generating C Files) -------------------------- @@ -76,29 +76,36 @@ Just the compilers generating these C files can be made with or `make standalone-haskell` for compiler binaries generated with Haskell, or `make standalone` for both the Haskell and OCaml compiler binaries. The binaries are located in `src/ExtractionOcaml/` and `src/ExtractionHaskell/` respectively. -There is a separate compiler binary for each implementation strategy: +There is one compiler binary for all implementation strategies: + + - `fiat_crypto` + +This binary takes arguments for the strategy: - - `saturated_solinas` - - `unsaturated_solinas` - - `word_by_word_montgomery` + - `saturated-solinas` + - `unsaturated-solinas` + - `word-by-word-montgomery` + - `dettman-multiplication` + - `solinas-reduction` + - `base-conversion` Passing no arguments, or passing `-h` or `--help` (or any other invalid arguments) will result in a usage message being printed. These binaries output C code on stdout. Here are some examples of ways to invoke the binaries (from the directories that they live in): # Generate code for 2^255-19 - ./unsaturated_solinas '25519' '64' '5' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c - ./unsaturated_solinas '25519' '32' '10' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c + ./fiat_crypto unsaturated-solinas '25519' '64' '5' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c + ./fiat_crypto unsaturated-solinas '25519' '32' '10' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c # Generate code for NIST-P256 (2^256 - 2^224 + 2^192 + 2^96 - 1) - ./word_by_word_montgomery 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c - ./word_by_word_montgomery 'p256' '64' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_64.c + ./fiat_crypto word-by-word-montgomery 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c + ./fiat_crypto word-by-word-montgomery 'p256' '64' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_64.c You can find more examples in the [`Makefile`](./Makefile). Note that for large primes, you may need to increase the stack size to avoid stack overflows. For example: - ulimit -S -s 1048576; ./word_by_word_montgomery --static gost_512_paramSetB 32 '2^511 + 111' + ulimit -S -s 1048576; ./fiat_crypto word-by-word-montgomery --static gost_512_paramSetB 32 '2^511 + 111' This sets the stack size to 1 GB (= 1024 MB = 1024 * 1024 KB = 1048576 KB) before running the command. As of the last edit of this line, this command takes about an hour to run, but does in fact complete successfully. @@ -124,27 +131,34 @@ Just the compilers generating these bedrock2/C files can be made with or `make standalone-haskell` for binaries generated with Haskell, or `make standalone` for both the Haskell and OCaml binaries. The binaries are located in `src/ExtractionOcaml/` and `src/ExtractionHaskell/` respectively. -There is a separate compiler binary for each implementation strategy: +There is one compiler binary for all implementation strategies: + + - `bedrock2_fiat_crypto` + +This binary takes arguments for the strategy: - - `bedrock2_saturated_solinas` - - `bedrock2_unsaturated_solinas` - - `bedrock2_word_by_word_montgomery` + - `saturated-solinas` + - `unsaturated-solinas` + - `word-by-word-montgomery` + - `dettman-multiplication` + - `solinas-reduction` + - `base-conversion` Passing no arguments, or passing `-h` or `--help` (or any other invalid arguments) will result in a usage message being printed. These binaries output bedrock2/C code on stdout. Here are some examples of ways to invoke the binaries (from the directories that they live in): # Generate code for 2^255-19 - ./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select '25519' '64' '5' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c - ./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select '25519' '32' '10' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c + ./bedrock2_fiat_crypto unsaturated-solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select '25519' '64' '5' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_64.c + ./bedrock2_fiat_crypto unsaturated-solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select '25519' '32' '10' '2^255 - 19' carry_mul carry_square carry_scmul121666 carry add sub opp selectznz to_bytes from_bytes > curve25519_32.c # Generate code for NIST-P256 (2^256 - 2^224 + 2^192 + 2^96 - 1) - ./bedrock2_word_by_word_montgomery --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c - ./bedrock2_word_by_word_montgomery --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'p256' '64' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_64.c + ./bedrock2_fiat_crypto word-by-word-montgomery --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'p256' '32' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_32.c + ./bedrock2_fiat_crypto word-by-word-montgomery --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'p256' '64' '2^256 - 2^224 + 2^192 + 2^96 - 1' > p256_64.c # Generate code for 2^130 - 5 - ./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'poly1305' '64' '3' '2^130 - 5' > poly1305_64.c - ./bedrock2_unsaturated_solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'poly1305' '32' '5' '2^130 - 5' > poly1305_32.c + ./bedrock2_fiat_crypto unsaturated-solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'poly1305' '64' '3' '2^130 - 5' > poly1305_64.c + ./bedrock2_fiat_crypto unsaturated-solinas --no-wide-int --widen-carry --widen-bytes --split-multiret --no-select 'poly1305' '32' '5' '2^130 - 5' > poly1305_32.c You can find more examples in [`Makefile.examples`](./Makefile.examples). diff --git a/src/CLI.v b/src/CLI.v index 36cbd05930e..2e9d71f955e 100644 --- a/src/CLI.v +++ b/src/CLI.v @@ -17,6 +17,7 @@ Require Import Crypto.Util.Strings.NamingConventions. Require Import Crypto.Util.Option. Require Import Crypto.Util.OptionList. Require Import Crypto.Util.Strings.Show. +Require Import Crypto.Util.Strings.Show.Enum. Require Import Crypto.Util.Strings.Sorting. Require Import Crypto.Util.Strings.ParseFlagOptions. Require Import Crypto.Util.DebugMonad. @@ -44,6 +45,32 @@ Import Stringification.C.Compilers. Module ForExtraction. + Variant SynthesisKind : Set := + | word_by_word_montgomery + | unsaturated_solinas + | saturated_solinas + | dettman_multiplication + | solinas_reduction + | base_conversion + . + + Derive SynthesisKind_Listable SuchThat (@FinitelyListable SynthesisKind SynthesisKind_Listable) As SynthesisKind_FinitelyListable. + Proof. prove_ListableDerive. Qed. + Global Existing Instances SynthesisKind_Listable SynthesisKind_FinitelyListable. + + Global Instance show_SynthesisKind : Show SynthesisKind. + Proof. prove_Show_enum (). Defined. + Global Instance show_lvl_SynthesisKind : ShowLevel SynthesisKind := show_SynthesisKind. + + Definition parse_SynthesisKind_list : list (string * SynthesisKind) + := Eval vm_compute in + List.map + (fun r => (String.replace "_" "-" (show r), r)) + (list_all SynthesisKind). + + Definition parse_SynthesisKind_act : ParserAction SynthesisKind + := parse_strs parse_SynthesisKind_list. + Definition parse_string_and {T} (parse_T : string -> option T) (s : string) : option (string * T) := option_map (@pair _ _ s) (parse_T s). Definition parse_Z (s : string) : option Z := parseZ_arith_strict s. @@ -62,6 +89,9 @@ Module ForExtraction. ls <-- List.map ParseArithmetic.Q_to_Z_strict ls; Some ls). + Definition parse_SynthesisKind (s : string) : option SynthesisKind + := finalize parse_SynthesisKind_act s. + Definition parse_list_REG (s : string) : option (list REG) := finalize (parse_comma_list parse_REG) s. @@ -77,9 +107,6 @@ Module ForExtraction. Definition parse_callee_saved_registers (s : string) : option assembly_callee_saved_registers_opt := finalize parse_assembly_callee_saved_registers_opt s. - (* Workaround for lack of notation in 8.8 *) - Local Notation "x =? y" := (if string_dec x y then true else false) : string_scope. - Definition parse_n (n : string) : option MaybeLimbCount := match parse_nat n with | Some n => Some (NumLimbs n) @@ -301,6 +328,10 @@ Module ForExtraction. end)%string special_options)). + Definition synthesis_kind_spec : anon_argT + := ("synthesis_kind", + Arg.CustomSymbol parse_SynthesisKind_list, + ["The algorithm for field arithmetic. Further options depend on the choice of algorithm, and can be viewed by passing -h after this argument. Note that no options other than -h are permitted before this argument."]). Definition curve_description_spec : anon_argT := ("curve_description", Arg.String, @@ -1003,6 +1034,7 @@ Module ForExtraction. end. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1105,6 +1137,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1147,6 +1180,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1182,6 +1216,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1228,6 +1263,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1263,6 +1299,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1331,6 +1368,7 @@ Module ForExtraction. }. Definition PipelineMain + {prog_name_count : Arg.prog_name_countT} {supported_languages : supported_languagesT} {A} {io_driver : IODriverAPI A} @@ -1338,4 +1376,46 @@ Module ForExtraction. : A := Parameterized.PipelineMain argv. End BaseConversion. + + (** The combined binary that delegates *) + Module FiatCrypto. + Definition PipelineMain + {supported_languages : supported_languagesT} + {A} + {io_driver : IODriverAPI A} + (argv : list string) + : A + := let spec + := {| Arg.named_args := [] + ; Arg.anon_args := [synthesis_kind_spec] + ; Arg.anon_opt_args := [] + ; Arg.anon_opt_repeated_arg := None |} in + match Arg.parse_argv (List.firstn 2 argv) spec with + | ErrorT.Success (tt as _named_data, anon_data, tt as _anon_opt_data, tt as _anon_opt_repeated_data) + => let synthesis_kind := anon_data in + let prog_name_count : Arg.prog_name_countT := 2%nat in + match synthesis_kind with + | word_by_word_montgomery + => WordByWordMontgomery.PipelineMain (prog_name_count:=prog_name_count) argv + | unsaturated_solinas + => UnsaturatedSolinas.PipelineMain (prog_name_count:=prog_name_count) argv + | saturated_solinas + => SaturatedSolinas.PipelineMain (prog_name_count:=prog_name_count) argv + | dettman_multiplication + => DettmanMultiplication.PipelineMain (prog_name_count:=prog_name_count) argv + | solinas_reduction + => SolinasReduction.PipelineMain (prog_name_count:=prog_name_count) argv + | base_conversion + => BaseConversion.PipelineMain (prog_name_count:=prog_name_count) argv + end + | ErrorT.Error err + => let display := Arg.show_list_parse_error spec err in + if Arg.is_real_error err + then error display + else (* just a requested help/usage message *) + write_stdout_then + (List.map (fun s => s ++ String.NewLine)%string display) + ret + end. + End FiatCrypto. End ForExtraction. diff --git a/src/ExtractionHaskell/bedrock2_fiat_crypto.v b/src/ExtractionHaskell/bedrock2_fiat_crypto.v new file mode 100644 index 00000000000..509dd3ced04 --- /dev/null +++ b/src/ExtractionHaskell/bedrock2_fiat_crypto.v @@ -0,0 +1,5 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain. +Import Bedrock2First. + +(*Redirect "/tmp/bedrock2_fiat_crypto.hs" *)Recursive Extraction FiatCrypto.main. +(* cat /tmp/bedrock2_fiat_crypto.hs.out | sed -f haskell.sed > ../../bedrock2_fiat_crypto.hs *) diff --git a/src/ExtractionHaskell/fiat_crypto.v b/src/ExtractionHaskell/fiat_crypto.v new file mode 100644 index 00000000000..89a96038958 --- /dev/null +++ b/src/ExtractionHaskell/fiat_crypto.v @@ -0,0 +1,4 @@ +Require Import Crypto.StandaloneHaskellMain. + +(*Redirect "/tmp/fiat_crypto.hs" *)Recursive Extraction FiatCrypto.main. +(* cat /tmp/fiat_crypto.hs.out | sed -f haskell.sed > ../../fiat_crypto.hs *) diff --git a/src/ExtractionHaskell/with_bedrock2_fiat_crypto.v b/src/ExtractionHaskell/with_bedrock2_fiat_crypto.v new file mode 100644 index 00000000000..2b175121a05 --- /dev/null +++ b/src/ExtractionHaskell/with_bedrock2_fiat_crypto.v @@ -0,0 +1,5 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneHaskellMain. +Import Bedrock2Later. + +(*Redirect "/tmp/bedrock2_fiat_crypto.hs" *)Recursive Extraction FiatCrypto.main. +(* cat /tmp/bedrock2_fiat_crypto.hs.out | sed -f haskell.sed > ../../bedrock2_fiat_crypto.hs *) diff --git a/src/ExtractionOCaml/bedrock2_fiat_crypto.v b/src/ExtractionOCaml/bedrock2_fiat_crypto.v new file mode 100644 index 00000000000..a2b85f8dc8c --- /dev/null +++ b/src/ExtractionOCaml/bedrock2_fiat_crypto.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. +Import Bedrock2First. + +Extraction "src/ExtractionOCaml/bedrock2_fiat_crypto.tmp" FiatCrypto.main. diff --git a/src/ExtractionOCaml/fiat_crypto.v b/src/ExtractionOCaml/fiat_crypto.v new file mode 100644 index 00000000000..fcd64cad02f --- /dev/null +++ b/src/ExtractionOCaml/fiat_crypto.v @@ -0,0 +1,3 @@ +Require Import Crypto.StandaloneOCamlMain. + +Extraction "src/ExtractionOCaml/fiat_crypto.tmp" FiatCrypto.main. diff --git a/src/ExtractionOCaml/with_bedrock2_fiat_crypto.v b/src/ExtractionOCaml/with_bedrock2_fiat_crypto.v new file mode 100644 index 00000000000..70b1716025e --- /dev/null +++ b/src/ExtractionOCaml/with_bedrock2_fiat_crypto.v @@ -0,0 +1,4 @@ +Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. +Import Bedrock2Later. + +Extraction "src/ExtractionOCaml/with_bedrock2_fiat_crypto.tmp" FiatCrypto.main. diff --git a/src/StandaloneDebuggingExamples.v b/src/StandaloneDebuggingExamples.v index 0cabb7f19b8..4016d40f1c6 100644 --- a/src/StandaloneDebuggingExamples.v +++ b/src/StandaloneDebuggingExamples.v @@ -42,13 +42,13 @@ Module debugging_no_asm. ;" mov [ rsp + 0x58 ], r14; saving to stack" ])) by admit. clearbody k; subst k. - set (k := string_dec _ _) in (value of v) at 1; vm_compute in k; subst k; cbv beta iota in v. + set (k := (_ =? _)%string) in (value of v) at 1; vm_compute in k; subst k; cbv beta iota in v. vm_compute ForExtraction.parse_args in v. cbv beta iota zeta in v. vm_compute concat in v. cbv [ForExtraction.output_file_name ForExtraction.asm_output_file_name] in v. cbn [Option.sequence_return nth_error] in v. - set (k := string_dec _ _) in (value of v). + set (k := (_ =? _)%string) in (value of v). vm_compute in k; subst k. cbv beta iota zeta in v. cbv [ForExtraction.Parameterized.Pipeline] in v. @@ -57,7 +57,7 @@ Module debugging_no_asm. cbv [ForExtraction.UnsaturatedSolinas.api] in v. cbn [fst snd] in v. repeat (set (x := ((_ ++ _)%string)) in (value of v) at 1; vm_compute in x; subst x). - repeat (set (x := string_dec _ _) in (value of v) at 1; vm_compute in x; subst x). + repeat (set (x := (_ =? _)%string) in (value of v) at 1; vm_compute in x; subst x). cbv beta iota zeta in v. repeat (set (x := ((_ ++ _)%list)) in (value of v) at 1; vm_compute in x; subst x). cbv [ForExtraction.Synthesize] in v. @@ -134,7 +134,7 @@ Module debugging_typedef_bounds. vm_compute concat in v. cbv [ForExtraction.output_file_name ForExtraction.asm_output_file_name] in v. cbn [Option.sequence_return nth_error] in v. - set (k := string_dec _ _) in (value of v). + set (k := (_ =? _)%string) in (value of v). vm_compute in k; subst k. cbv beta iota zeta in v. cbv [ForExtraction.Parameterized.Pipeline] in v. @@ -143,7 +143,7 @@ Module debugging_typedef_bounds. cbv [ForExtraction.UnsaturatedSolinas.api] in v. cbn [fst snd] in v. repeat (set (x := ((_ ++ _)%string)) in (value of v) at 1; vm_compute in x; subst x). - repeat (set (x := string_dec _ _) in (value of v) at 1; vm_compute in x; subst x). + repeat (set (x := (_ =? _)%string) in (value of v) at 1; vm_compute in x; subst x). cbv beta iota zeta in v. repeat (set (x := ((_ ++ _)%list)) in (value of v) at 1; vm_compute in x; subst x). cbv [ForExtraction.Synthesize] in v. diff --git a/src/StandaloneHaskellMain.v b/src/StandaloneHaskellMain.v index b6e2923a96f..ac897510e81 100644 --- a/src/StandaloneHaskellMain.v +++ b/src/StandaloneHaskellMain.v @@ -144,3 +144,8 @@ Module BaseConversion. Definition main : IO_unit := main_gen ForExtraction.BaseConversion.PipelineMain. End BaseConversion. + +Module FiatCrypto. + Definition main : IO_unit + := main_gen ForExtraction.FiatCrypto.PipelineMain. +End FiatCrypto. diff --git a/src/StandaloneOCamlMain.v b/src/StandaloneOCamlMain.v index 2a19c9baee6..9c7710a56ff 100644 --- a/src/StandaloneOCamlMain.v +++ b/src/StandaloneOCamlMain.v @@ -233,3 +233,8 @@ Module BaseConversion. Definition main : unit := main_gen ForExtraction.BaseConversion.PipelineMain. End BaseConversion. + +Module FiatCrypto. + Definition main : unit + := main_gen ForExtraction.FiatCrypto.PipelineMain. +End FiatCrypto. diff --git a/src/Util/Arg.v b/src/Util/Arg.v index f61be6b2807..3e9ea65ef82 100644 --- a/src/Util/Arg.v +++ b/src/Util/Arg.v @@ -548,15 +548,24 @@ Definition default_named_results {ls} | (_, s, _) :: ss => @default_named_results' _ ss default_named_result end. -Definition parse_argv (argv : list string) (arg_spec : arg_spec) +Class prog_name_countT := prog_name_count : nat. +Global Typeclasses Opaque prog_name_countT. +Ltac fill_default_prog_name_countT _ + := lazymatch goal with + | [ H : prog_name_countT |- prog_name_countT ] => exact H + | [ |- prog_name_countT ] => exact 1%nat + end. +Global Hint Extern 1 prog_name_countT => fill_default_prog_name_countT () : typeclass_instances. + +Definition parse_argv {prog_name_count : prog_name_countT} (argv : list string) (arg_spec : arg_spec) : parse_result (arg_spec_results arg_spec) - := match argv with - | nil => Error missing_prog_name - | prog_name :: argv - => (res <- consume_args (10 + (List.length argv)) argv arg_spec (missing prog_name) (wrong prog_name) (too_many_args prog_name) (internal_error prog_name) (no_keyed_arg prog_name) (help prog_name) (out_of_fuel prog_name); + := if (List.length argv false | _ => true end.