module Execution.ResourceGraph

import Std.List

-- Graph IDs name execution resources, independently of logical learning roles.
-- A relation domain can describe a host, fast-link set, power/fault group, rack
-- or storage scope; sharing that domain never grants a transfer realization.
-- Capacity domains have explicit units. Limits are admitted facts/reservations,
-- never performance estimates; a missing limit retains its reason.
--
-- Fact references identify external architectural evidence, run receipts or
-- operator reservations. These values do not authenticate evidence or establish
-- physical identity. Target owners and deployment admission remain responsible
-- for their provenance and runtime guards.
family ResourceUnit : Type 0
constructor ResourceMemoryBytes
constructor ResourceBandwidthBytesPerSecond

end-family

family ResourceFact : Type 0
constructor ResourceAbsent
field unrestricted resourceAbsentReason : Bytes
constructor ResourceEstablished
field unrestricted resourceEstablishedLimit : Nat
field unrestricted resourceEstablishedReference : Bytes

end-family

family ResourceDomain : Type 0
constructor ResourceCapacityDomain
field unrestricted resourceCapacityDomainId : Nat
field unrestricted resourceCapacityDomainName : Bytes
field unrestricted resourceCapacityDomainUnit : (family ResourceUnit)
field unrestricted resourceCapacityDomainFact : (family ResourceFact)
constructor ResourceRelationDomain
field unrestricted resourceRelationDomainId : Nat
field unrestricted resourceRelationDomainName : Bytes

end-family

family ResourceEndpoint : Type 0
constructor ResourceEndpointOf
field unrestricted resourceEndpointOfId : Nat
field unrestricted resourceEndpointOfIdentity : Bytes
field unrestricted resourceEndpointOfRealization : Bytes
field unrestricted resourceEndpointOfCapabilities : (family StdList Bytes)
field unrestricted resourceEndpointOfDomains : (family StdList Nat)

end-family

family ResourceLink : Type 0
constructor ResourceLinkOf
field unrestricted resourceLinkOfId : Nat
field unrestricted resourceLinkOfSource : Nat
field unrestricted resourceLinkOfDestination : Nat
field unrestricted resourceLinkOfRealization : Bytes
field unrestricted resourceLinkOfEnvelope : (family ResourceFact)

end-family

family ResourceGraph : Type 0
constructor ResourceGraphOf
field unrestricted resourceGraphOfEndpoints : (family StdList (family ResourceEndpoint))
field unrestricted resourceGraphOfDomains : (family StdList (family ResourceDomain))
field unrestricted resourceGraphOfLinks : (family StdList (family ResourceLink))

end-family

family ResourcePlacement : Type 0
constructor ResourcePlacementOf
field unrestricted resourcePlacementOfRole : Nat
field unrestricted resourcePlacementOfEndpoint : Nat
field unrestricted resourcePlacementOfCapability : Bytes

end-family

family ResourceLease : Type 0
constructor ResourceLeaseOf
field unrestricted resourceLeaseOfIdentity : Bytes
field unrestricted resourceLeaseOfEndpoint : Nat
field unrestricted resourceLeaseOfDomain : Nat
field unrestricted resourceLeaseOfUnit : (family ResourceUnit)
field unrestricted resourceLeaseOfAmount : Nat
field unrestricted resourceLeaseOfBegin : Nat
field unrestricted resourceLeaseOfUntil : Nat

end-family

family ResourceSchedule : Type 0
constructor ResourceScheduleOf
field unrestricted resourceScheduleOfGraph : (family ResourceGraph)
field unrestricted resourceScheduleOfPlacements : (family StdList (family ResourcePlacement))
field unrestricted resourceScheduleOfLeases : (family StdList (family ResourceLease))

end-family

family ResourceFailure : Type 0
constructor ResourceBudgetExceeded
constructor ResourceMalformedGraph
constructor ResourceInvalidPlacement
constructor ResourceInvalidLease
constructor ResourceCapacityUnavailable
constructor ResourceCapacityExceeded
constructor ResourceRouteUnavailable

end-family

def resourceEndpointId =
  (lambda unrestricted value : (family ResourceEndpoint) .
    (eliminate
      ResourceEndpoint
      (lambda unrestricted current : (family ResourceEndpoint) . Nat)
      value
      (branch ResourceEndpointOf id identity realization capabilities domains . id)))

def resourceEndpointIdentity =
  (lambda unrestricted value : (family ResourceEndpoint) .
    (eliminate
      ResourceEndpoint
      (lambda unrestricted current : (family ResourceEndpoint) . Bytes)
      value
      (branch ResourceEndpointOf id identity realization capabilities domains . identity)))

def resourceEndpointRealization =
  (lambda unrestricted value : (family ResourceEndpoint) .
    (eliminate
      ResourceEndpoint
      (lambda unrestricted current : (family ResourceEndpoint) . Bytes)
      value
      (branch ResourceEndpointOf id identity realization capabilities domains . realization)))

def resourceEndpointCapabilities =
  (lambda unrestricted value : (family ResourceEndpoint) .
    (eliminate
      ResourceEndpoint
      (lambda unrestricted current : (family ResourceEndpoint) . (family StdList Bytes))
      value
      (branch ResourceEndpointOf id identity realization capabilities domains . capabilities)))

def resourceEndpointDomains =
  (lambda unrestricted value : (family ResourceEndpoint) .
    (eliminate
      ResourceEndpoint
      (lambda unrestricted current : (family ResourceEndpoint) . (family StdList Nat))
      value
      (branch ResourceEndpointOf id identity realization capabilities domains . domains)))

def resourceLinkId =
  (lambda unrestricted value : (family ResourceLink) .
    (eliminate
      ResourceLink
      (lambda unrestricted current : (family ResourceLink) . Nat)
      value
      (branch ResourceLinkOf id source destination realization envelope . id)))

def resourceLinkSource =
  (lambda unrestricted value : (family ResourceLink) .
    (eliminate
      ResourceLink
      (lambda unrestricted current : (family ResourceLink) . Nat)
      value
      (branch ResourceLinkOf id source destination realization envelope . source)))

def resourceLinkDestination =
  (lambda unrestricted value : (family ResourceLink) .
    (eliminate
      ResourceLink
      (lambda unrestricted current : (family ResourceLink) . Nat)
      value
      (branch ResourceLinkOf id source destination realization envelope . destination)))

def resourceLinkRealization =
  (lambda unrestricted value : (family ResourceLink) .
    (eliminate
      ResourceLink
      (lambda unrestricted current : (family ResourceLink) . Bytes)
      value
      (branch ResourceLinkOf id source destination realization envelope . realization)))

def resourceLinkEnvelope =
  (lambda unrestricted value : (family ResourceLink) .
    (eliminate
      ResourceLink
      (lambda unrestricted current : (family ResourceLink) . (family ResourceFact))
      value
      (branch ResourceLinkOf id source destination realization envelope . envelope)))

def resourceGraphEndpoints =
  (lambda unrestricted value : (family ResourceGraph) .
    (eliminate
      ResourceGraph
      (lambda unrestricted current : (family ResourceGraph) .
        (family StdList (family ResourceEndpoint)))
      value
      (branch ResourceGraphOf endpoints domains links . endpoints)))

def resourceGraphDomains =
  (lambda unrestricted value : (family ResourceGraph) .
    (eliminate
      ResourceGraph
      (lambda unrestricted current : (family ResourceGraph) .
        (family StdList (family ResourceDomain)))
      value
      (branch ResourceGraphOf endpoints domains links . domains)))

def resourceGraphLinks =
  (lambda unrestricted value : (family ResourceGraph) .
    (eliminate
      ResourceGraph
      (lambda unrestricted current : (family ResourceGraph) .
        (family StdList (family ResourceLink)))
      value
      (branch ResourceGraphOf endpoints domains links . links)))

def resourcePlacementRole =
  (lambda unrestricted value : (family ResourcePlacement) .
    (eliminate
      ResourcePlacement
      (lambda unrestricted current : (family ResourcePlacement) . Nat)
      value
      (branch ResourcePlacementOf role endpoint capability . role)))

def resourcePlacementEndpoint =
  (lambda unrestricted value : (family ResourcePlacement) .
    (eliminate
      ResourcePlacement
      (lambda unrestricted current : (family ResourcePlacement) . Nat)
      value
      (branch ResourcePlacementOf role endpoint capability . endpoint)))

def resourcePlacementCapability =
  (lambda unrestricted value : (family ResourcePlacement) .
    (eliminate
      ResourcePlacement
      (lambda unrestricted current : (family ResourcePlacement) . Bytes)
      value
      (branch ResourcePlacementOf role endpoint capability . capability)))

def resourceLeaseIdentity =
  (lambda unrestricted value : (family ResourceLease) .
    (eliminate
      ResourceLease
      (lambda unrestricted current : (family ResourceLease) . Bytes)
      value
      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . identity)))

def resourceLeaseEndpoint =
  (lambda unrestricted value : (family ResourceLease) .
    (eliminate
      ResourceLease
      (lambda unrestricted current : (family ResourceLease) . Nat)
      value
      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . endpoint)))

def resourceLeaseDomain =
  (lambda unrestricted value : (family ResourceLease) .
    (eliminate
      ResourceLease
      (lambda unrestricted current : (family ResourceLease) . Nat)
      value
      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . domain)))

def resourceLeaseUnit =
  (lambda unrestricted value : (family ResourceLease) .
    (eliminate
      ResourceLease
      (lambda unrestricted current : (family ResourceLease) . (family ResourceUnit))
      value
      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . unit)))

def resourceLeaseAmount =
  (lambda unrestricted value : (family ResourceLease) .
    (eliminate
      ResourceLease
      (lambda unrestricted current : (family ResourceLease) . Nat)
      value
      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . amount)))

def resourceLeaseBegin =
  (lambda unrestricted value : (family ResourceLease) .
    (eliminate
      ResourceLease
      (lambda unrestricted current : (family ResourceLease) . Nat)
      value
      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . begin)))

def resourceLeaseUntil =
  (lambda unrestricted value : (family ResourceLease) .
    (eliminate
      ResourceLease
      (lambda unrestricted current : (family ResourceLease) . Nat)
      value
      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . until)))

def resourceScheduleGraph =
  (lambda unrestricted value : (family ResourceSchedule) .
    (eliminate
      ResourceSchedule
      (lambda unrestricted current : (family ResourceSchedule) . (family ResourceGraph))
      value
      (branch ResourceScheduleOf graph placements leases . graph)))

def resourceSchedulePlacements =
  (lambda unrestricted value : (family ResourceSchedule) .
    (eliminate
      ResourceSchedule
      (lambda unrestricted current : (family ResourceSchedule) .
        (family StdList (family ResourcePlacement)))
      value
      (branch ResourceScheduleOf graph placements leases . placements)))

def resourceScheduleLeases =
  (lambda unrestricted value : (family ResourceSchedule) .
    (eliminate
      ResourceSchedule
      (lambda unrestricted current : (family ResourceSchedule) .
        (family StdList (family ResourceLease)))
      value
      (branch ResourceScheduleOf graph placements leases . leases)))

def resourceDomainId =
  (lambda unrestricted value : (family ResourceDomain) .
    (eliminate
      ResourceDomain
      (lambda unrestricted current : (family ResourceDomain) . Nat)
      value
      (branch ResourceCapacityDomain id name unit fact . id)
      (branch ResourceRelationDomain id name . id)))

def resourceDomainName =
  (lambda unrestricted value : (family ResourceDomain) .
    (eliminate
      ResourceDomain
      (lambda unrestricted current : (family ResourceDomain) . Bytes)
      value
      (branch ResourceCapacityDomain id name unit fact . name)
      (branch ResourceRelationDomain id name . name)))