src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
changeset 41561 d1318f3c86ba
child 41588 9546828c0eb3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,47 @@
     1.4 +(*  Title:      HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
     1.5 +    Author:     Fabian Immler, TU Muenchen
     1.6 +
     1.7 +Verification of the RIPEMD-160 hash function
     1.8 +*)
     1.9 +
    1.10 +theory RMD_Specification
    1.11 +imports RMD SPARK
    1.12 +
    1.13 +begin
    1.14 +
    1.15 +(* bit operations *)
    1.16 +
    1.17 +abbreviation rotate_left :: "int \<Rightarrow> int \<Rightarrow> int" where
    1.18 +  "rotate_left i w == uint (word_rotl (nat i) (word_of_int w::word32))"
    1.19 +
    1.20 +spark_proof_functions
    1.21 +  wordops__rotate_left = rotate_left
    1.22 +
    1.23 +
    1.24 +(* Conversions for proof functions *)
    1.25 +abbreviation k_l_spec :: " int => int " where
    1.26 +  "k_l_spec j == uint (K (nat j))"
    1.27 +abbreviation k_r_spec :: " int => int " where
    1.28 +  "k_r_spec j == uint (K' (nat j))"
    1.29 +abbreviation r_l_spec :: " int => int " where
    1.30 +  "r_l_spec j == int (r (nat j))"
    1.31 +abbreviation r_r_spec :: " int => int " where
    1.32 +  "r_r_spec j == int (r' (nat j))"
    1.33 +abbreviation s_l_spec :: " int => int " where
    1.34 +  "s_l_spec j == int (s (nat j))"
    1.35 +abbreviation s_r_spec :: " int => int " where
    1.36 +  "s_r_spec j == int (s' (nat j))"
    1.37 +abbreviation f_spec :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
    1.38 +  "f_spec j x y z ==
    1.39 +    uint (f (nat j) (word_of_int x::word32) (word_of_int y) (word_of_int z))"
    1.40 +
    1.41 +spark_proof_functions
    1.42 +  k_l_spec = k_l_spec
    1.43 +  k_r_spec = k_r_spec
    1.44 +  r_l_spec = r_l_spec
    1.45 +  r_r_spec = r_r_spec
    1.46 +  s_l_spec = s_l_spec
    1.47 +  s_r_spec = s_r_spec
    1.48 +  f_spec = f_spec
    1.49 +
    1.50 +end