1module Runtime.NativeSocketPlan
2
3import Runtime.NativeDescriptor
4import Runtime.NativeSocketRoutine
5import Runtime.NativeSocketEndpoint
6import Runtime.SocketAddress
7import Runtime.NativePhysicalProgram
8import Runtime.NativeLaunchRecipeLoad
9import Model.Word64
10import Std.Natural
11
12-- Target-local lowering of a bounded stream operation into the existing
13-- native program. Admission/liveness owns the buffer extent. The caller must
14-- assert the exact count before publishing destination visibility. Failures
15-- can leave a partial prefix and require abandonment of this edge/session.
16-- This declares the Linux x86-64 ABI. AArch64 HostLowering maps connected
17-- stream IO to its native realization; endpoint establishment still requires
18-- its own target support and is refused when that lowering is unavailable.
19def nativeSocketOperation =
20 (lambda unrestricted code : Bytes .
21 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
22 (lambda unrestricted buffer : (family NativePhysicalOperand) .
23 (lambda unrestricted extent : (family NativePhysicalOperand) .
24 (lambda unrestricted timeoutMilliseconds : (family NativePhysicalOperand) .
25 (lambda unrestricted attempts : (family NativePhysicalOperand) .
26 (lambda unrestricted result : (family NativePhysicalResultBinding) .
27 (constructor
28 NativePhysicalOperation
29 NativePhysicalMachineRoutine
30 code
31 (constructor
32 NativePhysicalArguments
33 NativePhysicalArgumentsValue
34 descriptor
35 buffer
36 extent
37 timeoutMilliseconds
38 attempts
39 (constructor
40 NativePhysicalOperand
41 NativePhysicalImmediate
42 (modelWord64FromNaturalTruncated 0)))
43 result))))))))
44
45def nativeSocketRead =
46 (nativeSocketOperation nativeSocketReadCode)
47
48def nativeSocketWrite =
49 (nativeSocketOperation nativeSocketWriteCode)
50
51-- Endpoint operations speak the same Linux x86-64 ABI as stream IO. The
52-- program owns every produced descriptor and must close it at session end.
53-- Creation/accept use NONBLOCK|CLOEXEC atomically; connect/accept also check
54-- NONBLOCK before entering a readiness race. Failure requires abandonment.
55def nativeSocketConnect =
56 (nativeSocketOperation nativeSocketConnectCode)
57
58def nativeSocketAccept =
59 (lambda unrestricted listener : (family NativePhysicalOperand) .
60 (lambda unrestricted timeout : (family NativePhysicalOperand) .
61 (lambda unrestricted attempts : (family NativePhysicalOperand) .
62 (nativeSocketOperation
63 nativeSocketAcceptCode
64 listener
65 (nativeLaunchRecipeImmediate 0)
66 (nativeLaunchRecipeImmediate 1)
67 timeout
68 attempts))))
69
70def nativeSocketDescriptorStatus =
71 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
72 (nativeSocketOperation
73 nativeSocketDescriptorStatusCode
74 descriptor
75 (nativeLaunchRecipeImmediate 0)
76 (nativeLaunchRecipeImmediate 0)
77 (nativeLaunchRecipeImmediate 0)
78 (nativeLaunchRecipeImmediate 0)))
79
80def nativeSocketSystemCall =
81 (lambda unrestricted number : Nat .
82 (lambda unrestricted arguments : (family NativePhysicalArguments) .
83 (lambda unrestricted result : (family NativePhysicalResultBinding) .
84 (constructor
85 NativePhysicalOperation
86 NativePhysicalSystemCall
87 (nativeLaunchRecipeImmediate number)
88 arguments
89 b""
90 result))))
91
92def nativeSocketCreateIPv4 =
93 (nativeSocketSystemCall
94 41
95 (nativeLaunchRecipeArguments
96 (nativeLaunchRecipeImmediate linuxIPv4Family)
97 (nativeLaunchRecipeImmediate (naturalAdd 1 nativeSocketEndpointFlags))
98 (nativeLaunchRecipeImmediate 0)
99 (nativeLaunchRecipeImmediate 0)))
100
101-- Explicit latency policy for small request/acknowledgment frames. Linux TCP
102-- may otherwise delay the separate digest write behind unacknowledged bytes.
103-- The option is per socket, never a host-wide network setting. The caller
104-- supplies a Linux int (0 or 1) at valueAddress and checks the syscall result.
105-- Linux UAPI: IPPROTO_TCP=6, TCP_NODELAY=1, sizeof(int)=4 on this ABI.
106-- https://man7.org/linux/man-pages/man7/tcp.7.html (TCP_NODELAY)
107-- https://man7.org/linux/man-pages/man2/setsockopt.2.html
108def nativeSocketNoDelay =
109 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
110 (lambda unrestricted valueAddress : (family NativePhysicalOperand) .
111 (nativeSocketSystemCall
112 54
113 (constructor
114 NativePhysicalArguments
115 NativePhysicalArgumentsValue
116 descriptor
117 (nativeLaunchRecipeImmediate 6)
118 (nativeLaunchRecipeImmediate 1)
119 valueAddress
120 (nativeLaunchRecipeImmediate 4)
121 (nativeLaunchRecipeImmediate 0)))))
122
123def nativeSocketBindIPv4 =
124 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
125 (lambda unrestricted address : (family NativePhysicalOperand) .
126 (nativeSocketSystemCall
127 49
128 (nativeLaunchRecipeArguments
129 descriptor
130 address
131 (nativeLaunchRecipeImmediate linuxIPv4SocketAddressBytes)
132 (nativeLaunchRecipeImmediate 0)))))
133
134def nativeSocketListen =
135 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
136 (lambda unrestricted backlog : (family NativePhysicalOperand) .
137 (nativeSocketSystemCall
138 50
139 (nativeLaunchRecipeArguments
140 descriptor
141 backlog
142 (nativeLaunchRecipeImmediate 0)
143 (nativeLaunchRecipeImmediate 0)))))
144
145def nativeSocketLocalAddress =
146 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
147 (lambda unrestricted address : (family NativePhysicalOperand) .
148 (lambda unrestricted lengthAddress : (family NativePhysicalOperand) .
149 (nativeSocketSystemCall
150 51
151 (nativeLaunchRecipeArguments
152 descriptor
153 address
154 lengthAddress
155 (nativeLaunchRecipeImmediate 0))))))
156
157def nativeSocketClose =
158 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
159 (nativeSocketSystemCall
160 3
161 (nativeLaunchRecipeArguments
162 descriptor
163 (nativeLaunchRecipeImmediate 0)
164 (nativeLaunchRecipeImmediate 0)
165 (nativeLaunchRecipeImmediate 0))))
166
167def nativeSocketRequireDescriptor =
168 nativeDescriptorRequire
169
170def nativeSocketRequireZero =
171 (lambda unrestricted operation : (family NativePhysicalOperation) .
172 (lambda unrestricted scratchSlot : Nat .
173 (lambda unrestricted error : Bytes .
174 (lambda unrestricted tail : (family NativePhysicalCommands) .
175 (nativeLaunchRecipeCommand
176 operation
177 error
178 (nativeLaunchRecipeAssertEqual
179 (nativeLaunchRecipeSlotValue scratchSlot)
180 (nativeLaunchRecipeImmediate 0)
181 error
182 tail))))))
183
184def nativeSocketOpenIPv4 =
185 (lambda unrestricted descriptorSlot : Nat .
186 (lambda unrestricted scratchSlot : Nat .
187 (lambda unrestricted tail : (family NativePhysicalCommands) .
188 (nativeLaunchRecipeCommand
189 (nativeSocketCreateIPv4 (nativeLaunchRecipeStore descriptorSlot))
190 b"socket-create"
191 (nativeSocketRequireDescriptor
192 (nativeLaunchRecipeSlotValue descriptorSlot)
193 scratchSlot
194 b"socket-create"
195 tail)))))
196
197def nativeSocketBindListener =
198 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
199 (lambda unrestricted address : (family NativePhysicalOperand) .
200 (lambda unrestricted backlog : (family NativePhysicalOperand) .
201 (lambda unrestricted scratchSlot : Nat .
202 (lambda unrestricted tail : (family NativePhysicalCommands) .
203 (nativeSocketRequireZero
204 (nativeSocketBindIPv4 descriptor address (nativeLaunchRecipeStore scratchSlot))
205 scratchSlot
206 b"socket-bind"
207 (nativeSocketRequireZero
208 (nativeSocketListen descriptor backlog (nativeLaunchRecipeStore scratchSlot))
209 scratchSlot
210 b"socket-listen"
211 tail)))))))
212
213def nativeSocketConnectChecked =
214 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
215 (lambda unrestricted address : (family NativePhysicalOperand) .
216 (lambda unrestricted timeout : (family NativePhysicalOperand) .
217 (lambda unrestricted attempts : (family NativePhysicalOperand) .
218 (lambda unrestricted scratchSlot : Nat .
219 (nativeSocketRequireZero
220 (nativeSocketConnect
221 descriptor
222 address
223 (nativeLaunchRecipeImmediate linuxIPv4SocketAddressBytes)
224 timeout
225 attempts
226 (nativeLaunchRecipeStore scratchSlot))
227 scratchSlot
228 b"socket-connect"))))))
229
230def nativeSocketAcceptChecked =
231 (lambda unrestricted listener : (family NativePhysicalOperand) .
232 (lambda unrestricted timeout : (family NativePhysicalOperand) .
233 (lambda unrestricted attempts : (family NativePhysicalOperand) .
234 (lambda unrestricted descriptorSlot : Nat .
235 (lambda unrestricted scratchSlot : Nat .
236 (lambda unrestricted tail : (family NativePhysicalCommands) .
237 (nativeLaunchRecipeCommand
238 (nativeSocketAccept
239 listener
240 timeout
241 attempts
242 (nativeLaunchRecipeStore descriptorSlot))
243 b"socket-accept"
244 (nativeSocketRequireDescriptor
245 (nativeLaunchRecipeSlotValue descriptorSlot)
246 scratchSlot
247 b"socket-accept"
248 tail))))))))
249
250def nativeSocketCloseChecked =
251 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
252 (lambda unrestricted scratchSlot : Nat .
253 (nativeSocketRequireZero
254 (nativeSocketClose descriptor (nativeLaunchRecipeStore scratchSlot))
255 scratchSlot
256 b"socket-close")))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.