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