diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml index 91ae5187a8..c785ac7f90 100644 --- a/.github/workflows/coq-alpine.yml +++ b/.github/workflows/coq-alpine.yml @@ -42,166 +42,6 @@ jobs: - name: chroot build params shell: alpine.sh {0} run: etc/ci/describe-system-config.sh - - name: etc/ci/github-actions-make.sh deps + - name: bench garagedoor shell: alpine.sh {0} - run: etc/ci/github-actions-make.sh -j2 deps - - name: all-except-generated-and-js-of-ocaml - shell: alpine.sh {0} - run: etc/ci/github-actions-make.sh -j2 CAMLEXTRAFLAGS="-ccopt -static" all-except-generated-and-js-of-ocaml - - name: install-standalone-unified-ocaml - shell: alpine.sh {0} - run: make install-standalone-unified-ocaml BINDIR=dist -# - name: install-standalone-js-of-ocaml -# shell: alpine.sh {0} -# run: make install-standalone-js-of-ocaml - - name: upload standalone files - uses: actions/upload-artifact@v3 - with: - name: standalone-${{ matrix.alpine }} - path: dist/fiat_crypto -# - name: upload standalone js files -# uses: actions/upload-artifact@v3 -# with: -# name: standalone-html-${{ matrix.alpine }} -# path: fiat-html - - name: upload OCaml files - uses: actions/upload-artifact@v3 - with: - name: ExtractionOCaml-${{ matrix.alpine }} - path: src/ExtractionOCaml - if: always () -# - name: upload js_of_ocaml files -# uses: actions/upload-artifact@v3 -# with: -# name: ExtractionJsOfOCaml-${{ matrix.alpine }} -# path: src/ExtractionJsOfOCaml -# if: always () - - name: generated-files - shell: alpine.sh {0} - run: etc/ci/github-actions-make.sh -j2 generated-files - - run: tar -czvf generated-files.tgz fiat-*/ - if: ${{ failure() }} - - name: upload generated files - uses: actions/upload-artifact@v3 - with: - name: generated-files-${{ matrix.alpine }} - path: generated-files.tgz - if: ${{ failure() }} - - name: standalone-haskell - shell: alpine.sh {0} - run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS' - - name: upload Haskell files - uses: actions/upload-artifact@v3 - with: - name: ExtractionHaskell-${{ matrix.alpine }} - path: src/ExtractionHaskell - if: always () - - name: only-test-amd64-files-lite - shell: alpine.sh {0} - run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1 - - name: install - shell: alpine.sh {0} - run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml - - name: install-without-bedrock2 - shell: alpine.sh {0} - run: sudo make EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml - - name: install-dev - shell: alpine.sh {0} - run: sudo make EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml - - name: display timing info - run: cat time-of-build-pretty.log || true - - name: display per-line timing info - run: etc/ci/github-actions-display-per-line-timing.sh - - test-standalone: - strategy: - fail-fast: false - matrix: - include: - - alpine: 'edge' -# - alpine: 'latest-stable' - runs-on: ubuntu-latest - name: test-standalone-${{ matrix.alpine }} - needs: build - steps: - - uses: actions/checkout@v4 - - name: Download standalone ${{ matrix.alpine }} - uses: actions/download-artifact@v3 - with: - name: standalone-${{ matrix.alpine }} - path: dist/ - - name: List files - run: find dist - - run: chmod +x dist/fiat_crypto - - name: Test files (host) - run: | - echo "::group::file fiat_crypto" - file dist/fiat_crypto - echo "::endgroup::" - echo "::group::ldd fiat_crypto" - ldd dist/fiat_crypto || true - echo "::endgroup::" - etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto - - uses: jirutka/setup-alpine@v1 - with: - branch: ${{ matrix.alpine }} - extra-repositories: https://dl-cdn.alpinelinux.org/alpine/edge/testing - - name: Test files (container) - shell: alpine.sh {0} - run: etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto - - publish-standalone: - runs-on: ubuntu-latest - needs: build - permissions: - contents: write # IMPORTANT: mandatory for making GitHub Releases - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 # Fetch all history for all tags and branches - tags: true # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version - - name: Download standalone edge - uses: actions/download-artifact@v3 - with: - name: standalone-edge - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - echo "::group::find arch" - arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Linux_${arch}" - echo "$fname" - mv dist/fiat_crypto "dist/$fname" - find dist - file "dist/$fname" - - name: Upload artifacts to GitHub Release - env: - GITHUB_TOKEN: ${{ github.token }} - # Upload to GitHub Release using the `gh` CLI. - # `dist/` contains the built packages - run: >- - gh release upload - '${{ github.ref_name }}' dist/** - --repo '${{ github.repository }}' - if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }} - - alpine-check-all: - runs-on: ubuntu-latest - needs: [build, test-standalone, publish-standalone] - if: always() - steps: - - run: echo 'build passed' - if: ${{ needs.build.result == 'success' }} - - run: echo 'test-standalone passed' - if: ${{ needs.test-standalone.result == 'success' }} - - run: echo 'publish-standalone passed' - if: ${{ needs.publish-standalone.result == 'success' }} - - run: echo 'build failed' && false - if: ${{ needs.build.result != 'success' }} - - run: echo 'test-standalone failed' && false - if: ${{ needs.test-standalone.result != 'success' }} - - run: echo 'publish-standalone failed' && false - if: ${{ needs.publish-standalone.result != 'success' }} + run: /usr/bin/time -v make -j src/Bedrock/End2End/X25519/GarageDoorTop.vo diff --git a/.github/workflows/coq-archlinux.yml b/.github/workflows/coq-archlinux.yml index 71beb5334d..b9d1763378 100644 --- a/.github/workflows/coq-archlinux.yml +++ b/.github/workflows/coq-archlinux.yml @@ -38,147 +38,5 @@ jobs: run: git config --global --add safe.directory "*" - name: chroot build params run: etc/ci/describe-system-config.sh - - name: make deps - run: etc/ci/github-actions-make.sh -j2 deps - - name: all-except-generated-and-js-of-ocaml - run: etc/ci/github-actions-make.sh -j2 all-except-generated-and-js-of-ocaml - - name: generated-files - run: etc/ci/github-actions-make.sh -j2 generated-files - - run: tar -czvf generated-files.tgz fiat-*/ - if: ${{ failure() }} - - name: upload generated files - uses: actions/upload-artifact@v3 - with: - name: generated-files-archlinux - path: generated-files.tgz - if: ${{ failure() }} - - name: install-standalone-unified-ocaml - run: etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist - #- name: standalone-js-of-ocaml - # run: etc/ci/github-actions-make.sh -j2 standalone-js-of-ocaml - #- name: install-standalone-js-of-ocaml - # run: etc/ci/github-actions-make.sh install-standalone-js-of-ocaml - - name: upload standalone files - uses: actions/upload-artifact@v3 - with: - name: standalone-archlinux - path: dist/fiat_crypto - #- name: upload standalone js files - # uses: actions/upload-artifact@v3 - # with: - # name: standalone-html-archlinux - # path: fiat-html - - name: upload OCaml files - uses: actions/upload-artifact@v3 - with: - name: ExtractionOCaml-archlinux - path: src/ExtractionOCaml - if: always () - #- name: upload js_of_ocaml files - # uses: actions/upload-artifact@v3 - # with: - # name: ExtractionJsOfOCaml-archlinux - # path: src/ExtractionJsOfOCaml - # if: always () - - name: standalone-haskell - run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS' - - name: upload Haskell files - uses: actions/upload-artifact@v3 - with: - name: ExtractionHaskell-archlinux - path: src/ExtractionHaskell - if: always () - - name: only-test-amd64-files-lite - run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1 - - name: install - run: etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml - - name: install-without-bedrock2 - run: etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml - - name: install-dev - run: etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml - - name: display timing info - run: cat time-of-build-pretty.log - - name: display per-line timing info - run: etc/ci/github-actions-display-per-line-timing.sh - - test-standalone: - runs-on: ubuntu-latest - container: archlinux - needs: build - steps: - - name: Install system dependencies - run: | - pacman --noconfirm -Syu git --needed - - uses: actions/checkout@v4 - - name: Download standalone archlinux - uses: actions/download-artifact@v3 - with: - name: standalone-archlinux - path: dist/ - - name: List files - run: find dist - - run: chmod +x dist/fiat_crypto - - name: Test files (container) - run: | - echo "::group::file fiat_crypto" - file dist/fiat_crypto - echo "::endgroup::" - echo "::group::ldd fiat_crypto" - ldd dist/fiat_crypto - echo "::endgroup::" - etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto - - publish-standalone-dry-run: - runs-on: ubuntu-latest - needs: build -# permissions: -# contents: write # IMPORTANT: mandatory for making GitHub Releases - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 # Fetch all history for all tags and branches - tags: true # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version - - name: Download standalone archlinux - uses: actions/download-artifact@v3 - with: - name: standalone-archlinux - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - echo "::group::find arch" - arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Linux_archlinux_${arch}" - echo "$fname" - mv dist/fiat_crypto "dist/$fname" - find dist -# - name: Upload artifacts to GitHub Release -# env: -# GITHUB_TOKEN: ${{ github.token }} -# # Upload to GitHub Release using the `gh` CLI. -# # `dist/` contains the built packages -# run: >- -# gh release upload -# '${{ github.ref_name }}' dist/** -# --repo '${{ github.repository }}' -# if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }} - - archlinux-check-all: - runs-on: ubuntu-latest - needs: [build, test-standalone, publish-standalone-dry-run] - if: always() - steps: - - run: echo 'build passed' - if: ${{ needs.build.result == 'success' }} - - run: echo 'test-standalone passed' - if: ${{ needs.test-standalone.result == 'success' }} - - run: echo 'publish-standalone-dry-run passed' - if: ${{ needs.publish-standalone-dry-run.result == 'success' }} - - run: echo 'build failed' && false - if: ${{ needs.build.result != 'success' }} - - run: echo 'test-standalone failed' && false - if: ${{ needs.test-standalone.result != 'success' }} - - run: echo 'publish-standalone-dry-run failed' && false - if: ${{ needs.publish-standalone-dry-run.result != 'success' }} + - name: bench garagedoor + run: /usr/bin/time -v make -j src/Bedrock/End2End/X25519/GarageDoorTop.vo diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml index cd6199912b..ecf6242b69 100644 --- a/.github/workflows/coq-debian.yml +++ b/.github/workflows/coq-debian.yml @@ -40,172 +40,6 @@ jobs: - name: chroot build params shell: in-debian-chroot.sh {0} run: CI=1 etc/ci/describe-system-config.sh - - name: make deps + - name: bench garagedoor shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j2 deps - - name: all-except-generated-and-js-of-ocaml - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j2 all-except-generated-and-js-of-ocaml - - name: generated-files - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j2 generated-files - - run: tar -czvf generated-files.tgz fiat-*/ - if: ${{ failure() }} - - name: upload generated files - uses: actions/upload-artifact@v3 - with: - name: generated-files-${{ matrix.env.DEBIAN }} - path: generated-files.tgz - if: ${{ failure() }} - - name: install-standalone-unified-ocaml - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist - - name: standalone-js-of-ocaml - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j2 standalone-js-of-ocaml - - name: install-standalone-js-of-ocaml - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh install-standalone-js-of-ocaml - - name: upload standalone files - uses: actions/upload-artifact@v3 - with: - name: standalone-${{ matrix.env.DEBIAN }} - path: dist/fiat_crypto - - name: upload standalone js files - uses: actions/upload-artifact@v3 - with: - name: standalone-html-${{ matrix.env.DEBIAN }} - path: fiat-html - - name: upload OCaml files - uses: actions/upload-artifact@v3 - with: - name: ExtractionOCaml-${{ matrix.env.DEBIAN }} - path: src/ExtractionOCaml - if: always () - - name: upload js_of_ocaml files - uses: actions/upload-artifact@v3 - with: - name: ExtractionJsOfOCaml-${{ matrix.env.DEBIAN }} - path: src/ExtractionJsOfOCaml - if: always () - - name: standalone-haskell - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS' - - name: upload Haskell files - uses: actions/upload-artifact@v3 - with: - name: ExtractionHaskell-${{ matrix.env.DEBIAN }} - path: src/ExtractionHaskell - if: always () - - name: only-test-amd64-files-lite - shell: in-debian-chroot.sh {0} - run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1 - - name: install - shell: in-debian-chroot.sh {0} - run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml - - name: install-without-bedrock2 - shell: in-debian-chroot.sh {0} - run: sudo etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml - - name: install-dev - shell: in-debian-chroot.sh {0} - run: sudo etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml - - name: display timing info - run: cat time-of-build-pretty.log - - name: display per-line timing info - run: etc/ci/github-actions-display-per-line-timing.sh - - test-standalone: - strategy: - fail-fast: false - matrix: - include: - - debian: sid - #- debian: bookworm # restore once 8.17 lands in Debian stable - runs-on: ubuntu-latest - needs: build - steps: - - uses: actions/checkout@v4 - - name: Download standalone ${{ matrix.debian }} - uses: actions/download-artifact@v3 - with: - name: standalone-${{ matrix.debian }} - path: dist/ - - name: List files - run: find dist - - run: chmod +x dist/fiat_crypto - - name: Test files (host) - run: | - echo "::group::file fiat_crypto" - file dist/fiat_crypto - echo "::endgroup::" - echo "::group::ldd fiat_crypto" - ldd dist/fiat_crypto - echo "::endgroup::" - etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto - - name: setup Debian chroot - run: etc/ci/setup-debian-chroot.sh "${{ matrix.debian }}" - - name: Test files (container) - shell: in-debian-chroot.sh {0} - run: | - echo "::group::file fiat_crypto" - file dist/fiat_crypto - echo "::endgroup::" - echo "::group::ldd fiat_crypto" - ldd dist/fiat_crypto - echo "::endgroup::" - etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto - - publish-standalone-dry-run: - runs-on: ubuntu-latest - needs: build -# permissions: -# contents: write # IMPORTANT: mandatory for making GitHub Releases - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 # Fetch all history for all tags and branches - tags: true # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version - - name: Download standalone sid - uses: actions/download-artifact@v3 - with: - name: standalone-sid - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - echo "::group::find arch" - arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Linux_debian_sid_${arch}" - echo "$fname" - mv dist/fiat_crypto "dist/$fname" - find dist -# - name: Upload artifacts to GitHub Release -# env: -# GITHUB_TOKEN: ${{ github.token }} -# # Upload to GitHub Release using the `gh` CLI. -# # `dist/` contains the built packages -# run: >- -# gh release upload -# '${{ github.ref_name }}' dist/** -# --repo '${{ github.repository }}' -# if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }} - - debian-check-all: - runs-on: ubuntu-latest - needs: [build, test-standalone, publish-standalone-dry-run] - if: always() - steps: - - run: echo 'build passed' - if: ${{ needs.build.result == 'success' }} - - run: echo 'test-standalone passed' - if: ${{ needs.test-standalone.result == 'success' }} - - run: echo 'publish-standalone-dry-run passed' - if: ${{ needs.publish-standalone-dry-run.result == 'success' }} - - run: echo 'build failed' && false - if: ${{ needs.build.result != 'success' }} - - run: echo 'test-standalone failed' && false - if: ${{ needs.test-standalone.result != 'success' }} - - run: echo 'publish-standalone-dry-run failed' && false - if: ${{ needs.publish-standalone-dry-run.result != 'success' }} + run: /usr/bin/time -v make -j src/Bedrock/End2End/X25519/GarageDoorTop.vo diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml index 28680c4b76..f2a4d82deb 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq-docker.yml @@ -43,497 +43,10 @@ jobs: custom_script: | eval $(opam env) etc/ci/describe-system-config.sh - - name: deps + - name: bench uses: coq-community/docker-coq-action@v1 with: coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: etc/ci/github-actions-docker-make.sh COQBIN="$(dirname "$(which coqc)")/" -j2 deps - - name: all-except-generated-and-js-of-ocaml - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated-and-js-of-ocaml - - name: pre-standalone-extracted - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 pre-standalone-extracted - - name: upload OCaml files - uses: actions/upload-artifact@v3 - with: - name: ExtractionOCaml-${{ matrix.env.COQ_VERSION }} - path: src/ExtractionOCaml - if: always () - - name: upload js_of_ocaml source files - uses: actions/upload-artifact@v3 - with: - name: ExtractionJsOfOCaml-source-${{ matrix.env.COQ_VERSION }} - path: src/ExtractionJsOfOCaml - if: always () - - name: upload Haskell source files - uses: actions/upload-artifact@v3 - with: - name: ExtractionHaskell-source-${{ matrix.env.COQ_VERSION }} - path: src/ExtractionHaskell - if: always () - - 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: dist/fiat_crypto - - run: git config --file .gitmodules --get-regexp path | awk '{ print $2 }' | xargs tar -czvf fiat-crypto-build.tar.gz src - - name: Upload built files - uses: actions/upload-artifact@v3 - with: - name: build-outputs-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }}-ocaml-${{ matrix.env.DOCKER_OCAML_VERSION }} - path: fiat-crypto-build.tar.gz - - name: install - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: | - sudo git config --global --add safe.directory "*" - sudo make EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 COQBIN="$(dirname "$(which coqc)")/" install install-standalone-ocaml - - name: install-without-bedrock2 - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: | - sudo git config --global --add safe.directory "*" - sudo make EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 COQBIN="$(dirname "$(which coqc)")/" install-without-bedrock2 install-standalone-ocaml - - name: install-dev - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: | - sudo git config --global --add safe.directory "*" - sudo make EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 COQBIN="$(dirname "$(which coqc)")/" install install-standalone-ocaml - - name: display timing info - run: cat time-of-build-pretty.log - - name: display per-line timing info - run: etc/ci/github-actions-display-per-line-timing.sh - - validate: - strategy: - fail-fast: false - matrix: - include: - - env: { COQ_VERSION: "master", DOCKER_COQ_VERSION: "dev", DOCKER_OCAML_VERSION: "default", SKIP_VALIDATE: "" , COQCHKEXTRAFLAGS: "-bytecode-compiler yes", EXTRA_GH_REPORTIFY: "--warnings", ALLOW_DIFF: "1", CI: "1" } - os: 'ubuntu-latest' - - runs-on: ${{ matrix.os }} - env: ${{ matrix.env }} - name: validate-docker-${{ matrix.env.COQ_VERSION }} - - concurrency: - group: ${{ github.workflow }}-validate-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - - needs: build - - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Download a Build Artifact - uses: actions/download-artifact@v3 - with: - name: build-outputs-docker-coq-${{ matrix.env.DOCKER_COQ_VERSION }}-ocaml-${{ matrix.env.DOCKER_OCAML_VERSION }} - path: . - - name: Unpack build artifact - run: tar --overwrite -xzvf fiat-crypto-build.tar.gz - - name: validate - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} - ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF COQCHKEXTRAFLAGS - custom_script: etc/ci/github-actions-docker-make.sh TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}" - if: env.SKIP_VALIDATE == '' && github.event_name != 'pull_request' - - build-js-of-ocaml: - needs: build - runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - coq-version: [ 'master' ] - ocaml-compiler: [ '4.11.1' ] - concurrency: - group: ${{ github.workflow }}-build-js-of-ocaml-${{ matrix.coq-version }}-${{ matrix.ocaml-compiler }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Set up OCaml - uses: ocaml/setup-ocaml@v2 - with: - ocaml-compiler: ${{ matrix.ocaml-compiler }} - - name: opam install deps - run: | - eval $(opam env) - opam update -y - opam install -y js_of_ocaml ocamlfind - - name: echo build params - run: etc/ci/describe-system-config.sh - - name: Download a Build Artifact - uses: actions/download-artifact@v3 - with: - name: ExtractionJsOfOCaml-source-${{ matrix.coq-version }} - path: src/ExtractionJsOfOCaml - - name: standalone-js-of-ocaml - run: | - eval $(opam env) - etc/ci/github-actions-make.sh --warnings -f Makefile.standalone -j2 standalone-js-of-ocaml - - name: install-standalone-js-of-ocaml - run: make -f Makefile.standalone install-standalone-js-of-ocaml - - name: upload js_of_ocaml build files - uses: actions/upload-artifact@v3 - with: - name: ExtractionJsOfOCaml-${{ matrix.coq-version }}-ocaml-${{ matrix.ocaml-compiler }} - path: src/ExtractionJsOfOCaml - if: always () - - name: Upload js_of_ocaml outputs - uses: actions/upload-artifact@v3 - with: - name: fiat-html-js-of-ocaml - path: fiat-html - - build-wasm-of-ocaml: - needs: build - runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - coq-version: [ 'master' ] - ocaml-compiler: [ '4.14.1' ] - concurrency: - group: ${{ github.workflow }}-build-wasm-of-ocaml-${{ matrix.coq-version }}-${{ matrix.ocaml-compiler }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Set up OCaml - uses: ocaml/setup-ocaml@v2 - with: - ocaml-compiler: ${{ matrix.ocaml-compiler }} - - name: echo build params - run: etc/ci/describe-system-config.sh - - name: Set up binaryen >= 116 - uses: acifani/setup-tinygo@v2 - with: - tinygo-version: '0.30.0' - binaryen-version: '117' - - name: set up custom dune and wasm_of_ocaml - run: | - eval $(opam env) - opam update -y - opam pin add -y 'https://github.com/ocaml-wasm/dune.git#wasm' - opam pin add -y --no-action --cli=2.1 --with-version 5.3.0 https://github.com/ocaml-wasm/wasm_of_ocaml.git - - name: install wasm_of_ocaml - run: | - eval $(opam env) - opam install -y wasm_of_ocaml-compiler ocamlfind - - name: echo build params - run: etc/ci/describe-system-config.sh - - name: Download a Build Artifact - uses: actions/download-artifact@v3 - with: - name: ExtractionJsOfOCaml-source-${{ matrix.coq-version }} - path: src/ExtractionJsOfOCaml - - name: standalone-wasm-of-ocaml - run: | - eval $(opam env) - etc/ci/github-actions-make.sh --warnings -f Makefile.standalone -j2 standalone-wasm-of-ocaml - - name: install-standalone-wasm-of-ocaml - run: make -f Makefile.standalone install-standalone-wasm-of-ocaml - - name: upload wasm_of_ocaml build files - uses: actions/upload-artifact@v3 - with: - name: ExtractionJsOfOCaml-${{ matrix.coq-version }}-ocaml-${{ matrix.ocaml-compiler }}+wasm - path: src/ExtractionJsOfOCaml - if: always () - - name: Upload wasm_of_ocaml outputs - uses: actions/upload-artifact@v3 - with: - name: fiat-html-wasm-of-ocaml - path: fiat-html - - deploy-js-wasm-of-ocaml: - needs: [build-js-of-ocaml, build-wasm-of-ocaml] - runs-on: ubuntu-latest - concurrency: - group: ${{ github.workflow }}-deploy-js-wasm-of-ocaml-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - fetch-depth: 0 # Fetch all history for all tags and branches, for fiat-html/version.js - tags: true # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version - - name: Download a Build Artifact - uses: actions/download-artifact@v3 - with: - name: fiat-html-js-of-ocaml - path: fiat-html - - run: find fiat-html - - run: ls -la fiat-html - - name: Download a Build Artifact - uses: actions/download-artifact@v3 - with: - name: fiat-html-wasm-of-ocaml - path: fiat-html - - run: find fiat-html - - run: ls -la fiat-html - - run: make -f Makefile.js-html fiat-html/version.js - - run: find fiat-html - - run: ls -la fiat-html - - name: backup .gitignore - run: mv .gitignore{,.bak} - - name: Deploy js_of_ocaml and wasm_of_ocaml 🚀 ${{ ( github.ref != 'refs/heads/master' && '(dry run)' ) || '' }} - uses: JamesIves/github-pages-deploy-action@v4.5.0 - with: - branch: gh-pages # The branch the action should deploy to. - folder: fiat-html # The folder the action should deploy. - git-config-email: JasonGross@users.noreply.github.com - target-folder: . - single-commit: true # otherwise the repo will get too big - dry-run: ${{ github.ref != 'refs/heads/master' }} - - name: restore .gitignore - run: mv .gitignore{.bak,} - - - generated-files: - needs: build - runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - coq-version: [ 'master' ] - concurrency: - group: ${{ github.workflow }}-generated-files-${{ matrix.coq-version }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Download a Build Artifact - uses: actions/download-artifact@v3 - with: - name: ExtractionOCaml-${{ matrix.coq-version }} - path: src/ExtractionOCaml - - name: make binaries executable - run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x - - name: generated-files - run: etc/ci/github-actions-make.sh --warnings -f Makefile.examples -j2 generated-files - if: github.event_name == 'pull_request' - - run: tar -czvf generated-files.tgz fiat-*/ - if: ${{ failure() }} - - name: upload generated files - uses: actions/upload-artifact@v3 - with: - name: generated-files-${{ matrix.coq-version }} - path: generated-files.tgz - if: ${{ failure() }} - - standalone-haskell: - needs: build - runs-on: ubuntu-latest - strategy: - fail-fast: false - matrix: - coq-version: [ 'master' ] - concurrency: - group: ${{ github.workflow }}-standalone-haskell-${{ matrix.coq-version }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - steps: - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Download a Build Artifact - uses: actions/download-artifact@v3 - with: - name: ExtractionHaskell-source-${{ matrix.coq-version }} - path: src/ExtractionHaskell - - name: standalone-haskell - run: etc/ci/github-actions-make.sh -f Makefile.standalone -j1 standalone-haskell GHCFLAGS='+RTS -M7G -RTS' - - name: upload Haskell files - uses: actions/upload-artifact@v3 - with: - name: ExtractionHaskell-${{ matrix.coq-version }} - path: src/ExtractionHaskell - if: always () - - - test-amd64: - - runs-on: ubuntu-latest - - concurrency: - group: ${{ github.workflow }}-test-amd64-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - needs: build - - steps: - - name: checkout repo - uses: actions/checkout@v4 - with: - submodules: recursive - - name: Download a Build Artifact - uses: actions/download-artifact@v3 - with: - name: ExtractionOCaml-master - path: src/ExtractionOCaml - - name: make binaries executable - run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x - - name: only-test-amd64-files - run: etc/ci/github-actions-make.sh -f Makefile.examples -j2 only-test-amd64-files SLOWEST_FIRST=1 - env: - ALLOW_DIFF: 1 - - test-standalone: - strategy: - fail-fast: false - matrix: - include: - - coq-version: master - docker-coq-version: dev - docker-ocaml-version: default - - runs-on: ubuntu-latest - needs: build - steps: - - uses: actions/checkout@v4 - - name: Download standalone Docker - uses: actions/download-artifact@v3 - with: - name: standalone-docker-coq-${{ matrix.docker-coq-version }} - path: dist/ - - name: List files - run: find dist - - run: chmod +x dist/fiat_crypto - - name: Test files (host) - run: | - echo "::group::file fiat_crypto" - file dist/fiat_crypto - echo "::endgroup::" - echo "::group::ldd fiat_crypto" - ldd dist/fiat_crypto - echo "::endgroup::" - etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto - - name: Test files (container) - uses: coq-community/docker-coq-action@v1 - with: - coq_version: ${{ matrix.docker-coq-version }} - ocaml_version: ${{ matrix.docker-ocaml-version }} - custom_script: | - echo "::group::install dependencies" - sudo apt-get update -y - sudo apt-get install -y file - echo "::endgroup::" - echo "::group::file fiat_crypto" - file dist/fiat_crypto - echo "::endgroup::" - echo "::group::ldd fiat_crypto" - ldd dist/fiat_crypto - echo "::endgroup::" - etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto - - publish-standalone-dry-run: - runs-on: ubuntu-latest - needs: build -# permissions: -# contents: write # IMPORTANT: mandatory for making GitHub Releases - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 # Fetch all history for all tags and branches - tags: true # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version - - name: Download standalone Docker - uses: actions/download-artifact@v3 - with: - name: standalone-docker-coq-dev - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - echo "::group::find arch" - arch="$(etc/ci/find-arch.sh dist/fiat_crypto "unknown")" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Linux_docker_dev_${arch}" - echo "$fname" - mv dist/fiat_crypto "dist/$fname" - find dist -# - name: Upload artifacts to GitHub Release -# env: -# GITHUB_TOKEN: ${{ github.token }} -# # Upload to GitHub Release using the `gh` CLI. -# # `dist/` contains the built packages -# run: >- -# gh release upload -# '${{ github.ref_name }}' dist/** -# --repo '${{ github.repository }}' -# if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }} - - docker-check-all: - runs-on: ubuntu-latest - needs: [build, validate, build-js-of-ocaml, build-wasm-of-ocaml, deploy-js-wasm-of-ocaml, generated-files, standalone-haskell, test-amd64, test-standalone, publish-standalone-dry-run] - if: always() - steps: - - run: echo 'build passed' - if: ${{ needs.build.result == 'success' }} - - run: echo 'validate passed' - if: ${{ needs.validate.result == 'success' }} - - run: echo 'build-js-of-ocaml passed' - if: ${{ needs.build-js-of-ocaml.result == 'success' }} - - run: echo 'build-wasm-of-ocaml passed' - if: ${{ needs.build-wasm-of-ocaml.result == 'success' }} - - run: echo 'deploy-js-wasm-of-ocaml passed' - if: ${{ needs.deploy-js-wasm-of-ocaml.result == 'success' }} - - run: echo 'generated-files passed' - if: ${{ needs.generated-files.result == 'success' }} - - run: echo 'standalone-haskell passed' - if: ${{ needs.standalone-haskell.result == 'success' }} - - run: echo 'test-amd64 passed' - if: ${{ needs.test-amd64.result == 'success' }} - - run: echo 'test-standalone passed' - if: ${{ needs.test-standalone.result == 'success' }} - - run: echo 'publish-standalone-dry-run passed' - if: ${{ needs.publish-standalone-dry-run.result == 'success' }} - - run: echo 'build failed' && false - if: ${{ needs.build.result != 'success' }} - - run: echo 'validate failed' && false - if: ${{ needs.validate.result != 'success' }} - - run: echo 'build-js-of-ocaml failed' && false - if: ${{ needs.build-js-of-ocaml.result != 'success' }} - - run: echo 'build-wasm-of-ocaml failed' && false - if: ${{ needs.build-wasm-of-ocaml.result != 'success' }} - - run: echo 'deploy-js-wasm-of-ocaml failed' && false - if: ${{ needs.deploy-js-wasm-of-ocaml.result != 'success' }} - - run: echo 'generated-files failed' && false - if: ${{ needs.generated-files.result != 'success' }} - - run: echo 'standalone-haskell failed' && false - if: ${{ needs.standalone-haskell.result != 'success' }} - - run: echo 'test-amd64 failed' && false - if: ${{ needs.test-amd64.result != 'success' }} - - run: echo 'test-standalone failed' && false - if: ${{ needs.test-standalone.result != 'success' }} - - run: echo 'publish-standalone-dry-run failed' && false - if: ${{ needs.publish-standalone-dry-run.result != 'success' }} + custom_script: /usr/bin/time -v make COQBIN="$(dirname "$(which coqc)")/" -j src/Bedrock/End2End/X25519/GarageDoorTop.vo diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml index 0d100a1aa5..b9da232e78 100644 --- a/.github/workflows/coq-macos.yml +++ b/.github/workflows/coq-macos.yml @@ -68,151 +68,4 @@ jobs: - name: deps run: | eval $(opam env) - etc/ci/github-actions-make.sh -j2 deps - - name: all - run: | - eval $(opam env) - etc/ci/github-actions-make.sh -j2 all - - - name: install-standalone-unified-ocaml - run: | - eval $(opam env) - etc/ci/github-actions-make.sh install-standalone-unified-ocaml BINDIR=dist - - - name: install-standalone-js-of-ocaml - run: | - eval $(opam env) - etc/ci/github-actions-make.sh install-standalone-js-of-ocaml - - - name: only-test-amd64-files-lite - run: | - eval $(opam env) - etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1 - - - name: upload OCaml files - uses: actions/upload-artifact@v3 - with: - name: ExtractionOCaml - path: src/ExtractionOCaml - - name: upload js_of_ocaml files - uses: actions/upload-artifact@v3 - with: - name: ExtractionJsOfOCaml - path: src/ExtractionJsOfOCaml - - name: upload standalone files - uses: actions/upload-artifact@v3 - with: - name: standalone-macos - path: dist/fiat_crypto - - name: upload standalone js files - uses: actions/upload-artifact@v3 - with: - name: standalone-html-macos - path: fiat-html - - name: install - run: | - eval $(opam env) - etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml - - name: install-without-bedrock2 - run: | - eval $(opam env) - etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml - - name: install-dev - run: | - eval $(opam env) - etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml - - name: display timing info - run: cat time-of-build-pretty.log - - name: display per-line timing info - run: etc/ci/github-actions-display-per-line-timing.sh -# - name: upload timing and .vo info -# uses: actions/upload-artifact@v3 -# with: -# name: build-outputs -# path: . -# if: always () -# - name: validate -# run: | -# eval $(opam env) -# make TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}" -# if: github.event_name != 'pull_request' - - test-standalone: - runs-on: macos-latest - needs: build - steps: - - uses: actions/checkout@v4 - - name: Download standalone MacOS - uses: actions/download-artifact@v3 - with: - name: standalone-macos - path: dist/ - - name: List files - run: find dist - - run: chmod +x dist/fiat_crypto - - name: Test files - run: | - echo "::group::file fiat_crypto" - file dist/fiat_crypto - echo "::endgroup::" - echo "::group::otool -L fiat_crypto" - otool -L dist/fiat_crypto - echo "::endgroup::" - echo "::group::lipo -info fiat_crypto" - lipo -info dist/fiat_crypto - echo "::endgroup::" - etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto - - publish-standalone: - runs-on: ubuntu-latest - needs: build - permissions: - contents: write # IMPORTANT: mandatory for making GitHub Releases - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 # Fetch all history for all tags and branches - tags: true # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version - - name: Download standalone MacOS - uses: actions/download-artifact@v3 - with: - name: standalone-macos - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - arch="$(etc/ci/find-arch.sh dist/fiat_crypto)" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_macOS_${arch}" - echo "$fname" - mv dist/fiat_crypto "dist/$fname" - find dist - - name: Upload artifacts to GitHub Release - env: - GITHUB_TOKEN: ${{ github.token }} - # Upload to GitHub Release using the `gh` CLI. - # `dist/` contains the built packages - run: >- - gh release upload - '${{ github.ref_name }}' dist/** - --repo '${{ github.repository }}' - if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }} - - macos-check-all: - runs-on: ubuntu-latest - needs: [build, test-standalone, publish-standalone] - if: always() - steps: - - run: echo 'build passed' - if: ${{ needs.build.result == 'success' }} - - run: echo 'test-standalone passed' - if: ${{ needs.test-standalone.result == 'success' }} - - run: echo 'publish-standalone passed' - if: ${{ needs.publish-standalone.result == 'success' }} - - run: echo 'build failed' && false - if: ${{ needs.build.result != 'success' }} - - run: echo 'test-standalone failed' && false - if: ${{ needs.test-standalone.result != 'success' }} - - run: echo 'publish-standalone failed' && false - if: ${{ needs.publish-standalone.result != 'success' }} + /usr/bin/time -v make -j src/Bedrock/End2End/X25519/GarageDoorTop.vo diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml index 196d8d4369..90c8ec93fc 100644 --- a/.github/workflows/coq-windows.yml +++ b/.github/workflows/coq-windows.yml @@ -67,172 +67,5 @@ jobs: shell: cmd - name: deps run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} deps' + %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- /usr/bin/time -v make -j src/Bedrock/End2End/X25519/GarageDoorTop.vo' shell: cmd - - name: standalone-ocaml - 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: install-standalone-unified-ocaml - run: | - %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: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 coq' - shell: cmd - - name: all-except-generated-and-js-of-ocaml - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 all-except-generated-and-js-of-ocaml' - shell: cmd - - name: standalone-js-of-ocaml - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j1 standalone-js-of-ocaml' - shell: cmd - - name: install-standalone-js-of-ocaml - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh install-standalone-js-of-ocaml' - shell: cmd - - name: c-files lite-generated-files - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} c-files lite-generated-files' - shell: cmd - - name: only-test-amd64-files-lite - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh -j${NJOBS} only-test-amd64-files-lite SLOWEST_FIRST=1' - shell: cmd - - name: upload OCaml files - uses: actions/upload-artifact@v3 - with: - name: ExtractionOCaml - path: src/ExtractionOCaml - - name: upload js_of_ocaml files - uses: actions/upload-artifact@v3 - with: - name: ExtractionJsOfOCaml - path: src/ExtractionJsOfOCaml - - name: upload standalone files - uses: actions/upload-artifact@v3 - with: - name: standalone-windows - path: dist/fiat_crypto.exe - - name: upload standalone js files - uses: actions/upload-artifact@v3 - with: - name: standalone-html-windows - path: fiat-html - - name: install - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_COQSCRIPTS_INCLUDE=1 install install-standalone-ocaml' - shell: cmd - - name: install-without-bedrock2 - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_DEPENDENCIES=1 SKIP_BEDROCK2=1 install-without-bedrock2 install-standalone-ocaml' - shell: cmd - - name: install-dev - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- etc/ci/github-actions-make.sh EXTERNAL_REWRITER=1 EXTERNAL_COQPRIME=1 install install-standalone-ocaml' - shell: cmd - - name: display timing info - run: type time-of-build-pretty.log - shell: cmd - - name: display per-line timing info - run: | - %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; etc/ci/github-actions-display-per-line-timing.sh' - shell: cmd -# - name: upload timing and .vo info -# uses: actions/upload-artifact@v3 -# with: -# name: build-outputs -# path: . -# if: always () -# - name: validate -# run: | -# %CYGWIN_ROOT%\bin\bash.exe -l -c 'cd "%cd%"; opam exec -- make TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"' -# shell: cmd -# if: github.event_name != 'pull_request' - - test-standalone: - runs-on: windows-latest - needs: build - steps: - - uses: actions/checkout@v4 - - name: Download standalone Windows - uses: actions/download-artifact@v3 - with: - name: standalone-windows - path: dist/ - - name: List files - 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: | - 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 - fiat_crypto" - dumpbin.exe /dependents .\dist\fiat_crypto.exe - Write-Host "::endgroup::" - - publish-standalone: - runs-on: ubuntu-latest - needs: build - permissions: - contents: write # IMPORTANT: mandatory for making GitHub Releases - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 # Fetch all history for all tags and branches - tags: true # Fetch all tags as well, `fetch-depth: 0` might be sufficient depending on Git version - - name: Download standalone Windows - uses: actions/download-artifact@v3 - with: - name: standalone-windows - path: dist/ - - name: List files - run: find dist - - name: Rename files - run: | - arch="$(etc/ci/find-arch.sh dist/fiat_crypto.exe "x86_64")" - tag="$(git describe --tags HEAD)" - fname="Fiat-Cryptography_${tag}_Windows_${arch}.exe" - echo "$fname" - mv dist/fiat_crypto.exe "dist/$fname" - find dist - - name: Upload artifacts to GitHub Release - env: - GITHUB_TOKEN: ${{ github.token }} - # Upload to GitHub Release using the `gh` CLI. - # `dist/` contains the built packages - run: >- - gh release upload - '${{ github.ref_name }}' dist/** - --repo '${{ github.repository }}' - if: ${{ startsWith(github.ref, 'refs/tags/') && github.event_name == 'release' }} - - windows-check-all: - runs-on: ubuntu-latest - needs: [build, test-standalone, publish-standalone] - if: always() - steps: - - run: echo 'build passed' - if: ${{ needs.build.result == 'success' }} - - run: echo 'test-standalone passed' - if: ${{ needs.test-standalone.result == 'success' }} - - run: echo 'publish-standalone passed' - if: ${{ needs.publish-standalone.result == 'success' }} - - run: echo 'build failed' && false - if: ${{ needs.build.result != 'success' }} - - run: echo 'test-standalone failed' && false - if: ${{ needs.test-standalone.result != 'success' }} - - run: echo 'publish-standalone failed' && false - if: ${{ needs.publish-standalone.result != 'success' }} diff --git a/rupicola b/rupicola index d9d95afe2e..73addd218f 160000 --- a/rupicola +++ b/rupicola @@ -1 +1 @@ -Subproject commit d9d95afe2e03f1c5bbac5a710279ddc5c2c7ea6d +Subproject commit 73addd218fb07836f21c6f1c872548d07306a9de diff --git a/src/Bedrock/End2End/X25519/GarageDoor.v b/src/Bedrock/End2End/X25519/GarageDoor.v index d38dbb27b5..109ff3493a 100644 --- a/src/Bedrock/End2End/X25519/GarageDoor.v +++ b/src/Bedrock/End2End/X25519/GarageDoor.v @@ -181,14 +181,14 @@ Goal True. Abort. Definition protocol_step : state -> list MMIO -> state -> Prop := - fun '(Build_state seed sk) ioh '(Build_state SEED SK) => + fun '(Build_state seed x25519_ephemeral_secret) ioh '(Build_state SEED SK) => (lightbulb_spec.lan9250_recv_no_packet _ ioh \/ lightbulb_spec.lan9250_recv_packet_too_long _ ioh \/ - TracePredicate.concat TracePredicate.any (lightbulb_spec.spi_timeout _) ioh) /\ SEED=seed /\ SK=sk \/ + TracePredicate.concat TracePredicate.any (lightbulb_spec.spi_timeout _) ioh) /\ SEED=seed /\ SK=x25519_ephemeral_secret \/ (exists incoming, lightbulb_spec.lan9250_recv _ incoming ioh /\ let ethertype := le_combine (rev (firstn 2 (skipn 12 incoming))) in ethertype < 1536 \/ let ipproto := nth 23 incoming x00 in (ipproto <> x11 \/ - length incoming <> 14+20+8 +2+16 +4 /\ length incoming <> 14+20+8 +2+32 +4)%nat) /\ SEED=seed /\ SK=sk \/ + length incoming <> 14+20+8 +2+16 +4 /\ length incoming <> 14+20+8 +2+32 +4)%nat) /\ SEED=seed /\ SK=x25519_ephemeral_secret \/ exists (mac_local mac_remote : tuple byte 6), exists (ethertype : Z) (ih_const : tuple byte 2) (ip_length : Z) (ip_idff : tuple byte 5), exists (ipproto := x11) (ip_checksum : Z) (ip_local ip_remote : tuple byte 4), @@ -209,28 +209,29 @@ Definition protocol_step : state -> list MMIO -> state -> Prop := (TracePredicate.one ("st", lightbulb_spec.GPIO_DATA_ADDR _, action))) ioh /\ ( let m := firstn 16 garagedoor_payload in - let v := x25519_spec sk garageowner_P in + let v := x25519_spec x25519_ephemeral_secret garageowner_P in exists set0 set1 : Naive.word32, (word.unsigned set0 = 1 <-> firstn 16 v = m) /\ (word.unsigned set1 = 1 <-> skipn 16 v = m) /\ action = word.or (word.and doorstate (word.of_Z (Z.clearbit (Z.clearbit (2^32-1) 11) 12))) (word.slu (word.or (word.slu set1 (word.of_Z 1)) set0) (word.of_Z 11)) /\ - (word.unsigned (word.or set0 set1) = 0 -> SEED=seed /\ SK=sk) /\ + (word.unsigned (word.or set0 set1) = 0 -> SEED=seed /\ SK=x25519_ephemeral_secret) /\ (word.unsigned (word.or set0 set1) <> 0 -> SEED++SK = RupicolaCrypto.Spec.chacha20_block seed (ChaCha20.le_split 4 (word.of_Z 0) ++ firstn 12 garageowner)) )) \/ TracePredicate.concat (lightbulb_spec.lan9250_recv _ incoming) (lightbulb_spec.lan9250_send _ (let ip_length := 62 in let udp_length := 42 in + mac_remote ++ mac_local ++ be2 ethertype ++ - let ih C := ih_const ++ be2 ip_length ++ - ip_idff ++ [ipproto] ++ le_split 2 C ++ - ip_local ++ ip_remote in - ih (Spec.ip_checksum (ih 0)) ++ - udp_local ++ udp_remote ++ - be2 udp_length ++ be2 0 ++ + let ip_hdr checksum := ih_const ++ be2 ip_length ++ + ip_idff ++ [ipproto] ++ le_split 2 checksum ++ + ip_local ++ ip_remote in + ip_hdr (IPChecksum.Spec.ip_checksum (ip_hdr 0)) ++ + udp_local ++ udp_remote ++ be2 udp_length ++ be2 0 ++ garagedoor_header ++ - x25519_spec sk Curve25519.M.B)) - ioh /\ SEED=seed /\ SK=sk. + x25519_spec x25519_ephemeral_secret Curve25519.M.B + + )) ioh /\ SEED=seed /\ SK=x25519_ephemeral_secret. Local Instance spec_of_recvEthernet : spec_of "recvEthernet" := spec_of_recvEthernet. Local Instance spec_of_lan9250_tx : spec_of "lan9250_tx" := spec_of_lan9250_tx. diff --git a/src/Bedrock/End2End/X25519/GarageDoorTop.v b/src/Bedrock/End2End/X25519/GarageDoorTop.v index 92c1442569..552305aa4e 100644 --- a/src/Bedrock/End2End/X25519/GarageDoorTop.v +++ b/src/Bedrock/End2End/X25519/GarageDoorTop.v @@ -173,7 +173,7 @@ Local Notation labeled_transitions := stateful. Local Notation boot_seq := BootSeq. Definition protocol_spec l := exists s s', labeled_transitions protocol_step s s' l. -Definition io_spec : list LogItem -> Prop := only_mmio_satisfying (boot_seq +++ protocol_spec). +Definition io_spec : list _ -> Prop := only_mmio_satisfying (boot_seq +++ protocol_spec). Import ExprImpEventLoopSpec. Definition garagedoor_spec : ProgramSpec := {| @@ -258,7 +258,9 @@ Import bedrock2.Map.Separation. Local Open Scope sep_scope. Require Import bedrock2.ReversedListNotations. Local Notation run1 := (mcomp_sat (run1 Decode.RV32IM)). Local Notation RiscvMachine := MetricRiscvMachine. +Local Notation MMIO := (string * word.rep * word.rep)%type. Goal True. + pose (fun bs => lan9250_writepacket _ (bs : list byte) : list MMIO -> Prop). pose (run1 : RiscvMachine -> (RiscvMachine -> Prop) -> Prop). pose (always(iset:=Decode.RV32IM) : (RiscvMachine -> Prop) -> RiscvMachine -> Prop). Abort.