ephapax/.github/workflows/abi-verify.yml at main · hyperpolymath/ephapax · 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
# SPDX-License-Identifier: MPL-2.0
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# abi-verify.yml — machine-checks the Ephapax Rust↔SPARK ABI seam.
#
# The seam (src/abi/Ephapax/ABI/{Types,Foreign,Invariants}.idr) states
# the correctness-critical invariants E1–E6 (see PROOF-NEEDS.md and
# RUST-SPARK-STANCE.adoc). Some properties have discharged proofs in
# the broader formalisation (cited from Invariants.idr — e.g.
# `splitLinearCoverage`, `noEscapeTheorem`); the rest are explicit
# erased OWED obligations.
#
# This gate exists so the discharged proofs cannot silently regress
# and an OWED postulate cannot quietly become a `believe_me`. Mirrors
# the proof-of-work `abi-verify.yml` (snazzybucket/idris2 container,
# the estate-standard image). HARD GATE.

name: ABI Seam Verification

on:
  pull_request:
    paths:
      - 'src/abi/**'
      - 'src/formal/**'
      - 'idris2/**'
      - '.github/workflows/abi-verify.yml'
  push:
    branches: [main]
    paths:
      - 'src/abi/**'
      - 'src/formal/**'
      - 'idris2/**'

permissions:
  contents: read

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

jobs:
  idris2-abi:
    name: Idris2 ABI seam (ephapax-abi.ipkg)
    runs-on: ubuntu-latest
    timeout-minutes: 20
    container:
      image: snazzybucket/idris2:latest  # estate-standard Idris2 image
    steps:
      - name: Checkout repository
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v4

      - name: Build (typecheck) the ABI seam
        working-directory: src/abi
        run: |
          idris2 --version
          # --build typechecks every module in the .ipkg in dependency
          # order. A real regression (ill-typed lemma, a discharged
          # proof that stops reducing, a stray `?hole`/`believe_me`)
          # fails here. The intentional erased OWED postulates are
          # well-typed and do NOT fail the build — they are tracked in
          # PROOF-NEEDS.md, not hidden.
          idris2 --build ephapax-abi.ipkg

  idris2-formal:
    name: Idris2 formal seam (ephapax-formal.ipkg)
    runs-on: ubuntu-latest
    timeout-minutes: 20
    container:
      image: snazzybucket/idris2:latest  # estate-standard Idris2 image
    steps:
      - name: Checkout repository
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v4

      - name: Build (typecheck) the formal package
        working-directory: src/formal
        run: |
          idris2 --version
          idris2 --build ephapax-formal.ipkg

  idris2-parse-front:
    name: Idris2 parse front-end (ephapax-parse-tests.ipkg)
    runs-on: ubuntu-latest
    timeout-minutes: 20
    container:
      image: snazzybucket/idris2:latest  # estate-standard Idris2 image
    steps:
      - name: Checkout repository
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v4

      - name: Build the parse front-end + test executable
        working-directory: idris2
        run: |
          idris2 --version
          # Compile-time gate only: the %foreign C bindings in
          # Parse/ZigBuffer.idr resolve libephapax_tokbuf at RUNTIME
          # (Chez dlopen), so building the executable needs no zig.
          # Running it does — that path is exercised locally via
          #   zig build-lib -dynamic -lc ffi/zig/tokbuf.zig \
          #     -femit-bin=libephapax_tokbuf.so
          #   LD_LIBRARY_PATH=. ./build/exec/ephapax-parse-tests
          # and the zig side is unit-gated by ffi-seams.yml.
          # (ephapax-affine.ipkg is NOT gated here: it depends on the
          # external `proven` package — see PROOF-NEEDS.md.)
          idris2 --build ephapax-parse-tests.ipkg