1module Hardware.Nvidia.SM86.Command.QMD
2
3import Accelerator.SM86.QMD
4import Model.Word32
5import Model.Word32Logic
6import Model.Word64
7import Std.Byte
8import Std.Natural
9import Model.Config
10import Model.Parameter
11
12family QMDErrorCode : Type 0
13constructor QMDProgramAddressOutOfRange
14constructor QMDScratchAddressOutOfRange
15constructor QMDGridDimensionZero
16constructor QMDGridYZOutOfRange
17constructor QMDBlockDimensionZero
18constructor QMDBlockDimensionOutOfRange
19constructor QMDBlockVolumeOutOfRange
20constructor QMDProgramBytesZero
21constructor QMDSharedMemoryOutOfRange
22constructor QMDRegisterCountOutOfRange
23constructor QMDPrefetchUnitsOutOfRange
24constructor QMDConstantBufferAddressOutOfRange
25constructor QMDConstantBufferSizeOutOfRange
26
27end-family
28
29family QMDOptionalScratch : Type 0
30constructor QMDNoScratch
31constructor QMDScratch
32field unrestricted qmdScratchAddress : (family ModelWord64)
33
34end-family
35
36-- QMD V03 constant-buffer binding. This is deliberately separate from the
37-- historical OptionalScratch input above: the old owner encoded the address
38-- and INVALIDATE bit but did not set CONSTANT_BUFFER_VALID(0), and fixed the
39-- size to 64 KiB. Maintained callers that need a real parameter bank use this
40-- explicit address-and-extent contract; the historical API remains stable.
41family QMDOptionalConstantBuffer : Type 0
42constructor QMDNoConstantBuffer
43constructor QMDConstantBuffer
44field unrestricted qmdConstantBufferAddress : (family ModelWord64)
45field unrestricted qmdConstantBufferBytes : (family ModelWord32)
46
47end-family
48
49family QMDConfig : Type 0
50constructor QMDConfigValue
51field unrestricted qmdProgramAddress : (family ModelWord64)
52field unrestricted qmdProgramBytes : (family ModelWord32)
53field unrestricted qmdPrefetchUnits : (family ModelWord32)
54field unrestricted qmdGridX : (family ModelWord32)
55field unrestricted qmdGridY : (family ModelWord32)
56field unrestricted qmdGridZ : (family ModelWord32)
57field unrestricted qmdBlockX : (family ModelWord32)
58field unrestricted qmdBlockY : (family ModelWord32)
59field unrestricted qmdBlockZ : (family ModelWord32)
60field unrestricted qmdSharedBytes : (family ModelWord32)
61field unrestricted qmdRegisterCount : (family ModelWord32)
62field unrestricted qmdOptionalScratch : (family QMDOptionalScratch)
63
64end-family
65
66family QMDValidationResult : Type 0
67constructor QMDValidated
68constructor QMDRejected
69field unrestricted qmdValidationError : (family QMDErrorCode)
70
71end-family
72
73family QMDConstantFields : Type 0
74constructor QMDConstantFieldsValue
75field unrestricted qmdConstantEnable : (family ModelWord32)
76field unrestricted qmdConstantLow : (family ModelWord32)
77field unrestricted qmdConstantHigh : (family ModelWord32)
78
79end-family
80
81family QMDBuildResult : Type 0
82constructor QMDBuilt
83field unrestricted qmdEndodedBytes : Bytes
84field unrestricted qmdEncodedDwords : Nat
85field unrestricted qmdEncodedAlignment : Nat
86field unrestricted qmdHostFallbacks : Nat
87constructor QMDBuildRejected
88field unrestricted qmdBuildError : (family QMDErrorCode)
89
90end-family
91
92family QMDIdentityBinding : Type 0
93constructor QMDIdentityBindingValue
94field unrestricted qmdProgramIdentity : Bytes
95field unrestricted qmdResourceIdentity : Bytes
96field unrestricted qmdConstantIdentity : Bytes
97
98end-family
99
100family QMDAttestationError : Type 0
101constructor QMDPrefetchGeometryMismatch
102constructor QMDEncodingExtentMismatch
103constructor QMDIdentityMalformed
104constructor QMDIdentityMismatch
105constructor QMDEncodingRejected
106field unrestricted qmdEncodingRejectedError : (family QMDErrorCode)
107
108end-family
109
110family QMDAttestedReceipt : Type 0
111constructor QMDAttestedReceiptValue
112field unrestricted qmdAttestedBytes : Bytes
113field unrestricted qmdAttestedBinding : (family QMDIdentityBinding)
114field unrestricted qmdAttestedDwords : Nat
115field unrestricted qmdAttestedAlignment : Nat
116field unrestricted qmdAttestedHostFallbacks : Nat
117
118end-family
119
120family QMDAttestedResult : Type 0
121constructor QMDAttested
122field unrestricted qmdAttestedReceiptValue : (family QMDAttestedReceipt)
123constructor QMDAttestationRejected
124field unrestricted qmdAttestationFailure : (family QMDAttestationError)
125
126end-family
127
128-- Field projection (fields do not create definitions).
129def qmdRegisterCount =
130 (lambda unrestricted value : (family QMDConfig) .
131 (eliminate
132 QMDConfig
133 (lambda unrestricted current : (family QMDConfig) . (family ModelWord32))
134 value
135 (branch
136 QMDConfigValue
137 hermesQMDProgramAddress
138 hermesQMDProgramBytes
139 hermesQMDPrefetchUnits
140 hermesQMDGridX
141 hermesQMDGridY
142 hermesQMDGridZ
143 hermesQMDBlockX
144 hermesQMDBlockY
145 hermesQMDBlockZ
146 hermesQMDSharedBytes
147 hermesQMDRegisterCountField
148 hermesQMDOptionalScratch
149 .
150 hermesQMDRegisterCountField)))
151
152-- Field projection (fields do not create definitions).
153def qmdSharedBytes =
154 (lambda unrestricted value : (family QMDConfig) .
155 (eliminate
156 QMDConfig
157 (lambda unrestricted current : (family QMDConfig) . (family ModelWord32))
158 value
159 (branch
160 QMDConfigValue
161 hermesQMDProgramAddress
162 hermesQMDProgramBytes
163 hermesQMDPrefetchUnits
164 hermesQMDGridX
165 hermesQMDGridY
166 hermesQMDGridZ
167 hermesQMDBlockX
168 hermesQMDBlockY
169 hermesQMDBlockZ
170 hermesQMDSharedBytesField
171 hermesQMDRegisterCount
172 hermesQMDOptionalScratch
173 .
174 hermesQMDSharedBytesField)))
175
176def qmdErrorCodeBytes =
177 (lambda unrestricted code : (family QMDErrorCode) .
178 (eliminate
179 QMDErrorCode
180 (lambda unrestricted current : (family QMDErrorCode) . Bytes)
181 code
182 (branch QMDProgramAddressOutOfRange . b"ALPHA-HQMD-501")
183 (branch QMDScratchAddressOutOfRange . b"ALPHA-HQMD-502")
184 (branch QMDGridDimensionZero . b"ALPHA-HQMD-503")
185 (branch QMDGridYZOutOfRange . b"ALPHA-HQMD-504")
186 (branch QMDBlockDimensionZero . b"ALPHA-HQMD-505")
187 (branch QMDBlockDimensionOutOfRange . b"ALPHA-HQMD-506")
188 (branch QMDBlockVolumeOutOfRange . b"ALPHA-HQMD-507")
189 (branch QMDProgramBytesZero . b"ALPHA-HQMD-508")
190 (branch QMDSharedMemoryOutOfRange . b"ALPHA-HQMD-509")
191 (branch QMDRegisterCountOutOfRange . b"ALPHA-HQMD-510")
192 (branch QMDPrefetchUnitsOutOfRange . b"ALPHA-HQMD-511")
193 (branch QMDConstantBufferAddressOutOfRange . b"ALPHA-HQMD-512")
194 (branch QMDConstantBufferSizeOutOfRange . b"ALPHA-HQMD-513")))
195
196def qmdFlagAnd =
197 (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (naturalAnd left right)))
198
199def qmdWord32Positive =
200 (lambda unrestricted value : (family ModelWord32) .
201 (nat-less-than zero (modelWord32ToNatural value)))
202
203def qmdWord32AtMost =
204 (lambda unrestricted value : (family ModelWord32) .
205 (lambda unrestricted limit : Nat . (nat-less-than (modelWord32ToNatural value) (succ limit))))
206
207def qmdAddress49 =
208 (lambda unrestricted address : (family ModelWord64) .
209 (eliminate
210 ModelWord64
211 (lambda unrestricted current : (family ModelWord64) . Nat)
212 address
213 (branch
214 ModelWord64Value
215 b0
216 b1
217 b2
218 b3
219 b4
220 b5
221 b6
222 b7
223 .
224 (qmdFlagAnd
225 (byte-equal b7 (byte 0))
226 (nat-less-than (byte-to-nat b6) (byte-to-nat (byte 2)))))))
227
228def qmdScratchAddressValid =
229 (lambda unrestricted scratch : (family QMDOptionalScratch) .
230 (eliminate
231 QMDOptionalScratch
232 (lambda unrestricted current : (family QMDOptionalScratch) . Nat)
233 scratch
234 (branch QMDNoScratch . (succ zero))
235 (branch QMDScratch address . (qmdAddress49 address))))
236
237def qmdThreePositive =
238 (lambda unrestricted first : (family ModelWord32) .
239 (lambda unrestricted second : (family ModelWord32) .
240 (lambda unrestricted third : (family ModelWord32) .
241 (qmdFlagAnd
242 (qmdWord32Positive first)
243 (qmdFlagAnd (qmdWord32Positive second) (qmdWord32Positive third))))))
244
245def qmdThreeAtMost =
246 (lambda unrestricted first : (family ModelWord32) .
247 (lambda unrestricted second : (family ModelWord32) .
248 (lambda unrestricted third : (family ModelWord32) .
249 (lambda unrestricted limit : Nat .
250 (qmdFlagAnd
251 (qmdWord32AtMost first limit)
252 (qmdFlagAnd (qmdWord32AtMost second limit) (qmdWord32AtMost third limit)))))))
253
254def qmdBlockVolume =
255 (lambda unrestricted blockX : (family ModelWord32) .
256 (lambda unrestricted blockY : (family ModelWord32) .
257 (lambda unrestricted blockZ : (family ModelWord32) .
258 (naturalMultiply
259 (modelWord32ToNatural blockX)
260 (naturalMultiply (modelWord32ToNatural blockY) (modelWord32ToNatural blockZ))))))
261
262def qmdRoundedSharedBytes =
263 (lambda unrestricted shared : (family ModelWord32) .
264 (modelWord32ShiftLeft
265 (modelWord32ShiftRight (modelWord32Add shared 255) (byte-to-nat (byte 8)))
266 (byte-to-nat (byte 8))))
267
268def qmdSharedMemoryValid =
269 (lambda unrestricted shared : (family ModelWord32) .
270 (nat-less-than
271 (modelWord32ToNatural (qmdRoundedSharedBytes shared))
272 (succ (naturalMultiply (byte-to-nat (byte 99)) (naturalPowerOfTwo (byte-to-nat (byte 10)))))))
273
274def qmdRequire =
275 (lambda unrestricted condition : Nat .
276 (lambda unrestricted error : (family QMDErrorCode) .
277 (lambda unrestricted success : (family QMDValidationResult) .
278 (nat-eliminate
279 (lambda unrestricted current : Nat . (family QMDValidationResult))
280 (constructor QMDValidationResult QMDRejected error)
281 (lambda unrestricted predecessor : Nat .
282 (lambda unrestricted induction : (family QMDValidationResult) . success))
283 condition))))
284
285def qmdValidate =
286 (lambda unrestricted config : (family QMDConfig) .
287 (eliminate
288 QMDConfig
289 (lambda unrestricted current : (family QMDConfig) . (family QMDValidationResult))
290 config
291 (branch
292 QMDConfigValue
293 programAddress
294 programBytes
295 prefetchUnits
296 gridX
297 gridY
298 gridZ
299 blockX
300 blockY
301 blockZ
302 shared
303 registers
304 scratch
305 .
306 (qmdRequire
307 (qmdAddress49 programAddress)
308 (constructor QMDErrorCode QMDProgramAddressOutOfRange)
309 (qmdRequire
310 (qmdScratchAddressValid scratch)
311 (constructor QMDErrorCode QMDScratchAddressOutOfRange)
312 (qmdRequire
313 (qmdThreePositive gridX gridY gridZ)
314 (constructor QMDErrorCode QMDGridDimensionZero)
315 (qmdRequire
316 (qmdFlagAnd
317 (qmdWord32AtMost
318 gridY
319 (naturalSaturatingSubtract
320 (naturalPowerOfTwo (byte-to-nat (byte 16)))
321 (succ zero)))
322 (qmdWord32AtMost
323 gridZ
324 (naturalSaturatingSubtract
325 (naturalPowerOfTwo (byte-to-nat (byte 16)))
326 (succ zero))))
327 (constructor QMDErrorCode QMDGridYZOutOfRange)
328 (qmdRequire
329 (qmdThreePositive blockX blockY blockZ)
330 (constructor QMDErrorCode QMDBlockDimensionZero)
331 (qmdRequire
332 (qmdThreeAtMost
333 blockX
334 blockY
335 blockZ
336 (naturalSaturatingSubtract
337 (naturalPowerOfTwo (byte-to-nat (byte 16)))
338 (succ zero)))
339 (constructor QMDErrorCode QMDBlockDimensionOutOfRange)
340 (qmdRequire
341 (nat-less-than
342 (qmdBlockVolume blockX blockY blockZ)
343 (succ (naturalPowerOfTwo (byte-to-nat (byte 10)))))
344 (constructor QMDErrorCode QMDBlockVolumeOutOfRange)
345 (qmdRequire
346 (qmdWord32Positive programBytes)
347 (constructor QMDErrorCode QMDProgramBytesZero)
348 (qmdRequire
349 (qmdSharedMemoryValid shared)
350 (constructor QMDErrorCode QMDSharedMemoryOutOfRange)
351 (qmdRequire
352 (qmdFlagAnd
353 (qmdWord32Positive registers)
354 (qmdWord32AtMost registers (byte-to-nat (byte 255))))
355 (constructor QMDErrorCode QMDRegisterCountOutOfRange)
356 (qmdRequire
357 (qmdFlagAnd
358 (qmdWord32Positive prefetchUnits)
359 (qmdWord32AtMost
360 prefetchUnits
361 (naturalSaturatingSubtract
362 (naturalPowerOfTwo (byte-to-nat (byte 9)))
363 (succ zero))))
364 (constructor QMDErrorCode QMDPrefetchUnitsOutOfRange)
365 (constructor QMDValidationResult QMDValidated)))))))))))))))
366
367def qmdPhysicalWord =
368 (lambda unrestricted value : (family ModelWord32) .
369 (eliminate
370 ModelWord32
371 (lambda unrestricted current : (family ModelWord32) . (family SM86QMDWord32))
372 value
373 (branch
374 ModelWord32Value
375 b0
376 b1
377 b2
378 b3
379 .
380 (constructor SM86QMDWord32 SM86QMDWord32Value b0 b1 b2 b3))))
381
382def qmdProgramAddressLow =
383 (lambda unrestricted address : (family ModelWord64) .
384 (eliminate
385 ModelWord64
386 (lambda unrestricted current : (family ModelWord64) . (family ModelWord32))
387 address
388 (branch
389 ModelWord64Value
390 b0
391 b1
392 b2
393 b3
394 b4
395 b5
396 b6
397 b7
398 .
399 (constructor ModelWord32 ModelWord32Value b0 b1 b2 b3))))
400
401def qmdProgramAddressHigh =
402 (lambda unrestricted address : (family ModelWord64) .
403 (eliminate
404 ModelWord64
405 (lambda unrestricted current : (family ModelWord64) . (family ModelWord32))
406 address
407 (branch
408 ModelWord64Value
409 b0
410 b1
411 b2
412 b3
413 b4
414 b5
415 b6
416 b7
417 .
418 (constructor ModelWord32 ModelWord32Value b4 b5 (byteAnd b6 (byte 1)) (byte 0)))))
419
420def qmdPrefetchBaseShifted =
421 (lambda unrestricted address : (family ModelWord64) .
422 (eliminate
423 ModelWord64
424 (lambda unrestricted current : (family ModelWord64) . (family ModelWord32))
425 address
426 (branch
427 ModelWord64Value
428 b0
429 b1
430 b2
431 b3
432 b4
433 b5
434 b6
435 b7
436 .
437 (constructor ModelWord32 ModelWord32Value b1 b2 b3 b4))))
438
439def qmdPrefetchHigh =
440 (lambda unrestricted address : (family ModelWord64) .
441 (eliminate
442 ModelWord64
443 (lambda unrestricted current : (family ModelWord64) . (family ModelWord32))
444 address
445 (branch
446 ModelWord64Value
447 b0
448 b1
449 b2
450 b3
451 b4
452 b5
453 b6
454 b7
455 .
456 (constructor ModelWord32 ModelWord32Value b5 (byteAnd b6 (byte 1)) (byte 0) (byte 0)))))
457
458def qmdConstantFieldsForScratch =
459 (lambda unrestricted scratch : (family QMDOptionalScratch) .
460 (eliminate
461 QMDOptionalScratch
462 (lambda unrestricted current : (family QMDOptionalScratch) . (family QMDConstantFields))
463 scratch
464 (branch QMDNoScratch . (constructor QMDConstantFields QMDConstantFieldsValue 0 0 0))
465 (branch
466 QMDScratch
467 address
468 .
469 (constructor
470 QMDConstantFields
471 QMDConstantFieldsValue
472 1
473 (qmdProgramAddressLow address)
474 (modelWord32Or (qmdProgramAddressHigh address) 2147745792)))))
475
476def qmdConstantBufferAddressValid =
477 (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
478 (eliminate
479 QMDOptionalConstantBuffer
480 (lambda unrestricted current : (family QMDOptionalConstantBuffer) . Nat)
481 constantBuffer
482 (branch QMDNoConstantBuffer . (succ zero))
483 (branch QMDConstantBuffer address extent . (qmdAddress49 address))))
484
485-- Constant bank 0 as an SM86 kernel sees it: the driver's words below the
486-- parameters (the block's X extent at 0), the kernel's parameters from
487-- 0x160. A launch's parameter block is laid out against these.
488def qmdBlockDimensionXOffset : Nat = 0
489def qmdKernelParameterBase : Nat = 0x160
490
491-- one launch record in a QMD table
492def qmdRecordBytes : Nat = 256
493
494def qmdConstantBufferMaximumBytes : Nat =
495 (naturalMultiply
496 (naturalSaturatingSubtract (naturalPowerOfTwo (byte-to-nat (byte 13))) (succ zero))
497 (byte-to-nat (byte 16)))
498
499def qmdConstantBufferSizeValid =
500 (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
501 (eliminate
502 QMDOptionalConstantBuffer
503 (lambda unrestricted current : (family QMDOptionalConstantBuffer) . Nat)
504 constantBuffer
505 (branch QMDNoConstantBuffer . (succ zero))
506 (branch
507 QMDConstantBuffer
508 address
509 extent
510 .
511 (qmdFlagAnd
512 (qmdWord32Positive extent)
513 (qmdWord32AtMost extent qmdConstantBufferMaximumBytes)))))
514
515-- QMDV03_00 slot zero:
516-- dword 32 = ADDRESS_LOWER
517-- dword 33 bits 0..16 = ADDRESS_UPPER, bit 18 = INVALIDATE,
518-- bits 19..31 = ceil(bytes / 16)
519-- dword 20 bit 0 = CONSTANT_BUFFER_VALID(0)
520def qmdConstantFieldsForBuffer =
521 (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
522 (eliminate
523 QMDOptionalConstantBuffer
524 (lambda unrestricted current : (family QMDOptionalConstantBuffer) .
525 (family QMDConstantFields))
526 constantBuffer
527 (branch QMDNoConstantBuffer . (constructor QMDConstantFields QMDConstantFieldsValue 0 0 0))
528 (branch
529 QMDConstantBuffer
530 address
531 extent
532 .
533 (constructor
534 QMDConstantFields
535 QMDConstantFieldsValue
536 1
537 (qmdProgramAddressLow address)
538 (modelWord32Or
539 (qmdProgramAddressHigh address)
540 (modelWord32Or
541 262144
542 (modelWord32ShiftLeft
543 (modelWord32ShiftRight (modelWord32Add extent 15) (byte-to-nat (byte 4)))
544 (byte-to-nat (byte 19)))))))))
545
546def qmdSharedField =
547 (lambda unrestricted shared : (family ModelWord32) .
548 (modelWord32Or (modelWord32Add (qmdRoundedSharedBytes shared) 1024) 879230976))
549
550def qmdBlockXField =
551 (lambda unrestricted blockX : (family ModelWord32) .
552 (modelWord32Or (modelWord32ShiftLeft blockX (byte-to-nat (byte 16))) 48))
553
554def qmdBlockYZField =
555 (lambda unrestricted blockY : (family ModelWord32) .
556 (lambda unrestricted blockZ : (family ModelWord32) .
557 (modelWord32Or blockY (modelWord32ShiftLeft blockZ (byte-to-nat (byte 16))))))
558
559-- The register field holds the allocation, not the program's count: the
560-- registers the program names and the two per-thread registers the hardware
561-- reserves (Accelerator.SM86.Operands.sm86ReservedRegisters), in units of
562-- eight, as the sm_121 QMD's. A raw count that is not a multiple of eight
563-- leaves the program's highest registers outside the allocated granule:
564-- Xid 13 on the RTX 3090 (the tiled product's 164, 2026-09-27).
565def qmdAllocatedRegisters =
566 (lambda unrestricted registers : (family ModelWord32) .
567 (modelWord32ShiftLeft
568 (modelWord32ShiftRight (modelWord32Add registers 9) (byte-to-nat (byte 3)))
569 (byte-to-nat (byte 3))))
570
571def qmdRegisterField =
572 (lambda unrestricted registers : (family ModelWord32) .
573 (lambda unrestricted constantEnable : (family ModelWord32) .
574 (modelWord32Or
575 constantEnable
576 (modelWord32Or (modelWord32ShiftLeft (qmdAllocatedRegisters registers) (byte-to-nat (byte 8))) 3407872))))
577
578def qmdPrefetchControl =
579 (lambda unrestricted address : (family ModelWord64) .
580 (lambda unrestricted units : (family ModelWord32) .
581 (modelWord32Or
582 (qmdPrefetchHigh address)
583 (modelWord32Or (modelWord32ShiftLeft units (byte-to-nat (byte 9))) 2248146944))))
584
585-- QMD v03 is shared by SM86 and SM89. The upper byte of this word is the
586-- target SASS architecture tag; keep it explicit for compatible binaries
587-- launched through a different compute class.
588def qmdPrefetchControlForArchitecture =
589 (lambda unrestricted architecture : (family ModelWord32) .
590 (lambda unrestricted address : (family ModelWord64) .
591 (lambda unrestricted units : (family ModelWord32) .
592 (modelWord32Or
593 (qmdPrefetchHigh address)
594 (modelWord32Or
595 (modelWord32ShiftLeft units (byte-to-nat (byte 9)))
596 (modelWord32ShiftLeft architecture (byte-to-nat (byte 24))))))))
597
598def qmdBuildPhysicalConfig =
599 (lambda unrestricted config : (family QMDConfig) .
600 (eliminate
601 QMDConfig
602 (lambda unrestricted current : (family QMDConfig) . (family SM86QMDPhysicalConfig))
603 config
604 (branch
605 QMDConfigValue
606 programAddress
607 programBytes
608 prefetchUnits
609 gridX
610 gridY
611 gridZ
612 blockX
613 blockY
614 blockZ
615 shared
616 registers
617 scratch
618 .
619 (eliminate
620 QMDConstantFields
621 (lambda unrestricted current : (family QMDConstantFields) .
622 (family SM86QMDPhysicalConfig))
623 (qmdConstantFieldsForScratch scratch)
624 (branch
625 QMDConstantFieldsValue
626 constantEnable
627 constantLow
628 constantHigh
629 .
630 (constructor
631 SM86QMDPhysicalConfig
632 SM86QMDPhysicalConfigValue
633 (qmdPhysicalWord (qmdPrefetchBaseShifted programAddress))
634 (qmdPhysicalWord gridX)
635 (qmdPhysicalWord gridY)
636 (qmdPhysicalWord gridZ)
637 (qmdPhysicalWord (qmdSharedField shared))
638 (qmdPhysicalWord (qmdBlockXField blockX))
639 (qmdPhysicalWord (qmdBlockYZField blockY blockZ))
640 (qmdPhysicalWord (qmdRegisterField registers constantEnable))
641 (qmdPhysicalWord constantLow)
642 (qmdPhysicalWord constantHigh)
643 (qmdPhysicalWord (qmdProgramAddressLow programAddress))
644 (qmdPhysicalWord (qmdProgramAddressHigh programAddress))
645 (qmdPhysicalWord (qmdPrefetchControl programAddress prefetchUnits))))))))
646
647def qmdBuildPhysicalConfigWithConstantBufferForArchitecture =
648 (lambda unrestricted architecture : (family ModelWord32) .
649 (lambda unrestricted config : (family QMDConfig) .
650 (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
651 (eliminate
652 QMDConfig
653 (lambda unrestricted current : (family QMDConfig) . (family SM86QMDPhysicalConfig))
654 config
655 (branch
656 QMDConfigValue
657 programAddress
658 programBytes
659 prefetchUnits
660 gridX
661 gridY
662 gridZ
663 blockX
664 blockY
665 blockZ
666 shared
667 registers
668 scratch
669 .
670 (eliminate
671 QMDConstantFields
672 (lambda unrestricted current : (family QMDConstantFields) .
673 (family SM86QMDPhysicalConfig))
674 (qmdConstantFieldsForBuffer constantBuffer)
675 (branch
676 QMDConstantFieldsValue
677 constantEnable
678 constantLow
679 constantHigh
680 .
681 (constructor
682 SM86QMDPhysicalConfig
683 SM86QMDPhysicalConfigValue
684 (qmdPhysicalWord (qmdPrefetchBaseShifted programAddress))
685 (qmdPhysicalWord gridX)
686 (qmdPhysicalWord gridY)
687 (qmdPhysicalWord gridZ)
688 (qmdPhysicalWord (qmdSharedField shared))
689 (qmdPhysicalWord (qmdBlockXField blockX))
690 (qmdPhysicalWord (qmdBlockYZField blockY blockZ))
691 (qmdPhysicalWord (qmdRegisterField registers constantEnable))
692 (qmdPhysicalWord constantLow)
693 (qmdPhysicalWord constantHigh)
694 (qmdPhysicalWord (qmdProgramAddressLow programAddress))
695 (qmdPhysicalWord (qmdProgramAddressHigh programAddress))
696 (qmdPhysicalWord
697 (qmdPrefetchControlForArchitecture
698 architecture
699 programAddress
700 prefetchUnits))))))))))
701
702def qmdBuildPhysicalConfigWithConstantBuffer =
703 (lambda unrestricted config : (family QMDConfig) .
704 (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
705 (qmdBuildPhysicalConfigWithConstantBufferForArchitecture
706 (constructor ModelWord32 ModelWord32Value (byte 134) (byte 0) (byte 0) (byte 0))
707 config
708 constantBuffer)))
709
710def qmdBuild =
711 (lambda unrestricted config : (family QMDConfig) .
712 (eliminate
713 QMDValidationResult
714 (lambda unrestricted current : (family QMDValidationResult) . (family QMDBuildResult))
715 (qmdValidate config)
716 (branch
717 QMDValidated
718 .
719 (constructor
720 QMDBuildResult
721 QMDBuilt
722 (sm86EncodeQMD (qmdBuildPhysicalConfig config))
723 (byte-to-nat (byte 64))
724 (succ (byte-to-nat (byte 255)))
725 zero))
726 (branch QMDRejected error . (constructor QMDBuildResult QMDBuildRejected error))))
727
728def qmdBuildWithConstantBufferForArchitecture =
729 (lambda unrestricted architecture : (family ModelWord32) .
730 (lambda unrestricted config : (family QMDConfig) .
731 (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
732 (eliminate
733 QMDValidationResult
734 (lambda unrestricted current : (family QMDValidationResult) . (family QMDBuildResult))
735 (qmdValidate config)
736 (branch
737 QMDValidated
738 .
739 (nat-eliminate
740 (lambda unrestricted addressValid : Nat . (family QMDBuildResult))
741 (constructor
742 QMDBuildResult
743 QMDBuildRejected
744 (constructor QMDErrorCode QMDConstantBufferAddressOutOfRange))
745 (lambda unrestricted addressPredecessor : Nat .
746 (lambda unrestricted addressInduction : (family QMDBuildResult) .
747 (nat-eliminate
748 (lambda unrestricted sizeValid : Nat . (family QMDBuildResult))
749 (constructor
750 QMDBuildResult
751 QMDBuildRejected
752 (constructor QMDErrorCode QMDConstantBufferSizeOutOfRange))
753 (lambda unrestricted sizePredecessor : Nat .
754 (lambda unrestricted sizeInduction : (family QMDBuildResult) .
755 (constructor
756 QMDBuildResult
757 QMDBuilt
758 (sm86EncodeQMD
759 (qmdBuildPhysicalConfigWithConstantBufferForArchitecture
760 architecture config constantBuffer))
761 (byte-to-nat (byte 64))
762 (succ (byte-to-nat (byte 255)))
763 zero)))
764 (qmdConstantBufferSizeValid constantBuffer))))
765 (qmdConstantBufferAddressValid constantBuffer)))
766 (branch QMDRejected error . (constructor QMDBuildResult QMDBuildRejected error))))))
767
768def qmdBuildWithConstantBuffer =
769 (lambda unrestricted config : (family QMDConfig) .
770 (lambda unrestricted constantBuffer : (family QMDOptionalConstantBuffer) .
771 (qmdBuildWithConstantBufferForArchitecture
772 (constructor ModelWord32 ModelWord32Value (byte 134) (byte 0) (byte 0) (byte 0))
773 config
774 constantBuffer)))
775
776-- The Stage-0 oracle derives prefetch units from the unaligned program start
777-- and byte extent. A supplied value is accepted only when it is identical.
778def qmdProgramLowByteNatural =
779 (lambda unrestricted address : (family ModelWord64) .
780 (eliminate
781 ModelWord64
782 (lambda unrestricted current : (family ModelWord64) . Nat)
783 address
784 (branch ModelWord64Value b0 b1 b2 b3 b4 b5 b6 b7 . (byte-to-nat b0))))
785
786def qmdExpectedPrefetchUnitsNatural =
787 (lambda unrestricted address : (family ModelWord64) .
788 (lambda unrestricted programBytes : (family ModelWord32) .
789 (app
790 (lambda unrestricted requested : Nat .
791 (nat-eliminate
792 (lambda unrestricted aboveMaximum : Nat . Nat)
793 requested
794 (lambda unrestricted predecessor : Nat .
795 (lambda unrestricted induction : Nat .
796 (naturalSaturatingSubtract (naturalPowerOfTwo (byte-to-nat (byte 9))) (succ zero))))
797 (nat-less-than
798 (naturalSaturatingSubtract (naturalPowerOfTwo (byte-to-nat (byte 9))) (succ zero))
799 requested)))
800 (naturalDivideUnchecked
801 (naturalAdd
802 (naturalAdd (qmdProgramLowByteNatural address) (modelWord32ToNatural programBytes))
803 (naturalSaturatingSubtract (naturalPowerOfTwo (byte-to-nat (byte 8))) (succ zero)))
804 (naturalPowerOfTwo (byte-to-nat (byte 8)))))))
805
806def qmdPrefetchGeometryMatches =
807 (lambda unrestricted config : (family QMDConfig) .
808 (eliminate
809 QMDConfig
810 (lambda unrestricted current : (family QMDConfig) . Nat)
811 config
812 (branch
813 QMDConfigValue
814 programAddress
815 programBytes
816 prefetchUnits
817 gridX
818 gridY
819 gridZ
820 blockX
821 blockY
822 blockZ
823 shared
824 registers
825 scratch
826 .
827 (naturalEqual
828 (modelWord32ToNatural prefetchUnits)
829 (qmdExpectedPrefetchUnitsNatural programAddress programBytes)))))
830
831def qmdIdentityBindingValid =
832 (lambda unrestricted binding : (family QMDIdentityBinding) .
833 (eliminate
834 QMDIdentityBinding
835 (lambda unrestricted current : (family QMDIdentityBinding) . Nat)
836 binding
837 (branch
838 QMDIdentityBindingValue
839 program
840 resource
841 constant
842 .
843 (naturalAnd
844 (naturalEqual (bytes-length program) (byte-to-nat (byte 64)))
845 (naturalAnd
846 (naturalEqual (bytes-length resource) (byte-to-nat (byte 64)))
847 (naturalEqual (bytes-length constant) (byte-to-nat (byte 64))))))))
848
849def qmdIdentityBindingEqual =
850 (lambda unrestricted expected : (family QMDIdentityBinding) .
851 (lambda unrestricted observed : (family QMDIdentityBinding) .
852 (eliminate
853 QMDIdentityBinding
854 (lambda unrestricted current : (family QMDIdentityBinding) . Nat)
855 expected
856 (branch
857 QMDIdentityBindingValue
858 expectedProgram
859 expectedResource
860 expectedConstant
861 .
862 (eliminate
863 QMDIdentityBinding
864 (lambda unrestricted current : (family QMDIdentityBinding) . Nat)
865 observed
866 (branch
867 QMDIdentityBindingValue
868 observedProgram
869 observedResource
870 observedConstant
871 .
872 (naturalAnd
873 (bytes-equal expectedProgram observedProgram)
874 (naturalAnd
875 (bytes-equal expectedResource observedResource)
876 (bytes-equal expectedConstant observedConstant)))))))))
877
878def qmdAttestationErrorBytes =
879 (lambda unrestricted error : (family QMDAttestationError) .
880 (eliminate
881 QMDAttestationError
882 (lambda unrestricted current : (family QMDAttestationError) . Bytes)
883 error
884 (branch QMDPrefetchGeometryMismatch . b"ALPHA-HQAT-101")
885 (branch QMDEncodingExtentMismatch . b"ALPHA-HQAT-102")
886 (branch QMDIdentityMalformed . b"ALPHA-HQAT-103")
887 (branch QMDIdentityMismatch . b"ALPHA-HQAT-104")
888 (branch QMDEncodingRejected cause . (qmdErrorCodeBytes cause))))
889
890def qmdBuildAttested =
891 (lambda unrestricted expected : (family QMDIdentityBinding) .
892 (lambda unrestricted observed : (family QMDIdentityBinding) .
893 (lambda unrestricted config : (family QMDConfig) .
894 (nat-eliminate
895 (lambda unrestricted identitiesValid : Nat . (family QMDAttestedResult))
896 (constructor
897 QMDAttestedResult
898 QMDAttestationRejected
899 (constructor QMDAttestationError QMDIdentityMalformed))
900 (lambda unrestricted validPredecessor : Nat .
901 (lambda unrestricted validInduction : (family QMDAttestedResult) .
902 (nat-eliminate
903 (lambda unrestricted identitiesMatch : Nat . (family QMDAttestedResult))
904 (constructor
905 QMDAttestedResult
906 QMDAttestationRejected
907 (constructor QMDAttestationError QMDIdentityMismatch))
908 (lambda unrestricted matchPredecessor : Nat .
909 (lambda unrestricted matchInduction : (family QMDAttestedResult) .
910 (nat-eliminate
911 (lambda unrestricted geometryMatches : Nat . (family QMDAttestedResult))
912 (constructor
913 QMDAttestedResult
914 QMDAttestationRejected
915 (constructor QMDAttestationError QMDPrefetchGeometryMismatch))
916 (lambda unrestricted geometryPredecessor : Nat .
917 (lambda unrestricted geometryInduction : (family QMDAttestedResult) .
918 (eliminate
919 QMDBuildResult
920 (lambda unrestricted current : (family QMDBuildResult) .
921 (family QMDAttestedResult))
922 (qmdBuild config)
923 (branch
924 QMDBuilt
925 encoded
926 dwords
927 alignment
928 hostFallbacks
929 .
930 (nat-eliminate
931 (lambda unrestricted exactExtent : Nat . (family QMDAttestedResult))
932 (constructor
933 QMDAttestedResult
934 QMDAttestationRejected
935 (constructor QMDAttestationError QMDEncodingExtentMismatch))
936 (lambda unrestricted extentPredecessor : Nat .
937 (lambda unrestricted extentInduction : (family QMDAttestedResult) .
938 (constructor
939 QMDAttestedResult
940 QMDAttested
941 (constructor
942 QMDAttestedReceipt
943 QMDAttestedReceiptValue
944 encoded
945 observed
946 dwords
947 alignment
948 hostFallbacks))))
949 (naturalEqual
950 (bytes-length encoded)
951 (naturalPowerOfTwo (byte-to-nat (byte 8))))))
952 (branch
953 QMDBuildRejected
954 cause
955 .
956 (constructor
957 QMDAttestedResult
958 QMDAttestationRejected
959 (constructor QMDAttestationError QMDEncodingRejected cause))))))
960 (qmdPrefetchGeometryMatches config))))
961 (qmdIdentityBindingEqual expected observed))))
962 (naturalAnd (qmdIdentityBindingValid expected) (qmdIdentityBindingValid observed))))))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.