Skip to content

Commit b2a2ff7

Browse files
hyperpolymathclaude
andcommitted
feat(l1-prep): scaffold all missing L1 Cap'n Proto artifacts
Five files land as pre-work so L1 can start immediately once the L3 gate opens (T1 green ≥ 7 days), with no design bikeshedding: schemas/VERSIONING.md Versioning policy: safe vs breaking changes, schemaVersion field convention, capnp-gen regeneration requirement, Idris2 ABI update instructions, multi-language consumer table. src/julia/ipc.jl (module EchidnaIPC) Julia IPC stub mirroring Rust src/rust/ipc/mod.rs: connect_ipc() with UDS primary / TCP fallback, gnn_rank_request() throwing until L1 wave 1 lands, ipc_available() probe, Option A/B decision block. src/abi/EchidnaABI/CapnSchemas.idr Idris2 ABI mirror of all 7 Cap'n Proto message types (ProofGoal 6 fields, OutcomeTag 8 variants, NodeKind 7, EdgeKind 8, DangerLevel 4, DispatchStrategy 3). 13 constructive proofs: schemaIdNonZero, 6× bounded (LTE n 256 via %search), 5× injective Fin maps, field-count Refl witnesses, topKDefaultPositive. Zero believe_me, zero postulate. ffi/zig/src/capnp_bridge.zig Zig C-ABI bridge: EchidnaGnnRequest/Response extern structs, echidna_capnp_connect (UDS via std.net), echidna_capnp_close, echidna_capnp_gnn_rank (stub returning -2 until bindings land), echidna_capnp_free_response, echidna_capnp_status_message. Thread-local error storage matches main.zig pattern. Justfile: capnp-gen recipe `capnp compile -orust schemas/echidna.capnp -I /usr/include` with guard for missing capnp binary and commit reminder. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 9baf375 commit b2a2ff7

5 files changed

Lines changed: 883 additions & 0 deletions

File tree

Justfile

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -358,6 +358,14 @@ doc:
358358
update:
359359
cargo update
360360

361+
# Regenerate Cap'n Proto bindings from schemas/echidna.capnp.
362+
# Requires capnp compiler: https://capnproto.org/install.html
363+
# Output: src/rust/ipc/echidna_capnp.rs (checked in; do not edit by hand)
364+
capnp-gen:
365+
@command -v capnp >/dev/null 2>&1 || { echo "capnp compiler not found — install from https://capnproto.org/install.html"; exit 1; }
366+
capnp compile -orust schemas/echidna.capnp -I /usr/include
367+
@echo "Rust bindings generated. Commit src/rust/ipc/echidna_capnp.rs."
368+
361369
# Audit dependencies
362370
audit:
363371
cargo audit

ffi/zig/src/capnp_bridge.zig

Lines changed: 193 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,193 @@
1+
// ECHIDNA Cap'n Proto C-ABI Bridge
2+
//
3+
// C-compatible functions for IPC between the Rust core and the Julia ML
4+
// layer over Unix domain sockets. Actual Cap'n Proto serialisation will
5+
// be generated by `just capnp-gen` in L1 wave 1; until then the
6+
// gnn_rank function is a clearly-labelled stub that returns an error
7+
// code so callers can wire the ABI boundary and test error paths now.
8+
//
9+
// Error reporting follows the same pattern as main.zig:
10+
// - Return value: 0 = success, negative = error
11+
// - Detail: call echidna_capnp_status_message(code, buf, buflen)
12+
// - Thread-local storage makes this safe for concurrent Rust threads.
13+
//
14+
// SPDX-License-Identifier: PMPL-1.0-or-later
15+
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
16+
17+
const std = @import("std");
18+
const builtin = @import("builtin");
19+
20+
const BRIDGE_VERSION = "0.1.0";
21+
22+
// ─── Status codes ─────────────────────────────────────────────────────────────
23+
24+
pub const CapnpStatus = enum(c_int) {
25+
ok = 0,
26+
not_connected = -1,
27+
stub_not_implemented = -2,
28+
invalid_param = -3,
29+
io_error = -4,
30+
connect_failed = -6,
31+
unknown_error = -99,
32+
};
33+
34+
// ─── Thread-local error storage ───────────────────────────────────────────────
35+
36+
threadlocal var last_error_buf: [512]u8 = undefined;
37+
threadlocal var last_error_len: usize = 0;
38+
threadlocal var last_error_status: CapnpStatus = .ok;
39+
40+
fn setError(status: CapnpStatus, comptime fmt: []const u8, args: anytype) void {
41+
last_error_status = status;
42+
const result = std.fmt.bufPrint(&last_error_buf, fmt, args) catch blk: {
43+
const msg = "(error message truncated)";
44+
@memcpy(last_error_buf[0..msg.len], msg);
45+
break :blk last_error_buf[0..msg.len];
46+
};
47+
last_error_len = result.len;
48+
}
49+
50+
fn clearError() void {
51+
last_error_status = .ok;
52+
last_error_len = 0;
53+
}
54+
55+
// ─── C-compatible structs ─────────────────────────────────────────────────────
56+
57+
/// GNN rank request passed across the C-ABI boundary.
58+
/// The graph is encoded as a pre-serialised JSON blob for the stub phase;
59+
/// L1 wave 1 replaces this with a zero-copy Cap'n Proto builder once
60+
/// `capnp compile -ozig` output is available.
61+
pub const EchidnaGnnRequest = extern struct {
62+
/// Opaque request identifier (null-terminated, max 63 chars + NUL).
63+
request_id: [64]u8,
64+
/// Pointer to UTF-8 JSON array of graph nodes (NOT null-terminated).
65+
graph_nodes_json_ptr: [*c]const u8,
66+
/// Byte length of graph_nodes_json_ptr.
67+
graph_nodes_len: usize,
68+
/// Maximum number of premises to return (must be > 0; default 20).
69+
top_k: u32,
70+
/// Minimum score threshold; results below this are suppressed.
71+
min_score: f32,
72+
};
73+
74+
/// GNN rank response returned across the C-ABI boundary.
75+
/// On success the caller owns rankings_json_ptr and MUST call
76+
/// echidna_capnp_free_response to release it.
77+
pub const EchidnaGnnResponse = extern struct {
78+
/// Echo of the request_id from the matching EchidnaGnnRequest.
79+
request_id: [64]u8,
80+
/// Pointer to UTF-8 JSON array of PremiseScore objects. NULL on error.
81+
rankings_json_ptr: [*c]const u8,
82+
/// Byte length of rankings_json (0 on error).
83+
rankings_len: u32,
84+
/// Round-trip wall-clock time in milliseconds.
85+
elapsed_ms: u64,
86+
};
87+
88+
// ─── Exported C-ABI functions ─────────────────────────────────────────────────
89+
90+
/// Open a Unix domain socket connection to the ECHIDNA IPC endpoint.
91+
///
92+
/// Returns: ≥ 0 file descriptor on success, -1 on failure.
93+
/// On failure call echidna_capnp_status_message(-1, buf, buflen) for details.
94+
export fn echidna_capnp_connect(sock_path: [*c]const u8) callconv(.C) i32 {
95+
if (sock_path == null) {
96+
setError(.invalid_param, "sock_path must not be NULL", .{});
97+
return -1;
98+
}
99+
const path_slice = std.mem.sliceTo(sock_path, 0);
100+
if (path_slice.len == 0) {
101+
setError(.invalid_param, "sock_path must not be empty", .{});
102+
return -1;
103+
}
104+
105+
const addr = std.net.Address.initUnix(path_slice) catch |err| {
106+
setError(.connect_failed, "invalid socket path '{s}': {}", .{ path_slice, err });
107+
return -1;
108+
};
109+
110+
const sock = std.net.tcpConnectToAddress(addr) catch |err| {
111+
setError(.connect_failed, "connect to '{s}' failed: {}", .{ path_slice, err });
112+
return -1;
113+
};
114+
115+
clearError();
116+
return sock.handle;
117+
}
118+
119+
/// Close a file descriptor previously returned by echidna_capnp_connect.
120+
/// Safe to call with fd < 0 (no-op).
121+
export fn echidna_capnp_close(fd: i32) callconv(.C) void {
122+
if (fd < 0) return;
123+
std.posix.close(@intCast(fd));
124+
}
125+
126+
/// Send a GNN rank request and receive the response.
127+
///
128+
/// STUB — returns CapnpStatus.stub_not_implemented until L1 wave 1 lands.
129+
/// The response struct is zeroed before returning so callers that check
130+
/// rankings_json_ptr for NULL get a well-defined value.
131+
///
132+
/// Returns: 0 on success, negative on error.
133+
/// -2 (stub_not_implemented): expected until `just capnp-gen` is run in L1 wave 1.
134+
export fn echidna_capnp_gnn_rank(
135+
fd: i32,
136+
req: *const EchidnaGnnRequest,
137+
resp: *EchidnaGnnResponse,
138+
) callconv(.C) i32 {
139+
if (fd < 0) {
140+
setError(.not_connected, "fd {d} is invalid (not connected)", .{fd});
141+
return @intFromEnum(CapnpStatus.not_connected);
142+
}
143+
_ = req;
144+
resp.* = std.mem.zeroes(EchidnaGnnResponse);
145+
setError(
146+
.stub_not_implemented,
147+
"L1 wave 1: Cap'n Proto bindings not yet generated — run `just capnp-gen`",
148+
.{},
149+
);
150+
return @intFromEnum(CapnpStatus.stub_not_implemented);
151+
}
152+
153+
/// Free a response buffer allocated by echidna_capnp_gnn_rank.
154+
/// No-op in the stub (no allocations are made). Must be called in the real
155+
/// implementation to release the Cap'n Proto message buffer.
156+
export fn echidna_capnp_free_response(resp: *EchidnaGnnResponse) callconv(.C) void {
157+
_ = resp;
158+
}
159+
160+
/// Write a human-readable description of `status` into `buf`.
161+
///
162+
/// If the most recent call on this thread stored a detailed message for
163+
/// this status code, that message is used. Otherwise a generic description
164+
/// is written. Output is always null-terminated and never exceeds buflen bytes.
165+
export fn echidna_capnp_status_message(
166+
status: i32,
167+
buf: [*c]u8,
168+
buflen: usize,
169+
) callconv(.C) void {
170+
if (buflen == 0 or buf == null) return;
171+
172+
if (last_error_len > 0 and @intFromEnum(last_error_status) == status) {
173+
const src = last_error_buf[0..last_error_len];
174+
const n = @min(src.len, buflen - 1);
175+
@memcpy(buf[0..n], src[0..n]);
176+
buf[n] = 0;
177+
return;
178+
}
179+
180+
const generic: []const u8 = switch (status) {
181+
0 => "ok",
182+
-1 => "not connected",
183+
-2 => "stub not implemented (L1 wave 1 pending)",
184+
-3 => "invalid parameter",
185+
-4 => "I/O error",
186+
-6 => "connect failed",
187+
-99 => "unknown error",
188+
else => "unrecognised status code",
189+
};
190+
const n = @min(generic.len, buflen - 1);
191+
@memcpy(buf[0..n], generic[0..n]);
192+
buf[n] = 0;
193+
}

schemas/VERSIONING.md

Lines changed: 107 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,107 @@
1+
<!--
2+
SPDX-License-Identifier: PMPL-1.0-or-later
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
-->
5+
6+
# Cap'n Proto Schema Versioning Policy
7+
8+
Schema file: `schemas/echidna.capnp`
9+
Schema ID: `@0xd3b45f8ae1c79012` (immutable — generated once, never changed)
10+
11+
## Wire Compatibility Guarantee
12+
13+
Cap'n Proto's wire format is **forward- and backward-compatible by default**,
14+
but only if the following rule is obeyed without exception:
15+
16+
> **Add fields at the end of a struct only. Never reorder, rename, or remove
17+
> existing fields. Never change an existing field's type or ordinal number.**
18+
19+
Each field carries an explicit ordinal (`@N`). The ordinal is its wire identity.
20+
Renaming a field in the `.capnp` source is safe (it only changes the generated
21+
symbol name). Changing `@N` or the field type is a **breaking change**.
22+
23+
## Non-Breaking Changes (safe to make freely)
24+
25+
| Change | Why it is safe |
26+
|--------|----------------|
27+
| Add a new field at the end of a struct (`@N` where N > current max) | Older readers ignore unknown fields; older writers produce zero for missing fields |
28+
| Add a new struct or enum anywhere in the file | Unused by older code |
29+
| Add a new enum variant at the end | Older code sees it as an unknown discriminant |
30+
| Rename a field or type (source only) | Ordinals and wire layout unchanged |
31+
| Change a default value in the schema | Wire encoding unaffected; generated code picks up the new default |
32+
| Add a new `annotation` | Not encoded on the wire |
33+
34+
## Breaking Changes (require a new struct name or a bumped `schemaVersion` field)
35+
36+
| Change | Why it breaks |
37+
|--------|---------------|
38+
| Remove or reorder a field | Changes the ordinal-to-meaning mapping |
39+
| Change a field's type | Existing wire bytes are misinterpreted |
40+
| Change a field's ordinal number | Direct wire breakage |
41+
| Remove an enum variant | Existing discriminant values become invalid |
42+
| Reorder enum variants | Discriminant values shift |
43+
44+
If a breaking change is truly necessary, **create a new top-level struct**
45+
(e.g. `GnnRankRequestV2`) and increment the `schemaVersion` content field.
46+
Do not alter `@0xd3b45f8ae1c79012`.
47+
48+
## Content Versioning (`schemaVersion` field)
49+
50+
The schema ID identifies the file-level wire format and is fixed. For
51+
application-level content versioning, add a `schemaVersion @N :UInt32`
52+
field to any message that needs it (default `1`). Consumers check this field
53+
and reject or transform messages from unexpected versions. Current L1 messages
54+
omit it — add when the first breaking content change is needed.
55+
56+
## Adding a New Message Type
57+
58+
1. Append the new struct or enum at the **end** of `echidna.capnp`.
59+
2. Add a section-header comment (see existing style).
60+
3. Run `just capnp-gen` to regenerate all language bindings.
61+
4. Update `src/abi/EchidnaABI/CapnSchemas.idr` (see §Idris2 below).
62+
5. If the new type is part of a breaking redesign, bump `schemaVersion` in
63+
the affected request/response structs rather than changing the schema ID.
64+
65+
## Regenerating Bindings (`just capnp-gen`)
66+
67+
After every schema change — including non-breaking additions — run:
68+
69+
```sh
70+
just capnp-gen
71+
```
72+
73+
This regenerates `src/rust/ipc/echidna_capnp.rs` (and future Zig/Julia targets
74+
as they are wired into the recipe). **Commit generated bindings.** They are
75+
checked in so that consumers without a local `capnp` installation can build.
76+
A CI check (`just capnp-gen-check`) verifies committed bindings match the
77+
schema; failing it is a merge blocker.
78+
79+
## Multi-Language Consumers
80+
81+
| Language | Binding mechanism | Status |
82+
|----------|------------------|--------|
83+
| **Rust** | `capnpc-rust` (generated `echidna_capnp.rs`) | L1 wave 1 target |
84+
| **Idris2** | `src/abi/EchidnaABI/CapnSchemas.idr` — type mirror + proofs | Present; update alongside schema |
85+
| **Julia** | `CapnProto.jl` or Zig C-ABI shim (TBD — see open question in TODO.md) | `src/julia/ipc.jl` stub present |
86+
| **Zig** | C-ABI bridge in `ffi/zig/src/capnp_bridge.zig` | Stub present; real impl in L1 wave 1 |
87+
88+
## Idris2 ABI Proofs (`src/abi/EchidnaABI/CapnSchemas.idr`)
89+
90+
`CapnSchemas.idr` mirrors enum cardinalities and struct field counts as Idris2
91+
types and proves bounded-representation invariants. When adding a field or
92+
enum variant:
93+
94+
1. Add the corresponding constructor to the Idris2 mirror type.
95+
2. Update the `allXxx` Vect witness and its `xxxCountCorrect : length … = n` proof.
96+
3. Re-run `%search` on the `xxxBounded : LTE n 256` proof (it will still hold).
97+
4. Zero `believe_me` is a hard invariant — all proofs must be constructive.
98+
99+
## Quick Reference
100+
101+
```
102+
Safe: add field at end, add struct, add enum variant at end, rename
103+
Unsafe: remove, reorder, change type, change ordinal
104+
If breaking: new struct name + increment schemaVersion field
105+
After any change: just capnp-gen && commit generated bindings
106+
Update CapnSchemas.idr to match
107+
```

0 commit comments

Comments
 (0)