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

tuned messages;

*****************************************************************************
                       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:28

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

function RMD.K_L




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

function_k_l_1.
*** true .          /* all conclusions proved */


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

function_k_l_2.
*** true .          /* all conclusions proved */


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

function_k_l_3.
*** true .          /* all conclusions proved */


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

function_k_l_4.
*** true .          /* all conclusions proved */


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

function_k_l_5.
*** true .          /* all conclusions proved */


For path(s) from start to finish:

function_k_l_6.
H1:    j >= 0 .
H2:    j <= 15 .
H3:    interfaces__unsigned_32__size >= 0 .
H4:    word__size >= 0 .
H5:    round_index__size >= 0 .
H6:    round_index__base__first <= round_index__base__last .
H7:    round_index__base__first <= 0 .
H8:    round_index__base__last >= 79 .
       ->
C1:    0 = k_l_spec(j) .


function_k_l_7.
H1:    16 <= j .
H2:    j <= 31 .
H3:    interfaces__unsigned_32__size >= 0 .
H4:    word__size >= 0 .
H5:    round_index__size >= 0 .
H6:    round_index__base__first <= round_index__base__last .
H7:    round_index__base__first <= 0 .
H8:    round_index__base__last >= 79 .
       ->
C1:    1518500249 = k_l_spec(j) .


function_k_l_8.
H1:    32 <= j .
H2:    j <= 47 .
H3:    interfaces__unsigned_32__size >= 0 .
H4:    word__size >= 0 .
H5:    round_index__size >= 0 .
H6:    round_index__base__first <= round_index__base__last .
H7:    round_index__base__first <= 0 .
H8:    round_index__base__last >= 79 .
       ->
C1:    1859775393 = k_l_spec(j) .


function_k_l_9.
H1:    48 <= j .
H2:    j <= 63 .
H3:    interfaces__unsigned_32__size >= 0 .
H4:    word__size >= 0 .
H5:    round_index__size >= 0 .
H6:    round_index__base__first <= round_index__base__last .
H7:    round_index__base__first <= 0 .
H8:    round_index__base__last >= 79 .
       ->
C1:    2400959708 = k_l_spec(j) .


function_k_l_10.
H1:    j >= 0 .
H2:    j <= 79 .
H3:    15 < j .
H4:    31 < j .
H5:    47 < j .
H6:    63 < j .
H7:    interfaces__unsigned_32__size >= 0 .
H8:    word__size >= 0 .
H9:    round_index__size >= 0 .
H10:   round_index__base__first <= round_index__base__last .
H11:   round_index__base__first <= 0 .
H12:   round_index__base__last >= 79 .
       ->
C1:    2840853838 = k_l_spec(j) .