src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
author haftmann
Sat, 01 Mar 2014 17:08:39 +0100
changeset 55818 d8b2f50705d0
parent 45546 6dd3e88de4c2
child 56798 939e88e79724
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/Round.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 Round
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
     8
imports RMD_Specification
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
spark_open "rmd/round.siv"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    12
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    13
abbreviation from_chain :: "chain \<Rightarrow> RMD.chain" where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    14
  "from_chain c \<equiv> (
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    15
    word_of_int (h0 c),
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    16
    word_of_int (h1 c),
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    17
    word_of_int (h2 c),
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    18
    word_of_int (h3 c),
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    19
    word_of_int (h4 c))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    20
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    21
abbreviation from_chain_pair :: "chain_pair \<Rightarrow> RMD.chain \<times> RMD.chain" where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    22
  "from_chain_pair cc \<equiv> (
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    23
    from_chain (left cc),
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    24
    from_chain (right cc))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    25
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    26
abbreviation to_chain :: "RMD.chain \<Rightarrow> chain" where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    27
  "to_chain c \<equiv>
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    28
    (let (h0, h1, h2, h3, h4) = c in
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    29
      (|h0 = uint h0,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    30
        h1 = uint h1,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    31
        h2 = uint h2,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    32
        h3 = uint h3,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    33
        h4 = uint h4|))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    34
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    35
abbreviation to_chain_pair :: "RMD.chain \<times> RMD.chain \<Rightarrow> chain_pair" where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    36
  "to_chain_pair c == (let (c1, c2) = c in
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    37
    (| left = to_chain c1,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    38
      right = to_chain c2 |))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    39
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    40
abbreviation steps' :: "chain_pair \<Rightarrow> int \<Rightarrow> block \<Rightarrow> chain_pair" where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    41
  "steps' cc i b == to_chain_pair (steps
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    42
    (\<lambda>n. word_of_int (b (int n)))
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    43
    (from_chain_pair cc)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    44
    (nat i))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    45
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    46
abbreviation round_spec :: "chain \<Rightarrow> block \<Rightarrow> chain" where
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    47
  "round_spec c b == to_chain (round (\<lambda>n. word_of_int (b (int n))) (from_chain c))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    48
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    49
spark_proof_functions
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    50
  steps = steps'
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    51
  round_spec = round_spec
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    52
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    53
lemma uint_word_of_int_id:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    54
  assumes "0 <= (x::int)"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    55
  assumes "x <= 4294967295"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    56
  shows"uint(word_of_int x::word32) = x"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    57
  unfolding int_word_uint
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    58
  using assms
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    59
  by (simp add:int_mod_eq')
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    60
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    61
lemma steps_step: "steps X cc (Suc i) = step_both X (steps X cc i) i"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    62
  unfolding steps_def
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    63
  by (induct i) simp_all
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    64
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    65
lemma from_to_id: "from_chain_pair (to_chain_pair CC) = CC"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    66
proof (cases CC)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    67
  fix a::RMD.chain
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    68
  fix b c d e f::word32
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    69
  assume "CC = (a, b, c, d, e, f)"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    70
  thus ?thesis by (cases a) simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    71
qed
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    72
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    73
lemma steps_to_steps':
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    74
  "F A (steps X cc i) B =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    75
   F A (from_chain_pair (to_chain_pair (steps X cc i))) B"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    76
  unfolding from_to_id ..
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    77
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    78
lemma steps'_step:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    79
  assumes "0 <= i"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    80
  shows
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    81
  "steps' cc (i + 1) X = to_chain_pair (
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    82
     step_both
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    83
       (\<lambda>n. word_of_int (X (int n)))
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    84
       (from_chain_pair (steps' cc i X))
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    85
       (nat i))"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    86
proof -
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    87
  have "nat (i + 1) = Suc (nat i)" using assms by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    88
  show ?thesis
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    89
    unfolding `nat (i + 1) = Suc (nat i)` steps_step steps_to_steps'
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    90
    ..
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    91
qed 
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    92
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    93
lemma step_from_hyp:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    94
  assumes
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    95
  step_hyp:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    96
  "\<lparr>left =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    97
      \<lparr>h0 = a, h1 = b, h2 = c, h3 = d, h4 = e\<rparr>,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    98
    right =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
    99
      \<lparr>h0 = a', h1 = b', h2 = c', h3 = d', h4 = e'\<rparr>\<rparr> =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   100
   steps'
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   101
     (\<lparr>left =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   102
         \<lparr>h0 = a_0, h1 = b_0, h2 = c_0,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   103
          h3 = d_0, h4 = e_0\<rparr>,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   104
       right =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   105
         \<lparr>h0 = a_0, h1 = b_0, h2 = c_0,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   106
          h3 = d_0, h4 = e_0\<rparr>\<rparr>)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   107
     j x"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   108
  assumes "a <= 4294967295" (is "_ <= ?M")
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   109
  assumes                "b  <= ?M" and "c  <= ?M" and "d  <= ?M" and "e  <= ?M"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   110
  assumes "a' <= ?M" and "b' <= ?M" and "c' <= ?M" and "d' <= ?M" and "e' <= ?M"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   111
  assumes "0 <= a " and "0 <= b " and "0 <= c " and "0 <= d " and "0 <= e "
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   112
  assumes "0 <= a'" and "0 <= b'" and "0 <= c'" and "0 <= d'" and "0 <= e'"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   113
  assumes "0 <= x (r_l_spec j)" and "x (r_l_spec j) <= ?M"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   114
  assumes "0 <= x (r_r_spec j)" and "x (r_r_spec j) <= ?M"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   115
  assumes "0 <= j" and "j <= 79"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   116
  shows
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   117
  "\<lparr>left =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   118
      \<lparr>h0 = e,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   119
         h1 =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   120
           (rotate_left (s_l_spec j)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   121
             ((((a + f_spec j b c d) mod 4294967296 +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   122
                x (r_l_spec j)) mod
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   123
               4294967296 +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   124
               k_l_spec j) mod
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   125
              4294967296) +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   126
            e) mod
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   127
           4294967296,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   128
         h2 = b, h3 = rotate_left 10 c,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   129
         h4 = d\<rparr>,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   130
      right =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   131
        \<lparr>h0 = e',
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   132
           h1 =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   133
             (rotate_left (s_r_spec j)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   134
               ((((a' + f_spec (79 - j) b' c' d') mod
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   135
                  4294967296 +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   136
                  x (r_r_spec j)) mod
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   137
                 4294967296 +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   138
                 k_r_spec j) mod
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   139
                4294967296) +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   140
              e') mod
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   141
             4294967296,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   142
           h2 = b', h3 = rotate_left 10 c',
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   143
           h4 = d'\<rparr>\<rparr> =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   144
   steps'
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   145
    (\<lparr>left =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   146
        \<lparr>h0 = a_0, h1 = b_0, h2 = c_0,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   147
           h3 = d_0, h4 = e_0\<rparr>,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   148
        right =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   149
          \<lparr>h0 = a_0, h1 = b_0, h2 = c_0,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   150
             h3 = d_0, h4 = e_0\<rparr>\<rparr>)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   151
    (j + 1) x"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   152
  using step_hyp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   153
proof -
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   154
  let ?MM = 4294967296
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   155
  have AL: "uint(word_of_int e::word32) = e"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   156
    by (rule uint_word_of_int_id[OF `0 <= e` `e <= ?M`])
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   157
  have CL: "uint(word_of_int b::word32) = b"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   158
    by (rule uint_word_of_int_id[OF `0 <= b` `b <= ?M`])
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   159
  have DL: "True" ..
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   160
  have EL: "uint(word_of_int d::word32) = d"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   161
    by (rule uint_word_of_int_id[OF `0 <= d` `d <= ?M`])
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   162
  have AR: "uint(word_of_int e'::word32) = e'"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   163
    by (rule uint_word_of_int_id[OF `0 <= e'` `e' <= ?M`])
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   164
  have CR: "uint(word_of_int b'::word32) = b'"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   165
    by (rule uint_word_of_int_id[OF `0 <= b'` `b' <= ?M`])
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   166
  have DR: "True" ..
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   167
  have ER: "uint(word_of_int d'::word32) = d'"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   168
    by (rule uint_word_of_int_id[OF `0 <= d'` `d' <= ?M`])
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   169
  have BL:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   170
    "(uint
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   171
      (word_rotl (s (nat j))
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   172
        ((word_of_int::int\<Rightarrow>word32)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   173
          ((((a + f_spec j b c d) mod ?MM +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   174
             x (r_l_spec j)) mod ?MM +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   175
            k_l_spec j) mod ?MM))) +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   176
        e) mod ?MM
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   177
    =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   178
    uint
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   179
              (word_rotl (s (nat j))
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   180
                (word_of_int a +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   181
                 f (nat j) (word_of_int b)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   182
                  (word_of_int c) (word_of_int d) +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   183
                 word_of_int (x (r_l_spec j)) +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   184
                 K (nat j)) +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   185
               word_of_int e)"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   186
    (is "(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _")
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   187
  proof -
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   188
    have "a mod ?MM = a" using `0 <= a` `a <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   189
      by (simp add: int_mod_eq')
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   190
    have "?X mod ?MM = ?X" using `0 <= ?X` `?X <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   191
      by (simp add: int_mod_eq')
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   192
    have "e mod ?MM = e" using `0 <= e` `e <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   193
      by (simp add: int_mod_eq')
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   194
    have "(?MM::int) = 2 ^ len_of TYPE(32)" by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   195
    show ?thesis
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   196
      unfolding
45546
6dd3e88de4c2 HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents: 41635
diff changeset
   197
        word_add_def
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   198
        uint_word_of_int_id[OF `0 <= a` `a <= ?M`]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   199
        uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   200
        int_word_uint
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   201
      unfolding `?MM = 2 ^ len_of TYPE(32)`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   202
      unfolding word_uint.Abs_norm
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   203
      by (simp add:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   204
        `a mod ?MM = a`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   205
        `e mod ?MM = e`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   206
        `?X mod ?MM = ?X`)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   207
  qed
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   208
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   209
  have BR:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   210
    "(uint
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   211
      (word_rotl (s' (nat j))
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   212
        ((word_of_int::int\<Rightarrow>word32)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   213
          ((((a' + f_spec (79 - j) b' c' d') mod ?MM +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   214
             x (r_r_spec j)) mod ?MM +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   215
            k_r_spec j) mod ?MM))) +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   216
        e') mod ?MM
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   217
    =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   218
    uint
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   219
              (word_rotl (s' (nat j))
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   220
                (word_of_int a' +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   221
                 f (79 - nat j) (word_of_int b')
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   222
                  (word_of_int c') (word_of_int d') +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   223
                 word_of_int (x (r_r_spec j)) +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   224
                 K' (nat j)) +
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   225
               word_of_int e')"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   226
    (is "(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _")
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   227
  proof -
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   228
    have "a' mod ?MM = a'" using `0 <= a'` `a' <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   229
      by (simp add: int_mod_eq')
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   230
    have "?X mod ?MM = ?X" using `0 <= ?X` `?X <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   231
      by (simp add: int_mod_eq')
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   232
    have "e' mod ?MM = e'" using `0 <= e'` `e' <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   233
      by (simp add: int_mod_eq')
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   234
    have "(?MM::int) = 2 ^ len_of TYPE(32)" by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   235
    have nat_transfer: "79 - nat j = nat (79 - j)"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   236
      using nat_diff_distrib `0 <= j`  `j <= 79`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   237
      by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   238
    show ?thesis
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   239
      unfolding
45546
6dd3e88de4c2 HOL-Word: removed many duplicate theorems (see NEWS)
huffman
parents: 41635
diff changeset
   240
        word_add_def
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   241
        uint_word_of_int_id[OF `0 <= a'` `a' <= ?M`]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   242
        uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   243
        int_word_uint
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   244
        nat_transfer
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   245
      unfolding `?MM = 2 ^ len_of TYPE(32)`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   246
      unfolding word_uint.Abs_norm
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   247
      by (simp add: 
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   248
        `a' mod ?MM = a'`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   249
        `e' mod ?MM = e'`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   250
        `?X mod ?MM = ?X`)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   251
  qed
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   252
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   253
  show ?thesis
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   254
    unfolding steps'_step[OF `0 <= j`] step_hyp[symmetric]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   255
      step_both_def step_r_def step_l_def
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   256
    by (simp add: AL BL CL DL EL AR BR CR DR ER)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   257
qed
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   258
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   259
spark_vc procedure_round_61
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   260
proof -
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   261
  let ?M = "4294967295::int"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   262
  have step_hyp:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   263
  "\<lparr>left =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   264
      \<lparr>h0 = ca, h1 = cb, h2 = cc,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   265
         h3 = cd, h4 = ce\<rparr>,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   266
      right =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   267
        \<lparr>h0 = ca, h1 = cb, h2 = cc,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   268
           h3 = cd, h4 = ce\<rparr>\<rparr> =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   269
   steps'
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   270
    (\<lparr>left =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   271
        \<lparr>h0 = ca, h1 = cb, h2 = cc,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   272
           h3 = cd, h4 = ce\<rparr>,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   273
        right =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   274
          \<lparr>h0 = ca, h1 = cb, h2 = cc,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   275
             h3 = cd, h4 = ce\<rparr>\<rparr>)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   276
    0 x"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   277
    unfolding steps_def 
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   278
    by (simp add:
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   279
      uint_word_of_int_id[OF `0 <= ca` `ca <= ?M`]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   280
      uint_word_of_int_id[OF `0 <= cb` `cb <= ?M`]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   281
      uint_word_of_int_id[OF `0 <= cc` `cc <= ?M`]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   282
      uint_word_of_int_id[OF `0 <= cd` `cd <= ?M`]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   283
      uint_word_of_int_id[OF `0 <= ce` `ce <= ?M`])
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   284
  let ?rotate_arg_l =
41635
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   285
    "((((ca + f 0 cb cc cd) mod 4294967296 +
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   286
        x (r_l 0)) mod 4294967296 + k_l 0) mod 4294967296)"
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   287
  let ?rotate_arg_r =
41635
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   288
    "((((ca + f 79 cb cc cd) mod 4294967296 +
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   289
        x (r_r 0)) mod 4294967296 + k_r 0) mod 4294967296)"
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   290
  note returns =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   291
    `wordops__rotate (s_l 0) ?rotate_arg_l =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   292
     rotate_left (s_l 0) ?rotate_arg_l`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   293
    `wordops__rotate (s_r 0) ?rotate_arg_r =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   294
     rotate_left (s_r 0) ?rotate_arg_r`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   295
    `wordops__rotate 10 cc = rotate_left 10 cc`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   296
    `f 0 cb cc cd = f_spec 0 cb cc cd`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   297
    `f 79 cb cc cd = f_spec 79 cb cc cd`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   298
    `k_l 0 = k_l_spec 0`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   299
    `k_r 0 = k_r_spec 0`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   300
    `r_l 0 = r_l_spec 0`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   301
    `r_r 0 = r_r_spec 0`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   302
    `s_l 0 = s_l_spec 0`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   303
    `s_r 0 = s_r_spec 0`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   304
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   305
  note x_borders = `\<forall>i. 0 \<le> i \<and> i \<le> 15 \<longrightarrow> 0 \<le> x i \<and> x i \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   306
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   307
  from `0 <= r_l 0` `r_l 0 <= 15` x_borders
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   308
  have "0 \<le> x (r_l 0)" by blast
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   309
  hence x_lower: "0 <= x (r_l_spec 0)" unfolding returns .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   310
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   311
  from `0 <= r_l 0` `r_l 0 <= 15` x_borders
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   312
  have "x (r_l 0) <= ?M" by blast
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   313
  hence x_upper: "x (r_l_spec 0) <= ?M" unfolding returns .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   314
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   315
  from `0 <= r_r 0` `r_r 0 <= 15` x_borders
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   316
  have "0 \<le> x (r_r 0)" by blast
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   317
  hence x_lower': "0 <= x (r_r_spec 0)" unfolding returns .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   318
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   319
  from `0 <= r_r 0` `r_r 0 <= 15` x_borders
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   320
  have "x (r_r 0) <= ?M" by blast
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   321
  hence x_upper': "x (r_r_spec 0) <= ?M" unfolding returns .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   322
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   323
  have "0 <= (0::int)" by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   324
  have "0 <= (79::int)" by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   325
  note step_from_hyp [OF
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   326
    step_hyp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   327
    H2 H4 H6 H8 H10 H2 H4 H6 H8 H10 (* upper bounds *)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   328
    H1 H3 H5 H7 H9  H1 H3 H5 H7 H9  (* lower bounds *)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   329
  ]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   330
  from this[OF x_lower x_upper x_lower' x_upper' `0 <= 0` `0 <= 79`]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   331
    `0 \<le> ca` `0 \<le> ce` x_lower x_lower'
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   332
  show ?thesis unfolding returns(1) returns(2) unfolding returns
41635
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   333
    by simp
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   334
qed
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   335
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   336
spark_vc procedure_round_62
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   337
proof -
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   338
  let ?M = "4294967295::int"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   339
  let ?rotate_arg_l =
41635
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   340
    "((((cla + f (loop__1__j + 1) clb clc cld) mod 4294967296 +
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   341
         x (r_l (loop__1__j + 1))) mod 4294967296 +
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   342
         k_l (loop__1__j + 1)) mod 4294967296)"
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   343
  let ?rotate_arg_r =
41635
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   344
    "((((cra + f (79 - (loop__1__j + 1)) crb crc crd) mod
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   345
         4294967296 + x (r_r (loop__1__j + 1))) mod 4294967296 +
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   346
         k_r (loop__1__j + 1)) mod 4294967296)"
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   347
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   348
  have s: "78 - loop__1__j = (79 - (loop__1__j + 1))" by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   349
  note returns =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   350
    `wordops__rotate (s_l (loop__1__j + 1)) ?rotate_arg_l =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   351
     rotate_left (s_l (loop__1__j + 1)) ?rotate_arg_l`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   352
    `wordops__rotate (s_r (loop__1__j + 1)) ?rotate_arg_r =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   353
     rotate_left (s_r (loop__1__j + 1)) ?rotate_arg_r`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   354
    `f (loop__1__j + 1) clb clc cld =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   355
     f_spec (loop__1__j + 1) clb clc cld`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   356
    `f (78 - loop__1__j) crb crc crd =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   357
     f_spec (78 - loop__1__j) crb crc crd`[simplified s]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   358
    `wordops__rotate 10 clc = rotate_left 10 clc`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   359
    `wordops__rotate 10 crc = rotate_left 10 crc`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   360
    `k_l (loop__1__j + 1) = k_l_spec (loop__1__j + 1)`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   361
    `k_r (loop__1__j + 1) = k_r_spec (loop__1__j + 1)`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   362
    `r_l (loop__1__j + 1) = r_l_spec (loop__1__j + 1)`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   363
    `r_r (loop__1__j + 1) = r_r_spec (loop__1__j + 1)`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   364
    `s_l (loop__1__j + 1) = s_l_spec (loop__1__j + 1)`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   365
    `s_r (loop__1__j + 1) = s_r_spec (loop__1__j + 1)`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   366
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   367
  note x_borders = `\<forall>i. 0 \<le> i \<and> i \<le> 15 \<longrightarrow> 0 \<le> x i \<and> x i \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   368
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   369
  from `0 <= r_l (loop__1__j + 1)` `r_l (loop__1__j + 1) <= 15` x_borders
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   370
  have "0 \<le> x (r_l (loop__1__j + 1))" by blast
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   371
  hence x_lower: "0 <= x (r_l_spec (loop__1__j + 1))" unfolding returns .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   372
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   373
  from `0 <= r_l (loop__1__j + 1)` `r_l (loop__1__j + 1) <= 15` x_borders
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   374
  have "x (r_l (loop__1__j + 1)) <= ?M" by blast
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   375
  hence x_upper: "x (r_l_spec (loop__1__j + 1)) <= ?M" unfolding returns .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   376
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   377
  from `0 <= r_r (loop__1__j + 1)` `r_r (loop__1__j + 1) <= 15` x_borders
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   378
  have "0 \<le> x (r_r (loop__1__j + 1))" by blast
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   379
  hence x_lower': "0 <= x (r_r_spec (loop__1__j + 1))" unfolding returns .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   380
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   381
  from `0 <= r_r (loop__1__j + 1)` `r_r (loop__1__j + 1) <= 15` x_borders
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   382
  have "x (r_r (loop__1__j + 1)) <= ?M" by blast
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   383
  hence x_upper': "x (r_r_spec (loop__1__j + 1)) <= ?M" unfolding returns .
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   384
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   385
  from `0 <= loop__1__j` have "0 <= loop__1__j + 1" by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   386
  from `loop__1__j <= 78` have "loop__1__j + 1 <= 79" by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   387
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   388
  have "loop__1__j + 1 + 1 = loop__1__j + 2" by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   389
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   390
  note step_from_hyp[OF H1
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   391
    `cla <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   392
    `clb <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   393
    `clc <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   394
    `cld <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   395
    `cle <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   396
    `cra <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   397
    `crb <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   398
    `crc <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   399
    `crd <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   400
    `cre <= ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   401
    
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   402
    `0 <= cla`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   403
    `0 <= clb`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   404
    `0 <= clc`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   405
    `0 <= cld`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   406
    `0 <= cle`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   407
    `0 <= cra`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   408
    `0 <= crb`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   409
    `0 <= crc`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   410
    `0 <= crd`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   411
    `0 <= cre`]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   412
  from this[OF
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   413
    x_lower x_upper x_lower' x_upper'
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   414
    `0 <= loop__1__j + 1` `loop__1__j + 1 <= 79`]
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   415
    `0 \<le> cla` `0 \<le> cle` `0 \<le> cra` `0 \<le> cre` x_lower x_lower'
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   416
  show ?thesis unfolding `loop__1__j + 1 + 1 = loop__1__j + 2`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   417
    unfolding returns(1) returns(2) unfolding returns
41635
f938a6022d2e Replaced smod by standard mod operator to reflect actual behaviour
berghofe
parents: 41561
diff changeset
   418
    by simp
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   419
qed
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   420
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   421
spark_vc procedure_round_76
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   422
proof -
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   423
  let ?M = "4294967295 :: int"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   424
  let ?INIT_CHAIN =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   425
     "\<lparr>h0 = ca_init, h1 = cb_init,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   426
         h2 = cc_init, h3 = cd_init,
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   427
         h4 = ce_init\<rparr>"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   428
  have steps_to_steps':
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   429
    "steps
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   430
       (\<lambda>n\<Colon>nat. word_of_int (x (int n)))
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   431
       (from_chain ?INIT_CHAIN, from_chain ?INIT_CHAIN)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   432
       80 =
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   433
    from_chain_pair (
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   434
      steps'
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   435
      (\<lparr>left = ?INIT_CHAIN, right = ?INIT_CHAIN\<rparr>)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   436
      80
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   437
      x)"
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   438
    unfolding from_to_id by simp
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   439
  from
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   440
    `0 \<le> ca_init` `ca_init \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   441
    `0 \<le> cb_init` `cb_init \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   442
    `0 \<le> cc_init` `cc_init \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   443
    `0 \<le> cd_init` `cd_init \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   444
    `0 \<le> ce_init` `ce_init \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   445
    `0 \<le> cla` `cla \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   446
    `0 \<le> clb` `clb \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   447
    `0 \<le> clc` `clc \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   448
    `0 \<le> cld` `cld \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   449
    `0 \<le> cle` `cle \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   450
    `0 \<le> cra` `cra \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   451
    `0 \<le> crb` `crb \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   452
    `0 \<le> crc` `crc \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   453
    `0 \<le> crd` `crd \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   454
    `0 \<le> cre` `cre \<le> ?M`
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   455
  show ?thesis
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   456
    unfolding round_def
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   457
    unfolding steps_to_steps'
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   458
    unfolding H1[symmetric]
55818
d8b2f50705d0 more precise imports;
haftmann
parents: 45546
diff changeset
   459
    by (simp add: uint_word_ariths(1) rdmods
41561
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   460
      uint_word_of_int_id)
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   461
qed
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   462
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   463
spark_end
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   464
d1318f3c86ba Added new SPARK verification environment.
berghofe
parents:
diff changeset
   465
end