Part of `sha256Update`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
1033def sha256UpdatePart2 =
1034 (lambda unrestricted input : Bytes .
1035 (lambda unrestricted state : (family SHA256State) .
1036 (lambda unrestricted totalBytes : (family ModelWord64) .
1037 (lambda unrestricted pending : Bytes .
1038 (lambda unrestricted inputBytes : Nat .
1039 (lambda unrestricted nextTotalBytes : (family ModelWord64) .
1040 (lambda unrestricted pendingBefore : Nat .
1041 (app
1042 (lambda unrestricted combined : Bytes .
1043 (app
1044 (lambda unrestricted combinedBytes : Nat .
1045 (app
1046 (lambda unrestricted compressedBytes : Nat .
1047 (sha256UpdatePart1
1048 state
1049 totalBytes
1050 inputBytes
1051 nextTotalBytes
1052 pendingBefore
1053 combined
1054 combinedBytes
1055 compressedBytes
1056 (naturalDivideUnchecked compressedBytes sha256NaturalSixtyFour)))
1057 (naturalSaturatingSubtract
1058 combinedBytes
1059 (naturalModuloUnchecked combinedBytes sha256NaturalSixtyFour))))
1060 (bytes-length combined)))
1061 (bytes-append pending input)))))))))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.