Repository navigation
Idris2 as source-of-truth: generate/verify Zig FFI from the ABI #92
Description
Activity
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— definesSsgState(7 variants 0–6),canTransition,ssgStateToInt,ssg_can_transition(FFI shim),ssg_tool_requires_build - Zig FFI:
ffi/ssg_ffi.zig— duplicatesSsgStateas anenum(c_int)with the same integer encodings, duplicatesisValidTransitionlogic in aswitchblock - Cross-check: Zig
isValidTransitionis 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— definesK9State,canTransition,exposureSatisfied, and FFI shims (k9_can_transition,k9_exposure_satisfied) - Zig FFI:
ffi/k9iser_ffi.zig— duplicatesK9Stateasenum(c_int), duplicates bothisValidTransitionand the exposure gate in Zigswitchblocks - Cross-check: 5-test truth table in adapter tests cross-checks the Zig exposure gate against the Idris2
exposureSatisfiedcontract
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 bothssgStateToInt(Idris2) andSsgState = enum(c_int)(Zig) - State transition relation —
canTransitionboolean function (Idris2) vsisValidTransitionswitch (Zig) - Exposure gate —
exposureSatisfied(Idris2) vsexposureSatisfied(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/k9StateToIntfor all variants andcanTransition/exposureSatisfiedfor 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
iseriserrepo is the right home (it already generates Zig FFI files and understands the ABI shape). Could be anabi-verifysubcommand.Phase 3 — Codegen (multi-session, blocked on tooling)
Generate the Zig FFI
enum(c_int)block andisValidTransitionfunction directly from the ABI manifest. The iseriser scaffold already has the structure (generate_zig_maininscaffold.rs) and understands theLanguageModeltype 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-truthcartridges/<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-verifyas a Rust tool iniseriserthat:- Accepts
--abi-manifest path/to/manifest.jsonand--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
- Idris2 ABI:
Phase 1 — first safe step landed as iseriser#13 (DRAFT)
Per the #92 design spec's First safe step (executable now) recommendation,
iseriser abi-verifyis now implemented as a Rust subcommand oniseriser(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) → OKk9iser-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 catchContentLoaded → PreviewingorGenerated → Applied)transition-allowed-but-rejectedtransition-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=2Reference 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-verifyinto per-cartridge CI onssg-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
- added 6 commits that reference this issue
on May 20, 2026 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=driftiseriser#14 Phase 1b iseriser abi-emit-manifest— emits the manifest fromSafe*.idr; the Idris2 source is now the single authority (no more hand-authoring)iseriser#15 Phase 1b follow-up Zig reserved-word converter ( error → errworkaround); unlocks airtable-mcp as a clean cartridgeboj-server#98 Phase 2 .github/workflows/abi-drift.yml— per-cartridge CI gate; allowlist starts at ssg-mcp + k9iser-mcpboj-server#102 sub-fix 007-mcp ToolRiskenum ABI parity (surfaced by the Phase 2 spot-check)boj-server#104 post-merge fix SHA-pin actions/cachein the gate workflow (boj-server policy mandate) — gate is now CI-greenEstate findings surfaced, not yet fixed
- postgresql-mcp:
BeginTransaction → begin_txetc. abbreviation drift. Separate naming-convention class (not reserved-word); fix would extend the verifier with an explicit per-variantzig_nameoverride 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/riskPromotionare Idris2-only).
Next
Phase 3 (codegen Zig FFI from manifest) and Phase 4 (Idris2 FFI type proof) remain, both multi-session.
Sub-issue 3 of #89 is meaningfully advanced but not closed; joint-close on owner agreement only.
Refs #89
🤖 Generated with Claude Code
- postgresql-mcp:
- added a commit that references this issue
on May 20, 2026 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 pairedSafe*.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-mcpis included because theToolRiskdrift surfaced earlier is fully resolved on main via boj-server#102.Drift taxonomy — 4 classes
Class A —
Error → error → erremitter 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 manifestiseriser#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 emitsError → errorinto 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
iseriseremitter; 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) vsgithub(Zig)queues-mcp:RabbitMQ → rabbit_mq(manifest) vsrabbitmq(Zig)ums-mcp:UmsProject → ums_project(manifest) vs different Zig formaws-mcp:DynamoDBnormalisation 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-mcpCloudflareResource,VercelResourcecomms-mcpGmailResource,CalendarResourceml-mcpHuggingFaceResourceresearch-mcpResearchResourcegitlab-api-mcp(one enum) mongodb-mcpBsonFieldTypeThese are 007-mcp-style fixes — same shape as boj-server#102.
Verifier parser limitation (5 cartridges) —
iseriserbug, not cartridge driftbsp-mcp,container-mcp,dap-mcp,lsp-mcp,vault-mcp: the Zig parser inabi-verifyrejects switch arms whose chunk isfalserather thanto == .<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-mcpIdris2 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
- added a commit that references this issue
on May 20, 2026 11 remaining items
- added 10 commits that reference this issue
on May 20, 2026 - added a commit that references this issue
on Jun 1, 2026 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.
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.