|
(* Title: HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
Author: Fabian Immler, TU Muenchen
Verification of the RIPEMD-160 hash function
*)
theory RMD_Specification
imports RMD "HOL-SPARK.SPARK"
begin
\<comment> \<open>bit operations\<close>
abbreviation rotate_left :: "int \ int \ int" where
"rotate_left i w == uint (word_rotl (nat i) (word_of_int w::word32))"
spark_proof_functions
wordops__rotate_left = rotate_left
\<comment> \<open>Conversions for proof functions\<close>
abbreviation k_l_spec :: " int => int " where
"k_l_spec j == uint (K (nat j))"
abbreviation k_r_spec :: " int => int " where
"k_r_spec j == uint (K' (nat j))"
abbreviation r_l_spec :: " int => int " where
"r_l_spec j == int (r (nat j))"
abbreviation r_r_spec :: " int => int " where
"r_r_spec j == int (r' (nat j))"
abbreviation s_l_spec :: " int => int " where
"s_l_spec j == int (s (nat j))"
abbreviation s_r_spec :: " int => int " where
"s_r_spec j == int (s' (nat j))"
abbreviation f_spec :: "int \ int \ int \ int \ int" where
"f_spec j x y z ==
uint (f (nat j) (word_of_int x::word32) (word_of_int y) (word_of_int z))"
spark_proof_functions
k_l_spec = k_l_spec
k_r_spec = k_r_spec
r_l_spec = r_l_spec
r_r_spec = r_r_spec
s_l_spec = s_l_spec
s_r_spec = s_r_spec
f_spec = f_spec
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
