1module Runtime.TelemetryIdentityRoutine
2
3import Runtime.TelemetryCapture
4import Runtime.TelemetryIdentity
5import Std.Natural
6
7-- Shared binary-role admission and process-birth identity acquisition. The
8-- host backend supplies exactly one nonblocking OS entropy request; it may
9-- return errors or short counts and must not retry or invent a fallback.
10-- AcquireEntropy reads Destination, Extent and VersionOrFlags (then flags),
11-- returns the actual signed syscall result in Result, and preserves the saved
12-- destination. Load reads a little-endian word relative to Destination.
13-- Other word operations wrap at 64 bits; Compare supplies unsigned ordering.
14-- Register assignment and the syscall ABI belong exclusively to each emitter.
15-- A failed acquisition may have touched bytes. They carry no authority until
16-- the count and every nonzero identity role have passed, returning status zero.
17family TelemetryIdentityCondition : Type 0
18constructor TelemetryIdentityZero
19constructor TelemetryIdentityNotZero
20constructor TelemetryIdentityBelow
21
22end-family
23
24family TelemetryIdentityRoutineKind : Type 0
25constructor TelemetryIdentityValidate
26constructor TelemetryIdentityReceipt
27constructor TelemetryIdentityCreate
28constructor TelemetryIdentityRenewEpoch
29
30end-family
31
32family TelemetryIdentityBackend : Type 0
33parameter erased A : Type 0
34parameter erased R : Type 0
35constructor TelemetryIdentityBackendValue
36field unrestricted backendIdentityLoad : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
37field unrestricted backendIdentityOr : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
38field unrestricted backendIdentityCompare : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
39field unrestricted backendIdentityMove : (pi unrestricted a0 : R . (pi unrestricted a1 : R . (pi unrestricted a2 : A . A)))
40field unrestricted backendIdentitySet : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
41field unrestricted backendIdentityAddImmediate : (pi unrestricted a0 : R . (pi unrestricted a1 : Nat . (pi unrestricted a2 : A . A)))
42field unrestricted backendIdentityReturn : (pi unrestricted a0 : Nat . (pi unrestricted a1 : A . A))
43field unrestricted backendIdentityLabel : (pi unrestricted a0 : Bytes . (pi unrestricted a1 : A . A))
44field unrestricted backendIdentityJumpIf : (pi unrestricted a0 : (family TelemetryIdentityCondition) . (pi unrestricted a1 : Bytes . (pi unrestricted a2 : A . A)))
45field unrestricted backendIdentityAcquireEntropy : (pi unrestricted a0 : A . A)
46field unrestricted backendIdentityEnd : A
47field unrestricted backendIdentityResult : R
48field unrestricted backendIdentityReceiptOrWord : R
49field unrestricted backendIdentityVersionOrFlags : R
50field unrestricted backendIdentityExtent : R
51field unrestricted backendIdentityDestination : R
52field unrestricted backendIdentitySavedDestination : R
53
54end-family
55
56def telemetryIdentityAssemblyFor =
57 (lambda erased A : Type 0 .
58 (lambda erased R : Type 0 .
59 (lambda unrestricted backend : (family TelemetryIdentityBackend A R) .
60 (lambda unrestricted kind : (family TelemetryIdentityRoutineKind) .
61 (eliminate
62 TelemetryIdentityBackend
63 (lambda unrestricted current : (family TelemetryIdentityBackend A R) . A)
64 backend
65 (branch
66 TelemetryIdentityBackendValue
67 identityLoad
68 identityOr
69 identityCompare
70 identityMove
71 identitySet
72 identityAddImmediate
73 identityReturn
74 identityLabel
75 identityJumpIf
76 identityAcquireEntropy
77 identityEnd
78 identityResult
79 identityReceiptOrWord
80 identityVersionOrFlags
81 identityExtent
82 identityDestination
83 identitySavedDestination
84 .
85 (let unrestricted identityCheckRole =
86 (lambda unrestricted index : Nat .
87 (lambda unrestricted tail : A .
88 (identityLoad
89 identityResult
90 (telemetryIdentityOffset index)
91 (identityLoad
92 identityReceiptOrWord
93 (naturalAdd (telemetryIdentityOffset index) captureWordBytes)
94 (identityOr
95 identityResult
96 identityReceiptOrWord
97 (identityCompare
98 identityResult
99 0
100 (identityJumpIf
101 (constructor TelemetryIdentityCondition TelemetryIdentityZero)
102 b"identity-zero"
103 tail)))))))
104 in
105 (let unrestricted identityFailures =
106 (identityLabel
107 b"identity-extent"
108 (identityReturn
109 1
110 (identityLabel
111 b"identity-entropy"
112 (identityReturn
113 2
114 (identityLabel
115 b"identity-zero"
116 (identityReturn
117 3
118 (identityLabel b"identity-version" (identityReturn 4 identityEnd))))))))
119 in
120 (let unrestricted identityValidateRoles =
121 (identityCheckRole
122 telemetryRunIdentityIndex
123 (identityCheckRole
124 telemetryAttemptIdentityIndex
125 (identityCheckRole
126 telemetryProducerIdentityIndex
127 (identityCheckRole
128 telemetryProducerEpochIndex
129 (identityReturn 0 identityFailures)))))
130 in
131 (let unrestricted identityAdmission =
132 (lambda unrestricted tail : A .
133 (identityCompare
134 identityVersionOrFlags
135 1
136 (identityJumpIf
137 (constructor TelemetryIdentityCondition TelemetryIdentityNotZero)
138 b"identity-version"
139 (identityCompare
140 identityExtent
141 telemetryIdentitySetBytes
142 (identityJumpIf
143 (constructor TelemetryIdentityCondition TelemetryIdentityBelow)
144 b"identity-extent"
145 tail)))))
146 in
147 (let unrestricted identityValidateAssembly =
148 (identityAdmission identityValidateRoles)
149 in
150 (let unrestricted identityEntropyCountAdmission =
151 (lambda unrestricted expected : Nat .
152 (lambda unrestricted received : R .
153 (identityCompare
154 received
155 expected
156 (identityJumpIf
157 (constructor TelemetryIdentityCondition TelemetryIdentityNotZero)
158 b"identity-entropy"
159 identityValidateRoles))))
160 in
161 (let unrestricted identityEntropyAdmission =
162 (identityEntropyCountAdmission telemetryIdentitySetBytes)
163 in
164 (let unrestricted identityReceiptAssembly =
165 (identityAdmission (identityEntropyAdmission identityReceiptOrWord))
166 in
167 (let unrestricted identityCreateAssembly =
168 (identityAdmission
169 (identityMove
170 identitySavedDestination
171 identityDestination
172 (identitySet
173 identityExtent
174 telemetryIdentitySetBytes
175 (identitySet
176 identityVersionOrFlags
177 1
178 (identityAcquireEntropy
179 (identityMove
180 identityDestination
181 identitySavedDestination
182 (identityEntropyAdmission identityResult)))))))
183 in
184 (let unrestricted identityEpochAssembly =
185 (identityAdmission
186 (identityCheckRole
187 telemetryRunIdentityIndex
188 (identityCheckRole
189 telemetryAttemptIdentityIndex
190 (identityCheckRole
191 telemetryProducerIdentityIndex
192 (identityMove
193 identitySavedDestination
194 identityDestination
195 (identityAddImmediate
196 identityDestination
197 telemetryIdentityBindingBytes
198 (identitySet
199 identityExtent
200 telemetryIdentityBytes
201 (identitySet
202 identityVersionOrFlags
203 1
204 (identityAcquireEntropy
205 (identityMove
206 identityDestination
207 identitySavedDestination
208 (identityEntropyCountAdmission
209 telemetryIdentityBytes
210 identityResult)))))))))))
211 in
212 (eliminate
213 TelemetryIdentityRoutineKind
214 (lambda unrestricted current : (family TelemetryIdentityRoutineKind) .
215 A)
216 kind
217 (branch TelemetryIdentityValidate . identityValidateAssembly)
218 (branch TelemetryIdentityReceipt . identityReceiptAssembly)
219 (branch TelemetryIdentityCreate . identityCreateAssembly)
220 (branch TelemetryIdentityRenewEpoch . identityEpochAssembly))))))))))))))))))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.