typedef byte := unsigned bits[8];
typedef word := unsigned bits[32];
typedef wordA := mod[2**32];

def A : word;
def B : word;
def C : word;
def D : word;
def E : word;
def W : vector[80] of word;

def K : vector[4] of word := { 
	(word)0x5A827999, (word)0x6ED9EBA1, (word)0x8F1BBCDC, (word)0xCA62C1D6 
};

/* SHA1 compression function modifying global state */

def sha1_compress(Mi : vector[16] of word) : void {

    def Al, Bl, Cl, Dl, El, T : word;

    W[0..15] := Mi;
    seq j := 16 to 79 { W[j] := (W[j-3] ^ W[j-8] ^ W[j-14] ^ W[j-16]) <| 1; }
    Al := A; Bl := B; Cl := C; Dl := D; El := E; 
    seq j := 0 to 19 {
        T := (word)((wordA)(A <| 5) + (wordA)((B&C)|((~B)&D)) 
           + (wordA)E + (wordA)K[0] + (wordA)W[j]);
        E := D; D := C; C := B <| 30; B := A; A := T;
    }
    seq j := 20 to 39 {
        T := (word)((wordA)(A <| 5) + (wordA)(B^C^D) 
           + (wordA)E + (wordA)K[1] + (wordA)W[j]);
        E := D; D := C; C := B <| 30; B := A; A := T;
    }
    seq j := 40 to 59 {
        T := (word)((wordA)(A <| 5) + (wordA)((B&C)|(B&D)|(C&D)) 
           + (wordA)E + (wordA)K[2] + (wordA)W[j]);
        E := D; D := C; C := B <| 30; B := A; A := T;
    }
    seq j := 60 to 79 {
        T := (word)((wordA)(A <| 5) + (wordA)(B^C^D) 
           + (wordA)E + (wordA)K[3] + (wordA)W[j]);
        E := D; D := C; C := B <| 30; B := A; A := T;
    }
    A := (word)((wordA)A + (wordA)Al);
    B := (word)((wordA)B + (wordA)Bl);
    C := (word)((wordA)C + (wordA)Cl);
    D := (word)((wordA)D + (wordA)Dl);
    E := (word)((wordA)E + (wordA)El);
 }

/* SHA1 padding: nWords is the correct multiple of 16 */
def sha1_padd(const l : register int { l > 0 }, const nWords : register int { nWords > 0}, msg : vector[l] of byte) : vector[nWords] of word {
    def c : register int;
    def M : vector[nWords] of word;

    c := 0;

    seq i := 0 to l / 4 - 1 { 
        M[i] := msg[c+3] @ msg[c+2] @ msg[c+1] @ msg[c];
        c := c + 4;
    }
 
    if (l - c == 0) {
        M[l / 4] := 0b10000000000000000000000000000000;
    }
    else {
        if (l - c == 1) {
            M[l / 4] := 0b100000000000000000000000 @ msg[c];
        }
        else {
            if (l - c == 2) {
                M[l / 4] := 0b1000000000000000 @ msg[c+1] @ msg[c];    
            }
            else /* (l - c == 3) */ {
                M[l / 4] := 0b10000000 @ msg[c+2] @ msg[c+1] @ msg[c];    
            }
        }
    }

    seq i := (l / 4 + 1) to (nWords - 3) {
      M[i] := 0b00000000000000000000000000000000;
    }

    M[nWords - 2] := (word) ((int)l * 8 / 0x100000000);
    M[nWords - 1] := (word) ((int)l * 8);

    return M;
}

/* SHA1 algorithm taking message of length l bytes */
def sha1(const l : register int { l > 0 }, msg : vector[l] of byte) : unsigned bits[160] {
    def M : vector[16] of word;
    def c, k: register int;
    def res : unsigned bits[160];

    /* Compute the padded input as vector of words */
    def const nBlocks : register int := (l * 8 + 64) / 512 + 1;
    def blocks : vector[16 * nBlocks] of word; 
    blocks := sha1_padd(l, 16 * nBlocks, msg); 

    /* Initialize state */
	A := (word)0x67452301;
	B := (word)0xEFCDAB89;
	C := (word)0x98BADCFE;
	D := (word)0x10325476;
	E := (word)0xC3D2E1F0;	

    /* Iterate compression function */
    seq i := 0 to nBlocks - 1 {
        M[0..15] := blocks[i * 16 .. i * 16 + 15];
        sha1_compress(M);
    }

    res := E @ D @ C @ B @ A;

    return res;
}

/* SHA1 test vector #1: "abc" */

def output : unsigned bits[160];

def sha1_test1() : void {
    def msg : vector[3] of byte := { (byte)0x61, (byte)0x62, (byte)0x63 };
    output := sha1(3,msg);
}

/* SHA1 test vector #2: "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq" */

def sha1_test2() : void {
    def msg : vector[56] of byte := { (byte)0x61, (byte)0x62, (byte)0x63, (byte)0x64, (byte)0x62, (byte)0x63, 
                                      (byte)0x64, (byte)0x65, (byte)0x63, (byte)0x64, (byte)0x65, (byte)0x66,
                                      (byte)0x64, (byte)0x65, (byte)0x66, (byte)0x67, (byte)0x65, (byte)0x66, 
                                      (byte)0x67, (byte)0x68, (byte)0x66, (byte)0x67, (byte)0x68, (byte)0x69,
                                      (byte)0x67, (byte)0x68, (byte)0x69, (byte)0x6a, (byte)0x68, (byte)0x69, 
                                      (byte)0x6a, (byte)0x6b, (byte)0x69, (byte)0x6a, (byte)0x6b, (byte)0x6c,
                                      (byte)0x6a, (byte)0x6b, (byte)0x6c, (byte)0x6d, (byte)0x6b, (byte)0x6c, 
                                      (byte)0x6d, (byte)0x6e, (byte)0x6c, (byte)0x6d, (byte)0x6e, (byte)0x6f,
                                      (byte)0x6d, (byte)0x6e, (byte)0x6f, (byte)0x70, (byte)0x6e, (byte)0x6f, 
                                      (byte)0x70, (byte)0x71 };

    output := sha1(56,msg);
}

/* SHA1 test vector #3: "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu" */

def sha1_test3() : void {
    def msg : vector[112] of byte := {(byte)0x61, (byte)0x62, (byte)0x63, (byte)0x64, (byte)0x65, (byte)0x66, 
                                      (byte)0x67, (byte)0x68, (byte)0x62, (byte)0x63, (byte)0x64, (byte)0x65,
                                      (byte)0x66, (byte)0x67, (byte)0x68, (byte)0x69, (byte)0x63, (byte)0x64, 
                                      (byte)0x65, (byte)0x66, (byte)0x67, (byte)0x68, (byte)0x69, (byte)0x6a,
                                      (byte)0x64, (byte)0x65, (byte)0x66, (byte)0x67, (byte)0x68, (byte)0x69, 
                                      (byte)0x6a, (byte)0x6b, (byte)0x65, (byte)0x66, (byte)0x67, (byte)0x68,
                                      (byte)0x69, (byte)0x6a, (byte)0x6b, (byte)0x6c, (byte)0x66, (byte)0x67, 
                                      (byte)0x68, (byte)0x69, (byte)0x6a, (byte)0x6b, (byte)0x6c, (byte)0x6d,
                                      (byte)0x67, (byte)0x68, (byte)0x69, (byte)0x6a, (byte)0x6b, (byte)0x6c, 
                                      (byte)0x6d, (byte)0x6e, (byte)0x68, (byte)0x69, (byte)0x6a, (byte)0x6b,
                                      (byte)0x6c, (byte)0x6d, (byte)0x6e, (byte)0x6f, (byte)0x69, (byte)0x6a, 
                                      (byte)0x6b, (byte)0x6c, (byte)0x6d, (byte)0x6e, (byte)0x6f, (byte)0x70,
                                      (byte)0x6a, (byte)0x6b, (byte)0x6c, (byte)0x6d, (byte)0x6e, (byte)0x6f, 
                                      (byte)0x70, (byte)0x71, (byte)0x6b, (byte)0x6c, (byte)0x6d, (byte)0x6e,
                                      (byte)0x6f, (byte)0x70, (byte)0x71, (byte)0x72, (byte)0x6c, (byte)0x6d, 
                                      (byte)0x6e, (byte)0x6f, (byte)0x70, (byte)0x71, (byte)0x72, (byte)0x73,
                                      (byte)0x6d, (byte)0x6e, (byte)0x6f, (byte)0x70, (byte)0x71, (byte)0x72, 
                                      (byte)0x73, (byte)0x74, (byte)0x6e, (byte)0x6f, (byte)0x70, (byte)0x71,
                                      (byte)0x72, (byte)0x73, (byte)0x74, (byte)0x75 };

    output := sha1(112,msg);
}

/* SHA1 test vector #4: one million repetitions of "a" */

def sha1_test4() : void {
    def msg : vector[1000000] of byte;

    seq i := 0 to 999999 {
        msg[i] := (byte)0x61;
    }

    output := sha1(1000000,msg);
}