Documentation

Cryptlib.Primitives.Hash.Sha512

SHA-512 (FIPS 180-4) #

64-bit words, 80 rounds, 128-byte blocks, 64-byte digest. Tested against testdata/sha512.json.

source
structure Cryptlib.Primitives.Hash.Sha512.Digest :
Type

The eight-word chaining state.

Instances For
    source
    def Cryptlib.Primitives.Hash.Sha512.initHash :
    Digest

    Initial hash values: fractional parts of the square roots of the first eight primes.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Cryptlib.Primitives.Hash.Sha512.K :
      Array UInt64

      Round constants: fractional parts of the cube roots of the first eighty primes.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Cryptlib.Primitives.Hash.Sha512.Digest.word (d : Digest) :
        Nat → UInt64
        Equations
        Instances For
          source
          def Cryptlib.Primitives.Hash.Sha512.Digest.toVec (d : Digest) :
          Vector UInt8 64

          The digest as 64 big-endian bytes.

          Equations
          Instances For
            source
            def Cryptlib.Primitives.Hash.Sha512.be128 (n : Nat) :
            ByteArray

            Big-endian 128-bit encoding of the message length in bits.

            Equations
            Instances For
              source
              def Cryptlib.Primitives.Hash.Sha512.pad (msg : ByteArray) :
              ByteArray

              FIPS 180-4 padding: 0x80, then zeros, then the 128-bit big-endian bit length, to a multiple of 128 bytes.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Cryptlib.Primitives.Hash.Sha512.toWords (b : ByteArray) :
                Array UInt64

                Big-endian 64-bit words of a padded message.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Cryptlib.Primitives.Hash.Sha512.schedule (block : Array UInt64) :
                  Array UInt64

                  The message schedule: sixteen words from the block, extended to eighty.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Cryptlib.Primitives.Hash.Sha512.compress (block : Array UInt64) (st : Digest) :
                    Digest

                    One application of the compression function.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Cryptlib.Primitives.Hash.Sha512.sha512 (msg : ByteArray) :
                      Vector UInt8 64

                      SHA-512.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Cryptlib.Primitives.Hash.Sha512.sha512_256 (msg : ByteArray) :
                        Vector UInt8 32
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          The Hash instance #

                          State is the accumulated message, so update_append and hash_spec follow from ByteArray append lemmas.

                          source
                          def Cryptlib.Primitives.Hash.Sha512.Scheme :
                          Hash.Hash
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For