Skip to content

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

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…#41
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 already integrated on main. Verified with git cherry: the PR head is patch-equivalent to origin/main, and current main passes cargo test.

@hyperpolymath
hyperpolymath deleted the feat/abi-verify-phase1 branch May 21, 2026 07:02
hyperpolymath added a commit that referenced this pull request Aug 25, 2026
…t) (#98)

Pins `hyperpolymath/standards@5b1d00229e5e…`, which **does not exist**
(`gh api` → 422 "No commit found for SHA").

A workflow that cannot resolve its reusable dies at `startup_failure`
with **zero jobs** — no logs, no annotation. It therefore produces no
check runs, which is why required contexts such as `governance /
Validate Hypatia Baseline` register as *phantom* and block every PR in
the repo.

Repinned to `d5fe075a` (current `standards` main).

**Verified, not assumed:** hyperpolymath/hypatia#722 applied this same
fix and `governance / Validate Hypatia Baseline` went from absent to
**produced**; Mirror, Secret Scanner and Hypatia Scan went from
`startup_failure` to `success`.

**How it was caught:** `5b1d0022…0fbfedc7e80f37ea50f49236` and
`d135b05b…0fbfedc7e80f37ea50f49236` share a 24-character suffix — real
git SHAs don't collide like that. Of 27 distinct `standards` pins in
estate use, 26 resolve and this one does not.

Scope measured live: 27 references across 15 repos. `rsr-template-repo`
was fixed first (#41 there) as the RSR spine, since it propagates the
defect to every newly minted repository.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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