src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
author haftmann
Sat, 01 Mar 2014 17:08:39 +0100
changeset 55818 d8b2f50705d0
parent 41588 9546828c0eb3
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
more precise imports; avoid duplicated simp rules in fact collections; dropped redundancy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     1
(*  Title:      HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     2
    Author:     Fabian Immler, TU Muenchen
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     3
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     4
Verification of the RIPEMD-160 hash function
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     5
*)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     6
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     7
theory RMD_Specification
55818
d8b2f50705d0 more precise imports;
haftmann
parents: 41588
diff changeset
     8
imports RMD "~~/src/HOL/SPARK/SPARK"
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     9
begin
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    10
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    11
(* bit operations *)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    12
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    13
abbreviation rotate_left :: "int \<Rightarrow> int \<Rightarrow> int" where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    14
  "rotate_left i w == uint (word_rotl (nat i) (word_of_int w::word32))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    15
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    16
spark_proof_functions
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    17
  wordops__rotate_left = rotate_left
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    18
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    19
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    20
(* Conversions for proof functions *)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    21
abbreviation k_l_spec :: " int => int " where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    22
  "k_l_spec j == uint (K (nat j))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    23
abbreviation k_r_spec :: " int => int " where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    24
  "k_r_spec j == uint (K' (nat j))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    25
abbreviation r_l_spec :: " int => int " where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    26
  "r_l_spec j == int (r (nat j))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    27
abbreviation r_r_spec :: " int => int " where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    28
  "r_r_spec j == int (r' (nat j))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    29
abbreviation s_l_spec :: " int => int " where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    30
  "s_l_spec j == int (s (nat j))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    31
abbreviation s_r_spec :: " int => int " where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    32
  "s_r_spec j == int (s' (nat j))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    33
abbreviation f_spec :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    34
  "f_spec j x y z ==
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    35
    uint (f (nat j) (word_of_int x::word32) (word_of_int y) (word_of_int z))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    36
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    37
spark_proof_functions
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    38
  k_l_spec = k_l_spec
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    39
  k_r_spec = k_r_spec
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    40
  r_l_spec = r_l_spec
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    41
  r_r_spec = r_r_spec
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    42
  s_l_spec = s_l_spec
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    43
  s_r_spec = s_r_spec
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    44
  f_spec = f_spec
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    45
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    46
end