Skip to content

Commit df0add7

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(groove): add groove-proxy as reference instance of typed-frame-router
groove-protocol/reference/groove-proxy/ — the IPv4→IPv6 frame-level proxy, specialised from proven-servers/core/proven-typed-frame-router. README.adoc: - Relationship diagram (general primitive → specific instance) - Usage examples in Zig, Idris2, and CLI - Formal guarantees inherited from typed-frame-router - Default Groove configuration (ports 6460-6500, loopback) - Table of other possible TFR instances (SAN Bridge, BLE Gateway, Avow LAN, InfiniBand Proxy) GrooveProxy.idr: - Thin Idris2 wrapper importing TypedFrameRouter - grooveProxyConfig: default config for IPv4→IPv6 on loopback - grooveNoReverse: proof that Groove proxy cannot be reversed - Re-exports general safety proofs for Groove consumers Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 86aefb3 commit df0add7

2 files changed

Lines changed: 207 additions & 0 deletions

File tree

‎groove-protocol/reference/groove-proxy/GrooveProxy.idr‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
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+
-- GrooveProxy: IPv4→IPv6 specialisation of the Typed Frame Router.
5+
--
6+
-- This is an INSTANCE of proven-servers/core/proven-typed-frame-router,
7+
-- configured for the Groove Protocol's IPv4 sunset strategy.
8+
--
9+
-- It re-exports the general router types with Groove-specific defaults
10+
-- and adds Groove discovery integration (sunset headers, attestation).
11+
12+
module GrooveProxy
13+
14+
import TypedFrameRouter.Types
15+
import TypedFrameRouterABI
16+
import TypedFrameRouterABI.Proofs
17+
18+
%default total
19+
20+
---------------------------------------------------------------------------
21+
-- Groove-specific configuration
22+
---------------------------------------------------------------------------
23+
24+
||| Default Groove proxy configuration.
25+
||| Translates IPv4→IPv6 on the loopback interface for a given port.
26+
|||
27+
||| @param port The groove service port to proxy
28+
public export
29+
grooveProxyConfig : (port : Bits16) -> RouterConfig
30+
grooveProxyConfig port = MkRouterConfig
31+
{ source = MkEndpoint IPv4 "127.0.0.1" port
32+
, target = MkEndpoint IPv6 "::1" port
33+
, maxConnections = 64
34+
, bufferSize = 4096
35+
, translation = MkTranslation IPv4 IPv6
36+
}
37+
38+
||| The Groove proxy direction is always IPv4→IPv6.
39+
||| This is a specialisation of the general FrameTranslation.
40+
public export
41+
grooveDirection : FrameTranslation
42+
grooveDirection = MkTranslation IPv4 IPv6
43+
44+
---------------------------------------------------------------------------
45+
-- Groove-specific proofs (derived from general proofs)
46+
---------------------------------------------------------------------------
47+
48+
||| The Groove proxy inherits all four safety properties from
49+
||| the Typed Frame Router. This re-export makes them available
50+
||| to Groove consumers without importing the general module.
51+
public export
52+
grooveTransportSafe : (input : List Bits8) -> (output : List Bits8)
53+
-> (prf : input = output) -> input = output
54+
grooveTransportSafe = transportTransparency
55+
56+
||| The Groove proxy cannot be reversed to IPv6→IPv4.
57+
public export
58+
grooveNoReverse : (MkTranslation IPv6 IPv4 = grooveDirection) -> Void
59+
grooveNoReverse Refl impossible

‎groove-protocol/reference/groove-proxy/README.adoc‎

Lines changed: 148 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,148 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
3+
= Groove Proxy — IPv4→IPv6 Frame-Level Translation
4+
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
5+
:toc:
6+
7+
== Overview
8+
9+
The Groove Proxy is a specialisation of the
10+
link:https://github.com/hyperpolymath/proven-servers[Typed Frame Router]
11+
(proven-servers core primitive) for the specific case of IPv4→IPv6 frame
12+
translation on the loopback interface.
13+
14+
It is the reference implementation of Section 7.5 of the
15+
link:../../spec/TRANSPORT.adoc[Groove Transport Specification].
16+
17+
== Relationship to Typed Frame Router
18+
19+
[source]
20+
----
21+
proven-servers/core/proven-typed-frame-router/
22+
│
23+
│ General primitive: any frame translation with formal proofs
24+
│ (IPv4↔IPv6, FibreChannel, iSCSI, InfiniBand, BLE, Raw)
25+
│
26+
└─── groove-protocol/reference/groove-proxy/
27+
│
28+
│ Specific instance: IPv4→IPv6 on loopback for Groove
29+
│ Configured with: source=IPv4, target=IPv6, scope=localhost
30+
│
31+
└── This is an INSTANCE, not a fork.
32+
It imports the general primitive and specialises it.
33+
----
34+
35+
The Typed Frame Router provides:
36+
37+
- Idris2 ABI with 4 formal proofs (transport transparency, bounded memory,
38+
direction safety, connection liveness)
39+
- Zig FFI with zero-copy splice(2) on Linux
40+
- State machine with 7 valid transitions and impossibility proofs
41+
- C-compatible headers for any-language consumption
42+
43+
The Groove Proxy adds:
44+
45+
- Groove-specific configuration (default ports 6460-6500)
46+
- Integration with the Groove discovery protocol (`/.well-known/groove`)
47+
- IPv4 sunset headers (`Groove-Upgrade-To: ipv6`)
48+
- Provenance attestation via VeriSimDB (when grooved)
49+
50+
== Usage
51+
52+
=== As a Standalone Service
53+
54+
[source,bash]
55+
----
56+
# Start the groove proxy: accepts IPv4 on 6473, forwards to IPv6 [::1]:6473
57+
groove-proxy --ipv4-port 6473 --ipv6-port 6473
58+
----
59+
60+
=== As a Library (from Zig)
61+
62+
[source,zig]
63+
----
64+
const tfr = @import("typed_frame_router");
65+
66+
// Configure for Groove IPv4→IPv6 translation
67+
var router = try tfr.init(.{
68+
.source = .{ .family = .ipv4, .addr = "127.0.0.1", .port = 6473 },
69+
.target = .{ .family = .ipv6, .addr = "::1", .port = 6473 },
70+
.splice_mode = .auto, // kernel splice on Linux, userspace fallback elsewhere
71+
});
72+
defer router.deinit();
73+
74+
try router.run(); // Blocks, accepting and splicing connections
75+
----
76+
77+
=== As a Library (from Idris2)
78+
79+
[source,idris]
80+
----
81+
import TypedFrameRouterABI
82+
83+
-- Start the Groove proxy with proven safety
84+
main : IO ()
85+
main = do
86+
handle <- primIO $ typed_frame_router_start "127.0.0.1" 6473 "::1" 6473
87+
-- handle is linear: MUST be consumed by typed_frame_router_stop
88+
putStrLn "Groove proxy running: IPv4:6473 → [::1]:6473"
89+
-- ... wait for shutdown signal ...
90+
primIO $ typed_frame_router_stop handle
91+
----
92+
93+
== Formal Guarantees
94+
95+
Inherited from Typed Frame Router (proven in Idris2):
96+
97+
[cols="1,3"]
98+
|===
99+
| Property | What It Proves
100+
101+
| Transport Transparency
102+
| Every byte entering on IPv4 exits identically on IPv6. No corruption,
103+
no reordering, no duplication, no loss.
104+
105+
| Bounded Memory
106+
| The proxy uses at most 4,096 bytes of userspace buffer per connection.
107+
In kernel splice mode, userspace memory usage is zero.
108+
109+
| Direction Safety
110+
| The translation is always IPv4→IPv6. The type system makes it
111+
impossible to construct a reverse (IPv6→IPv4) proxy through this
112+
interface.
113+
114+
| Connection Liveness
115+
| Every connection that enters the Splicing state will eventually reach
116+
the Closed state. No connection can get stuck.
117+
|===
118+
119+
== Configuration for Groove
120+
121+
The default configuration matches the Groove Protocol defaults:
122+
123+
[cols="1,1,2"]
124+
|===
125+
| Parameter | Default | Notes
126+
127+
| IPv4 bind address | `127.0.0.1` | Loopback only (LAN requires explicit opt-in)
128+
| IPv4 port | Same as target | Mirrors the groove service port
129+
| IPv6 target address | `::1` | IPv6 loopback
130+
| IPv6 port | Service port | The real groove service
131+
| Max connections | 64 | Per-proxy concurrent connection limit
132+
| Buffer size | 4096 | Only used in userspace copy mode
133+
|===
134+
135+
== Other Instances of Typed Frame Router
136+
137+
The Groove Proxy is one instance. The general Typed Frame Router supports:
138+
139+
[cols="2,3"]
140+
|===
141+
| Instance | Translation
142+
143+
| **Groove Proxy** | IPv4 → IPv6 (this document)
144+
| **SAN Bridge** | iSCSI ↔ Fibre Channel (storage network translation)
145+
| **BLE Gateway** | Bluetooth LE → IPv6 (IoT device bridging)
146+
| **Avow LAN** | Raw frames → validated frames (network-level integrity)
147+
| **InfiniBand Proxy** | IB → IPv6 (HPC to standard networking)
148+
|===

0 commit comments

Comments
 (0)