module Compiler.Planning.Liveness import Model.Parameter import Model.Word32 import Model.Word64 import Std.Natural import Std.Physical import Model.Config family TensorId : Type 0 constructor TensorIdValue field unrestricted tensorIdWord : (family ModelWord32) end-family family Lifetime : Type 0 constructor LifetimeValue field unrestricted lifetimeTensor : (family TensorId) field unrestricted lifetimeFirstUse : (family ModelWord32) field unrestricted lifetimeLastUse : (family ModelWord32) field unrestricted lifetimeBytes : ByteCount field unrestricted lifetimeAlignment : ByteAlignment end-family family Lifetimes : Type 0 constructor LifetimesEnd constructor LifetimesNext field unrestricted lifetimeHead : (family Lifetime) recursive unrestricted lifetimeTail end-family family Placement : Type 0 constructor PlacementValue field unrestricted placementLifetime : (family Lifetime) field unrestricted placementOffset : ByteCount field unrestricted placementCapacity : ByteCount end-family family Placements : Type 0 constructor PlacementsEnd constructor PlacementsNext field unrestricted placementHead : (family Placement) recursive unrestricted placementTail end-family family MemoryPlan : Type 0 constructor MemoryPlanValue field unrestricted planArenaBytes : ByteCount field unrestricted planPeakBytes : ByteCount field unrestricted planPlacements : (family Placements) end-family family LivenessErrorCode : Type 0 constructor LifetimeTensorDuplicate constructor LifetimeIntervalInvalid constructor LifetimeBytesZero constructor LifetimeAlignmentInvalid constructor PlanPeakExceedsArena constructor PlacementMisaligned constructor PlacementCapacityTooSmall constructor PlacementRangeOverflow constructor PlacementOutsideArena constructor PlacementLiveCollision constructor PlacementArithmeticOverflow constructor PlacementArenaExhausted constructor CompiledPlanRejected end-family family LivenessOptionalError : Type 0 constructor LivenessNoError constructor LivenessSomeError field unrestricted livenessError : (family LivenessErrorCode) end-family family LivenessTelemetry : Type 0 constructor LivenessTelemetryValue field unrestricted livenessLifetimeCount : Nat field unrestricted livenessPlacementCount : Nat field unrestricted livenessInvalidLifetimeCount : Nat field unrestricted livenessInvalidPlacementCount : Nat field unrestricted livenessCollisionCount : Nat field unrestricted livenessArenaBytes : ByteCount field unrestricted livenessPeakBytes : ByteCount field unrestricted livenessSucceeded : Nat field unrestricted livenessFailure : (family LivenessOptionalError) field unrestricted livenessHostFallbacks : Nat end-family family LivenessValidationResult : Type 0 constructor LivenessValidationPassed field unrestricted livenessValidatedPlan : (family MemoryPlan) field unrestricted livenessPassedTelemetry : (family LivenessTelemetry) constructor LivenessValidationFailed field unrestricted livenessFailureCode : (family LivenessErrorCode) field unrestricted livenessFailedTelemetry : (family LivenessTelemetry) end-family family LivenessSlot : Type 0 constructor LivenessSlotValue field unrestricted livenessSlotOffset : ByteCount field unrestricted livenessSlotCapacity : ByteCount field unrestricted livenessSlotLastUse : (family ModelWord32) end-family family LivenessSlots : Type 0 constructor LivenessSlotsEnd constructor LivenessSlotsNext field unrestricted livenessSlotHead : (family LivenessSlot) recursive unrestricted livenessSlotTail end-family family LivenessOptionalSlot : Type 0 constructor LivenessNoSlot constructor LivenessSomeSlot field unrestricted livenessSelectedSlot : (family LivenessSlot) end-family family LivenessPlacementState : Type 0 constructor LivenessPlacementStateValue field unrestricted livenessStatePeak : ByteCount field unrestricted livenessStateSlots : (family LivenessSlots) field unrestricted livenessStatePlacements : (family Placements) field unrestricted livenessStateReusedSlots : Nat field unrestricted livenessStateFreshSlots : Nat end-family family LivenessPlacementStep : Type 0 constructor LivenessPlacementAdvanced field unrestricted livenessAdvancedState : (family LivenessPlacementState) constructor LivenessPlacementStopped field unrestricted livenessPlacementFailure : (family LivenessErrorCode) field unrestricted livenessStoppedState : (family LivenessPlacementState) end-family family LivenessCompileTelemetry : Type 0 constructor LivenessCompileTelemetryValue field unrestricted livenessCompileLifetimeCount : Nat field unrestricted livenessCompilePlacementCount : Nat field unrestricted livenessCompileReusedSlots : Nat field unrestricted livenessCompileFreshSlots : Nat field unrestricted livenessCompileArenaBytes : ByteCount field unrestricted livenessCompilePeakBytes : ByteCount field unrestricted livenessCompileSucceeded : Nat field unrestricted livenessCompileFailure : (family LivenessOptionalError) field unrestricted livenessCompileHostFallbacks : Nat end-family family MemoryPlanCompileResult : Type 0 constructor MemoryPlanCompiled field unrestricted compiledMemoryPlan : (family MemoryPlan) field unrestricted memoryPlanCompileTelemetry : (family LivenessCompileTelemetry) constructor MemoryPlanCompileFailed field unrestricted memoryPlanCompileFailure : (family LivenessErrorCode) field unrestricted memoryPlanFailureTelemetry : (family LivenessCompileTelemetry) end-family def livenessErrorCodeBytes = (lambda unrestricted code : (family LivenessErrorCode) . (eliminate LivenessErrorCode (lambda unrestricted current : (family LivenessErrorCode) . Bytes) code (branch LifetimeTensorDuplicate . b"ALPHA-GAIA-LIV-001") (branch LifetimeIntervalInvalid . b"ALPHA-GAIA-LIV-002") (branch LifetimeBytesZero . b"ALPHA-GAIA-LIV-003") (branch LifetimeAlignmentInvalid . b"ALPHA-GAIA-LIV-004") (branch PlanPeakExceedsArena . b"ALPHA-GAIA-LIV-005") (branch PlacementMisaligned . b"ALPHA-GAIA-LIV-006") (branch PlacementCapacityTooSmall . b"ALPHA-GAIA-LIV-007") (branch PlacementRangeOverflow . b"ALPHA-GAIA-LIV-008") (branch PlacementOutsideArena . b"ALPHA-GAIA-LIV-009") (branch PlacementLiveCollision . b"ALPHA-GAIA-LIV-010") (branch PlacementArithmeticOverflow . b"ALPHA-GAIA-LIV-011") (branch PlacementArenaExhausted . b"ALPHA-GAIA-LIV-012") (branch CompiledPlanRejected . b"ALPHA-GAIA-LIV-013"))) def naturalFlagNot = (lambda unrestricted value : Nat . (nat-eliminate (lambda unrestricted current : Nat . Nat) (succ zero) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero)) value)) def naturalFlagAnd = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-eliminate (lambda unrestricted current : Nat . Nat) zero (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . right)) left))) def naturalFlagOr = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (nat-eliminate (lambda unrestricted current : Nat . Nat) right (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (succ zero))) left))) def livenessNaturalEqual = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (naturalFlagNot (naturalFlagOr (nat-less-than left right) (nat-less-than right left))))) def naturalLessThanOrEqual = (lambda unrestricted left : Nat . (lambda unrestricted right : Nat . (naturalFlagNot (nat-less-than right left)))) def word64LessThanOrEqual = (lambda unrestricted left : (family ModelWord64) . (lambda unrestricted right : (family ModelWord64) . (naturalFlagOr (modelWord64LessThan left right) (modelWord64Equal left right)))) def tensorIdEqual = (lambda unrestricted left : (family TensorId) . (lambda unrestricted right : (family TensorId) . (eliminate TensorId (lambda unrestricted current : (family TensorId) . Nat) left (branch TensorIdValue leftWord . (eliminate TensorId (lambda unrestricted current : (family TensorId) . Nat) right (branch TensorIdValue rightWord . (livenessNaturalEqual (modelWord32ToNatural leftWord) (modelWord32ToNatural rightWord)))))))) def alignmentValid = (lambda unrestricted alignment : (family ModelWord64) . (nat-eliminate (lambda unrestricted alignmentIsZero : Nat . Nat) (modelWord64IsZero (modelWord64And alignment (modelWord64Subtract alignment modelWord64One))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero)) (modelWord64IsZero alignment))) def lifetimeTensorId = (lambda unrestricted lifetime : (family Lifetime) . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . (family TensorId)) lifetime (branch LifetimeValue tensor firstUse lastUse bytes alignment . tensor))) -- Remote reads retain the existing allocation through transport completion. -- Extending an earlier bound is monotone: a transfer cannot accidentally -- shorten an activation's already-established local lifetime. def retainLifetimeThrough = (lambda unrestricted remoteLastRead : (family ModelWord32) . (lambda unrestricted lifetime : (family Lifetime) . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . (family Lifetime)) lifetime (branch LifetimeValue tensor firstUse lastUse bytes alignment . (nat-eliminate (lambda unrestricted flag : Nat . (family Lifetime)) lifetime (lambda unrestricted previous : Nat . (lambda unrestricted ignored : (family Lifetime) . (constructor Lifetime LifetimeValue tensor firstUse remoteLastRead bytes alignment))) (naturalLess (modelWord32ToNatural lastUse) (modelWord32ToNatural remoteLastRead))))))) def lifetimeIsValid = (lambda unrestricted lifetime : (family Lifetime) . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . Nat) lifetime (branch LifetimeValue tensor firstUse lastUse bytes alignment . (naturalFlagAnd (naturalLessThanOrEqual (modelWord32ToNatural firstUse) (modelWord32ToNatural lastUse)) (naturalFlagAnd (naturalFlagNot (modelWord64IsZero (stdByteCountValue bytes))) (alignmentValid (stdByteAlignmentValue alignment))))))) def lifetimeError = (lambda unrestricted lifetime : (family Lifetime) . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . (family LivenessErrorCode)) lifetime (branch LifetimeValue tensor firstUse lastUse bytes alignment . (nat-eliminate (lambda unrestricted intervalInvalid : Nat . (family LivenessErrorCode)) (nat-eliminate (lambda unrestricted bytesAreZero : Nat . (family LivenessErrorCode)) (constructor LivenessErrorCode LifetimeAlignmentInvalid) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessErrorCode) . (constructor LivenessErrorCode LifetimeBytesZero))) (modelWord64IsZero (stdByteCountValue bytes))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessErrorCode) . (constructor LivenessErrorCode LifetimeIntervalInvalid))) (nat-less-than (modelWord32ToNatural lastUse) (modelWord32ToNatural firstUse)))))) def lifetimeIdOccurs = (lambda unrestricted tensor : (family TensorId) . (lambda unrestricted lifetimes : (family Lifetimes) . (eliminate Lifetimes (lambda unrestricted current : (family Lifetimes) . Nat) lifetimes (branch LifetimesEnd . zero) (branch LifetimesNext head tail ih_tail . (naturalFlagOr (tensorIdEqual tensor (lifetimeTensorId head)) ih_tail))))) def lifetimesUnique = (lambda unrestricted lifetimes : (family Lifetimes) . (eliminate Lifetimes (lambda unrestricted current : (family Lifetimes) . Nat) lifetimes (branch LifetimesEnd . (succ zero)) (branch LifetimesNext head tail ih_tail . (naturalFlagAnd (naturalFlagNot (lifetimeIdOccurs (lifetimeTensorId head) tail)) ih_tail)))) def lifetimesValid = (lambda unrestricted lifetimes : (family Lifetimes) . (eliminate Lifetimes (lambda unrestricted current : (family Lifetimes) . Nat) lifetimes (branch LifetimesEnd . (succ zero)) (branch LifetimesNext head tail ih_tail . (naturalFlagAnd (lifetimeIsValid head) ih_tail)))) def lifetimeCount = (lambda unrestricted lifetimes : (family Lifetimes) . (eliminate Lifetimes (lambda unrestricted current : (family Lifetimes) . Nat) lifetimes (branch LifetimesEnd . zero) (branch LifetimesNext head tail ih_tail . (succ ih_tail)))) def placementCount = (lambda unrestricted placements : (family Placements) . (eliminate Placements (lambda unrestricted current : (family Placements) . Nat) placements (branch PlacementsEnd . zero) (branch PlacementsNext head tail ih_tail . (succ ih_tail)))) def placementLifetimeList = (lambda unrestricted placements : (family Placements) . (eliminate Placements (lambda unrestricted current : (family Placements) . (family Lifetimes)) placements (branch PlacementsEnd . (constructor Lifetimes LifetimesEnd)) (branch PlacementsNext head tail ih_tail . (eliminate Placement (lambda unrestricted current : (family Placement) . (family Lifetimes)) head (branch PlacementValue lifetime offset capacity . (constructor Lifetimes LifetimesNext lifetime ih_tail)))))) def placementAligned = (lambda unrestricted placement : (family Placement) . (eliminate Placement (lambda unrestricted current : (family Placement) . Nat) placement (branch PlacementValue lifetime offset capacity . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . Nat) lifetime (branch LifetimeValue tensor firstUse lastUse bytes alignment . (modelWord64IsZero (modelWord64And (stdByteCountValue offset) (modelWord64Subtract (stdByteAlignmentValue alignment) modelWord64One)))))))) def placementCapacityValid = (lambda unrestricted placement : (family Placement) . (eliminate Placement (lambda unrestricted current : (family Placement) . Nat) placement (branch PlacementValue lifetime offset capacity . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . Nat) lifetime (branch LifetimeValue tensor firstUse lastUse bytes alignment . (word64LessThanOrEqual (stdByteCountValue bytes) (stdByteCountValue capacity))))))) def placementRangeValid = (lambda unrestricted arenaBytes : ByteCount . (lambda unrestricted placement : (family Placement) . (eliminate Placement (lambda unrestricted current : (family Placement) . Nat) placement (branch PlacementValue lifetime offset capacity . (eliminate ModelWord64CheckedResult (lambda unrestricted result : (family ModelWord64CheckedResult) . Nat) (modelWord64AddChecked (stdByteCountValue offset) (stdByteCountValue capacity)) (branch ModelWord64CheckedSucceeded end . (word64LessThanOrEqual end (stdByteCountValue arenaBytes))) (branch ModelWord64CheckedFailed error . zero)))))) def placementIsValid = (lambda unrestricted arenaBytes : ByteCount . (lambda unrestricted placement : (family Placement) . (eliminate Placement (lambda unrestricted current : (family Placement) . Nat) placement (branch PlacementValue lifetime offset capacity . (naturalFlagAnd (lifetimeIsValid lifetime) (naturalFlagAnd (placementAligned placement) (naturalFlagAnd (placementCapacityValid placement) (placementRangeValid arenaBytes placement)))))))) def placementInvalidCount = (lambda unrestricted arenaBytes : ByteCount . (lambda unrestricted placements : (family Placements) . (eliminate Placements (lambda unrestricted current : (family Placements) . Nat) placements (branch PlacementsEnd . zero) (branch PlacementsNext head tail ih_tail . (naturalAdd (naturalFlagNot (placementIsValid arenaBytes head)) ih_tail))))) def placementsValid = (lambda unrestricted arenaBytes : ByteCount . (lambda unrestricted placements : (family Placements) . (naturalFlagNot (naturalFlagNot (livenessNaturalEqual (placementInvalidCount arenaBytes placements) zero))))) def placementCollision = (lambda unrestricted left : (family Placement) . (lambda unrestricted right : (family Placement) . (eliminate Placement (lambda unrestricted current : (family Placement) . Nat) left (branch PlacementValue leftLifetime leftOffset leftCapacity . (eliminate Placement (lambda unrestricted current : (family Placement) . Nat) right (branch PlacementValue rightLifetime rightOffset rightCapacity . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . Nat) leftLifetime (branch LifetimeValue leftTensor leftFirst leftLast leftBytes leftAlignment . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . Nat) rightLifetime (branch LifetimeValue rightTensor rightFirst rightLast rightBytes rightAlignment . (eliminate ModelWord64CheckedResult (lambda unrestricted result : (family ModelWord64CheckedResult) . Nat) (modelWord64AddChecked (stdByteCountValue leftOffset) (stdByteCountValue leftBytes)) (branch ModelWord64CheckedSucceeded leftEnd . (eliminate ModelWord64CheckedResult (lambda unrestricted result : (family ModelWord64CheckedResult) . Nat) (modelWord64AddChecked (stdByteCountValue rightOffset) (stdByteCountValue rightBytes)) (branch ModelWord64CheckedSucceeded rightEnd . (naturalFlagAnd (naturalFlagAnd (naturalLessThanOrEqual (modelWord32ToNatural leftFirst) (modelWord32ToNatural rightLast)) (naturalLessThanOrEqual (modelWord32ToNatural rightFirst) (modelWord32ToNatural leftLast))) (naturalFlagAnd (modelWord64LessThan (stdByteCountValue leftOffset) rightEnd) (modelWord64LessThan (stdByteCountValue rightOffset) leftEnd)))) (branch ModelWord64CheckedFailed error . (succ zero)))) (branch ModelWord64CheckedFailed error . (succ zero))))))))))))) def placementCollisionCountWith = (lambda unrestricted placement : (family Placement) . (lambda unrestricted others : (family Placements) . (eliminate Placements (lambda unrestricted current : (family Placements) . Nat) others (branch PlacementsEnd . zero) (branch PlacementsNext head tail ih_tail . (naturalAdd (placementCollision placement head) ih_tail))))) def placementCollisionCount = (lambda unrestricted placements : (family Placements) . (eliminate Placements (lambda unrestricted current : (family Placements) . Nat) placements (branch PlacementsEnd . zero) (branch PlacementsNext head tail ih_tail . (naturalAdd (placementCollisionCountWith head tail) ih_tail)))) def livenessTelemetryFor = (lambda unrestricted plan : (family MemoryPlan) . (lambda unrestricted succeeded : Nat . (lambda unrestricted failure : (family LivenessOptionalError) . (eliminate MemoryPlan (lambda unrestricted current : (family MemoryPlan) . (family LivenessTelemetry)) plan (branch MemoryPlanValue arenaBytes peakBytes placements . (app (lambda unrestricted lifetimes : (family Lifetimes) . (constructor LivenessTelemetry LivenessTelemetryValue (lifetimeCount lifetimes) (placementCount placements) (naturalFlagNot (lifetimesValid lifetimes)) (placementInvalidCount arenaBytes placements) (placementCollisionCount placements) arenaBytes peakBytes succeeded failure zero)) (placementLifetimeList placements))))))) def livenessFailureResult = (lambda unrestricted plan : (family MemoryPlan) . (lambda unrestricted code : (family LivenessErrorCode) . (constructor LivenessValidationResult LivenessValidationFailed code (livenessTelemetryFor plan zero (constructor LivenessOptionalError LivenessSomeError code))))) def validatePlacements = (lambda unrestricted arenaBytes : ByteCount . (lambda unrestricted placements : (family Placements) . (eliminate Placements (lambda unrestricted current : (family Placements) . (family LivenessOptionalError)) placements (branch PlacementsEnd . (constructor LivenessOptionalError LivenessNoError)) (branch PlacementsNext head tail ih_tail . (nat-eliminate (lambda unrestricted lifetimeInvalid : Nat . (family LivenessOptionalError)) (nat-eliminate (lambda unrestricted misaligned : Nat . (family LivenessOptionalError)) (nat-eliminate (lambda unrestricted capacityInvalid : Nat . (family LivenessOptionalError)) (nat-eliminate (lambda unrestricted rangeInvalid : Nat . (family LivenessOptionalError)) ih_tail (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessOptionalError) . (constructor LivenessOptionalError LivenessSomeError (constructor LivenessErrorCode PlacementOutsideArena)))) (naturalFlagNot (placementRangeValid arenaBytes head))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessOptionalError) . (constructor LivenessOptionalError LivenessSomeError (constructor LivenessErrorCode PlacementCapacityTooSmall)))) (naturalFlagNot (placementCapacityValid head))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessOptionalError) . (constructor LivenessOptionalError LivenessSomeError (constructor LivenessErrorCode PlacementMisaligned)))) (naturalFlagNot (placementAligned head))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessOptionalError) . (eliminate Placement (lambda unrestricted current : (family Placement) . (family LivenessOptionalError)) head (branch PlacementValue lifetime offset capacity . (constructor LivenessOptionalError LivenessSomeError (lifetimeError lifetime)))))) (naturalFlagNot (eliminate Placement (lambda unrestricted current : (family Placement) . Nat) head (branch PlacementValue lifetime offset capacity . (lifetimeIsValid lifetime))))))))) def validateMemoryPlan = (lambda unrestricted plan : (family MemoryPlan) . (eliminate MemoryPlan (lambda unrestricted current : (family MemoryPlan) . (family LivenessValidationResult)) plan (branch MemoryPlanValue arenaBytes peakBytes placements . (app (lambda unrestricted lifetimes : (family Lifetimes) . (nat-eliminate (lambda unrestricted duplicateIds : Nat . (family LivenessValidationResult)) (nat-eliminate (lambda unrestricted peakInvalid : Nat . (family LivenessValidationResult)) (eliminate LivenessOptionalError (lambda unrestricted current : (family LivenessOptionalError) . (family LivenessValidationResult)) (validatePlacements arenaBytes placements) (branch LivenessNoError . (nat-eliminate (lambda unrestricted collisionsZero : Nat . (family LivenessValidationResult)) (livenessFailureResult plan (constructor LivenessErrorCode PlacementLiveCollision)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessValidationResult) . (constructor LivenessValidationResult LivenessValidationPassed plan (livenessTelemetryFor plan (succ zero) (constructor LivenessOptionalError LivenessNoError))))) (naturalFlagNot (placementCollisionCount placements)))) (branch LivenessSomeError error . (livenessFailureResult plan error))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessValidationResult) . (livenessFailureResult plan (constructor LivenessErrorCode PlanPeakExceedsArena)))) (modelWord64LessThan (stdByteCountValue arenaBytes) (stdByteCountValue peakBytes))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessValidationResult) . (livenessFailureResult plan (constructor LivenessErrorCode LifetimeTensorDuplicate)))) (naturalFlagNot (lifetimesUnique lifetimes)))) (placementLifetimeList placements))))) -- Fixed-shape liveness compilation. The result is a checked arena plan, not a -- runtime request to substitute a different tensor shape. def lifetimeComesBeforeOrEqual = (lambda unrestricted left : (family Lifetime) . (lambda unrestricted right : (family Lifetime) . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . Nat) left (branch LifetimeValue leftTensor leftFirst leftLast leftBytes leftAlignment . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . Nat) right (branch LifetimeValue rightTensor rightFirst rightLast rightBytes rightAlignment . (naturalFlagOr (nat-less-than (modelWord32ToNatural leftFirst) (modelWord32ToNatural rightFirst)) (naturalFlagAnd (livenessNaturalEqual (modelWord32ToNatural leftFirst) (modelWord32ToNatural rightFirst)) (eliminate TensorId (lambda unrestricted current : (family TensorId) . Nat) leftTensor (branch TensorIdValue leftId . (eliminate TensorId (lambda unrestricted current : (family TensorId) . Nat) rightTensor (branch TensorIdValue rightId . (naturalLessThanOrEqual (modelWord32ToNatural leftId) (modelWord32ToNatural rightId)))))))))))))) def lifetimesInsert = (lambda unrestricted lifetime : (family Lifetime) . (lambda unrestricted ordered : (family Lifetimes) . (eliminate Lifetimes (lambda unrestricted current : (family Lifetimes) . (family Lifetimes)) ordered (branch LifetimesEnd . (constructor Lifetimes LifetimesNext lifetime (constructor Lifetimes LifetimesEnd))) (branch LifetimesNext head tail ih_tail . (nat-eliminate (lambda unrestricted before : Nat . (family Lifetimes)) (constructor Lifetimes LifetimesNext head ih_tail) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family Lifetimes) . (constructor Lifetimes LifetimesNext lifetime ordered))) (lifetimeComesBeforeOrEqual lifetime head)))))) def lifetimesSort = (lambda unrestricted lifetimes : (family Lifetimes) . (eliminate Lifetimes (lambda unrestricted current : (family Lifetimes) . (family Lifetimes)) lifetimes (branch LifetimesEnd . (constructor Lifetimes LifetimesEnd)) (branch LifetimesNext head tail ih_tail . (lifetimesInsert head ih_tail)))) def placementsReverseOnto = (lambda unrestricted input : (family Placements) . (eliminate Placements (lambda unrestricted current : (family Placements) . (pi unrestricted output : (family Placements) . (family Placements))) input (branch PlacementsEnd . (lambda unrestricted output : (family Placements) . output)) (branch PlacementsNext head tail ih_tail . (lambda unrestricted output : (family Placements) . (ih_tail (constructor Placements PlacementsNext head output)))))) def placementsReverse = (lambda unrestricted placements : (family Placements) . (placementsReverseOnto placements (constructor Placements PlacementsEnd))) def livenessSlotReusable = (lambda unrestricted lifetime : (family Lifetime) . (lambda unrestricted slot : (family LivenessSlot) . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . Nat) lifetime (branch LifetimeValue tensor firstUse lastUse bytes alignment . (eliminate LivenessSlot (lambda unrestricted current : (family LivenessSlot) . Nat) slot (branch LivenessSlotValue offset capacity slotLastUse . (naturalFlagAnd (nat-less-than (modelWord32ToNatural slotLastUse) (modelWord32ToNatural firstUse)) (naturalFlagAnd (word64LessThanOrEqual (stdByteCountValue bytes) (stdByteCountValue capacity)) (modelWord64IsZero (modelWord64And (stdByteCountValue offset) (modelWord64Subtract (stdByteAlignmentValue alignment) modelWord64One))))))))))) def livenessSlotBetter = (lambda unrestricted candidate : (family LivenessSlot) . (lambda unrestricted current : (family LivenessSlot) . (eliminate LivenessSlot (lambda unrestricted value : (family LivenessSlot) . Nat) candidate (branch LivenessSlotValue candidateOffset candidateCapacity candidateLastUse . (eliminate LivenessSlot (lambda unrestricted value : (family LivenessSlot) . Nat) current (branch LivenessSlotValue currentOffset currentCapacity currentLastUse . (naturalFlagOr (modelWord64LessThan (stdByteCountValue candidateCapacity) (stdByteCountValue currentCapacity)) (naturalFlagAnd (modelWord64Equal (stdByteCountValue candidateCapacity) (stdByteCountValue currentCapacity)) (modelWord64LessThan (stdByteCountValue candidateOffset) (stdByteCountValue currentOffset)))))))))) def livenessBestReusable = (lambda unrestricted lifetime : (family Lifetime) . (lambda unrestricted slots : (family LivenessSlots) . (eliminate LivenessSlots (lambda unrestricted current : (family LivenessSlots) . (family LivenessOptionalSlot)) slots (branch LivenessSlotsEnd . (constructor LivenessOptionalSlot LivenessNoSlot)) (branch LivenessSlotsNext head tail ih_tail . (nat-eliminate (lambda unrestricted reusable : Nat . (family LivenessOptionalSlot)) ih_tail (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessOptionalSlot) . (eliminate LivenessOptionalSlot (lambda unrestricted current : (family LivenessOptionalSlot) . (family LivenessOptionalSlot)) ih_tail (branch LivenessNoSlot . (constructor LivenessOptionalSlot LivenessSomeSlot head)) (branch LivenessSomeSlot selected . (nat-eliminate (lambda unrestricted better : Nat . (family LivenessOptionalSlot)) ih_tail (lambda unrestricted betterPredecessor : Nat . (lambda unrestricted ignored : (family LivenessOptionalSlot) . (constructor LivenessOptionalSlot LivenessSomeSlot head))) (livenessSlotBetter head selected)))))) (livenessSlotReusable lifetime head)))))) def livenessReplaceSlot = (lambda unrestricted oldSlot : (family LivenessSlot) . (lambda unrestricted newSlot : (family LivenessSlot) . (lambda unrestricted slots : (family LivenessSlots) . (eliminate LivenessSlot (lambda unrestricted current : (family LivenessSlot) . (family LivenessSlots)) oldSlot (branch LivenessSlotValue oldOffset oldCapacity oldLastUse . (eliminate LivenessSlots (lambda unrestricted current : (family LivenessSlots) . (family LivenessSlots)) slots (branch LivenessSlotsEnd . (constructor LivenessSlots LivenessSlotsEnd)) (branch LivenessSlotsNext head tail ih_tail . (eliminate LivenessSlot (lambda unrestricted current : (family LivenessSlot) . (family LivenessSlots)) head (branch LivenessSlotValue offset capacity lastUse . (nat-eliminate (lambda unrestricted sameOffset : Nat . (family LivenessSlots)) (constructor LivenessSlots LivenessSlotsNext head ih_tail) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessSlots) . (constructor LivenessSlots LivenessSlotsNext newSlot tail))) (modelWord64Equal (stdByteCountValue offset) (stdByteCountValue oldOffset)))))))))))) def livenessAlignUp = (lambda unrestricted value : (family ModelWord64) . (lambda unrestricted alignment : (family ModelWord64) . (app (lambda unrestricted mask : (family ModelWord64) . (eliminate ModelWord64CheckedResult (lambda unrestricted result : (family ModelWord64CheckedResult) . (family ModelWord64CheckedResult)) (modelWord64AddChecked value mask) (branch ModelWord64CheckedSucceeded candidate . (constructor ModelWord64CheckedResult ModelWord64CheckedSucceeded (modelWord64And candidate (modelWord64Complement mask)))) (branch ModelWord64CheckedFailed error . (constructor ModelWord64CheckedResult ModelWord64CheckedFailed error)))) (modelWord64Subtract alignment modelWord64One)))) def livenessPlaceOne = (lambda unrestricted arenaBytes : (family ModelWord64) . (lambda unrestricted lifetime : (family Lifetime) . (lambda unrestricted state : (family LivenessPlacementState) . (eliminate LivenessPlacementState (lambda unrestricted current : (family LivenessPlacementState) . (family LivenessPlacementStep)) state (branch LivenessPlacementStateValue peak slots placements reused fresh . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . (family LivenessPlacementStep)) lifetime (branch LifetimeValue tensor firstUse lastUse bytes alignment . (eliminate LivenessOptionalSlot (lambda unrestricted current : (family LivenessOptionalSlot) . (family LivenessPlacementStep)) (livenessBestReusable lifetime slots) (branch LivenessNoSlot . (eliminate ModelWord64CheckedResult (lambda unrestricted result : (family ModelWord64CheckedResult) . (family LivenessPlacementStep)) (livenessAlignUp (stdByteCountValue peak) (stdByteAlignmentValue alignment)) (branch ModelWord64CheckedSucceeded offset . (eliminate ModelWord64CheckedResult (lambda unrestricted result : (family ModelWord64CheckedResult) . (family LivenessPlacementStep)) (modelWord64AddChecked offset (stdByteCountValue bytes)) (branch ModelWord64CheckedSucceeded end . (nat-eliminate (lambda unrestricted outside : Nat . (family LivenessPlacementStep)) (constructor LivenessPlacementStep LivenessPlacementAdvanced (constructor LivenessPlacementState LivenessPlacementStateValue (stdByteCount end) (constructor LivenessSlots LivenessSlotsNext (constructor LivenessSlot LivenessSlotValue (stdByteCount offset) bytes lastUse) slots) (constructor Placements PlacementsNext (constructor Placement PlacementValue lifetime (stdByteCount offset) bytes) placements) reused (succ fresh))) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessPlacementStep) . (constructor LivenessPlacementStep LivenessPlacementStopped (constructor LivenessErrorCode PlacementArenaExhausted) state))) (modelWord64LessThan arenaBytes end))) (branch ModelWord64CheckedFailed error . (constructor LivenessPlacementStep LivenessPlacementStopped (constructor LivenessErrorCode PlacementArithmeticOverflow) state)))) (branch ModelWord64CheckedFailed error . (constructor LivenessPlacementStep LivenessPlacementStopped (constructor LivenessErrorCode PlacementArithmeticOverflow) state)))) (branch LivenessSomeSlot selected . (eliminate LivenessSlot (lambda unrestricted current : (family LivenessSlot) . (family LivenessPlacementStep)) selected (branch LivenessSlotValue offset capacity previousLastUse . (constructor LivenessPlacementStep LivenessPlacementAdvanced (constructor LivenessPlacementState LivenessPlacementStateValue peak (livenessReplaceSlot selected (constructor LivenessSlot LivenessSlotValue offset capacity lastUse) slots) (constructor Placements PlacementsNext (constructor Placement PlacementValue lifetime offset capacity) placements) (succ reused) fresh))))))))))))) def livenessPlaceAll = (lambda unrestricted lifetimes : (family Lifetimes) . (eliminate Lifetimes (lambda unrestricted current : (family Lifetimes) . (pi unrestricted arenaBytes : (family ModelWord64) . (pi unrestricted state : (family LivenessPlacementState) . (family LivenessPlacementStep)))) lifetimes (branch LifetimesEnd . (lambda unrestricted arenaBytes : (family ModelWord64) . (lambda unrestricted state : (family LivenessPlacementState) . (constructor LivenessPlacementStep LivenessPlacementAdvanced state)))) (branch LifetimesNext head tail ih_tail . (lambda unrestricted arenaBytes : (family ModelWord64) . (lambda unrestricted state : (family LivenessPlacementState) . (eliminate LivenessPlacementStep (lambda unrestricted current : (family LivenessPlacementStep) . (family LivenessPlacementStep)) (livenessPlaceOne arenaBytes head state) (branch LivenessPlacementAdvanced following . (ih_tail arenaBytes following)) (branch LivenessPlacementStopped code stopped . (constructor LivenessPlacementStep LivenessPlacementStopped code stopped)))))))) def livenessCompileTelemetryFor = (lambda unrestricted lifetimeCount : Nat . (lambda unrestricted arenaBytes : ByteCount . (lambda unrestricted state : (family LivenessPlacementState) . (lambda unrestricted succeeded : Nat . (lambda unrestricted failure : (family LivenessOptionalError) . (eliminate LivenessPlacementState (lambda unrestricted current : (family LivenessPlacementState) . (family LivenessCompileTelemetry)) state (branch LivenessPlacementStateValue peak slots placements reused fresh . (constructor LivenessCompileTelemetry LivenessCompileTelemetryValue lifetimeCount (placementCount placements) reused fresh arenaBytes peak succeeded failure zero)))))))) def compileMemoryPlanFail = (lambda unrestricted lifetimeCount : Nat . (lambda unrestricted arenaBytes : ByteCount . (lambda unrestricted state : (family LivenessPlacementState) . (lambda unrestricted code : (family LivenessErrorCode) . (constructor MemoryPlanCompileResult MemoryPlanCompileFailed code (livenessCompileTelemetryFor lifetimeCount arenaBytes state zero (constructor LivenessOptionalError LivenessSomeError code))))))) def firstLifetimeError = (lambda unrestricted lifetimes : (family Lifetimes) . (eliminate Lifetimes (lambda unrestricted current : (family Lifetimes) . (family LivenessOptionalError)) lifetimes (branch LifetimesEnd . (constructor LivenessOptionalError LivenessNoError)) (branch LifetimesNext head tail ih_tail . (nat-eliminate (lambda unrestricted valid : Nat . (family LivenessOptionalError)) (constructor LivenessOptionalError LivenessSomeError (lifetimeError head)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family LivenessOptionalError) . ih_tail)) (lifetimeIsValid head))))) def compileMemoryPlan = (lambda unrestricted arenaBytes : ByteCount . (lambda unrestricted lifetimes : (family Lifetimes) . (app (lambda unrestricted initial : (family LivenessPlacementState) . (app (lambda unrestricted lifetimeCount : Nat . (nat-eliminate (lambda unrestricted unique : Nat . (family MemoryPlanCompileResult)) (compileMemoryPlanFail lifetimeCount arenaBytes initial (constructor LivenessErrorCode LifetimeTensorDuplicate)) (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : (family MemoryPlanCompileResult) . (eliminate LivenessOptionalError (lambda unrestricted current : (family LivenessOptionalError) . (family MemoryPlanCompileResult)) (firstLifetimeError lifetimes) (branch LivenessNoError . (eliminate LivenessPlacementStep (lambda unrestricted current : (family LivenessPlacementStep) . (family MemoryPlanCompileResult)) (livenessPlaceAll (lifetimesSort lifetimes) (stdByteCountValue arenaBytes) initial) (branch LivenessPlacementAdvanced state . (eliminate LivenessPlacementState (lambda unrestricted current : (family LivenessPlacementState) . (family MemoryPlanCompileResult)) state (branch LivenessPlacementStateValue peak slots placements reused fresh . (app (lambda unrestricted plan : (family MemoryPlan) . (eliminate LivenessValidationResult (lambda unrestricted result : (family LivenessValidationResult) . (family MemoryPlanCompileResult)) (validateMemoryPlan plan) (branch LivenessValidationPassed checked telemetry . (constructor MemoryPlanCompileResult MemoryPlanCompiled checked (livenessCompileTelemetryFor lifetimeCount arenaBytes state (succ zero) (constructor LivenessOptionalError LivenessNoError)))) (branch LivenessValidationFailed code telemetry . (compileMemoryPlanFail lifetimeCount arenaBytes state (constructor LivenessErrorCode CompiledPlanRejected))))) (constructor MemoryPlan MemoryPlanValue arenaBytes peak (placementsReverse placements)))))) (branch LivenessPlacementStopped code stopped . (compileMemoryPlanFail lifetimeCount arenaBytes stopped code)))) (branch LivenessSomeError code . (compileMemoryPlanFail lifetimeCount arenaBytes initial code))))) (lifetimesUnique lifetimes))) (lifetimeCount lifetimes))) (constructor LivenessPlacementState LivenessPlacementStateValue (stdByteCount modelWord64Zero) (constructor LivenessSlots LivenessSlotsEnd) (constructor Placements PlacementsEnd) zero zero))))