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

more robust;

*****************************************************************************
                       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.F




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

function_f_1.
*** true .          /* all conclusions proved */


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

function_f_2.
H1:    x >= 0 .
H2:    x <= 4294967295 .
H3:    y >= 0 .
H4:    y <= 4294967295 .
H5:    z >= 0 .
H6:    z <= 4294967295 .
H7:    16 <= j .
H8:    j <= 31 .
H9:    interfaces__unsigned_32__size >= 0 .
H10:   word__size >= 0 .
H11:   round_index__size >= 0 .
H12:   round_index__base__first <= round_index__base__last .
H13:   round_index__base__first <= 0 .
H14:   round_index__base__last >= 79 .
       ->
C1:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) >= 0 .
C2:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) <= 4294967295 .


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

function_f_3.
H1:    x >= 0 .
H2:    x <= 4294967295 .
H3:    y >= 0 .
H4:    y <= 4294967295 .
H5:    z >= 0 .
H6:    z <= 4294967295 .
H7:    32 <= j .
H8:    j <= 47 .
H9:    interfaces__unsigned_32__size >= 0 .
H10:   word__size >= 0 .
H11:   round_index__size >= 0 .
H12:   round_index__base__first <= round_index__base__last .
H13:   round_index__base__first <= 0 .
H14:   round_index__base__last >= 79 .
       ->
C1:    bit__xor(bit__or(x, 4294967295 - y), z) >= 0 .
C2:    bit__xor(bit__or(x, 4294967295 - y), z) <= 4294967295 .


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

function_f_4.
H1:    x >= 0 .
H2:    x <= 4294967295 .
H3:    y >= 0 .
H4:    y <= 4294967295 .
H5:    z >= 0 .
H6:    z <= 4294967295 .
H7:    48 <= j .
H8:    j <= 63 .
H9:    interfaces__unsigned_32__size >= 0 .
H10:   word__size >= 0 .
H11:   round_index__size >= 0 .
H12:   round_index__base__first <= round_index__base__last .
H13:   round_index__base__first <= 0 .
H14:   round_index__base__last >= 79 .
       ->
C1:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) >= 0 .
C2:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) <= 4294967295 .


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

function_f_5.
H1:    j >= 0 .
H2:    j <= 79 .
H3:    x >= 0 .
H4:    x <= 4294967295 .
H5:    y >= 0 .
H6:    y <= 4294967295 .
H7:    z >= 0 .
H8:    z <= 4294967295 .
H9:    15 < j .
H10:   31 < j .
H11:   47 < j .
H12:   63 < j .
H13:   interfaces__unsigned_32__size >= 0 .
H14:   word__size >= 0 .
H15:   round_index__size >= 0 .
H16:   round_index__base__first <= round_index__base__last .
H17:   round_index__base__first <= 0 .
H18:   round_index__base__last >= 79 .
       ->
C1:    bit__xor(x, bit__or(y, 4294967295 - z)) >= 0 .
C2:    bit__xor(x, bit__or(y, 4294967295 - z)) <= 4294967295 .


For path(s) from start to finish:

function_f_6.
H1:    j >= 0 .
H2:    x >= 0 .
H3:    x <= 4294967295 .
H4:    y >= 0 .
H5:    y <= 4294967295 .
H6:    z >= 0 .
H7:    z <= 4294967295 .
H8:    j <= 15 .
H9:    bit__xor(x, bit__xor(y, z)) >= 0 .
H10:   bit__xor(x, bit__xor(y, z)) <= 4294967295 .
H11:   interfaces__unsigned_32__size >= 0 .
H12:   word__size >= 0 .
H13:   round_index__size >= 0 .
H14:   round_index__base__first <= round_index__base__last .
H15:   round_index__base__first <= 0 .
H16:   round_index__base__last >= 79 .
       ->
C1:    bit__xor(x, bit__xor(y, z)) = f_spec(j, x, y, z) .


function_f_7.
H1:    x >= 0 .
H2:    x <= 4294967295 .
H3:    y >= 0 .
H4:    y <= 4294967295 .
H5:    z >= 0 .
H6:    z <= 4294967295 .
H7:    16 <= j .
H8:    j <= 31 .
H9:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) >= 0 .
H10:   bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) <= 4294967295 .
H11:   interfaces__unsigned_32__size >= 0 .
H12:   word__size >= 0 .
H13:   round_index__size >= 0 .
H14:   round_index__base__first <= round_index__base__last .
H15:   round_index__base__first <= 0 .
H16:   round_index__base__last >= 79 .
       ->
C1:    bit__or(bit__and(x, y), bit__and(4294967295 - x, z)) = f_spec(j, x, y, z)
           .


function_f_8.
H1:    x >= 0 .
H2:    x <= 4294967295 .
H3:    y >= 0 .
H4:    y <= 4294967295 .
H5:    z >= 0 .
H6:    z <= 4294967295 .
H7:    32 <= j .
H8:    j <= 47 .
H9:    bit__xor(bit__or(x, 4294967295 - y), z) >= 0 .
H10:   bit__xor(bit__or(x, 4294967295 - y), z) <= 4294967295 .
H11:   interfaces__unsigned_32__size >= 0 .
H12:   word__size >= 0 .
H13:   round_index__size >= 0 .
H14:   round_index__base__first <= round_index__base__last .
H15:   round_index__base__first <= 0 .
H16:   round_index__base__last >= 79 .
       ->
C1:    bit__xor(bit__or(x, 4294967295 - y), z) = f_spec(j, x, y, z) .


function_f_9.
H1:    x >= 0 .
H2:    x <= 4294967295 .
H3:    y >= 0 .
H4:    y <= 4294967295 .
H5:    z >= 0 .
H6:    z <= 4294967295 .
H7:    48 <= j .
H8:    j <= 63 .
H9:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) >= 0 .
H10:   bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) <= 4294967295 .
H11:   interfaces__unsigned_32__size >= 0 .
H12:   word__size >= 0 .
H13:   round_index__size >= 0 .
H14:   round_index__base__first <= round_index__base__last .
H15:   round_index__base__first <= 0 .
H16:   round_index__base__last >= 79 .
       ->
C1:    bit__or(bit__and(x, z), bit__and(y, 4294967295 - z)) = f_spec(j, x, y, z)
           .


function_f_10.
H1:    j >= 0 .
H2:    j <= 79 .
H3:    x >= 0 .
H4:    x <= 4294967295 .
H5:    y >= 0 .
H6:    y <= 4294967295 .
H7:    z >= 0 .
H8:    z <= 4294967295 .
H9:    15 < j .
H10:   31 < j .
H11:   47 < j .
H12:   63 < j .
H13:   bit__xor(x, bit__or(y, 4294967295 - z)) >= 0 .
H14:   bit__xor(x, bit__or(y, 4294967295 - z)) <= 4294967295 .
H15:   interfaces__unsigned_32__size >= 0 .
H16:   word__size >= 0 .
H17:   round_index__size >= 0 .
H18:   round_index__base__first <= round_index__base__last .
H19:   round_index__base__first <= 0 .
H20:   round_index__base__last >= 79 .
       ->
C1:    bit__xor(x, bit__or(y, 4294967295 - z)) = f_spec(j, x, y, z) .