Specification.cry

/*
 * Implementation of the secure hash algorithms known as SHA2 from [FIPS-180-4].
 *
 * This implementation does not support SHA-1. It does support:
 * - SHA-224
 * - SHA-256
 * - SHA-384
 * - SHA-512
 * - SHA-512/224
 * - SHA-512/256
 *
 * References
 * [FIPS-180-4]: National Institute of Standards and Technology. Secure Hash
 *     Standard (SHS). (Department of Commerce, Washington, D.C.), Federal
 *     Information Processing Standards Publication (FIPS) NIST FIPS 180-4.
 *     August 2015.
 *     @see https://doi.org/10.6028/NIST.FIPS.180-4
 *
 * @copyright Galois, Inc.
 * @author Marcella Hastings <marcella@galois.com>
 *
 */
module Primitive::Keyless::Hash::SHA2::Specification where

parameter
    /**
     * Length of words, in bits, that are used during hashing.
     *
     * The specification defines words to be either 32 bits (for
     * SHA-224 and SHA-256) or 64 bits (for SHA-384, SHA-512, and
     * SHA-512/t for any valid `t`).
     * [FIPS-180-4] Section 1, Figure 1.
     */
    type w : #
    type constraint (w % 32 == 0, 32 <= w, 64 >= w)

    /**
     * Length of the message digest produced by the hash algorithm.
     *
     * Allowable values for each word size `w` are defined in [FIPS-180-4]
     * Section 1, Figure 1.
     *
     * The spec does not explicitly require that the digest size is a multiple
     * of 8, but all the allowable sizes are; adding this explicit constraint
     * allows us to define a hash function that operates over bytes.
     */
    type DigestSize : #
    type constraint (8 * w >= DigestSize, DigestSize % 8 == 0)

    /**
     * Initial hash value.
     * These are defined in [FIPS-180-4] Section 5.3.
     */
    H0 : [8][w]

/**
 * Upper bound on the width of messages that can be processed.
 * [FIPS-180-4] Section 1, Figure 1, "Message Size (bits)"
 */
type MessageUpperBound = 2 * w
type constraint ValidMessageLength L = width L < MessageUpperBound

/**
 * Length of the hash digest.
 *
 * This is made public to instantiate the `HashInterface`.
 */
type DigestLength = DigestSize

/**
 * Security strength (in bits) of the hash function.
 * @see NIST SP 800-107 (to be withdrawn): https://csrc.nist.gov/pubs/sp/800/107/r1/final
 * @see Hash functions webpage: https://csrc.nist.gov/projects/hash-functions
 *
 * This is made public to instantiate the `HashInterface`.
 */
type SecurityStrength = DigestSize / 2

private
    /**
     * Size of blocks of data used in hashing, measured in bits.
     *
     * This is denoted `m` in the spec. [FIPS-180-4] Section 1, Figure 1.
     */
    type BlockSize = 16 * w

    /**
     * `ScheduleLength` is fixed based on `w`: 64 when `w = 32` and 80 when `w = 64`.
     * We encode this using the relation `48 + w/2`.
     *
     * It is not explicitly defined with this name in the spec. You can see it used
     * in several places:
     * - The constant `K` has `ScheduleLength` words ([FIPS-180-4] Section
     *   4.2.2 and 4.2.3)
     * - The message schedule `W` has length `ScheduleLength` ([FIPS-180-4]
     *   Section 6.2.2 #1 and Section 6.4.2 #1)
     */
    type ScheduleLength = 48 + w / 2

    /**
     * Circular rotate left operation.
     * [FIPS-180-4] Section 2.2.2 and Section 3.2 #5.
     */
    ROTL : {n} (n < w) => [w] -> [w]
    ROTL x = x <<< `n

    /**
     * Circular rotate right operation.
     * [FIPS-180-4] Section 2.2.2 and Section 3.2 #4.
     */
    ROTR : {n} (n < w) => [w] -> [w]
    ROTR x = x >>> `n

    /**
     * Circular rotations have a specific kind of circularity.
     * [FIPS-180-4] Section 3.2 #6.
     *
     * We check this for a sampling of `n`s.
     * ```repl
     * :prove rotationEquivalenceRelationsHold`{0}
     * :prove rotationEquivalenceRelationsHold`{1}
     * :prove rotationEquivalenceRelationsHold`{w-1}
     * :prove rotationEquivalenceRelationsHold`{w/2}
     * ```
     */
    rotationEquivalenceRelationsHold : {n} (n < w) => [w] -> Bool
    property rotationEquivalenceRelationsHold x = left && right where
        left = ROTL`{n} x == ROTR`{(w - n) % w} x
        right = ROTR`{n} x == ROTL`{(w - n) % w} x

    /**
     * Right shift operation.
     * [FIPS-180-4] Section 2.2.2 and Section 3.2 #3
     */
    SHR : {n} (n < w) => [w] -> [w]
    SHR x = x >> `n

    /**
     * The default Cryptol representation of hex digits and bit strings matches
     * the requirements of the spec.
     * [FIPS-180-4] Section 3.1, #1.
     * ```repl
     * :prove hexDigitsEncodeCorrectly
     * ```
     */
    property hexDigitsEncodeCorrectly = (0x7 == 0b0111) && (0xa == 0b1010)

    /**
     * The default Cryptol representation of hex words and bit strings matches
     * the requirements of the spec.
     * [FIPS-180-4] Section 3.1, #2.
     * ```repl
     * :prove wordsEncodeCorrectly
     * ```
     */
    property wordsEncodeCorrectly = short && long where
        short = 0xa103fe23 == 0b10100001000000111111111000100011
        long = 0xa103fe2332ef301a == 0b1010000100000011111111100010001100110010111011110011000000011010

    /**
     * The default Cryptol representation of integers and hex words matches
     * the requirements of the spec.
     * [FIPS-180-4] Section 3.1, #3.
     * ```repl
     * :prove integersEncodeCorrectly
     * ```
     */
    property integersEncodeCorrectly = 291 == 0x00000123

    /**
     * The first logical function for the SHA family.
     * [FIPS-180-4] Section 4.1.2, Equation 4.2 and Section 4.1.3, Equation 4.8.
     */
    Ch : [w] -> [w] -> [w] -> [w]
    Ch x y z = (x && y) ^ (~x && z)

    /**
     * The second logical function for the SHA family.
     * [FIPS-180-4] Section 4.1.2, Equation 4.3 and Section 4.1.3, Equation 4.9.
     */
    Maj : [w] -> [w] -> [w] -> [w]
    Maj x y z = (x && y) ^ (x && z) ^ (y && z)

    /**
     * The third logical function for the SHA family.
     * [FIPS-180-4] Section 4.1.2, Equation 4.4 and Section 4.1.3, Equation 4.10.
     */
    Sigma0: [w] -> [w]
    Sigma0 x
        | w == 32 => ROTR`{ 2} x ^ ROTR`{13} x ^ ROTR`{22} x
        | w == 64 => ROTR`{28} x ^ ROTR`{34} x ^ ROTR`{39} x

    /**
     * The fourth logical function for the SHA family.
     * [FIPS-180-4] Section 4.1.2, Equation 4.5 and Section 4.1.3, Equation 4.11.
     */
    Sigma1: [w] -> [w]
    Sigma1 x
        | w == 32 => ROTR`{ 6} x ^ ROTR`{11} x ^ ROTR`{25} x
        | w == 64 => ROTR`{14} x ^ ROTR`{18} x ^ ROTR`{41} x

    /**
     * The fifth logical function for the SHA family.
     * [FIPS-180-4] Section 4.1.2, Equation 4.6 and Section 4.1.3, Equation 4.12.
     */
    sigma0: [w] -> [w]
    sigma0 x
        | w == 32 => ROTR`{7} x ^ ROTR`{18} x ^ SHR`{3} x
        | w == 64 => ROTR`{1} x ^ ROTR`{ 8} x ^ SHR`{7} x

    /**
     * The sixth logical function for the SHA family.
     * [FIPS-180-4] Section 4.1.2, Equation 4.7 and Section 4.1.3, Equation 4.13.
     */
    sigma1: [w] -> [w]
    sigma1 x
        | w == 32 => ROTR`{17} x ^ ROTR`{19} x ^ SHR`{10} x
        | w == 64 => ROTR`{19} x ^ ROTR`{61} x ^ SHR`{ 6} x

    /**
     * The SHA family uses a sequence of constant `w`-bit words, which represent
     * the first `w` bits of the fractional parts of the cube roots of the first
     * `ScheduleLength` prime numbers.
     *
     * [FIPS-180-4] Section 4.2.2 and 4.2.3.
     */
    K : [ScheduleLength][w]
    K | w == 32 => [
        0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5,
        0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174,
        0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da,
        0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967,
        0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85,
        0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070,
        0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3,
        0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2]
      | w == 64 => [
        0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc,
        0x3956c25bf348b538, 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118,
        0xd807aa98a3030242, 0x12835b0145706fbe, 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2,
        0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235, 0xc19bf174cf692694,
        0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65,
        0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5,
        0x983e5152ee66dfab, 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4,
        0xc6e00bf33da88fc2, 0xd5a79147930aa725, 0x06ca6351e003826f, 0x142929670a0e6e70,
        0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed, 0x53380d139d95b3df,
        0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b,
        0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30,
        0xd192e819d6ef5218, 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8,
        0x19a4c116b8d2d0c8, 0x1e376c085141ab53, 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8,
        0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373, 0x682e6ff3d6b2b8a3,
        0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec,
        0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b,
        0xca273eceea26619c, 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178,
        0x06f067aa72176fba, 0x0a637dc5a2c898a6, 0x113f9804bef90dae, 0x1b710b35131c471b,
        0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc, 0x431d67c49c100d4c,
        0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817]


    /**
     * Number of bits used to encode the length of the message for padding.
     * [FIPS-180-4] Section 5.1.
     */
    type LengthBits = 2 * w
    /**
     * Number of blocks needed to hold the padded version of a message of length L.
     * [FIPS-180-4] Section 5.1.
     */
    type NumBlocks L = (L + 1 + LengthBits) /^ BlockSize

    /**
     * Deterministically pad a message to a multiple of the block size.
     *
     * [FIPS-180-4] Section 5.1.1 and 5.1.2.
     *
     * The constraint is not explicitly noted in Section 5.1, but all
     * messages to be hashed must not exceed the valid message length.
     */
    pad : {L} (ValidMessageLength L) => [L] -> [NumBlocks L * BlockSize]
    pad M = M # 0b1 # zero # (`L : [LengthBits])

    /**
     * The example used to demonstrate padding in the spec works.
     * [FIPS-180-4] Section 5.1.1 and Section 5.1.2.
     * ```repl
     * :prove paddingExampleWorks
     * ```
     */
    paddingExampleWorks : Bool
    paddingExampleWorks
        | w == 32 => pad (join "abc") == (0b01100001 # 0b01100010 # 0b01100011
            # 0b1 # (zero : [423]) # (zero : [59]) # 0b11000)
        | w == 64 => pad (join "abc") == (0b01100001 # 0b01100010 # 0b01100011
            # 0b1 # (zero : [871]) # (zero : [123]) # 0b11000)

    /**
     * The message and its padding must be parsed into `N` blocks.
     * [FIPS-180-4] Section 5.2.
     */
    parse : {N} () => [N * BlockSize] -> [N][BlockSize]
    parse M = split M


/**
 * Secure hash function.
 *
 * All the SHA functions (excluding SHA-1) share the same structure.
 * The primary differences can be handled through Cryptol's built-in
 * polymorphism:
 * - The word sizes are different;
 * - The length of the message schedule and subsequent number of iterations
 *   over the working variables are different; and
 * - The digest length is different.
 *
 * [FIPS-180-4] Section 6.2 - 6.7.
 * The hash functionality itself is primarily described in Sections 6.2 and
 * 6.4. The correct truncation for other bit lengths is in the other sections.
 */
hash: {l} (ValidMessageLength l) => [l] -> [DigestSize]
hash M = take (join (digest ! 0)) where
    digest = [H0] # [Hi'
        where
            // Step 1. Prepare the message schedule.
            Ws = messageSchedule (split Mi)

            // Step 2. Initialize the eight working variables with the
            // previous hash value.
            letters = [(Hi0, Hi1, Hi2, Hi3, Hi4, Hi5, Hi6, Hi7)] # [
                // Step 3. Update temporary and working variables...
                variableUpdate l Kt Wt
                | l <- letters

                // ...for t=0 to `ScheduleLength`.
                | Wt <- Ws
                | Kt <- K
            ]
            (a, b, c, d, e, f, g, h) = letters ! 0

            // Step 4. Compute the next intermediate hash value.
            // Note that in the spec, this is denoted H^(i).
            Hi' = [a + Hi0, b + Hi1, c + Hi2, d + Hi3, e + Hi4, f + Hi5, g + Hi6, h + Hi7]

        // Each message block is processed in order.
        | Mi <- parse (pad M)

        // An intermediate hash digest is computed at each iteration.
        // Note that in the spec, these are denoted H^(i-1)_j for j = 0..7.
        | [Hi0, Hi1, Hi2, Hi3, Hi4, Hi5, Hi6, Hi7] <- digest
    ]

    // Step 1. Prepare the message schedule.
    messageSchedule : [16][w] -> [ScheduleLength][w]
    messageSchedule Mi = take W where
        W : [inf][w]
        W = Mi # [ sigma1 w2 + w7 + sigma0 w15 + w16
            // The spec indexes these by counting from the other direction.
            // We can't do that here because it's an infinite sequence.
            // Note that 15 - the drop parameter is the index in the spec.
            | w16 <- W
            | w15 <- drop`{1} W
            | w7  <- drop`{9} W
            | w2  <- drop`{14} W
        ]

    // Convenience type to describe the set of working variables a - h.
    type LetterVars = ([w], [w], [w], [w], [w], [w], [w], [w])

    // Step 3. Update temporary and working variables (one iteration).
    variableUpdate : LetterVars -> [w] -> [w] -> LetterVars
    variableUpdate (a, b, c, d, e, f, g, h) Kt Wt =
        (a', b', c', d', e', f', g', h')
        where
            T1 = h + Sigma1 e + Ch e f g + Kt + Wt
            T2 = Sigma0 a + Maj a b c
            h' = g
            g' = f
            f' = e
            e' = d + T1
            d' = c
            c' = b
            b' = a
            a' = T1 + T2

/**
 * Secure hash function, computed over bytes.
 *
 * This is not explicitly part of the spec, but many applications represent
 * their input and output over byte strings (rather than bit strings as used
 * in the spec itself).
 */
hashBytes: {l} (ValidMessageLength (8 * l)) => [l][8] -> [DigestSize / 8][8]
hashBytes M = groupBy`{8} (hash (join M))