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.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
```