Padding for an already resident message. Derive only the at-most-two-block
suffix; callers need not materialize the message to plan its native layout.
The checked length bound precedes multiplication into the 64-bit bit count.
294def sha256PaddingSuffix =
295 (lambda unrestricted originalBytes : Nat .
296 (nat-eliminate
297 (lambda unrestricted valid : Nat . (family StdResult (family SHA256ErrorCode) Bytes))
298 (constructor
299 StdResult
300 StdFailure
301 (family SHA256ErrorCode)
302 Bytes
303 (constructor SHA256ErrorCode SHA256InputLengthOverflow))
304 (lambda unrestricted previous : Nat .
305 (lambda unrestricted ignored : (family StdResult (family SHA256ErrorCode) Bytes) .
306 (eliminate
307 SHA256LengthEncodingResult
308 (lambda unrestricted current : (family SHA256LengthEncodingResult) .
309 (family StdResult (family SHA256ErrorCode) Bytes))
310 (sha256EncodeBitLength (naturalMultiply originalBytes 8))
311 (branch
312 SHA256LengthEncodingSucceeded
313 encoded
314 bitLength
315 .
316 (constructor
317 StdResult
318 StdSuccess
319 (family SHA256ErrorCode)
320 Bytes
321 (bytes-cons
322 (byte 128)
323 (bytes-append (sha256ZeroBytes (sha256PaddingZeroCount originalBytes)) encoded))))
324 (branch
325 SHA256LengthEncodingFailed
326 code
327 remaining
328 .
329 (constructor StdResult StdFailure (family SHA256ErrorCode) Bytes code)))))
330 (naturalLessOrEqual originalBytes (modelWord64Natural sha256MaximumInputBytes))))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.