Skip to content

Commit 5d2ac53

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat: add ABI/FFI for 4 incomplete cartridges
- burble-admin-mcp: Idris2 permission proofs, Zig FFI with tests - idaptik-admin-mcp: game admin ops, level designer permissions - game-admin-mcp: server lifecycle, read-only proofs - model-router-mcp: LLM tier routing, fallback chain proof All match the echidna-llm-mcp reference pattern: abi/ → Idris2 Protocol.idr with dependent type proofs ffi/ → Zig C-compatible bridge with build.zig and tests Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 8e1a519 commit 5d2ac53

16 files changed

Lines changed: 665 additions & 0 deletions

File tree

‎cartridges/burble-admin-mcp/abi/BurbleAdmin/Protocol.idr‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
||| Protocol: Burble voice platform administration via BoJ MCP
4+
|||
5+
||| Cartridge: burble-admin
6+
||| Matrix cell: Voice Platform x Administration
7+
|||
8+
||| Defines the formal interface for managing Burble rooms, users,
9+
||| and voice sessions through the BoJ Server. Proves that:
10+
||| 1. Admin operations require authentication
11+
||| 2. Room capacity is bounded
12+
||| 3. Recording access is permission-gated
13+
module BurbleAdmin.Protocol
14+
15+
import Data.Fin
16+
17+
%default total
18+
19+
-- ═══════════════════════════════════════════════════════════════════════
20+
-- Core Types
21+
-- ═══════════════════════════════════════════════════════════════════════
22+
23+
||| Administrative operation on a Burble instance
24+
public export
25+
data Operation
26+
= ListRooms -- List active voice rooms
27+
| CreateRoom -- Create a new room
28+
| DeleteRoom -- Delete an existing room
29+
| ListUsers -- List connected users
30+
| KickUser -- Remove a user from a room
31+
| GetMetrics -- Get platform metrics
32+
| ManageRecordings -- Access recording management
33+
34+
||| Permission level required for operations
35+
public export
36+
data PermLevel = ReadOnly | Moderator | Admin
37+
38+
||| Proof that an operation requires at least the given permission
39+
public export
40+
data RequiresPermission : Operation -> PermLevel -> Type where
41+
ListRoomsRead : RequiresPermission ListRooms ReadOnly
42+
CreateRoomMod : RequiresPermission CreateRoom Moderator
43+
DeleteRoomAdmin : RequiresPermission DeleteRoom Admin
44+
ListUsersRead : RequiresPermission ListUsers ReadOnly
45+
KickUserMod : RequiresPermission KickUser Moderator
46+
GetMetricsRead : RequiresPermission GetMetrics ReadOnly
47+
RecordingsAdmin : RequiresPermission ManageRecordings Admin
48+
49+
||| Room capacity is bounded (1-500 participants)
50+
public export
51+
data RoomCapacity = MkCapacity (n : Fin 500)
52+
53+
-- ═══════════════════════════════════════════════════════════════════════
54+
-- C ABI Exports
55+
-- ═══════════════════════════════════════════════════════════════════════
56+
57+
export
58+
operationToInt : Operation -> Int
59+
operationToInt ListRooms = 0
60+
operationToInt CreateRoom = 1
61+
operationToInt DeleteRoom = 2
62+
operationToInt ListUsers = 3
63+
operationToInt KickUser = 4
64+
operationToInt GetMetrics = 5
65+
operationToInt ManageRecordings = 6
66+
67+
export
68+
permLevelToInt : PermLevel -> Int
69+
permLevelToInt ReadOnly = 0
70+
permLevelToInt Moderator = 1
71+
permLevelToInt Admin = 2
72+
73+
||| Minimum permission level for an operation (C ABI)
74+
export
75+
burble_min_perm : Int -> Int
76+
burble_min_perm 0 = 0 -- ListRooms → ReadOnly
77+
burble_min_perm 1 = 1 -- CreateRoom → Moderator
78+
burble_min_perm 2 = 2 -- DeleteRoom → Admin
79+
burble_min_perm 3 = 0 -- ListUsers → ReadOnly
80+
burble_min_perm 4 = 1 -- KickUser → Moderator
81+
burble_min_perm 5 = 0 -- GetMetrics → ReadOnly
82+
burble_min_perm 6 = 2 -- ManageRecordings → Admin
83+
burble_min_perm _ = 2 -- Unknown → require Admin (safe default)

‎cartridges/burble-admin-mcp/abi/burble-admin.ipkg‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
package burbleAdmin
3+
4+
modules = BurbleAdmin.Protocol
5+
6+
sourcedir = "."

‎cartridges/burble-admin-mcp/ffi/build.zig‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
const std = @import("std");
3+
4+
pub fn build(b: *std.Build) void {
5+
const target = b.standardTargetOptions(.{});
6+
const optimize = b.standardOptimizeOption(.{});
7+
8+
const lib = b.addStaticLibrary(.{
9+
.name = "burble_admin_ffi",
10+
.root_source_file = b.path("burble_admin_ffi.zig"),
11+
.target = target,
12+
.optimize = optimize,
13+
});
14+
b.installArtifact(lib);
15+
16+
const tests = b.addTest(.{
17+
.root_source_file = b.path("burble_admin_ffi.zig"),
18+
.target = target,
19+
.optimize = optimize,
20+
});
21+
const run_tests = b.addRunArtifact(tests);
22+
const test_step = b.step("test", "Run FFI tests");
23+
test_step.dependOn(&run_tests.step);
24+
}

‎cartridges/burble-admin-mcp/ffi/burble_admin_ffi.zig‎

Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
//
4+
// Burble Admin FFI — C-compatible bridge for BoJ MCP cartridge.
5+
// Implements the operations defined in BurbleAdmin.Protocol (Idris2 ABI).
6+
7+
const std = @import("std");
8+
9+
// ═══════════════════════════════════════════════════════════════════════
10+
// Types (mirrors Idris2 ABI)
11+
// ═══════════════════════════════════════════════════════════════════════
12+
13+
pub const Operation = enum(i32) {
14+
list_rooms = 0,
15+
create_room = 1,
16+
delete_room = 2,
17+
list_users = 3,
18+
kick_user = 4,
19+
get_metrics = 5,
20+
manage_recordings = 6,
21+
};
22+
23+
pub const PermLevel = enum(i32) {
24+
read_only = 0,
25+
moderator = 1,
26+
admin = 2,
27+
};
28+
29+
// ═══════════════════════════════════════════════════════════════════════
30+
// Permission checking (matches Idris2 proof)
31+
// ═══════════════════════════════════════════════════════════════════════
32+
33+
/// Returns the minimum permission level for an operation.
34+
/// Matches burble_min_perm in Protocol.idr exactly.
35+
pub export fn burble_admin_min_perm(op: i32) callconv(.C) i32 {
36+
return switch (@as(Operation, @enumFromInt(op))) {
37+
.list_rooms => 0,
38+
.create_room => 1,
39+
.delete_room => 2,
40+
.list_users => 0,
41+
.kick_user => 1,
42+
.get_metrics => 0,
43+
.manage_recordings => 2,
44+
};
45+
}
46+
47+
/// Check if a user with the given permission level can perform the operation.
48+
/// Returns 1 if allowed, 0 if denied.
49+
pub export fn burble_admin_check_perm(op: i32, user_perm: i32) callconv(.C) i32 {
50+
const required = burble_admin_min_perm(op);
51+
return if (user_perm >= required) 1 else 0;
52+
}
53+
54+
// ═══════════════════════════════════════════════════════════════════════
55+
// Room capacity validation
56+
// ═══════════════════════════════════════════════════════════════════════
57+
58+
/// Validate room capacity (1-500). Returns clamped value.
59+
pub export fn burble_admin_clamp_capacity(requested: i32) callconv(.C) i32 {
60+
if (requested < 1) return 1;
61+
if (requested > 500) return 500;
62+
return requested;
63+
}
64+
65+
// ═══════════════════════════════════════════════════════════════════════
66+
// Tests
67+
// ═══════════════════════════════════════════════════════════════════════
68+
69+
test "permission levels match ABI" {
70+
// ReadOnly ops
71+
try std.testing.expectEqual(@as(i32, 0), burble_admin_min_perm(0)); // list_rooms
72+
try std.testing.expectEqual(@as(i32, 0), burble_admin_min_perm(3)); // list_users
73+
try std.testing.expectEqual(@as(i32, 0), burble_admin_min_perm(5)); // get_metrics
74+
75+
// Moderator ops
76+
try std.testing.expectEqual(@as(i32, 1), burble_admin_min_perm(1)); // create_room
77+
try std.testing.expectEqual(@as(i32, 1), burble_admin_min_perm(4)); // kick_user
78+
79+
// Admin ops
80+
try std.testing.expectEqual(@as(i32, 2), burble_admin_min_perm(2)); // delete_room
81+
try std.testing.expectEqual(@as(i32, 2), burble_admin_min_perm(6)); // manage_recordings
82+
}
83+
84+
test "permission check" {
85+
// Admin can do everything
86+
try std.testing.expectEqual(@as(i32, 1), burble_admin_check_perm(0, 2));
87+
try std.testing.expectEqual(@as(i32, 1), burble_admin_check_perm(2, 2));
88+
89+
// ReadOnly can't delete
90+
try std.testing.expectEqual(@as(i32, 0), burble_admin_check_perm(2, 0));
91+
}
92+
93+
test "capacity clamping" {
94+
try std.testing.expectEqual(@as(i32, 1), burble_admin_clamp_capacity(0));
95+
try std.testing.expectEqual(@as(i32, 50), burble_admin_clamp_capacity(50));
96+
try std.testing.expectEqual(@as(i32, 500), burble_admin_clamp_capacity(999));
97+
}

‎cartridges/game-admin-mcp/abi/GameAdmin/Protocol.idr‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
||| Protocol: Game Server Administration via BoJ MCP
4+
|||
5+
||| Cartridge: game-admin
6+
||| Matrix cell: Game Servers x Administration
7+
|||
8+
||| Defines the formal interface for managing dedicated game servers
9+
||| (DST, Void Expanse, etc.) through the BoJ Server. Proves that:
10+
||| 1. Server lifecycle operations are admin-only
11+
||| 2. Probe operations are safe (read-only)
12+
||| 3. Config changes require explicit confirmation
13+
module GameAdmin.Protocol
14+
15+
import Data.Fin
16+
17+
%default total
18+
19+
-- ═══════════════════════════════════════════════════════════════════════
20+
-- Core Types
21+
-- ═══════════════════════════════════════════════════════════════════════
22+
23+
||| Administrative operation on a game server
24+
public export
25+
data Operation
26+
= ListServers -- List managed game servers
27+
| GetServerStatus -- Get server health/status
28+
| StartServer -- Start a game server
29+
| StopServer -- Stop a game server
30+
| RestartServer -- Restart a game server
31+
| UpdateConfig -- Modify server configuration
32+
| GetLogs -- Retrieve server logs
33+
| ProbeHealth -- Quick health probe (Groove)
34+
35+
||| Permission level for game admin ops
36+
public export
37+
data PermLevel = Viewer | Operator | Admin
38+
39+
||| Operations that are read-only (safe to call without side effects)
40+
public export
41+
data IsReadOnly : Operation -> Type where
42+
ListReadOnly : IsReadOnly ListServers
43+
StatusReadOnly : IsReadOnly GetServerStatus
44+
LogsReadOnly : IsReadOnly GetLogs
45+
ProbeReadOnly : IsReadOnly ProbeHealth
46+
47+
-- ═══════════════════════════════════════════════════════════════════════
48+
-- C ABI Exports
49+
-- ═══════════════════════════════════════════════════════════════════════
50+
51+
export
52+
operationToInt : Operation -> Int
53+
operationToInt ListServers = 0
54+
operationToInt GetServerStatus = 1
55+
operationToInt StartServer = 2
56+
operationToInt StopServer = 3
57+
operationToInt RestartServer = 4
58+
operationToInt UpdateConfig = 5
59+
operationToInt GetLogs = 6
60+
operationToInt ProbeHealth = 7
61+
62+
export
63+
game_min_perm : Int -> Int
64+
game_min_perm 0 = 0 -- ListServers → Viewer
65+
game_min_perm 1 = 0 -- GetServerStatus → Viewer
66+
game_min_perm 2 = 1 -- StartServer → Operator
67+
game_min_perm 3 = 1 -- StopServer → Operator
68+
game_min_perm 4 = 1 -- RestartServer → Operator
69+
game_min_perm 5 = 2 -- UpdateConfig → Admin
70+
game_min_perm 6 = 0 -- GetLogs → Viewer
71+
game_min_perm 7 = 0 -- ProbeHealth → Viewer
72+
game_min_perm _ = 2 -- Unknown → require Admin
73+
74+
||| Check if operation is read-only (C ABI: 1=yes, 0=no)
75+
export
76+
game_is_readonly : Int -> Int
77+
game_is_readonly 0 = 1 -- ListServers
78+
game_is_readonly 1 = 1 -- GetServerStatus
79+
game_is_readonly 6 = 1 -- GetLogs
80+
game_is_readonly 7 = 1 -- ProbeHealth
81+
game_is_readonly _ = 0 -- All others have side effects

‎cartridges/game-admin-mcp/abi/game-admin.ipkg‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
-- SPDX-License-Identifier: PMPL-1.0-or-later
2+
package gameAdmin
3+
4+
modules = GameAdmin.Protocol
5+
6+
sourcedir = "."

‎cartridges/game-admin-mcp/ffi/build.zig‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
const std = @import("std");
3+
4+
pub fn build(b: *std.Build) void {
5+
const target = b.standardTargetOptions(.{});
6+
const optimize = b.standardOptimizeOption(.{});
7+
8+
const lib = b.addStaticLibrary(.{
9+
.name = "game_admin_ffi",
10+
.root_source_file = b.path("game_admin_ffi.zig"),
11+
.target = target,
12+
.optimize = optimize,
13+
});
14+
b.installArtifact(lib);
15+
16+
const tests = b.addTest(.{
17+
.root_source_file = b.path("game_admin_ffi.zig"),
18+
.target = target,
19+
.optimize = optimize,
20+
});
21+
const run_tests = b.addRunArtifact(tests);
22+
const test_step = b.step("test", "Run FFI tests");
23+
test_step.dependOn(&run_tests.step);
24+
}

‎cartridges/game-admin-mcp/ffi/game_admin_ffi.zig‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
//
4+
// Game Admin FFI — C-compatible bridge for BoJ MCP cartridge.
5+
6+
const std = @import("std");
7+
8+
pub const Operation = enum(i32) {
9+
list_servers = 0,
10+
get_server_status = 1,
11+
start_server = 2,
12+
stop_server = 3,
13+
restart_server = 4,
14+
update_config = 5,
15+
get_logs = 6,
16+
probe_health = 7,
17+
};
18+
19+
pub const PermLevel = enum(i32) {
20+
viewer = 0,
21+
operator_ = 1,
22+
admin = 2,
23+
};
24+
25+
pub export fn game_admin_min_perm(op: i32) callconv(.C) i32 {
26+
return switch (@as(Operation, @enumFromInt(op))) {
27+
.list_servers => 0,
28+
.get_server_status => 0,
29+
.start_server => 1,
30+
.stop_server => 1,
31+
.restart_server => 1,
32+
.update_config => 2,
33+
.get_logs => 0,
34+
.probe_health => 0,
35+
};
36+
}
37+
38+
pub export fn game_admin_check_perm(op: i32, user_perm: i32) callconv(.C) i32 {
39+
const required = game_admin_min_perm(op);
40+
return if (user_perm >= required) 1 else 0;
41+
}
42+
43+
pub export fn game_admin_is_readonly(op: i32) callconv(.C) i32 {
44+
return switch (@as(Operation, @enumFromInt(op))) {
45+
.list_servers, .get_server_status, .get_logs, .probe_health => 1,
46+
else => 0,
47+
};
48+
}
49+
50+
test "permission levels match ABI" {
51+
try std.testing.expectEqual(@as(i32, 0), game_admin_min_perm(0));
52+
try std.testing.expectEqual(@as(i32, 1), game_admin_min_perm(2));
53+
try std.testing.expectEqual(@as(i32, 2), game_admin_min_perm(5));
54+
}
55+
56+
test "readonly operations" {
57+
try std.testing.expectEqual(@as(i32, 1), game_admin_is_readonly(0));
58+
try std.testing.expectEqual(@as(i32, 1), game_admin_is_readonly(1));
59+
try std.testing.expectEqual(@as(i32, 0), game_admin_is_readonly(2));
60+
try std.testing.expectEqual(@as(i32, 0), game_admin_is_readonly(5));
61+
try std.testing.expectEqual(@as(i32, 1), game_admin_is_readonly(7));
62+
}

0 commit comments

Comments
 (0)