1module Hardware.Nvidia.SM86.Command.Pushbuffer
2
3import Data.Bytes
4import Model.Word32
5import Model.Word32Logic
6import Model.Word64
7import Std.Byte
8import Std.Natural
9import Model.Parameter
10import Model.Config
11
12family PushbufferErrorCode : Type 0
13constructor PushbufferOpcodeOutOfRange
14constructor PushbufferCountOutOfRange
15constructor PushbufferSubchannelOutOfRange
16constructor PushbufferMethodAddressUnaligned
17constructor PushbufferMethodAddressOutOfRange
18constructor PushbufferAddressUnaligned
19constructor PushbufferAddressOutOfRange
20constructor PushbufferLengthOutOfRange
21constructor PushbufferAlignmentOverflow
22constructor PushbufferQMDAddressUnaligned
23
24end-family
25
26family PushbufferBytesResult : Type 0
27constructor PushbufferBytesReady
28field unrestricted pushbufferEncodedBytes : Bytes
29constructor PushbufferBytesRejected
30field unrestricted pushbufferBytesError : (family PushbufferErrorCode)
31
32end-family
33
34family PushbufferDwordList : Type 0
35constructor PushbufferDwordEnd
36constructor PushbufferDwordNext
37field unrestricted pushbufferDwordHead : (family ModelWord32)
38recursive unrestricted pushbufferDwordTail
39
40end-family
41
42family PushbufferGPFIFOEntryResult : Type 0
43constructor PushbufferGPFIFOEntryReady
44field unrestricted pushbufferGPFIFOLow : (family ModelWord32)
45field unrestricted pushbufferGPFIFOHigh : (family ModelWord32)
46constructor PushbufferGPFIFOEntryRejected
47field unrestricted pushbufferGPFIFOError : (family PushbufferErrorCode)
48
49end-family
50
51family PushbufferAlignedDwordsResult : Type 0
52constructor PushbufferAlignedDwordsReady
53field unrestricted pushbufferAlignedDwords : (family ModelWord32)
54constructor PushbufferAlignedDwordsRejected
55field unrestricted pushbufferAlignedDwordsError : (family PushbufferErrorCode)
56
57end-family
58
59family PushbufferConstructionError : Type 0
60constructor PushbufferInlineQMDLengthMismatch
61constructor PushbufferComputeConfigurationMismatch
62constructor PushbufferConstructionIdentityMalformed
63constructor PushbufferConstructionRejected
64field unrestricted pushbufferConstructionCause : (family PushbufferErrorCode)
65
66end-family
67
68family PushbufferComputeConfig : Type 0
69constructor PushbufferComputeConfigValue
70field unrestricted pushbufferComputeClass : (family ModelWord32)
71field unrestricted pushbufferComputeSharedWindow : (family ModelWord64)
72field unrestricted pushbufferComputeLocalMemory : (family ModelWord64)
73field unrestricted pushbufferComputeLocalMemoryBytes : (family ModelWord64)
74field unrestricted pushbufferComputeLocalWindow : (family ModelWord64)
75field unrestricted pushbufferComputeSMCount : (family ModelWord32)
76field unrestricted pushbufferComputeSPAVersion : (family ModelWord32)
77
78end-family
79
80family PushbufferConstructionReceipt : Type 0
81constructor PushbufferConstructionReceiptValue
82field unrestricted pushbufferConstructionIdentity : Bytes
83field unrestricted pushbufferConstructionBytes : Bytes
84field unrestricted pushbufferConstructionDwords : Nat
85field unrestricted pushbufferConstructionHostFallbacks : Nat
86
87end-family
88
89family PushbufferConstructionResult : Type 0
90constructor PushbufferConstructionReady
91field unrestricted pushbufferConstructionReadyReceipt : (family PushbufferConstructionReceipt)
92constructor PushbufferConstructionFailed
93field unrestricted pushbufferConstructionError : (family PushbufferConstructionError)
94
95end-family
96
97def pushbufferErrorCodeBytes =
98 (lambda unrestricted code : (family PushbufferErrorCode) .
99 (eliminate
100 PushbufferErrorCode
101 (lambda unrestricted current : (family PushbufferErrorCode) . Bytes)
102 code
103 (branch PushbufferOpcodeOutOfRange . b"ALPHA-HPB-201")
104 (branch PushbufferCountOutOfRange . b"ALPHA-HPB-202")
105 (branch PushbufferSubchannelOutOfRange . b"ALPHA-HPB-203")
106 (branch PushbufferMethodAddressUnaligned . b"ALPHA-HPB-204")
107 (branch PushbufferMethodAddressOutOfRange . b"ALPHA-HPB-205")
108 (branch PushbufferAddressUnaligned . b"ALPHA-HPB-206")
109 (branch PushbufferAddressOutOfRange . b"ALPHA-HPB-207")
110 (branch PushbufferLengthOutOfRange . b"ALPHA-HPB-208")
111 (branch PushbufferAlignmentOverflow . b"ALPHA-HPB-209")
112 (branch PushbufferQMDAddressUnaligned . b"ALPHA-HPB-210")))
113
114def pushbufferDwordCount =
115 (lambda unrestricted values : (family PushbufferDwordList) .
116 (eliminate
117 PushbufferDwordList
118 (lambda unrestricted current : (family PushbufferDwordList) . Nat)
119 values
120 (branch PushbufferDwordEnd . zero)
121 (branch PushbufferDwordNext head tail ih_tail . (succ ih_tail))))
122
123def pushbufferEncodeDwords =
124 (lambda unrestricted values : (family PushbufferDwordList) .
125 (eliminate
126 PushbufferDwordList
127 (lambda unrestricted current : (family PushbufferDwordList) . Bytes)
128 values
129 (branch PushbufferDwordEnd . b"")
130 (branch
131 PushbufferDwordNext
132 head
133 tail
134 ih_tail
135 .
136 (bytes-append (dataBytesWord32LE head) ih_tail))))
137
138def pushbufferFlagAnd =
139 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (naturalAnd left right)))
140
141def pushbufferFlagOr =
142 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (naturalOr left right)))
143
144def pushbufferIfFlag =
145 (lambda unrestricted condition : Nat .
146 (lambda unrestricted whenTrue : Nat .
147 (lambda unrestricted whenFalse : Nat .
148 (nat-eliminate
149 (lambda unrestricted current : Nat . Nat)
150 whenFalse
151 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . whenTrue))
152 condition))))
153
154def pushbufferByteIsZero =
155 (lambda unrestricted value : Byte . (naturalIsZero (byte-to-nat value)))
156
157def pushbufferByteNonZero =
158 (lambda unrestricted value : Byte . (naturalIsZero (pushbufferByteIsZero value)))
159
160def pushbufferWord32NonZero =
161 (lambda unrestricted value : (family ModelWord32) .
162 (eliminate
163 ModelWord32
164 (lambda unrestricted current : (family ModelWord32) . Nat)
165 value
166 (branch
167 ModelWord32Value
168 b0
169 b1
170 b2
171 b3
172 .
173 (pushbufferFlagOr
174 (pushbufferByteNonZero b0)
175 (pushbufferFlagOr
176 (pushbufferByteNonZero b1)
177 (pushbufferFlagOr (pushbufferByteNonZero b2) (pushbufferByteNonZero b3)))))))
178
179def pushbufferAddressAligned4 =
180 (lambda unrestricted address : (family ModelWord64) .
181 (eliminate
182 ModelWord64
183 (lambda unrestricted current : (family ModelWord64) . Nat)
184 address
185 (branch
186 ModelWord64Value
187 b0
188 b1
189 b2
190 b3
191 b4
192 b5
193 b6
194 b7
195 .
196 (naturalIsZero (naturalModuloUnchecked (byte-to-nat b0) (byte-to-nat (byte 4)))))))
197
198def pushbufferAddressAligned16 =
199 (lambda unrestricted address : (family ModelWord64) .
200 (eliminate
201 ModelWord64
202 (lambda unrestricted current : (family ModelWord64) . Nat)
203 address
204 (branch
205 ModelWord64Value
206 b0
207 b1
208 b2
209 b3
210 b4
211 b5
212 b6
213 b7
214 .
215 (naturalIsZero (naturalModuloUnchecked (byte-to-nat b0) (byte-to-nat (byte 16)))))))
216
217def pushbufferAddressAligned256 =
218 (lambda unrestricted address : (family ModelWord64) .
219 (eliminate
220 ModelWord64
221 (lambda unrestricted current : (family ModelWord64) . Nat)
222 address
223 (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (pushbufferByteIsZero b0))))
224
225def pushbufferAddressIn40Bits =
226 (lambda unrestricted address : (family ModelWord64) .
227 (eliminate
228 ModelWord64
229 (lambda unrestricted current : (family ModelWord64) . Nat)
230 address
231 (branch
232 ModelWord64Value
233 b0
234 b1
235 b2
236 b3
237 b4
238 b5
239 b6
240 b7
241 .
242 (pushbufferFlagAnd
243 (pushbufferByteIsZero b5)
244 (pushbufferFlagAnd (pushbufferByteIsZero b6) (pushbufferByteIsZero b7))))))
245
246def pushbufferMethodHeaderUnchecked =
247 (lambda unrestricted opcode : Nat .
248 (lambda unrestricted count : Nat .
249 (lambda unrestricted subchannel : Nat .
250 (lambda unrestricted byteAddress : Nat .
251 (app
252 (lambda unrestricted dwordAddress : Nat .
253 (bytes
254 (nat-to-byte (naturalModuloUnchecked dwordAddress (succ (byte-to-nat (byte 255)))))
255 (nat-to-byte
256 (naturalAdd
257 (naturalDivideUnchecked dwordAddress (succ (byte-to-nat (byte 255))))
258 (naturalMultiply subchannel (byte-to-nat (byte 32)))))
259 (nat-to-byte (naturalModuloUnchecked count (succ (byte-to-nat (byte 255)))))
260 (nat-to-byte
261 (naturalAdd
262 (naturalDivideUnchecked count (succ (byte-to-nat (byte 255))))
263 (naturalMultiply opcode (byte-to-nat (byte 32)))))))
264 (naturalDivideUnchecked byteAddress (byte-to-nat (byte 4))))))))
265
266def pushbufferMethodHeader =
267 (lambda unrestricted opcode : Nat .
268 (lambda unrestricted count : Nat .
269 (lambda unrestricted subchannel : Nat .
270 (lambda unrestricted byteAddress : Nat .
271 (nat-eliminate
272 (lambda unrestricted opcodeValid : Nat . (family PushbufferBytesResult))
273 (constructor
274 PushbufferBytesResult
275 PushbufferBytesRejected
276 (constructor PushbufferErrorCode PushbufferOpcodeOutOfRange))
277 (lambda unrestricted opcodePredecessor : Nat .
278 (lambda unrestricted opcodeInduction : (family PushbufferBytesResult) .
279 (nat-eliminate
280 (lambda unrestricted countValid : Nat . (family PushbufferBytesResult))
281 (constructor
282 PushbufferBytesResult
283 PushbufferBytesRejected
284 (constructor PushbufferErrorCode PushbufferCountOutOfRange))
285 (lambda unrestricted countPredecessor : Nat .
286 (lambda unrestricted countInduction : (family PushbufferBytesResult) .
287 (nat-eliminate
288 (lambda unrestricted subchannelValid : Nat . (family PushbufferBytesResult))
289 (constructor
290 PushbufferBytesResult
291 PushbufferBytesRejected
292 (constructor PushbufferErrorCode PushbufferSubchannelOutOfRange))
293 (lambda unrestricted subchannelPredecessor : Nat .
294 (lambda unrestricted subchannelInduction : (family PushbufferBytesResult) .
295 (nat-eliminate
296 (lambda unrestricted addressAligned : Nat .
297 (family PushbufferBytesResult))
298 (constructor
299 PushbufferBytesResult
300 PushbufferBytesRejected
301 (constructor PushbufferErrorCode PushbufferMethodAddressUnaligned))
302 (lambda unrestricted alignedPredecessor : Nat .
303 (lambda unrestricted alignedInduction : (family PushbufferBytesResult) .
304 (nat-eliminate
305 (lambda unrestricted addressValid : Nat .
306 (family PushbufferBytesResult))
307 (constructor
308 PushbufferBytesResult
309 PushbufferBytesRejected
310 (constructor
311 PushbufferErrorCode
312 PushbufferMethodAddressOutOfRange))
313 (lambda unrestricted addressPredecessor : Nat .
314 (lambda unrestricted addressInduction : (family PushbufferBytesResult) .
315 (constructor
316 PushbufferBytesResult
317 PushbufferBytesReady
318 (pushbufferMethodHeaderUnchecked
319 opcode
320 count
321 subchannel
322 byteAddress))))
323 (nat-less-than
324 (naturalDivideUnchecked byteAddress (byte-to-nat (byte 4)))
325 (naturalPowerOfTwo (byte-to-nat (byte 13)))))))
326 (naturalIsZero
327 (naturalModuloUnchecked byteAddress (byte-to-nat (byte 4)))))))
328 (nat-less-than subchannel (byte-to-nat (byte 8))))))
329 (nat-less-than count (naturalPowerOfTwo (byte-to-nat (byte 13)))))))
330 (nat-less-than opcode (byte-to-nat (byte 8))))))))
331
332def pushbufferIncrementingMethod =
333 (lambda unrestricted subchannel : Nat .
334 (lambda unrestricted byteAddress : Nat .
335 (lambda unrestricted values : (family PushbufferDwordList) .
336 (eliminate
337 PushbufferBytesResult
338 (lambda unrestricted current : (family PushbufferBytesResult) .
339 (family PushbufferBytesResult))
340 (pushbufferMethodHeader (succ zero) (pushbufferDwordCount values) subchannel byteAddress)
341 (branch
342 PushbufferBytesReady
343 header
344 .
345 (constructor
346 PushbufferBytesResult
347 PushbufferBytesReady
348 (bytes-append header (pushbufferEncodeDwords values))))
349 (branch
350 PushbufferBytesRejected
351 error
352 .
353 (constructor PushbufferBytesResult PushbufferBytesRejected error))))))
354
355def pushbufferImmediateMethod =
356 (lambda unrestricted subchannel : Nat .
357 (lambda unrestricted byteAddress : Nat .
358 (lambda unrestricted value : Nat .
359 (pushbufferMethodHeader (byte-to-nat (byte 4)) value subchannel byteAddress))))
360
361def pushbufferSemaphoreRelease =
362 (lambda unrestricted address : (family ModelWord64) .
363 (lambda unrestricted payload : (family ModelWord32) .
364 (nat-eliminate
365 (lambda unrestricted aligned : Nat . (family PushbufferBytesResult))
366 (constructor
367 PushbufferBytesResult
368 PushbufferBytesRejected
369 (constructor PushbufferErrorCode PushbufferAddressUnaligned))
370 (lambda unrestricted alignedPredecessor : Nat .
371 (lambda unrestricted alignedInduction : (family PushbufferBytesResult) .
372 (nat-eliminate
373 (lambda unrestricted inRange : Nat . (family PushbufferBytesResult))
374 (constructor
375 PushbufferBytesResult
376 PushbufferBytesRejected
377 (constructor PushbufferErrorCode PushbufferAddressOutOfRange))
378 (lambda unrestricted rangePredecessor : Nat .
379 (lambda unrestricted rangeInduction : (family PushbufferBytesResult) .
380 (eliminate
381 ModelWord64
382 (lambda unrestricted current : (family ModelWord64) .
383 (family PushbufferBytesResult))
384 address
385 (branch
386 ModelWord64Value
387 b0
388 b1
389 b2
390 b3
391 b4
392 b5
393 b6
394 b7
395 .
396 (constructor
397 PushbufferBytesResult
398 PushbufferBytesReady
399 (bytes-append
400 (bytes 23 32 5 32)
401 (bytes-append
402 (bytes b0 b1 b2 b3)
403 (bytes-append
404 (bytes b4 0 0 0)
405 (bytes-append
406 (dataBytesWord32LE payload)
407 (bytes-append (bytes 0 0 0 0) (bytes 1 0 16 0)))))))))))
408 (pushbufferAddressIn40Bits address))))
409 (pushbufferAddressAligned4 address))))
410
411def pushbufferSemaphoreAcquire =
412 (lambda unrestricted address : (family ModelWord64) .
413 (lambda unrestricted payload : (family ModelWord32) .
414 (nat-eliminate
415 (lambda unrestricted aligned : Nat . (family PushbufferBytesResult))
416 (constructor
417 PushbufferBytesResult
418 PushbufferBytesRejected
419 (constructor PushbufferErrorCode PushbufferAddressUnaligned))
420 (lambda unrestricted alignedPredecessor : Nat .
421 (lambda unrestricted alignedInduction : (family PushbufferBytesResult) .
422 (nat-eliminate
423 (lambda unrestricted inRange : Nat . (family PushbufferBytesResult))
424 (constructor
425 PushbufferBytesResult
426 PushbufferBytesRejected
427 (constructor PushbufferErrorCode PushbufferAddressOutOfRange))
428 (lambda unrestricted rangePredecessor : Nat .
429 (lambda unrestricted rangeInduction : (family PushbufferBytesResult) .
430 (eliminate
431 ModelWord64
432 (lambda unrestricted current : (family ModelWord64) .
433 (family PushbufferBytesResult))
434 address
435 (branch
436 ModelWord64Value
437 b0
438 b1
439 b2
440 b3
441 b4
442 b5
443 b6
444 b7
445 .
446 (constructor
447 PushbufferBytesResult
448 PushbufferBytesReady
449 (bytes-append
450 (bytes 23 32 5 32)
451 (bytes-append
452 (bytes b0 b1 b2 b3)
453 (bytes-append
454 (bytes b4 0 0 0)
455 (bytes-append
456 (dataBytesWord32LE payload)
457 (bytes-append (bytes 0 0 0 0) (bytes 0 0 0 0)))))))))))
458 (pushbufferAddressIn40Bits address))))
459 (pushbufferAddressAligned4 address))))
460
461def pushbufferSemaphoreReleaseTimestamp =
462 (lambda unrestricted address : (family ModelWord64) .
463 (lambda unrestricted payload : (family ModelWord64) .
464 (nat-eliminate
465 (lambda unrestricted aligned : Nat . (family PushbufferBytesResult))
466 (constructor
467 PushbufferBytesResult
468 PushbufferBytesRejected
469 (constructor PushbufferErrorCode PushbufferAddressUnaligned))
470 (lambda unrestricted alignedPredecessor : Nat .
471 (lambda unrestricted alignedInduction : (family PushbufferBytesResult) .
472 (nat-eliminate
473 (lambda unrestricted inRange : Nat . (family PushbufferBytesResult))
474 (constructor
475 PushbufferBytesResult
476 PushbufferBytesRejected
477 (constructor PushbufferErrorCode PushbufferAddressOutOfRange))
478 (lambda unrestricted rangePredecessor : Nat .
479 (lambda unrestricted rangeInduction : (family PushbufferBytesResult) .
480 (eliminate
481 ModelWord64
482 (lambda unrestricted currentAddress : (family ModelWord64) .
483 (family PushbufferBytesResult))
484 address
485 (branch
486 ModelWord64Value
487 a0
488 a1
489 a2
490 a3
491 a4
492 a5
493 a6
494 a7
495 .
496 (eliminate
497 ModelWord64
498 (lambda unrestricted currentPayload : (family ModelWord64) .
499 (family PushbufferBytesResult))
500 payload
501 (branch
502 ModelWord64Value
503 p0
504 p1
505 p2
506 p3
507 p4
508 p5
509 p6
510 p7
511 .
512 (constructor
513 PushbufferBytesResult
514 PushbufferBytesReady
515 (bytes-append
516 (bytes 23 32 5 32)
517 (bytes-append
518 (bytes a0 a1 a2 a3)
519 (bytes-append
520 (bytes a4 0 0 0)
521 (bytes-append
522 (bytes p0 p1 p2 p3)
523 (bytes-append (bytes p4 p5 p6 p7) (bytes 1 0 16 3)))))))))))))
524 (pushbufferAddressIn40Bits address))))
525 (pushbufferAddressAligned16 address))))
526
527-- QMDV03/NVC56F release form used by the physically accepted multi-launch
528-- stream. The operation word is explicit because a pre-launch timestamp is
529-- RELEASE|TIMESTAMP (0x02000001), whereas the retiring fence is additionally
530-- RELEASE_WFI (0x02100001). Both carry a 32-bit payload and a zero high word.
531def pushbufferSemaphoreRelease32Operation =
532 (lambda unrestricted address : (family ModelWord64) .
533 (lambda unrestricted payload : (family ModelWord32) .
534 (lambda unrestricted operation : (family ModelWord32) .
535 (nat-eliminate
536 (lambda unrestricted aligned : Nat . (family PushbufferBytesResult))
537 (constructor
538 PushbufferBytesResult
539 PushbufferBytesRejected
540 (constructor PushbufferErrorCode PushbufferAddressUnaligned))
541 (lambda unrestricted alignedPredecessor : Nat .
542 (lambda unrestricted alignedInduction : (family PushbufferBytesResult) .
543 (nat-eliminate
544 (lambda unrestricted inRange : Nat . (family PushbufferBytesResult))
545 (constructor
546 PushbufferBytesResult
547 PushbufferBytesRejected
548 (constructor PushbufferErrorCode PushbufferAddressOutOfRange))
549 (lambda unrestricted rangePredecessor : Nat .
550 (lambda unrestricted rangeInduction : (family PushbufferBytesResult) .
551 (eliminate
552 ModelWord64
553 (lambda unrestricted currentAddress : (family ModelWord64) .
554 (family PushbufferBytesResult))
555 address
556 (branch
557 ModelWord64Value
558 a0
559 a1
560 a2
561 a3
562 a4
563 a5
564 a6
565 a7
566 .
567 (constructor
568 PushbufferBytesResult
569 PushbufferBytesReady
570 (bytes-append
571 -- SEM_EXECUTE belongs to the host subchannel (0),
572 -- while the compute launch methods use subchannel 1.
573 (bytes 23 0 5 32)
574 (bytes-append
575 (bytes a0 a1 a2 a3)
576 (bytes-append
577 (bytes a4 0 0 0)
578 (bytes-append
579 (dataBytesWord32LE payload)
580 (bytes-append (bytes 0 0 0 0) (dataBytesWord32LE operation)))))))))))
581 (pushbufferAddressIn40Bits address))))
582 (pushbufferAddressAligned16 address)))))
583
584def pushbufferBarrier =
585 (constructor PushbufferBytesResult PushbufferBytesReady (bytes 135 32 1 32 20 0 0 0))
586
587def pushbufferPCASLaunch =
588 (lambda unrestricted address : (family ModelWord64) .
589 (nat-eliminate
590 (lambda unrestricted aligned : Nat . (family PushbufferBytesResult))
591 (constructor
592 PushbufferBytesResult
593 PushbufferBytesRejected
594 (constructor PushbufferErrorCode PushbufferQMDAddressUnaligned))
595 (lambda unrestricted alignedPredecessor : Nat .
596 (lambda unrestricted alignedInduction : (family PushbufferBytesResult) .
597 (nat-eliminate
598 (lambda unrestricted inRange : Nat . (family PushbufferBytesResult))
599 (constructor
600 PushbufferBytesResult
601 PushbufferBytesRejected
602 (constructor PushbufferErrorCode PushbufferAddressOutOfRange))
603 (lambda unrestricted rangePredecessor : Nat .
604 (lambda unrestricted rangeInduction : (family PushbufferBytesResult) .
605 (eliminate
606 ModelWord64
607 (lambda unrestricted current : (family ModelWord64) .
608 (family PushbufferBytesResult))
609 address
610 (branch
611 ModelWord64Value
612 b0
613 b1
614 b2
615 b3
616 b4
617 b5
618 b6
619 b7
620 .
621 (constructor
622 PushbufferBytesResult
623 PushbufferBytesReady
624 (bytes 173 32 1 32 b1 b2 b3 b4 176 32 9 128))))))
625 (pushbufferAddressIn40Bits address))))
626 (pushbufferAddressAligned256 address)))
627
628def pushbufferPCASLaunchWithBarrier =
629 (lambda unrestricted address : (family ModelWord64) .
630 (eliminate
631 PushbufferBytesResult
632 (lambda unrestricted current : (family PushbufferBytesResult) .
633 (family PushbufferBytesResult))
634 (pushbufferPCASLaunch address)
635 (branch
636 PushbufferBytesReady
637 launchBytes
638 .
639 (constructor
640 PushbufferBytesResult
641 PushbufferBytesReady
642 (bytes-append launchBytes (bytes 135 32 1 32 20 0 0 0))))
643 (branch
644 PushbufferBytesRejected
645 error
646 .
647 (constructor PushbufferBytesResult PushbufferBytesRejected error))))
648
649-- The accepted QMDV03 batch stream uses an explicit one-dword
650-- SEND_SIGNALING_PCAS2_B method followed by the idle barrier. Keep the older
651-- compact immediate-method owner above stable for its attested callers.
652def pushbufferPCASLaunchV03WithBarrier =
653 (lambda unrestricted address : (family ModelWord64) .
654 (nat-eliminate
655 (lambda unrestricted aligned : Nat . (family PushbufferBytesResult))
656 (constructor
657 PushbufferBytesResult
658 PushbufferBytesRejected
659 (constructor PushbufferErrorCode PushbufferQMDAddressUnaligned))
660 (lambda unrestricted alignedPredecessor : Nat .
661 (lambda unrestricted alignedInduction : (family PushbufferBytesResult) .
662 (nat-eliminate
663 (lambda unrestricted inRange : Nat . (family PushbufferBytesResult))
664 (constructor
665 PushbufferBytesResult
666 PushbufferBytesRejected
667 (constructor PushbufferErrorCode PushbufferAddressOutOfRange))
668 (lambda unrestricted rangePredecessor : Nat .
669 (lambda unrestricted rangeInduction : (family PushbufferBytesResult) .
670 (eliminate
671 ModelWord64
672 (lambda unrestricted current : (family ModelWord64) .
673 (family PushbufferBytesResult))
674 address
675 (branch
676 ModelWord64Value
677 b0
678 b1
679 b2
680 b3
681 b4
682 b5
683 b6
684 b7
685 .
686 (constructor
687 PushbufferBytesResult
688 PushbufferBytesReady
689 (bytes 173 32 1 32 b1 b2 b3 b4 176 32 1 32 3 0 0 0 135 32 1 32 20 0 0 0))))))
690 (pushbufferAddressIn40Bits address))))
691 (pushbufferAddressAligned256 address)))
692
693def pushbufferDwordLengthInRange =
694 (lambda unrestricted dwords : (family ModelWord32) .
695 (eliminate
696 ModelWord32
697 (lambda unrestricted current : (family ModelWord32) . Nat)
698 dwords
699 (branch
700 ModelWord32Value
701 b0
702 b1
703 b2
704 b3
705 .
706 (pushbufferFlagAnd
707 (pushbufferWord32NonZero dwords)
708 (pushbufferFlagAnd
709 (pushbufferByteIsZero b3)
710 (nat-less-than (byte-to-nat b2) (byte-to-nat (byte 32))))))))
711
712def pushbufferGPFIFOEntry =
713 (lambda unrestricted address : (family ModelWord64) .
714 (lambda unrestricted dwords : (family ModelWord32) .
715 (nat-eliminate
716 (lambda unrestricted aligned : Nat . (family PushbufferGPFIFOEntryResult))
717 (constructor
718 PushbufferGPFIFOEntryResult
719 PushbufferGPFIFOEntryRejected
720 (constructor PushbufferErrorCode PushbufferAddressUnaligned))
721 (lambda unrestricted alignedPredecessor : Nat .
722 (lambda unrestricted alignedInduction : (family PushbufferGPFIFOEntryResult) .
723 (nat-eliminate
724 (lambda unrestricted inRange : Nat . (family PushbufferGPFIFOEntryResult))
725 (constructor
726 PushbufferGPFIFOEntryResult
727 PushbufferGPFIFOEntryRejected
728 (constructor PushbufferErrorCode PushbufferAddressOutOfRange))
729 (lambda unrestricted rangePredecessor : Nat .
730 (lambda unrestricted rangeInduction : (family PushbufferGPFIFOEntryResult) .
731 (nat-eliminate
732 (lambda unrestricted lengthValid : Nat . (family PushbufferGPFIFOEntryResult))
733 (constructor
734 PushbufferGPFIFOEntryResult
735 PushbufferGPFIFOEntryRejected
736 (constructor PushbufferErrorCode PushbufferLengthOutOfRange))
737 (lambda unrestricted lengthPredecessor : Nat .
738 (lambda unrestricted lengthInduction : (family PushbufferGPFIFOEntryResult) .
739 (eliminate
740 ModelWord64
741 (lambda unrestricted current : (family ModelWord64) .
742 (family PushbufferGPFIFOEntryResult))
743 address
744 (branch
745 ModelWord64Value
746 b0
747 b1
748 b2
749 b3
750 b4
751 b5
752 b6
753 b7
754 .
755 (constructor
756 PushbufferGPFIFOEntryResult
757 PushbufferGPFIFOEntryReady
758 (constructor
759 ModelWord32
760 ModelWord32Value
761 (byteAnd b0 (byte 252))
762 b1
763 b2
764 b3)
765 (modelWord32Or
766 (constructor
767 ModelWord32
768 ModelWord32Value
769 b4
770 (byte 0)
771 (byte 0)
772 (byte 0))
773 (modelWord32ShiftLeft dwords (byte-to-nat (byte 10)))))))))
774 (pushbufferDwordLengthInRange dwords))))
775 (pushbufferAddressIn40Bits address))))
776 (pushbufferAddressAligned4 address))))
777
778def pushbufferCanAdd63 =
779 (lambda unrestricted value : (family ModelWord32) .
780 (eliminate
781 ModelWord32
782 (lambda unrestricted current : (family ModelWord32) . Nat)
783 value
784 (branch
785 ModelWord32Value
786 b0
787 b1
788 b2
789 b3
790 .
791 (pushbufferIfFlag
792 (nat-less-than (byte-to-nat b3) (byte-to-nat (byte 255)))
793 (succ zero)
794 (pushbufferIfFlag
795 (nat-less-than (byte-to-nat b2) (byte-to-nat (byte 255)))
796 (succ zero)
797 (pushbufferIfFlag
798 (nat-less-than (byte-to-nat b1) (byte-to-nat (byte 255)))
799 (succ zero)
800 (nat-less-than (byte-to-nat b0) (byte-to-nat (byte 193)))))))))
801
802def pushbufferAlignedSegmentDwords =
803 (lambda unrestricted dwords : (family ModelWord32) .
804 (nat-eliminate
805 (lambda unrestricted nonzero : Nat . (family PushbufferAlignedDwordsResult))
806 (constructor
807 PushbufferAlignedDwordsResult
808 PushbufferAlignedDwordsRejected
809 (constructor PushbufferErrorCode PushbufferLengthOutOfRange))
810 (lambda unrestricted nonzeroPredecessor : Nat .
811 (lambda unrestricted nonzeroInduction : (family PushbufferAlignedDwordsResult) .
812 (nat-eliminate
813 (lambda unrestricted noOverflow : Nat . (family PushbufferAlignedDwordsResult))
814 (constructor
815 PushbufferAlignedDwordsResult
816 PushbufferAlignedDwordsRejected
817 (constructor PushbufferErrorCode PushbufferAlignmentOverflow))
818 (lambda unrestricted overflowPredecessor : Nat .
819 (lambda unrestricted overflowInduction : (family PushbufferAlignedDwordsResult) .
820 (constructor
821 PushbufferAlignedDwordsResult
822 PushbufferAlignedDwordsReady
823 (modelWord32And (modelWord32Add dwords 63) 4294967232))))
824 (pushbufferCanAdd63 dwords))))
825 (pushbufferWord32NonZero dwords)))
826
827def pushbufferConstructionErrorBytes =
828 (lambda unrestricted error : (family PushbufferConstructionError) .
829 (eliminate
830 PushbufferConstructionError
831 (lambda unrestricted current : (family PushbufferConstructionError) . Bytes)
832 error
833 (branch PushbufferInlineQMDLengthMismatch . b"ALPHA-HPBC-201")
834 (branch PushbufferComputeConfigurationMismatch . b"ALPHA-HPBC-202")
835 (branch PushbufferConstructionIdentityMalformed . b"ALPHA-HPBC-203")
836 (branch PushbufferConstructionRejected cause . (pushbufferErrorCodeBytes cause))))
837
838def pushbufferInlineLaunch =
839 (lambda unrestricted stagingAddress : (family ModelWord64) .
840 (lambda unrestricted descriptor : (family PushbufferDwordList) .
841 (nat-eliminate
842 (lambda unrestricted aligned : Nat . (family PushbufferBytesResult))
843 (constructor
844 PushbufferBytesResult
845 PushbufferBytesRejected
846 (constructor PushbufferErrorCode PushbufferQMDAddressUnaligned))
847 (lambda unrestricted alignedPredecessor : Nat .
848 (lambda unrestricted alignedInduction : (family PushbufferBytesResult) .
849 (nat-eliminate
850 (lambda unrestricted descriptorLength : Nat . (family PushbufferBytesResult))
851 (constructor
852 PushbufferBytesResult
853 PushbufferBytesRejected
854 (constructor PushbufferErrorCode PushbufferLengthOutOfRange))
855 (lambda unrestricted lengthPredecessor : Nat .
856 (lambda unrestricted lengthInduction : (family PushbufferBytesResult) .
857 (eliminate
858 ModelWord64
859 (lambda unrestricted current : (family ModelWord64) .
860 (family PushbufferBytesResult))
861 stagingAddress
862 (branch
863 ModelWord64Value
864 b0
865 b1
866 b2
867 b3
868 b4
869 b5
870 b6
871 b7
872 .
873 (constructor
874 PushbufferBytesResult
875 PushbufferBytesReady
876 (bytes-append
877 (bytes 198 32 66 32 b5 b6 b7 0 b1 b2 b3 b4)
878 (pushbufferEncodeDwords descriptor)))))))
879 (naturalEqual (pushbufferDwordCount descriptor) (byte-to-nat (byte 64))))))
880 (pushbufferAddressAligned256 stagingAddress))))
881
882def pushbufferAddressIn49Bits =
883 (lambda unrestricted address : (family ModelWord64) .
884 (eliminate
885 ModelWord64
886 (lambda unrestricted current : (family ModelWord64) . Nat)
887 address
888 (branch
889 ModelWord64Value
890 b0
891 b1
892 b2
893 b3
894 b4
895 b5
896 b6
897 b7
898 .
899 (pushbufferFlagAnd
900 (byte-equal b7 (byte 0))
901 (nat-less-than (byte-to-nat b6) (byte-to-nat (byte 2)))))))
902
903def pushbufferExtentIn40Bits =
904 (lambda unrestricted extent : (family ModelWord64) .
905 (eliminate
906 ModelWord64
907 (lambda unrestricted current : (family ModelWord64) . Nat)
908 extent
909 (branch
910 ModelWord64Value
911 b0
912 b1
913 b2
914 b3
915 b4
916 b5
917 b6
918 b7
919 .
920 (pushbufferFlagAnd
921 (pushbufferWord32NonZero (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3))
922 (pushbufferFlagAnd
923 (byte-equal b5 (byte 0))
924 (pushbufferFlagAnd (byte-equal b6 (byte 0)) (byte-equal b7 (byte 0))))))))
925
926def pushbufferComputeArchitecturePairValid =
927 (lambda unrestricted class : (family ModelWord32) .
928 (lambda unrestricted spa : (family ModelWord32) .
929 (naturalOr
930 (naturalAnd
931 (bytes-equal (dataBytesWord32LE class) (bytes 192 199 0 0))
932 (bytes-equal (dataBytesWord32LE spa) (bytes 6 8 0 0)))
933 (naturalAnd
934 (bytes-equal (dataBytesWord32LE class) (bytes 192 201 0 0))
935 (bytes-equal (dataBytesWord32LE spa) (bytes 9 8 0 0))))))
936
937def pushbufferComputeConfigValid =
938 (lambda unrestricted config : (family PushbufferComputeConfig) .
939 (eliminate
940 PushbufferComputeConfig
941 (lambda unrestricted current : (family PushbufferComputeConfig) . Nat)
942 config
943 (branch
944 PushbufferComputeConfigValue
945 class
946 shared
947 local
948 localBytes
949 localWindow
950 smCount
951 spa
952 .
953 (naturalAnd
954 (pushbufferComputeArchitecturePairValid class spa)
955 (naturalAnd
956 (bytes-equal (dataBytesWord64LE shared) (bytes 0 0 0 254 0 0 0 0))
957 (naturalAnd
958 (bytes-equal (dataBytesWord64LE localWindow) (bytes 0 0 0 255 0 0 0 0))
959 (naturalAnd
960 (pushbufferAddressIn49Bits local)
961 (naturalAnd
962 (pushbufferExtentIn40Bits localBytes)
963 (naturalAnd
964 (naturalAnd
965 (pushbufferWord32NonZero smCount)
966 (nat-less-than
967 (modelWord32ToNatural smCount)
968 (naturalPowerOfTwo (byte-to-nat (byte 9)))))
969 1)))))))))
970
971def pushbufferReferenceCounterBytes =
972 (lambda unrestricted count : Nat .
973 (nat-eliminate
974 (lambda unrestricted current : Nat . Bytes)
975 b""
976 (lambda unrestricted predecessor : Nat .
977 (lambda unrestricted induction : Bytes .
978 (bytes-append (bytes 146 32 1 32 (nat-to-byte predecessor) 160 8 0) induction)))
979 count))
980
981def pushbufferComputeInitializationBytes =
982 (lambda unrestricted config : (family PushbufferComputeConfig) .
983 (eliminate
984 PushbufferComputeConfig
985 (lambda unrestricted current : (family PushbufferComputeConfig) . Bytes)
986 config
987 (branch
988 PushbufferComputeConfigValue
989 class
990 shared
991 local
992 localBytes
993 localWindow
994 smCount
995 spa
996 .
997 (eliminate
998 ModelWord64
999 (lambda unrestricted currentShared : (family ModelWord64) . Bytes)
1000 shared
1001 (branch
1002 ModelWord64Value
1003 s0
1004 s1
1005 s2
1006 s3
1007 s4
1008 s5
1009 s6
1010 s7
1011 .
1012 (eliminate
1013 ModelWord64
1014 (lambda unrestricted currentLocal : (family ModelWord64) . Bytes)
1015 local
1016 (branch
1017 ModelWord64Value
1018 l0
1019 l1
1020 l2
1021 l3
1022 l4
1023 l5
1024 l6
1025 l7
1026 .
1027 (eliminate
1028 ModelWord64
1029 (lambda unrestricted currentBytes : (family ModelWord64) . Bytes)
1030 localBytes
1031 (branch
1032 ModelWord64Value
1033 z0
1034 z1
1035 z2
1036 z3
1037 z4
1038 z5
1039 z6
1040 z7
1041 .
1042 (eliminate
1043 ModelWord64
1044 (lambda unrestricted currentWindow : (family ModelWord64) . Bytes)
1045 localWindow
1046 (branch
1047 ModelWord64Value
1048 w0
1049 w1
1050 w2
1051 w3
1052 w4
1053 w5
1054 w6
1055 w7
1056 .
1057 (bytes-append
1058 (bytes 0 32 1 32)
1059 (bytes-append
1060 (dataBytesWord32LE class)
1061 (bytes-append
1062 (bytes 64 32 1 32 0 0 0 0)
1063 (bytes-append
1064 (bytes 168 32 2 32 s4 s5 s6 s7 s0 s1 s2 s3)
1065 (bytes-append
1066 (bytes 228 33 2 32 l4 l5 (byteAnd l6 (byte 1)) 0 l0 l1 l2 l3)
1067 (bytes-append
1068 (bytes 236 33 2 32 w4 w5 (byteAnd w6 (byte 1)) 0 w0 w1 w2 w3)
1069 (bytes-append
1070 (bytes 185 32 3 32 z4 0 0 0 z0 z1 z2 z3)
1071 (bytes-append
1072 (dataBytesWord32LE smCount)
1073 (bytes-append
1074 (bytes 196 32 1 32)
1075 (bytes-append
1076 (dataBytesWord32LE spa)
1077 (pushbufferReferenceCounterBytes (byte-to-nat (byte 64))))))))))))))))))))))))
1078
1079def pushbufferReferenceCounterBytesAscendingFrom =
1080 (lambda unrestricted count : Nat .
1081 (nat-eliminate
1082 (lambda unrestricted current : Nat . (pi unrestricted start : Nat . Bytes))
1083 (lambda unrestricted start : Nat . b"")
1084 (lambda unrestricted predecessor : Nat .
1085 (lambda unrestricted induction : (pi unrestricted start : Nat . Bytes) .
1086 (lambda unrestricted start : Nat .
1087 (bytes-append (bytes 146 32 1 32 (nat-to-byte start) 160 8 0) (induction (succ start))))))
1088 count))
1089
1090def pushbufferReferenceCounterBytesAscending =
1091 (lambda unrestricted count : Nat . (pushbufferReferenceCounterBytesAscendingFrom count zero))
1092
1093-- Exact QMDV03 compute initialization used by the accepted Coppelius channel.
1094-- In particular it writes the SPA version before the windows, emits the
1095-- 64 CWD reference counters in ascending order, and invalidates the shader
1096-- cache with value one. The older owner above remains byte-stable.
1097def pushbufferComputeInitializationV03Bytes =
1098 (lambda unrestricted config : (family PushbufferComputeConfig) .
1099 (eliminate
1100 PushbufferComputeConfig
1101 (lambda unrestricted current : (family PushbufferComputeConfig) . Bytes)
1102 config
1103 (branch
1104 PushbufferComputeConfigValue
1105 class
1106 shared
1107 local
1108 localBytes
1109 localWindow
1110 smCount
1111 spa
1112 .
1113 (eliminate
1114 ModelWord64
1115 (lambda unrestricted currentShared : (family ModelWord64) . Bytes)
1116 shared
1117 (branch
1118 ModelWord64Value
1119 s0
1120 s1
1121 s2
1122 s3
1123 s4
1124 s5
1125 s6
1126 s7
1127 .
1128 (eliminate
1129 ModelWord64
1130 (lambda unrestricted currentLocal : (family ModelWord64) . Bytes)
1131 local
1132 (branch
1133 ModelWord64Value
1134 l0
1135 l1
1136 l2
1137 l3
1138 l4
1139 l5
1140 l6
1141 l7
1142 .
1143 (eliminate
1144 ModelWord64
1145 (lambda unrestricted currentBytes : (family ModelWord64) . Bytes)
1146 localBytes
1147 (branch
1148 ModelWord64Value
1149 z0
1150 z1
1151 z2
1152 z3
1153 z4
1154 z5
1155 z6
1156 z7
1157 .
1158 (eliminate
1159 ModelWord64
1160 (lambda unrestricted currentWindow : (family ModelWord64) . Bytes)
1161 localWindow
1162 (branch
1163 ModelWord64Value
1164 w0
1165 w1
1166 w2
1167 w3
1168 w4
1169 w5
1170 w6
1171 w7
1172 .
1173 (bytes-append
1174 (bytes 0 32 1 32)
1175 (bytes-append
1176 (dataBytesWord32LE class)
1177 (bytes-append
1178 (bytes 196 32 1 32)
1179 (bytes-append
1180 (dataBytesWord32LE spa)
1181 (bytes-append
1182 (bytes 168 32 2 32 s4 s5 s6 s7 s0 s1 s2 s3)
1183 (bytes-append
1184 (bytes 228 33 2 32 l4 l5 (byteAnd l6 (byte 1)) 0 l0 l1 l2 l3)
1185 (bytes-append
1186 (bytes 236 33 2 32 w4 w5 (byteAnd w6 (byte 1)) 0 w0 w1 w2 w3)
1187 (bytes-append
1188 (bytes 185 32 1 32 z0 z1 z2 z3)
1189 (bytes-append
1190 (pushbufferReferenceCounterBytesAscending
1191 (byte-to-nat (byte 64)))
1192 (bytes 135 32 1 32 1 0 0 0)))))))))))))))))))))
1193
1194def pushbufferBuildComputeInitialization =
1195 (lambda unrestricted identity : Bytes .
1196 (lambda unrestricted config : (family PushbufferComputeConfig) .
1197 (nat-eliminate
1198 (lambda unrestricted identityValid : Nat . (family PushbufferConstructionResult))
1199 (constructor
1200 PushbufferConstructionResult
1201 PushbufferConstructionFailed
1202 (constructor PushbufferConstructionError PushbufferConstructionIdentityMalformed))
1203 (lambda unrestricted identityPredecessor : Nat .
1204 (lambda unrestricted identityInduction : (family PushbufferConstructionResult) .
1205 (nat-eliminate
1206 (lambda unrestricted configValid : Nat . (family PushbufferConstructionResult))
1207 (constructor
1208 PushbufferConstructionResult
1209 PushbufferConstructionFailed
1210 (constructor PushbufferConstructionError PushbufferComputeConfigurationMismatch))
1211 (lambda unrestricted configPredecessor : Nat .
1212 (lambda unrestricted configInduction : (family PushbufferConstructionResult) .
1213 (app
1214 (lambda unrestricted encoded : Bytes .
1215 (constructor
1216 PushbufferConstructionResult
1217 PushbufferConstructionReady
1218 (constructor
1219 PushbufferConstructionReceipt
1220 PushbufferConstructionReceiptValue
1221 identity
1222 encoded
1223 (naturalDivideUnchecked (bytes-length encoded) (byte-to-nat (byte 4)))
1224 zero)))
1225 (pushbufferComputeInitializationBytes config))))
1226 (pushbufferComputeConfigValid config))))
1227 (naturalEqual (bytes-length identity) (byte-to-nat (byte 64))))))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.