41561

1 
(* Title: HOL/SPARK/Examples/RIPEMD160/RMD_Specification.thy


2 
Author: Fabian Immler, TU Muenchen


3 


4 
Verification of the RIPEMD160 hash function


5 
*)


6 


7 
theory RMD_Specification

55818

8 
imports RMD "~~/src/HOL/SPARK/SPARK"

41561

9 
begin


10 


11 
(* bit operations *)


12 


13 
abbreviation rotate_left :: "int \<Rightarrow> int \<Rightarrow> int" where


14 
"rotate_left i w == uint (word_rotl (nat i) (word_of_int w::word32))"


15 


16 
spark_proof_functions


17 
wordops__rotate_left = rotate_left


18 


19 


20 
(* Conversions for proof functions *)


21 
abbreviation k_l_spec :: " int => int " where


22 
"k_l_spec j == uint (K (nat j))"


23 
abbreviation k_r_spec :: " int => int " where


24 
"k_r_spec j == uint (K' (nat j))"


25 
abbreviation r_l_spec :: " int => int " where


26 
"r_l_spec j == int (r (nat j))"


27 
abbreviation r_r_spec :: " int => int " where


28 
"r_r_spec j == int (r' (nat j))"


29 
abbreviation s_l_spec :: " int => int " where


30 
"s_l_spec j == int (s (nat j))"


31 
abbreviation s_r_spec :: " int => int " where


32 
"s_r_spec j == int (s' (nat j))"


33 
abbreviation f_spec :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where


34 
"f_spec j x y z ==


35 
uint (f (nat j) (word_of_int x::word32) (word_of_int y) (word_of_int z))"


36 


37 
spark_proof_functions


38 
k_l_spec = k_l_spec


39 
k_r_spec = k_r_spec


40 
r_l_spec = r_l_spec


41 
r_r_spec = r_r_spec


42 
s_l_spec = s_l_spec


43 
s_r_spec = s_r_spec


44 
f_spec = f_spec


45 


46 
end
