Part of `sha256Update`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
937def sha256UpdatePart1 =
938 (lambda unrestricted state : (family SHA256State) .
939 (lambda unrestricted totalBytes : (family ModelWord64) .
940 (lambda unrestricted inputBytes : Nat .
941 (lambda unrestricted nextTotalBytes : (family ModelWord64) .
942 (lambda unrestricted pendingBefore : Nat .
943 (lambda unrestricted combined : Bytes .
944 (lambda unrestricted combinedBytes : Nat .
945 (lambda unrestricted compressedBytes : Nat .
946 (lambda unrestricted compressedBlocks : Nat .
947 (app
948 (lambda unrestricted compressed : Bytes .
949 (app
950 (lambda unrestricted nextPending : Bytes .
951 (app
952 (lambda unrestricted operations : (family SHA256DigestTelemetry) .
953 (eliminate
954 SHA256DigestBlockRunResult
955 (lambda unrestricted current : (family SHA256DigestBlockRunResult) .
956 (family SHA256ContextUpdateResult))
957 (sha256DigestRunBlocks
958 compressedBlocks
959 state
960 compressed
961 operations)
962 (branch
963 SHA256DigestBlocksSucceeded
964 nextState
965 nextOperations
966 .
967 (app
968 (lambda unrestricted nextContext : (family SHA256Context) .
969 (eliminate
970 SHA256ContextValidationResult
971 (lambda unrestricted current : (family SHA256ContextValidationResult) .
972 (family SHA256ContextUpdateResult))
973 (sha256ValidateContext nextContext)
974 (branch
975 SHA256ContextValidated
976 checkedContext
977 checkedTelemetry
978 .
979 (constructor
980 SHA256ContextUpdateResult
981 SHA256ContextUpdateSucceeded
982 checkedContext
983 (constructor
984 SHA256UpdateTelemetry
985 SHA256UpdateTelemetryValue
986 inputBytes
987 totalBytes
988 pendingBefore
989 combinedBytes
990 compressedBytes
991 compressedBlocks
992 (bytes-length nextPending)
993 nextTotalBytes
994 nextOperations)))
995 (branch
996 SHA256ContextValidationFailed
997 nextError
998 nextValidation
999 .
1000 (constructor
1001 SHA256ContextUpdateResult
1002 SHA256ContextUpdateFailed
1003 nextError
1004 compressedBlocks
1005 zero
1006 nextOperations))))
1007 (constructor
1008 SHA256Context
1009 SHA256ContextValue
1010 nextState
1011 nextTotalBytes
1012 nextPending)))
1013 (branch
1014 SHA256DigestBlocksFailed
1015 blockError
1016 blockOrdinal
1017 internalIndex
1018 partialTelemetry
1019 .
1020 (constructor
1021 SHA256ContextUpdateResult
1022 SHA256ContextUpdateFailed
1023 blockError
1024 blockOrdinal
1025 internalIndex
1026 partialTelemetry))))
1027 (sha256DigestTelemetryInitial inputBytes compressedBytes)))
1028 (sha256DigestDropWithFuel compressedBytes combined)))
1029 (sha256DigestTakeWithFuel compressedBytes combined)))))))))))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.