feat: formalize slot_is_justifiable_after in Lean4
#787
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: CI | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| branches: ["**"] | |
| workflow_dispatch: | |
| # Cancel in-progress runs when a new commit is pushed to the same PR or branch | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} | |
| cancel-in-progress: true | |
| env: | |
| CARGO_NET_GIT_FETCH_WITH_CLI: "true" | |
| CARGO_NET_RETRY: "10" | |
| jobs: | |
| lint: | |
| name: Lint | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - name: Setup Rust | |
| uses: dtolnay/rust-toolchain@stable | |
| with: | |
| toolchain: "1.92.0" | |
| components: rustfmt, clippy | |
| - name: Setup cache | |
| uses: Swatinem/rust-cache@v2 | |
| - name: Check formatting | |
| run: cargo fmt --all -- --check | |
| - name: Cargo check | |
| run: cargo check --workspace --all-targets --exclude ethlambda-lean-ffi | |
| - name: Clippy | |
| run: cargo clippy --workspace --all-targets --exclude ethlambda-lean-ffi -- -D warnings | |
| test: | |
| name: Test | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v6 | |
| # Read the pinned leanSpec commit from the Makefile (single source of truth) | |
| - name: Get leanSpec pinned commit | |
| id: lean-spec | |
| run: echo "commit=$(sed -n 's/^LEAN_SPEC_COMMIT_HASH:= *//p' Makefile)" >> $GITHUB_OUTPUT | |
| - name: Cache test fixtures | |
| id: cache-fixtures | |
| uses: actions/cache@v5 | |
| with: | |
| path: leanSpec/fixtures | |
| key: leanspec-fixtures-${{ steps.lean-spec.outputs.commit }} | |
| # All fixture generation steps are skipped when the cache hits | |
| - name: Checkout leanSpec at pinned commit | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| uses: actions/checkout@v6 | |
| with: | |
| repository: leanEthereum/leanSpec | |
| ref: ${{ steps.lean-spec.outputs.commit }} | |
| path: leanSpec | |
| - name: Install uv and Python 3.14 | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| uses: astral-sh/setup-uv@v4 | |
| with: | |
| enable-cache: true | |
| cache-dependency-glob: "leanSpec/pyproject.toml" | |
| python-version: "3.14" | |
| - name: Sync leanSpec dependencies | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| working-directory: leanSpec | |
| run: uv sync --no-progress | |
| - name: Get production keys URL hash | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| id: prod-keys-url | |
| working-directory: leanSpec | |
| run: | | |
| URL=$(uv run python -c "from consensus_testing.keys import KEY_DOWNLOAD_URLS; print(KEY_DOWNLOAD_URLS['prod'])") | |
| HASH=$(echo -n "$URL" | sha256sum | awk '{print $1}') | |
| echo "hash=$HASH" >> $GITHUB_OUTPUT | |
| - name: Cache production keys | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| id: cache-prod-keys | |
| uses: actions/cache@v5 | |
| with: | |
| path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme | |
| key: prod-keys-${{ steps.prod-keys-url.outputs.hash }} | |
| - name: Download production keys | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' && steps.cache-prod-keys.outputs.cache-hit != 'true' | |
| working-directory: leanSpec | |
| run: uv run python -m consensus_testing.keys --download --scheme prod | |
| - name: Generate test fixtures | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| working-directory: leanSpec | |
| run: uv run fill --fork=Devnet --scheme prod -o fixtures -n 2 | |
| # Ensure make sees fixtures as up-to-date (its timestamp must be | |
| # newer than leanSpec/, which intermediate steps may have modified). | |
| - name: Mark fixtures as up-to-date | |
| run: touch leanSpec/fixtures | |
| - name: Setup Rust | |
| uses: dtolnay/rust-toolchain@stable | |
| with: | |
| toolchain: "1.92.0" | |
| - name: Setup cache | |
| uses: Swatinem/rust-cache@v2 | |
| - name: Run tests | |
| run: make test | |
| lean-build: | |
| name: Build Lean | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - name: Install elan | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| - name: Cache Lake packages | |
| uses: actions/cache@v5 | |
| with: | |
| path: | | |
| ~/.elan | |
| formal/.lake | |
| key: ${{ runner.os }}-lake-${{ hashFiles('formal/lean-toolchain', 'formal/lakefile.toml', 'formal/lake-manifest.json') }} | |
| restore-keys: | | |
| ${{ runner.os }}-lake- | |
| - name: Fetch Mathlib cache | |
| working-directory: formal | |
| run: lake exe cache get | |
| - name: Build both libraries | |
| working-directory: formal | |
| run: lake build | |
| - name: Verify zero sorries | |
| working-directory: formal | |
| run: | | |
| if grep -rn "sorry" EthLambda/ EthLambdaProofs/ --include="*.lean"; then | |
| echo "::error::Found sorry in Lean sources" | |
| exit 1 | |
| fi | |
| lean-ffi-test: | |
| name: Test with Lean FFI | |
| runs-on: ubuntu-latest | |
| needs: [lean-build, test] | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - name: Install elan | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> $GITHUB_PATH | |
| # Reuse the Lake cache from the lean-build job | |
| - name: Cache Lake packages | |
| uses: actions/cache@v5 | |
| with: | |
| path: | | |
| ~/.elan | |
| formal/.lake | |
| key: ${{ runner.os }}-lake-${{ hashFiles('formal/lean-toolchain', 'formal/lakefile.toml', 'formal/lake-manifest.json') }} | |
| restore-keys: | | |
| ${{ runner.os }}-lake- | |
| # Read the pinned leanSpec commit from the Makefile (single source of truth) | |
| - name: Get leanSpec pinned commit | |
| id: lean-spec | |
| run: echo "commit=$(sed -n 's/^LEAN_SPEC_COMMIT_HASH:= *//p' Makefile)" >> $GITHUB_OUTPUT | |
| # Reuse the fixtures cache from the test job | |
| - name: Cache test fixtures | |
| id: cache-fixtures | |
| uses: actions/cache@v5 | |
| with: | |
| path: leanSpec/fixtures | |
| key: leanspec-fixtures-${{ steps.lean-spec.outputs.commit }} | |
| # All fixture generation steps are skipped when the cache hits | |
| - name: Checkout leanSpec at pinned commit | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| uses: actions/checkout@v6 | |
| with: | |
| repository: leanEthereum/leanSpec | |
| ref: ${{ steps.lean-spec.outputs.commit }} | |
| path: leanSpec | |
| - name: Install uv and Python 3.14 | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| uses: astral-sh/setup-uv@v4 | |
| with: | |
| enable-cache: true | |
| cache-dependency-glob: "leanSpec/pyproject.toml" | |
| python-version: "3.14" | |
| - name: Sync leanSpec dependencies | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| working-directory: leanSpec | |
| run: uv sync --no-progress | |
| - name: Get production keys URL hash | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| id: prod-keys-url | |
| working-directory: leanSpec | |
| run: | | |
| URL=$(uv run python -c "from consensus_testing.keys import KEY_DOWNLOAD_URLS; print(KEY_DOWNLOAD_URLS['prod'])") | |
| HASH=$(echo -n "$URL" | sha256sum | awk '{print $1}') | |
| echo "hash=$HASH" >> $GITHUB_OUTPUT | |
| - name: Cache production keys | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| id: cache-prod-keys | |
| uses: actions/cache@v5 | |
| with: | |
| path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme | |
| key: prod-keys-${{ steps.prod-keys-url.outputs.hash }} | |
| - name: Download production keys | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' && steps.cache-prod-keys.outputs.cache-hit != 'true' | |
| working-directory: leanSpec | |
| run: uv run python -m consensus_testing.keys --download --scheme prod | |
| - name: Generate test fixtures | |
| if: steps.cache-fixtures.outputs.cache-hit != 'true' | |
| working-directory: leanSpec | |
| run: uv run fill --fork=Devnet --scheme prod -o fixtures -n 2 | |
| - name: Mark fixtures as up-to-date | |
| run: touch leanSpec/fixtures | |
| - name: Setup Rust | |
| uses: dtolnay/rust-toolchain@stable | |
| with: | |
| toolchain: "1.92.0" | |
| components: clippy | |
| - name: Setup Rust cache | |
| uses: Swatinem/rust-cache@v2 | |
| - name: Clippy (lean-ffi) | |
| run: cargo clippy -p ethlambda-lean-ffi -- -D warnings | |
| - name: Test with lean-ffi | |
| run: cargo test --workspace --release --features lean-ffi |