[#92 Class E] vordr-mcp: malformed Idris2 ABI source (data declaration has no =)

[hyperpolymath]

Problem

cartridges/vordr-mcp/abi/.../Safe*.idr does not parse via iseriser abi-emit-manifest:

Error: data declaration has no \`=\`

The Idris2 source has a data declaration without an = in a position the emitter expects (most likely a data Foo : Type decl missing the variant list, or similar shape mismatch).

This is the only cartridge in the boj-server full-tree survey (standards#92 comment 4496082335) whose Idris2 source itself doesn't parse — distinct from drift (Zig FFI mismatch) or verifier-parser limits.

Fix shape

Open cartridges/vordr-mcp/abi/.../Safe*.idr, inspect the offending data decl, and fix it to either:

1. Add the missing variant list (data Foo = Bar | Baz | …), if the intent was a state machine
2. Convert to a type alias / record / etc. if data was the wrong keyword

Cross-check against a sibling cartridge's Safe*.idr for the canonical shape.

Acceptance criteria

iseriser abi-emit-manifest --idris cartridges/vordr-mcp/abi/.../Safe*.idr --cartridge vordr-mcp …
# exit 0
iseriser abi-verify …
# exit 0 (clean), exit 2 (real drift), or one of the known classes (A/B/C)

Then vordr-mcp is unblocked for the standards#92 allowlist work.

Refs hyperpolymath/standards#92 (Phase 2 allowlist expansion).
Refs hyperpolymath/standards#89 (epic — sub-issue 3).

🤖 Generated with Claude Code

[hyperpolymath]

Root cause: iseriser abi-emit-manifest did not handle GADT-style data … where declarations. The vordr-mcp SafeVordr.idr file has a valid MonotonicDegradation proof relation alongside the ADT IntegrityState, and iseriser's parser bombed on the GADT.

Fix: iseriser PR hyperpolymath/iseriser#20 — collect_data_body detects GADT form (body starts with :, not =) and skips the declaration. Proof/relation types are not exported enums and have no place in the ABI manifest.

End-to-end verification on this cartridge with the patched binary:

$ iseriser abi-emit-manifest \
    --idris cartridges/vordr-mcp/abi/VordrMcp/SafeVordr.idr \
    --cartridge vordr-mcp --out /tmp/v.json
abi-emit-manifest: wrote /tmp/v.json (0 enums, 0 transitions)

$ iseriser abi-verify --manifest /tmp/v.json --zig-ffi cartridges/vordr-mcp/ffi/vordr_ffi.zig
abi-verify: OK — cartridge \`vordr-mcp\` ABI manifest agrees with …
exit: 0

Closure path: once iseriser#20 merges + the boj-server abi-drift workflow picks up the new binary, vordr-mcp is allowlist-clean. This issue can then be closed-completed.

Refs hyperpolymath/standards#92, hyperpolymath/iseriser#20.

🤖 Generated with Claude Code