459def sha256PadMessage =
460 (lambda unrestricted input : Bytes .
461 (app
462 (lambda unrestricted originalBytes : Nat .
463 (app
464 (lambda unrestricted bitLength : Nat .
465 (eliminate
466 SHA256LengthEncodingResult
467 (lambda unrestricted current : (family SHA256LengthEncodingResult) .
468 (family SHA256PaddingResult))
469 (sha256EncodeBitLength bitLength)
470 (branch
471 SHA256LengthEncodingSucceeded
472 lengthBytes
473 encodedBitLength
474 .
475 (app
476 (lambda unrestricted zeroCount : Nat .
477 (app
478 (lambda unrestricted padded : Bytes .
479 (app
480 (lambda unrestricted totalBytes : Nat .
481 (nat-eliminate
482 (lambda unrestricted aligned : Nat . (family SHA256PaddingResult))
483 (constructor
484 SHA256PaddingResult
485 SHA256PaddingFailed
486 (constructor SHA256ErrorCode SHA256BlockLengthInvalid))
487 (lambda unrestricted predecessor : Nat .
488 (lambda unrestricted induction : (family SHA256PaddingResult) .
489 (constructor
490 SHA256PaddingResult
491 SHA256PaddingSucceeded
492 padded
493 (constructor
494 SHA256PaddingTelemetry
495 SHA256PaddingTelemetryValue
496 originalBytes
497 encodedBitLength
498 zeroCount
499 totalBytes
500 (naturalDivideUnchecked totalBytes sha256NaturalSixtyFour)))))
501 (naturalIsZero
502 (naturalModuloUnchecked totalBytes sha256NaturalSixtyFour))))
503 (bytes-length padded)))
504 (bytes-append
505 input
506 (bytes-cons
507 (byte 128)
508 (bytes-append (sha256ZeroBytes zeroCount) lengthBytes)))))
509 (sha256PaddingZeroCount originalBytes)))
510 (branch
511 SHA256LengthEncodingFailed
512 error
513 remaining
514 .
515 (constructor SHA256PaddingResult SHA256PaddingFailed error))))
516 (naturalMultiply originalBytes sha256PaddingNaturalEight)))
517 (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.