Theory Hash

(*  Title:      HOL/SPARK/Examples/RIPEMD-160/Hash.thy
    Author:     Fabian Immler, TU Muenchen

Verification of the RIPEMD-160 hash function
*)

theory Hash
imports RMD_Specification
begin

spark_open ‹rmd/hash›

abbreviation from_chain :: "chain ⇒ RMD.chain" where
  "from_chain c ≡ (
    word_of_int (h0 c),
    word_of_int (h1 c),
    word_of_int (h2 c),
    word_of_int (h3 c),
    word_of_int (h4 c))"

abbreviation to_chain :: "RMD.chain ⇒ chain" where
  "to_chain c ≡
    (let (h0, h1, h2, h3, h4) = c in
      (|h0 = uint h0,
        h1 = uint h1,
        h2 = uint h2,
        h3 = uint h3,
        h4 = uint h4|))"

abbreviation round' :: "chain ⇒ block ⇒ chain" where
  "round' c b == to_chain (round (λn. word_of_int (b (int n))) (from_chain c))"

abbreviation rounds' :: "chain ⇒ int ⇒ message ⇒ chain" where
  "rounds' h i X ==
     to_chain (rounds
      (λn. λm. word_of_int (X (int n) (int m)))
      (from_chain h)
      (nat i))"

abbreviation rmd_hash :: "message ⇒ int ⇒ chain" where
  "rmd_hash X i == to_chain (rmd
    (λn. λm. word_of_int (X (int n) (int m)))
    (nat i))"

spark_proof_functions
  round_spec = round'
  rounds = rounds'
  rmd_hash = rmd_hash

spark_vc function_hash_12
  using H1 H6
  by (simp add:
    rounds_def rmd_body_def round_def
    h_0_def h0_0_def h1_0_def h2_0_def h3_0_def h4_0_def)


lemma rounds_step:
  assumes "0 <= i"
  shows "rounds X b (Suc i) = round (X i) (rounds X b i)"
  by (simp add: rounds_def rmd_body_def)

lemma from_to_id: "from_chain (to_chain C) = C"
proof (cases C)
  fix a b c d e f::word32
  assume "C = (a, b, c, d, e)"
  thus ?thesis by (cases a) (simp add: take_bit_nat_eq_self)
qed

lemma steps_to_steps':
  "round X (foldl a b c) = round X (from_chain (to_chain (foldl a b c)))"
  unfolding from_to_id ..

lemma rounds'_step:
  assumes "0 <= i"
  shows "rounds' c (i + 1) x = round' (rounds' c i x) (x i)"
proof -
  have makesuc: "nat (i + 1) = Suc (nat i)" using assms by simp
  show ?thesis using assms
    by (simp add: makesuc rounds_def rmd_body_def steps_to_steps')
qed


spark_vc function_hash_13
proof -
  have loop_suc: "loop__1__i + 2 = (loop__1__i + 1) + 1" by simp
  have "0 <= loop__1__i + 1" using ‹0 <= loop__1__i› by simp
  show ?thesis
    unfolding loop_suc
    unfolding rounds'_step[OF ‹0 <= loop__1__i + 1›]
    unfolding H1[symmetric]
    unfolding H18 ..
qed


spark_vc function_hash_17
  unfolding rmd_def H1 rounds_def ..

spark_end

end