src/HOL/SPARK/Examples/RIPEMD-160/rmd/f.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/f.siv	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,228 @@
     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:19  SIMPLIFIED 29-NOV-2010, 14:30:28
    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.F
    1.17 +
    1.18 +
    1.19 +
    1.20 +
    1.21 +For path(s) from start to run-time check associated with statement of line 9:
    1.22 +
    1.23 +function_f_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 10:
    1.28 +
    1.29 +function_f_2.
    1.30 +H1:    x >= 0 .
    1.31 +H2:    x <= 4294967295 .
    1.32 +H3:    y >= 0 .
    1.33 +H4:    y <= 4294967295 .
    1.34 +H5:    z >= 0 .
    1.35 +H6:    z <= 4294967295 .
    1.36 +H7:    16 <= j .
    1.37 +H8:    j <= 31 .
    1.38 +H9:    interfaces__unsigned_32__size >= 0 .
    1.39 +H10:   word__size >= 0 .
    1.40 +H11:   round_index__size >= 0 .
    1.41 +H12:   round_index__base__first <= round_index__base__last .
    1.42 +H13:   round_index__base__first <= 0 .
    1.43 +H14:   round_index__base__last >= 79 .
    1.44 +       ->
    1.45 +C1:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) >= 0 .
    1.46 +C2:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) <= 4294967295 .
    1.47 +
    1.48 +
    1.49 +For path(s) from start to run-time check associated with statement of line 11:
    1.50 +
    1.51 +function_f_3.
    1.52 +H1:    x >= 0 .
    1.53 +H2:    x <= 4294967295 .
    1.54 +H3:    y >= 0 .
    1.55 +H4:    y <= 4294967295 .
    1.56 +H5:    z >= 0 .
    1.57 +H6:    z <= 4294967295 .
    1.58 +H7:    32 <= j .
    1.59 +H8:    j <= 47 .
    1.60 +H9:    interfaces__unsigned_32__size >= 0 .
    1.61 +H10:   word__size >= 0 .
    1.62 +H11:   round_index__size >= 0 .
    1.63 +H12:   round_index__base__first <= round_index__base__last .
    1.64 +H13:   round_index__base__first <= 0 .
    1.65 +H14:   round_index__base__last >= 79 .
    1.66 +       ->
    1.67 +C1:    bit__xor(bit__or(x, 4294967295 - y), z) >= 0 .
    1.68 +C2:    bit__xor(bit__or(x, 4294967295 - y), z) <= 4294967295 .
    1.69 +
    1.70 +
    1.71 +For path(s) from start to run-time check associated with statement of line 12:
    1.72 +
    1.73 +function_f_4.
    1.74 +H1:    x >= 0 .
    1.75 +H2:    x <= 4294967295 .
    1.76 +H3:    y >= 0 .
    1.77 +H4:    y <= 4294967295 .
    1.78 +H5:    z >= 0 .
    1.79 +H6:    z <= 4294967295 .
    1.80 +H7:    48 <= j .
    1.81 +H8:    j <= 63 .
    1.82 +H9:    interfaces__unsigned_32__size >= 0 .
    1.83 +H10:   word__size >= 0 .
    1.84 +H11:   round_index__size >= 0 .
    1.85 +H12:   round_index__base__first <= round_index__base__last .
    1.86 +H13:   round_index__base__first <= 0 .
    1.87 +H14:   round_index__base__last >= 79 .
    1.88 +       ->
    1.89 +C1:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) >= 0 .
    1.90 +C2:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) <= 4294967295 .
    1.91 +
    1.92 +
    1.93 +For path(s) from start to run-time check associated with statement of line 13:
    1.94 +
    1.95 +function_f_5.
    1.96 +H1:    j >= 0 .
    1.97 +H2:    j <= 79 .
    1.98 +H3:    x >= 0 .
    1.99 +H4:    x <= 4294967295 .
   1.100 +H5:    y >= 0 .
   1.101 +H6:    y <= 4294967295 .
   1.102 +H7:    z >= 0 .
   1.103 +H8:    z <= 4294967295 .
   1.104 +H9:    15 < j .
   1.105 +H10:   31 < j .
   1.106 +H11:   47 < j .
   1.107 +H12:   63 < j .
   1.108 +H13:   interfaces__unsigned_32__size >= 0 .
   1.109 +H14:   word__size >= 0 .
   1.110 +H15:   round_index__size >= 0 .
   1.111 +H16:   round_index__base__first <= round_index__base__last .
   1.112 +H17:   round_index__base__first <= 0 .
   1.113 +H18:   round_index__base__last >= 79 .
   1.114 +       ->
   1.115 +C1:    bit__xor(x, bit__or(y, 4294967295 - z)) >= 0 .
   1.116 +C2:    bit__xor(x, bit__or(y, 4294967295 - z)) <= 4294967295 .
   1.117 +
   1.118 +
   1.119 +For path(s) from start to finish:
   1.120 +
   1.121 +function_f_6.
   1.122 +H1:    j >= 0 .
   1.123 +H2:    x >= 0 .
   1.124 +H3:    x <= 4294967295 .
   1.125 +H4:    y >= 0 .
   1.126 +H5:    y <= 4294967295 .
   1.127 +H6:    z >= 0 .
   1.128 +H7:    z <= 4294967295 .
   1.129 +H8:    j <= 15 .
   1.130 +H9:    bit__xor(x, bit__xor(y, z)) >= 0 .
   1.131 +H10:   bit__xor(x, bit__xor(y, z)) <= 4294967295 .
   1.132 +H11:   interfaces__unsigned_32__size >= 0 .
   1.133 +H12:   word__size >= 0 .
   1.134 +H13:   round_index__size >= 0 .
   1.135 +H14:   round_index__base__first <= round_index__base__last .
   1.136 +H15:   round_index__base__first <= 0 .
   1.137 +H16:   round_index__base__last >= 79 .
   1.138 +       ->
   1.139 +C1:    bit__xor(x, bit__xor(y, z)) = f_spec(j, x, y, z) .
   1.140 +
   1.141 +
   1.142 +function_f_7.
   1.143 +H1:    x >= 0 .
   1.144 +H2:    x <= 4294967295 .
   1.145 +H3:    y >= 0 .
   1.146 +H4:    y <= 4294967295 .
   1.147 +H5:    z >= 0 .
   1.148 +H6:    z <= 4294967295 .
   1.149 +H7:    16 <= j .
   1.150 +H8:    j <= 31 .
   1.151 +H9:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) >= 0 .
   1.152 +H10:   bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) <= 4294967295 .
   1.153 +H11:   interfaces__unsigned_32__size >= 0 .
   1.154 +H12:   word__size >= 0 .
   1.155 +H13:   round_index__size >= 0 .
   1.156 +H14:   round_index__base__first <= round_index__base__last .
   1.157 +H15:   round_index__base__first <= 0 .
   1.158 +H16:   round_index__base__last >= 79 .
   1.159 +       ->
   1.160 +C1:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) = f_spec(j, x, y, z)
   1.161 +           .
   1.162 +
   1.163 +
   1.164 +function_f_8.
   1.165 +H1:    x >= 0 .
   1.166 +H2:    x <= 4294967295 .
   1.167 +H3:    y >= 0 .
   1.168 +H4:    y <= 4294967295 .
   1.169 +H5:    z >= 0 .
   1.170 +H6:    z <= 4294967295 .
   1.171 +H7:    32 <= j .
   1.172 +H8:    j <= 47 .
   1.173 +H9:    bit__xor(bit__or(x, 4294967295 - y), z) >= 0 .
   1.174 +H10:   bit__xor(bit__or(x, 4294967295 - y), z) <= 4294967295 .
   1.175 +H11:   interfaces__unsigned_32__size >= 0 .
   1.176 +H12:   word__size >= 0 .
   1.177 +H13:   round_index__size >= 0 .
   1.178 +H14:   round_index__base__first <= round_index__base__last .
   1.179 +H15:   round_index__base__first <= 0 .
   1.180 +H16:   round_index__base__last >= 79 .
   1.181 +       ->
   1.182 +C1:    bit__xor(bit__or(x, 4294967295 - y), z) = f_spec(j, x, y, z) .
   1.183 +
   1.184 +
   1.185 +function_f_9.
   1.186 +H1:    x >= 0 .
   1.187 +H2:    x <= 4294967295 .
   1.188 +H3:    y >= 0 .
   1.189 +H4:    y <= 4294967295 .
   1.190 +H5:    z >= 0 .
   1.191 +H6:    z <= 4294967295 .
   1.192 +H7:    48 <= j .
   1.193 +H8:    j <= 63 .
   1.194 +H9:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) >= 0 .
   1.195 +H10:   bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) <= 4294967295 .
   1.196 +H11:   interfaces__unsigned_32__size >= 0 .
   1.197 +H12:   word__size >= 0 .
   1.198 +H13:   round_index__size >= 0 .
   1.199 +H14:   round_index__base__first <= round_index__base__last .
   1.200 +H15:   round_index__base__first <= 0 .
   1.201 +H16:   round_index__base__last >= 79 .
   1.202 +       ->
   1.203 +C1:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) = f_spec(j, x, y, z)
   1.204 +           .
   1.205 +
   1.206 +
   1.207 +function_f_10.
   1.208 +H1:    j >= 0 .
   1.209 +H2:    j <= 79 .
   1.210 +H3:    x >= 0 .
   1.211 +H4:    x <= 4294967295 .
   1.212 +H5:    y >= 0 .
   1.213 +H6:    y <= 4294967295 .
   1.214 +H7:    z >= 0 .
   1.215 +H8:    z <= 4294967295 .
   1.216 +H9:    15 < j .
   1.217 +H10:   31 < j .
   1.218 +H11:   47 < j .
   1.219 +H12:   63 < j .
   1.220 +H13:   bit__xor(x, bit__or(y, 4294967295 - z)) >= 0 .
   1.221 +H14:   bit__xor(x, bit__or(y, 4294967295 - z)) <= 4294967295 .
   1.222 +H15:   interfaces__unsigned_32__size >= 0 .
   1.223 +H16:   word__size >= 0 .
   1.224 +H17:   round_index__size >= 0 .
   1.225 +H18:   round_index__base__first <= round_index__base__last .
   1.226 +H19:   round_index__base__first <= 0 .
   1.227 +H20:   round_index__base__last >= 79 .
   1.228 +       ->
   1.229 +C1:    bit__xor(x, bit__or(y, 4294967295 - z)) = f_spec(j, x, y, z) .
   1.230 +
   1.231 +