absolute-zero/.github/workflows/proofs.yml at main · hyperpolymath/absolute-zero · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
# This workflow is managed by gh actions-lock.
# SPDX-License-Identifier: MPL-2.0
# Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
#
# Proof verification CI for the ACTIVE proof stack (owner ruling 2026-10-10):
#   * Agda      — CNO + OND + EchoBridge (--safe --without-K)
#   * Z3        — CNO + OND bounded checks (expect-annotated)
#   * Idris 2   — the ABI package (absolute-zero-abi.ipkg)
# Each is an INDEPENDENT job, so one flaking never blocks the others.
#
# Coq, Lean 4, Isabelle/HOL and Mizar are ARCHIVED under archive/proofs/ and are
# not gated here. See archive/README.adoc for the archive and its status.
name: Proofs

on:
  push:
    branches: [main, master]
  pull_request:
    paths:
      - 'proofs/**'
      - 'src/**'
      - 'scripts/check-proof-patterns.sh'
      - 'tests/check-proof-patterns.sh'
      - '.machine_readable/contractiles/trust/trust.k9.ncl'
      - 'absolute-zero-abi.ipkg'
      - '.github/workflows/proofs.yml'
      - 'Justfile'
      - '*.agda-lib'

permissions:
  contents: read

# Cancel superseded runs on the same ref (don't pile up on force-pushes).
concurrency:
  group: proofs-${{ github.ref }}
  cancel-in-progress: true

jobs:
  proof-patterns:
    name: Proof escape-hatch baseline
    runs-on: ubuntu-24.04
    steps:
      - uses: actions/checkout@v7.0.1
      - run: bash scripts/check-proof-patterns.sh
      - run: bash tests/check-proof-patterns.sh

  agda:
    name: Agda — CNO + OND + EchoBridge
    runs-on: ubuntu-24.04
    timeout-minutes: 25
    steps:
      - uses: actions/checkout@v7.0.1
      - name: Install Agda (binary only)
        # Install just the `agda` binary (2.6.3 on 24.04). NOT `agda-stdlib` —
        # the Ubuntu stdlib package ships no usable library manifest; we fetch a
        # version-matched stdlib from git instead (validated locally).
        run: sudo apt-get update && sudo apt-get install -y agda
      - name: Fetch + register agda-stdlib v1.7.3 (matches Agda 2.6.3)
        run: |
          git clone -q --depth 1 --branch v1.7.3 \
            https://github.com/agda/agda-stdlib.git "$HOME/agda-stdlib"
          # The upstream manifest is named `standard-library-1.7.3`; the repo's
          # absolute-zero.agda-lib depends on `standard-library`, so align it.
          sed -i 's/^name: .*/name: standard-library/' \
            "$HOME/agda-stdlib/standard-library.agda-lib"
          mkdir -p "$HOME/.agda"
          echo "$HOME/agda-stdlib/standard-library.agda-lib" > "$HOME/.agda/libraries"
          echo "standard-library" > "$HOME/.agda/defaults"
      - name: Type-check CNO + OND + EchoBridge (4 modules, --safe --without-K)
        working-directory: proofs/agda
        run: |
          agda --version
          agda --safe --without-K CNO.agda
          agda --safe --without-K OND.agda
          agda --safe --without-K EchoBridgeScaffold.agda
          agda --safe --without-K EchoBridgeCNO.agda
          echo "✓ Agda: CNO + OND + EchoBridgeScaffold + EchoBridgeCNO type-check"

  z3:
    name: Z3 — CNO + OND bounded checks
    runs-on: ubuntu-24.04
    steps:
      - uses: actions/checkout@v7.0.1
      - name: Install Z3
        run: sudo apt-get update && sudo apt-get install -y z3
      - name: Run Z3 checks
        run: |
          z3 --version
          bash proofs/z3/verify.sh
          echo "✓ Z3: every (check-sat) verdict matched its ; expect annotation"

  idris:
    name: Idris 2 — ABI package (absolute-zero-abi.ipkg)
    runs-on: ubuntu-latest
    timeout-minutes: 30
    container:
      # Same pinned idris2-pack image as pages.yml (digest-pinned).
      image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff
    steps:
      - uses: actions/checkout@v7.0.1
      - name: Build the ABI package (type-checks every src/abi module)
        run: |
          idris2 --version
          idris2 --build absolute-zero-abi.ipkg
          echo "✓ Idris 2: absolute-zero-abi.ipkg builds"