1module Runtime.NativeRegionFrame
2
3import Compiler.Planning.RegionFrame
4import Runtime.RegionFrame
5import Runtime.NativeSocketPlan
6import Runtime.NativeMemoryPlan
7import Runtime.NativeMemoryRoutine
8import Runtime.NativeWordArithmetic
9import Runtime.NativeWordDigest
10import Runtime.NativePhysicalProgram
11import Runtime.NativeLaunchRecipeLoad
12import Model.Word64
13import Std.Natural
14
15-- Endpoint-local ownership: validated means verified bytes in host staging.
16-- It is not GPU visibility. Device upload/fences belong to the target session.
17-- A layout is initialized once. Completed rounds advance explicitly; replacing
18-- a live session with another epoch remains the caller's admission obligation.
19family NativeFramePhase : Type 0
20constructor NativeFrameUnissued
21constructor NativeFrameActive
22constructor NativeFrameValidated
23constructor NativeFrameConsumed
24constructor NativeFrameSent
25
26end-family
27
28-- Rearming cannot accept an arbitrary phase such as Active or Validated.
29family NativeFrameTerminal : Type 0
30constructor NativeFrameSendComplete
31constructor NativeFrameConsumeComplete
32
33end-family
34
35def nativeFramePhaseCode =
36 (lambda unrestricted phase : (family NativeFramePhase) .
37 (eliminate
38 NativeFramePhase
39 (lambda unrestricted p : (family NativeFramePhase) . Nat)
40 phase
41 (branch NativeFrameUnissued . 0)
42 (branch NativeFrameActive . 1)
43 (branch NativeFrameValidated . 2)
44 (branch NativeFrameConsumed . 3)
45 (branch NativeFrameSent . 4)))
46
47def frameNativeState =
48 nativeMemoryState
49
50def frameNativeLoad =
51 nativeMemoryLoad
52
53def frameNativeCopy =
54 nativeMemoryCopyPayload
55
56def frameNativePhase =
57 (lambda unrestricted layout : (family RegionFrameLayout) .
58 (lambda unrestricted phase : (family NativeFramePhase) .
59 (nativeLaunchRecipeCommand
60 (constructor
61 NativePhysicalOperation
62 NativePhysicalStoreWord64
63 (frameNativeState (framePhaseAt layout))
64 (nativeLaunchRecipeImmediate (nativeFramePhaseCode phase)))
65 b"frame-phase")))
66
67def frameNativeRequirePhase =
68 (lambda unrestricted layout : (family RegionFrameLayout) .
69 (lambda unrestricted phase : (family NativeFramePhase) .
70 (nativeLaunchRecipeAssertEqual
71 (frameNativeLoad (framePhaseAt layout))
72 (nativeLaunchRecipeImmediate (nativeFramePhaseCode phase))
73 b"frame-phase-mismatch")))
74
75def nativeFrameInitialize =
76 (lambda unrestricted layout : (family RegionFrameLayout) .
77 (lambda unrestricted tail : (family NativePhysicalCommands) .
78 (frameNativeCopy
79 (frameExpectedAt layout)
80 (frameHeader layout)
81 (frameNativePhase layout (constructor NativeFramePhase NativeFrameUnissued) tail))))
82
83-- Resume initializes a fresh slot from admitted runtime state. It does not
84-- authorize reinitializing a live slot or choosing a peer-supplied epoch.
85def nativeFrameInitializeRound =
86 (lambda unrestricted layout : (family RegionFrameLayout) .
87 (lambda unrestricted epoch : (family NativePhysicalOperand) .
88 (lambda unrestricted version : (family NativePhysicalOperand) .
89 (lambda unrestricted tail : (family NativePhysicalCommands) .
90 (nativeFrameInitialize
91 layout
92 (nativeLaunchRecipeCommand
93 (constructor
94 NativePhysicalOperation
95 NativePhysicalStoreWord64
96 (frameNativeState (frameExpectedEpochAt layout))
97 epoch)
98 b"frame-initialize-epoch"
99 (nativeLaunchRecipeCommand
100 (constructor
101 NativePhysicalOperation
102 NativePhysicalStoreWord64
103 (frameNativeState (frameExpectedVersionAt layout))
104 version)
105 b"frame-initialize-version"
106 tail)))))))
107
108def nativeFrameAdvance =
109 (lambda unrestricted layout : (family RegionFrameLayout) .
110 (lambda unrestricted terminal : (family NativeFrameTerminal) .
111 (lambda unrestricted slot : Nat .
112 (lambda unrestricted tail : (family NativePhysicalCommands) .
113 (frameNativeRequirePhase
114 layout
115 (eliminate
116 NativeFrameTerminal
117 (lambda unrestricted current : (family NativeFrameTerminal) .
118 (family NativeFramePhase))
119 terminal
120 (branch NativeFrameSendComplete . (constructor NativeFramePhase NativeFrameSent))
121 (branch
122 NativeFrameConsumeComplete
123 .
124 (constructor NativeFramePhase NativeFrameConsumed)))
125 (nativeCheckedWordAdd
126 (frameNativeState (frameExpectedVersionAt layout))
127 (frameNativeLoad (frameExpectedVersionAt layout))
128 (nativeLaunchRecipeImmediate 1)
129 slot
130 b"frame-version-overflow"
131 (frameNativePhase layout (constructor NativeFramePhase NativeFrameUnissued) tail)))))))
132
133-- Copy the current expected header, including its runtime round. Recopying
134-- the static layout header here would silently retransmit the first version.
135def frameNativeCopyHeader =
136 (lambda unrestricted layout : (family RegionFrameLayout) .
137 (lambda unrestricted slot : Nat .
138 (nativeMemoryCopyOperands
139 (frameNativeState (frameHeaderAt layout))
140 (frameNativeState (frameExpectedAt layout))
141 (bytes-length (frameHeader layout))
142 slot
143 b"frame-header-copy")))
144
145def frameNativeCompare =
146 nativeMemoryCompareRegions
147
148def frameNativeHash =
149 (lambda unrestricted layout : (family RegionFrameLayout) .
150 (lambda unrestricted slot : Nat .
151 (lambda unrestricted tail : (family NativePhysicalCommands) .
152 (frameNativeCopy
153 (framePaddingAt layout)
154 (framePadding layout)
155 (nativeLaunchRecipeCommand
156 (constructor
157 NativePhysicalOperation
158 NativePhysicalMachineRoutine
159 nativeWordDigestRoutine
160 (constructor
161 NativePhysicalArguments
162 NativePhysicalArgumentsValue
163 (frameNativeState (frameHeaderAt layout))
164 (nativeLaunchRecipeImmediate (frameBlockCount layout))
165 (frameNativeState (frameComputedAt layout))
166 (nativeLaunchRecipeImmediate 0)
167 (nativeLaunchRecipeImmediate 0)
168 (frameNativeState (frameWorkAt layout)))
169 (nativeLaunchRecipeStore slot))
170 b"frame-hash"
171 (nativeLaunchRecipeAssertEqual
172 (nativeLaunchRecipeSlotValue slot)
173 (nativeLaunchRecipeImmediate regionFrameDigestBytes)
174 b"frame-hash-count"
175 tail))))))
176
177def frameNativeIO =
178 (lambda unrestricted send : Nat .
179 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
180 (lambda unrestricted offset : Nat .
181 (lambda unrestricted extent : Nat .
182 (lambda unrestricted timeout : (family NativePhysicalOperand) .
183 (lambda unrestricted attempts : (family NativePhysicalOperand) .
184 (lambda unrestricted slot : Nat .
185 (lambda unrestricted tail : (family NativePhysicalCommands) .
186 (nativeLaunchRecipeCommand
187 (nat-eliminate
188 (lambda unrestricted n : Nat . (family NativePhysicalOperation))
189 (nativeSocketRead
190 descriptor
191 (frameNativeState offset)
192 (nativeLaunchRecipeImmediate extent)
193 timeout
194 attempts
195 (nativeLaunchRecipeStore slot))
196 (lambda unrestricted n : Nat .
197 (lambda unrestricted ignored : (family NativePhysicalOperation) .
198 (nativeSocketWrite
199 descriptor
200 (frameNativeState offset)
201 (nativeLaunchRecipeImmediate extent)
202 timeout
203 attempts
204 (nativeLaunchRecipeStore slot))))
205 send)
206 b"frame-stream"
207 (nativeLaunchRecipeAssertEqual
208 (nativeLaunchRecipeSlotValue slot)
209 (nativeLaunchRecipeImmediate extent)
210 b"frame-stream-count"
211 tail))))))))))
212
213-- Read/compare the locally known header before any body read. The trailer
214-- has its own region, so digest padding cannot destroy the peer's claim.
215-- Every failure is fatal to this stream; partial bytes are never consumed.
216def nativeFrameReceive =
217 (lambda unrestricted layout : (family RegionFrameLayout) .
218 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
219 (lambda unrestricted timeout : (family NativePhysicalOperand) .
220 (lambda unrestricted attempts : (family NativePhysicalOperand) .
221 (lambda unrestricted slot : Nat .
222 (lambda unrestricted tail : (family NativePhysicalCommands) .
223 (frameNativeRequirePhase
224 layout
225 (constructor NativeFramePhase NativeFrameUnissued)
226 (frameNativePhase
227 layout
228 (constructor NativeFramePhase NativeFrameActive)
229 (frameNativeIO
230 0
231 descriptor
232 (frameHeaderAt layout)
233 (bytes-length (frameHeader layout))
234 timeout
235 attempts
236 slot
237 (frameNativeCompare
238 (frameHeaderAt layout)
239 (frameExpectedAt layout)
240 (bytes-length (frameHeader layout))
241 slot
242 b"frame-header-mismatch"
243 (frameNativeIO
244 0
245 descriptor
246 (framePayloadAt layout)
247 (framePayloadBytes layout)
248 timeout
249 attempts
250 slot
251 (frameNativeIO
252 0
253 descriptor
254 (frameReceivedAt layout)
255 regionFrameDigestBytes
256 timeout
257 attempts
258 slot
259 (frameNativeHash
260 layout
261 slot
262 (frameNativeCompare
263 (frameComputedAt layout)
264 (frameReceivedAt layout)
265 regionFrameDigestBytes
266 slot
267 b"frame-digest-mismatch"
268 (frameNativePhase
269 layout
270 (constructor NativeFramePhase NativeFrameValidated)
271 tail)))))))))))))))
272
273-- The producer owns the payload and may fill it before this fragment. A
274-- complete socket write releases this local source; it is not a peer ACK.
275def nativeFrameSend =
276 (lambda unrestricted layout : (family RegionFrameLayout) .
277 (lambda unrestricted descriptor : (family NativePhysicalOperand) .
278 (lambda unrestricted timeout : (family NativePhysicalOperand) .
279 (lambda unrestricted attempts : (family NativePhysicalOperand) .
280 (lambda unrestricted slot : Nat .
281 (lambda unrestricted tail : (family NativePhysicalCommands) .
282 (frameNativeRequirePhase
283 layout
284 (constructor NativeFramePhase NativeFrameUnissued)
285 (frameNativePhase
286 layout
287 (constructor NativeFramePhase NativeFrameActive)
288 (frameNativeCopyHeader
289 layout
290 slot
291 (frameNativeHash
292 layout
293 slot
294 (frameNativeIO
295 1
296 descriptor
297 (frameHeaderAt layout)
298 (frameContentBytes layout)
299 timeout
300 attempts
301 slot
302 (frameNativeIO
303 1
304 descriptor
305 (frameComputedAt layout)
306 regionFrameDigestBytes
307 timeout
308 attempts
309 slot
310 (frameNativePhase
311 layout
312 (constructor NativeFramePhase NativeFrameSent)
313 tail)))))))))))))
314
315def nativeFrameConsume =
316 (lambda unrestricted layout : (family RegionFrameLayout) .
317 (lambda unrestricted tail : (family NativePhysicalCommands) .
318 (frameNativeRequirePhase
319 layout
320 (constructor NativeFramePhase NativeFrameValidated)
321 (frameNativePhase layout (constructor NativeFramePhase NativeFrameConsumed) tail))))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.