Skip to content

Commit

Permalink
update benchmark specs
Browse files Browse the repository at this point in the history
  • Loading branch information
Dwight Guth committed Mar 19, 2024
1 parent fd32f43 commit 4af3ad2
Show file tree
Hide file tree
Showing 27 changed files with 27 additions and 27 deletions.
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/address00-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module ADDRESS00-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #address(A0)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/bytes00-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module BYTES00-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #bytes(#bufStrict(DATA_LEN, DATA))) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/dynamicarray00-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module DYNAMICARRAY00-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData2("execute(uint256[])", #array(#uint256(1), 3, #uint256(A0), #uint256(A1), #uint256(A2), .TypedArgs)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/ecrecover00-siginvalid-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module ECRECOVER00-SIGINVALID-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #bytes32(HASH), #uint8(SIGV), #bytes32(SIGR), #bytes32(SIGS)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/ecrecover00-sigvalid-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module ECRECOVER00-SIGVALID-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #bytes32(HASH), #uint8(SIGV), #bytes32(SIGR), #bytes32(SIGS)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ module ECRECOVERLOOP00-SIG0-INVALID-SPEC
#bytes32(SIGR0), #bytes32(SIGR1),
#bytes32(SIGS0), #bytes32(SIGS1)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ module ECRECOVERLOOP00-SIG1-INVALID-SPEC
#bytes32(SIGR0), #bytes32(SIGR1),
#bytes32(SIGS0), #bytes32(SIGS1)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ module ECRECOVERLOOP00-SIGS-VALID-SPEC
#bytes32(SIGR0), #bytes32(SIGR1),
#bytes32(SIGS0), #bytes32(SIGS1)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ module ECRECOVERLOOP02-SIG0-INVALID-SPEC
#bytes32(SIGR0), #bytes32(SIGR1),
#bytes32(SIGS0), #bytes32(SIGS1)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ module ECRECOVERLOOP02-SIG1-INVALID-SPEC
#bytes32(SIGR0), #bytes32(SIGR1),
#bytes32(SIGS0), #bytes32(SIGS1)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ module ECRECOVERLOOP02-SIGS-VALID-SPEC
#bytes32(SIGR0), #bytes32(SIGR1),
#bytes32(SIGS0), #bytes32(SIGS1)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/encode-keccak00-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module ENCODE-KECCAK00-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #bytes32(A0), #bytes32(A1)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/encodepacked-keccak01-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module ENCODEPACKED-KECCAK01-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #bytes32(A0)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/keccak00-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module KECCAK00-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #bytes(#bufStrict(DATA_LEN,DATA))) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/overflow00-nooverflow-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module OVERFLOW00-NOOVERFLOW-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #uint256(A0)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/overflow00-overflow-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module OVERFLOW00-OVERFLOW-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #uint256(A0)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/requires01-a0gt0-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module REQUIRES01-A0GT0-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #uint256(A0)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/requires01-a0le0-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module REQUIRES01-A0LE0-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #uint256(A0)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/staticarray00-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module STATICARRAY00-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData2("execute(uint256[3])", #uint256(A0), #uint256(A1), #uint256(A2)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/staticloop00-a0lt10-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module STATICLOOP00-A0LT10-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", #uint256(A0)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/storagevar00-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module STORAGEVAR00-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", .TypedArgs) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/storagevar01-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module STORAGEVAR01-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", .TypedArgs) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/storagevar02-nooverflow-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module STORAGEVAR02-NOOVERFLOW-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", .TypedArgs) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/storagevar02-overflow-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module STORAGEVAR02-OVERFLOW-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", .TypedArgs) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/storagevar03-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module STORAGEVAR03-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData("execute", .TypedArgs) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/structarg00-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module STRUCTARG00-SPEC
<caller> MSG_SENDER </caller> // msg.sender
<callData> #abiCallData2("execute((uint256,uint8))", #tuple(#uint256(A0), #uint8(A1), .TypedArgs)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down
2 changes: 1 addition & 1 deletion tests/specs/benchmarks/structarg01-spec.k
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ module STRUCTARG01-SPEC
<caller> CALLEE_ID </caller> // msg.sender
<callData> #abiCallData2("execute((bytes,uint256,uint256))", #tuple(#bytes(A0), #uint256(A1), #uint256(A2), .TypedArgs)) </callData> // msg.data
<callValue> 0 </callValue> // msg.value
<wordStack> .WordStack => ?_ </wordStack>
<wordStack> .List => ?_ </wordStack>
<localMem> .Bytes => ?_ </localMem>
<pc> 0 => ?_ </pc>
<gas> #gas(_VGAS) => ?_ </gas>
Expand Down

0 comments on commit 4af3ad2

Please sign in to comment.