Skip to content

Commit 4cf2cc2

Browse files
committed
fix(abi)!: unify result-code contract across Zig and Idris2 (18 codes, machine-checked)
The two sides of the 'contractual' result-code mapping had silently diverged: Zig GsaResult codes 5-12 (not_initialized/timeout/...) encoded different concepts than Types.idr Result codes 5-12 (AlreadyConsumed/ ResourceLeaked/...). Nothing cross-checked them, so 124 green tests shipped a broken cross-language contract. - Types.idr keeps its stable 0-12 encoding and gains the five Zig-side failure modes as codes 13-17 (NotInitialized, ProtocolError, IoError, PermissionDenied, NotFound); all total functions extended. - GsaResult now mirrors Result name-for-name and value-for-value, including the linear-resource codes (already_consumed/resource_leaked/ double_free) the multi-handle model needs. - New scripts/gen_result_codes.zig parses Types.idr's resultToInt clauses into result_codes_expected.zig (same pattern as gen_abi_expected.zig); a comptime block next to GsaResult turns any name/value/cardinality drift into a compile error (verified by injecting a deliberate mismatch). - Call sites retargeted: parse_error -> config_parse_error, VeriSimDB failures -> verisimdb_unavailable. - The old 'values match Idris2 ABI' test asserted Zig literals against the Zig enum; renamed to a sanity check, with the generated table as the real contract. BREAKING CHANGE: integer values of result codes 5-12 changed; consumers holding numeric codes must rebuild against the new table. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TaWWedv6VQqeZaPvc94keN
1 parent 85c6621 commit 4cf2cc2

8 files changed

Lines changed: 279 additions & 45 deletions

File tree

scripts/gen_result_codes.zig

Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,113 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
//
4+
// gen_result_codes.zig — extract the canonical result-code contract from the
5+
// Idris2 model (src/interface/abi/Types.idr) and emit the Zig source file
6+
// (src/interface/ffi/src/result_codes_expected.zig) consumed by the comptime
7+
// cross-check next to GsaResult in main.zig.
8+
//
9+
// Types.idr is the single source of truth: its `resultToInt` clauses define
10+
// the stable (constructor, code) pairs. This tool lifts them into Zig so the
11+
// compiler can assert GsaResult agrees name-for-name and value-for-value —
12+
// the drift this closes shipped once already (codes 5-12 diverged silently).
13+
//
14+
// Run from the repository root:
15+
// zig run scripts/gen_result_codes.zig
16+
// CI re-runs this and `git diff --exit-code`s the result (abi-contract job).
17+
18+
const std = @import("std");
19+
20+
const TYPES_IDR = "src/interface/abi/Types.idr";
21+
const OUT_ZIG = "src/interface/ffi/src/result_codes_expected.zig";
22+
23+
// Constructors whose Zig field name is not the mechanical CamelCase ->
24+
// snake_case conversion. A constructor missing from both this table and the
25+
// mechanical rule fails the build of the *generator*, forcing a conscious
26+
// mapping decision for every new code.
27+
const Override = struct { idris: []const u8, zig: []const u8 };
28+
const overrides = [_]Override{
29+
.{ .idris = "Error", .zig = "err" },
30+
.{ .idris = "VeriSimDBUnavailable", .zig = "verisimdb_unavailable" },
31+
};
32+
33+
const HEADER =
34+
\\// SPDX-License-Identifier: MPL-2.0
35+
\\// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
36+
\\//
37+
\\// @generated by scripts/gen_result_codes.zig from src/interface/abi/Types.idr
38+
\\// DO NOT EDIT. Regenerate with: zig run scripts/gen_result_codes.zig
39+
\\//
40+
\\// Canonical result-code contract lifted from the Idris2 model
41+
\\// (GSA.ABI.Types.resultToInt). Consumed by the comptime block next to
42+
\\// GsaResult in main.zig to assert the two enums agree.
43+
\\
44+
\\pub const ResultCode = struct {
45+
\\ idris_ctor: []const u8,
46+
\\ zig_field: []const u8,
47+
\\ code: c_int,
48+
\\};
49+
\\
50+
\\pub const all = [_]ResultCode{
51+
\\
52+
;
53+
54+
fn zigFieldFor(alloc: std.mem.Allocator, ctor: []const u8) ![]const u8 {
55+
for (overrides) |o| {
56+
if (std.mem.eql(u8, o.idris, ctor)) return try alloc.dupe(u8, o.zig);
57+
}
58+
// Mechanical CamelCase -> snake_case (no consecutive-capital handling:
59+
// constructors needing that must go in `overrides`).
60+
var out = std.array_list.Managed(u8).init(alloc);
61+
errdefer out.deinit();
62+
for (ctor, 0..) |c, i| {
63+
if (std.ascii.isUpper(c)) {
64+
if (i != 0) try out.append('_');
65+
try out.append(std.ascii.toLower(c));
66+
} else {
67+
try out.append(c);
68+
}
69+
}
70+
return out.toOwnedSlice();
71+
}
72+
73+
pub fn main() !void {
74+
var gpa = std.heap.GeneralPurposeAllocator(.{}){};
75+
defer _ = gpa.deinit();
76+
const alloc = gpa.allocator();
77+
78+
const src = try std.fs.cwd().readFileAlloc(alloc, TYPES_IDR, 4 * 1024 * 1024);
79+
defer alloc.free(src);
80+
81+
var out = std.array_list.Managed(u8).init(alloc);
82+
defer out.deinit();
83+
try out.appendSlice(HEADER);
84+
85+
var count: usize = 0;
86+
var lines = std.mem.splitScalar(u8, src, '\n');
87+
while (lines.next()) |line| {
88+
const trimmed = std.mem.trim(u8, line, " \r\t");
89+
if (!std.mem.startsWith(u8, trimmed, "resultToInt ")) continue;
90+
if (std.mem.indexOfScalar(u8, trimmed, ':') != null) continue; // type signature
91+
92+
var it = std.mem.tokenizeAny(u8, trimmed, " \t");
93+
_ = it.next(); // "resultToInt"
94+
const ctor = it.next() orelse return error.BadClause;
95+
const eq = it.next() orelse return error.BadClause;
96+
if (!std.mem.eql(u8, eq, "=")) return error.BadClause;
97+
const code = try std.fmt.parseInt(c_int, it.next() orelse return error.BadClause, 10);
98+
99+
const field = try zigFieldFor(alloc, ctor);
100+
defer alloc.free(field);
101+
try out.writer().print(
102+
" .{{ .idris_ctor = \"{s}\", .zig_field = \"{s}\", .code = {d} }},\n",
103+
.{ ctor, field, code },
104+
);
105+
count += 1;
106+
}
107+
try out.appendSlice("};\n");
108+
109+
if (count == 0) return error.NoClausesFound;
110+
111+
try std.fs.cwd().writeFile(.{ .sub_path = OUT_ZIG, .data = out.items });
112+
std.debug.print("wrote {s} ({d} result codes)\n", .{ OUT_ZIG, count });
113+
}

src/interface/abi/Types.idr

Lines changed: 45 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -34,9 +34,14 @@ import Data.Vect
3434
--------------------------------------------------------------------------------
3535

3636
||| Result codes for all FFI operations.
37-
||| Maps to C int32 values 0-12. Each variant has a fixed integer encoding
37+
||| Maps to C int32 values 0-17. Each variant has a fixed integer encoding
3838
||| used across the ABI boundary. Results are classified as terminal (no retry)
3939
||| or transient (retry may succeed).
40+
|||
41+
||| This is the single source of truth for the cross-language contract:
42+
||| scripts/gen_result_codes.zig parses the `resultToInt` clauses below and the
43+
||| Zig build asserts (at comptime) that GsaResult matches name-for-name and
44+
||| value-for-value. Regenerate after any change here.
4045
public export
4146
data Result : Type where
4247
||| Operation completed successfully (code 0)
@@ -65,6 +70,16 @@ data Result : Type where
6570
ConfigParseError : Result
6671
||| VeriSimDB instance is unreachable or not running (code 12)
6772
VeriSimDBUnavailable : Result
73+
||| The library was used before gossamer_gsa_init succeeded (code 13)
74+
NotInitialized : Result
75+
||| A wire protocol violation was detected while probing (code 14)
76+
ProtocolError : Result
77+
||| An OS-level I/O operation failed (code 15)
78+
IoError : Result
79+
||| The operation was denied by a permission check (code 16)
80+
PermissionDenied : Result
81+
||| A requested entity (profile, server, file) does not exist (code 17)
82+
NotFound : Result
6883

6984
||| Convert a Result to its C-compatible integer representation.
7085
||| These values are stable across ABI versions and must not change.
@@ -83,6 +98,11 @@ resultToInt ConnectionRefused = 9
8398
resultToInt AuthFailed = 10
8499
resultToInt ConfigParseError = 11
85100
resultToInt VeriSimDBUnavailable = 12
101+
resultToInt NotInitialized = 13
102+
resultToInt ProtocolError = 14
103+
resultToInt IoError = 15
104+
resultToInt PermissionDenied = 16
105+
resultToInt NotFound = 17
86106

87107
||| Parse a C integer back into a Result.
88108
||| Returns Nothing for unrecognised codes, providing forward compatibility
@@ -102,6 +122,11 @@ resultFromInt 9 = Just ConnectionRefused
102122
resultFromInt 10 = Just AuthFailed
103123
resultFromInt 11 = Just ConfigParseError
104124
resultFromInt 12 = Just VeriSimDBUnavailable
125+
resultFromInt 13 = Just NotInitialized
126+
resultFromInt 14 = Just ProtocolError
127+
resultFromInt 15 = Just IoError
128+
resultFromInt 16 = Just PermissionDenied
129+
resultFromInt 17 = Just NotFound
105130
resultFromInt _ = Nothing
106131

107132
||| Classify whether a Result is terminal (will never succeed on retry)
@@ -110,9 +135,11 @@ resultFromInt _ = Nothing
110135
||| may be retried with backoff.
111136
|||
112137
||| Terminal: InvalidParam, NullPointer, AlreadyConsumed, ResourceLeaked,
113-
||| DoubleFree, ConfigParseError (these indicate bugs, not transient failures)
138+
||| DoubleFree, ConfigParseError, NotInitialized, ProtocolError,
139+
||| PermissionDenied, NotFound (these indicate bugs or fixed
140+
||| preconditions, not transient failures)
114141
||| Transient: ProbeTimeout, ConnectionRefused, AuthFailed, VeriSimDBUnavailable,
115-
||| OutOfMemory, Error (these may resolve with retry)
142+
||| OutOfMemory, IoError, Error (these may resolve with retry)
116143
||| Ok is neither — it indicates success.
117144
public export
118145
resultIsTerminal : Result -> Bool
@@ -129,6 +156,11 @@ resultIsTerminal ConnectionRefused = False
129156
resultIsTerminal AuthFailed = False
130157
resultIsTerminal ConfigParseError = True
131158
resultIsTerminal VeriSimDBUnavailable = False
159+
resultIsTerminal NotInitialized = True
160+
resultIsTerminal ProtocolError = True
161+
resultIsTerminal IoError = False
162+
resultIsTerminal PermissionDenied = True
163+
resultIsTerminal NotFound = True
132164

133165
||| Human-readable description of each result code.
134166
||| Used for logging and error reporting.
@@ -147,6 +179,11 @@ resultDescription ConnectionRefused = "Connection refused"
147179
resultDescription AuthFailed = "Authentication failed"
148180
resultDescription ConfigParseError = "Configuration parse error"
149181
resultDescription VeriSimDBUnavailable = "VeriSimDB instance unavailable"
182+
resultDescription NotInitialized = "Library not initialised"
183+
resultDescription ProtocolError = "Wire protocol violation"
184+
resultDescription IoError = "I/O operation failed"
185+
resultDescription PermissionDenied = "Permission denied"
186+
resultDescription NotFound = "Requested entity not found"
150187

151188
||| Decidable equality for Result, enabling pattern matching and proof
152189
||| construction over result codes at the type level.
@@ -165,6 +202,11 @@ Eq Result where
165202
AuthFailed == AuthFailed = True
166203
ConfigParseError == ConfigParseError = True
167204
VeriSimDBUnavailable == VeriSimDBUnavailable = True
205+
NotInitialized == NotInitialized = True
206+
ProtocolError == ProtocolError = True
207+
IoError == IoError = True
208+
PermissionDenied == PermissionDenied = True
209+
NotFound == NotFound = True
168210
_ == _ = False
169211

170212
||| Show instance for logging and debugging

src/interface/ffi/src/game_profiles.zig

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -544,7 +544,7 @@ pub export fn gossamer_gsa_add_profile(
544544
const a2ml_str = std.mem.span(a2ml);
545545
var profile = parseA2MLProfile(a2ml_str, std.heap.c_allocator) catch |err| {
546546
main.setError("profile parse failed: {s}", .{@errorName(err)});
547-
return @intFromEnum(main.GsaResult.parse_error);
547+
return @intFromEnum(main.GsaResult.config_parse_error);
548548
};
549549
errdefer profile.deinit();
550550

src/interface/ffi/src/main.zig

Lines changed: 57 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -81,22 +81,64 @@ pub const BUILD_INFO: [:0]const u8 = "libgsa 0.1.0 (Zig " ++ @import("builtin").
8181

8282
/// FFI result codes. The integer values are contractual; the Idris2 ABI layer
8383
/// converts between these and the dependent-type Result via `resultToInt`.
84+
///
85+
/// Codes 0-12 mirror the original (stable) Idris constructors; 13-17 are the
86+
/// Zig-side failure modes added to `Types.idr` in the same change. The
87+
/// mapping is machine-checked: `scripts/gen_result_codes.zig` parses
88+
/// `Types.idr` into `result_codes_expected.zig`, and the comptime block below
89+
/// the enum turns any name/value/cardinality drift into a compile error.
8490
pub const GsaResult = enum(c_int) {
8591
ok = 0,
8692
err = 1,
8793
invalid_param = 2,
8894
out_of_memory = 3,
8995
null_pointer = 4,
90-
not_initialized = 5,
91-
timeout = 6,
92-
connection_refused = 7,
93-
protocol_error = 8,
94-
parse_error = 9,
95-
io_error = 10,
96-
permission_denied = 11,
97-
not_found = 12,
96+
/// A linear resource was used after consumption.
97+
already_consumed = 5,
98+
/// A linear resource went out of scope without being consumed.
99+
resource_leaked = 6,
100+
/// A handle was closed more than once.
101+
double_free = 7,
102+
probe_timeout = 8,
103+
connection_refused = 9,
104+
auth_failed = 10,
105+
config_parse_error = 11,
106+
/// VeriSimDB instance is unreachable or not running.
107+
verisimdb_unavailable = 12,
108+
not_initialized = 13,
109+
protocol_error = 14,
110+
io_error = 15,
111+
permission_denied = 16,
112+
not_found = 17,
98113
};
99114

115+
// Cross-language contract check: every (constructor, code) pair extracted from
116+
// Types.idr must exist here with the same value, and the counts must match.
117+
// See scripts/gen_result_codes.zig (regenerate after editing Types.idr).
118+
const result_codes_expected = @import("result_codes_expected.zig");
119+
comptime {
120+
const fields = @typeInfo(GsaResult).@"enum".fields;
121+
if (fields.len != result_codes_expected.all.len) {
122+
@compileError(std.fmt.comptimePrint(
123+
"GsaResult has {d} variants but Types.idr declares {d} — regenerate result_codes_expected.zig and reconcile",
124+
.{ fields.len, result_codes_expected.all.len },
125+
));
126+
}
127+
for (result_codes_expected.all) |entry| {
128+
if (!@hasField(GsaResult, entry.zig_field)) {
129+
@compileError("GsaResult is missing variant '" ++ entry.zig_field ++
130+
"' declared in Types.idr as '" ++ entry.idris_ctor ++ "'");
131+
}
132+
const actual = @intFromEnum(@field(GsaResult, entry.zig_field));
133+
if (actual != entry.code) {
134+
@compileError(std.fmt.comptimePrint(
135+
"GsaResult.{s} = {d} but Types.idr declares {s} = {d}",
136+
.{ entry.zig_field, actual, entry.idris_ctor, entry.code },
137+
));
138+
}
139+
}
140+
}
141+
100142
// ═══════════════════════════════════════════════════════════════════════════════
101143
// Thread-local error buffer
102144
// ═══════════════════════════════════════════════════════════════════════════════
@@ -249,7 +291,7 @@ pub fn getGlobalHandle() ?*GsaHandle {
249291
/// `profiles_dir` — filesystem path to directory containing .a2ml game
250292
/// profiles.
251293
///
252-
/// Returns 0 on success, negative GsaResult on failure.
294+
/// Returns 0 on success, a positive GsaResult code on failure.
253295
pub export fn gossamer_gsa_init(
254296
verisimdb_url: [*:0]const u8,
255297
profiles_dir: [*:0]const u8,
@@ -278,7 +320,7 @@ pub export fn gossamer_gsa_init(
278320

279321
/// Shut down the library and release all resources.
280322
///
281-
/// Returns 0 on success, negative GsaResult on failure.
323+
/// Returns 0 on success, a positive GsaResult code on failure.
282324
pub export fn gossamer_gsa_shutdown() callconv(.c) c_int {
283325
global_mutex.lock();
284326
defer global_mutex.unlock();
@@ -311,20 +353,13 @@ pub export fn gossamer_gsa_version() callconv(.c) [*:0]const u8 {
311353
// Unit tests
312354
// ═══════════════════════════════════════════════════════════════════════════════
313355

314-
test "GsaResult values match Idris2 ABI" {
356+
test "GsaResult sanity (cross-language check is the comptime block above)" {
357+
// The authoritative Idris2 cross-check is the comptime block after the
358+
// enum definition, driven by result_codes_expected.zig. This test only
359+
// pins the two values other modules rely on unconditionally.
315360
try std.testing.expectEqual(@as(c_int, 0), @intFromEnum(GsaResult.ok));
316361
try std.testing.expectEqual(@as(c_int, 1), @intFromEnum(GsaResult.err));
317-
try std.testing.expectEqual(@as(c_int, 2), @intFromEnum(GsaResult.invalid_param));
318-
try std.testing.expectEqual(@as(c_int, 3), @intFromEnum(GsaResult.out_of_memory));
319-
try std.testing.expectEqual(@as(c_int, 4), @intFromEnum(GsaResult.null_pointer));
320-
try std.testing.expectEqual(@as(c_int, 5), @intFromEnum(GsaResult.not_initialized));
321-
try std.testing.expectEqual(@as(c_int, 6), @intFromEnum(GsaResult.timeout));
322-
try std.testing.expectEqual(@as(c_int, 7), @intFromEnum(GsaResult.connection_refused));
323-
try std.testing.expectEqual(@as(c_int, 8), @intFromEnum(GsaResult.protocol_error));
324-
try std.testing.expectEqual(@as(c_int, 9), @intFromEnum(GsaResult.parse_error));
325-
try std.testing.expectEqual(@as(c_int, 10), @intFromEnum(GsaResult.io_error));
326-
try std.testing.expectEqual(@as(c_int, 11), @intFromEnum(GsaResult.permission_denied));
327-
try std.testing.expectEqual(@as(c_int, 12), @intFromEnum(GsaResult.not_found));
362+
try std.testing.expectEqual(@as(usize, 18), @typeInfo(GsaResult).@"enum".fields.len);
328363
}
329364

330365
test "error buffer round-trip" {
Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
//
4+
// @generated by scripts/gen_result_codes.zig from src/interface/abi/Types.idr
5+
// DO NOT EDIT. Regenerate with: zig run scripts/gen_result_codes.zig
6+
//
7+
// Canonical result-code contract lifted from the Idris2 model
8+
// (GSA.ABI.Types.resultToInt). Consumed by the comptime block next to
9+
// GsaResult in main.zig to assert the two enums agree.
10+
11+
pub const ResultCode = struct {
12+
idris_ctor: []const u8,
13+
zig_field: []const u8,
14+
code: c_int,
15+
};
16+
17+
pub const all = [_]ResultCode{
18+
.{ .idris_ctor = "Ok", .zig_field = "ok", .code = 0 },
19+
.{ .idris_ctor = "Error", .zig_field = "err", .code = 1 },
20+
.{ .idris_ctor = "InvalidParam", .zig_field = "invalid_param", .code = 2 },
21+
.{ .idris_ctor = "OutOfMemory", .zig_field = "out_of_memory", .code = 3 },
22+
.{ .idris_ctor = "NullPointer", .zig_field = "null_pointer", .code = 4 },
23+
.{ .idris_ctor = "AlreadyConsumed", .zig_field = "already_consumed", .code = 5 },
24+
.{ .idris_ctor = "ResourceLeaked", .zig_field = "resource_leaked", .code = 6 },
25+
.{ .idris_ctor = "DoubleFree", .zig_field = "double_free", .code = 7 },
26+
.{ .idris_ctor = "ProbeTimeout", .zig_field = "probe_timeout", .code = 8 },
27+
.{ .idris_ctor = "ConnectionRefused", .zig_field = "connection_refused", .code = 9 },
28+
.{ .idris_ctor = "AuthFailed", .zig_field = "auth_failed", .code = 10 },
29+
.{ .idris_ctor = "ConfigParseError", .zig_field = "config_parse_error", .code = 11 },
30+
.{ .idris_ctor = "VeriSimDBUnavailable", .zig_field = "verisimdb_unavailable", .code = 12 },
31+
.{ .idris_ctor = "NotInitialized", .zig_field = "not_initialized", .code = 13 },
32+
.{ .idris_ctor = "ProtocolError", .zig_field = "protocol_error", .code = 14 },
33+
.{ .idris_ctor = "IoError", .zig_field = "io_error", .code = 15 },
34+
.{ .idris_ctor = "PermissionDenied", .zig_field = "permission_denied", .code = 16 },
35+
.{ .idris_ctor = "NotFound", .zig_field = "not_found", .code = 17 },
36+
};

0 commit comments

Comments
 (0)