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

doc update

*****************************************************************************
                       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:20  SIMPLIFIED 29-NOV-2010, 14:30:20

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

function RMD.Hash




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

function_hash_1.
*** true .          /* all conclusions proved */


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

function_hash_2.
*** true .          /* all conclusions proved */


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

function_hash_3.
*** true .          /* all conclusions proved */


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

function_hash_4.
*** true .          /* all conclusions proved */


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

function_hash_5.
*** true .          /* all conclusions proved */


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

function_hash_6.
*** true .          /* all conclusions proved */


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

function_hash_7.
*** true .          /* all conclusions proved */


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

function_hash_8.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 178 to run-time check associated with 
          statement of line 177:

function_hash_9.
*** true .          /* all conclusions proved */


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

function_hash_10.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 178 to run-time check associated with 
          statement of line 177:

function_hash_11.
*** true .          /* all conclusions proved */


For path(s) from start to assertion of line 178:

function_hash_12.
H1:    x__index__subtype__1__first = 0 .
H2:    for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 
          integer, x__index__subtype__1__first <= i___1 and i___1 <= 
          x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
          i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
H3:    x__index__subtype__1__last >= 0 .
H4:    x__index__subtype__1__last <= 4294967296 .
H5:    x__index__subtype__1__first <= x__index__subtype__1__last .
H6:    mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
          ce__1) = round_spec(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 
          := 2562383102, h3 := 271733878, h4 := 3285377520), element(x, [
          x__index__subtype__1__first])) .
H7:    ca__1 >= 0 .
H8:    ca__1 <= 4294967295 .
H9:    cb__1 >= 0 .
H10:   cb__1 <= 4294967295 .
H11:   cc__1 >= 0 .
H12:   cc__1 <= 4294967295 .
H13:   cd__1 >= 0 .
H14:   cd__1 <= 4294967295 .
H15:   ce__1 >= 0 .
H16:   ce__1 <= 4294967295 .
       ->
C1:    mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
          ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 
          2562383102, h3 := 271733878, h4 := 3285377520), 
          x__index__subtype__1__first + 1, x) .


For path(s) from assertion of line 178 to assertion of line 178:

function_hash_13.
H1:    mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds(
          mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 
          271733878, h4 := 3285377520), loop__1__i + 1, x) .
H2:    for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 
          integer, x__index__subtype__1__first <= i___1 and i___1 <= 
          x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
          i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
H3:    x__index__subtype__1__first = 0 .
H4:    loop__1__i >= 0 .
H5:    loop__1__i <= 4294967296 .
H6:    loop__1__i >= x__index__subtype__1__first .
H7:    ca >= 0 .
H8:    ca <= 4294967295 .
H9:    cb >= 0 .
H10:   cb <= 4294967295 .
H11:   cc >= 0 .
H12:   cc <= 4294967295 .
H13:   cd >= 0 .
H14:   cd <= 4294967295 .
H15:   ce >= 0 .
H16:   ce <= 4294967295 .
H17:   loop__1__i + 1 <= x__index__subtype__1__last .
H18:   mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
          ce__1) = round_spec(mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, 
          h4 := ce), element(x, [loop__1__i + 1])) .
H19:   ca__1 >= 0 .
H20:   ca__1 <= 4294967295 .
H21:   cb__1 >= 0 .
H22:   cb__1 <= 4294967295 .
H23:   cc__1 >= 0 .
H24:   cc__1 <= 4294967295 .
H25:   cd__1 >= 0 .
H26:   cd__1 <= 4294967295 .
H27:   ce__1 >= 0 .
H28:   ce__1 <= 4294967295 .
H29:   interfaces__unsigned_32__size >= 0 .
H30:   word__size >= 0 .
H31:   chain__size >= 0 .
H32:   block_index__size >= 0 .
H33:   block_index__base__first <= block_index__base__last .
H34:   message_index__size >= 0 .
H35:   message_index__base__first <= message_index__base__last .
H36:   x__index__subtype__1__first <= x__index__subtype__1__last .
H37:   block_index__base__first <= 0 .
H38:   block_index__base__last >= 15 .
H39:   message_index__base__first <= 0 .
H40:   x__index__subtype__1__first >= 0 .
H41:   x__index__subtype__1__last >= 0 .
H42:   message_index__base__last >= 4294967296 .
H43:   x__index__subtype__1__last <= 4294967296 .
H44:   x__index__subtype__1__first <= 4294967296 .
       ->
C1:    mk__chain(h0 := ca__1, h1 := cb__1, h2 := cc__1, h3 := cd__1, h4 := 
          ce__1) = rounds(mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 
          2562383102, h3 := 271733878, h4 := 3285377520), loop__1__i + 2, x) .


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

function_hash_14.
*** true .          /* all conclusions proved */


For path(s) from assertion of line 178 to run-time check associated with 
          statement of line 183:

function_hash_15.
*** true .          /* all conclusions proved */


For path(s) from start to finish:

function_hash_16.
*** true .   /* contradiction within hypotheses. */



For path(s) from assertion of line 178 to finish:

function_hash_17.
H1:    mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rounds(
          mk__chain(h0 := 1732584193, h1 := 4023233417, h2 := 2562383102, h3 := 
          271733878, h4 := 3285377520), x__index__subtype__1__last + 1, x) .
H2:    for_all(i___2 : integer, 0 <= i___2 and i___2 <= 15 -> for_all(i___1 : 
          integer, x__index__subtype__1__first <= i___1 and i___1 <= 
          x__index__subtype__1__last -> 0 <= element(element(x, [i___1]), [
          i___2]) and element(element(x, [i___1]), [i___2]) <= 4294967295)) .
H3:    x__index__subtype__1__first = 0 .
H4:    x__index__subtype__1__last >= 0 .
H5:    x__index__subtype__1__last <= 4294967296 .
H6:    x__index__subtype__1__last >= x__index__subtype__1__first .
H7:    ca >= 0 .
H8:    ca <= 4294967295 .
H9:    cb >= 0 .
H10:   cb <= 4294967295 .
H11:   cc >= 0 .
H12:   cc <= 4294967295 .
H13:   cd >= 0 .
H14:   cd <= 4294967295 .
H15:   ce >= 0 .
H16:   ce <= 4294967295 .
H17:   interfaces__unsigned_32__size >= 0 .
H18:   word__size >= 0 .
H19:   chain__size >= 0 .
H20:   block_index__size >= 0 .
H21:   block_index__base__first <= block_index__base__last .
H22:   message_index__size >= 0 .
H23:   message_index__base__first <= message_index__base__last .
H24:   x__index__subtype__1__first <= x__index__subtype__1__last .
H25:   block_index__base__first <= 0 .
H26:   block_index__base__last >= 15 .
H27:   message_index__base__first <= 0 .
H28:   x__index__subtype__1__first >= 0 .
H29:   message_index__base__last >= 4294967296 .
H30:   x__index__subtype__1__first <= 4294967296 .
       ->
C1:    mk__chain(h0 := ca, h1 := cb, h2 := cc, h3 := cd, h4 := ce) = rmd_hash(
          x, x__index__subtype__1__last + 1) .