Skip to content

feat(abi): generate the Zig and Rust wire enums from the normative Idris2 ABI (#120) #811

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 2 commits into from
Sep 22, 2026
Merged

feat(abi): generate the Zig and Rust wire enums from the normative Idris2 ABI (#120) #811

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
086998f
feat(abi): generate the Zig and Rust wire enums from the normative Id…
hyperpolymath Sep 22, 2026
fbd3b26
Merge branch 'main' into feat/issue-120-abi-codegen
hyperpolymath Sep 22, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
164 changes: 164 additions & 0 deletions .github/workflows/abi-codegen-drift.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,164 @@
# SPDX-License-Identifier: MPL-2.0
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# ABI codegen drift gate.
#
# Re-runs `hypatia-abi-gen` against the normative Idris2 ABI and fails if any
# generated file in the tree differs from what the generator emits now.
#
# Deliberately has NO `paths:` filter. `verify-proofs.yml` -- the obvious home
# for this job -- filters on `src/abi/**`, `src/Hypatia/ABI/**`, `verify/**`
# and friends, and lists none of the generated targets, so a hand-edit to
# `ffi/zig/src/connector_generated.zig` would not have fired it at all. An
# unfiltered workflow also stays eligible to be made a required check without
# deadlocking PRs that touch none of those paths.

name: ABI codegen drift

on:
push:
branches: [main]
pull_request:
workflow_dispatch:

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

permissions: read-all

jobs:
abi-codegen-drift:
name: abi-codegen-drift
runs-on: ubuntu-latest
timeout-minutes: 25
permissions:
contents: read

env:
IDRIS2_VERSION: v0.7.0

steps:
- name: Checkout
uses: actions/checkout@v7.0.1

- name: Install Chez Scheme
run: |
set -euo pipefail
sudo apt-get update
sudo apt-get install -y chezscheme

- name: Cache Idris 2 install
id: cache-idris
uses: actions/cache@v6.1.0
with:
path: |
/usr/local/bin/idris2
/usr/local/bin/idris2_app
/usr/local/lib/idris2
~/.idris2
# Same key as verify-proofs.yml on purpose: this job shares that
# workflow's warm cache rather than paying a second ~20-min
# bootstrap. Keep the `-2` suffix in step with it.
key: idris2-${{ env.IDRIS2_VERSION }}-${{ runner.os }}-2

- name: Build Idris 2 from source
if: steps.cache-idris.outputs.cache-hit != 'true'
run: |
set -euo pipefail
git clone --depth 1 --branch "${IDRIS2_VERSION}" \
https://github.com/idris-lang/Idris2 /tmp/idris2
cd /tmp/idris2
make bootstrap SCHEME=chezscheme
sudo make install PREFIX=/usr/local
idris2 --version

- name: Verify Idris is on PATH
run: idris2 --version

- name: Build the generator
run: |
set -euo pipefail
cd src/abi
idris2 --build hypatia-abi-gen.ipkg

- name: Regenerate into a temp dir and compare
run: |
set -euo pipefail
# NOTE: `set -o pipefail` (via -euo) is load-bearing below. A
# pipeline's exit status is its LAST command's, so `generator | tee`
# would report success for a generator that died.

OUT="${RUNNER_TEMP}/abi-gen"
rm -rf "${OUT}"
mkdir -p "${OUT}"

# Regenerate into a TEMP dir, never in place. Regenerating in place
# and running `git diff` means a generator that silently failed to
# run leaves an empty diff -- which reads as green.
./build/abi-gen/exec/hypatia-abi-gen \
--out-dir "${OUT}" \
--abi-hash "$(git hash-object src/Hypatia/ABI/Types.idr)" \
| tee "${RUNNER_TEMP}/gen.log"

emitted=$(sed -n 's/^connectors emitted:[[:space:]]*//p' "${RUNNER_TEMP}/gen.log")
emitted=${emitted:-0}

# published path <- emitted filename
targets="ffi/zig/src/connector_generated.zig:connector_generated.zig
clients/rust/hypatia-client/src/connector_generated.rs:connector_generated.rs
ffi/connectors.json:connectors.json"

compared=0
drifted=0
total=0
for pair in ${targets}; do
total=$((total + 1))
tracked=${pair%%:*}
emitted_file="${OUT}/${pair##*:}"

if [ ! -f "${tracked}" ]; then
echo "::error::tracked file missing: ${tracked}"
drifted=$((drifted + 1))
continue
fi
if [ ! -s "${emitted_file}" ]; then
echo "::error::generator emitted nothing for ${tracked} (${emitted_file} missing or zero bytes)"
drifted=$((drifted + 1))
continue
fi

compared=$((compared + 1))
if diff -u "${tracked}" "${emitted_file}"; then
echo "✓ ${tracked}"
else
echo "::error::${tracked} is out of date -- run \`just abi-gen\` and commit the result"
drifted=$((drifted + 1))
fi
done

# The denominator. A gate that cannot state how much it checked is
# not evidence -- an empty output dir must fail loudly, not print
# "ok" because the comparison loop had nothing to iterate over.
echo "connectors emitted: ${emitted}"
echo "files compared: ${compared} of ${total}"
{
echo "### ABI codegen drift"
echo ""
echo "- connectors emitted: \`${emitted}\`"
echo "- files compared: \`${compared} of ${total}\`"
} >> "${GITHUB_STEP_SUMMARY}"

if [ "${emitted}" -eq 0 ]; then
echo "::error::generator emitted 0 connectors -- it did not run, or the ABI is empty"
exit 1
fi
if [ "${compared}" -ne "${total}" ]; then
echo "::error::compared ${compared} of ${total} generated files"
exit 1
fi
if [ "${drifted}" -ne 0 ]; then
echo "::error::${drifted} generated file(s) drifted from the Idris2 ABI"
exit 1
fi
echo "No drift: every generated file matches src/Hypatia/ABI/Types.idr"
6 changes: 6 additions & 0 deletions .github/workflows/actions.lock
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,9 @@
# Docs: https://gh.io/actions-lockfile
version: 'v0.0.2'
workflows:
'.github/workflows/abi-codegen-drift.yml':
- 'actions/cache@v6.1.0'
- 'actions/checkout@v7.0.1'
'.github/workflows/bridge-gate.yml':
- 'actions/checkout@v7.0.1'
'.github/workflows/build-gossamer-gui.yml':
Expand Down Expand Up @@ -115,6 +118,9 @@ workflows:
- 'actions/checkout@v7.0.1'
- 'actions/setup-java@v6.0.1'
- 'actions/upload-artifact@v7.0.1'
'.github/workflows/zig.yml':
- 'actions/cache@v6.1.0'
- 'actions/checkout@v7.0.1'
dependencies:
'actions/attest-build-provenance@v4.2.2':
ref: 'v4.2.2'
Expand Down
124 changes: 124 additions & 0 deletions .github/workflows/zig.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,124 @@
# SPDX-License-Identifier: MPL-2.0
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# Zig wire-contract tests.
#
# Scope is deliberately narrow: `zig test ffi/zig/src/unified-api-adapter.zig`,
# NOT `zig build test`.
#
# Why. The adapter carries the `comptime` 16-connector assertion and the four
# wire-contract tests, and it was reachable from no test root at all -- none of
# `main.zig`, `json_writer.zig`, `file_ops.zig` or `test/integration_test.zig`
# imports it -- so those assertions had never executed anywhere, locally or in
# CI. `build.zig` now roots it too, but `zig build test` is independently RED
# on `main` for pre-existing reasons (below), so gating on the whole build
# would land a workflow that is red on arrival and says nothing about this
# contract.
#
# Measured 2026-09-22 with Zig 0.16.0: `zig build test` reports
# "4/11 steps succeeded (3 failed); 7/7 tests passed". Three of the four
# pre-existing roots (main.zig, file_ops.zig, test/integration_test.zig) fail to
# COMPILE against the 0.16 standard library -- 16 call sites across six removed
# or relocated symbols (std.fs.cwd, std.posix.getenv, std.fs.openFileAbsolute,
# std.fs.createFileAbsolute, std.fs.deleteFileAbsolute, std.time.timestamp),
# plus an `opaque` type declared with fields at main.zig:46. That is a
# pre-existing un-migrated tree, not a regression from this change.
#
# The 7 passing tests are json_writer.zig's 3 and this adapter's 4 -- so
# adding the adapter root took `zig build test` from 3 tests to 7.
#
# This job runs the maximal subset that is green today. Widen it to
# `zig build test` once the tree is migrated to the 0.16 std API.
#
# No `paths:` filter, deliberately -- so it stays eligible to be made a
# required check without the filter/required deadlock.

name: Zig

on:
push:
branches: [main]
pull_request:
workflow_dispatch:

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

permissions: read-all

jobs:
zig-test:
name: zig test (wire contract)
runs-on: ubuntu-latest
timeout-minutes: 15
permissions:
contents: read

env:
# Matches the owner's local toolchain
# (developer/tools/opt/mise/installs/zig/0.16.0).
ZIG_VERSION: '0.16.0'
# Official shasum for zig-x86_64-linux-0.16.0.tar.xz. Pinned rather than
# installed via a third-party action: it adds no `uses:` entry to
# actions.lock, and it cannot float the way `mise.toml`'s `zig = "latest"`
# does.
ZIG_SHA256: '70e49664a74374b48b51e6f3fdfbf437f6395d42509050588bd49abe52ba3d00'

steps:
- name: Checkout
uses: actions/checkout@v7.0.1

- name: Cache the Zig toolchain
id: cache-zig
uses: actions/cache@v6.1.0
with:
path: ~/.local/zig
key: zig-${{ env.ZIG_VERSION }}-x86_64-linux-${{ env.ZIG_SHA256 }}

- name: Install Zig
if: steps.cache-zig.outputs.cache-hit != 'true'
run: |
set -euo pipefail
tarball="zig-x86_64-linux-${ZIG_VERSION}.tar.xz"
curl -fsSL -o "/tmp/${tarball}" \
"https://ziglang.org/download/${ZIG_VERSION}/${tarball}"
echo "${ZIG_SHA256} /tmp/${tarball}" | sha256sum -c -
mkdir -p ~/.local/zig
tar -xJf "/tmp/${tarball}" -C ~/.local/zig --strip-components=1

- name: Put Zig on PATH
run: echo "$HOME/.local/zig" >> "$GITHUB_PATH"

- name: Verify the toolchain
run: |
set -euo pipefail
zig version
test "$(zig version)" = "${ZIG_VERSION}"

- name: Run the wire-contract tests
run: |
set -euo pipefail
# `zig test` writes its summary to stderr; keep both streams.
zig test ffi/zig/src/unified-api-adapter.zig 2>&1 | tee "${RUNNER_TEMP}/zig-test.log"

# The denominator. `zig test` on a file containing no `test` blocks
# exits 0 -- a green tick that proves nothing. Insist that it says
# how many it ran, and that the number is not zero.
summary=$(grep -Eo '[0-9]+ of [0-9]+ test[s]? passed|All [0-9]+ tests passed' \
"${RUNNER_TEMP}/zig-test.log" | tail -1 || true)
count=$(printf '%s' "${summary}" | grep -Eo '[0-9]+' | tail -1 || true)
count=${count:-0}

echo "zig tests run: ${count}"
{
echo "### Zig wire contract"
echo ""
echo "- root: \`ffi/zig/src/unified-api-adapter.zig\`"
echo "- tests run: \`${count}\`"
} >> "${GITHUB_STEP_SUMMARY}"

if [ "${count}" -lt 1 ]; then
echo "::error::zig test reported ${count} tests -- the wire-contract tests did not run"
exit 1
fi
15 changes: 15 additions & 0 deletions Justfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,21 @@ invariant-path *ARGS:
compile-abi:
cd src/abi && idris2 --build hypatia-abi.ipkg

# Regenerate the wire contract from the normative Idris2 ABI, then commit the
# result. The provenance stamp is a content hash of Types.idr, so ANY byte
# change to the ABI -- a comment included -- reddens abi-codegen-drift until
# this is re-run. That is deliberate: touching the normative ABI should force
# you to look at what it generated.
abi-gen:
cd src/abi && idris2 --build hypatia-abi-gen.ipkg
mkdir -p build/abi-gen/out
./build/abi-gen/exec/hypatia-abi-gen \
--out-dir build/abi-gen/out \
--abi-hash "$(git hash-object src/Hypatia/ABI/Types.idr)"
cp build/abi-gen/out/connector_generated.zig ffi/zig/src/connector_generated.zig
cp build/abi-gen/out/connector_generated.rs clients/rust/hypatia-client/src/connector_generated.rs
cp build/abi-gen/out/connectors.json ffi/connectors.json

# Compile Idris2 verification proofs
compile-verify:
cd verify && idris2 --build hypatia-verify.ipkg
Expand Down
Loading
Loading