Deposit: further improvement of specs

deposit/bytecode-verification/Makefile

@@ -17,10 +17,10 @@ SPEC_NAMES:=
 SPEC_NAMES += init-success
 SPEC_NAMES += init-revert
 
-SPEC_NAMES += get_deposit_root-success-loop1-then
-SPEC_NAMES += get_deposit_root-success-loop1-else
-SPEC_NAMES += get_deposit_root-success-loop-body-then
-SPEC_NAMES += get_deposit_root-success-loop-body-else
+SPEC_NAMES += get_deposit_root-success-init-then
+SPEC_NAMES += get_deposit_root-success-init-else
+SPEC_NAMES += get_deposit_root-success-loop-enter-then
+SPEC_NAMES += get_deposit_root-success-loop-enter-else
 SPEC_NAMES += get_deposit_root-success-loop-exit
 SPEC_NAMES += get_deposit_root-revert
 

deposit/bytecode-verification/deposit-spec.ini

@@ -7,8 +7,8 @@ k: #execute
 pc: 0 => _
 word_stack: .WordStack => _
 local_mem: .Map => _
-gas: #symGas(G, 0, 0, .List, Cmem({SCHEDULE}, #symMem(0, .Set))) => _
-memory_used: #symMem(0, .Set) => _
+gas: #symGas(G, 0 => {GAS_COST_MIN}, 0 => {GAS_COST_MAX}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
+memory_used: #symMem({PRE_MEM_COST} => {MEM_COST}, .Set)
 ; no changes
 call_data: _
 log: _
@@ -24,12 +24,10 @@ status_code: _ => _
 ; variables
 comment:
 schedule:       ISTANBUL
-call_stack:     CALL_STACK
 this:           THIS
 msg_sender:     MSG_SENDER
 call_value:     CALL_VALUE
 call_depth:     CALL_DEPTH
-coinbase:       COIN_BASE
 active_accounts:
 accounts:
 requires:
@@ -46,6 +44,9 @@ requires:
     andBool isInitGas(G)
 ensures:
 attribute:
+GAS_COST_MIN: {GAS_COST}
+GAS_COST_MAX: {GAS_COST}
+PRE_MEM_COST: 0
 VYPER_GENERATED_BOUNDS:
     ; bounds - vyper generated
     [  32 := #buf(32, 1461501637330902918203684832716283019655932542976) ]
@@ -105,7 +106,7 @@ LET_BINDINGS_OF_TO_LITTLE_ENDIAN_64_DEPOSIT_AMOUNT:
 [init]
 ; for create
 code: {INIT_CODE}
-call_data: .WordStack
+call_data: #buf(CALL_DATA_SIZE, CALL_DATA) /* The expected call_data is empty, but we want to ensure that any accidental or malicious garbage doesn't break the logic. */
 storage: .Map
 orig_storage: .Map
 
@@ -214,9 +215,8 @@ refund: _ => _
 +requires:
     // conditions
     andBool CALL_VALUE ==Int 0
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(0 => 4278, .Set)
 GAS_COST: 672893
+MEM_COST: 4278
 
 [init-revert]
 k: #execute => #halt
@@ -225,9 +225,8 @@ pc: 0 => 151
 +requires:
     // conditions
     andBool CALL_VALUE =/=Int 0
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(0 => 192, .Set)
 GAS_COST: 69
+MEM_COST: 192
 
 ;
 ; get_deposit_root
@@ -254,7 +253,7 @@ WORD_STACK_LOOP: {LOOP_BOUND} : {LOOP_INDEX_ADDR} : .WordStack
 LOOP_BOUND: 32
 LOOP_INDEX_ADDR: 416
 
-[get_deposit_root-success-loop1]
+[get_deposit_root-success-init]
 pc: 0 => {PC_LOOPHEAD}
 word_stack: .WordStack => 1 : {WORD_STACK_LOOP}
 local_mem: .Map => NEW_MEM
@@ -264,10 +263,8 @@ local_mem: .Map => NEW_MEM
     andBool #range(NEW_MEM, 352, 32) ==K #buf(32, {NODE_1})
     andBool #range(NEW_MEM, 384, 32) ==K #buf(32, DEPOSIT_COUNT /Int 2)
     andBool #range(NEW_MEM, 416, 32) ==K #buf(32, 1)
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(0 => {MEM_COST}, .Set)
 
-[get_deposit_root-success-loop1-then]
+[get_deposit_root-success-init-then]
 NODE_1: #sha256(#buf(32, {BRANCH_0}) ++ #buf(32, 0))
 BRANCH_0: select(M, #hashedLocation({COMPILER}, {BRANCH}, 0))
 +requires:
@@ -276,7 +273,7 @@ BRANCH_0: select(M, #hashedLocation({COMPILER}, {BRANCH}, 0))
 GAS_COST: 1728
 MEM_COST: 672
 
-[get_deposit_root-success-loop1-else]
+[get_deposit_root-success-init-else]
 NODE_1: #sha256(#buf(32, 0) ++ #buf(32, {ZERO_HASHES_0}))
 ZERO_HASHES_0: select(M, #hashedLocation({COMPILER}, {ZERO_HASHES}, 0))
 +requires:
@@ -288,19 +285,21 @@ MEM_COST: 544
 [get_deposit_root-success-loop]
 LOCAL_MEM_LOOPHEAD: MEM
     {VYPER_GENERATED_BOUNDS}
-    ; locals
+    ; locals - invariants
     [ 320 /* = 320 + 32 * 0 */ := #buf(32, 0) ]          /* zero_bytes32: bytes32 = 0x0 */
     [ 352 /* = 320 + 32 * 1 */ := #buf(32, NODE) ]       /* node: bytes32 */
     [ 384 /* = 320 + 32 * 2 */ := #buf(32, SIZE) ]       /* size: uint256 */
     [ 416 /* = 320 + 32 * 3 */ := #buf(32, HEIGHT) ]     /* height */
 +requires:
-    // conditions
-    andBool #range(0 <= HEIGHT <= 32)
+    // conditions - invariants
+    andBool HEIGHT <=Int 32
     // types
     andBool #rangeUInt(256, NODE)
     andBool #rangeUInt(256, SIZE)
+    andBool #rangeUInt(256, HEIGHT)
+PRE_MEM_COST: 672
 
-[get_deposit_root-success-loop-body]
+[get_deposit_root-success-loop-enter]
 pc: {PC_LOOPHEAD}
 word_stack: (HEIGHT => HEIGHT +Int 1) : {WORD_STACK_LOOP}
 local_mem: {LOCAL_MEM_LOOPHEAD} => NEW_MEM
@@ -312,41 +311,40 @@ local_mem: {LOCAL_MEM_LOOPHEAD} => NEW_MEM
     andBool #range(NEW_MEM, 416, 32) ==K #buf(32, HEIGHT +Int 1)
 +requires:
     // conditions
-    andBool HEIGHT <Int 32
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(672, .Set)
+    andBool HEIGHT =/=Int 32
 
-[get_deposit_root-success-loop-body-then]
+[get_deposit_root-success-loop-enter-then]
 NODE_NEW: #sha256(#buf(32, {BRANCH_HEIGHT}) ++ #buf(32, NODE))
 BRANCH_HEIGHT: select(M, #hashedLocation({COMPILER}, {BRANCH}, HEIGHT))
 +requires:
     // conditions
     andBool SIZE &Int 1 ==Int 1
 GAS_COST: 1350
+MEM_COST: 672
 
-[get_deposit_root-success-loop-body-else]
+[get_deposit_root-success-loop-enter-else]
 NODE_NEW: #sha256(#buf(32, NODE) ++ #buf(32, {ZERO_HASHES_HEIGHT}))
 ZERO_HASHES_HEIGHT: select(M, #hashedLocation({COMPILER}, {ZERO_HASHES}, HEIGHT))
 +requires:
     // conditions
     andBool SIZE &Int 1 =/=Int 1
 GAS_COST: 1340
+MEM_COST: 672
 
 [get_deposit_root-success-loop-exit]
 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:
     // conditions
     andBool HEIGHT ==Int 32
     {LET_BINDINGS_OF_TO_LITTLE_ENDIAN_64_DEPOSIT_COUNT}
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(672 => 1216, .Set)
 GAS_COST: 11385
+MEM_COST: 1216
 
 [get_deposit_root-revert]
 k: #execute => #halt
@@ -355,9 +353,8 @@ pc: 0 => 663
 +requires:
     // conditions
     andBool CALL_VALUE =/=Int 0
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(0 => 192, .Set)
 GAS_COST: 154
+MEM_COST: 192
 
 ;
 ; get_deposit_count
@@ -385,9 +382,8 @@ local_mem: .Map => _
     // let-bindings
     andBool DEPOSIT_COUNT ==Int select(M, #hashedLocation({COMPILER}, {DEPOSIT_COUNT}, .IntList))
     {LET_BINDINGS_OF_TO_LITTLE_ENDIAN_64_DEPOSIT_COUNT}
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(0 => 832, .Set)
 GAS_COST: 11424
+MEM_COST: 832
 
 [get_deposit_count-revert]
 k: #execute => #halt
@@ -396,9 +392,8 @@ pc: 0 => 1318
 +requires:
     // conditions
     andBool CALL_VALUE =/=Int 0
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(0 => 192, .Set)
 GAS_COST: 183
+MEM_COST: 192
 
 ;
 ; deposit
@@ -485,30 +480,32 @@ local_mem: .Map => NEW_MEM
 +ensures:
     {ENSURES_VYPER_GENERATED_BOUNDS}
     andBool #range(NEW_MEM, 2784, 32) ==K #buf(32, {NODE})
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(0 => {MU_DATA}, .Set)
-GAS_COST: 769 +Int 10925 +Int 12354 +Int 17029 +Int 14366
 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: 32 : 3360 : .WordStack
+WORD_STACK_INIT: {LOOP_BOUND} : {LOOP_INDEX_ADDR} : .WordStack
+LOOP_BOUND: 32
+LOOP_INDEX_ADDR: 3360
 
 [deposit-success-insert-init]
 LOCAL_MEM_DATA: MEM
     {VYPER_GENERATED_BOUNDS}
     ; locals
     [ 2784 := #buf(32, {NODE}) ]      /* node */
+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
@@ -518,8 +515,9 @@ refund: _ => _
 +requires:
     // conditions
     andBool (DEPOSIT_COUNT +Int 1) &Int 1 ==Int 1
-gas:         #symGas(G, 0 => 11019, 0 => 41019, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem({MU_DATA} => {MU_ADD_ODD}, .Set)
+GAS_COST_MIN: 11019
+GAS_COST_MAX: 41019
+MEM_COST: {MU_ADD_ODD}
 
 [deposit-success-insert-init-else]
 pc: {PC_ADD_BEGIN} => {PC_ADD_LOOPHEAD}
@@ -538,33 +536,36 @@ refund: _ => _
 +requires:
     // conditions
     andBool (DEPOSIT_COUNT +Int 1) &Int 1 =/=Int 1
-gas:         #symGas(G, 0 => 7196, 0 => 22196, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem({MU_DATA} => {MU_ADD_EVEN}, .Set)
+GAS_COST_MIN:  7196
+GAS_COST_MAX: 22196
+MEM_COST: {MU_ADD_EVEN}
 
 [deposit-success-insert-loop]
 LOCAL_MEM_LOOPHEAD: MEM
     {VYPER_GENERATED_BOUNDS}
-    ; locals
+    ; locals - invariants
     [ 2784 := #buf(32, NODE) ]      /* node */
     [ 3328 := #buf(32, SIZE) ]      /* size */
     [ 3360 := #buf(32, HEIGHT) ]    /* height */
 +requires:
-    // conditions
-    andBool #range(0 <= HEIGHT <= 32)
+    // conditions - invariants
+    andBool HEIGHT <=Int 32
     // types
     andBool #rangeUInt(256, NODE)
     andBool #rangeUInt(256, SIZE)
+    andBool #rangeUInt(256, HEIGHT)
+PRE_MEM_COST: maxInt({MU_ADD_ODD}, {MU_ADD_EVEN})
 
 [deposit-success-insert-loop-enter]
 +requires:
     // conditions
-    andBool HEIGHT <Int 32
+    andBool HEIGHT =/=Int 32
 
 [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
@@ -573,8 +574,9 @@ refund: _ => _
 +requires:
     // conditions
     andBool SIZE &Int 1 ==Int 1
-gas:         #symGas(G, 0 => 5162, 0 => 20162, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem({MU_ADD_EVEN}, .Set)
+GAS_COST_MIN:  5162
+GAS_COST_MAX: 20162
+MEM_COST: maxInt({MU_ADD_ODD}, {MU_ADD_EVEN})
 
 [deposit-success-insert-loop-enter-else]
 pc: {PC_ADD_LOOPHEAD}
@@ -590,32 +592,28 @@ BRANCH_HEIGHT: select(M, #hashedLocation({COMPILER}, {BRANCH}, HEIGHT))
 +requires:
     // conditions
     andBool SIZE &Int 1 =/=Int 1
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem({MU_ADD_EVEN}, .Set)
 GAS_COST: 1339
+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:
     // conditions
     andBool HEIGHT ==Int 32
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem({MU_ADD_EVEN}, .Set)
 GAS_COST: 27
+MEM_COST: maxInt({MU_ADD_ODD}, {MU_ADD_EVEN})
 
 [deposit-revert]
 k: #execute => #halt
 status_code: _ => EVMC_REVERT
 word_stack: .WordStack => _
 local_mem: .Map => _
 log: _ => _
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(0 => {MEM_COST}, .Set)
 
 [deposit-revert-1]
 pc: 0 => 1691
@@ -654,8 +652,6 @@ call_data: #buf(CALL_DATA_SIZE, CALL_DATA)
     // conditions
     andBool DEPOSIT_COUNT <Int {MAX_DEPOSIT_COUNT}
     andBool CALL_VALUE /Int {GWEI_IN_WEI} >=Int {MIN_DEPOSIT_AMOUNT}
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(0 => {MEM_COST}, .Set)
 ;
 CALLDATALOAD_0: #take(32, {CALL_DATA})
 FUNCTION_SELECTOR: #asWord(#take(4, {CALLDATALOAD_0}))
@@ -775,8 +771,6 @@ status_code: _ => EVMC_REVERT
 [revert-invalid_function_identifier]
 call_data: #buf(CALL_DATA_SIZE, CALL_DATA)
 pc: 0 => 4277
-gas:         #symGas(G, 0 => {GAS_COST}, 0 => {GAS_COST}, .List, Cmem({SCHEDULE}, {MEMORY_USED}))
-memory_used: #symMem(0 => {MEM_COST}, .Set)
 
 [revert-invalid_function_identifier-lt_4]
 +requires: