# HG changeset patch # User berghofe # Date 1295091329 -3600 # Node ID d1318f3c86bab2689f893358e9d6c3be8922ab3e # Parent 236cd8f07f7b9830aa678fbbf85ddd23946860de Added new SPARK verification environment. diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Gcd/Gcd.adb --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Gcd/Gcd.adb Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,17 @@ +package body Greatest_Common_Divisor +is + + procedure G_C_D(M, N: in Natural; G: out Natural) + is + C, D, R: Integer; + begin + C := M; D := N; + while D /= 0 loop + --# assert C >= 0 and D > 0 and Gcd(C, D) = Gcd(M, N); + R := C rem D; + C := D; D := R; + end loop; + G := C; + end G_C_D; + +end Greatest_Common_Divisor; diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Gcd/Gcd.ads --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Gcd/Gcd.ads Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,11 @@ +package Greatest_Common_Divisor +is + + --# function Gcd(A, B: Natural) return Natural; + + procedure G_C_D(M, N: in Natural; G: out Natural); + --# derives G from M, N; + --# pre M >= 0 and N > 0; + --# post G = Gcd(M,N); + +end Greatest_Common_Divisor; diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,36 @@ +(* Title: HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy + Author: Stefan Berghofer + Copyright: secunet Security Networks AG +*) + +theory Greatest_Common_Divisor +imports SPARK GCD +begin + +spark_proof_functions + gcd = "gcd :: int \ int \ int" + +spark_open "greatest_common_divisor/g_c_d.siv" + +spark_vc procedure_g_c_d_4 +proof - + from `0 < d` have "0 \ c mod d" by (rule pos_mod_sign) + with `0 \ c` `0 < d` `c - c sdiv d * d \ 0` show ?C1 + by (simp add: sdiv_pos_pos zmod_zdiv_equality') +next + from `0 \ c` `0 < d` `gcd c d = gcd m n` show ?C2 + by (simp add: sdiv_pos_pos zmod_zdiv_equality' gcd_non_0_int) +qed + +spark_vc procedure_g_c_d_11 +proof - + from `0 \ c` `0 < d` `c - c sdiv d * d = 0` + have "d dvd c" + by (auto simp add: sdiv_pos_pos dvd_def mult_ac) + with `0 < d` `gcd c d = gcd m n` show ?C1 + by simp +qed + +spark_end + +end diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.fdl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.fdl Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,32 @@ + {*******************************************************} + {FDL Declarations} + {Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039} + {Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.} + {*******************************************************} + + + {DATE : 29-NOV-2010 14:30:10.98} + + {procedure Greatest_Common_Divisor.G_C_D} + + +title procedure g_c_d; + + function round__(real) : integer; + const natural__base__first : integer = pending; + const natural__base__last : integer = pending; + const integer__base__first : integer = pending; + const integer__base__last : integer = pending; + const natural__first : integer = pending; + const natural__last : integer = pending; + const natural__size : integer = pending; + const integer__first : integer = pending; + const integer__last : integer = pending; + const integer__size : integer = pending; + var m : integer; + var n : integer; + var c : integer; + var d : integer; + function gcd(integer, integer) : integer; + +end; diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,27 @@ + /*********************************************************/ + /*Proof Rule Declarations*/ + /*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/ + /*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/ + /*********************************************************/ + + + /*DATE : 29-NOV-2010 14:30:10.98*/ + + /*procedure Greatest_Common_Divisor.G_C_D*/ + + +rule_family g_c_d_rules: + X requires [X:any] & + X <= Y requires [X:ire, Y:ire] & + X >= Y requires [X:ire, Y:ire]. + +g_c_d_rules(1): integer__size >= 0 may_be_deduced. +g_c_d_rules(2): integer__first may_be_replaced_by -2147483648. +g_c_d_rules(3): integer__last may_be_replaced_by 2147483647. +g_c_d_rules(4): integer__base__first may_be_replaced_by -2147483648. +g_c_d_rules(5): integer__base__last may_be_replaced_by 2147483647. +g_c_d_rules(6): natural__size >= 0 may_be_deduced. +g_c_d_rules(7): natural__first may_be_replaced_by 0. +g_c_d_rules(8): natural__last may_be_replaced_by 2147483647. +g_c_d_rules(9): natural__base__first may_be_replaced_by -2147483648. +g_c_d_rules(10): natural__base__last may_be_replaced_by 2147483647. diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,117 @@ +***************************************************************************** + Semantic Analysis of SPARK Text + Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039 + Copyright (C) 2010 Altran Praxis Limited, Bath, U.K. +***************************************************************************** + + +CREATED 29-NOV-2010, 14:30:10 SIMPLIFIED 29-NOV-2010, 14:30:11 + +SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039 +Copyright (C) 2010 Altran Praxis Limited, Bath, U.K. + +procedure Greatest_Common_Divisor.G_C_D + + + + +For path(s) from start to run-time check associated with statement of line 8: + +procedure_g_c_d_1. +*** true . /* all conclusions proved */ + + +For path(s) from start to run-time check associated with statement of line 8: + +procedure_g_c_d_2. +*** true . /* all conclusions proved */ + + +For path(s) from start to assertion of line 10: + +procedure_g_c_d_3. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 10 to assertion of line 10: + +procedure_g_c_d_4. +H1: c >= 0 . +H2: d > 0 . +H3: gcd(c, d) = gcd(m, n) . +H4: m >= 0 . +H5: m <= 2147483647 . +H6: n <= 2147483647 . +H7: n > 0 . +H8: c <= 2147483647 . +H9: d <= 2147483647 . +H10: c - c div d * d >= - 2147483648 . +H11: c - c div d * d <= 2147483647 . +H12: c - c div d * d <> 0 . +H13: integer__size >= 0 . +H14: natural__size >= 0 . + -> +C1: c - c div d * d > 0 . +C2: gcd(d, c - c div d * d) = gcd(m, n) . + + +For path(s) from assertion of line 10 to run-time check associated with + statement of line 11: + +procedure_g_c_d_5. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 10 to run-time check associated with + statement of line 12: + +procedure_g_c_d_6. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 10 to run-time check associated with + statement of line 12: + +procedure_g_c_d_7. +*** true . /* all conclusions proved */ + + +For path(s) from start to run-time check associated with statement of line 14: + +procedure_g_c_d_8. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 10 to run-time check associated with + statement of line 14: + +procedure_g_c_d_9. +*** true . /* all conclusions proved */ + + +For path(s) from start to finish: + +procedure_g_c_d_10. +*** true . /* contradiction within hypotheses. */ + + + +For path(s) from assertion of line 10 to finish: + +procedure_g_c_d_11. +H1: c >= 0 . +H2: d > 0 . +H3: gcd(c, d) = gcd(m, n) . +H4: m >= 0 . +H5: m <= 2147483647 . +H6: n <= 2147483647 . +H7: n > 0 . +H8: c <= 2147483647 . +H9: d <= 2147483647 . +H10: c - c div d * d = 0 . +H11: integer__size >= 0 . +H12: natural__size >= 0 . + -> +C1: d = gcd(m, n) . + + diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Liseq/Liseq.adb --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Liseq/Liseq.adb Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,55 @@ +------------------------------------------------------------------------------- +-- Longest increasing subsequence of an array of integers +------------------------------------------------------------------------------- + +package body Liseq is + + procedure Liseq_length(A: in Vector; L: in out Vector; maxi: out Integer) + is + maxj,i,j,pmax : Integer; + begin + L(0) := 1; + pmax := 0; + maxi := 1; + i := 1; + while i <= L'Last + --# assert + --# (for all i2 in Integer range 0 .. i-1 => + --# (L(i2) = Liseq_ends_at(A, i2))) and + --# L(pmax) = maxi and L(pmax) = Liseq_prfx(A, i) and + --# 0 <= i and i <= L'Last+1 and 0 <= pmax and pmax < i and + --# A'First = 0 and L'First = 0 and A'Last = L'Last and A'Last < Integer'Last; + loop + if A(i) < A(pmax) then + maxj := 0; + j := 0; + while j < i + --# assert + --# (for all i2 in Integer range 0 .. i-1 => + --# (L(i2) = Liseq_ends_at(A, i2))) and + --# L(pmax) = maxi and L(pmax) = Liseq_prfx(A, I) and + --# 0 <= i and i <= L'Last and 0 <= pmax and pmax < i and + --# 0 <= j and j <= i and + --# maxj = Max_ext (A, i, j) and + --# A'First = 0 and L'First = 0 and A'Last = L'Last and A'Last < Integer'Last; + loop + if (A(j) <= A(i) and + maxj < L(j)) then + maxj := L(j); + end if; + j := j+1; + end loop; + L(i) := maxj+1; + if L(i) > maxi then + maxi := maxi+1; + pmax := i; + end if; + else + maxi := maxi+1; + L(i) := maxi; + pmax := i; + end if; + i := i+1; + end loop; + end Liseq_length; +end Liseq; diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Liseq/Liseq.ads --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Liseq/Liseq.ads Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,18 @@ +------------------------------------------------------------------------------- +-- Longest increasing subsequence of an array of integers +------------------------------------------------------------------------------- + +package Liseq is + + type Vector is array (Integer range <>) of Integer; + + --# function Liseq_prfx(A: Vector; i: Integer) return Integer; + --# function Liseq_ends_at(A: Vector; i: Integer) return Integer; + --# function Max_ext(A: Vector; i, j: Integer) return Integer; + + procedure Liseq_length(A: in Vector; L: in out Vector; maxi: out Integer); + --# derives maxi, L from A, L; + --# pre A'First = 0 and L'First = 0 and A'Last = L'Last and A'Last < Integer'Last; + --# post maxi = Liseq_prfx (A, A'Last+1); + +end Liseq; diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,665 @@ +(* Title: HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy + Author: Stefan Berghofer + Copyright: secunet Security Networks AG +*) + +theory Longest_Increasing_Subsequence +imports SPARK +begin + +text {* +Set of all increasing subsequences in a prefix of an array +*} + +definition iseq :: "(nat \ 'a::linorder) \ nat \ nat set set" where + "iseq xs l = {is. (\i\is. i < l) \ + (\i\is. \j\is. i \ j \ xs i \ xs j)}" + +text {* +Length of longest increasing subsequence in a prefix of an array +*} + +definition liseq :: "(nat \ 'a::linorder) \ nat \ nat" where + "liseq xs i = Max (card ` iseq xs i)" + +text {* +Length of longest increasing subsequence ending at a particular position +*} + +definition liseq' :: "(nat \ 'a::linorder) \ nat \ nat" where + "liseq' xs i = Max (card ` (iseq xs (Suc i) \ {is. Max is = i}))" + +lemma iseq_finite: "finite (iseq xs i)" + apply (simp add: iseq_def) + apply (rule finite_subset [OF _ + finite_Collect_subsets [of "{j. j < i}"]]) + apply auto + done + +lemma iseq_finite': "is \ iseq xs i \ finite is" + by (auto simp add: iseq_def bounded_nat_set_is_finite) + +lemma iseq_singleton: "i < l \ {i} \ iseq xs l" + by (simp add: iseq_def) + +lemma iseq_trivial: "{} \ iseq xs i" + by (simp add: iseq_def) + +lemma iseq_nonempty: "iseq xs i \ {}" + by (auto intro: iseq_trivial) + +lemma liseq'_ge1: "1 \ liseq' xs x" + apply (simp add: liseq'_def) + apply (subgoal_tac "iseq xs (Suc x) \ {is. Max is = x} \ {}") + apply (simp add: Max_ge_iff iseq_finite) + apply (rule_tac x="{x}" in bexI) + apply (auto intro: iseq_singleton) + done + +lemma liseq_expand: + assumes R: "\is. liseq xs i = card is \ is \ iseq xs i \ + (\js. js \ iseq xs i \ card js \ card is) \ P" + shows "P" +proof - + have "Max (card ` iseq xs i) \ card ` iseq xs i" + by (rule Max_in) (simp_all add: iseq_finite iseq_nonempty) + then obtain js where js: "liseq xs i = card js" and "js \ iseq xs i" + by (rule imageE) (simp add: liseq_def) + moreover { + fix js' + assume "js' \ iseq xs i" + then have "card js' \ card js" + by (simp add: js [symmetric] liseq_def iseq_finite iseq_trivial) + } + ultimately show ?thesis by (rule R) +qed + +lemma liseq'_expand: + assumes R: "\is. liseq' xs i = card is \ is \ iseq xs (Suc i) \ + finite is \ Max is = i \ + (\js. js \ iseq xs (Suc i) \ Max js = i \ card js \ card is) \ + is \ {} \ P" + shows "P" +proof - + have "Max (card ` (iseq xs (Suc i) \ {is. Max is = i})) \ + card ` (iseq xs (Suc i) \ {is. Max is = i})" + by (auto simp add: iseq_finite intro!: iseq_singleton Max_in) + then obtain js where js: "liseq' xs i = card js" and "js \ iseq xs (Suc i)" + and "finite js" and "Max js = i" + by (auto simp add: liseq'_def intro: iseq_finite') + moreover { + fix js' + assume "js' \ iseq xs (Suc i)" "Max js' = i" + then have "card js' \ card js" + by (auto simp add: js [symmetric] liseq'_def iseq_finite intro!: iseq_singleton) + } + note max = this + moreover have "card {i} \ card js" + by (rule max) (simp_all add: iseq_singleton) + then have "js \ {}" by auto + ultimately show ?thesis by (rule R) +qed + +lemma liseq'_ge: + "j = card js \ js \ iseq xs (Suc i) \ Max js = i \ + js \ {} \ j \ liseq' xs i" + by (simp add: liseq'_def iseq_finite) + +lemma liseq'_eq: + "j = card js \ js \ iseq xs (Suc i) \ Max js = i \ + js \ {} \ (\js'. js' \ iseq xs (Suc i) \ Max js' = i \ finite js' \ + js' \ {} \ card js' \ card js) \ + j = liseq' xs i" + by (fastsimp simp add: liseq'_def iseq_finite + intro: Max_eqI [symmetric]) + +lemma liseq_ge: + "j = card js \ js \ iseq xs i \ j \ liseq xs i" + by (auto simp add: liseq_def iseq_finite) + +lemma liseq_eq: + "j = card js \ js \ iseq xs i \ + (\js'. js' \ iseq xs i \ finite js' \ + js' \ {} \ card js' \ card js) \ + j = liseq xs i" + by (fastsimp simp add: liseq_def iseq_finite + intro: Max_eqI [symmetric]) + +lemma max_notin: "finite xs \ Max xs < x \ x \ xs" + by (cases "xs = {}") auto + +lemma iseq_insert: + "xs (Max is) \ xs i \ is \ iseq xs i \ + is \ {i} \ iseq xs (Suc i)" + apply (frule iseq_finite') + apply (cases "is = {}") + apply (auto simp add: iseq_def) + apply (rule order_trans [of _ "xs (Max is)"]) + apply auto + apply (thin_tac "\a\is. a < i") + apply (drule_tac x=ia in bspec) + apply assumption + apply (drule_tac x="Max is" in bspec) + apply (auto intro: Max_in) + done + +lemma iseq_diff: "is \ iseq xs (Suc (Max is)) \ + is - {Max is} \ iseq xs (Suc (Max (is - {Max is})))" + apply (frule iseq_finite') + apply (simp add: iseq_def less_Suc_eq_le) + done + +lemma iseq_butlast: + assumes "js \ iseq xs (Suc i)" and "js \ {}" + and "Max js \ i" + shows "js \ iseq xs i" +proof - + from assms have fin: "finite js" + by (simp add: iseq_finite') + with assms have "Max js \ js" + by auto + with assms have "Max js < i" + by (auto simp add: iseq_def) + with fin assms have "\j\js. j < i" + by (simp add: Max_less_iff) + with assms show ?thesis + by (simp add: iseq_def) +qed + +lemma iseq_mono: "is \ iseq xs i \ i \ j \ is \ iseq xs j" + by (auto simp add: iseq_def) + +lemma diff_nonempty: + assumes "1 < card is" + shows "is - {i} \ {}" +proof - + from assms have fin: "finite is" by (auto intro: card_ge_0_finite) + with assms fin have "card is - 1 \ card (is - {i})" + by (simp add: card_Diff_singleton_if) + with assms have "0 < card (is - {i})" by simp + then show ?thesis by (simp add: card_gt_0_iff) +qed + +lemma Max_diff: + assumes "1 < card is" + shows "Max (is - {Max is}) < Max is" +proof - + from assms have "finite is" by (auto intro: card_ge_0_finite) + moreover from assms have "is - {Max is} \ {}" + by (rule diff_nonempty) + ultimately show ?thesis using assms + apply (auto simp add: not_less) + apply (subgoal_tac "a \ Max is") + apply auto + done +qed + +lemma iseq_nth: "js \ iseq xs l \ 1 < card js \ + xs (Max (js - {Max js})) \ xs (Max js)" + apply (auto simp add: iseq_def) + apply (subgoal_tac "Max (js - {Max js}) \ js") + apply (thin_tac "\i\js. i < l") + apply (drule_tac x="Max (js - {Max js})" in bspec) + apply assumption + apply (drule_tac x="Max js" in bspec) + using card_gt_0_iff [of js] + apply simp + using Max_diff [of js] + apply simp + using Max_in [of "js - {Max js}", OF _ diff_nonempty] card_gt_0_iff [of js] + apply auto + done + +lemma card_leq1_singleton: + assumes "finite xs" "xs \ {}" "card xs \ 1" + obtains x where "xs = {x}" + using assms + by induct simp_all + +lemma longest_iseq1: + "liseq' xs i = + Max ({0} \ {liseq' xs j |j. j < i \ xs j \ xs i}) + 1" +proof - + have "Max ({0} \ {liseq' xs j |j. j < i \ xs j \ xs i}) = liseq' xs i - 1" + proof (rule Max_eqI) + fix y + assume "y \ {0} \ {liseq' xs j |j. j < i \ xs j \ xs i}" + then show "y \ liseq' xs i - 1" + proof + assume "y \ {liseq' xs j |j. j < i \ xs j \ xs i}" + then obtain j where j: "j < i" "xs j \ xs i" "y = liseq' xs j" + by auto + have "liseq' xs j + 1 \ liseq' xs i" + proof (rule liseq'_expand) + fix "is" + assume H: "liseq' xs j = card is" "is \ iseq xs (Suc j)" + "finite is" "Max is = j" "is \ {}" + from H j have "card is + 1 = card (is \ {i})" + by (simp add: card_insert max_notin) + moreover { + from H j have "xs (Max is) \ xs i" by simp + moreover from `j < i` have "Suc j \ i" by simp + with `is \ iseq xs (Suc j)` have "is \ iseq xs i" + by (rule iseq_mono) + ultimately have "is \ {i} \ iseq xs (Suc i)" + by (rule iseq_insert) + } moreover from H j have "Max (is \ {i}) = i" by simp + moreover have "is \ {i} \ {}" by simp + ultimately have "card is + 1 \ liseq' xs i" + by (rule liseq'_ge) + with H show ?thesis by simp + qed + with j show "y \ liseq' xs i - 1" + by simp + qed simp + next + have "liseq' xs i \ 1 \ + (\j. liseq' xs i - 1 = liseq' xs j \ j < i \ xs j \ xs i)" + proof (rule liseq'_expand) + fix "is" + assume H: "liseq' xs i = card is" "is \ iseq xs (Suc i)" + "finite is" "Max is = i" "is \ {}" + assume R: "\js. js \ iseq xs (Suc i) \ Max js = i \ + card js \ card is" + show ?thesis + proof (cases "card is \ 1") + case True with H show ?thesis by simp + next + case False + then have "1 < card is" by simp + then have "Max (is - {Max is}) < Max is" + by (rule Max_diff) + from `is \ iseq xs (Suc i)` `1 < card is` + have "xs (Max (is - {Max is})) \ xs (Max is)" + by (rule iseq_nth) + have "card is - 1 = liseq' xs (Max (is - {i}))" + proof (rule liseq'_eq) + from `Max is = i` [symmetric] `finite is` `is \ {}` + show "card is - 1 = card (is - {i})" by simp + next + from `is \ iseq xs (Suc i)` `Max is = i` [symmetric] + show "is - {i} \ iseq xs (Suc (Max (is - {i})))" + by simp (rule iseq_diff) + next + from `1 < card is` + show "is - {i} \ {}" by (rule diff_nonempty) + next + fix js + assume "js \ iseq xs (Suc (Max (is - {i})))" + "Max js = Max (is - {i})" "finite js" "js \ {}" + from `xs (Max (is - {Max is})) \ xs (Max is)` + `Max js = Max (is - {i})` `Max is = i` + have "xs (Max js) \ xs i" by simp + moreover from `Max is = i` `Max (is - {Max is}) < Max is` + have "Suc (Max (is - {i})) \ i" + by simp + with `js \ iseq xs (Suc (Max (is - {i})))` + have "js \ iseq xs i" + by (rule iseq_mono) + ultimately have "js \ {i} \ iseq xs (Suc i)" + by (rule iseq_insert) + moreover from `js \ {}` `finite js` `Max js = Max (is - {i})` + `Max is = i` [symmetric] `Max (is - {Max is}) < Max is` + have "Max (js \ {i}) = i" + by simp + ultimately have "card (js \ {i}) \ card is" by (rule R) + moreover from `Max is = i` [symmetric] `finite js` + `Max (is - {Max is}) < Max is` `Max js = Max (is - {i})` + have "i \ js" by (simp add: max_notin) + with `finite js` + have "card (js \ {i}) = card ((js \ {i}) - {i}) + 1" + by simp + ultimately show "card js \ card (is - {i})" + using `i \ js` `Max is = i` [symmetric] `is \ {}` `finite is` + by simp + qed simp + with H `Max (is - {Max is}) < Max is` + `xs (Max (is - {Max is})) \ xs (Max is)` + show ?thesis by auto + qed + qed + then show "liseq' xs i - 1 \ {0} \ + {liseq' xs j |j. j < i \ xs j \ xs i}" by simp + qed simp + moreover have "1 \ liseq' xs i" by (rule liseq'_ge1) + ultimately show ?thesis by simp +qed + +lemma longest_iseq2': "liseq xs i < liseq' xs i \ + liseq xs (Suc i) = liseq' xs i" + apply (rule_tac xs=xs and i=i in liseq'_expand) + apply simp + apply (rule liseq_eq [symmetric]) + apply (rule refl) + apply assumption + apply (case_tac "Max js' = i") + apply simp + apply (drule_tac js=js' in iseq_butlast) + apply assumption+ + apply (drule_tac js=js' in liseq_ge [OF refl]) + apply simp + done + +lemma longest_iseq2: "liseq xs i < liseq' xs i \ + liseq xs i + 1 = liseq' xs i" + apply (rule_tac xs=xs and i=i in liseq'_expand) + apply simp + apply (rule_tac xs=xs and i=i in liseq_expand) + apply (drule_tac s="Max is" in sym) + apply simp + apply (case_tac "card is \ 1") + apply simp + apply (drule iseq_diff) + apply (drule_tac i="Suc (Max (is - {Max is}))" and j="Max is" in iseq_mono) + apply (simp add: less_eq_Suc_le [symmetric]) + apply (rule Max_diff) + apply simp + apply (drule_tac x="is - {Max is}" in meta_spec, + drule meta_mp, assumption) + apply simp + done + +lemma longest_iseq3: + "liseq xs j = liseq' xs i \ xs i \ xs j \ i < j \ + liseq xs (Suc j) = liseq xs j + 1" + apply (rule_tac xs=xs and i=j in liseq_expand) + apply simp + apply (rule_tac xs=xs and i=i in liseq'_expand) + apply simp + apply (rule_tac js="isa \ {j}" in liseq_eq [symmetric]) + apply (simp add: card_insert card_Diff_singleton_if max_notin) + apply (rule iseq_insert) + apply simp + apply (erule iseq_mono) + apply simp + apply (case_tac "j = Max js'") + apply simp + apply (drule iseq_diff) + apply (drule_tac x="js' - {j}" in meta_spec) + apply (drule meta_mp) + apply simp + apply (case_tac "card js' \ 1") + apply (erule_tac xs=js' in card_leq1_singleton) + apply assumption+ + apply (simp add: iseq_trivial) + apply (erule iseq_mono) + apply (simp add: less_eq_Suc_le [symmetric]) + apply (rule Max_diff) + apply simp + apply (rule le_diff_iff [THEN iffD1, of 1]) + apply (simp add: card_0_eq [symmetric] del: card_0_eq) + apply (simp add: card_insert) + apply (subgoal_tac "card (js' - {j}) = card js' - 1") + apply (simp add: card_insert card_Diff_singleton_if max_notin) + apply (frule_tac A=js' in Max_in) + apply assumption + apply (simp add: card_Diff_singleton_if) + apply (drule_tac js=js' in iseq_butlast) + apply assumption + apply (erule not_sym) + apply (drule_tac x=js' in meta_spec) + apply (drule meta_mp) + apply assumption + apply (simp add: card_insert_disjoint max_notin) + done + +lemma longest_iseq4: + "liseq xs j = liseq' xs i \ xs i \ xs j \ i < j \ + liseq' xs j = liseq' xs i + 1" + apply (rule_tac xs=xs and i=j in liseq_expand) + apply simp + apply (rule_tac xs=xs and i=i in liseq'_expand) + apply simp + apply (rule_tac js="isa \ {j}" in liseq'_eq [symmetric]) + apply (simp add: card_insert card_Diff_singleton_if max_notin) + apply (rule iseq_insert) + apply simp + apply (erule iseq_mono) + apply simp + apply simp + apply simp + apply (drule_tac s="Max js'" in sym) + apply simp + apply (drule iseq_diff) + apply (drule_tac x="js' - {j}" in meta_spec) + apply (drule meta_mp) + apply simp + apply (case_tac "card js' \ 1") + apply (erule_tac xs=js' in card_leq1_singleton) + apply assumption+ + apply (simp add: iseq_trivial) + apply (erule iseq_mono) + apply (simp add: less_eq_Suc_le [symmetric]) + apply (rule Max_diff) + apply simp + apply (rule le_diff_iff [THEN iffD1, of 1]) + apply (simp add: card_0_eq [symmetric] del: card_0_eq) + apply (simp add: card_insert) + apply (subgoal_tac "card (js' - {j}) = card js' - 1") + apply (simp add: card_insert card_Diff_singleton_if max_notin) + apply (frule_tac A=js' in Max_in) + apply assumption + apply (simp add: card_Diff_singleton_if) + done + +lemma longest_iseq5: "liseq' xs i \ liseq xs i \ + liseq xs (Suc i) = liseq xs i" + apply (rule_tac i=i and xs=xs in liseq'_expand) + apply simp + apply (rule_tac xs=xs and i=i in liseq_expand) + apply simp + apply (rule liseq_eq [symmetric]) + apply (rule refl) + apply (erule iseq_mono) + apply simp + apply (case_tac "Max js' = i") + apply (drule_tac x=js' in meta_spec) + apply simp + apply (drule iseq_butlast, assumption, assumption) + apply simp + done + +lemma liseq_empty: "liseq xs 0 = 0" + apply (rule_tac js="{}" in liseq_eq [symmetric]) + apply simp + apply (rule iseq_trivial) + apply (simp add: iseq_def) + done + +lemma liseq'_singleton: "liseq' xs 0 = 1" + by (simp add: longest_iseq1 [of _ 0]) + +lemma liseq_singleton: "liseq xs (Suc 0) = Suc 0" + by (simp add: longest_iseq2' liseq_empty liseq'_singleton) + +lemma liseq'_Suc_unfold: + "A j \ x \ + (insert 0 {liseq' A j' |j'. j' < Suc j \ A j' \ x}) = + (insert 0 {liseq' A j' |j'. j' < j \ A j' \ x}) \ + {liseq' A j}" + by (auto simp add: less_Suc_eq) + +lemma liseq'_Suc_unfold': + "\ (A j \ x) \ + {liseq' A j' |j'. j' < Suc j \ A j' \ x} = + {liseq' A j' |j'. j' < j \ A j' \ x}" + by (auto simp add: less_Suc_eq) + +lemma iseq_card_limit: + assumes "is \ iseq A i" + shows "card is \ i" +proof - + from assms have "is \ {0.. card {0.. i" + by (rule_tac xs=A and i=i in liseq_expand) + (simp add: iseq_card_limit) + +lemma liseq'_limit: "liseq' A i \ i + 1" + by (rule_tac xs=A and i=i in liseq'_expand) + (simp add: iseq_card_limit) + +definition max_ext :: "(nat \ 'a::linorder) \ nat \ nat \ nat" where + "max_ext A i j = Max ({0} \ {liseq' A j' |j'. j' < j \ A j' \ A i})" + +lemma max_ext_limit: "max_ext A i j \ j" + apply (auto simp add: max_ext_def) + apply (drule Suc_leI) + apply (cut_tac i=j' and A=A in liseq'_limit) + apply simp + done + + +text {* Proof functions *} + +abbreviation (input) + "arr_conv a \ (\n. a (int n))" + +lemma idx_conv_suc: + "0 \ i \ nat (i + 1) = nat i + 1" + by simp + +abbreviation liseq_ends_at' :: "(int \ 'a::linorder) \ int \ int" where + "liseq_ends_at' A i \ int (liseq' (\l. A (int l)) (nat i))" + +abbreviation liseq_prfx' :: "(int \ 'a::linorder) \ int \ int" where + "liseq_prfx' A i \ int (liseq (\l. A (int l)) (nat i))" + +abbreviation max_ext' :: "(int \ 'a::linorder) \ int \ int \ int" where + "max_ext' A i j \ int (max_ext (\l. A (int l)) (nat i) (nat j))" + +spark_proof_functions + liseq_ends_at = "liseq_ends_at' :: (int \ int) \ int \ int" + liseq_prfx = "liseq_prfx' :: (int \ int) \ int \ int" + max_ext = "max_ext' :: (int \ int) \ int \ int \ int" + + +text {* The verification conditions *} + +spark_open "liseq/liseq_length.siv" + +spark_vc procedure_liseq_length_5 + by (simp_all add: liseq_singleton liseq'_singleton) + +spark_vc procedure_liseq_length_6 +proof - + from H1 H2 H3 H4 + have eq: "liseq (arr_conv a) (nat i) = + liseq' (arr_conv a) (nat pmax)" + by simp + from H14 H3 H4 + have pmax1: "arr_conv a (nat pmax) \ arr_conv a (nat i)" + by simp + from H3 H4 have pmax2: "nat pmax < nat i" + by simp + { + fix i2 + assume i2: "0 \ i2" "i2 \ i" + have "(l(i := l pmax + 1)) i2 = + int (liseq' (arr_conv a) (nat i2))" + proof (cases "i2 = i") + case True + from eq pmax1 pmax2 have "liseq' (arr_conv a) (nat i) = + liseq' (arr_conv a) (nat pmax) + 1" + by (rule longest_iseq4) + with True H1 H3 H4 show ?thesis + by simp + next + case False + with H1 i2 show ?thesis + by simp + qed + } + then show ?C1 by simp + from eq pmax1 pmax2 + have "liseq (arr_conv a) (Suc (nat i)) = + liseq (arr_conv a) (nat i) + 1" + by (rule longest_iseq3) + with H2 H3 H4 show ?C2 + by (simp add: idx_conv_suc) +qed + +spark_vc procedure_liseq_length_7 +proof - + from H1 show ?C1 + by (simp add: max_ext_def longest_iseq1 [of _ "nat i"]) + from H6 + have m: "max_ext (arr_conv a) (nat i) (nat i) + 1 = + liseq' (arr_conv a) (nat i)" + by (simp add: max_ext_def longest_iseq1 [of _ "nat i"]) + with H2 H18 + have gt: "liseq (arr_conv a) (nat i) < liseq' (arr_conv a) (nat i)" + by simp + then have "liseq' (arr_conv a) (nat i) = liseq (arr_conv a) (nat i) + 1" + by (rule longest_iseq2 [symmetric]) + with H2 m show ?C2 by simp + from gt have "liseq (arr_conv a) (Suc (nat i)) = liseq' (arr_conv a) (nat i)" + by (rule longest_iseq2') + with m H6 show ?C3 by (simp add: idx_conv_suc) +qed + +spark_vc procedure_liseq_length_8 +proof - + { + fix i2 + assume i2: "0 \ i2" "i2 \ i" + have "(l(i := max_ext' a i i + 1)) i2 = + int (liseq' (arr_conv a) (nat i2))" + proof (cases "i2 = i") + case True + with H1 show ?thesis + by (simp add: max_ext_def longest_iseq1 [of _ "nat i"]) + next + case False + with H1 i2 show ?thesis by simp + qed + } + then show ?C1 by simp + from H2 H6 H18 + have "liseq' (arr_conv a) (nat i) \ liseq (arr_conv a) (nat i)" + by (simp add: max_ext_def longest_iseq1 [of _ "nat i"]) + then have "liseq (arr_conv a) (Suc (nat i)) = liseq (arr_conv a) (nat i)" + by (rule longest_iseq5) + with H2 H6 show ?C2 by (simp add: idx_conv_suc) +qed + +spark_vc procedure_liseq_length_12 + by (simp add: max_ext_def) + +spark_vc procedure_liseq_length_13 + using H1 H6 H13 H21 H22 + by (simp add: max_ext_def + idx_conv_suc liseq'_Suc_unfold max_def del: Max_less_iff) + +spark_vc procedure_liseq_length_14 + using H1 H6 H13 H21 + by (cases "a j \ a i") + (simp_all add: max_ext_def + idx_conv_suc liseq'_Suc_unfold liseq'_Suc_unfold') + +spark_vc procedure_liseq_length_19 + using H3 H4 H5 H8 H9 + apply (rule_tac y="int (nat i)" in order_trans) + apply (cut_tac A="arr_conv a" and i="nat i" and j="nat i" in max_ext_limit) + apply simp_all + done + +spark_vc procedure_liseq_length_23 + using H2 H3 H4 H7 H8 H11 + apply (rule_tac y="int (nat i)" in order_trans) + apply (cut_tac A="arr_conv a" and i="nat i" in liseq_limit) + apply simp_all + done + +spark_vc procedure_liseq_length_29 + using H2 H3 H8 H13 + by (simp add: add1_zle_eq [symmetric]) + +spark_end + +end diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.fdl --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.fdl Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,37 @@ + {*******************************************************} + {FDL Declarations} + {Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039} + {Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.} + {*******************************************************} + + + {DATE : 29-NOV-2010 14:30:13.02} + + {procedure Liseq.Liseq_length} + + +title procedure liseq_length; + + function round__(real) : integer; + type vector = array [integer] of integer; + const integer__base__first : integer = pending; + const integer__base__last : integer = pending; + const l__index__subtype__1__first : integer = pending; + const l__index__subtype__1__last : integer = pending; + const a__index__subtype__1__first : integer = pending; + const a__index__subtype__1__last : integer = pending; + const integer__first : integer = pending; + const integer__last : integer = pending; + const integer__size : integer = pending; + var a : vector; + var l : vector; + var maxi : integer; + var maxj : integer; + var i : integer; + var j : integer; + var pmax : integer; + function liseq_prfx(vector, integer) : integer; + function liseq_ends_at(vector, integer) : integer; + function max_ext(vector, integer, integer) : integer; + +end; diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.rls --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.rls Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,34 @@ + /*********************************************************/ + /*Proof Rule Declarations*/ + /*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/ + /*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/ + /*********************************************************/ + + + /*DATE : 29-NOV-2010 14:30:13.02*/ + + /*procedure Liseq.Liseq_length*/ + + +rule_family liseq_length_rules: + X requires [X:any] & + X <= Y requires [X:ire, Y:ire] & + X >= Y requires [X:ire, Y:ire]. + +liseq_length_rules(1): integer__size >= 0 may_be_deduced. +liseq_length_rules(2): integer__first may_be_replaced_by -2147483648. +liseq_length_rules(3): integer__last may_be_replaced_by 2147483647. +liseq_length_rules(4): integer__base__first may_be_replaced_by -2147483648. +liseq_length_rules(5): integer__base__last may_be_replaced_by 2147483647. +liseq_length_rules(6): a__index__subtype__1__first >= integer__first may_be_deduced. +liseq_length_rules(7): a__index__subtype__1__last <= integer__last may_be_deduced. +liseq_length_rules(8): a__index__subtype__1__first <= + a__index__subtype__1__last may_be_deduced. +liseq_length_rules(9): a__index__subtype__1__last >= integer__first may_be_deduced. +liseq_length_rules(10): a__index__subtype__1__first <= integer__last may_be_deduced. +liseq_length_rules(11): l__index__subtype__1__first >= integer__first may_be_deduced. +liseq_length_rules(12): l__index__subtype__1__last <= integer__last may_be_deduced. +liseq_length_rules(13): l__index__subtype__1__first <= + l__index__subtype__1__last may_be_deduced. +liseq_length_rules(14): l__index__subtype__1__last >= integer__first may_be_deduced. +liseq_length_rules(15): l__index__subtype__1__first <= integer__last may_be_deduced. diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.siv --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.siv Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,547 @@ +***************************************************************************** + Semantic Analysis of SPARK Text + Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039 + Copyright (C) 2010 Altran Praxis Limited, Bath, U.K. +***************************************************************************** + + +CREATED 29-NOV-2010, 14:30:13 SIMPLIFIED 29-NOV-2010, 14:30:13 + +SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039 +Copyright (C) 2010 Altran Praxis Limited, Bath, U.K. + +procedure Liseq.Liseq_length + + + + +For path(s) from start to run-time check associated with statement of line 11: + +procedure_liseq_length_1. +*** true . /* all conclusions proved */ + + +For path(s) from start to run-time check associated with statement of line 12: + +procedure_liseq_length_2. +*** true . /* all conclusions proved */ + + +For path(s) from start to run-time check associated with statement of line 13: + +procedure_liseq_length_3. +*** true . /* all conclusions proved */ + + +For path(s) from start to run-time check associated with statement of line 14: + +procedure_liseq_length_4. +*** true . /* all conclusions proved */ + + +For path(s) from start to assertion of line 15: + +procedure_liseq_length_5. +H1: a__index__subtype__1__first = 0 . +H2: l__index__subtype__1__first = 0 . +H3: a__index__subtype__1__last = l__index__subtype__1__last . +H4: a__index__subtype__1__last < 2147483647 . +H5: for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 + <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) + and element(a, [i___1]) <= 2147483647) . +H6: for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 + <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) + and element(l, [i___1]) <= 2147483647) . +H7: 0 <= l__index__subtype__1__last . +H8: integer__size >= 0 . +H9: a__index__subtype__1__first <= a__index__subtype__1__last . +H10: l__index__subtype__1__first <= l__index__subtype__1__last . +H11: a__index__subtype__1__first >= - 2147483648 . +H12: a__index__subtype__1__last >= - 2147483648 . +H13: l__index__subtype__1__first >= - 2147483648 . +H14: l__index__subtype__1__last >= - 2147483648 . +H15: a__index__subtype__1__last <= 2147483647 . +H16: a__index__subtype__1__first <= 2147483647 . +H17: l__index__subtype__1__last <= 2147483647 . +H18: l__index__subtype__1__first <= 2147483647 . + -> +C1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= 0 -> element(update(l, [0], 1) + , [i2_]) = liseq_ends_at(a, i2_)) . +C2: 1 = liseq_prfx(a, 1) . + + +For path(s) from assertion of line 15 to assertion of line 15: + +procedure_liseq_length_6. +H1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = + liseq_ends_at(a, i2_)) . +H2: element(l, [pmax]) = liseq_prfx(a, i) . +H3: 0 <= pmax . +H4: pmax < i . +H5: a__index__subtype__1__first = 0 . +H6: l__index__subtype__1__first = 0 . +H7: a__index__subtype__1__last = l__index__subtype__1__last . +H8: a__index__subtype__1__last < 2147483647 . +H9: for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 + <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) + and element(a, [i___1]) <= 2147483647) . +H10: for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 + <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) + and element(l, [i___1]) <= 2147483647) . +H11: i <= l__index__subtype__1__last . +H12: pmax >= a__index__subtype__1__first . +H13: i <= a__index__subtype__1__last . +H14: element(a, [pmax]) <= element(a, [i]) . +H15: element(l, [pmax]) >= - 2147483648 . +H16: element(l, [pmax]) <= 2147483646 . +H17: i >= l__index__subtype__1__first . +H18: i <= 2147483646 . +H19: integer__size >= 0 . +H20: a__index__subtype__1__first <= a__index__subtype__1__last . +H21: l__index__subtype__1__first <= l__index__subtype__1__last . +H22: a__index__subtype__1__first >= - 2147483648 . +H23: a__index__subtype__1__last >= - 2147483648 . +H24: l__index__subtype__1__first >= - 2147483648 . +H25: l__index__subtype__1__last >= - 2147483648 . +H26: a__index__subtype__1__last <= 2147483647 . +H27: a__index__subtype__1__first <= 2147483647 . +H28: l__index__subtype__1__last <= 2147483647 . +H29: l__index__subtype__1__first <= 2147483647 . + -> +C1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i -> element(update(l, [i], + element(l, [pmax]) + 1), [i2_]) = liseq_ends_at(a, i2_)) . +C2: element(l, [pmax]) + 1 = liseq_prfx(a, i + 1) . + + +For path(s) from assertion of line 26 to assertion of line 15: + +procedure_liseq_length_7. +H1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = + liseq_ends_at(a, i2_)) . +H2: element(l, [pmax]) = liseq_prfx(a, i) . +H3: i <= l__index__subtype__1__last . +H4: 0 <= pmax . +H5: pmax < i . +H6: 0 <= i . +H7: a__index__subtype__1__first = 0 . +H8: l__index__subtype__1__first = 0 . +H9: a__index__subtype__1__last = l__index__subtype__1__last . +H10: a__index__subtype__1__last < 2147483647 . +H11: for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 + <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) + and element(a, [i___1]) <= 2147483647) . +H12: for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 + <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) + and element(l, [i___1]) <= 2147483647) . +H13: i <= 2147483647 . +H14: max_ext(a, i, i) >= - 2147483648 . +H15: max_ext(a, i, i) <= 2147483646 . +H16: i >= l__index__subtype__1__first . +H17: element(l, [pmax]) >= - 2147483648 . +H18: max_ext(a, i, i) + 1 > element(l, [pmax]) . +H19: element(l, [pmax]) <= 2147483646 . +H20: i <= 2147483646 . +H21: integer__size >= 0 . +H22: a__index__subtype__1__first <= a__index__subtype__1__last . +H23: l__index__subtype__1__first <= l__index__subtype__1__last . +H24: a__index__subtype__1__first >= - 2147483648 . +H25: a__index__subtype__1__last >= - 2147483648 . +H26: l__index__subtype__1__first >= - 2147483648 . +H27: l__index__subtype__1__last >= - 2147483648 . +H28: a__index__subtype__1__last <= 2147483647 . +H29: a__index__subtype__1__first <= 2147483647 . +H30: l__index__subtype__1__last <= 2147483647 . +H31: l__index__subtype__1__first <= 2147483647 . + -> +C1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i -> element(update(l, [i], + max_ext(a, i, i) + 1), [i2_]) = liseq_ends_at(a, i2_)) . +C2: max_ext(a, i, i) + 1 = element(l, [pmax]) + 1 . +C3: max_ext(a, i, i) + 1 = liseq_prfx(a, i + 1) . + + +procedure_liseq_length_8. +H1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = + liseq_ends_at(a, i2_)) . +H2: element(l, [pmax]) = liseq_prfx(a, i) . +H3: i <= l__index__subtype__1__last . +H4: 0 <= pmax . +H5: pmax < i . +H6: 0 <= i . +H7: a__index__subtype__1__first = 0 . +H8: l__index__subtype__1__first = 0 . +H9: a__index__subtype__1__last = l__index__subtype__1__last . +H10: a__index__subtype__1__last < 2147483647 . +H11: for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 + <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) + and element(a, [i___1]) <= 2147483647) . +H12: for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 + <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) + and element(l, [i___1]) <= 2147483647) . +H13: i <= 2147483647 . +H14: max_ext(a, i, i) >= - 2147483648 . +H15: max_ext(a, i, i) <= 2147483646 . +H16: i >= l__index__subtype__1__first . +H17: element(l, [pmax]) <= 2147483647 . +H18: max_ext(a, i, i) + 1 <= element(l, [pmax]) . +H19: i <= 2147483646 . +H20: integer__size >= 0 . +H21: a__index__subtype__1__first <= a__index__subtype__1__last . +H22: l__index__subtype__1__first <= l__index__subtype__1__last . +H23: a__index__subtype__1__first >= - 2147483648 . +H24: a__index__subtype__1__last >= - 2147483648 . +H25: l__index__subtype__1__first >= - 2147483648 . +H26: l__index__subtype__1__last >= - 2147483648 . +H27: a__index__subtype__1__last <= 2147483647 . +H28: a__index__subtype__1__first <= 2147483647 . +H29: l__index__subtype__1__last <= 2147483647 . +H30: l__index__subtype__1__first <= 2147483647 . + -> +C1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i -> element(update(l, [i], + max_ext(a, i, i) + 1), [i2_]) = liseq_ends_at(a, i2_)) . +C2: element(l, [pmax]) = liseq_prfx(a, i + 1) . + + +For path(s) from assertion of line 15 to run-time check associated with + statement of line 23: + +procedure_liseq_length_9. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 15 to run-time check associated with + statement of line 24: + +procedure_liseq_length_10. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 15 to run-time check associated with + statement of line 25: + +procedure_liseq_length_11. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 15 to assertion of line 26: + +procedure_liseq_length_12. +H1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = + liseq_ends_at(a, i2_)) . +H2: element(l, [pmax]) = liseq_prfx(a, i) . +H3: 0 <= pmax . +H4: pmax < i . +H5: a__index__subtype__1__first = 0 . +H6: l__index__subtype__1__first = 0 . +H7: a__index__subtype__1__last = l__index__subtype__1__last . +H8: a__index__subtype__1__last < 2147483647 . +H9: for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 + <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) + and element(a, [i___1]) <= 2147483647) . +H10: for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 + <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) + and element(l, [i___1]) <= 2147483647) . +H11: i <= l__index__subtype__1__last . +H12: pmax <= 2147483647 . +H13: pmax >= a__index__subtype__1__first . +H14: i <= a__index__subtype__1__last . +H15: element(a, [i]) < element(a, [pmax]) . +H16: integer__size >= 0 . +H17: a__index__subtype__1__first <= a__index__subtype__1__last . +H18: l__index__subtype__1__first <= l__index__subtype__1__last . +H19: a__index__subtype__1__first >= - 2147483648 . +H20: a__index__subtype__1__last >= - 2147483648 . +H21: l__index__subtype__1__first >= - 2147483648 . +H22: l__index__subtype__1__last >= - 2147483648 . +H23: a__index__subtype__1__last <= 2147483647 . +H24: a__index__subtype__1__first <= 2147483647 . +H25: l__index__subtype__1__last <= 2147483647 . +H26: l__index__subtype__1__first <= 2147483647 . + -> +C1: 0 = max_ext(a, i, 0) . + + +For path(s) from assertion of line 26 to assertion of line 26: + +procedure_liseq_length_13. +H1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = + liseq_ends_at(a, i2_)) . +H2: element(l, [pmax]) = liseq_prfx(a, i) . +H3: i <= l__index__subtype__1__last . +H4: 0 <= pmax . +H5: pmax < i . +H6: 0 <= j . +H7: a__index__subtype__1__first = 0 . +H8: l__index__subtype__1__first = 0 . +H9: a__index__subtype__1__last = l__index__subtype__1__last . +H10: a__index__subtype__1__last < 2147483647 . +H11: for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 + <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) + and element(a, [i___1]) <= 2147483647) . +H12: for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 + <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) + and element(l, [i___1]) <= 2147483647) . +H13: j < i . +H14: max_ext(a, i, j) >= - 2147483648 . +H15: max_ext(a, i, j) <= 2147483647 . +H16: j >= l__index__subtype__1__first . +H17: i >= a__index__subtype__1__first . +H18: i <= a__index__subtype__1__last . +H19: j >= a__index__subtype__1__first . +H20: j <= a__index__subtype__1__last . +H21: element(a, [j]) <= element(a, [i]) . +H22: max_ext(a, i, j) < element(l, [j]) . +H23: element(l, [j]) >= - 2147483648 . +H24: element(l, [j]) <= 2147483647 . +H25: j <= 2147483646 . +H26: integer__size >= 0 . +H27: a__index__subtype__1__first <= a__index__subtype__1__last . +H28: l__index__subtype__1__first <= l__index__subtype__1__last . +H29: a__index__subtype__1__first >= - 2147483648 . +H30: a__index__subtype__1__last >= - 2147483648 . +H31: l__index__subtype__1__first >= - 2147483648 . +H32: l__index__subtype__1__last >= - 2147483648 . +H33: a__index__subtype__1__last <= 2147483647 . +H34: a__index__subtype__1__first <= 2147483647 . +H35: l__index__subtype__1__last <= 2147483647 . +H36: l__index__subtype__1__first <= 2147483647 . + -> +C1: element(l, [j]) = max_ext(a, i, j + 1) . + + +procedure_liseq_length_14. +H1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = + liseq_ends_at(a, i2_)) . +H2: element(l, [pmax]) = liseq_prfx(a, i) . +H3: i <= l__index__subtype__1__last . +H4: 0 <= pmax . +H5: pmax < i . +H6: 0 <= j . +H7: a__index__subtype__1__first = 0 . +H8: l__index__subtype__1__first = 0 . +H9: a__index__subtype__1__last = l__index__subtype__1__last . +H10: a__index__subtype__1__last < 2147483647 . +H11: for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 + <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) + and element(a, [i___1]) <= 2147483647) . +H12: for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 + <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) + and element(l, [i___1]) <= 2147483647) . +H13: j < i . +H14: max_ext(a, i, j) >= - 2147483648 . +H15: max_ext(a, i, j) <= 2147483647 . +H16: j >= l__index__subtype__1__first . +H17: i >= a__index__subtype__1__first . +H18: i <= a__index__subtype__1__last . +H19: j >= a__index__subtype__1__first . +H20: j <= a__index__subtype__1__last . +H21: element(a, [i]) < element(a, [j]) or element(l, [j]) <= max_ext(a, i, j) + . +H22: j <= 2147483646 . +H23: integer__size >= 0 . +H24: a__index__subtype__1__first <= a__index__subtype__1__last . +H25: l__index__subtype__1__first <= l__index__subtype__1__last . +H26: a__index__subtype__1__first >= - 2147483648 . +H27: a__index__subtype__1__last >= - 2147483648 . +H28: l__index__subtype__1__first >= - 2147483648 . +H29: l__index__subtype__1__last >= - 2147483648 . +H30: a__index__subtype__1__last <= 2147483647 . +H31: a__index__subtype__1__first <= 2147483647 . +H32: l__index__subtype__1__last <= 2147483647 . +H33: l__index__subtype__1__first <= 2147483647 . + -> +C1: max_ext(a, i, j) = max_ext(a, i, j + 1) . + + +For path(s) from assertion of line 26 to run-time check associated with + statement of line 36: + +procedure_liseq_length_15. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 26 to run-time check associated with + statement of line 38: + +procedure_liseq_length_16. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 26 to run-time check associated with + statement of line 40: + +procedure_liseq_length_17. +*** true . /* all conclusions proved */ + + +procedure_liseq_length_18. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 26 to run-time check associated with + statement of line 42: + +procedure_liseq_length_19. +H1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = + liseq_ends_at(a, i2_)) . +H2: element(l, [pmax]) = liseq_prfx(a, i) . +H3: i <= l__index__subtype__1__last . +H4: 0 <= pmax . +H5: pmax < i . +H6: a__index__subtype__1__first = 0 . +H7: l__index__subtype__1__first = 0 . +H8: a__index__subtype__1__last = l__index__subtype__1__last . +H9: a__index__subtype__1__last < 2147483647 . +H10: for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 + <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) + and element(a, [i___1]) <= 2147483647) . +H11: for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 + <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) + and element(l, [i___1]) <= 2147483647) . +H12: i <= 2147483647 . +H13: max_ext(a, i, i) >= - 2147483648 . +H14: max_ext(a, i, i) <= 2147483647 . +H15: integer__size >= 0 . +H16: a__index__subtype__1__first <= a__index__subtype__1__last . +H17: l__index__subtype__1__first <= l__index__subtype__1__last . +H18: a__index__subtype__1__first >= - 2147483648 . +H19: a__index__subtype__1__last >= - 2147483648 . +H20: l__index__subtype__1__first >= - 2147483648 . +H21: l__index__subtype__1__last >= - 2147483648 . +H22: a__index__subtype__1__last <= 2147483647 . +H23: a__index__subtype__1__first <= 2147483647 . +H24: l__index__subtype__1__last <= 2147483647 . +H25: l__index__subtype__1__first <= 2147483647 . + -> +C1: max_ext(a, i, i) <= 2147483646 . + + +For path(s) from assertion of line 26 to run-time check associated with + statement of line 43: + +procedure_liseq_length_20. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 26 to run-time check associated with + statement of line 44: + +procedure_liseq_length_21. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 26 to run-time check associated with + statement of line 45: + +procedure_liseq_length_22. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 15 to run-time check associated with + statement of line 48: + +procedure_liseq_length_23. +H1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = + liseq_ends_at(a, i2_)) . +H2: element(l, [pmax]) = liseq_prfx(a, i) . +H3: 0 <= pmax . +H4: pmax < i . +H5: a__index__subtype__1__first = 0 . +H6: l__index__subtype__1__first = 0 . +H7: a__index__subtype__1__last = l__index__subtype__1__last . +H8: a__index__subtype__1__last < 2147483647 . +H9: for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 + <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) + and element(a, [i___1]) <= 2147483647) . +H10: for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 + <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) + and element(l, [i___1]) <= 2147483647) . +H11: i <= l__index__subtype__1__last . +H12: pmax <= 2147483647 . +H13: pmax >= a__index__subtype__1__first . +H14: i <= a__index__subtype__1__last . +H15: element(a, [pmax]) <= element(a, [i]) . +H16: element(l, [pmax]) >= - 2147483648 . +H17: element(l, [pmax]) <= 2147483647 . +H18: integer__size >= 0 . +H19: a__index__subtype__1__first <= a__index__subtype__1__last . +H20: l__index__subtype__1__first <= l__index__subtype__1__last . +H21: a__index__subtype__1__first >= - 2147483648 . +H22: a__index__subtype__1__last >= - 2147483648 . +H23: l__index__subtype__1__first >= - 2147483648 . +H24: l__index__subtype__1__last >= - 2147483648 . +H25: a__index__subtype__1__last <= 2147483647 . +H26: a__index__subtype__1__first <= 2147483647 . +H27: l__index__subtype__1__last <= 2147483647 . +H28: l__index__subtype__1__first <= 2147483647 . + -> +C1: element(l, [pmax]) <= 2147483646 . + + +For path(s) from assertion of line 15 to run-time check associated with + statement of line 49: + +procedure_liseq_length_24. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 15 to run-time check associated with + statement of line 50: + +procedure_liseq_length_25. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 15 to run-time check associated with + statement of line 52: + +procedure_liseq_length_26. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 26 to run-time check associated with + statement of line 52: + +procedure_liseq_length_27. +*** true . /* all conclusions proved */ + + +procedure_liseq_length_28. +*** true . /* all conclusions proved */ + + +For path(s) from assertion of line 15 to finish: + +procedure_liseq_length_29. +H1: for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = + liseq_ends_at(a, i2_)) . +H2: element(l, [pmax]) = liseq_prfx(a, i) . +H3: i <= l__index__subtype__1__last + 1 . +H4: 0 <= pmax . +H5: pmax < i . +H6: a__index__subtype__1__first = 0 . +H7: l__index__subtype__1__first = 0 . +H8: a__index__subtype__1__last = l__index__subtype__1__last . +H9: a__index__subtype__1__last < 2147483647 . +H10: for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 + <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) + and element(a, [i___1]) <= 2147483647) . +H11: for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 + <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) + and element(l, [i___1]) <= 2147483647) . +H12: i <= 2147483647 . +H13: l__index__subtype__1__last < i . +H14: integer__size >= 0 . +H15: a__index__subtype__1__first <= a__index__subtype__1__last . +H16: l__index__subtype__1__first <= l__index__subtype__1__last . +H17: a__index__subtype__1__first >= - 2147483648 . +H18: a__index__subtype__1__last >= - 2147483648 . +H19: l__index__subtype__1__first >= - 2147483648 . +H20: l__index__subtype__1__last >= - 2147483648 . +H21: a__index__subtype__1__last <= 2147483647 . +H22: a__index__subtype__1__first <= 2147483647 . +H23: l__index__subtype__1__last <= 2147483647 . +H24: l__index__subtype__1__first <= 2147483647 . + -> +C1: element(l, [pmax]) = liseq_prfx(a, a__index__subtype__1__last + 1) . + + diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/README --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/README Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,3 @@ +The copyright notice contained in the *.siv, *.fdl, and *.rls files in +the example subdirectories refers to the tools that have been used to +generate the files, but not to the files themselves. diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/RIPEMD-160/F.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/F.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,66 @@ +(* Title: HOL/SPARK/Examples/RIPEMD-160/F.thy + Author: Fabian Immler, TU Muenchen + +Verification of the RIPEMD-160 hash function +*) + +theory F +imports RMD_Specification +begin + +spark_open "rmd/f.siv" + +spark_vc function_f_2 + using assms by simp_all + +spark_vc function_f_3 + using assms by simp_all + +spark_vc function_f_4 + using assms by simp_all + +spark_vc function_f_5 + using assms by simp_all + +spark_vc function_f_6 +proof - + from H8 have "nat j <= 15" by simp + with assms show ?thesis + by (simp add: f_def bwsimps int_word_uint int_mod_eq') +qed + +spark_vc function_f_7 +proof - + from H7 have "16 <= nat j" by simp + moreover from H8 have "nat j <= 31" by simp + ultimately show ?thesis using assms + by (simp add: f_def bwsimps int_word_uint int_mod_eq') +qed + +spark_vc function_f_8 +proof - + from H7 have "32 <= nat j" by simp + moreover from H8 have "nat j <= 47" by simp + ultimately show ?thesis using assms + by (simp add: f_def bwsimps int_word_uint int_mod_eq') +qed + +spark_vc function_f_9 +proof - + from H7 have "48 <= nat j" by simp + moreover from H8 have "nat j <= 63" by simp + ultimately show ?thesis using assms + by (simp add: f_def bwsimps int_word_uint int_mod_eq') +qed + +spark_vc function_f_10 +proof - + from H2 have "nat j <= 79" by simp + moreover from H12 have "64 <= nat j" by simp + ultimately show ?thesis using assms + by (simp add: f_def bwsimps int_word_uint int_mod_eq') +qed + +spark_end + +end diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Hash.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,100 @@ +(* Title: HOL/SPARK/Examples/RIPEMD-160/Hash.thy + Author: Fabian Immler, TU Muenchen + +Verification of the RIPEMD-160 hash function +*) + +theory Hash +imports RMD_Specification +begin + +spark_open "rmd/hash.siv" + +abbreviation from_chain :: "chain \ RMD.chain" where + "from_chain c \ ( + word_of_int (h0 c), + word_of_int (h1 c), + word_of_int (h2 c), + word_of_int (h3 c), + word_of_int (h4 c))" + +abbreviation to_chain :: "RMD.chain \ chain" where + "to_chain c \ + (let (h0, h1, h2, h3, h4) = c in + (|h0 = uint h0, + h1 = uint h1, + h2 = uint h2, + h3 = uint h3, + h4 = uint h4|))" + +abbreviation round' :: "chain \ block \ chain" where + "round' c b == to_chain (round (\n. word_of_int (b (int n))) (from_chain c))" + +abbreviation rounds' :: "chain \ int \ message \ chain" where + "rounds' h i X == + to_chain (rounds + (\n. \m. word_of_int (X (int n) (int m))) + (from_chain h) + (nat i))" + +abbreviation rmd_hash :: "message \ int \ chain" where + "rmd_hash X i == to_chain (rmd + (\n. \m. word_of_int (X (int n) (int m))) + (nat i))" + +spark_proof_functions + round_spec = round' + rounds = rounds' + rmd_hash = rmd_hash + +spark_vc function_hash_12 + using H1 H6 + by (simp add: + rounds_def rmd_body_def round_def + h_0_def h0_0_def h1_0_def h2_0_def h3_0_def h4_0_def) + + +lemma rounds_step: + assumes "0 <= i" + shows "rounds X b (Suc i) = round (X i) (rounds X b i)" + by (simp add: rounds_def rmd_body_def) + +lemma from_to_id: "from_chain (to_chain C) = C" +proof (cases C) + fix a b c d e f::word32 + assume "C = (a, b, c, d, e)" + thus ?thesis by (cases a) simp +qed + +lemma steps_to_steps': + "round X (foldl a b c) = round X (from_chain (to_chain (foldl a b c)))" + unfolding from_to_id .. + +lemma rounds'_step: + assumes "0 <= i" + shows "rounds' c (i + 1) x = round' (rounds' c i x) (x i)" +proof - + have makesuc: "nat (i + 1) = Suc (nat i)" using assms by simp + show ?thesis using assms + by (simp add: makesuc rounds_def rmd_body_def steps_to_steps') +qed + + +spark_vc function_hash_13 +proof - + have loop_suc: "loop__1__i + 2 = (loop__1__i + 1) + 1" by simp + have "0 <= loop__1__i + 1" using `0 <= loop__1__i` by simp + show ?thesis + unfolding loop_suc + unfolding rounds'_step[OF `0 <= loop__1__i + 1`] + unfolding H1[symmetric] + unfolding H18 .. +qed + + +spark_vc function_hash_17 + unfolding rmd_def H1 rounds_def .. + +spark_end + +end diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/K_L.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,46 @@ +(* Title: HOL/SPARK/Examples/RIPEMD-160/K_L.thy + Author: Fabian Immler, TU Muenchen + +Verification of the RIPEMD-160 hash function +*) + +theory K_L +imports RMD_Specification +begin + +spark_open "rmd/k_l.siv" + +spark_vc function_k_l_6 + using assms by (simp add: K_def) + +spark_vc function_k_l_7 +proof - + from H1 have "16 <= nat j" by simp + moreover from H2 have "nat j <= 31" by simp + ultimately show ?thesis by (simp add: K_def) +qed + +spark_vc function_k_l_8 +proof - + from H1 have "32 <= nat j" by simp + moreover from H2 have "nat j <= 47" by simp + ultimately show ?thesis by (simp add: K_def) +qed + +spark_vc function_k_l_9 +proof - + from H1 have "48 <= nat j" by simp + moreover from H2 have "nat j <= 63" by simp + ultimately show ?thesis by (simp add: K_def) +qed + +spark_vc function_k_l_10 +proof - + from H6 have "64 <= nat j" by simp + moreover from H2 have "nat j <= 79" by simp + ultimately show ?thesis by (simp add: K_def) +qed + +spark_end + +end diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/K_R.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,46 @@ +(* Title: HOL/SPARK/Examples/RIPEMD-160/K_R.thy + Author: Fabian Immler, TU Muenchen + +Verification of the RIPEMD-160 hash function +*) + +theory K_R +imports RMD_Specification +begin + +spark_open "rmd/k_r.siv" + +spark_vc function_k_r_6 + using assms by (simp add: K'_def) + +spark_vc function_k_r_7 +proof- + from H1 have "16 <= nat j" by simp + moreover from H2 have "nat j <= 31" by simp + ultimately show ?thesis by (simp add: K'_def) +qed + +spark_vc function_k_r_8 +proof - + from H1 have "32 <= nat j" by simp + moreover from H2 have "nat j <= 47" by simp + ultimately show ?thesis by (simp add: K'_def) +qed + +spark_vc function_k_r_9 +proof - + from H1 have "48 <= nat j" by simp + moreover from H2 have "nat j <= 63" by simp + ultimately show ?thesis by (simp add: K'_def) +qed + +spark_vc function_k_r_10 +proof - + from H6 have "64 <= nat j" by simp + moreover from H2 have "nat j <= 79" by simp + ultimately show ?thesis by (simp add: K'_def) +qed + +spark_end + +end diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,180 @@ +(* Title: HOL/SPARK/Examples/RIPEMD-160/RMD.thy + Author: Fabian Immler, TU Muenchen + +Verification of the RIPEMD-160 hash function +*) + +theory RMD +imports Word +begin + + +(* all operations are defined on 32-bit words *) + +types word32 = "32 word" +types byte = "8 word" +types perm = "nat \ nat" +types chain = "word32 * word32 * word32 * word32 * word32" +types block = "nat \ word32" +types message = "nat \ block" + +(* nonlinear functions at bit level *) + +definition f::"[nat, word32, word32, word32] => word32" +where +"f j x y z = + (if ( 0 <= j & j <= 15) then x XOR y XOR z + else if (16 <= j & j <= 31) then (x AND y) OR (NOT x AND z) + else if (32 <= j & j <= 47) then (x OR NOT y) XOR z + else if (48 <= j & j <= 63) then (x AND z) OR (y AND NOT z) + else if (64 <= j & j <= 79) then x XOR (y OR NOT z) + else 0)" + + +(* added constants (hexadecimal) *) + +definition K::"nat => word32" +where +"K j = + (if ( 0 <= j & j <= 15) then 0x00000000 + else if (16 <= j & j <= 31) then 0x5A827999 + else if (32 <= j & j <= 47) then 0x6ED9EBA1 + else if (48 <= j & j <= 63) then 0x8F1BBCDC + else if (64 <= j & j <= 79) then 0xA953FD4E + else 0)" + +definition K'::"nat => word32" +where +"K' j = + (if ( 0 <= j & j <= 15) then 0x50A28BE6 + else if (16 <= j & j <= 31) then 0x5C4DD124 + else if (32 <= j & j <= 47) then 0x6D703EF3 + else if (48 <= j & j <= 63) then 0x7A6D76E9 + else if (64 <= j & j <= 79) then 0x00000000 + else 0)" + + +(* selection of message word *) + +definition r_list :: "nat list" + where "r_list = [ + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, + 7, 4, 13, 1, 10, 6, 15, 3, 12, 0, 9, 5, 2, 14, 11, 8, + 3, 10, 14, 4, 9, 15, 8, 1, 2, 7, 0, 6, 13, 11, 5, 12, + 1, 9, 11, 10, 0, 8, 12, 4, 13, 3, 7, 15, 14, 5, 6, 2, + 4, 0, 5, 9, 7, 12, 2, 10, 14, 1, 3, 8, 11, 6, 15, 13 + ]" + +definition r'_list :: "nat list" + where "r'_list = [ + 5, 14, 7, 0, 9, 2, 11, 4, 13, 6, 15, 8, 1, 10, 3, 12, + 6, 11, 3, 7, 0, 13, 5, 10, 14, 15, 8, 12, 4, 9, 1, 2, + 15, 5, 1, 3, 7, 14, 6, 9, 11, 8, 12, 2, 10, 0, 4, 13, + 8, 6, 4, 1, 3, 11, 15, 0, 5, 12, 2, 13, 9, 7, 10, 14, + 12, 15, 10, 4, 1, 5, 8, 7, 6, 2, 13, 14, 0, 3, 9, 11 + ]" + +definition r :: perm + where "r j = r_list ! j" + +definition r' :: perm + where "r' j = r'_list ! j" + + +(* amount for rotate left (rol) *) + +definition s_list :: "nat list" + where "s_list = [ + 11, 14, 15, 12, 5, 8, 7, 9, 11, 13, 14, 15, 6, 7, 9, 8, + 7, 6, 8, 13, 11, 9, 7, 15, 7, 12, 15, 9, 11, 7, 13, 12, + 11, 13, 6, 7, 14, 9, 13, 15, 14, 8, 13, 6, 5, 12, 7, 5, + 11, 12, 14, 15, 14, 15, 9, 8, 9, 14, 5, 6, 8, 6, 5, 12, + 9, 15, 5, 11, 6, 8, 13, 12, 5, 12, 13, 14, 11, 8, 5, 6 + ]" + +definition s'_list :: "nat list" + where "s'_list = [ + 8, 9, 9, 11, 13, 15, 15, 5, 7, 7, 8, 11, 14, 14, 12, 6, + 9, 13, 15, 7, 12, 8, 9, 11, 7, 7, 12, 7, 6, 15, 13, 11, + 9, 7, 15, 11, 8, 6, 6, 14, 12, 13, 5, 14, 13, 13, 7, 5, + 15, 5, 8, 11, 14, 14, 6, 14, 6, 9, 12, 9, 12, 5, 15, 8, + 8, 5, 12, 9, 12, 5, 14, 6, 8, 13, 6, 5, 15, 13, 11, 11 + ]" + +definition s :: perm + where "s j = s_list ! j" + +definition s' :: perm + where "s' j = s'_list ! j" + + +(* Initial value (hexadecimal *) + +definition h0_0::word32 where "h0_0 = 0x67452301" +definition h1_0::word32 where "h1_0 = 0xEFCDAB89" +definition h2_0::word32 where "h2_0 = 0x98BADCFE" +definition h3_0::word32 where "h3_0 = 0x10325476" +definition h4_0::word32 where "h4_0 = 0xC3D2E1F0" +definition h_0::chain where "h_0 = (h0_0, h1_0, h2_0, h3_0, h4_0)" + + +definition step_l :: + "[ block, + chain, + nat + ] => chain" + where + "step_l X c j = + (let (A, B, C, D, E) = c in + ((* A *) E, + (* B *) word_rotl (s j) (A + f j B C D + X (r j) + K j) + E, + (* C *) B, + (* D *) word_rotl 10 C, + (* E *) D))" + +definition step_r :: + "[ block, + chain, + nat + ] \ chain" +where + "step_r X c' j = + (let (A', B', C', D', E') = c' in + ((* A' *) E', + (* B' *) word_rotl (s' j) (A' + f (79 - j) B' C' D' + X (r' j) + K' j) + E', + (* C' *) B', + (* D' *) word_rotl 10 C', + (* E' *) D'))" + +definition step_both :: + "[ block, chain * chain, nat ] \ chain * chain" + where + "step_both X cc j = (case cc of (c, c') \ + (step_l X c j, step_r X c' j))" + +definition steps::"[ block, chain * chain, nat] \ chain * chain" + where "steps X cc i = foldl (step_both X) cc [0.. chain" + where "round X h = + (let (h0, h1, h2, h3, h4) = h in + let ((A, B, C, D, E), (A', B', C', D', E')) = steps X (h, h) 80 in + ((* h0 *) h1 + C + D', + (* h1 *) h2 + D + E', + (* h2 *) h3 + E + A', + (* h3 *) h4 + A + B', + (* h4 *) h0 + B + C'))" + +definition rmd_body::"[ message, chain, nat ] => chain" +where + "rmd_body X h i = round (X i) h" + +definition rounds::"message \ chain \ nat \ chain" +where + "rounds X h i = foldl (rmd_body X) h_0 [0.. nat \ chain" +where + "rmd X len = rounds X h_0 len" + +end \ No newline at end of file diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,27 @@ +(* Title: HOL/SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy + Author: Fabian Immler, TU Muenchen + +Verification of the RIPEMD-160 hash function +*) + +theory RMD_Lemmas +imports Main +begin + +definition "fun_of_list i xs g j = + (if j < i \ i + int (length xs) \ j then g j else xs ! nat (j - i))" + +lemma fun_of_list_Nil [simp]: "fun_of_list i [] g = g" + by (auto simp add: fun_eq_iff fun_of_list_def) + +lemma fun_of_list_Cons [simp]: + "fun_of_list i (x # xs) g = fun_of_list (i + 1) xs (g(i:=x))" + by (auto simp add: fun_eq_iff fun_of_list_def nth_Cons' + nat_diff_distrib [of "int (Suc 0)", simplified, symmetric] + diff_diff_eq) + +lemma nth_fun_of_list_eq: + "0 \ i \ i < int (length xs) \ xs ! nat i = fun_of_list 0 xs g i" + by (simp add: fun_of_list_def) + +end diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,47 @@ +(* Title: HOL/SPARK/Examples/RIPEMD-160/RMD_Specification.thy + Author: Fabian Immler, TU Muenchen + +Verification of the RIPEMD-160 hash function +*) + +theory RMD_Specification +imports RMD SPARK + +begin + +(* bit operations *) + +abbreviation rotate_left :: "int \ int \ int" where + "rotate_left i w == uint (word_rotl (nat i) (word_of_int w::word32))" + +spark_proof_functions + wordops__rotate_left = rotate_left + + +(* Conversions for proof functions *) +abbreviation k_l_spec :: " int => int " where + "k_l_spec j == uint (K (nat j))" +abbreviation k_r_spec :: " int => int " where + "k_r_spec j == uint (K' (nat j))" +abbreviation r_l_spec :: " int => int " where + "r_l_spec j == int (r (nat j))" +abbreviation r_r_spec :: " int => int " where + "r_r_spec j == int (r' (nat j))" +abbreviation s_l_spec :: " int => int " where + "s_l_spec j == int (s (nat j))" +abbreviation s_r_spec :: " int => int " where + "s_r_spec j == int (s' (nat j))" +abbreviation f_spec :: "int \ int \ int \ int \ int" where + "f_spec j x y z == + uint (f (nat j) (word_of_int x::word32) (word_of_int y) (word_of_int z))" + +spark_proof_functions + k_l_spec = k_l_spec + k_r_spec = k_r_spec + r_l_spec = r_l_spec + r_r_spec = r_r_spec + s_l_spec = s_l_spec + s_r_spec = s_r_spec + f_spec = f_spec + +end diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/R_L.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,30 @@ +(* Title: HOL/SPARK/Examples/RIPEMD-160/R_L.thy + Author: Fabian Immler, TU Muenchen + +Verification of the RIPEMD-160 hash function +*) + +theory R_L +imports RMD_Specification RMD_Lemmas +begin + +spark_open "rmd/r_l.siv" + +spark_vc function_r_l_2 +proof - + from `0 \ j` `j \ 79` + show C: ?C1 + by (simp add: r_def r_list_def nth_map [symmetric, of _ _ int] del: fun_upd_apply) + (simp add: nth_fun_of_list_eq [of _ _ undefined] del: fun_upd_apply) + from C show ?C2 by simp + have "list_all (\n. int n \ 15) r_list" + by (simp add: r_list_def) + moreover have "length r_list = 80" + by (simp add: r_list_def) + ultimately show ?C3 unfolding C using `j \ 79` + by (simp add: r_def list_all_length) +qed + +spark_end + +end diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/R_R.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,30 @@ +(* Title: HOL/SPARK/Examples/RIPEMD-160/R_R.thy + Author: Fabian Immler, TU Muenchen + +Verification of the RIPEMD-160 hash function +*) + +theory R_R +imports RMD_Specification RMD_Lemmas +begin + +spark_open "rmd/r_r.siv" + +spark_vc function_r_r_2 +proof - + from `0 \ j` `j \ 79` + show C: ?C1 + by (simp add: r'_def r'_list_def nth_map [symmetric, of _ _ int] del: fun_upd_apply) + (simp add: nth_fun_of_list_eq [of _ _ undefined] del: fun_upd_apply) + from C show ?C2 by simp + have "list_all (\n. int n \ 15) r'_list" + by (simp add: r'_list_def) + moreover have "length r'_list = 80" + by (simp add: r'_list_def) + ultimately show ?C3 unfolding C using `j \ 79` + by (simp add: r'_def list_all_length) +qed + +spark_end + +end diff -r 236cd8f07f7b -r d1318f3c86ba src/HOL/SPARK/Examples/RIPEMD-160/Round.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Sat Jan 15 12:35:29 2011 +0100 @@ -0,0 +1,465 @@ +(* Title: HOL/SPARK/Examples/RIPEMD-160/Round.thy + Author: Fabian Immler, TU Muenchen + +Verification of the RIPEMD-160 hash function +*) + +theory Round +imports RMD_Specification +begin + +spark_open "rmd/round.siv" + +abbreviation from_chain :: "chain \ RMD.chain" where + "from_chain c \ ( + word_of_int (h0 c), + word_of_int (h1 c), + word_of_int (h2 c), + word_of_int (h3 c), + word_of_int (h4 c))" + +abbreviation from_chain_pair :: "chain_pair \ RMD.chain \ RMD.chain" where + "from_chain_pair cc \ ( + from_chain (left cc), + from_chain (right cc))" + +abbreviation to_chain :: "RMD.chain \ chain" where + "to_chain c \ + (let (h0, h1, h2, h3, h4) = c in + (|h0 = uint h0, + h1 = uint h1, + h2 = uint h2, + h3 = uint h3, + h4 = uint h4|))" + +abbreviation to_chain_pair :: "RMD.chain \ RMD.chain \ chain_pair" where + "to_chain_pair c == (let (c1, c2) = c in + (| left = to_chain c1, + right = to_chain c2 |))" + +abbreviation steps' :: "chain_pair \ int \ block \ chain_pair" where + "steps' cc i b == to_chain_pair (steps + (\n. word_of_int (b (int n))) + (from_chain_pair cc) + (nat i))" + +abbreviation round_spec :: "chain \ block \ chain" where + "round_spec c b == to_chain (round (\n. word_of_int (b (int n))) (from_chain c))" + +spark_proof_functions + steps = steps' + round_spec = round_spec + +lemma uint_word_of_int_id: + assumes "0 <= (x::int)" + assumes "x <= 4294967295" + shows"uint(word_of_int x::word32) = x" + unfolding int_word_uint + using assms + by (simp add:int_mod_eq') + +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 add: int_mod_eq') + have "?X mod ?MM = ?X" using `0 <= ?X` `?X <= ?M` + by (simp add: int_mod_eq') + have "e mod ?MM = e" using `0 <= e` `e <= ?M` + by (simp add: int_mod_eq') + have "(?MM::int) = 2 ^ len_of TYPE(32)" by simp + show ?thesis + unfolding + word_add_alt + uint_word_of_int_id[OF `0 <= a` `a <= ?M`] + uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`] + int_word_uint + unfolding `?MM = 2 ^ len_of TYPE(32)` + unfolding word_uint.Abs_norm + by (simp add: + `a mod ?MM = a` + `e mod ?MM = e` + `?X mod ?MM = ?X`) + 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 add: int_mod_eq') + have "?X mod ?MM = ?X" using `0 <= ?X` `?X <= ?M` + by (simp add: int_mod_eq') + have "e' mod ?MM = e'" using `0 <= e'` `e' <= ?M` + by (simp add: int_mod_eq') + have "(?MM::int) = 2 ^ len_of TYPE(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_alt + uint_word_of_int_id[OF `0 <= a'` `a' <= ?M`] + uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`] + int_word_uint + nat_transfer + unfolding `?MM = 2 ^ len_of TYPE(32)` + unfolding word_uint.Abs_norm + by (simp add: + `a' mod ?MM = a'` + `e' mod ?MM = e'` + `?X mod ?MM = ?X`) + qed + + show ?thesis + unfolding steps'_step[OF `0 <= j`] step_hyp[symmetric] + step_both_def step_r_def step_l_def + by (simp add: AL BL CL DL EL AR BR CR DR ER) +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 = + \