Skip to content

Commit d384a39

Browse files
hyperpolymathhyperpolymath
committed
Merge PR #146: coord-fed-phase1-identity (#146)
2 parents d3da963 + 1de44b3 commit d384a39

19 files changed

Lines changed: 1084 additions & 18 deletions

‎.hypatia-ignore‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,3 +39,22 @@ cicd_rules/banned_language_file:panll/src/modules/BojModule.res
3939
cicd_rules/banned_language_file:cartridges/orchestrator-lsp-mcp/panels/src/Extension.res
4040
cicd_rules/banned_language_file:cartridges/orchestrator-lsp-mcp/panels/src/LanguageClient.res
4141
cicd_rules/banned_language_file:cartridges/orchestrator-lsp-mcp/panels/src/VscodeApi.res
42+
43+
# ─── MCP cartridge adapters — TypeScript exemption (CLAUDE.md §TS Exemptions) ─
44+
#
45+
# The "no new TypeScript" rule has 6 approved exemptions, all MCP cartridge
46+
# adapters that use the TypeScript-native @anthropic/sdk. The exemption is
47+
# documented in .claude/CLAUDE.md with full rationale, audit lineage
48+
# (TS-elimination audit, 2026-05-02) and an unblock condition (AffineScript
49+
# bindings to MCP). Mirroring it here so the Hypatia scanner stops
50+
# flagging them as critical "banned_language_file" findings — the
51+
# governance policy and the scanner exemption must agree.
52+
#
53+
# Adding new entries requires explicit user approval and an unblock
54+
# condition (per CLAUDE.md). The 6 files below are the closed set.
55+
cicd_rules/banned_language_file:cartridges/academic-workflow-mcp/adapter/mod.ts
56+
cicd_rules/banned_language_file:cartridges/bofig-mcp/adapter/mod.ts
57+
cicd_rules/banned_language_file:cartridges/ephapax-mcp/adapter/mod.ts
58+
cicd_rules/banned_language_file:cartridges/fireflag-mcp/adapter/mod.ts
59+
cicd_rules/banned_language_file:cartridges/hesiod-mcp/adapter/mod.ts
60+
cicd_rules/banned_language_file:cartridges/sanctify-mcp/adapter/mod.ts

‎cartridges/local-coord-mcp/abi/LocalCoord/Identity.idr‎

Lines changed: 213 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,213 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
||| LocalCoord.Identity: Cryptographic peer identity for the local-coord
4+
||| cartridge.
5+
|||
6+
||| Cartridge: local-coord-mcp
7+
||| ADR: 0016 (mTLS + ed25519 federation stop-gap), Phase 1 — identity
8+
||| foundation. No transport here; this module defines the *types* and
9+
||| *FFI signatures* for an ed25519 keypair per peer, the public key as
10+
||| federated identity, and the known_peers.toml entry shape. The Zig
11+
||| implementation (cartridges/local-coord-mcp/adapter/) realises these
12+
||| signatures with std.crypto.sign.Ed25519.
13+
|||
14+
||| Phase-1 scope (deliberate non-promises):
15+
||| * Generates / loads ed25519 keypair material on disk.
16+
||| * Exposes the public key for human export.
17+
||| * Parses known_peers.toml.
18+
||| * Does NOT sign or verify anything — Phase 2.
19+
||| * Does NOT bind to any non-loopback address — Phase 3.
20+
||| * Does NOT change the `FederationPolicy = LocalOnly` invariant from
21+
||| SafeLocalCoord.idr. Identity material is necessary-but-not-
22+
||| sufficient for federation; carrying a keypair does not enable it.
23+
module LocalCoord.Identity
24+
25+
import Data.List
26+
import Data.Vect
27+
import Data.Nat
28+
29+
import LocalCoord.SafeLocalCoord
30+
31+
%default total
32+
33+
-- ═══════════════════════════════════════════════════════════════════════════
34+
-- Key Material — Size-Indexed Byte Vectors
35+
-- ═══════════════════════════════════════════════════════════════════════════
36+
37+
||| ed25519 public-key length in bytes. RFC 8032 §5.1.5.
38+
public export
39+
ed25519PubKeyBytes : Nat
40+
ed25519PubKeyBytes = 32
41+
42+
||| ed25519 private-key length in bytes (seed form). RFC 8032 §5.1.5.
43+
||| The expanded secret-scalar form is 64 bytes; we store the 32-byte
44+
||| seed and derive the scalar at sign time.
45+
public export
46+
ed25519PrivKeyBytes : Nat
47+
ed25519PrivKeyBytes = 32
48+
49+
||| ed25519 signature length in bytes (R || S). RFC 8032 §5.1.6.
50+
public export
51+
ed25519SigBytes : Nat
52+
ed25519SigBytes = 64
53+
54+
||| A fixed-width byte vector. Used to enforce key-material sizes at
55+
||| the type level — the only way to construct an `Ed25519PublicKey`
56+
||| is via a value of `Bytes 32`, so any code holding one *knows* it
57+
||| has 32 bytes without runtime checks.
58+
public export
59+
Bytes : Nat -> Type
60+
Bytes n = Vect n Bits8
61+
62+
||| An ed25519 public key. Wrapper around `Bytes 32` so the type system
63+
||| distinguishes pubkeys from arbitrary 32-byte blobs.
64+
public export
65+
record Ed25519PublicKey where
66+
constructor MkPubKey
67+
bytes : Bytes ed25519PubKeyBytes
68+
69+
||| An ed25519 private key (seed form). NEVER crosses the FFI boundary
70+
||| as a payload — the Zig adapter holds it in process memory and
71+
||| references it via opaque handle. This type exists in the ABI only
72+
||| to document the contract.
73+
public export
74+
record Ed25519PrivateKey where
75+
constructor MkPrivKey
76+
bytes : Bytes ed25519PrivKeyBytes
77+
78+
||| An ed25519 signature over arbitrary bytes.
79+
public export
80+
record Ed25519Signature where
81+
constructor MkSig
82+
bytes : Bytes ed25519SigBytes
83+
84+
-- ═══════════════════════════════════════════════════════════════════════════
85+
-- Proof Obligation P-20: Ed25519 Key Material Well-Formedness
86+
-- ═══════════════════════════════════════════════════════════════════════════
87+
--
88+
-- A public key value carries exactly `ed25519PubKeyBytes` bytes; a
89+
-- signature value carries exactly `ed25519SigBytes`. This is enforced
90+
-- *by construction* via `Vect n` — the only inhabitants of
91+
-- `Bytes ed25519PubKeyBytes` are length-32 byte vectors, so any code
92+
-- receiving an `Ed25519PublicKey` is statically guaranteed it has the
93+
-- right length. No runtime size check is needed; no
94+
-- malformed-key branch can exist in the protocol layer.
95+
--
96+
-- The "proof" is the type itself: pattern-matching `MkPubKey bs`
97+
-- recovers a `bs : Vect 32 Bits8`, whose index is fixed at the
98+
-- definition site and cannot be shrunk or grown.
99+
--
100+
-- Demonstration: a concrete zero-keyed pubkey is built-in-shape.
101+
102+
||| Demonstration witness — a concrete pubkey value built from a
103+
||| size-32 literal compiles iff the type's size invariant holds.
104+
||| If this line fails to compile, P-20 has been broken.
105+
public export
106+
zeroPubKey : Ed25519PublicKey
107+
zeroPubKey = MkPubKey (replicate ed25519PubKeyBytes 0)
108+
109+
||| Same demonstration for signatures.
110+
public export
111+
zeroSig : Ed25519Signature
112+
zeroSig = MkSig (replicate ed25519SigBytes 0)
113+
114+
-- ═══════════════════════════════════════════════════════════════════════════
115+
-- Peer Identity = PeerId + Public Key
116+
-- ═══════════════════════════════════════════════════════════════════════════
117+
118+
||| A peer's complete identity: the human-readable `PeerId` (from
119+
||| SafeLocalCoord) plus the ed25519 public key that vouches for it.
120+
||| The PeerId is for humans; the pubkey is for crypto.
121+
public export
122+
record PeerIdentity where
123+
constructor MkPeerIdentity
124+
peerId : PeerId
125+
pubKey : Ed25519PublicKey
126+
127+
||| Extract the display form of a peer identity. Goes through the
128+
||| existing PeerId display — the pubkey is intentionally not rendered
129+
||| here (use `pubKeyHex` for that, in a UI context).
130+
public export
131+
identityToString : PeerIdentity -> String
132+
identityToString pi = peerIdToString (peerId pi)
133+
134+
-- ═══════════════════════════════════════════════════════════════════════════
135+
-- Known Peers (known_peers.toml entries) — Trust List
136+
-- ═══════════════════════════════════════════════════════════════════════════
137+
138+
||| An entry in `~/.config/coord-tui/known_peers.toml`. Manual trust
139+
||| list: peers we have explicitly agreed to federate with. No
140+
||| discovery, no CA hierarchy — SSH known_hosts model.
141+
|||
142+
||| The `host` and `port` fields are Phase-3 wire material; Phase 1
143+
||| parses them but does not connect to them.
144+
public export
145+
record KnownPeer where
146+
constructor MkKnownPeer
147+
peerId : PeerId
148+
pubKey : Ed25519PublicKey
149+
host : String -- DNS name or literal IP — validated at use-site
150+
port : Nat
151+
152+
||| The maximum number of known peers a single host may trust.
153+
||| Bound is generous; it exists to make `Vect`-based loading easy.
154+
public export
155+
maxKnownPeers : Nat
156+
maxKnownPeers = 64
157+
158+
-- ═══════════════════════════════════════════════════════════════════════════
159+
-- Federation Invariant Preservation
160+
-- ═══════════════════════════════════════════════════════════════════════════
161+
--
162+
-- Crucially: this module adds *types*. It does not add a path from
163+
-- those types to any non-loopback bind. The `FederationPolicy` value
164+
-- in SafeLocalCoord remains `LocalOnly`, and `IsFederated LocalOnly`
165+
-- remains uninhabited. Phase 3 will widen this — Phase 1 must not.
166+
167+
||| Proof that having a PeerIdentity does not unlock federation. The
168+
||| federation policy is still `LocalOnly`, and the negative proof
169+
||| from `SafeLocalCoord.localOnlyNotFederated` carries through.
170+
||| Discharge is structural: the LHS doesn't influence the RHS at all.
171+
export
172+
identityDoesNotEnableFederation
173+
: (_ : PeerIdentity)
174+
-> IsFederated coordFederationPolicy
175+
-> Void
176+
identityDoesNotEnableFederation _ x = localOnlyNotFederated x
177+
178+
-- ═══════════════════════════════════════════════════════════════════════════
179+
-- C-ABI Contract (Phase 1) — documentation, not %foreign import
180+
-- ═══════════════════════════════════════════════════════════════════════════
181+
--
182+
-- The Zig adapter exposes the following entry points. They are NOT
183+
-- imported via `%foreign` here because the Idris2 ABI module's job is
184+
-- to *type* the contract; the actual calls are made from Zig (intra-
185+
-- cartridge) and from the Deno/Node bridge (over HTTP). This mirrors
186+
-- the convention used in `SafeLocalCoord.idr`, which defines the type
187+
-- envelope but doesn't import the Zig functions.
188+
--
189+
-- int boj_coord_identity_init(const char *key_path);
190+
-- Generates a fresh keypair if none exists at `key_path`, otherwise
191+
-- loads the existing seed. Persists the seed (0600) on disk. Phase
192+
-- 1 keys live at ~/.cache/coord-tui/peer.key.
193+
-- Returns: 0 on success, non-zero error code otherwise.
194+
--
195+
-- int boj_coord_identity_get_pubkey(uint8_t *out, size_t out_len);
196+
-- Copies `ed25519PubKeyBytes` (32) bytes of the local public key
197+
-- into `out`. The corresponding `Ed25519PublicKey` value can be
198+
-- reconstructed from the bytes on the consumer side.
199+
-- Returns: bytes written (== 32) on success, -1 if not initialised
200+
-- or buffer too small.
201+
--
202+
-- int boj_coord_identity_load_known_peers(const char *toml_path);
203+
-- Parses `~/.config/coord-tui/known_peers.toml` (or supplied path)
204+
-- into an in-process trust table of `KnownPeer` entries. Replaces
205+
-- any previously loaded set (full reload).
206+
-- Returns: number of entries loaded (>= 0) on success, -1 on error
207+
-- (missing file is treated as zero entries, not an error).
208+
--
209+
-- int boj_coord_identity_known_peer_count(void);
210+
-- Returns the current count of loaded known peers.
211+
--
212+
-- Phase 2 will add `boj_coord_envelope_sign` / `boj_coord_envelope_verify`
213+
-- once `LocalCoord.Federation` lands the P-22 obligation.

‎cartridges/local-coord-mcp/abi/LocalCoord/PROOF-SCHEDULE.adoc‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,10 @@ toc::[]
4343
| P-17 | Echo-type formalisation of audit + summary + hash chain | P-15, P-16 | Phase 3 (deferred) | Agda (echo-types repo)
4444
| P-18 | Tropical-semiring model of TTL + trust | P-17 | Phase 3 (deferred) | Agda (EchoTropical)
4545
| P-19 | Cross-site primacy ceremony | P-15…P-18 | Phase 4 (deferred) | Idris2 + Agda
46+
| P-20 | Ed25519 key-material well-formedness (pubkey ≡ 32B, sig ≡ 64B by construction) | — | ✅ done | Idris2 (`LocalCoord.Identity`)
47+
| P-21 | Identity carries forward `FederationPolicy ≡ LocalOnly` (identity ≠ federation) | P-20, P-02 | ✅ done | Idris2 (`LocalCoord.Identity.identityDoesNotEnableFederation`)
48+
| P-22 | Envelope signature soundness (sign-then-verify roundtrip on bytes) | P-20 | ADR-0016 Phase 5 | Idris2 (planned `LocalCoord.Federation`)
49+
| P-23 | mTLS peer pinning matches `known_peers.toml` pubkey | P-20, P-22 | ADR-0016 Phase 5 | Idris2 + std.crypto axiomatised
4650
|===
4751

4852
Stage priorities:

‎cartridges/local-coord-mcp/abi/local-coord-mcp.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,4 +9,5 @@ brief = "Local-coord MCP cartridge — localhost multi-instance coordinatio
99
sourcedir = "."
1010
modules = LocalCoord.SafeLocalCoord
1111
, LocalCoord.Protocol
12+
, LocalCoord.Identity
1213
depends = base

‎cartridges/local-coord-mcp/ffi/cartridge_shim.zig‎

Lines changed: 16 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -58,8 +58,14 @@ pub fn invokeArgsNull(
5858
/// Compare a C-NUL-terminated tool-name pointer against a Zig string
5959
/// literal. Caller must have already verified `tool_name` is non-null
6060
/// (usually via `invokeArgsNull`).
61+
///
62+
/// Implementation note (CWE-704 fix, post-#146): uses
63+
/// `std.mem.sliceTo(ptr, 0)` which scans the C string up to the first
64+
/// NUL — no `@ptrCast` and no `[*:0]` re-typing. The earlier
65+
/// `std.mem.spanZ` call was removed in Zig 0.14+ and would not
66+
/// compile under the 0.15.1 CI pin.
6167
pub fn toolIs(tool_name: [*c]const u8, expected: []const u8) bool {
62-
const s = std.mem.span(@as([*:0]const u8, @ptrCast(tool_name)));
68+
const s = std.mem.sliceTo(tool_name, 0);
6369
return std.mem.eql(u8, s, expected);
6470
}
6571

@@ -124,19 +130,19 @@ test "writeResult: empty body" {
124130
}
125131

126132
test "toolIs: matches and rejects" {
127-
const name: [*:0]const u8 = "foo";
128-
try std.testing.expect(toolIs(@ptrCast(name), "foo"));
129-
try std.testing.expect(!toolIs(@ptrCast(name), "bar"));
130-
try std.testing.expect(!toolIs(@ptrCast(name), "foobar"));
131-
try std.testing.expect(!toolIs(@ptrCast(name), "fo"));
133+
const name: [*c]const u8 = "foo";
134+
try std.testing.expect(toolIs(name, "foo"));
135+
try std.testing.expect(!toolIs(name, "bar"));
136+
try std.testing.expect(!toolIs(name, "foobar"));
137+
try std.testing.expect(!toolIs(name, "fo"));
132138
}
133139

134140
test "invokeArgsNull: detects each null slot" {
135141
var buf: [4]u8 = undefined;
136142
var len: usize = 4;
137-
const name: [*:0]const u8 = "x";
138-
try std.testing.expect(!invokeArgsNull(@ptrCast(name), &buf, &len));
143+
const name: [*c]const u8 = "x";
144+
try std.testing.expect(!invokeArgsNull(name, &buf, &len));
139145
try std.testing.expect(invokeArgsNull(null, &buf, &len));
140-
try std.testing.expect(invokeArgsNull(@ptrCast(name), null, &len));
141-
try std.testing.expect(invokeArgsNull(@ptrCast(name), &buf, null));
146+
try std.testing.expect(invokeArgsNull(name, null, &len));
147+
try std.testing.expect(invokeArgsNull(name, &buf, null));
142148
}

0 commit comments

Comments
 (0)