# Copyright (c) 2026 Ahmad Ali Parr. All rights reserved.
# SPDX-License-Identifier: LicenseRef-Proprietary
# Public source visibility does not grant an open-source license. See LICENSE.

name: ATS and SPARK validation

on:
  push:
  pull_request:
  workflow_dispatch:

permissions:
  contents: read

jobs:
  ats:
    runs-on: ubuntu-24.04
    timeout-minutes: 15
    steps:
      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
      - name: Install ATS compiler
        run: |
          sudo apt-get update
          sudo apt-get install -y ats2-lang=0.4.2-1.1 build-essential
      - name: Typecheck supplied ATS interfaces
        run: |
          mkdir -p build/reports/ats
          set -o pipefail
          patsopt --version | tee build/reports/ats/version.txt
          patsopt -tc -s ats/heap.sats 2>&1 | tee build/reports/ats/heap-typecheck.txt
          patsopt -tc -s ats/state.sats 2>&1 | tee build/reports/ats/state-typecheck.txt
      - name: Preserve ATS evidence
        if: always()
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: ats-validation-evidence
          path: build/reports/ats/
  spark:
    runs-on: ubuntu-24.04
    timeout-minutes: 20
    steps:
      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
      - name: Install native Ada compiler
        run: |
          sudo apt-get update
          sudo apt-get install -y gnat gprbuild
      - name: Restore pinned SPARK toolchain
        id: spark-cache
        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830
        with:
          path: ~/.local/gnatprove-15.1.0
          key: gnatprove-linux-aad9a73f600d3008-v1
      - name: Install checksum-verified GNATprove
        if: steps.spark-cache.outputs.cache-hit != 'true'
        run: |
          curl --fail --location --retry 3 \
            https://github.com/alire-project/GNAT-FSF-builds/releases/download/gnatprove-15.1.0-1/gnatprove-x86_64-linux-15.1.0-1.tar.gz \
            -o "$RUNNER_TEMP/gnatprove.tar.gz"
          echo "aad9a73f600d3008f33141a6cd4c5314d4c210e8928edc172c23c76104ddf7b2  $RUNNER_TEMP/gnatprove.tar.gz" | sha256sum --check
          mkdir -p "$HOME/.local/gnatprove-15.1.0"
          tar -xzf "$RUNNER_TEMP/gnatprove.tar.gz" --strip-components=1 -C "$HOME/.local/gnatprove-15.1.0"
      - name: Save prover before running project checks
        if: steps.spark-cache.outputs.cache-hit != 'true'
        uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830
        with:
          path: ~/.local/gnatprove-15.1.0
          key: gnatprove-linux-aad9a73f600d3008-v1
      - name: Build and run heap smoke test
        run: |
          mkdir -p build/reports/spark
          set -o pipefail
          gnat --version | tee build/reports/spark/compiler-version.txt
          gprbuild -p -P ada/heap_model.gpr 2>&1 | tee build/reports/spark/build.txt
          build/heap_demo | tee build/reports/spark/smoke.txt
          test "$(cat build/reports/spark/smoke.txt)" = 'heap contract smoke test: PASS'
      - name: Prove all heap obligations and fail on unproved checks
        run: |
          export PATH="$HOME/.local/gnatprove-15.1.0/bin:$PATH"
          mkdir -p build/reports/spark
          set -o pipefail
          gnatprove --version | tee build/reports/spark/prover-version.txt
          gnatprove -P ada/heap_model.gpr -u heap_model.adb --mode=all \
            --checks-as-errors=on --warnings=error --report=all --level=2 \
            2>&1 | tee build/reports/spark/proof.txt
      - name: Preserve SPARK evidence
        if: always()
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: spark-validation-evidence
          path: |
            build/reports/spark/
            build/ada_obj/gnatprove/
  combined:
    needs: [ats, spark]
    runs-on: ubuntu-24.04
    timeout-minutes: 35
    steps:
      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
      - name: Install combined compiler dependencies
        run: |
          sudo apt-get update
          sudo apt-get install -y ats2-lang=0.4.2-1.1 gnat gprbuild chezscheme build-essential libgmp-dev
      - name: Restore pinned Idris compiler
        id: combined-idris
        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830
        with:
          path: ~/.idris2
          key: idris2-ubuntu24-15a3e4e70843f7a34100f6470c04b791330788df-v1
      - name: Bootstrap Idris if cache was evicted
        if: steps.combined-idris.outputs.cache-hit != 'true'
        run: |
          git clone https://github.com/idris-lang/Idris2.git "$RUNNER_TEMP/Idris2"
          cd "$RUNNER_TEMP/Idris2"
          git checkout 15a3e4e70843f7a34100f6470c04b791330788df
          make bootstrap SCHEME=chezscheme
          make install
      - name: Restore SPARK toolchain validated by prerequisite job
        uses: actions/cache/restore@0057852bfaa89a56745cba8c7296529d2fc39830
        with:
          path: ~/.local/gnatprove-15.1.0
          key: gnatprove-linux-aad9a73f600d3008-v1
          fail-on-cache-miss: true
      - name: Run the complete checked-component entry point
        run: |
          export PATH="$HOME/.idris2/bin:$HOME/.local/gnatprove-15.1.0/bin:$PATH"
          mkdir -p build/reports
          set -o pipefail
          bash verify.sh 2>&1 | tee build/reports/combined.txt
      - name: Preserve combined evidence
        if: always()
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
        with:
          name: combined-validation-evidence
          path: build/reports/combined.txt