Idris2 as source-of-truth: generate/verify Zig FFI from the ABI

Idris2 as source-of-truth for the cartridge interface. Today the cartridge ABI is dual-encoded: the Idris2 contract (e.g. SafeK9iser.canTransition/exposureSatisfied) and the Zig FFI mirror are written by hand and only cross-checked by tests. The estate ideal (interface-safety policy) is the Zig interface generated from / proven against the Idris2 ABI. Affects ssg-mcp, k9iser-mcp (boj-server#73), and every future cartridge. Pre-existing pattern, not introduced by the pilot.

Root-cause analysis and design spec — Idris2 as source-of-truth for Zig FFI

Current hand-mirrored dual-encoding (verified, session 2026-05-19)

Two cartridges exhibit the pattern:

ssg-mcp (boj-server/cartridges/ssg-mcp/):

Idris2 ABI: abi/SsgMcp/SafeSsg.idr — defines SsgState (7 variants 0–6), canTransition, ssgStateToInt, ssg_can_transition (FFI shim), ssg_tool_requires_build
Zig FFI: ffi/ssg_ffi.zig — duplicates SsgState as an enum(c_int) with the same integer encodings, duplicates isValidTransition logic in a switch block
Cross-check: Zig isValidTransition is tested against known-valid/invalid transitions in unit tests; tests fail if encodings drift

k9iser-mcp (boj-server/cartridges/k9iser-mcp/, merged via #73):

Idris2 ABI: abi/K9iserMcp/SafeK9iser.idr — defines K9State, canTransition, exposureSatisfied, and FFI shims (k9_can_transition, k9_exposure_satisfied)
Zig FFI: ffi/k9iser_ffi.zig — duplicates K9State as enum(c_int), duplicates both isValidTransition and the exposure gate in Zig switch blocks
Cross-check: 5-test truth table in adapter tests cross-checks the Zig exposure gate against the Idris2 exposureSatisfied contract

The encoding contract (what must be kept in sync manually)

For each cartridge, the following are hand-duplicated between Idris2 and Zig:

State enum integer encoding — e.g. Empty=0, ContentLoaded=1, … in both ssgStateToInt (Idris2) and SsgState = enum(c_int) (Zig)
State transition relation — canTransition boolean function (Idris2) vs isValidTransition switch (Zig)
Exposure gate — exposureSatisfied (Idris2) vs exposureSatisfied (Zig)

Any discrepancy is caught only by the cross-check tests — there is no structural/type-level guarantee.

Proposed generation/verification direction

Recommended approach: ABI manifest extraction + CI diff (verification harness, not a codegen rewrite)

This is a phased plan. Full Zig codegen from Idris2 is multi-session and requires tooling that doesn't exist yet.

Phase 1 — Extractable ABI manifest (tractable now, ~1 session)

Add a step to each cartridge's Idris2 build that produces a machine-readable ABI manifest (e.g. abi-manifest.json) listing:

Each enum: name, variants with their integer values
Each transition: (fromVariant, toVariant, allowed: bool)
Each exposure rule: (required, presented, is_local, result: bool)

The Idris2 source is the authority: the manifest is derived by evaluating ssgStateToInt/k9StateToInt for all variants and canTransition/exposureSatisfied for all argument combinations.

This can be done as an Idris2 program that runs at build time and writes JSON, or as a shell script that pattern-matches the well-structured Idris2 source (both variants have consistent formatting).

Phase 2 — CI diff gate (no codegen, no rewrite)

Add a CI step that:

Reads the ABI manifest
Parses the Zig FFI file (regex or tree-sitter) to extract its enum declarations and switch cases
Diffs them: if any variant encoding or transition row disagrees, the CI step fails

This is a verification harness, not codegen. It turns the current test-only cross-check into a structural CI gate that fires before any PR merges with a drift.

Implementation: Rust or shell. A Rust tool in the iseriser repo is the right home (it already generates Zig FFI files and understands the ABI shape). Could be an abi-verify subcommand.

Phase 3 — Codegen (multi-session, blocked on tooling)

Generate the Zig FFI enum(c_int) block and isValidTransition function directly from the ABI manifest. The iseriser scaffold already has the structure (generate_zig_main in scaffold.rs) and understands the LanguageModel type system. Extending it to emit a manifest-driven Zig state machine is natural.

Requires: the ABI manifest from Phase 1. Does NOT require Idris2 compilation in CI — manifest is the intermediate representation.

Phase 4 — Proof against ABI (long-term, Idris2 FFI types)

Use Idris2's foreign type declarations to prove at the type level that the Zig symbol signatures match the Idris2 ABI contract. This is the ideal but requires Idris2 FFI work and is ~2+ sessions.

Affected files

Per cartridge:

cartridges/<name>-mcp/abi/<Module>/Safe<Name>.idr — Idris2 source-of-truth
cartridges/<name>-mcp/ffi/<name>_ffi.zig — Zig mirror (to be verified/generated)

Estate-wide: iseriser/src/codegen/scaffold.rs (generates both files for new -isers)

First safe step (executable now)

Implement abi-verify as a Rust tool in iseriser that:

Accepts --abi-manifest path/to/manifest.json and --zig-ffi path/to/ffi.zig
Parses both
Reports mismatches

A DRAFT PR implementing this can follow once the ABI manifest format is agreed. The manifest format itself is tractable to agree on in one review cycle.

This issue is explicitly multi-session. The full Idris2→Zig codegen rewrite (Phase 3+) should not be rushed before the verification harness (Phase 1+2) is in place and catching real drift.

Refs #89 (sub-issue 3)

🤖 Generated with Claude Code

Phase 1 — first safe step landed as iseriser#13 (DRAFT)

Per the #92 design spec's First safe step (executable now) recommendation, iseriser abi-verify is now implemented as a Rust subcommand on iseriser (DRAFT PR #13). Diffs an Idris2-derived ABI manifest against a cartridge's Zig FFI source; exit 0 on agreement, exit 2 on drift.

Verified clean against both pilot cartridges on boj-server main:

ssg-mcp (SsgState×11 transitions + SsgEngine) → OK
k9iser-mcp (K9State×10 transitions + K9Format) → OK

Drift classes surfaced:

enum encoding (variant integer mismatches)
transition-forbidden-but-accepted (the safety-critical class — e.g. would catch ContentLoaded → Previewing or Generated → Applied)
transition-allowed-but-rejected
transition-accepted-but-undeclared (Zig accept-by-omission)
transition-table-uses-else (refuses to certify non-exhaustive switches)

Negative control (injected drift):

$ # inject Built → Deployed in ssg_ffi.zig
abi-verify: DRIFT — cartridge `ssg-mcp` ABI manifest disagrees …
  [transition-forbidden-but-accepted] manifest forbids `Built → Deployed` but Zig `isValidTransition` accepts it
exit=2

Reference manifests (examples/abi-manifests/{ssg-mcp,k9iser-mcp}.json) hand-authored from the Idris2 source as Phase 1 specifies. schema_version: "1.0" is the contract Phase 1b's emitter should target.

Remaining for sub-issue 3:

Phase 1b — emit the manifest from the Idris2 build instead of hand-authoring (1 session, tractable next)
Phase 2 — wire abi-verify into per-cartridge CI on ssg-mcp + k9iser-mcp
Phase 3 — generate Zig FFI from manifest (multi-session)
Phase 4 — prove FFI signatures at the Idris2 type level (long-term)

Refs #89

🤖 Generated with Claude Code

feat(abi-verify): structural ABI gate — Idris2 manifest ↔ Zig FFI dif…

feat(abi-emit-manifest): emit ABI manifest from Idris2 source (standa…

ci(abi-drift): wire emit→verify gate per cartridge (standards#92 Phas…

fix(007-mcp): add missing ToolRisk enum to Zig FFI (ABI drift, standa…

feat(abi-verify): teach the converter Zig reserved words (standards#9…

fix(ci): SHA-pin actions/cache in abi-drift workflow (standards#92 fo…

Phase 1 + 1b + 2 ALL LANDED on main (2026-05-20)

Update since the Phase 1 comment above. Sub-issue 3's verification/emission pair is now end-to-end live + gated in CI.

Merged

PR	Phase	Scope
iseriser#13	Phase 1	`iseriser abi-verify` — diffs an Idris2-derived manifest against a Zig FFI; exit 0=clean, 2=drift
iseriser#14	Phase 1b	`iseriser abi-emit-manifest` — emits the manifest from `Safe.idr`; the Idris2 source is now the single authority* (no more hand-authoring)
iseriser#15	Phase 1b follow-up	Zig reserved-word converter (`error → err` workaround); unlocks airtable-mcp as a clean cartridge
boj-server#98	Phase 2	`.github/workflows/abi-drift.yml` — per-cartridge CI gate; allowlist starts at ssg-mcp + k9iser-mcp
boj-server#102	sub-fix	007-mcp `ToolRisk` enum ABI parity (surfaced by the Phase 2 spot-check)
boj-server#104	post-merge fix	SHA-pin `actions/cache` in the gate workflow (boj-server policy mandate) — gate is now CI-green

Estate findings surfaced, not yet fixed

postgresql-mcp: BeginTransaction → begin_tx etc. abbreviation drift. Separate naming-convention class (not reserved-word); fix would extend the verifier with an explicit per-variant zig_name override channel.
~77 unsurveyed cartridges with paired Safe*.idr + *_ffi.zig. Phase 2 allowlist expands as each is individually audited.
007-mcp risk-tier enforcement: only ABI parity is fixed. The Zig dispatcher does not yet gate tool invocations on ToolRisk (categoryDefaultRisk/riskPromotion are Idris2-only).

Full-tree cartridge survey — Phase 2 allowlist expansion (2026-05-20)

Aggressive batch survey of the 80 cartridges in boj-server/cartridges/ that carry a paired Safe*.idr + *_ffi.zig, using the current Phase-1b emitter + Phase-1 verifier.

Counts

Bucket	Count
Clean ✓	16
Drift (real)	63
Verifier limit	5
Idris2 src bad	1
Total	80

Clean (16) — allowlist expansion in boj-server#110

007-mcp, agent-mcp, dns-shield-mcp, feedback-mcp, fleet-mcp, iac-mcp, k8s-mcp, k9iser-mcp, local-coord-mcp, nesy-mcp, observe-mcp, opsm-mcp, pmpl-mcp, proof-mcp, secrets-mcp, ssg-mcp. (*= already enforced; 14 are new.)

007-mcp is included because the ToolRisk drift surfaced earlier is fully resolved on main via boj-server#102.

Drift taxonomy — 4 classes

Class A — `Error → error → err` emitter half-fix (~50 cartridges)

The single biggest class. Pattern, identical across every cartridge:

[variant-missing-in-zig] enum `SessionState` variant `Error` (Zig: `error`) is in the manifest but absent from the Zig FFI
[variant-extra-in-zig]   enum `SessionState` has Zig variant `err` that is not declared in the manifest

iseriser#15 taught the converter that Error → err (reserved-word avoidance) — but only on the Zig FFI side. The Phase-1b emitter (iseriser abi-emit-manifest) still emits Error → error into the manifest. So the FFI is correct, the manifest is wrong, and 50 cartridges flag a false positive against the gate.

One-line/one-file fix on iseriser emitter; allowlists ~50 cartridges in one go.

Affected (subset, full list ~50): affinescript-mcp, airtable-mcp, arango-mcp, aws-mcp, browser-mcp, buildkite-mcp, circleci-mcp, clickhouse-mcp, cloudflare-mcp, crates-mcp, database-mcp, digitalocean-mcp, discord-mcp, docker-hub-mcp, duckdb-mcp, fly-mcp, gcp-mcp, github-actions-mcp, github-api-mcp, gitlab-api-mcp, google-docs-mcp, google-sheets-mcp, grafana-mcp, hackage-mcp, hetzner-mcp, hex-mcp, jira-mcp, linear-mcp, linode-mcp, matrix-mcp, mongodb-mcp, neo4j-mcp, neon-mcp, notion-mcp, npm-registry-mcp, obsidian-mcp, opam-mcp, postgresql-mcp, prometheus-mcp, pypi-mcp, railway-mcp, redis-mcp, render-mcp, rokur-mcp, sentry-mcp, slack-mcp, supabase-mcp, telegram-mcp, todoist-mcp, turso-mcp, zotero-mcp.

Class B — multi-cap name-normalisation mismatches (~8 cartridges)

Idris2 emitter applies snake_case normalisation that the Zig source doesn't (or vice versa). Examples:

git-mcp: GitHub → git_hub (manifest) vs github (Zig)
queues-mcp: RabbitMQ → rabbit_mq (manifest) vs rabbitmq (Zig)
ums-mcp: UmsProject → ums_project (manifest) vs different Zig form
aws-mcp: DynamoDB normalisation mismatch
(similar handful)

Converter-rule fix on iseriser — establish ONE canonical normalisation and apply consistently both ends.

Class C — genuine missing-enum-in-Zig (~6 cartridges)

The Idris2 source declares an enum the Zig FFI doesn't have at all. Real ABI gap, per-cartridge fix needed:

Cartridge	Missing Zig enum(s)
`cloud-mcp`	`CloudflareResource`, `VercelResource`
`comms-mcp`	`GmailResource`, `CalendarResource`
`ml-mcp`	`HuggingFaceResource`
`research-mcp`	`ResearchResource`
`gitlab-api-mcp`	(one enum)
`mongodb-mcp`	`BsonFieldType`

These are 007-mcp-style fixes — same shape as boj-server#102.

Verifier parser limitation (5 cartridges) — `iseriser` bug, not cartridge drift

bsp-mcp, container-mcp, dap-mcp, lsp-mcp, vault-mcp: the Zig parser in abi-verify rejects switch arms whose chunk is false rather than to == .<v>. Pure tooling issue — file on iseriser.

Idris2 source malformed (1 cartridge)

vordr-mcp/abi/.../Safe*.idr — emitter fails with "data declaration has no =". Per-cartridge fix in the cartridge itself.

Asks (owner decision before sub-issue filing)

Filing 63 individual sub-issues is noise. Proposed structuring (the user previously OK'd this batched survey form):

iseriser sub-issue — Class A emitter half-fix (Error → err), one-file change, unblocks ~50 cartridges.
iseriser sub-issue — Class B name-normalisation canonicalisation (~8 cartridges).
iseriser sub-issue — verifier Zig-parser tolerance for non-canonical switch arm forms (5 cartridges).
standards#92 sub-issues × 6 — one per Class C cartridge with a missing enum (per-cartridge ABI work, same shape as boj-server#102).
boj-server cartridge sub-issue — vordr-mcp Idris2 source fix.

= 3 iseriser + 6 standards + 1 boj-server = 10 sub-issues, not 63. Awaiting owner go-ahead before filing.

Refs #89 (epic — sub-issue 3).

🤖 Generated with Claude Code

chore(abi-drift): expand allowlist from 2 → 16 (full-tree survey) (#110)

fix(abi): accept runtogether form for multi-cap acronym variants (ise…

fix(abi-verify): tolerate non-canonical Zig switch arm `false` shorth…

ci(abi-drift): expand allowlist 56 -> 66 (Refs standards#92) (#133)

fix(browser-mcp): rename BrowserAction.Type -> TypeText (#134)

chore(abi-drift): restore browser-mcp to allowlist after #134 landed (#…

fix(abi-emit-manifest): skip GADT-style `data … where` declarations (#34

fix(abi): accept runtogether form for multi-cap acronym variants (ise…

fix(abi-verify): tolerate non-canonical Zig switch arm `false` shorth…

fix(abi-emit-manifest): skip GADT-style `data … where` declarations (#37

fix(abi-emit-manifest): skip GADT-style `data … where` declarations (#38

ci(abi-drift): SHA-pin iseriser, drop sticky restore-keys (#111) (#172)

Next step (re-verified 2026-08-27): unstarted, premise intact — boj-server/ffi/zig/src/ is hand-written with no generator, no gen script, no generation step in any workflow or Justfile.

→ The first commit is a design decision, not a sweep: either generate the Zig from the Idris2 ABI, or emit a conformance checker from it. Structurally this is sub-issue 3 of #89 but separable. Recommend deciding the direction in a short ADR before any code.

Navigation Menu

Repository navigation

Idris2 as source-of-truth: generate/verify Zig FFI from the ABI #92

Root-cause analysis and design spec — Idris2 as source-of-truth for Zig FFI

Current hand-mirrored dual-encoding (verified, session 2026-05-19)

The encoding contract (what must be kept in sync manually)

Proposed generation/verification direction

Phase 1 — Extractable ABI manifest (tractable now, ~1 session)

Phase 2 — CI diff gate (no codegen, no rewrite)

Phase 3 — Codegen (multi-session, blocked on tooling)

Phase 4 — Proof against ABI (long-term, Idris2 FFI types)

Affected files

First safe step (executable now)

Phase 1 — first safe step landed as iseriser#13 (DRAFT)

Phase 1 + 1b + 2 ALL LANDED on main (2026-05-20)

Merged

Estate findings surfaced, not yet fixed

Next

Full-tree cartridge survey — Phase 2 allowlist expansion (2026-05-20)

Counts

Clean (16) — allowlist expansion in boj-server#110

Drift taxonomy — 4 classes

Class A — `Error → error → err` emitter half-fix (~50 cartridges)

Class B — multi-cap name-normalisation mismatches (~8 cartridges)

Class C — genuine missing-enum-in-Zig (~6 cartridges)

Verifier parser limitation (5 cartridges) — `iseriser` bug, not cartridge drift

Idris2 source malformed (1 cartridge)

Asks (owner decision before sub-issue filing)

11 remaining items

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Idris2 as source-of-truth: generate/verify Zig FFI from the ABI #92

Description

Activity

hyperpolymath commented on May 19, 2026

Root-cause analysis and design spec — Idris2 as source-of-truth for Zig FFI

Current hand-mirrored dual-encoding (verified, session 2026-05-19)

The encoding contract (what must be kept in sync manually)

Proposed generation/verification direction

Phase 1 — Extractable ABI manifest (tractable now, ~1 session)

Phase 2 — CI diff gate (no codegen, no rewrite)

Phase 3 — Codegen (multi-session, blocked on tooling)

Phase 4 — Proof against ABI (long-term, Idris2 FFI types)

Affected files

First safe step (executable now)

hyperpolymath commented on May 20, 2026

Phase 1 — first safe step landed as iseriser#13 (DRAFT)

hyperpolymath commented on May 20, 2026

Phase 1 + 1b + 2 ALL LANDED on main (2026-05-20)

Merged

Estate findings surfaced, not yet fixed

Next

hyperpolymath commented on May 20, 2026

Full-tree cartridge survey — Phase 2 allowlist expansion (2026-05-20)

Counts

Clean (16) — allowlist expansion in boj-server#110

Drift taxonomy — 4 classes

Class A — Error → error → err emitter half-fix (~50 cartridges)

Class B — multi-cap name-normalisation mismatches (~8 cartridges)

Class C — genuine missing-enum-in-Zig (~6 cartridges)

Verifier parser limitation (5 cartridges) — iseriser bug, not cartridge drift

Idris2 source malformed (1 cartridge)

Asks (owner decision before sub-issue filing)

11 remaining items

hyperpolymath commented on Aug 27, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions

Class A — `Error → error → err` emitter half-fix (~50 cartridges)

Verifier parser limitation (5 cartridges) — `iseriser` bug, not cartridge drift