--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/rmd.adb Sat Jan 15 12:35:29 2011 +0100
@@ -0,0 +1,187 @@
+package body RMD is
+
+
+
+ function F(J : Round_Index; X,Y,Z : Word) return Word
+ is
+ Result: Word;
+ begin
+ if 0 <= J and J <= 15 then Result := X xor Y xor Z;
+ elsif 16 <= J and J <= 31 then Result := (X and Y) or (not X and Z);
+ elsif 32 <= J and J <= 47 then Result := (X or not Y) xor Z;
+ elsif 48 <= J and J <= 63 then Result := (X and Z) or (Y and not Z);
+ else Result := X xor (Y or not Z);
+ end if;
+ return Result;
+ end F;
+
+
+
+ function K_L(J : Round_Index) return Word
+ is
+ K: Word;
+ begin
+ if 0 <= J and J <= 15 then K := 16#0000_0000#;
+ elsif 16 <= J and J <= 31 then K := 16#5A82_7999#;
+ elsif 32 <= J and J <= 47 then K := 16#6ED9_EBA1#;
+ elsif 48 <= J and J <= 63 then K := 16#8F1B_BCDC#;
+ else K := 16#A953_FD4E#;
+ end if;
+ return K;
+ end K_L;
+
+
+ function K_R(J : Round_Index) return Word
+ is
+ K: Word;
+ begin
+ if 0 <= J and J <= 15 then K := 16#50A2_8BE6#;
+ elsif 16 <= J and J <= 31 then K := 16#5C4D_D124#;
+ elsif 32 <= J and J <= 47 then K := 16#6D70_3EF3#;
+ elsif 48 <= J and J <= 63 then K := 16#7A6D_76E9#;
+ else K := 16#0000_0000#;
+ end if;
+ return K;
+ end K_R;
+
+
+
+ function R_L(J : Round_Index) return Block_Index
+ is
+ R_Values : constant Block_Permutation := Block_Permutation'
+ (0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15,
+ 7, 4, 13, 1, 10, 6, 15, 3, 12, 0, 9, 5, 2, 14, 11, 8,
+ 3, 10, 14, 4, 9, 15, 8, 1, 2, 7, 0, 6, 13, 11, 5, 12,
+ 1, 9, 11, 10, 0, 8, 12, 4, 13, 3, 7, 15, 14, 5, 6, 2,
+ 4, 0, 5, 9, 7, 12, 2, 10, 14, 1, 3, 8, 11, 6, 15, 13);
+ --# for R_Values declare rule;
+ begin
+ return R_Values(J);
+ end R_L;
+
+
+ function R_R(J : Round_Index) return Block_Index
+ is
+ R_Values : constant Block_Permutation := Block_Permutation'
+ (5, 14, 7, 0, 9, 2, 11, 4, 13, 6, 15, 8, 1, 10, 3, 12,
+ 6, 11, 3, 7, 0, 13, 5, 10, 14, 15, 8, 12, 4, 9, 1, 2,
+ 15, 5, 1, 3, 7, 14, 6, 9, 11, 8, 12, 2, 10, 0, 4, 13,
+ 8, 6, 4, 1, 3, 11, 15, 0, 5, 12, 2, 13, 9, 7, 10, 14,
+ 12, 15, 10, 4, 1, 5, 8, 7, 6, 2, 13, 14, 0, 3, 9, 11);
+ --# for R_Values declare rule;
+ begin
+ return R_Values(J);
+ end R_R;
+
+
+ function S_L(J : Round_Index) return Rotate_Amount
+ is
+ S_Values : constant Rotate_Definition := Rotate_Definition'
+ (11, 14, 15, 12, 5, 8, 7, 9, 11, 13, 14, 15, 6, 7, 9, 8,
+ 7, 6, 8, 13, 11, 9, 7, 15, 7, 12, 15, 9, 11, 7, 13, 12,
+ 11, 13, 6, 7, 14, 9, 13, 15, 14, 8, 13, 6, 5, 12, 7, 5,
+ 11, 12, 14, 15, 14, 15, 9, 8, 9, 14, 5, 6, 8, 6, 5, 12,
+ 9, 15, 5, 11, 6, 8, 13, 12, 5, 12, 13, 14, 11, 8, 5, 6);
+ --# for S_Values declare rule;
+ begin
+ return S_Values(J);
+ end S_L;
+
+
+ function S_R(J : Round_Index) return Rotate_Amount
+ is
+ S_Values : constant Rotate_Definition := Rotate_Definition'
+ (8, 9, 9, 11, 13, 15, 15, 5, 7, 7, 8, 11, 14, 14, 12, 6,
+ 9, 13, 15, 7, 12, 8, 9, 11, 7, 7, 12, 7, 6, 15, 13, 11,
+ 9, 7, 15, 11, 8, 6, 6, 14, 12, 13, 5, 14, 13, 13, 7, 5,
+ 15, 5, 8, 11, 14, 14, 6, 14, 6, 9, 12, 9, 12, 5, 15, 8,
+ 8, 5, 12, 9, 12, 5, 14, 6, 8, 13, 6, 5, 15, 13, 11, 11);
+ --# for S_Values declare rule;
+ begin
+ return S_Values(J);
+ end S_R;
+
+
+
+ procedure Round(CA, CB, CC, CD, CE : in out Word; X : in Block)
+ is
+ CLA, CLB, CLC, CLD, CLE, CRA, CRB, CRC, CRD, CRE : Word;
+ T : Word;
+ begin
+ CLA := CA;
+ CLB := CB;
+ CLC := CC;
+ CLD := CD;
+ CLE := CE;
+ CRA := CA;
+ CRB := CB;
+ CRC := CC;
+ CRD := CD;
+ CRE := CE;
+ for J in Round_Index range 0..79
+ loop
+ -- left
+ T := Wordops.Rotate(S_L(J),
+ CLA +
+ F(J, CLB, CLC, CLD) +
+ X(R_L(J)) +
+ K_L(J)) +
+ CLE;
+ CLA := CLE;
+ CLE := CLD;
+ CLD := Wordops.Rotate(10, CLC);
+ CLC := CLB;
+ CLB := T;
+ -- right
+ T := Wordops.Rotate(S_R(J),
+ CRA +
+ F(79 - J, CRB, CRC, CRD) +
+ X(R_R(J)) +
+ K_R(J)) +
+ CRE;
+ CRA := CRE;
+ CRE := CRD;
+ CRD := Wordops.Rotate(10, CRC);
+ CRC := CRB;
+ CRB := T;
+ --# assert Chain_Pair'(Chain'(CLA, CLB, CLC, CLD, CLE),
+ --# Chain'(CRA, CRB, CRC, CRD, CRE)) =
+ --# steps(Chain_Pair'(Chain'(CA~, CB~, CC~, CD~, CE~),
+ --# Chain'(CA~, CB~, CC~, CD~, CE~)), J + 1, X)
+ --# and CA = CA~ and CB = CB~ and CC = CC~ and CD = CD~ and CE = CE~;
+ end loop;
+ T := CB + CLC + CRD;
+ CB := CC + CLD + CRE;
+ CC := CD + CLE + CRA;
+ CD := CE + CLA + CRB;
+ CE := CA + CLB + CRC;
+ CA := T;
+ end Round;
+
+ function Hash(X : Message) return Chain
+ is
+ CA_Init : constant Word := 16#6745_2301#;
+ CB_Init : constant Word := 16#EFCD_AB89#;
+ CC_Init : constant Word := 16#98BA_DCFE#;
+ CD_Init : constant Word := 16#1032_5476#;
+ CE_Init : constant Word := 16#C3D2_E1F0#;
+ CA, CB, CC, CD, CE : Word;
+ begin
+ CA := CA_Init;
+ CB := CB_Init;
+ CC := CC_Init;
+ CD := CD_Init;
+ CE := CE_Init;
+ for I in Message_Index range X'First..X'Last
+ loop
+ Round(CA, CB, CC, CD, CE, X(I));
+ --# assert Chain'(CA, CB, CC, CD, CE) = rounds(
+ --# Chain'(CA_Init, CB_Init, CC_Init, CD_Init, CE_Init),
+ --# I + 1,
+ --# X);
+ end loop;
+ return Chain'(CA, CB, CC, CD, CE);
+ end Hash;
+
+end RMD;
+