src/HOL/SPARK/Examples/RIPEMD-160/rmd/hash.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/hash.rls	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,61 @@
     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:20.17*/
    1.12 +
    1.13 +                             /*function RMD.Hash*/
    1.14 +
    1.15 +
    1.16 +rule_family hash_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 +hash_rules(1): ca_init may_be_replaced_by 1732584193.
    1.22 +hash_rules(2): cb_init may_be_replaced_by 4023233417.
    1.23 +hash_rules(3): cc_init may_be_replaced_by 2562383102.
    1.24 +hash_rules(4): cd_init may_be_replaced_by 271733878.
    1.25 +hash_rules(5): ce_init may_be_replaced_by 3285377520.
    1.26 +hash_rules(6): interfaces__unsigned_32__size >= 0 may_be_deduced.
    1.27 +hash_rules(7): interfaces__unsigned_32__first may_be_replaced_by 0.
    1.28 +hash_rules(8): interfaces__unsigned_32__last may_be_replaced_by 4294967295.
    1.29 +hash_rules(9): interfaces__unsigned_32__base__first may_be_replaced_by 0.
    1.30 +hash_rules(10): interfaces__unsigned_32__base__last may_be_replaced_by 4294967295.
    1.31 +hash_rules(11): interfaces__unsigned_32__modulus may_be_replaced_by 4294967296.
    1.32 +hash_rules(12): word__size >= 0 may_be_deduced.
    1.33 +hash_rules(13): word__first may_be_replaced_by 0.
    1.34 +hash_rules(14): word__last may_be_replaced_by 4294967295.
    1.35 +hash_rules(15): word__base__first may_be_replaced_by 0.
    1.36 +hash_rules(16): word__base__last may_be_replaced_by 4294967295.
    1.37 +hash_rules(17): word__modulus may_be_replaced_by 4294967296.
    1.38 +hash_rules(18): chain__size >= 0 may_be_deduced.
    1.39 +hash_rules(19): A = B may_be_deduced_from
    1.40 +     [goal(checktype(A,chain)),
    1.41 +      goal(checktype(B,chain)),
    1.42 +      fld_h0(A) = fld_h0(B),
    1.43 +      fld_h1(A) = fld_h1(B),
    1.44 +      fld_h2(A) = fld_h2(B),
    1.45 +      fld_h3(A) = fld_h3(B),
    1.46 +      fld_h4(A) = fld_h4(B)].
    1.47 +hash_rules(20): block_index__size >= 0 may_be_deduced.
    1.48 +hash_rules(21): block_index__first may_be_replaced_by 0.
    1.49 +hash_rules(22): block_index__last may_be_replaced_by 15.
    1.50 +hash_rules(23): block_index__base__first <= block_index__base__last may_be_deduced.
    1.51 +hash_rules(24): block_index__base__first <= block_index__first may_be_deduced.
    1.52 +hash_rules(25): block_index__base__last >= block_index__last may_be_deduced.
    1.53 +hash_rules(26): message_index__size >= 0 may_be_deduced.
    1.54 +hash_rules(27): message_index__first may_be_replaced_by 0.
    1.55 +hash_rules(28): message_index__last may_be_replaced_by 4294967296.
    1.56 +hash_rules(29): message_index__base__first <= message_index__base__last may_be_deduced.
    1.57 +hash_rules(30): message_index__base__first <= message_index__first may_be_deduced.
    1.58 +hash_rules(31): message_index__base__last >= message_index__last may_be_deduced.
    1.59 +hash_rules(32): x__index__subtype__1__first >= message_index__first may_be_deduced.
    1.60 +hash_rules(33): x__index__subtype__1__last <= message_index__last may_be_deduced.
    1.61 +hash_rules(34): x__index__subtype__1__first <= 
    1.62 +     x__index__subtype__1__last may_be_deduced.
    1.63 +hash_rules(35): x__index__subtype__1__last >= message_index__first may_be_deduced.
    1.64 +hash_rules(36): x__index__subtype__1__first <= message_index__last may_be_deduced.