Large source region · 2,921 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.PlanHostPeers
import Platform.Linux.Nvidia.DeviceBinding
import Runtime.ArenaCertificate
import Runtime.NativeFileStatus
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.
-- Every SHA-256 this host computes -- the envelope's components, a
-- checkpoint's chunks and manifest, the input's content identity -- is
-- prDigestFileRange: Alpha's own streamed digest (Runtime.NativeWordDigest)
-- over bounded pread windows. None depends on the kernel's crypto sockets
-- (AF_ALG), which container hosts may deny (comparisons/h100/README.md:
-- two of three RunPod H100 hosts refused them, 2026-10-10).
-- 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
-- Semantic observation boundaries retain their ordering through schedule
-- transforms. The interpreter chooses the recorder; the system never emits
-- bytes or reaches into recorder-private storage.
constructor NvidiaPlanHostStepBoundary
field unrestricted nvidiaPlanHostStepBoundaryPhase : Nat
field unrestricted nvidiaPlanHostStepBoundaryName : Bytes
recursive unrestricted nvidiaPlanHostStepBoundaryTail
-- 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
-- From here on, the steps run on session `session`'s card (PlanHost's
-- sessions, docs/PRD-8XH100-ON-A-BUDGET.md F4): submissions issue and await
-- on that card's channel, with its layout, token and doorbell. A schedule
-- starts on session 0; a repeat's body ends on the session it began on
-- (nvidiaPlanHostSessionsBalanced), so its tail runs where the repeat
-- began. A host of one card never names another.
constructor NvidiaPlanHostStepSession
field unrestricted nvidiaPlanHostStepSessionIndex : Nat
recursive unrestricted nvidiaPlanHostStepSessionTail
-- Await a submission issued ahead (NvidiaPlanHostStepReissueAhead) on the
-- current session: its piece's semaphore slot, as a reissue awaits its own.
-- gpPut names the submission awaited; gpPut and piece advance by their
-- strides per iteration of an enclosing repeat. What lets a host of
-- several cards issue every card's work, then wait for all of it.
constructor NvidiaPlanHostStepAwait
field unrestricted nvidiaPlanHostStepAwaitGPPut : Nat
field unrestricted nvidiaPlanHostStepAwaitGPPutStride : Nat
field unrestricted nvidiaPlanHostStepAwaitPiece : Nat
field unrestricted nvidiaPlanHostStepAwaitPieceStride : Nat
recursive unrestricted nvidiaPlanHostStepAwaitTail
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 = nativeFileStatusScratchBytes
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 prGPPut : Nat = (prAfter prIdentityScratch nativePhysicalEmbeddedIdentityLength)
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)
-- The streamed file digest's state (prDigestFileRange). One bounded window
-- and its chaining state serve every file range the host hashes -- the
-- envelope's components, checkpoint chunks and manifests, the input -- one at
-- a time; no range-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 prStreamDigestWork : Nat = (prAfter prCursorScratch 8)
def prStreamDigestPlan : Nat = (prAfter prStreamDigestWork digestWorkBytes)
def prStreamDigestCursor : Nat = (prAfter prStreamDigestPlan byteDigestChunkPlanBytes)
def prStreamDigestBuffer : Nat = (prAfter prStreamDigestCursor 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 prStreamDigestBuffer byteDigestChunkBufferBytes)
def prScheduleScratchExtent : Nat = 256
-- Checkpoint manifest commitments survive later input and chunk hashing.
-- These are distinct from the working digest and from data-stream identity,
-- and like the schedule scratch they follow every other area so that no
-- earlier offset moves.
def prInputIdentityExtent : Nat = (prAfter prScheduleScratch prScheduleScratchExtent)
def prCheckpointInputManifest : Nat = (prAfter prInputIdentityExtent nativePhysicalWordBytes)
def prCheckpointOutputManifest : Nat = (prAfter prCheckpointInputManifest checkpointEnvelopeDigestBytes)
def prAreasEnd : Nat = (prAfter prCheckpointOutputManifest checkpointEnvelopeDigestBytes)
-- 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
-- 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 = phSysFstat
def prSysLseek : Nat = 8
def prSysPread : Nat = 17
def prSysPwrite : Nat = 18
def prSysFsync : Nat = phSysFsync
def prSysFdatasync : Nat = 75
def prSysClockGettime : Nat = 228
def prSysPrctl : Nat = 157
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 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
-- These boundaries surround the retired-token loop, after checkpoint loading
-- and before final count/status publication. Their clock is the native host's
-- monotonic clock; neither boundary is a device timer or a civil timestamp.
def prTelemetryGenerationBegin : Nat = 7
def prTelemetryGenerationEnd : Nat = 8
-- A schedule places this only after its learning quantity is host-readable.
-- The selected system capture plan supplies its meaning and exact source.
def prTelemetryLearningValue : Nat = (succ prTelemetryGenerationEnd)
-- Placed by the owner after all checkpoint-to-device restoration completes.
def prTelemetryStateRestored : Nat = (succ prTelemetryLearningValue)
-- Persistence reports intent separately from reaching a writable temporary
-- checkpoint. Only the existing post-sync publication boundary means commit.
def prTelemetryCheckpointPreparing : Nat = (succ prTelemetryStateRestored)
def prTelemetryCheckpointWriting : Nat = (succ prTelemetryCheckpointPreparing)
def prTelemetryInputBound : Nat = (succ prTelemetryCheckpointWriting)
def prGenerationBegin =
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phTelemetry prTelemetryGenerationBegin b"request-host:generation-begin" tail))
def prGenerationEnd =
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phTelemetry prTelemetryGenerationEnd b"request-host:generation-end" tail))
-- ---- 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 ----
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))
-- The SHA-256 of `extent` bytes of the file in `fileSlot` from `offset`,
-- written to the 32-byte state area `destination`: Alpha's own streamed
-- digest (Runtime.NativeWordDigest; one compression owner, Runtime.WordDigest)
-- over whole windows read serially into the shared state buffer, retaining
-- the chaining words between them. Hashing must not depend on a provider's
-- kernel-crypto policy, so there is no AF_ALG path and no fallback.
-- * The start routine refuses an extent of 2^32 bytes or more (it plans
-- full windows and the tail from a u32 total), naming `<name>-hash-start`.
-- * Every read is exact: an error or short read -- a file shorter than
-- offset + extent -- refuses by `<name>-hash-read`.
-- * The tail is padded with the whole range's byte count, never the tail's.
-- `offset` and `extent` are operands. `offset` is read once, into the cursor,
-- before the window loop opens, and `extent` only outside it, so a caller's
-- loop-affine offset (a checkpoint's n-th chunk) is resolved in the caller's
-- repeat frame; the window loop is a nested repeat with its own frame. The
-- window, padding and work area are bounded by prAreasFit, independently of
-- file size. `destination` also receives each window's intermediate chaining
-- output, so it must not alias a value the caller still needs; the final
-- digest overwrites it. Descriptor and request extents are zero-extended u32
-- or plan constants, so advancing the u64 cursor cannot overflow.
def prDigestFileRange =
(lambda unrestricted name : Bytes .
(lambda unrestricted fileSlot : Nat .
(lambda unrestricted offset : (family NativePhysicalOperand) .
(lambda unrestricted extent : (family NativePhysicalOperand) .
(lambda unrestricted destination : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted tailBytes = (phLoad (naturalAdd prStreamDigestPlan digestAddressBytes)) in
(phNext
(constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeByteDigestStreamStartRoutine
(phArgs extent (phState prStreamDigestPlan)
(phImm 0) (phImm 0) (phImm 0) (phState prStreamDigestWork))
(phStore prSlotStatus))
(prAssertStatus (bytes-append name b"-hash-start") digestStateBytes
(phNext
(constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prStreamDigestCursor) offset)
(phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (phLoad prStreamDigestPlan))
(phCall prSysPread
(phArgs (phSlot fileSlot) (phState prStreamDigestBuffer) (phImm byteDigestChunkBytes)
(phLoad prStreamDigestCursor) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
(prAssertStatus (bytes-append name b"-hash-read") byteDigestChunkBytes
(phNext
(constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeWordDigestContinueRoutine
(phArgs (phState prStreamDigestBuffer) (phImm (naturalDivideUnchecked byteDigestChunkBytes digestBlockBytes))
(phState destination) (phImm 0) (phImm 0) (phState prStreamDigestWork))
(phStore prSlotStatus))
(prAssertStatus (bytes-append name b"-hash-count") digestStateBytes
(phNext
(constructor NativePhysicalOperation NativePhysicalAddWord64
(phState prStreamDigestCursor) (phLoad prStreamDigestCursor) (phImm byteDigestChunkBytes))
(phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd)
(phCall prSysPread
(phArgs (phSlot fileSlot) (phState prStreamDigestBuffer) tailBytes
(phLoad prStreamDigestCursor) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
(prAssertEqual (bytes-append name b"-hash-read") prStatus tailBytes
(phNext
(constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeByteDigestStreamFinishRoutine
(phArgs (phState prStreamDigestBuffer) tailBytes
(phState destination) (phImm 0) extent (phState prStreamDigestWork))
(phStore prSlotStatus))
(prAssertStatus (bytes-append name b"-hash-count") digestStateBytes tail)))))))))))))))))))))
-- a component's bytes in this executable, at the offset and length its
-- descriptor gives; this runs before any request schedule's repeat frame
def prHashComponent =
(lambda unrestricted index : Nat .
(prDigestFileRange b"envelope" prSlotExe
(phLoad (prDescriptorOffsetWord index)) (phLoad (prDescriptorLengthWord index)) prDigest))
-- 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) .
(prDigestFileRange b"checkpoint-chunk" fileSlot offset (phImm extent) prDigest
(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 header is a compact manifest: fixed contract/counters plus every
-- payload chunk digest and canonical padding. Hashing it commits to that
-- checkpoint without rereading the payload. This is a manifest hash, never
-- presented as the SHA-256 of the complete checkpoint file. The digest reads
-- with pread at explicit offsets, preserving the caller's descriptor position.
def prCheckpointManifest =
(lambda unrestricted contract : (family CheckpointEnvelopeContract) .
(lambda unrestricted fileSlot : Nat .
(lambda unrestricted destination : Nat .
(prDigestFileRange b"checkpoint-manifest" fileSlot
(phImm 0) (phImm (checkpointEnvelopeHeaderBytes contract)) destination))))
-- 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)
(prChunksCheck contract prSlotCheckpointIn (phLoad (naturalAdd prCheckpointHeaderIn checkpointEnvelopeFullChunksAt)) version
(phNext (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted version)
(prCheckpointManifest contract prSlotCheckpointIn prCheckpointInputManifest
(phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd) 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) .
(prDigestFileRange b"checkpoint-readback" prSlotCheckpointOut offset (phImm extent) prDigest
(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) .
(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))))
(prCheckpointManifest contract prSlotCheckpointOut prCheckpointOutputManifest 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))))
-- the request's timer slack to 1 ns (prctl PR_SET_TIMERSLACK): every fence
-- wait's nanosleep then lasts its interval, not the interval plus Linux's
-- default 50 us (PlanHost's nvidiaPlanHostFenceInterval)
def prTimerSlackOption : Nat = 29
def prTimerSlack =
(lambda unrestricted tail : (family NativePhysicalCommands) .
(phCall prSysPrctl (phArgs3 (phImm prTimerSlackOption) (phImm 1) (phImm 0)) b"" phDiscard tail))
-- 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 prSubmitS =
(lambda unrestricted session : Nat .
(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))
(phLoadTokenS session
(prFence
(phPublishOperandS session (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))))))))))))))
def prSubmit =
(prSubmitS 0)
-- 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 prReissueCoreS =
(lambda unrestricted session : Nat .
(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)
(phLoadTokenS session
(prFence
(prWrapGPFIFOCount (prRingEntries layout) gpPut
(phPublishOperandS session (naturalAdd (phUSERDHost layout) nvidiaPlanHostUSERDGPPutOffset) (phLoad prWordScratch)
(prFence
(phNext (constructor NativePhysicalOperation NativePhysicalFenceWait
slot (phImm nvidiaPlanHostFenceValue)
(phWord nvidiaPlanHostFenceMaximumPolls) (phWord nvidiaPlanHostFenceInterval)) tail)))))))))))))))))
))
def prReissueCore =
(prReissueCoreS 0)
def prReissueS =
(lambda unrestricted session : Nat .
(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
(prReissueCoreS session layout (prAffine (prOrdinal gpPut) stride) (prAffine gpPut stride)
(prAffine slot slotStride) (prAffine (naturalAdd slot 16) slotStride)
(prAffine entry entryStride) (prStamp gpPut stride 16 tail))))))))))))))
def prReissue =
(prReissueS 0)
-- 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 prReissueCountedS =
(lambda unrestricted session : Nat .
(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"
(prReissueCoreS session layout (phLoad counterAt) (phLoad prGPPut)
(phImm slot) (phImm (naturalAdd slot 16)) (phImm entry)
(phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64
(phState counterAt) (phLoad prGPPut)) tail))))))))))
def prReissueCounted =
(prReissueCountedS 0)
-- the wait of NvidiaPlanHostStepAwait: the piece's slot (its release),
-- then the stamp an awaited reissue records
def prAwaitS =
(lambda unrestricted session : Nat .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted gpPut : Nat .
(lambda unrestricted stride : Nat .
(lambda unrestricted piece : Nat .
(lambda unrestricted pieceStride : Nat .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(let unrestricted slot = (naturalAdd (prSemaphoreHost layout) (naturalMultiply prSemaphoreStride piece)) in
(phNext (constructor NativePhysicalOperation NativePhysicalFenceWait
(prAffine slot (naturalMultiply prSemaphoreStride pieceStride)) (phImm nvidiaPlanHostFenceValue)
(phWord nvidiaPlanHostFenceMaximumPolls) (phWord nvidiaPlanHostFenceInterval))
(prStamp gpPut stride 16 tail))))))))))
-- prReissue without the wait (NvidiaPlanHostStepReissueAhead)
def prReissueAheadS =
(lambda unrestricted session : Nat .
(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))
(phLoadTokenS session
(prFence
(prWrapGPFIFOCount (prRingEntries layout) (prAffine gpPut stride)
(phPublishOperandS session (naturalAdd (phUSERDHost layout) nvidiaPlanHostUSERDGPPutOffset) (phLoad prWordScratch)
(prFence tail))))))))))))))))))))))
def prReissueAhead =
(prReissueAheadS 0)
-- 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))))))))))))
-- The digest must read the entire admitted input exactly (prDigestFileRange):
-- a short read 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) .
(phNext (constructor NativePhysicalOperation NativePhysicalStoreWord64 (phState prInputIdentityExtent) (phImm inputExtent))
(prDigestFileRange b"input-identity" prSlotInput (phImm 0) (phImm inputExtent) prInputIdentity
(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)
-- The schedule has one semantic interpreter. `emit` chooses its output
-- representation; `boundary` supplies the recorder effect after a committed
-- checkpoint. Typed capture and legacy commands therefore share all file,
-- learner, submission, repeat and checkpoint ordering mechanisms.
def nvidiaPlanHostSessionStepsWith =
(lambda unrestricted A : Type 0 .
(lambda unrestricted emit : (pi unrestricted fragment : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (pi unrestricted rest : A . A)) .
(lambda unrestricted boundary : (pi unrestricted phase : Nat . (pi unrestricted name : Bytes . (pi unrestricted rest : A . A))) .
(lambda unrestricted layouts : (pi unrestricted session : Nat . (family NvidiaPlanHostLayout)) .
(lambda unrestricted submissionCount : Nat .
(lambda unrestricted contract : (family CheckpointEnvelopeContract) .
(lambda unrestricted steps : (family NvidiaPlanHostSteps) .
(lambda unrestricted final : A .
(app
(eliminate NvidiaPlanHostSteps
(lambda unrestricted current : (family NvidiaPlanHostSteps) . (pi unrestricted session : Nat . (pi unrestricted rest : A . A)))
steps
(branch NvidiaPlanHostStepsEnd . (lambda unrestricted session : Nat . (lambda unrestricted rest : A . rest)))
(branch NvidiaPlanHostStepSubmit gpPut stride tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) . (prSubmitS session (layouts session) gpPut stride after))
(induction session rest)))))
(branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBegin (phWord count)))
(bodyInduction session
(emit (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEnd))
(tailInduction session rest)))))))
(branch NvidiaPlanHostStepRepeatUntil count observed expected body tail bodyInduction tailInduction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (phNext (constructor NativePhysicalOperation NativePhysicalRepeatBegin (phWord count)))
(bodyInduction session
(emit (phNext (constructor NativePhysicalOperation NativePhysicalRepeatEndWhen observed expected))
(tailInduction session rest)))))))
(branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (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)
after))))
(induction session rest)))))
(branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index stride tail induction . (lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prReadCyclic host extent offset recordBytes count index stride after))
(induction session rest)))))
(branch NvidiaPlanHostStepWrite file host extent tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prWriteFrom b"write-extent" file (phImm host) extent after))
(induction session rest)))))
(branch NvidiaPlanHostStepWriteAt file host extent offset tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (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 after)))
(induction session rest)))))
(branch NvidiaPlanHostStepWriteStat file tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prWriteFrom b"write-stat" file (phState prStat) prStatExtent after))
(induction session rest)))))
(branch NvidiaPlanHostStepWriteStatus file tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prStatusBlockCommands (prWriteFrom b"write-status" file (phState prStatusBlock) prStatusBlockExtent after)))
(induction session rest)))))
(branch NvidiaPlanHostStepWriteTimestamps file tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prWriteFrom b"write-timestamps" file (phImm nvidiaPlanHostStaging) (naturalMultiply nvidiaPlanHostTimestampRecord submissionCount) after))
(induction session rest)))))
(branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(phCopyMappedToState host (naturalAdd prStat statOffset) extent after))
(induction session rest)))))
(branch NvidiaPlanHostStepStamp gpPut stride which tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) . (prStamp gpPut stride which after))
(induction session rest)))))
(branch NvidiaPlanHostStepFill host payload tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) . (phFill host payload after))
(induction session rest)))))
(branch NvidiaPlanHostStepAssertWord identity host expected tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prAssertMappedWord identity host expected after))
(induction session rest)))))
(branch NvidiaPlanHostStepBindInputIdentity offset inputExtent tail induction . (lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prBindInputIdentity contract offset inputExtent after))
(boundary prTelemetryInputBound b"request-host:input-bound"
(induction session rest))))))
(branch NvidiaPlanHostStepWriteInputIdentity tail induction . (lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prWriteFrom b"input-identity-write" (constructor NvidiaPlanHostFile NvidiaPlanHostCheckpointOut)
(phState prInputIdentity) checkpointEnvelopeDigestBytes after))
(induction session rest)))))
(branch NvidiaPlanHostStepBeginCheckpoint tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(boundary prTelemetryCheckpointPreparing b"request-host:checkpoint-preparing"
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prCheckpointTemporary contract after))
(boundary prTelemetryCheckpointWriting b"request-host:checkpoint-writing"
(induction session rest)))))))
(branch NvidiaPlanHostStepOperation tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(boundary prTelemetryCheckpointPreparing b"request-host:checkpoint-preparing"
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(phNext (constructor NativePhysicalOperation NativePhysicalSystemCall (phLoad (naturalAdd prRequest 16)) (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard)
(prCheckpointTemporary contract after)))
(boundary prTelemetryCheckpointWriting b"request-host:checkpoint-writing"
(induction session rest)))))))
(branch NvidiaPlanHostStepSync file tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(phCall prSysFsync (phArgs3 (phSlot (prFileSlot file)) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
(prAssertStatus b"sync" 0 after)))
(induction session rest)))))
(branch NvidiaPlanHostStepDataSync file tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(phCall prSysFdatasync (phArgs3 (phSlot (prFileSlot file)) (phImm 0) (phImm 0)) b"" (phStore prSlotStatus)
(prAssertStatus b"sync" 0 after)))
(induction session rest)))))
(branch NvidiaPlanHostStepClose file tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(nat-eliminate (lambda unrestricted publishing : Nat . A)
(emit (prClose b"close" (prFileSlot file)) (induction session rest))
(lambda unrestricted q : Nat . (lambda unrestricted ignored : A .
(emit (prPublishCheckpoint contract)
(boundary prTelemetryPublished b"request-host:checkpoint-published" (induction session rest)))))
(prIsCheckpointOut file)))))
(branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prReissueS session (layouts session) gpPut stride piece pieceStride entry entryStride after))
(induction session rest)))))
(branch NvidiaPlanHostStepReissueAhead gpPut stride piece pieceStride entry entryStride tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prReissueAheadS session (layouts session) gpPut stride piece pieceStride entry entryStride after))
(induction session rest)))))
(branch NvidiaPlanHostStepBoundary phase name tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A . (boundary phase name (induction session rest)))))
(branch NvidiaPlanHostStepCommands commands tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) . (prSplice commands after))
(induction session rest)))))
(branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) . (prCursorFromCheckpoint base scale after))
(induction session rest)))))
(branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (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 after))))
(induction session rest)))))
(branch NvidiaPlanHostStepCursorAdvance bytes tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(phNext (constructor NativePhysicalOperation NativePhysicalAddWord64 (phState prCursor) (phLoad prCursor) (phImm bytes)) after))
(induction session rest)))))
(branch NvidiaPlanHostStepCheckpointBegin tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(boundary prTelemetryCheckpointPreparing b"request-host:checkpoint-preparing"
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prCheckpointTemporary contract after))
(boundary prTelemetryCheckpointWriting b"request-host:checkpoint-writing"
(induction session rest)))))))
(branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prPublishCheckpointCounting contract prPublishStages updates invocations after))
(boundary prTelemetryPublished b"request-host:checkpoint-published"
(induction session rest))))))
(branch NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prPublishCheckpointRestated restated perInvocation after))
(boundary prTelemetryPublished b"request-host:checkpoint-published"
(induction session rest))))))
(branch NvidiaPlanHostStepSession next tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A . (induction next rest))))
(branch NvidiaPlanHostStepAwait gpPut stride piece pieceStride tail induction .
(lambda unrestricted session : Nat . (lambda unrestricted rest : A .
(emit (lambda unrestricted after : (family NativePhysicalCommands) .
(prAwaitS session (layouts session) gpPut stride piece pieceStride after))
(induction session rest))))))
0 final)))))))))
-- one card's steps (every step on session 0's layout)
def nvidiaPlanHostStepsWith =
(lambda unrestricted A : Type 0 .
(lambda unrestricted emit : (pi unrestricted fragment : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (pi unrestricted rest : A . A)) .
(lambda unrestricted boundary : (pi unrestricted phase : Nat . (pi unrestricted name : Bytes . (pi unrestricted rest : A . A))) .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(nvidiaPlanHostSessionStepsWith A emit boundary (lambda unrestricted session : Nat . layout))))))
def prSteps =
(nvidiaPlanHostStepsWith (family NativePhysicalCommands)
(lambda unrestricted fragment : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . fragment)
phTelemetry)
-- ---- sessions ----
-- a step kept, or dropped for the rest
def prKeepStep = (lambda unrestricted keep : Nat .
(lambda unrestricted step : (family NvidiaPlanHostSteps) . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(nat-eliminate (lambda unrestricted current : Nat . (family NvidiaPlanHostSteps)) rest
(lambda unrestricted p : Nat . (lambda unrestricted ignored : (family NvidiaPlanHostSteps) . step)) keep))))
-- The session a schedule ends on, begun on `start` (a repeat's tail on the
-- session its body began on: nvidiaPlanHostSessionsBalanced).
def nvidiaPlanHostStepsEndSession =
(lambda unrestricted steps : (family NvidiaPlanHostSteps) . (lambda unrestricted start : Nat .
(app
(eliminate NvidiaPlanHostSteps
(lambda unrestricted c : (family NvidiaPlanHostSteps) . (pi unrestricted current : Nat . Nat))
steps
(branch NvidiaPlanHostStepsEnd . (lambda unrestricted current : Nat . current))
(branch NvidiaPlanHostStepSubmit x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepRepeat x0 r0 r1 i0 i1 . (lambda unrestricted current : Nat . (i1 current)))
(branch NvidiaPlanHostStepRepeatUntil x0 x1 x2 r0 r1 i0 i1 . (lambda unrestricted current : Nat . (i1 current)))
(branch NvidiaPlanHostStepRead x0 x1 x2 x3 x4 x5 r0 i0 . i0)
(branch NvidiaPlanHostStepReadCyclic x0 x1 x2 x3 x4 x5 x6 r0 i0 . i0)
(branch NvidiaPlanHostStepWrite x0 x1 x2 r0 i0 . i0)
(branch NvidiaPlanHostStepWriteAt x0 x1 x2 x3 r0 i0 . i0)
(branch NvidiaPlanHostStepWriteStat x0 r0 i0 . i0)
(branch NvidiaPlanHostStepWriteStatus x0 r0 i0 . i0)
(branch NvidiaPlanHostStepWriteTimestamps x0 r0 i0 . i0)
(branch NvidiaPlanHostStepRecordStat x0 x1 x2 r0 i0 . i0)
(branch NvidiaPlanHostStepStamp x0 x1 x2 r0 i0 . i0)
(branch NvidiaPlanHostStepFill x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepAssertWord x0 x1 x2 r0 i0 . i0)
(branch NvidiaPlanHostStepBindInputIdentity x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepWriteInputIdentity r0 i0 . i0)
(branch NvidiaPlanHostStepBeginCheckpoint r0 i0 . i0)
(branch NvidiaPlanHostStepOperation r0 i0 . i0)
(branch NvidiaPlanHostStepSync x0 r0 i0 . i0)
(branch NvidiaPlanHostStepDataSync x0 r0 i0 . i0)
(branch NvidiaPlanHostStepClose x0 r0 i0 . i0)
(branch NvidiaPlanHostStepReissue x0 x1 x2 x3 x4 x5 r0 i0 . i0)
(branch NvidiaPlanHostStepReissueAhead x0 x1 x2 x3 x4 x5 r0 i0 . i0)
(branch NvidiaPlanHostStepBoundary x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepCommands x0 r0 i0 . i0)
(branch NvidiaPlanHostStepCursorFromCheckpoint x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepReadAtCursor x0 x1 x2 x3 r0 i0 . i0)
(branch NvidiaPlanHostStepCursorAdvance x0 r0 i0 . i0)
(branch NvidiaPlanHostStepCheckpointBegin r0 i0 . i0)
(branch NvidiaPlanHostStepCheckpointPublish x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepCheckpointPublishRestated x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepSession x0 r0 i0 . (lambda unrestricted current : Nat . (i0 x0)))
(branch NvidiaPlanHostStepAwait x0 x1 x2 x3 r0 i0 . i0)
)
start)))
-- 1 when every repeat's body ends on the session it began on, the schedule
-- begun on session 0: what lets the interpreter run a repeat's tail where
-- the repeat began.
def nvidiaPlanHostSessionsBalanced =
(lambda unrestricted steps : (family NvidiaPlanHostSteps) .
(app
(eliminate NvidiaPlanHostSteps
(lambda unrestricted c : (family NvidiaPlanHostSteps) . (pi unrestricted current : Nat . Nat))
steps
(branch NvidiaPlanHostStepsEnd . (lambda unrestricted current : Nat . 1))
(branch NvidiaPlanHostStepSubmit x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepRepeat x0 r0 r1 i0 i1 . (lambda unrestricted current : Nat . (naturalAnd (naturalEqual (nvidiaPlanHostStepsEndSession r0 current) current) (naturalAnd (i0 current) (i1 current)))))
(branch NvidiaPlanHostStepRepeatUntil x0 x1 x2 r0 r1 i0 i1 . (lambda unrestricted current : Nat . (naturalAnd (naturalEqual (nvidiaPlanHostStepsEndSession r0 current) current) (naturalAnd (i0 current) (i1 current)))))
(branch NvidiaPlanHostStepRead x0 x1 x2 x3 x4 x5 r0 i0 . i0)
(branch NvidiaPlanHostStepReadCyclic x0 x1 x2 x3 x4 x5 x6 r0 i0 . i0)
(branch NvidiaPlanHostStepWrite x0 x1 x2 r0 i0 . i0)
(branch NvidiaPlanHostStepWriteAt x0 x1 x2 x3 r0 i0 . i0)
(branch NvidiaPlanHostStepWriteStat x0 r0 i0 . i0)
(branch NvidiaPlanHostStepWriteStatus x0 r0 i0 . i0)
(branch NvidiaPlanHostStepWriteTimestamps x0 r0 i0 . i0)
(branch NvidiaPlanHostStepRecordStat x0 x1 x2 r0 i0 . i0)
(branch NvidiaPlanHostStepStamp x0 x1 x2 r0 i0 . i0)
(branch NvidiaPlanHostStepFill x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepAssertWord x0 x1 x2 r0 i0 . i0)
(branch NvidiaPlanHostStepBindInputIdentity x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepWriteInputIdentity r0 i0 . i0)
(branch NvidiaPlanHostStepBeginCheckpoint r0 i0 . i0)
(branch NvidiaPlanHostStepOperation r0 i0 . i0)
(branch NvidiaPlanHostStepSync x0 r0 i0 . i0)
(branch NvidiaPlanHostStepDataSync x0 r0 i0 . i0)
(branch NvidiaPlanHostStepClose x0 r0 i0 . i0)
(branch NvidiaPlanHostStepReissue x0 x1 x2 x3 x4 x5 r0 i0 . i0)
(branch NvidiaPlanHostStepReissueAhead x0 x1 x2 x3 x4 x5 r0 i0 . i0)
(branch NvidiaPlanHostStepBoundary x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepCommands x0 r0 i0 . i0)
(branch NvidiaPlanHostStepCursorFromCheckpoint x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepReadAtCursor x0 x1 x2 x3 r0 i0 . i0)
(branch NvidiaPlanHostStepCursorAdvance x0 r0 i0 . i0)
(branch NvidiaPlanHostStepCheckpointBegin r0 i0 . i0)
(branch NvidiaPlanHostStepCheckpointPublish x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepCheckpointPublishRestated x0 x1 r0 i0 . i0)
(branch NvidiaPlanHostStepSession x0 r0 i0 . (lambda unrestricted current : Nat . (i0 x0)))
(branch NvidiaPlanHostStepAwait x0 x1 x2 x3 r0 i0 . i0)
)
0))
-- The steps a session runs: those after a switch to it (session 0's also
-- those before the first switch), the switches dropped, repeats kept. Each
-- session is a card of its own channel, ring, semaphores and layout, so
-- each projection is certified alone exactly as a one-card schedule is
-- (nvidiaPlanHostScheduleCertified, nvidiaPlanHostReissuesAdmitted).
def nvidiaPlanHostStepsOfSession =
(lambda unrestricted target : Nat . (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
(app
(eliminate NvidiaPlanHostSteps
(lambda unrestricted c : (family NvidiaPlanHostSteps) . (pi unrestricted current : Nat . (family NvidiaPlanHostSteps)))
steps
(branch NvidiaPlanHostStepsEnd . (lambda unrestricted current : Nat . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))
(branch NvidiaPlanHostStepSubmit x0 x1 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSubmit x0 x1 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepRepeat x0 r0 r1 i0 i1 . (lambda unrestricted current : Nat . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRepeat x0 (i0 current) (i1 current))))
(branch NvidiaPlanHostStepRepeatUntil x0 x1 x2 r0 r1 i0 i1 . (lambda unrestricted current : Nat . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRepeatUntil x0 x1 x2 (i0 current) (i1 current))))
(branch NvidiaPlanHostStepRead x0 x1 x2 x3 x4 x5 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRead x0 x1 x2 x3 x4 x5 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepReadCyclic x0 x1 x2 x3 x4 x5 x6 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReadCyclic x0 x1 x2 x3 x4 x5 x6 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepWrite x0 x1 x2 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWrite x0 x1 x2 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepWriteAt x0 x1 x2 x3 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteAt x0 x1 x2 x3 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepWriteStat x0 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteStat x0 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepWriteStatus x0 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteStatus x0 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepWriteTimestamps x0 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteTimestamps x0 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepRecordStat x0 x1 x2 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRecordStat x0 x1 x2 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepStamp x0 x1 x2 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepStamp x0 x1 x2 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepFill x0 x1 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepFill x0 x1 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepAssertWord x0 x1 x2 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepAssertWord x0 x1 x2 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepBindInputIdentity x0 x1 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBindInputIdentity x0 x1 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepWriteInputIdentity r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteInputIdentity (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepBeginCheckpoint r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBeginCheckpoint (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepOperation r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepOperation (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepSync x0 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSync x0 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepDataSync x0 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepDataSync x0 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepClose x0 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepClose x0 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepReissue x0 x1 x2 x3 x4 x5 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReissue x0 x1 x2 x3 x4 x5 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepReissueAhead x0 x1 x2 x3 x4 x5 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReissueAhead x0 x1 x2 x3 x4 x5 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepBoundary x0 x1 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBoundary x0 x1 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepCommands x0 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCommands x0 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepCursorFromCheckpoint x0 x1 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCursorFromCheckpoint x0 x1 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepReadAtCursor x0 x1 x2 x3 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReadAtCursor x0 x1 x2 x3 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepCursorAdvance x0 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCursorAdvance x0 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepCheckpointBegin r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointBegin (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepCheckpointPublish x0 x1 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointPublish x0 x1 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepCheckpointPublishRestated x0 x1 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointPublishRestated x0 x1 (i0 current)) (i0 current))))
(branch NvidiaPlanHostStepSession x0 r0 i0 . (lambda unrestricted current : Nat . (i0 x0)))
(branch NvidiaPlanHostStepAwait x0 x1 x2 x3 r0 i0 . (lambda unrestricted current : Nat . (prKeepStep (naturalEqual current target) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepAwait x0 x1 x2 x3 (i0 current)) (i0 current))))
)
0)))
-- 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 NvidiaPlanHostStepBoundary phase name 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)
(branch NvidiaPlanHostStepSession session tail induction . induction)
(branch NvidiaPlanHostStepAwait gpPut stride piece pieceStride 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 NvidiaPlanHostStepBoundary phase name 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)
(branch NvidiaPlanHostStepSession session tail induction . induction)
(branch NvidiaPlanHostStepAwait gpPut stride piece pieceStride 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 NvidiaPlanHostStepBoundary phase name 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)
(branch NvidiaPlanHostStepSession session tail induction . induction)
(branch NvidiaPlanHostStepAwait gpPut stride piece pieceStride 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)))))
-- The steps as the iteration `start` of an enclosing repeat runs them
-- (nvidiaPlanHostStepsExpand: iteration 0).
def nvidiaPlanHostStepsExpandAt =
(lambda unrestricted preservePredicate : Nat .
(lambda unrestricted start : 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 NvidiaPlanHostStepBoundary phase name tail induction .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepBoundary phase name (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)))))
(branch NvidiaPlanHostStepSession session tail induction .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepSession session (induction iteration rest)))))
(branch NvidiaPlanHostStepAwait gpPut stride piece pieceStride tail induction .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepAwait (prAt gpPut stride iteration) 0 (prAt piece pieceStride iteration) 0
(induction iteration rest))))))
start) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))
-- The steps with each repeat's first and last iterations only: every bound
-- a step's affine operands must keep (a ring entry, a piece, a cyclic
-- index) is kept by all the iterations between when by those two, the
-- operands monotone in the iteration -- so a long run's bounds are checked
-- without its every iteration.
def nvidiaPlanHostStepsExtremesAt =
(lambda unrestricted preservePredicate : Nat .
(lambda unrestricted start : 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) .
(nat-eliminate (lambda unrestricted n : Nat . (family NvidiaPlanHostSteps))
(tailInduction iteration rest)
(lambda unrestricted p : Nat . (lambda unrestricted ignored : (family NvidiaPlanHostSteps) .
(bodyInduction 0
(nat-eliminate (lambda unrestricted n : Nat . (family NvidiaPlanHostSteps))
(tailInduction iteration rest)
(lambda unrestricted q : Nat . (lambda unrestricted ignored2 : (family NvidiaPlanHostSteps) .
(bodyInduction (naturalPredecessor count) (tailInduction iteration rest))))
(naturalLess 1 count)))))
(naturalNonzero count)))))
(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 NvidiaPlanHostStepBoundary phase name tail induction .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepBoundary phase name (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)))))
(branch NvidiaPlanHostStepSession session tail induction .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepSession session (induction iteration rest)))))
(branch NvidiaPlanHostStepAwait gpPut stride piece pieceStride tail induction .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepAwait (prAt gpPut stride iteration) 0 (prAt piece pieceStride iteration) 0
(induction iteration rest))))))
start) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))
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 NvidiaPlanHostStepBoundary phase name tail induction .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepBoundary phase name (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)))))
(branch NvidiaPlanHostStepSession session tail induction .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepSession session (induction iteration rest)))))
(branch NvidiaPlanHostStepAwait gpPut stride piece pieceStride tail induction .
(lambda unrestricted iteration : Nat . (lambda unrestricted rest : (family NvidiaPlanHostSteps) .
(constructor NvidiaPlanHostSteps NvidiaPlanHostStepAwait (prAt gpPut stride iteration) 0 (prAt piece pieceStride iteration) 0
(induction iteration rest))))))
0) (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd))))
def nvidiaPlanHostStepsUnrolled = (nvidiaPlanHostStepsExpand 1)
def nvidiaPlanHostStepsExtremes = (nvidiaPlanHostStepsExtremesAt 0 0)
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 NvidiaPlanHostStepBoundary phase name 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)
(branch NvidiaPlanHostStepSession session tail induction . induction)
(branch NvidiaPlanHostStepAwait gpPut stride piece pieceStride tail induction . (prEvent (constructor ArenaEvent ArenaAwait gpPut) 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)))))
-- The schedule certificate without the iterations of its repeats: each
-- step's events run as nvidiaPlanHostScheduleCertified runs them, each
-- repeat's by Runtime.ArenaCertificate's arenaScheduleRepeat (two
-- iterations, the third checked a shift of the second, the rest a jump), so
-- a run of thousands of steps is certified at the cost of a few. The same
-- verdict as the unrolled walk on a schedule whose repeats advance their
-- generations evenly; one whose repeat does not is refused.
def nvidiaPlanHostScheduleState =
(lambda unrestricted steps : (family NvidiaPlanHostSteps) .
(lambda unrestricted start : (family ArenaScheduleState) .
(app
(eliminate NvidiaPlanHostSteps
(lambda unrestricted c : (family NvidiaPlanHostSteps) . (pi unrestricted state : (family ArenaScheduleState) . (family ArenaScheduleState)))
steps
(branch NvidiaPlanHostStepsEnd . (lambda unrestricted state : (family ArenaScheduleState) . state))
(branch NvidiaPlanHostStepSubmit x0 x1 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSubmit x0 x1 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepRepeat x0 r0 r1 i0 i1 . (lambda unrestricted state : (family ArenaScheduleState) . (i1 (arenaScheduleRepeat x0
(lambda unrestricted k : Nat . (nvidiaPlanHostStepEvents (nvidiaPlanHostStepsExpandAt 0 k r0))) state))))
(branch NvidiaPlanHostStepRepeatUntil x0 x1 x2 r0 r1 i0 i1 . (lambda unrestricted state : (family ArenaScheduleState) . (i1 (arenaScheduleRepeat x0
(lambda unrestricted k : Nat . (nvidiaPlanHostStepEvents (nvidiaPlanHostStepsExpandAt 0 k r0))) state))))
(branch NvidiaPlanHostStepRead x0 x1 x2 x3 x4 x5 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRead x0 x1 x2 x3 x4 x5 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepReadCyclic x0 x1 x2 x3 x4 x5 x6 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReadCyclic x0 x1 x2 x3 x4 x5 x6 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepWrite x0 x1 x2 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWrite x0 x1 x2 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepWriteAt x0 x1 x2 x3 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteAt x0 x1 x2 x3 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepWriteStat x0 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteStat x0 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepWriteStatus x0 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteStatus x0 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepWriteTimestamps x0 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteTimestamps x0 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepRecordStat x0 x1 x2 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRecordStat x0 x1 x2 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepStamp x0 x1 x2 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepStamp x0 x1 x2 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepFill x0 x1 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepFill x0 x1 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepAssertWord x0 x1 x2 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepAssertWord x0 x1 x2 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepBindInputIdentity x0 x1 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBindInputIdentity x0 x1 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepWriteInputIdentity r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteInputIdentity (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepBeginCheckpoint r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBeginCheckpoint (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepOperation r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepOperation (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepSync x0 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSync x0 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepDataSync x0 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepDataSync x0 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepClose x0 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepClose x0 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepReissue x0 x1 x2 x3 x4 x5 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReissue x0 x1 x2 x3 x4 x5 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepReissueAhead x0 x1 x2 x3 x4 x5 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReissueAhead x0 x1 x2 x3 x4 x5 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepBoundary x0 x1 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBoundary x0 x1 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepCommands x0 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCommands x0 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepCursorFromCheckpoint x0 x1 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCursorFromCheckpoint x0 x1 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepReadAtCursor x0 x1 x2 x3 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReadAtCursor x0 x1 x2 x3 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepCursorAdvance x0 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCursorAdvance x0 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepCheckpointBegin r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointBegin (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepCheckpointPublish x0 x1 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointPublish x0 x1 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepCheckpointPublishRestated x0 x1 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointPublishRestated x0 x1 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepSession x0 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSession x0 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)))))))
(branch NvidiaPlanHostStepAwait x0 x1 x2 x3 r0 i0 . (lambda unrestricted state : (family ArenaScheduleState) . (i0 (arenaScheduleRun state (nvidiaPlanHostStepEvents (constructor NvidiaPlanHostSteps NvidiaPlanHostStepAwait x0 x1 x2 x3 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd))))))))
start)))
def nvidiaPlanHostScheduleCertifiedFolded =
(lambda unrestricted submissionCount : Nat .
(lambda unrestricted steps : (family NvidiaPlanHostSteps) .
(naturalIsZero (arenaScheduleEnd submissionCount (nvidiaPlanHostScheduleState steps arenaScheduleStart)))))
-- 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 NvidiaPlanHostStepBoundary phase name 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)
(branch NvidiaPlanHostStepSession session tail induction . induction)
(branch NvidiaPlanHostStepAwait gpPut stride piece pieceStride 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 NvidiaPlanHostStepBoundary phase name 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)
(branch NvidiaPlanHostStepSession session tail induction . induction)
(branch NvidiaPlanHostStepAwait gpPut stride piece pieceStride tail induction . induction))))
-- A request host is a pairing's executable: its layout names the card the
-- pairing was built for, and PlanHost refuses any other card by name
-- (`card-name`) before allocating anything. An unnamed layout would skip
-- that comparison, so the request host refuses it by name (`card-unnamed`)
-- before opening any card: no pairing runs silently on a GPU it did not
-- name. Admission certifies layouts with a placeholder name (the card is
-- the pairing's choice), so the check belongs here, where a host is
-- emitted; a named layout's commands are unchanged. Qualification probes
-- built on PlanHost alone (Checked.*Artifact) stay card-agnostic within
-- their architecture by design: their silicon records span several sm_86
-- cards, and they are not request hosts.
def prRequireNamedCard =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NativePhysicalCommands)) layout
(branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
(phWhen (naturalIsZero (bytes-length expectedName))
(lambda unrestricted after : (family NativePhysicalCommands) .
(nativeLaunchRecipeAssertEqual (phImm 0) (phImm 1) b"card-unnamed" after))
tail)))))
def prPreludeNamed =
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(prRequireNamedCard layout
(phPreludeOn device (constructor NvidiaPlanHostMode NvidiaPlanHostStrict) layout tail)))))
-- ---- 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.
-- Command fragments and lifecycle effects share one ordering definition.
-- `completed` runs only after the done boundary; an observed instance places
-- terminal publication there before caller cleanup can close its descriptors.
def nvidiaPlanHostRequestWithOn =
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(lambda unrestricted A : Type 0 .
(lambda unrestricted emit : (pi unrestricted fragment : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (pi unrestricted rest : A . A)) .
(lambda unrestricted recorderOpen : (pi unrestricted after : A . A) .
(lambda unrestricted boundary : (pi unrestricted phase : Nat . (pi unrestricted name : Bytes . (pi unrestricted after : A . A))) .
(lambda unrestricted completed : A .
(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) .
(emit prTimerSlack
(emit prFenceRegister
(emit phPipeCreate
(recorderOpen (boundary prTelemetryBegin b"request-host:begin"
(emit (prEnvelope hostIdentity programIdentity qmdIdentity pushIdentity gpfifoIdentity programLength qmdLength pushLength gpfifoLength)
(emit (prRequestOpen input contract)
(boundary prTelemetryChecked b"request-host:request-checked"
(emit (prPreludeNamed device layout)
(boundary prTelemetryChannel b"request-host:channel-ready"
(emit (nativeLaunchRecipeStagingCommands nvidiaPlanHostStaging nvidiaPlanHostStagingExtent prSlotStatus phIdentity)
(emit (prRecipeFills fills)
(boundary prTelemetryUploaded b"request-host:uploaded"
(emit learner
(boundary prTelemetryLearner b"request-host:learner-scalars"
(nvidiaPlanHostStepsWith A emit boundary layout submissionCount contract steps
(boundary prTelemetryDone b"request-host:done"
completed)))))))))))))))))))))))))))))))))))))))
def nvidiaPlanHostRequestWith = (nvidiaPlanHostRequestWithOn nvidiaDeviceZero)
def nvidiaPlanHostRequestCommandsOn =
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(nvidiaPlanHostRequestWithOn device (family NativePhysicalCommands)
(lambda unrestricted fragment : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . fragment)
phTelemetryOpen phTelemetry
(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 NvidiaPlanHostStepBoundary phase name tail induction . induction)
(branch NvidiaPlanHostStepCommands commands tail induction . induction)
(branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction)
(branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . (naturalAnd (nvidiaPlanHostContains layout host extent) induction))
(branch NvidiaPlanHostStepCursorAdvance bytes tail induction . induction)
(branch NvidiaPlanHostStepCheckpointBegin tail induction . induction)
(branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction) (branch NvidiaPlanHostStepCheckpointPublishRestated restated perInvocation tail induction . induction) (branch NvidiaPlanHostStepSession session tail induction . induction)
(branch NvidiaPlanHostStepAwait gpPut stride piece pieceStride tail induction . (naturalAnd (naturalLess piece (prRingEntries layout)) 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 (nvidiaPlanHostStepsExtremes steps)))
(naturalAnd (naturalLessOrEqual submissionCount
(naturalDivideUnchecked nvidiaPlanHostStagingExtent nvidiaPlanHostTimestampRecord))
(nvidiaPlanHostScheduleCertifiedFolded submissionCount steps))))))))))
-- ---- a request host of several cards ----
-- One process driving `sessions` cards (PlanHost's sessions, the peers'
-- windows of PlanHostPeers; docs/PRD-8XH100-ON-A-BUDGET.md F4): the
-- envelope and the request as one card's host checks them, then each
-- session's prelude in turn (session 0's creating the RM client the others
-- join), every pair of cards joined and every card's window of every card's
-- buffer `peerIndex` mapped, each session's recipes expanded into its own
-- mapped tables, the learner's commands, then the schedule: its steps run
-- on session 0 until a NvidiaPlanHostStepSession names another.
-- `devices s` and `layouts s` are session s's card and layout; `fills s`
-- its recipe tables. Every layout uses the same ABI (session 0's).
def prLayoutABI =
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family NvidiaPlanHostABI)) layout
(branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost . abi)))
-- the commands of sessions 0 .. count - 1, each by `each`, in order
def prEachSession =
(lambda unrestricted count : Nat .
(lambda unrestricted each : (pi unrestricted session : Nat . (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands))) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(app
(nat-eliminate (lambda unrestricted n : Nat . (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)))
(lambda unrestricted after : (family NativePhysicalCommands) . after)
(lambda unrestricted session : Nat .
(lambda unrestricted earlier : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
(lambda unrestricted after : (family NativePhysicalCommands) . (earlier (each session after)))))
count)
tail))))
def prSessionPrelude =
(lambda unrestricted session : Nat .
(lambda unrestricted device : (family NvidiaDeviceBinding) .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted tail : (family NativePhysicalCommands) .
(prRequireNamedCard layout
(phPreludeOnS session device (constructor NvidiaPlanHostMode NvidiaPlanHostStrict) layout tail))))))
def nvidiaPlanHostRequestSessionsCommands =
(lambda unrestricted sessions : Nat .
(lambda unrestricted devices : (pi unrestricted session : Nat . (family NvidiaDeviceBinding)) .
(lambda unrestricted layouts : (pi unrestricted session : Nat . (family NvidiaPlanHostLayout)) .
(lambda unrestricted peerIndex : Nat .
(lambda unrestricted peerExtent : Nat .
(lambda unrestricted window : (pi unrestricted peer : Nat . Nat) .
(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 : (pi unrestricted session : Nat . (family NvidiaPlanHostRecipeFills)) .
(lambda unrestricted learner : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) .
(lambda unrestricted steps : (family NvidiaPlanHostSteps) .
(let unrestricted A = (family NativePhysicalCommands) in
(let unrestricted emit = (lambda unrestricted fragment : (pi unrestricted after : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . fragment) in
(prTimerSlack
(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"
(prEachSession sessions
(lambda unrestricted session : Nat . (prSessionPrelude session (devices session) (layouts session)))
(phTelemetry prTelemetryChannel b"request-host:channel-ready"
(ppPeers (prLayoutABI (layouts 0)) (lambda unrestricted session : Nat . (nvidiaDeviceBindingMinor (devices session))) sessions peerIndex peerExtent window
(nativeLaunchRecipeStagingCommands nvidiaPlanHostStaging nvidiaPlanHostStagingExtent prSlotStatus phIdentity
(prEachSession sessions (lambda unrestricted session : Nat . (prRecipeFills (fills session)))
(phTelemetry prTelemetryUploaded b"request-host:uploaded"
(learner
(phTelemetry prTelemetryLearner b"request-host:learner-scalars"
(nvidiaPlanHostSessionStepsWith A emit phTelemetry layouts submissionCount contract steps
(phTelemetry prTelemetryDone b"request-host:done"
(phCall phSysExitGroup (phArgs3 (phImm 0) (phImm 0) (phImm 0)) b"" phDiscard
(phNext (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
(constructor NativePhysicalCommands NativePhysicalCommandsEnd))))))))))))))))))))))))))))))))))))))))))))
-- ---- admission of several cards ----
-- the host mappings of every session at once (each session's buffers, its
-- doorbell and error page), the shared parameter page and recipe staging:
-- disjoint, so no session's mapping lands on another's
def prSessionHostResidents =
(lambda unrestricted session : Nat .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted rest : (family ArenaResidents) .
(phEachResident phHostResident (phAllocatedBuffers layout)
(phResident b"doorbell" (phDoorHostS session) 0x10000
(eliminate NvidiaPlanHostLayout (lambda unrestricted current : (family NvidiaPlanHostLayout) . (family ArenaResidents)) layout
(branch NvidiaPlanHostLayoutValue gpfifo push sem program qmd userd data abi lifecycle expectedName errorHost .
(nat-eliminate (lambda unrestricted current : Nat . (family ArenaResidents)) rest
(lambda unrestricted p : Nat . (lambda unrestricted ignored : (family ArenaResidents) .
(phResident b"error-notifier" errorHost nvidiaPlanHostErrorPageBytes rest)))
(naturalNonzero errorHost)))))))))
def prSessionsHostApart =
(lambda unrestricted sessions : Nat .
(lambda unrestricted layouts : (pi unrestricted session : Nat . (family NvidiaPlanHostLayout)) .
(arenaCertificate phHostSpaceBytes
(nat-eliminate (lambda unrestricted n : Nat . (family ArenaResidents))
(phResident b"parameters" phParams nvidiaPlanHostParameterMappingBytes
(phResident b"recipe-staging" nvidiaPlanHostStaging nvidiaPlanHostStagingExtent
(constructor ArenaResidents ArenaResidentsEnd)))
(lambda unrestricted session : Nat . (lambda unrestricted earlier : (family ArenaResidents) .
(prSessionHostResidents session (layouts session) earlier)))
sessions))))
-- every card's address space: its own buffers and the `sessions` windows,
-- disjoint
def prSessionWindowsApart =
(lambda unrestricted sessions : Nat .
(lambda unrestricted layout : (family NvidiaPlanHostLayout) .
(lambda unrestricted peerExtent : Nat .
(lambda unrestricted window : (pi unrestricted peer : Nat . Nat) .
(arenaCertificate phGPUSpaceBytes
(phEachResident phGPUResident (phAllocatedBuffers layout)
(nat-eliminate (lambda unrestricted n : Nat . (family ArenaResidents)) (constructor ArenaResidents ArenaResidentsEnd)
(lambda unrestricted peer : Nat . (lambda unrestricted earlier : (family ArenaResidents) .
(phResident b"peer-window" (window peer) peerExtent earlier)))
sessions)))))))
-- Each session admitted as a one-card request host is, on its own
-- projection of the schedule (nvidiaPlanHostStepsOfSession), with its own
-- doorbell; the sessions' host mappings and every card's windows apart; the
-- schedule's repeats balanced; and every session's projection submitting
-- exactly the plan's submissions.
def nvidiaPlanHostRequestSessionsAdmitted =
(lambda unrestricted sessions : Nat .
(lambda unrestricted layouts : (pi unrestricted session : Nat . (family NvidiaPlanHostLayout)) .
(lambda unrestricted peerExtent : Nat .
(lambda unrestricted window : (pi unrestricted peer : Nat . Nat) .
(lambda unrestricted submissionCount : Nat .
(lambda unrestricted fills : (pi unrestricted session : Nat . (family NvidiaPlanHostRecipeFills)) .
(lambda unrestricted steps : (family NvidiaPlanHostSteps) .
(naturalAnd (naturalLess 0 sessions)
(naturalAnd (naturalLessOrEqual sessions 16)
(naturalAnd (nvidiaPlanHostSessionsBalanced steps)
(naturalAnd (prSessionsHostApart sessions layouts)
(naturalAllBelow sessions (lambda unrestricted session : Nat .
(let unrestricted layout = (layouts session) in
(let unrestricted own = (nvidiaPlanHostStepsOfSession session steps) in
(naturalAnd (nvidiaPlanHostLayoutAdmitted layout)
(naturalAnd (nvidiaPlanHostLayoutCertifiedS session layout
(constructor ArenaResidents ArenaResidentsNext
(constructor ArenaResident ArenaResidentValue b"recipe-staging" nvidiaPlanHostStaging nvidiaPlanHostStagingExtent 0x1000)
(constructor ArenaResidents ArenaResidentsEnd)))
(naturalAnd (prSessionWindowsApart sessions layout peerExtent window)
(naturalAnd (prRecipesAdmitted layout (fills session))
(naturalAnd (naturalAnd (prStepsAdmitted layout submissionCount own)
(prStepsAdmitted layout submissionCount (nvidiaPlanHostStepsExtremes own)))
(naturalAnd (naturalLessOrEqual submissionCount
(naturalDivideUnchecked nvidiaPlanHostStagingExtent nvidiaPlanHostTimestampRecord))
(nvidiaPlanHostScheduleCertifiedFolded submissionCount own))))))))))))))))))))))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.