Sphincs FV in ROM #169
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Lean | |
| on: | |
| push: | |
| branches: [ "main" ] | |
| pull_request: | |
| workflow_dispatch: | |
| permissions: | |
| contents: read | |
| concurrency: | |
| group: lean-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| xmss-formalization: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| # Cheap first pass: the axiom guard in `XmssSecurity.lean` catches a `sorry` | |
| # or a `native_decide` reaching the root theorem, this catches one parked | |
| # anywhere in the project. | |
| - name: Forbid proof escapes | |
| run: | | |
| ! grep -rnE '\b(sorry|sorryAx|admit|native_decide|unsafe|implemented_by)\b|#exit' \ | |
| --include='*.lean' formal/xmss | grep -vE ':[0-9]+: *(--|/-)' | |
| # Installs the toolchain from `formal/xmss/lean-toolchain`, fetches the | |
| # mathlib cache, and runs `lake build` on the default target, which | |
| # elaborates the root module and with it both `#guard_msgs` checks. The | |
| # checked-in manifest is used as is: no `lake update`. | |
| - uses: leanprover/lean-action@v1 | |
| with: | |
| lake-package-directory: formal/xmss | |
| # The root module guards its own footprint with `#guard_msgs`, which an | |
| # edit to the expected message would silence. This asks again from | |
| # outside, against the list written here. | |
| - name: Check the axiom footprint | |
| working-directory: formal/xmss | |
| run: | | |
| printf 'import XmssSecurity\n#print axioms XmssSecurity.xmss_has_127_bits_of_classical_security\n' \ | |
| > "$RUNNER_TEMP/axioms.lean" | |
| lake env lean "$RUNNER_TEMP/axioms.lean" | tee "$RUNNER_TEMP/axioms.txt" | |
| grep -qF "'XmssSecurity.xmss_has_127_bits_of_classical_security' depends on axioms: [propext, Classical.choice, Quot.sound]" \ | |
| "$RUNNER_TEMP/axioms.txt" | |
| - uses: actions/upload-artifact@v4 | |
| with: | |
| name: xmss-axioms | |
| path: ${{ runner.temp }}/axioms.txt |