1module Platform.AArch64.HostCapability
2
3import Model.Parameter
4import Model.Word64
5import Std.Natural
6import Std.Word
7
8-- Host-CPU capability admission for an AArch64 build or execution host. It
9-- mirrors Accelerator.SM86.Capability: a caller supplies measured facts, a
10-- system supplies exact minimums, and marketing names, hostnames, kernel and
11-- driver strings stay in the physical receipt, never in admission. Core
12-- identity is carried as the raw MIDR_EL1 implementer and part fields so that
13-- a heterogeneous (performance + efficiency) cluster is described without a
14-- product-name field.
15family AArch64HostCapabilities : Type 0
16constructor AArch64HostCapabilitiesValue
17field unrestricted aarch64HostImplementer : Nat
18field unrestricted aarch64HostPerformanceCorePart : Nat
19field unrestricted aarch64HostPerformanceCoreCount : Nat
20field unrestricted aarch64HostEfficiencyCorePart : Nat
21field unrestricted aarch64HostEfficiencyCoreCount : Nat
22field unrestricted aarch64HostTotalMemoryBytes : (family ModelWord64)
23field unrestricted aarch64HostPageSizeBytes : Nat
24field unrestricted aarch64HostLevel2CacheBytes : (family ModelWord64)
25field unrestricted aarch64HostLevel3CacheBytes : (family ModelWord64)
26field unrestricted aarch64HostUnifiedMemory : Nat
27field unrestricted aarch64HostFallbacks : Nat
28
29end-family
30
31family AArch64HostRequirements : Type 0
32constructor AArch64HostRequirementsValue
33field unrestricted aarch64RequirementImplementer : Nat
34field unrestricted aarch64RequirementMinimumCores : Nat
35field unrestricted aarch64RequirementMinimumMemoryBytes : (family ModelWord64)
36field unrestricted aarch64RequirementPageSizeBytes : Nat
37field unrestricted aarch64RequirementNoHostFallback : Nat
38
39end-family
40
41family AArch64HostChecks : Type 0
42constructor AArch64HostChecksValue
43field unrestricted aarch64HostImplementerAccepted : Nat
44field unrestricted aarch64HostCoreCountAccepted : Nat
45field unrestricted aarch64HostMemoryAccepted : Nat
46field unrestricted aarch64HostPageSizeAccepted : Nat
47field unrestricted aarch64HostNoFallbackAccepted : Nat
48
49end-family
50
51family AArch64HostAdmission : Type 0
52constructor AArch64HostAccepted
53field unrestricted aarch64HostAcceptedChecks : (family AArch64HostChecks)
54constructor AArch64HostRejected
55field unrestricted aarch64HostRejectedChecks : (family AArch64HostChecks)
56
57end-family
58
59def aarch64HostOne : Nat =
60 (succ zero)
61
62def aarch64HostWord64AtLeast =
63 (lambda unrestricted observed : (family ModelWord64) .
64 (lambda unrestricted required : (family ModelWord64) .
65 (naturalIsZero (modelWord64LessThan observed required))))
66
67def aarch64HostChecks =
68 (lambda unrestricted requirements : (family AArch64HostRequirements) .
69 (lambda unrestricted observed : (family AArch64HostCapabilities) .
70 (eliminate
71 AArch64HostRequirements
72 (lambda unrestricted current : (family AArch64HostRequirements) .
73 (family AArch64HostChecks))
74 requirements
75 (branch
76 AArch64HostRequirementsValue
77 requiredImplementer
78 requiredCores
79 requiredMemory
80 requiredPageSize
81 requiredNoFallback
82 .
83 (eliminate
84 AArch64HostCapabilities
85 (lambda unrestricted current : (family AArch64HostCapabilities) .
86 (family AArch64HostChecks))
87 observed
88 (branch
89 AArch64HostCapabilitiesValue
90 observedImplementer
91 observedPerformancePart
92 observedPerformanceCount
93 observedEfficiencyPart
94 observedEfficiencyCount
95 observedMemory
96 observedPageSize
97 observedLevel2
98 observedLevel3
99 observedUnified
100 observedFallbacks
101 .
102 (constructor
103 AArch64HostChecks
104 AArch64HostChecksValue
105 (naturalEqual observedImplementer requiredImplementer)
106 (naturalLessOrEqual
107 requiredCores
108 (naturalAdd observedPerformanceCount observedEfficiencyCount))
109 (aarch64HostWord64AtLeast observedMemory requiredMemory)
110 (naturalEqual observedPageSize requiredPageSize)
111 (naturalEqual (naturalIsZero observedFallbacks) requiredNoFallback))))))))
112
113def aarch64HostChecksAccepted =
114 (lambda unrestricted checks : (family AArch64HostChecks) .
115 (eliminate
116 AArch64HostChecks
117 (lambda unrestricted current : (family AArch64HostChecks) . Nat)
118 checks
119 (branch
120 AArch64HostChecksValue
121 implementer
122 coreCount
123 memory
124 pageSize
125 noFallback
126 .
127 (naturalAnd
128 implementer
129 (naturalAnd coreCount (naturalAnd memory (naturalAnd pageSize noFallback)))))))
130
131def aarch64HostAdmit =
132 (lambda unrestricted requirements : (family AArch64HostRequirements) .
133 (lambda unrestricted observed : (family AArch64HostCapabilities) .
134 (app
135 (lambda unrestricted checks : (family AArch64HostChecks) .
136 (nat-eliminate
137 (lambda unrestricted accepted : Nat . (family AArch64HostAdmission))
138 (constructor AArch64HostAdmission AArch64HostRejected checks)
139 (lambda unrestricted predecessor : Nat .
140 (lambda unrestricted induction : (family AArch64HostAdmission) .
141 (constructor AArch64HostAdmission AArch64HostAccepted checks)))
142 (aarch64HostChecksAccepted checks)))
143 (aarch64HostChecks requirements observed))))
144
145def aarch64HostAdmissionAccepted =
146 (lambda unrestricted admission : (family AArch64HostAdmission) .
147 (eliminate
148 AArch64HostAdmission
149 (lambda unrestricted current : (family AArch64HostAdmission) . Nat)
150 admission
151 (branch AArch64HostAccepted checks . aarch64HostOne)
152 (branch AArch64HostRejected checks . zero)))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.