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