Execution.ResourceGraph

1module Execution.ResourceGraph
2
3import Std.List
4
5-- Graph IDs name execution resources, independently of logical learning roles.
6-- A relation domain can describe a host, fast-link set, power/fault group, rack
7-- or storage scope; sharing that domain never grants a transfer realization.
8-- Capacity domains have explicit units. Limits are admitted facts/reservations,
9-- never performance estimates; a missing limit retains its reason.
10--
11-- Fact references identify external architectural evidence, run receipts or
12-- operator reservations. These values do not authenticate evidence or establish
13-- physical identity. Target owners and deployment admission remain responsible
14-- for their provenance and runtime guards.
15family ResourceUnit : Type 0
16constructor ResourceMemoryBytes
17constructor ResourceBandwidthBytesPerSecond
18
19end-family
20
21family ResourceFact : Type 0
22constructor ResourceAbsent
23field unrestricted resourceAbsentReason : Bytes
24constructor ResourceEstablished
25field unrestricted resourceEstablishedLimit : Nat
26field unrestricted resourceEstablishedReference : Bytes
27
28end-family
29
30family ResourceDomain : Type 0
31constructor ResourceCapacityDomain
32field unrestricted resourceCapacityDomainId : Nat
33field unrestricted resourceCapacityDomainName : Bytes
34field unrestricted resourceCapacityDomainUnit : (family ResourceUnit)
35field unrestricted resourceCapacityDomainFact : (family ResourceFact)
36constructor ResourceRelationDomain
37field unrestricted resourceRelationDomainId : Nat
38field unrestricted resourceRelationDomainName : Bytes
39
40end-family
41
42family ResourceEndpoint : Type 0
43constructor ResourceEndpointOf
44field unrestricted resourceEndpointOfId : Nat
45field unrestricted resourceEndpointOfIdentity : Bytes
46field unrestricted resourceEndpointOfRealization : Bytes
47field unrestricted resourceEndpointOfCapabilities : (family StdList Bytes)
48field unrestricted resourceEndpointOfDomains : (family StdList Nat)
49
50end-family
51
52family ResourceLink : Type 0
53constructor ResourceLinkOf
54field unrestricted resourceLinkOfId : Nat
55field unrestricted resourceLinkOfSource : Nat
56field unrestricted resourceLinkOfDestination : Nat
57field unrestricted resourceLinkOfRealization : Bytes
58field unrestricted resourceLinkOfEnvelope : (family ResourceFact)
59
60end-family
61
62family ResourceGraph : Type 0
63constructor ResourceGraphOf
64field unrestricted resourceGraphOfEndpoints : (family StdList (family ResourceEndpoint))
65field unrestricted resourceGraphOfDomains : (family StdList (family ResourceDomain))
66field unrestricted resourceGraphOfLinks : (family StdList (family ResourceLink))
67
68end-family
69
70family ResourcePlacement : Type 0
71constructor ResourcePlacementOf
72field unrestricted resourcePlacementOfRole : Nat
73field unrestricted resourcePlacementOfEndpoint : Nat
74field unrestricted resourcePlacementOfCapability : Bytes
75
76end-family
77
78family ResourceLease : Type 0
79constructor ResourceLeaseOf
80field unrestricted resourceLeaseOfIdentity : Bytes
81field unrestricted resourceLeaseOfEndpoint : Nat
82field unrestricted resourceLeaseOfDomain : Nat
83field unrestricted resourceLeaseOfUnit : (family ResourceUnit)
84field unrestricted resourceLeaseOfAmount : Nat
85field unrestricted resourceLeaseOfBegin : Nat
86field unrestricted resourceLeaseOfUntil : Nat
87
88end-family
89
90family ResourceSchedule : Type 0
91constructor ResourceScheduleOf
92field unrestricted resourceScheduleOfGraph : (family ResourceGraph)
93field unrestricted resourceScheduleOfPlacements : (family StdList (family ResourcePlacement))
94field unrestricted resourceScheduleOfLeases : (family StdList (family ResourceLease))
95
96end-family
97
98family ResourceFailure : Type 0
99constructor ResourceBudgetExceeded
100constructor ResourceMalformedGraph
101constructor ResourceInvalidPlacement
102constructor ResourceInvalidLease
103constructor ResourceCapacityUnavailable
104constructor ResourceCapacityExceeded
105constructor ResourceRouteUnavailable
106
107end-family
108
109def resourceEndpointId =
110  (lambda unrestricted value : (family ResourceEndpoint) .
111    (eliminate
112      ResourceEndpoint
113      (lambda unrestricted current : (family ResourceEndpoint) . Nat)
114      value
115      (branch ResourceEndpointOf id identity realization capabilities domains . id)))
116
117def resourceEndpointIdentity =
118  (lambda unrestricted value : (family ResourceEndpoint) .
119    (eliminate
120      ResourceEndpoint
121      (lambda unrestricted current : (family ResourceEndpoint) . Bytes)
122      value
123      (branch ResourceEndpointOf id identity realization capabilities domains . identity)))
124
125def resourceEndpointRealization =
126  (lambda unrestricted value : (family ResourceEndpoint) .
127    (eliminate
128      ResourceEndpoint
129      (lambda unrestricted current : (family ResourceEndpoint) . Bytes)
130      value
131      (branch ResourceEndpointOf id identity realization capabilities domains . realization)))
132
133def resourceEndpointCapabilities =
134  (lambda unrestricted value : (family ResourceEndpoint) .
135    (eliminate
136      ResourceEndpoint
137      (lambda unrestricted current : (family ResourceEndpoint) . (family StdList Bytes))
138      value
139      (branch ResourceEndpointOf id identity realization capabilities domains . capabilities)))
140
141def resourceEndpointDomains =
142  (lambda unrestricted value : (family ResourceEndpoint) .
143    (eliminate
144      ResourceEndpoint
145      (lambda unrestricted current : (family ResourceEndpoint) . (family StdList Nat))
146      value
147      (branch ResourceEndpointOf id identity realization capabilities domains . domains)))
148
149def resourceLinkId =
150  (lambda unrestricted value : (family ResourceLink) .
151    (eliminate
152      ResourceLink
153      (lambda unrestricted current : (family ResourceLink) . Nat)
154      value
155      (branch ResourceLinkOf id source destination realization envelope . id)))
156
157def resourceLinkSource =
158  (lambda unrestricted value : (family ResourceLink) .
159    (eliminate
160      ResourceLink
161      (lambda unrestricted current : (family ResourceLink) . Nat)
162      value
163      (branch ResourceLinkOf id source destination realization envelope . source)))
164
165def resourceLinkDestination =
166  (lambda unrestricted value : (family ResourceLink) .
167    (eliminate
168      ResourceLink
169      (lambda unrestricted current : (family ResourceLink) . Nat)
170      value
171      (branch ResourceLinkOf id source destination realization envelope . destination)))
172
173def resourceLinkRealization =
174  (lambda unrestricted value : (family ResourceLink) .
175    (eliminate
176      ResourceLink
177      (lambda unrestricted current : (family ResourceLink) . Bytes)
178      value
179      (branch ResourceLinkOf id source destination realization envelope . realization)))
180
181def resourceLinkEnvelope =
182  (lambda unrestricted value : (family ResourceLink) .
183    (eliminate
184      ResourceLink
185      (lambda unrestricted current : (family ResourceLink) . (family ResourceFact))
186      value
187      (branch ResourceLinkOf id source destination realization envelope . envelope)))
188
189def resourceGraphEndpoints =
190  (lambda unrestricted value : (family ResourceGraph) .
191    (eliminate
192      ResourceGraph
193      (lambda unrestricted current : (family ResourceGraph) .
194        (family StdList (family ResourceEndpoint)))
195      value
196      (branch ResourceGraphOf endpoints domains links . endpoints)))
197
198def resourceGraphDomains =
199  (lambda unrestricted value : (family ResourceGraph) .
200    (eliminate
201      ResourceGraph
202      (lambda unrestricted current : (family ResourceGraph) .
203        (family StdList (family ResourceDomain)))
204      value
205      (branch ResourceGraphOf endpoints domains links . domains)))
206
207def resourceGraphLinks =
208  (lambda unrestricted value : (family ResourceGraph) .
209    (eliminate
210      ResourceGraph
211      (lambda unrestricted current : (family ResourceGraph) .
212        (family StdList (family ResourceLink)))
213      value
214      (branch ResourceGraphOf endpoints domains links . links)))
215
216def resourcePlacementRole =
217  (lambda unrestricted value : (family ResourcePlacement) .
218    (eliminate
219      ResourcePlacement
220      (lambda unrestricted current : (family ResourcePlacement) . Nat)
221      value
222      (branch ResourcePlacementOf role endpoint capability . role)))
223
224def resourcePlacementEndpoint =
225  (lambda unrestricted value : (family ResourcePlacement) .
226    (eliminate
227      ResourcePlacement
228      (lambda unrestricted current : (family ResourcePlacement) . Nat)
229      value
230      (branch ResourcePlacementOf role endpoint capability . endpoint)))
231
232def resourcePlacementCapability =
233  (lambda unrestricted value : (family ResourcePlacement) .
234    (eliminate
235      ResourcePlacement
236      (lambda unrestricted current : (family ResourcePlacement) . Bytes)
237      value
238      (branch ResourcePlacementOf role endpoint capability . capability)))
239
240def resourceLeaseIdentity =
241  (lambda unrestricted value : (family ResourceLease) .
242    (eliminate
243      ResourceLease
244      (lambda unrestricted current : (family ResourceLease) . Bytes)
245      value
246      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . identity)))
247
248def resourceLeaseEndpoint =
249  (lambda unrestricted value : (family ResourceLease) .
250    (eliminate
251      ResourceLease
252      (lambda unrestricted current : (family ResourceLease) . Nat)
253      value
254      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . endpoint)))
255
256def resourceLeaseDomain =
257  (lambda unrestricted value : (family ResourceLease) .
258    (eliminate
259      ResourceLease
260      (lambda unrestricted current : (family ResourceLease) . Nat)
261      value
262      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . domain)))
263
264def resourceLeaseUnit =
265  (lambda unrestricted value : (family ResourceLease) .
266    (eliminate
267      ResourceLease
268      (lambda unrestricted current : (family ResourceLease) . (family ResourceUnit))
269      value
270      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . unit)))
271
272def resourceLeaseAmount =
273  (lambda unrestricted value : (family ResourceLease) .
274    (eliminate
275      ResourceLease
276      (lambda unrestricted current : (family ResourceLease) . Nat)
277      value
278      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . amount)))
279
280def resourceLeaseBegin =
281  (lambda unrestricted value : (family ResourceLease) .
282    (eliminate
283      ResourceLease
284      (lambda unrestricted current : (family ResourceLease) . Nat)
285      value
286      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . begin)))
287
288def resourceLeaseUntil =
289  (lambda unrestricted value : (family ResourceLease) .
290    (eliminate
291      ResourceLease
292      (lambda unrestricted current : (family ResourceLease) . Nat)
293      value
294      (branch ResourceLeaseOf identity endpoint domain unit amount begin until . until)))
295
296def resourceScheduleGraph =
297  (lambda unrestricted value : (family ResourceSchedule) .
298    (eliminate
299      ResourceSchedule
300      (lambda unrestricted current : (family ResourceSchedule) . (family ResourceGraph))
301      value
302      (branch ResourceScheduleOf graph placements leases . graph)))
303
304def resourceSchedulePlacements =
305  (lambda unrestricted value : (family ResourceSchedule) .
306    (eliminate
307      ResourceSchedule
308      (lambda unrestricted current : (family ResourceSchedule) .
309        (family StdList (family ResourcePlacement)))
310      value
311      (branch ResourceScheduleOf graph placements leases . placements)))
312
313def resourceScheduleLeases =
314  (lambda unrestricted value : (family ResourceSchedule) .
315    (eliminate
316      ResourceSchedule
317      (lambda unrestricted current : (family ResourceSchedule) .
318        (family StdList (family ResourceLease)))
319      value
320      (branch ResourceScheduleOf graph placements leases . leases)))
321
322def resourceDomainId =
323  (lambda unrestricted value : (family ResourceDomain) .
324    (eliminate
325      ResourceDomain
326      (lambda unrestricted current : (family ResourceDomain) . Nat)
327      value
328      (branch ResourceCapacityDomain id name unit fact . id)
329      (branch ResourceRelationDomain id name . id)))
330
331def resourceDomainName =
332  (lambda unrestricted value : (family ResourceDomain) .
333    (eliminate
334      ResourceDomain
335      (lambda unrestricted current : (family ResourceDomain) . Bytes)
336      value
337      (branch ResourceCapacityDomain id name unit fact . name)
338      (branch ResourceRelationDomain id name . name)))