Source/Packages

Data.SHA256Compress

packages/foundation/standard/src/Data/SHA256Compress.alpha

354 lines36 declarations12.8 KiBSHA-256 2c70c5d89292

def · lines 319–354

sha256CompressBlock

Full file
319def sha256CompressBlock =
320  (lambda unrestricted initialState : (family SHA256State) .
321    (lambda unrestricted block : Bytes .
322      (eliminate
323        SHA256BlockDecodeResult
324        (lambda unrestricted current : (family SHA256BlockDecodeResult) .
325          (family SHA256CompressionResult))
326        (sha256DecodeBlockWords block)
327        (branch
328          SHA256BlockDecodeSucceeded
329          initialSchedule
330          decodedCount
331          .
332          (eliminate
333            SHA256ScheduleExpansionResult
334            (lambda unrestricted current : (family SHA256ScheduleExpansionResult) .
335              (family SHA256CompressionResult))
336            (sha256ExpandSchedule initialSchedule)
337            (branch
338              SHA256ScheduleExpansionSucceeded
339              expandedSchedule
340              telemetry
341              .
342              (sha256CompressExpandedSchedule initialState expandedSchedule telemetry))
343            (branch
344              SHA256ScheduleExpansionFailed
345              error
346              failedIndex
347              .
348              (constructor SHA256CompressionResult SHA256CompressionFailed error failedIndex))))
349        (branch
350          SHA256BlockDecodeFailed
351          error
352          failedOrdinal
353          .
354          (constructor SHA256CompressionResult SHA256CompressionFailed error failedOrdinal)))))

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.