ci.yml

name: Build cedar-spec

on:
  pull_request:

env:
  dotnet-version: 6.0.x # SDK Version for building Dafny

jobs:
  build_and_test_dafny:
    name: Build and Test Dafny
    runs-on: ubuntu-latest
    strategy:
      fail-fast: false
      matrix:
        toolchain:
          - stable

    steps:
      - name: Checkout cedar-spec
        uses: actions/checkout@v3
      - name: Install Z3
        shell: bash
        run: |
          wget -q --show-progress https://github.com/Z3Prover/z3/releases/download/z3-4.12.1/z3-4.12.1-x64-glibc-2.35.zip
          unzip z3-4.12.1-x64-glibc-2.35.zip
          echo "$(pwd)/z3-4.12.1-x64-glibc-2.35/bin" >> $GITHUB_PATH
      - name: Audit Dafny files
        shell: bash
        working-directory: ./cedar-dafny
        run : |
          dotnet tool restore
          sudo apt-get install ack
          find . -path test -prune -o -name '*.dfy' | xargs -I {} sh -c "printf '%s: ' {} && (dotnet tool run dafny audit {} | ack --passthru --nocolor '0 findings')"
      - name: verify dafny
        working-directory: ./cedar-dafny
        run: make GEN_STATS=1 verify
      - name: test dafny
        working-directory: ./cedar-dafny
        run: make test
      - name: log resource usage
        working-directory: ./cedar-dafny
        run: |
          dotnet tool restore
          dotnet tool run dafny-reportgenerator summarize-csv-results --max-resource-count 10000000 . || true

  build_and_test_drt:
    name: Build and Test DRT
    runs-on: ubuntu-latest
    strategy:
      matrix:
        toolchain:
          - stable

    steps:
      - name: Checkout cedar-spec
        uses: actions/checkout@v3
        with:
          submodules: recursive
      - name: Get Java 17
        uses: actions/setup-java@v3
        with:
          distribution: 'corretto'
          java-version: '17'
          cache: 'gradle'
      - name: Build Dafny def engine
        working-directory: ./cedar-dafny
        shell: bash
        run: make compile-difftest
      - name: Build cedar-dafny-java-wrapper
        working-directory: ./cedar-dafny-java-wrapper
        shell: bash
        run: ./gradlew build dumpClasspath
      - name: rustup
        run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }}
      - name: cargo fmt (cedar-policy-generators)
        working-directory: ./cedar-policy-generators
        run: cargo fmt --all --check
      - name: cargo fmt (cedar-drt)
        working-directory: ./cedar-drt
        run: cargo fmt --all --check
      - name: cargo fmt (cedar-drt/fuzz/)
        working-directory: ./cedar-drt/fuzz
        run: cargo fmt --all --check
      - name: cargo rustc (cedar-policy-generators)
        working-directory: ./cedar-policy-generators
        run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose
      - name: cargo rustc (cedar-drt)
        working-directory: ./cedar-drt
        run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose
      - name: cargo rustc (cedar-drt/fuzz/)
        working-directory: ./cedar-drt/fuzz
        run: RUSTFLAGS="-D warnings -F unsafe-code" cargo build --verbose
      - name: cargo test (cedar-policy-generators)
        working-directory: ./cedar-policy-generators
        run: cargo test --verbose
      - name: cargo test (cedar-drt)
        working-directory: ./cedar-drt
        shell: bash
        run: |
             source ./set_env_vars.sh
             export LD_LIBRARY_PATH=${LD_LIBRARY_PATH+$LD_LIBRARY_PATH:}$JAVA_HOME/lib/server
             cargo test --verbose

  build_cedar_lean:
    name: Build cedar-lean
    runs-on: ubuntu-latest
    strategy:
      matrix:
        toolchain:
          - stable

    steps:
      - name: Checkout cedar-spec
        uses: actions/checkout@v3
        with:
          submodules: recursive
      - name: Install Lean
        shell: bash
        run: |
              wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
              bash elan-init.sh -y
      - name: Build
        working-directory: ./cedar-lean
        shell: bash
        run: source ~/.profile && lake build Cedar
      - name: Test
        working-directory: ./cedar-lean
        shell: bash
        run: source ~/.profile && lake exe CedarUnitTests