The public shape is unchanged: exactly `blockCount` blocks must consume the
whole input, or the run fails with SHA256BlockLengthInvalid.
801def sha256DigestRunBlocks =
802 (lambda unrestricted blockCount : Nat .
803 (lambda unrestricted state : (family SHA256State) .
804 (lambda unrestricted input : Bytes .
805 (lambda unrestricted telemetry : (family SHA256DigestTelemetry) .
806 (eliminate
807 SHA256DigestGroupResult
808 (lambda unrestricted current : (family SHA256DigestGroupResult) .
809 (family SHA256DigestBlockRunResult))
810 (sha256DigestRunBlockGroups
811 (naturalDivideUnchecked blockCount sha256DigestBlocksPerGroup)
812 (naturalModuloUnchecked blockCount sha256DigestBlocksPerGroup)
813 state
814 input
815 telemetry)
816 (branch
817 SHA256DigestGroupSucceeded
818 finalState
819 remaining
820 finalTelemetry
821 .
822 (nat-eliminate
823 (lambda unrestricted empty : Nat . (family SHA256DigestBlockRunResult))
824 (constructor
825 SHA256DigestBlockRunResult
826 SHA256DigestBlocksFailed
827 (constructor SHA256ErrorCode SHA256BlockLengthInvalid)
828 (sha256DigestTelemetryBlockCount finalTelemetry)
829 zero
830 finalTelemetry)
831 (lambda unrestricted predecessor : Nat .
832 (lambda unrestricted induction : (family SHA256DigestBlockRunResult) .
833 (constructor
834 SHA256DigestBlockRunResult
835 SHA256DigestBlocksSucceeded
836 finalState
837 finalTelemetry)))
838 (naturalIsZero (bytes-length remaining))))
839 (branch
840 SHA256DigestGroupFailed
841 error
842 ordinal
843 internalIndex
844 before
845 .
846 (constructor
847 SHA256DigestBlockRunResult
848 SHA256DigestBlocksFailed
849 error
850 ordinal
851 internalIndex
852 before)))))))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.