Source/Packages

Data.SHA256Digest

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

1,631 lines150 declarations64.2 KiBSHA-256 c46a79f2ab9a

def · lines 1164–1277

sha256Finalize

Full file
1164def sha256Finalize =
1165  (lambda unrestricted context : (family SHA256Context) .
1166    (eliminate
1167      SHA256Context
1168      (lambda unrestricted current : (family SHA256Context) . (family SHA256ContextFinalizeResult))
1169      context
1170      (branch
1171        SHA256ContextValue
1172        state
1173        totalBytes
1174        pending
1175        .
1176        (eliminate
1177          SHA256ContextPaddingResult
1178          (lambda unrestricted current : (family SHA256ContextPaddingResult) .
1179            (family SHA256ContextFinalizeResult))
1180          (sha256PadContext context)
1181          (branch
1182            SHA256ContextPaddingSucceeded
1183            suffix
1184            paddingTelemetry
1185            .
1186            (eliminate
1187              SHA256ContextPaddingTelemetry
1188              (lambda unrestricted current : (family SHA256ContextPaddingTelemetry) .
1189                (family SHA256ContextFinalizeResult))
1190              paddingTelemetry
1191              (branch
1192                SHA256ContextPaddingTelemetryValue
1193                checkedTotal
1194                pendingBytes
1195                bitLength
1196                zeroBytes
1197                finalBytes
1198                blockCount
1199                .
1200                (app
1201                  (lambda unrestricted operations : (family SHA256DigestTelemetry) .
1202                    (eliminate
1203                      SHA256DigestBlockRunResult
1204                      (lambda unrestricted current : (family SHA256DigestBlockRunResult) .
1205                        (family SHA256ContextFinalizeResult))
1206                      (sha256DigestRunBlocks blockCount state suffix operations)
1207                      (branch
1208                        SHA256DigestBlocksSucceeded
1209                        finalState
1210                        finalOperations
1211                        .
1212                        (app
1213                          (lambda unrestricted digestBytes : Bytes .
1214                            (eliminate
1215                              SHA256Result
1216                              (lambda unrestricted current : (family SHA256Result) .
1217                                (family SHA256ContextFinalizeResult))
1218                              (sha256DigestFromBytes digestBytes)
1219                              (branch
1220                                SHA256Succeeded
1221                                digest
1222                                .
1223                                (constructor
1224                                  SHA256ContextFinalizeResult
1225                                  SHA256ContextFinalizeSucceeded
1226                                  digest
1227                                  (constructor
1228                                    SHA256FinalizeTelemetry
1229                                    SHA256FinalizeTelemetryValue
1230                                    checkedTotal
1231                                    pendingBytes
1232                                    bitLength
1233                                    zeroBytes
1234                                    finalBytes
1235                                    blockCount
1236                                    (bytes-length digestBytes)
1237                                    finalOperations)))
1238                              (branch
1239                                SHA256Failed
1240                                error
1241                                .
1242                                (constructor
1243                                  SHA256ContextFinalizeResult
1244                                  SHA256ContextFinalizeFailed
1245                                  error
1246                                  blockCount
1247                                  zero
1248                                  finalOperations))))
1249                          (sha256DigestStateBytes finalState)))
1250                      (branch
1251                        SHA256DigestBlocksFailed
1252                        blockError
1253                        blockOrdinal
1254                        internalIndex
1255                        partialTelemetry
1256                        .
1257                        (constructor
1258                          SHA256ContextFinalizeResult
1259                          SHA256ContextFinalizeFailed
1260                          blockError
1261                          blockOrdinal
1262                          internalIndex
1263                          partialTelemetry))))
1264                  (sha256DigestTelemetryInitial pendingBytes finalBytes)))))
1265          (branch
1266            SHA256ContextPaddingFailed
1267            error
1268            stage
1269            validationTelemetry
1270            .
1271            (constructor
1272              SHA256ContextFinalizeResult
1273              SHA256ContextFinalizeFailed
1274              error
1275              stage
1276              zero
1277              (sha256DigestTelemetryInitial (bytes-length pending) zero)))))))

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.