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.
