1module Platform.Linux.Nvidia.Memory.ABI
2
3import Model.Config
4import Model.Parameter
5import Model.Word32
6import Model.Word64
7import Std.Natural
8
9family MemoryLocation : Type 0
10constructor SystemMemory
11constructor VideoMemory
12
13end-family
14
15family CachePolicy : Type 0
16constructor HostCached
17constructor WriteCombined
18
19end-family
20
21family Physicality : Type 0
22constructor Contiguous
23constructor AllowNoncontiguous
24
25end-family
26
27family DMAABI : Type 0
28constructor DMAABI550
29constructor DMAABI580
30
31end-family
32
33family OptionalDMAABI : Type 0
34constructor NoDMAABI
35constructor SomeDMAABI
36field unrestricted selectedDMAABI : (family DMAABI)
37
38end-family
39
40family MemoryAllocation : Type 0
41constructor MemoryAllocationValue
42field unrestricted memoryAllocationBytes : (family ModelWord64)
43field unrestricted allocationLocation : (family MemoryLocation)
44field unrestricted allocationCache : (family CachePolicy)
45
46end-family
47
48family DMAMapping : Type 0
49constructor DMAMappingValue
50field unrestricted dMAClient : (family ModelWord32)
51field unrestricted dMADevice : (family ModelWord32)
52field unrestricted dMARange : (family ModelWord32)
53field unrestricted dMAMemory : (family ModelWord32)
54field unrestricted dMAMemoryOffset : (family ModelWord64)
55field unrestricted dMALength : (family ModelWord64)
56field unrestricted dMAFlags : (family ModelWord32)
57field unrestricted dMAAddress : (family ModelWord64)
58field unrestricted dMAStatus : (family ModelWord32)
59
60end-family
61
62family DMAUnmapping : Type 0
63constructor DMAUnmappingValue
64field unrestricted unmapClient : (family ModelWord32)
65field unrestricted unmapDevice : (family ModelWord32)
66field unrestricted unmapRange : (family ModelWord32)
67field unrestricted unmapMemory : (family ModelWord32)
68field unrestricted unmapAddress : (family ModelWord64)
69field unrestricted unmapBytes : (family ModelWord64)
70field unrestricted unmapStatus : (family ModelWord32)
71
72end-family
73
74family MemoryABIErrorCode : Type 0
75constructor MemoryABIUnsupportedDriver
76constructor MemoryABIAllocationSizeZero
77constructor MemoryABIMappingLengthZero
78constructor MemoryABIMappingAddressNull
79constructor MemoryABIUnmapAddressNull
80constructor MemoryABIReservationBaseNull
81constructor MemoryABIReservationSizeZero
82constructor MemoryABIReservationOverflow
83constructor MemoryABIMappingPayloadSizeMismatch
84constructor MemoryABIUnmappingPayloadSizeMismatch
85constructor MemoryABIMappingStatusRejected
86constructor MemoryABIMappingAddressMismatch
87constructor MemoryABIUnmappingStatusRejected
88
89end-family
90
91family MemoryABIOptionalError : Type 0
92constructor MemoryABINoError
93constructor MemoryABISomeError
94field unrestricted memoryABIOptionalErrorCode : (family MemoryABIErrorCode)
95
96end-family
97
98family MemoryABIBytesResult : Type 0
99constructor MemoryABIBytesSucceeded
100field unrestricted memoryABIEncodedBytes : Bytes
101constructor MemoryABIBytesFailed
102field unrestricted memoryABIBytesError : (family MemoryABIErrorCode)
103
104end-family
105
106family MemoryABIWord32Result : Type 0
107constructor MemoryABIWord32Succeeded
108field unrestricted memoryABIDecodedWord32 : (family ModelWord32)
109constructor MemoryABIWord32Failed
110field unrestricted memoryABIWord32Error : (family MemoryABIErrorCode)
111
112end-family
113
114family MemoryABIWord64Result : Type 0
115constructor MemoryABIWord64Succeeded
116field unrestricted memoryABIDecodedWord64 : (family ModelWord64)
117constructor MemoryABIWord64Failed
118field unrestricted memoryABIWord64Error : (family MemoryABIErrorCode)
119
120end-family
121
122family DMAABIResult : Type 0
123constructor DMAABISelected
124field unrestricted dMAABIValue : (family DMAABI)
125constructor DMAABIRejected
126field unrestricted dMAABIError : (family MemoryABIErrorCode)
127
128end-family
129
130family MemoryABIOperation : Type 0
131constructor MemoryABISelectDriver
132constructor MemoryABIEncodeMemoryAllocation
133constructor MemoryABIEncodeDMAMapping
134constructor MemoryABIEncodeDMAUnmapping
135constructor MemoryABIEncodeVAReservation
136constructor MemoryABIDecodeDMAAddress
137constructor MemoryABIDecodeDMAStatus
138constructor MemoryABIDecodeDMAUnmapStatus
139
140end-family
141
142family MemoryABITelemetry : Type 0
143constructor MemoryABITelemetryValue
144field unrestricted memoryABITelemetrySequence : Nat
145field unrestricted memoryABITelemetryOperation : (family MemoryABIOperation)
146field unrestricted memoryABITelemetryDMAABI : (family OptionalDMAABI)
147field unrestricted memoryABITelemetryInputBytes : Nat
148field unrestricted memoryABITelemetryOutputBytes : Nat
149field unrestricted memoryABITelemetrySucceeded : Nat
150field unrestricted memoryABITelemetryError : (family MemoryABIOptionalError)
151field unrestricted memoryABITelemetryHostFallbacks : Nat
152
153end-family
154
155family MemoryABIDMAMapReceipt : Type 0
156constructor MemoryABIDMAMapReceiptValue
157field unrestricted memoryABIDMAMapReceiptABI : (family DMAABI)
158field unrestricted memoryABIDMAMapReceiptAddress : (family ModelWord64)
159field unrestricted memoryABIDMAMapReceiptStatus : (family ModelWord32)
160field unrestricted memoryABIDMAMapReceiptPayloadBytes : Nat
161
162end-family
163
164family MemoryABIDMAMapReceiptResult : Type 0
165constructor MemoryABIDMAMapReceiptAccepted
166field unrestricted memoryABIAcceptedDMAMapReceipt : (family MemoryABIDMAMapReceipt)
167field unrestricted memoryABIAcceptedDMAMapTelemetry : (family MemoryABITelemetry)
168constructor MemoryABIDMAMapReceiptRejected
169field unrestricted memoryABIRejectedDMAMapError : (family MemoryABIErrorCode)
170field unrestricted memoryABIRejectedDMAMapTelemetry : (family MemoryABITelemetry)
171
172end-family
173
174family MemoryABIDMAUnmapReceipt : Type 0
175constructor MemoryABIDMAUnmapReceiptValue
176field unrestricted memoryABIDMAUnmapReceiptABI : (family DMAABI)
177field unrestricted memoryABIDMAUnmapReceiptStatus : (family ModelWord32)
178field unrestricted memoryABIDMAUnmapReceiptPayloadBytes : Nat
179
180end-family
181
182family MemoryABIDMAUnmapReceiptResult : Type 0
183constructor MemoryABIDMAUnmapReceiptAccepted
184field unrestricted memoryABIAcceptedDMAUnmapReceipt : (family MemoryABIDMAUnmapReceipt)
185field unrestricted memoryABIAcceptedDMAUnmapTelemetry : (family MemoryABITelemetry)
186constructor MemoryABIDMAUnmapReceiptRejected
187field unrestricted memoryABIRejectedDMAUnmapError : (family MemoryABIErrorCode)
188field unrestricted memoryABIRejectedDMAUnmapTelemetry : (family MemoryABITelemetry)
189
190end-family
191
192def memoryABIErrorCodeBytes =
193 (lambda unrestricted code : (family MemoryABIErrorCode) .
194 (eliminate
195 MemoryABIErrorCode
196 (lambda unrestricted current : (family MemoryABIErrorCode) . Bytes)
197 code
198 (branch
199 MemoryABIUnsupportedDriver
200 .
201 b"ALPHA-GAIA-ABI-001")
202 (branch
203 MemoryABIAllocationSizeZero
204 .
205 b"ALPHA-GAIA-ABI-002")
206 (branch
207 MemoryABIMappingLengthZero
208 .
209 b"ALPHA-GAIA-ABI-003")
210 (branch
211 MemoryABIMappingAddressNull
212 .
213 b"ALPHA-GAIA-ABI-004")
214 (branch
215 MemoryABIUnmapAddressNull
216 .
217 b"ALPHA-GAIA-ABI-005")
218 (branch
219 MemoryABIReservationBaseNull
220 .
221 b"ALPHA-GAIA-ABI-006")
222 (branch
223 MemoryABIReservationSizeZero
224 .
225 b"ALPHA-GAIA-ABI-007")
226 (branch
227 MemoryABIReservationOverflow
228 .
229 b"ALPHA-GAIA-ABI-008")
230 (branch
231 MemoryABIMappingPayloadSizeMismatch
232 .
233 b"ALPHA-GAIA-ABI-009")
234 (branch
235 MemoryABIUnmappingPayloadSizeMismatch
236 .
237 b"ALPHA-GAIA-ABI-010")
238 (branch
239 MemoryABIMappingStatusRejected
240 .
241 b"ALPHA-GAIA-ABI-011")
242 (branch
243 MemoryABIMappingAddressMismatch
244 .
245 b"ALPHA-GAIA-ABI-012")
246 (branch
247 MemoryABIUnmappingStatusRejected
248 .
249 b"ALPHA-GAIA-ABI-013")))
250
251def memoryABIZeroBytes =
252 (lambda unrestricted count : Nat .
253 (nat-eliminate
254 (lambda unrestricted current : Nat . Bytes)
255 b""
256 (lambda unrestricted predecessor : Nat .
257 (lambda unrestricted induction : Bytes . (bytes-cons (byte 0) induction)))
258 count))
259
260def memoryABIEncodeWord32LE =
261 (lambda unrestricted value : (family ModelWord32) .
262 (eliminate
263 ModelWord32
264 (lambda unrestricted current : (family ModelWord32) . Bytes)
265 value
266 (branch
267 ModelWord32Value
268 b0
269 b1
270 b2
271 b3
272 .
273 (bytes-cons b0 (bytes-cons b1 (bytes-cons b2 (bytes-cons b3 b"")))))))
274
275def memoryABIEncodeWord64LE =
276 (lambda unrestricted value : (family ModelWord64) .
277 (eliminate
278 ModelWord64
279 (lambda unrestricted current : (family ModelWord64) . Bytes)
280 value
281 (branch
282 ModelWord64Value
283 b0
284 b1
285 b2
286 b3
287 b4
288 b5
289 b6
290 b7
291 .
292 (bytes-cons
293 b0
294 (bytes-cons
295 b1
296 (bytes-cons
297 b2
298 (bytes-cons
299 b3
300 (bytes-cons b4 (bytes-cons b5 (bytes-cons b6 (bytes-cons b7 b"")))))))))))
301
302def memoryABIDropBytes =
303 (lambda unrestricted count : Nat .
304 (nat-eliminate
305 (lambda unrestricted current : Nat . (pi unrestricted input : Bytes . Bytes))
306 (lambda unrestricted input : Bytes . input)
307 (lambda unrestricted predecessor : Nat .
308 (lambda unrestricted induction : (pi unrestricted input : Bytes . Bytes) .
309 (lambda unrestricted input : Bytes . (induction (bytes-tail input)))))
310 count))
311
312def memoryABIDecodeWord32LEAt =
313 (lambda unrestricted offset : Nat .
314 (lambda unrestricted input : Bytes .
315 (app
316 (lambda unrestricted tail0 : Bytes .
317 (app
318 (lambda unrestricted tail1 : Bytes .
319 (app
320 (lambda unrestricted tail2 : Bytes .
321 (constructor
322 ModelWord32
323 ModelWord32Value
324 (bytes-head tail0)
325 (bytes-head tail1)
326 (bytes-head tail2)
327 (bytes-head (bytes-tail tail2))))
328 (bytes-tail tail1)))
329 (bytes-tail tail0)))
330 (memoryABIDropBytes offset input))))
331
332def memoryABIDecodeWord64LEAt =
333 (lambda unrestricted offset : Nat .
334 (lambda unrestricted input : Bytes .
335 (app
336 (lambda unrestricted t0 : Bytes .
337 (app
338 (lambda unrestricted t1 : Bytes .
339 (app
340 (lambda unrestricted t2 : Bytes .
341 (app
342 (lambda unrestricted t3 : Bytes .
343 (app
344 (lambda unrestricted t4 : Bytes .
345 (app
346 (lambda unrestricted t5 : Bytes .
347 (app
348 (lambda unrestricted t6 : Bytes .
349 (constructor
350 ModelWord64
351 ModelWord64Value
352 (bytes-head t0)
353 (bytes-head t1)
354 (bytes-head t2)
355 (bytes-head t3)
356 (bytes-head t4)
357 (bytes-head t5)
358 (bytes-head t6)
359 (bytes-head (bytes-tail t6))))
360 (bytes-tail t5)))
361 (bytes-tail t4)))
362 (bytes-tail t3)))
363 (bytes-tail t2)))
364 (bytes-tail t1)))
365 (bytes-tail t0)))
366 (memoryABIDropBytes offset input))))
367
368def memoryABINaturalFlagAnd =
369 (lambda unrestricted left : Nat .
370 (lambda unrestricted right : Nat .
371 (nat-eliminate
372 (lambda unrestricted current : Nat . Nat)
373 zero
374 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . right))
375 left)))
376
377def memoryABINaturalFlagOr =
378 (lambda unrestricted left : Nat .
379 (lambda unrestricted right : Nat .
380 (nat-eliminate
381 (lambda unrestricted current : Nat . Nat)
382 right
383 (lambda unrestricted predecessor : Nat .
384 (lambda unrestricted induction : Nat . (succ zero)))
385 left)))
386
387def memoryABIDriverPrefixMatches =
388 (lambda unrestricted input : Bytes .
389 (lambda unrestricted digit1 : Byte .
390 (lambda unrestricted digit2 : Byte .
391 (lambda unrestricted digit3 : Byte .
392 (nat-eliminate
393 (lambda unrestricted longEnough : Nat . Nat)
394 zero
395 (lambda unrestricted predecessor : Nat .
396 (lambda unrestricted induction : Nat .
397 (app
398 (lambda unrestricted t1 : Bytes .
399 (app
400 (lambda unrestricted t2 : Bytes .
401 (app
402 (lambda unrestricted t3 : Bytes .
403 (memoryABINaturalFlagAnd
404 (byte-equal (bytes-head input) digit1)
405 (memoryABINaturalFlagAnd
406 (byte-equal (bytes-head t1) digit2)
407 (memoryABINaturalFlagAnd
408 (byte-equal (bytes-head t2) digit3)
409 (byte-equal (bytes-head t3) (byte 46))))))
410 (bytes-tail t2)))
411 (bytes-tail t1)))
412 (bytes-tail input))))
413 (nat-less-than (byte-to-nat (byte 3)) (bytes-length input)))))))
414
415def dMAABIForDriver =
416 (lambda unrestricted driverVersion : Bytes .
417 (nat-eliminate
418 (lambda unrestricted is550 : Nat . (family DMAABIResult))
419 (nat-eliminate
420 (lambda unrestricted is580 : Nat . (family DMAABIResult))
421 (constructor
422 DMAABIResult
423 DMAABIRejected
424 (constructor MemoryABIErrorCode MemoryABIUnsupportedDriver))
425 (lambda unrestricted predecessor : Nat .
426 (lambda unrestricted induction : (family DMAABIResult) .
427 (constructor DMAABIResult DMAABISelected (constructor DMAABI DMAABI580))))
428 (memoryABIDriverPrefixMatches driverVersion (byte 53) (byte 56) (byte 48)))
429 (lambda unrestricted predecessor : Nat .
430 (lambda unrestricted induction : (family DMAABIResult) .
431 (constructor DMAABIResult DMAABISelected (constructor DMAABI DMAABI550))))
432 (memoryABIDriverPrefixMatches driverVersion (byte 53) (byte 53) (byte 48))))
433
434def memoryABIMemoryAllocationSize =
435 (byte-to-nat (byte 128))
436
437def memoryABIVAReservationSize =
438 (byte-to-nat (byte 24))
439
440def memoryABIDMAMappingSize =
441 (lambda unrestricted abi : (family DMAABI) .
442 (eliminate
443 DMAABI
444 (lambda unrestricted current : (family DMAABI) . Nat)
445 abi
446 (branch DMAABI550 . (byte-to-nat (byte 56)))
447 (branch DMAABI580 . (byte-to-nat (byte 64)))))
448
449def memoryABIDMAUnmappingSize =
450 (lambda unrestricted abi : (family DMAABI) . (byte-to-nat (byte 48)))
451
452def memoryABIMemoryClass =
453 (lambda unrestricted location : (family MemoryLocation) .
454 (eliminate
455 MemoryLocation
456 (lambda unrestricted current : (family MemoryLocation) . (family ModelWord32))
457 location
458 (branch
459 SystemMemory
460 .
461 (constructor ModelWord32 ModelWord32Value (byte 62) (byte 0) (byte 0) (byte 0)))
462 (branch
463 VideoMemory
464 .
465 (constructor ModelWord32 ModelWord32Value (byte 64) (byte 0) (byte 0) (byte 0)))))
466
467def memoryABIAllocationAttributeWith =
468 (lambda unrestricted location : (family MemoryLocation) .
469 (lambda unrestricted cache : (family CachePolicy) .
470 (lambda unrestricted physicality : (family Physicality) .
471 (eliminate
472 MemoryLocation
473 (lambda unrestricted current : (family MemoryLocation) . (family ModelWord32))
474 location
475 (branch
476 SystemMemory
477 .
478 (eliminate
479 CachePolicy
480 (lambda unrestricted current : (family CachePolicy) . (family ModelWord32))
481 cache
482 (branch
483 HostCached
484 .
485 (eliminate
486 Physicality
487 (lambda unrestricted current : (family Physicality) . (family ModelWord32))
488 physicality
489 (branch
490 Contiguous
491 .
492 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 50)))
493 (branch
494 AllowNoncontiguous
495 .
496 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 58)))))
497 (branch
498 WriteCombined
499 .
500 (eliminate
501 Physicality
502 (lambda unrestricted current : (family Physicality) . (family ModelWord32))
503 physicality
504 (branch
505 Contiguous
506 .
507 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 82)))
508 (branch
509 AllowNoncontiguous
510 .
511 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 90)))))))
512 (branch
513 VideoMemory
514 .
515 (eliminate
516 CachePolicy
517 (lambda unrestricted current : (family CachePolicy) . (family ModelWord32))
518 cache
519 (branch
520 HostCached
521 .
522 (eliminate
523 Physicality
524 (lambda unrestricted current : (family Physicality) . (family ModelWord32))
525 physicality
526 (branch
527 Contiguous
528 .
529 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 48)))
530 (branch
531 AllowNoncontiguous
532 .
533 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 56)))))
534 (branch
535 WriteCombined
536 .
537 (eliminate
538 Physicality
539 (lambda unrestricted current : (family Physicality) . (family ModelWord32))
540 physicality
541 (branch
542 Contiguous
543 .
544 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 80)))
545 (branch
546 AllowNoncontiguous
547 .
548 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 88)))))))))))
549
550def memoryABIAllocationAttribute =
551 (lambda unrestricted location : (family MemoryLocation) .
552 (lambda unrestricted cache : (family CachePolicy) .
553 (memoryABIAllocationAttributeWith location cache (constructor Physicality AllowNoncontiguous))))
554
555def memoryABIMapFlagsSystem =
556 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 128) (byte 0) (byte 3))
557
558def memoryABIMapFlagsVideo =
559 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 1) (byte 1))
560
561def memoryABIMapFlagsRegisters =
562 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 0) (byte 0) (byte 0))
563
564def memoryABIDMAMappingFlags =
565 (lambda unrestricted location : (family MemoryLocation) .
566 (lambda unrestricted cache : (family CachePolicy) .
567 (eliminate
568 MemoryLocation
569 (lambda unrestricted current : (family MemoryLocation) . (family ModelWord32))
570 location
571 (branch
572 SystemMemory
573 .
574 (eliminate
575 CachePolicy
576 (lambda unrestricted current : (family CachePolicy) . (family ModelWord32))
577 cache
578 (branch
579 HostCached
580 .
581 (constructor ModelWord32 ModelWord32Value (byte 16) (byte 128) (byte 0) (byte 0)))
582 (branch
583 WriteCombined
584 .
585 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 128) (byte 0) (byte 0)))))
586 (branch
587 VideoMemory
588 .
589 (constructor ModelWord32 ModelWord32Value (byte 0) (byte 128) (byte 0) (byte 0))))))
590
591def memoryABIEncodeMemoryAllocationWith =
592 (lambda unrestricted physicality : (family Physicality) .
593 (lambda unrestricted allocation : (family MemoryAllocation) .
594 (eliminate
595 MemoryAllocation
596 (lambda unrestricted current : (family MemoryAllocation) . (family MemoryABIBytesResult))
597 allocation
598 (branch
599 MemoryAllocationValue
600 bytes
601 location
602 cache
603 .
604 (nat-eliminate
605 (lambda unrestricted sizeIsZero : Nat . (family MemoryABIBytesResult))
606 (constructor
607 MemoryABIBytesResult
608 MemoryABIBytesSucceeded
609 (bytes-append
610 (bytes 73 76 69 72 0 0 0 0 0 128 0 0)
611 (bytes-append
612 (memoryABIZeroBytes (byte-to-nat (byte 12)))
613 (bytes-append
614 (memoryABIEncodeWord32LE
615 (memoryABIAllocationAttributeWith location cache physicality))
616 (bytes-append
617 (memoryABIZeroBytes (byte-to-nat (byte 36)))
618 (bytes-append
619 (memoryABIEncodeWord64LE bytes)
620 (bytes-append
621 (bytes 0 16 0 0 0 0 0 0)
622 (memoryABIZeroBytes (byte-to-nat (byte 48))))))))))
623 (lambda unrestricted predecessor : Nat .
624 (lambda unrestricted induction : (family MemoryABIBytesResult) .
625 (constructor
626 MemoryABIBytesResult
627 MemoryABIBytesFailed
628 (constructor MemoryABIErrorCode MemoryABIAllocationSizeZero))))
629 (modelWord64IsZero bytes))))))
630
631def memoryABIEncodeMemoryAllocation =
632 (lambda unrestricted allocation : (family MemoryAllocation) .
633 (memoryABIEncodeMemoryAllocationWith (constructor Physicality AllowNoncontiguous) allocation))
634
635def memoryABIEncodeDMAMapping =
636 (lambda unrestricted abi : (family DMAABI) .
637 (lambda unrestricted mapping : (family DMAMapping) .
638 (eliminate
639 DMAMapping
640 (lambda unrestricted current : (family DMAMapping) . (family MemoryABIBytesResult))
641 mapping
642 (branch
643 DMAMappingValue
644 client
645 device
646 range
647 memory
648 memoryOffset
649 length
650 flags
651 address
652 status
653 .
654 (nat-eliminate
655 (lambda unrestricted lengthIsZero : Nat . (family MemoryABIBytesResult))
656 (nat-eliminate
657 (lambda unrestricted addressIsZero : Nat . (family MemoryABIBytesResult))
658 (constructor
659 MemoryABIBytesResult
660 MemoryABIBytesSucceeded
661 (bytes-append
662 (memoryABIEncodeWord32LE client)
663 (bytes-append
664 (memoryABIEncodeWord32LE device)
665 (bytes-append
666 (memoryABIEncodeWord32LE range)
667 (bytes-append
668 (memoryABIEncodeWord32LE memory)
669 (bytes-append
670 (memoryABIEncodeWord64LE memoryOffset)
671 (bytes-append
672 (memoryABIEncodeWord64LE length)
673 (bytes-append
674 (memoryABIEncodeWord32LE flags)
675 (eliminate
676 DMAABI
677 (lambda unrestricted current : (family DMAABI) . Bytes)
678 abi
679 (branch
680 DMAABI550
681 .
682 (bytes-append
683 (memoryABIZeroBytes (byte-to-nat (byte 4)))
684 (bytes-append
685 (memoryABIEncodeWord64LE address)
686 (bytes-append
687 (memoryABIEncodeWord32LE status)
688 (memoryABIZeroBytes (byte-to-nat (byte 4)))))))
689 (branch
690 DMAABI580
691 .
692 (bytes-append
693 (memoryABIZeroBytes (byte-to-nat (byte 12)))
694 (bytes-append
695 (memoryABIEncodeWord64LE address)
696 (bytes-append
697 (memoryABIEncodeWord32LE status)
698 (memoryABIZeroBytes (byte-to-nat (byte 4))))))))))))))))
699 (lambda unrestricted predecessor : Nat .
700 (lambda unrestricted induction : (family MemoryABIBytesResult) .
701 (constructor
702 MemoryABIBytesResult
703 MemoryABIBytesFailed
704 (constructor MemoryABIErrorCode MemoryABIMappingAddressNull))))
705 (modelWord64IsZero address))
706 (lambda unrestricted predecessor : Nat .
707 (lambda unrestricted induction : (family MemoryABIBytesResult) .
708 (constructor
709 MemoryABIBytesResult
710 MemoryABIBytesFailed
711 (constructor MemoryABIErrorCode MemoryABIMappingLengthZero))))
712 (modelWord64IsZero length))))))
713
714def memoryABIEncodeDMAUnmapping =
715 (lambda unrestricted abi : (family DMAABI) .
716 (lambda unrestricted unmapping : (family DMAUnmapping) .
717 (eliminate
718 DMAUnmapping
719 (lambda unrestricted current : (family DMAUnmapping) . (family MemoryABIBytesResult))
720 unmapping
721 (branch
722 DMAUnmappingValue
723 client
724 device
725 range
726 memory
727 address
728 bytes
729 status
730 .
731 (nat-eliminate
732 (lambda unrestricted addressIsZero : Nat . (family MemoryABIBytesResult))
733 (constructor
734 MemoryABIBytesResult
735 MemoryABIBytesSucceeded
736 (bytes-append
737 (memoryABIEncodeWord32LE client)
738 (bytes-append
739 (memoryABIEncodeWord32LE device)
740 (bytes-append
741 (memoryABIEncodeWord32LE range)
742 (bytes-append
743 (memoryABIEncodeWord32LE memory)
744 (bytes-append
745 (memoryABIZeroBytes (byte-to-nat (byte 8)))
746 (bytes-append
747 (memoryABIEncodeWord64LE address)
748 (bytes-append
749 (memoryABIEncodeWord64LE bytes)
750 (bytes-append
751 (memoryABIEncodeWord32LE status)
752 (memoryABIZeroBytes (byte-to-nat (byte 4))))))))))))
753 (lambda unrestricted predecessor : Nat .
754 (lambda unrestricted induction : (family MemoryABIBytesResult) .
755 (constructor
756 MemoryABIBytesResult
757 MemoryABIBytesFailed
758 (constructor MemoryABIErrorCode MemoryABIUnmapAddressNull))))
759 (modelWord64IsZero address))))))
760
761def memoryABIEncodeVAReservation =
762 (lambda unrestricted vaspace : (family ModelWord32) .
763 (lambda unrestricted base : (family ModelWord64) .
764 (lambda unrestricted size : (family ModelWord64) .
765 (nat-eliminate
766 (lambda unrestricted baseIsZero : Nat . (family MemoryABIBytesResult))
767 (nat-eliminate
768 (lambda unrestricted sizeIsZero : Nat . (family MemoryABIBytesResult))
769 (eliminate
770 ModelWord64CheckedResult
771 (lambda unrestricted result : (family ModelWord64CheckedResult) .
772 (family MemoryABIBytesResult))
773 (modelWord64AddChecked base (modelWord64Subtract size modelWord64One))
774 (branch
775 ModelWord64CheckedSucceeded
776 limit
777 .
778 (constructor
779 MemoryABIBytesResult
780 MemoryABIBytesSucceeded
781 (bytes-append
782 (memoryABIEncodeWord64LE base)
783 (bytes-append
784 (memoryABIEncodeWord64LE limit)
785 (bytes-append
786 (memoryABIEncodeWord32LE vaspace)
787 (memoryABIZeroBytes (byte-to-nat (byte 4))))))))
788 (branch
789 ModelWord64CheckedFailed
790 error
791 .
792 (constructor
793 MemoryABIBytesResult
794 MemoryABIBytesFailed
795 (constructor MemoryABIErrorCode MemoryABIReservationOverflow))))
796 (lambda unrestricted predecessor : Nat .
797 (lambda unrestricted induction : (family MemoryABIBytesResult) .
798 (constructor
799 MemoryABIBytesResult
800 MemoryABIBytesFailed
801 (constructor MemoryABIErrorCode MemoryABIReservationSizeZero))))
802 (modelWord64IsZero size))
803 (lambda unrestricted predecessor : Nat .
804 (lambda unrestricted induction : (family MemoryABIBytesResult) .
805 (constructor
806 MemoryABIBytesResult
807 MemoryABIBytesFailed
808 (constructor MemoryABIErrorCode MemoryABIReservationBaseNull))))
809 (modelWord64IsZero base)))))
810
811def memoryABIDecodeDMAAddress =
812 (lambda unrestricted abi : (family DMAABI) .
813 (lambda unrestricted input : Bytes .
814 (nat-eliminate
815 (lambda unrestricted sizeMatches : Nat . (family MemoryABIWord64Result))
816 (constructor
817 MemoryABIWord64Result
818 MemoryABIWord64Failed
819 (constructor MemoryABIErrorCode MemoryABIMappingPayloadSizeMismatch))
820 (lambda unrestricted predecessor : Nat .
821 (lambda unrestricted induction : (family MemoryABIWord64Result) .
822 (constructor
823 MemoryABIWord64Result
824 MemoryABIWord64Succeeded
825 (memoryABIDecodeWord64LEAt
826 (eliminate
827 DMAABI
828 (lambda unrestricted current : (family DMAABI) . Nat)
829 abi
830 (branch DMAABI550 . (byte-to-nat (byte 40)))
831 (branch DMAABI580 . (byte-to-nat (byte 48))))
832 input))))
833 (naturalEqual (bytes-length input) (memoryABIDMAMappingSize abi)))))
834
835def memoryABIDecodeDMAStatus =
836 (lambda unrestricted abi : (family DMAABI) .
837 (lambda unrestricted input : Bytes .
838 (nat-eliminate
839 (lambda unrestricted sizeMatches : Nat . (family MemoryABIWord32Result))
840 (constructor
841 MemoryABIWord32Result
842 MemoryABIWord32Failed
843 (constructor MemoryABIErrorCode MemoryABIMappingPayloadSizeMismatch))
844 (lambda unrestricted predecessor : Nat .
845 (lambda unrestricted induction : (family MemoryABIWord32Result) .
846 (constructor
847 MemoryABIWord32Result
848 MemoryABIWord32Succeeded
849 (memoryABIDecodeWord32LEAt
850 (eliminate
851 DMAABI
852 (lambda unrestricted current : (family DMAABI) . Nat)
853 abi
854 (branch DMAABI550 . (byte-to-nat (byte 48)))
855 (branch DMAABI580 . (byte-to-nat (byte 56))))
856 input))))
857 (naturalEqual (bytes-length input) (memoryABIDMAMappingSize abi)))))
858
859def memoryABIDecodeDMAUnmapStatus =
860 (lambda unrestricted abi : (family DMAABI) .
861 (lambda unrestricted input : Bytes .
862 (nat-eliminate
863 (lambda unrestricted sizeMatches : Nat . (family MemoryABIWord32Result))
864 (constructor
865 MemoryABIWord32Result
866 MemoryABIWord32Failed
867 (constructor MemoryABIErrorCode MemoryABIUnmappingPayloadSizeMismatch))
868 (lambda unrestricted predecessor : Nat .
869 (lambda unrestricted induction : (family MemoryABIWord32Result) .
870 (constructor
871 MemoryABIWord32Result
872 MemoryABIWord32Succeeded
873 (memoryABIDecodeWord32LEAt (byte-to-nat (byte 40)) input))))
874 (naturalEqual (bytes-length input) (memoryABIDMAUnmappingSize abi)))))
875
876def memoryABITelemetrySucceededFor =
877 (lambda unrestricted sequence : Nat .
878 (lambda unrestricted operation : (family MemoryABIOperation) .
879 (lambda unrestricted abi : (family OptionalDMAABI) .
880 (lambda unrestricted inputBytes : Nat .
881 (lambda unrestricted outputBytes : Nat .
882 (constructor
883 MemoryABITelemetry
884 MemoryABITelemetryValue
885 sequence
886 operation
887 abi
888 inputBytes
889 outputBytes
890 (succ zero)
891 (constructor MemoryABIOptionalError MemoryABINoError)
892 zero))))))
893
894def memoryABITelemetryFailedFor =
895 (lambda unrestricted sequence : Nat .
896 (lambda unrestricted operation : (family MemoryABIOperation) .
897 (lambda unrestricted abi : (family OptionalDMAABI) .
898 (lambda unrestricted inputBytes : Nat .
899 (lambda unrestricted error : (family MemoryABIErrorCode) .
900 (constructor
901 MemoryABITelemetry
902 MemoryABITelemetryValue
903 sequence
904 operation
905 abi
906 inputBytes
907 zero
908 zero
909 (constructor MemoryABIOptionalError MemoryABISomeError error)
910 zero))))))
911
912-- Exact NVOS46/NVOS47 replies become typed receipts only after payload size,
913-- RM status, and returned address have all been checked.
914def memoryABIMapReceiptFailure =
915 (lambda unrestricted sequence : Nat .
916 (lambda unrestricted abi : (family DMAABI) .
917 (lambda unrestricted inputBytes : Nat .
918 (lambda unrestricted code : (family MemoryABIErrorCode) .
919 (constructor
920 MemoryABIDMAMapReceiptResult
921 MemoryABIDMAMapReceiptRejected
922 code
923 (memoryABITelemetryFailedFor
924 sequence
925 (constructor MemoryABIOperation MemoryABIDecodeDMAStatus)
926 (constructor OptionalDMAABI SomeDMAABI abi)
927 inputBytes
928 code))))))
929
930def memoryABIUnmapReceiptFailure =
931 (lambda unrestricted sequence : Nat .
932 (lambda unrestricted abi : (family DMAABI) .
933 (lambda unrestricted inputBytes : Nat .
934 (lambda unrestricted code : (family MemoryABIErrorCode) .
935 (constructor
936 MemoryABIDMAUnmapReceiptResult
937 MemoryABIDMAUnmapReceiptRejected
938 code
939 (memoryABITelemetryFailedFor
940 sequence
941 (constructor MemoryABIOperation MemoryABIDecodeDMAUnmapStatus)
942 (constructor OptionalDMAABI SomeDMAABI abi)
943 inputBytes
944 code))))))
945
946def memoryABIDecodeDMAMapReceipt =
947 (lambda unrestricted sequence : Nat .
948 (lambda unrestricted abi : (family DMAABI) .
949 (lambda unrestricted expectedAddress : (family ModelWord64) .
950 (lambda unrestricted input : Bytes .
951 (eliminate
952 MemoryABIWord32Result
953 (lambda unrestricted result : (family MemoryABIWord32Result) .
954 (family MemoryABIDMAMapReceiptResult))
955 (memoryABIDecodeDMAStatus abi input)
956 (branch
957 MemoryABIWord32Succeeded
958 status
959 .
960 (nat-eliminate
961 (lambda unrestricted statusValue : Nat . (family MemoryABIDMAMapReceiptResult))
962 (eliminate
963 MemoryABIWord64Result
964 (lambda unrestricted result : (family MemoryABIWord64Result) .
965 (family MemoryABIDMAMapReceiptResult))
966 (memoryABIDecodeDMAAddress abi input)
967 (branch
968 MemoryABIWord64Succeeded
969 address
970 .
971 (nat-eliminate
972 (lambda unrestricted addressMatches : Nat .
973 (family MemoryABIDMAMapReceiptResult))
974 (memoryABIMapReceiptFailure
975 sequence
976 abi
977 (bytes-length input)
978 (constructor MemoryABIErrorCode MemoryABIMappingAddressMismatch))
979 (lambda unrestricted predecessor : Nat .
980 (lambda unrestricted induction : (family MemoryABIDMAMapReceiptResult) .
981 (constructor
982 MemoryABIDMAMapReceiptResult
983 MemoryABIDMAMapReceiptAccepted
984 (constructor
985 MemoryABIDMAMapReceipt
986 MemoryABIDMAMapReceiptValue
987 abi
988 address
989 status
990 (bytes-length input))
991 (memoryABITelemetrySucceededFor
992 sequence
993 (constructor MemoryABIOperation MemoryABIDecodeDMAAddress)
994 (constructor OptionalDMAABI SomeDMAABI abi)
995 (bytes-length input)
996 (bytes-length input)))))
997 (modelWord64Equal address expectedAddress)))
998 (branch
999 MemoryABIWord64Failed
1000 code
1001 .
1002 (memoryABIMapReceiptFailure sequence abi (bytes-length input) code)))
1003 (lambda unrestricted predecessor : Nat .
1004 (lambda unrestricted induction : (family MemoryABIDMAMapReceiptResult) .
1005 (memoryABIMapReceiptFailure
1006 sequence
1007 abi
1008 (bytes-length input)
1009 (constructor MemoryABIErrorCode MemoryABIMappingStatusRejected))))
1010 (modelWord32ToNatural status)))
1011 (branch
1012 MemoryABIWord32Failed
1013 code
1014 .
1015 (memoryABIMapReceiptFailure sequence abi (bytes-length input) code)))))))
1016
1017def memoryABIDecodeDMAUnmapReceipt =
1018 (lambda unrestricted sequence : Nat .
1019 (lambda unrestricted abi : (family DMAABI) .
1020 (lambda unrestricted input : Bytes .
1021 (eliminate
1022 MemoryABIWord32Result
1023 (lambda unrestricted result : (family MemoryABIWord32Result) .
1024 (family MemoryABIDMAUnmapReceiptResult))
1025 (memoryABIDecodeDMAUnmapStatus abi input)
1026 (branch
1027 MemoryABIWord32Succeeded
1028 status
1029 .
1030 (nat-eliminate
1031 (lambda unrestricted statusValue : Nat . (family MemoryABIDMAUnmapReceiptResult))
1032 (constructor
1033 MemoryABIDMAUnmapReceiptResult
1034 MemoryABIDMAUnmapReceiptAccepted
1035 (constructor
1036 MemoryABIDMAUnmapReceipt
1037 MemoryABIDMAUnmapReceiptValue
1038 abi
1039 status
1040 (bytes-length input))
1041 (memoryABITelemetrySucceededFor
1042 sequence
1043 (constructor MemoryABIOperation MemoryABIDecodeDMAUnmapStatus)
1044 (constructor OptionalDMAABI SomeDMAABI abi)
1045 (bytes-length input)
1046 (bytes-length input)))
1047 (lambda unrestricted predecessor : Nat .
1048 (lambda unrestricted induction : (family MemoryABIDMAUnmapReceiptResult) .
1049 (memoryABIUnmapReceiptFailure
1050 sequence
1051 abi
1052 (bytes-length input)
1053 (constructor MemoryABIErrorCode MemoryABIUnmappingStatusRejected))))
1054 (modelWord32ToNatural status)))
1055 (branch
1056 MemoryABIWord32Failed
1057 code
1058 .
1059 (memoryABIUnmapReceiptFailure sequence abi (bytes-length input) code))))))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.