Permalink
Browse files

wip

  • Loading branch information...
daejunpark committed Jan 11, 2019
1 parent 83f9e19 commit 27f137a5680398bbfef845e4cae1a69e09e4d4c4
Showing with 7 additions and 0 deletions.
  1. +7 −0 gnosis-imap/gnosis-imap-spec.ini
@@ -681,6 +681,13 @@ MEM_RHS: M2
andBool #rangeAddress(select(S, #hashedLocation({COMPILER}, {OWNERS}, #signer({SIGS_BUF}, 0, TX_DATA_HASH))))
andBool #rangeAddress(#signer({SIGS_BUF}, 0, TX_DATA_HASH))

+ensures:
andBool selectRange(M2, TX_DATA_LOC , 32 ) ==K #buf(32, TX_DATA_LEN)
andBool selectRange(M2, TX_DATA_LOC +Int 32, TX_DATA_LEN) ==K #buf(TX_DATA_LEN, TX_DATA)
andBool selectRange(M2, SIGS_LOC , 32 ) ==K #buf(32, SIGS_LEN)
andBool selectRange(M2, SIGS_LOC +Int 32, SIGS_LEN) ==K #buf(SIGS_LEN, SIGS)
andBool #asWord(selectRange(M2, 64, 32)) >=Int NEXT_LOC

CONSUME_HASH: 1

PC_FUN_START: 18250

0 comments on commit 27f137a

Please sign in to comment.