1module Runtime.DeviceArenaCertificate
2
3import Hardware.Nvidia.SM86.Command.WholeProgramPlan
4import Model.Parameter
5import Model.Word64
6import Runtime.ArenaCertificate
7import Std.Foundation
8import Std.Natural
9
10-- THE DEVICE SIDE OF AN ARENA: which ranges a whole program's launches read
11-- and write, decided on the launch schedule itself.
12--
13-- A plan names every tensor it places. Some live for the whole program
14-- (the globals: parameter banks, the residual stream); the rest belong to
15-- phases. Each launch carries its phase in its source identity (the
16-- backend never reads that field), and each phase declares its planes:
17-- fresh ones (written in the phase before they are read) and carried ones
18-- (holding a value an earlier phase left). Planes of different phases may
19-- share bytes -- that is how a workspace is reused -- and the certificate
20-- decides that the sharing is sound:
21-- (A) the globals are aligned, non-empty and pairwise disjoint;
22-- (B) each phase's planes are aligned, non-empty, pairwise disjoint and
23-- disjoint from the globals: two tensors live in one phase never
24-- share a byte;
25-- (C) every parameter word of every launch that lies in one of the
26-- plan's address windows lies in a plane of the launch's phase or in
27-- a global: no launch reaches memory its phase did not name. A
28-- repeat is not unrolled: each launch of its body stands for all its
29-- iterations, each word with intervals covering its values over them
30-- (the iteration's deltas, or its table frames, applied to the
31-- ordinals the launch stands for: an interval per iteration while
32-- they are few and one delta names the word, their hull otherwise);
33-- a word each of whose intervals lies in one named range lies in a
34-- named range at every iteration;
35-- (D) in the order the launches run -- the submission schedule's
36-- references, in order, each a range of the launch table -- a carried
37-- plane was declared, in the same place, by an earlier phase instance
38-- (a maximal run of executed launches of one phase), and no instance
39-- since declared a different plane over any of its bytes: no value is
40-- overwritten while a later phase still needs it.
41-- What it trusts is each phase's fresh/carried split; everything else is
42-- derived from the schedule.
43--
44-- The verdict is 0 when certified; 1 when (A) or (B) fails; 2 + i when
45-- the i-th launch as written (counted from 0, a repeat's body once) breaks
46-- (C) -- a word in no named range, or a launch of no declared phase; 2 + n
47-- + k (n the launches as written) when the k-th executed instance breaks
48-- (D).
49family DeviceArenaPhase : Type 0
50constructor DeviceArenaPhaseValue
51field unrestricted deviceArenaPhaseIdentity : Bytes
52field unrestricted deviceArenaPhaseFresh : (family ArenaResidents)
53field unrestricted deviceArenaPhaseCarried : (family ArenaResidents)
54
55end-family
56
57family DeviceArenaPhases : Type 0
58constructor DeviceArenaPhasesEnd
59constructor DeviceArenaPhasesNext
60field unrestricted deviceArenaPhasesHead : (family DeviceArenaPhase)
61recursive unrestricted deviceArenaPhasesTail
62
63end-family
64
65-- a launch as the certificate sees it: its phase, the ordinals of the
66-- expanded schedule it stands for (base + the sum of k * stride over its
67-- generators, 0 <= k < count, outermost first), and, for each parameter
68-- word, intervals covering every value the word takes over them -- one per
69-- iteration of an enclosing repeat while few, their hull beyond that --
70-- with what an enclosing repeat is accumulating: the sums of the positive
71-- and negative deltas naming the word, whether they are one delta naming
72-- each of its ordinals at most once, that delta, and those ordinals
73family DeviceArenaIntervals : Type 0
74constructor DeviceArenaIntervalsEnd
75constructor DeviceArenaIntervalsNext
76field unrestricted deviceArenaIntervalLow : Nat
77field unrestricted deviceArenaIntervalHigh : Nat
78recursive unrestricted deviceArenaIntervalsTail
79
80end-family
81
82family DeviceArenaOrdinals : Type 0
83constructor DeviceArenaOrdinalsEnd
84constructor DeviceArenaOrdinalsNext
85field unrestricted deviceArenaOrdinal : Nat
86recursive unrestricted deviceArenaOrdinalsTail
87
88end-family
89
90family DeviceArenaSpans : Type 0
91constructor DeviceArenaSpansEnd
92constructor DeviceArenaSpansNext
93field unrestricted deviceArenaSpanOffset : Nat
94field unrestricted deviceArenaSpanIntervals : (family DeviceArenaIntervals)
95field unrestricted deviceArenaSpanRise : Nat
96field unrestricted deviceArenaSpanFall : Nat
97field unrestricted deviceArenaSpanUniform : Nat
98field unrestricted deviceArenaSpanDelta : Nat
99field unrestricted deviceArenaSpanOrdinals : (family DeviceArenaOrdinals)
100recursive unrestricted deviceArenaSpansTail
101
102end-family
103
104family DeviceArenaGenerators : Type 0
105constructor DeviceArenaGeneratorsEnd
106constructor DeviceArenaGeneratorsNext
107field unrestricted deviceArenaGeneratorStride : Nat
108field unrestricted deviceArenaGeneratorCount : Nat
109recursive unrestricted deviceArenaGeneratorsTail
110
111end-family
112
113family DeviceArenaLaunch : Type 0
114constructor DeviceArenaLaunchValue
115field unrestricted deviceArenaLaunchIdentity : Bytes
116field unrestricted deviceArenaLaunchBase : Nat
117field unrestricted deviceArenaLaunchGenerators : (family DeviceArenaGenerators)
118field unrestricted deviceArenaLaunchSpans : (family DeviceArenaSpans)
119
120end-family
121
122family DeviceArenaLaunches : Type 0
123constructor DeviceArenaLaunchesEnd
124constructor DeviceArenaLaunchesNext
125field unrestricted deviceArenaLaunchesHead : (family DeviceArenaLaunch)
126recursive unrestricted deviceArenaLaunchesTail
127
128end-family
129
130-- the planes (D) tracks: each with whether a different plane has been
131-- declared over it since it was last declared
132family DeviceArenaTracked : Type 0
133constructor DeviceArenaTrackedEnd
134constructor DeviceArenaTrackedNext
135field unrestricted deviceArenaTrackedResident : (family ArenaResident)
136field unrestricted deviceArenaTrackedClobbered : Nat
137recursive unrestricted deviceArenaTrackedTail
138
139end-family
140
141-- ---- the order the launches run ----
142-- the launch table as runs of one phase: identity, first launch, count
143family DeviceArenaRuns : Type 0
144constructor DeviceArenaRunsEnd
145constructor DeviceArenaRunsNext
146field unrestricted deviceArenaRunIdentity : Bytes
147field unrestricted deviceArenaRunFirst : Nat
148field unrestricted deviceArenaRunCount : Nat
149recursive unrestricted deviceArenaRunsTail
150
151end-family
152
153-- the executed instances: phase identities in the order they run
154family DeviceArenaInstances : Type 0
155constructor DeviceArenaInstancesEnd
156constructor DeviceArenaInstancesNext
157field unrestricted deviceArenaInstanceIdentity : Bytes
158recursive unrestricted deviceArenaInstancesTail
159
160end-family
161
162-- ---- words modulo 2^64 (the build's naturals are 64-bit words) ----
163def deviceArenaWordMaximum : Nat =
164 18446744073709551615
165
166-- a + b modulo 2^64; both arms are evaluated, so neither may overflow
167def deviceArenaAddModulo =
168 (lambda unrestricted a : Nat .
169 (lambda unrestricted b : Nat .
170 (let unrestricted room =
171 (naturalSaturatingSubtract deviceArenaWordMaximum a)
172 in
173 (naturalSelect
174 (naturalLess room b)
175 (naturalSaturatingSubtract (naturalSaturatingSubtract b room) 1)
176 (naturalAdd a (naturalSelect (naturalLess room b) room b))))))
177
178-- ---- residents ----
179def deviceArenaResidentIdentity =
180 (lambda unrestricted resident : (family ArenaResident) .
181 (eliminate
182 ArenaResident
183 (lambda unrestricted current : (family ArenaResident) . Bytes)
184 resident
185 (branch ArenaResidentValue identity offset extent alignment . identity)))
186
187def deviceArenaContains =
188 (lambda unrestricted resident : (family ArenaResident) .
189 (lambda unrestricted address : Nat .
190 (naturalAnd
191 (naturalLessOrEqual (arenaResidentOffsetOf resident) address)
192 (naturalLess address (arenaResidentEndOf resident)))))
193
194def deviceArenaAnyContains =
195 (lambda unrestricted residents : (family ArenaResidents) .
196 (lambda unrestricted address : Nat .
197 (eliminate
198 ArenaResidents
199 (lambda unrestricted current : (family ArenaResidents) . Nat)
200 residents
201 (branch ArenaResidentsEnd . 0)
202 (branch
203 ArenaResidentsNext
204 head
205 tail
206 induction
207 .
208 (naturalOr (deviceArenaContains head address) induction)))))
209
210def deviceArenaAppend =
211 (lambda unrestricted left : (family ArenaResidents) .
212 (lambda unrestricted right : (family ArenaResidents) .
213 (eliminate
214 ArenaResidents
215 (lambda unrestricted current : (family ArenaResidents) . (family ArenaResidents))
216 left
217 (branch ArenaResidentsEnd . right)
218 (branch
219 ArenaResidentsNext
220 head
221 tail
222 induction
223 .
224 (constructor ArenaResidents ArenaResidentsNext head induction)))))
225
226-- a different plane over any byte of `resident`
227def deviceArenaOverlapsOther =
228 (lambda unrestricted resident : (family ArenaResident) .
229 (lambda unrestricted residents : (family ArenaResidents) .
230 (eliminate
231 ArenaResidents
232 (lambda unrestricted current : (family ArenaResidents) . Nat)
233 residents
234 (branch ArenaResidentsEnd . 0)
235 (branch
236 ArenaResidentsNext
237 head
238 tail
239 induction
240 .
241 (naturalOr
242 (naturalAnd
243 (naturalIsZero
244 (bytes-equal
245 (deviceArenaResidentIdentity head)
246 (deviceArenaResidentIdentity resident)))
247 (naturalIsZero (arenaDisjoint head resident)))
248 induction)))))
249
250-- ---- phases ----
251def deviceArenaPhaseIdentityOf =
252 (lambda unrestricted phase : (family DeviceArenaPhase) .
253 (eliminate
254 DeviceArenaPhase
255 (lambda unrestricted current : (family DeviceArenaPhase) . Bytes)
256 phase
257 (branch DeviceArenaPhaseValue identity fresh carried . identity)))
258
259def deviceArenaPhaseFreshOf =
260 (lambda unrestricted phase : (family DeviceArenaPhase) .
261 (eliminate
262 DeviceArenaPhase
263 (lambda unrestricted current : (family DeviceArenaPhase) . (family ArenaResidents))
264 phase
265 (branch DeviceArenaPhaseValue identity fresh carried . fresh)))
266
267def deviceArenaPhaseCarriedOf =
268 (lambda unrestricted phase : (family DeviceArenaPhase) .
269 (eliminate
270 DeviceArenaPhase
271 (lambda unrestricted current : (family DeviceArenaPhase) . (family ArenaResidents))
272 phase
273 (branch DeviceArenaPhaseValue identity fresh carried . carried)))
274
275def deviceArenaPhasePlanes =
276 (lambda unrestricted phase : (family DeviceArenaPhase) .
277 (deviceArenaAppend (deviceArenaPhaseFreshOf phase) (deviceArenaPhaseCarriedOf phase)))
278
279-- 1 when a phase of this identity is declared
280def deviceArenaPhaseKnown =
281 (lambda unrestricted phases : (family DeviceArenaPhases) .
282 (lambda unrestricted identity : Bytes .
283 (eliminate
284 DeviceArenaPhases
285 (lambda unrestricted current : (family DeviceArenaPhases) . Nat)
286 phases
287 (branch DeviceArenaPhasesEnd . 0)
288 (branch
289 DeviceArenaPhasesNext
290 head
291 tail
292 induction
293 .
294 (naturalOr (bytes-equal (deviceArenaPhaseIdentityOf head) identity) induction)))))
295
296-- the phase of this identity (the first declared; an unknown identity gets
297-- the empty phase, which the caller has refused already)
298def deviceArenaPhaseOf =
299 (lambda unrestricted phases : (family DeviceArenaPhases) .
300 (lambda unrestricted identity : Bytes .
301 (eliminate
302 DeviceArenaPhases
303 (lambda unrestricted current : (family DeviceArenaPhases) . (family DeviceArenaPhase))
304 phases
305 (branch
306 DeviceArenaPhasesEnd
307 .
308 (constructor
309 DeviceArenaPhase
310 DeviceArenaPhaseValue
311 identity
312 (constructor ArenaResidents ArenaResidentsEnd)
313 (constructor ArenaResidents ArenaResidentsEnd)))
314 (branch
315 DeviceArenaPhasesNext
316 head
317 tail
318 induction
319 .
320 (nat-eliminate
321 (lambda unrestricted found : Nat . (family DeviceArenaPhase))
322 induction
323 (lambda unrestricted p : Nat .
324 (lambda unrestricted ignored : (family DeviceArenaPhase) . head))
325 (bytes-equal (deviceArenaPhaseIdentityOf head) identity))))))
326
327-- (A) and (B): 1 when the globals and every phase's planes are placed
328def deviceArenaPlaced =
329 (lambda unrestricted globals : (family ArenaResidents) .
330 (lambda unrestricted phases : (family DeviceArenaPhases) .
331 (naturalAnd
332 (arenaCertificate deviceArenaWordMaximum globals)
333 (eliminate
334 DeviceArenaPhases
335 (lambda unrestricted current : (family DeviceArenaPhases) . Nat)
336 phases
337 (branch DeviceArenaPhasesEnd . 1)
338 (branch
339 DeviceArenaPhasesNext
340 head
341 tail
342 induction
343 .
344 (naturalAnd
345 (arenaCertificate
346 deviceArenaWordMaximum
347 (deviceArenaAppend (deviceArenaPhasePlanes head) globals))
348 induction))))))
349
350-- ---- saturating words ----
351def deviceArenaSaturatingAdd =
352 (lambda unrestricted a : Nat .
353 (lambda unrestricted b : Nat .
354 (naturalAdd
355 a
356 (naturalSelect
357 (naturalLess (naturalSaturatingSubtract deviceArenaWordMaximum a) b)
358 (naturalSaturatingSubtract deviceArenaWordMaximum a)
359 b))))
360
361def deviceArenaSaturatingMultiply =
362 (lambda unrestricted a : Nat .
363 (lambda unrestricted b : Nat .
364 (let unrestricted room =
365 (naturalDivideUnchecked deviceArenaWordMaximum a)
366 in
367 (naturalMultiply a (naturalSelect (naturalLess room b) room b)))))
368
369-- a delta word read as signed: the rise (below 2^63) or the fall (2^64 - d)
370def deviceArenaNegative =
371 (lambda unrestricted delta : Nat .
372 (naturalLess (naturalDivideUnchecked deviceArenaWordMaximum 2) delta))
373
374def deviceArenaRise =
375 (lambda unrestricted delta : Nat . (naturalSelect (deviceArenaNegative delta) 0 delta))
376
377def deviceArenaFall =
378 (lambda unrestricted delta : Nat .
379 (naturalSelect
380 (deviceArenaNegative delta)
381 (deviceArenaSaturatingAdd (naturalSaturatingSubtract deviceArenaWordMaximum delta) 1)
382 0))
383
384-- ---- the schedule as written ----
385def deviceArenaSpansOf =
386 (lambda unrestricted patches : (family NvidiaParameterPatches) .
387 (eliminate
388 NvidiaParameterPatches
389 (lambda unrestricted current : (family NvidiaParameterPatches) . (family DeviceArenaSpans))
390 patches
391 (branch NvidiaParameterPatchesEnd . (constructor DeviceArenaSpans DeviceArenaSpansEnd))
392 (branch
393 NvidiaParameterPatchesNext
394 head
395 tail
396 induction
397 .
398 (eliminate
399 NvidiaParameterPatch
400 (lambda unrestricted current : (family NvidiaParameterPatch) . (family DeviceArenaSpans))
401 head
402 (branch
403 NvidiaParameterPatchValue
404 offset
405 value
406 .
407 (let unrestricted word =
408 (modelWord64Natural value)
409 in
410 (constructor
411 DeviceArenaSpans
412 DeviceArenaSpansNext
413 offset
414 (constructor
415 DeviceArenaIntervals
416 DeviceArenaIntervalsNext
417 word
418 word
419 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd))
420 0
421 0
422 1
423 0
424 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd)
425 induction)))))))
426
427def deviceArenaLaunchOf =
428 (lambda unrestricted template : (family NvidiaLaunchTemplate) .
429 (eliminate
430 NvidiaLaunchTemplate
431 (lambda unrestricted current : (family NvidiaLaunchTemplate) . (family DeviceArenaLaunch))
432 template
433 (branch
434 NvidiaLaunchTemplateValue
435 identity
436 kernel
437 block
438 .
439 (eliminate
440 NvidiaParameterBlock
441 (lambda unrestricted current : (family NvidiaParameterBlock) . (family DeviceArenaLaunch))
442 block
443 (branch
444 NvidiaParameterBlockValue
445 patches
446 .
447 (constructor
448 DeviceArenaLaunch
449 DeviceArenaLaunchValue
450 identity
451 0
452 (constructor DeviceArenaGenerators DeviceArenaGeneratorsEnd)
453 (deviceArenaSpansOf patches)))))))
454
455def deviceArenaLaunchIdentityOf =
456 (lambda unrestricted launch : (family DeviceArenaLaunch) .
457 (eliminate
458 DeviceArenaLaunch
459 (lambda unrestricted current : (family DeviceArenaLaunch) . Bytes)
460 launch
461 (branch DeviceArenaLaunchValue identity base generators spans . identity)))
462
463def deviceArenaLaunchSpansOf =
464 (lambda unrestricted launch : (family DeviceArenaLaunch) .
465 (eliminate
466 DeviceArenaLaunch
467 (lambda unrestricted current : (family DeviceArenaLaunch) . (family DeviceArenaSpans))
468 launch
469 (branch DeviceArenaLaunchValue identity base generators spans . spans)))
470
471def deviceArenaAppendLaunches =
472 (lambda unrestricted left : (family DeviceArenaLaunches) .
473 (lambda unrestricted right : (family DeviceArenaLaunches) .
474 (eliminate
475 DeviceArenaLaunches
476 (lambda unrestricted current : (family DeviceArenaLaunches) . (family DeviceArenaLaunches))
477 left
478 (branch DeviceArenaLaunchesEnd . right)
479 (branch
480 DeviceArenaLaunchesNext
481 head
482 tail
483 induction
484 .
485 (constructor DeviceArenaLaunches DeviceArenaLaunchesNext head induction)))))
486
487-- each launch moved `shift` ordinals on (a later part of a sequence)
488def deviceArenaShift =
489 (lambda unrestricted shift : Nat .
490 (lambda unrestricted launches : (family DeviceArenaLaunches) .
491 (eliminate
492 DeviceArenaLaunches
493 (lambda unrestricted current : (family DeviceArenaLaunches) . (family DeviceArenaLaunches))
494 launches
495 (branch DeviceArenaLaunchesEnd . (constructor DeviceArenaLaunches DeviceArenaLaunchesEnd))
496 (branch
497 DeviceArenaLaunchesNext
498 head
499 tail
500 induction
501 .
502 (constructor
503 DeviceArenaLaunches
504 DeviceArenaLaunchesNext
505 (eliminate
506 DeviceArenaLaunch
507 (lambda unrestricted current : (family DeviceArenaLaunch) .
508 (family DeviceArenaLaunch))
509 head
510 (branch
511 DeviceArenaLaunchValue
512 identity
513 base
514 generators
515 spans
516 .
517 (constructor
518 DeviceArenaLaunch
519 DeviceArenaLaunchValue
520 identity
521 (naturalAdd base shift)
522 generators
523 spans)))
524 induction)))))
525
526-- 1 when ordinal `b` is one the launch stands for: the generators are
527-- nested (each stride is at least the extent of those inside it), so the
528-- decomposition is greedy
529def deviceArenaGenerated =
530 (lambda unrestricted base : Nat .
531 (lambda unrestricted generators : (family DeviceArenaGenerators) .
532 (lambda unrestricted b : Nat .
533 (naturalAnd
534 (naturalLessOrEqual base b)
535 (app
536 (eliminate
537 DeviceArenaGenerators
538 (lambda unrestricted current : (family DeviceArenaGenerators) .
539 (pi unrestricted rest : Nat . Nat))
540 generators
541 (branch
542 DeviceArenaGeneratorsEnd
543 .
544 (lambda unrestricted rest : Nat . (naturalIsZero rest)))
545 (branch
546 DeviceArenaGeneratorsNext
547 stride
548 count
549 tail
550 induction
551 .
552 (lambda unrestricted rest : Nat .
553 (naturalAnd
554 (naturalLess (naturalDivideUnchecked rest stride) count)
555 (induction (naturalModuloUnchecked rest stride))))))
556 (naturalSaturatingSubtract b base))))))
557
558def deviceArenaOrdinalsEmpty =
559 (lambda unrestricted ordinals : (family DeviceArenaOrdinals) .
560 (eliminate
561 DeviceArenaOrdinals
562 (lambda unrestricted current : (family DeviceArenaOrdinals) . Nat)
563 ordinals
564 (branch DeviceArenaOrdinalsEnd . 1)
565 (branch DeviceArenaOrdinalsNext ordinal tail induction . 0)))
566
567def deviceArenaOrdinalsHas =
568 (lambda unrestricted ordinals : (family DeviceArenaOrdinals) .
569 (lambda unrestricted wanted : Nat .
570 (eliminate
571 DeviceArenaOrdinals
572 (lambda unrestricted current : (family DeviceArenaOrdinals) . Nat)
573 ordinals
574 (branch DeviceArenaOrdinalsEnd . 0)
575 (branch
576 DeviceArenaOrdinalsNext
577 ordinal
578 tail
579 induction
580 .
581 (naturalOr (naturalEqual ordinal wanted) induction)))))
582
583def deviceArenaOrdinalsCount =
584 (lambda unrestricted ordinals : (family DeviceArenaOrdinals) .
585 (eliminate
586 DeviceArenaOrdinals
587 (lambda unrestricted current : (family DeviceArenaOrdinals) . Nat)
588 ordinals
589 (branch DeviceArenaOrdinalsEnd . 0)
590 (branch DeviceArenaOrdinalsNext ordinal tail induction . (succ induction))))
591
592-- a delta accumulated on the word at `offset` (a word the block does not
593-- patch is zero)
594def deviceArenaAccumulate =
595 (lambda unrestricted ordinal : Nat .
596 (lambda unrestricted offset : Nat .
597 (lambda unrestricted delta : Nat .
598 (lambda unrestricted spans : (family DeviceArenaSpans) .
599 (eliminate
600 DeviceArenaSpans
601 (lambda unrestricted current : (family DeviceArenaSpans) . (family DeviceArenaSpans))
602 spans
603 (branch
604 DeviceArenaSpansEnd
605 .
606 (constructor
607 DeviceArenaSpans
608 DeviceArenaSpansNext
609 offset
610 (constructor
611 DeviceArenaIntervals
612 DeviceArenaIntervalsNext
613 0
614 0
615 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd))
616 (deviceArenaRise delta)
617 (deviceArenaFall delta)
618 (naturalLess ordinal deviceArenaWordMaximum)
619 delta
620 (constructor
621 DeviceArenaOrdinals
622 DeviceArenaOrdinalsNext
623 ordinal
624 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd))
625 spans))
626 (branch
627 DeviceArenaSpansNext
628 at
629 intervals
630 rise
631 fall
632 uniform
633 last
634 ordinals
635 tail
636 induction
637 .
638 (nat-eliminate
639 (lambda unrestricted same : Nat . (family DeviceArenaSpans))
640 (constructor
641 DeviceArenaSpans
642 DeviceArenaSpansNext
643 at
644 intervals
645 rise
646 fall
647 uniform
648 last
649 ordinals
650 induction)
651 (lambda unrestricted q : Nat .
652 (lambda unrestricted ignored : (family DeviceArenaSpans) .
653 (let unrestricted first =
654 (deviceArenaOrdinalsEmpty ordinals)
655 in
656 (constructor
657 DeviceArenaSpans
658 DeviceArenaSpansNext
659 at
660 intervals
661 (deviceArenaSaturatingAdd rise (deviceArenaRise delta))
662 (deviceArenaSaturatingAdd fall (deviceArenaFall delta))
663 (naturalAnd
664 uniform
665 (naturalAnd
666 (naturalLess ordinal deviceArenaWordMaximum)
667 (naturalOr
668 first
669 (naturalAnd
670 (naturalEqual delta last)
671 (naturalIsZero (deviceArenaOrdinalsHas ordinals ordinal))))))
672 delta
673 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsNext ordinal ordinals)
674 tail))))
675 (naturalEqual at offset))))))))
676
677-- a frame's exact value taken into the word's span
678def deviceArenaInclude =
679 (lambda unrestricted ordinal : Nat .
680 (lambda unrestricted offset : Nat .
681 (lambda unrestricted value : Nat .
682 (lambda unrestricted spans : (family DeviceArenaSpans) .
683 (eliminate
684 DeviceArenaSpans
685 (lambda unrestricted current : (family DeviceArenaSpans) . (family DeviceArenaSpans))
686 spans
687 (branch
688 DeviceArenaSpansEnd
689 .
690 (constructor
691 DeviceArenaSpans
692 DeviceArenaSpansNext
693 offset
694 (constructor
695 DeviceArenaIntervals
696 DeviceArenaIntervalsNext
697 0
698 0
699 (constructor
700 DeviceArenaIntervals
701 DeviceArenaIntervalsNext
702 value
703 value
704 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd)))
705 0
706 0
707 1
708 0
709 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd)
710 spans))
711 (branch
712 DeviceArenaSpansNext
713 at
714 intervals
715 rise
716 fall
717 uniform
718 last
719 ordinals
720 tail
721 induction
722 .
723 (nat-eliminate
724 (lambda unrestricted same : Nat . (family DeviceArenaSpans))
725 (constructor
726 DeviceArenaSpans
727 DeviceArenaSpansNext
728 at
729 intervals
730 rise
731 fall
732 uniform
733 last
734 ordinals
735 induction)
736 (lambda unrestricted q : Nat .
737 (lambda unrestricted ignored : (family DeviceArenaSpans) .
738 (constructor
739 DeviceArenaSpans
740 DeviceArenaSpansNext
741 at
742 (constructor
743 DeviceArenaIntervals
744 DeviceArenaIntervalsNext
745 value
746 value
747 intervals)
748 rise
749 fall
750 uniform
751 last
752 ordinals
753 tail)))
754 (naturalEqual at offset))))))))
755
756def deviceArenaIntervalCount =
757 (lambda unrestricted intervals : (family DeviceArenaIntervals) .
758 (eliminate
759 DeviceArenaIntervals
760 (lambda unrestricted current : (family DeviceArenaIntervals) . Nat)
761 intervals
762 (branch DeviceArenaIntervalsEnd . 0)
763 (branch DeviceArenaIntervalsNext low high tail induction . (succ induction))))
764
765def deviceArenaLowest =
766 (lambda unrestricted intervals : (family DeviceArenaIntervals) .
767 (eliminate
768 DeviceArenaIntervals
769 (lambda unrestricted current : (family DeviceArenaIntervals) . Nat)
770 intervals
771 (branch DeviceArenaIntervalsEnd . deviceArenaWordMaximum)
772 (branch
773 DeviceArenaIntervalsNext
774 low
775 high
776 tail
777 induction
778 .
779 (naturalSelect (naturalLess low induction) low induction))))
780
781def deviceArenaHighest =
782 (lambda unrestricted intervals : (family DeviceArenaIntervals) .
783 (eliminate
784 DeviceArenaIntervals
785 (lambda unrestricted current : (family DeviceArenaIntervals) . Nat)
786 intervals
787 (branch DeviceArenaIntervalsEnd . 0)
788 (branch
789 DeviceArenaIntervalsNext
790 low
791 high
792 tail
793 induction
794 .
795 (naturalSelect (naturalLess induction high) high induction))))
796
797-- every interval moved by `delta` (modulo 2^64), then `rest`
798def deviceArenaMoved =
799 (lambda unrestricted delta : Nat .
800 (lambda unrestricted intervals : (family DeviceArenaIntervals) .
801 (lambda unrestricted rest : (family DeviceArenaIntervals) .
802 (eliminate
803 DeviceArenaIntervals
804 (lambda unrestricted current : (family DeviceArenaIntervals) .
805 (family DeviceArenaIntervals))
806 intervals
807 (branch DeviceArenaIntervalsEnd . rest)
808 (branch
809 DeviceArenaIntervalsNext
810 low
811 high
812 tail
813 induction
814 .
815 (constructor
816 DeviceArenaIntervals
817 DeviceArenaIntervalsNext
818 (deviceArenaAddModulo low delta)
819 (deviceArenaAddModulo high delta)
820 induction))))))
821
822-- the intervals of `count` iterations, each the previous moved by `delta`
823def deviceArenaIterations =
824 (lambda unrestricted count : Nat .
825 (lambda unrestricted delta : Nat .
826 (lambda unrestricted intervals : (family DeviceArenaIntervals) .
827 (app
828 (nat-eliminate
829 (lambda unrestricted remaining : Nat .
830 (pi unrestricted current : (family DeviceArenaIntervals) .
831 (family DeviceArenaIntervals)))
832 (lambda unrestricted current : (family DeviceArenaIntervals) .
833 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd))
834 (lambda unrestricted p : Nat .
835 (lambda unrestricted induction : (pi unrestricted current : (family DeviceArenaIntervals) . (family DeviceArenaIntervals)) .
836 (lambda unrestricted current : (family DeviceArenaIntervals) .
837 (deviceArenaMoved
838 0
839 current
840 (induction
841 (deviceArenaMoved
842 delta
843 current
844 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd)))))))
845 count)
846 intervals))))
847
848-- iterations kept apart while there are at most this many intervals
849def deviceArenaExactIntervals : Nat =
850 64
851
852-- the accumulated deltas applied `steps` times: each span widened to
853-- cover every iteration
854def deviceArenaWiden =
855 (lambda unrestricted steps : Nat .
856 (lambda unrestricted stands : Nat .
857 (lambda unrestricted spans : (family DeviceArenaSpans) .
858 (eliminate
859 DeviceArenaSpans
860 (lambda unrestricted current : (family DeviceArenaSpans) . (family DeviceArenaSpans))
861 spans
862 (branch DeviceArenaSpansEnd . (constructor DeviceArenaSpans DeviceArenaSpansEnd))
863 (branch
864 DeviceArenaSpansNext
865 at
866 intervals
867 rise
868 fall
869 uniform
870 last
871 ordinals
872 tail
873 induction
874 .
875 (let unrestricted hull =
876 (constructor
877 DeviceArenaIntervals
878 DeviceArenaIntervalsNext
879 (naturalSaturatingSubtract
880 (deviceArenaLowest intervals)
881 (deviceArenaSaturatingMultiply steps fall))
882 (deviceArenaSaturatingAdd
883 (deviceArenaHighest intervals)
884 (deviceArenaSaturatingMultiply steps rise))
885 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd))
886 in
887 (let unrestricted exact =
888 (naturalAnd
889 uniform
890 (naturalAnd
891 (naturalEqual (deviceArenaOrdinalsCount ordinals) stands)
892 (naturalLessOrEqual
893 (deviceArenaSaturatingMultiply
894 (succ steps)
895 (deviceArenaIntervalCount intervals))
896 deviceArenaExactIntervals)))
897 in
898 (constructor
899 DeviceArenaSpans
900 DeviceArenaSpansNext
901 at
902 (nat-eliminate
903 (lambda unrestricted adjusted : Nat . (family DeviceArenaIntervals))
904 intervals
905 (lambda unrestricted q : Nat .
906 (lambda unrestricted ignored : (family DeviceArenaIntervals) .
907 (nat-eliminate
908 (lambda unrestricted apart : Nat . (family DeviceArenaIntervals))
909 hull
910 (lambda unrestricted r : Nat .
911 (lambda unrestricted unused : (family DeviceArenaIntervals) .
912 (deviceArenaIterations (succ steps) last intervals)))
913 exact)))
914 (naturalIsZero (deviceArenaOrdinalsEmpty ordinals)))
915 0
916 0
917 1
918 0
919 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd)
920 induction))))))))
921
922-- the adjustments naming a launch (by one of its ordinals, or all blocks)
923-- folded into its spans by `step`
924def deviceArenaFold =
925 (lambda unrestricted step : (pi unrestricted ordinal : Nat . (pi unrestricted offset : Nat . (pi unrestricted value : Nat . (pi unrestricted spans : (family DeviceArenaSpans) . (family DeviceArenaSpans))))) .
926 (lambda unrestricted adjustments : (family NvidiaParameterAdjustments) .
927 (lambda unrestricted launch : (family DeviceArenaLaunch) .
928 (eliminate
929 DeviceArenaLaunch
930 (lambda unrestricted current : (family DeviceArenaLaunch) . (family DeviceArenaLaunch))
931 launch
932 (branch
933 DeviceArenaLaunchValue
934 identity
935 base
936 generators
937 spans
938 .
939 (constructor
940 DeviceArenaLaunch
941 DeviceArenaLaunchValue
942 identity
943 base
944 generators
945 (eliminate
946 NvidiaParameterAdjustments
947 (lambda unrestricted current : (family NvidiaParameterAdjustments) .
948 (family DeviceArenaSpans))
949 adjustments
950 (branch NvidiaParameterAdjustmentsEnd . spans)
951 (branch
952 NvidiaParameterAdjustmentsNext
953 head
954 tail
955 induction
956 .
957 (eliminate
958 NvidiaParameterAdjustment
959 (lambda unrestricted current : (family NvidiaParameterAdjustment) .
960 (family DeviceArenaSpans))
961 head
962 (branch
963 NvidiaParameterAdjustmentValue
964 scope
965 offset
966 value
967 .
968 (nat-eliminate
969 (lambda unrestricted applies : Nat . (family DeviceArenaSpans))
970 induction
971 (lambda unrestricted q : Nat .
972 (lambda unrestricted ignored : (family DeviceArenaSpans) .
973 (step
974 (eliminate
975 NvidiaParameterAdjustmentScope
976 (lambda unrestricted current : (family NvidiaParameterAdjustmentScope) .
977 Nat)
978 scope
979 (branch NvidiaParameterAdjustmentAllBlocks . deviceArenaWordMaximum)
980 (branch NvidiaParameterAdjustmentBlock at . at))
981 offset
982 (modelWord64Natural value)
983 induction)))
984 (eliminate
985 NvidiaParameterAdjustmentScope
986 (lambda unrestricted current : (family NvidiaParameterAdjustmentScope) .
987 Nat)
988 scope
989 (branch NvidiaParameterAdjustmentAllBlocks . 1)
990 (branch
991 NvidiaParameterAdjustmentBlock
992 at
993 .
994 (deviceArenaGenerated base generators at))))))))))))))
995
996def deviceArenaMapLaunches =
997 (lambda unrestricted f : (pi unrestricted launch : (family DeviceArenaLaunch) . (family DeviceArenaLaunch)) .
998 (lambda unrestricted launches : (family DeviceArenaLaunches) .
999 (eliminate
1000 DeviceArenaLaunches
1001 (lambda unrestricted current : (family DeviceArenaLaunches) . (family DeviceArenaLaunches))
1002 launches
1003 (branch DeviceArenaLaunchesEnd . (constructor DeviceArenaLaunches DeviceArenaLaunchesEnd))
1004 (branch
1005 DeviceArenaLaunchesNext
1006 head
1007 tail
1008 induction
1009 .
1010 (constructor DeviceArenaLaunches DeviceArenaLaunchesNext (f head) induction)))))
1011
1012-- how many ordinals a launch stands for
1013def deviceArenaStands =
1014 (lambda unrestricted generators : (family DeviceArenaGenerators) .
1015 (eliminate
1016 DeviceArenaGenerators
1017 (lambda unrestricted current : (family DeviceArenaGenerators) . Nat)
1018 generators
1019 (branch DeviceArenaGeneratorsEnd . 1)
1020 (branch
1021 DeviceArenaGeneratorsNext
1022 stride
1023 count
1024 tail
1025 induction
1026 .
1027 (naturalMultiply count induction))))
1028
1029def deviceArenaWidenLaunch =
1030 (lambda unrestricted steps : Nat .
1031 (lambda unrestricted launch : (family DeviceArenaLaunch) .
1032 (eliminate
1033 DeviceArenaLaunch
1034 (lambda unrestricted current : (family DeviceArenaLaunch) . (family DeviceArenaLaunch))
1035 launch
1036 (branch
1037 DeviceArenaLaunchValue
1038 identity
1039 base
1040 generators
1041 spans
1042 .
1043 (constructor
1044 DeviceArenaLaunch
1045 DeviceArenaLaunchValue
1046 identity
1047 base
1048 generators
1049 (deviceArenaWiden steps (deviceArenaStands generators) spans))))))
1050
1051-- frames of a table iteration: every value any frame gives a launch's
1052-- word taken into its span
1053def deviceArenaFrames =
1054 (lambda unrestricted frames : (family NvidiaParameterAdjustmentFrames) .
1055 (lambda unrestricted launch : (family DeviceArenaLaunch) .
1056 (eliminate
1057 NvidiaParameterAdjustmentFrames
1058 (lambda unrestricted current : (family NvidiaParameterAdjustmentFrames) .
1059 (family DeviceArenaLaunch))
1060 frames
1061 (branch NvidiaParameterAdjustmentFramesEnd . launch)
1062 (branch
1063 NvidiaParameterAdjustmentFramesNext
1064 frame
1065 tail
1066 induction
1067 .
1068 (deviceArenaFold deviceArenaInclude frame induction)))))
1069
1070-- a repeat's body launches, standing for all its iterations: spans widened
1071-- by the iteration's deltas, and the repeat's generator added
1072def deviceArenaRepeat =
1073 (lambda unrestricted count : Nat .
1074 (lambda unrestricted extent : Nat .
1075 (lambda unrestricted iteration : (family NvidiaParameterIteration) .
1076 (lambda unrestricted body : (family DeviceArenaLaunches) .
1077 (deviceArenaMapLaunches
1078 (lambda unrestricted launch : (family DeviceArenaLaunch) .
1079 (eliminate
1080 DeviceArenaLaunch
1081 (lambda unrestricted current : (family DeviceArenaLaunch) .
1082 (family DeviceArenaLaunch))
1083 (eliminate
1084 NvidiaParameterIteration
1085 (lambda unrestricted current : (family NvidiaParameterIteration) .
1086 (family DeviceArenaLaunch))
1087 iteration
1088 (branch NvidiaParameterIterationUnchanged . launch)
1089 (branch
1090 NvidiaParameterIterationAffine
1091 adjustments
1092 .
1093 (deviceArenaWidenLaunch
1094 (naturalSaturatingSubtract count 1)
1095 (deviceArenaFold deviceArenaAccumulate adjustments launch)))
1096 (branch
1097 NvidiaParameterIterationQuotientRemainder
1098 divisor
1099 remainders
1100 quotients
1101 .
1102 (deviceArenaWidenLaunch
1103 (naturalDivideUnchecked (naturalSaturatingSubtract count 1) divisor)
1104 (deviceArenaFold
1105 deviceArenaAccumulate
1106 quotients
1107 (deviceArenaWidenLaunch
1108 (naturalSaturatingSubtract
1109 (naturalSelect (naturalLess count divisor) count divisor)
1110 1)
1111 (deviceArenaFold deviceArenaAccumulate remainders launch)))))
1112 (branch NvidiaParameterIterationTable frames . (deviceArenaFrames frames launch)))
1113 (branch
1114 DeviceArenaLaunchValue
1115 identity
1116 base
1117 generators
1118 spans
1119 .
1120 (constructor
1121 DeviceArenaLaunch
1122 DeviceArenaLaunchValue
1123 identity
1124 base
1125 (constructor
1126 DeviceArenaGenerators
1127 DeviceArenaGeneratorsNext
1128 extent
1129 count
1130 generators)
1131 spans))))
1132 body)))))
1133
1134-- the schedule's launches as written, each standing for its iterations
1135def deviceArenaLaunches =
1136 (lambda unrestricted schedule : (family NvidiaLaunchSchedule) .
1137 (eliminate
1138 NvidiaLaunchSchedule
1139 (lambda unrestricted current : (family NvidiaLaunchSchedule) . (family DeviceArenaLaunches))
1140 schedule
1141 (branch NvidiaLaunchScheduleEmpty . (constructor DeviceArenaLaunches DeviceArenaLaunchesEnd))
1142 (branch
1143 NvidiaLaunchScheduleOne
1144 template
1145 .
1146 (constructor
1147 DeviceArenaLaunches
1148 DeviceArenaLaunchesNext
1149 (deviceArenaLaunchOf template)
1150 (constructor DeviceArenaLaunches DeviceArenaLaunchesEnd)))
1151 (branch
1152 NvidiaLaunchScheduleAppend
1153 left
1154 right
1155 il
1156 ir
1157 .
1158 (deviceArenaAppendLaunches il (deviceArenaShift (nvidiaLaunchScheduleCount left) ir)))
1159 (branch
1160 NvidiaLaunchScheduleRepeat
1161 count
1162 iteration
1163 body
1164 ib
1165 .
1166 (deviceArenaRepeat count (nvidiaLaunchScheduleCount body) iteration ib))))
1167
1168-- ---- (C): every span in a window lies in one named range ----
1169def deviceArenaWithin =
1170 (lambda unrestricted residents : (family ArenaResidents) .
1171 (lambda unrestricted low : Nat .
1172 (lambda unrestricted high : Nat .
1173 (eliminate
1174 ArenaResidents
1175 (lambda unrestricted current : (family ArenaResidents) . Nat)
1176 residents
1177 (branch ArenaResidentsEnd . 0)
1178 (branch
1179 ArenaResidentsNext
1180 head
1181 tail
1182 induction
1183 .
1184 (naturalOr
1185 (naturalAnd (deviceArenaContains head low) (deviceArenaContains head high))
1186 induction))))))
1187
1188def deviceArenaMeets =
1189 (lambda unrestricted windows : (family ArenaResidents) .
1190 (lambda unrestricted low : Nat .
1191 (lambda unrestricted high : Nat .
1192 (eliminate
1193 ArenaResidents
1194 (lambda unrestricted current : (family ArenaResidents) . Nat)
1195 windows
1196 (branch ArenaResidentsEnd . 0)
1197 (branch
1198 ArenaResidentsNext
1199 head
1200 tail
1201 induction
1202 .
1203 (naturalOr
1204 (naturalAnd
1205 (naturalLess low (arenaResidentEndOf head))
1206 (naturalLessOrEqual (arenaResidentOffsetOf head) high))
1207 induction))))))
1208
1209def deviceArenaIntervalsNamed =
1210 (lambda unrestricted windows : (family ArenaResidents) .
1211 (lambda unrestricted named : (family ArenaResidents) .
1212 (lambda unrestricted intervals : (family DeviceArenaIntervals) .
1213 (eliminate
1214 DeviceArenaIntervals
1215 (lambda unrestricted current : (family DeviceArenaIntervals) . Nat)
1216 intervals
1217 (branch DeviceArenaIntervalsEnd . 1)
1218 (branch
1219 DeviceArenaIntervalsNext
1220 low
1221 high
1222 tail
1223 induction
1224 .
1225 (naturalAnd
1226 (naturalOr
1227 (naturalIsZero (deviceArenaMeets windows low high))
1228 (deviceArenaWithin named low high))
1229 induction))))))
1230
1231def deviceArenaSpansNamed =
1232 (lambda unrestricted windows : (family ArenaResidents) .
1233 (lambda unrestricted named : (family ArenaResidents) .
1234 (lambda unrestricted spans : (family DeviceArenaSpans) .
1235 (eliminate
1236 DeviceArenaSpans
1237 (lambda unrestricted current : (family DeviceArenaSpans) . Nat)
1238 spans
1239 (branch DeviceArenaSpansEnd . 1)
1240 (branch
1241 DeviceArenaSpansNext
1242 offset
1243 intervals
1244 rise
1245 fall
1246 uniform
1247 last
1248 ordinals
1249 tail
1250 induction
1251 .
1252 (naturalAnd (deviceArenaIntervalsNamed windows named intervals) induction))))))
1253
1254-- ---- (D): carried planes intact ----
1255def deviceArenaTrackedEnd : (family DeviceArenaTracked) =
1256 (constructor DeviceArenaTracked DeviceArenaTrackedEnd)
1257
1258-- 1 when `resident` was declared, in the same place, and nothing has been
1259-- declared over it since
1260def deviceArenaIntact =
1261 (lambda unrestricted tracked : (family DeviceArenaTracked) .
1262 (lambda unrestricted resident : (family ArenaResident) .
1263 (eliminate
1264 DeviceArenaTracked
1265 (lambda unrestricted current : (family DeviceArenaTracked) . Nat)
1266 tracked
1267 (branch DeviceArenaTrackedEnd . 0)
1268 (branch
1269 DeviceArenaTrackedNext
1270 head
1271 clobbered
1272 tail
1273 induction
1274 .
1275 (nat-eliminate
1276 (lambda unrestricted same : Nat . Nat)
1277 induction
1278 (lambda unrestricted p : Nat .
1279 (lambda unrestricted ignored : Nat .
1280 (naturalAnd
1281 (naturalIsZero clobbered)
1282 (naturalAnd
1283 (naturalEqual (arenaResidentOffsetOf head) (arenaResidentOffsetOf resident))
1284 (naturalEqual (arenaResidentEndOf head) (arenaResidentEndOf resident))))))
1285 (bytes-equal (deviceArenaResidentIdentity head) (deviceArenaResidentIdentity resident)))))))
1286
1287def deviceArenaAllIntact =
1288 (lambda unrestricted tracked : (family DeviceArenaTracked) .
1289 (lambda unrestricted carried : (family ArenaResidents) .
1290 (eliminate
1291 ArenaResidents
1292 (lambda unrestricted current : (family ArenaResidents) . Nat)
1293 carried
1294 (branch ArenaResidentsEnd . 1)
1295 (branch
1296 ArenaResidentsNext
1297 head
1298 tail
1299 induction
1300 .
1301 (naturalAnd (deviceArenaIntact tracked head) induction)))))
1302
1303-- 1 when a resident of this name is among `residents`
1304def deviceArenaAnyNamed =
1305 (lambda unrestricted residents : (family ArenaResidents) .
1306 (lambda unrestricted resident : (family ArenaResident) .
1307 (eliminate
1308 ArenaResidents
1309 (lambda unrestricted current : (family ArenaResidents) . Nat)
1310 residents
1311 (branch ArenaResidentsEnd . 0)
1312 (branch
1313 ArenaResidentsNext
1314 head
1315 tail
1316 induction
1317 .
1318 (naturalOr
1319 (bytes-equal (deviceArenaResidentIdentity head) (deviceArenaResidentIdentity resident))
1320 induction)))))
1321
1322-- an instance of a phase declaring `planes`: every tracked plane they
1323-- overlap (under another name) is clobbered, and those some phase carries
1324-- (the only ones a later instance can need) are tracked afresh
1325def deviceArenaDeclare =
1326 (lambda unrestricted carried : (family ArenaResidents) .
1327 (lambda unrestricted tracked : (family DeviceArenaTracked) .
1328 (lambda unrestricted planes : (family ArenaResidents) .
1329 (eliminate
1330 ArenaResidents
1331 (lambda unrestricted current : (family ArenaResidents) . (family DeviceArenaTracked))
1332 planes
1333 (branch
1334 ArenaResidentsEnd
1335 .
1336 (eliminate
1337 DeviceArenaTracked
1338 (lambda unrestricted current : (family DeviceArenaTracked) .
1339 (family DeviceArenaTracked))
1340 tracked
1341 (branch DeviceArenaTrackedEnd . deviceArenaTrackedEnd)
1342 (branch
1343 DeviceArenaTrackedNext
1344 head
1345 clobbered
1346 tail
1347 induction
1348 .
1349 (nat-eliminate
1350 (lambda unrestricted redeclared : Nat . (family DeviceArenaTracked))
1351 (constructor
1352 DeviceArenaTracked
1353 DeviceArenaTrackedNext
1354 head
1355 (naturalOr clobbered (deviceArenaOverlapsOther head planes))
1356 induction)
1357 (lambda unrestricted p : Nat .
1358 (lambda unrestricted ignored : (family DeviceArenaTracked) . induction))
1359 (deviceArenaAnyNamed planes head)))))
1360 (branch
1361 ArenaResidentsNext
1362 head
1363 tail
1364 induction
1365 .
1366 (nat-eliminate
1367 (lambda unrestricted kept : Nat . (family DeviceArenaTracked))
1368 induction
1369 (lambda unrestricted p : Nat .
1370 (lambda unrestricted ignored : (family DeviceArenaTracked) .
1371 (constructor DeviceArenaTracked DeviceArenaTrackedNext head 0 induction)))
1372 (deviceArenaAnyNamed carried head)))))))
1373
1374-- ---- (C) over the launches as written ----
1375-- the first launch breaking (C), as 2 + its index among the launches as
1376-- written (a repeat's body once); 0 when none does
1377def deviceArenaWordsHazard =
1378 (lambda unrestricted windows : (family ArenaResidents) .
1379 (lambda unrestricted globals : (family ArenaResidents) .
1380 (lambda unrestricted phases : (family DeviceArenaPhases) .
1381 (lambda unrestricted launches : (family DeviceArenaLaunches) .
1382 (app
1383 (eliminate
1384 DeviceArenaLaunches
1385 (lambda unrestricted current : (family DeviceArenaLaunches) .
1386 (pi unrestricted index : Nat . Nat))
1387 launches
1388 (branch DeviceArenaLaunchesEnd . (lambda unrestricted index : Nat . 0))
1389 (branch
1390 DeviceArenaLaunchesNext
1391 head
1392 tail
1393 induction
1394 .
1395 (lambda unrestricted index : Nat .
1396 (let unrestricted identity =
1397 (deviceArenaLaunchIdentityOf head)
1398 in
1399 (let unrestricted later =
1400 (induction (succ index))
1401 in
1402 (nat-eliminate
1403 (lambda unrestricted sound : Nat . Nat)
1404 (naturalAdd 2 index)
1405 (lambda unrestricted p : Nat . (lambda unrestricted ignored : Nat . later))
1406 (naturalAnd
1407 (deviceArenaPhaseKnown phases identity)
1408 (deviceArenaSpansNamed
1409 windows
1410 (deviceArenaAppend
1411 (deviceArenaPhasePlanes (deviceArenaPhaseOf phases identity))
1412 globals)
1413 (deviceArenaLaunchSpansOf head)))))))))
1414 0)))))
1415
1416def deviceArenaLaunchCount =
1417 (lambda unrestricted launches : (family DeviceArenaLaunches) .
1418 (eliminate
1419 DeviceArenaLaunches
1420 (lambda unrestricted current : (family DeviceArenaLaunches) . Nat)
1421 launches
1422 (branch DeviceArenaLaunchesEnd . 0)
1423 (branch DeviceArenaLaunchesNext head tail induction . (succ induction))))
1424
1425-- ---- the order the launches run ----
1426-- the runs of a schedule, from ordinal 0: a repeat's body runs once per
1427-- iteration, and neighbouring runs of one phase merge
1428def deviceArenaPrependRun =
1429 (lambda unrestricted identity : Bytes .
1430 (lambda unrestricted first : Nat .
1431 (lambda unrestricted count : Nat .
1432 (lambda unrestricted rest : (family DeviceArenaRuns) .
1433 (eliminate
1434 DeviceArenaRuns
1435 (lambda unrestricted current : (family DeviceArenaRuns) . (family DeviceArenaRuns))
1436 rest
1437 (branch
1438 DeviceArenaRunsEnd
1439 .
1440 (constructor DeviceArenaRuns DeviceArenaRunsNext identity first count rest))
1441 (branch
1442 DeviceArenaRunsNext
1443 nextIdentity
1444 nextFirst
1445 nextCount
1446 nextTail
1447 ignored
1448 .
1449 (nat-eliminate
1450 (lambda unrestricted merges : Nat . (family DeviceArenaRuns))
1451 (constructor DeviceArenaRuns DeviceArenaRunsNext identity first count rest)
1452 (lambda unrestricted q : Nat .
1453 (lambda unrestricted unused : (family DeviceArenaRuns) .
1454 (constructor
1455 DeviceArenaRuns
1456 DeviceArenaRunsNext
1457 identity
1458 first
1459 (naturalAdd count nextCount)
1460 nextTail)))
1461 (naturalAnd
1462 (bytes-equal identity nextIdentity)
1463 (naturalEqual (naturalAdd first count) nextFirst)))))))))
1464
1465-- `runs` moved `shift` on, then `rest`
1466def deviceArenaRunsShifted =
1467 (lambda unrestricted shift : Nat .
1468 (lambda unrestricted runs : (family DeviceArenaRuns) .
1469 (lambda unrestricted rest : (family DeviceArenaRuns) .
1470 (eliminate
1471 DeviceArenaRuns
1472 (lambda unrestricted current : (family DeviceArenaRuns) . (family DeviceArenaRuns))
1473 runs
1474 (branch DeviceArenaRunsEnd . rest)
1475 (branch
1476 DeviceArenaRunsNext
1477 identity
1478 first
1479 count
1480 tail
1481 induction
1482 .
1483 (deviceArenaPrependRun identity (naturalAdd first shift) count induction))))))
1484
1485def deviceArenaRunsOf =
1486 (lambda unrestricted schedule : (family NvidiaLaunchSchedule) .
1487 (eliminate
1488 NvidiaLaunchSchedule
1489 (lambda unrestricted current : (family NvidiaLaunchSchedule) . (family DeviceArenaRuns))
1490 schedule
1491 (branch NvidiaLaunchScheduleEmpty . (constructor DeviceArenaRuns DeviceArenaRunsEnd))
1492 (branch
1493 NvidiaLaunchScheduleOne
1494 template
1495 .
1496 (constructor
1497 DeviceArenaRuns
1498 DeviceArenaRunsNext
1499 (deviceArenaLaunchIdentityOf (deviceArenaLaunchOf template))
1500 0
1501 1
1502 (constructor DeviceArenaRuns DeviceArenaRunsEnd)))
1503 (branch
1504 NvidiaLaunchScheduleAppend
1505 left
1506 right
1507 il
1508 ir
1509 .
1510 (deviceArenaRunsShifted
1511 0
1512 il
1513 (deviceArenaRunsShifted
1514 (nvidiaLaunchScheduleCount left)
1515 ir
1516 (constructor DeviceArenaRuns DeviceArenaRunsEnd))))
1517 (branch
1518 NvidiaLaunchScheduleRepeat
1519 count
1520 iteration
1521 body
1522 ib
1523 .
1524 (let unrestricted extent =
1525 (nvidiaLaunchScheduleCount body)
1526 in
1527 (nat-eliminate
1528 (lambda unrestricted remaining : Nat . (family DeviceArenaRuns))
1529 (constructor DeviceArenaRuns DeviceArenaRunsEnd)
1530 (lambda unrestricted p : Nat .
1531 (lambda unrestricted induction : (family DeviceArenaRuns) .
1532 (deviceArenaRunsShifted
1533 (naturalMultiply
1534 (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) p)
1535 extent)
1536 ib
1537 induction)))
1538 count)))))
1539
1540-- the identities of the runs meeting [first, first + count), then `rest`
1541def deviceArenaRangeInstances =
1542 (lambda unrestricted runs : (family DeviceArenaRuns) .
1543 (lambda unrestricted first : Nat .
1544 (lambda unrestricted count : Nat .
1545 (lambda unrestricted rest : (family DeviceArenaInstances) .
1546 (eliminate
1547 DeviceArenaRuns
1548 (lambda unrestricted current : (family DeviceArenaRuns) . (family DeviceArenaInstances))
1549 runs
1550 (branch DeviceArenaRunsEnd . rest)
1551 (branch
1552 DeviceArenaRunsNext
1553 identity
1554 runFirst
1555 runCount
1556 tail
1557 induction
1558 .
1559 (nat-eliminate
1560 (lambda unrestricted meets : Nat . (family DeviceArenaInstances))
1561 induction
1562 (lambda unrestricted p : Nat .
1563 (lambda unrestricted ignored : (family DeviceArenaInstances) .
1564 (constructor DeviceArenaInstances DeviceArenaInstancesNext identity induction)))
1565 (naturalAnd
1566 (naturalLess runFirst (naturalAdd first count))
1567 (naturalLess first (naturalAdd runFirst runCount))))))))))
1568
1569-- a submission's references, `shift` launches on (a repeated submission's
1570-- iteration), then `rest`
1571def deviceArenaReferenceInstances =
1572 (lambda unrestricted runs : (family DeviceArenaRuns) .
1573 (lambda unrestricted references : (family NvidiaLaunchReferences) .
1574 (eliminate
1575 NvidiaLaunchReferences
1576 (lambda unrestricted current : (family NvidiaLaunchReferences) .
1577 (pi unrestricted shift : Nat .
1578 (pi unrestricted rest : (family DeviceArenaInstances) . (family DeviceArenaInstances))))
1579 references
1580 (branch
1581 NvidiaLaunchReferencesEmpty
1582 .
1583 (lambda unrestricted shift : Nat .
1584 (lambda unrestricted rest : (family DeviceArenaInstances) . rest)))
1585 (branch
1586 NvidiaLaunchReferencesRange
1587 first
1588 count
1589 .
1590 (lambda unrestricted shift : Nat .
1591 (lambda unrestricted rest : (family DeviceArenaInstances) .
1592 (deviceArenaRangeInstances runs (naturalAdd first shift) count rest))))
1593 (branch
1594 NvidiaLaunchReferencesAppend
1595 left
1596 right
1597 il
1598 ir
1599 .
1600 (lambda unrestricted shift : Nat .
1601 (lambda unrestricted rest : (family DeviceArenaInstances) . (il shift (ir shift rest))))))))
1602
1603def deviceArenaSubmissionInstances =
1604 (lambda unrestricted runs : (family DeviceArenaRuns) .
1605 (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
1606 (eliminate
1607 NvidiaSubmissionSchedule
1608 (lambda unrestricted current : (family NvidiaSubmissionSchedule) .
1609 (pi unrestricted shift : Nat .
1610 (pi unrestricted rest : (family DeviceArenaInstances) . (family DeviceArenaInstances))))
1611 submissions
1612 (branch
1613 NvidiaSubmissionScheduleEmpty
1614 .
1615 (lambda unrestricted shift : Nat .
1616 (lambda unrestricted rest : (family DeviceArenaInstances) . rest)))
1617 (branch
1618 NvidiaSubmissionScheduleOne
1619 batch
1620 .
1621 (lambda unrestricted shift : Nat .
1622 (lambda unrestricted rest : (family DeviceArenaInstances) .
1623 (eliminate
1624 NvidiaSubmissionBatch
1625 (lambda unrestricted current : (family NvidiaSubmissionBatch) .
1626 (family DeviceArenaInstances))
1627 batch
1628 (branch
1629 NvidiaSubmissionBatchValue
1630 identity
1631 semaphore
1632 references
1633 .
1634 (deviceArenaReferenceInstances runs references shift rest))))))
1635 (branch
1636 NvidiaSubmissionScheduleAppend
1637 left
1638 right
1639 il
1640 ir
1641 .
1642 (lambda unrestricted shift : Nat .
1643 (lambda unrestricted rest : (family DeviceArenaInstances) . (il shift (ir shift rest)))))
1644 (branch
1645 NvidiaSubmissionScheduleRepeat
1646 count
1647 referenceStride
1648 semaphoreStride
1649 body
1650 ib
1651 .
1652 (lambda unrestricted shift : Nat .
1653 (lambda unrestricted rest : (family DeviceArenaInstances) .
1654 (app
1655 (nat-eliminate
1656 (lambda unrestricted remaining : Nat .
1657 (pi unrestricted iterationShift : Nat . (family DeviceArenaInstances)))
1658 (lambda unrestricted iterationShift : Nat . rest)
1659 (lambda unrestricted p : Nat .
1660 (lambda unrestricted induction : (pi unrestricted iterationShift : Nat . (family DeviceArenaInstances)) .
1661 (lambda unrestricted iterationShift : Nat .
1662 (ib iterationShift (induction (naturalAdd iterationShift referenceStride))))))
1663 count)
1664 shift))))
1665 -- a profile's releases touch only the semaphore region: the launches
1666 -- are the body's
1667 (branch
1668 NvidiaSubmissionScheduleProfiled
1669 offset
1670 body
1671 ib
1672 .
1673 ib))))
1674
1675-- ---- (D) over the executed instances ----
1676-- the first instance breaking (D), as `base` + its index; 0 when none does.
1677-- The build's evaluator evaluates both arms of a choice, so each step makes
1678-- exactly one recursive call (the walk goes on past a hazard; the first one
1679-- found wins).
1680-- every plane some phase carries
1681def deviceArenaCarriedAnywhere =
1682 (lambda unrestricted phases : (family DeviceArenaPhases) .
1683 (eliminate
1684 DeviceArenaPhases
1685 (lambda unrestricted current : (family DeviceArenaPhases) . (family ArenaResidents))
1686 phases
1687 (branch DeviceArenaPhasesEnd . (constructor ArenaResidents ArenaResidentsEnd))
1688 (branch
1689 DeviceArenaPhasesNext
1690 head
1691 tail
1692 induction
1693 .
1694 (deviceArenaAppend (deviceArenaPhaseCarriedOf head) induction))))
1695
1696def deviceArenaLifetimeHazard =
1697 (lambda unrestricted phases : (family DeviceArenaPhases) .
1698 (lambda unrestricted base : Nat .
1699 (lambda unrestricted instances : (family DeviceArenaInstances) .
1700 (let unrestricted carried =
1701 (deviceArenaCarriedAnywhere phases)
1702 in
1703 (app
1704 (eliminate
1705 DeviceArenaInstances
1706 (lambda unrestricted current : (family DeviceArenaInstances) .
1707 (pi unrestricted tracked : (family DeviceArenaTracked) .
1708 (pi unrestricted previous : Bytes . (pi unrestricted index : Nat . Nat))))
1709 instances
1710 (branch
1711 DeviceArenaInstancesEnd
1712 .
1713 (lambda unrestricted tracked : (family DeviceArenaTracked) .
1714 (lambda unrestricted previous : Bytes . (lambda unrestricted index : Nat . 0))))
1715 (branch
1716 DeviceArenaInstancesNext
1717 identity
1718 tail
1719 induction
1720 .
1721 (lambda unrestricted tracked : (family DeviceArenaTracked) .
1722 (lambda unrestricted previous : Bytes .
1723 (lambda unrestricted index : Nat .
1724 (let unrestricted starts =
1725 (naturalIsZero (bytes-equal identity previous))
1726 in
1727 (let unrestricted phase =
1728 (deviceArenaPhaseOf phases identity)
1729 in
1730 (let unrestricted broken =
1731 (naturalAnd
1732 starts
1733 (naturalIsZero
1734 (deviceArenaAllIntact tracked (deviceArenaPhaseCarriedOf phase))))
1735 in
1736 (let unrestricted next =
1737 (nat-eliminate
1738 (lambda unrestricted fresh : Nat . (family DeviceArenaTracked))
1739 tracked
1740 (lambda unrestricted q : Nat .
1741 (lambda unrestricted unused : (family DeviceArenaTracked) .
1742 (deviceArenaDeclare
1743 carried
1744 tracked
1745 (deviceArenaPhasePlanes phase))))
1746 starts)
1747 in
1748 (let unrestricted later =
1749 (induction next identity (naturalAdd index starts))
1750 in
1751 (nat-eliminate
1752 (lambda unrestricted found : Nat . Nat)
1753 later
1754 (lambda unrestricted q : Nat .
1755 (lambda unrestricted unused : Nat . (naturalAdd base index)))
1756 broken)))))))))))
1757 deviceArenaTrackedEnd
1758 b"\x00"
1759 0)))))
1760
1761-- ---- the verdict ----
1762-- 0 when the plan's device side is certified (see the top of this module)
1763def deviceArenaHazard =
1764 (lambda unrestricted windows : (family ArenaResidents) .
1765 (lambda unrestricted globals : (family ArenaResidents) .
1766 (lambda unrestricted phases : (family DeviceArenaPhases) .
1767 (lambda unrestricted schedule : (family NvidiaLaunchSchedule) .
1768 (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
1769 (nat-eliminate
1770 (lambda unrestricted placed : Nat . Nat)
1771 1
1772 (lambda unrestricted p : Nat .
1773 (lambda unrestricted ignored : Nat .
1774 (let unrestricted launches =
1775 (deviceArenaLaunches schedule)
1776 in
1777 (let unrestricted words =
1778 (deviceArenaWordsHazard windows globals phases launches)
1779 in
1780 (let unrestricted lifetimes =
1781 (deviceArenaLifetimeHazard
1782 phases
1783 (naturalAdd 2 (deviceArenaLaunchCount launches))
1784 (deviceArenaSubmissionInstances
1785 (deviceArenaRunsOf schedule)
1786 submissions
1787 0
1788 (constructor DeviceArenaInstances DeviceArenaInstancesEnd)))
1789 in
1790 (naturalSelect (naturalIsZero words) lifetimes words))))))
1791 (deviceArenaPlaced globals phases)))))))
1792
1793-- 1 when certified
1794def deviceArenaCertificate =
1795 (lambda unrestricted windows : (family ArenaResidents) .
1796 (lambda unrestricted globals : (family ArenaResidents) .
1797 (lambda unrestricted phases : (family DeviceArenaPhases) .
1798 (lambda unrestricted schedule : (family NvidiaLaunchSchedule) .
1799 (lambda unrestricted submissions : (family NvidiaSubmissionSchedule) .
1800 (naturalIsZero (deviceArenaHazard windows globals phases schedule submissions)))))))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.