prover-test.yml

name: Test gnark prover
on:
  push:
    branches:
      - main
    paths:
      - "light-prover/**"
      - ".github/workflows/prover-test.yml"
      - ".github/workflows/prover-release.yml"
  pull_request:
    branches:
      - "*"
    paths:
      - "light-prover/**"
      - ".github/workflows/prover-test.yml"
      - ".github/workflows/prover-release.yml"
    types:
      - opened
      - synchronize
      - reopened
      - ready_for_review

jobs:
  build-and-test:
    if: github.event.pull_request.draft == false
    runs-on: ubuntu-latest
    timeout-minutes: 60
    steps:
      - name: Checkout sources
        uses: actions/checkout@v4

      - name: Set up Go
        uses: actions/setup-go@v5
        with:
          go-version-file: "./light-prover/go.mod"

      - name: Install Elan
        run: |
          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y -v --default-toolchain leanprover/lean4:v4.2.0
          echo "LAKE_VERSION=$(~/.elan/bin/lake --version)" >> "$GITHUB_ENV"

      - name: Cache dependencies
        uses: actions/cache@v3
        with:
          path: light-prover/formal-verification/lake-packages
          key: "${{ env.LAKE_VERSION }}"

      - name: Download keys
        run: |
          cd light-prover
          ./scripts/download_keys.sh

      - name: Build
        run: |
          cd light-prover
          go build

      - name: Unit tests
        run: |
          cd light-prover
          go test ./prover -timeout 30m

      - name: Integration tests
        run: |
          cd light-prover
          go test -timeout 30m

      - name: Extract circuit to Lean
        run: |
          cd light-prover
          ./light-prover extract-circuit --output formal-verification/FormalVerification/Circuit.lean --tree-depth=26 --compressed-accounts=8

      - name: Build lean project
        run: |
          cd light-prover/formal-verification
          ~/.elan/bin/lake exe cache get
          ~/.elan/bin/lake build