Large source region · 2,012 lines
module Platform.Linux.Nvidia.PlanHostRequest
import Checkpoint.Envelope
import Data.Bytes
import Data.SHA256
import Data.SHA256Constants
import Model.Config
import Model.Parameter
import Model.Word32
import Model.Word64
import Platform.Linux.Nvidia.PlanHost
import Platform.Linux.Nvidia.DeviceBinding
import Runtime.ArenaCertificate
import Runtime.NativeLaunchRecipeLoad
import Runtime.NativePhysicalEmbeddedArtifact
import Runtime.NativePhysicalNativeELF
import Runtime.NativePhysicalProgram
import Runtime.NativeWordDigest
import Runtime.WordDigest
import Runtime.NativeWordArithmetic
import Runtime.NativeFilePlan
import Runtime.NativeCyclicRecordOffset
import Runtime.NativeFiniteWords
import Runtime.CyclicRecordOffset
import Runtime.TextArtifactRequest
import Std.List
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 shared native
-- digest 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
-- A bounded dynamic loop. Resource/submission counts are upper bounds;
-- expansion must retain the predicate, never unroll it into mandatory work.
constructor NvidiaPlanHostStepRepeatUntil
field unrestricted nvidiaPlanHostStepUntilCount : Nat
field unrestricted nvidiaPlanHostStepUntilObserved : (family NativePhysicalOperand)
field unrestricted nvidiaPlanHostStepUntilExpected : (family NativePhysicalOperand)
recursive unrestricted nvidiaPlanHostStepUntilBody
recursive unrestricted nvidiaPlanHostStepUntilTail
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
-- The same reissue without awaiting it: the host stamps, writes the entry,
-- clears the slot and publishes gpPut, then goes on. The channel runs its
-- submissions in order, so a later awaited submission's completion is this
-- one's too; the arena certificate sees no await for it (its writes stay
-- pending until that later await), so it may not end a schedule.
constructor NvidiaPlanHostStepReissueAhead
field unrestricted nvidiaPlanHostStepReissueAheadGPPut : Nat
field unrestricted nvidiaPlanHostStepReissueAheadGPPutStride : Nat
field unrestricted nvidiaPlanHostStepReissueAheadPiece : Nat
field unrestricted nvidiaPlanHostStepReissueAheadPieceStride : Nat
field unrestricted nvidiaPlanHostStepReissueAheadEntry : Nat
field unrestricted nvidiaPlanHostStepReissueAheadEntryStride : Nat
recursive unrestricted nvidiaPlanHostStepReissueAheadTail
-- 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
-- the checkpoint read, published under `restated` (another contract for the
-- same payload layout: a changed learner), its invocations kept and its
-- update count restated as invocations x `perInvocation`
-- (prPublishCheckpointRestated)
constructor NvidiaPlanHostStepCheckpointPublishRestated
field unrestricted nvidiaPlanHostStepCheckpointPublishRestatedContract : (family CheckpointEnvelopeContract)
field unrestricted nvidiaPlanHostStepCheckpointPublishRestatedPerInvocation : Nat
recursive unrestricted nvidiaPlanHostStepCheckpointPublishRestatedTail
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)
-- Envelope hashing completes before device setup. One bounded window and its
-- chaining state serve every component; no component-sized mapping is needed.
-- These regions are part of the interpreter's admitted state extent, disjoint
-- from descriptor words, expected digests, and each other's live values.
def prEnvelopeHashWork : Nat = (prAfter prCursorScratch 8)
def prEnvelopeHashPlan : Nat = (prAfter prEnvelopeHashWork digestWorkBytes)
def prEnvelopeHashCursor : Nat = (prAfter prEnvelopeHashPlan byteDigestChunkPlanBytes)
def prEnvelopeHashBuffer : Nat = (prAfter prEnvelopeHashCursor digestAddressBytes)
-- a scheduled learner's further scalars (Platform.Linux.Nvidia.PlanHostAdamW's
-- warmup-cosine schedule): thirty-two binary64 words, after every other
-- area so that no earlier offset moves
def prScheduleScratch : Nat = (prAfter prEnvelopeHashBuffer byteDigestChunkBufferBytes)
def prScheduleScratchExtent : Nat = 256
def prAreasEnd : Nat = (prAfter prScheduleScratch prScheduleScratchExtent)
-- 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 prSysMunmap : Nat = 11
-- Linux MAP_PRIVATE | MAP_ANONYMOUS; the kernel selects a disjoint address.
def prMapPrivateAnonymous : Nat = (naturalAdd 2 32)
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))))
-- Inspect a mapped checkpoint staging span after its GPU copy has retired.
-- The caller supplies a bank's representation and a span admitted by its
-- host layout. A failed scan halts before that span reaches the checkpoint.
def nvidiaPlanHostRejectNonfiniteMapped =
(lambda unrestricted identity : Bytes .
(lambda unrestricted format : (family NativeFiniteWordFormat) .
(lambda unrestricted host : Nat .
(lambda unrestricted extent : Nat .
(lambda unrestricted tail : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepCommands
(phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine
(nativeFiniteRoutineFor format)
(phArgs3 (phImm host) (phImm extent) (phImm 0))
(phStore prSlotStatus))
(prAssertStatus identity 0
(constructor NativePhysicalCommands NativePhysicalCommandsEnd)))
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))
-- Hashing the executable cannot depend on provider AF_ALG policy. Read whole
-- windows serially into the shared state buffer, retaining the chaining words.
-- Exact reads fail closed (including errors and short reads); the final tail
-- is padded with the original byte count. Descriptor fields are zero-extended
-- u32, so advancing their file cursor by their extent cannot overflow u64.
-- The window, padding and work area are bounded by prAreasFit, independently
-- of executable size. This runs before any request schedule's repeat frame.
def prHashComponent =
(lambda unrestricted index : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phNext
(constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeByteDigestStreamStartRoutine
(phArgs (phLoad (prDescriptorLengthWord index)) (phState prEnvelopeHashPlan)
(phImm 0) (phImm 0) (phImm 0) (phState prEnvelopeHashWork))
(phStore prSlotStatus))
(prAssertStatus b"envelope-hash-start" digestStateBytes
(phNext
(constructor NativePhysicalOperation NativePhysicalStoreWord64
(phState prEnvelopeHashCursor) (phLoad (prDescriptorOffsetWord index)))
(phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (phLoad prEnvelopeHashPlan))
(phCall prSysPread
(phArgs (phSlot prSlotExe) (phState prEnvelopeHashBuffer) (phImm byteDigestChunkBytes)
(phLoad prEnvelopeHashCursor) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
(prAssertStatus b"envelope-hash-read" byteDigestChunkBytes
(phNext
(constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeWordDigestContinueRoutine
(phArgs (phState prEnvelopeHashBuffer) (phImm (naturalDivideUnchecked byteDigestChunkBytes digestBlockBytes))
(phState prDigest) (phImm 0) (phImm 0) (phState prEnvelopeHashWork))
(phStore prSlotStatus))
(prAssertStatus b"envelope-hash-count" digestStateBytes
(phNext
(constructor NativePhysicalOperation NativePhysicalAddWord64
(phState prEnvelopeHashCursor) (phLoad prEnvelopeHashCursor) (phImm byteDigestChunkBytes))
(phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
(phCall prSysPread
(phArgs (phSlot prSlotExe) (phState prEnvelopeHashBuffer) (phLoad (naturalAdd prEnvelopeHashPlan digestAddressBytes))
(phLoad prEnvelopeHashCursor) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
(prAssertEqual b"envelope-hash-read" prStatus (phLoad (naturalAdd prEnvelopeHashPlan digestAddressBytes))
(phNext
(constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeByteDigestStreamFinishRoutine
(phArgs (phState prEnvelopeHashBuffer) (phLoad (naturalAdd prEnvelopeHashPlan digestAddressBytes))
(phState prDigest) (phImm 0) (phLoad (prDescriptorLengthWord index)) (phState prEnvelopeHashWork))
(phStore prSlotStatus))
(prAssertStatus b"envelope-hash-count" digestStateBytes tail))))))))))))))))
-- 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
(prHashComponent index
(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))
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
-- `counts` writes the header's update and invocation counts
def prPublishCheckpointWith =
(lambda unrestricted contract : (family CheckpointEnvelopeContract) .
(lambda unrestricted stages : Nat .
(lambda unrestricted counts :
(pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
(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)
(counts
(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)))))))
(nativeFileCommitStages stages 1 prSlotCheckpointOut prSlotStatus
(phState (prPath prCheckpointTemporaryPath)) (phState (prPath prCheckpointOutPath))
(phState (prPath prCheckpointDirectoryPath)) tail)))))))))))
-- the update count and invocations after this invocation's: the read
-- checkpoint's plus `updates` and `invocations`
def prPublishCheckpointCounting =
(lambda unrestricted contract : (family CheckpointEnvelopeContract) .
(lambda unrestricted stages : Nat .
(lambda unrestricted updates : Nat .
(lambda unrestricted invocations : Nat .
(prPublishCheckpointWith contract stages
(lambda unrestricted after : (family NativePhysicalCommands) .
(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))
after))))))))
-- A learner change carries the read state to `restated`: the read
-- checkpoint's invocations, and as many updates as `perInvocation` a
-- completed invocation (a learner's updates count its steps, not its
-- data). The checked cyclic-offset routine bounds the invocations and forms
-- the product exactly; it leaves its output untouched on rejection.
def prPublishCheckpointRestated =
(lambda unrestricted restated : (family CheckpointEnvelopeContract) .
(lambda unrestricted perInvocation : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted invocations =
(phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeInvocationsAt)) in
(phNext
(constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeCyclicRecordOffsetRoutine
(phArgs (phState prWordScratch) invocations (phImm 0)
(phImm (naturalDivideUnchecked cyclicRecordFileMaximum perInvocation))
(phImm 1) (phImm 0))
(phStore prSlotStatus))
(prAssertStatus b"checkpoint-restated-invocation-bound" 0
(nativeLaunchRecipeAssertEqual (phLoad prWordScratch) invocations
b"checkpoint-restated-invocation-bound"
(phNext
(constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeCyclicRecordOffsetRoutine
(phArgs (phState prWordScratch) invocations (phImm 0)
(phImm (naturalDivideUnchecked cyclicRecordFileMaximum perInvocation))
(phImm perInvocation) (phImm 0))
(phStore prSlotStatus))
(prAssertStatus b"checkpoint-restated-update-product" 0
(prPublishCheckpointWith restated prPublishStages
(lambda unrestricted after : (family NativePhysicalCommands) .
(phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64
(phState (naturalAdd prCheckpointHeaderOut checkpointEnvelopeUpdatesAt))
(phLoad prWordScratch))
(phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64
(phState (naturalAdd prCheckpointHeaderOut checkpointEnvelopeInvocationsAt))
invocations)
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 .
(phRingEntries lifecycle))))
-- The ring has a fixed mapped extent while the scheduler counts all issues.
-- The cyclic-offset primitive checks the extent and wraps the ordinal before
-- a write; its scratch word is dead after this command sequence.
def prStoreRingEntry =
(lambda unrestricted ringBase : (family NativePhysicalOperand) .
(lambda unrestricted entries : Nat .
(lambda unrestricted ordinal : (family NativePhysicalOperand) .
(lambda unrestricted entry : (family NativePhysicalOperand) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine
nativeCyclicRecordOffsetRoutine
(phArgs (phState prWordScratch) ordinal (phImm 0)
(phImm entries) (phImm 8) (phImm 0))
(phStore prSlotStatus))
(prAssertStatus b"gpfifo-ring-offset" 0
(phNext (constructor NativePhysicalOperation NativePhysicalAddWord64
(phState prWordScratch) (phLoad prWordScratch) ringBase)
(phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64
(phLoad prWordScratch) entry) tail)))))))))
-- USERD GP_PUT names the next slot in the configured GPFIFO ring. The issue
-- count stays monotonic for telemetry and token cursors, but the word sent to
-- USERD must wrap with the ring. At issue 32768 on the 3090's 32768-entry
-- UVM ring, publishing 32768 left the GPU idle while the host waited for its
-- semaphore. The cyclic primitive already proves the bounded modulo before
-- it touches the scratch word; a failed computation cannot publish a put.
def prWrapGPFIFOCount =
(lambda unrestricted entries : Nat .
(lambda unrestricted issued : (family NativePhysicalOperand) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phNext (constructor NativePhysicalOperation NativePhysicalMachineRoutine
nativeCyclicRecordOffsetRoutine
(phArgs (phState prWordScratch) issued (phImm 0)
(phImm entries) (phImm 1) (phImm 0))
(phStore prSlotStatus))
(prAssertStatus b"gpfifo-put-wrap" 0 tail)))))
-- 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. The scheduler's issue count is monotonic; the USERD GP_PUT and
-- mapped ring address both wrap at the ABI's entry count. The cyclic-offset
-- routine bounds that write on every iteration instead of extending the
-- mapping as a long training run advances past the first turn of the ring.
-- This core accepts an explicit issue ordinal so a scheduler driven by
-- received state can use the same publication protocol as a counted loop.
-- Both releases belong to the selected, already-retired submission piece.
def prReissueCore =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted ordinal : (family NativePhysicalOperand) .
(lambda unrestricted gpPut : (family NativePhysicalOperand) .
(lambda unrestricted slot : (family NativePhysicalOperand) .
(lambda unrestricted release : (family NativePhysicalOperand) .
(lambda unrestricted entry : (family NativePhysicalOperand) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(prStoreRingEntry (phImm (prRingHost layout)) (prRingEntries layout) ordinal entry
(phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 slot (phImm 0))
(phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 release (phImm 0))
(prFence
(phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prGPPut) gpPut)
(phLoadToken
(prFence
(prWrapGPFIFOCount (prRingEntries layout) gpPut
(phPublishOperand (naturalAdd (phUSERDHost layout) nvidiaPlanHostUSERDGPPutOffset) (phLoad prWordScratch)
(prFence
(phNext (constructor NativePhysicalOperation NativePhysicalFenceWait
slot (phImm nvidiaPlanHostFenceValue)
(phWord nvidiaPlanHostFenceMaximumPolls) (phWord nvidiaPlanHostFenceInterval)) tail)))))))))))))))))
)
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
(prReissueCore layout (prAffine (prOrdinal gpPut) stride) (prAffine gpPut stride)
(prAffine slot slotStride) (prAffine (naturalAdd slot 16) slotStride)
(prAffine entry entryStride) (prStamp gpPut stride 16 tail)))))))))))))
-- A fresh channel starts at zero even after a learner checkpoint is restored.
-- Increment before any publication, refusing u64 exhaustion; commit the issue
-- count only after this submission's fence. The caller owns counterAt and must
-- initialize it once, outside its update loop. There is one in-flight issue.
def prReissueCounted =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted counterAt : Nat .
(lambda unrestricted piece : Nat .
(lambda unrestricted entry : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted slot = (naturalAdd (prSemaphoreHost layout) (naturalMultiply prSemaphoreStride piece)) in
(nativeCheckedWordAdd (phState prGPPut) (phLoad counterAt) (phImm 1)
prSlotStatus b"submission-counter-overflow"
(prReissueCore layout (phLoad counterAt) (phLoad prGPPut)
(phImm slot) (phImm (naturalAdd slot 16)) (phImm entry)
(phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64
(phState counterAt) (phLoad prGPPut)) tail)))))))))
-- prReissue without the wait (NvidiaPlanHostStepReissueAhead)
def prReissueAhead =
(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
(prStoreRingEntry (phImm (prRingHost layout))
(prRingEntries layout) (prAffine (prOrdinal gpPut) 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
(prWrapGPFIFOCount (prRingEntries layout) (prAffine gpPut stride)
(phPublishOperand (naturalAdd (phUSERDHost layout) nvidiaPlanHostUSERDGPPutOffset) (phLoad prWordScratch)
(prFence 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 completed updates x scale. A
-- checkpoint may be published partway through an invocation, so invocation
-- count cannot locate the next token window after a restart.
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 checkpointEnvelopeUpdatesAt)))
(prScaleBits prCursor prCursorScratch scale tail))))))
-- A resumed invocation owns only its current input file. Reduce the saved
-- cumulative update count by the invocation length before locating its next
-- record. The shared cyclic-offset routine checks the product against the
-- signed file-offset range and leaves the cursor untouched on rejection.
def prCursorFromCheckpointCycle =
(lambda unrestricted records : Nat .
(lambda unrestricted recordBytes : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phNext
(constructor NativePhysicalOperation NativePhysicalMachineRoutine
nativeCyclicRecordOffsetRoutine
(phArgs (phState prCursor)
(phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeUpdatesAt))
(phImm 0) (phImm records) (phImm recordBytes) (phImm 0))
(phStore prSlotStatus))
(prAssertStatus b"checkpoint-cycle-cursor" 0 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)))))))
-- A positional write updates a bounded record field without changing the
-- sequential output cursor. Both arena and state operands use the same owner.
def prWriteFromAt =
(lambda unrestricted identity : Bytes .
(lambda unrestricted file : (family NvidiaPlanHostFile) .
(lambda unrestricted source : (family NativePhysicalOperand) .
(lambda unrestricted extent : Nat .
(lambda unrestricted offset : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall prSysPwrite
(phArgs (phSlot (prFileSlot file)) source (phImm extent)
(phImm offset) (phImm 0) (phImm 0)) 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.
-- A resumed invocation compares the digest already in its checkpoint; an
-- explicitly admitted next invocation hashes its new input and writes that
-- digest into the next checkpoint. The latter requires its caller to assert
-- the completed-update boundary and retain the prior input in the run ledger.
def prInputIdentityComparisonCount =
(lambda unrestricted comparePrevious : Nat .
(nat-eliminate
(lambda unrestricted flag : Nat . (family NativePhysicalOperand))
(phImm 0)
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored : (family NativePhysicalOperand) .
(phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeVersionAt))))
comparePrevious))
def prBindInputIdentityWith = (lambda unrestricted comparePrevious : Nat .
(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
(prInputIdentityComparisonCount comparePrevious))
(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 prBindInputIdentity = (prBindInputIdentityWith 1)
-- the read checkpoint's input identity (at `offset` in its payload) taken
-- as this request's, for state carried on without new input
-- (WriteInputIdentity then writes it)
def prInputIdentityFromCheckpoint = (lambda unrestricted contract : (family CheckpointEnvelopeContract) .
(lambda unrestricted offset : Nat . (lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall prSysPread (phArgs (phSlot prSlotCheckpointIn) (phState prInputIdentity)
(phImm checkpointEnvelopeDigestBytes) (phImm (naturalAdd (checkpointEnvelopeHeaderBytes contract) offset))
(phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
(prAssertStatus b"input-identity-checkpoint-read" checkpointEnvelopeDigestBytes tail)))))
def prBindNextInputIdentity = (prBindInputIdentityWith 0)
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 NvidiaPlanHostStepRepeatUntil count observed expected body tail bodyInduction tailInduction .
(lambda unrestricted rest : (family NativePhysicalCommands) .
(phNext (constructor NativePhysicalOperation NativePhysicalRepeatBegin (phWord count))
(bodyInduction
(phNext (constructor NativePhysicalOperation NativePhysicalRepeatEndWhen observed expected)
(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 NvidiaPlanHostStepReissueAhead gpPut stride piece pieceStride entry entryStride tail induction .
(lambda unrestricted rest : (family NativePhysicalCommands) .
(prReissueAhead 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))))
(branch NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation tail induction .
(lambda unrestricted rest : (family NativePhysicalCommands) .
(prPublishCheckpointRestated restated perInvocation (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 NvidiaPlanHostStepRepeatUntil count observed expected 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 NvidiaPlanHostStepReissueAhead 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) (branch NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation 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 NvidiaPlanHostStepRepeatUntil count observed expected 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 NvidiaPlanHostStepReissueAhead 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) (branch NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation 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 NvidiaPlanHostStepRepeatUntil count observed expected 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 NvidiaPlanHostStepReissueAhead 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) (branch NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation 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)))))
-- Runtime expansion retains dynamic predicates. The proof view expands their
-- entire cap, so admission sees every possible affine address and generation.
-- A derived schedule may have no full chunks. Normalize that empty loop
-- before encoding native commands, whose repeat ABI requires positive count.
-- Eliminate only the 0/1 flag, never the potentially large iteration count.
def nvidiaPlanHostRepeatSteps =
(lambda unrestricted count : Nat .
(lambda unrestricted body : (family NvidiaPlanHostSteps) .
(lambda unrestricted tail : (family NvidiaPlanHostSteps) .
(nat-eliminate
(lambda unrestricted flag : Nat . (family NvidiaPlanHostSteps))
tail
(lambda unrestricted predecessor : Nat .
(lambda unrestricted induction : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepRepeat count body tail)))
(naturalNonzero count)))))
def nvidiaPlanHostStepsExpand =
(lambda unrestricted preservePredicate : Nat .
(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 NvidiaPlanHostStepRepeatUntil count observed expected body tail bodyInduction tailInduction .
(nat-eliminate
(lambda unrestricted mode : Nat .
(pi unrestricted iteration : Nat .
(pi unrestricted rest : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps))))
(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))))
(lambda unrestricted predecessor : Nat .
(lambda unrestricted ignored :
(pi unrestricted iteration : Nat .
(pi unrestricted rest : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps))) .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepRepeatUntil
count observed expected body (tailInduction iteration rest))))))
preservePredicate))
(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 NvidiaPlanHostStepReissueAhead gpPut stride piece pieceStride entry entryStride tail induction .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepReissueAhead (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)))))
(branch NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation tail induction .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation
(induction iteration rest))))))
0) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd))))
def nvidiaPlanHostStepsUnrolled = (nvidiaPlanHostStepsExpand 1)
def nvidiaPlanHostStepsForBounds = (nvidiaPlanHostStepsExpand 0)
-- ---- 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 NvidiaPlanHostStepRepeatUntil count observed expected 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 NvidiaPlanHostStepReissueAhead 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 . (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) (branch NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation 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 (nvidiaPlanHostStepsForBounds 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))
(nvidiaPlanHostStepsForBounds 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 NvidiaPlanHostStepRepeatUntil count observed expected 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 NvidiaPlanHostStepReissueAhead 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) (branch NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation 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)
(nvidiaPlanHostStepsForBounds steps)
(branch NvidiaPlanHostStepsEnd . 1)
(branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction)
(branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . tailInduction)
(branch NvidiaPlanHostStepRepeatUntil count observed expected 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 NvidiaPlanHostStepReissueAhead 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) (branch NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation 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 nvidiaPlanHostRequestCommandsOn =
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(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"
(phPreludeOn device (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))))))))))))))))))))))))))))))))))))
def nvidiaPlanHostRequestCommands = (nvidiaPlanHostRequestCommandsOn nvidiaDeviceZero)
-- ---- 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 nvidiaPlanHostRecipeCommandsOn =
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(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) .
(nvidiaPlanHostPreparedCommandsOn device
(prEnvelope hostIdentity programIdentity qmdIdentity pushIdentity gpfifoIdentity
programLength qmdLength pushLength gpfifoLength)
(lambda unrestricted tail : (family NativePhysicalCommands) .
(nativeLaunchRecipeStagingCommands nvidiaPlanHostStaging nvidiaPlanHostStagingExtent prSlotStatus phIdentity
(prRecipeFills recipes tail)))))))))))))))
def nvidiaPlanHostRecipeCommands = (nvidiaPlanHostRecipeCommandsOn nvidiaDeviceZero)
-- 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 .
(naturalAnd (naturalLessOrEqual gpPut (prRingEntries layout)) induction))
(branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . (naturalAnd bodyInduction tailInduction))
(branch NvidiaPlanHostStepRepeatUntil count observed expected 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 .
(naturalAnd (naturalLess piece (prRingEntries layout)) induction))
(branch NvidiaPlanHostStepReissueAhead gpPut stride piece pieceStride entry entryStride tail induction .
(naturalAnd (naturalLess piece (prRingEntries layout)) 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) (branch NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation 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 (nvidiaPlanHostStepsForBounds steps)))
(naturalAnd (naturalLessOrEqual submissionCount
(naturalDivideUnchecked nvidiaPlanHostStagingExtent nvidiaPlanHostTimestampRecord))
(nvidiaPlanHostScheduleCertified submissionCount steps))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.