1063def sha256Update =
1064 (lambda unrestricted context : (family SHA256Context) .
1065 (lambda unrestricted input : Bytes .
1066 (eliminate
1067 SHA256ContextValidationResult
1068 (lambda unrestricted current : (family SHA256ContextValidationResult) .
1069 (family SHA256ContextUpdateResult))
1070 (sha256ValidateContext context)
1071 (branch
1072 SHA256ContextValidated
1073 validated
1074 validationTelemetry
1075 .
1076 (eliminate
1077 SHA256Context
1078 (lambda unrestricted current : (family SHA256Context) .
1079 (family SHA256ContextUpdateResult))
1080 validated
1081 (branch
1082 SHA256ContextValue
1083 state
1084 totalBytes
1085 pending
1086 .
1087 (app
1088 (lambda unrestricted inputBytes : Nat .
1089 (eliminate
1090 SHA256NaturalWord64Result
1091 (lambda unrestricted current : (family SHA256NaturalWord64Result) .
1092 (family SHA256ContextUpdateResult))
1093 (sha256NaturalToWord64 inputBytes)
1094 (branch
1095 SHA256NaturalWord64Succeeded
1096 inputWord64
1097 .
1098 (eliminate
1099 ModelWord64CheckedResult
1100 (lambda unrestricted current : (family ModelWord64CheckedResult) .
1101 (family SHA256ContextUpdateResult))
1102 (modelWord64AddChecked totalBytes inputWord64)
1103 (branch
1104 ModelWord64CheckedSucceeded
1105 nextTotalBytes
1106 .
1107 (nat-eliminate
1108 (lambda unrestricted withinLimit : Nat .
1109 (family SHA256ContextUpdateResult))
1110 (constructor
1111 SHA256ContextUpdateResult
1112 SHA256ContextUpdateFailed
1113 (constructor SHA256ErrorCode SHA256InputLengthOverflow)
1114 zero
1115 zero
1116 (sha256DigestTelemetryInitial inputBytes zero))
1117 (lambda unrestricted limitPredecessor : Nat .
1118 (lambda unrestricted limitInduction : (family SHA256ContextUpdateResult) .
1119 (sha256UpdatePart2
1120 input
1121 state
1122 totalBytes
1123 pending
1124 inputBytes
1125 nextTotalBytes
1126 (bytes-length pending))))
1127 (sha256Word64WithinInputLimit nextTotalBytes)))
1128 (branch
1129 ModelWord64CheckedFailed
1130 arithmeticError
1131 .
1132 (constructor
1133 SHA256ContextUpdateResult
1134 SHA256ContextUpdateFailed
1135 (constructor SHA256ErrorCode SHA256InputLengthOverflow)
1136 zero
1137 zero
1138 (sha256DigestTelemetryInitial inputBytes zero)))))
1139 (branch
1140 SHA256NaturalWord64Failed
1141 error
1142 .
1143 (constructor
1144 SHA256ContextUpdateResult
1145 SHA256ContextUpdateFailed
1146 error
1147 zero
1148 zero
1149 (sha256DigestTelemetryInitial inputBytes zero)))))
1150 (bytes-length input)))))
1151 (branch
1152 SHA256ContextValidationFailed
1153 error
1154 validationTelemetry
1155 .
1156 (constructor
1157 SHA256ContextUpdateResult
1158 SHA256ContextUpdateFailed
1159 error
1160 zero
1161 zero
1162 (sha256DigestTelemetryInitial (bytes-length input) 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.