module Bob.Build.NativeHost import Bob.ArenaPlan import Bob.Build.PhysicalComponents import Bob.Learner import Bob.Model import Checkpoint.Envelope import Bob.TrainingRun import Data.Bytes import Data.Float32Bits import Data.JSON import Data.JSONAccess import Data.UTF8 import Data.JSONRender import Model.Config import Model.Parameter import Model.Word64 import Model.Word32 import Observe.CapturePolicy import Observe.Interchange import Observe.Value import Observe.Metric import Runtime.NativeObservedProgram import Observe.Execution import Runtime.NativeTelemetry import Runtime.NativeTelemetryIdentity import Runtime.ArenaCertificate import Runtime.TelemetryValue import Runtime.TelemetryRecord import Runtime.TelemetryPolicy import Runtime.TelemetryDrain import Runtime.TelemetryCapture import Platform.Linux.Nvidia.Compatibility import Platform.Linux.Nvidia.PlanHost import Platform.Linux.Nvidia.PlanHostAdamW import Platform.Linux.Nvidia.PlanHostRequest import Platform.Linux.Nvidia.RequestCapture import Runtime.NativePhysicalEmbeddedArtifact import Realization.Nvidia.SM86.AdamWSM86 import Runtime.NativePhysicalProgram import Std.Float import Std.List import Std.Natural -- what the realization reports of the parameter blocks: each launch's -- block's address, and the word at the AdamW step size's offset in it -- (Bob.Build.DirectArtifact passes them) family BobRealizedTables : Type 0 constructor BobRealizedTablesValue field unrestricted bobRealizedParameterAddresses : Bytes field unrestricted bobRealizedStepWords : Bytes end-family -- Values are taken from the semantics that also construct the executable. -- These describe its available training policy, not completed updates, restored -- state, input contents or facts about the device on which it eventually runs. def bobNativeExecutionConfiguration : (family AosValue) = (constructor AosValue AosMap (constructor AosValue AosMembersNext b"model" (constructor AosValue AosMap (constructor AosValue AosMembersNext b"input" (constructor AosValue AosText (project BobModelSemantics bobModelInputIdentity bobModel)) (constructor AosValue AosMembersNext b"vocabulary" (constructor AosValue AosU64 bobVocabularySize) (constructor AosValue AosMembersNext b"context_length" (constructor AosValue AosU64 bobContextLength) (constructor AosValue AosMembersNext b"parameter_count" (constructor AosValue AosU64 bobParameterCount) (constructor AosValue AosMembersEnd)))))) (constructor AosValue AosMembersNext b"learning" (constructor AosValue AosMap (constructor AosValue AosMembersNext b"objective" (constructor AosValue AosText bobObjectiveIdentity) (constructor AosValue AosMembersNext b"learner" (constructor AosValue AosText bobLearnerIdentity) (constructor AosValue AosMembersNext b"learning_rate" (constructor AosValue AosF32 (dataBytesRenderHex (dataFloat32EncodeBE bobLearningRate))) (constructor AosValue AosMembersNext b"first_moment_decay" (constructor AosValue AosF32 (dataBytesRenderHex (dataFloat32EncodeBE bobBeta1))) (constructor AosValue AosMembersNext b"second_moment_decay" (constructor AosValue AosF32 (dataBytesRenderHex (dataFloat32EncodeBE bobBeta2))) (constructor AosValue AosMembersNext b"epsilon" (constructor AosValue AosF32 (dataBytesRenderHex (dataFloat32EncodeBE bobEpsilon))) (constructor AosValue AosMembersNext b"weight_decay" (constructor AosValue AosF32 (dataBytesRenderHex (dataFloat32EncodeBE bobWeightDecay))) (constructor AosValue AosMembersEnd))))))))) (constructor AosValue AosMembersNext b"run_policy" (constructor AosValue AosMap (constructor AosValue AosMembersNext b"updates_per_training_invocation" (constructor AosValue AosU64 bobUpdatesPerInvocation) (constructor AosValue AosMembersNext b"initialization" (constructor AosValue AosText (project BobTrainingRunSemantics bobRunDeterministicInitializationIdentity bobTrainingRunSemantics)) (constructor AosValue AosMembersNext b"input_record_bytes" (constructor AosValue AosU64 bobInputRecordBytes) (constructor AosValue AosMembersNext b"native_only_required" (constructor AosValue AosBool (project BobTrainingRunSemantics bobRunNativeOnlyRequired bobTrainingRunSemantics)) (constructor AosValue AosMembersNext b"allowed_host_fallbacks" (constructor AosValue AosU64 (project BobTrainingRunSemantics bobRunAllowedHostFallbacks bobTrainingRunSemantics)) (constructor AosValue AosMembersEnd))))))) (constructor AosValue AosMembersNext b"checkpoint" (constructor AosValue AosMap (constructor AosValue AosMembersNext b"schema" (constructor AosValue AosText (project BobCheckpointTransportSchema bobCheckpointSchemaIdentity bobCheckpointSchema)) (constructor AosValue AosMembersNext b"ordering" (constructor AosValue AosText (project BobCheckpointTransportSchema bobCheckpointOrderingIdentity bobCheckpointSchema)) (constructor AosValue AosMembersNext b"payload_bytes" (constructor AosValue AosU64 (checkpointEnvelopeContractPayload bobCheckpointContract)) (constructor AosValue AosMembersNext b"planes" (constructor AosValue AosU64 bobCheckpointPlaneCount) (constructor AosValue AosMembersNext b"bytes_per_scalar" (constructor AosValue AosU64 bobCheckpointBytesPerScalar) (constructor AosValue AosMembersEnd))))))) (constructor AosValue AosMembersEnd)))))) -- This is a source declaration of the workload, not a claim that a run -- trained successfully. The frame binds its fresh run identity at import. -- One explicitly selected row, not a full-objective estimate. All numeric -- payload values are copied from the existing retired readback. def bobNativeRowDeclaration = (lambda unrestricted stage : Bytes . (constructor TelemetryRecordDeclaration TelemetryRecordDeclarationValue b"alpha.learning.bob_row_loss@1" b"metric" (capturePolicyIdentifier nvidiaRequestCapturePolicy) b"direct" b"native row zero loss copied from retired readback; one row sample" (constructor TelemetryCaptureValue TelemetryMembersNext b"row_loss" (constructor TelemetryCaptureValue TelemetryFloat32 0) (constructor TelemetryCaptureValue TelemetryMembersNext b"completed_submissions" (constructor TelemetryCaptureValue TelemetryUnsigned 1) (constructor TelemetryCaptureValue TelemetryMembersNext b"row_index" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosU64 0)) (constructor TelemetryCaptureValue TelemetryMembersNext b"sample_count" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosU64 1)) (constructor TelemetryCaptureValue TelemetryMembersNext b"stage" (constructor TelemetryCaptureValue TelemetryConstant (constructor AosValue AosText stage)) (constructor TelemetryCaptureValue TelemetryMembersEnd)))))))) def bobNativeRowSchema = (telemetryRecordJSON (telemetryRecordSchemaJSON (bobNativeRowDeclaration b"") b"Native row-zero loss diagnostic" (constructor JSON JSONObject (aosField b"row_loss" (nvidiaRequestCaptureField b"f32") (aosField b"completed_submissions" (nvidiaRequestCaptureField b"u64") (aosField b"row_index" (nvidiaRequestCaptureField b"u64") (aosField b"sample_count" (nvidiaRequestCaptureField b"u64") (aosField b"stage" (nvidiaRequestCaptureField b"text") aosObjectEnd)))))))) def bobNativeRowMeaning = (telemetryRecordJSON (aosSampledRowMetric b"metric:alpha.learning.bob_row_loss@1:row_loss" b"alpha.learning.bob_row_loss@1" b"Native row-zero cross entropy" b"nat/target-token" b"row zero log(sum(exp(scores))) minus the target score; binary32 native result" b"unbound")) def bobNativeRowTag0 : Nat = (succ nvidiaRequestCaptureLastTag) def bobNativeRowTag1 : Nat = (succ bobNativeRowTag0) def bobNativeCaptureSites = (constructor TelemetryPolicySites TelemetryPolicySitesNext bobNativeRowTag0 (constructor CaptureSite CaptureSiteValue b"0000000000000000000000000000050b" b"bob:before-training" (constructor CaptureClass CaptureLifecycleClass) 1 2 1) (bobNativeRowDeclaration b"before-training") (constructor TelemetryPolicySites TelemetryPolicySitesNext bobNativeRowTag1 (constructor CaptureSite CaptureSiteValue b"0000000000000000000000000000050c" b"bob:after-training" (constructor CaptureClass CaptureLifecycleClass) 1 2 1) (bobNativeRowDeclaration b"after-training") nvidiaRequestCaptureSitesWithCheckpoint)) def bobNativeRequestCapturePlan : (family TelemetryRoutedPolicyPlan) = (compile-time (nvidiaRequestCapturePlanWithSites bobNativeCaptureSites (constructor StdList StdListCons Bytes bobNativeRowSchema (constructor StdList StdListCons Bytes bobNativeRowMeaning (constructor StdList StdListCons Bytes (telemetryRecordJSON (aosExecutionTemplate b"execution-template:Bob.TrainingRun@1" b"Bob" b"learning" b"alpha.systems")) (constructor StdList StdListCons Bytes (telemetryRecordJSON (aosExecutionConfiguration b"configuration:Bob.TrainingRun@1" bobNativeExecutionConfiguration)) (constructor StdList StdListEmpty Bytes))))))) -- Bob's host, derived from its plans by Platform.Linux.Nvidia.PlanHost: the -- UVM lifecycle with no video arena (every buffer is system memory), the -- four launch-table recipes expanded at startup, and the request schedule -- below -- the input record and the checkpoint staged, the forward -- launches (the initial loss and the three prompts' predictions) submitted -- one at a time, their results written, the request's operation, then the -- training steps and the predictions again, the results and the checkpoint -- written. Every number here is the physical components' or the training -- run's; the host addresses are this pairing's placement of its mappings -- in the process. -- ---- host placement (Bob.ArenaPlan places the mappings) ---- -- buffer extents: the tables' bytes rounded to the mapping unit; the -- semaphores to a page; the GPFIFO with its USERD page after it def bobGPFIFOBufferBytes : Nat = (naturalAdd nvidiaPlanHostUVMGPFIFOBytes nvidiaPlanHostPageBytes) def bobSemaphoreBytes : Nat = (nvidiaPlanHostRoundUp (naturalMultiply prSemaphoreStride bobSubmissionCount) nvidiaPlanHostPageBytes) def bobStagingBytes : Nat = (nvidiaPlanHostRoundUp bobArenaBytes nvidiaPlanHostMappingUnit) def bobSystemBuffer = (lambda unrestricted identity : Bytes . (lambda unrestricted gpu : Nat . (lambda unrestricted host : Nat . (lambda unrestricted extent : Nat . (constructor NvidiaPlanHostBuffer NvidiaPlanHostBufferValue identity gpu host extent (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory)))))) def bobVideoBuffer = (lambda unrestricted identity : Bytes . (lambda unrestricted gpu : Nat . (lambda unrestricted host : Nat . (lambda unrestricted extent : Nat . (constructor NvidiaPlanHostBuffer NvidiaPlanHostBufferValue identity gpu host extent (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory)))))) -- The layout: the GPFIFO and its USERD page in one video buffer, the -- pushbuffer, semaphores, program and QMD tables in system memory at the -- plan's bases, the staging buffer holding the arena. No external range -- (extent 0): nothing lives in video memory but the GPFIFO. def bobHostLayout = (lambda unrestricted expectedName : Bytes . (lambda unrestricted qmdLength : Nat . (lambda unrestricted pushLength : Nat . (constructor NvidiaPlanHostLayout NvidiaPlanHostLayoutValue (bobVideoBuffer b"gpfifo+userd" bobGPFIFOBase bobHostGPFIFO bobGPFIFOBufferBytes) (bobSystemBuffer b"pushbuffer" bobPushbufferBase bobHostPushbuffer (nvidiaPlanHostRoundUp pushLength nvidiaPlanHostMappingUnit)) (bobSystemBuffer b"semaphores" bobSemaphoreBase bobHostSemaphores bobSemaphoreBytes) (bobSystemBuffer b"program" bobProgramBase bobHostProgram (nvidiaPlanHostRoundUp bobProgramBytes nvidiaPlanHostMappingUnit)) (bobSystemBuffer b"qmd" bobQMDBase bobHostQMD (nvidiaPlanHostRoundUp qmdLength nvidiaPlanHostMappingUnit)) (bobSystemBuffer b"userd-alias" (naturalAdd bobGPFIFOBase nvidiaPlanHostUVMGPFIFOBytes) (naturalAdd bobHostGPFIFO nvidiaPlanHostUVMGPFIFOBytes) nvidiaPlanHostPageBytes) (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersNext (bobSystemBuffer b"arena" bobParametersAddress bobHostStaging bobStagingBytes) (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersEnd)) nvidiaPlanHostAmpere580 (constructor NvidiaPlanHostLifecycle NvidiaPlanHostUVM 0 0) expectedName 0)))) def bobRecipeFills = (lambda unrestricted qmdExpanded : Nat . (lambda unrestricted pushExpanded : Nat . (lambda unrestricted gpfifoExpanded : Nat . (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsNext bobHostProgram bobProgramBytes (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedProgramTable) (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsNext bobHostQMD qmdExpanded (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedQMDTable) (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsNext bobHostPushbuffer pushExpanded (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedPushbuffer) (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsNext bobHostGPFIFO gpfifoExpanded (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedGPFIFO) (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsEnd)))))))) -- ---- the schedule ---- def bobStagingAt = (lambda unrestricted address : Nat . (naturalAdd bobHostStaging (naturalSaturatingSubtract address bobParametersAddress))) def bobTrainingSubmissions : Nat = (naturalSaturatingSubtract bobSubmissionCount bobForwardLaunches) def bobInput : (family NvidiaPlanHostFile) = (constructor NvidiaPlanHostFile NvidiaPlanHostInput) def bobCheckpointIn : (family NvidiaPlanHostFile) = (constructor NvidiaPlanHostFile NvidiaPlanHostCheckpointIn) def bobCheckpointOut : (family NvidiaPlanHostFile) = (constructor NvidiaPlanHostFile NvidiaPlanHostCheckpointOut) def bobPredictions : (family NvidiaPlanHostFile) = (constructor NvidiaPlanHostFile NvidiaPlanHostPredictions) def bobResult : (family NvidiaPlanHostFile) = (constructor NvidiaPlanHostFile NvidiaPlanHostResult) def bobStepsEnd : (family NvidiaPlanHostSteps) = (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd) def bobWriteAt = (lambda unrestricted file : (family NvidiaPlanHostFile) . (lambda unrestricted address : Nat . (lambda unrestricted extent : Nat . (lambda unrestricted offset : Nat . (lambda unrestricted tail : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteAt file (bobStagingAt address) extent offset tail)))))) -- the results after the forward launches and after the training: the loss -- block of that phase, the logit rows, the predictions def bobWriteResults = (lambda unrestricted lossAddress : Nat . (lambda unrestricted lossOffset : Nat . (lambda unrestricted tail : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBoundary prTelemetryLearningValue (aosChoose Bytes (naturalEqual lossAddress bobInitialLossAddress) b"Bob:loss-before-training" b"Bob:loss-after-training") (bobWriteAt bobResult lossAddress bobLossBytes lossOffset (bobWriteAt bobResult bobLogitRowsAddress bobLogitRowsBytes bobResultLogitRowsOffset (bobWriteAt bobPredictions bobPredictionsAddress bobPredictionsBytes 0 tail))))))) def bobSubmitEachStep = (lambda unrestricted count : Nat . (lambda unrestricted firstGPPut : Nat . (lambda unrestricted tail : (family NvidiaPlanHostSteps) . (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRepeat count (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSubmit firstGPPut 1 bobStepsEnd) tail)))) def bobHostSteps : (family NvidiaPlanHostSteps) = (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRead bobInput (bobStagingAt bobInputAddress) bobInputRecordBytes 0 0 0 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRead bobCheckpointIn bobHostStaging bobCheckpointPayloadBytes 0 0 1 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepBoundary prTelemetryStateRestored b"request-host:checkpoint-restored" (bobSubmitEachStep bobForwardLaunches 1 (bobWriteResults bobInitialLossAddress bobResultInitialLossOffset (constructor NvidiaPlanHostSteps NvidiaPlanHostStepOperation (bobSubmitEachStep bobTrainingSubmissions (naturalAdd bobForwardLaunches 1) (bobWriteResults bobTrainingLossAddress bobResultTrainingLossOffset (bobWriteAt bobCheckpointOut bobParametersAddress bobCheckpointPayloadBytes 0 (constructor NvidiaPlanHostSteps NvidiaPlanHostStepClose bobCheckpointOut (constructor NvidiaPlanHostSteps NvidiaPlanHostStepDataSync bobPredictions (constructor NvidiaPlanHostSteps NvidiaPlanHostStepDataSync bobResult bobStepsEnd)))))))))))) -- ---- AdamW's step-dependent scalars ---- def bobRealizedAddresses = (lambda unrestricted realized : (family BobRealizedTables) . (eliminate BobRealizedTables (lambda unrestricted current : (family BobRealizedTables) . Bytes) realized (branch BobRealizedTablesValue addresses words . addresses))) -- Bob's learner computes them in binary32 (Bob.Learner.bobAdamStepScalars); -- the host continues the step count from the checkpoint's header. def bobHostAdamW : (family NvidiaPlanHostAdamW) = (constructor NvidiaPlanHostAdamW NvidiaPlanHostAdamWValue (constructor NvidiaPlanHostArithmetic NvidiaPlanHostBinary32) (constructor NvidiaPlanHostConstant NvidiaPlanHostBinary32Bits (nvidiaPlanHostBinary32Of bobLearningRate)) (constructor NvidiaPlanHostConstant NvidiaPlanHostBinary32Bits (nvidiaPlanHostBinary32Of bobBeta1)) (constructor NvidiaPlanHostConstant NvidiaPlanHostBinary32Bits (nvidiaPlanHostBinary32Of bobBeta2)) (constructor NvidiaPlanHostConstant NvidiaPlanHostBinary32Bits (nvidiaPlanHostBinary32Of bobEpsilon))) -- where the host writes: the step-size word of the parameter block (the -- epsilon beside it) of update k's AdamW launch def bobAdamWWordOffset : Nat = (adamWF32CorrectedStepSizeOffsetOf adamWF32ABI) def bobAdamWLaunches = (lambda unrestricted k : Nat . (constructor StdList StdListCons Nat (bobAdamWLaunch k) (constructor StdList StdListEmpty Nat))) -- the word the plan bakes there for update k: step k + 1's step size and -- epsilon (Bob.Learner.bobAdamStepScalars, its seventh and eighth scalars) def bobAdamWBaked = (lambda unrestricted k : Nat . (nvidiaPlanHostLittleNatural 8 (dataBytesDropValidated (naturalMultiply 4 6) (bobAdamStepScalars (succ k))))) def bobHostLearner = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted addresses : Bytes . (nvidiaPlanHostAdamWCommands bobHostAdamW bobUpdatesPerInvocation (nvidiaPlanHostAdamWHostSites layout addresses bobAdamWWordOffset bobUpdatesPerInvocation bobAdamWLaunches)))) def bobHostLearnerAdmitted = (lambda unrestricted layout : (family NvidiaPlanHostLayout) . (lambda unrestricted realized : (family BobRealizedTables) . (eliminate BobRealizedTables (lambda unrestricted current : (family BobRealizedTables) . Nat) realized (branch BobRealizedTablesValue addresses words . (naturalAnd (naturalEqual (adamWF32ScaledEpsilonOffsetOf adamWF32ABI) (naturalAdd bobAdamWWordOffset 4)) (nvidiaPlanHostAdamWSitesAdmitted layout addresses words bobAdamWWordOffset bobUpdatesPerInvocation bobAdamWLaunches bobAdamWBaked)))))) -- ---- contracts the pairing decides ---- def bobHostSubmitsPlan : Nat = (naturalEqual (nvidiaPlanHostStepSubmissions bobHostSteps) bobSubmissionCount) def bobHostMovesCheckpoint : Nat = (naturalAnd (nvidiaPlanHostFileReadsTile bobCheckpointIn bobCheckpointPayloadBytes bobHostSteps) (naturalEqual (nvidiaPlanHostStepBytesWritten bobCheckpointOut bobHostSteps) bobCheckpointPayloadBytes)) def bobHostCertified = (lambda unrestricted qmdLength : Nat . (lambda unrestricted pushLength : Nat . (lambda unrestricted gpfifoLength : Nat . (naturalAnd bobHostSubmitsPlan (naturalAnd bobHostMovesCheckpoint (nvidiaPlanHostRequestAdmitted (bobHostLayout b"" qmdLength pushLength) bobSubmissionCount (bobRecipeFills qmdLength pushLength gpfifoLength) bobHostSteps)))))) -- the host's side (its schedule, and the AdamW sites the realization -- placed), then (only when it holds) the device's -- (Bob.Build.PhysicalComponents.bobDeviceHazard) def bobHostAdmitted = (lambda unrestricted qmdLength : Nat . (lambda unrestricted pushLength : Nat . (lambda unrestricted gpfifoLength : Nat . (lambda unrestricted realized : (family BobRealizedTables) . (nat-eliminate (lambda unrestricted host : Nat . Nat) 0 (lambda unrestricted p : Nat . (lambda unrestricted ignored : Nat . (naturalIsZero (bobDeviceHazardOf p)))) (naturalAnd (bobHostLearnerAdmitted (bobHostLayout b"" qmdLength pushLength) realized) (bobHostCertified qmdLength pushLength gpfifoLength))))))) -- ---- the host ELF ---- -- `productIdentity` is the pairing's padded card name: the host payload's -- identity in the envelope and the name the card must report. -- `hostWriter` makes the host program an executable for the pairing's host: -- Runtime.NativePhysicalNativeELF's direct writer for x86-64, Platform. -- AArch64.HostLowering's for the DGX Spark. def bobNativeCaptureBoundary = (lambda unrestricted phase : Nat . (lambda unrestricted name : Bytes . (lambda unrestricted after : (family NativeObservedSteps) . (aosChoose (family NativeObservedSteps) (naturalAnd (naturalEqual phase prTelemetryLearningValue) (bytes-equal name b"Bob:loss-before-training")) (nvidiaRequestCaptureMappedF32 bobNativeRowTag0 (bobStagingAt bobInitialLossAddress) (phLoad prGPPut) after) (aosChoose (family NativeObservedSteps) (naturalAnd (naturalEqual phase prTelemetryLearningValue) (bytes-equal name b"Bob:loss-after-training")) (nvidiaRequestCaptureMappedF32 bobNativeRowTag1 (bobStagingAt bobTrainingLossAddress) (phLoad prGPPut) after) (nvidiaRequestCaptureBoundaryWithCheckpoint phase name after)))))) def bobNativeHostELFWithIdentitySource = (lambda unrestricted source : (family NativeTelemetryIdentitySource) . (lambda unrestricted hostWriter : (pi unrestricted program : (family NativePhysicalProgram) . Bytes) . (lambda unrestricted productIdentity : 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 qmdExpanded : Nat . (lambda unrestricted pushExpanded : Nat . (lambda unrestricted gpfifoExpanded : Nat . (lambda unrestricted realized : (family BobRealizedTables) . (nat-eliminate (lambda unrestricted admitted : Nat . Bytes) b"" (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Bytes . (hostWriter (nvidiaPlanHostManagedRequestProgramWithBoundary bobNativeCaptureBoundary source bobNativeRequestCapturePlan (bobHostLayout productIdentity qmdExpanded pushExpanded) productIdentity programIdentity qmdIdentity pushIdentity gpfifoIdentity programLength qmdLength pushLength gpfifoLength bobSubmissionCount (constructor NvidiaPlanHostInputContract NvidiaPlanHostInputExact bobInputRecordBytes) bobCheckpointContract (bobRecipeFills qmdExpanded pushExpanded gpfifoExpanded) (bobHostLearner (bobHostLayout productIdentity qmdExpanded pushExpanded) (bobRealizedAddresses realized)) bobHostSteps)))) (bobHostAdmitted qmdExpanded pushExpanded gpfifoExpanded realized))))))))))))))))) -- Existing pairings retain fresh identities unless the artifact explicitly -- declares an assigned input. No environment-dependent runtime fallback. def bobNativeHostELF = (bobNativeHostELFWithIdentitySource (constructor NativeTelemetryIdentitySource NativeTelemetryFreshIdentity)) -- ---- what the artifact demands of a card (Platform.Linux.Nvidia.Compatibility) ---- -- the instruction set its QMDs are built for, its kernels' resources, the -- video memory it reserves, and its host's driver branch, compute class and -- unified memory; a pairing admits a card whose profile supplies them all def bobCompatDemands = (lambda unrestricted architecture : (family ModelWord32) . (nvidiaPlanDemands (nvidiaInstructionSetOf (modelWord32ToNatural architecture)) bobRegions bobMinimumVideoBytes (nvidiaHostDemands (bobHostLayout b"" 0 0) nvidiaNoDemands)))