1module Compiler.Planning.Liveness
2
3import Model.Parameter
4import Model.Word32
5import Model.Word64
6import Std.Natural
7import Std.Physical
8import Model.Config
9
10family TensorId : Type 0
11constructor TensorIdValue
12field unrestricted tensorIdWord : (family ModelWord32)
13
14end-family
15
16family Lifetime : Type 0
17constructor LifetimeValue
18field unrestricted lifetimeTensor : (family TensorId)
19field unrestricted lifetimeFirstUse : (family ModelWord32)
20field unrestricted lifetimeLastUse : (family ModelWord32)
21field unrestricted lifetimeBytes : ByteCount
22field unrestricted lifetimeAlignment : ByteAlignment
23
24end-family
25
26family Lifetimes : Type 0
27constructor LifetimesEnd
28constructor LifetimesNext
29field unrestricted lifetimeHead : (family Lifetime)
30recursive unrestricted lifetimeTail
31
32end-family
33
34family Placement : Type 0
35constructor PlacementValue
36field unrestricted placementLifetime : (family Lifetime)
37field unrestricted placementOffset : ByteCount
38field unrestricted placementCapacity : ByteCount
39
40end-family
41
42family Placements : Type 0
43constructor PlacementsEnd
44constructor PlacementsNext
45field unrestricted placementHead : (family Placement)
46recursive unrestricted placementTail
47
48end-family
49
50family MemoryPlan : Type 0
51constructor MemoryPlanValue
52field unrestricted planArenaBytes : ByteCount
53field unrestricted planPeakBytes : ByteCount
54field unrestricted planPlacements : (family Placements)
55
56end-family
57
58family LivenessErrorCode : Type 0
59constructor LifetimeTensorDuplicate
60constructor LifetimeIntervalInvalid
61constructor LifetimeBytesZero
62constructor LifetimeAlignmentInvalid
63constructor PlanPeakExceedsArena
64constructor PlacementMisaligned
65constructor PlacementCapacityTooSmall
66constructor PlacementRangeOverflow
67constructor PlacementOutsideArena
68constructor PlacementLiveCollision
69constructor PlacementArithmeticOverflow
70constructor PlacementArenaExhausted
71constructor CompiledPlanRejected
72
73end-family
74
75family LivenessOptionalError : Type 0
76constructor LivenessNoError
77constructor LivenessSomeError
78field unrestricted livenessError : (family LivenessErrorCode)
79
80end-family
81
82family LivenessTelemetry : Type 0
83constructor LivenessTelemetryValue
84field unrestricted livenessLifetimeCount : Nat
85field unrestricted livenessPlacementCount : Nat
86field unrestricted livenessInvalidLifetimeCount : Nat
87field unrestricted livenessInvalidPlacementCount : Nat
88field unrestricted livenessCollisionCount : Nat
89field unrestricted livenessArenaBytes : ByteCount
90field unrestricted livenessPeakBytes : ByteCount
91field unrestricted livenessSucceeded : Nat
92field unrestricted livenessFailure : (family LivenessOptionalError)
93field unrestricted livenessHostFallbacks : Nat
94
95end-family
96
97family LivenessValidationResult : Type 0
98constructor LivenessValidationPassed
99field unrestricted livenessValidatedPlan : (family MemoryPlan)
100field unrestricted livenessPassedTelemetry : (family LivenessTelemetry)
101constructor LivenessValidationFailed
102field unrestricted livenessFailureCode : (family LivenessErrorCode)
103field unrestricted livenessFailedTelemetry : (family LivenessTelemetry)
104
105end-family
106
107family LivenessSlot : Type 0
108constructor LivenessSlotValue
109field unrestricted livenessSlotOffset : ByteCount
110field unrestricted livenessSlotCapacity : ByteCount
111field unrestricted livenessSlotLastUse : (family ModelWord32)
112
113end-family
114
115family LivenessSlots : Type 0
116constructor LivenessSlotsEnd
117constructor LivenessSlotsNext
118field unrestricted livenessSlotHead : (family LivenessSlot)
119recursive unrestricted livenessSlotTail
120
121end-family
122
123family LivenessOptionalSlot : Type 0
124constructor LivenessNoSlot
125constructor LivenessSomeSlot
126field unrestricted livenessSelectedSlot : (family LivenessSlot)
127
128end-family
129
130family LivenessPlacementState : Type 0
131constructor LivenessPlacementStateValue
132field unrestricted livenessStatePeak : ByteCount
133field unrestricted livenessStateSlots : (family LivenessSlots)
134field unrestricted livenessStatePlacements : (family Placements)
135field unrestricted livenessStateReusedSlots : Nat
136field unrestricted livenessStateFreshSlots : Nat
137
138end-family
139
140family LivenessPlacementStep : Type 0
141constructor LivenessPlacementAdvanced
142field unrestricted livenessAdvancedState : (family LivenessPlacementState)
143constructor LivenessPlacementStopped
144field unrestricted livenessPlacementFailure : (family LivenessErrorCode)
145field unrestricted livenessStoppedState : (family LivenessPlacementState)
146
147end-family
148
149family LivenessCompileTelemetry : Type 0
150constructor LivenessCompileTelemetryValue
151field unrestricted livenessCompileLifetimeCount : Nat
152field unrestricted livenessCompilePlacementCount : Nat
153field unrestricted livenessCompileReusedSlots : Nat
154field unrestricted livenessCompileFreshSlots : Nat
155field unrestricted livenessCompileArenaBytes : ByteCount
156field unrestricted livenessCompilePeakBytes : ByteCount
157field unrestricted livenessCompileSucceeded : Nat
158field unrestricted livenessCompileFailure : (family LivenessOptionalError)
159field unrestricted livenessCompileHostFallbacks : Nat
160
161end-family
162
163family MemoryPlanCompileResult : Type 0
164constructor MemoryPlanCompiled
165field unrestricted compiledMemoryPlan : (family MemoryPlan)
166field unrestricted memoryPlanCompileTelemetry : (family LivenessCompileTelemetry)
167constructor MemoryPlanCompileFailed
168field unrestricted memoryPlanCompileFailure : (family LivenessErrorCode)
169field unrestricted memoryPlanFailureTelemetry : (family LivenessCompileTelemetry)
170
171end-family
172
173def livenessErrorCodeBytes =
174 (lambda unrestricted code : (family LivenessErrorCode) .
175 (eliminate
176 LivenessErrorCode
177 (lambda unrestricted current : (family LivenessErrorCode) . Bytes)
178 code
179 (branch LifetimeTensorDuplicate . b"ALPHA-GAIA-LIV-001")
180 (branch LifetimeIntervalInvalid . b"ALPHA-GAIA-LIV-002")
181 (branch LifetimeBytesZero . b"ALPHA-GAIA-LIV-003")
182 (branch LifetimeAlignmentInvalid . b"ALPHA-GAIA-LIV-004")
183 (branch PlanPeakExceedsArena . b"ALPHA-GAIA-LIV-005")
184 (branch PlacementMisaligned . b"ALPHA-GAIA-LIV-006")
185 (branch PlacementCapacityTooSmall . b"ALPHA-GAIA-LIV-007")
186 (branch PlacementRangeOverflow . b"ALPHA-GAIA-LIV-008")
187 (branch PlacementOutsideArena . b"ALPHA-GAIA-LIV-009")
188 (branch PlacementLiveCollision . b"ALPHA-GAIA-LIV-010")
189 (branch PlacementArithmeticOverflow . b"ALPHA-GAIA-LIV-011")
190 (branch PlacementArenaExhausted . b"ALPHA-GAIA-LIV-012")
191 (branch CompiledPlanRejected . b"ALPHA-GAIA-LIV-013")))
192
193def naturalFlagNot =
194 (lambda unrestricted value : Nat .
195 (nat-eliminate
196 (lambda unrestricted current : Nat . Nat)
197 (succ zero)
198 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
199 value))
200
201def naturalFlagAnd =
202 (lambda unrestricted left : Nat .
203 (lambda unrestricted right : Nat .
204 (nat-eliminate
205 (lambda unrestricted current : Nat . Nat)
206 zero
207 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . right))
208 left)))
209
210def naturalFlagOr =
211 (lambda unrestricted left : Nat .
212 (lambda unrestricted right : Nat .
213 (nat-eliminate
214 (lambda unrestricted current : Nat . Nat)
215 right
216 (lambda unrestricted predecessor : Nat .
217 (lambda unrestricted induction : Nat . (succ zero)))
218 left)))
219
220def livenessNaturalEqual =
221 (lambda unrestricted left : Nat .
222 (lambda unrestricted right : Nat .
223 (naturalFlagNot (naturalFlagOr (nat-less-than left right) (nat-less-than right left)))))
224
225def naturalLessThanOrEqual =
226 (lambda unrestricted left : Nat .
227 (lambda unrestricted right : Nat . (naturalFlagNot (nat-less-than right left))))
228
229def word64LessThanOrEqual =
230 (lambda unrestricted left : (family ModelWord64) .
231 (lambda unrestricted right : (family ModelWord64) .
232 (naturalFlagOr (modelWord64LessThan left right) (modelWord64Equal left right))))
233
234def tensorIdEqual =
235 (lambda unrestricted left : (family TensorId) .
236 (lambda unrestricted right : (family TensorId) .
237 (eliminate
238 TensorId
239 (lambda unrestricted current : (family TensorId) . Nat)
240 left
241 (branch
242 TensorIdValue
243 leftWord
244 .
245 (eliminate
246 TensorId
247 (lambda unrestricted current : (family TensorId) . Nat)
248 right
249 (branch
250 TensorIdValue
251 rightWord
252 .
253 (livenessNaturalEqual
254 (modelWord32ToNatural leftWord)
255 (modelWord32ToNatural rightWord))))))))
256
257def alignmentValid =
258 (lambda unrestricted alignment : (family ModelWord64) .
259 (nat-eliminate
260 (lambda unrestricted alignmentIsZero : Nat . Nat)
261 (modelWord64IsZero (modelWord64And alignment (modelWord64Subtract alignment modelWord64One)))
262 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
263 (modelWord64IsZero alignment)))
264
265def lifetimeTensorId =
266 (lambda unrestricted lifetime : (family Lifetime) .
267 (eliminate
268 Lifetime
269 (lambda unrestricted current : (family Lifetime) . (family TensorId))
270 lifetime
271 (branch LifetimeValue tensor firstUse lastUse bytes alignment . tensor)))
272
273-- Remote reads retain the existing allocation through transport completion.
274-- Extending an earlier bound is monotone: a transfer cannot accidentally
275-- shorten an activation's already-established local lifetime.
276def retainLifetimeThrough =
277 (lambda unrestricted remoteLastRead : (family ModelWord32) .
278 (lambda unrestricted lifetime : (family Lifetime) .
279 (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . (family Lifetime))
280 lifetime
281 (branch LifetimeValue tensor firstUse lastUse bytes alignment .
282 (nat-eliminate
283 (lambda unrestricted flag : Nat . (family Lifetime))
284 lifetime
285 (lambda unrestricted previous : Nat .
286 (lambda unrestricted ignored : (family Lifetime) .
287 (constructor Lifetime LifetimeValue tensor firstUse remoteLastRead bytes alignment)))
288 (naturalLess (modelWord32ToNatural lastUse) (modelWord32ToNatural remoteLastRead)))))))
289
290def lifetimeIsValid =
291 (lambda unrestricted lifetime : (family Lifetime) .
292 (eliminate
293 Lifetime
294 (lambda unrestricted current : (family Lifetime) . Nat)
295 lifetime
296 (branch
297 LifetimeValue
298 tensor
299 firstUse
300 lastUse
301 bytes
302 alignment
303 .
304 (naturalFlagAnd
305 (naturalLessThanOrEqual (modelWord32ToNatural firstUse) (modelWord32ToNatural lastUse))
306 (naturalFlagAnd
307 (naturalFlagNot (modelWord64IsZero (stdByteCountValue bytes)))
308 (alignmentValid (stdByteAlignmentValue alignment)))))))
309
310def lifetimeError =
311 (lambda unrestricted lifetime : (family Lifetime) .
312 (eliminate
313 Lifetime
314 (lambda unrestricted current : (family Lifetime) . (family LivenessErrorCode))
315 lifetime
316 (branch
317 LifetimeValue
318 tensor
319 firstUse
320 lastUse
321 bytes
322 alignment
323 .
324 (nat-eliminate
325 (lambda unrestricted intervalInvalid : Nat . (family LivenessErrorCode))
326 (nat-eliminate
327 (lambda unrestricted bytesAreZero : Nat . (family LivenessErrorCode))
328 (constructor LivenessErrorCode LifetimeAlignmentInvalid)
329 (lambda unrestricted predecessor : Nat .
330 (lambda unrestricted induction : (family LivenessErrorCode) .
331 (constructor LivenessErrorCode LifetimeBytesZero)))
332 (modelWord64IsZero (stdByteCountValue bytes)))
333 (lambda unrestricted predecessor : Nat .
334 (lambda unrestricted induction : (family LivenessErrorCode) .
335 (constructor LivenessErrorCode LifetimeIntervalInvalid)))
336 (nat-less-than (modelWord32ToNatural lastUse) (modelWord32ToNatural firstUse))))))
337
338def lifetimeIdOccurs =
339 (lambda unrestricted tensor : (family TensorId) .
340 (lambda unrestricted lifetimes : (family Lifetimes) .
341 (eliminate
342 Lifetimes
343 (lambda unrestricted current : (family Lifetimes) . Nat)
344 lifetimes
345 (branch LifetimesEnd . zero)
346 (branch
347 LifetimesNext
348 head
349 tail
350 ih_tail
351 .
352 (naturalFlagOr (tensorIdEqual tensor (lifetimeTensorId head)) ih_tail)))))
353
354def lifetimesUnique =
355 (lambda unrestricted lifetimes : (family Lifetimes) .
356 (eliminate
357 Lifetimes
358 (lambda unrestricted current : (family Lifetimes) . Nat)
359 lifetimes
360 (branch LifetimesEnd . (succ zero))
361 (branch
362 LifetimesNext
363 head
364 tail
365 ih_tail
366 .
367 (naturalFlagAnd (naturalFlagNot (lifetimeIdOccurs (lifetimeTensorId head) tail)) ih_tail))))
368
369def lifetimesValid =
370 (lambda unrestricted lifetimes : (family Lifetimes) .
371 (eliminate
372 Lifetimes
373 (lambda unrestricted current : (family Lifetimes) . Nat)
374 lifetimes
375 (branch LifetimesEnd . (succ zero))
376 (branch LifetimesNext head tail ih_tail . (naturalFlagAnd (lifetimeIsValid head) ih_tail))))
377
378def lifetimeCount =
379 (lambda unrestricted lifetimes : (family Lifetimes) .
380 (eliminate
381 Lifetimes
382 (lambda unrestricted current : (family Lifetimes) . Nat)
383 lifetimes
384 (branch LifetimesEnd . zero)
385 (branch LifetimesNext head tail ih_tail . (succ ih_tail))))
386
387def placementCount =
388 (lambda unrestricted placements : (family Placements) .
389 (eliminate
390 Placements
391 (lambda unrestricted current : (family Placements) . Nat)
392 placements
393 (branch PlacementsEnd . zero)
394 (branch PlacementsNext head tail ih_tail . (succ ih_tail))))
395
396def placementLifetimeList =
397 (lambda unrestricted placements : (family Placements) .
398 (eliminate
399 Placements
400 (lambda unrestricted current : (family Placements) . (family Lifetimes))
401 placements
402 (branch PlacementsEnd . (constructor Lifetimes LifetimesEnd))
403 (branch
404 PlacementsNext
405 head
406 tail
407 ih_tail
408 .
409 (eliminate
410 Placement
411 (lambda unrestricted current : (family Placement) . (family Lifetimes))
412 head
413 (branch
414 PlacementValue
415 lifetime
416 offset
417 capacity
418 .
419 (constructor Lifetimes LifetimesNext lifetime ih_tail))))))
420
421def placementAligned =
422 (lambda unrestricted placement : (family Placement) .
423 (eliminate
424 Placement
425 (lambda unrestricted current : (family Placement) . Nat)
426 placement
427 (branch
428 PlacementValue
429 lifetime
430 offset
431 capacity
432 .
433 (eliminate
434 Lifetime
435 (lambda unrestricted current : (family Lifetime) . Nat)
436 lifetime
437 (branch
438 LifetimeValue
439 tensor
440 firstUse
441 lastUse
442 bytes
443 alignment
444 .
445 (modelWord64IsZero
446 (modelWord64And
447 (stdByteCountValue offset)
448 (modelWord64Subtract (stdByteAlignmentValue alignment) modelWord64One))))))))
449
450def placementCapacityValid =
451 (lambda unrestricted placement : (family Placement) .
452 (eliminate
453 Placement
454 (lambda unrestricted current : (family Placement) . Nat)
455 placement
456 (branch
457 PlacementValue
458 lifetime
459 offset
460 capacity
461 .
462 (eliminate
463 Lifetime
464 (lambda unrestricted current : (family Lifetime) . Nat)
465 lifetime
466 (branch
467 LifetimeValue
468 tensor
469 firstUse
470 lastUse
471 bytes
472 alignment
473 .
474 (word64LessThanOrEqual (stdByteCountValue bytes) (stdByteCountValue capacity)))))))
475
476def placementRangeValid =
477 (lambda unrestricted arenaBytes : ByteCount .
478 (lambda unrestricted placement : (family Placement) .
479 (eliminate
480 Placement
481 (lambda unrestricted current : (family Placement) . Nat)
482 placement
483 (branch
484 PlacementValue
485 lifetime
486 offset
487 capacity
488 .
489 (eliminate
490 ModelWord64CheckedResult
491 (lambda unrestricted result : (family ModelWord64CheckedResult) . Nat)
492 (modelWord64AddChecked (stdByteCountValue offset) (stdByteCountValue capacity))
493 (branch
494 ModelWord64CheckedSucceeded
495 end
496 .
497 (word64LessThanOrEqual end (stdByteCountValue arenaBytes)))
498 (branch ModelWord64CheckedFailed error . zero))))))
499
500def placementIsValid =
501 (lambda unrestricted arenaBytes : ByteCount .
502 (lambda unrestricted placement : (family Placement) .
503 (eliminate
504 Placement
505 (lambda unrestricted current : (family Placement) . Nat)
506 placement
507 (branch
508 PlacementValue
509 lifetime
510 offset
511 capacity
512 .
513 (naturalFlagAnd
514 (lifetimeIsValid lifetime)
515 (naturalFlagAnd
516 (placementAligned placement)
517 (naturalFlagAnd
518 (placementCapacityValid placement)
519 (placementRangeValid arenaBytes placement))))))))
520
521def placementInvalidCount =
522 (lambda unrestricted arenaBytes : ByteCount .
523 (lambda unrestricted placements : (family Placements) .
524 (eliminate
525 Placements
526 (lambda unrestricted current : (family Placements) . Nat)
527 placements
528 (branch PlacementsEnd . zero)
529 (branch
530 PlacementsNext
531 head
532 tail
533 ih_tail
534 .
535 (naturalAdd (naturalFlagNot (placementIsValid arenaBytes head)) ih_tail)))))
536
537def placementsValid =
538 (lambda unrestricted arenaBytes : ByteCount .
539 (lambda unrestricted placements : (family Placements) .
540 (naturalFlagNot
541 (naturalFlagNot (livenessNaturalEqual (placementInvalidCount arenaBytes placements) zero)))))
542
543def placementCollision =
544 (lambda unrestricted left : (family Placement) .
545 (lambda unrestricted right : (family Placement) .
546 (eliminate
547 Placement
548 (lambda unrestricted current : (family Placement) . Nat)
549 left
550 (branch
551 PlacementValue
552 leftLifetime
553 leftOffset
554 leftCapacity
555 .
556 (eliminate
557 Placement
558 (lambda unrestricted current : (family Placement) . Nat)
559 right
560 (branch
561 PlacementValue
562 rightLifetime
563 rightOffset
564 rightCapacity
565 .
566 (eliminate
567 Lifetime
568 (lambda unrestricted current : (family Lifetime) . Nat)
569 leftLifetime
570 (branch
571 LifetimeValue
572 leftTensor
573 leftFirst
574 leftLast
575 leftBytes
576 leftAlignment
577 .
578 (eliminate
579 Lifetime
580 (lambda unrestricted current : (family Lifetime) . Nat)
581 rightLifetime
582 (branch
583 LifetimeValue
584 rightTensor
585 rightFirst
586 rightLast
587 rightBytes
588 rightAlignment
589 .
590 (eliminate
591 ModelWord64CheckedResult
592 (lambda unrestricted result : (family ModelWord64CheckedResult) . Nat)
593 (modelWord64AddChecked
594 (stdByteCountValue leftOffset)
595 (stdByteCountValue leftBytes))
596 (branch
597 ModelWord64CheckedSucceeded
598 leftEnd
599 .
600 (eliminate
601 ModelWord64CheckedResult
602 (lambda unrestricted result : (family ModelWord64CheckedResult) . Nat)
603 (modelWord64AddChecked
604 (stdByteCountValue rightOffset)
605 (stdByteCountValue rightBytes))
606 (branch
607 ModelWord64CheckedSucceeded
608 rightEnd
609 .
610 (naturalFlagAnd
611 (naturalFlagAnd
612 (naturalLessThanOrEqual
613 (modelWord32ToNatural leftFirst)
614 (modelWord32ToNatural rightLast))
615 (naturalLessThanOrEqual
616 (modelWord32ToNatural rightFirst)
617 (modelWord32ToNatural leftLast)))
618 (naturalFlagAnd
619 (modelWord64LessThan (stdByteCountValue leftOffset) rightEnd)
620 (modelWord64LessThan (stdByteCountValue rightOffset) leftEnd))))
621 (branch ModelWord64CheckedFailed error . (succ zero))))
622 (branch ModelWord64CheckedFailed error . (succ zero)))))))))))))
623
624def placementCollisionCountWith =
625 (lambda unrestricted placement : (family Placement) .
626 (lambda unrestricted others : (family Placements) .
627 (eliminate
628 Placements
629 (lambda unrestricted current : (family Placements) . Nat)
630 others
631 (branch PlacementsEnd . zero)
632 (branch
633 PlacementsNext
634 head
635 tail
636 ih_tail
637 .
638 (naturalAdd (placementCollision placement head) ih_tail)))))
639
640def placementCollisionCount =
641 (lambda unrestricted placements : (family Placements) .
642 (eliminate
643 Placements
644 (lambda unrestricted current : (family Placements) . Nat)
645 placements
646 (branch PlacementsEnd . zero)
647 (branch
648 PlacementsNext
649 head
650 tail
651 ih_tail
652 .
653 (naturalAdd (placementCollisionCountWith head tail) ih_tail))))
654
655def livenessTelemetryFor =
656 (lambda unrestricted plan : (family MemoryPlan) .
657 (lambda unrestricted succeeded : Nat .
658 (lambda unrestricted failure : (family LivenessOptionalError) .
659 (eliminate
660 MemoryPlan
661 (lambda unrestricted current : (family MemoryPlan) . (family LivenessTelemetry))
662 plan
663 (branch
664 MemoryPlanValue
665 arenaBytes
666 peakBytes
667 placements
668 .
669 (app
670 (lambda unrestricted lifetimes : (family Lifetimes) .
671 (constructor
672 LivenessTelemetry
673 LivenessTelemetryValue
674 (lifetimeCount lifetimes)
675 (placementCount placements)
676 (naturalFlagNot (lifetimesValid lifetimes))
677 (placementInvalidCount arenaBytes placements)
678 (placementCollisionCount placements)
679 arenaBytes
680 peakBytes
681 succeeded
682 failure
683 zero))
684 (placementLifetimeList placements)))))))
685
686def livenessFailureResult =
687 (lambda unrestricted plan : (family MemoryPlan) .
688 (lambda unrestricted code : (family LivenessErrorCode) .
689 (constructor
690 LivenessValidationResult
691 LivenessValidationFailed
692 code
693 (livenessTelemetryFor plan zero (constructor LivenessOptionalError LivenessSomeError code)))))
694
695def validatePlacements =
696 (lambda unrestricted arenaBytes : ByteCount .
697 (lambda unrestricted placements : (family Placements) .
698 (eliminate
699 Placements
700 (lambda unrestricted current : (family Placements) . (family LivenessOptionalError))
701 placements
702 (branch PlacementsEnd . (constructor LivenessOptionalError LivenessNoError))
703 (branch
704 PlacementsNext
705 head
706 tail
707 ih_tail
708 .
709 (nat-eliminate
710 (lambda unrestricted lifetimeInvalid : Nat . (family LivenessOptionalError))
711 (nat-eliminate
712 (lambda unrestricted misaligned : Nat . (family LivenessOptionalError))
713 (nat-eliminate
714 (lambda unrestricted capacityInvalid : Nat . (family LivenessOptionalError))
715 (nat-eliminate
716 (lambda unrestricted rangeInvalid : Nat . (family LivenessOptionalError))
717 ih_tail
718 (lambda unrestricted predecessor : Nat .
719 (lambda unrestricted induction : (family LivenessOptionalError) .
720 (constructor
721 LivenessOptionalError
722 LivenessSomeError
723 (constructor LivenessErrorCode PlacementOutsideArena))))
724 (naturalFlagNot (placementRangeValid arenaBytes head)))
725 (lambda unrestricted predecessor : Nat .
726 (lambda unrestricted induction : (family LivenessOptionalError) .
727 (constructor
728 LivenessOptionalError
729 LivenessSomeError
730 (constructor LivenessErrorCode PlacementCapacityTooSmall))))
731 (naturalFlagNot (placementCapacityValid head)))
732 (lambda unrestricted predecessor : Nat .
733 (lambda unrestricted induction : (family LivenessOptionalError) .
734 (constructor
735 LivenessOptionalError
736 LivenessSomeError
737 (constructor LivenessErrorCode PlacementMisaligned))))
738 (naturalFlagNot (placementAligned head)))
739 (lambda unrestricted predecessor : Nat .
740 (lambda unrestricted induction : (family LivenessOptionalError) .
741 (eliminate
742 Placement
743 (lambda unrestricted current : (family Placement) .
744 (family LivenessOptionalError))
745 head
746 (branch
747 PlacementValue
748 lifetime
749 offset
750 capacity
751 .
752 (constructor LivenessOptionalError LivenessSomeError (lifetimeError lifetime))))))
753 (naturalFlagNot
754 (eliminate
755 Placement
756 (lambda unrestricted current : (family Placement) . Nat)
757 head
758 (branch PlacementValue lifetime offset capacity . (lifetimeIsValid lifetime)))))))))
759
760def validateMemoryPlan =
761 (lambda unrestricted plan : (family MemoryPlan) .
762 (eliminate
763 MemoryPlan
764 (lambda unrestricted current : (family MemoryPlan) . (family LivenessValidationResult))
765 plan
766 (branch
767 MemoryPlanValue
768 arenaBytes
769 peakBytes
770 placements
771 .
772 (app
773 (lambda unrestricted lifetimes : (family Lifetimes) .
774 (nat-eliminate
775 (lambda unrestricted duplicateIds : Nat . (family LivenessValidationResult))
776 (nat-eliminate
777 (lambda unrestricted peakInvalid : Nat . (family LivenessValidationResult))
778 (eliminate
779 LivenessOptionalError
780 (lambda unrestricted current : (family LivenessOptionalError) .
781 (family LivenessValidationResult))
782 (validatePlacements arenaBytes placements)
783 (branch
784 LivenessNoError
785 .
786 (nat-eliminate
787 (lambda unrestricted collisionsZero : Nat . (family LivenessValidationResult))
788 (livenessFailureResult
789 plan
790 (constructor LivenessErrorCode PlacementLiveCollision))
791 (lambda unrestricted predecessor : Nat .
792 (lambda unrestricted induction : (family LivenessValidationResult) .
793 (constructor
794 LivenessValidationResult
795 LivenessValidationPassed
796 plan
797 (livenessTelemetryFor
798 plan
799 (succ zero)
800 (constructor LivenessOptionalError LivenessNoError)))))
801 (naturalFlagNot (placementCollisionCount placements))))
802 (branch LivenessSomeError error . (livenessFailureResult plan error)))
803 (lambda unrestricted predecessor : Nat .
804 (lambda unrestricted induction : (family LivenessValidationResult) .
805 (livenessFailureResult
806 plan
807 (constructor LivenessErrorCode PlanPeakExceedsArena))))
808 (modelWord64LessThan (stdByteCountValue arenaBytes) (stdByteCountValue peakBytes)))
809 (lambda unrestricted predecessor : Nat .
810 (lambda unrestricted induction : (family LivenessValidationResult) .
811 (livenessFailureResult
812 plan
813 (constructor LivenessErrorCode LifetimeTensorDuplicate))))
814 (naturalFlagNot (lifetimesUnique lifetimes))))
815 (placementLifetimeList placements)))))
816
817-- Fixed-shape liveness compilation. The result is a checked arena plan, not a
818-- runtime request to substitute a different tensor shape.
819def lifetimeComesBeforeOrEqual =
820 (lambda unrestricted left : (family Lifetime) .
821 (lambda unrestricted right : (family Lifetime) .
822 (eliminate
823 Lifetime
824 (lambda unrestricted current : (family Lifetime) . Nat)
825 left
826 (branch
827 LifetimeValue
828 leftTensor
829 leftFirst
830 leftLast
831 leftBytes
832 leftAlignment
833 .
834 (eliminate
835 Lifetime
836 (lambda unrestricted current : (family Lifetime) . Nat)
837 right
838 (branch
839 LifetimeValue
840 rightTensor
841 rightFirst
842 rightLast
843 rightBytes
844 rightAlignment
845 .
846 (naturalFlagOr
847 (nat-less-than (modelWord32ToNatural leftFirst) (modelWord32ToNatural rightFirst))
848 (naturalFlagAnd
849 (livenessNaturalEqual
850 (modelWord32ToNatural leftFirst)
851 (modelWord32ToNatural rightFirst))
852 (eliminate
853 TensorId
854 (lambda unrestricted current : (family TensorId) . Nat)
855 leftTensor
856 (branch
857 TensorIdValue
858 leftId
859 .
860 (eliminate
861 TensorId
862 (lambda unrestricted current : (family TensorId) . Nat)
863 rightTensor
864 (branch
865 TensorIdValue
866 rightId
867 .
868 (naturalLessThanOrEqual
869 (modelWord32ToNatural leftId)
870 (modelWord32ToNatural rightId))))))))))))))
871
872def lifetimesInsert =
873 (lambda unrestricted lifetime : (family Lifetime) .
874 (lambda unrestricted ordered : (family Lifetimes) .
875 (eliminate
876 Lifetimes
877 (lambda unrestricted current : (family Lifetimes) . (family Lifetimes))
878 ordered
879 (branch
880 LifetimesEnd
881 .
882 (constructor Lifetimes LifetimesNext lifetime (constructor Lifetimes LifetimesEnd)))
883 (branch
884 LifetimesNext
885 head
886 tail
887 ih_tail
888 .
889 (nat-eliminate
890 (lambda unrestricted before : Nat . (family Lifetimes))
891 (constructor Lifetimes LifetimesNext head ih_tail)
892 (lambda unrestricted predecessor : Nat .
893 (lambda unrestricted induction : (family Lifetimes) .
894 (constructor Lifetimes LifetimesNext lifetime ordered)))
895 (lifetimeComesBeforeOrEqual lifetime head))))))
896
897def lifetimesSort =
898 (lambda unrestricted lifetimes : (family Lifetimes) .
899 (eliminate
900 Lifetimes
901 (lambda unrestricted current : (family Lifetimes) . (family Lifetimes))
902 lifetimes
903 (branch LifetimesEnd . (constructor Lifetimes LifetimesEnd))
904 (branch LifetimesNext head tail ih_tail . (lifetimesInsert head ih_tail))))
905
906def placementsReverseOnto =
907 (lambda unrestricted input : (family Placements) .
908 (eliminate
909 Placements
910 (lambda unrestricted current : (family Placements) .
911 (pi unrestricted output : (family Placements) . (family Placements)))
912 input
913 (branch PlacementsEnd . (lambda unrestricted output : (family Placements) . output))
914 (branch
915 PlacementsNext
916 head
917 tail
918 ih_tail
919 .
920 (lambda unrestricted output : (family Placements) .
921 (ih_tail (constructor Placements PlacementsNext head output))))))
922
923def placementsReverse =
924 (lambda unrestricted placements : (family Placements) .
925 (placementsReverseOnto placements (constructor Placements PlacementsEnd)))
926
927def livenessSlotReusable =
928 (lambda unrestricted lifetime : (family Lifetime) .
929 (lambda unrestricted slot : (family LivenessSlot) .
930 (eliminate
931 Lifetime
932 (lambda unrestricted current : (family Lifetime) . Nat)
933 lifetime
934 (branch
935 LifetimeValue
936 tensor
937 firstUse
938 lastUse
939 bytes
940 alignment
941 .
942 (eliminate
943 LivenessSlot
944 (lambda unrestricted current : (family LivenessSlot) . Nat)
945 slot
946 (branch
947 LivenessSlotValue
948 offset
949 capacity
950 slotLastUse
951 .
952 (naturalFlagAnd
953 (nat-less-than (modelWord32ToNatural slotLastUse) (modelWord32ToNatural firstUse))
954 (naturalFlagAnd
955 (word64LessThanOrEqual (stdByteCountValue bytes) (stdByteCountValue capacity))
956 (modelWord64IsZero
957 (modelWord64And
958 (stdByteCountValue offset)
959 (modelWord64Subtract (stdByteAlignmentValue alignment) modelWord64One)))))))))))
960
961def livenessSlotBetter =
962 (lambda unrestricted candidate : (family LivenessSlot) .
963 (lambda unrestricted current : (family LivenessSlot) .
964 (eliminate
965 LivenessSlot
966 (lambda unrestricted value : (family LivenessSlot) . Nat)
967 candidate
968 (branch
969 LivenessSlotValue
970 candidateOffset
971 candidateCapacity
972 candidateLastUse
973 .
974 (eliminate
975 LivenessSlot
976 (lambda unrestricted value : (family LivenessSlot) . Nat)
977 current
978 (branch
979 LivenessSlotValue
980 currentOffset
981 currentCapacity
982 currentLastUse
983 .
984 (naturalFlagOr
985 (modelWord64LessThan
986 (stdByteCountValue candidateCapacity)
987 (stdByteCountValue currentCapacity))
988 (naturalFlagAnd
989 (modelWord64Equal
990 (stdByteCountValue candidateCapacity)
991 (stdByteCountValue currentCapacity))
992 (modelWord64LessThan
993 (stdByteCountValue candidateOffset)
994 (stdByteCountValue currentOffset))))))))))
995
996def livenessBestReusable =
997 (lambda unrestricted lifetime : (family Lifetime) .
998 (lambda unrestricted slots : (family LivenessSlots) .
999 (eliminate
1000 LivenessSlots
1001 (lambda unrestricted current : (family LivenessSlots) . (family LivenessOptionalSlot))
1002 slots
1003 (branch LivenessSlotsEnd . (constructor LivenessOptionalSlot LivenessNoSlot))
1004 (branch
1005 LivenessSlotsNext
1006 head
1007 tail
1008 ih_tail
1009 .
1010 (nat-eliminate
1011 (lambda unrestricted reusable : Nat . (family LivenessOptionalSlot))
1012 ih_tail
1013 (lambda unrestricted predecessor : Nat .
1014 (lambda unrestricted induction : (family LivenessOptionalSlot) .
1015 (eliminate
1016 LivenessOptionalSlot
1017 (lambda unrestricted current : (family LivenessOptionalSlot) .
1018 (family LivenessOptionalSlot))
1019 ih_tail
1020 (branch LivenessNoSlot . (constructor LivenessOptionalSlot LivenessSomeSlot head))
1021 (branch
1022 LivenessSomeSlot
1023 selected
1024 .
1025 (nat-eliminate
1026 (lambda unrestricted better : Nat . (family LivenessOptionalSlot))
1027 ih_tail
1028 (lambda unrestricted betterPredecessor : Nat .
1029 (lambda unrestricted ignored : (family LivenessOptionalSlot) .
1030 (constructor LivenessOptionalSlot LivenessSomeSlot head)))
1031 (livenessSlotBetter head selected))))))
1032 (livenessSlotReusable lifetime head))))))
1033
1034def livenessReplaceSlot =
1035 (lambda unrestricted oldSlot : (family LivenessSlot) .
1036 (lambda unrestricted newSlot : (family LivenessSlot) .
1037 (lambda unrestricted slots : (family LivenessSlots) .
1038 (eliminate
1039 LivenessSlot
1040 (lambda unrestricted current : (family LivenessSlot) . (family LivenessSlots))
1041 oldSlot
1042 (branch
1043 LivenessSlotValue
1044 oldOffset
1045 oldCapacity
1046 oldLastUse
1047 .
1048 (eliminate
1049 LivenessSlots
1050 (lambda unrestricted current : (family LivenessSlots) . (family LivenessSlots))
1051 slots
1052 (branch LivenessSlotsEnd . (constructor LivenessSlots LivenessSlotsEnd))
1053 (branch
1054 LivenessSlotsNext
1055 head
1056 tail
1057 ih_tail
1058 .
1059 (eliminate
1060 LivenessSlot
1061 (lambda unrestricted current : (family LivenessSlot) . (family LivenessSlots))
1062 head
1063 (branch
1064 LivenessSlotValue
1065 offset
1066 capacity
1067 lastUse
1068 .
1069 (nat-eliminate
1070 (lambda unrestricted sameOffset : Nat . (family LivenessSlots))
1071 (constructor LivenessSlots LivenessSlotsNext head ih_tail)
1072 (lambda unrestricted predecessor : Nat .
1073 (lambda unrestricted induction : (family LivenessSlots) .
1074 (constructor LivenessSlots LivenessSlotsNext newSlot tail)))
1075 (modelWord64Equal (stdByteCountValue offset) (stdByteCountValue oldOffset))))))))))))
1076
1077def livenessAlignUp =
1078 (lambda unrestricted value : (family ModelWord64) .
1079 (lambda unrestricted alignment : (family ModelWord64) .
1080 (app
1081 (lambda unrestricted mask : (family ModelWord64) .
1082 (eliminate
1083 ModelWord64CheckedResult
1084 (lambda unrestricted result : (family ModelWord64CheckedResult) .
1085 (family ModelWord64CheckedResult))
1086 (modelWord64AddChecked value mask)
1087 (branch
1088 ModelWord64CheckedSucceeded
1089 candidate
1090 .
1091 (constructor
1092 ModelWord64CheckedResult
1093 ModelWord64CheckedSucceeded
1094 (modelWord64And candidate (modelWord64Complement mask))))
1095 (branch
1096 ModelWord64CheckedFailed
1097 error
1098 .
1099 (constructor ModelWord64CheckedResult ModelWord64CheckedFailed error))))
1100 (modelWord64Subtract alignment modelWord64One))))
1101
1102def livenessPlaceOne =
1103 (lambda unrestricted arenaBytes : (family ModelWord64) .
1104 (lambda unrestricted lifetime : (family Lifetime) .
1105 (lambda unrestricted state : (family LivenessPlacementState) .
1106 (eliminate
1107 LivenessPlacementState
1108 (lambda unrestricted current : (family LivenessPlacementState) .
1109 (family LivenessPlacementStep))
1110 state
1111 (branch
1112 LivenessPlacementStateValue
1113 peak
1114 slots
1115 placements
1116 reused
1117 fresh
1118 .
1119 (eliminate
1120 Lifetime
1121 (lambda unrestricted current : (family Lifetime) . (family LivenessPlacementStep))
1122 lifetime
1123 (branch
1124 LifetimeValue
1125 tensor
1126 firstUse
1127 lastUse
1128 bytes
1129 alignment
1130 .
1131 (eliminate
1132 LivenessOptionalSlot
1133 (lambda unrestricted current : (family LivenessOptionalSlot) .
1134 (family LivenessPlacementStep))
1135 (livenessBestReusable lifetime slots)
1136 (branch
1137 LivenessNoSlot
1138 .
1139 (eliminate
1140 ModelWord64CheckedResult
1141 (lambda unrestricted result : (family ModelWord64CheckedResult) .
1142 (family LivenessPlacementStep))
1143 (livenessAlignUp (stdByteCountValue peak) (stdByteAlignmentValue alignment))
1144 (branch
1145 ModelWord64CheckedSucceeded
1146 offset
1147 .
1148 (eliminate
1149 ModelWord64CheckedResult
1150 (lambda unrestricted result : (family ModelWord64CheckedResult) .
1151 (family LivenessPlacementStep))
1152 (modelWord64AddChecked offset (stdByteCountValue bytes))
1153 (branch
1154 ModelWord64CheckedSucceeded
1155 end
1156 .
1157 (nat-eliminate
1158 (lambda unrestricted outside : Nat . (family LivenessPlacementStep))
1159 (constructor
1160 LivenessPlacementStep
1161 LivenessPlacementAdvanced
1162 (constructor
1163 LivenessPlacementState
1164 LivenessPlacementStateValue
1165 (stdByteCount end)
1166 (constructor
1167 LivenessSlots
1168 LivenessSlotsNext
1169 (constructor
1170 LivenessSlot
1171 LivenessSlotValue
1172 (stdByteCount offset)
1173 bytes
1174 lastUse)
1175 slots)
1176 (constructor
1177 Placements
1178 PlacementsNext
1179 (constructor
1180 Placement
1181 PlacementValue
1182 lifetime
1183 (stdByteCount offset)
1184 bytes)
1185 placements)
1186 reused
1187 (succ fresh)))
1188 (lambda unrestricted predecessor : Nat .
1189 (lambda unrestricted induction : (family LivenessPlacementStep) .
1190 (constructor
1191 LivenessPlacementStep
1192 LivenessPlacementStopped
1193 (constructor LivenessErrorCode PlacementArenaExhausted)
1194 state)))
1195 (modelWord64LessThan arenaBytes end)))
1196 (branch
1197 ModelWord64CheckedFailed
1198 error
1199 .
1200 (constructor
1201 LivenessPlacementStep
1202 LivenessPlacementStopped
1203 (constructor LivenessErrorCode PlacementArithmeticOverflow)
1204 state))))
1205 (branch
1206 ModelWord64CheckedFailed
1207 error
1208 .
1209 (constructor
1210 LivenessPlacementStep
1211 LivenessPlacementStopped
1212 (constructor LivenessErrorCode PlacementArithmeticOverflow)
1213 state))))
1214 (branch
1215 LivenessSomeSlot
1216 selected
1217 .
1218 (eliminate
1219 LivenessSlot
1220 (lambda unrestricted current : (family LivenessSlot) .
1221 (family LivenessPlacementStep))
1222 selected
1223 (branch
1224 LivenessSlotValue
1225 offset
1226 capacity
1227 previousLastUse
1228 .
1229 (constructor
1230 LivenessPlacementStep
1231 LivenessPlacementAdvanced
1232 (constructor
1233 LivenessPlacementState
1234 LivenessPlacementStateValue
1235 peak
1236 (livenessReplaceSlot
1237 selected
1238 (constructor LivenessSlot LivenessSlotValue offset capacity lastUse)
1239 slots)
1240 (constructor
1241 Placements
1242 PlacementsNext
1243 (constructor Placement PlacementValue lifetime offset capacity)
1244 placements)
1245 (succ reused)
1246 fresh)))))))))))))
1247
1248def livenessPlaceAll =
1249 (lambda unrestricted lifetimes : (family Lifetimes) .
1250 (eliminate
1251 Lifetimes
1252 (lambda unrestricted current : (family Lifetimes) .
1253 (pi unrestricted arenaBytes : (family ModelWord64) .
1254 (pi unrestricted state : (family LivenessPlacementState) . (family LivenessPlacementStep))))
1255 lifetimes
1256 (branch
1257 LifetimesEnd
1258 .
1259 (lambda unrestricted arenaBytes : (family ModelWord64) .
1260 (lambda unrestricted state : (family LivenessPlacementState) .
1261 (constructor LivenessPlacementStep LivenessPlacementAdvanced state))))
1262 (branch
1263 LifetimesNext
1264 head
1265 tail
1266 ih_tail
1267 .
1268 (lambda unrestricted arenaBytes : (family ModelWord64) .
1269 (lambda unrestricted state : (family LivenessPlacementState) .
1270 (eliminate
1271 LivenessPlacementStep
1272 (lambda unrestricted current : (family LivenessPlacementStep) .
1273 (family LivenessPlacementStep))
1274 (livenessPlaceOne arenaBytes head state)
1275 (branch LivenessPlacementAdvanced following . (ih_tail arenaBytes following))
1276 (branch
1277 LivenessPlacementStopped
1278 code
1279 stopped
1280 .
1281 (constructor LivenessPlacementStep LivenessPlacementStopped code stopped))))))))
1282
1283def livenessCompileTelemetryFor =
1284 (lambda unrestricted lifetimeCount : Nat .
1285 (lambda unrestricted arenaBytes : ByteCount .
1286 (lambda unrestricted state : (family LivenessPlacementState) .
1287 (lambda unrestricted succeeded : Nat .
1288 (lambda unrestricted failure : (family LivenessOptionalError) .
1289 (eliminate
1290 LivenessPlacementState
1291 (lambda unrestricted current : (family LivenessPlacementState) .
1292 (family LivenessCompileTelemetry))
1293 state
1294 (branch
1295 LivenessPlacementStateValue
1296 peak
1297 slots
1298 placements
1299 reused
1300 fresh
1301 .
1302 (constructor
1303 LivenessCompileTelemetry
1304 LivenessCompileTelemetryValue
1305 lifetimeCount
1306 (placementCount placements)
1307 reused
1308 fresh
1309 arenaBytes
1310 peak
1311 succeeded
1312 failure
1313 zero))))))))
1314
1315def compileMemoryPlanFail =
1316 (lambda unrestricted lifetimeCount : Nat .
1317 (lambda unrestricted arenaBytes : ByteCount .
1318 (lambda unrestricted state : (family LivenessPlacementState) .
1319 (lambda unrestricted code : (family LivenessErrorCode) .
1320 (constructor
1321 MemoryPlanCompileResult
1322 MemoryPlanCompileFailed
1323 code
1324 (livenessCompileTelemetryFor
1325 lifetimeCount
1326 arenaBytes
1327 state
1328 zero
1329 (constructor LivenessOptionalError LivenessSomeError code)))))))
1330
1331def firstLifetimeError =
1332 (lambda unrestricted lifetimes : (family Lifetimes) .
1333 (eliminate
1334 Lifetimes
1335 (lambda unrestricted current : (family Lifetimes) . (family LivenessOptionalError))
1336 lifetimes
1337 (branch LifetimesEnd . (constructor LivenessOptionalError LivenessNoError))
1338 (branch
1339 LifetimesNext
1340 head
1341 tail
1342 ih_tail
1343 .
1344 (nat-eliminate
1345 (lambda unrestricted valid : Nat . (family LivenessOptionalError))
1346 (constructor LivenessOptionalError LivenessSomeError (lifetimeError head))
1347 (lambda unrestricted predecessor : Nat .
1348 (lambda unrestricted induction : (family LivenessOptionalError) . ih_tail))
1349 (lifetimeIsValid head)))))
1350
1351def compileMemoryPlan =
1352 (lambda unrestricted arenaBytes : ByteCount .
1353 (lambda unrestricted lifetimes : (family Lifetimes) .
1354 (app
1355 (lambda unrestricted initial : (family LivenessPlacementState) .
1356 (app
1357 (lambda unrestricted lifetimeCount : Nat .
1358 (nat-eliminate
1359 (lambda unrestricted unique : Nat . (family MemoryPlanCompileResult))
1360 (compileMemoryPlanFail
1361 lifetimeCount
1362 arenaBytes
1363 initial
1364 (constructor LivenessErrorCode LifetimeTensorDuplicate))
1365 (lambda unrestricted predecessor : Nat .
1366 (lambda unrestricted induction : (family MemoryPlanCompileResult) .
1367 (eliminate
1368 LivenessOptionalError
1369 (lambda unrestricted current : (family LivenessOptionalError) .
1370 (family MemoryPlanCompileResult))
1371 (firstLifetimeError lifetimes)
1372 (branch
1373 LivenessNoError
1374 .
1375 (eliminate
1376 LivenessPlacementStep
1377 (lambda unrestricted current : (family LivenessPlacementStep) .
1378 (family MemoryPlanCompileResult))
1379 (livenessPlaceAll
1380 (lifetimesSort lifetimes)
1381 (stdByteCountValue arenaBytes)
1382 initial)
1383 (branch
1384 LivenessPlacementAdvanced
1385 state
1386 .
1387 (eliminate
1388 LivenessPlacementState
1389 (lambda unrestricted current : (family LivenessPlacementState) .
1390 (family MemoryPlanCompileResult))
1391 state
1392 (branch
1393 LivenessPlacementStateValue
1394 peak
1395 slots
1396 placements
1397 reused
1398 fresh
1399 .
1400 (app
1401 (lambda unrestricted plan : (family MemoryPlan) .
1402 (eliminate
1403 LivenessValidationResult
1404 (lambda unrestricted result : (family LivenessValidationResult) .
1405 (family MemoryPlanCompileResult))
1406 (validateMemoryPlan plan)
1407 (branch
1408 LivenessValidationPassed
1409 checked
1410 telemetry
1411 .
1412 (constructor
1413 MemoryPlanCompileResult
1414 MemoryPlanCompiled
1415 checked
1416 (livenessCompileTelemetryFor
1417 lifetimeCount
1418 arenaBytes
1419 state
1420 (succ zero)
1421 (constructor LivenessOptionalError LivenessNoError))))
1422 (branch
1423 LivenessValidationFailed
1424 code
1425 telemetry
1426 .
1427 (compileMemoryPlanFail
1428 lifetimeCount
1429 arenaBytes
1430 state
1431 (constructor LivenessErrorCode CompiledPlanRejected)))))
1432 (constructor
1433 MemoryPlan
1434 MemoryPlanValue
1435 arenaBytes
1436 peak
1437 (placementsReverse placements))))))
1438 (branch
1439 LivenessPlacementStopped
1440 code
1441 stopped
1442 .
1443 (compileMemoryPlanFail lifetimeCount arenaBytes stopped code))))
1444 (branch
1445 LivenessSomeError
1446 code
1447 .
1448 (compileMemoryPlanFail lifetimeCount arenaBytes initial code)))))
1449 (lifetimesUnique lifetimes)))
1450 (lifetimeCount lifetimes)))
1451 (constructor
1452 LivenessPlacementState
1453 LivenessPlacementStateValue
1454 (stdByteCount modelWord64Zero)
1455 (constructor LivenessSlots LivenessSlotsEnd)
1456 (constructor Placements PlacementsEnd)
1457 zero
1458 zero))))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.