1module Runtime.NativePeerEndpoint
2
3import Compiler.Planning.RegionFrame
4import Runtime.NativeRegionFrame
5import Runtime.NativePhysicalProgram
6import Runtime.NativeLaunchRecipeLoad
7import Runtime.NativeMemoryPlan
8import Runtime.NativeSocketPlan
9import Runtime.SocketAddress
10import Runtime.WordDigest
11import Std.List
12import Data.Bytes
13import Std.Natural
14
15-- ---- edges ----
16-- A participant's sessions are its incident edges, in ascending peer order.
17-- Each edge has one IPv4 address. The lower role of an edge binds and listens
18-- on it; the higher role connects to it. Every edge owns a listener slot and
19-- a connection slot, so a peer's descriptor is a static slot, never a
20-- runtime lookup, and the protocol layer can name it by peer role.
21--
22-- Establishment order: copy every address, bind and listen on every edge to
23-- a higher peer, announce those ports (two bytes each, big-endian, edge
24-- order), then establish edges in order: connect to each lower peer, accept
25-- each higher peer and close that listener. Launching participants in role
26-- order, each after the previous announced, therefore never connects to an
27-- absent listener, and no participant accepts before it has finished its own
28-- connects. A star (role 0 listens for every other role) and a two-role pair
29-- are instances; with one edge this is exactly the earlier two-role setup.
30-- Fixed membership: the addresses are compiled in, and a missing or late
31-- peer exhausts the bounded accept/connect budgets and aborts.
32family NativePeerEdge : Type 0
33constructor NativePeerEdgeOf
34field unrestricted nativePeerEdgePeer : Nat
35field unrestricted nativePeerEdgeAddress : Bytes
36
37end-family
38
39-- Endpoint policy shared by learning compositions: a participant's incident
40-- edges (two-role pairs are the one-edge case). It owns their result slots,
41-- bounded establishment/IO and listener reporting; it does not define a
42-- learning equation, membership authentication or device fallback.
43def nativePeerWordBytes : Nat =
44 digestAddressBytes
45
46def nativePeerIOWithBudget =
47 (lambda unrestricted timeout : (family NativePhysicalOperand) .
48 (lambda unrestricted attempts : (family NativePhysicalOperand) .
49 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
50 (lambda unrestricted send : Nat .
51 (lambda unrestricted layout : (family RegionFrameLayout) .
52 (lambda unrestricted tail : (family NativePhysicalCommands) .
53 (nat-eliminate
54 (lambda unrestricted n : Nat . (family NativePhysicalCommands))
55 (nativeFrameReceive layout descriptor timeout attempts 0 tail)
56 (lambda unrestricted n : Nat .
57 (lambda unrestricted ignored : (family NativePhysicalCommands) .
58 (nativeFrameSend layout descriptor timeout attempts 0 tail)))
59 send)))))))
60
61-- These are explicit fixed-membership policy defaults, not measured device
62-- latency bounds. A caller waiting for durable publication chooses its own
63-- larger admitted budget through nativePeerIOWithBudget.
64def nativePeerIOAttempts : Nat =
65 4096
66
67def nativePeerIO =
68 (nativePeerIOWithBudget
69 (nativeLaunchRecipeImmediate 1000)
70 (nativeLaunchRecipeImmediate nativePeerIOAttempts))
71
72def nativePeerScratchSlot : Nat =
73 0
74
75def nativePeerListenerSlot =
76 (naturalAdd nativePeerScratchSlot 1)
77
78def nativePeerConnectionSlot =
79 (naturalAdd nativePeerListenerSlot 1)
80
81def nativePeerEndpointSlots =
82 (naturalAdd nativePeerConnectionSlot 1)
83
84def nativePeerEndpointLengthAt =
85 (lambda unrestricted base : Nat . (naturalAdd base linuxIPv4SocketAddressBytes))
86
87def nativePeerEndpointEnd =
88 (lambda unrestricted base : Nat .
89 (naturalAdd (nativePeerEndpointLengthAt base) nativePeerWordBytes))
90
91def nativePeerPortWrite =
92 (lambda unrestricted base : Nat .
93 (lambda unrestricted tail : (family NativePhysicalCommands) .
94 (nativeLaunchRecipeCommand
95 (nativeSocketSystemCall
96 1
97 (nativeLaunchRecipeArguments
98 (nativeLaunchRecipeImmediate 1)
99 (frameNativeState (naturalAdd base linuxIPv4PortAt))
100 (nativeLaunchRecipeImmediate linuxIPv4PortBytes)
101 (nativeLaunchRecipeImmediate 0))
102 (nativeLaunchRecipeStore nativePeerScratchSlot))
103 b"peer-listening-port"
104 (nativeLaunchRecipeAssertEqual
105 (nativeLaunchRecipeSlotValue nativePeerScratchSlot)
106 (nativeLaunchRecipeImmediate linuxIPv4PortBytes)
107 b"peer-listening-port-count"
108 tail))))
109
110def nativePeerEdgePeerOf =
111 (lambda unrestricted edge : (family NativePeerEdge) .
112 (eliminate
113 NativePeerEdge
114 (lambda unrestricted current : (family NativePeerEdge) . Nat)
115 edge
116 (branch NativePeerEdgeOf peer address . peer)))
117
118def nativePeerEdgeAddressOf =
119 (lambda unrestricted edge : (family NativePeerEdge) .
120 (eliminate
121 NativePeerEdge
122 (lambda unrestricted current : (family NativePeerEdge) . Bytes)
123 edge
124 (branch NativePeerEdgeOf peer address . address)))
125
126def nativePeerEdgeListenerSlot =
127 (lambda unrestricted index : Nat . (naturalAdd nativePeerListenerSlot (naturalMultiply 2 index)))
128
129def nativePeerEdgeConnectionSlot =
130 (lambda unrestricted index : Nat .
131 (naturalAdd nativePeerConnectionSlot (naturalMultiply 2 index)))
132
133def nativePeerEdgeSlots =
134 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
135 (nativePeerEdgeListenerSlot (stdListLength (family NativePeerEdge) edges)))
136
137-- One address entry: the socket address followed by its socklen word.
138def nativePeerEdgeEntryBytes =
139 (nativePeerEndpointEnd 0)
140
141def nativePeerEdgeAddressAt =
142 (lambda unrestricted base : Nat .
143 (lambda unrestricted index : Nat .
144 (naturalAdd base (naturalMultiply index nativePeerEdgeEntryBytes))))
145
146def nativePeerEdgesEnd =
147 (lambda unrestricted base : Nat .
148 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
149 (nativePeerEdgeAddressAt base (stdListLength (family NativePeerEdge) edges))))
150
151-- Edges in order with their positions, for folds that need the slot index.
152def nativePeerEdgesFold =
153 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
154 (lambda unrestricted step : (pi unrestricted index : Nat . (pi unrestricted edge : (family NativePeerEdge) . (pi unrestricted rest : (family NativePhysicalCommands) . (family NativePhysicalCommands)))) .
155 (lambda unrestricted tail : (family NativePhysicalCommands) .
156 (stdListFold
157 (family NativePeerEdge)
158 (pi unrestricted index : Nat . (family NativePhysicalCommands))
159 (lambda unrestricted edge : (family NativePeerEdge) .
160 (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
161 (lambda unrestricted index : Nat . (step index edge (next (succ index))))))
162 (lambda unrestricted index : Nat . tail)
163 edges
164 0))))
165
166def nativePeerEdgeListens =
167 (lambda unrestricted role : Nat .
168 (lambda unrestricted edge : (family NativePeerEdge) .
169 (naturalLess role (nativePeerEdgePeerOf edge))))
170
171def nativePeerEdgeWhenListening =
172 (lambda unrestricted role : Nat .
173 (lambda unrestricted edge : (family NativePeerEdge) .
174 (lambda unrestricted listening : (family NativePhysicalCommands) .
175 (lambda unrestricted connecting : (family NativePhysicalCommands) .
176 (nat-eliminate
177 (lambda unrestricted current : Nat . (family NativePhysicalCommands))
178 connecting
179 (lambda unrestricted previous : Nat .
180 (lambda unrestricted ignored : (family NativePhysicalCommands) . listening))
181 (nativePeerEdgeListens role edge))))))
182
183def nativePeerEdgeListen =
184 (lambda unrestricted at : Nat .
185 (lambda unrestricted index : Nat .
186 (lambda unrestricted tail : (family NativePhysicalCommands) .
187 (nativeSocketOpenIPv4
188 (nativePeerEdgeListenerSlot index)
189 nativePeerScratchSlot
190 (nativeSocketBindListener
191 (nativeLaunchRecipeSlotValue (nativePeerEdgeListenerSlot index))
192 (frameNativeState at)
193 (nativeLaunchRecipeImmediate 1)
194 nativePeerScratchSlot
195 (nativeMemoryStoreWord64
196 b"peer-state"
197 (nativePeerEndpointLengthAt at)
198 (nativeLaunchRecipeImmediate linuxIPv4SocketAddressBytes)
199 (nativeSocketRequireZero
200 (nativeSocketLocalAddress
201 (nativeLaunchRecipeSlotValue (nativePeerEdgeListenerSlot index))
202 (frameNativeState at)
203 (frameNativeState (nativePeerEndpointLengthAt at))
204 (nativeLaunchRecipeStore nativePeerScratchSlot))
205 nativePeerScratchSlot
206 b"peer-local-address"
207 (nativeLaunchRecipeAssertEqual
208 (frameNativeLoad (nativePeerEndpointLengthAt at))
209 (nativeLaunchRecipeImmediate linuxIPv4SocketAddressBytes)
210 b"peer-local-address-extent"
211 tail))))))))
212
213def nativePeerEdgeEstablish =
214 (lambda unrestricted role : Nat .
215 (lambda unrestricted base : Nat .
216 (lambda unrestricted index : Nat .
217 (lambda unrestricted edge : (family NativePeerEdge) .
218 (lambda unrestricted tail : (family NativePhysicalCommands) .
219 (nativePeerEdgeWhenListening
220 role
221 edge
222 (nativeSocketAcceptChecked
223 (nativeLaunchRecipeSlotValue (nativePeerEdgeListenerSlot index))
224 (nativeLaunchRecipeImmediate 30000)
225 (nativeLaunchRecipeImmediate 64)
226 (nativePeerEdgeConnectionSlot index)
227 nativePeerScratchSlot
228 (nativeSocketCloseChecked
229 (nativeLaunchRecipeSlotValue (nativePeerEdgeListenerSlot index))
230 nativePeerScratchSlot
231 tail))
232 (nativeSocketOpenIPv4
233 (nativePeerEdgeConnectionSlot index)
234 nativePeerScratchSlot
235 (nativeSocketConnectChecked
236 (nativeLaunchRecipeSlotValue (nativePeerEdgeConnectionSlot index))
237 (frameNativeState (nativePeerEdgeAddressAt base index))
238 (nativeLaunchRecipeImmediate 5000)
239 (nativeLaunchRecipeImmediate 64)
240 nativePeerScratchSlot
241 tail))))))))
242
243def nativePeerEdgeSetup =
244 (lambda unrestricted role : Nat .
245 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
246 (lambda unrestricted base : Nat .
247 (lambda unrestricted tail : (family NativePhysicalCommands) .
248 (nativePeerEdgesFold
249 edges
250 (lambda unrestricted index : Nat .
251 (lambda unrestricted edge : (family NativePeerEdge) .
252 (lambda unrestricted rest : (family NativePhysicalCommands) .
253 (frameNativeCopy
254 (nativePeerEdgeAddressAt base index)
255 (nativePeerEdgeAddressOf edge)
256 rest))))
257 (nativePeerEdgesFold
258 edges
259 (lambda unrestricted index : Nat .
260 (lambda unrestricted edge : (family NativePeerEdge) .
261 (lambda unrestricted rest : (family NativePhysicalCommands) .
262 (nativePeerEdgeWhenListening
263 role
264 edge
265 (nativePeerEdgeListen (nativePeerEdgeAddressAt base index) index rest)
266 rest))))
267 (nativePeerEdgesFold
268 edges
269 (lambda unrestricted index : Nat .
270 (lambda unrestricted edge : (family NativePeerEdge) .
271 (lambda unrestricted rest : (family NativePhysicalCommands) .
272 (nativePeerEdgeWhenListening
273 role
274 edge
275 (nativePeerPortWrite (nativePeerEdgeAddressAt base index) rest)
276 rest))))
277 (nativePeerEdgesFold
278 edges
279 (lambda unrestricted index : Nat .
280 (lambda unrestricted edge : (family NativePeerEdge) .
281 (lambda unrestricted rest : (family NativePhysicalCommands) .
282 (nativePeerEdgeEstablish role base index edge rest))))
283 tail))))))))
284
285-- The connection slot of the edge to `peer`, or the scratch slot (which no
286-- edge owns) when the participant has no such edge; admission of the caller's
287-- topology must refuse that case before commands are generated.
288def nativePeerEdgeConnectionTo =
289 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
290 (lambda unrestricted peer : Nat .
291 (stdListFold
292 (family NativePeerEdge)
293 (pi unrestricted index : Nat . Nat)
294 (lambda unrestricted edge : (family NativePeerEdge) .
295 (lambda unrestricted next : (pi unrestricted index : Nat . Nat) .
296 (lambda unrestricted index : Nat .
297 (naturalSelect
298 (naturalEqual (nativePeerEdgePeerOf edge) peer)
299 (nativePeerEdgeConnectionSlot index)
300 (next (succ index))))))
301 (lambda unrestricted index : Nat . nativePeerScratchSlot)
302 edges
303 0)))
304
305-- Edges are admitted when their peers are distinct, strictly ascending,
306-- differ from this role, and every address is one IPv4 socket address.
307def nativePeerEdgesAdmitted =
308 (lambda unrestricted role : Nat .
309 (lambda unrestricted edges : (family StdList (family NativePeerEdge)) .
310 (stdListFold
311 (family NativePeerEdge)
312 (pi unrestricted floor : Nat . Nat)
313 (lambda unrestricted edge : (family NativePeerEdge) .
314 (lambda unrestricted next : (pi unrestricted floor : Nat . Nat) .
315 (lambda unrestricted floor : Nat .
316 (naturalAnd
317 (naturalLessOrEqual floor (nativePeerEdgePeerOf edge))
318 (naturalAnd
319 (naturalIsZero (naturalEqual role (nativePeerEdgePeerOf edge)))
320 (naturalAnd
321 (naturalEqual
322 (bytes-length (nativePeerEdgeAddressOf edge))
323 linuxIPv4SocketAddressBytes)
324 (next (succ (nativePeerEdgePeerOf edge)))))))))
325 (lambda unrestricted floor : Nat . 1)
326 edges
327 0)))
328
329-- A star centred on role 0: role 0 has an edge to every other role, in
330-- order, at `addresses`; every other role has one edge, to role 0, at its
331-- one address.
332def nativePeerStarEdges =
333 (lambda unrestricted role : Nat .
334 (lambda unrestricted addresses : (family StdList Bytes) .
335 (stdListFold
336 Bytes
337 (pi unrestricted index : Nat . (family StdList (family NativePeerEdge)))
338 (lambda unrestricted address : Bytes .
339 (lambda unrestricted next : (pi unrestricted index : Nat . (family StdList (family NativePeerEdge))) .
340 (lambda unrestricted index : Nat .
341 (constructor
342 StdList
343 StdListCons
344 (family NativePeerEdge)
345 (constructor
346 NativePeerEdge
347 NativePeerEdgeOf
348 (naturalSelect (naturalIsZero role) (succ index) 0)
349 address)
350 (next (succ index))))))
351 (lambda unrestricted index : Nat . (constructor StdList StdListEmpty (family NativePeerEdge)))
352 addresses
353 0)))
354
355-- A star of `owners` admits owner 0 with one address per other owner and
356-- every other owner with exactly one address, all admitted edges.
357def nativePeerStarAdmitted =
358 (lambda unrestricted owners : Nat .
359 (lambda unrestricted role : Nat .
360 (lambda unrestricted addresses : (family StdList Bytes) .
361 (naturalAnd
362 (naturalLess role owners)
363 (naturalAnd
364 (naturalEqual
365 (stdListLength Bytes addresses)
366 (naturalSelect (naturalIsZero role) (naturalPredecessor owners) 1))
367 (nativePeerEdgesAdmitted role (nativePeerStarEdges role addresses)))))))
368
369-- The two-role pair: role 0 listens for role 1 at `address`, role 1
370-- connects to it. Same commands, slots and state as one admitted edge.
371def nativePeerEdgesOfPair =
372 (lambda unrestricted worker : Nat .
373 (lambda unrestricted address : Bytes .
374 (constructor
375 StdList
376 StdListCons
377 (family NativePeerEdge)
378 (constructor
379 NativePeerEdge
380 NativePeerEdgeOf
381 (naturalSelect (naturalIsZero worker) 1 0)
382 address)
383 (constructor StdList StdListEmpty (family NativePeerEdge)))))
384
385def nativePeerSetup =
386 (lambda unrestricted worker : Nat .
387 (lambda unrestricted address : Bytes .
388 (lambda unrestricted base : Nat .
389 (lambda unrestricted tail : (family NativePhysicalCommands) .
390 (nativePeerEdgeSetup
391 (naturalSelect (naturalIsZero worker) 0 1)
392 (nativePeerEdgesOfPair worker address)
393 base
394 tail)))))
395
396def nativePeerByRole =
397 (lambda unrestricted worker : Nat .
398 (lambda unrestricted coordinator : (family NativePhysicalCommands) .
399 (lambda unrestricted participant : (family NativePhysicalCommands) .
400 (nat-eliminate
401 (lambda unrestricted role : Nat . (family NativePhysicalCommands))
402 coordinator
403 (lambda unrestricted previous : Nat .
404 (lambda unrestricted ignored : (family NativePhysicalCommands) . participant))
405 worker))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.