src/HOL/SPARK/Examples/RIPEMD-160/rmd/round.rls
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/round.rls	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,77 @@
     1.4 +           /*********************************************************/
     1.5 +                           /*Proof Rule Declarations*/
     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 +                        /*DATE : 29-NOV-2010 14:30:19.87*/
    1.12 +
    1.13 +                            /*procedure RMD.Round*/
    1.14 +
    1.15 +
    1.16 +rule_family round_rules:
    1.17 +     X      requires [X:any] &
    1.18 +     X <= Y requires [X:ire, Y:ire] &
    1.19 +     X >= Y requires [X:ire, Y:ire].
    1.20 +
    1.21 +round_rules(1): integer__size >= 0 may_be_deduced.
    1.22 +round_rules(2): integer__first may_be_replaced_by -2147483648.
    1.23 +round_rules(3): integer__last may_be_replaced_by 2147483647.
    1.24 +round_rules(4): integer__base__first may_be_replaced_by -2147483648.
    1.25 +round_rules(5): integer__base__last may_be_replaced_by 2147483647.
    1.26 +round_rules(6): interfaces__unsigned_32__size >= 0 may_be_deduced.
    1.27 +round_rules(7): interfaces__unsigned_32__first may_be_replaced_by 0.
    1.28 +round_rules(8): interfaces__unsigned_32__last may_be_replaced_by 4294967295.
    1.29 +round_rules(9): interfaces__unsigned_32__base__first may_be_replaced_by 0.
    1.30 +round_rules(10): interfaces__unsigned_32__base__last may_be_replaced_by 4294967295.
    1.31 +round_rules(11): interfaces__unsigned_32__modulus may_be_replaced_by 4294967296.
    1.32 +round_rules(12): wordops__word__size >= 0 may_be_deduced.
    1.33 +round_rules(13): wordops__word__first may_be_replaced_by 0.
    1.34 +round_rules(14): wordops__word__last may_be_replaced_by 4294967295.
    1.35 +round_rules(15): wordops__word__base__first may_be_replaced_by 0.
    1.36 +round_rules(16): wordops__word__base__last may_be_replaced_by 4294967295.
    1.37 +round_rules(17): wordops__word__modulus may_be_replaced_by 4294967296.
    1.38 +round_rules(18): wordops__rotate_amount__size >= 0 may_be_deduced.
    1.39 +round_rules(19): wordops__rotate_amount__first may_be_replaced_by 0.
    1.40 +round_rules(20): wordops__rotate_amount__last may_be_replaced_by 15.
    1.41 +round_rules(21): wordops__rotate_amount__base__first may_be_replaced_by -2147483648.
    1.42 +round_rules(22): wordops__rotate_amount__base__last may_be_replaced_by 2147483647.
    1.43 +round_rules(23): word__size >= 0 may_be_deduced.
    1.44 +round_rules(24): word__first may_be_replaced_by 0.
    1.45 +round_rules(25): word__last may_be_replaced_by 4294967295.
    1.46 +round_rules(26): word__base__first may_be_replaced_by 0.
    1.47 +round_rules(27): word__base__last may_be_replaced_by 4294967295.
    1.48 +round_rules(28): word__modulus may_be_replaced_by 4294967296.
    1.49 +round_rules(29): chain__size >= 0 may_be_deduced.
    1.50 +round_rules(30): A = B may_be_deduced_from
    1.51 +     [goal(checktype(A,chain)),
    1.52 +      goal(checktype(B,chain)),
    1.53 +      fld_h0(A) = fld_h0(B),
    1.54 +      fld_h1(A) = fld_h1(B),
    1.55 +      fld_h2(A) = fld_h2(B),
    1.56 +      fld_h3(A) = fld_h3(B),
    1.57 +      fld_h4(A) = fld_h4(B)].
    1.58 +round_rules(31): block_index__size >= 0 may_be_deduced.
    1.59 +round_rules(32): block_index__first may_be_replaced_by 0.
    1.60 +round_rules(33): block_index__last may_be_replaced_by 15.
    1.61 +round_rules(34): block_index__base__first <= block_index__base__last may_be_deduced.
    1.62 +round_rules(35): block_index__base__first <= block_index__first may_be_deduced.
    1.63 +round_rules(36): block_index__base__last >= block_index__last may_be_deduced.
    1.64 +round_rules(37): round_index__size >= 0 may_be_deduced.
    1.65 +round_rules(38): round_index__first may_be_replaced_by 0.
    1.66 +round_rules(39): round_index__last may_be_replaced_by 79.
    1.67 +round_rules(40): round_index__base__first <= round_index__base__last may_be_deduced.
    1.68 +round_rules(41): round_index__base__first <= round_index__first may_be_deduced.
    1.69 +round_rules(42): round_index__base__last >= round_index__last may_be_deduced.
    1.70 +round_rules(43): chain_pair__size >= 0 may_be_deduced.
    1.71 +round_rules(44): A = B may_be_deduced_from
    1.72 +     [goal(checktype(A,chain_pair)),
    1.73 +      goal(checktype(B,chain_pair)),
    1.74 +      fld_left(A) = fld_left(B),
    1.75 +      fld_right(A) = fld_right(B)].
    1.76 +round_rules(45): rotate_amount__size >= 0 may_be_deduced.
    1.77 +round_rules(46): rotate_amount__first may_be_replaced_by 0.
    1.78 +round_rules(47): rotate_amount__last may_be_replaced_by 15.
    1.79 +round_rules(48): rotate_amount__base__first may_be_replaced_by -2147483648.
    1.80 +round_rules(49): rotate_amount__base__last may_be_replaced_by 2147483647.