1module ResourcePlanContract
2
3import Platform.Linux.Nvidia.ResourcePlan
4import Platform.Linux.Nvidia.PlanHost
5import Platform.Linux.Nvidia.LinearStep
6import Platform.Linux.Nvidia.ProgramPlan
7import Runtime.NativeResourcePlan
8import Runtime.NativePhysicalMemory
9import Runtime.NativePhysicalProgram
10import Runtime.NativeLaunchRecipeLoad
11import Runtime.ArenaCertificate
12import Execution.ResourceGraph
13import Compiler.Planning.Resources
14import Std.List
15import Std.Foundation
16import Std.Natural
17import Data.Bytes
18import Model.Config
19import Model.Parameter
20import Model.Word64
21
22-- Hand-computed accounting fixtures. No capacity, page size or alias here
23-- is a measured device fact. Two process contexts share one host domain;
24-- their independent GPU domains cannot borrow each other's unused capacity.
25def rpGraph =
26 (lambda unrestricted host : Nat .
27 (lambda unrestricted left : Nat .
28 (lambda unrestricted right : Nat .
29 (constructor
30 ResourceGraph
31 ResourceGraphOf
32 (constructor
33 StdList
34 StdListCons
35 (family ResourceEndpoint)
36 (constructor
37 ResourceEndpoint
38 ResourceEndpointOf
39 0
40 b"fixture-engine-0"
41 b"fixture-native"
42 (constructor StdList StdListEmpty Bytes)
43 (constructor StdList StdListCons Nat 0 (constructor StdList StdListEmpty Nat)))
44 (constructor
45 StdList
46 StdListCons
47 (family ResourceEndpoint)
48 (constructor
49 ResourceEndpoint
50 ResourceEndpointOf
51 1
52 b"fixture-engine-1"
53 b"fixture-native"
54 (constructor StdList StdListEmpty Bytes)
55 (constructor
56 StdList
57 StdListCons
58 Nat
59 0
60 (constructor StdList StdListCons Nat 1 (constructor StdList StdListEmpty Nat))))
61 (constructor
62 StdList
63 StdListCons
64 (family ResourceEndpoint)
65 (constructor
66 ResourceEndpoint
67 ResourceEndpointOf
68 2
69 b"fixture-engine-2"
70 b"fixture-native"
71 (constructor StdList StdListEmpty Bytes)
72 (constructor
73 StdList
74 StdListCons
75 Nat
76 0
77 (constructor StdList StdListCons Nat 2 (constructor StdList StdListEmpty Nat))))
78 (constructor StdList StdListEmpty (family ResourceEndpoint)))))
79 (constructor
80 StdList
81 StdListCons
82 (family ResourceDomain)
83 (constructor
84 ResourceDomain
85 ResourceCapacityDomain
86 0
87 b"fixture-memory-0"
88 (constructor ResourceUnit ResourceMemoryBytes)
89 (constructor ResourceFact ResourceEstablished host b"hand-computed-reservation"))
90 (constructor
91 StdList
92 StdListCons
93 (family ResourceDomain)
94 (constructor
95 ResourceDomain
96 ResourceCapacityDomain
97 1
98 b"fixture-memory-1"
99 (constructor ResourceUnit ResourceMemoryBytes)
100 (constructor ResourceFact ResourceEstablished left b"hand-computed-reservation"))
101 (constructor
102 StdList
103 StdListCons
104 (family ResourceDomain)
105 (constructor
106 ResourceDomain
107 ResourceCapacityDomain
108 2
109 b"fixture-memory-2"
110 (constructor ResourceUnit ResourceMemoryBytes)
111 (constructor ResourceFact ResourceEstablished right b"hand-computed-reservation"))
112 (constructor StdList StdListEmpty (family ResourceDomain)))))
113 (constructor StdList StdListEmpty (family ResourceLink))))))
114
115def rpContext =
116 (lambda unrestricted identity : Bytes .
117 (lambda unrestricted gpu : Nat .
118 (lambda unrestricted host : Nat .
119 (lambda unrestricted left : Nat .
120 (lambda unrestricted right : Nat .
121 (constructor
122 NvidiaResourceContext
123 NvidiaResourceContextOf
124 (constructor
125 NativeResourceContext
126 NativeResourceContextOf
127 (constructor
128 ResourceSchedule
129 ResourceScheduleOf
130 (rpGraph host left right)
131 (constructor StdList StdListEmpty (family ResourcePlacement))
132 (constructor StdList StdListEmpty (family ResourceLease)))
133 identity
134 0
135 0
136 4096
137 128
138 16384)
139 gpu
140 gpu
141 4096
142 4096
143 65536))))))
144
145def rpSystem =
146 (constructor NvidiaPlanHostMemory NvidiaPlanHostSystemMemory)
147
148def rpVideo =
149 (constructor NvidiaPlanHostMemory NvidiaPlanHostVideoMemory)
150
151def rpPaged =
152 (constructor NvidiaPlanHostMemory NvidiaPlanHostPagedSystemMemory)
153
154def rpCached =
155 (constructor NvidiaPlanHostMemory NvidiaPlanHostGPUCachedSystemMemory)
156
157def rpBuffer =
158 (lambda unrestricted identity : Bytes .
159 (lambda unrestricted gpu : Nat .
160 (lambda unrestricted host : Nat .
161 (lambda unrestricted extent : Nat .
162 (lambda unrestricted kind : (family NvidiaPlanHostMemory) .
163 (constructor
164 NvidiaPlanHostBuffer
165 NvidiaPlanHostBufferValue
166 identity
167 gpu
168 host
169 extent
170 kind))))))
171
172-- The fixture's 4 KiB ring buffer holds a 512-entry direct-RM ring (8 bytes
173-- an entry); admission refuses a lifecycle whose ring the buffer cannot hold.
174def rpDirectRingEntries : Nat =
175 512
176
177def rpDirect =
178 (lambda unrestricted dataBytes : Nat .
179 (lambda unrestricted errorHost : Nat .
180 (constructor
181 NvidiaPlanHostLayout
182 NvidiaPlanHostLayoutValue
183 (rpBuffer b"ring" 0x10000 0x60010000 4096 rpSystem)
184 (rpBuffer b"push" 0x20000 0x60020000 4096 rpSystem)
185 (rpBuffer b"semaphore" 0x30000 0x60030000 4096 rpSystem)
186 (rpBuffer b"program" 0x40000 0x60040000 4096 rpSystem)
187 (rpBuffer b"qmd" 0x50000 0x60050000 4096 rpSystem)
188 (rpBuffer b"userd" 0x60000 0 4096 rpVideo)
189 (constructor
190 NvidiaPlanHostBuffers
191 NvidiaPlanHostBuffersNext
192 (rpBuffer b"data" 0x80000 0 dataBytes rpVideo)
193 (constructor
194 NvidiaPlanHostBuffers
195 NvidiaPlanHostBuffersNext
196 (rpBuffer b"cached" 0x90000 0 65536 rpCached)
197 (constructor
198 NvidiaPlanHostBuffers
199 NvidiaPlanHostBuffersNext
200 (rpBuffer b"paged" 0xa0000 0x600a0000 8192 rpPaged)
201 (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersEnd))))
202 nvidiaPlanHostAmpere580
203 (constructor NvidiaPlanHostLifecycle NvidiaPlanHostDirectRM rpDirectRingEntries)
204 b"fixture"
205 errorHost)))
206
207-- The UVM channel's GPFIFO buffer: its fixed 0x8000-entry ring and the
208-- USERD page after the entries, which the userd entry aliases (offset
209-- 0x40000 inside; 0x41000 is past the buffer's end).
210def rpUVMRingBytes : Nat =
211 (naturalAdd nvidiaPlanHostUVMGPFIFOBytes nvidiaPlanHostPageBytes)
212
213def rpAliased =
214 (lambda unrestricted dataBytes : Nat .
215 (lambda unrestricted errorHost : Nat .
216 (lambda unrestricted aliasOffset : Nat .
217 (constructor
218 NvidiaPlanHostLayout
219 NvidiaPlanHostLayoutValue
220 (rpBuffer b"ring" 0x10000 0 rpUVMRingBytes rpVideo)
221 (rpBuffer b"push" 0x60000 0x60020000 4096 rpSystem)
222 (rpBuffer b"semaphore" 0x70000 0x60030000 4096 rpSystem)
223 (rpBuffer b"program" 0x80000 0x60040000 4096 rpSystem)
224 (rpBuffer b"qmd" 0x90000 0x60050000 4096 rpSystem)
225 (rpBuffer b"userd" (naturalAdd 0x10000 aliasOffset) 0 4096 rpVideo)
226 (constructor
227 NvidiaPlanHostBuffers
228 NvidiaPlanHostBuffersNext
229 (rpBuffer b"data" 0xa0000 0 dataBytes rpVideo)
230 (constructor
231 NvidiaPlanHostBuffers
232 NvidiaPlanHostBuffersNext
233 (rpBuffer b"cached" 0xb0000 0 65536 rpCached)
234 (constructor
235 NvidiaPlanHostBuffers
236 NvidiaPlanHostBuffersNext
237 (rpBuffer b"paged" 0xc0000 0x600a0000 8192 rpPaged)
238 (constructor NvidiaPlanHostBuffers NvidiaPlanHostBuffersEnd))))
239 nvidiaPlanHostAmpere580
240 (constructor NvidiaPlanHostLifecycle NvidiaPlanHostUVM 65536 1048576)
241 b"fixture"
242 errorHost))))
243
244def rpProgram =
245 (nativePhysicalProgramFromCommands
246 b"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"
247 64
248 2
249 (nativeLaunchRecipeCommand
250 (constructor NativePhysicalOperation NativePhysicalHaltSuccess)
251 b"done"
252 (constructor NativePhysicalCommands NativePhysicalCommandsEnd)))
253
254def rpLeaseAmount =
255 (lambda unrestricted value : (family StdResult (family NativePhysicalMemoryFailure) (family ResourceLease)) .
256 (eliminate
257 StdResult
258 (lambda unrestricted r : (family StdResult (family NativePhysicalMemoryFailure) (family ResourceLease)) .
259 Nat)
260 value
261 (branch StdFailure error . 0)
262 (branch StdSuccess lease . (resourceLeaseAmount lease))))
263
264def rpLeaseTotal =
265 (lambda unrestricted domain : Nat .
266 (lambda unrestricted leases : (family StdResult (family NativePhysicalMemoryFailure) (family StdList (family ResourceLease))) .
267 (eliminate
268 StdResult
269 (lambda unrestricted r : (family StdResult (family NativePhysicalMemoryFailure) (family StdList (family ResourceLease))) .
270 Nat)
271 leases
272 (branch StdFailure error . 0)
273 (branch
274 StdSuccess
275 values
276 .
277 (stdListFold
278 (family ResourceLease)
279 Nat
280 (lambda unrestricted lease : (family ResourceLease) .
281 (lambda unrestricted total : Nat .
282 (naturalAdd
283 (naturalSelect
284 (naturalEqual domain (resourceLeaseDomain lease))
285 (resourceLeaseAmount lease)
286 0)
287 total)))
288 0
289 values)))))
290
291def rpBoth =
292 (lambda unrestricted host : Nat .
293 (lambda unrestricted left : Nat .
294 (lambda unrestricted right : Nat .
295 (lambda unrestricted identity : Bytes .
296 (eliminate
297 StdResult
298 (lambda unrestricted r : (family StdResult (family NativeResourceFailure) (family ResourceSchedule)) .
299 Nat)
300 (admitNvidiaPlanHostResources
301 (rpContext b"first" 1 host left right)
302 (rpDirect 8192 0)
303 rpProgram)
304 (branch StdFailure reason . 0)
305 (branch
306 StdSuccess
307 schedule
308 .
309 (nvidiaPlanHostResourcesAdmitted
310 (nvidiaResourceWithNative
311 (rpContext identity 2 host left right)
312 (nativeResourceContextAddLeases
313 (nvidiaResourceNative (rpContext identity 2 host left right))
314 (resourceScheduleLeases schedule)))
315 (rpDirect 8192 0)
316 rpProgram)))))))
317
318def rpWithStaging =
319 (lambda unrestricted host : Nat .
320 (eliminate
321 StdResult
322 (lambda unrestricted r : (family StdResult (family NativePhysicalMemoryFailure) (family NvidiaResourceContext)) .
323 Nat)
324 (nlsResourceContext (rpContext b"first" 1 host 12288 1048576))
325 (branch StdFailure reason . 0)
326 (branch
327 StdSuccess
328 context
329 .
330 (nvidiaPlanHostResourcesAdmitted context (rpDirect 8192 0) rpProgram))))
331
332def resultdirectLayout =
333 (nvidiaPlanHostLayoutCertified (rpDirect 8192 0) (constructor ArenaResidents ArenaResidentsEnd))
334
335def directLayout : (equal Nat resultdirectLayout 1) =
336 (refl Nat 1)
337
338def resultdirectHostCharge =
339 (rpLeaseTotal
340 0
341 (nvidiaPlanHostResourceLeases (rpContext b"first" 1 1048576 1048576 1048576) (rpDirect 8192 0)))
342
343def directHostCharge : (equal Nat resultdirectHostCharge 163840) =
344 (refl Nat 163840)
345
346def resultdirectVideoCharge =
347 (rpLeaseTotal
348 1
349 (nvidiaPlanHostResourceLeases (rpContext b"first" 1 1048576 1048576 1048576) (rpDirect 8192 0)))
350
351def directVideoCharge : (equal Nat resultdirectVideoCharge 12288) =
352 (refl Nat 12288)
353
354def resultsystemPageCharge =
355 (rpLeaseAmount
356 (nvidiaResourceBufferLease
357 (rpContext b"first" 1 1048576 1048576 1048576)
358 (rpBuffer b"small" 0xb0000 0 1 rpSystem)))
359
360def systemPageCharge : (equal Nat resultsystemPageCharge 4096) =
361 (refl Nat 4096)
362
363def resultpagedSystemCharge =
364 (rpLeaseAmount
365 (nvidiaResourceBufferLease
366 (rpContext b"first" 1 1048576 1048576 1048576)
367 (rpBuffer b"small" 0xb0000 0 1 rpPaged)))
368
369def pagedSystemCharge : (equal Nat resultpagedSystemCharge 4096) =
370 (refl Nat 4096)
371
372def resultcachedSystemCharge =
373 (rpLeaseAmount
374 (nvidiaResourceBufferLease
375 (rpContext b"first" 1 1048576 1048576 1048576)
376 (rpBuffer b"small" 0xb0000 0 1 rpCached)))
377
378def cachedSystemCharge : (equal Nat resultcachedSystemCharge 65536) =
379 (refl Nat 65536)
380
381def resultvideoPageCharge =
382 (rpLeaseAmount
383 (nvidiaResourceBufferLease
384 (rpContext b"first" 1 1048576 1048576 1048576)
385 (rpBuffer b"small" 0xb0000 0 1 rpVideo)))
386
387def videoPageCharge : (equal Nat resultvideoPageCharge 4096) =
388 (refl Nat 4096)
389
390def resultmappedErrorSameCharge =
391 (rpLeaseTotal
392 0
393 (nvidiaPlanHostResourceLeases
394 (rpContext b"first" 1 1048576 1048576 1048576)
395 (rpDirect 8192 0x60150000)))
396
397def mappedErrorSameCharge : (equal Nat resultmappedErrorSameCharge 163840) =
398 (refl Nat 163840)
399
400def resulterrorUnmappedStillCharged =
401 (nvidiaPlanHostResourcesAdmitted
402 (rpContext b"first" 1 163840 12288 1048576)
403 (rpDirect 8192 0)
404 rpProgram)
405
406def errorUnmappedStillCharged : (equal Nat resulterrorUnmappedStillCharged 0) =
407 (refl Nat 0)
408
409def resultexactHostAndVideo =
410 (nvidiaPlanHostResourcesAdmitted
411 (rpContext b"first" 1 167936 12288 1048576)
412 (rpDirect 8192 0)
413 rpProgram)
414
415def exactHostAndVideo : (equal Nat resultexactHostAndVideo 1) =
416 (refl Nat 1)
417
418def resultshortHost =
419 (nvidiaPlanHostResourcesAdmitted
420 (rpContext b"first" 1 167935 12288 1048576)
421 (rpDirect 8192 0)
422 rpProgram)
423
424def shortHost : (equal Nat resultshortHost 0) =
425 (refl Nat 0)
426
427def resultshortVideo =
428 (nvidiaPlanHostResourcesAdmitted
429 (rpContext b"first" 1 167936 12287 1048576)
430 (rpDirect 8192 0)
431 rpProgram)
432
433def shortVideo : (equal Nat resultshortVideo 0) =
434 (refl Nat 0)
435
436def resultlargerDeviceStateRefused =
437 (nvidiaPlanHostResourcesAdmitted
438 (rpContext b"first" 1 1048576 12288 1048576)
439 (rpDirect 12288 0)
440 rpProgram)
441
442def largerDeviceStateRefused : (equal Nat resultlargerDeviceStateRefused 0) =
443 (refl Nat 0)
444
445def resultuvmLayout =
446 (nvidiaPlanHostLayoutCertified
447 (rpAliased 8192 0 0x40000)
448 (constructor ArenaResidents ArenaResidentsEnd))
449
450def uvmLayout : (equal Nat resultuvmLayout 1) =
451 (refl Nat 1)
452
453def resultuvmHostCharge =
454 (rpLeaseTotal
455 0
456 (nvidiaPlanHostResourceLeases
457 (rpContext b"first" 1 1048576 1048576 1048576)
458 (rpAliased 8192 0 0x40000)))
459
460def uvmHostCharge : (equal Nat resultuvmHostCharge 159744) =
461 (refl Nat 159744)
462
463def resultuvmVideoAliasChargedOnce =
464 (rpLeaseTotal
465 1
466 (nvidiaPlanHostResourceLeases
467 (rpContext b"first" 1 1048576 1048576 1048576)
468 (rpAliased 8192 0 0x40000)))
469
470def uvmVideoAliasChargedOnce : (equal Nat resultuvmVideoAliasChargedOnce 274432) =
471 (refl Nat 274432)
472
473def resultuvmExactReservation =
474 (nvidiaPlanHostResourcesAdmitted
475 (rpContext b"first" 1 163840 274432 1048576)
476 (rpAliased 8192 0 0x40000)
477 rpProgram)
478
479def uvmExactReservation : (equal Nat resultuvmExactReservation 1) =
480 (refl Nat 1)
481
482-- one video byte fewer than the ring, its USERD page and the data is refused
483def resultuvmShortVideo =
484 (nvidiaPlanHostResourcesAdmitted
485 (rpContext b"first" 1 163840 274431 1048576)
486 (rpAliased 8192 0 0x40000)
487 rpProgram)
488
489def uvmShortVideo : (equal Nat resultuvmShortVideo 0) =
490 (refl Nat 0)
491
492def resultuvmAliasOutsideRefused =
493 (nvidiaPlanHostResourcesAdmitted
494 (rpContext b"first" 1 1048576 1048576 1048576)
495 (rpAliased 8192 0 0x41000)
496 rpProgram)
497
498def uvmAliasOutsideRefused : (equal Nat resultuvmAliasOutsideRefused 0) =
499 (refl Nat 0)
500
501def resulttwoDevicesExact =
502 (rpBoth 335872 12288 12288 b"second")
503
504def twoDevicesExact : (equal Nat resulttwoDevicesExact 1) =
505 (refl Nat 1)
506
507def resultsharedHostOneByteShort =
508 (rpBoth 335871 12288 12288 b"second")
509
510def sharedHostOneByteShort : (equal Nat resultsharedHostOneByteShort 0) =
511 (refl Nat 0)
512
513def resultfirstCannotBorrowSecondVideo =
514 (rpBoth 1048576 4096 28672 b"second")
515
516def firstCannotBorrowSecondVideo : (equal Nat resultfirstCannotBorrowSecondVideo 0) =
517 (refl Nat 0)
518
519def resultsecondCannotBorrowFirstVideo =
520 (rpBoth 1048576 28672 4096 b"second")
521
522def secondCannotBorrowFirstVideo : (equal Nat resultsecondCannotBorrowFirstVideo 0) =
523 (refl Nat 0)
524
525def resultduplicateAllocationNamesRefused =
526 (rpBoth 1048576 1048576 1048576 b"first")
527
528def duplicateAllocationNamesRefused : (equal Nat resultduplicateAllocationNamesRefused 0) =
529 (refl Nat 0)
530
531def resultzeroMappingRefused =
532 (stdBoolToNatural
533 (stdResultIsSuccess (family NativePhysicalMemoryFailure) Nat (nativeMemoryMappedBytes 4096 0)))
534
535def zeroMappingRefused : (equal Nat resultzeroMappingRefused 0) =
536 (refl Nat 0)
537
538def resultwordRoundingOverflowRefused =
539 (stdBoolToNatural
540 (stdResultIsSuccess
541 (family NativePhysicalMemoryFailure)
542 Nat
543 (nativeMemoryMappedBytes 4096 18446744073709551615)))
544
545def wordRoundingOverflowRefused : (equal Nat resultwordRoundingOverflowRefused 0) =
546 (refl Nat 0)
547
548def resultstagingIncluded =
549 (rpWithStaging 16945152)
550
551def stagingIncluded : (equal Nat resultstagingIncluded 1) =
552 (refl Nat 1)
553
554def resultstagingOneByteShort =
555 (rpWithStaging 16945151)
556
557def stagingOneByteShort : (equal Nat resultstagingOneByteShort 0) =
558 (refl Nat 0)
559
560def observations =
561 (bytes-append
562 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultdirectLayout))
563 (bytes-append
564 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultdirectHostCharge))
565 (bytes-append
566 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultdirectVideoCharge))
567 (bytes-append
568 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultsystemPageCharge))
569 (bytes-append
570 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultpagedSystemCharge))
571 (bytes-append
572 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultcachedSystemCharge))
573 (bytes-append
574 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultvideoPageCharge))
575 (bytes-append
576 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultmappedErrorSameCharge))
577 (bytes-append
578 (dataBytesWord64LE
579 (modelWord64FromNaturalTruncated resulterrorUnmappedStillCharged))
580 (bytes-append
581 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultexactHostAndVideo))
582 (bytes-append
583 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultshortHost))
584 (bytes-append
585 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultshortVideo))
586 (bytes-append
587 (dataBytesWord64LE
588 (modelWord64FromNaturalTruncated resultlargerDeviceStateRefused))
589 (bytes-append
590 (dataBytesWord64LE (modelWord64FromNaturalTruncated resultuvmLayout))
591 (bytes-append
592 (dataBytesWord64LE
593 (modelWord64FromNaturalTruncated resultuvmHostCharge))
594 (bytes-append
595 (dataBytesWord64LE
596 (modelWord64FromNaturalTruncated resultuvmVideoAliasChargedOnce))
597 (bytes-append
598 (dataBytesWord64LE
599 (modelWord64FromNaturalTruncated resultuvmExactReservation))
600 (bytes-append
601 (dataBytesWord64LE
602 (modelWord64FromNaturalTruncated
603 resultuvmAliasOutsideRefused))
604 (bytes-append
605 (dataBytesWord64LE
606 (modelWord64FromNaturalTruncated resulttwoDevicesExact))
607 (bytes-append
608 (dataBytesWord64LE
609 (modelWord64FromNaturalTruncated
610 resultsharedHostOneByteShort))
611 (bytes-append
612 (dataBytesWord64LE
613 (modelWord64FromNaturalTruncated
614 resultfirstCannotBorrowSecondVideo))
615 (bytes-append
616 (dataBytesWord64LE
617 (modelWord64FromNaturalTruncated
618 resultsecondCannotBorrowFirstVideo))
619 (bytes-append
620 (dataBytesWord64LE
621 (modelWord64FromNaturalTruncated
622 resultduplicateAllocationNamesRefused))
623 (bytes-append
624 (dataBytesWord64LE
625 (modelWord64FromNaturalTruncated resultzeroMappingRefused))
626 (bytes-append
627 (dataBytesWord64LE
628 (modelWord64FromNaturalTruncated
629 resultwordRoundingOverflowRefused))
630 (bytes-append
631 (dataBytesWord64LE
632 (modelWord64FromNaturalTruncated resultstagingIncluded))
633 (bytes-append
634 (dataBytesWord64LE
635 (modelWord64FromNaturalTruncated resultstagingOneByteShort))
636 b"")))))))))))))))))))))))))))
637
638def main : Nat =
639 0The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.