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)))))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.