Hand-computed accounting fixtures. No capacity, page size or alias here
is a measured device fact. Two process contexts share one host domain;
their independent GPU domains cannot borrow each other's unused capacity.
25def rpGraph =
26 (lambda unrestricted host : Nat .
27 (lambda unrestricted left : Nat .
28 (lambda unrestricted right : Nat .
29 (constructor
30 ResourceGraph
31 ResourceGraphOf
32 (constructor
33 StdList
34 StdListCons
35 (family ResourceEndpoint)
36 (constructor
37 ResourceEndpoint
38 ResourceEndpointOf
39 0
40 b"fixture-engine-0"
41 b"fixture-native"
42 (constructor StdList StdListEmpty Bytes)
43 (constructor StdList StdListCons Nat 0 (constructor StdList StdListEmpty Nat)))
44 (constructor
45 StdList
46 StdListCons
47 (family ResourceEndpoint)
48 (constructor
49 ResourceEndpoint
50 ResourceEndpointOf
51 1
52 b"fixture-engine-1"
53 b"fixture-native"
54 (constructor StdList StdListEmpty Bytes)
55 (constructor
56 StdList
57 StdListCons
58 Nat
59 0
60 (constructor StdList StdListCons Nat 1 (constructor StdList StdListEmpty Nat))))
61 (constructor
62 StdList
63 StdListCons
64 (family ResourceEndpoint)
65 (constructor
66 ResourceEndpoint
67 ResourceEndpointOf
68 2
69 b"fixture-engine-2"
70 b"fixture-native"
71 (constructor StdList StdListEmpty Bytes)
72 (constructor
73 StdList
74 StdListCons
75 Nat
76 0
77 (constructor StdList StdListCons Nat 2 (constructor StdList StdListEmpty Nat))))
78 (constructor StdList StdListEmpty (family ResourceEndpoint)))))
79 (constructor
80 StdList
81 StdListCons
82 (family ResourceDomain)
83 (constructor
84 ResourceDomain
85 ResourceCapacityDomain
86 0
87 b"fixture-memory-0"
88 (constructor ResourceUnit ResourceMemoryBytes)
89 (constructor ResourceFact ResourceEstablished host b"hand-computed-reservation"))
90 (constructor
91 StdList
92 StdListCons
93 (family ResourceDomain)
94 (constructor
95 ResourceDomain
96 ResourceCapacityDomain
97 1
98 b"fixture-memory-1"
99 (constructor ResourceUnit ResourceMemoryBytes)
100 (constructor ResourceFact ResourceEstablished left b"hand-computed-reservation"))
101 (constructor
102 StdList
103 StdListCons
104 (family ResourceDomain)
105 (constructor
106 ResourceDomain
107 ResourceCapacityDomain
108 2
109 b"fixture-memory-2"
110 (constructor ResourceUnit ResourceMemoryBytes)
111 (constructor ResourceFact ResourceEstablished right b"hand-computed-reservation"))
112 (constructor StdList StdListEmpty (family ResourceDomain)))))
113 (constructor StdList StdListEmpty (family ResourceLink))))))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.