Skip to content

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

Closed
hyperpolymath wants to merge 1 commit into
mainfrom
feat/abi-verify-phase1
Closed

feat(abi-verify): structural ABI gate — Idris2 manifest ↔ Zig FFI dif…#31
hyperpolymath wants to merge 1 commit into
mainfrom
feat/abi-verify-phase1

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

…f (standards#92 Phase 1)

Adds iseriser abi-verify, a structural CI gate that diffs an Idris2-derived ABI manifest against a cartridge's Zig FFI source. Replaces today's test-only cross-check (ssg-mcp / k9iser-mcp cartridges under boj-server) with a CI-grade gate that catches:

  • enum encoding drift (variant integer value mismatches);
  • transition-allowed-but-rejected (manifest allows what Zig rejects);
  • transition-forbidden-but-accepted (manifest forbids what Zig accepts — the safety-critical class, e.g. ContentLoaded → Previewing for SSG or Generated → Applied for K9);
  • transition-accepted-but-undeclared (Zig accept-by-omission);
  • transition-table-uses-else (refuses to certify non-exhaustive switches).

Includes hand-authored reference manifests for ssg-mcp (SsgState×11, SsgEngine) and k9iser-mcp (K9State×10, K9Format), both verified clean against the live Zig FFI on boj-server main. Phase 1b will emit the manifests from the Idris2 build; this commit deliberately stops at the verification-harness boundary per the #92 design spec.

Exit code 0 = clean, 2 = drift. JSON output available via --json for CI ingestion.

33 lib tests + 9 integration tests green. New code is clippy-clean (pre- existing baseline warnings on src/scan/mod.rs left as-is).

Refs hyperpolymath/standards#92
Refs hyperpolymath/standards#89

Summary

Changes

RSR Quality Checklist

Required

  • Tests pass (just test or equivalent)
  • Code is formatted (just fmt or equivalent)
  • Linter is clean (no new warnings or errors)
  • No banned language patterns (no TypeScript, no npm/bun, no Go/Python)
  • No unsafe blocks without // SAFETY: comments
  • No banned functions (believe_me, unsafeCoerce, Obj.magic, Admitted, sorry)
  • SPDX license headers present on all new/modified source files
  • No secrets, credentials, or .env files included

As Applicable

  • .machine_readable/STATE.a2ml updated (if project state changed)
  • .machine_readable/ECOSYSTEM.a2ml updated (if integrations changed)
  • .machine_readable/META.a2ml updated (if architectural decisions changed)
  • Documentation updated for user-facing changes
  • TOPOLOGY.md updated (if architecture changed)
  • CHANGELOG or release notes updated
  • New dependencies reviewed for license compatibility (PMPL-1.0-or-later / MPL-2.0)
  • ABI/FFI changes validated (src/interface/abi/ and src/interface/ffi/ consistent)

Testing

Screenshots

…f (standards#92 Phase 1)

Adds `iseriser abi-verify`, a structural CI gate that diffs an
Idris2-derived ABI manifest against a cartridge's Zig FFI source.
Replaces today's test-only cross-check (`ssg-mcp` / `k9iser-mcp` cartridges
under boj-server) with a CI-grade gate that catches:

  * enum encoding drift (variant integer value mismatches);
  * `transition-allowed-but-rejected` (manifest allows what Zig rejects);
  * `transition-forbidden-but-accepted` (manifest forbids what Zig accepts —
    the safety-critical class, e.g. `ContentLoaded → Previewing` for SSG
    or `Generated → Applied` for K9);
  * `transition-accepted-but-undeclared` (Zig accept-by-omission);
  * `transition-table-uses-else` (refuses to certify non-exhaustive switches).

Includes hand-authored reference manifests for `ssg-mcp` (SsgState×11,
SsgEngine) and `k9iser-mcp` (K9State×10, K9Format), both verified clean
against the live Zig FFI on boj-server `main`. Phase 1b will emit the
manifests from the Idris2 build; this commit deliberately stops at the
verification-harness boundary per the #92 design spec.

Exit code 0 = clean, 2 = drift. JSON output available via `--json` for
CI ingestion.

33 lib tests + 9 integration tests green. New code is clippy-clean (pre-
existing baseline warnings on `src/scan/mod.rs` left as-is).

Refs hyperpolymath/standards#92
Refs hyperpolymath/standards#89

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath
Copy link
Copy Markdown
Owner Author

Closing as superseded. Branch tip (feat(abi-verify): structural ABI gate — Idris2 manifest ↔ Zig FFI diff (standards#92 Phase 1)) was already merged via #13. Re-diff vs current main shows merging this branch would delete ~2609 lines of subsequently-merged work — net regression.

@hyperpolymath hyperpolymath deleted the feat/abi-verify-phase1 branch May 21, 2026 07:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant