src/HOL/SPARK/Examples/RIPEMD-160/Round.thy
changeset 41561 d1318f3c86ba
child 41635 f938a6022d2e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,465 @@
     1.4 +(*  Title:      HOL/SPARK/Examples/RIPEMD-160/Round.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 Round
    1.11 +imports RMD_Specification
    1.12 +begin
    1.13 +
    1.14 +spark_open "rmd/round.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 from_chain_pair :: "chain_pair \<Rightarrow> RMD.chain \<times> RMD.chain" where
    1.25 +  "from_chain_pair cc \<equiv> (
    1.26 +    from_chain (left cc),
    1.27 +    from_chain (right cc))"
    1.28 +
    1.29 +abbreviation to_chain :: "RMD.chain \<Rightarrow> chain" where
    1.30 +  "to_chain c \<equiv>
    1.31 +    (let (h0, h1, h2, h3, h4) = c in
    1.32 +      (|h0 = uint h0,
    1.33 +        h1 = uint h1,
    1.34 +        h2 = uint h2,
    1.35 +        h3 = uint h3,
    1.36 +        h4 = uint h4|))"
    1.37 +
    1.38 +abbreviation to_chain_pair :: "RMD.chain \<times> RMD.chain \<Rightarrow> chain_pair" where
    1.39 +  "to_chain_pair c == (let (c1, c2) = c in
    1.40 +    (| left = to_chain c1,
    1.41 +      right = to_chain c2 |))"
    1.42 +
    1.43 +abbreviation steps' :: "chain_pair \<Rightarrow> int \<Rightarrow> block \<Rightarrow> chain_pair" where
    1.44 +  "steps' cc i b == to_chain_pair (steps
    1.45 +    (\<lambda>n. word_of_int (b (int n)))
    1.46 +    (from_chain_pair cc)
    1.47 +    (nat i))"
    1.48 +
    1.49 +abbreviation round_spec :: "chain \<Rightarrow> block \<Rightarrow> chain" where
    1.50 +  "round_spec c b == to_chain (round (\<lambda>n. word_of_int (b (int n))) (from_chain c))"
    1.51 +
    1.52 +spark_proof_functions
    1.53 +  steps = steps'
    1.54 +  round_spec = round_spec
    1.55 +
    1.56 +lemma uint_word_of_int_id:
    1.57 +  assumes "0 <= (x::int)"
    1.58 +  assumes "x <= 4294967295"
    1.59 +  shows"uint(word_of_int x::word32) = x"
    1.60 +  unfolding int_word_uint
    1.61 +  using assms
    1.62 +  by (simp add:int_mod_eq')
    1.63 +
    1.64 +lemma steps_step: "steps X cc (Suc i) = step_both X (steps X cc i) i"
    1.65 +  unfolding steps_def
    1.66 +  by (induct i) simp_all
    1.67 +
    1.68 +lemma from_to_id: "from_chain_pair (to_chain_pair CC) = CC"
    1.69 +proof (cases CC)
    1.70 +  fix a::RMD.chain
    1.71 +  fix b c d e f::word32
    1.72 +  assume "CC = (a, b, c, d, e, f)"
    1.73 +  thus ?thesis by (cases a) simp
    1.74 +qed
    1.75 +
    1.76 +lemma steps_to_steps':
    1.77 +  "F A (steps X cc i) B =
    1.78 +   F A (from_chain_pair (to_chain_pair (steps X cc i))) B"
    1.79 +  unfolding from_to_id ..
    1.80 +
    1.81 +lemma steps'_step:
    1.82 +  assumes "0 <= i"
    1.83 +  shows
    1.84 +  "steps' cc (i + 1) X = to_chain_pair (
    1.85 +     step_both
    1.86 +       (\<lambda>n. word_of_int (X (int n)))
    1.87 +       (from_chain_pair (steps' cc i X))
    1.88 +       (nat i))"
    1.89 +proof -
    1.90 +  have "nat (i + 1) = Suc (nat i)" using assms by simp
    1.91 +  show ?thesis
    1.92 +    unfolding `nat (i + 1) = Suc (nat i)` steps_step steps_to_steps'
    1.93 +    ..
    1.94 +qed 
    1.95 +
    1.96 +lemma step_from_hyp:
    1.97 +  assumes
    1.98 +  step_hyp:
    1.99 +  "\<lparr>left =
   1.100 +      \<lparr>h0 = a, h1 = b, h2 = c, h3 = d, h4 = e\<rparr>,
   1.101 +    right =
   1.102 +      \<lparr>h0 = a', h1 = b', h2 = c', h3 = d', h4 = e'\<rparr>\<rparr> =
   1.103 +   steps'
   1.104 +     (\<lparr>left =
   1.105 +         \<lparr>h0 = a_0, h1 = b_0, h2 = c_0,
   1.106 +          h3 = d_0, h4 = e_0\<rparr>,
   1.107 +       right =
   1.108 +         \<lparr>h0 = a_0, h1 = b_0, h2 = c_0,
   1.109 +          h3 = d_0, h4 = e_0\<rparr>\<rparr>)
   1.110 +     j x"
   1.111 +  assumes "a <= 4294967295" (is "_ <= ?M")
   1.112 +  assumes                "b  <= ?M" and "c  <= ?M" and "d  <= ?M" and "e  <= ?M"
   1.113 +  assumes "a' <= ?M" and "b' <= ?M" and "c' <= ?M" and "d' <= ?M" and "e' <= ?M"
   1.114 +  assumes "0 <= a " and "0 <= b " and "0 <= c " and "0 <= d " and "0 <= e "
   1.115 +  assumes "0 <= a'" and "0 <= b'" and "0 <= c'" and "0 <= d'" and "0 <= e'"
   1.116 +  assumes "0 <= x (r_l_spec j)" and "x (r_l_spec j) <= ?M"
   1.117 +  assumes "0 <= x (r_r_spec j)" and "x (r_r_spec j) <= ?M"
   1.118 +  assumes "0 <= j" and "j <= 79"
   1.119 +  shows
   1.120 +  "\<lparr>left =
   1.121 +      \<lparr>h0 = e,
   1.122 +         h1 =
   1.123 +           (rotate_left (s_l_spec j)
   1.124 +             ((((a + f_spec j b c d) mod 4294967296 +
   1.125 +                x (r_l_spec j)) mod
   1.126 +               4294967296 +
   1.127 +               k_l_spec j) mod
   1.128 +              4294967296) +
   1.129 +            e) mod
   1.130 +           4294967296,
   1.131 +         h2 = b, h3 = rotate_left 10 c,
   1.132 +         h4 = d\<rparr>,
   1.133 +      right =
   1.134 +        \<lparr>h0 = e',
   1.135 +           h1 =
   1.136 +             (rotate_left (s_r_spec j)
   1.137 +               ((((a' + f_spec (79 - j) b' c' d') mod
   1.138 +                  4294967296 +
   1.139 +                  x (r_r_spec j)) mod
   1.140 +                 4294967296 +
   1.141 +                 k_r_spec j) mod
   1.142 +                4294967296) +
   1.143 +              e') mod
   1.144 +             4294967296,
   1.145 +           h2 = b', h3 = rotate_left 10 c',
   1.146 +           h4 = d'\<rparr>\<rparr> =
   1.147 +   steps'
   1.148 +    (\<lparr>left =
   1.149 +        \<lparr>h0 = a_0, h1 = b_0, h2 = c_0,
   1.150 +           h3 = d_0, h4 = e_0\<rparr>,
   1.151 +        right =
   1.152 +          \<lparr>h0 = a_0, h1 = b_0, h2 = c_0,
   1.153 +             h3 = d_0, h4 = e_0\<rparr>\<rparr>)
   1.154 +    (j + 1) x"
   1.155 +  using step_hyp
   1.156 +proof -
   1.157 +  let ?MM = 4294967296
   1.158 +  have AL: "uint(word_of_int e::word32) = e"
   1.159 +    by (rule uint_word_of_int_id[OF `0 <= e` `e <= ?M`])
   1.160 +  have CL: "uint(word_of_int b::word32) = b"
   1.161 +    by (rule uint_word_of_int_id[OF `0 <= b` `b <= ?M`])
   1.162 +  have DL: "True" ..
   1.163 +  have EL: "uint(word_of_int d::word32) = d"
   1.164 +    by (rule uint_word_of_int_id[OF `0 <= d` `d <= ?M`])
   1.165 +  have AR: "uint(word_of_int e'::word32) = e'"
   1.166 +    by (rule uint_word_of_int_id[OF `0 <= e'` `e' <= ?M`])
   1.167 +  have CR: "uint(word_of_int b'::word32) = b'"
   1.168 +    by (rule uint_word_of_int_id[OF `0 <= b'` `b' <= ?M`])
   1.169 +  have DR: "True" ..
   1.170 +  have ER: "uint(word_of_int d'::word32) = d'"
   1.171 +    by (rule uint_word_of_int_id[OF `0 <= d'` `d' <= ?M`])
   1.172 +  have BL:
   1.173 +    "(uint
   1.174 +      (word_rotl (s (nat j))
   1.175 +        ((word_of_int::int\<Rightarrow>word32)
   1.176 +          ((((a + f_spec j b c d) mod ?MM +
   1.177 +             x (r_l_spec j)) mod ?MM +
   1.178 +            k_l_spec j) mod ?MM))) +
   1.179 +        e) mod ?MM
   1.180 +    =
   1.181 +    uint
   1.182 +              (word_rotl (s (nat j))
   1.183 +                (word_of_int a +
   1.184 +                 f (nat j) (word_of_int b)
   1.185 +                  (word_of_int c) (word_of_int d) +
   1.186 +                 word_of_int (x (r_l_spec j)) +
   1.187 +                 K (nat j)) +
   1.188 +               word_of_int e)"
   1.189 +    (is "(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _")
   1.190 +  proof -
   1.191 +    have "a mod ?MM = a" using `0 <= a` `a <= ?M`
   1.192 +      by (simp add: int_mod_eq')
   1.193 +    have "?X mod ?MM = ?X" using `0 <= ?X` `?X <= ?M`
   1.194 +      by (simp add: int_mod_eq')
   1.195 +    have "e mod ?MM = e" using `0 <= e` `e <= ?M`
   1.196 +      by (simp add: int_mod_eq')
   1.197 +    have "(?MM::int) = 2 ^ len_of TYPE(32)" by simp
   1.198 +    show ?thesis
   1.199 +      unfolding
   1.200 +        word_add_alt
   1.201 +        uint_word_of_int_id[OF `0 <= a` `a <= ?M`]
   1.202 +        uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`]
   1.203 +        int_word_uint
   1.204 +      unfolding `?MM = 2 ^ len_of TYPE(32)`
   1.205 +      unfolding word_uint.Abs_norm
   1.206 +      by (simp add:
   1.207 +        `a mod ?MM = a`
   1.208 +        `e mod ?MM = e`
   1.209 +        `?X mod ?MM = ?X`)
   1.210 +  qed
   1.211 +
   1.212 +  have BR:
   1.213 +    "(uint
   1.214 +      (word_rotl (s' (nat j))
   1.215 +        ((word_of_int::int\<Rightarrow>word32)
   1.216 +          ((((a' + f_spec (79 - j) b' c' d') mod ?MM +
   1.217 +             x (r_r_spec j)) mod ?MM +
   1.218 +            k_r_spec j) mod ?MM))) +
   1.219 +        e') mod ?MM
   1.220 +    =
   1.221 +    uint
   1.222 +              (word_rotl (s' (nat j))
   1.223 +                (word_of_int a' +
   1.224 +                 f (79 - nat j) (word_of_int b')
   1.225 +                  (word_of_int c') (word_of_int d') +
   1.226 +                 word_of_int (x (r_r_spec j)) +
   1.227 +                 K' (nat j)) +
   1.228 +               word_of_int e')"
   1.229 +    (is "(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _")
   1.230 +  proof -
   1.231 +    have "a' mod ?MM = a'" using `0 <= a'` `a' <= ?M`
   1.232 +      by (simp add: int_mod_eq')
   1.233 +    have "?X mod ?MM = ?X" using `0 <= ?X` `?X <= ?M`
   1.234 +      by (simp add: int_mod_eq')
   1.235 +    have "e' mod ?MM = e'" using `0 <= e'` `e' <= ?M`
   1.236 +      by (simp add: int_mod_eq')
   1.237 +    have "(?MM::int) = 2 ^ len_of TYPE(32)" by simp
   1.238 +    have nat_transfer: "79 - nat j = nat (79 - j)"
   1.239 +      using nat_diff_distrib `0 <= j`  `j <= 79`
   1.240 +      by simp
   1.241 +    show ?thesis
   1.242 +      unfolding
   1.243 +        word_add_alt
   1.244 +        uint_word_of_int_id[OF `0 <= a'` `a' <= ?M`]
   1.245 +        uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`]
   1.246 +        int_word_uint
   1.247 +        nat_transfer
   1.248 +      unfolding `?MM = 2 ^ len_of TYPE(32)`
   1.249 +      unfolding word_uint.Abs_norm
   1.250 +      by (simp add: 
   1.251 +        `a' mod ?MM = a'`
   1.252 +        `e' mod ?MM = e'`
   1.253 +        `?X mod ?MM = ?X`)
   1.254 +  qed
   1.255 +
   1.256 +  show ?thesis
   1.257 +    unfolding steps'_step[OF `0 <= j`] step_hyp[symmetric]
   1.258 +      step_both_def step_r_def step_l_def
   1.259 +    by (simp add: AL BL CL DL EL AR BR CR DR ER)
   1.260 +qed
   1.261 +
   1.262 +spark_vc procedure_round_61
   1.263 +proof -
   1.264 +  let ?M = "4294967295::int"
   1.265 +  have step_hyp:
   1.266 +  "\<lparr>left =
   1.267 +      \<lparr>h0 = ca, h1 = cb, h2 = cc,
   1.268 +         h3 = cd, h4 = ce\<rparr>,
   1.269 +      right =
   1.270 +        \<lparr>h0 = ca, h1 = cb, h2 = cc,
   1.271 +           h3 = cd, h4 = ce\<rparr>\<rparr> =
   1.272 +   steps'
   1.273 +    (\<lparr>left =
   1.274 +        \<lparr>h0 = ca, h1 = cb, h2 = cc,
   1.275 +           h3 = cd, h4 = ce\<rparr>,
   1.276 +        right =
   1.277 +          \<lparr>h0 = ca, h1 = cb, h2 = cc,
   1.278 +             h3 = cd, h4 = ce\<rparr>\<rparr>)
   1.279 +    0 x"
   1.280 +    unfolding steps_def 
   1.281 +    by (simp add:
   1.282 +      uint_word_of_int_id[OF `0 <= ca` `ca <= ?M`]
   1.283 +      uint_word_of_int_id[OF `0 <= cb` `cb <= ?M`]
   1.284 +      uint_word_of_int_id[OF `0 <= cc` `cc <= ?M`]
   1.285 +      uint_word_of_int_id[OF `0 <= cd` `cd <= ?M`]
   1.286 +      uint_word_of_int_id[OF `0 <= ce` `ce <= ?M`])
   1.287 +  let ?rotate_arg_l =
   1.288 +    "((((ca + f 0 cb cc cd) smod 4294967296 +
   1.289 +        x (r_l 0)) smod 4294967296 + k_l 0) smod 4294967296)"
   1.290 +  let ?rotate_arg_r =
   1.291 +    "((((ca + f 79 cb cc cd) smod 4294967296 +
   1.292 +        x (r_r 0)) smod 4294967296 + k_r 0) smod 4294967296)"
   1.293 +  note returns =
   1.294 +    `wordops__rotate (s_l 0) ?rotate_arg_l =
   1.295 +     rotate_left (s_l 0) ?rotate_arg_l`
   1.296 +    `wordops__rotate (s_r 0) ?rotate_arg_r =
   1.297 +     rotate_left (s_r 0) ?rotate_arg_r`
   1.298 +    `wordops__rotate 10 cc = rotate_left 10 cc`
   1.299 +    `f 0 cb cc cd = f_spec 0 cb cc cd`
   1.300 +    `f 79 cb cc cd = f_spec 79 cb cc cd`
   1.301 +    `k_l 0 = k_l_spec 0`
   1.302 +    `k_r 0 = k_r_spec 0`
   1.303 +    `r_l 0 = r_l_spec 0`
   1.304 +    `r_r 0 = r_r_spec 0`
   1.305 +    `s_l 0 = s_l_spec 0`
   1.306 +    `s_r 0 = s_r_spec 0`
   1.307 +
   1.308 +  note x_borders = `\<forall>i. 0 \<le> i \<and> i \<le> 15 \<longrightarrow> 0 \<le> x i \<and> x i \<le> ?M`
   1.309 +
   1.310 +  from `0 <= r_l 0` `r_l 0 <= 15` x_borders
   1.311 +  have "0 \<le> x (r_l 0)" by blast
   1.312 +  hence x_lower: "0 <= x (r_l_spec 0)" unfolding returns .
   1.313 +
   1.314 +  from `0 <= r_l 0` `r_l 0 <= 15` x_borders
   1.315 +  have "x (r_l 0) <= ?M" by blast
   1.316 +  hence x_upper: "x (r_l_spec 0) <= ?M" unfolding returns .
   1.317 +
   1.318 +  from `0 <= r_r 0` `r_r 0 <= 15` x_borders
   1.319 +  have "0 \<le> x (r_r 0)" by blast
   1.320 +  hence x_lower': "0 <= x (r_r_spec 0)" unfolding returns .
   1.321 +
   1.322 +  from `0 <= r_r 0` `r_r 0 <= 15` x_borders
   1.323 +  have "x (r_r 0) <= ?M" by blast
   1.324 +  hence x_upper': "x (r_r_spec 0) <= ?M" unfolding returns .
   1.325 +
   1.326 +  have "0 <= (0::int)" by simp
   1.327 +  have "0 <= (79::int)" by simp
   1.328 +  note step_from_hyp [OF
   1.329 +    step_hyp
   1.330 +    H2 H4 H6 H8 H10 H2 H4 H6 H8 H10 (* upper bounds *)
   1.331 +    H1 H3 H5 H7 H9  H1 H3 H5 H7 H9  (* lower bounds *)
   1.332 +  ]
   1.333 +  from this[OF x_lower x_upper x_lower' x_upper' `0 <= 0` `0 <= 79`]
   1.334 +    `0 \<le> ca` `0 \<le> ce` x_lower x_lower'
   1.335 +  show ?thesis unfolding returns(1) returns(2) unfolding returns
   1.336 +    by (simp add: smod_pos_pos)
   1.337 +qed
   1.338 +
   1.339 +spark_vc procedure_round_62
   1.340 +proof -
   1.341 +  let ?M = "4294967295::int"
   1.342 +  let ?rotate_arg_l =
   1.343 +    "((((cla + f (loop__1__j + 1) clb clc cld) smod 4294967296 +
   1.344 +         x (r_l (loop__1__j + 1))) smod 4294967296 +
   1.345 +         k_l (loop__1__j + 1)) smod 4294967296)"
   1.346 +  let ?rotate_arg_r =
   1.347 +    "((((cra + f (79 - (loop__1__j + 1)) crb crc crd) smod
   1.348 +         4294967296 + x (r_r (loop__1__j + 1))) smod 4294967296 +
   1.349 +         k_r (loop__1__j + 1)) smod 4294967296)"
   1.350 +
   1.351 +  have s: "78 - loop__1__j = (79 - (loop__1__j + 1))" by simp
   1.352 +  note returns =
   1.353 +    `wordops__rotate (s_l (loop__1__j + 1)) ?rotate_arg_l =
   1.354 +     rotate_left (s_l (loop__1__j + 1)) ?rotate_arg_l`
   1.355 +    `wordops__rotate (s_r (loop__1__j + 1)) ?rotate_arg_r =
   1.356 +     rotate_left (s_r (loop__1__j + 1)) ?rotate_arg_r`
   1.357 +    `f (loop__1__j + 1) clb clc cld =
   1.358 +     f_spec (loop__1__j + 1) clb clc cld`
   1.359 +    `f (78 - loop__1__j) crb crc crd =
   1.360 +     f_spec (78 - loop__1__j) crb crc crd`[simplified s]
   1.361 +    `wordops__rotate 10 clc = rotate_left 10 clc`
   1.362 +    `wordops__rotate 10 crc = rotate_left 10 crc`
   1.363 +    `k_l (loop__1__j + 1) = k_l_spec (loop__1__j + 1)`
   1.364 +    `k_r (loop__1__j + 1) = k_r_spec (loop__1__j + 1)`
   1.365 +    `r_l (loop__1__j + 1) = r_l_spec (loop__1__j + 1)`
   1.366 +    `r_r (loop__1__j + 1) = r_r_spec (loop__1__j + 1)`
   1.367 +    `s_l (loop__1__j + 1) = s_l_spec (loop__1__j + 1)`
   1.368 +    `s_r (loop__1__j + 1) = s_r_spec (loop__1__j + 1)`
   1.369 +
   1.370 +  note x_borders = `\<forall>i. 0 \<le> i \<and> i \<le> 15 \<longrightarrow> 0 \<le> x i \<and> x i \<le> ?M`
   1.371 +
   1.372 +  from `0 <= r_l (loop__1__j + 1)` `r_l (loop__1__j + 1) <= 15` x_borders
   1.373 +  have "0 \<le> x (r_l (loop__1__j + 1))" by blast
   1.374 +  hence x_lower: "0 <= x (r_l_spec (loop__1__j + 1))" unfolding returns .
   1.375 +
   1.376 +  from `0 <= r_l (loop__1__j + 1)` `r_l (loop__1__j + 1) <= 15` x_borders
   1.377 +  have "x (r_l (loop__1__j + 1)) <= ?M" by blast
   1.378 +  hence x_upper: "x (r_l_spec (loop__1__j + 1)) <= ?M" unfolding returns .
   1.379 +
   1.380 +  from `0 <= r_r (loop__1__j + 1)` `r_r (loop__1__j + 1) <= 15` x_borders
   1.381 +  have "0 \<le> x (r_r (loop__1__j + 1))" by blast
   1.382 +  hence x_lower': "0 <= x (r_r_spec (loop__1__j + 1))" unfolding returns .
   1.383 +
   1.384 +  from `0 <= r_r (loop__1__j + 1)` `r_r (loop__1__j + 1) <= 15` x_borders
   1.385 +  have "x (r_r (loop__1__j + 1)) <= ?M" by blast
   1.386 +  hence x_upper': "x (r_r_spec (loop__1__j + 1)) <= ?M" unfolding returns .
   1.387 +
   1.388 +  from `0 <= loop__1__j` have "0 <= loop__1__j + 1" by simp
   1.389 +  from `loop__1__j <= 78` have "loop__1__j + 1 <= 79" by simp
   1.390 +
   1.391 +  have "loop__1__j + 1 + 1 = loop__1__j + 2" by simp
   1.392 +
   1.393 +  note step_from_hyp[OF H1
   1.394 +    `cla <= ?M`
   1.395 +    `clb <= ?M`
   1.396 +    `clc <= ?M`
   1.397 +    `cld <= ?M`
   1.398 +    `cle <= ?M`
   1.399 +    `cra <= ?M`
   1.400 +    `crb <= ?M`
   1.401 +    `crc <= ?M`
   1.402 +    `crd <= ?M`
   1.403 +    `cre <= ?M`
   1.404 +    
   1.405 +    `0 <= cla`
   1.406 +    `0 <= clb`
   1.407 +    `0 <= clc`
   1.408 +    `0 <= cld`
   1.409 +    `0 <= cle`
   1.410 +    `0 <= cra`
   1.411 +    `0 <= crb`
   1.412 +    `0 <= crc`
   1.413 +    `0 <= crd`
   1.414 +    `0 <= cre`]
   1.415 +  from this[OF
   1.416 +    x_lower x_upper x_lower' x_upper'
   1.417 +    `0 <= loop__1__j + 1` `loop__1__j + 1 <= 79`]
   1.418 +    `0 \<le> cla` `0 \<le> cle` `0 \<le> cra` `0 \<le> cre` x_lower x_lower'
   1.419 +  show ?thesis unfolding `loop__1__j + 1 + 1 = loop__1__j + 2`
   1.420 +    unfolding returns(1) returns(2) unfolding returns
   1.421 +    by (simp add: smod_pos_pos)
   1.422 +qed
   1.423 +
   1.424 +spark_vc procedure_round_76
   1.425 +proof -
   1.426 +  let ?M = "4294967295 :: int"
   1.427 +  let ?INIT_CHAIN =
   1.428 +     "\<lparr>h0 = ca_init, h1 = cb_init,
   1.429 +         h2 = cc_init, h3 = cd_init,
   1.430 +         h4 = ce_init\<rparr>"
   1.431 +  have steps_to_steps':
   1.432 +    "steps
   1.433 +       (\<lambda>n\<Colon>nat. word_of_int (x (int n)))
   1.434 +       (from_chain ?INIT_CHAIN, from_chain ?INIT_CHAIN)
   1.435 +       80 =
   1.436 +    from_chain_pair (
   1.437 +      steps'
   1.438 +      (\<lparr>left = ?INIT_CHAIN, right = ?INIT_CHAIN\<rparr>)
   1.439 +      80
   1.440 +      x)"
   1.441 +    unfolding from_to_id by simp
   1.442 +  from
   1.443 +    `0 \<le> ca_init` `ca_init \<le> ?M`
   1.444 +    `0 \<le> cb_init` `cb_init \<le> ?M`
   1.445 +    `0 \<le> cc_init` `cc_init \<le> ?M`
   1.446 +    `0 \<le> cd_init` `cd_init \<le> ?M`
   1.447 +    `0 \<le> ce_init` `ce_init \<le> ?M`
   1.448 +    `0 \<le> cla` `cla \<le> ?M`
   1.449 +    `0 \<le> clb` `clb \<le> ?M`
   1.450 +    `0 \<le> clc` `clc \<le> ?M`
   1.451 +    `0 \<le> cld` `cld \<le> ?M`
   1.452 +    `0 \<le> cle` `cle \<le> ?M`
   1.453 +    `0 \<le> cra` `cra \<le> ?M`
   1.454 +    `0 \<le> crb` `crb \<le> ?M`
   1.455 +    `0 \<le> crc` `crc \<le> ?M`
   1.456 +    `0 \<le> crd` `crd \<le> ?M`
   1.457 +    `0 \<le> cre` `cre \<le> ?M`
   1.458 +  show ?thesis
   1.459 +    unfolding round_def
   1.460 +    unfolding steps_to_steps'
   1.461 +    unfolding H1[symmetric]
   1.462 +    by (simp add: uint_word_ariths(2) rdmods smod_pos_pos
   1.463 +      uint_word_of_int_id)
   1.464 +qed
   1.465 +
   1.466 +spark_end
   1.467 +
   1.468 +end