Skip to content
ABI Seam Verification

fix(ci): reconcile the workflows with actions.lock (gh-actions-lock) #28

Sign in to view logs

fix(ci): reconcile the workflows with actions.lock (gh-actions-lock)

fix(ci): reconcile the workflows with actions.lock (gh-actions-lock) #28

Workflow file for this run

.github/workflows/abi-verify.yml at a40f6c8
# This workflow is managed by gh actions-lock.
# SPDX-License-Identifier: MPL-2.0
# This workflow is managed by gh actions-lock.
# 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@v7.0.1
- 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@v7.0.1
- 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@v7.0.1
- 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