feat(abi-emit-manifest): emit ABI manifest from Idris2 source (standa…#30
Closed
hyperpolymath wants to merge 1 commit into
Closed
feat(abi-emit-manifest): emit ABI manifest from Idris2 source (standa…#30hyperpolymath wants to merge 1 commit into
hyperpolymath wants to merge 1 commit into
Conversation
…rds#92 Phase 1b)
Phase 1b of standards#89 sub-issue 3 / standards#92. Adds the
`abi-emit-manifest` subcommand, which parses a cartridge's `Safe*.idr`
and emits the JSON manifest the existing `abi-verify` subcommand
consumes. Together with Phase 1 this closes the loop: the Idris2 source
is now the **single authority** — the manifest is derived, not
hand-authored.
## Scope
Parses the cartridge convention shape:
* `data <Enum> = A | B | C` (one-line or multi-line; with or without
parameterised variants like `Custom String`)
* `<fn> : <Enum> -> Int` type signatures (associates each enum with
its `*ToInt` function; necessary because the convention is loose —
`SsgEngine` uses `engineToInt`, `K9Format` uses `formatToInt`,
not the naive `ssgEngineToInt` etc.)
* `<fn> <variant> = <int>` value-encoding equations (including
parameterised forms like `(Custom _) = 99`)
* `canTransition <From> <To> = True` allowed-transition equations
(catch-all `_ _ = False` skipped; the verifier already catches
accept-by-omission as drift)
Not a general Idris2 parser; deliberately shape-specific.
## End-to-end smoke
```
$ iseriser abi-emit-manifest \
--idris ../boj-server/cartridges/ssg-mcp/abi/SsgMcp/SafeSsg.idr \
--cartridge ssg-mcp \
--source-path "boj-server/cartridges/ssg-mcp/abi/SsgMcp/SafeSsg.idr" \
--out /tmp/ssg.json
abi-emit-manifest: wrote /tmp/ssg.json (2 enums, 11 transitions)
$ iseriser abi-verify --manifest /tmp/ssg.json \
--zig-ffi ../boj-server/cartridges/ssg-mcp/ffi/ssg_ffi.zig
abi-verify: OK — cartridge `ssg-mcp` ABI manifest agrees with `…/ssg_ffi.zig`
```
Same for `k9iser-mcp` (2 enums, 10 transitions, verify clean).
The diff between hand-authored and emitted manifests is just JSON
formatting + the absence of the `allowed:false` safety-invariant rows
(documented in README.adoc — the verifier's
`transition-accepted-but-undeclared` finding covers the same drift
class, so safety is preserved). Verify result is identical.
## Tests
6 new unit tests in `idris_emitter::tests`:
* one-line data declaration
* multi-line data declaration with parameterised variant
* type-signature-based fn↔enum association (the SsgEngine→engineToInt case)
* variant without ToInt mapping is dropped
* canTransition parsing skips the catch-all
* Idris2 doc-comment stripping
39 lib tests green (was 33).
Next: Phase 2 — wire the emit→verify pair into per-cartridge CI.
Refs hyperpolymath/standards#92
Refs hyperpolymath/standards#89
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Owner
Author
|
Closing as superseded. Branch tip ( |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
…rds#92 Phase 1b)
Phase 1b of standards#89 sub-issue 3 / standards#92. Adds the
abi-emit-manifestsubcommand, which parses a cartridge'sSafe*.idrand emits the JSON manifest the existingabi-verifysubcommand consumes. Together with Phase 1 this closes the loop: the Idris2 source is now the single authority — the manifest is derived, not hand-authored.Scope
Parses the cartridge convention shape:
data <Enum> = A | B | C(one-line or multi-line; with or without parameterised variants likeCustom String)<fn> : <Enum> -> Inttype signatures (associates each enum with its*ToIntfunction; necessary because the convention is loose —SsgEngineusesengineToInt,K9FormatusesformatToInt, not the naivessgEngineToIntetc.)<fn> <variant> = <int>value-encoding equations (including parameterised forms like(Custom _) = 99)canTransition <From> <To> = Trueallowed-transition equations (catch-all_ _ = Falseskipped; the verifier already catches accept-by-omission as drift)Not a general Idris2 parser; deliberately shape-specific.
End-to-end smoke
Same for
k9iser-mcp(2 enums, 10 transitions, verify clean).The diff between hand-authored and emitted manifests is just JSON formatting + the absence of the
allowed:falsesafety-invariant rows (documented in README.adoc — the verifier'stransition-accepted-but-undeclaredfinding covers the same drift class, so safety is preserved). Verify result is identical.Tests
6 new unit tests in
idris_emitter::tests:39 lib tests green (was 33).
Next: Phase 2 — wire the emit→verify pair into per-cartridge CI.
Refs hyperpolymath/standards#92
Refs hyperpolymath/standards#89
Summary
Changes
RSR Quality Checklist
Required
just testor equivalent)just fmtor equivalent)unsafeblocks without// SAFETY:commentsbelieve_me,unsafeCoerce,Obj.magic,Admitted,sorry).envfiles includedAs Applicable
.machine_readable/STATE.a2mlupdated (if project state changed).machine_readable/ECOSYSTEM.a2mlupdated (if integrations changed).machine_readable/META.a2mlupdated (if architectural decisions changed)TOPOLOGY.mdupdated (if architecture changed)CHANGELOGor release notes updatedsrc/interface/abi/andsrc/interface/ffi/consistent)Testing
Screenshots