Compress `count` blocks off the front of `input`, returning the state and
what is left (no length check: the caller sizes the groups).
708def sha256DigestRunBlockGroup =
709 (lambda unrestricted count : Nat .
710 (nat-eliminate
711 (lambda unrestricted current : Nat .
712 (pi unrestricted state : (family SHA256State) .
713 (pi unrestricted input : Bytes .
714 (pi unrestricted telemetry : (family SHA256DigestTelemetry) .
715 (family SHA256DigestGroupResult)))))
716 (lambda unrestricted state : (family SHA256State) .
717 (lambda unrestricted input : Bytes .
718 (lambda unrestricted telemetry : (family SHA256DigestTelemetry) .
719 (constructor SHA256DigestGroupResult SHA256DigestGroupSucceeded state input telemetry))))
720 (lambda unrestricted predecessor : Nat .
721 (lambda unrestricted induction : (pi unrestricted state : (family SHA256State) . (pi unrestricted input : Bytes . (pi unrestricted telemetry : (family SHA256DigestTelemetry) . (family SHA256DigestGroupResult)))) .
722 (lambda unrestricted state : (family SHA256State) .
723 (lambda unrestricted input : Bytes .
724 (lambda unrestricted telemetry : (family SHA256DigestTelemetry) .
725 (eliminate
726 SHA256CompressionResult
727 (lambda unrestricted current : (family SHA256CompressionResult) .
728 (family SHA256DigestGroupResult))
729 (sha256CompressBlock
730 state
731 (sha256DigestTakeWithFuel sha256NaturalSixtyFour input))
732 (branch
733 SHA256CompressionSucceeded
734 nextState
735 compressionTelemetry
736 .
737 (induction
738 nextState
739 (sha256DigestDropWithFuel sha256NaturalSixtyFour input)
740 (sha256DigestTelemetryAddCompression telemetry compressionTelemetry)))
741 (branch
742 SHA256CompressionFailed
743 error
744 failedIndex
745 .
746 (constructor
747 SHA256DigestGroupResult
748 SHA256DigestGroupFailed
749 error
750 (sha256DigestTelemetryBlockCount telemetry)
751 failedIndex
752 telemetry))))))))
753 count))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.