Skip to content

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

Merged
hyperpolymath merged 1 commit into
mainfrom
fix/abi-emit-skip-gadt-data
May 20, 2026
Merged

fix(abi-emit-manifest): skip GADT-style data … where declarations#20
hyperpolymath merged 1 commit into
mainfrom
fix/abi-emit-skip-gadt-data

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

  • iseriser abi-emit-manifest bombed with `data declaration has no `=`` on any Idris2 module containing a GADT — e.g. boj-server's vordr-mcp `MonotonicDegradation` proof relation.
  • These are proof / relation types, not exported enums; the emitter now detects GADT form (`data Foo : … where …`) and skips them, the way it already walks past records/interfaces/functions.
  • Two unit tests added (vordr-mcp shape + degenerate signature-only GADT). End-to-end verified against the real cartridge: emit exits 0 + abi-verify clean.

Refs

Test plan

  • `cargo test --release` (lib + integration): 8 emitter tests + 9 integration tests pass
  • Real-cartridge smoke: `iseriser abi-emit-manifest` against vordr-mcp's SafeVordr.idr now exits 0
  • Real-cartridge follow-on: `iseriser abi-verify` on the emitted manifest exits 0 (clean)
  • CI green on this PR
  • Post-merge: `cargo build --release` consumers (boj-server abi-drift workflow) pick up the fixed binary

🤖 Generated with Claude Code

`iseriser abi-emit-manifest` bombed with "data declaration has no `=`"
on any Idris2 module that declared a GADT — e.g. boj-server's
vordr-mcp `MonotonicDegradation` proof relation:

    data MonotonicDegradation : IntegrityState -> IntegrityState -> Type where
      StayHealthy  : MonotonicDegradation Healthy Healthy
      ...

These are proof / relation types, not exported enums, and have no
place in the ABI manifest. The emitter must walk past them without
choking the way it must already walk past records, interfaces, and
function definitions.

`collect_data_body` now detects GADT form (body starts with `:`,
not `=`) and delegates to a new `skip_gadt_block` helper that
consumes the type signature + indented constructor block. Empty
variant lists were already silently dropped by `parse_enum_declarations`
so no further plumbing is needed.

Two unit tests added: a vordr-mcp shape (real ADT + sibling GADT +
to-int mapping) and a degenerate signature-only GADT (`data Phantom :
Type` with no `where`). Both pass; all 8 emitter tests + 9 integration
tests stay green.

Verified end-to-end against the real cartridge:

    $ iseriser abi-emit-manifest \
        --idris …/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 …/vordr_ffi.zig
    abi-verify: OK
    exit: 0

Refs hyperpolymath/standards#92 (Phase 2 allowlist expansion).
Refs hyperpolymath/boj-server#111 (the cartridge that motivated the fix).

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

🔍 Hypatia Security Scan

Findings: 19 issues detected

Severity Count
🔴 Critical 2
🟠 High 5
🟡 Medium 12

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/upload-artifact@v4 needs attention",
    "type": "unpinned_action",
    "file": "release.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/download-artifact@v4 needs attention",
    "type": "unpinned_action",
    "file": "release.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "codeql.yml lists `language: javascript-typescript` but the repo has no source files in any CodeQL-scannable language. The analyze job will exit 'no source files' on every run. Switch the matrix to `actions` (which scans workflow files — every repo has those).",
    "type": "codeql_language_matrix_mismatch",
    "file": "codeql.yml",
    "action": "switch_codeql_matrix_to_actions",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "unwrap_or(0) with dangerous default (1 occurrences, CWE-754)",
    "type": "unwrap_dangerous_default",
    "file": "/home/runner/work/iseriser/iseriser/src/abi/zig_ffi_parser.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "unwrap() without prior check -- DoS via panic (1 occurrences, CWE-754)",
    "type": "unwrap_without_check",
    "file": "/home/runner/work/iseriser/iseriser/src/abi/idris_emitter.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "expect() in hot path (14 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/iseriser/iseriser/src/codegen/scaffold.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  },
  {
    "reason": "expect() in hot path (11 occurrences, CWE-754)",
    "type": "expect_in_hot_path",
    "file": "/home/runner/work/iseriser/iseriser/benches/iseriser_bench.rs",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath hyperpolymath merged commit 3f06d72 into main May 20, 2026
14 of 16 checks passed
hyperpolymath added a commit to hyperpolymath/boj-server that referenced this pull request May 20, 2026
## Summary

Re-surveyed all 81 paired cartridges against the freshly-merged iseriser
binary (#20 GADT-skip emitter, #21 runtogether candidate, #22
terminal-\`false\` switch-arm tolerance). Allowlist grows from **56 →
66** cartridges.

### Newly clean (+11) — unblocked by iseriser #20/#21/#22

\`chapeliser-mcp\`, \`cloud-mcp\`, \`comms-mcp\`, \`container-mcp\`,
\`git-mcp\`, \`gitlab-api-mcp\`, \`ml-mcp\`, \`mongodb-mcp\`,
\`queues-mcp\`, \`research-mcp\`, \`vordr-mcp\`

### Newly drifting (-1) — browser-mcp

Genuine cartridge-side drift: Idris2 \`BrowserAction.Type\` (Zig
candidate \`type\`) vs Zig \`type_text\`. Cartridge-side fix needed, not
a verifier defect; not Class B/C/D — filed as out-of-scope.

### Class taxonomy after the fixes

| Class | Pre-PR | Post-PR | Status |
| --- | --- | --- | --- |
| Clean (allowlist) | 56 | **66** | this PR |
| Class B (name-norm) | covered | partial | iseriser#21 closed multi-cap
acronyms; remaining ums-mcp prefix-stripping is open |
| Class C (missing Zig enum) | tracked | tracked | standards#150-155 |
| Class D (abbreviation/acronym boundary) | implicit | filed |
standards#156 (3 cartridges: postgresql/hetzner/redis) |
| Class P (verifier parser limit) | 5 | **0** | iseriser#22 closed |
| Class E (malformed Idris2 source) | 1 | **0** | iseriser#20 closed |

## Test plan

- [x] Local re-survey on \`origin/main\` snapshot (zero cartridge
changes between survey and this PR's base commit)
- [x] All 66 cartridges in the new list verified \`abi-verify: OK\`
- [x] Removed cartridge (browser-mcp) verified to actually drift
- [ ] CI green on this PR (the workflow itself runs the same
66-cartridge check)

Refs hyperpolymath/standards#92, hyperpolymath/standards#89,
hyperpolymath/iseriser#20, hyperpolymath/iseriser#21,
hyperpolymath/iseriser#22.

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

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 20, 2026
PR #26 cross-referenced `examples/cartridge-skeleton/README.adoc` from
`README.adoc` but never created it. ROADMAP.adoc still ended at Phase 0
even though Phase 2b (standards#89) and standards#92 Phase 1+1b both
landed today. Cleaning both up.

- `examples/cartridge-skeleton/README.adoc`: a full worked example —
  manifest, CLI invocation, expected output, the three end-to-end
  verification commands (`idris2 --build`, `zig build test` on `ffi/`
  and `adapter/`), a customising-the-cartridge guide for adding tools,
  and the cross-references (standards#89/#90/#91, ADR-0004, ADR-0006,
  k9iser-mcp pilot). Mirrors the style of the existing
  `examples/abi-manifests/README.adoc`.
- `ROADMAP.adoc`: new "Phase 2b: BoJ-server cartridge skeleton"
  section marking the cartridge scaffolder COMPLETE with checked
  boxes for each piece (13-file emit, Idris2 ABI, ADR-0006 5-symbol C
  ABI, unified gated adapter, end-to-end build verification, docs).
  Also a new "ABI verification harness" section marking standards#92
  Phase 1 + 1b COMPLETE (`abi-verify` + `abi-emit-manifest` + four
  emitter/verifier fixes from iseriser #15/#20/#21/#22 + the
  `abi-manifests` docs). Notes that the standards#90 fan-out across
  the 28 -isers stays correctly gated on standards#91.

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

Co-authored-by: Claude Opus 4.7 (1M context) <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