cao-0.1: example/sha1.cao
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);
}