One native host process reserving `budget` bytes for its interpreter
mapping: the context a single-participant host pairing admits against.
`kind` names the executor (for example b"x86-64-native" or
b"aarch64-native"); it is evidence naming the target, not a capability the
admission checks.
244def nativeSingleHostResources =
245 (lambda unrestricted name : Bytes .
246 (lambda unrestricted kind : Bytes .
247 (lambda unrestricted budget : Nat .
248 (constructor
249 NativeResourceContext
250 NativeResourceContextOf
251 (constructor
252 ResourceSchedule
253 ResourceScheduleOf
254 (constructor
255 ResourceGraph
256 ResourceGraphOf
257 (constructor
258 StdList
259 StdListCons
260 (family ResourceEndpoint)
261 (constructor
262 ResourceEndpoint
263 ResourceEndpointOf
264 0
265 name
266 kind
267 (constructor
268 StdList
269 StdListCons
270 Bytes
271 b"native-interpreter"
272 (constructor StdList StdListEmpty Bytes))
273 (constructor StdList StdListCons Nat 0 (constructor StdList StdListEmpty Nat)))
274 (constructor StdList StdListEmpty (family ResourceEndpoint)))
275 (constructor
276 StdList
277 StdListCons
278 (family ResourceDomain)
279 (constructor
280 ResourceDomain
281 ResourceCapacityDomain
282 0
283 (bytes-append name b"-interpreter-reservation")
284 (constructor ResourceUnit ResourceMemoryBytes)
285 (constructor
286 ResourceFact
287 ResourceEstablished
288 budget
289 b"qualification-process-reservation"))
290 (constructor StdList StdListEmpty (family ResourceDomain)))
291 (constructor StdList StdListEmpty (family ResourceLink)))
292 (constructor StdList StdListEmpty (family ResourcePlacement))
293 (constructor StdList StdListEmpty (family ResourceLease)))
294 (bytes-append name b"-interpreter")
295 0
296 0
297 4096
298 16
299 256))))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.