Skip to content

Commit aa2484c

Browse files
feat(abi-emit-manifest): emit ABI manifest from Idris2 source (standards#92 Phase 1b) (#14)
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>
1 parent 89cbe0c commit aa2484c

4 files changed

Lines changed: 630 additions & 6 deletions

File tree

examples/abi-manifests/README.adoc

Lines changed: 48 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -28,12 +28,54 @@ reports drift in three categories:
2828

2929
== Phase boundary
3030

31-
Phase 1 (this commit) is a *verification harness*, not codegen. The
32-
manifests are hand-authored from the Idris2 source. Phase 1b will emit
33-
the manifest from the Idris2 build at compile time; Phase 2 will wire
34-
the verifier into per-cartridge CI; Phase 3 generates the Zig FFI from
35-
the manifest; Phase 4 proves the FFI signatures at the Idris2 type
36-
level.
31+
Phase 1 (the `abi-verify` subcommand) is a *verification harness*, not
32+
codegen. Phase 1b (the `abi-emit-manifest` subcommand, this section)
33+
emits the manifest from the Idris2 source — so the Idris2 source is
34+
now the *single authority* and hand-authoring drops out. Phase 2 will
35+
wire the emit→verify pair into per-cartridge CI; Phase 3 generates the
36+
Zig FFI from the manifest; Phase 4 proves the FFI signatures at the
37+
Idris2 type level.
38+
39+
=== Emit a manifest from Idris2
40+
41+
[source,bash]
42+
----
43+
iseriser abi-emit-manifest \
44+
--idris ../boj-server/cartridges/ssg-mcp/abi/SsgMcp/SafeSsg.idr \
45+
--cartridge ssg-mcp \
46+
--source-path "boj-server/cartridges/ssg-mcp/abi/SsgMcp/SafeSsg.idr" \
47+
--out /tmp/ssg-mcp.json
48+
# then pipe straight into the verifier:
49+
iseriser abi-verify --manifest /tmp/ssg-mcp.json --zig-ffi ../boj-server/cartridges/ssg-mcp/ffi/ssg_ffi.zig
50+
----
51+
52+
The emitter parses:
53+
54+
* `data <Enum> = A | B | C` (one-line or multi-line form, with or
55+
without parameterised variants like `Custom String`)
56+
* `<fn> : <Enum> -> Int` type signatures (to associate enums with
57+
their `*ToInt` functions, since the convention is loose — `SsgEngine`
58+
uses `engineToInt`, `K9Format` uses `formatToInt`)
59+
* `<fn> <variant> = <int>` value-encoding equations (including
60+
parameterised forms like `(Custom _) = 99`)
61+
* `canTransition <From> <To> = True` allowed-transition equations
62+
(`canTransition _ _ = False` catch-all is skipped — accept-by-omission
63+
is caught by the verifier separately)
64+
65+
=== What the emitter does NOT preserve
66+
67+
Hand-authored manifests can include `allowed: false` rows that
68+
*explicitly* pin safety-critical invariants — e.g.
69+
`ContentLoaded → Previewing` in ssg-mcp, or `Generated → Applied` in
70+
k9iser-mcp. These have documentation value but no enforcement value:
71+
the verifier's `transition-accepted-but-undeclared` finding catches
72+
the same drift class. The emitter does not generate them — round-tripping
73+
through emit replaces the explicit `allowed:false` rows with
74+
accept-by-omission protection.
75+
76+
The hand-authored reference manifests in this directory keep the
77+
`allowed:false` rows as readable documentation. CI uses the emitted
78+
form (no `allowed:false` rows; same safety).
3779

3880
== Usage
3981

0 commit comments

Comments
 (0)