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.