Skip to content

Commit 93ffe14

Browse files
claudeclaude
committed
feat(capnp-l1.0): add echidna-wire crate with 7 Cap'n Proto schemas
First slice of L1 Cap'n Proto work (ECHIDNA IPC protocol swap). L1.0 scope is schema + build + bindings-compile only; transport layer (UDS, WebSocket), peer integrations (Julia, Chapel, UI), Idris2 ABI proofs and core conversion helpers ship in L1.1+. New workspace member `crates/echidna-wire/` mirrors the `crates/typed_wasm/` pattern from S3. Contains: Schemas (4 .capnp files, all high-bit file IDs per capnp convention): - common.capnp (92 LoC) — Term (15-variant union), Pattern, Tactic (10-variant union), Hypothesis, Goal, Theorem, Context, Definition, Variable. Term is structured recursive union (not s-expr string) so Rust/Julia/Chapel/UI all zero-copy. - prover.capnp (68 LoC) — AxiomUsage, TrustedOutcome (mirrors ProverOutcome's 8-variant taxonomy from provers/outcome.rs + TrustFactors from verification/confidence.rs), ProverInvocation. - proof.capnp (52 LoC) — ProofGoal, ProofResult, RunDiagnostics, PerProverRecord. Imports prover.capnp (for TrustedOutcome + AxiomUsage — placed in prover.capnp to break what would otherwise be a proof↔prover import cycle). - gnn.capnp (62 LoC) — GnnGraphPayload, GnnServerHints, GnnRankRequest, GnnRankResponse, FloatVec, TacticSuggestion. Field names preserved verbatim from current JSON shape in src/rust/gnn/client.rs so the Julia side needs only a JSON→capnp adapter, not a rename table. ProverKind encoding on the wire: `UInt16` stable discriminant (from kind_to_u8 in ffi/mod.rs) + `Text` canonical name as defence-in-depth, never enumerated as a capnp union (105 variants, would churn). Every root message stamps `schemaVersion :UInt16 = 1`. VERSIONING.md documents the append-only evolution policy and connection-time Hello negotiation (schema deferred to L1.1). Build + tests: - Cargo.toml: capnp = "0.20" runtime, capnpc = "0.20" build-dep. - build.rs: capnpc::CompilerCommand over the 4 schemas with src_prefix="schemas". - src/lib.rs: 4 pub mods named `<stem>_capnp` to match capnpc-rust's generated cross-file references, plus ergonomic `pub use common_capnp as common;` aliases for downstream consumers. - 3 smoke tests (ProofGoal round-trip, GnnRankRequest construction, TrustedOutcome::Proved union) pass under `cargo test -p echidna-wire --lib smoke`. Root Cargo.toml workspace.members gains "crates/echidna-wire". Root echidna crate does NOT yet depend on echidna-wire — nothing consumes wire types at L1.0.
1 parent 667110f commit 93ffe14

10 files changed

Lines changed: 508 additions & 0 deletions

File tree

‎Cargo.lock‎

Lines changed: 32 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎Cargo.toml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,7 @@ harness = false
112112

113113
[workspace]
114114
members = [
115+
"crates/echidna-wire",
115116
"crates/typed_wasm",
116117
"src/interfaces/graphql",
117118
"src/interfaces/grpc",

‎crates/echidna-wire/Cargo.toml‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
3+
[package]
4+
name = "echidna-wire"
5+
version = "0.1.0"
6+
edition = "2021"
7+
authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
8+
license = "PMPL-1.0-or-later"
9+
description = "L1 IPC wire types for ECHIDNA (Cap'n Proto schemas + generated bindings)"
10+
repository = "https://github.com/hyperpolymath/echidna"
11+
build = "build.rs"
12+
13+
[dependencies]
14+
capnp = "0.20"
15+
16+
[build-dependencies]
17+
capnpc = "0.20"

‎crates/echidna-wire/build.rs‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
3+
fn main() {
4+
capnpc::CompilerCommand::new()
5+
.src_prefix("schemas")
6+
.file("schemas/common.capnp")
7+
.file("schemas/prover.capnp")
8+
.file("schemas/proof.capnp")
9+
.file("schemas/gnn.capnp")
10+
.run()
11+
.expect("capnpc build failed");
12+
}

‎crates/echidna-wire/schemas/VERSIONING.md‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
2+
3+
# ECHIDNA Wire Schema Versioning Policy (`crates/echidna-wire`)
4+
5+
Every root message MUST carry `schemaVersion :UInt16`. Current: **1**.
6+
File-level capnp IDs (`@0x…;`) are generated once and NEVER changed.
7+
8+
## Compatibility model
9+
10+
Cap'n Proto is structurally forward/backward-compatible within a major
11+
version provided the rules below are respected. Major version bumps are
12+
breaking and require a coordinated rollout across Rust core, Julia,
13+
Chapel, and UI peers.
14+
15+
## Adding a field (SAFE — no version bump)
16+
17+
- Append new fields at the next unused `@N`.
18+
- New fields MUST either:
19+
- (a) have a default value (e.g. `@N :Bool = false`), OR
20+
- (b) be paired with a `has<Name> :Bool` sibling for optional semantics.
21+
- New union variants may be appended at the end of an existing union.
22+
- New nested structs may be added freely.
23+
24+
## Removing / changing a field (UNSAFE — major bump)
25+
26+
- Reordering `@N` IDs of existing fields.
27+
- Changing a field's wire type (e.g. `UInt32` → `UInt64`).
28+
- Removing a non-optional field.
29+
- Reordering union discriminants.
30+
- Changing the stable `ProverKind` discriminant mapping
31+
(mirrored in `src/rust/ffi/mod.rs`).
32+
33+
## Deprecation flow
34+
35+
1. Mark the field obsolete in this file and in a comment on the `.capnp`
36+
line. Add a new replacement field at the next `@N`.
37+
2. Wait ONE minor version before removal candidacy (L1.0 → L1.1).
38+
3. Field removal = major bump (L1.x → L2.0). Must ship an
39+
`echidna-wire v2` alongside v1 for at least one release cycle.
40+
41+
## Connection-time negotiation
42+
43+
Every transport session opens with a `Hello` exchange (schema deferred
44+
to L1.1 in `version.capnp`):
45+
46+
```
47+
client → server : Hello { supportedMajors :List(UInt16); preferredMajor :UInt16; }
48+
server → client : HelloAck { agreedMajor :UInt16; agreedMinor :UInt16; }
49+
```
50+
51+
If no overlap: server returns `HelloAck { agreedMajor = 0 }` and closes.
52+
53+
## ProverKind discriminant governance
54+
55+
Appending a new variant to `ProverKind` (`src/rust/provers/mod.rs`) is
56+
SAFE iff:
57+
58+
- the next contiguous `u16` is used (currently 105),
59+
- `kind_from_u8` / `kind_to_u8` are updated in lockstep
60+
(`src/rust/ffi/mod.rs`),
61+
- this file records the assignment.
62+
63+
Holes in the discriminant space are FORBIDDEN — the invertibility test
64+
at `src/rust/ffi/mod.rs` (see `kind_to_u8_injective` / round-trip tests)
65+
must keep passing.
66+
67+
## Current assignments
68+
69+
- Schema major: **1**. Minor: **0**.
70+
- File IDs:
71+
- `common.capnp` = `@0xf2f7187fddaa9139`
72+
- `proof.capnp` = `@0xfa73f2ec7415f450`
73+
- `prover.capnp` = `@0xf1841ae6bbc44651`
74+
- `gnn.capnp` = `@0xfbb66b8481def8a0`
75+
- Deprecations in flight: none.

‎crates/echidna-wire/schemas/common.capnp‎

Lines changed: 92 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
@0xf2f7187fddaa9139;
2+
3+
# Schema version stamped into every root message. Bumped only on incompatible
4+
# changes per VERSIONING.md. L1.0 = 1.
5+
const schemaVersionMajor :UInt16 = 1;
6+
const schemaVersionMinor :UInt16 = 0;
7+
8+
struct Term {
9+
union {
10+
var @0 :Text;
11+
const @1 :Text;
12+
app @2 :App;
13+
lambda @3 :Lambda;
14+
pi @4 :Pi;
15+
sigma @5 :Sigma;
16+
typeU @6 :UInt32;
17+
sort @7 :UInt32;
18+
universe @8 :UInt32;
19+
letBind @9 :Let;
20+
matchE @10 :Match;
21+
fixE @11 :Fix;
22+
hole @12 :Text;
23+
meta @13 :UInt64;
24+
proverSpecific @14 :ProverSpecific;
25+
}
26+
27+
struct App { func @0 :Term; args @1 :List(Term); }
28+
struct Lambda { param @0 :Text; paramType @1 :Term; body @2 :Term; hasParamType @3 :Bool; }
29+
struct Pi { param @0 :Text; paramType @1 :Term; body @2 :Term; }
30+
struct Sigma { param @0 :Text; paramType @1 :Term; body @2 :Term; }
31+
struct Let { name @0 :Text; ty @1 :Term; value @2 :Term; body @3 :Term; hasTy @4 :Bool; }
32+
struct Match { scrutinee @0 :Term; returnType @1 :Term; hasReturnType @2 :Bool;
33+
branches @3 :List(Branch); }
34+
struct Fix { name @0 :Text; ty @1 :Term; body @2 :Term; hasTy @3 :Bool; }
35+
struct ProverSpecific { prover @0 :Text; dataJson @1 :Text; }
36+
struct Branch { pattern @0 :Pattern; body @1 :Term; }
37+
}
38+
39+
struct Pattern {
40+
union {
41+
wildcard @0 :Void;
42+
var @1 :Text;
43+
constructor @2 :Ctor;
44+
}
45+
struct Ctor { name @0 :Text; args @1 :List(Pattern); }
46+
}
47+
48+
struct Tactic {
49+
union {
50+
apply @0 :Text;
51+
intro @1 :IntroT;
52+
cases @2 :Term;
53+
induction @3 :Term;
54+
rewrite @4 :Text;
55+
simplify @5 :Void;
56+
reflexivity @6 :Void;
57+
assumption @7 :Void;
58+
exact @8 :Term;
59+
custom @9 :Custom;
60+
}
61+
struct IntroT { name @0 :Text; hasName @1 :Bool; }
62+
struct Custom { prover @0 :Text; command @1 :Text; args @2 :List(Text); }
63+
}
64+
65+
struct Hypothesis {
66+
name @0 :Text;
67+
ty @1 :Term;
68+
body @2 :Term;
69+
hasBody @3 :Bool;
70+
}
71+
72+
struct Goal {
73+
id @0 :Text;
74+
target @1 :Term;
75+
hypotheses @2 :List(Hypothesis);
76+
}
77+
78+
struct Theorem {
79+
name @0 :Text;
80+
statement @1 :Term;
81+
aspects @2 :List(Text);
82+
}
83+
84+
struct Context {
85+
theorems @0 :List(Theorem);
86+
axioms @1 :List(Text);
87+
definitions @2 :List(Definition);
88+
variables @3 :List(Variable);
89+
}
90+
91+
struct Definition { name @0 :Text; ty @1 :Term; body @2 :Term; }
92+
struct Variable { name @0 :Text; ty @1 :Term; }

‎crates/echidna-wire/schemas/gnn.capnp‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,62 @@
1+
@0xfbb66b8481def8a0;
2+
3+
using Common = import "common.capnp";
4+
5+
struct GnnGraphPayload {
6+
numNodes @0 :UInt32;
7+
numEdges @1 :UInt32;
8+
edgeSrc @2 :List(UInt32);
9+
edgeDst @3 :List(UInt32);
10+
edgeWeights @4 :List(Float32);
11+
edgeKinds @5 :List(Text);
12+
nodeFeatures @6 :List(Float32);
13+
featureDim @7 :UInt32;
14+
nodeKinds @8 :List(Text);
15+
nodeLabels @9 :List(Text);
16+
goalNodeIdx @10 :UInt32 = 4294967295;
17+
hasGoalNode @11 :Bool;
18+
premiseNodeIndices @12 :List(UInt32);
19+
}
20+
21+
struct GnnServerHints {
22+
numGnnLayers @0 :UInt16 = 4;
23+
useAttention @1 :Bool = true;
24+
}
25+
26+
struct GnnRankRequest {
27+
schemaVersion @0 :UInt16 = 1;
28+
requestId @1 :Text;
29+
graph @2 :GnnGraphPayload;
30+
topK @3 :UInt32 = 20;
31+
minScore @4 :Float32 = 0.05;
32+
includeEmbeddings @5 :Bool = false;
33+
config @6 :GnnServerHints;
34+
}
35+
36+
struct FloatVec { values @0 :List(Float32); }
37+
38+
struct GnnRankResponse {
39+
schemaVersion @0 :UInt16 = 1;
40+
requestId @1 :Text;
41+
success @2 :Bool;
42+
scores @3 :List(Float32);
43+
premiseNames @4 :List(Text);
44+
embeddings @5 :List(FloatVec);
45+
inferenceTimeMs @6 :Float32;
46+
error @7 :Text;
47+
}
48+
49+
struct TacticSuggestion {
50+
schemaVersion @0 :UInt16 = 1;
51+
requestId @1 :Text;
52+
tactic @2 :Text;
53+
structuredTactic @3 :Common.Tactic;
54+
hasStructured @4 :Bool;
55+
confidence @5 :Float32;
56+
premise @6 :Text;
57+
hasPremise @7 :Bool;
58+
aspectTags @8 :List(Text);
59+
gnnScore @9 :Float32 = 0;
60+
symbolicScore @10 :Float32 = 0;
61+
fromServer @11 :Bool = false;
62+
}

‎crates/echidna-wire/schemas/proof.capnp‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
@0xfa73f2ec7415f450;
2+
3+
using Common = import "common.capnp";
4+
using Prover = import "prover.capnp";
5+
6+
struct ProofGoal {
7+
schemaVersion @0 :UInt16 = 1;
8+
requestId @1 :Text;
9+
sessionId @2 :Text;
10+
goal @3 :Common.Goal;
11+
context @4 :Common.Context;
12+
preferredProverKind @5 :UInt16 = 65535;
13+
preferredProverName @6 :Text;
14+
timeoutMs @7 :UInt32 = 300000;
15+
minTrustLevel @8 :UInt8 = 2;
16+
crossCheck @9 :Bool = false;
17+
requestDiagnostics @10 :Bool = false;
18+
trackAxioms @11 :Bool = true;
19+
generateCertificate @12 :Bool = false;
20+
metadataJson @13 :Text;
21+
}
22+
23+
struct ProofResult {
24+
schemaVersion @0 :UInt16 = 1;
25+
requestId @1 :Text;
26+
verified @2 :Bool;
27+
trustLevel @3 :UInt8;
28+
proversUsed @4 :List(Text);
29+
proofTimeMs @5 :UInt64;
30+
goalsRemaining @6 :UInt32;
31+
message @7 :Text;
32+
crossChecked @8 :Bool;
33+
outcome @9 :Prover.TrustedOutcome;
34+
axiomReport @10 :Prover.AxiomUsage;
35+
hasAxiomReport @11 :Bool;
36+
certificateHash @12 :Text;
37+
hasCertificate @13 :Bool;
38+
diagnostics @14 :RunDiagnostics;
39+
hasDiagnostics @15 :Bool;
40+
}
41+
42+
struct RunDiagnostics {
43+
normalizedInput @0 :Text;
44+
proversSelected @1 :List(Text);
45+
perProver @2 :List(PerProverRecord);
46+
}
47+
48+
struct PerProverRecord {
49+
prover @0 :Text;
50+
outcome @1 :Prover.TrustedOutcome;
51+
elapsedMs @2 :UInt64;
52+
}

0 commit comments

Comments
 (0)