1module Platform.Linux.Nvidia.PlanHostRequest
2
3import Checkpoint.Envelope
4import Data.Bytes
5import Model.Config
6import Model.Parameter
7import Model.Word32
8import Model.Word64
9import Platform.Linux.Nvidia.PlanHost
10import Runtime.ArenaCertificate
11import Runtime.NativeLaunchRecipeLoad
12import Runtime.NativePhysicalEmbeddedArtifact
13import Runtime.NativePhysicalNativeELF
14import Runtime.NativePhysicalProgram
15import Runtime.NativeCyclicRecordOffset
16import Runtime.NativeFiniteWords
17import Runtime.CyclicRecordOffset
18import Runtime.TextArtifactRequest
19import Std.Natural
20
21-- The request-driven host the compiler derives for a text artifact: the
22-- host Bob and Coppelius run, on PlanHost's compute channel. In order:
23-- 1. register for the private expedited membarrier (the doorbell fence);
24-- 2. the envelope: open /proc/self/exe, read the footer and the manifest
25-- through it, require the magics, every descriptor's tag and identity,
26-- the recipe lengths, and each component's SHA-256 (the kernel's
27-- AF_ALG hasher over the executable's own bytes) against the manifest
28-- -- an executable that is not the one the compiler wrote refuses
29-- itself before touching the card;
30-- 3. the request record (Runtime.TextArtifactRequest) named by the one
31-- process argument: length, magic, version, operation, then the five
32-- paths opened, the input's extent and the checkpoint's (empty or
33-- full) required;
34-- 4. PlanHost's prelude: the channel;
35-- 5. the staging area and the launch-table recipes expanded into the
36-- mapped arena (Runtime.NativeLaunchRecipeLoad) at the offsets the
37-- manifest names;
38-- 6. the schedule: submissions waited on their own semaphore slot, repeat
39-- bodies with loop-affine gpPut, semaphore and file offsets, the
40-- checkpoint and batch I/O between them, the request's operation
41-- (train continues, predict exits), the result record; exit 0. A run
42-- loop issues a submission of the plan again and again (Reissue): the
43-- host writes the ring entry itself, so one pushbuffer piece serves
44-- every step; the input is then a stream read at a cursor the
45-- checkpoint positions, and the checkpoint is published as often as the
46-- schedule says.
47-- Every offset and extent below is either PlanHost's state layout or a
48-- parameter the pairing derives from its plans.
49
50-- a launch-table recipe expanded into the mapped arena at startup
51family NvidiaPlanHostRecipeFills : Type 0
52constructor NvidiaPlanHostRecipeFillsEnd
53constructor NvidiaPlanHostRecipeFillsNext
54field unrestricted nvidiaPlanHostRecipeFillHost : Nat
55field unrestricted nvidiaPlanHostRecipeFillTableExtent : Nat
56field unrestricted nvidiaPlanHostRecipeFillKind : (family NativePhysicalEmbeddedComponentKind)
57recursive unrestricted nvidiaPlanHostRecipeFillsTail
58end-family
59
60-- the five files a request names
61family NvidiaPlanHostFile : Type 0
62constructor NvidiaPlanHostInput
63constructor NvidiaPlanHostCheckpointIn
64constructor NvidiaPlanHostCheckpointOut
65constructor NvidiaPlanHostPredictions
66constructor NvidiaPlanHostResult
67end-family
68
69-- A step names a submission by its gpPut (the GPFIFO entries issued so far
70-- once it is written; the submission waited on is ordinal gpPut - 1, its
71-- semaphore slot 32 x ordinal, its timestamp record 64 x ordinal). Inside
72-- a repeat body a step's gpPut, semaphore, stamps and file offset advance by
73-- `stride` per iteration (loop-affine operands); outside, stride is 0.
74family NvidiaPlanHostSteps : Type 0
75constructor NvidiaPlanHostStepsEnd
76constructor NvidiaPlanHostStepSubmit
77field unrestricted nvidiaPlanHostStepSubmitGPPut : Nat
78field unrestricted nvidiaPlanHostStepSubmitStride : Nat
79recursive unrestricted nvidiaPlanHostStepSubmitTail
80constructor NvidiaPlanHostStepRepeat
81field unrestricted nvidiaPlanHostStepRepeatCount : Nat
82recursive unrestricted nvidiaPlanHostStepRepeatBody
83recursive unrestricted nvidiaPlanHostStepRepeatTail
84constructor NvidiaPlanHostStepRead
85field unrestricted nvidiaPlanHostStepReadFile : (family NvidiaPlanHostFile)
86field unrestricted nvidiaPlanHostStepReadHost : Nat
87field unrestricted nvidiaPlanHostStepReadExtent : Nat
88field unrestricted nvidiaPlanHostStepReadOffset : Nat
89field unrestricted nvidiaPlanHostStepReadStride : Nat
90field unrestricted nvidiaPlanHostStepReadTolerateEmpty : Nat
91recursive unrestricted nvidiaPlanHostStepReadTail
92-- Read from ((completed updates + index + loop * indexStride) mod count).
93-- The checkpoint header owns the persisted count. File identity admission is
94-- separate; this step alone proves neither corpus identity nor authenticity.
95constructor NvidiaPlanHostStepReadCyclic
96field unrestricted nvidiaPlanHostStepCyclicHost : Nat
97field unrestricted nvidiaPlanHostStepCyclicExtent : Nat
98field unrestricted nvidiaPlanHostStepCyclicOffset : Nat
99field unrestricted nvidiaPlanHostStepCyclicRecordBytes : Nat
100field unrestricted nvidiaPlanHostStepCyclicCount : Nat
101field unrestricted nvidiaPlanHostStepCyclicIndex : Nat
102field unrestricted nvidiaPlanHostStepCyclicIndexStride : Nat
103recursive unrestricted nvidiaPlanHostStepCyclicTail
104constructor NvidiaPlanHostStepWrite
105field unrestricted nvidiaPlanHostStepWriteFile : (family NvidiaPlanHostFile)
106field unrestricted nvidiaPlanHostStepWriteHost : Nat
107field unrestricted nvidiaPlanHostStepWriteExtent : Nat
108recursive unrestricted nvidiaPlanHostStepWriteTail
109constructor NvidiaPlanHostStepWriteAt
110field unrestricted nvidiaPlanHostStepWriteAtFile : (family NvidiaPlanHostFile)
111field unrestricted nvidiaPlanHostStepWriteAtHost : Nat
112field unrestricted nvidiaPlanHostStepWriteAtExtent : Nat
113field unrestricted nvidiaPlanHostStepWriteAtOffset : Nat
114recursive unrestricted nvidiaPlanHostStepWriteAtTail
115constructor NvidiaPlanHostStepWriteStat
116field unrestricted nvidiaPlanHostStepWriteStatFile : (family NvidiaPlanHostFile)
117recursive unrestricted nvidiaPlanHostStepWriteStatTail
118constructor NvidiaPlanHostStepWriteStatus
119field unrestricted nvidiaPlanHostStepWriteStatusFile : (family NvidiaPlanHostFile)
120recursive unrestricted nvidiaPlanHostStepWriteStatusTail
121constructor NvidiaPlanHostStepWriteTimestamps
122field unrestricted nvidiaPlanHostStepWriteTimestampsFile : (family NvidiaPlanHostFile)
123recursive unrestricted nvidiaPlanHostStepWriteTimestampsTail
124constructor NvidiaPlanHostStepRecordStat
125field unrestricted nvidiaPlanHostStepRecordHost : Nat
126field unrestricted nvidiaPlanHostStepRecordStatOffset : Nat
127field unrestricted nvidiaPlanHostStepRecordExtent : Nat
128recursive unrestricted nvidiaPlanHostStepRecordTail
129constructor NvidiaPlanHostStepStamp
130field unrestricted nvidiaPlanHostStepStampGPPut : Nat
131field unrestricted nvidiaPlanHostStepStampStride : Nat
132field unrestricted nvidiaPlanHostStepStampWhich : Nat
133recursive unrestricted nvidiaPlanHostStepStampTail
134constructor NvidiaPlanHostStepFill
135field unrestricted nvidiaPlanHostStepFillHost : Nat
136field unrestricted nvidiaPlanHostStepFillPayload : Bytes
137recursive unrestricted nvidiaPlanHostStepFillTail
138-- A completed device word checked before any dependent file publication.
139-- The word may contain multiple packed statuses; every bit is compared.
140constructor NvidiaPlanHostStepAssertWord
141field unrestricted nvidiaPlanHostStepAssertIdentity : Bytes
142field unrestricted nvidiaPlanHostStepAssertHost : Nat
143field unrestricted nvidiaPlanHostStepAssertExpected : Nat
144recursive unrestricted nvidiaPlanHostStepAssertTail
145-- Begin publication after the caller admits its operation, without encoding
146-- that operation as a runtime-selected architecture-specific syscall.
147-- Hash the complete admitted input and bind it to a checkpoint payload
148-- field. An empty checkpoint captures the identity; a resumed one must agree.
149constructor NvidiaPlanHostStepBindInputIdentity
150field unrestricted nvidiaPlanHostStepInputIdentityOffset : Nat
151field unrestricted nvidiaPlanHostStepInputIdentityExtent : Nat
152recursive unrestricted nvidiaPlanHostStepInputIdentityTail
153constructor NvidiaPlanHostStepWriteInputIdentity
154recursive unrestricted nvidiaPlanHostStepWriteInputIdentityTail
155constructor NvidiaPlanHostStepBeginCheckpoint
156recursive unrestricted nvidiaPlanHostStepBeginCheckpointTail
157constructor NvidiaPlanHostStepOperation
158recursive unrestricted nvidiaPlanHostStepOperationTail
159constructor NvidiaPlanHostStepSync
160field unrestricted nvidiaPlanHostStepSyncFile : (family NvidiaPlanHostFile)
161recursive unrestricted nvidiaPlanHostStepSyncTail
162constructor NvidiaPlanHostStepDataSync
163field unrestricted nvidiaPlanHostStepDataSyncFile : (family NvidiaPlanHostFile)
164recursive unrestricted nvidiaPlanHostStepDataSyncTail
165constructor NvidiaPlanHostStepClose
166field unrestricted nvidiaPlanHostStepCloseFile : (family NvidiaPlanHostFile)
167recursive unrestricted nvidiaPlanHostStepCloseTail
168-- Submission `piece` of the plan issued again: the host writes the plan's
169-- GPFIFO entry for it (`entry`, as realized) into the ring at ordinal
170-- gpPut - 1, clears the piece's semaphore slot (its pushbuffer releases the
171-- same slot every time), then publishes gpPut and awaits the slot as a
172-- Submit does. gpPut, piece and entry advance by their strides per
173-- iteration of an enclosing repeat (equal pieces laid end to end: the
174-- pairing's admission holds each iteration's entry to the realized table).
175constructor NvidiaPlanHostStepReissue
176field unrestricted nvidiaPlanHostStepReissueGPPut : Nat
177field unrestricted nvidiaPlanHostStepReissueGPPutStride : Nat
178field unrestricted nvidiaPlanHostStepReissuePiece : Nat
179field unrestricted nvidiaPlanHostStepReissuePieceStride : Nat
180field unrestricted nvidiaPlanHostStepReissueEntry : Nat
181field unrestricted nvidiaPlanHostStepReissueEntryStride : Nat
182recursive unrestricted nvidiaPlanHostStepReissueTail
183-- host commands run in place (a learner's per-update scalars,
184-- Platform.Linux.Nvidia.PlanHostAdamW); they may not repeat
185constructor NvidiaPlanHostStepCommands
186field unrestricted nvidiaPlanHostStepCommandsList : (family NativePhysicalCommands)
187recursive unrestricted nvidiaPlanHostStepCommandsTail
188-- the input stream's cursor: `base` bytes, plus `scale` for every
189-- invocation the checkpoint read has counted (0 for a fresh start), so a
190-- resumed run reads on from where its checkpoint left the stream
191constructor NvidiaPlanHostStepCursorFromCheckpoint
192field unrestricted nvidiaPlanHostStepCursorBase : Nat
193field unrestricted nvidiaPlanHostStepCursorScale : Nat
194recursive unrestricted nvidiaPlanHostStepCursorFromCheckpointTail
195-- `extent` bytes of the file at the cursor plus `delta`, into `host`; a
196-- short read is a command failure
197constructor NvidiaPlanHostStepReadAtCursor
198field unrestricted nvidiaPlanHostStepReadAtCursorFile : (family NvidiaPlanHostFile)
199field unrestricted nvidiaPlanHostStepReadAtCursorHost : Nat
200field unrestricted nvidiaPlanHostStepReadAtCursorExtent : Nat
201field unrestricted nvidiaPlanHostStepReadAtCursorDelta : Nat
202recursive unrestricted nvidiaPlanHostStepReadAtCursorTail
203constructor NvidiaPlanHostStepCursorAdvance
204field unrestricted nvidiaPlanHostStepCursorAdvanceBytes : Nat
205recursive unrestricted nvidiaPlanHostStepCursorAdvanceTail
206-- the checkpoint's temporary created (as a train request's operation
207-- does), for a checkpoint published later in the schedule
208constructor NvidiaPlanHostStepCheckpointBegin
209recursive unrestricted nvidiaPlanHostStepCheckpointBeginTail
210-- the checkpoint published (prPublishCheckpointStages): its header counts
211-- `updates` updates and `invocations` invocations past the checkpoint read
212constructor NvidiaPlanHostStepCheckpointPublish
213field unrestricted nvidiaPlanHostStepCheckpointPublishUpdates : Nat
214field unrestricted nvidiaPlanHostStepCheckpointPublishInvocations : Nat
215recursive unrestricted nvidiaPlanHostStepCheckpointPublishTail
216end-family
217
218-- What a request's input must be: exactly `extent` bytes, or a stream the
219-- schedule reads at its cursor (any length: every read of it must return
220-- whole, so a stream that ends early stops the run at that read).
221family NvidiaPlanHostInputContract : Type 0
222constructor NvidiaPlanHostInputExact
223field unrestricted nvidiaPlanHostInputExactExtent : Nat
224constructor NvidiaPlanHostInputStream
225end-family
226
227-- ---- state areas after PlanHost's buffer call blocks ----
228-- each after the previous, 8-byte aligned
229def prAfter =
230 (lambda unrestricted at : Nat .
231 (lambda unrestricted bytes : Nat . (naturalMultiply (naturalDivideUnchecked (naturalAdd (naturalAdd at bytes) 7) 8) 8)))
232def prRequest : Nat = phBufferBlocksEnd
233def prStat : Nat = (prAfter prRequest textArtifactRequestEncodedLength)
234def prStatExtent : Nat = 160
235def prFooter : Nat = (prAfter prStat prStatExtent)
236def prManifest : Nat = (prAfter prFooter nativePhysicalEmbeddedFooterLength)
237def prDescriptorWords : Nat = (prAfter prManifest nativePhysicalEmbeddedManifestLength)
238def prDigest : Nat = (prAfter prDescriptorWords 80)
239def prIdentityScratch : Nat = (prAfter prDigest nativePhysicalEmbeddedDigestLength)
240def prSendOffset : Nat = (prAfter prIdentityScratch nativePhysicalEmbeddedIdentityLength)
241def prGPPut : Nat = (prAfter prSendOffset 8)
242def prWordScratch : Nat = (prAfter prGPPut 8)
243def prStatusBlock : Nat = (prAfter prWordScratch 8)
244def prStatusBlockExtent : Nat = 160
245def prExpected : Nat = (prAfter prStatusBlock prStatusBlockExtent)
246-- the checkpoint read's header and the written one's (Checkpoint.Envelope:
247-- the fields before the chunk digests), and a chunk's expected digest
248def prCheckpointHeaderIn : Nat = (prAfter prExpected 8)
249def prCheckpointHeaderOut : Nat = (prAfter prCheckpointHeaderIn checkpointEnvelopeDigestsAt)
250def prExpectedDigest : Nat = (prAfter prCheckpointHeaderOut checkpointEnvelopeDigestsAt)
251-- the learner's per-update scalars (Platform.Linux.Nvidia.PlanHostAdamW):
252-- sixteen binary64 words
253def prLearnerScratch : Nat = (prAfter prExpectedDigest checkpointEnvelopeDigestBytes)
254def prLearnerScratchExtent : Nat = 128
255-- Retained separately from prDigest, which checkpoint chunk hashing reuses.
256def prInputIdentity : Nat = (prAfter prLearnerScratch prLearnerScratchExtent)
257-- the input stream's cursor and the offset a cursor read computes
258def prCursor : Nat = (prAfter prInputIdentity checkpointEnvelopeDigestBytes)
259def prCursorOffset : Nat = (prAfter prCursor 8)
260def prCursorScratch : Nat = (prAfter prCursorOffset 8)
261def prAreasEnd : Nat = (prAfter prCursorScratch 8)
262-- every area inside PlanHost's state
263def prAreasFit : (equal Nat (naturalLessOrEqual prAreasEnd phStateExtent) 1) = (refl Nat 1)
264
265-- result slots after PlanHost's four
266def prSlotExe : Nat = 4
267def prSlotRequest : Nat = 5
268def prSlotInput : Nat = 6
269def prSlotCheckpointIn : Nat = 7
270def prSlotCheckpointOut : Nat = 8
271def prSlotPredictions : Nat = 9
272def prSlotResult : Nat = 10
273def prSlotStatus : Nat = 11
274def prSlotAlg : Nat = 12
275def prSlotHash : Nat = 13
276
277-- Linux x86-64
278def prSysClose : Nat = 3
279def prSysFstat : Nat = 5
280def prSysLseek : Nat = 8
281def prSysPread : Nat = 17
282def prSysPwrite : Nat = 18
283def prSysSendfile : Nat = 40
284def prSysSocket : Nat = 41
285def prSysAccept : Nat = 43
286def prSysBind : Nat = 49
287def prSysFsync : Nat = 74
288def prSysFdatasync : Nat = 75
289def prSysClockGettime : Nat = 228
290def prSysMembarrier : Nat = 324
291def prSysRename : Nat = 82
292-- a temporary a crashed run left, removed before the new one is created
293def prSysUnlink : Nat = 87
294def prSeekEnd : Nat = 2
295def prMinusFooter : Nat = 18446744073709551600
296def prOpenWriteCreate : Nat = 577
297def prCreateMode : Nat = 384
298-- O_RDWR | O_CREAT | O_EXCL: the checkpoint's temporary, which must be new
299def prOpenReadWriteExclusive : Nat = 194
300-- O_RDONLY | O_DIRECTORY
301def prOpenDirectory : Nat = 65536
302def prMembarrierRegister : Nat = 16
303def prMembarrierFence : Nat = 8
304def prAddressFamilyAlg : Nat = 38
305def prSocketSeqpacket : Nat = 5
306def prStatSize : Nat = 48
307def prClockRealtime : Nat = 0
308
309-- The mapped recipe staging area, and the host timestamp table that lives
310-- in it once the recipes are expanded: a 64-byte record per submission
311-- ([+0] before the doorbell, [+16] after the wait, [+32] and [+48] around
312-- the I/O that follows), CLOCK_REALTIME, the clock the device stamps its
313-- semaphores with.
314def nvidiaPlanHostStaging : Nat = 0x40000000
315def nvidiaPlanHostStagingExtent : Nat = 0x1000000
316def nvidiaPlanHostTimestampRecord : Nat = 64
317
318-- ---- telemetry ----
319-- The request host's phase boundaries, each an ALPHATEL record sealed and
320-- appended to `alpha-host.alphatel` in its working directory as the plan
321-- host's are (PlanHost.phTelemetry): begun; the request and the checkpoint
322-- checked; the channel up; the recipes expanded; the learner's scalars
323-- written; the checkpoint published (a train request); every step done. A
324-- record exists only if the host got there.
325def prTelemetryBegin : Nat = 0
326def prTelemetryChecked : Nat = 1
327def prTelemetryChannel : Nat = 2
328def prTelemetryUploaded : Nat = 3
329def prTelemetryLearner : Nat = 4
330def prTelemetryPublished : Nat = 5
331def prTelemetryDone : Nat = 6
332
333-- ---- operands and assertions ----
334def prStatus : (family NativePhysicalOperand) = (phSlot prSlotStatus)
335
336def prAssertStatus =
337 (lambda unrestricted identity : Bytes .
338 (lambda unrestricted expected : Nat .
339 (lambda unrestricted tail : (family NativePhysicalCommands) .
340 (nativeLaunchRecipeAssertEqual prStatus (phImm expected) identity tail))))
341
342-- Inspect a mapped checkpoint staging span after its GPU copy has retired.
343-- The caller supplies a bank's representation and a span admitted by its
344-- host layout. A failed scan halts before that span reaches the checkpoint.
345def nvidiaPlanHostRejectNonfiniteMapped =
346 (lambda unrestricted identity : Bytes .
347 (lambda unrestricted format : (family NativeFiniteWordFormat) .
348 (lambda unrestricted host : Nat .
349 (lambda unrestricted extent : Nat .
350 (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
351 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCommands
352 (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine
353 (nativeFiniteRoutineFor format)
354 (phArgs3 (phImm host) (phImm extent) (phImm 0))
355 (phStore prSlotStatus))
356 (prAssertStatus identity 0
357 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))
358 tail))))))
359
360def prAssertEqual =
361 (lambda unrestricted identity : Bytes .
362 (lambda unrestricted left : (family NativePhysicalOperand) .
363 (lambda unrestricted right : (family NativePhysicalOperand) .
364 (lambda unrestricted tail : (family NativePhysicalCommands) .
365 (nativeLaunchRecipeAssertEqual left right identity tail)))))
366
367def prAssertOneOf =
368 (lambda unrestricted identity : Bytes .
369 (lambda unrestricted observed : (family NativePhysicalOperand) .
370 (lambda unrestricted first : Nat .
371 (lambda unrestricted second : Nat .
372 (lambda unrestricted tail : (family NativePhysicalCommands) .
373 (nativeLaunchRecipeCommand
374 (constructor NativePhysicalOperation NativePhysicalAssertOneOf observed (phImm first) (phImm second)
375 (constructor NativePhysicalErrorCode NativePhysicalExecutionAssertionFailed))
376 identity tail))))))
377
378-- the 8-byte word at a state offset equals these 8 bytes
379def prExpectBytes =
380 (lambda unrestricted identity : Bytes .
381 (lambda unrestricted offset : Nat .
382 (lambda unrestricted payload : Bytes .
383 (lambda unrestricted tail : (family NativePhysicalCommands) .
384 (phCopy prExpected payload
385 (prAssertEqual identity (phLoad offset) (phLoad prExpected) tail))))))
386
387-- `count` words from a state offset equal these bytes
388def prExpectWords =
389 (lambda unrestricted identity : Bytes .
390 (lambda unrestricted offset : Nat .
391 (lambda unrestricted payload : Bytes .
392 (lambda unrestricted count : Nat .
393 (lambda unrestricted tail : (family NativePhysicalCommands) .
394 (nat-eliminate
395 (lambda unrestricted current : Nat . (family NativePhysicalCommands))
396 tail
397 (lambda unrestricted index : Nat .
398 (lambda unrestricted induction : (family NativePhysicalCommands) .
399 (prExpectBytes identity (naturalAdd offset (naturalMultiply index 8)) (phTake 8 (phDrop (naturalMultiply index 8) payload)) induction)))
400 count))))))
401
402-- a 32-bit word of the state zero-extended into an 8-byte word
403def prLoad32 =
404 (lambda unrestricted source : Nat .
405 (lambda unrestricted destination : Nat .
406 (lambda unrestricted tail : (family NativePhysicalCommands) .
407 (phCopy destination (phZeros 8) (phCopyStateToState destination source 4 tail)))))
408
409def prClose =
410 (lambda unrestricted identity : Bytes .
411 (lambda unrestricted slot : Nat .
412 (lambda unrestricted tail : (family NativePhysicalCommands) .
413 (phCall prSysClose (phArgs3 (phSlot slot) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
414 (prAssertStatus identity 0 tail)))))
415
416def prFstat =
417 (lambda unrestricted identity : Bytes .
418 (lambda unrestricted slot : Nat .
419 (lambda unrestricted tail : (family NativePhysicalCommands) .
420 (phCall prSysFstat (phArgs3 (phSlot slot) (phState prStat) (phImm 0)) b"" (phStore prSlotStatus)
421 (prAssertStatus identity 0 tail)))))
422
423-- an immediate, or loop-affine when the stride is not 0
424def prAffine =
425 (lambda unrestricted base : Nat .
426 (lambda unrestricted stride : Nat .
427 (nat-eliminate
428 (lambda unrestricted current : Nat . (family NativePhysicalOperand))
429 (phImm base)
430 (lambda unrestricted predecessor : Nat .
431 (lambda unrestricted ignored : (family NativePhysicalOperand) .
432 (constructor NativePhysicalOperand NativePhysicalLoopAffine (phWord base) (phWord stride))))
433 stride)))
434
435-- ---- 1. the fence ----
436def prFenceRegister =
437 (lambda unrestricted tail : (family NativePhysicalCommands) .
438 (phCall prSysMembarrier (phArgs3 (phImm prMembarrierRegister) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
439 (prAssertStatus b"membarrier-register" 0 tail)))
440
441def prFence =
442 (lambda unrestricted tail : (family NativePhysicalCommands) .
443 (phCall prSysMembarrier (phArgs3 (phImm prMembarrierFence) (phImm 0) (phImm 0)) b"" phDiscard tail))
444
445-- ---- 2. the envelope ----
446-- sockaddr_alg: AF_ALG, "hash", feat, mask, "sha256"
447def prSockaddrAlg : Bytes =
448 (bytes-append (bytes 38 0)
449 (bytes-append b"hash" (bytes-append (phZeros 10)
450 (bytes-append (phZeros 8) (bytes-append b"sha256" (phZeros 58))))))
451def prSockaddrAlgExtent : Nat = 88
452
453def prDescriptor =
454 (lambda unrestricted index : Nat .
455 (naturalAdd prManifest (naturalAdd 12 (naturalMultiply index nativePhysicalEmbeddedDescriptorLength))))
456def prDescriptorOffsetWord =
457 (lambda unrestricted index : Nat . (naturalAdd prDescriptorWords (naturalMultiply index 16)))
458def prDescriptorLengthWord =
459 (lambda unrestricted index : Nat . (naturalAdd (prDescriptorOffsetWord index) 8))
460
461-- One descriptor: its tag is the component's, its offset and length are
462-- kept as words, its identity is the one the pairing embedded, and the
463-- SHA-256 of the component's bytes in this executable equals the digest
464-- the manifest carries.
465def prVerifyComponent =
466 (lambda unrestricted index : Nat .
467 (lambda unrestricted identity : Bytes .
468 (lambda unrestricted tail : (family NativePhysicalCommands) .
469 (let unrestricted descriptor = (prDescriptor index)
470 in
471 (prLoad32 descriptor prWordScratch
472 (prAssertEqual b"envelope-tag" (phLoad prWordScratch) (phImm (naturalAdd index 1))
473 (prLoad32 (naturalAdd descriptor 4) (prDescriptorOffsetWord index)
474 (prLoad32 (naturalAdd descriptor 8) (prDescriptorLengthWord index)
475 (phCopyStateToState prIdentityScratch (naturalAdd descriptor 12) nativePhysicalEmbeddedIdentityLength
476 (prExpectWords b"envelope-identity" prIdentityScratch identity 8
477 (phCall prSysSocket (phArgs3 (phImm prAddressFamilyAlg) (phImm prSocketSeqpacket) (phImm 0)) b"" (phStore prSlotAlg)
478 (phCall prSysBind (phArgs3 (phSlot prSlotAlg) phPayload (phImm prSockaddrAlgExtent)) prSockaddrAlg (phStore prSlotStatus)
479 (prAssertStatus b"envelope-hash-bind" 0
480 (phCall prSysAccept (phArgs3 (phSlot prSlotAlg) (phImm 0) (phImm 0)) b"" (phStore prSlotHash)
481 (prLoad32 (naturalAdd descriptor 4) prSendOffset
482 (phCall prSysSendfile (phArgs (phSlot prSlotHash) (phSlot prSlotExe) (phState prSendOffset) (phLoad (prDescriptorLengthWord index)) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
483 (prAssertEqual b"envelope-hash-send" prStatus (phLoad (prDescriptorLengthWord index))
484 (phCall phSysRead (phArgs3 (phSlot prSlotHash) (phState prDigest) (phImm nativePhysicalEmbeddedDigestLength)) b"" (phStore prSlotStatus)
485 (prAssertStatus b"envelope-hash-read" nativePhysicalEmbeddedDigestLength
486 (phCopyStateToState prIdentityScratch (naturalAdd descriptor 76) nativePhysicalEmbeddedDigestLength
487 (prAssertEqual b"envelope-digest" (phLoad prDigest) (phLoad prIdentityScratch)
488 (prAssertEqual b"envelope-digest" (phLoad (naturalAdd prDigest 8)) (phLoad (naturalAdd prIdentityScratch 8))
489 (prAssertEqual b"envelope-digest" (phLoad (naturalAdd prDigest 16)) (phLoad (naturalAdd prIdentityScratch 16))
490 (prAssertEqual b"envelope-digest" (phLoad (naturalAdd prDigest 24)) (phLoad (naturalAdd prIdentityScratch 24))
491 (prClose b"envelope-hash-close" prSlotHash
492 (prClose b"envelope-alg-close" prSlotAlg
493 tail))))))))))))))))))))))))))
494
495-- a recipe descriptor's length is the recipe's
496def prVerifyRecipe =
497 (lambda unrestricted index : Nat .
498 (lambda unrestricted identity : Bytes .
499 (lambda unrestricted length : Nat .
500 (lambda unrestricted tail : (family NativePhysicalCommands) .
501 (prVerifyComponent index identity
502 (prAssertEqual b"envelope-recipe-length" (phLoad (prDescriptorLengthWord index)) (phImm length) tail))))))
503
504def prEnvelope =
505 (lambda unrestricted hostIdentity : Bytes .
506 (lambda unrestricted programIdentity : Bytes .
507 (lambda unrestricted qmdIdentity : Bytes .
508 (lambda unrestricted pushIdentity : Bytes .
509 (lambda unrestricted gpfifoIdentity : Bytes .
510 (lambda unrestricted programLength : Nat .
511 (lambda unrestricted qmdLength : Nat .
512 (lambda unrestricted pushLength : Nat .
513 (lambda unrestricted gpfifoLength : Nat .
514 (lambda unrestricted tail : (family NativePhysicalCommands) .
515 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm 0)) b"/proc/self/exe\x00" (phStore prSlotExe)
516 (prFstat b"envelope-stat" prSlotExe
517 (phCall prSysLseek (phArgs3 (phSlot prSlotExe) (phImm prMinusFooter) (phImm prSeekEnd)) b"" phDiscard
518 (phCall phSysRead (phArgs3 (phSlot prSlotExe) (phState prFooter) (phImm nativePhysicalEmbeddedFooterLength)) b"" (phStore prSlotStatus)
519 (prAssertStatus b"envelope-footer-read" nativePhysicalEmbeddedFooterLength
520 (prExpectBytes b"envelope-footer-magic" prFooter nativePhysicalEmbeddedFooterMagic
521 (prLoad32 (naturalAdd prFooter 12) prWordScratch
522 (prAssertEqual b"envelope-footer-length" (phLoad prWordScratch) (phImm nativePhysicalEmbeddedManifestLength)
523 (prLoad32 (naturalAdd prFooter 8) prWordScratch
524 (phCall prSysPread (phArgs (phSlot prSlotExe) (phState prManifest) (phImm nativePhysicalEmbeddedManifestLength) (phLoad prWordScratch) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
525 (prAssertStatus b"envelope-manifest-read" nativePhysicalEmbeddedManifestLength
526 (prExpectBytes b"envelope-manifest-magic" prManifest nativePhysicalEmbeddedManifestMagic
527 (prExpectBytes b"envelope-manifest-version" (naturalAdd prManifest 8)
528 (bytes-append (phW32 nativePhysicalEmbeddedVersion) (phW32 (nativePhysicalEmbeddedComponentTag (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedHostELF))))
529 (prVerifyComponent 0 hostIdentity
530 (prVerifyRecipe 1 programIdentity programLength
531 (prVerifyRecipe 2 qmdIdentity qmdLength
532 (prVerifyRecipe 3 pushIdentity pushLength
533 (prVerifyRecipe 4 gpfifoIdentity gpfifoLength
534 tail))))))))))))))))))))))))))))
535
536-- ---- 3. the request ----
537def prPath =
538 (lambda unrestricted which : Nat .
539 (naturalAdd prRequest (naturalAdd 24 (naturalMultiply which textArtifactPathExtent))))
540
541def prOpenPath =
542 (lambda unrestricted which : Nat .
543 (lambda unrestricted flags : Nat .
544 (lambda unrestricted slot : Nat .
545 (lambda unrestricted tail : (family NativePhysicalCommands) .
546 (phCall phSysOpenat (phArgs (phImm phAtFdCwd) (phState (prPath which)) (phImm flags) (phImm prCreateMode) (phImm 0) (phImm 0)) b"" (phStore slot) tail)))))
547
548-- the checkpoint read: when the file is not empty, its envelope
549-- (Checkpoint.Envelope) -- the fixed fields, the four identities, every
550-- chunk's digest -- before any buffer is allocated. An empty file is a
551-- fresh start: its header reads as zeros, so its version (the count of the
552-- conditional block) is 0 and so is its chunk count; a file of the full
553-- size must say version 1 (the size plus the version is 0 or the full size
554-- plus 1), so the checks are skipped only for an empty one.
555def prChunkCheck =
556 (lambda unrestricted fileSlot : Nat .
557 (lambda unrestricted offset : (family NativePhysicalOperand) .
558 (lambda unrestricted extent : Nat .
559 (lambda unrestricted digestAt : (family NativePhysicalOperand) .
560 (lambda unrestricted tail : (family NativePhysicalCommands) .
561 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prSendOffset) offset)
562 (phCall prSysSendfile (phArgs (phSlot prSlotHash) (phSlot fileSlot) (phState prSendOffset) (phImm extent) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
563 (prAssertStatus b"checkpoint-chunk-read" extent
564 (phCall phSysRead (phArgs3 (phSlot prSlotHash) (phState prDigest) (phImm checkpointEnvelopeDigestBytes)) b"" (phStore prSlotStatus)
565 (prAssertStatus b"checkpoint-chunk-hash" checkpointEnvelopeDigestBytes
566 (phCall prSysPread (phArgs (phSlot fileSlot) (phState prExpectedDigest) (phImm checkpointEnvelopeDigestBytes) digestAt (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
567 (prAssertStatus b"checkpoint-chunk-digest-read" checkpointEnvelopeDigestBytes
568 (prAssertEqual b"checkpoint-chunk" (phLoad prDigest) (phLoad prExpectedDigest)
569 (prAssertEqual b"checkpoint-chunk" (phLoad (naturalAdd prDigest 8)) (phLoad (naturalAdd prExpectedDigest 8))
570 (prAssertEqual b"checkpoint-chunk" (phLoad (naturalAdd prDigest 16)) (phLoad (naturalAdd prExpectedDigest 16))
571 (prAssertEqual b"checkpoint-chunk" (phLoad (naturalAdd prDigest 24)) (phLoad (naturalAdd prExpectedDigest 24))
572 tail))))))))))))))))
573
574-- the hasher: an AF_ALG SHA-256 socket and the connection hashes go through
575def prHasherOpen =
576 (lambda unrestricted identity : Bytes .
577 (lambda unrestricted tail : (family NativePhysicalCommands) .
578 (phCall prSysSocket (phArgs3 (phImm prAddressFamilyAlg) (phImm prSocketSeqpacket) (phImm 0)) b"" (phStore prSlotAlg)
579 (phCall prSysBind (phArgs3 (phSlot prSlotAlg) phPayload (phImm prSockaddrAlgExtent)) prSockaddrAlg (phStore prSlotStatus)
580 (prAssertStatus identity 0
581 (phCall prSysAccept (phArgs3 (phSlot prSlotAlg) (phImm 0) (phImm 0)) b"" (phStore prSlotHash) tail))))))
582
583def prHasherClose =
584 (lambda unrestricted tail : (family NativePhysicalCommands) .
585 (prClose b"checkpoint-hash-close" prSlotHash (prClose b"checkpoint-alg-close" prSlotAlg tail)))
586
587-- every chunk of a file's payload, from `header` on, against the digests
588-- the file's header carries: the full ones (their count a state word or an
589-- immediate), then the tail when the contract has one (under `tailCount`)
590def prChunksCheck =
591 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
592 (lambda unrestricted fileSlot : Nat .
593 (lambda unrestricted fullCount : (family NativePhysicalOperand) .
594 (lambda unrestricted tailCount : (family NativePhysicalOperand) .
595 (lambda unrestricted tail : (family NativePhysicalCommands) .
596 (let unrestricted header = (checkpointEnvelopeHeaderBytes contract) in
597 (let unrestricted chunk = (checkpointEnvelopeContractChunk contract) in
598 (let unrestricted full = (checkpointEnvelopeFullChunks contract) in
599 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted fullCount)
600 (prChunkCheck fileSlot (prAffine header chunk) chunk (prAffine checkpointEnvelopeDigestsAt checkpointEnvelopeDigestBytes)
601 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
602 (phWhen (naturalNonzero (checkpointEnvelopeTailBytes contract))
603 (lambda unrestricted after : (family NativePhysicalCommands) .
604 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted tailCount)
605 (prChunkCheck fileSlot (phImm (naturalAdd header (naturalMultiply chunk full))) (checkpointEnvelopeTailBytes contract)
606 (phImm (naturalAdd checkpointEnvelopeDigestsAt (naturalMultiply checkpointEnvelopeDigestBytes full)))
607 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd) after))))
608 tail))))))))))))
609
610def prCheckpointValidate =
611 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
612 (lambda unrestricted tail : (family NativePhysicalCommands) .
613 (let unrestricted version = (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeVersionAt)) in
614 (phCall prSysPread (phArgs (phSlot prSlotCheckpointIn) (phState prCheckpointHeaderIn) (phImm checkpointEnvelopeDigestsAt) (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard
615 (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState prWordScratch) (phLoad (naturalAdd prStat prStatSize)) version)
616 (prAssertOneOf b"checkpoint-version" (phLoad prWordScratch) 0 (succ (checkpointEnvelopeFileBytes contract))
617 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted version)
618 (prExpectWords b"checkpoint-layout" prCheckpointHeaderIn (checkpointEnvelopeFixed contract) (naturalDivideUnchecked checkpointEnvelopeFixedBytes 8)
619 (prExpectWords b"checkpoint-schema" (naturalAdd prCheckpointHeaderIn checkpointEnvelopeSchemaAt) (dataBytesTakeValidated 32 (checkpointEnvelopeIdentityDigests contract)) 4
620 (prExpectWords b"checkpoint-learner" (naturalAdd prCheckpointHeaderIn checkpointEnvelopeLearnerAt) (dataBytesTakeValidated 32 (dataBytesDropValidated 32 (checkpointEnvelopeIdentityDigests contract))) 4
621 (prExpectWords b"checkpoint-data" (naturalAdd prCheckpointHeaderIn checkpointEnvelopeDataAt) (dataBytesTakeValidated 32 (dataBytesDropValidated 64 (checkpointEnvelopeIdentityDigests contract))) 4
622 (prExpectWords b"checkpoint-seed" (naturalAdd prCheckpointHeaderIn checkpointEnvelopeSeedAt) (dataBytesDropValidated 96 (checkpointEnvelopeIdentityDigests contract)) 4
623 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
624 (prHasherOpen b"checkpoint-hash-bind"
625 (prChunksCheck contract prSlotCheckpointIn (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeFullChunksAt)) version
626 (prHasherClose tail))))))))))))))))
627
628-- the input's extent, when the contract fixes it
629def prInputExtentCheck =
630 (lambda unrestricted input : (family NvidiaPlanHostInputContract) .
631 (lambda unrestricted tail : (family NativePhysicalCommands) .
632 (eliminate NvidiaPlanHostInputContract (lambda unrestricted current : (family NvidiaPlanHostInputContract) . (family NativePhysicalCommands)) input
633 (branch NvidiaPlanHostInputExact extent .
634 (prAssertEqual b"input-extent" (phLoad (naturalAdd prStat prStatSize)) (phImm extent) tail))
635 (branch NvidiaPlanHostInputStream . tail))))
636
637def prRequestOpen =
638 (lambda unrestricted input : (family NvidiaPlanHostInputContract) .
639 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
640 (lambda unrestricted tail : (family NativePhysicalCommands) .
641 (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) (constructor NativePhysicalOperand NativePhysicalProcessArgument (phWord 1)) (phImm 0)) b"" (phStore prSlotRequest)
642 (prFstat b"request-stat" prSlotRequest
643 (prAssertEqual b"request-length" (phLoad (naturalAdd prStat prStatSize)) (phImm textArtifactRequestEncodedLength)
644 (phCall phSysRead (phArgs3 (phSlot prSlotRequest) (phState prRequest) (phImm textArtifactRequestEncodedLength)) b"" (phStore prSlotStatus)
645 (prAssertStatus b"request-read" textArtifactRequestEncodedLength
646 (prExpectBytes b"request-magic" prRequest textArtifactRequestMagic
647 (prAssertEqual b"request-version" (phLoad (naturalAdd prRequest 8)) (phImm textArtifactRequestVersion)
648 (prAssertOneOf b"request-operation" (phLoad (naturalAdd prRequest 16)) textArtifactTrainOperationWord textArtifactPredictOperationWord
649 (prOpenPath 0 0 prSlotInput
650 (prOpenPath 1 0 prSlotCheckpointIn
651 (prOpenPath 3 prOpenWriteCreate prSlotPredictions
652 (prOpenPath 4 prOpenWriteCreate prSlotResult
653 (prFstat b"input-stat" prSlotInput
654 (prInputExtentCheck input
655 (prFstat b"checkpoint-stat" prSlotCheckpointIn
656 (prAssertOneOf b"checkpoint-truncated" (phLoad (naturalAdd prStat prStatSize)) 0 (checkpointEnvelopeFileBytes contract)
657 (prCheckpointValidate contract tail))))))))))))))))))))
658
659-- the paths the request names, by index
660def prCheckpointOutPath : Nat = 2
661def prCheckpointTemporaryPath : Nat = 5
662def prCheckpointDirectoryPath : Nat = 6
663
664-- A train request's checkpoint is written to its temporary, created new
665-- (a temporary a crashed run left is removed first) and positioned after
666-- the header.
667-- With one byte in one record, offset computation isolates the checked
668-- counter addition: the only possible rejection is completed + increment
669-- exceeding u64. The discarded offset is zero on success.
670def prCheckCounterAddition = (lambda unrestricted identity : Bytes . (lambda unrestricted counterAt : Nat .
671 (lambda unrestricted increment : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) .
672 (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeCyclicRecordOffsetRoutine
673 (phArgs (phState prWordScratch) (phLoad counterAt) (phImm increment) (phImm 1) (phImm 1) (phImm 0)) (phStore prSlotStatus))
674 (prAssertStatus identity 0 tail))))))
675def prCheckpointTemporary =
676 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
677 (lambda unrestricted tail : (family NativePhysicalCommands) .
678 (prCheckCounterAddition b"checkpoint-update-count-overflow"
679 (naturalAdd prCheckpointHeaderIn checkpointEnvelopeUpdatesAt) (checkpointEnvelopeContractUpdates contract)
680 (prCheckCounterAddition b"checkpoint-invocation-count-overflow"
681 (naturalAdd prCheckpointHeaderIn checkpointEnvelopeInvocationsAt) 1
682 (phCall prSysUnlink (phArgs3 (phState (prPath prCheckpointTemporaryPath)) (phImm 0) (phImm 0)) b"" phDiscard
683 (prOpenPath prCheckpointTemporaryPath prOpenReadWriteExclusive prSlotCheckpointOut
684 (phCall prSysLseek (phArgs3 (phSlot prSlotCheckpointOut) (phImm (checkpointEnvelopeHeaderBytes contract)) (phImm 0)) b"" (phStore prSlotStatus)
685 (prAssertStatus b"checkpoint-temporary" (checkpointEnvelopeHeaderBytes contract) tail))))))))
686
687-- a chunk of the written checkpoint hashed back from it, its digest written
688-- into the header
689def prDigestWrite =
690 (lambda unrestricted offset : (family NativePhysicalOperand) .
691 (lambda unrestricted extent : Nat .
692 (lambda unrestricted digestAt : (family NativePhysicalOperand) .
693 (lambda unrestricted tail : (family NativePhysicalCommands) .
694 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prSendOffset) offset)
695 (phCall prSysSendfile (phArgs (phSlot prSlotHash) (phSlot prSlotCheckpointOut) (phState prSendOffset) (phImm extent) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
696 (prAssertStatus b"checkpoint-readback" extent
697 (phCall phSysRead (phArgs3 (phSlot prSlotHash) (phState prDigest) (phImm checkpointEnvelopeDigestBytes)) b"" (phStore prSlotStatus)
698 (prAssertStatus b"checkpoint-readback-hash" checkpointEnvelopeDigestBytes
699 (phCall prSysPwrite (phArgs (phSlot prSlotCheckpointOut) (phState prDigest) (phImm checkpointEnvelopeDigestBytes) digestAt (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
700 (prAssertStatus b"checkpoint-digest-write" checkpointEnvelopeDigestBytes tail)))))))))))
701
702-- Publishing the checkpoint (a train request's; Checkpoint.Envelope), in
703-- stages: 1 the header -- the fixed fields, the update count and
704-- invocations after this invocation's, the identities; 2 each chunk's
705-- digest (hashed back from the temporary: the readback); 3 the data synced;
706-- 4 the temporary closed; 5 renamed over the output path; 6 the directory
707-- synced. Until the rename the output path holds what it held. A host
708-- runs all six; `prPublishCheckpointStages` stops after the first `stages`,
709-- which is how the publication is tested at every boundary
710-- (scripts/ci/checkpoint-envelope.sh).
711def prPublishStages : Nat = 6
712
713def prPublishCheckpointCounting =
714 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
715 (lambda unrestricted stages : Nat .
716 (lambda unrestricted updates : Nat .
717 (lambda unrestricted invocations : Nat .
718 (lambda unrestricted tail : (family NativePhysicalCommands) .
719 (let unrestricted header = (checkpointEnvelopeHeaderBytes contract) in
720 (let unrestricted chunk = (checkpointEnvelopeContractChunk contract) in
721 (let unrestricted full = (checkpointEnvelopeFullChunks contract) in
722 (let unrestricted stage = (lambda unrestricted index : Nat . (phWhen (naturalLessOrEqual index stages))) in
723 (stage 1
724 (lambda unrestricted after : (family NativePhysicalCommands) .
725 (phCopy prCheckpointHeaderOut (checkpointEnvelopeFixed contract)
726 (phCopy (naturalAdd prCheckpointHeaderOut checkpointEnvelopeSchemaAt) (checkpointEnvelopeIdentityDigests contract)
727 (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64
728 (phState (naturalAdd prCheckpointHeaderOut checkpointEnvelopeUpdatesAt))
729 (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeUpdatesAt))
730 (phImm updates))
731 (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64
732 (phState (naturalAdd prCheckpointHeaderOut checkpointEnvelopeInvocationsAt))
733 (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeInvocationsAt))
734 (phImm invocations))
735 (phCall prSysPwrite (phArgs (phSlot prSlotCheckpointOut) (phState prCheckpointHeaderOut) (phImm checkpointEnvelopeDigestsAt) (phImm 0) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
736 (prAssertStatus b"checkpoint-header-write" checkpointEnvelopeDigestsAt after)))))))
737 (stage 2
738 (lambda unrestricted after : (family NativePhysicalCommands) .
739 (prHasherOpen b"checkpoint-hash-bind"
740 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (phImm full))
741 (prDigestWrite (prAffine header chunk) chunk (prAffine checkpointEnvelopeDigestsAt checkpointEnvelopeDigestBytes)
742 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
743 (phWhen (naturalNonzero (checkpointEnvelopeTailBytes contract))
744 (prDigestWrite (phImm (naturalAdd header (naturalMultiply chunk full))) (checkpointEnvelopeTailBytes contract)
745 (phImm (naturalAdd checkpointEnvelopeDigestsAt (naturalMultiply checkpointEnvelopeDigestBytes full))))
746 (prHasherClose after)))))))
747 (stage 3
748 (lambda unrestricted after : (family NativePhysicalCommands) .
749 (phCall prSysFdatasync (phArgs3 (phSlot prSlotCheckpointOut) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
750 (prAssertStatus b"checkpoint-sync" 0 after)))
751 (stage 4
752 (lambda unrestricted after : (family NativePhysicalCommands) .
753 (prClose b"checkpoint-close" prSlotCheckpointOut after))
754 (stage 5
755 (lambda unrestricted after : (family NativePhysicalCommands) .
756 (phCall prSysRename (phArgs3 (phState (prPath prCheckpointTemporaryPath)) (phState (prPath prCheckpointOutPath)) (phImm 0)) b"" (phStore prSlotStatus)
757 (prAssertStatus b"checkpoint-rename" 0 after)))
758 (stage 6
759 (lambda unrestricted after : (family NativePhysicalCommands) .
760 (prOpenPath prCheckpointDirectoryPath prOpenDirectory prSlotCheckpointOut
761 (phCall prSysFsync (phArgs3 (phSlot prSlotCheckpointOut) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
762 (prAssertStatus b"checkpoint-directory-sync" 0
763 (prClose b"checkpoint-directory-close" prSlotCheckpointOut after)))))
764 tail)))))))))))))))
765
766-- an invocation's publication: its contract's updates, one invocation
767def prPublishCheckpointStages =
768 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
769 (lambda unrestricted stages : Nat .
770 (prPublishCheckpointCounting contract stages (checkpointEnvelopeContractUpdates contract) 1)))
771
772def prPublishCheckpoint =
773 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
774 (prPublishCheckpointStages contract prPublishStages))
775
776-- ---- 5. the recipes ----
777def prKindIndex =
778 (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) .
779 (naturalSaturatingSubtract (nativePhysicalEmbeddedComponentTag kind) 1))
780
781def prRecipeFills =
782 (lambda unrestricted fills : (family NvidiaPlanHostRecipeFills) .
783 (lambda unrestricted tail : (family NativePhysicalCommands) .
784 (eliminate NvidiaPlanHostRecipeFills
785 (lambda unrestricted current : (family NvidiaPlanHostRecipeFills) . (family NativePhysicalCommands))
786 fills
787 (branch NvidiaPlanHostRecipeFillsEnd . tail)
788 (branch NvidiaPlanHostRecipeFillsNext host tableExtent kind rest induction .
789 (nativeLaunchRecipeLoadOperands (phSlot prSlotExe) nvidiaPlanHostStaging
790 (phLoad (prDescriptorOffsetWord (prKindIndex kind))) (phLoad (prDescriptorLengthWord (prKindIndex kind)))
791 host tableExtent prSlotStatus phIdentity induction)))))
792
793-- ---- 6. the schedule ----
794def prFileSlot =
795 (lambda unrestricted file : (family NvidiaPlanHostFile) .
796 (eliminate NvidiaPlanHostFile (lambda unrestricted current : (family NvidiaPlanHostFile) . Nat) file
797 (branch NvidiaPlanHostInput . prSlotInput)
798 (branch NvidiaPlanHostCheckpointIn . prSlotCheckpointIn)
799 (branch NvidiaPlanHostCheckpointOut . prSlotCheckpointOut)
800 (branch NvidiaPlanHostPredictions . prSlotPredictions)
801 (branch NvidiaPlanHostResult . prSlotResult)))
802
803def prOrdinal = (lambda unrestricted gpPut : Nat . (naturalSaturatingSubtract gpPut 1))
804def prSemaphoreStride : Nat = 32
805
806def prStampAddress =
807 (lambda unrestricted gpPut : Nat .
808 (lambda unrestricted which : Nat .
809 (naturalAdd nvidiaPlanHostStaging (naturalAdd which (naturalMultiply nvidiaPlanHostTimestampRecord (prOrdinal gpPut))))))
810
811def prClock =
812 (lambda unrestricted destination : (family NativePhysicalOperand) .
813 (lambda unrestricted tail : (family NativePhysicalCommands) .
814 (phCall prSysClockGettime (phArgs3 (phImm prClockRealtime) destination (phImm 0)) b"" phDiscard tail)))
815
816def prStamp =
817 (lambda unrestricted gpPut : Nat .
818 (lambda unrestricted stride : Nat .
819 (lambda unrestricted which : Nat .
820 (lambda unrestricted tail : (family NativePhysicalCommands) .
821 (prClock (prAffine (prStampAddress gpPut which) (naturalMultiply nvidiaPlanHostTimestampRecord stride)) tail)))))
822
823def prSemaphoreHost =
824 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
825 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout
826 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
827 (phBufferHost sem))))
828
829-- One submission: stamp, fence, gpPut staged in the state and written to
830-- USERD and the doorbell rung with the channel's token by PlanHost's
831-- publication routine (store, SFENCE, store: a membarrier does not order
832-- the write-combined gpPut ahead of the doorbell), fence, wait for the
833-- submission's own semaphore slot, stamp.
834def prSubmit =
835 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
836 (lambda unrestricted gpPut : Nat .
837 (lambda unrestricted stride : Nat .
838 (lambda unrestricted tail : (family NativePhysicalCommands) .
839 (prStamp gpPut stride 0
840 (prFence
841 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prGPPut) (prAffine gpPut stride))
842 (phLoadToken
843 (prFence
844 (phPublishOperand (naturalAdd (phUSERDHost layout) nvidiaPlanHostUSERDGPPutOffset) (prAffine gpPut stride)
845 (prFence
846 (phNext (constructor NativePhysicalOperation NativePhysicalFenceWait
847 (prAffine (naturalAdd (prSemaphoreHost layout) (naturalMultiply prSemaphoreStride (prOrdinal gpPut))) (naturalMultiply prSemaphoreStride stride))
848 (phImm nvidiaPlanHostFenceValue) (phWord nvidiaPlanHostFenceMaximumPolls) (phWord nvidiaPlanHostFenceInterval))
849 (prStamp gpPut stride 16 tail)))))))))))))
850
851-- the ring the host writes entries into, and how many entries it has
852def prRingHost =
853 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
854 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout
855 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
856 (phBufferHost gpfifo))))
857
858def prRingEntries =
859 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
860 (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout
861 (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
862 (naturalSelect (phIsUVM lifecycle) nvidiaPlanHostUVMGPFIFOEntries nvidiaPlanHostDirectGPFIFOEntries))))
863
864-- The ring has a fixed mapped extent while the scheduler counts all issues.
865-- The cyclic-offset primitive checks the extent and wraps the ordinal before
866-- a write; its scratch word is dead after this command sequence.
867def prStoreRingEntry =
868 (lambda unrestricted ringBase : (family NativePhysicalOperand) .
869 (lambda unrestricted entries : Nat .
870 (lambda unrestricted ordinal : (family NativePhysicalOperand) .
871 (lambda unrestricted entry : (family NativePhysicalOperand) .
872 (lambda unrestricted tail : (family NativePhysicalCommands) .
873 (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine
874 nativeCyclicRecordOffsetRoutine
875 (phArgs (phState prWordScratch) ordinal (phImm 0)
876 (phImm entries) (phImm 8) (phImm 0))
877 (phStore prSlotStatus))
878 (prAssertStatus b"gpfifo-ring-offset" 0
879 (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64
880 (phState prWordScratch) (phLoad prWordScratch) ringBase)
881 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64
882 (phLoad prWordScratch) entry) tail)))))))))
883
884-- USERD GP_PUT names the next slot in the configured GPFIFO ring. The issue
885-- count stays monotonic for telemetry and token cursors, but the word sent to
886-- USERD must wrap with the ring. At issue 32768 on the 3090's 32768-entry
887-- UVM ring, publishing 32768 left the GPU idle while the host waited for its
888-- semaphore. The cyclic primitive already proves the bounded modulo before
889-- it touches the scratch word; a failed computation cannot publish a put.
890def prWrapGPFIFOCount =
891 (lambda unrestricted entries : Nat .
892 (lambda unrestricted issued : (family NativePhysicalOperand) .
893 (lambda unrestricted tail : (family NativePhysicalCommands) .
894 (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine
895 nativeCyclicRecordOffsetRoutine
896 (phArgs (phState prWordScratch) issued (phImm 0)
897 (phImm entries) (phImm 1) (phImm 0))
898 (phStore prSlotStatus))
899 (prAssertStatus b"gpfifo-put-wrap" 0 tail)))))
900
901-- A submission of the plan issued again: its entry into the ring at
902-- ordinal gpPut - 1 and its semaphore slot (both releases) cleared, then
903-- the ring entry published and the slot awaited as in prSubmit. The piece's
904-- pushbuffer releases the same slot at every issue; the slot is cleared
905-- only after the issue before was awaited, so the wait sees this issue's
906-- release. The scheduler's issue count is monotonic; the USERD GP_PUT and
907-- mapped ring address both wrap at the ABI's entry count. The cyclic-offset
908-- routine bounds that write on every iteration instead of extending the
909-- mapping as a long training run advances past the first turn of the ring.
910def prReissue =
911 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
912 (lambda unrestricted gpPut : Nat . (lambda unrestricted stride : Nat .
913 (lambda unrestricted piece : Nat . (lambda unrestricted pieceStride : Nat .
914 (lambda unrestricted entry : Nat . (lambda unrestricted entryStride : Nat .
915 (lambda unrestricted tail : (family NativePhysicalCommands) .
916 (let unrestricted slot = (naturalAdd (prSemaphoreHost layout) (naturalMultiply prSemaphoreStride piece)) in
917 (let unrestricted slotStride = (naturalMultiply prSemaphoreStride pieceStride) in
918 (prStamp gpPut stride 0
919 (prStoreRingEntry (phImm (prRingHost layout))
920 (prRingEntries layout) (prAffine (prOrdinal gpPut) stride)
921 (prAffine entry entryStride)
922 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (prAffine slot slotStride) (phImm 0))
923 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (prAffine (naturalAdd slot 16) slotStride) (phImm 0))
924 (prFence
925 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prGPPut) (prAffine gpPut stride))
926 (phLoadToken
927 (prFence
928 (prWrapGPFIFOCount (prRingEntries layout) (prAffine gpPut stride)
929 (phPublishOperand (naturalAdd (phUSERDHost layout) nvidiaPlanHostUSERDGPPutOffset) (phLoad prWordScratch)
930 (prFence
931 (phNext (constructor NativePhysicalOperation NativePhysicalFenceWait
932 (prAffine slot slotStride)
933 (phImm nvidiaPlanHostFenceValue) (phWord nvidiaPlanHostFenceMaximumPolls) (phWord nvidiaPlanHostFenceInterval))
934 (prStamp gpPut stride 16 tail)))))))))))))))))))))))
935
936-- a list of commands run before `tail`
937def prSplice =
938 (lambda unrestricted commands : (family NativePhysicalCommands) .
939 (lambda unrestricted tail : (family NativePhysicalCommands) .
940 (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . (family NativePhysicalCommands)) commands
941 (branch NativePhysicalCommandsEnd . tail)
942 (branch NativePhysicalCommandsNext head rest induction . (constructor NativePhysicalCommands NativePhysicalCommandsNext head induction)))))
943
944-- `destination` = `source` x `scale` (words of the state), by doubling and
945-- adding over the bits of the scale, low bit first; `source` is consumed
946-- (it ends doubled once per bit)
947def prScaleBits =
948 (lambda unrestricted destination : Nat .
949 (lambda unrestricted source : Nat .
950 (lambda unrestricted scale : Nat .
951 (lambda unrestricted tail : (family NativePhysicalCommands) .
952 (app (app
953 (nat-eliminate
954 (lambda unrestricted current : Nat . (pi unrestricted remaining : Nat . (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands))))
955 (lambda unrestricted remaining : Nat . (lambda unrestricted after : (family NativePhysicalCommands) . after))
956 (lambda unrestricted predecessor : Nat .
957 (lambda unrestricted induction : (pi unrestricted remaining : Nat . (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands))) .
958 (lambda unrestricted remaining : Nat . (lambda unrestricted after : (family NativePhysicalCommands) .
959 (phWhen (naturalNonzero remaining)
960 (lambda unrestricted next : (family NativePhysicalCommands) .
961 (phWhen (naturalModuloUnchecked remaining 2)
962 (lambda unrestricted doubled : (family NativePhysicalCommands) .
963 (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState destination) (phLoad destination) (phLoad source)) doubled))
964 (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState source) (phLoad source) (phLoad source))
965 (induction (naturalDivideUnchecked remaining 2) next))))
966 after)))))
967 64)
968 scale) tail)))))
969
970-- the cursor: base + the checkpoint read's completed updates x scale. A
971-- checkpoint may be published partway through an invocation, so invocation
972-- count cannot locate the next token window after a restart.
973def prCursorFromCheckpoint =
974 (lambda unrestricted base : Nat .
975 (lambda unrestricted scale : Nat .
976 (lambda unrestricted tail : (family NativePhysicalCommands) .
977 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prCursor) (phImm base))
978 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prCursorScratch)
979 (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeUpdatesAt)))
980 (prScaleBits prCursor prCursorScratch scale tail))))))
981
982def prWriteFrom =
983 (lambda unrestricted identity : Bytes .
984 (lambda unrestricted file : (family NvidiaPlanHostFile) .
985 (lambda unrestricted source : (family NativePhysicalOperand) .
986 (lambda unrestricted extent : Nat .
987 (lambda unrestricted tail : (family NativePhysicalCommands) .
988 (phCall phSysWrite (phArgs3 (phSlot (prFileSlot file)) source (phImm extent)) b"" (phStore prSlotStatus)
989 (prAssertStatus identity extent tail)))))))
990
991-- the status block appended to a result: PlanHost's RM status slots, then
992-- its UVM status slots
993def prStatusBlockCommands =
994 (lambda unrestricted tail : (family NativePhysicalCommands) .
995 (phCopyStateToState prStatusBlock (phRMStatusSlot 0) 80
996 (phCopyStateToState (naturalAdd prStatusBlock 80) phUVMStatusRecord 80 tail)))
997
998-- how far a file's offsets move: a checkpoint's payload follows its header
999def prFileShift =
1000 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
1001 (lambda unrestricted file : (family NvidiaPlanHostFile) .
1002 (eliminate NvidiaPlanHostFile (lambda unrestricted current : (family NvidiaPlanHostFile) . Nat) file
1003 (branch NvidiaPlanHostInput . 0)
1004 (branch NvidiaPlanHostCheckpointIn . (checkpointEnvelopeHeaderBytes contract))
1005 (branch NvidiaPlanHostCheckpointOut . (checkpointEnvelopeHeaderBytes contract))
1006 (branch NvidiaPlanHostPredictions . 0)
1007 (branch NvidiaPlanHostResult . 0))))
1008
1009-- 1 for the checkpoint being written
1010def prIsCheckpointOut =
1011 (lambda unrestricted file : (family NvidiaPlanHostFile) .
1012 (naturalEqual (prFileSlot file) prSlotCheckpointOut))
1013
1014-- Copy through a state scratch word: host/device mappings are not state
1015-- offsets, and the typed command language keeps that distinction explicit.
1016def prAssertMappedWord = (lambda unrestricted identity : Bytes . (lambda unrestricted host : Nat .
1017 (lambda unrestricted expected : Nat . (lambda unrestricted after : (family NativePhysicalCommands) .
1018 (phCopyMappedToState host prExpected 8
1019 (prAssertEqual identity (phLoad prExpected) (phImm expected) after))))))
1020
1021-- Arithmetic is checked before pread: a zero record count, counter overflow
1022-- or file offset overflow never becomes a successful read from another row.
1023def prReadCyclic = (lambda unrestricted host : Nat . (lambda unrestricted extent : Nat .
1024 (lambda unrestricted offset : Nat . (lambda unrestricted recordBytes : Nat . (lambda unrestricted count : Nat .
1025 (lambda unrestricted index : Nat . (lambda unrestricted stride : Nat .
1026 (lambda unrestricted tail : (family NativePhysicalCommands) .
1027 (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeCyclicRecordOffsetRoutine
1028 (phArgs (phState prWordScratch) (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeUpdatesAt))
1029 (prAffine index stride) (phImm count) (phImm recordBytes) (phImm offset)) (phStore prSlotStatus))
1030 (prAssertStatus b"cyclic-record-offset" 0
1031 (phCall prSysPread (phArgs (phSlot prSlotInput) (phImm host) (phImm extent)
1032 (phLoad prWordScratch) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
1033 (prAssertStatus b"cyclic-read-extent" extent tail))))))))))))
1034
1035-- A single bounded sendfile must transfer the entire admitted input. A
1036-- partial transfer rejects by name; no prefix hash is accepted as its identity.
1037-- The enclosing request already checked the input's exact extent. This
1038-- content binding is additional to the checkpoint's schema/data-policy hash.
1039-- A resumed invocation compares the digest already in its checkpoint; an
1040-- explicitly admitted next invocation hashes its new input and writes that
1041-- digest into the next checkpoint. The latter requires its caller to assert
1042-- the completed-update boundary and retain the prior input in the run ledger.
1043def prInputIdentityComparisonCount =
1044 (lambda unrestricted comparePrevious : Nat .
1045 (nat-eliminate
1046 (lambda unrestricted flag : Nat . (family NativePhysicalOperand))
1047 (phImm 0)
1048 (lambda unrestricted predecessor : Nat .
1049 (lambda unrestricted ignored : (family NativePhysicalOperand) .
1050 (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeVersionAt))))
1051 comparePrevious))
1052def prBindInputIdentityWith = (lambda unrestricted comparePrevious : Nat .
1053 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
1054 (lambda unrestricted offset : Nat . (lambda unrestricted inputExtent : Nat .
1055 (lambda unrestricted tail : (family NativePhysicalCommands) .
1056 (prHasherOpen b"input-identity-hash-bind"
1057 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prSendOffset) (phImm 0))
1058 (phCall prSysSendfile (phArgs (phSlot prSlotHash) (phSlot prSlotInput) (phState prSendOffset)
1059 (phImm inputExtent) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
1060 (prAssertStatus b"input-identity-read" inputExtent
1061 (phCall phSysRead (phArgs3 (phSlot prSlotHash) (phState prInputIdentity) (phImm checkpointEnvelopeDigestBytes)) b"" (phStore prSlotStatus)
1062 (prAssertStatus b"input-identity-hash" checkpointEnvelopeDigestBytes
1063 (prHasherClose
1064 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted
1065 (prInputIdentityComparisonCount comparePrevious))
1066 (phCall prSysPread (phArgs (phSlot prSlotCheckpointIn) (phState prExpectedDigest)
1067 (phImm checkpointEnvelopeDigestBytes) (phImm (naturalAdd (checkpointEnvelopeHeaderBytes contract) offset))
1068 (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
1069 (prAssertStatus b"input-identity-checkpoint-read" checkpointEnvelopeDigestBytes
1070 (prAssertEqual b"input-identity-changed" (phLoad prInputIdentity) (phLoad prExpectedDigest)
1071 (prAssertEqual b"input-identity-changed" (phLoad (naturalAdd prInputIdentity 8)) (phLoad (naturalAdd prExpectedDigest 8))
1072 (prAssertEqual b"input-identity-changed" (phLoad (naturalAdd prInputIdentity 16)) (phLoad (naturalAdd prExpectedDigest 16))
1073 (prAssertEqual b"input-identity-changed" (phLoad (naturalAdd prInputIdentity 24)) (phLoad (naturalAdd prExpectedDigest 24))
1074 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd) tail))))))))))))))))))))
1075def prBindInputIdentity = (prBindInputIdentityWith 1)
1076def prBindNextInputIdentity = (prBindInputIdentityWith 0)
1077
1078def prSteps =
1079 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1080 (lambda unrestricted submissionCount : Nat .
1081 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
1082 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1083 (lambda unrestricted final : (family NativePhysicalCommands) .
1084 (app
1085 (eliminate NvidiaPlanHostSteps
1086 (lambda unrestricted current : (family NvidiaPlanHostSteps) . (pi unrestricted rest : (family NativePhysicalCommands) . (family NativePhysicalCommands)))
1087 steps
1088 (branch NvidiaPlanHostStepsEnd . (lambda unrestricted rest : (family NativePhysicalCommands) . rest))
1089 (branch NvidiaPlanHostStepSubmit gpPut stride tail induction .
1090 (lambda unrestricted rest : (family NativePhysicalCommands) . (prSubmit layout gpPut stride (induction rest))))
1091 (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction .
1092 (lambda unrestricted rest : (family NativePhysicalCommands) .
1093 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBegin (phWord count))
1094 (bodyInduction
1095 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
1096 (tailInduction rest))))))
1097 (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction .
1098 (lambda unrestricted rest : (family NativePhysicalCommands) .
1099 (phCall prSysPread (phArgs (phSlot (prFileSlot file)) (phImm host) (phImm extent) (prAffine (naturalAdd offset (prFileShift contract file)) stride) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
1100 (phWhen (naturalIsZero tolerateEmpty) (prAssertStatus b"read-extent" extent)
1101 (phWhen tolerateEmpty (prAssertOneOf b"read-extent" prStatus 0 extent)
1102 (induction rest))))))
1103 (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) .
1104 (prReadCyclic host extent offset recordBytes count index stride (induction rest))))
1105 (branch NvidiaPlanHostStepWrite file host extent tail induction .
1106 (lambda unrestricted rest : (family NativePhysicalCommands) .
1107 (prWriteFrom b"write-extent" file (phImm host) extent (induction rest))))
1108 (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction .
1109 (lambda unrestricted rest : (family NativePhysicalCommands) .
1110 (phCall prSysPwrite (phArgs (phSlot (prFileSlot file)) (phImm host) (phImm extent) (phImm (naturalAdd offset (prFileShift contract file))) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
1111 (prAssertStatus b"write-extent" extent (induction rest)))))
1112 (branch NvidiaPlanHostStepWriteStat file tail induction .
1113 (lambda unrestricted rest : (family NativePhysicalCommands) .
1114 (prWriteFrom b"write-stat" file (phState prStat) prStatExtent (induction rest))))
1115 (branch NvidiaPlanHostStepWriteStatus file tail induction .
1116 (lambda unrestricted rest : (family NativePhysicalCommands) .
1117 (prStatusBlockCommands (prWriteFrom b"write-status" file (phState prStatusBlock) prStatusBlockExtent (induction rest)))))
1118 (branch NvidiaPlanHostStepWriteTimestamps file tail induction .
1119 (lambda unrestricted rest : (family NativePhysicalCommands) .
1120 (prWriteFrom b"write-timestamps" file (phImm nvidiaPlanHostStaging) (naturalMultiply nvidiaPlanHostTimestampRecord submissionCount) (induction rest))))
1121 (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction .
1122 (lambda unrestricted rest : (family NativePhysicalCommands) .
1123 (phCopyMappedToState host (naturalAdd prStat statOffset) extent (induction rest))))
1124 (branch NvidiaPlanHostStepStamp gpPut stride which tail induction .
1125 (lambda unrestricted rest : (family NativePhysicalCommands) . (prStamp gpPut stride which (induction rest))))
1126 (branch NvidiaPlanHostStepFill host payload tail induction .
1127 (lambda unrestricted rest : (family NativePhysicalCommands) . (phFill host payload (induction rest))))
1128 (branch NvidiaPlanHostStepAssertWord identity host expected tail induction .
1129 (lambda unrestricted rest : (family NativePhysicalCommands) .
1130 (prAssertMappedWord identity host expected (induction rest))))
1131 (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prBindInputIdentity contract offset inputExtent (induction rest))))
1132 (branch NvidiaPlanHostStepWriteInputIdentity tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) .
1133 (prWriteFrom b"input-identity-write" (constructor NvidiaPlanHostFile NvidiaPlanHostCheckpointOut)
1134 (phState prInputIdentity) checkpointEnvelopeDigestBytes (induction rest))))
1135 (branch NvidiaPlanHostStepBeginCheckpoint tail induction .
1136 (lambda unrestricted rest : (family NativePhysicalCommands) .
1137 (prCheckpointTemporary contract (induction rest))))
1138 (branch NvidiaPlanHostStepOperation tail induction .
1139 (lambda unrestricted rest : (family NativePhysicalCommands) .
1140 (phNext (constructor NativePhysicalOperation NativePhysicalSystemCall (phLoad (naturalAdd prRequest 16)) (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard)
1141 (prCheckpointTemporary contract (induction rest)))))
1142 (branch NvidiaPlanHostStepSync file tail induction .
1143 (lambda unrestricted rest : (family NativePhysicalCommands) .
1144 (phCall prSysFsync (phArgs3 (phSlot (prFileSlot file)) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
1145 (prAssertStatus b"sync" 0 (induction rest)))))
1146 (branch NvidiaPlanHostStepDataSync file tail induction .
1147 (lambda unrestricted rest : (family NativePhysicalCommands) .
1148 (phCall prSysFdatasync (phArgs3 (phSlot (prFileSlot file)) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
1149 (prAssertStatus b"sync" 0 (induction rest)))))
1150 (branch NvidiaPlanHostStepClose file tail induction .
1151 (lambda unrestricted rest : (family NativePhysicalCommands) .
1152 (nat-eliminate (lambda unrestricted publishing : Nat . (family NativePhysicalCommands))
1153 (prClose b"close" (prFileSlot file) (induction rest))
1154 (lambda unrestricted q : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) .
1155 (prPublishCheckpoint contract (phTelemetry prTelemetryPublished b"request-host:checkpoint-published" (induction rest)))))
1156 (prIsCheckpointOut file))))
1157 (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction .
1158 (lambda unrestricted rest : (family NativePhysicalCommands) .
1159 (prReissue layout gpPut stride piece pieceStride entry entryStride (induction rest))))
1160 (branch NvidiaPlanHostStepCommands commands tail induction .
1161 (lambda unrestricted rest : (family NativePhysicalCommands) . (prSplice commands (induction rest))))
1162 (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction .
1163 (lambda unrestricted rest : (family NativePhysicalCommands) . (prCursorFromCheckpoint base scale (induction rest))))
1164 (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction .
1165 (lambda unrestricted rest : (family NativePhysicalCommands) .
1166 (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState prCursorOffset) (phLoad prCursor) (phImm delta))
1167 (phCall prSysPread (phArgs (phSlot (prFileSlot file)) (phImm host) (phImm extent) (phLoad prCursorOffset) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
1168 (prAssertStatus b"stream-read" extent (induction rest))))))
1169 (branch NvidiaPlanHostStepCursorAdvance bytes tail induction .
1170 (lambda unrestricted rest : (family NativePhysicalCommands) .
1171 (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState prCursor) (phLoad prCursor) (phImm bytes)) (induction rest))))
1172 (branch NvidiaPlanHostStepCheckpointBegin tail induction .
1173 (lambda unrestricted rest : (family NativePhysicalCommands) . (prCheckpointTemporary contract (induction rest))))
1174 (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction .
1175 (lambda unrestricted rest : (family NativePhysicalCommands) .
1176 (prPublishCheckpointCounting contract prPublishStages updates invocations (induction rest)))))
1177 final))))))
1178
1179-- The number of submissions a schedule issues, for the pairing's contract
1180-- against its plan's submission count.
1181def nvidiaPlanHostStepSubmissions =
1182 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1183 (eliminate NvidiaPlanHostSteps
1184 (lambda unrestricted current : (family NvidiaPlanHostSteps) . Nat)
1185 steps
1186 (branch NvidiaPlanHostStepsEnd . 0)
1187 (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . (naturalAdd 1 induction))
1188 (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . (naturalAdd (naturalMultiply count bodyInduction) tailInduction))
1189 (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . induction)
1190 (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . induction)
1191 (branch NvidiaPlanHostStepWrite file host extent tail induction . induction)
1192 (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . induction)
1193 (branch NvidiaPlanHostStepWriteStat file tail induction . induction)
1194 (branch NvidiaPlanHostStepWriteStatus file tail induction . induction)
1195 (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction)
1196 (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction)
1197 (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction)
1198 (branch NvidiaPlanHostStepFill host payload tail induction . induction)
1199 (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction)
1200 (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . induction)
1201 (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction)
1202 (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction)
1203 (branch NvidiaPlanHostStepOperation tail induction . induction)
1204 (branch NvidiaPlanHostStepSync file tail induction . induction)
1205 (branch NvidiaPlanHostStepDataSync file tail induction . induction)
1206 (branch NvidiaPlanHostStepClose file tail induction . induction)
1207 (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . (naturalAdd 1 induction))
1208 (branch NvidiaPlanHostStepCommands commands tail induction . induction)
1209 (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction)
1210 (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . induction)
1211 (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction)
1212 (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction)
1213 (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction)))
1214
1215-- The bytes a schedule moves through a file, for the pairing's contract
1216-- against its checkpoint extent: reads of a file, or writes of it.
1217def nvidiaPlanHostStepBytesRead =
1218 (lambda unrestricted which : (family NvidiaPlanHostFile) .
1219 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1220 (eliminate NvidiaPlanHostSteps
1221 (lambda unrestricted current : (family NvidiaPlanHostSteps) . Nat)
1222 steps
1223 (branch NvidiaPlanHostStepsEnd . 0)
1224 (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction)
1225 (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . (naturalAdd (naturalMultiply count bodyInduction) tailInduction))
1226 (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction .
1227 (naturalAdd (naturalMultiply (naturalEqual (prFileSlot file) (prFileSlot which)) extent) induction))
1228 (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (naturalAdd (naturalMultiply (naturalEqual prSlotInput (prFileSlot which)) extent) induction))
1229 (branch NvidiaPlanHostStepWrite file host extent tail induction . induction)
1230 (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . induction)
1231 (branch NvidiaPlanHostStepWriteStat file tail induction . induction)
1232 (branch NvidiaPlanHostStepWriteStatus file tail induction . induction)
1233 (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction)
1234 (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction)
1235 (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction)
1236 (branch NvidiaPlanHostStepFill host payload tail induction . induction)
1237 (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction)
1238 (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . (naturalAdd (naturalMultiply (naturalEqual prSlotCheckpointIn (prFileSlot which)) checkpointEnvelopeDigestBytes) induction))
1239 (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction)
1240 (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction)
1241 (branch NvidiaPlanHostStepOperation tail induction . induction)
1242 (branch NvidiaPlanHostStepSync file tail induction . induction)
1243 (branch NvidiaPlanHostStepDataSync file tail induction . induction)
1244 (branch NvidiaPlanHostStepClose file tail induction . induction)
1245 (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . induction)
1246 (branch NvidiaPlanHostStepCommands commands tail induction . induction)
1247 (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction)
1248 (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . (naturalAdd (naturalMultiply (naturalEqual (prFileSlot file) (prFileSlot which)) extent) induction))
1249 (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction)
1250 (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction)
1251 (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction))))
1252
1253def nvidiaPlanHostStepBytesWritten =
1254 (lambda unrestricted which : (family NvidiaPlanHostFile) .
1255 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1256 (eliminate NvidiaPlanHostSteps
1257 (lambda unrestricted current : (family NvidiaPlanHostSteps) . Nat)
1258 steps
1259 (branch NvidiaPlanHostStepsEnd . 0)
1260 (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction)
1261 (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . (naturalAdd (naturalMultiply count bodyInduction) tailInduction))
1262 (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . induction)
1263 (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . induction)
1264 (branch NvidiaPlanHostStepWrite file host extent tail induction .
1265 (naturalAdd (naturalMultiply (naturalEqual (prFileSlot file) (prFileSlot which)) extent) induction))
1266 (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction .
1267 (naturalAdd (naturalMultiply (naturalEqual (prFileSlot file) (prFileSlot which)) extent) induction))
1268 (branch NvidiaPlanHostStepWriteStat file tail induction . induction)
1269 (branch NvidiaPlanHostStepWriteStatus file tail induction . induction)
1270 (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction)
1271 (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction)
1272 (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction)
1273 (branch NvidiaPlanHostStepFill host payload tail induction . induction)
1274 (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction)
1275 (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . induction)
1276 (branch NvidiaPlanHostStepWriteInputIdentity tail induction . (naturalAdd (naturalMultiply (naturalEqual prSlotCheckpointOut (prFileSlot which)) checkpointEnvelopeDigestBytes) induction))
1277 (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction)
1278 (branch NvidiaPlanHostStepOperation tail induction . induction)
1279 (branch NvidiaPlanHostStepSync file tail induction . induction)
1280 (branch NvidiaPlanHostStepDataSync file tail induction . induction)
1281 (branch NvidiaPlanHostStepClose file tail induction . induction)
1282 (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . induction)
1283 (branch NvidiaPlanHostStepCommands commands tail induction . induction)
1284 (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction)
1285 (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . induction)
1286 (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction)
1287 (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction)
1288 (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction))))
1289
1290-- ---- the schedule, unrolled ----
1291-- The steps as they run: every repeat body once per iteration, its
1292-- loop-affine operands (gpPut, stamps, file offsets) at that iteration, so
1293-- no stride and no repeat remains. What the certificate below and a
1294-- pairing's contracts walk.
1295def prAt =
1296 (lambda unrestricted base : Nat . (lambda unrestricted stride : Nat . (lambda unrestricted iteration : Nat .
1297 (naturalAdd base (naturalMultiply stride iteration)))))
1298
1299def nvidiaPlanHostStepsUnrolled =
1300 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1301 (app (app
1302 (eliminate NvidiaPlanHostSteps
1303 (lambda unrestricted current : (family NvidiaPlanHostSteps) . (pi unrestricted iteration : Nat . (pi unrestricted rest : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps))))
1304 steps
1305 (branch NvidiaPlanHostStepsEnd . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . rest)))
1306 (branch NvidiaPlanHostStepSubmit gpPut stride tail induction .
1307 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1308 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSubmit (prAt gpPut stride iteration) 0 (induction iteration rest)))))
1309 (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction .
1310 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1311 (app
1312 (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted after : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps)))
1313 (lambda unrestricted after : (family NvidiaPlanHostSteps) . after)
1314 (lambda unrestricted inner : Nat . (lambda unrestricted earlier : (pi unrestricted after : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps)) .
1315 (lambda unrestricted after : (family NvidiaPlanHostSteps) . (earlier (bodyInduction inner after)))))
1316 count)
1317 (tailInduction iteration rest)))))
1318 (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction .
1319 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1320 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRead file host extent (prAt offset stride iteration) 0 tolerateEmpty (induction iteration rest)))))
1321 (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1322 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReadCyclic host extent offset recordBytes count
1323 (prAt index stride iteration) 0 (induction iteration rest)))))
1324 (branch NvidiaPlanHostStepWrite file host extent tail induction .
1325 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1326 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWrite file host extent (induction iteration rest)))))
1327 (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction .
1328 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1329 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteAt file host extent offset (induction iteration rest)))))
1330 (branch NvidiaPlanHostStepWriteStat file tail induction .
1331 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1332 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteStat file (induction iteration rest)))))
1333 (branch NvidiaPlanHostStepWriteStatus file tail induction .
1334 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1335 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteStatus file (induction iteration rest)))))
1336 (branch NvidiaPlanHostStepWriteTimestamps file tail induction .
1337 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1338 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteTimestamps file (induction iteration rest)))))
1339 (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction .
1340 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1341 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRecordStat host statOffset extent (induction iteration rest)))))
1342 (branch NvidiaPlanHostStepStamp gpPut stride which tail induction .
1343 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1344 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepStamp (prAt gpPut stride iteration) 0 which (induction iteration rest)))))
1345 (branch NvidiaPlanHostStepFill host payload tail induction .
1346 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1347 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepFill host payload (induction iteration rest)))))
1348 (branch NvidiaPlanHostStepAssertWord identity host expected tail induction .
1349 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1350 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepAssertWord identity host expected (induction iteration rest)))))
1351 (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1352 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBindInputIdentity offset inputExtent (induction iteration rest)))))
1353 (branch NvidiaPlanHostStepWriteInputIdentity tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1354 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteInputIdentity (induction iteration rest)))))
1355 (branch NvidiaPlanHostStepBeginCheckpoint tail induction .
1356 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1357 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBeginCheckpoint (induction iteration rest)))))
1358 (branch NvidiaPlanHostStepOperation tail induction .
1359 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1360 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepOperation (induction iteration rest)))))
1361 (branch NvidiaPlanHostStepSync file tail induction .
1362 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1363 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSync file (induction iteration rest)))))
1364 (branch NvidiaPlanHostStepDataSync file tail induction .
1365 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1366 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepDataSync file (induction iteration rest)))))
1367 (branch NvidiaPlanHostStepClose file tail induction .
1368 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1369 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepClose file (induction iteration rest)))))
1370 (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction .
1371 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1372 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReissue (prAt gpPut stride iteration) 0 (prAt piece pieceStride iteration) 0
1373 (prAt entry entryStride iteration) 0 (induction iteration rest)))))
1374 (branch NvidiaPlanHostStepCommands commands tail induction .
1375 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1376 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCommands commands (induction iteration rest)))))
1377 (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction .
1378 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1379 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCursorFromCheckpoint base scale (induction iteration rest)))))
1380 (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction .
1381 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1382 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReadAtCursor file host extent delta (induction iteration rest)))))
1383 (branch NvidiaPlanHostStepCursorAdvance bytes tail induction .
1384 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1385 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCursorAdvance bytes (induction iteration rest)))))
1386 (branch NvidiaPlanHostStepCheckpointBegin tail induction .
1387 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1388 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointBegin (induction iteration rest)))))
1389 (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction .
1390 (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
1391 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointPublish updates invocations (induction iteration rest))))))
1392 0) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))
1393
1394-- ---- the schedule's certificate ----
1395-- What Runtime.ArenaCertificate's schedule certificate sees of an unrolled
1396-- schedule: a file read or a fill writes host memory, a file write or a
1397-- recorded word reads it, a submission is awaited at its gpPut (every
1398-- submission is waited on its own semaphore slot before the host goes on),
1399-- and a stamp observes the submission it names. The status, statistics and
1400-- timestamp writes read PlanHost's own state, not the arena.
1401def prEvent =
1402 (lambda unrestricted event : (family ArenaEvent) .
1403 (lambda unrestricted rest : (family ArenaEvents) .
1404 (constructor ArenaEvents ArenaEventsNext event rest)))
1405
1406def nvidiaPlanHostStepEvents =
1407 (lambda unrestricted unrolled : (family NvidiaPlanHostSteps) .
1408 (eliminate NvidiaPlanHostSteps
1409 (lambda unrestricted current : (family NvidiaPlanHostSteps) . (family ArenaEvents))
1410 unrolled
1411 (branch NvidiaPlanHostStepsEnd . (constructor ArenaEvents ArenaEventsEnd))
1412 (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . (prEvent (constructor ArenaEvent ArenaAwait gpPut) induction))
1413 (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . tailInduction)
1414 (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction .
1415 (prEvent (constructor ArenaEvent ArenaHostWrite host extent) induction))
1416 (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (prEvent (constructor ArenaEvent ArenaHostWrite host extent) induction))
1417 (branch NvidiaPlanHostStepWrite file host extent tail induction .
1418 (prEvent (constructor ArenaEvent ArenaHostRead host extent) induction))
1419 (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction .
1420 (prEvent (constructor ArenaEvent ArenaHostRead host extent) induction))
1421 (branch NvidiaPlanHostStepWriteStat file tail induction . induction)
1422 (branch NvidiaPlanHostStepWriteStatus file tail induction . induction)
1423 (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction)
1424 (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction .
1425 (prEvent (constructor ArenaEvent ArenaHostRead host extent) induction))
1426 (branch NvidiaPlanHostStepStamp gpPut stride which tail induction .
1427 (prEvent (constructor ArenaEvent ArenaObserve gpPut) induction))
1428 (branch NvidiaPlanHostStepFill host payload tail induction .
1429 (prEvent (constructor ArenaEvent ArenaHostWrite host (bytes-length payload)) induction))
1430 (branch NvidiaPlanHostStepAssertWord identity host expected tail induction .
1431 (prEvent (constructor ArenaEvent ArenaHostRead host 8) induction))
1432 (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . induction)
1433 (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction)
1434 (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction)
1435 (branch NvidiaPlanHostStepOperation tail induction . induction)
1436 (branch NvidiaPlanHostStepSync file tail induction . induction)
1437 (branch NvidiaPlanHostStepDataSync file tail induction . induction)
1438 (branch NvidiaPlanHostStepClose file tail induction . induction)
1439 (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . (prEvent (constructor ArenaEvent ArenaAwait gpPut) induction))
1440 (branch NvidiaPlanHostStepCommands commands tail induction . induction)
1441 (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction)
1442 (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . (prEvent (constructor ArenaEvent ArenaHostWrite host extent) induction))
1443 (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction)
1444 (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction)
1445 (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction)))
1446
1447-- 1 when every submission of the plan is awaited, in order, each at a
1448-- generation of its own, and no staged range is overwritten, read back or
1449-- left unconsumed (Runtime.ArenaCertificate.arenaScheduleCertificate)
1450def nvidiaPlanHostScheduleCertified =
1451 (lambda unrestricted submissionCount : Nat .
1452 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1453 (arenaScheduleCertificate submissionCount (nvidiaPlanHostStepEvents (nvidiaPlanHostStepsUnrolled steps)))))
1454
1455-- 1 when the reads of a file, as they run, take it in order and whole: each
1456-- starts where the one before ended, the first at 0, the last ending at the
1457-- file's extent. (A byte count alone admits a chunk read twice and another
1458-- never.)
1459def nvidiaPlanHostFileReadsTile =
1460 (lambda unrestricted which : (family NvidiaPlanHostFile) .
1461 (lambda unrestricted fileExtent : Nat .
1462 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1463 (app
1464 (eliminate NvidiaPlanHostSteps
1465 (lambda unrestricted current : (family NvidiaPlanHostSteps) . (pi unrestricted next : Nat . Nat))
1466 (nvidiaPlanHostStepsUnrolled steps)
1467 (branch NvidiaPlanHostStepsEnd . (lambda unrestricted next : Nat . (naturalEqual next fileExtent)))
1468 (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction)
1469 (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . tailInduction)
1470 (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction .
1471 (lambda unrestricted next : Nat .
1472 (let unrestricted same = (naturalEqual (prFileSlot file) (prFileSlot which))
1473 in (naturalAnd (naturalSelect same (naturalEqual offset next) 1)
1474 (induction (naturalAdd next (naturalSelect same extent 0)))))))
1475 (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (lambda unrestricted next : Nat .
1476 (naturalAnd (naturalIsZero (naturalEqual prSlotInput (prFileSlot which))) (induction next))))
1477 (branch NvidiaPlanHostStepWrite file host extent tail induction . induction)
1478 (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . induction)
1479 (branch NvidiaPlanHostStepWriteStat file tail induction . induction)
1480 (branch NvidiaPlanHostStepWriteStatus file tail induction . induction)
1481 (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction)
1482 (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction)
1483 (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction)
1484 (branch NvidiaPlanHostStepFill host payload tail induction . induction)
1485 (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction)
1486 (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . (lambda unrestricted next : Nat .
1487 (let unrestricted same = (naturalEqual prSlotCheckpointIn (prFileSlot which)) in
1488 (naturalAnd (naturalSelect same (naturalEqual offset next) 1)
1489 (induction (naturalAdd next (naturalSelect same checkpointEnvelopeDigestBytes 0)))))))
1490 (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction)
1491 (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction)
1492 (branch NvidiaPlanHostStepOperation tail induction . induction)
1493 (branch NvidiaPlanHostStepSync file tail induction . induction)
1494 (branch NvidiaPlanHostStepDataSync file tail induction . induction)
1495 (branch NvidiaPlanHostStepClose file tail induction . induction)
1496 (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . induction)
1497 (branch NvidiaPlanHostStepCommands commands tail induction . induction)
1498 (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction)
1499 (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . (lambda unrestricted next : Nat . (naturalAnd (naturalIsZero (naturalEqual (prFileSlot file) (prFileSlot which))) (induction next))))
1500 (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction)
1501 (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction)
1502 (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction))
1503 0))))
1504
1505-- a little-endian natural of `count` bytes
1506def nvidiaPlanHostLittleNatural =
1507 (lambda unrestricted count : Nat .
1508 (lambda unrestricted bytes : Bytes .
1509 (app
1510 (nat-eliminate
1511 (lambda unrestricted current : Nat . (pi unrestricted rest : Bytes . Nat))
1512 (lambda unrestricted rest : Bytes . 0)
1513 (lambda unrestricted p : Nat .
1514 (lambda unrestricted induction : (pi unrestricted rest : Bytes . Nat) .
1515 (lambda unrestricted rest : Bytes .
1516 (naturalAdd (byte-to-nat (bytes-head rest)) (naturalMultiply 256 (induction (bytes-tail rest)))))))
1517 count)
1518 bytes)))
1519
1520-- entry `ordinal` of a table of 8-byte little-endian words
1521def nvidiaPlanHostTableWord =
1522 (lambda unrestricted table : Bytes .
1523 (lambda unrestricted ordinal : Nat .
1524 (nvidiaPlanHostLittleNatural 8 (dataBytesDropValidated (naturalMultiply 8 ordinal) table))))
1525
1526-- 1 when every issue again, as it runs, writes the ring entry the
1527-- realization gave its piece (`entries`: the plan's GPFIFO table)
1528def nvidiaPlanHostReissuesAdmitted =
1529 (lambda unrestricted entries : Bytes .
1530 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1531 (eliminate NvidiaPlanHostSteps
1532 (lambda unrestricted current : (family NvidiaPlanHostSteps) . Nat)
1533 (nvidiaPlanHostStepsUnrolled steps)
1534 (branch NvidiaPlanHostStepsEnd . 1)
1535 (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction)
1536 (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . tailInduction)
1537 (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . induction)
1538 (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index indexStride tail induction . induction)
1539 (branch NvidiaPlanHostStepWrite file host extent tail induction . induction)
1540 (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . induction)
1541 (branch NvidiaPlanHostStepWriteStat file tail induction . induction)
1542 (branch NvidiaPlanHostStepWriteStatus file tail induction . induction)
1543 (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction)
1544 (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction)
1545 (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction)
1546 (branch NvidiaPlanHostStepFill host payload tail induction . induction)
1547 (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction)
1548 (branch NvidiaPlanHostStepBindInputIdentity offset extent tail induction . induction)
1549 (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction)
1550 (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction)
1551 (branch NvidiaPlanHostStepOperation tail induction . induction)
1552 (branch NvidiaPlanHostStepSync file tail induction . induction)
1553 (branch NvidiaPlanHostStepDataSync file tail induction . induction)
1554 (branch NvidiaPlanHostStepClose file tail induction . induction)
1555 (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction .
1556 (naturalAnd (naturalEqual entry (nvidiaPlanHostTableWord entries piece)) induction))
1557 (branch NvidiaPlanHostStepCommands commands tail induction . induction)
1558 (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction)
1559 (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . induction)
1560 (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction)
1561 (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction)
1562 (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction))))
1563
1564-- ---- the whole request host ----
1565-- `learner` runs after the recipes are expanded and before anything is
1566-- submitted: the commands that supply parameter words at run time
1567-- (Platform.Linux.Nvidia.PlanHostAdamW), or none.
1568def nvidiaPlanHostRequestCommands =
1569 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1570 (lambda unrestricted hostIdentity : Bytes .
1571 (lambda unrestricted programIdentity : Bytes .
1572 (lambda unrestricted qmdIdentity : Bytes .
1573 (lambda unrestricted pushIdentity : Bytes .
1574 (lambda unrestricted gpfifoIdentity : Bytes .
1575 (lambda unrestricted programLength : Nat .
1576 (lambda unrestricted qmdLength : Nat .
1577 (lambda unrestricted pushLength : Nat .
1578 (lambda unrestricted gpfifoLength : Nat .
1579 (lambda unrestricted submissionCount : Nat .
1580 (lambda unrestricted input : (family NvidiaPlanHostInputContract) .
1581 (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
1582 (lambda unrestricted fills : (family NvidiaPlanHostRecipeFills) .
1583 (lambda unrestricted learner : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
1584 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1585 (prFenceRegister
1586 (phPipeCreate
1587 (phTelemetryOpen (phTelemetry prTelemetryBegin b"request-host:begin"
1588 (prEnvelope hostIdentity programIdentity qmdIdentity pushIdentity gpfifoIdentity programLength qmdLength pushLength gpfifoLength
1589 (prRequestOpen input contract
1590 (phTelemetry prTelemetryChecked b"request-host:request-checked"
1591 (phPrelude (constructor NvidiaPlanHostMode NvidiaPlanHostStrict) layout
1592 (phTelemetry prTelemetryChannel b"request-host:channel-ready"
1593 (nativeLaunchRecipeStagingCommands nvidiaPlanHostStaging nvidiaPlanHostStagingExtent prSlotStatus phIdentity
1594 (prRecipeFills fills
1595 (phTelemetry prTelemetryUploaded b"request-host:uploaded"
1596 (learner
1597 (phTelemetry prTelemetryLearner b"request-host:learner-scalars"
1598 (prSteps layout submissionCount contract steps
1599 (phTelemetry prTelemetryDone b"request-host:done"
1600 (phCall phSysExitGroup (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard
1601 (phNext (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
1602 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))))))))))))))))))))))))))))))))))
1603
1604-- ---- admission ----
1605-- A fixed-input probe needs the authenticated envelope and recipe loader,
1606-- but no text request or checkpoint protocol. The standard host still owns
1607-- channel creation, uploads, submission, completion and telemetry. Tables
1608-- are expanded only after their destination buffers have been mapped.
1609def nvidiaPlanHostRecipeCommands =
1610 (lambda unrestricted hostIdentity : Bytes .
1611 (lambda unrestricted programIdentity : Bytes .
1612 (lambda unrestricted qmdIdentity : Bytes .
1613 (lambda unrestricted pushIdentity : Bytes .
1614 (lambda unrestricted gpfifoIdentity : Bytes .
1615 (lambda unrestricted programLength : Nat .
1616 (lambda unrestricted qmdLength : Nat .
1617 (lambda unrestricted pushLength : Nat .
1618 (lambda unrestricted gpfifoLength : Nat .
1619 (lambda unrestricted recipes : (family NvidiaPlanHostRecipeFills) .
1620 (nvidiaPlanHostPreparedCommands
1621 (prEnvelope hostIdentity programIdentity qmdIdentity pushIdentity gpfifoIdentity
1622 programLength qmdLength pushLength gpfifoLength)
1623 (lambda unrestricted tail : (family NativePhysicalCommands) .
1624 (nativeLaunchRecipeStagingCommands nvidiaPlanHostStaging nvidiaPlanHostStagingExtent prSlotStatus phIdentity
1625 (prRecipeFills recipes tail))))))))))))))
1626
1627-- The layout's placement certified (PlanHost.nvidiaPlanHostLayoutCertified,
1628-- the recipe staging area among the host's mappings), the schedule's order
1629-- certified (above), and every host range the request host writes into or reads out of lies inside a
1630-- host-mapped buffer of its layout (PlanHost.nvidiaPlanHostContains): each
1631-- recipe's expanded table, and each step's file transfer, fill, write or
1632-- recorded word. A table larger than its buffer used to be built and then
1633-- copied past the mapping at run time.
1634def prRecipesAdmitted =
1635 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1636 (lambda unrestricted fills : (family NvidiaPlanHostRecipeFills) .
1637 (eliminate NvidiaPlanHostRecipeFills (lambda unrestricted current : (family NvidiaPlanHostRecipeFills) . Nat) fills
1638 (branch NvidiaPlanHostRecipeFillsEnd . 1)
1639 (branch NvidiaPlanHostRecipeFillsNext host tableExtent kind rest induction .
1640 (naturalAnd (nvidiaPlanHostContains layout host tableExtent) induction)))))
1641
1642def prStepsAdmitted =
1643 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1644 (lambda unrestricted submissionCount : Nat .
1645 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1646 (eliminate NvidiaPlanHostSteps
1647 (lambda unrestricted current : (family NvidiaPlanHostSteps) . Nat)
1648 steps
1649 (branch NvidiaPlanHostStepsEnd . 1)
1650 (branch NvidiaPlanHostStepSubmit gpPut stride tail induction .
1651 (naturalAnd (naturalLessOrEqual gpPut (prRingEntries layout)) induction))
1652 (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . (naturalAnd bodyInduction tailInduction))
1653 (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction .
1654 (naturalAnd (nvidiaPlanHostContains layout host extent) induction))
1655 (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (naturalAnd (nvidiaPlanHostContains layout host extent)
1656 (naturalAnd (naturalLess 0 count) (naturalAnd (naturalLess 0 extent)
1657 (naturalAnd (naturalLessOrEqual (naturalAdd offset extent) recordBytes)
1658 (naturalAnd (naturalLessOrEqual (naturalMultiply count recordBytes) cyclicRecordFileMaximum)
1659 (naturalAnd (naturalLessOrEqual index cyclicRecordWordMaximum)
1660 (naturalAnd (naturalLessOrEqual stride cyclicRecordWordMaximum) induction))))))))
1661 (branch NvidiaPlanHostStepWrite file host extent tail induction .
1662 (naturalAnd (nvidiaPlanHostContains layout host extent) induction))
1663 (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction .
1664 (naturalAnd (nvidiaPlanHostContains layout host extent) induction))
1665 (branch NvidiaPlanHostStepWriteStat file tail induction . induction)
1666 (branch NvidiaPlanHostStepWriteStatus file tail induction . induction)
1667 (branch NvidiaPlanHostStepWriteTimestamps file tail induction .
1668 (naturalAnd (naturalLessOrEqual (naturalMultiply nvidiaPlanHostTimestampRecord submissionCount) nvidiaPlanHostStagingExtent) induction))
1669 (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction .
1670 (naturalAnd (nvidiaPlanHostContains layout host extent) induction))
1671 (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction)
1672 (branch NvidiaPlanHostStepFill host payload tail induction .
1673 (naturalAnd (nvidiaPlanHostContains layout host (bytes-length payload)) induction))
1674 (branch NvidiaPlanHostStepAssertWord identity host expected tail induction .
1675 (naturalAnd (nvidiaPlanHostContains layout host 8) induction))
1676 (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . (naturalAnd (naturalLess 0 inputExtent) (naturalAnd (naturalLessOrEqual inputExtent cyclicRecordFileMaximum) induction)))
1677 (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction)
1678 (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction)
1679 (branch NvidiaPlanHostStepOperation tail induction . induction)
1680 (branch NvidiaPlanHostStepSync file tail induction . induction)
1681 (branch NvidiaPlanHostStepDataSync file tail induction . induction)
1682 (branch NvidiaPlanHostStepClose file tail induction . induction)
1683 (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction .
1684 (naturalAnd (naturalLess piece (prRingEntries layout)) induction))
1685 (branch NvidiaPlanHostStepCommands commands tail induction . induction)
1686 (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction)
1687 (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . (naturalAnd (nvidiaPlanHostContains layout host extent) induction))
1688 (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction)
1689 (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction)
1690 (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction)))))
1691
1692def nvidiaPlanHostRequestAdmitted =
1693 (lambda unrestricted layout : (family NvidiaPlanHostLayout) .
1694 (lambda unrestricted submissionCount : Nat .
1695 (lambda unrestricted fills : (family NvidiaPlanHostRecipeFills) .
1696 (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
1697 (naturalAnd (nvidiaPlanHostLayoutAdmitted layout)
1698 (naturalAnd (nvidiaPlanHostLayoutCertified layout
1699 (constructor ArenaResidents ArenaResidentsNext
1700 (constructor ArenaResident ArenaResidentValue b"recipe-staging" nvidiaPlanHostStaging nvidiaPlanHostStagingExtent 0x1000)
1701 (constructor ArenaResidents ArenaResidentsEnd)))
1702 (naturalAnd (prRecipesAdmitted layout fills)
1703 (naturalAnd (naturalAnd (prStepsAdmitted layout submissionCount steps)
1704 (prStepsAdmitted layout submissionCount (nvidiaPlanHostStepsUnrolled steps)))
1705 (naturalAnd (naturalLessOrEqual submissionCount
1706 (naturalDivideUnchecked nvidiaPlanHostStagingExtent nvidiaPlanHostTimestampRecord))
1707 (nvidiaPlanHostScheduleCertified submissionCount steps))))))))))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.