422def sha256PadMessage =
423 (lambda unrestricted input : Bytes .
424 (app
425 (lambda unrestricted originalBytes : Nat .
426 (app
427 (lambda unrestricted bitLength : Nat .
428 (eliminate
429 SHA256LengthEncodingResult
430 (lambda unrestricted current : (family SHA256LengthEncodingResult) .
431 (family SHA256PaddingResult))
432 (sha256EncodeBitLength bitLength)
433 (branch
434 SHA256LengthEncodingSucceeded
435 lengthBytes
436 encodedBitLength
437 .
438 (app
439 (lambda unrestricted zeroCount : Nat .
440 (app
441 (lambda unrestricted padded : Bytes .
442 (app
443 (lambda unrestricted totalBytes : Nat .
444 (nat-eliminate
445 (lambda unrestricted aligned : Nat . (family SHA256PaddingResult))
446 (constructor
447 SHA256PaddingResult
448 SHA256PaddingFailed
449 (constructor SHA256ErrorCode SHA256BlockLengthInvalid))
450 (lambda unrestricted predecessor : Nat .
451 (lambda unrestricted induction : (family SHA256PaddingResult) .
452 (constructor
453 SHA256PaddingResult
454 SHA256PaddingSucceeded
455 padded
456 (constructor
457 SHA256PaddingTelemetry
458 SHA256PaddingTelemetryValue
459 originalBytes
460 encodedBitLength
461 zeroCount
462 totalBytes
463 (naturalDivideUnchecked totalBytes sha256NaturalSixtyFour)))))
464 (naturalIsZero
465 (naturalModuloUnchecked totalBytes sha256NaturalSixtyFour))))
466 (bytes-length padded)))
467 (bytes-append
468 input
469 (bytes-cons
470 (byte 128)
471 (bytes-append (sha256ZeroBytes zeroCount) lengthBytes)))))
472 (sha256PaddingZeroCount originalBytes)))
473 (branch
474 SHA256LengthEncodingFailed
475 error
476 remaining
477 .
478 (constructor SHA256PaddingResult SHA256PaddingFailed error))))
479 (naturalMultiply originalBytes sha256PaddingNaturalEight)))
480 (bytes-length 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.