module Compiler.Planning.Resources import Execution.ResourceGraph import Compiler.Planning.Liveness import Model.Config import Model.Parameter import Model.Word32 import Model.Word64 import Std.Physical import Std.Foundation import Std.List import Std.Natural -- This explicit collection planner is for bounded deployment descriptions. -- It admits no transfer merely from vendor, host or failure-domain affinity. -- Its duplicate and interval checks are quadratic in description entries; -- callers bound entry count and its square (a work estimate, not CPU time). -- The square is checked by division without overflowing a runtime word. This is not -- the eventual sharded fleet search/index implementation. family ResourceUsage : Type 0 constructor ResourceUsageWithin field unrestricted resourceUsageAmount : Nat constructor ResourceUsageOverflow end-family def resourceWordLimit = 18446744073709551615 def resourceCount = (lambda erased element : Type 0 . (lambda unrestricted predicate : (pi unrestricted value : element . Nat) . (stdListFold element Nat (lambda unrestricted value : element . (lambda unrestricted total : Nat . (naturalAdd (naturalNonzero (predicate value)) total))) 0))) def resourceAll = (lambda erased element : Type 0 . (lambda unrestricted predicate : (pi unrestricted value : element . Nat) . (stdListFold element Nat (lambda unrestricted value : element . (lambda unrestricted valid : Nat . (naturalAnd (predicate value) valid))) 1))) def resourceDistinct = (lambda erased element : Type 0 . (lambda unrestricted same : (pi unrestricted left : element . (pi unrestricted right : element . Nat)) . (lambda unrestricted values : (family StdList element) . (eliminate StdList (lambda unrestricted current : (family StdList element) . Nat) values (branch StdListEmpty . 1) (branch StdListCons head tail induction . (naturalAnd (naturalIsZero (resourceCount element (same head) tail)) induction)))))) def resourceRequire = (lambda erased value : Type 0 . (lambda unrestricted condition : Nat . (lambda unrestricted reason : (family ResourceFailure) . (lambda unrestricted next : (family StdResult (family ResourceFailure) value) . (nat-eliminate (lambda unrestricted flag : Nat . (family StdResult (family ResourceFailure) value)) (constructor StdResult StdFailure (family ResourceFailure) value reason) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family StdResult (family ResourceFailure) value) . next)) condition))))) def resourceUnitCode = (lambda unrestricted unit : (family ResourceUnit) . (eliminate ResourceUnit (lambda unrestricted current : (family ResourceUnit) . Nat) unit (branch ResourceMemoryBytes . 0) (branch ResourceBandwidthBytesPerSecond . 1))) def resourceFactValid = (lambda unrestricted fact : (family ResourceFact) . (eliminate ResourceFact (lambda unrestricted current : (family ResourceFact) . Nat) fact (branch ResourceAbsent reason . (naturalNonzero (bytes-length reason))) (branch ResourceEstablished limit reference . (naturalAnd (naturalLessOrEqual limit resourceWordLimit) (naturalNonzero (bytes-length reference)))))) def resourceFactKnown = (lambda unrestricted fact : (family ResourceFact) . (eliminate ResourceFact (lambda unrestricted current : (family ResourceFact) . Nat) fact (branch ResourceAbsent reason . 0) (branch ResourceEstablished limit reference . 1))) def resourceFactAllows = (lambda unrestricted fact : (family ResourceFact) . (lambda unrestricted amount : Nat . (eliminate ResourceFact (lambda unrestricted current : (family ResourceFact) . Nat) fact (branch ResourceAbsent reason . 0) (branch ResourceEstablished limit reference . (naturalLessOrEqual amount limit))))) def resourceDomainValid = (lambda unrestricted domain : (family ResourceDomain) . (eliminate ResourceDomain (lambda unrestricted current : (family ResourceDomain) . Nat) domain (branch ResourceCapacityDomain id name unit fact . (naturalAnd (naturalLessOrEqual id resourceWordLimit) (naturalAnd (naturalNonzero (bytes-length name)) (resourceFactValid fact)))) (branch ResourceRelationDomain id name . (naturalAnd (naturalLessOrEqual id resourceWordLimit) (naturalNonzero (bytes-length name)))))) def resourceDomainUnitMatches = (lambda unrestricted domain : (family ResourceDomain) . (lambda unrestricted expected : (family ResourceUnit) . (eliminate ResourceDomain (lambda unrestricted current : (family ResourceDomain) . Nat) domain (branch ResourceCapacityDomain id name unit fact . (naturalEqual (resourceUnitCode unit) (resourceUnitCode expected))) (branch ResourceRelationDomain id name . 0)))) def resourceDomainKnown = (lambda unrestricted domain : (family ResourceDomain) . (eliminate ResourceDomain (lambda unrestricted current : (family ResourceDomain) . Nat) domain (branch ResourceCapacityDomain id name unit fact . (resourceFactKnown fact)) (branch ResourceRelationDomain id name . 0))) def resourceDomainAllows = (lambda unrestricted domain : (family ResourceDomain) . (lambda unrestricted amount : Nat . (eliminate ResourceDomain (lambda unrestricted current : (family ResourceDomain) . Nat) domain (branch ResourceCapacityDomain id name unit fact . (resourceFactAllows fact amount)) (branch ResourceRelationDomain id name . 0)))) def resourceHasEndpoint = (lambda unrestricted graph : (family ResourceGraph) . (lambda unrestricted id : Nat . (naturalNonzero (resourceCount (family ResourceEndpoint) (lambda unrestricted e : (family ResourceEndpoint) . (naturalEqual id (resourceEndpointId e))) (resourceGraphEndpoints graph))))) def resourceHasDomain = (lambda unrestricted graph : (family ResourceGraph) . (lambda unrestricted id : Nat . (naturalNonzero (resourceCount (family ResourceDomain) (lambda unrestricted d : (family ResourceDomain) . (naturalEqual id (resourceDomainId d))) (resourceGraphDomains graph))))) def resourceEndpointValid = (lambda unrestricted graph : (family ResourceGraph) . (lambda unrestricted endpoint : (family ResourceEndpoint) . (naturalAnd (naturalLessOrEqual (resourceEndpointId endpoint) resourceWordLimit) (naturalAnd (naturalNonzero (bytes-length (resourceEndpointIdentity endpoint))) (naturalAnd (naturalNonzero (bytes-length (resourceEndpointRealization endpoint))) (naturalAnd (resourceAll Bytes (lambda unrestricted cap : Bytes . (naturalNonzero (bytes-length cap))) (resourceEndpointCapabilities endpoint)) (naturalAnd (resourceDistinct Bytes (lambda unrestricted a : Bytes . (lambda unrestricted b : Bytes . (bytes-equal a b))) (resourceEndpointCapabilities endpoint)) (naturalAnd (resourceAll Nat (lambda unrestricted id : Nat . (resourceHasDomain graph id)) (resourceEndpointDomains endpoint)) (naturalAnd (resourceDistinct Nat (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (naturalEqual a b))) (resourceEndpointDomains endpoint)) 1))))))))) def resourceLinkValid = (lambda unrestricted graph : (family ResourceGraph) . (lambda unrestricted link : (family ResourceLink) . (naturalAnd (naturalLessOrEqual (resourceLinkId link) resourceWordLimit) (naturalAnd (naturalNonzero (bytes-length (resourceLinkRealization link))) (naturalAnd (resourceHasEndpoint graph (resourceLinkSource link)) (naturalAnd (resourceHasEndpoint graph (resourceLinkDestination link)) (naturalAnd (naturalIsZero (naturalEqual (resourceLinkSource link) (resourceLinkDestination link))) (naturalAnd (resourceFactValid (resourceLinkEnvelope link)) 1)))))))) def resourceGraphValid = (lambda unrestricted graph : (family ResourceGraph) . (naturalAnd (naturalNonzero (stdListLength (family ResourceEndpoint) (resourceGraphEndpoints graph))) (naturalAnd (resourceDistinct (family ResourceEndpoint) (lambda unrestricted a : (family ResourceEndpoint) . (lambda unrestricted b : (family ResourceEndpoint) . (naturalOr (naturalEqual (resourceEndpointId a) (resourceEndpointId b)) (bytes-equal (resourceEndpointIdentity a) (resourceEndpointIdentity b))))) (resourceGraphEndpoints graph)) (naturalAnd (resourceDistinct (family ResourceDomain) (lambda unrestricted a : (family ResourceDomain) . (lambda unrestricted b : (family ResourceDomain) . (naturalOr (naturalEqual (resourceDomainId a) (resourceDomainId b)) (bytes-equal (resourceDomainName a) (resourceDomainName b))))) (resourceGraphDomains graph)) (naturalAnd (resourceDistinct (family ResourceLink) (lambda unrestricted a : (family ResourceLink) . (lambda unrestricted b : (family ResourceLink) . (naturalEqual (resourceLinkId a) (resourceLinkId b)))) (resourceGraphLinks graph)) (naturalAnd (resourceAll (family ResourceDomain) resourceDomainValid (resourceGraphDomains graph)) (naturalAnd (resourceAll (family ResourceEndpoint) (resourceEndpointValid graph) (resourceGraphEndpoints graph)) (naturalAnd (resourceAll (family ResourceLink) (resourceLinkValid graph) (resourceGraphLinks graph)) 1)))))))) def resourcePlacementValid = (lambda unrestricted graph : (family ResourceGraph) . (lambda unrestricted placement : (family ResourcePlacement) . (naturalAnd (naturalLessOrEqual (resourcePlacementRole placement) resourceWordLimit) (naturalAnd (naturalNonzero (resourceCount (family ResourceEndpoint) (lambda unrestricted endpoint : (family ResourceEndpoint) . (naturalAnd (naturalEqual (resourceEndpointId endpoint) (resourcePlacementEndpoint placement)) (naturalAnd (naturalNonzero (resourceCount Bytes (lambda unrestricted cap : Bytes . (bytes-equal cap (resourcePlacementCapability placement))) (resourceEndpointCapabilities endpoint))) 1))) (resourceGraphEndpoints graph))) 1)))) def resourceLeaseValid = (lambda unrestricted graph : (family ResourceGraph) . (lambda unrestricted lease : (family ResourceLease) . (naturalAnd (naturalNonzero (bytes-length (resourceLeaseIdentity lease))) (naturalAnd (naturalNonzero (resourceLeaseAmount lease)) (naturalAnd (naturalLessOrEqual (resourceLeaseAmount lease) resourceWordLimit) (naturalAnd (naturalLess (resourceLeaseBegin lease) (resourceLeaseUntil lease)) (naturalAnd (naturalLessOrEqual (resourceLeaseUntil lease) resourceWordLimit) (naturalAnd (naturalNonzero (resourceCount (family ResourceEndpoint) (lambda unrestricted endpoint : (family ResourceEndpoint) . (naturalAnd (naturalEqual (resourceEndpointId endpoint) (resourceLeaseEndpoint lease)) (naturalAnd (naturalNonzero (resourceCount Nat (lambda unrestricted id : Nat . (naturalEqual id (resourceLeaseDomain lease))) (resourceEndpointDomains endpoint))) 1))) (resourceGraphEndpoints graph))) (naturalAnd (naturalNonzero (resourceCount (family ResourceDomain) (lambda unrestricted domain : (family ResourceDomain) . (naturalAnd (naturalEqual (resourceDomainId domain) (resourceLeaseDomain lease)) (naturalAnd (resourceDomainUnitMatches domain (resourceLeaseUnit lease)) 1))) (resourceGraphDomains graph))) 1))))))))) def resourceUsageAdd = (lambda unrestricted total : (family ResourceUsage) . (lambda unrestricted amount : Nat . (eliminate ResourceUsage (lambda unrestricted current : (family ResourceUsage) . (family ResourceUsage)) total (branch ResourceUsageWithin value . (eliminate StdBool (lambda unrestricted flag : (family StdBool) . (family ResourceUsage)) (stdBoolFromNatural (naturalLessOrEqual amount (naturalSaturatingSubtract resourceWordLimit value))) (branch StdTrue . (constructor ResourceUsage ResourceUsageWithin (naturalAdd value amount))) (branch StdFalse . (constructor ResourceUsage ResourceUsageOverflow)))) (branch ResourceUsageOverflow . (constructor ResourceUsage ResourceUsageOverflow))))) -- A peak occurs at a lease start: amounts are nonnegative and only those -- events add reservations. Ends are exclusive; device completion alone cannot -- end a lease still extended by a transport read. def resourceUsageAt = (lambda unrestricted leases : (family StdList (family ResourceLease)) . (lambda unrestricted domain : Nat . (lambda unrestricted event : Nat . (stdListFold (family ResourceLease) (family ResourceUsage) (lambda unrestricted lease : (family ResourceLease) . (lambda unrestricted total : (family ResourceUsage) . (resourceUsageAdd total (naturalSelect (naturalAnd (naturalEqual domain (resourceLeaseDomain lease)) (naturalAnd (naturalLessOrEqual (resourceLeaseBegin lease) event) (naturalLess event (resourceLeaseUntil lease)))) (resourceLeaseAmount lease) 0)))) (constructor ResourceUsage ResourceUsageWithin 0) leases)))) def resourceLeaseKnown = (lambda unrestricted graph : (family ResourceGraph) . (lambda unrestricted lease : (family ResourceLease) . (naturalNonzero (resourceCount (family ResourceDomain) (lambda unrestricted domain : (family ResourceDomain) . (naturalAnd (naturalEqual (resourceDomainId domain) (resourceLeaseDomain lease)) (naturalAnd (resourceDomainKnown domain) 1))) (resourceGraphDomains graph))))) def resourceLeaseFits = (lambda unrestricted graph : (family ResourceGraph) . (lambda unrestricted leases : (family StdList (family ResourceLease)) . (lambda unrestricted lease : (family ResourceLease) . (eliminate ResourceUsage (lambda unrestricted current : (family ResourceUsage) . Nat) (resourceUsageAt leases (resourceLeaseDomain lease) (resourceLeaseBegin lease)) (branch ResourceUsageWithin total . (naturalNonzero (resourceCount (family ResourceDomain) (lambda unrestricted domain : (family ResourceDomain) . (naturalAnd (naturalEqual (resourceDomainId domain) (resourceLeaseDomain lease)) (resourceDomainAllows domain total))) (resourceGraphDomains graph)))) (branch ResourceUsageOverflow . 0))))) def resourceGraphEntries = (lambda unrestricted graph : (family ResourceGraph) . (naturalAdd (stdListLength (family ResourceDomain) (resourceGraphDomains graph)) (naturalAdd (stdListLength (family ResourceLink) (resourceGraphLinks graph)) (stdListFold (family ResourceEndpoint) Nat (lambda unrestricted endpoint : (family ResourceEndpoint) . (lambda unrestricted total : Nat . (naturalAdd total (naturalAdd 1 (naturalAdd (stdListLength Bytes (resourceEndpointCapabilities endpoint)) (stdListLength Nat (resourceEndpointDomains endpoint))))))) 0 (resourceGraphEndpoints graph))))) def resourceScheduleEntries = (lambda unrestricted schedule : (family ResourceSchedule) . (naturalAdd (resourceGraphEntries (resourceScheduleGraph schedule)) (naturalAdd (stdListLength (family ResourcePlacement) (resourceSchedulePlacements schedule)) (stdListLength (family ResourceLease) (resourceScheduleLeases schedule))))) def admitResourceSchedule = (lambda unrestricted entryBudget : Nat . (lambda unrestricted pairBudget : Nat . (lambda unrestricted schedule : (family ResourceSchedule) . (let unrestricted graph = (resourceScheduleGraph schedule) in (let unrestricted placements = (resourceSchedulePlacements schedule) in (let unrestricted leases = (resourceScheduleLeases schedule) in (let unrestricted entries = (resourceScheduleEntries schedule) in (resourceRequire (family ResourceSchedule) (naturalAnd (naturalLessOrEqual entries entryBudget) (naturalLessOrEqual entries (naturalDivideUnchecked pairBudget (naturalSelect (naturalNonzero entries) entries 1)))) (constructor ResourceFailure ResourceBudgetExceeded) (resourceRequire (family ResourceSchedule) (resourceGraphValid graph) (constructor ResourceFailure ResourceMalformedGraph) (resourceRequire (family ResourceSchedule) (naturalAnd (resourceDistinct (family ResourcePlacement) (lambda unrestricted a : (family ResourcePlacement) . (lambda unrestricted b : (family ResourcePlacement) . (naturalEqual (resourcePlacementRole a) (resourcePlacementRole b)))) placements) (naturalAnd (resourceAll (family ResourcePlacement) (resourcePlacementValid graph) placements) 1)) (constructor ResourceFailure ResourceInvalidPlacement) (resourceRequire (family ResourceSchedule) (naturalAnd (resourceDistinct (family ResourceLease) (lambda unrestricted a : (family ResourceLease) . (lambda unrestricted b : (family ResourceLease) . (bytes-equal (resourceLeaseIdentity a) (resourceLeaseIdentity b)))) leases) (naturalAnd (resourceAll (family ResourceLease) (resourceLeaseValid graph) leases) 1)) (constructor ResourceFailure ResourceInvalidLease) (resourceRequire (family ResourceSchedule) (resourceAll (family ResourceLease) (resourceLeaseKnown graph) leases) (constructor ResourceFailure ResourceCapacityUnavailable) (resourceRequire (family ResourceSchedule) (resourceAll (family ResourceLease) (resourceLeaseFits graph leases) leases) (constructor ResourceFailure ResourceCapacityExceeded) (constructor StdResult StdSuccess (family ResourceFailure) (family ResourceSchedule) schedule)))))))))))))) -- These lookups consume an admitted schedule. Resolve each logical role once; -- nesting full collection scans for every candidate would make routing cubic. def resourcePlacementForRole = (lambda unrestricted role : Nat . (stdListFold (family ResourcePlacement) (family StdOption Nat) (lambda unrestricted placement : (family ResourcePlacement) . (lambda unrestricted next : (family StdOption Nat) . (eliminate StdBool (lambda unrestricted flag : (family StdBool) . (family StdOption Nat)) (stdBoolFromNatural (naturalEqual (resourcePlacementRole placement) role)) (branch StdTrue . (constructor StdOption StdSome Nat (resourcePlacementEndpoint placement))) (branch StdFalse . next)))) (constructor StdOption StdNone Nat))) def resourceRouteAllowed = (lambda unrestricted schedule : (family ResourceSchedule) . (lambda unrestricted sourceRole : Nat . (lambda unrestricted destinationRole : Nat . (lambda unrestricted linkId : Nat . (lambda unrestricted realization : Bytes . (lambda unrestricted bytes : Nat . (eliminate StdOption (lambda unrestricted current : (family StdOption Nat) . Nat) (resourcePlacementForRole sourceRole (resourceSchedulePlacements schedule)) (branch StdNone . 0) (branch StdSome source . (eliminate StdOption (lambda unrestricted current : (family StdOption Nat) . Nat) (resourcePlacementForRole destinationRole (resourceSchedulePlacements schedule)) (branch StdNone . 0) (branch StdSome destination . (naturalNonzero (resourceCount (family ResourceLink) (lambda unrestricted link : (family ResourceLink) . (naturalAnd (naturalEqual (resourceLinkId link) linkId) (naturalAnd (naturalEqual (resourceLinkSource link) source) (naturalAnd (naturalEqual (resourceLinkDestination link) destination) (naturalAnd (bytes-equal (resourceLinkRealization link) realization) (resourceFactAllows (resourceLinkEnvelope link) bytes)))))) (resourceGraphLinks (resourceScheduleGraph schedule)))))))))))))) -- Lifetimes use inclusive last-use events. Leases are half-open: retain bytes -- through lastUse, including any extension made by the transfer planner. The -- lifetime owner is U32, so adding one here fits the resource event word. def resourceLeaseFromLifetime = (lambda unrestricted identity : Bytes . (lambda unrestricted endpoint : Nat . (lambda unrestricted domain : Nat . (lambda unrestricted lifetime : (family Lifetime) . (eliminate Lifetime (lambda unrestricted current : (family Lifetime) . (family ResourceLease)) lifetime (branch LifetimeValue tensor first last bytes alignment . (constructor ResourceLease ResourceLeaseOf identity endpoint domain (constructor ResourceUnit ResourceMemoryBytes) (modelWord64Natural (stdByteCountValue bytes)) (modelWord32ToNatural first) (naturalAdd (modelWord32ToNatural last) 1))))))))