Skip to content

Commit 89cbe0c

Browse files
feat(abi-verify): structural ABI gate — Idris2 manifest ↔ Zig FFI diff (standards#92 Phase 1) (#13)
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>
1 parent 109b656 commit 89cbe0c

8 files changed

Lines changed: 995 additions & 0 deletions

File tree

examples/abi-manifests/README.adoc

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
= ABI manifests
2+
:source-highlighter: pygments
3+
4+
Phase 1 of https://github.com/hyperpolymath/standards/issues/89[standards#89]
5+
sub-issue 3 / https://github.com/hyperpolymath/standards/issues/92[standards#92].
6+
7+
== Purpose
8+
9+
The Idris2 `Safe*.idr` source defines a cartridge's ABI contract (state
10+
enum encoding + transition relation). The Zig FFI mirror hand-duplicates
11+
this contract. Today the cross-check is test-only.
12+
13+
`iseriser abi-verify` turns the cross-check into a structural CI gate: it
14+
diffs an Idris2-derived ABI manifest against the Zig FFI source and
15+
reports drift in three categories:
16+
17+
* `variant-value-mismatch` / `variant-missing-in-zig` / `variant-extra-in-zig`
18+
— enum encoding drift.
19+
* `transition-allowed-but-rejected` — manifest allows a transition the
20+
Zig switch rejects.
21+
* `transition-forbidden-but-accepted` — manifest forbids a transition
22+
the Zig switch accepts (this is the safety-critical class: e.g.
23+
`ContentLoaded → Previewing`, `Generated → Applied`).
24+
* `transition-accepted-but-undeclared` — Zig accepts a transition the
25+
manifest neither allows nor forbids (accept-by-omission is drift).
26+
* `transition-table-uses-else` — Zig switch uses `else =>`; the gate
27+
refuses to certify non-exhaustive switches.
28+
29+
== Phase boundary
30+
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.
37+
38+
== Usage
39+
40+
[source,bash]
41+
----
42+
# From an iseriser checkout:
43+
cargo run -- abi-verify \
44+
--manifest examples/abi-manifests/ssg-mcp.json \
45+
--zig-ffi ../boj-server/cartridges/ssg-mcp/ffi/ssg_ffi.zig
46+
47+
# JSON output for CI ingestion:
48+
cargo run -- abi-verify --json --manifest <m> --zig-ffi <f>
49+
----
50+
51+
Exit code `0` means clean; `2` means drift (with the report on stderr
52+
in the human form, or stdout JSON when `--json` is set).
53+
54+
== Reference manifests
55+
56+
* `ssg-mcp.json` — covers `SsgState` (7 variants), `SsgEngine`
57+
(5 variants), and the 11-row transition table from
58+
`SafeSsg.idr::canTransition`. Pins the two safety invariants
59+
`ContentLoaded → Previewing` (must build first) and
60+
`Built → Deployed` (must preview first) as `allowed: false`.
61+
* `k9iser-mcp.json` — covers `K9State` (6 variants), `K9Format`
62+
(5 variants), and the 10-row transition table from
63+
`SafeK9iser.idr::canTransition`. Pins `Generated → Applied` (must
64+
validate first) and `ManifestLoaded → Validated` (must generate
65+
first) as `allowed: false`.
66+
67+
Both manifests verify clean against the corresponding Zig FFI on
68+
boj-server `main` at the cut date of this PR.
69+
70+
== Schema
71+
72+
[source,json]
73+
----
74+
{
75+
"schema_version": "1.0",
76+
"cartridge": "<name>",
77+
"source_idris": "path/to/Safe<Name>.idr",
78+
"enums": [
79+
{ "name": "CamelCase",
80+
"variants": [ { "name": "CamelCase", "value": 0 }, ... ] }
81+
],
82+
"transition_table": {
83+
"state_enum": "CamelCase",
84+
"rows": [
85+
{ "from": "CamelCase", "to": "CamelCase", "allowed": true|false }
86+
]
87+
}
88+
}
89+
----
90+
91+
Variant names are the Idris2-side CamelCase. The verifier maps each
92+
to its Zig snake_case form via the hyperpolymath cartridge convention
93+
(`ManifestLoaded → manifest_loaded`, `K9Error → k9_error`,
94+
`SsgError → ssg_error`, `ReadyToDeploy → ready_to_deploy`).
Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
{
2+
"schema_version": "1.0",
3+
"cartridge": "k9iser-mcp",
4+
"source_idris": "boj-server/cartridges/k9iser-mcp/abi/K9iserMcp/SafeK9iser.idr",
5+
"enums": [
6+
{
7+
"name": "K9State",
8+
"variants": [
9+
{ "name": "Empty", "value": 0 },
10+
{ "name": "ManifestLoaded", "value": 1 },
11+
{ "name": "Generated", "value": 2 },
12+
{ "name": "Validated", "value": 3 },
13+
{ "name": "Applied", "value": 4 },
14+
{ "name": "K9Error", "value": 5 }
15+
]
16+
},
17+
{
18+
"name": "K9Format",
19+
"variants": [
20+
{ "name": "Toml", "value": 1 },
21+
{ "name": "Yaml", "value": 2 },
22+
{ "name": "Json", "value": 3 },
23+
{ "name": "Ini", "value": 4 },
24+
{ "name": "Custom", "value": 99 }
25+
]
26+
}
27+
],
28+
"transition_table": {
29+
"state_enum": "K9State",
30+
"rows": [
31+
{ "from": "Empty", "to": "ManifestLoaded", "allowed": true },
32+
{ "from": "ManifestLoaded", "to": "Generated", "allowed": true },
33+
{ "from": "Generated", "to": "Generated", "allowed": true },
34+
{ "from": "Generated", "to": "Validated", "allowed": true },
35+
{ "from": "Validated", "to": "Applied", "allowed": true },
36+
{ "from": "Applied", "to": "Empty", "allowed": true },
37+
{ "from": "Validated", "to": "Empty", "allowed": true },
38+
{ "from": "ManifestLoaded", "to": "K9Error", "allowed": true },
39+
{ "from": "Generated", "to": "K9Error", "allowed": true },
40+
{ "from": "K9Error", "to": "Empty", "allowed": true },
41+
{ "from": "ManifestLoaded", "to": "Validated", "allowed": false },
42+
{ "from": "Generated", "to": "Applied", "allowed": false }
43+
]
44+
}
45+
}
Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
{
2+
"schema_version": "1.0",
3+
"cartridge": "ssg-mcp",
4+
"source_idris": "boj-server/cartridges/ssg-mcp/abi/SsgMcp/SafeSsg.idr",
5+
"enums": [
6+
{
7+
"name": "SsgState",
8+
"variants": [
9+
{ "name": "Empty", "value": 0 },
10+
{ "name": "ContentLoaded", "value": 1 },
11+
{ "name": "Built", "value": 2 },
12+
{ "name": "Previewing", "value": 3 },
13+
{ "name": "ReadyToDeploy", "value": 4 },
14+
{ "name": "Deployed", "value": 5 },
15+
{ "name": "SsgError", "value": 6 }
16+
]
17+
},
18+
{
19+
"name": "SsgEngine",
20+
"variants": [
21+
{ "name": "Hugo", "value": 1 },
22+
{ "name": "Zola", "value": 2 },
23+
{ "name": "Astro", "value": 3 },
24+
{ "name": "Casket", "value": 4 },
25+
{ "name": "Custom", "value": 99 }
26+
]
27+
}
28+
],
29+
"transition_table": {
30+
"state_enum": "SsgState",
31+
"rows": [
32+
{ "from": "Empty", "to": "ContentLoaded", "allowed": true },
33+
{ "from": "ContentLoaded", "to": "Built", "allowed": true },
34+
{ "from": "Built", "to": "Built", "allowed": true },
35+
{ "from": "Built", "to": "Previewing", "allowed": true },
36+
{ "from": "Previewing", "to": "ReadyToDeploy", "allowed": true },
37+
{ "from": "ReadyToDeploy", "to": "Deployed", "allowed": true },
38+
{ "from": "Deployed", "to": "Empty", "allowed": true },
39+
{ "from": "ReadyToDeploy", "to": "Empty", "allowed": true },
40+
{ "from": "ContentLoaded", "to": "SsgError", "allowed": true },
41+
{ "from": "ReadyToDeploy", "to": "SsgError", "allowed": true },
42+
{ "from": "SsgError", "to": "Empty", "allowed": true },
43+
{ "from": "ContentLoaded", "to": "Previewing", "allowed": false },
44+
{ "from": "Built", "to": "Deployed", "allowed": false }
45+
]
46+
}
47+
}

src/abi/manifest_schema.rs

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
//
4+
// ABI manifest schema — the Idris2-derived, language-neutral
5+
// description of a cartridge's ABI surface. The verifier (verify.rs)
6+
// diffs this against a parsed Zig FFI file to detect drift.
7+
//
8+
// Phase 1 of standards#89 sub-issue 3 / standards#92.
9+
// Phase 1b will emit this from the Idris2 build instead of hand-authoring.
10+
11+
use serde::{Deserialize, Serialize};
12+
13+
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
14+
pub struct AbiManifest {
15+
pub schema_version: String,
16+
pub cartridge: String,
17+
pub source_idris: String,
18+
pub enums: Vec<EnumDecl>,
19+
#[serde(default)]
20+
pub transition_table: Option<TransitionTable>,
21+
}
22+
23+
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
24+
pub struct EnumDecl {
25+
pub name: String,
26+
pub variants: Vec<EnumVariant>,
27+
}
28+
29+
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
30+
pub struct EnumVariant {
31+
pub name: String,
32+
pub value: i64,
33+
}
34+
35+
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
36+
pub struct TransitionTable {
37+
pub state_enum: String,
38+
pub rows: Vec<TransitionRow>,
39+
}
40+
41+
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
42+
pub struct TransitionRow {
43+
pub from: String,
44+
pub to: String,
45+
pub allowed: bool,
46+
}
47+
48+
/// CamelCase → snake_case using the Zig convention used by hyperpolymath
49+
/// cartridges: underscore is inserted before every uppercase letter whose
50+
/// previous character is a lowercase letter or digit, then the whole string
51+
/// is lowercased. Examples (hand-verified against both real cartridges):
52+
/// `ManifestLoaded` → `manifest_loaded`
53+
/// `K9Error` → `k9_error`
54+
/// `SsgError` → `ssg_error`
55+
/// `ReadyToDeploy` → `ready_to_deploy`
56+
pub fn to_snake_case(s: &str) -> String {
57+
let chars: Vec<char> = s.chars().collect();
58+
let mut out = String::with_capacity(s.len() + 4);
59+
for (i, c) in chars.iter().enumerate() {
60+
if i > 0 && c.is_ascii_uppercase() {
61+
let prev = chars[i - 1];
62+
if prev.is_ascii_lowercase() || prev.is_ascii_digit() {
63+
out.push('_');
64+
}
65+
}
66+
out.push(c.to_ascii_lowercase());
67+
}
68+
out
69+
}
70+
71+
#[cfg(test)]
72+
mod tests {
73+
use super::*;
74+
75+
#[test]
76+
fn snake_case_matches_cartridge_conventions() {
77+
assert_eq!(to_snake_case("Empty"), "empty");
78+
assert_eq!(to_snake_case("ManifestLoaded"), "manifest_loaded");
79+
assert_eq!(to_snake_case("ContentLoaded"), "content_loaded");
80+
assert_eq!(to_snake_case("K9Error"), "k9_error");
81+
assert_eq!(to_snake_case("SsgError"), "ssg_error");
82+
assert_eq!(to_snake_case("ReadyToDeploy"), "ready_to_deploy");
83+
assert_eq!(to_snake_case("Hugo"), "hugo");
84+
}
85+
}

src/abi/mod.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,10 @@ use serde::{Deserialize, Serialize};
1010
use std::fmt;
1111
use std::path::PathBuf;
1212

13+
pub mod manifest_schema;
14+
pub mod verify;
15+
pub mod zig_ffi_parser;
16+
1317
// ---------------------------------------------------------------------------
1418
// Paradigm
1519
// ---------------------------------------------------------------------------

0 commit comments

Comments
 (0)