module Platform.Linux.Nvidia.PlanHostRequest import Checkpoint.Envelope import Data.Bytes import Model.Config import Model.Parameter import Model.Word32 import Model.Word64 import Platform.Linux.Nvidia.PlanHost import Runtime.ArenaCertificate import Runtime.NativeLaunchRecipeLoad import Runtime.NativePhysicalEmbeddedArtifact import Runtime.NativePhysicalNativeELF import Runtime.NativePhysicalProgram import Runtime.NativeCyclicRecordOffset import Runtime.CyclicRecordOffset import Runtime.TextArtifactRequest import Std.Natural -- The request-driven host the compiler derives for a text artifact: the -- host Bob and Coppelius run, on PlanHost's compute channel. In order: -- 1. register for the private expedited membarrier (the doorbell fence); -- 2. the envelope: open /proc/self/exe, read the footer and the manifest -- through it, require the magics, every descriptor's tag and identity, -- the recipe lengths, and each component's SHA-256 (the kernel's -- AF_ALG hasher over the executable's own bytes) against the manifest -- -- an executable that is not the one the compiler wrote refuses -- itself before touching the card; -- 3. the request record (Runtime.TextArtifactRequest) named by the one -- process argument: length, magic, version, operation, then the five -- paths opened, the input's extent and the checkpoint's (empty or -- full) required; -- 4. PlanHost's prelude: the channel; -- 5. the staging area and the launch-table recipes expanded into the -- mapped arena (Runtime.NativeLaunchRecipeLoad) at the offsets the -- manifest names; -- 6. the schedule: submissions waited on their own semaphore slot, repeat -- bodies with loop-affine gpPut, semaphore and file offsets, the -- checkpoint and batch I/O between them, the request's operation -- (train continues, predict exits), the result record; exit 0. A run -- loop issues a submission of the plan again and again (Reissue): the -- host writes the ring entry itself, so one pushbuffer piece serves -- every step; the input is then a stream read at a cursor the -- checkpoint positions, and the checkpoint is published as often as the -- schedule says. -- Every offset and extent below is either PlanHost's state layout or a -- parameter the pairing derives from its plans. -- a launch-table recipe expanded into the mapped arena at startup family NvidiaPlanHostRecipeFills : Type 0 constructor NvidiaPlanHostRecipeFillsEnd constructor NvidiaPlanHostRecipeFillsNext field unrestricted nvidiaPlanHostRecipeFillHost : Nat field unrestricted nvidiaPlanHostRecipeFillTableExtent : Nat field unrestricted nvidiaPlanHostRecipeFillKind : (family NativePhysicalEmbeddedComponentKind) recursive unrestricted nvidiaPlanHostRecipeFillsTail end-family -- the five files a request names family NvidiaPlanHostFile : Type 0 constructor NvidiaPlanHostInput constructor NvidiaPlanHostCheckpointIn constructor NvidiaPlanHostCheckpointOut constructor NvidiaPlanHostPredictions constructor NvidiaPlanHostResult end-family -- A step names a submission by its gpPut (the GPFIFO entries issued so far -- once it is written; the submission waited on is ordinal gpPut - 1, its -- semaphore slot 32 x ordinal, its timestamp record 64 x ordinal). Inside -- a repeat body a step's gpPut, semaphore, stamps and file offset advance by -- `stride` per iteration (loop-affine operands); outside, stride is 0. family NvidiaPlanHostSteps : Type 0 constructor NvidiaPlanHostStepsEnd constructor NvidiaPlanHostStepSubmit field unrestricted nvidiaPlanHostStepSubmitGPPut : Nat field unrestricted nvidiaPlanHostStepSubmitStride : Nat recursive unrestricted nvidiaPlanHostStepSubmitTail constructor NvidiaPlanHostStepRepeat field unrestricted nvidiaPlanHostStepRepeatCount : Nat recursive unrestricted nvidiaPlanHostStepRepeatBody recursive unrestricted nvidiaPlanHostStepRepeatTail constructor NvidiaPlanHostStepRead field unrestricted nvidiaPlanHostStepReadFile : (family NvidiaPlanHostFile) field unrestricted nvidiaPlanHostStepReadHost : Nat field unrestricted nvidiaPlanHostStepReadExtent : Nat field unrestricted nvidiaPlanHostStepReadOffset : Nat field unrestricted nvidiaPlanHostStepReadStride : Nat field unrestricted nvidiaPlanHostStepReadTolerateEmpty : Nat recursive unrestricted nvidiaPlanHostStepReadTail -- Read from ((completed updates + index + loop * indexStride) mod count). -- The checkpoint header owns the persisted count. File identity admission is -- separate; this step alone proves neither corpus identity nor authenticity. constructor NvidiaPlanHostStepReadCyclic field unrestricted nvidiaPlanHostStepCyclicHost : Nat field unrestricted nvidiaPlanHostStepCyclicExtent : Nat field unrestricted nvidiaPlanHostStepCyclicOffset : Nat field unrestricted nvidiaPlanHostStepCyclicRecordBytes : Nat field unrestricted nvidiaPlanHostStepCyclicCount : Nat field unrestricted nvidiaPlanHostStepCyclicIndex : Nat field unrestricted nvidiaPlanHostStepCyclicIndexStride : Nat recursive unrestricted nvidiaPlanHostStepCyclicTail constructor NvidiaPlanHostStepWrite field unrestricted nvidiaPlanHostStepWriteFile : (family NvidiaPlanHostFile) field unrestricted nvidiaPlanHostStepWriteHost : Nat field unrestricted nvidiaPlanHostStepWriteExtent : Nat recursive unrestricted nvidiaPlanHostStepWriteTail constructor NvidiaPlanHostStepWriteAt field unrestricted nvidiaPlanHostStepWriteAtFile : (family NvidiaPlanHostFile) field unrestricted nvidiaPlanHostStepWriteAtHost : Nat field unrestricted nvidiaPlanHostStepWriteAtExtent : Nat field unrestricted nvidiaPlanHostStepWriteAtOffset : Nat recursive unrestricted nvidiaPlanHostStepWriteAtTail constructor NvidiaPlanHostStepWriteStat field unrestricted nvidiaPlanHostStepWriteStatFile : (family NvidiaPlanHostFile) recursive unrestricted nvidiaPlanHostStepWriteStatTail constructor NvidiaPlanHostStepWriteStatus field unrestricted nvidiaPlanHostStepWriteStatusFile : (family NvidiaPlanHostFile) recursive unrestricted nvidiaPlanHostStepWriteStatusTail constructor NvidiaPlanHostStepWriteTimestamps field unrestricted nvidiaPlanHostStepWriteTimestampsFile : (family NvidiaPlanHostFile) recursive unrestricted nvidiaPlanHostStepWriteTimestampsTail constructor NvidiaPlanHostStepRecordStat field unrestricted nvidiaPlanHostStepRecordHost : Nat field unrestricted nvidiaPlanHostStepRecordStatOffset : Nat field unrestricted nvidiaPlanHostStepRecordExtent : Nat recursive unrestricted nvidiaPlanHostStepRecordTail constructor NvidiaPlanHostStepStamp field unrestricted nvidiaPlanHostStepStampGPPut : Nat field unrestricted nvidiaPlanHostStepStampStride : Nat field unrestricted nvidiaPlanHostStepStampWhich : Nat recursive unrestricted nvidiaPlanHostStepStampTail constructor NvidiaPlanHostStepFill field unrestricted nvidiaPlanHostStepFillHost : Nat field unrestricted nvidiaPlanHostStepFillPayload : Bytes recursive unrestricted nvidiaPlanHostStepFillTail -- A completed device word checked before any dependent file publication. -- The word may contain multiple packed statuses; every bit is compared. constructor NvidiaPlanHostStepAssertWord field unrestricted nvidiaPlanHostStepAssertIdentity : Bytes field unrestricted nvidiaPlanHostStepAssertHost : Nat field unrestricted nvidiaPlanHostStepAssertExpected : Nat recursive unrestricted nvidiaPlanHostStepAssertTail -- Begin publication after the caller admits its operation, without encoding -- that operation as a runtime-selected architecture-specific syscall. -- Hash the complete admitted input and bind it to a checkpoint payload -- field. An empty checkpoint captures the identity; a resumed one must agree. constructor NvidiaPlanHostStepBindInputIdentity field unrestricted nvidiaPlanHostStepInputIdentityOffset : Nat field unrestricted nvidiaPlanHostStepInputIdentityExtent : Nat recursive unrestricted nvidiaPlanHostStepInputIdentityTail constructor NvidiaPlanHostStepWriteInputIdentity recursive unrestricted nvidiaPlanHostStepWriteInputIdentityTail constructor NvidiaPlanHostStepBeginCheckpoint recursive unrestricted nvidiaPlanHostStepBeginCheckpointTail constructor NvidiaPlanHostStepOperation recursive unrestricted nvidiaPlanHostStepOperationTail constructor NvidiaPlanHostStepSync field unrestricted nvidiaPlanHostStepSyncFile : (family NvidiaPlanHostFile) recursive unrestricted nvidiaPlanHostStepSyncTail constructor NvidiaPlanHostStepDataSync field unrestricted nvidiaPlanHostStepDataSyncFile : (family NvidiaPlanHostFile) recursive unrestricted nvidiaPlanHostStepDataSyncTail constructor NvidiaPlanHostStepClose field unrestricted nvidiaPlanHostStepCloseFile : (family NvidiaPlanHostFile) recursive unrestricted nvidiaPlanHostStepCloseTail -- Submission `piece` of the plan issued again: the host writes the plan's -- GPFIFO entry for it (`entry`, as realized) into the ring at ordinal -- gpPut - 1, clears the piece's semaphore slot (its pushbuffer releases the -- same slot every time), then publishes gpPut and awaits the slot as a -- Submit does. gpPut, piece and entry advance by their strides per -- iteration of an enclosing repeat (equal pieces laid end to end: the -- pairing's admission holds each iteration's entry to the realized table). constructor NvidiaPlanHostStepReissue field unrestricted nvidiaPlanHostStepReissueGPPut : Nat field unrestricted nvidiaPlanHostStepReissueGPPutStride : Nat field unrestricted nvidiaPlanHostStepReissuePiece : Nat field unrestricted nvidiaPlanHostStepReissuePieceStride : Nat field unrestricted nvidiaPlanHostStepReissueEntry : Nat field unrestricted nvidiaPlanHostStepReissueEntryStride : Nat recursive unrestricted nvidiaPlanHostStepReissueTail -- host commands run in place (a learner's per-update scalars, -- Platform.Linux.Nvidia.PlanHostAdamW); they may not repeat constructor NvidiaPlanHostStepCommands field unrestricted nvidiaPlanHostStepCommandsList : (family NativePhysicalCommands) recursive unrestricted nvidiaPlanHostStepCommandsTail -- the input stream's cursor: `base` bytes, plus `scale` for every -- invocation the checkpoint read has counted (0 for a fresh start), so a -- resumed run reads on from where its checkpoint left the stream constructor NvidiaPlanHostStepCursorFromCheckpoint field unrestricted nvidiaPlanHostStepCursorBase : Nat field unrestricted nvidiaPlanHostStepCursorScale : Nat recursive unrestricted nvidiaPlanHostStepCursorFromCheckpointTail -- `extent` bytes of the file at the cursor plus `delta`, into `host`; a -- short read is a command failure constructor NvidiaPlanHostStepReadAtCursor field unrestricted nvidiaPlanHostStepReadAtCursorFile : (family NvidiaPlanHostFile) field unrestricted nvidiaPlanHostStepReadAtCursorHost : Nat field unrestricted nvidiaPlanHostStepReadAtCursorExtent : Nat field unrestricted nvidiaPlanHostStepReadAtCursorDelta : Nat recursive unrestricted nvidiaPlanHostStepReadAtCursorTail constructor NvidiaPlanHostStepCursorAdvance field unrestricted nvidiaPlanHostStepCursorAdvanceBytes : Nat recursive unrestricted nvidiaPlanHostStepCursorAdvanceTail -- the checkpoint's temporary created (as a train request's operation -- does), for a checkpoint published later in the schedule constructor NvidiaPlanHostStepCheckpointBegin recursive unrestricted nvidiaPlanHostStepCheckpointBeginTail -- the checkpoint published (prPublishCheckpointStages): its header counts -- `updates` updates and `invocations` invocations past the checkpoint read constructor NvidiaPlanHostStepCheckpointPublish field unrestricted nvidiaPlanHostStepCheckpointPublishUpdates : Nat field unrestricted nvidiaPlanHostStepCheckpointPublishInvocations : Nat recursive unrestricted nvidiaPlanHostStepCheckpointPublishTail end-family -- What a request's input must be: exactly `extent` bytes, or a stream the -- schedule reads at its cursor (any length: every read of it must return -- whole, so a stream that ends early stops the run at that read). family NvidiaPlanHostInputContract : Type 0 constructor NvidiaPlanHostInputExact field unrestricted nvidiaPlanHostInputExactExtent : Nat constructor NvidiaPlanHostInputStream end-family -- ---- state areas after PlanHost's buffer call blocks ---- -- each after the previous, 8-byte aligned def prAfter = (lambda unrestricted at : Nat . (lambda unrestricted bytes : Nat . (naturalMultiply (naturalDivideUnchecked (naturalAdd (naturalAdd at bytes) 7) 8) 8))) def prRequest : Nat = phBufferBlocksEnd def prStat : Nat = (prAfter prRequest textArtifactRequestEncodedLength) def prStatExtent : Nat = 160 def prFooter : Nat = (prAfter prStat prStatExtent) def prManifest : Nat = (prAfter prFooter nativePhysicalEmbeddedFooterLength) def prDescriptorWords : Nat = (prAfter prManifest nativePhysicalEmbeddedManifestLength) def prDigest : Nat = (prAfter prDescriptorWords 80) def prIdentityScratch : Nat = (prAfter prDigest nativePhysicalEmbeddedDigestLength) def prSendOffset : Nat = (prAfter prIdentityScratch nativePhysicalEmbeddedIdentityLength) def prGPPut : Nat = (prAfter prSendOffset 8) def prWordScratch : Nat = (prAfter prGPPut 8) def prStatusBlock : Nat = (prAfter prWordScratch 8) def prStatusBlockExtent : Nat = 160 def prExpected : Nat = (prAfter prStatusBlock prStatusBlockExtent) -- the checkpoint read's header and the written one's (Checkpoint.Envelope: -- the fields before the chunk digests), and a chunk's expected digest def prCheckpointHeaderIn : Nat = (prAfter prExpected 8) def prCheckpointHeaderOut : Nat = (prAfter prCheckpointHeaderIn checkpointEnvelopeDigestsAt) def prExpectedDigest : Nat = (prAfter prCheckpointHeaderOut checkpointEnvelopeDigestsAt) -- the learner's per-update scalars (Platform.Linux.Nvidia.PlanHostAdamW): -- sixteen binary64 words def prLearnerScratch : Nat = (prAfter prExpectedDigest checkpointEnvelopeDigestBytes) def prLearnerScratchExtent : Nat = 128 -- Retained separately from prDigest, which checkpoint chunk hashing reuses. def prInputIdentity : Nat = (prAfter prLearnerScratch prLearnerScratchExtent) -- the input stream's cursor and the offset a cursor read computes def prCursor : Nat = (prAfter prInputIdentity checkpointEnvelopeDigestBytes) def prCursorOffset : Nat = (prAfter prCursor 8) def prCursorScratch : Nat = (prAfter prCursorOffset 8) def prAreasEnd : Nat = (prAfter prCursorScratch 8) -- every area inside PlanHost's state def prAreasFit : (equal Nat (naturalLessOrEqual prAreasEnd phStateExtent) 1) = (refl Nat 1) -- result slots after PlanHost's four def prSlotExe : Nat = 4 def prSlotRequest : Nat = 5 def prSlotInput : Nat = 6 def prSlotCheckpointIn : Nat = 7 def prSlotCheckpointOut : Nat = 8 def prSlotPredictions : Nat = 9 def prSlotResult : Nat = 10 def prSlotStatus : Nat = 11 def prSlotAlg : Nat = 12 def prSlotHash : Nat = 13 -- Linux x86-64 def prSysClose : Nat = 3 def prSysFstat : Nat = 5 def prSysLseek : Nat = 8 def prSysPread : Nat = 17 def prSysPwrite : Nat = 18 def prSysSendfile : Nat = 40 def prSysSocket : Nat = 41 def prSysAccept : Nat = 43 def prSysBind : Nat = 49 def prSysFsync : Nat = 74 def prSysFdatasync : Nat = 75 def prSysClockGettime : Nat = 228 def prSysMembarrier : Nat = 324 def prSysRename : Nat = 82 -- a temporary a crashed run left, removed before the new one is created def prSysUnlink : Nat = 87 def prSeekEnd : Nat = 2 def prMinusFooter : Nat = 18446744073709551600 def prOpenWriteCreate : Nat = 577 def prCreateMode : Nat = 384 -- O_RDWR | O_CREAT | O_EXCL: the checkpoint's temporary, which must be new def prOpenReadWriteExclusive : Nat = 194 -- O_RDONLY | O_DIRECTORY def prOpenDirectory : Nat = 65536 def prMembarrierRegister : Nat = 16 def prMembarrierFence : Nat = 8 def prAddressFamilyAlg : Nat = 38 def prSocketSeqpacket : Nat = 5 def prStatSize : Nat = 48 def prClockRealtime : Nat = 0 -- The mapped recipe staging area, and the host timestamp table that lives -- in it once the recipes are expanded: a 64-byte record per submission -- ([+0] before the doorbell, [+16] after the wait, [+32] and [+48] around -- the I/O that follows), CLOCK_REALTIME, the clock the device stamps its -- semaphores with. def nvidiaPlanHostStaging : Nat = 0x40000000 def nvidiaPlanHostStagingExtent : Nat = 0x1000000 def nvidiaPlanHostTimestampRecord : Nat = 64 -- ---- telemetry ---- -- The request host's phase boundaries, each an ALPHATEL record sealed and -- appended to `alpha-host.alphatel` in its working directory as the plan -- host's are (PlanHost.phTelemetry): begun; the request and the checkpoint -- checked; the channel up; the recipes expanded; the learner's scalars -- written; the checkpoint published (a train request); every step done. A -- record exists only if the host got there. def prTelemetryBegin : Nat = 0 def prTelemetryChecked : Nat = 1 def prTelemetryChannel : Nat = 2 def prTelemetryUploaded : Nat = 3 def prTelemetryLearner : Nat = 4 def prTelemetryPublished : Nat = 5 def prTelemetryDone : Nat = 6 -- ---- operands and assertions ---- def prStatus : (family NativePhysicalOperand) = (phSlot prSlotStatus) def prAssertStatus = (lambda unrestricted identity : Bytes . (lambda unrestricted expected : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeAssertEqual prStatus (phImm expected) identity tail)))) def prAssertEqual = (lambda unrestricted identity : Bytes . (lambda unrestricted left : (family NativePhysicalOperand) . (lambda unrestricted right : (family NativePhysicalOperand) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeAssertEqual left right identity tail))))) def prAssertOneOf = (lambda unrestricted identity : Bytes . (lambda unrestricted observed : (family NativePhysicalOperand) . (lambda unrestricted first : Nat . (lambda unrestricted second : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalAssertOneOf observed (phImm first) (phImm second) (constructor NativePhysicalErrorCode NativePhysicalExecutionAssertionFailed)) identity tail)))))) -- the 8-byte word at a state offset equals these 8 bytes def prExpectBytes = (lambda unrestricted identity : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted payload : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCopy prExpected payload (prAssertEqual identity (phLoad offset) (phLoad prExpected) tail)))))) -- `count` words from a state offset equal these bytes def prExpectWords = (lambda unrestricted identity : Bytes . (lambda unrestricted offset : Nat . (lambda unrestricted payload : Bytes . (lambda unrestricted count : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalCommands)) tail (lambda unrestricted index : Nat . (lambda unrestricted induction : (family NativePhysicalCommands) . (prExpectBytes identity (naturalAdd offset (naturalMultiply index 8)) (phTake 8 (phDrop (naturalMultiply index 8) payload)) induction))) count)))))) -- a 32-bit word of the state zero-extended into an 8-byte word def prLoad32 = (lambda unrestricted source : Nat . (lambda unrestricted destination : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCopy destination (phZeros 8) (phCopyStateToState destination source 4 tail))))) def prClose = (lambda unrestricted identity : Bytes . (lambda unrestricted slot : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall prSysClose (phArgs3 (phSlot slot) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus identity 0 tail))))) def prFstat = (lambda unrestricted identity : Bytes . (lambda unrestricted slot : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall prSysFstat (phArgs3 (phSlot slot) (phState prStat) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus identity 0 tail))))) -- an immediate, or loop-affine when the stride is not 0 def prAffine = (lambda unrestricted base : Nat . (lambda unrestricted stride : Nat . (nat-eliminate (lambda unrestricted current : Nat . (family NativePhysicalOperand)) (phImm base) (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NativePhysicalOperand) . (constructor NativePhysicalOperand NativePhysicalLoopAffine (phWord base) (phWord stride)))) stride))) -- ---- 1. the fence ---- def prFenceRegister = (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall prSysMembarrier (phArgs3 (phImm prMembarrierRegister) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"membarrier-register" 0 tail))) def prFence = (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall prSysMembarrier (phArgs3 (phImm prMembarrierFence) (phImm 0) (phImm 0)) b"" phDiscard tail)) -- ---- 2. the envelope ---- -- sockaddr_alg: AF_ALG, "hash", feat, mask, "sha256" def prSockaddrAlg : Bytes = (bytes-append (bytes 38 0) (bytes-append b"hash" (bytes-append (phZeros 10) (bytes-append (phZeros 8) (bytes-append b"sha256" (phZeros 58)))))) def prSockaddrAlgExtent : Nat = 88 def prDescriptor = (lambda unrestricted index : Nat . (naturalAdd prManifest (naturalAdd 12 (naturalMultiply index nativePhysicalEmbeddedDescriptorLength)))) def prDescriptorOffsetWord = (lambda unrestricted index : Nat . (naturalAdd prDescriptorWords (naturalMultiply index 16))) def prDescriptorLengthWord = (lambda unrestricted index : Nat . (naturalAdd (prDescriptorOffsetWord index) 8)) -- One descriptor: its tag is the component's, its offset and length are -- kept as words, its identity is the one the pairing embedded, and the -- SHA-256 of the component's bytes in this executable equals the digest -- the manifest carries. def prVerifyComponent = (lambda unrestricted index : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted descriptor = (prDescriptor index) in (prLoad32 descriptor prWordScratch (prAssertEqual b"envelope-tag" (phLoad prWordScratch) (phImm (naturalAdd index 1)) (prLoad32 (naturalAdd descriptor 4) (prDescriptorOffsetWord index) (prLoad32 (naturalAdd descriptor 8) (prDescriptorLengthWord index) (phCopyStateToState prIdentityScratch (naturalAdd descriptor 12) nativePhysicalEmbeddedIdentityLength (prExpectWords b"envelope-identity" prIdentityScratch identity 8 (phCall prSysSocket (phArgs3 (phImm prAddressFamilyAlg) (phImm prSocketSeqpacket) (phImm 0)) b"" (phStore prSlotAlg) (phCall prSysBind (phArgs3 (phSlot prSlotAlg) phPayload (phImm prSockaddrAlgExtent)) prSockaddrAlg (phStore prSlotStatus) (prAssertStatus b"envelope-hash-bind" 0 (phCall prSysAccept (phArgs3 (phSlot prSlotAlg) (phImm 0) (phImm 0)) b"" (phStore prSlotHash) (prLoad32 (naturalAdd descriptor 4) prSendOffset (phCall prSysSendfile (phArgs (phSlot prSlotHash) (phSlot prSlotExe) (phState prSendOffset) (phLoad (prDescriptorLengthWord index)) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertEqual b"envelope-hash-send" prStatus (phLoad (prDescriptorLengthWord index)) (phCall phSysRead (phArgs3 (phSlot prSlotHash) (phState prDigest) (phImm nativePhysicalEmbeddedDigestLength)) b"" (phStore prSlotStatus) (prAssertStatus b"envelope-hash-read" nativePhysicalEmbeddedDigestLength (phCopyStateToState prIdentityScratch (naturalAdd descriptor 76) nativePhysicalEmbeddedDigestLength (prAssertEqual b"envelope-digest" (phLoad prDigest) (phLoad prIdentityScratch) (prAssertEqual b"envelope-digest" (phLoad (naturalAdd prDigest 8)) (phLoad (naturalAdd prIdentityScratch 8)) (prAssertEqual b"envelope-digest" (phLoad (naturalAdd prDigest 16)) (phLoad (naturalAdd prIdentityScratch 16)) (prAssertEqual b"envelope-digest" (phLoad (naturalAdd prDigest 24)) (phLoad (naturalAdd prIdentityScratch 24)) (prClose b"envelope-hash-close" prSlotHash (prClose b"envelope-alg-close" prSlotAlg tail)))))))))))))))))))))))))) -- a recipe descriptor's length is the recipe's def prVerifyRecipe = (lambda unrestricted index : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted length : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (prVerifyComponent index identity (prAssertEqual b"envelope-recipe-length" (phLoad (prDescriptorLengthWord index)) (phImm length) tail)))))) def prEnvelope = (lambda unrestricted hostIdentity : Bytes . (lambda unrestricted programIdentity : Bytes . (lambda unrestricted qmdIdentity : Bytes . (lambda unrestricted pushIdentity : Bytes . (lambda unrestricted gpfifoIdentity : Bytes . (lambda unrestricted programLength : Nat . (lambda unrestricted qmdLength : Nat . (lambda unrestricted pushLength : Nat . (lambda unrestricted gpfifoLength : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) phPayload (phImm 0)) b"/proc/self/exe\x00" (phStore prSlotExe) (prFstat b"envelope-stat" prSlotExe (phCall prSysLseek (phArgs3 (phSlot prSlotExe) (phImm prMinusFooter) (phImm prSeekEnd)) b"" phDiscard (phCall phSysRead (phArgs3 (phSlot prSlotExe) (phState prFooter) (phImm nativePhysicalEmbeddedFooterLength)) b"" (phStore prSlotStatus) (prAssertStatus b"envelope-footer-read" nativePhysicalEmbeddedFooterLength (prExpectBytes b"envelope-footer-magic" prFooter nativePhysicalEmbeddedFooterMagic (prLoad32 (naturalAdd prFooter 12) prWordScratch (prAssertEqual b"envelope-footer-length" (phLoad prWordScratch) (phImm nativePhysicalEmbeddedManifestLength) (prLoad32 (naturalAdd prFooter 8) prWordScratch (phCall prSysPread (phArgs (phSlot prSlotExe) (phState prManifest) (phImm nativePhysicalEmbeddedManifestLength) (phLoad prWordScratch) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"envelope-manifest-read" nativePhysicalEmbeddedManifestLength (prExpectBytes b"envelope-manifest-magic" prManifest nativePhysicalEmbeddedManifestMagic (prExpectBytes b"envelope-manifest-version" (naturalAdd prManifest 8) (bytes-append (phW32 nativePhysicalEmbeddedVersion) (phW32 (nativePhysicalEmbeddedComponentTag (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedHostELF)))) (prVerifyComponent 0 hostIdentity (prVerifyRecipe 1 programIdentity programLength (prVerifyRecipe 2 qmdIdentity qmdLength (prVerifyRecipe 3 pushIdentity pushLength (prVerifyRecipe 4 gpfifoIdentity gpfifoLength tail)))))))))))))))))))))))))))) -- ---- 3. the request ---- def prPath = (lambda unrestricted which : Nat . (naturalAdd prRequest (naturalAdd 24 (naturalMultiply which textArtifactPathExtent)))) def prOpenPath = (lambda unrestricted which : Nat . (lambda unrestricted flags : Nat . (lambda unrestricted slot : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysOpenat (phArgs (phImm phAtFdCwd) (phState (prPath which)) (phImm flags) (phImm prCreateMode) (phImm 0) (phImm 0)) b"" (phStore slot) tail))))) -- the checkpoint read: when the file is not empty, its envelope -- (Checkpoint.Envelope) -- the fixed fields, the four identities, every -- chunk's digest -- before any buffer is allocated. An empty file is a -- fresh start: its header reads as zeros, so its version (the count of the -- conditional block) is 0 and so is its chunk count; a file of the full -- size must say version 1 (the size plus the version is 0 or the full size -- plus 1), so the checks are skipped only for an empty one. def prChunkCheck = (lambda unrestricted fileSlot : Nat . (lambda unrestricted offset : (family NativePhysicalOperand) . (lambda unrestricted extent : Nat . (lambda unrestricted digestAt : (family NativePhysicalOperand) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prSendOffset) offset) (phCall prSysSendfile (phArgs (phSlot prSlotHash) (phSlot fileSlot) (phState prSendOffset) (phImm extent) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"checkpoint-chunk-read" extent (phCall phSysRead (phArgs3 (phSlot prSlotHash) (phState prDigest) (phImm checkpointEnvelopeDigestBytes)) b"" (phStore prSlotStatus) (prAssertStatus b"checkpoint-chunk-hash" checkpointEnvelopeDigestBytes (phCall prSysPread (phArgs (phSlot fileSlot) (phState prExpectedDigest) (phImm checkpointEnvelopeDigestBytes) digestAt (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"checkpoint-chunk-digest-read" checkpointEnvelopeDigestBytes (prAssertEqual b"checkpoint-chunk" (phLoad prDigest) (phLoad prExpectedDigest) (prAssertEqual b"checkpoint-chunk" (phLoad (naturalAdd prDigest 8)) (phLoad (naturalAdd prExpectedDigest 8)) (prAssertEqual b"checkpoint-chunk" (phLoad (naturalAdd prDigest 16)) (phLoad (naturalAdd prExpectedDigest 16)) (prAssertEqual b"checkpoint-chunk" (phLoad (naturalAdd prDigest 24)) (phLoad (naturalAdd prExpectedDigest 24)) tail)))))))))))))))) -- the hasher: an AF_ALG SHA-256 socket and the connection hashes go through def prHasherOpen = (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall prSysSocket (phArgs3 (phImm prAddressFamilyAlg) (phImm prSocketSeqpacket) (phImm 0)) b"" (phStore prSlotAlg) (phCall prSysBind (phArgs3 (phSlot prSlotAlg) phPayload (phImm prSockaddrAlgExtent)) prSockaddrAlg (phStore prSlotStatus) (prAssertStatus identity 0 (phCall prSysAccept (phArgs3 (phSlot prSlotAlg) (phImm 0) (phImm 0)) b"" (phStore prSlotHash) tail)))))) def prHasherClose = (lambda unrestricted tail : (family NativePhysicalCommands) . (prClose b"checkpoint-hash-close" prSlotHash (prClose b"checkpoint-alg-close" prSlotAlg tail))) -- every chunk of a file's payload, from `header` on, against the digests -- the file's header carries: the full ones (their count a state word or an -- immediate), then the tail when the contract has one (under `tailCount`) def prChunksCheck = (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (lambda unrestricted fileSlot : Nat . (lambda unrestricted fullCount : (family NativePhysicalOperand) . (lambda unrestricted tailCount : (family NativePhysicalOperand) . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted header = (checkpointEnvelopeHeaderBytes contract) in (let unrestricted chunk = (checkpointEnvelopeContractChunk contract) in (let unrestricted full = (checkpointEnvelopeFullChunks contract) in (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted fullCount) (prChunkCheck fileSlot (prAffine header chunk) chunk (prAffine checkpointEnvelopeDigestsAt checkpointEnvelopeDigestBytes) (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd) (phWhen (naturalNonzero (checkpointEnvelopeTailBytes contract)) (lambda unrestricted after : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted tailCount) (prChunkCheck fileSlot (phImm (naturalAdd header (naturalMultiply chunk full))) (checkpointEnvelopeTailBytes contract) (phImm (naturalAdd checkpointEnvelopeDigestsAt (naturalMultiply checkpointEnvelopeDigestBytes full))) (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd) after)))) tail)))))))))))) def prCheckpointValidate = (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted version = (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeVersionAt)) in (phCall prSysPread (phArgs (phSlot prSlotCheckpointIn) (phState prCheckpointHeaderIn) (phImm checkpointEnvelopeDigestsAt) (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState prWordScratch) (phLoad (naturalAdd prStat prStatSize)) version) (prAssertOneOf b"checkpoint-version" (phLoad prWordScratch) 0 (succ (checkpointEnvelopeFileBytes contract)) (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted version) (prExpectWords b"checkpoint-layout" prCheckpointHeaderIn (checkpointEnvelopeFixed contract) (naturalDivideUnchecked checkpointEnvelopeFixedBytes 8) (prExpectWords b"checkpoint-schema" (naturalAdd prCheckpointHeaderIn checkpointEnvelopeSchemaAt) (dataBytesTakeValidated 32 (checkpointEnvelopeIdentityDigests contract)) 4 (prExpectWords b"checkpoint-learner" (naturalAdd prCheckpointHeaderIn checkpointEnvelopeLearnerAt) (dataBytesTakeValidated 32 (dataBytesDropValidated 32 (checkpointEnvelopeIdentityDigests contract))) 4 (prExpectWords b"checkpoint-data" (naturalAdd prCheckpointHeaderIn checkpointEnvelopeDataAt) (dataBytesTakeValidated 32 (dataBytesDropValidated 64 (checkpointEnvelopeIdentityDigests contract))) 4 (prExpectWords b"checkpoint-seed" (naturalAdd prCheckpointHeaderIn checkpointEnvelopeSeedAt) (dataBytesDropValidated 96 (checkpointEnvelopeIdentityDigests contract)) 4 (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd) (prHasherOpen b"checkpoint-hash-bind" (prChunksCheck contract prSlotCheckpointIn (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeFullChunksAt)) version (prHasherClose tail)))))))))))))))) -- the input's extent, when the contract fixes it def prInputExtentCheck = (lambda unrestricted input : (family NvidiaPlanHostInputContract) . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate NvidiaPlanHostInputContract (lambda unrestricted current : (family NvidiaPlanHostInputContract) . (family NativePhysicalCommands)) input (branch NvidiaPlanHostInputExact extent . (prAssertEqual b"input-extent" (phLoad (naturalAdd prStat prStatSize)) (phImm extent) tail)) (branch NvidiaPlanHostInputStream . tail)))) def prRequestOpen = (lambda unrestricted input : (family NvidiaPlanHostInputContract) . (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysOpenat (phArgs3 (phImm phAtFdCwd) (constructor NativePhysicalOperand NativePhysicalProcessArgument (phWord 1)) (phImm 0)) b"" (phStore prSlotRequest) (prFstat b"request-stat" prSlotRequest (prAssertEqual b"request-length" (phLoad (naturalAdd prStat prStatSize)) (phImm textArtifactRequestEncodedLength) (phCall phSysRead (phArgs3 (phSlot prSlotRequest) (phState prRequest) (phImm textArtifactRequestEncodedLength)) b"" (phStore prSlotStatus) (prAssertStatus b"request-read" textArtifactRequestEncodedLength (prExpectBytes b"request-magic" prRequest textArtifactRequestMagic (prAssertEqual b"request-version" (phLoad (naturalAdd prRequest 8)) (phImm textArtifactRequestVersion) (prAssertOneOf b"request-operation" (phLoad (naturalAdd prRequest 16)) textArtifactTrainOperationWord textArtifactPredictOperationWord (prOpenPath 0 0 prSlotInput (prOpenPath 1 0 prSlotCheckpointIn (prOpenPath 3 prOpenWriteCreate prSlotPredictions (prOpenPath 4 prOpenWriteCreate prSlotResult (prFstat b"input-stat" prSlotInput (prInputExtentCheck input (prFstat b"checkpoint-stat" prSlotCheckpointIn (prAssertOneOf b"checkpoint-truncated" (phLoad (naturalAdd prStat prStatSize)) 0 (checkpointEnvelopeFileBytes contract) (prCheckpointValidate contract tail)))))))))))))))))))) -- the paths the request names, by index def prCheckpointOutPath : Nat = 2 def prCheckpointTemporaryPath : Nat = 5 def prCheckpointDirectoryPath : Nat = 6 -- A train request's checkpoint is written to its temporary, created new -- (a temporary a crashed run left is removed first) and positioned after -- the header. -- With one byte in one record, offset computation isolates the checked -- counter addition: the only possible rejection is completed + increment -- exceeding u64. The discarded offset is zero on success. def prCheckCounterAddition = (lambda unrestricted identity : Bytes . (lambda unrestricted counterAt : Nat . (lambda unrestricted increment : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeCyclicRecordOffsetRoutine (phArgs (phState prWordScratch) (phLoad counterAt) (phImm increment) (phImm 1) (phImm 1) (phImm 0)) (phStore prSlotStatus)) (prAssertStatus identity 0 tail)))))) def prCheckpointTemporary = (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (lambda unrestricted tail : (family NativePhysicalCommands) . (prCheckCounterAddition b"checkpoint-update-count-overflow" (naturalAdd prCheckpointHeaderIn checkpointEnvelopeUpdatesAt) (checkpointEnvelopeContractUpdates contract) (prCheckCounterAddition b"checkpoint-invocation-count-overflow" (naturalAdd prCheckpointHeaderIn checkpointEnvelopeInvocationsAt) 1 (phCall prSysUnlink (phArgs3 (phState (prPath prCheckpointTemporaryPath)) (phImm 0) (phImm 0)) b"" phDiscard (prOpenPath prCheckpointTemporaryPath prOpenReadWriteExclusive prSlotCheckpointOut (phCall prSysLseek (phArgs3 (phSlot prSlotCheckpointOut) (phImm (checkpointEnvelopeHeaderBytes contract)) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"checkpoint-temporary" (checkpointEnvelopeHeaderBytes contract) tail)))))))) -- a chunk of the written checkpoint hashed back from it, its digest written -- into the header def prDigestWrite = (lambda unrestricted offset : (family NativePhysicalOperand) . (lambda unrestricted extent : Nat . (lambda unrestricted digestAt : (family NativePhysicalOperand) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prSendOffset) offset) (phCall prSysSendfile (phArgs (phSlot prSlotHash) (phSlot prSlotCheckpointOut) (phState prSendOffset) (phImm extent) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"checkpoint-readback" extent (phCall phSysRead (phArgs3 (phSlot prSlotHash) (phState prDigest) (phImm checkpointEnvelopeDigestBytes)) b"" (phStore prSlotStatus) (prAssertStatus b"checkpoint-readback-hash" checkpointEnvelopeDigestBytes (phCall prSysPwrite (phArgs (phSlot prSlotCheckpointOut) (phState prDigest) (phImm checkpointEnvelopeDigestBytes) digestAt (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"checkpoint-digest-write" checkpointEnvelopeDigestBytes tail))))))))))) -- Publishing the checkpoint (a train request's; Checkpoint.Envelope), in -- stages: 1 the header -- the fixed fields, the update count and -- invocations after this invocation's, the identities; 2 each chunk's -- digest (hashed back from the temporary: the readback); 3 the data synced; -- 4 the temporary closed; 5 renamed over the output path; 6 the directory -- synced. Until the rename the output path holds what it held. A host -- runs all six; `prPublishCheckpointStages` stops after the first `stages`, -- which is how the publication is tested at every boundary -- (scripts/ci/checkpoint-envelope.sh). def prPublishStages : Nat = 6 def prPublishCheckpointCounting = (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (lambda unrestricted stages : Nat . (lambda unrestricted updates : Nat . (lambda unrestricted invocations : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted header = (checkpointEnvelopeHeaderBytes contract) in (let unrestricted chunk = (checkpointEnvelopeContractChunk contract) in (let unrestricted full = (checkpointEnvelopeFullChunks contract) in (let unrestricted stage = (lambda unrestricted index : Nat . (phWhen (naturalLessOrEqual index stages))) in (stage 1 (lambda unrestricted after : (family NativePhysicalCommands) . (phCopy prCheckpointHeaderOut (checkpointEnvelopeFixed contract) (phCopy (naturalAdd prCheckpointHeaderOut checkpointEnvelopeSchemaAt) (checkpointEnvelopeIdentityDigests contract) (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState (naturalAdd prCheckpointHeaderOut checkpointEnvelopeUpdatesAt)) (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeUpdatesAt)) (phImm updates)) (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState (naturalAdd prCheckpointHeaderOut checkpointEnvelopeInvocationsAt)) (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeInvocationsAt)) (phImm invocations)) (phCall prSysPwrite (phArgs (phSlot prSlotCheckpointOut) (phState prCheckpointHeaderOut) (phImm checkpointEnvelopeDigestsAt) (phImm 0) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"checkpoint-header-write" checkpointEnvelopeDigestsAt after))))))) (stage 2 (lambda unrestricted after : (family NativePhysicalCommands) . (prHasherOpen b"checkpoint-hash-bind" (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (phImm full)) (prDigestWrite (prAffine header chunk) chunk (prAffine checkpointEnvelopeDigestsAt checkpointEnvelopeDigestBytes) (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd) (phWhen (naturalNonzero (checkpointEnvelopeTailBytes contract)) (prDigestWrite (phImm (naturalAdd header (naturalMultiply chunk full))) (checkpointEnvelopeTailBytes contract) (phImm (naturalAdd checkpointEnvelopeDigestsAt (naturalMultiply checkpointEnvelopeDigestBytes full)))) (prHasherClose after))))))) (stage 3 (lambda unrestricted after : (family NativePhysicalCommands) . (phCall prSysFdatasync (phArgs3 (phSlot prSlotCheckpointOut) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"checkpoint-sync" 0 after))) (stage 4 (lambda unrestricted after : (family NativePhysicalCommands) . (prClose b"checkpoint-close" prSlotCheckpointOut after)) (stage 5 (lambda unrestricted after : (family NativePhysicalCommands) . (phCall prSysRename (phArgs3 (phState (prPath prCheckpointTemporaryPath)) (phState (prPath prCheckpointOutPath)) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"checkpoint-rename" 0 after))) (stage 6 (lambda unrestricted after : (family NativePhysicalCommands) . (prOpenPath prCheckpointDirectoryPath prOpenDirectory prSlotCheckpointOut (phCall prSysFsync (phArgs3 (phSlot prSlotCheckpointOut) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"checkpoint-directory-sync" 0 (prClose b"checkpoint-directory-close" prSlotCheckpointOut after))))) tail))))))))))))))) -- an invocation's publication: its contract's updates, one invocation def prPublishCheckpointStages = (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (lambda unrestricted stages : Nat . (prPublishCheckpointCounting contract stages (checkpointEnvelopeContractUpdates contract) 1))) def prPublishCheckpoint = (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (prPublishCheckpointStages contract prPublishStages)) -- ---- 5. the recipes ---- def prKindIndex = (lambda unrestricted kind : (family NativePhysicalEmbeddedComponentKind) . (naturalSaturatingSubtract (nativePhysicalEmbeddedComponentTag kind) 1)) def prRecipeFills = (lambda unrestricted fills : (family NvidiaPlanHostRecipeFills) . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate NvidiaPlanHostRecipeFills (lambda unrestricted current : (family NvidiaPlanHostRecipeFills) . (family NativePhysicalCommands)) fills (branch NvidiaPlanHostRecipeFillsEnd . tail) (branch NvidiaPlanHostRecipeFillsNext host tableExtent kind rest induction . (nativeLaunchRecipeLoadOperands (phSlot prSlotExe) nvidiaPlanHostStaging (phLoad (prDescriptorOffsetWord (prKindIndex kind))) (phLoad (prDescriptorLengthWord (prKindIndex kind))) host tableExtent prSlotStatus phIdentity induction))))) -- ---- 6. the schedule ---- def prFileSlot = (lambda unrestricted file : (family NvidiaPlanHostFile) . (eliminate NvidiaPlanHostFile (lambda unrestricted current : (family NvidiaPlanHostFile) . Nat) file (branch NvidiaPlanHostInput . prSlotInput) (branch NvidiaPlanHostCheckpointIn . prSlotCheckpointIn) (branch NvidiaPlanHostCheckpointOut . prSlotCheckpointOut) (branch NvidiaPlanHostPredictions . prSlotPredictions) (branch NvidiaPlanHostResult . prSlotResult))) def prOrdinal = (lambda unrestricted gpPut : Nat . (naturalSaturatingSubtract gpPut 1)) def prSemaphoreStride : Nat = 32 def prStampAddress = (lambda unrestricted gpPut : Nat . (lambda unrestricted which : Nat . (naturalAdd nvidiaPlanHostStaging (naturalAdd which (naturalMultiply nvidiaPlanHostTimestampRecord (prOrdinal gpPut)))))) def prClock = (lambda unrestricted destination : (family NativePhysicalOperand) . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall prSysClockGettime (phArgs3 (phImm prClockRealtime) destination (phImm 0)) b"" phDiscard tail))) def prStamp = (lambda unrestricted gpPut : Nat . (lambda unrestricted stride : Nat . (lambda unrestricted which : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (prClock (prAffine (prStampAddress gpPut which) (naturalMultiply nvidiaPlanHostTimestampRecord stride)) tail))))) def prSemaphoreHost = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (phBufferHost sem)))) -- One submission: stamp, fence, gpPut staged in the state and written to -- USERD and the doorbell rung with the channel's token by PlanHost's -- publication routine (store, SFENCE, store: a membarrier does not order -- the write-combined gpPut ahead of the doorbell), fence, wait for the -- submission's own semaphore slot, stamp. def prSubmit = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted gpPut : Nat . (lambda unrestricted stride : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (prStamp gpPut stride 0 (prFence (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prGPPut) (prAffine gpPut stride)) (phLoadToken (prFence (phPublishOperand (naturalAdd (phUSERDHost layout) nvidiaPlanHostUSERDGPPutOffset) (prAffine gpPut stride) (prFence (phNext (constructor NativePhysicalOperation NativePhysicalFenceWait (prAffine (naturalAdd (prSemaphoreHost layout) (naturalMultiply prSemaphoreStride (prOrdinal gpPut))) (naturalMultiply prSemaphoreStride stride)) (phImm nvidiaPlanHostFenceValue) (phWord nvidiaPlanHostFenceMaximumPolls) (phWord nvidiaPlanHostFenceInterval)) (prStamp gpPut stride 16 tail))))))))))))) -- the ring the host writes entries into, and how many entries it has def prRingHost = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (phBufferHost gpfifo)))) def prRingEntries = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . Nat) layout (branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . (naturalSelect (phIsUVM lifecycle) nvidiaPlanHostUVMGPFIFOEntries nvidiaPlanHostDirectGPFIFOEntries)))) -- A submission of the plan issued again: its entry into the ring at -- ordinal gpPut - 1 and its semaphore slot (both releases) cleared, then -- the ring entry published and the slot awaited as in prSubmit. The piece's -- pushbuffer releases the same slot at every issue; the slot is cleared -- only after the issue before was awaited, so the wait sees this issue's -- release. def prReissue = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted gpPut : Nat . (lambda unrestricted stride : Nat . (lambda unrestricted piece : Nat . (lambda unrestricted pieceStride : Nat . (lambda unrestricted entry : Nat . (lambda unrestricted entryStride : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted slot = (naturalAdd (prSemaphoreHost layout) (naturalMultiply prSemaphoreStride piece)) in (let unrestricted slotStride = (naturalMultiply prSemaphoreStride pieceStride) in (prStamp gpPut stride 0 (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (prAffine (naturalAdd (prRingHost layout) (naturalMultiply 8 (prOrdinal gpPut))) (naturalMultiply 8 stride)) (prAffine entry entryStride)) (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (prAffine slot slotStride) (phImm 0)) (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (prAffine (naturalAdd slot 16) slotStride) (phImm 0)) (prFence (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prGPPut) (prAffine gpPut stride)) (phLoadToken (prFence (phPublishOperand (naturalAdd (phUSERDHost layout) nvidiaPlanHostUSERDGPPutOffset) (prAffine gpPut stride) (prFence (phNext (constructor NativePhysicalOperation NativePhysicalFenceWait (prAffine slot slotStride) (phImm nvidiaPlanHostFenceValue) (phWord nvidiaPlanHostFenceMaximumPolls) (phWord nvidiaPlanHostFenceInterval)) (prStamp gpPut stride 16 tail)))))))))))))))))))))) -- a list of commands run before `tail` def prSplice = (lambda unrestricted commands : (family NativePhysicalCommands) . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate NativePhysicalCommands (lambda unrestricted current : (family NativePhysicalCommands) . (family NativePhysicalCommands)) commands (branch NativePhysicalCommandsEnd . tail) (branch NativePhysicalCommandsNext head rest induction . (constructor NativePhysicalCommands NativePhysicalCommandsNext head induction))))) -- `destination` = `source` x `scale` (words of the state), by doubling and -- adding over the bits of the scale, low bit first; `source` is consumed -- (it ends doubled once per bit) def prScaleBits = (lambda unrestricted destination : Nat . (lambda unrestricted source : Nat . (lambda unrestricted scale : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (app (app (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted remaining : Nat . (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)))) (lambda unrestricted remaining : Nat . (lambda unrestricted after : (family NativePhysicalCommands) . after)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (pi unrestricted remaining : Nat . (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands))) . (lambda unrestricted remaining : Nat . (lambda unrestricted after : (family NativePhysicalCommands) . (phWhen (naturalNonzero remaining) (lambda unrestricted next : (family NativePhysicalCommands) . (phWhen (naturalModuloUnchecked remaining 2) (lambda unrestricted doubled : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState destination) (phLoad destination) (phLoad source)) doubled)) (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState source) (phLoad source) (phLoad source)) (induction (naturalDivideUnchecked remaining 2) next)))) after))))) 64) scale) tail))))) -- the cursor: base + the checkpoint read's invocations x scale def prCursorFromCheckpoint = (lambda unrestricted base : Nat . (lambda unrestricted scale : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prCursor) (phImm base)) (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prCursorScratch) (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeInvocationsAt))) (prScaleBits prCursor prCursorScratch scale tail)))))) def prWriteFrom = (lambda unrestricted identity : Bytes . (lambda unrestricted file : (family NvidiaPlanHostFile) . (lambda unrestricted source : (family NativePhysicalOperand) . (lambda unrestricted extent : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phCall phSysWrite (phArgs3 (phSlot (prFileSlot file)) source (phImm extent)) b"" (phStore prSlotStatus) (prAssertStatus identity extent tail))))))) -- the status block appended to a result: PlanHost's RM status slots, then -- its UVM status slots def prStatusBlockCommands = (lambda unrestricted tail : (family NativePhysicalCommands) . (phCopyStateToState prStatusBlock (phRMStatusSlot 0) 80 (phCopyStateToState (naturalAdd prStatusBlock 80) phUVMStatusRecord 80 tail))) -- how far a file's offsets move: a checkpoint's payload follows its header def prFileShift = (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (lambda unrestricted file : (family NvidiaPlanHostFile) . (eliminate NvidiaPlanHostFile (lambda unrestricted current : (family NvidiaPlanHostFile) . Nat) file (branch NvidiaPlanHostInput . 0) (branch NvidiaPlanHostCheckpointIn . (checkpointEnvelopeHeaderBytes contract)) (branch NvidiaPlanHostCheckpointOut . (checkpointEnvelopeHeaderBytes contract)) (branch NvidiaPlanHostPredictions . 0) (branch NvidiaPlanHostResult . 0)))) -- 1 for the checkpoint being written def prIsCheckpointOut = (lambda unrestricted file : (family NvidiaPlanHostFile) . (naturalEqual (prFileSlot file) prSlotCheckpointOut)) -- Copy through a state scratch word: host/device mappings are not state -- offsets, and the typed command language keeps that distinction explicit. def prAssertMappedWord = (lambda unrestricted identity : Bytes . (lambda unrestricted host : Nat . (lambda unrestricted expected : Nat . (lambda unrestricted after : (family NativePhysicalCommands) . (phCopyMappedToState host prExpected 8 (prAssertEqual identity (phLoad prExpected) (phImm expected) after)))))) -- Arithmetic is checked before pread: a zero record count, counter overflow -- or file offset overflow never becomes a successful read from another row. def prReadCyclic = (lambda unrestricted host : Nat . (lambda unrestricted extent : Nat . (lambda unrestricted offset : Nat . (lambda unrestricted recordBytes : Nat . (lambda unrestricted count : Nat . (lambda unrestricted index : Nat . (lambda unrestricted stride : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeCyclicRecordOffsetRoutine (phArgs (phState prWordScratch) (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeUpdatesAt)) (prAffine index stride) (phImm count) (phImm recordBytes) (phImm offset)) (phStore prSlotStatus)) (prAssertStatus b"cyclic-record-offset" 0 (phCall prSysPread (phArgs (phSlot prSlotInput) (phImm host) (phImm extent) (phLoad prWordScratch) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"cyclic-read-extent" extent tail)))))))))))) -- A single bounded sendfile must transfer the entire admitted input. A -- partial transfer rejects by name; no prefix hash is accepted as its identity. -- The enclosing request already checked the input's exact extent. This -- content binding is additional to the checkpoint's schema/data-policy hash. def prBindInputIdentity = (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (lambda unrestricted offset : Nat . (lambda unrestricted inputExtent : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) . (prHasherOpen b"input-identity-hash-bind" (phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prSendOffset) (phImm 0)) (phCall prSysSendfile (phArgs (phSlot prSlotHash) (phSlot prSlotInput) (phState prSendOffset) (phImm inputExtent) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"input-identity-read" inputExtent (phCall phSysRead (phArgs3 (phSlot prSlotHash) (phState prInputIdentity) (phImm checkpointEnvelopeDigestBytes)) b"" (phStore prSlotStatus) (prAssertStatus b"input-identity-hash" checkpointEnvelopeDigestBytes (prHasherClose (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeVersionAt))) (phCall prSysPread (phArgs (phSlot prSlotCheckpointIn) (phState prExpectedDigest) (phImm checkpointEnvelopeDigestBytes) (phImm (naturalAdd (checkpointEnvelopeHeaderBytes contract) offset)) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"input-identity-checkpoint-read" checkpointEnvelopeDigestBytes (prAssertEqual b"input-identity-changed" (phLoad prInputIdentity) (phLoad prExpectedDigest) (prAssertEqual b"input-identity-changed" (phLoad (naturalAdd prInputIdentity 8)) (phLoad (naturalAdd prExpectedDigest 8)) (prAssertEqual b"input-identity-changed" (phLoad (naturalAdd prInputIdentity 16)) (phLoad (naturalAdd prExpectedDigest 16)) (prAssertEqual b"input-identity-changed" (phLoad (naturalAdd prInputIdentity 24)) (phLoad (naturalAdd prExpectedDigest 24)) (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd) tail))))))))))))))))))) def prSteps = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted submissionCount : Nat . (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (lambda unrestricted final : (family NativePhysicalCommands) . (app (eliminate NvidiaPlanHostSteps (lambda unrestricted current : (family NvidiaPlanHostSteps) . (pi unrestricted rest : (family NativePhysicalCommands) . (family NativePhysicalCommands))) steps (branch NvidiaPlanHostStepsEnd . (lambda unrestricted rest : (family NativePhysicalCommands) . rest)) (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prSubmit layout gpPut stride (induction rest)))) (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . (lambda unrestricted rest : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBegin (phWord count)) (bodyInduction (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd) (tailInduction rest)))))) (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (phCall prSysPread (phArgs (phSlot (prFileSlot file)) (phImm host) (phImm extent) (prAffine (naturalAdd offset (prFileShift contract file)) stride) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (phWhen (naturalIsZero tolerateEmpty) (prAssertStatus b"read-extent" extent) (phWhen tolerateEmpty (prAssertOneOf b"read-extent" prStatus 0 extent) (induction rest)))))) (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prReadCyclic host extent offset recordBytes count index stride (induction rest)))) (branch NvidiaPlanHostStepWrite file host extent tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prWriteFrom b"write-extent" file (phImm host) extent (induction rest)))) (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (phCall prSysPwrite (phArgs (phSlot (prFileSlot file)) (phImm host) (phImm extent) (phImm (naturalAdd offset (prFileShift contract file))) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"write-extent" extent (induction rest))))) (branch NvidiaPlanHostStepWriteStat file tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prWriteFrom b"write-stat" file (phState prStat) prStatExtent (induction rest)))) (branch NvidiaPlanHostStepWriteStatus file tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prStatusBlockCommands (prWriteFrom b"write-status" file (phState prStatusBlock) prStatusBlockExtent (induction rest))))) (branch NvidiaPlanHostStepWriteTimestamps file tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prWriteFrom b"write-timestamps" file (phImm nvidiaPlanHostStaging) (naturalMultiply nvidiaPlanHostTimestampRecord submissionCount) (induction rest)))) (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (phCopyMappedToState host (naturalAdd prStat statOffset) extent (induction rest)))) (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prStamp gpPut stride which (induction rest)))) (branch NvidiaPlanHostStepFill host payload tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (phFill host payload (induction rest)))) (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prAssertMappedWord identity host expected (induction rest)))) (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prBindInputIdentity contract offset inputExtent (induction rest)))) (branch NvidiaPlanHostStepWriteInputIdentity tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prWriteFrom b"input-identity-write" (constructor NvidiaPlanHostFile NvidiaPlanHostCheckpointOut) (phState prInputIdentity) checkpointEnvelopeDigestBytes (induction rest)))) (branch NvidiaPlanHostStepBeginCheckpoint tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prCheckpointTemporary contract (induction rest)))) (branch NvidiaPlanHostStepOperation tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalSystemCall (phLoad (naturalAdd prRequest 16)) (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard) (prCheckpointTemporary contract (induction rest))))) (branch NvidiaPlanHostStepSync file tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (phCall prSysFsync (phArgs3 (phSlot (prFileSlot file)) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"sync" 0 (induction rest))))) (branch NvidiaPlanHostStepDataSync file tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (phCall prSysFdatasync (phArgs3 (phSlot (prFileSlot file)) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"sync" 0 (induction rest))))) (branch NvidiaPlanHostStepClose file tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (nat-eliminate (lambda unrestricted publishing : Nat . (family NativePhysicalCommands)) (prClose b"close" (prFileSlot file) (induction rest)) (lambda unrestricted q : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (prPublishCheckpoint contract (phTelemetry prTelemetryPublished b"request-host:checkpoint-published" (induction rest))))) (prIsCheckpointOut file)))) (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prReissue layout gpPut stride piece pieceStride entry entryStride (induction rest)))) (branch NvidiaPlanHostStepCommands commands tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prSplice commands (induction rest)))) (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prCursorFromCheckpoint base scale (induction rest)))) (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState prCursorOffset) (phLoad prCursor) (phImm delta)) (phCall prSysPread (phArgs (phSlot (prFileSlot file)) (phImm host) (phImm extent) (phLoad prCursorOffset) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus) (prAssertStatus b"stream-read" extent (induction rest)))))) (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState prCursor) (phLoad prCursor) (phImm bytes)) (induction rest)))) (branch NvidiaPlanHostStepCheckpointBegin tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prCheckpointTemporary contract (induction rest)))) (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . (lambda unrestricted rest : (family NativePhysicalCommands) . (prPublishCheckpointCounting contract prPublishStages updates invocations (induction rest))))) final)))))) -- The number of submissions a schedule issues, for the pairing's contract -- against its plan's submission count. def nvidiaPlanHostStepSubmissions = (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (eliminate NvidiaPlanHostSteps (lambda unrestricted current : (family NvidiaPlanHostSteps) . Nat) steps (branch NvidiaPlanHostStepsEnd . 0) (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . (naturalAdd 1 induction)) (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . (naturalAdd (naturalMultiply count bodyInduction) tailInduction)) (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . induction) (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . induction) (branch NvidiaPlanHostStepWrite file host extent tail induction . induction) (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . induction) (branch NvidiaPlanHostStepWriteStat file tail induction . induction) (branch NvidiaPlanHostStepWriteStatus file tail induction . induction) (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction) (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction) (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction) (branch NvidiaPlanHostStepFill host payload tail induction . induction) (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction) (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . induction) (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction) (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction) (branch NvidiaPlanHostStepOperation tail induction . induction) (branch NvidiaPlanHostStepSync file tail induction . induction) (branch NvidiaPlanHostStepDataSync file tail induction . induction) (branch NvidiaPlanHostStepClose file tail induction . induction) (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . (naturalAdd 1 induction)) (branch NvidiaPlanHostStepCommands commands tail induction . induction) (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction) (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . induction) (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction) (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction) (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction))) -- The bytes a schedule moves through a file, for the pairing's contract -- against its checkpoint extent: reads of a file, or writes of it. def nvidiaPlanHostStepBytesRead = (lambda unrestricted which : (family NvidiaPlanHostFile) . (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (eliminate NvidiaPlanHostSteps (lambda unrestricted current : (family NvidiaPlanHostSteps) . Nat) steps (branch NvidiaPlanHostStepsEnd . 0) (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction) (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . (naturalAdd (naturalMultiply count bodyInduction) tailInduction)) (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . (naturalAdd (naturalMultiply (naturalEqual (prFileSlot file) (prFileSlot which)) extent) induction)) (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (naturalAdd (naturalMultiply (naturalEqual prSlotInput (prFileSlot which)) extent) induction)) (branch NvidiaPlanHostStepWrite file host extent tail induction . induction) (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . induction) (branch NvidiaPlanHostStepWriteStat file tail induction . induction) (branch NvidiaPlanHostStepWriteStatus file tail induction . induction) (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction) (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction) (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction) (branch NvidiaPlanHostStepFill host payload tail induction . induction) (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction) (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . (naturalAdd (naturalMultiply (naturalEqual prSlotCheckpointIn (prFileSlot which)) checkpointEnvelopeDigestBytes) induction)) (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction) (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction) (branch NvidiaPlanHostStepOperation tail induction . induction) (branch NvidiaPlanHostStepSync file tail induction . induction) (branch NvidiaPlanHostStepDataSync file tail induction . induction) (branch NvidiaPlanHostStepClose file tail induction . induction) (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . induction) (branch NvidiaPlanHostStepCommands commands tail induction . induction) (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction) (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . (naturalAdd (naturalMultiply (naturalEqual (prFileSlot file) (prFileSlot which)) extent) induction)) (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction) (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction) (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction)))) def nvidiaPlanHostStepBytesWritten = (lambda unrestricted which : (family NvidiaPlanHostFile) . (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (eliminate NvidiaPlanHostSteps (lambda unrestricted current : (family NvidiaPlanHostSteps) . Nat) steps (branch NvidiaPlanHostStepsEnd . 0) (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction) (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . (naturalAdd (naturalMultiply count bodyInduction) tailInduction)) (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . induction) (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . induction) (branch NvidiaPlanHostStepWrite file host extent tail induction . (naturalAdd (naturalMultiply (naturalEqual (prFileSlot file) (prFileSlot which)) extent) induction)) (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . (naturalAdd (naturalMultiply (naturalEqual (prFileSlot file) (prFileSlot which)) extent) induction)) (branch NvidiaPlanHostStepWriteStat file tail induction . induction) (branch NvidiaPlanHostStepWriteStatus file tail induction . induction) (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction) (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction) (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction) (branch NvidiaPlanHostStepFill host payload tail induction . induction) (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction) (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . induction) (branch NvidiaPlanHostStepWriteInputIdentity tail induction . (naturalAdd (naturalMultiply (naturalEqual prSlotCheckpointOut (prFileSlot which)) checkpointEnvelopeDigestBytes) induction)) (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction) (branch NvidiaPlanHostStepOperation tail induction . induction) (branch NvidiaPlanHostStepSync file tail induction . induction) (branch NvidiaPlanHostStepDataSync file tail induction . induction) (branch NvidiaPlanHostStepClose file tail induction . induction) (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . induction) (branch NvidiaPlanHostStepCommands commands tail induction . induction) (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction) (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . induction) (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction) (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction) (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction)))) -- ---- the schedule, unrolled ---- -- The steps as they run: every repeat body once per iteration, its -- loop-affine operands (gpPut, stamps, file offsets) at that iteration, so -- no stride and no repeat remains. What the certificate below and a -- pairing's contracts walk. def prAt = (lambda unrestricted base : Nat . (lambda unrestricted stride : Nat . (lambda unrestricted iteration : Nat . (naturalAdd base (naturalMultiply stride iteration))))) def nvidiaPlanHostStepsUnrolled = (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (app (app (eliminate NvidiaPlanHostSteps (lambda unrestricted current : (family NvidiaPlanHostSteps) . (pi unrestricted iteration : Nat . (pi unrestricted rest : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps)))) steps (branch NvidiaPlanHostStepsEnd . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . rest))) (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSubmit (prAt gpPut stride iteration) 0 (induction iteration rest))))) (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (app (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted after : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps))) (lambda unrestricted after : (family NvidiaPlanHostSteps) . after) (lambda unrestricted inner : Nat . (lambda unrestricted earlier : (pi unrestricted after : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps)) . (lambda unrestricted after : (family NvidiaPlanHostSteps) . (earlier (bodyInduction inner after))))) count) (tailInduction iteration rest))))) (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRead file host extent (prAt offset stride iteration) 0 tolerateEmpty (induction iteration rest))))) (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReadCyclic host extent offset recordBytes count (prAt index stride iteration) 0 (induction iteration rest))))) (branch NvidiaPlanHostStepWrite file host extent tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWrite file host extent (induction iteration rest))))) (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteAt file host extent offset (induction iteration rest))))) (branch NvidiaPlanHostStepWriteStat file tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteStat file (induction iteration rest))))) (branch NvidiaPlanHostStepWriteStatus file tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteStatus file (induction iteration rest))))) (branch NvidiaPlanHostStepWriteTimestamps file tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteTimestamps file (induction iteration rest))))) (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRecordStat host statOffset extent (induction iteration rest))))) (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepStamp (prAt gpPut stride iteration) 0 which (induction iteration rest))))) (branch NvidiaPlanHostStepFill host payload tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepFill host payload (induction iteration rest))))) (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepAssertWord identity host expected (induction iteration rest))))) (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBindInputIdentity offset inputExtent (induction iteration rest))))) (branch NvidiaPlanHostStepWriteInputIdentity tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteInputIdentity (induction iteration rest))))) (branch NvidiaPlanHostStepBeginCheckpoint tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBeginCheckpoint (induction iteration rest))))) (branch NvidiaPlanHostStepOperation tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepOperation (induction iteration rest))))) (branch NvidiaPlanHostStepSync file tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSync file (induction iteration rest))))) (branch NvidiaPlanHostStepDataSync file tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepDataSync file (induction iteration rest))))) (branch NvidiaPlanHostStepClose file tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepClose file (induction iteration rest))))) (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReissue (prAt gpPut stride iteration) 0 (prAt piece pieceStride iteration) 0 (prAt entry entryStride iteration) 0 (induction iteration rest))))) (branch NvidiaPlanHostStepCommands commands tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCommands commands (induction iteration rest))))) (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCursorFromCheckpoint base scale (induction iteration rest))))) (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReadAtCursor file host extent delta (induction iteration rest))))) (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCursorAdvance bytes (induction iteration rest))))) (branch NvidiaPlanHostStepCheckpointBegin tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointBegin (induction iteration rest))))) (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . (lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointPublish updates invocations (induction iteration rest)))))) 0) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd))) -- ---- the schedule's certificate ---- -- What Runtime.ArenaCertificate's schedule certificate sees of an unrolled -- schedule: a file read or a fill writes host memory, a file write or a -- recorded word reads it, a submission is awaited at its gpPut (every -- submission is waited on its own semaphore slot before the host goes on), -- and a stamp observes the submission it names. The status, statistics and -- timestamp writes read PlanHost's own state, not the arena. def prEvent = (lambda unrestricted event : (family ArenaEvent) . (lambda unrestricted rest : (family ArenaEvents) . (constructor ArenaEvents ArenaEventsNext event rest))) def nvidiaPlanHostStepEvents = (lambda unrestricted unrolled : (family NvidiaPlanHostSteps) . (eliminate NvidiaPlanHostSteps (lambda unrestricted current : (family NvidiaPlanHostSteps) . (family ArenaEvents)) unrolled (branch NvidiaPlanHostStepsEnd . (constructor ArenaEvents ArenaEventsEnd)) (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . (prEvent (constructor ArenaEvent ArenaAwait gpPut) induction)) (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . tailInduction) (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . (prEvent (constructor ArenaEvent ArenaHostWrite host extent) induction)) (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (prEvent (constructor ArenaEvent ArenaHostWrite host extent) induction)) (branch NvidiaPlanHostStepWrite file host extent tail induction . (prEvent (constructor ArenaEvent ArenaHostRead host extent) induction)) (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . (prEvent (constructor ArenaEvent ArenaHostRead host extent) induction)) (branch NvidiaPlanHostStepWriteStat file tail induction . induction) (branch NvidiaPlanHostStepWriteStatus file tail induction . induction) (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction) (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . (prEvent (constructor ArenaEvent ArenaHostRead host extent) induction)) (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . (prEvent (constructor ArenaEvent ArenaObserve gpPut) induction)) (branch NvidiaPlanHostStepFill host payload tail induction . (prEvent (constructor ArenaEvent ArenaHostWrite host (bytes-length payload)) induction)) (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . (prEvent (constructor ArenaEvent ArenaHostRead host 8) induction)) (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . induction) (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction) (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction) (branch NvidiaPlanHostStepOperation tail induction . induction) (branch NvidiaPlanHostStepSync file tail induction . induction) (branch NvidiaPlanHostStepDataSync file tail induction . induction) (branch NvidiaPlanHostStepClose file tail induction . induction) (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . (prEvent (constructor ArenaEvent ArenaAwait gpPut) induction)) (branch NvidiaPlanHostStepCommands commands tail induction . induction) (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction) (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . (prEvent (constructor ArenaEvent ArenaHostWrite host extent) induction)) (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction) (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction) (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction))) -- 1 when every submission of the plan is awaited, in order, each at a -- generation of its own, and no staged range is overwritten, read back or -- left unconsumed (Runtime.ArenaCertificate.arenaScheduleCertificate) def nvidiaPlanHostScheduleCertified = (lambda unrestricted submissionCount : Nat . (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (arenaScheduleCertificate submissionCount (nvidiaPlanHostStepEvents (nvidiaPlanHostStepsUnrolled steps))))) -- 1 when the reads of a file, as they run, take it in order and whole: each -- starts where the one before ended, the first at 0, the last ending at the -- file's extent. (A byte count alone admits a chunk read twice and another -- never.) def nvidiaPlanHostFileReadsTile = (lambda unrestricted which : (family NvidiaPlanHostFile) . (lambda unrestricted fileExtent : Nat . (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (app (eliminate NvidiaPlanHostSteps (lambda unrestricted current : (family NvidiaPlanHostSteps) . (pi unrestricted next : Nat . Nat)) (nvidiaPlanHostStepsUnrolled steps) (branch NvidiaPlanHostStepsEnd . (lambda unrestricted next : Nat . (naturalEqual next fileExtent))) (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction) (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . tailInduction) (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . (lambda unrestricted next : Nat . (let unrestricted same = (naturalEqual (prFileSlot file) (prFileSlot which)) in (naturalAnd (naturalSelect same (naturalEqual offset next) 1) (induction (naturalAdd next (naturalSelect same extent 0))))))) (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (lambda unrestricted next : Nat . (naturalAnd (naturalIsZero (naturalEqual prSlotInput (prFileSlot which))) (induction next)))) (branch NvidiaPlanHostStepWrite file host extent tail induction . induction) (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . induction) (branch NvidiaPlanHostStepWriteStat file tail induction . induction) (branch NvidiaPlanHostStepWriteStatus file tail induction . induction) (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction) (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction) (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction) (branch NvidiaPlanHostStepFill host payload tail induction . induction) (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction) (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . (lambda unrestricted next : Nat . (let unrestricted same = (naturalEqual prSlotCheckpointIn (prFileSlot which)) in (naturalAnd (naturalSelect same (naturalEqual offset next) 1) (induction (naturalAdd next (naturalSelect same checkpointEnvelopeDigestBytes 0))))))) (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction) (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction) (branch NvidiaPlanHostStepOperation tail induction . induction) (branch NvidiaPlanHostStepSync file tail induction . induction) (branch NvidiaPlanHostStepDataSync file tail induction . induction) (branch NvidiaPlanHostStepClose file tail induction . induction) (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . induction) (branch NvidiaPlanHostStepCommands commands tail induction . induction) (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction) (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . (lambda unrestricted next : Nat . (naturalAnd (naturalIsZero (naturalEqual (prFileSlot file) (prFileSlot which))) (induction next)))) (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction) (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction) (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction)) 0)))) -- a little-endian natural of `count` bytes def nvidiaPlanHostLittleNatural = (lambda unrestricted count : Nat . (lambda unrestricted bytes : Bytes . (app (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted rest : Bytes . Nat)) (lambda unrestricted rest : Bytes . 0) (lambda unrestricted p : Nat . (lambda unrestricted induction : (pi unrestricted rest : Bytes . Nat) . (lambda unrestricted rest : Bytes . (naturalAdd (byte-to-nat (bytes-head rest)) (naturalMultiply 256 (induction (bytes-tail rest))))))) count) bytes))) -- entry `ordinal` of a table of 8-byte little-endian words def nvidiaPlanHostTableWord = (lambda unrestricted table : Bytes . (lambda unrestricted ordinal : Nat . (nvidiaPlanHostLittleNatural 8 (dataBytesDropValidated (naturalMultiply 8 ordinal) table)))) -- 1 when every issue again, as it runs, writes the ring entry the -- realization gave its piece (`entries`: the plan's GPFIFO table) def nvidiaPlanHostReissuesAdmitted = (lambda unrestricted entries : Bytes . (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (eliminate NvidiaPlanHostSteps (lambda unrestricted current : (family NvidiaPlanHostSteps) . Nat) (nvidiaPlanHostStepsUnrolled steps) (branch NvidiaPlanHostStepsEnd . 1) (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction) (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . tailInduction) (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . induction) (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index indexStride tail induction . induction) (branch NvidiaPlanHostStepWrite file host extent tail induction . induction) (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . induction) (branch NvidiaPlanHostStepWriteStat file tail induction . induction) (branch NvidiaPlanHostStepWriteStatus file tail induction . induction) (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction) (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction) (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction) (branch NvidiaPlanHostStepFill host payload tail induction . induction) (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction) (branch NvidiaPlanHostStepBindInputIdentity offset extent tail induction . induction) (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction) (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction) (branch NvidiaPlanHostStepOperation tail induction . induction) (branch NvidiaPlanHostStepSync file tail induction . induction) (branch NvidiaPlanHostStepDataSync file tail induction . induction) (branch NvidiaPlanHostStepClose file tail induction . induction) (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . (naturalAnd (naturalEqual entry (nvidiaPlanHostTableWord entries piece)) induction)) (branch NvidiaPlanHostStepCommands commands tail induction . induction) (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction) (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . induction) (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction) (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction) (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction)))) -- ---- the whole request host ---- -- `learner` runs after the recipes are expanded and before anything is -- submitted: the commands that supply parameter words at run time -- (Platform.Linux.Nvidia.PlanHostAdamW), or none. def nvidiaPlanHostRequestCommands = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted hostIdentity : Bytes . (lambda unrestricted programIdentity : Bytes . (lambda unrestricted qmdIdentity : Bytes . (lambda unrestricted pushIdentity : Bytes . (lambda unrestricted gpfifoIdentity : Bytes . (lambda unrestricted programLength : Nat . (lambda unrestricted qmdLength : Nat . (lambda unrestricted pushLength : Nat . (lambda unrestricted gpfifoLength : Nat . (lambda unrestricted submissionCount : Nat . (lambda unrestricted input : (family NvidiaPlanHostInputContract) . (lambda unrestricted contract : (family CheckpointEnvelopeContract) . (lambda unrestricted fills : (family NvidiaPlanHostRecipeFills) . (lambda unrestricted learner : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (prFenceRegister (phPipeCreate (phTelemetryOpen (phTelemetry prTelemetryBegin b"request-host:begin" (prEnvelope hostIdentity programIdentity qmdIdentity pushIdentity gpfifoIdentity programLength qmdLength pushLength gpfifoLength (prRequestOpen input contract (phTelemetry prTelemetryChecked b"request-host:request-checked" (phPrelude (constructor NvidiaPlanHostMode NvidiaPlanHostStrict) layout (phTelemetry prTelemetryChannel b"request-host:channel-ready" (nativeLaunchRecipeStagingCommands nvidiaPlanHostStaging nvidiaPlanHostStagingExtent prSlotStatus phIdentity (prRecipeFills fills (phTelemetry prTelemetryUploaded b"request-host:uploaded" (learner (phTelemetry prTelemetryLearner b"request-host:learner-scalars" (prSteps layout submissionCount contract steps (phTelemetry prTelemetryDone b"request-host:done" (phCall phSysExitGroup (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard (phNext (constructor NativePhysicalOperation NativePhysicalHaltSuccess) (constructor NativePhysicalCommands NativePhysicalCommandsEnd))))))))))))))))))))))))))))))))))) -- ---- admission ---- -- A fixed-input probe needs the authenticated envelope and recipe loader, -- but no text request or checkpoint protocol. The standard host still owns -- channel creation, uploads, submission, completion and telemetry. Tables -- are expanded only after their destination buffers have been mapped. def nvidiaPlanHostRecipeCommands = (lambda unrestricted hostIdentity : Bytes . (lambda unrestricted programIdentity : Bytes . (lambda unrestricted qmdIdentity : Bytes . (lambda unrestricted pushIdentity : Bytes . (lambda unrestricted gpfifoIdentity : Bytes . (lambda unrestricted programLength : Nat . (lambda unrestricted qmdLength : Nat . (lambda unrestricted pushLength : Nat . (lambda unrestricted gpfifoLength : Nat . (lambda unrestricted recipes : (family NvidiaPlanHostRecipeFills) . (nvidiaPlanHostPreparedCommands (prEnvelope hostIdentity programIdentity qmdIdentity pushIdentity gpfifoIdentity programLength qmdLength pushLength gpfifoLength) (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeStagingCommands nvidiaPlanHostStaging nvidiaPlanHostStagingExtent prSlotStatus phIdentity (prRecipeFills recipes tail)))))))))))))) -- The layout's placement certified (PlanHost.nvidiaPlanHostLayoutCertified, -- the recipe staging area among the host's mappings), the schedule's order -- certified (above), and every host range the request host writes into or reads out of lies inside a -- host-mapped buffer of its layout (PlanHost.nvidiaPlanHostContains): each -- recipe's expanded table, and each step's file transfer, fill, write or -- recorded word. A table larger than its buffer used to be built and then -- copied past the mapping at run time. def prRecipesAdmitted = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted fills : (family NvidiaPlanHostRecipeFills) . (eliminate NvidiaPlanHostRecipeFills (lambda unrestricted current : (family NvidiaPlanHostRecipeFills) . Nat) fills (branch NvidiaPlanHostRecipeFillsEnd . 1) (branch NvidiaPlanHostRecipeFillsNext host tableExtent kind rest induction . (naturalAnd (nvidiaPlanHostContains layout host tableExtent) induction))))) def prStepsAdmitted = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted submissionCount : Nat . (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (eliminate NvidiaPlanHostSteps (lambda unrestricted current : (family NvidiaPlanHostSteps) . Nat) steps (branch NvidiaPlanHostStepsEnd . 1) (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction) (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . (naturalAnd bodyInduction tailInduction)) (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . (naturalAnd (nvidiaPlanHostContains layout host extent) induction)) (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (naturalAnd (nvidiaPlanHostContains layout host extent) (naturalAnd (naturalLess 0 count) (naturalAnd (naturalLess 0 extent) (naturalAnd (naturalLessOrEqual (naturalAdd offset extent) recordBytes) (naturalAnd (naturalLessOrEqual (naturalMultiply count recordBytes) cyclicRecordFileMaximum) (naturalAnd (naturalLessOrEqual index cyclicRecordWordMaximum) (naturalAnd (naturalLessOrEqual stride cyclicRecordWordMaximum) induction)))))))) (branch NvidiaPlanHostStepWrite file host extent tail induction . (naturalAnd (nvidiaPlanHostContains layout host extent) induction)) (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . (naturalAnd (nvidiaPlanHostContains layout host extent) induction)) (branch NvidiaPlanHostStepWriteStat file tail induction . induction) (branch NvidiaPlanHostStepWriteStatus file tail induction . induction) (branch NvidiaPlanHostStepWriteTimestamps file tail induction . (naturalAnd (naturalLessOrEqual (naturalMultiply nvidiaPlanHostTimestampRecord submissionCount) nvidiaPlanHostStagingExtent) induction)) (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . (naturalAnd (nvidiaPlanHostContains layout host extent) induction)) (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction) (branch NvidiaPlanHostStepFill host payload tail induction . (naturalAnd (nvidiaPlanHostContains layout host (bytes-length payload)) induction)) (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . (naturalAnd (nvidiaPlanHostContains layout host 8) induction)) (branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . (naturalAnd (naturalLess 0 inputExtent) (naturalAnd (naturalLessOrEqual inputExtent cyclicRecordFileMaximum) induction))) (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction) (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction) (branch NvidiaPlanHostStepOperation tail induction . induction) (branch NvidiaPlanHostStepSync file tail induction . induction) (branch NvidiaPlanHostStepDataSync file tail induction . induction) (branch NvidiaPlanHostStepClose file tail induction . induction) (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction . induction) (branch NvidiaPlanHostStepCommands commands tail induction . induction) (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction) (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . (naturalAnd (nvidiaPlanHostContains layout host extent) induction)) (branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction) (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction) (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction))))) def nvidiaPlanHostRequestAdmitted = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted submissionCount : Nat . (lambda unrestricted fills : (family NvidiaPlanHostRecipeFills) . (lambda unrestricted steps : (family NvidiaPlanHostSteps) . (naturalAnd (nvidiaPlanHostLayoutAdmitted layout) (naturalAnd (nvidiaPlanHostLayoutCertified layout (constructor ArenaResidents ArenaResidentsNext (constructor ArenaResident ArenaResidentValue b"recipe-staging" nvidiaPlanHostStaging nvidiaPlanHostStagingExtent 0x1000) (constructor ArenaResidents ArenaResidentsEnd))) (naturalAnd (prRecipesAdmitted layout fills) (naturalAnd (naturalAnd (prStepsAdmitted layout submissionCount steps) (prStepsAdmitted layout submissionCount (nvidiaPlanHostStepsUnrolled steps))) (naturalAnd (naturalLessOrEqual submissionCount (prRingEntries layout)) (nvidiaPlanHostScheduleCertified submissionCount steps))))))))))