244def sha256CompressExpandedSchedule =
245 (lambda unrestricted initialState : (family SHA256State) .
246 (lambda unrestricted expandedSchedule : (family SHA256Schedule) .
247 (lambda unrestricted expansionTelemetry : (family SHA256ScheduleExpansionTelemetry) .
248 (eliminate
249 SHA256CompressionRoundsResult
250 (lambda unrestricted current : (family SHA256CompressionRoundsResult) .
251 (family SHA256CompressionResult))
252 (sha256CompressionRounds
253 expandedSchedule
254 sha256RoundConstants
255 (constructor
256 SHA256CompressionRoundState
257 SHA256CompressionRoundStateValue
258 initialState
259 zero
260 zero
261 zero
262 zero
263 zero))
264 (branch
265 SHA256CompressionRoundsSucceeded
266 roundState
267 .
268 (eliminate
269 SHA256CompressionRoundState
270 (lambda unrestricted current : (family SHA256CompressionRoundState) .
271 (family SHA256CompressionResult))
272 roundState
273 (branch
274 SHA256CompressionRoundStateValue
275 workingState
276 rounds
277 rotates
278 shifts
279 booleans
280 adds
281 .
282 (eliminate
283 SHA256ScheduleExpansionTelemetry
284 (lambda unrestricted current : (family SHA256ScheduleExpansionTelemetry) .
285 (family SHA256CompressionResult))
286 expansionTelemetry
287 (branch
288 SHA256ScheduleExpansionTelemetryValue
289 generated
290 lookups
291 sigmas
292 expansionRotates
293 expansionShifts
294 expansionAdds
295 .
296 (constructor
297 SHA256CompressionResult
298 SHA256CompressionSucceeded
299 (sha256StateAdd initialState workingState)
300 (constructor
301 SHA256CompressionTelemetry
302 SHA256CompressionTelemetryValue
303 sha256NaturalSixteen
304 generated
305 rounds
306 lookups
307 sigmas
308 (naturalAdd expansionRotates rotates)
309 (naturalAdd expansionShifts shifts)
310 booleans
311 (naturalAdd (byte-to-nat (byte 8)) (naturalAdd expansionAdds adds)))))))))
312 (branch
313 SHA256CompressionRoundsFailed
314 error
315 failedIndex
316 .
317 (constructor SHA256CompressionResult SHA256CompressionFailed error failedIndex))))))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.