solutions/zokrates_prover/.zokrates/stdlib/hashes/sha256/shaRound.zok

// FIPS 180-3, section 4.2.2
// https://csrc.nist.gov/csrc/media/publications/fips/180/3/archive/2008-10-31/documents/fips180-3_final.pdf
const u32[64] K = [
    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
];

def rotr32<N>(u32 x) -> u32 {
    return (x >> N) | (x << (32 - N));
}

def extend(u32[64] w, u32 i) -> u32 {
    u32 s0 = rotr32::<7>(w[i-15]) ^ rotr32::<18>(w[i-15]) ^ (w[i-15] >> 3);
    u32 s1 = rotr32::<17>(w[i-2]) ^ rotr32::<19>(w[i-2]) ^ (w[i-2] >> 10);
    return w[i-16] + s0 + w[i-7] + s1;
}

def temp1(u32 e, u32 f, u32 g, u32 h, u32 k, u32 w) -> u32 {
    // ch := (e and f) xor ((not e) and g)
    u32 ch = (e & f) ^ ((!e) & g);

    // S1 := (e rightrotate 6) xor (e rightrotate 11) xor (e rightrotate 25)
    u32 S1 = rotr32::<6>(e) ^ rotr32::<11>(e) ^ rotr32::<25>(e);
    
    // temp1 := h + S1 + ch + k + w
    return h + S1 + ch + k + w;
}

def temp2(u32 a, u32 b, u32 c) -> u32 {
    // maj := (a and b) xor (a and c) xor (b and c)
    u32 maj = (a & b) ^ (a & c) ^ (b & c);

    // S0 := (a rightrotate 2) xor (a rightrotate 13) xor (a rightrotate 22)
    u32 S0 = rotr32::<2>(a) ^ rotr32::<13>(a) ^ rotr32::<22>(a);

    // temp2 := S0 + maj
    return S0 + maj;
}

// A function that computes one round of the SHA256 compression function given an input and the current value of the hash
// this is used by other components however many times needed
def main(u32[16] input, u32[8] current) -> u32[8] {
    u32 mut h0 = current[0];
    u32 mut h1 = current[1];
    u32 mut h2 = current[2];
    u32 mut h3 = current[3];
    u32 mut h4 = current[4];
    u32 mut h5 = current[5];
    u32 mut h6 = current[6];
    u32 mut h7 = current[7];

    u32[64] mut w = [...input, ...[0u32; 48]];

    for u32 i in 16..64 {
        w[i] = extend(w, i);
    }

    u32 mut a = h0;
    u32 mut b = h1;
    u32 mut c = h2;
    u32 mut d = h3;
    u32 mut e = h4;
    u32 mut f = h5;
    u32 mut g = h6;
    u32 mut h = h7;

    for u32 i in 0..64 {
        u32 t1 = temp1(e, f, g, h, K[i], w[i]);
        u32 t2 = temp2(a, b, c);

        h = g;
        g = f;
        f = e;
        e = d + t1;
        d = c;
        c = b;
        b = a;
        a = t1 + t2;
    }

    h0 = h0 + a;
    h1 = h1 + b;
    h2 = h2 + c;
    h3 = h3 + d;
    h4 = h4 + e;
    h5 = h5 + f;
    h6 = h6 + g;
    h7 = h7 + h;

    return [h0, h1, h2, h3, h4, h5, h6, h7];
}