1 /*********************************************************/ 2 /*Proof Rule Declarations*/ 3 /*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/ 4 /*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/ 5 /*********************************************************/ 6 7 8 /*DATE : 29-NOV-2010 14:30:19.84*/ 9 10 /*function RMD.S_R*/ 11 12 13rule_family s_r_rules: 14 X requires [X:any] & 15 X <= Y requires [X:ire, Y:ire] & 16 X >= Y requires [X:ire, Y:ire]. 17 18s_r_rules(1): rotate_amount__first <= element(s_values, [I]) may_be_deduced_from [0 <= I, I <= 79]. 19s_r_rules(2): element(s_values, [I]) <= rotate_amount__last may_be_deduced_from [0 <= I, I <= 79]. 20s_r_rules(3): s_values may_be_replaced_by 21 mk__rotate_definition([round_index__first] := 8, [ 22 round_index__first + 1] := 9, [round_index__first + 2] := 9, [ 23 round_index__first + 3] := 11, [round_index__first + 4] := 24 13, [round_index__first + 5] := 15, [round_index__first + 6] := 25 15, [round_index__first + 7] := 5, [round_index__first + 8] := 26 7, [round_index__first + 9] := 7, [round_index__first + 10] := 27 8, [round_index__first + 11] := 11, [round_index__first + 12] := 28 14, [round_index__first + 13] := 14, [ 29 round_index__first + 14] := 12, [round_index__first + 15] := 30 6, [round_index__first + 16] := 9, [round_index__first + 17] := 31 13, [round_index__first + 18] := 15, [ 32 round_index__first + 19] := 7, [round_index__first + 20] := 33 12, [round_index__first + 21] := 8, [round_index__first + 22] := 34 9, [round_index__first + 23] := 11, [round_index__first + 24] := 35 7, [round_index__first + 25] := 7, [round_index__first + 26] := 36 12, [round_index__first + 27] := 7, [round_index__first + 28] := 37 6, [round_index__first + 29] := 15, [round_index__first + 30] := 38 13, [round_index__first + 31] := 11, [ 39 round_index__first + 32] := 9, [round_index__first + 33] := 40 7, [round_index__first + 34] := 15, [round_index__first + 35] := 41 11, [round_index__first + 36] := 8, [round_index__first + 37] := 42 6, [round_index__first + 38] := 6, [round_index__first + 39] := 43 14, [round_index__first + 40] := 12, [ 44 round_index__first + 41] := 13, [round_index__first + 42] := 45 5, [round_index__first + 43] := 14, [round_index__first + 44] := 46 13, [round_index__first + 45] := 13, [ 47 round_index__first + 46] := 7, [round_index__first + 47] := 48 5, [round_index__first + 48] := 15, [round_index__first + 49] := 49 5, [round_index__first + 50] := 8, [round_index__first + 51] := 50 11, [round_index__first + 52] := 14, [ 51 round_index__first + 53] := 14, [round_index__first + 54] := 52 6, [round_index__first + 55] := 14, [round_index__first + 56] := 53 6, [round_index__first + 57] := 9, [round_index__first + 58] := 54 12, [round_index__first + 59] := 9, [round_index__first + 60] := 55 12, [round_index__first + 61] := 5, [round_index__first + 62] := 56 15, [round_index__first + 63] := 8, [round_index__first + 64] := 57 8, [round_index__first + 65] := 5, [round_index__first + 66] := 58 12, [round_index__first + 67] := 9, [round_index__first + 68] := 59 12, [round_index__first + 69] := 5, [round_index__first + 70] := 60 14, [round_index__first + 71] := 6, [round_index__first + 72] := 61 8, [round_index__first + 73] := 13, [round_index__first + 74] := 62 6, [round_index__first + 75] := 5, [round_index__first + 76] := 63 15, [round_index__first + 77] := 13, [ 64 round_index__first + 78] := 11, [round_index__first + 79] := 65 11). 66s_r_rules(4): integer__size >= 0 may_be_deduced. 67s_r_rules(5): integer__first may_be_replaced_by -2147483648. 68s_r_rules(6): integer__last may_be_replaced_by 2147483647. 69s_r_rules(7): integer__base__first may_be_replaced_by -2147483648. 70s_r_rules(8): integer__base__last may_be_replaced_by 2147483647. 71s_r_rules(9): round_index__size >= 0 may_be_deduced. 72s_r_rules(10): round_index__first may_be_replaced_by 0. 73s_r_rules(11): round_index__last may_be_replaced_by 79. 74s_r_rules(12): round_index__base__first <= round_index__base__last may_be_deduced. 75s_r_rules(13): round_index__base__first <= round_index__first may_be_deduced. 76s_r_rules(14): round_index__base__last >= round_index__last may_be_deduced. 77s_r_rules(15): rotate_amount__size >= 0 may_be_deduced. 78s_r_rules(16): rotate_amount__first may_be_replaced_by 0. 79s_r_rules(17): rotate_amount__last may_be_replaced_by 15. 80s_r_rules(18): rotate_amount__base__first may_be_replaced_by -2147483648. 81s_r_rules(19): rotate_amount__base__last may_be_replaced_by 2147483647. 82