Coppelius.Build.NativeHost

1module Coppelius.Build.NativeHost
2
3import Coppelius.ArenaPlan
4import Coppelius.Build.DeviceImages
5import Coppelius.Build.PhysicalComponents
6import Coppelius.Build.Placement
7import Coppelius.Build.Graph
8import Coppelius.Learner
9import Coppelius.TrainingRun
10import Data.Bytes
11import Hardware.Nvidia.SM86.Command.WholeProgramPlan
12import Model.Config
13import Model.Parameter
14import Model.Word64
15import Model.Word32
16import Platform.Linux.Nvidia.Compatibility
17import Platform.Linux.Nvidia.PlanHost
18import Platform.Linux.Nvidia.PlanHostAdamW
19import Platform.Linux.Nvidia.PlanHostRequest
20import Runtime.NativePhysicalEmbeddedArtifact
21import Realization.Nvidia.SM86.AdamWHalfSM86
22import Runtime.NativePhysicalProgram
23import Std.List
24import Std.Natural
25
26-- what the realization reports: each launch's parameter block's address,
27-- the word at the AdamW step size's offset in it, and the GPFIFO table --
28-- each submission's ring entry, which the host writes into the ring
29-- itself when it issues the submission again
30-- (Coppelius.Build.DirectArtifact passes them)
31family CoppeliusRealizedTables : Type 0
32constructor CoppeliusRealizedTablesValue
33field unrestricted coppeliusRealizedParameterAddresses : Bytes
34field unrestricted coppeliusRealizedStepWords : Bytes
35field unrestricted coppeliusRealizedRingEntries : Bytes
36end-family
37
38-- The card a host drives: its plan-host ABI, and the memory its channel
39-- (GPFIFO and USERD) and its arena live in -- video memory on the RTX
40-- cards; on the DGX Spark's GB10, which has no frame buffer (a video
41-- allocation is refused with NV_ERR_NOT_SUPPORTED), system memory, paged
42-- for the arena (1.34 GB is no contiguous allocation).
43family CoppeliusHostTarget : Type 0
44constructor CoppeliusHostTargetValue
45field unrestricted coppeliusHostTargetABI : (family NvidiaPlanHostABI)
46field unrestricted coppeliusHostTargetChannelMemory : (family NvidiaPlanHostMemory)
47field unrestricted coppeliusHostTargetArenaMemory : (family NvidiaPlanHostMemory)
48end-family
49
50-- a run of checkpoint gathers issued by one repeat (coppeliusGathers):
51-- its first chunk and how many
52family CoppeliusGatherRun : Type 0
53constructor CoppeliusGatherRunValue
54field unrestricted coppeliusGatherRunFirst : Nat
55field unrestricted coppeliusGatherRunLength : Nat
56end-family
57
58-- Coppelius's host, derived from its plans by Platform.Linux.Nvidia.PlanHost:
59-- the UVM lifecycle over the arena plan's regions, the four launch-table
60-- recipes expanded at startup, and the request schedule below -- the
61-- checkpoint scattered into the video arena two submissions per staged
62-- chunk, the forward submission and its predictions, then the run policy
63-- (Coppelius.TrainingRun): every step's context read from the token
64-- stream, its AdamW scalars computed, the update issued; the checkpoint
65-- gathered back one submission per chunk and published after every
66-- interval; the result record.  Every number here is the arena plan's, the training run's
67-- or the submission plan's; the host addresses are this pairing's placement
68-- of its mappings in the process.
69
70-- ---- host placement (Coppelius.ArenaPlan and Coppelius.Build.Placement
71-- place the mappings) ----
72def coppeliusHostQMDOverflow : Nat = (naturalAdd coppeliusHostQMD coppeliusSM86CompatQMDPrimaryBytesNatural)
73def coppeliusQMDOverflowBytes : Nat =
74  (naturalSaturatingSubtract coppeliusSM86CompatQMDBytesNatural coppeliusSM86CompatQMDPrimaryBytesNatural)
75
76def coppeliusSystemBuffer =
77  (lambda unrestricted identity : Bytes .
78    (lambda unrestricted gpu : Nat .
79      (lambda unrestricted host : Nat .
80        (lambda unrestricted extent : Nat .
81          (constructor NvidiaPlanHostBuffer NvidiaPlanHostBufferValue identity gpu host extent
82            (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory))))))
83
84
85def coppeliusHostAmpere : (family CoppeliusHostTarget) =
86  (constructor CoppeliusHostTarget CoppeliusHostTargetValue nvidiaPlanHostAmpere580
87    (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory)
88    (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory))
89
90-- The GB10's arena is GPU-cached system memory (the
91-- allocation cudaMalloc makes there, L2-cacheable by the GPU; the paged
92-- system memory it had ran L2-resident copies 4.6 times slower); it is
93-- never host-mapped.
94def coppeliusHostGB10 : (family CoppeliusHostTarget) =
95  (constructor CoppeliusHostTarget CoppeliusHostTargetValue nvidiaPlanHostBlackwell580
96    (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory)
97    (constructor NvidiaPlanHostMemory NvidiaPlanHostGPUCachedSystemMemory))
98
99def coppeliusHostTargetABI =
100  (lambda unrestricted target : (family CoppeliusHostTarget) .
101    (eliminate CoppeliusHostTarget (lambda unrestricted current : (family CoppeliusHostTarget) . (family NvidiaPlanHostABI)) target
102      (branch CoppeliusHostTargetValue abi channel arena . abi)))
103
104def coppeliusHostTargetChannelMemory =
105  (lambda unrestricted target : (family CoppeliusHostTarget) .
106    (eliminate CoppeliusHostTarget (lambda unrestricted current : (family CoppeliusHostTarget) . (family NvidiaPlanHostMemory)) target
107      (branch CoppeliusHostTargetValue abi channel arena . channel)))
108
109def coppeliusHostTargetArenaMemory =
110  (lambda unrestricted target : (family CoppeliusHostTarget) .
111    (eliminate CoppeliusHostTarget (lambda unrestricted current : (family CoppeliusHostTarget) . (family NvidiaPlanHostMemory)) target
112      (branch CoppeliusHostTargetValue abi channel arena . arena)))
113
114def coppeliusVideoBuffer =
115  (lambda unrestricted memory : (family NvidiaPlanHostMemory) .
116  (lambda unrestricted identity : Bytes .
117    (lambda unrestricted gpu : Nat .
118      (lambda unrestricted host : Nat .
119        (lambda unrestricted extent : Nat .
120          (constructor NvidiaPlanHostBuffer NvidiaPlanHostBufferValue identity gpu host extent memory))))))
121
122-- The layout: the GPFIFO and its USERD page in one video buffer, the
123-- pushbuffer (its extent the expansion's, `pushExpanded`), semaphores,
124-- program and QMD tables in system memory at the plan's bases, the
125-- checkpoint staging buffer, the QMD overflow adjacent to the QMD, and the
126-- video arena itself inside the UVM external range (not host-mapped).  The
127-- pairing's card name is asserted.
128def coppeliusHostLayoutFor =
129  (lambda unrestricted target : (family CoppeliusHostTarget) .
130  (lambda unrestricted pushExpanded : Nat .
131  (lambda unrestricted expectedName : Bytes .
132    (constructor NvidiaPlanHostLayout NvidiaPlanHostLayoutValue
133      (coppeliusVideoBuffer (coppeliusHostTargetChannelMemory target) b"gpfifo+userd" coppeliusGPFIFOBase coppeliusHostGPFIFO coppeliusSM86CompatGPFIFOAndUSERDBytesNatural)
134      (coppeliusSystemBuffer b"pushbuffer" coppeliusPushbufferBase coppeliusHostPushbuffer (coppeliusPushbufferBytes pushExpanded))
135      (coppeliusSystemBuffer b"semaphores" coppeliusSemaphoreBase coppeliusHostSemaphores coppeliusSemaphoreBytes)
136      (coppeliusSystemBuffer b"program" coppeliusProgramBase coppeliusHostProgram coppeliusSM86CompatProgramBytesNatural)
137      (coppeliusSystemBuffer b"qmd" coppeliusQMDBase coppeliusHostQMD coppeliusSM86CompatQMDPrimaryBytesNatural)
138      (coppeliusSystemBuffer b"userd-alias" (naturalAdd coppeliusGPFIFOBase nvidiaPlanHostUVMGPFIFOBytes) (naturalAdd coppeliusHostGPFIFO nvidiaPlanHostUVMGPFIFOBytes) nvidiaPlanHostUSERDBytes)
139      (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersNext
140        (coppeliusSystemBuffer b"checkpoint-staging" coppeliusStagingBase coppeliusHostStaging coppeliusSM86CompatCheckpointStagingBytesNatural)
141        (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersNext
142          (coppeliusSystemBuffer b"qmd-overflow" (naturalAdd coppeliusQMDBase coppeliusSM86CompatQMDPrimaryBytesNatural) coppeliusHostQMDOverflow coppeliusQMDOverflowBytes)
143          (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersNext
144            (coppeliusVideoBuffer (coppeliusHostTargetArenaMemory target) b"video-arena" coppeliusSM86CompatVideoBaseNatural 0 coppeliusSM86CompatVideoBytesNatural)
145            (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersEnd))))
146      (coppeliusHostTargetABI target)
147      (constructor NvidiaPlanHostLifecycle NvidiaPlanHostUVM coppeliusSM86CompatVideoBaseNatural coppeliusSM86CompatVideoBytesNatural)
148      expectedName
149      coppeliusHostErrorNotifier))))
150
151-- the RTX pairings' layout (the arena certificate and the admissions below
152-- decide it; the GB10's differs only in memory kinds and ABI)
153def coppeliusHostLayout = (coppeliusHostLayoutFor coppeliusHostAmpere)
154
155-- the four recipes and the extents their expansions must have
156def coppeliusRecipeFills =
157  (lambda unrestricted qmdExpanded : Nat .
158    (lambda unrestricted pushExpanded : Nat .
159      (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsNext coppeliusHostProgram coppeliusSM86CompatProgramBytesNatural
160        (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedProgramTable)
161        (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsNext coppeliusHostQMD qmdExpanded
162          (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedQMDTable)
163          (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsNext coppeliusHostPushbuffer pushExpanded
164            (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedPushbuffer)
165            (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsNext coppeliusHostGPFIFO coppeliusGPFIFOTableBytes
166              (constructor NativePhysicalEmbeddedComponentKind NativePhysicalEmbeddedGPFIFO)
167              (constructor NvidiaPlanHostRecipeFills NvidiaPlanHostRecipeFillsEnd)))))))
168
169-- ---- the schedule ----
170-- The checkpoint moves through the staging buffer a chunk at a time: the
171-- full chunks, then the tail.
172def coppeliusChunkBytes : Nat = coppeliusSM86CompatCheckpointStagingBytesNatural
173def coppeliusFullChunks : Nat = (naturalDivideUnchecked coppeliusCheckpointPayloadBytesNatural coppeliusChunkBytes)
174def coppeliusTailBytes : Nat = (naturalModuloUnchecked coppeliusCheckpointPayloadBytesNatural coppeliusChunkBytes)
175def coppeliusTailOffset : Nat = (naturalMultiply coppeliusFullChunks coppeliusChunkBytes)
176
177-- The load: after the first two submissions the first chunk is staged, then
178-- every two submissions scatter the staged chunk and the next is staged
179-- (one repeat iteration per remaining full chunk), then two submissions and
180-- the tail, then one submission scatters it.  The forward submission
181-- follows the run's first context; its predictions and the forward part of
182-- the result record are written before the request's operation decides
183-- whether training continues.
184def coppeliusLoadIterations : Nat = (naturalSaturatingSubtract coppeliusFullChunks 1)
185def coppeliusLoadFirst : Nat = 3
186def coppeliusLoadEnd : Nat = (naturalAdd 2 (naturalMultiply 2 coppeliusLoadIterations))
187def coppeliusTailLoadFirst : Nat = (naturalAdd coppeliusLoadEnd 1)
188def coppeliusTailScatter : Nat = (naturalAdd coppeliusLoadEnd 3)
189def coppeliusForwardSubmission : Nat = (naturalAdd coppeliusLoadEnd 4)
190
191-- The plan's submissions by ordinal (Coppelius.Build.Graph.
192-- coppeliusSubmissionSchedule): initialize; two per checkpoint chunk; the
193-- forward; the update (one step: forward, backward, AdamW, the half copies,
194-- the step's loss copy); the final forward; a gather per chunk; the report
195-- put back.  The run issues the update, the final forward, the gathers and
196-- the report again from their ordinals.
197def coppeliusForwardPiece : Nat = (naturalSaturatingSubtract coppeliusForwardSubmission 1)
198def coppeliusUpdatePiece : Nat = (succ coppeliusForwardPiece)
199def coppeliusFinalPiece : Nat = (naturalAdd coppeliusUpdatePiece coppeliusUpdatePieces)
200def coppeliusGatherPiece = (lambda unrestricted chunk : Nat . (naturalAdd (succ coppeliusFinalPiece) chunk))
201def coppeliusRestorePiece : Nat = (coppeliusGatherPiece cgChunks)
202-- the host's chunks are the plan's, and the report put back is its last
203-- submission
204def coppeliusChunksAgree :
205  (equal Nat cgChunks (naturalAdd coppeliusFullChunks (naturalNonzero coppeliusTailBytes))) =
206  (refl Nat cgChunks)
207def coppeliusPiecesArePlans : (equal Nat (succ coppeliusRestorePiece) coppeliusSubmissionCount) =
208  (refl Nat coppeliusSubmissionCount)
209
210def coppeliusStagingAt = (lambda unrestricted offset : Nat . (naturalAdd coppeliusHostStaging offset))
211def coppeliusUSERDHost : Nat = (naturalAdd coppeliusHostGPFIFO nvidiaPlanHostUVMGPFIFOBytes)
212
213def coppeliusCheckpointIn : (family NvidiaPlanHostFile) = (constructor NvidiaPlanHostFile NvidiaPlanHostCheckpointIn)
214def coppeliusCheckpointOut : (family NvidiaPlanHostFile) = (constructor NvidiaPlanHostFile NvidiaPlanHostCheckpointOut)
215def coppeliusInput : (family NvidiaPlanHostFile) = (constructor NvidiaPlanHostFile NvidiaPlanHostInput)
216def coppeliusPredictions : (family NvidiaPlanHostFile) = (constructor NvidiaPlanHostFile NvidiaPlanHostPredictions)
217def coppeliusResult : (family NvidiaPlanHostFile) = (constructor NvidiaPlanHostFile NvidiaPlanHostResult)
218
219def coppeliusSubmit =
220  (lambda unrestricted gpPut : Nat .
221    (lambda unrestricted stride : Nat .
222      (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
223        (constructor NvidiaPlanHostSteps NvidiaPlanHostStepSubmit gpPut stride tail))))
224
225def coppeliusStamp =
226  (lambda unrestricted gpPut : Nat .
227    (lambda unrestricted stride : Nat .
228      (lambda unrestricted which : Nat .
229        (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
230          (constructor NvidiaPlanHostSteps NvidiaPlanHostStepStamp gpPut stride which tail)))))
231
232def coppeliusReadCheckpoint =
233  (lambda unrestricted extent : Nat .
234    (lambda unrestricted offset : Nat .
235      (lambda unrestricted stride : Nat .
236        (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
237          (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRead coppeliusCheckpointIn coppeliusHostStaging extent offset stride 1 tail)))))
238
239def coppeliusWriteCheckpoint =
240  (lambda unrestricted extent : Nat .
241    (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
242      (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWrite coppeliusCheckpointOut coppeliusHostStaging extent tail)))
243
244def coppeliusWriteResult =
245  (lambda unrestricted host : Nat .
246    (lambda unrestricted extent : Nat .
247      (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
248        (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWrite coppeliusResult host extent tail))))
249
250def coppeliusRecordWord =
251  (lambda unrestricted host : Nat .
252    (lambda unrestricted statOffset : Nat .
253      (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
254        (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRecordStat host statOffset 4 tail))))
255
256def coppeliusStepsEnd : (family NvidiaPlanHostSteps) = (constructor NvidiaPlanHostSteps NvidiaPlanHostStepsEnd)
257
258def coppeliusLoadBody : (family NvidiaPlanHostSteps) =
259  (coppeliusSubmit coppeliusLoadFirst 2
260    (coppeliusSubmit (naturalAdd coppeliusLoadFirst 1) 2
261      (coppeliusStamp (naturalAdd coppeliusLoadFirst 1) 2 32
262        (coppeliusReadCheckpoint coppeliusChunkBytes coppeliusChunkBytes coppeliusChunkBytes
263          (coppeliusStamp (naturalAdd coppeliusLoadFirst 1) 2 48
264            coppeliusStepsEnd)))))
265
266-- the context at the stream's cursor into the staging record: its inputs,
267-- and its targets (the same window one token on)
268def coppeliusReadContext =
269  (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
270    (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReadAtCursor coppeliusInput coppeliusHostStaging coppeliusContextStreamBytes 0
271      (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReadAtCursor coppeliusInput (coppeliusStagingAt coppeliusInputTargetsOffset)
272        coppeliusContextStreamBytes coppeliusTokenBytes tail)))
273
274def coppeliusReissue =
275  (lambda unrestricted entries : Bytes .
276    (lambda unrestricted gpPut : Nat .
277      (lambda unrestricted piece : Nat .
278        (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
279          (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReissue gpPut 0 piece 0 (nvidiaPlanHostTableWord entries piece) 0 tail)))))
280
281-- ---- the run ----
282-- After the forward submission the ring carries the run, period by period
283-- (coppeliusRunCheckpointInterval steps each): the update issued once per
284-- step, then the checkpoint gathered back; the last period issues the
285-- final forward before its gathers and the report put back after them.
286def coppeliusPeriodSubmissions : Nat = (naturalAdd coppeliusRunCheckpointInterval cgChunks)
287def coppeliusPeriodFirst =
288  (lambda unrestricted period : Nat .
289    (naturalAdd (succ coppeliusForwardSubmission) (naturalMultiply period coppeliusPeriodSubmissions)))
290def coppeliusLastPeriod : Nat = (naturalSaturatingSubtract coppeliusRunPublications 1)
291def coppeliusRunSubmissionCount : Nat =
292  (naturalAdd coppeliusForwardSubmission (naturalAdd (naturalMultiply coppeliusRunPublications coppeliusPeriodSubmissions) 2))
293
294-- One step: its context read and the cursor moved on; its AdamW scalars
295-- computed into the update's AdamW launches (`adamW`); the update issued;
296-- its per-row losses (the update's loss copy put them in the loss-record
297-- window) appended to the result.
298def coppeliusStepBody =
299  (lambda unrestricted entries : Bytes .
300    (lambda unrestricted adamW : (family NativePhysicalCommands) .
301      (lambda unrestricted first : Nat .
302        (coppeliusReadContext
303          (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCursorAdvance coppeliusContextStreamBytes
304            (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCommands adamW
305              (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReissue first 1 coppeliusUpdatePiece 0
306                (nvidiaPlanHostTableWord entries coppeliusUpdatePiece) 0
307                (coppeliusWriteResult (coppeliusStagingAt coppeliusResultLossRecordOffset) coppeliusResultWindowBytes
308                  coppeliusStepsEnd))))))))
309
310-- The checkpoint gathered back, from gpPut `first`: each chunk's gather
311-- issued and the staged chunk written to the temporary.  Gathers laid end
312-- to end at a common stride (equal pieces) are issued by one repeat, the
313-- piece and its ring entry advancing per iteration; a chunk whose piece
314-- differs (one that spans two planes takes a launch more) starts a run of
315-- its own.  The runs are read off the realized table (the stride is the
316-- second full chunk's step from the first), and nvidiaPlanHostReissuesAdmitted
317-- holds every entry issued to it.
318def coppeliusGatherEntry =
319  (lambda unrestricted entries : Bytes . (lambda unrestricted chunk : Nat .
320    (nvidiaPlanHostTableWord entries (coppeliusGatherPiece chunk))))
321
322def coppeliusGatherStride =
323  (lambda unrestricted entries : Bytes .
324    (naturalSaturatingSubtract (coppeliusGatherEntry entries 1) (coppeliusGatherEntry entries 0)))
325
326-- the full chunks, as runs in order (built last run first, from the last
327-- chunk back: a chunk joins the run after it when that run's first entry is
328-- one stride past its own)
329def coppeliusGatherRuns =
330  (lambda unrestricted entries : Bytes .
331    (let unrestricted stride = (coppeliusGatherStride entries) in
332    (nat-eliminate
333      (lambda unrestricted current : Nat . (family StdList (family CoppeliusGatherRun)))
334      (constructor StdList StdListEmpty (family CoppeliusGatherRun))
335      (lambda unrestricted p : Nat .
336        (lambda unrestricted later : (family StdList (family CoppeliusGatherRun)) .
337          (let unrestricted chunk = (naturalSaturatingSubtract (naturalSaturatingSubtract coppeliusFullChunks 1) p) in
338          (let unrestricted alone = (constructor StdList StdListCons (family CoppeliusGatherRun)
339                                      (constructor CoppeliusGatherRun CoppeliusGatherRunValue chunk 1) later) in
340          (eliminate StdList (lambda unrestricted current : (family StdList (family CoppeliusGatherRun)) . (family StdList (family CoppeliusGatherRun))) later
341            (branch StdListEmpty . alone)
342            (branch StdListCons run rest induction .
343              (eliminate CoppeliusGatherRun (lambda unrestricted current : (family CoppeliusGatherRun) . (family StdList (family CoppeliusGatherRun))) run
344                (branch CoppeliusGatherRunValue first length .
345                  (nat-eliminate (lambda unrestricted current : Nat . (family StdList (family CoppeliusGatherRun)))
346                    alone
347                    (lambda unrestricted q : Nat . (lambda unrestricted ignored : (family StdList (family CoppeliusGatherRun)) .
348                      (constructor StdList StdListCons (family CoppeliusGatherRun)
349                        (constructor CoppeliusGatherRun CoppeliusGatherRunValue chunk (succ length)) rest)))
350                    (naturalEqual (coppeliusGatherEntry entries first) (naturalAdd (coppeliusGatherEntry entries chunk) stride)))))))))))
351      coppeliusFullChunks)))
352
353def coppeliusGathers =
354  (lambda unrestricted entries : Bytes .
355    (lambda unrestricted first : Nat .
356      (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
357        (stdListFold (family CoppeliusGatherRun) (family NvidiaPlanHostSteps)
358          (lambda unrestricted run : (family CoppeliusGatherRun) .
359            (lambda unrestricted after : (family NvidiaPlanHostSteps) .
360              (eliminate CoppeliusGatherRun (lambda unrestricted current : (family CoppeliusGatherRun) . (family NvidiaPlanHostSteps)) run
361                (branch CoppeliusGatherRunValue chunk length .
362                  (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRepeat length
363                    (constructor NvidiaPlanHostSteps NvidiaPlanHostStepReissue (naturalAdd first chunk) 1 (coppeliusGatherPiece chunk) 1
364                      (coppeliusGatherEntry entries chunk) (coppeliusGatherStride entries)
365                      (coppeliusWriteCheckpoint coppeliusChunkBytes coppeliusStepsEnd))
366                    after)))))
367          (coppeliusReissue entries (naturalAdd first coppeliusFullChunks) (coppeliusGatherPiece coppeliusFullChunks)
368            (coppeliusWriteCheckpoint coppeliusTailBytes tail))
369          (coppeliusGatherRuns entries)))))
370
371-- `chosen` when the flag is nonzero, else `otherwise`
372def coppeliusStepsWhen =
373  (lambda unrestricted flag : Nat .
374    (lambda unrestricted chosen : (family NvidiaPlanHostSteps) .
375      (lambda unrestricted otherwise : (family NvidiaPlanHostSteps) .
376        (nat-eliminate (lambda unrestricted current : Nat . (family NvidiaPlanHostSteps)) otherwise
377          (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family NvidiaPlanHostSteps) . chosen))
378          flag))))
379
380-- Period p: its steps; in the last, the final forward; the checkpoint's
381-- temporary (the first period's the train operation made); the gathers;
382-- in the last, the report put back; the checkpoint published, counting the
383-- steps (and the contexts) taken so far.
384def coppeliusPeriod =
385  (lambda unrestricted entries : Bytes .
386    (lambda unrestricted adamW : (family NativePhysicalCommands) .
387      (lambda unrestricted period : Nat .
388        (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
389          (let unrestricted first = (coppeliusPeriodFirst period) in
390          (let unrestricted last = (naturalEqual period coppeliusLastPeriod) in
391          (let unrestricted gathered = (naturalAdd (naturalAdd first coppeliusRunCheckpointInterval) last) in
392          (let unrestricted taken = (naturalMultiply (succ period) coppeliusRunCheckpointInterval) in
393          (let unrestricted publish =
394            (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointPublish taken taken tail) in
395          (let unrestricted gathers =
396            (coppeliusGathers entries gathered
397              (coppeliusStepsWhen last
398                (coppeliusReissue entries (naturalAdd gathered cgChunks) coppeliusRestorePiece publish)
399                publish)) in
400          (let unrestricted begun =
401            (coppeliusStepsWhen period
402              (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCheckpointBegin gathers)
403              gathers) in
404          (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRepeat coppeliusRunCheckpointInterval
405            (coppeliusStepBody entries adamW first)
406            (coppeliusStepsWhen last
407              (coppeliusReissue entries (naturalAdd first coppeliusRunCheckpointInterval) coppeliusFinalPiece begun)
408              begun)))))))))))))
409
410def coppeliusRunPeriods =
411  (lambda unrestricted entries : Bytes .
412    (lambda unrestricted adamW : (family NativePhysicalCommands) .
413      (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
414        (app
415          (nat-eliminate
416            (lambda unrestricted current : Nat . (pi unrestricted after : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps)))
417            (lambda unrestricted after : (family NvidiaPlanHostSteps) . after)
418            (lambda unrestricted p : Nat .
419              (lambda unrestricted induction : (pi unrestricted after : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps)) .
420                (lambda unrestricted after : (family NvidiaPlanHostSteps) . (induction (coppeliusPeriod entries adamW p after)))))
421            coppeliusRunPublications)
422          tail))))
423
424-- The whole schedule.  The stream's cursor starts at the checkpoint's
425-- position; the run's first context is staged for the forward submission
426-- (read again for the first step: the cursor moves only there).
427def coppeliusHostStepsFor =
428  (lambda unrestricted entries : Bytes .
429    (lambda unrestricted adamW : (family NativePhysicalCommands) .
430  (constructor NvidiaPlanHostSteps NvidiaPlanHostStepCursorFromCheckpoint coppeliusTokenStreamHeaderBytes coppeliusContextStreamBytes
431  (coppeliusSubmit 1 0
432    (coppeliusSubmit 2 0
433      (coppeliusReadCheckpoint coppeliusChunkBytes 0 0
434        (constructor NvidiaPlanHostSteps NvidiaPlanHostStepRepeat coppeliusLoadIterations coppeliusLoadBody
435          (coppeliusSubmit coppeliusTailLoadFirst 0
436            (coppeliusSubmit (naturalAdd coppeliusTailLoadFirst 1) 0
437              (coppeliusReadCheckpoint coppeliusTailBytes coppeliusTailOffset 0
438                (coppeliusSubmit coppeliusTailScatter 0
439                  (coppeliusReadContext
440                    (constructor NvidiaPlanHostSteps NvidiaPlanHostStepFill (coppeliusStagingAt coppeliusResultRecordOffset) coppeliusResultRecordMarker
441                      (coppeliusSubmit coppeliusForwardSubmission 0
442                        (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWrite coppeliusPredictions (coppeliusStagingAt coppeliusResultPredictionsOffset) coppeliusResultPredictionsBytes
443                          (coppeliusWriteResult (coppeliusStagingAt coppeliusResultRecordOffset) coppeliusResultRecordForwardBytes
444                            (constructor NvidiaPlanHostSteps NvidiaPlanHostStepOperation
445                              (coppeliusRunPeriods entries adamW
446                                (coppeliusRecordWord (naturalAdd coppeliusUSERDHost nvidiaPlanHostUSERDGPGetOffset) coppeliusResultStatGPGetOffset
447                                  (coppeliusRecordWord (naturalAdd coppeliusUSERDHost nvidiaPlanHostUSERDGPPutOffset) coppeliusResultStatGPPutOffset
448                                    (coppeliusRecordWord coppeliusHostSemaphores coppeliusResultStatSemaphoreOffset
449                                      (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteStat coppeliusResult
450                                        (coppeliusWriteResult (coppeliusStagingAt coppeliusResultLossBlockOffset) coppeliusResultLossBlockBytes
451                                          (coppeliusWriteResult (coppeliusStagingAt coppeliusResultRecordOffset) coppeliusResultRecordFinalBytes
452                                            (coppeliusWriteResult coppeliusHostSemaphores coppeliusSemaphoreBytes
453                                              (coppeliusWriteResult coppeliusHostErrorNotifier coppeliusResultErrorNotifierBytes
454                                                (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteStatus coppeliusResult
455                                                  (constructor NvidiaPlanHostSteps NvidiaPlanHostStepWriteTimestamps coppeliusResult
456                                                    coppeliusStepsEnd))))))))))))))))))))))))))))
457
458-- ---- AdamW's step-dependent scalars ----
459-- Coppelius's learner defines them exactly (Coppelius.Build.Graph: the
460-- binary32 nearest lr sqrt(1 - beta2^t) / (1 - beta1^t)); the host computes
461-- them in binary64 from the same ratios, continuing the step count from the
462-- checkpoint's header (scripts/ci/adamw-schedule.sh holds the two to each
463-- other): the constants and the powers first, then one update's scalars
464-- per step, written into the update's AdamW launches.
465def coppeliusHostAdamW : (family NvidiaPlanHostAdamW) =
466  (constructor NvidiaPlanHostAdamW NvidiaPlanHostAdamWValue
467    (constructor NvidiaPlanHostArithmetic NvidiaPlanHostBinary64)
468    (constructor NvidiaPlanHostConstant NvidiaPlanHostRatio coppeliusLearningRateNumerator coppeliusLearningRateDenominator)
469    (constructor NvidiaPlanHostConstant NvidiaPlanHostRatio coppeliusBeta1Numerator coppeliusBeta1Denominator)
470    (constructor NvidiaPlanHostConstant NvidiaPlanHostRatio coppeliusBeta2Numerator coppeliusBeta2Denominator)
471    (constructor NvidiaPlanHostConstant NvidiaPlanHostRatio (naturalMultiply coppeliusEpsilonNumerator coppeliusLossScale) coppeliusEpsilonDenominator))
472
473def coppeliusRealizedAddresses =
474  (lambda unrestricted realized : (family CoppeliusRealizedTables) .
475    (eliminate CoppeliusRealizedTables (lambda unrestricted current : (family CoppeliusRealizedTables) . Bytes) realized
476      (branch CoppeliusRealizedTablesValue addresses words entries . addresses)))
477
478def coppeliusRealizedEntries =
479  (lambda unrestricted realized : (family CoppeliusRealizedTables) .
480    (eliminate CoppeliusRealizedTables (lambda unrestricted current : (family CoppeliusRealizedTables) . Bytes) realized
481      (branch CoppeliusRealizedTablesValue addresses words entries . entries)))
482
483-- where the host writes: the step-size word of the parameter block (the
484-- epsilon beside it) of each of the update's AdamW launches
485def coppeliusAdamWWordOffset : Nat = adamWHalfSM86StepSizeOffset
486
487def coppeliusAdamWLaunches =
488  (lambda unrestricted k : Nat .
489    (stdListReverse Nat
490      (nat-eliminate
491        (lambda unrestricted current : Nat . (family StdList Nat))
492        (constructor StdList StdListEmpty Nat)
493        (lambda unrestricted piece : Nat .
494          (lambda unrestricted rest : (family StdList Nat) .
495            (constructor StdList StdListCons Nat (coppeliusAdamWLaunch k piece) rest)))
496        coppeliusAdamWPieces)))
497
498-- the word the plan bakes there: the first step's step size and epsilon
499-- (Coppelius.Build.Graph)
500def coppeliusAdamWBaked =
501  (lambda unrestricted k : Nat .
502    (let unrestricted step = (naturalAdd coppeliusFirstStep k) in
503    (naturalAdd (cgAdamStepSize step) (naturalMultiply 4294967296 (cgAdamEpsilon step)))))
504
505def coppeliusAdamWSites =
506  (lambda unrestricted pushExpanded : Nat .
507    (lambda unrestricted addresses : Bytes .
508      (nvidiaPlanHostAdamWHostSites (coppeliusHostLayout pushExpanded b"") addresses coppeliusAdamWWordOffset coppeliusUpdatePieces coppeliusAdamWLaunches)))
509
510-- the learner's prelude (the constants, the powers the checkpoint counts)
511-- and one step's commands
512def coppeliusHostLearner =
513  (lambda unrestricted pushExpanded : Nat .
514  (lambda unrestricted addresses : Bytes .
515    (nvidiaPlanHostAdamWCommands coppeliusHostAdamW 0 (coppeliusAdamWSites pushExpanded addresses))))
516
517def coppeliusHostStepAdamW =
518  (lambda unrestricted pushExpanded : Nat .
519  (lambda unrestricted addresses : Bytes .
520    (nvidiaPlanHostAdamWStepCommands coppeliusHostAdamW (coppeliusAdamWSites pushExpanded addresses 0))))
521
522def coppeliusHostStepsOf =
523  (lambda unrestricted pushExpanded : Nat .
524    (lambda unrestricted realized : (family CoppeliusRealizedTables) .
525      (coppeliusHostStepsFor (coppeliusRealizedEntries realized)
526        (coppeliusHostStepAdamW pushExpanded (coppeliusRealizedAddresses realized)))))
527
528-- ---- contracts the pairing decides ----
529-- the schedule issues the run's submissions, every step on a fresh
530-- context; it moves the whole checkpoint in -- in order, every chunk once --
531-- and out at every publication; every
532-- submission it issues again writes the ring entry the realization gave
533-- it; and the plan's device side is certified (Coppelius.Build.Graph.
534-- coppeliusDeviceHazard: every pointer in a named plane, no two live
535-- planes sharing a byte)
536def coppeliusHostIssuesRun =
537  (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
538    (naturalEqual (nvidiaPlanHostStepSubmissions steps) coppeliusRunSubmissionCount))
539def coppeliusHostMovesCheckpoint =
540  (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
541    (naturalAnd
542      (nvidiaPlanHostFileReadsTile coppeliusCheckpointIn coppeliusCheckpointPayloadBytesNatural steps)
543      (naturalEqual (nvidiaPlanHostStepBytesWritten coppeliusCheckpointOut steps)
544        (naturalMultiply coppeliusRunPublications coppeliusCheckpointPayloadBytesNatural))))
545
546-- every issue of the update trains on a context no earlier step read: the
547-- cursor moves on by one context exactly once before each (it starts at
548-- the checkpoint's position, the forward's context, which the first step
549-- trains on and moves past), and the run issues the update once per step
550def coppeliusHostStepsFresh =
551  (lambda unrestricted steps : (family NvidiaPlanHostSteps) .
552    (app (app (app
553      (eliminate NvidiaPlanHostSteps
554        (lambda unrestricted current : (family NvidiaPlanHostSteps) .
555          (pi unrestricted moved : Nat . (pi unrestricted issued : Nat . (pi unrestricted ok : Nat . Nat))))
556        (nvidiaPlanHostStepsUnrolled steps)
557        (branch NvidiaPlanHostStepsEnd .
558          (lambda unrestricted moved : Nat . (lambda unrestricted issued : Nat . (lambda unrestricted ok : Nat .
559            (naturalAnd ok (naturalAnd (naturalIsZero moved) (naturalEqual issued coppeliusRunSteps)))))))
560        (branch NvidiaPlanHostStepSubmit gpPut stride tail induction . induction)
561        (branch NvidiaPlanHostStepRepeat count body tail bodyInduction tailInduction . tailInduction)
562        (branch NvidiaPlanHostStepRead file host extent offset stride tolerateEmpty tail induction . induction)
563        (branch NvidiaPlanHostStepReadCyclic host extent offset recordBytes count index indexStride tail induction . induction)
564        (branch NvidiaPlanHostStepWrite file host extent tail induction . induction)
565        (branch NvidiaPlanHostStepWriteAt file host extent offset tail induction . induction)
566        (branch NvidiaPlanHostStepWriteStat file tail induction . induction)
567        (branch NvidiaPlanHostStepWriteStatus file tail induction . induction)
568        (branch NvidiaPlanHostStepWriteTimestamps file tail induction . induction)
569        (branch NvidiaPlanHostStepRecordStat host statOffset extent tail induction . induction)
570        (branch NvidiaPlanHostStepStamp gpPut stride which tail induction . induction)
571        (branch NvidiaPlanHostStepFill host payload tail induction . induction)
572        (branch NvidiaPlanHostStepAssertWord identity host expected tail induction . induction)
573        (branch NvidiaPlanHostStepBindInputIdentity offset extent tail induction . induction)
574        (branch NvidiaPlanHostStepWriteInputIdentity tail induction . induction)
575        (branch NvidiaPlanHostStepBeginCheckpoint tail induction . induction)
576        (branch NvidiaPlanHostStepOperation tail induction . induction)
577        (branch NvidiaPlanHostStepSync file tail induction . induction)
578        (branch NvidiaPlanHostStepDataSync file tail induction . induction)
579        (branch NvidiaPlanHostStepClose file tail induction . induction)
580        (branch NvidiaPlanHostStepReissue gpPut stride piece pieceStride entry entryStride tail induction .
581          (lambda unrestricted moved : Nat . (lambda unrestricted issued : Nat . (lambda unrestricted ok : Nat .
582            (let unrestricted update = (naturalEqual piece coppeliusUpdatePiece) in
583            (induction (naturalSelect update 0 moved) (naturalAdd issued update)
584              (naturalAnd ok (naturalSelect update moved 1))))))))
585        (branch NvidiaPlanHostStepCommands commands tail induction . induction)
586        (branch NvidiaPlanHostStepCursorFromCheckpoint base scale tail induction . induction)
587        (branch NvidiaPlanHostStepReadAtCursor file host extent delta tail induction . induction)
588        (branch NvidiaPlanHostStepCursorAdvance bytes tail induction .
589          (lambda unrestricted moved : Nat . (lambda unrestricted issued : Nat . (lambda unrestricted ok : Nat .
590            (induction 1 issued (naturalAnd ok (naturalAnd (naturalIsZero moved) (naturalEqual bytes coppeliusContextStreamBytes))))))))
591        (branch NvidiaPlanHostStepCheckpointBegin tail induction . induction)
592        (branch NvidiaPlanHostStepCheckpointPublish updates invocations tail induction . induction))
593      0) 0) 1))
594
595def coppeliusHostLearnerAdmitted =
596  (lambda unrestricted pushExpanded : Nat .
597  (lambda unrestricted realized : (family CoppeliusRealizedTables) .
598    (eliminate CoppeliusRealizedTables (lambda unrestricted current : (family CoppeliusRealizedTables) . Nat) realized
599      (branch CoppeliusRealizedTablesValue addresses words entries .
600        (naturalAnd
601          (naturalEqual adamWHalfSM86EpsilonOffset (naturalAdd coppeliusAdamWWordOffset 4))
602          (nvidiaPlanHostAdamWSitesAdmitted (coppeliusHostLayout pushExpanded b"") addresses words coppeliusAdamWWordOffset
603            coppeliusUpdatePieces coppeliusAdamWLaunches coppeliusAdamWBaked))))))
604
605def coppeliusHostCertified =
606  (lambda unrestricted qmdExpanded : Nat .
607    (lambda unrestricted pushExpanded : Nat .
608      (lambda unrestricted realized : (family CoppeliusRealizedTables) .
609        (let unrestricted steps = (coppeliusHostStepsOf pushExpanded realized) in
610        (naturalAnd (coppeliusHostIssuesRun steps)
611          (naturalAnd (coppeliusHostStepsFresh steps)
612          (naturalAnd (coppeliusHostMovesCheckpoint steps)
613            (naturalAnd (nvidiaPlanHostReissuesAdmitted (coppeliusRealizedEntries realized) steps)
614              (nvidiaPlanHostRequestAdmitted (coppeliusHostLayout pushExpanded b"") coppeliusRunSubmissionCount
615                (coppeliusRecipeFills qmdExpanded pushExpanded) steps)))))))))
616
617-- the host's side (its schedule, and the AdamW sites the realization
618-- placed), then (only when it holds) the device's: the plan's order, then
619-- (only when it holds) the run's -- a refusal stops at the first that fails
620def coppeliusHostAdmitted =
621  (lambda unrestricted qmdExpanded : Nat .
622    (lambda unrestricted pushExpanded : Nat .
623      (lambda unrestricted realized : (family CoppeliusRealizedTables) .
624        (nat-eliminate (lambda unrestricted host : Nat . Nat) 0
625          (lambda unrestricted p : Nat . (lambda unrestricted ignored : Nat .
626            (nat-eliminate (lambda unrestricted plan : Nat . Nat) 0
627              (lambda unrestricted q : Nat . (lambda unrestricted ignoredToo : Nat . (naturalIsZero (coppeliusRunDeviceHazardOf q))))
628              (naturalIsZero (coppeliusDeviceHazardOf p)))))
629          (naturalAnd coppeliusSchedulesAdmitted
630            (naturalAnd (coppeliusHostLearnerAdmitted pushExpanded realized) (coppeliusHostCertified qmdExpanded pushExpanded realized)))))))
631
632-- ---- the host ELF ----
633-- `productIdentity` is the pairing's padded card name: the host payload's
634-- identity in the envelope and the name the card must report.
635-- `hostWriter` makes the host program an executable for the pairing's host:
636-- Runtime.NativePhysicalNativeELF's direct writer for x86-64, Platform.
637-- AArch64.HostLowering's for the DGX Spark.
638def coppeliusNativeHostELF =
639  (lambda unrestricted hostWriter : (pi unrestricted program : (family NativePhysicalProgram) . Bytes) .
640  (lambda unrestricted hostTarget : (family CoppeliusHostTarget) .
641  (lambda unrestricted productIdentity : Bytes .
642    (lambda unrestricted programIdentity : Bytes .
643      (lambda unrestricted qmdIdentity : Bytes .
644        (lambda unrestricted pushIdentity : Bytes .
645          (lambda unrestricted gpfifoIdentity : Bytes .
646            (lambda unrestricted programLength : Nat .
647              (lambda unrestricted qmdLength : Nat .
648                (lambda unrestricted pushLength : Nat .
649                  (lambda unrestricted gpfifoLength : Nat .
650                    (lambda unrestricted qmdExpanded : Nat .
651                      (lambda unrestricted pushExpanded : Nat .
652                      (lambda unrestricted realized : (family CoppeliusRealizedTables) .
653                        (nat-eliminate
654                          (lambda unrestricted admitted : Nat . Bytes)
655                          b""
656                          (lambda unrestricted predecessor : Nat .
657                            (lambda unrestricted induction : Bytes .
658                              (hostWriter (nvidiaPlanHostProgram productIdentity
659                                (nvidiaPlanHostRequestCommands (coppeliusHostLayoutFor hostTarget pushExpanded productIdentity)
660                                  productIdentity programIdentity qmdIdentity pushIdentity gpfifoIdentity
661                                  programLength qmdLength pushLength gpfifoLength
662                                  coppeliusRunSubmissionCount (constructor NvidiaPlanHostInputContract NvidiaPlanHostInputStream) coppeliusCheckpointContract
663                                  (coppeliusRecipeFills qmdExpanded pushExpanded)
664                                  (coppeliusHostLearner pushExpanded (coppeliusRealizedAddresses realized))
665                                  (coppeliusHostStepsOf pushExpanded realized))))))
666                          (coppeliusHostAdmitted qmdExpanded pushExpanded realized))))))))))))))))
667
668-- ---- what the artifact demands of a card (Platform.Linux.Nvidia.Compatibility) ----
669-- the instruction set its QMDs are built for, its kernels' resources, the
670-- video memory it reserves, and its host's driver branch, compute class and
671-- unified memory; a pairing admits a card whose profile supplies them all.
672-- The host demands read only the layout's ABI and lifecycle, so the
673-- pushbuffer's extent (known only at build, from its expansion) is 0 here.
674def coppeliusCompatDemands =
675  (lambda unrestricted architecture : (family ModelWord32) .
676    (nvidiaPlanDemands (nvidiaInstructionSetOf (modelWord32ToNatural architecture)) coppeliusWholeProgramDeviceRegions coppeliusSM86CompatVideoBytesNatural
677      (nvidiaHostDemands (coppeliusHostLayout 0 b"") nvidiaNoDemands)))