src/HOL/SPARK/Examples/RIPEMD-160/rmd.ads
changeset 41561 d1318f3c86ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/rmd.ads	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,92 @@
     1.4 +with Wordops;
     1.5 +use type Wordops.Word;
     1.6 +--# inherit Wordops;
     1.7 +
     1.8 +package RMD
     1.9 +is
    1.10 +
    1.11 +   -- Types
    1.12 +
    1.13 +   subtype Word is Wordops.Word;
    1.14 +
    1.15 +   type Chain is
    1.16 +     record
    1.17 +        H0, H1, H2, H3, H4 : Word;
    1.18 +     end record;
    1.19 +
    1.20 +   type Block_Index is range 0..15;
    1.21 +   type Block is array(Block_Index) of Word;
    1.22 +
    1.23 +   type Message_Index is range 0..2**32;
    1.24 +   type Message is array(Message_Index range <>) of Block;
    1.25 +
    1.26 +   -- Isabelle specification
    1.27 +
    1.28 +   --# function rmd_hash(X : Message; L : Message_Index) return Chain;
    1.29 +
    1.30 +   function Hash(X : Message) return Chain;
    1.31 +   --# pre X'First = 0;
    1.32 +   --# return rmd_hash(X, X'Last + 1);
    1.33 +
    1.34 +private
    1.35 +
    1.36 +   -- Types
    1.37 +
    1.38 +   type Round_Index is range 0..79;
    1.39 +
    1.40 +   type Chain_Pair is
    1.41 +      record
    1.42 +         Left, Right : Chain;
    1.43 +      end record;
    1.44 +
    1.45 +   type Block_Permutation is array(Round_Index) of Block_Index;
    1.46 +
    1.47 +   subtype Rotate_Amount is Wordops.Rotate_Amount;
    1.48 +   type Rotate_Definition is array(Round_Index) of Rotate_Amount;
    1.49 +
    1.50 +
    1.51 +   -- Isabelle proof functions
    1.52 +
    1.53 +   --# function f_spec(J : Round_Index; X,Y,Z : Word) return Word;
    1.54 +   --# function K_l_spec(J : Round_Index) return Word;
    1.55 +   --# function K_r_spec(J : Round_Index) return Word;
    1.56 +   --# function r_l_spec(J : Round_Index) return Block_Index;
    1.57 +   --# function r_r_spec(J : Round_Index) return Block_Index;
    1.58 +   --# function s_l_spec(J : Round_Index) return Rotate_Amount;
    1.59 +   --# function s_r_spec(J : Round_Index) return Rotate_Amount;
    1.60 +   --# function steps(CS : Chain_Pair; I : Round_Index; B : Block)
    1.61 +   --#    return Chain_Pair;
    1.62 +   --# function round_spec(C : Chain; B : Block) return Chain;
    1.63 +   --# function rounds(C : Chain; I : Message_Index; X : Message)
    1.64 +   --#    return Chain;
    1.65 +
    1.66 +
    1.67 +   -- Spark Implementation
    1.68 +
    1.69 +   function F(J : Round_Index; X,Y,Z : Word) return Word;
    1.70 +   --# return f_spec(J, X, Y, Z);
    1.71 +
    1.72 +   function K_L(J : Round_Index) return Word;
    1.73 +   --# return K_l_spec(J);
    1.74 +
    1.75 +   function K_R(J : Round_Index) return Word;
    1.76 +   --# return K_r_spec(J);
    1.77 +
    1.78 +   function R_L(J : Round_Index) return Block_Index;
    1.79 +   --# return r_l_spec(J);
    1.80 +
    1.81 +   function R_R(J : Round_Index) return Block_Index;
    1.82 +   --# return r_r_spec(J);
    1.83 +
    1.84 +   function S_L(J : Round_Index) return Rotate_Amount;
    1.85 +   --# return s_l_spec(J);
    1.86 +
    1.87 +   function S_R(J : Round_Index) return Rotate_Amount;
    1.88 +   --# return s_r_spec(J);
    1.89 +
    1.90 +   procedure Round(CA, CB, CC, CD, CE : in out Word; X: in Block);
    1.91 +   --# derives CA, CB, CC, CD, CE from X, CA, CB, CC, CD, CE;
    1.92 +   --# post Chain'(CA, CB, CC, CD, CE) =
    1.93 +   --#        round_spec(Chain'(CA~, CB~, CC~, CD~, CE~), X);
    1.94 +
    1.95 +end RMD;