lemma uint_word_of_int_id: assumes"0 <= (x::int)" assumes"x <= 4294967295" shows"uint(word_of_int x::word32) = x" using assms by (simp add: take_bit_int_eq_self unsigned_of_int)
lemma steps_step: "steps X cc (Suc i) = step_both X (steps X cc i) i" unfolding steps_def by (induct i) simp_all
lemma from_to_id: "from_chain_pair (to_chain_pair CC) = CC" proof (cases CC) fix a::RMD.chain fix b c d e f::word32 assume"CC = (a, b, c, d, e, f)" thus ?thesis by (cases a) simp qed
lemma steps_to_steps': "F A (steps X cc i) B =
F A (from_chain_pair (to_chain_pair (steps X cc i))) B" unfolding from_to_id ..
lemma steps'_step: assumes"0 <= i" shows "steps' cc (i + 1) X = to_chain_pair (
step_both
(λn. word_of_int (X (int n)))
(from_chain_pair (steps' cc i X))
(nat i))" proof - have"nat (i + 1) = Suc (nat i)"using assms by simp show ?thesis unfolding‹nat (i + 1) = Suc (nat i)› steps_step steps_to_steps'
.. qed
lemma step_from_hyp: assumes
step_hyp: "\left = (h0 = a, h1 = b, h2 = c, h3 = d, h4 = e),
right = (h0 = a', h1 = b', h2 = c', h3 = d', h4 = e'\\ =
steps'
((left = (h0 = a_0, h1 = b_0, h2 = c_0,
h3 = d_0, h4 = e_0),
right = (h0 = a_0, h1 = b_0, h2 = c_0,
h3 = d_0, h4 = e_0)))
j x" assumes"a <= 4294967295" (is"_ <= ?M") assumes"b <= ?M"and"c <= ?M"and"d <= ?M"and"e <= ?M" assumes"a' <= ?M"and"b' <= ?M"and"c' <= ?M"and"d' <= ?M"and"e' <= ?M" assumes"0 <= a "and"0 <= b "and"0 <= c "and"0 <= d "and"0 <= e " assumes"0 <= a'"and"0 <= b'"and"0 <= c'"and"0 <= d'"and"0 <= e'" assumes"0 <= x (r_l_spec j)"and"x (r_l_spec j) <= ?M" assumes"0 <= x (r_r_spec j)"and"x (r_r_spec j) <= ?M" assumes"0 <= j"and"j <= 79" shows "\left = (h0 = e,
h1 =
(rotate_left (s_l_spec j)
((((a + f_spec j b c d) mod 4294967296 +
x (r_l_spec j)) mod
4294967296 +
k_l_spec j) mod
4294967296) +
e) mod
4294967296,
h2 = b, h3 = rotate_left 10 c,
h4 = d),
right = (h0 = e',
h1 =
(rotate_left (s_r_spec j)
((((a' + f_spec (79 - j) b' c' d') mod
4294967296 +
x (r_r_spec j)) mod
4294967296 +
k_r_spec j) mod
4294967296) +
e') mod
4294967296,
h2 = b', h3 = rotate_left 10 c',
h4 = d'\\ =
steps'
((left = (h0 = a_0, h1 = b_0, h2 = c_0,
h3 = d_0, h4 = e_0),
right = (h0 = a_0, h1 = b_0, h2 = c_0,
h3 = d_0, h4 = e_0)))
(j + 1) x" using step_hyp proof - let ?MM = 4294967296 have AL: "uint(word_of_int e::word32) = e" by (rule uint_word_of_int_id[OF ‹0 <= e›‹e <= ?M›]) have CL: "uint(word_of_int b::word32) = b" by (rule uint_word_of_int_id[OF ‹0 <= b›‹b <= ?M›]) have DL: "True" .. have EL: "uint(word_of_int d::word32) = d" by (rule uint_word_of_int_id[OF ‹0 <= d›‹d <= ?M›]) have AR: "uint(word_of_int e'::word32) = e'" by (rule uint_word_of_int_id[OF ‹0 <= e'\ \e' <= ?M›]) have CR: "uint(word_of_int b'::word32) = b'" by (rule uint_word_of_int_id[OF ‹0 <= b'\ \b' <= ?M›]) have DR: "True" .. have ER: "uint(word_of_int d'::word32) = d'" by (rule uint_word_of_int_id[OF ‹0 <= d'\ \d' <= ?M›]) have BL: "(uint
(word_rotl (s (nat j))
((word_of_int::int==>word32)
((((a + f_spec j b c d) mod ?MM +
x (r_l_spec j)) mod ?MM +
k_l_spec j) mod ?MM))) +
e) mod ?MM
=
uint
(word_rotl (s (nat j))
(word_of_int a +
f (nat j) (word_of_int b)
(word_of_int c) (word_of_int d) +
word_of_int (x (r_l_spec j)) +
K (nat j)) +
word_of_int e)"
(is"(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _") proof - have"a mod ?MM = a"using‹0 <= a›‹a <= ?M› by simp have"?X mod ?MM = ?X"using‹0 <= ?X›‹?X <= ?M› by simp have"e mod ?MM = e"using‹0 <= e›‹e <= ?M› by simp have"(?MM::int) = 2 ^ LENGTH(32)"by simp show ?thesis unfolding
word_add_def
uint_word_of_int_id[OF ‹0 <= a›‹a <= ?M›]
uint_word_of_int_id[OF ‹0 <= ?X›‹?X <= ?M›] using‹a mod ?MM = a› ‹e mod ?MM = e› ‹?X mod ?MM = ?X› unfolding‹?MM = 2 ^ LENGTH(32)› apply (simp only: flip: take_bit_eq_mod add: uint_word_of_int_eq) apply (metis (mono_tags, opaque_lifting) of_int_of_nat_eq ucast_id uint_word_of_int_eq unsigned_of_int) done qed
have BR: "(uint
(word_rotl (s' (nat j))
((word_of_int::int==>word32)
((((a' + f_spec (79 - j) b' c' d') mod ?MM +
x (r_r_spec j)) mod ?MM +
k_r_spec j) mod ?MM))) +
e') mod ?MM
=
uint
(word_rotl (s' (nat j))
(word_of_int a' +
f (79 - nat j) (word_of_int b')
(word_of_int c') (word_of_int d') +
word_of_int (x (r_r_spec j)) +
K' (nat j)) +
word_of_int e')"
(is"(uint (word_rotl _ (_ ((((_ + ?F) mod _ + ?X) mod _ + _) mod _))) + _) mod _ = _") proof - have"a' mod ?MM = a'"using‹0 <= a'\ \a' <= ?M› by simp have"?X mod ?MM = ?X"using‹0 <= ?X›‹?X <= ?M› by simp have"e' mod ?MM = e'"using‹0 <= e'\ \e' <= ?M› by simp have"(?MM::int) = 2 ^ LENGTH(32)"by simp have nat_transfer: "79 - nat j = nat (79 - j)" using nat_diff_distrib ‹0 <= j›‹j <= 79› by simp show ?thesis unfolding
word_add_def
uint_word_of_int_id[OF ‹0 <= a'\ \a' <= ?M›]
uint_word_of_int_id[OF ‹0 <= ?X›‹?X <= ?M›]
nat_transfer using‹a' mod ?MM = a'› ‹e' mod ?MM = e'› ‹?X mod ?MM = ?X› unfolding‹?MM = 2 ^ LENGTH(32)› apply (simp only: flip: take_bit_eq_mod add: uint_word_of_int_eq) apply (metis (mono_tags, opaque_lifting) of_nat_nat_take_bit_eq ucast_id unsigned_of_int) done qed
show ?thesis unfolding steps'_step[OF \0 <= j\] step_hyp[symmetric]
step_both_def step_r_def step_l_def using AL CL EL AR CR ER by (simp add: BL DL BR DR take_bit_int_eq_self_iff take_bit_int_eq_self) qed
spark_vc procedure_round_61 proof - let ?M = "4294967295::int" have step_hyp: "\left = (h0 = ca, h1 = cb, h2 = cc,
h3 = cd, h4 = ce),
right = (h0 = ca, h1 = cb, h2 = cc,
h3 = cd, h4 = ce)) =
steps'
((left = (h0 = ca, h1 = cb, h2 = cc,
h3 = cd, h4 = ce),
right = (h0 = ca, h1 = cb, h2 = cc,
h3 = cd, h4 = ce)))
0 x" unfolding steps_def using
uint_word_of_int_id[OF ‹0 <= ca›‹ca <= ?M›]
uint_word_of_int_id[OF ‹0 <= cb›‹cb <= ?M›]
uint_word_of_int_id[OF ‹0 <= cc›‹cc <= ?M›]
uint_word_of_int_id[OF ‹0 <= cd›‹cd <= ?M›]
uint_word_of_int_id[OF ‹0 <= ce›‹ce <= ?M›] by (simp add: take_bit_int_eq_self_iff take_bit_int_eq_self) let ?rotate_arg_l = "((((ca + f 0 cb cc cd) mod 4294967296 +
x (r_l 0)) mod 4294967296 + k_l 0) mod 4294967296)" let ?rotate_arg_r = "((((ca + f 79 cb cc cd) mod 4294967296 +
x (r_r 0)) mod 4294967296 + k_r 0) mod 4294967296)" note returns = ‹wordops__rotate (s_l 0) ?rotate_arg_l =
rotate_left (s_l 0) ?rotate_arg_l› ‹wordops__rotate (s_r 0) ?rotate_arg_r =
rotate_left (s_r 0) ?rotate_arg_r› ‹wordops__rotate 10 cc = rotate_left 10 cc› ‹f 0 cb cc cd = f_spec 0 cb cc cd› ‹f 79 cb cc cd = f_spec 79 cb cc cd› ‹k_l 0 = k_l_spec 0› ‹k_r 0 = k_r_spec 0› ‹r_l 0 = r_l_spec 0› ‹r_r 0 = r_r_spec 0› ‹s_l 0 = s_l_spec 0› ‹s_r 0 = s_r_spec 0›
note x_borders = ‹∀i. 0 ≤ i ∧ i ≤ 15 ⟶ 0 ≤ x i ∧ x i ≤ ?M›
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
