1module Realization.Nvidia.SM86.EmbeddingGatherF32SM86
2
3import Accelerator.SM86.Control
4import Accelerator.SM86.Immediate
5import Accelerator.SM86.Instruction
6import Accelerator.SM86.InstructionEncoding
7import Accelerator.SM86.Program
8import Accelerator.SM86.Types
9import Data.SHA256Digest
10import Std.Natural
11import Std.Byte
12
13family EmbeddingGatherF32FailureCode : Type 0
14constructor EmbeddingGatherF32TokenOutOfBounds
15constructor EmbeddingGatherF32ChannelOutOfBounds
16constructor EmbeddingGatherF32TokenCountZero
17constructor EmbeddingGatherF32InstructionCountMismatch
18constructor EmbeddingGatherF32EncodingFailed
19constructor EmbeddingGatherF32IdentityInvalid
20
21end-family
22
23family EmbeddingGatherF32OffsetResult : Type 0
24constructor EmbeddingGatherF32OffsetValid
25field unrestricted embeddingGatherF32OffsetBytes : Nat
26constructor EmbeddingGatherF32OffsetInvalid
27field unrestricted embeddingGatherF32OffsetFailure : (family EmbeddingGatherF32FailureCode)
28field unrestricted embeddingGatherF32RejectedToken : Nat
29field unrestricted embeddingGatherF32RejectedChannel : Nat
30
31end-family
32
33family EmbeddingGatherF32Telemetry : Type 0
34constructor EmbeddingGatherF32TelemetryValue
35field unrestricted embeddingGatherF32TelemetryExpectedInstructions : Nat
36field unrestricted embeddingGatherF32TelemetryActualInstructions : Nat
37field unrestricted embeddingGatherF32TelemetryRegisterCount : Nat
38field unrestricted embeddingGatherF32TelemetryTokenCount : Nat
39field unrestricted embeddingGatherF32TelemetryGridY : Nat
40field unrestricted embeddingGatherF32TelemetryBlockX : Nat
41field unrestricted embeddingGatherF32TelemetryWidth : Nat
42field unrestricted embeddingGatherF32TelemetryVocabulary : Nat
43field unrestricted embeddingGatherF32TelemetryScalarLoads : Nat
44field unrestricted embeddingGatherF32TelemetryScalarStores : Nat
45field unrestricted embeddingGatherF32TelemetryHostOperations : Nat
46field unrestricted embeddingGatherF32TelemetryEncodedBytes : Nat
47field unrestricted embeddingGatherF32TelemetryEncodedFields : Nat
48field unrestricted embeddingGatherF32TelemetryEncodedBits : Nat
49constructor EmbeddingGatherF32TelemetryRejected
50field unrestricted embeddingGatherF32TelemetryFailure : (family EmbeddingGatherF32FailureCode)
51field unrestricted embeddingGatherF32TelemetryFailureOrdinal : Nat
52
53end-family
54
55family EmbeddingGatherF32Plan : Type 0
56constructor EmbeddingGatherF32PlanValue
57field unrestricted embeddingGatherF32PlanTokenCount : Nat
58field unrestricted embeddingGatherF32PlanProgram : (family SM86Program)
59field unrestricted embeddingGatherF32PlanTelemetry : (family EmbeddingGatherF32Telemetry)
60
61end-family
62
63family EmbeddingGatherF32PlanResult : Type 0
64constructor EmbeddingGatherF32PlanReady
65field unrestricted embeddingGatherF32ReadyPlan : (family EmbeddingGatherF32Plan)
66constructor EmbeddingGatherF32PlanFailed
67field unrestricted embeddingGatherF32PlanFailure : (family EmbeddingGatherF32FailureCode)
68field unrestricted embeddingGatherF32PlanFailureTelemetry : (family EmbeddingGatherF32Telemetry)
69
70end-family
71
72family EmbeddingGatherF32ImageResult : Type 0
73constructor EmbeddingGatherF32ImageReady
74field unrestricted embeddingGatherF32ImageBytes : Bytes
75field unrestricted embeddingGatherF32ImageSHA256 : Bytes
76field unrestricted embeddingGatherF32ImageTelemetry : (family EmbeddingGatherF32Telemetry)
77constructor EmbeddingGatherF32ImageFailed
78field unrestricted embeddingGatherF32ImageFailure : (family EmbeddingGatherF32FailureCode)
79field unrestricted embeddingGatherF32ImageFailureInstruction : Nat
80field unrestricted embeddingGatherF32ImageFailureCode : Bytes
81field unrestricted embeddingGatherF32ImageFailureTelemetry : (family EmbeddingGatherF32Telemetry)
82
83end-family
84
85-- Each thread moves four floats. A width choice determines both the row
86-- stride in the program and the number of threads in its launch.
87family EmbeddingGatherF32Width : Type 0
88constructor EmbeddingGatherF32Width1024
89constructor EmbeddingGatherF32Width576
90constructor EmbeddingGatherF32Width512
91constructor EmbeddingGatherF32Width256
92
93end-family
94
95def embeddingGatherF32NaturalFour =
96 (byte-to-nat (byte 4))
97
98def embeddingGatherF32NaturalTwenty =
99 (byte-to-nat (byte 20))
100
101def embeddingGatherF32NaturalTwentyFour =
102 (byte-to-nat (byte 24))
103
104def embeddingGatherF32NaturalOneThousandTwentyFour =
105 (naturalMultiply (byte-to-nat (byte 4)) byteNaturalTwoHundredFiftySix)
106
107def embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight =
108 (naturalMultiply (byte-to-nat (byte 48)) byteNaturalTwoHundredFiftySix)
109
110def embeddingGatherF32Register =
111 (lambda unrestricted value : Byte . (sm86Register value))
112
113def embeddingGatherF32Unsigned32 =
114 (lambda unrestricted byte0 : Byte .
115 (lambda unrestricted byte1 : Byte .
116 (lambda unrestricted byte2 : Byte .
117 (lambda unrestricted byte3 : Byte . (sm86Unsigned32 byte0 byte1 byte2 byte3)))))
118
119def embeddingGatherF32ZeroImmediate =
120 (embeddingGatherF32Unsigned32 (byte 0) (byte 0) (byte 0) (byte 0))
121
122def embeddingGatherF32FourImmediate =
123 (embeddingGatherF32Unsigned32 (byte 4) (byte 0) (byte 0) (byte 0))
124
125def embeddingGatherF32EightImmediate =
126 (embeddingGatherF32Unsigned32 (byte 8) (byte 0) (byte 0) (byte 0))
127
128def embeddingGatherF32TwelveImmediate =
129 (embeddingGatherF32Unsigned32 (byte 12) (byte 0) (byte 0) (byte 0))
130
131def embeddingGatherF32WidthElements =
132 (lambda unrestricted width : (family EmbeddingGatherF32Width) .
133 (eliminate
134 EmbeddingGatherF32Width
135 (lambda unrestricted current : (family EmbeddingGatherF32Width) . Nat)
136 width
137 (branch EmbeddingGatherF32Width1024 . embeddingGatherF32NaturalOneThousandTwentyFour)
138 (branch EmbeddingGatherF32Width576 .
139 (naturalAdd
140 (naturalMultiply (byte-to-nat (byte 2)) byteNaturalTwoHundredFiftySix)
141 (byte-to-nat (byte 64))))
142 (branch
143 EmbeddingGatherF32Width512
144 .
145 (naturalAdd byteNaturalTwoHundredFiftySix byteNaturalTwoHundredFiftySix))
146 (branch EmbeddingGatherF32Width256 . byteNaturalTwoHundredFiftySix)))
147
148-- The family above bounds every width to a 32-bit immediate. Keeping this
149-- conversion tied to the row width prevents launch and address drift.
150def embeddingGatherF32WidthImmediateFor =
151 (lambda unrestricted width : (family EmbeddingGatherF32Width) .
152 (sm86Unsigned32FromNaturalTruncated (embeddingGatherF32WidthElements width)))
153
154def embeddingGatherF32BlockXFor =
155 (lambda unrestricted width : (family EmbeddingGatherF32Width) .
156 (naturalDivideUnchecked
157 (embeddingGatherF32WidthElements width)
158 embeddingGatherF32NaturalFour))
159
160def embeddingGatherF32ConstantBase =
161 (embeddingGatherF32Unsigned32 (byte 40) (byte 0) (byte 0) (byte 0))
162
163-- CB0 pointer ordinal contract for the gather's output, token stream and
164-- F32 embedding table. The launch planner turns these into QMD-relative
165-- parameter patches; system code never repeats their word offsets.
166def embeddingGatherF32OutputArgument : Nat = 0
167def embeddingGatherF32TokenIdsArgument : Nat = 1
168def embeddingGatherF32EmbeddingArgument : Nat = 2
169def embeddingGatherF32ArgumentCount : Nat = 3
170
171def embeddingGatherF32OutputPointer =
172 (embeddingGatherF32Unsigned32 (byte 96) (byte 1) (byte 0) (byte 0))
173
174def embeddingGatherF32TokenIdsPointer =
175 (embeddingGatherF32Unsigned32 (byte 104) (byte 1) (byte 0) (byte 0))
176
177def embeddingGatherF32EmbeddingPointer =
178 (embeddingGatherF32Unsigned32 (byte 112) (byte 1) (byte 0) (byte 0))
179
180def embeddingGatherF32SetBarrier0 =
181 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier0))
182
183def embeddingGatherF32SetBarrier1 =
184 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier1))
185
186def embeddingGatherF32SetBarrier2 =
187 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier2))
188
189def embeddingGatherF32SetBarrier3 =
190 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier3))
191
192def embeddingGatherF32SetBarrier4 =
193 (sm86SetBarrierControl (constructor SM86Barrier SM86Barrier4))
194
195def embeddingGatherF32WaitSpecials : (family SM86Control) =
196 (constructor
197 SM86Control
198 SM86ControlValue
199 (byte 7)
200 (constructor SM86YieldMode SM86Continue)
201 (constructor SM86Barrier SM86BarrierNone)
202 (constructor SM86Barrier SM86BarrierNone)
203 (byte 3)
204 (byte 0))
205
206def embeddingGatherF32WaitToken =
207 (sm86WaitBarrierControl (constructor SM86WaitBarrier SM86WaitBarrier0))
208
209def embeddingGatherF32WaitEmbedding : (family SM86Control) =
210 (constructor
211 SM86Control
212 SM86ControlValue
213 (byte 7)
214 (constructor SM86YieldMode SM86Continue)
215 (constructor SM86Barrier SM86BarrierNone)
216 (constructor SM86Barrier SM86BarrierNone)
217 (byte 30)
218 (byte 0))
219
220def embeddingGatherF32Instruction =
221 (lambda unrestricted body : (family SM86InstructionBody) .
222 (sm86ProgramSingleton
223 (constructor
224 SM86Instruction
225 SM86InstructionValue
226 (constructor SM86InstructionGuard SM86InstructionAlways)
227 body)))
228
229def embeddingGatherF32Append =
230 (lambda unrestricted left : (family SM86Program) .
231 (lambda unrestricted right : (family SM86Program) . (sm86ProgramAppend left right)))
232
233def embeddingGatherF32Prologue =
234 (embeddingGatherF32Append
235 (embeddingGatherF32Instruction
236 (constructor
237 SM86InstructionBody
238 SM86MoveConstant
239 (embeddingGatherF32Register (byte 1))
240 (byte 0)
241 embeddingGatherF32ConstantBase
242 sm86SafeControl))
243 (embeddingGatherF32Append
244 (embeddingGatherF32Instruction
245 (constructor
246 SM86InstructionBody
247 SM86SpecialToRegister
248 (embeddingGatherF32Register (byte 0))
249 (constructor SM86SpecialRegister SM86ThreadIdX)
250 embeddingGatherF32SetBarrier0))
251 (embeddingGatherF32Append
252 (embeddingGatherF32Instruction
253 (constructor
254 SM86InstructionBody
255 SM86SpecialToRegister
256 (embeddingGatherF32Register (byte 4))
257 (constructor SM86SpecialRegister SM86CooperativeThreadArrayIdY)
258 embeddingGatherF32SetBarrier1))
259 (embeddingGatherF32Instruction
260 (constructor
261 SM86InstructionBody
262 SM86MoveImmediate
263 (embeddingGatherF32Register (byte 3))
264 embeddingGatherF32FourImmediate
265 embeddingGatherF32WaitSpecials)))))
266
267def embeddingGatherF32AddressProgramFor =
268 (lambda unrestricted width : (family EmbeddingGatherF32Width) .
269 (embeddingGatherF32Append
270 (embeddingGatherF32Instruction
271 (constructor
272 SM86InstructionBody
273 SM86IntegerMultiplyAddImmediate
274 (embeddingGatherF32Register (byte 6))
275 (embeddingGatherF32Register (byte 0))
276 embeddingGatherF32FourImmediate
277 sm86ZeroRegister
278 sm86SafeControl))
279 (embeddingGatherF32Append
280 (embeddingGatherF32Instruction
281 (constructor
282 SM86InstructionBody
283 SM86IntegerMultiplyAddWideConstant
284 (embeddingGatherF32Register (byte 8))
285 (embeddingGatherF32Register (byte 4))
286 (embeddingGatherF32Register (byte 3))
287 (byte 0)
288 embeddingGatherF32TokenIdsPointer
289 sm86SafeControl))
290 (embeddingGatherF32Append
291 (embeddingGatherF32Instruction
292 (constructor
293 SM86InstructionBody
294 SM86LoadGlobal
295 (embeddingGatherF32Register (byte 10))
296 (embeddingGatherF32Register (byte 8))
297 embeddingGatherF32ZeroImmediate
298 embeddingGatherF32SetBarrier0))
299 (embeddingGatherF32Append
300 (embeddingGatherF32Instruction
301 (constructor
302 SM86InstructionBody
303 SM86IntegerMultiplyAddImmediate
304 (embeddingGatherF32Register (byte 18))
305 (embeddingGatherF32Register (byte 4))
306 (embeddingGatherF32WidthImmediateFor width)
307 (embeddingGatherF32Register (byte 6))
308 sm86SafeControl))
309 (embeddingGatherF32Append
310 (embeddingGatherF32Instruction
311 (constructor
312 SM86InstructionBody
313 SM86IntegerMultiplyAddWideConstant
314 (embeddingGatherF32Register (byte 20))
315 (embeddingGatherF32Register (byte 18))
316 (embeddingGatherF32Register (byte 3))
317 (byte 0)
318 embeddingGatherF32OutputPointer
319 sm86SafeControl))
320 (embeddingGatherF32Append
321 (embeddingGatherF32Instruction
322 (constructor
323 SM86InstructionBody
324 SM86IntegerMultiplyAddImmediate
325 (embeddingGatherF32Register (byte 12))
326 (embeddingGatherF32Register (byte 10))
327 (embeddingGatherF32WidthImmediateFor width)
328 (embeddingGatherF32Register (byte 6))
329 embeddingGatherF32WaitToken))
330 (embeddingGatherF32Instruction
331 (constructor
332 SM86InstructionBody
333 SM86IntegerMultiplyAddWideConstant
334 (embeddingGatherF32Register (byte 14))
335 (embeddingGatherF32Register (byte 12))
336 (embeddingGatherF32Register (byte 3))
337 (byte 0)
338 embeddingGatherF32EmbeddingPointer
339 sm86SafeControl)))))))))
340
341def embeddingGatherF32AddressProgram =
342 (embeddingGatherF32AddressProgramFor
343 (constructor EmbeddingGatherF32Width EmbeddingGatherF32Width1024))
344
345def embeddingGatherF32Loads =
346 (embeddingGatherF32Append
347 (embeddingGatherF32Instruction
348 (constructor
349 SM86InstructionBody
350 SM86LoadGlobal
351 (embeddingGatherF32Register (byte 16))
352 (embeddingGatherF32Register (byte 14))
353 embeddingGatherF32ZeroImmediate
354 embeddingGatherF32SetBarrier1))
355 (embeddingGatherF32Append
356 (embeddingGatherF32Instruction
357 (constructor
358 SM86InstructionBody
359 SM86LoadGlobal
360 (embeddingGatherF32Register (byte 17))
361 (embeddingGatherF32Register (byte 14))
362 embeddingGatherF32FourImmediate
363 embeddingGatherF32SetBarrier2))
364 (embeddingGatherF32Append
365 (embeddingGatherF32Instruction
366 (constructor
367 SM86InstructionBody
368 SM86LoadGlobal
369 (embeddingGatherF32Register (byte 18))
370 (embeddingGatherF32Register (byte 14))
371 embeddingGatherF32EightImmediate
372 embeddingGatherF32SetBarrier3))
373 (embeddingGatherF32Instruction
374 (constructor
375 SM86InstructionBody
376 SM86LoadGlobal
377 (embeddingGatherF32Register (byte 19))
378 (embeddingGatherF32Register (byte 14))
379 embeddingGatherF32TwelveImmediate
380 embeddingGatherF32SetBarrier4)))))
381
382def embeddingGatherF32Stores =
383 (embeddingGatherF32Append
384 (embeddingGatherF32Instruction
385 (constructor
386 SM86InstructionBody
387 SM86StoreGlobal
388 (embeddingGatherF32Register (byte 20))
389 (embeddingGatherF32Register (byte 16))
390 embeddingGatherF32ZeroImmediate
391 embeddingGatherF32WaitEmbedding))
392 (embeddingGatherF32Append
393 (embeddingGatherF32Instruction
394 (constructor
395 SM86InstructionBody
396 SM86StoreGlobal
397 (embeddingGatherF32Register (byte 20))
398 (embeddingGatherF32Register (byte 17))
399 embeddingGatherF32FourImmediate
400 sm86SafeControl))
401 (embeddingGatherF32Append
402 (embeddingGatherF32Instruction
403 (constructor
404 SM86InstructionBody
405 SM86StoreGlobal
406 (embeddingGatherF32Register (byte 20))
407 (embeddingGatherF32Register (byte 18))
408 embeddingGatherF32EightImmediate
409 sm86SafeControl))
410 (embeddingGatherF32Instruction
411 (constructor
412 SM86InstructionBody
413 SM86StoreGlobal
414 (embeddingGatherF32Register (byte 20))
415 (embeddingGatherF32Register (byte 19))
416 embeddingGatherF32TwelveImmediate
417 sm86SafeControl)))))
418
419def embeddingGatherF32Exit =
420 (embeddingGatherF32Instruction (constructor SM86InstructionBody SM86Exit sm86SafeControl))
421
422def embeddingGatherF32ProgramFor =
423 (lambda unrestricted width : (family EmbeddingGatherF32Width) .
424 (embeddingGatherF32Append
425 embeddingGatherF32Prologue
426 (embeddingGatherF32Append
427 (embeddingGatherF32AddressProgramFor width)
428 (embeddingGatherF32Append
429 embeddingGatherF32Loads
430 (embeddingGatherF32Append embeddingGatherF32Stores embeddingGatherF32Exit)))))
431
432def embeddingGatherF32Program : (family SM86Program) =
433 (embeddingGatherF32ProgramFor (constructor EmbeddingGatherF32Width EmbeddingGatherF32Width1024))
434
435def embeddingGatherF32FailureCodeBytes =
436 (lambda unrestricted code : (family EmbeddingGatherF32FailureCode) .
437 (eliminate
438 EmbeddingGatherF32FailureCode
439 (lambda unrestricted current : (family EmbeddingGatherF32FailureCode) . Bytes)
440 code
441 (branch EmbeddingGatherF32TokenOutOfBounds . b"ALPHA-SM86-EMB-001")
442 (branch EmbeddingGatherF32ChannelOutOfBounds . b"ALPHA-SM86-EMB-002")
443 (branch EmbeddingGatherF32TokenCountZero . b"ALPHA-SM86-EMB-003")
444 (branch EmbeddingGatherF32InstructionCountMismatch . b"ALPHA-SM86-EMB-004")
445 (branch EmbeddingGatherF32EncodingFailed . b"ALPHA-SM86-EMB-005")
446 (branch EmbeddingGatherF32IdentityInvalid . b"ALPHA-SM86-EMB-006")))
447
448def embeddingGatherF32Offset =
449 (lambda unrestricted token : Nat .
450 (lambda unrestricted channel : Nat .
451 (nat-eliminate
452 (lambda unrestricted tokenValid : Nat . (family EmbeddingGatherF32OffsetResult))
453 (constructor
454 EmbeddingGatherF32OffsetResult
455 EmbeddingGatherF32OffsetInvalid
456 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32TokenOutOfBounds)
457 token
458 channel)
459 (lambda unrestricted tokenPredecessor : Nat .
460 (lambda unrestricted tokenInduction : (family EmbeddingGatherF32OffsetResult) .
461 (nat-eliminate
462 (lambda unrestricted channelValid : Nat . (family EmbeddingGatherF32OffsetResult))
463 (constructor
464 EmbeddingGatherF32OffsetResult
465 EmbeddingGatherF32OffsetInvalid
466 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32ChannelOutOfBounds)
467 token
468 channel)
469 (lambda unrestricted channelPredecessor : Nat .
470 (lambda unrestricted channelInduction : (family EmbeddingGatherF32OffsetResult) .
471 (constructor
472 EmbeddingGatherF32OffsetResult
473 EmbeddingGatherF32OffsetValid
474 (naturalMultiply
475 embeddingGatherF32NaturalFour
476 (naturalAdd
477 (naturalMultiply token embeddingGatherF32NaturalOneThousandTwentyFour)
478 channel)))))
479 (naturalLess channel embeddingGatherF32NaturalOneThousandTwentyFour))))
480 (naturalLess token embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight))))
481
482def embeddingGatherF32RejectedTelemetry =
483 (lambda unrestricted code : (family EmbeddingGatherF32FailureCode) .
484 (lambda unrestricted ordinal : Nat .
485 (constructor EmbeddingGatherF32Telemetry EmbeddingGatherF32TelemetryRejected code ordinal)))
486
487def embeddingGatherF32PlanFor =
488 (lambda unrestricted width : (family EmbeddingGatherF32Width) .
489 (lambda unrestricted tokenCount : Nat .
490 (nat-eliminate
491 (lambda unrestricted tokenCountNonzero : Nat . (family EmbeddingGatherF32PlanResult))
492 (constructor
493 EmbeddingGatherF32PlanResult
494 EmbeddingGatherF32PlanFailed
495 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32TokenCountZero)
496 (embeddingGatherF32RejectedTelemetry
497 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32TokenCountZero)
498 zero))
499 (lambda unrestricted nonzeroPredecessor : Nat .
500 (lambda unrestricted nonzeroInduction : (family EmbeddingGatherF32PlanResult) .
501 (app
502 (lambda unrestricted actualInstructions : Nat .
503 (nat-eliminate
504 (lambda unrestricted countValid : Nat . (family EmbeddingGatherF32PlanResult))
505 (constructor
506 EmbeddingGatherF32PlanResult
507 EmbeddingGatherF32PlanFailed
508 (constructor
509 EmbeddingGatherF32FailureCode
510 EmbeddingGatherF32InstructionCountMismatch)
511 (embeddingGatherF32RejectedTelemetry
512 (constructor
513 EmbeddingGatherF32FailureCode
514 EmbeddingGatherF32InstructionCountMismatch)
515 actualInstructions))
516 (lambda unrestricted countPredecessor : Nat .
517 (lambda unrestricted countInduction : (family EmbeddingGatherF32PlanResult) .
518 (constructor
519 EmbeddingGatherF32PlanResult
520 EmbeddingGatherF32PlanReady
521 (constructor
522 EmbeddingGatherF32Plan
523 EmbeddingGatherF32PlanValue
524 tokenCount
525 (embeddingGatherF32ProgramFor width)
526 (constructor
527 EmbeddingGatherF32Telemetry
528 EmbeddingGatherF32TelemetryValue
529 embeddingGatherF32NaturalTwenty
530 actualInstructions
531 embeddingGatherF32NaturalTwentyFour
532 tokenCount
533 tokenCount
534 (embeddingGatherF32BlockXFor width)
535 (embeddingGatherF32WidthElements width)
536 embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight
537 embeddingGatherF32NaturalFour
538 embeddingGatherF32NaturalFour
539 zero
540 zero
541 zero
542 zero)))))
543 (naturalEqual actualInstructions embeddingGatherF32NaturalTwenty)))
544 (sm86ProgramCount (embeddingGatherF32ProgramFor width)))))
545 (naturalNonzero tokenCount))))
546
547def embeddingGatherF32Plan =
548 (lambda unrestricted tokenCount : Nat .
549 (embeddingGatherF32PlanFor
550 (constructor EmbeddingGatherF32Width EmbeddingGatherF32Width1024)
551 tokenCount))
552
553def embeddingGatherF32ImageFor =
554 (lambda unrestricted width : (family EmbeddingGatherF32Width) .
555 (lambda unrestricted tokenCount : Nat .
556 (eliminate
557 EmbeddingGatherF32PlanResult
558 (lambda unrestricted current : (family EmbeddingGatherF32PlanResult) .
559 (family EmbeddingGatherF32ImageResult))
560 (embeddingGatherF32PlanFor width tokenCount)
561 (branch
562 EmbeddingGatherF32PlanReady
563 plan
564 .
565 (eliminate
566 EmbeddingGatherF32Plan
567 (lambda unrestricted current : (family EmbeddingGatherF32Plan) .
568 (family EmbeddingGatherF32ImageResult))
569 plan
570 (branch
571 EmbeddingGatherF32PlanValue
572 plannedTokens
573 program
574 telemetry
575 .
576 (eliminate
577 SM86ProgramEncodingResult
578 (lambda unrestricted current : (family SM86ProgramEncodingResult) .
579 (family EmbeddingGatherF32ImageResult))
580 (sm86EncodeProgram program)
581 (branch
582 SM86ProgramEncodingSucceeded
583 image
584 encodingTelemetry
585 .
586 (app
587 (lambda unrestricted identity : Bytes .
588 (nat-eliminate
589 (lambda unrestricted identityValid : Nat .
590 (family EmbeddingGatherF32ImageResult))
591 (constructor
592 EmbeddingGatherF32ImageResult
593 EmbeddingGatherF32ImageFailed
594 (constructor
595 EmbeddingGatherF32FailureCode
596 EmbeddingGatherF32IdentityInvalid)
597 zero
598 (embeddingGatherF32FailureCodeBytes
599 (constructor
600 EmbeddingGatherF32FailureCode
601 EmbeddingGatherF32IdentityInvalid))
602 telemetry)
603 (lambda unrestricted identityPredecessor : Nat .
604 (lambda unrestricted identityInduction : (family EmbeddingGatherF32ImageResult) .
605 (eliminate
606 SM86ProgramEncodingTelemetry
607 (lambda unrestricted current : (family SM86ProgramEncodingTelemetry) .
608 (family EmbeddingGatherF32ImageResult))
609 encodingTelemetry
610 (branch
611 SM86ProgramEncodingTelemetryValue
612 instructions
613 bytes
614 fields
615 bits
616 highest
617 .
618 (constructor
619 EmbeddingGatherF32ImageResult
620 EmbeddingGatherF32ImageReady
621 image
622 identity
623 (constructor
624 EmbeddingGatherF32Telemetry
625 EmbeddingGatherF32TelemetryValue
626 embeddingGatherF32NaturalTwenty
627 instructions
628 embeddingGatherF32NaturalTwentyFour
629 plannedTokens
630 plannedTokens
631 (embeddingGatherF32BlockXFor width)
632 (embeddingGatherF32WidthElements width)
633 embeddingGatherF32NaturalTwelveThousandTwoHundredEightyEight
634 embeddingGatherF32NaturalFour
635 embeddingGatherF32NaturalFour
636 zero
637 bytes
638 fields
639 bits))))))
640 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64)))))
641 (sha256HexBytesOrEmpty (sha256Hex image))))
642 (branch
643 SM86ProgramEncodingFailed
644 instructionIndex
645 failure
646 encodingTelemetry
647 .
648 (constructor
649 EmbeddingGatherF32ImageResult
650 EmbeddingGatherF32ImageFailed
651 (constructor EmbeddingGatherF32FailureCode EmbeddingGatherF32EncodingFailed)
652 instructionIndex
653 (sm86InstructionEncodingStableCode failure)
654 telemetry))))))
655 (branch
656 EmbeddingGatherF32PlanFailed
657 code
658 telemetry
659 .
660 (constructor
661 EmbeddingGatherF32ImageResult
662 EmbeddingGatherF32ImageFailed
663 code
664 zero
665 (embeddingGatherF32FailureCodeBytes code)
666 telemetry)))))
667
668def embeddingGatherF32Image =
669 (lambda unrestricted tokenCount : Nat .
670 (embeddingGatherF32ImageFor
671 (constructor EmbeddingGatherF32Width EmbeddingGatherF32Width1024)
672 tokenCount))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.