src/HOL/SPARK/Examples/RIPEMD-160/rmd/hash.siv
changeset 41561 d1318f3c86ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/rmd/hash.siv	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,240 @@
     1.4 +*****************************************************************************
     1.5 +                       Semantic Analysis of SPARK Text
     1.6 +    Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
     1.7 +             Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
     1.8 +*****************************************************************************
     1.9 +
    1.10 +
    1.11 +CREATED 29-NOV-2010, 14:30:20  SIMPLIFIED 29-NOV-2010, 14:30:20
    1.12 +
    1.13 +SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
    1.14 +Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
    1.15 +
    1.16 +function RMD.Hash
    1.17 +
    1.18 +
    1.19 +
    1.20 +
    1.21 +For path(s) from start to run-time check associated with statement of line 170:
    1.22 +
    1.23 +function_hash_1.
    1.24 +*** true .          /* all conclusions proved */
    1.25 +
    1.26 +
    1.27 +For path(s) from start to run-time check associated with statement of line 171:
    1.28 +
    1.29 +function_hash_2.
    1.30 +*** true .          /* all conclusions proved */
    1.31 +
    1.32 +
    1.33 +For path(s) from start to run-time check associated with statement of line 172:
    1.34 +
    1.35 +function_hash_3.
    1.36 +*** true .          /* all conclusions proved */
    1.37 +
    1.38 +
    1.39 +For path(s) from start to run-time check associated with statement of line 173:
    1.40 +
    1.41 +function_hash_4.
    1.42 +*** true .          /* all conclusions proved */
    1.43 +
    1.44 +
    1.45 +For path(s) from start to run-time check associated with statement of line 174:
    1.46 +
    1.47 +function_hash_5.
    1.48 +*** true .          /* all conclusions proved */
    1.49 +
    1.50 +
    1.51 +For path(s) from start to run-time check associated with statement of line 175:
    1.52 +
    1.53 +function_hash_6.
    1.54 +*** true .          /* all conclusions proved */
    1.55 +
    1.56 +
    1.57 +For path(s) from start to run-time check associated with statement of line 175:
    1.58 +
    1.59 +function_hash_7.
    1.60 +*** true .          /* all conclusions proved */
    1.61 +
    1.62 +
    1.63 +For path(s) from start to run-time check associated with statement of line 177:
    1.64 +
    1.65 +function_hash_8.
    1.66 +*** true .          /* all conclusions proved */
    1.67 +
    1.68 +
    1.69 +For path(s) from assertion of line 178 to run-time check associated with 
    1.70 +          statement of line 177:
    1.71 +
    1.72 +function_hash_9.
    1.73 +*** true .          /* all conclusions proved */
    1.74 +
    1.75 +
    1.76 +For path(s) from start to run-time check associated with statement of line 177:
    1.77 +
    1.78 +function_hash_10.
    1.79 +*** true .          /* all conclusions proved */
    1.80 +
    1.81 +
    1.82 +For path(s) from assertion of line 178 to run-time check associated with 
    1.83 +          statement of line 177:
    1.84 +
    1.85 +function_hash_11.
    1.86 +*** true .          /* all conclusions proved */
    1.87 +
    1.88 +
    1.89 +For path(s) from start to assertion of line 178:
    1.90 +
    1.91 +function_hash_12.
    1.92 +H1:    x__index__subtype__1__first = 0 .
    1.93 +H2:    for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 
    1.94 +          integer, x__index__subtype__1__first <= i___1 and i___1 <= 
    1.95 +          x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
    1.96 +          i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
    1.97 +H3:    x__index__subtype__1__last >= 0 .
    1.98 +H4:    x__index__subtype__1__last <= 4294967296 .
    1.99 +H5:    x__index__subtype__1__first <= x__index__subtype__1__last .
   1.100 +H6:    mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
   1.101 +          ce__1) = round_spec(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 
   1.102 +          := 2562383102, h3 := 271733878, h4 := 3285377520), element(x, [
   1.103 +          x__index__subtype__1__first])) .
   1.104 +H7:    ca__1 >= 0 .
   1.105 +H8:    ca__1 <= 4294967295 .
   1.106 +H9:    cb__1 >= 0 .
   1.107 +H10:   cb__1 <= 4294967295 .
   1.108 +H11:   cc__1 >= 0 .
   1.109 +H12:   cc__1 <= 4294967295 .
   1.110 +H13:   cd__1 >= 0 .
   1.111 +H14:   cd__1 <= 4294967295 .
   1.112 +H15:   ce__1 >= 0 .
   1.113 +H16:   ce__1 <= 4294967295 .
   1.114 +       ->
   1.115 +C1:    mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
   1.116 +          ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 
   1.117 +          2562383102, h3 := 271733878, h4 := 3285377520), 
   1.118 +          x__index__subtype__1__first + 1, x) .
   1.119 +
   1.120 +
   1.121 +For path(s) from assertion of line 178 to assertion of line 178:
   1.122 +
   1.123 +function_hash_13.
   1.124 +H1:    mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds(
   1.125 +          mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 
   1.126 +          271733878, h4 := 3285377520), loop__1__i + 1, x) .
   1.127 +H2:    for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 
   1.128 +          integer, x__index__subtype__1__first <= i___1 and i___1 <= 
   1.129 +          x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
   1.130 +          i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
   1.131 +H3:    x__index__subtype__1__first = 0 .
   1.132 +H4:    loop__1__i >= 0 .
   1.133 +H5:    loop__1__i <= 4294967296 .
   1.134 +H6:    loop__1__i >= x__index__subtype__1__first .
   1.135 +H7:    ca >= 0 .
   1.136 +H8:    ca <= 4294967295 .
   1.137 +H9:    cb >= 0 .
   1.138 +H10:   cb <= 4294967295 .
   1.139 +H11:   cc >= 0 .
   1.140 +H12:   cc <= 4294967295 .
   1.141 +H13:   cd >= 0 .
   1.142 +H14:   cd <= 4294967295 .
   1.143 +H15:   ce >= 0 .
   1.144 +H16:   ce <= 4294967295 .
   1.145 +H17:   loop__1__i + 1 <= x__index__subtype__1__last .
   1.146 +H18:   mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
   1.147 +          ce__1) = round_spec(mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, 
   1.148 +          h4 := ce), element(x, [loop__1__i + 1])) .
   1.149 +H19:   ca__1 >= 0 .
   1.150 +H20:   ca__1 <= 4294967295 .
   1.151 +H21:   cb__1 >= 0 .
   1.152 +H22:   cb__1 <= 4294967295 .
   1.153 +H23:   cc__1 >= 0 .
   1.154 +H24:   cc__1 <= 4294967295 .
   1.155 +H25:   cd__1 >= 0 .
   1.156 +H26:   cd__1 <= 4294967295 .
   1.157 +H27:   ce__1 >= 0 .
   1.158 +H28:   ce__1 <= 4294967295 .
   1.159 +H29:   interfaces__unsigned_32__size >= 0 .
   1.160 +H30:   word__size >= 0 .
   1.161 +H31:   chain__size >= 0 .
   1.162 +H32:   block_index__size >= 0 .
   1.163 +H33:   block_index__base__first <= block_index__base__last .
   1.164 +H34:   message_index__size >= 0 .
   1.165 +H35:   message_index__base__first <= message_index__base__last .
   1.166 +H36:   x__index__subtype__1__first <= x__index__subtype__1__last .
   1.167 +H37:   block_index__base__first <= 0 .
   1.168 +H38:   block_index__base__last >= 15 .
   1.169 +H39:   message_index__base__first <= 0 .
   1.170 +H40:   x__index__subtype__1__first >= 0 .
   1.171 +H41:   x__index__subtype__1__last >= 0 .
   1.172 +H42:   message_index__base__last >= 4294967296 .
   1.173 +H43:   x__index__subtype__1__last <= 4294967296 .
   1.174 +H44:   x__index__subtype__1__first <= 4294967296 .
   1.175 +       ->
   1.176 +C1:    mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
   1.177 +          ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 
   1.178 +          2562383102, h3 := 271733878, h4 := 3285377520), loop__1__i + 2, x) .
   1.179 +
   1.180 +
   1.181 +For path(s) from start to run-time check associated with statement of line 183:
   1.182 +
   1.183 +function_hash_14.
   1.184 +*** true .          /* all conclusions proved */
   1.185 +
   1.186 +
   1.187 +For path(s) from assertion of line 178 to run-time check associated with 
   1.188 +          statement of line 183:
   1.189 +
   1.190 +function_hash_15.
   1.191 +*** true .          /* all conclusions proved */
   1.192 +
   1.193 +
   1.194 +For path(s) from start to finish:
   1.195 +
   1.196 +function_hash_16.
   1.197 +*** true .   /* contradiction within hypotheses. */
   1.198 +
   1.199 +
   1.200 +
   1.201 +For path(s) from assertion of line 178 to finish:
   1.202 +
   1.203 +function_hash_17.
   1.204 +H1:    mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds(
   1.205 +          mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 
   1.206 +          271733878, h4 := 3285377520), x__index__subtype__1__last + 1, x) .
   1.207 +H2:    for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 
   1.208 +          integer, x__index__subtype__1__first <= i___1 and i___1 <= 
   1.209 +          x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
   1.210 +          i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
   1.211 +H3:    x__index__subtype__1__first = 0 .
   1.212 +H4:    x__index__subtype__1__last >= 0 .
   1.213 +H5:    x__index__subtype__1__last <= 4294967296 .
   1.214 +H6:    x__index__subtype__1__last >= x__index__subtype__1__first .
   1.215 +H7:    ca >= 0 .
   1.216 +H8:    ca <= 4294967295 .
   1.217 +H9:    cb >= 0 .
   1.218 +H10:   cb <= 4294967295 .
   1.219 +H11:   cc >= 0 .
   1.220 +H12:   cc <= 4294967295 .
   1.221 +H13:   cd >= 0 .
   1.222 +H14:   cd <= 4294967295 .
   1.223 +H15:   ce >= 0 .
   1.224 +H16:   ce <= 4294967295 .
   1.225 +H17:   interfaces__unsigned_32__size >= 0 .
   1.226 +H18:   word__size >= 0 .
   1.227 +H19:   chain__size >= 0 .
   1.228 +H20:   block_index__size >= 0 .
   1.229 +H21:   block_index__base__first <= block_index__base__last .
   1.230 +H22:   message_index__size >= 0 .
   1.231 +H23:   message_index__base__first <= message_index__base__last .
   1.232 +H24:   x__index__subtype__1__first <= x__index__subtype__1__last .
   1.233 +H25:   block_index__base__first <= 0 .
   1.234 +H26:   block_index__base__last >= 15 .
   1.235 +H27:   message_index__base__first <= 0 .
   1.236 +H28:   x__index__subtype__1__first >= 0 .
   1.237 +H29:   message_index__base__last >= 4294967296 .
   1.238 +H30:   x__index__subtype__1__first <= 4294967296 .
   1.239 +       ->
   1.240 +C1:    mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rmd_hash(
   1.241 +          x, x__index__subtype__1__last + 1) .
   1.242 +
   1.243 +