src/HOL/SPARK/Examples/RIPEMD-160/rmd/s_r.siv

tuned;

*****************************************************************************
                       Semantic Analysis of SPARK Text
    Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
             Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
*****************************************************************************


CREATED 29-NOV-2010, 14:30:19  SIMPLIFIED 29-NOV-2010, 14:30:30

SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.

function RMD.S_R




For path(s) from start to run-time check associated with statement of line 101:

function_s_r_1.
*** true .          /* all conclusions proved */


For path(s) from start to finish:

function_s_r_2.
H1:    j >= 0 .
H2:    j <= 79 .
H3:    integer__size >= 0 .
H4:    round_index__size >= 0 .
H5:    round_index__base__first <= round_index__base__last .
H6:    rotate_amount__size >= 0 .
H7:    round_index__base__first <= 0 .
H8:    round_index__base__last >= 79 .
       ->
C1:    element(mk__rotate_definition([0] := 8, [1] := 9, [2] := 9, [3] := 11, [
          4] := 13, [5] := 15, [6] := 15, [7] := 5, [8] := 7, [9] := 7, [10] := 
          8, [11] := 11, [12] := 14, [13] := 14, [14] := 12, [15] := 6, [16] := 
          9, [17] := 13, [18] := 15, [19] := 7, [20] := 12, [21] := 8, [22] := 
          9, [23] := 11, [24] := 7, [25] := 7, [26] := 12, [27] := 7, [28] := 
          6, [29] := 15, [30] := 13, [31] := 11, [32] := 9, [33] := 7, [34] := 
          15, [35] := 11, [36] := 8, [37] := 6, [38] := 6, [39] := 14, [40] := 
          12, [41] := 13, [42] := 5, [43] := 14, [44] := 13, [45] := 13, [46] 
          := 7, [47] := 5, [48] := 15, [49] := 5, [50] := 8, [51] := 11, [52] 
          := 14, [53] := 14, [54] := 6, [55] := 14, [56] := 6, [57] := 9, [58] 
          := 12, [59] := 9, [60] := 12, [61] := 5, [62] := 15, [63] := 8, [64] 
          := 8, [65] := 5, [66] := 12, [67] := 9, [68] := 12, [69] := 5, [70] 
          := 14, [71] := 6, [72] := 8, [73] := 13, [74] := 6, [75] := 5, [76] 
          := 15, [77] := 13, [78] := 11, [79] := 11), [j]) = s_r_spec(j) .
C2:    element(mk__rotate_definition([0] := 8, [1] := 9, [2] := 9, [3] := 11, [
          4] := 13, [5] := 15, [6] := 15, [7] := 5, [8] := 7, [9] := 7, [10] := 
          8, [11] := 11, [12] := 14, [13] := 14, [14] := 12, [15] := 6, [16] := 
          9, [17] := 13, [18] := 15, [19] := 7, [20] := 12, [21] := 8, [22] := 
          9, [23] := 11, [24] := 7, [25] := 7, [26] := 12, [27] := 7, [28] := 
          6, [29] := 15, [30] := 13, [31] := 11, [32] := 9, [33] := 7, [34] := 
          15, [35] := 11, [36] := 8, [37] := 6, [38] := 6, [39] := 14, [40] := 
          12, [41] := 13, [42] := 5, [43] := 14, [44] := 13, [45] := 13, [46] 
          := 7, [47] := 5, [48] := 15, [49] := 5, [50] := 8, [51] := 11, [52] 
          := 14, [53] := 14, [54] := 6, [55] := 14, [56] := 6, [57] := 9, [58] 
          := 12, [59] := 9, [60] := 12, [61] := 5, [62] := 15, [63] := 8, [64] 
          := 8, [65] := 5, [66] := 12, [67] := 9, [68] := 12, [69] := 5, [70] 
          := 14, [71] := 6, [72] := 8, [73] := 13, [74] := 6, [75] := 5, [76] 
          := 15, [77] := 13, [78] := 11, [79] := 11), [j]) >= 0 .
C3:    element(mk__rotate_definition([0] := 8, [1] := 9, [2] := 9, [3] := 11, [
          4] := 13, [5] := 15, [6] := 15, [7] := 5, [8] := 7, [9] := 7, [10] := 
          8, [11] := 11, [12] := 14, [13] := 14, [14] := 12, [15] := 6, [16] := 
          9, [17] := 13, [18] := 15, [19] := 7, [20] := 12, [21] := 8, [22] := 
          9, [23] := 11, [24] := 7, [25] := 7, [26] := 12, [27] := 7, [28] := 
          6, [29] := 15, [30] := 13, [31] := 11, [32] := 9, [33] := 7, [34] := 
          15, [35] := 11, [36] := 8, [37] := 6, [38] := 6, [39] := 14, [40] := 
          12, [41] := 13, [42] := 5, [43] := 14, [44] := 13, [45] := 13, [46] 
          := 7, [47] := 5, [48] := 15, [49] := 5, [50] := 8, [51] := 11, [52] 
          := 14, [53] := 14, [54] := 6, [55] := 14, [56] := 6, [57] := 9, [58] 
          := 12, [59] := 9, [60] := 12, [61] := 5, [62] := 15, [63] := 8, [64] 
          := 8, [65] := 5, [66] := 12, [67] := 9, [68] := 12, [69] := 5, [70] 
          := 14, [71] := 6, [72] := 8, [73] := 13, [74] := 6, [75] := 5, [76] 
          := 15, [77] := 13, [78] := 11, [79] := 11), [j]) <= 15 .