src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy
changeset 41561 d1318f3c86ba
child 56798 939e88e79724
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,100 @@
     1.4 +(*  Title:      HOL/SPARK/Examples/RIPEMD-160/Hash.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 Hash
    1.11 +imports RMD_Specification
    1.12 +begin
    1.13 +
    1.14 +spark_open "rmd/hash.siv"
    1.15 +
    1.16 +abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where
    1.17 +  "from_chain c \<equiv> (
    1.18 +    word_of_int (h0 c),
    1.19 +    word_of_int (h1 c),
    1.20 +    word_of_int (h2 c),
    1.21 +    word_of_int (h3 c),
    1.22 +    word_of_int (h4 c))"
    1.23 +
    1.24 +abbreviation to_chain :: "RMD.chain \<Rightarrow> chain" where
    1.25 +  "to_chain c \<equiv>
    1.26 +    (let (h0, h1, h2, h3, h4) = c in
    1.27 +      (|h0 = uint h0,
    1.28 +        h1 = uint h1,
    1.29 +        h2 = uint h2,
    1.30 +        h3 = uint h3,
    1.31 +        h4 = uint h4|))"
    1.32 +
    1.33 +abbreviation round' :: "chain \<Rightarrow> block \<Rightarrow> chain" where
    1.34 +  "round' c b == to_chain (round (\<lambda>n. word_of_int (b (int n))) (from_chain c))"
    1.35 +
    1.36 +abbreviation rounds' :: "chain \<Rightarrow> int \<Rightarrow> message \<Rightarrow> chain" where
    1.37 +  "rounds' h i X ==
    1.38 +     to_chain (rounds
    1.39 +      (\<lambda>n. \<lambda>m. word_of_int (X (int n) (int m)))
    1.40 +      (from_chain h)
    1.41 +      (nat i))"
    1.42 +
    1.43 +abbreviation rmd_hash :: "message \<Rightarrow> int \<Rightarrow> chain" where
    1.44 +  "rmd_hash X i == to_chain (rmd
    1.45 +    (\<lambda>n. \<lambda>m. word_of_int (X (int n) (int m)))
    1.46 +    (nat i))"
    1.47 +
    1.48 +spark_proof_functions
    1.49 +  round_spec = round'
    1.50 +  rounds = rounds'
    1.51 +  rmd_hash = rmd_hash
    1.52 +
    1.53 +spark_vc function_hash_12
    1.54 +  using H1 H6
    1.55 +  by (simp add:
    1.56 +    rounds_def rmd_body_def round_def
    1.57 +    h_0_def h0_0_def h1_0_def h2_0_def h3_0_def h4_0_def)
    1.58 +
    1.59 +
    1.60 +lemma rounds_step:
    1.61 +  assumes "0 <= i"
    1.62 +  shows "rounds X b (Suc i) = round (X i) (rounds X b i)"
    1.63 +  by (simp add: rounds_def rmd_body_def)
    1.64 +
    1.65 +lemma from_to_id: "from_chain (to_chain C) = C"
    1.66 +proof (cases C)
    1.67 +  fix a b c d e f::word32
    1.68 +  assume "C = (a, b, c, d, e)"
    1.69 +  thus ?thesis by (cases a) simp
    1.70 +qed
    1.71 +
    1.72 +lemma steps_to_steps':
    1.73 +  "round X (foldl a b c) = round X (from_chain (to_chain (foldl a b c)))"
    1.74 +  unfolding from_to_id ..
    1.75 +
    1.76 +lemma rounds'_step:
    1.77 +  assumes "0 <= i"
    1.78 +  shows "rounds' c (i + 1) x = round' (rounds' c i x) (x i)"
    1.79 +proof -
    1.80 +  have makesuc: "nat (i + 1) = Suc (nat i)" using assms by simp
    1.81 +  show ?thesis using assms
    1.82 +    by (simp add: makesuc rounds_def rmd_body_def steps_to_steps')
    1.83 +qed
    1.84 +
    1.85 +
    1.86 +spark_vc function_hash_13
    1.87 +proof -
    1.88 +  have loop_suc: "loop__1__i + 2 = (loop__1__i + 1) + 1" by simp
    1.89 +  have "0 <= loop__1__i + 1" using `0 <= loop__1__i` by simp
    1.90 +  show ?thesis
    1.91 +    unfolding loop_suc
    1.92 +    unfolding rounds'_step[OF `0 <= loop__1__i + 1`]
    1.93 +    unfolding H1[symmetric]
    1.94 +    unfolding H18 ..
    1.95 +qed
    1.96 +
    1.97 +
    1.98 +spark_vc function_hash_17
    1.99 +  unfolding rmd_def H1 rounds_def ..
   1.100 +
   1.101 +spark_end
   1.102 +
   1.103 +end