Platform.Linux.Nvidia.PlanHostRequest

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