minor reorg

runtimeverification · Mar 20, 2020 · fc22f6b · fc22f6b
1 parent 78bf93f
commit fc22f6b
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/deposit/bytecode-verification/deposit-spec.ini b/deposit/bytecode-verification/deposit-spec.ini
@@ -337,8 +337,8 @@ MEM_COST: 672
 k: #execute => #halt
 status_code: _ => EVMC_SUCCESS
 pc: {PC_LOOPHEAD} => {PC_END}
-RETURN_VAL: #sha256(#buf(32, NODE) ++ #bufSeg(#buf(32, Y8), 24, 8) ++ #buf(24, 0))
 output: _ => #buf(32, {RETURN_VAL})
+RETURN_VAL: #sha256(#buf(32, NODE) ++ #bufSeg(#buf(32, Y8), 24, 8) ++ #buf(24, 0))
 word_stack: HEIGHT : {WORD_STACK_LOOP} => .WordStack
 local_mem: {LOCAL_MEM_LOOPHEAD} => _
 +requires:
@@ -482,14 +482,14 @@ local_mem: .Map => NEW_MEM
 +ensures:
     {ENSURES_VYPER_GENERATED_BOUNDS}
     andBool #range(NEW_MEM, 2784, 32) ==K #buf(32, {NODE})
-GAS_COST: 769 +Int 10925 +Int 12354 +Int 17029 +Int 14366
-MEM_COST: {MU_DATA}
 log: _:List ( .List => ListItem(#abiEventLog(THIS, "DepositEvent",
             #bytes(#buf({PUBKEY_LENGTH}, PUBKEY)),
             #bytes(#buf({WITHDRAWAL_CREDENTIALS_LENGTH}, WITHDRAWAL_CREDENTIALS)),
             #bytes(#bufSeg(#buf(32, YY8), 24, 8)),
             #bytes(#buf({SIGNATURE_LENGTH}, SIGNATURE)),
             #bytes(#bufSeg(#buf(32, Y8), 24, 8)) )))
+GAS_COST: 55443
+MEM_COST: {MU_DATA}
 
 [deposit-success-insert]
 WORD_STACK_INIT: {LOOP_BOUND} : {LOOP_INDEX_ADDR} : .WordStack
@@ -505,9 +505,9 @@ PRE_MEM_COST: {MU_DATA}
 
 [deposit-success-insert-init-then]
 k: #execute => #halt
-output: _ => .WordStack
 status_code: _ => EVMC_SUCCESS
 pc: {PC_ADD_BEGIN} => {PC_ADD_END}
+output: _ => .WordStack
 word_stack: .WordStack
 local_mem: {LOCAL_MEM_DATA} => _
 storage: M => M
@@ -565,9 +565,9 @@ PRE_MEM_COST: maxInt({MU_ADD_ODD}, {MU_ADD_EVEN})
 
 [deposit-success-insert-loop-enter-then]
 k: #execute => #halt
-output: _ => .WordStack
 status_code: _ => EVMC_SUCCESS
 pc: {PC_ADD_LOOPHEAD} => {PC_ADD_END}
+output: _ => .WordStack
 word_stack: HEIGHT : {WORD_STACK_INIT} => .WordStack
 local_mem: {LOCAL_MEM_LOOPHEAD} => _
 storage: M => M
@@ -599,9 +599,9 @@ MEM_COST: maxInt({MU_ADD_ODD}, {MU_ADD_EVEN})
 
 [deposit-success-insert-loop-exit]
 k: #execute => #halt
-output: _ => .WordStack
 status_code: _ => EVMC_SUCCESS
 pc: {PC_ADD_LOOPHEAD} => {PC_ADD_END}
+output: _ => .WordStack
 word_stack: HEIGHT : {WORD_STACK_INIT} => .WordStack
 local_mem: {LOCAL_MEM_LOOPHEAD}
 +requires: