1module Checkpoint.NativePeerPublication
2
3import Checkpoint.NativeRegions
4import Checkpoint.NativeEnvelope
5import Compiler.Planning.RegionFrame
6import Runtime.NativePhysicalProgram
7import Runtime.NativeLaunchRecipeLoad
8import Runtime.NativeMemoryPlan
9import Runtime.NativePeerEndpoint
10import Runtime.NativeRegionFrame
11import Representation.Partition
12import Runtime.ArenaCertificate
13import Std.Foundation
14import Model.Word64
15import Std.List
16import Std.Natural
17
18family NativeRegionPaths : Type 0
19constructor NativeRegionPathsOf
20field unrestricted nativeRegionFirstArgument : Nat
21field unrestricted nativeRegionPathCount : Nat
22
23end-family
24
25-- A star capture and durable publication strategy over owners 0..peers.
26-- State meaning, local computation, source placement and numerical policy
27-- belong to the caller. Owner 0 publishes: it prepares its own shards from
28-- its local state, then receives each other owner's captured state in turn
29-- over that owner's edge, checks that the agreed leading bytes (at least the
30-- (version, cursor, epoch) prefix) are identical to its own, and prepares
31-- that owner's shards from it. Only after
32-- every shard and the manifest are durable does it release each owner with
33-- the committed version; every owner, publisher included, completes only
34-- then. A missing, late or differently advanced owner publishes nothing.
35--
36-- Per-owner frames carry that owner's identity, so a capture received on the
37-- wrong edge fails its frame check. All capture frames share one storage
38-- region (and all committed frames another): they are used one owner at a
39-- time, so the publisher's frame storage does not grow with the owner count.
40family NativePeerRegionPublication : Type 0
41constructor NativePeerRegionPublicationOf
42field unrestricted peerPublicationCheckpoint : (family NativeRegionCheckpoint)
43-- owners other than the publisher
44field unrestricted peerPublicationPeers : Nat
45-- the frame carrying `owner`'s capture to the publisher, and the one releasing it
46field unrestricted peerPublicationCapture : (pi unrestricted owner : Nat . (family RegionFrameLayout))
47field unrestricted peerPublicationCommitted : (pi unrestricted owner : Nat . (family RegionFrameLayout))
48-- the connection slot to `peer` (Runtime.NativePeerEndpoint.nativePeerEdgeConnectionTo)
49field unrestricted peerPublicationConnection : (pi unrestricted peer : Nat . Nat)
50field unrestricted peerPublicationStateAt : Nat
51field unrestricted peerPublicationStateBytes : Nat
52-- the leading bytes of every owner's state that must equal the publisher's:
53-- at least the (version, cursor, epoch) capture prefix; a replicated learner
54-- names its whole replicated state, so diverged replicas publish nothing
55field unrestricted peerPublicationAgreedBytes : Nat
56-- which owner's state holds a shard, and the shard's byte offset in it
57field unrestricted peerPublicationOwner : (pi unrestricted shard : (family NativeRegionShard) . Nat)
58field unrestricted peerPublicationOffset : (pi unrestricted shard : (family NativeRegionShard) . Nat)
59field unrestricted peerPublicationPaths : (family NativeRegionPaths)
60
61end-family
62
63def nativeRegionPathFirst =
64 (lambda unrestricted paths : (family NativeRegionPaths) .
65 (eliminate
66 NativeRegionPaths
67 (lambda unrestricted current : (family NativeRegionPaths) . Nat)
68 paths
69 (branch NativeRegionPathsOf first count . first)))
70
71def nativeRegionPathCountOf =
72 (lambda unrestricted paths : (family NativeRegionPaths) .
73 (eliminate
74 NativeRegionPaths
75 (lambda unrestricted current : (family NativeRegionPaths) . Nat)
76 paths
77 (branch NativeRegionPathsOf first count . count)))
78
79def nativeRegionPathArgument =
80 (lambda unrestricted index : Nat .
81 (constructor
82 NativePhysicalOperand
83 NativePhysicalProcessArgument
84 (modelWord64FromNaturalTruncated index)))
85
86def nativeRegionInputShardBase =
87 (lambda unrestricted paths : (family NativeRegionPaths) . (succ (nativeRegionPathFirst paths)))
88
89def nativeRegionOutputShardBase =
90 (lambda unrestricted paths : (family NativeRegionPaths) .
91 (naturalAdd (nativeRegionInputShardBase paths) (nativeRegionPathCountOf paths)))
92
93def nativeRegionManifestCandidateIndex =
94 (lambda unrestricted paths : (family NativeRegionPaths) .
95 (naturalAdd
96 (nativeRegionOutputShardBase paths)
97 (naturalMultiply 2 (nativeRegionPathCountOf paths))))
98
99def nativeRegionManifestCommittedIndex =
100 (lambda unrestricted paths : (family NativeRegionPaths) .
101 (succ (nativeRegionManifestCandidateIndex paths)))
102
103def nativeRegionDirectoryIndex =
104 (lambda unrestricted paths : (family NativeRegionPaths) .
105 (succ (nativeRegionManifestCommittedIndex paths)))
106
107def nativeRegionShardPath =
108 (lambda unrestricted paths : (family NativeRegionPaths) .
109 (lambda unrestricted index : Nat .
110 (lambda unrestricted committed : Nat .
111 (nativeRegionPathArgument
112 (naturalAdd
113 (nativeRegionOutputShardBase paths)
114 (naturalAdd (naturalMultiply 2 index) committed))))))
115
116-- Publication may include several durable file syncs. It has its own bounded
117-- 30-second readiness policy, independent of ordinary learning-message waits.
118def nativePeerPublicationIO =
119 (nativePeerIOWithBudget
120 (nativeLaunchRecipeImmediate 30000)
121 (nativeLaunchRecipeImmediate nativePeerIOAttempts))
122
123-- Prepare the shards held by `owner`, each from `stateBase` plus its offset,
124-- keeping each shard's index for its paths. Shards are independent: each has
125-- its own checkpoint layout, so grouping them by owner preserves the plan.
126def nativeRegionPrepareOwner =
127 (lambda unrestricted plan : (family NativeRegionCheckpoint) .
128 (lambda unrestricted captureAt : Nat .
129 (lambda unrestricted ownerOf : (pi unrestricted shard : (family NativeRegionShard) . Nat) .
130 (lambda unrestricted offsetOf : (pi unrestricted shard : (family NativeRegionShard) . Nat) .
131 (lambda unrestricted owner : Nat .
132 (lambda unrestricted stateBase : Nat .
133 (lambda unrestricted paths : (family NativeRegionPaths) .
134 (lambda unrestricted tail : (family NativePhysicalCommands) .
135 (stdListFold
136 (family NativeRegionShard)
137 (pi unrestricted index : Nat . (family NativePhysicalCommands))
138 (lambda unrestricted shard : (family NativeRegionShard) .
139 (lambda unrestricted next : (pi unrestricted index : Nat . (family NativePhysicalCommands)) .
140 (lambda unrestricted index : Nat .
141 (nat-eliminate
142 (lambda unrestricted held : Nat . (family NativePhysicalCommands))
143 (next (succ index))
144 (lambda unrestricted previous : Nat .
145 (lambda unrestricted ignored : (family NativePhysicalCommands) .
146 (nativeRegionPrepareShard
147 shard
148 (nativeMemoryState captureAt)
149 (nativeMemoryState (naturalAdd stateBase (offsetOf shard)))
150 (nativeRegionShardPath paths index 0)
151 (nativeRegionShardPath paths index 1)
152 (nativeRegionPathArgument (nativeRegionDirectoryIndex paths))
153 nativePeerListenerSlot
154 nativePeerScratchSlot
155 (next (succ index)))))
156 (naturalEqual (ownerOf shard) owner)))))
157 (lambda unrestricted index : Nat . tail)
158 (nativeRegionShards plan)
159 0)))))))))
160
161-- `body owner` for owners 1..peers, in order.
162def nativePeerEachOwner =
163 (lambda unrestricted peers : Nat .
164 (lambda unrestricted body : (pi unrestricted owner : Nat . (pi unrestricted rest : (family NativePhysicalCommands) . (family NativePhysicalCommands))) .
165 (lambda unrestricted tail : (family NativePhysicalCommands) .
166 (stdListFold
167 Nat
168 (family NativePhysicalCommands)
169 (lambda unrestricted index : Nat .
170 (lambda unrestricted rest : (family NativePhysicalCommands) . (body (succ index) rest)))
171 tail
172 (stdListNaturalsBelow peers)))))
173
174def nativePeerRegionPublish =
175 (lambda unrestricted publication : (family NativePeerRegionPublication) .
176 (lambda unrestricted role : Nat .
177 (lambda unrestricted success : (family NativePhysicalCommands) .
178 (eliminate
179 NativePeerRegionPublication
180 (lambda unrestricted current : (family NativePeerRegionPublication) .
181 (family NativePhysicalCommands))
182 publication
183 (branch
184 NativePeerRegionPublicationOf
185 plan
186 peers
187 capture
188 committed
189 connection
190 stateAt
191 stateBytes
192 agreed
193 ownerOf
194 offsetOf
195 paths
196 .
197 (let unrestricted version =
198 (nativeMemoryLoad stateAt)
199 in
200 (let unrestricted epoch =
201 (nativeMemoryLoad
202 (naturalAdd stateAt (naturalMultiply 2 nativeCheckpointWordBytes)))
203 in
204 (nat-eliminate
205 (lambda unrestricted current : Nat . (family NativePhysicalCommands))
206 (nativeRegionPrepareOwner
207 plan
208 stateAt
209 ownerOf
210 offsetOf
211 0
212 stateAt
213 paths
214 (nativePeerEachOwner
215 peers
216 (lambda unrestricted owner : Nat .
217 (lambda unrestricted rest : (family NativePhysicalCommands) .
218 (let unrestricted frame =
219 (capture owner)
220 in
221 (nativeFrameInitializeRound
222 frame
223 epoch
224 version
225 (nativePeerPublicationIO
226 (nativeLaunchRecipeSlotValue (connection owner))
227 0
228 frame
229 (nativeFrameConsume
230 frame
231 (nativeMemoryCompareRegions
232 stateAt
233 (framePayloadAt frame)
234 agreed
235 nativePeerScratchSlot
236 b"checkpoint-captured-position"
237 (nativeRegionPrepareOwner
238 plan
239 stateAt
240 ownerOf
241 offsetOf
242 owner
243 (framePayloadAt frame)
244 paths
245 rest))))))))
246 (nativeRegionPublish
247 plan
248 stateAt
249 (lambda unrestricted index : Nat . (nativeRegionShardPath paths index 1))
250 (nativeRegionPathArgument (nativeRegionManifestCandidateIndex paths))
251 (nativeRegionPathArgument (nativeRegionManifestCommittedIndex paths))
252 (nativeRegionPathArgument (nativeRegionDirectoryIndex paths))
253 nativePeerListenerSlot
254 nativePeerScratchSlot
255 6
256 (nativePeerEachOwner
257 peers
258 (lambda unrestricted owner : Nat .
259 (lambda unrestricted rest : (family NativePhysicalCommands) .
260 (let unrestricted released =
261 (committed owner)
262 in
263 (nativeFrameInitializeRound
264 released
265 epoch
266 version
267 (nativeMemoryStoreWord64
268 b"checkpoint-committed-version"
269 (framePayloadAt released)
270 version
271 (nativePeerPublicationIO
272 (nativeLaunchRecipeSlotValue (connection owner))
273 1
274 released
275 rest))))))
276 success))))
277 (lambda unrestricted previous : Nat .
278 (lambda unrestricted ignored : (family NativePhysicalCommands) .
279 (let unrestricted channel =
280 (nativeLaunchRecipeSlotValue (connection 0))
281 in
282 (let unrestricted frame =
283 (capture role)
284 in
285 (let unrestricted released =
286 (committed role)
287 in
288 (nativeFrameInitializeRound
289 frame
290 epoch
291 version
292 (nativeFrameInitializeRound
293 released
294 epoch
295 version
296 (nativeMemoryCopyOperands
297 (nativeMemoryState (framePayloadAt frame))
298 (nativeMemoryState stateAt)
299 stateBytes
300 nativePeerScratchSlot
301 b"checkpoint-capture-state"
302 (nativePeerPublicationIO
303 channel
304 1
305 frame
306 (nativePeerPublicationIO
307 channel
308 0
309 released
310 (nativeFrameConsume
311 released
312 (nativeLaunchRecipeAssertEqual
313 (nativeMemoryLoad (framePayloadAt released))
314 version
315 b"checkpoint-committed-version"
316 success))))))))))))
317 role))))))))
318
319-- Publication owns the frame and checkpoint scratch arenas. A shard's bytes
320-- must lie entirely within its owner's captured state payload, past the
321-- capture prefix, never in a header or digest workspace that publication
322-- itself overwrites. Offsets are relative to the owner's state.
323def nativePublicationSourceWithin =
324 (lambda unrestricted start : Nat .
325 (lambda unrestricted count : Nat .
326 (lambda unrestricted base : Nat .
327 (lambda unrestricted size : Nat .
328 (naturalAnd
329 (naturalLessOrEqual (naturalAdd base nativeRegionCaptureBytes) start)
330 (naturalLessOrEqual (naturalAdd start count) (naturalAdd base size)))))))
331
332-- Every owner's frame occupies the first owner's storage exactly: same base,
333-- payload extent and end, so one arena resident covers all of them.
334def nativePeerFramesShareStorage =
335 (lambda unrestricted peers : Nat .
336 (lambda unrestricted frame : (pi unrestricted owner : Nat . (family RegionFrameLayout)) .
337 (lambda unrestricted payload : Nat .
338 (let unrestricted first =
339 (frame 1)
340 in
341 (stdListFold
342 Nat
343 Nat
344 (lambda unrestricted index : Nat .
345 (lambda unrestricted rest : Nat .
346 (let unrestricted current =
347 (frame (succ index))
348 in
349 (naturalAnd
350 rest
351 (naturalAnd
352 (naturalEqual (framePayloadBytes current) payload)
353 (naturalAnd
354 (naturalEqual (frameBase current) (frameBase first))
355 (naturalEqual (frameEnd current) (frameEnd first))))))))
356 1
357 (stdListNaturalsBelow peers))))))
358
359def nativePeerPublicationAdmitted =
360 (lambda unrestricted publication : (family NativePeerRegionPublication) .
361 (lambda unrestricted available : Nat .
362 (lambda unrestricted role : Nat .
363 (eliminate
364 NativePeerRegionPublication
365 (lambda unrestricted current : (family NativePeerRegionPublication) . Nat)
366 publication
367 (branch
368 NativePeerRegionPublicationOf
369 plan
370 peers
371 capture
372 committed
373 connection
374 stateAt
375 stateBytes
376 agreed
377 ownerOf
378 offsetOf
379 paths
380 .
381 (naturalAnd
382 (naturalNonzero peers)
383 (naturalAnd
384 (naturalLessOrEqual role peers)
385 (naturalAnd
386 (naturalBelowTwoPower 64 available)
387 (naturalAnd
388 (nativePeerFramesShareStorage peers capture stateBytes)
389 (naturalAnd
390 (nativePeerFramesShareStorage peers committed nativeCheckpointWordBytes)
391 (naturalAnd
392 (naturalAnd
393 (naturalLess nativeRegionCaptureBytes stateBytes)
394 (naturalAnd
395 (naturalLessOrEqual nativeRegionCaptureBytes agreed)
396 (naturalLessOrEqual agreed stateBytes)))
397 (naturalAnd
398 (naturalEqual
399 (nativeRegionPathCountOf paths)
400 (stdListLength (family NativeRegionShard) (nativeRegionShards plan)))
401 (naturalAnd
402 (arenaCertificate
403 available
404 (constructor
405 ArenaResidents
406 ArenaResidentsNext
407 (constructor
408 ArenaResident
409 ArenaResidentValue
410 b"captured-local-state"
411 stateAt
412 stateBytes
413 nativeCheckpointWordBytes)
414 (constructor
415 ArenaResidents
416 ArenaResidentsNext
417 (constructor
418 ArenaResident
419 ArenaResidentValue
420 b"capture-frame"
421 (frameBase (capture 1))
422 (naturalSaturatingSubtract
423 (frameEnd (capture 1))
424 (frameBase (capture 1)))
425 1)
426 (constructor
427 ArenaResidents
428 ArenaResidentsNext
429 (constructor
430 ArenaResident
431 ArenaResidentValue
432 b"commit-frame"
433 (frameBase (committed 1))
434 (naturalSaturatingSubtract
435 (frameEnd (committed 1))
436 (frameBase (committed 1)))
437 1)
438 (nativeRegionResidents plan)))))
439 (stdListFold
440 (family NativeRegionShard)
441 Nat
442 (lambda unrestricted shard : (family NativeRegionShard) .
443 (lambda unrestricted rest : Nat .
444 (naturalAnd
445 rest
446 (naturalAnd
447 (naturalLessOrEqual (ownerOf shard) peers)
448 (nativePublicationSourceWithin
449 (offsetOf shard)
450 (intervalExtent (nativeRegionInterval shard))
451 0
452 stateBytes)))))
453 1
454 (nativeRegionShards plan)))))))))))))))
455
456def planNativePeerRegionPublish =
457 (lambda unrestricted publication : (family NativePeerRegionPublication) .
458 (lambda unrestricted available : Nat .
459 (lambda unrestricted role : Nat .
460 (lambda unrestricted success : (family NativePhysicalCommands) .
461 (nat-eliminate
462 (lambda unrestricted valid : Nat .
463 (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)))
464 (constructor
465 StdResult
466 StdFailure
467 (family NativeCheckpointFailure)
468 (family NativePhysicalCommands)
469 (constructor NativeCheckpointFailure NativeCheckpointBounds))
470 (lambda unrestricted previous : Nat .
471 (lambda unrestricted ignored : (family StdResult (family NativeCheckpointFailure) (family NativePhysicalCommands)) .
472 (constructor
473 StdResult
474 StdSuccess
475 (family NativeCheckpointFailure)
476 (family NativePhysicalCommands)
477 (nativePeerRegionPublish publication role success))))
478 (nativePeerPublicationAdmitted publication available role))))))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.