Skip to content

Commit a644b03

Browse files
fix(abi-verify): tolerate non-canonical Zig switch arm false shorthand (#22)
`abi-verify`'s Zig FFI parser bombed on 5 cartridges' `isValidTransition` switch arms because their terminal-state arm body is the literal `false` (no outgoing transitions allowed) rather than the canonical `to == .<v>` chunk form: fn isValidTransition(from: BspState, to: BspState) bool { return switch (from) { ... .exited => false, // <-- parser bombed here }; } The Zig is well-formed and the semantics ("empty allowed-set") are clear; the verifier just didn't accept the shorthand. `parse_arm_targets` now detects this form (body trimmed of trailing `,`/`;` and whitespace equals `false`) and returns the empty vec — equivalent to the "this state has no allowed outgoing transitions" manifest semantics, which is exactly what the cartridges intend. End-to-end verified against the 5 cartridges named in the issue (after a fresh `cargo build --release`): bsp-mcp → parses cleanly; surfaces real drift on BspCapability container-mcp → abi-verify OK dap-mcp → parses cleanly; surfaces real drift on StepGranularity lsp-mcp → parses cleanly; surfaces real drift on CompletionKind vault-mcp → parses cleanly; surfaces real drift on IdentityType All 5 now produce either exit 0 (clean) or a real drift diagnosis, which is precisely the acceptance criterion in iseriser#19. The post-parse drift findings are separate per-cartridge issues — not verifier defects — and out of scope for this PR. 44 lib tests + 9 integration tests pass. Refs hyperpolymath/standards#92 (Phase 2 allowlist expansion). Refs #19. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 17c7ca7 commit a644b03

1 file changed

Lines changed: 56 additions & 0 deletions

File tree

src/abi/zig_ffi_parser.rs

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -246,7 +246,21 @@ fn parse_switch_arms(body: &str) -> Result<BTreeMap<String, Vec<String>>> {
246246

247247
/// Parse `to == .<v1> or to == .<v2> or to == .<v3>` → `["v1","v2","v3"]`.
248248
/// Also accepts the singleton form `to == .<v>`.
249+
///
250+
/// Terminal-state shorthand: a body of `false` (with optional trailing
251+
/// `,` / `;` and surrounding whitespace) is accepted as the empty
252+
/// allowed-set — i.e. "no outgoing transitions allowed from this
253+
/// state". Cartridges like bsp-mcp, container-mcp, dap-mcp, lsp-mcp,
254+
/// vault-mcp use this form for their `exited` / terminal arms.
249255
fn parse_arm_targets(body: &str) -> Result<Vec<String>> {
256+
let trimmed = body
257+
.trim()
258+
.trim_end_matches(',')
259+
.trim_end_matches(';')
260+
.trim();
261+
if trimmed == "false" {
262+
return Ok(Vec::new());
263+
}
250264
let mut out = Vec::new();
251265
for chunk in body.split(" or ") {
252266
let chunk = chunk.trim();
@@ -338,4 +352,46 @@ mod tests {
338352
let tt = f.transition_table.unwrap();
339353
assert!(tt.arms.contains_key("_else"));
340354
}
355+
356+
#[test]
357+
fn tolerates_terminal_false_arm() {
358+
// bsp-mcp / container-mcp / dap-mcp / lsp-mcp / vault-mcp shape:
359+
// the terminal state's arm body is the literal `false` (meaning
360+
// no outgoing transitions allowed), not a `to == .<v>` chunk.
361+
// Without this tolerance the verifier mis-classifies the cartridge
362+
// as a parser error rather than the correct "empty allowed-set"
363+
// semantics.
364+
let src = r#"
365+
pub const BspState = enum(c_int) {
366+
uninitialized = 0,
367+
initializing = 1,
368+
ready = 2,
369+
exited = 3,
370+
};
371+
fn isValidTransition(from: BspState, to: BspState) bool {
372+
return switch (from) {
373+
.uninitialized => to == .initializing,
374+
.initializing => to == .ready or to == .exited,
375+
.ready => to == .exited,
376+
.exited => false,
377+
};
378+
}
379+
"#;
380+
let f = parse(src).unwrap();
381+
let tt = f.transition_table.unwrap();
382+
// The terminal arm parses and lands in the arms map with an
383+
// empty allowed-set; it MUST be present (otherwise the verifier
384+
// would surface accept-by-omission as drift) but it MUST be
385+
// empty (no targets).
386+
assert_eq!(tt.arms.get("exited"), Some(&Vec::<String>::new()));
387+
// The other arms still parse correctly.
388+
assert_eq!(
389+
tt.arms.get("uninitialized"),
390+
Some(&vec!["initializing".to_string()])
391+
);
392+
assert_eq!(
393+
tt.arms.get("initializing"),
394+
Some(&vec!["ready".to_string(), "exited".to_string()])
395+
);
396+
}
341397
}

0 commit comments

Comments
 (0)