Merge pull request #11785 from ethereum/someMoreBaseFees

Some more base fees.

Author: chriseth

libevmasm/SimplificationRule.h

@@ -126,6 +126,7 @@ struct EVMBuiltins
 	static auto constexpr GASLIMIT = PatternGenerator<Instruction::GASLIMIT>{};
 	static auto constexpr CHAINID = PatternGenerator<Instruction::CHAINID>{};
 	static auto constexpr SELFBALANCE = PatternGenerator<Instruction::SELFBALANCE>{};
+	static auto constexpr BASEFEE = PatternGenerator<Instruction::BASEFEE>{};
 	static auto constexpr POP = PatternGenerator<Instruction::POP>{};
 	static auto constexpr MLOAD = PatternGenerator<Instruction::MLOAD>{};
 	static auto constexpr MSTORE = PatternGenerator<Instruction::MSTORE>{};

libsolidity/formal/Predicate.cpp

@@ -518,6 +518,7 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
 map<string, optional<string>> Predicate::readTxVars(smtutil::Expression const& _tx) const
 {
 	map<string, Type const*> const txVars{
+		{"block.basefee", TypeProvider::uint256()},
 		{"block.chainid", TypeProvider::uint256()},
 		{"block.coinbase", TypeProvider::address()},
 		{"block.difficulty", TypeProvider::uint256()},

libsolidity/formal/SymbolicState.cpp

@@ -128,7 +128,9 @@ smtutil::Expression SymbolicState::txMember(string const& _member) const
 
 smtutil::Expression SymbolicState::txTypeConstraints() const
 {
-	return smt::symbolicUnknownConstraints(m_tx.member("block.chainid"), TypeProvider::uint256()) &&
+	return
+		smt::symbolicUnknownConstraints(m_tx.member("block.basefee"), TypeProvider::uint256()) &&
+		smt::symbolicUnknownConstraints(m_tx.member("block.chainid"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.coinbase"), TypeProvider::address()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.difficulty"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.gaslimit"), TypeProvider::uint256()) &&

libsolidity/formal/SymbolicState.h

@@ -65,6 +65,7 @@ class BlockchainVariable
  *   - TODO: potentially storage of contracts
  * - block and transaction properties, represented as a tuple of:
  *   - blockhash
+ *   - block basefee
  *   - block chainid
  *   - block coinbase
  *   - block difficulty
@@ -191,6 +192,7 @@ class SymbolicState
 	BlockchainVariable m_tx{
 		"tx",
 		{
+			{"block.basefee", smtutil::SortProvider::uintSort},
 			{"block.chainid", smtutil::SortProvider::uintSort},
 			{"block.coinbase", smt::smtSort(*TypeProvider::address())},
 			{"block.difficulty", smtutil::SortProvider::uintSort},

libyul/backends/wasm/WasmDialect.cpp

@@ -190,6 +190,7 @@ void WasmDialect::addExternals()
 	static vector<External> externals{
 		{"eth", "getAddress", {i32ptr}, {}},
 		{"eth", "getExternalBalance", {i32ptr, i32ptr}, {}},
+		{"eth", "getBlockBaseFee", {i32ptr}, {}},
 		{"eth", "getBlockHash", {i64, i32ptr}, {i32}},
 		{"eth", "call", {i64, i32ptr, i32ptr, i32ptr, i32}, {i32}},
 		{"eth", "callDataCopy", {i32ptr, i32, i32}, {}},

test/cmdlineTests/standard_model_checker_divModSlacks_default_all/output.json

@@ -1,4 +1,4 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0xa34579041bed3510aedf3c5d668d439af5c40bbce2c58c14276be21e3336813c":"(set-option :produce-models true)
+{"auxiliaryInputRequested":{"smtlib2queries":{"0x72b32f47722af7f889ab5740b229c1799f27d0a693995a581c00f65438255a15":"(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |a_3_3| () Int)
 (declare-fun |b_5_3| () Int)
@@ -9,7 +9,7 @@
 (declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
 (declare-fun |state_0| () |state_type|)
 (declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
 (declare-fun |tx_0| () |tx_type|)
 (declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
 (declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
@@ -28,9 +28,9 @@
 (declare-fun |expr_14_0| () Int)
 (declare-fun |expr_15_1| () Bool)
 
-(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1))
+(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1)))
 (check-sat)
-","0xee99a9e327c7e01c72a32bb73a3d6338ae9c47df718fd1bb11819f1a4d8bc2b8":"(set-option :produce-models true)
+","0x825b322db572f1c2705128460f2af503aeeb571f1c2e15207ce4fd0355accee6":"(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |a_3_3| () Int)
 (declare-fun |b_5_3| () Int)
@@ -41,7 +41,7 @@
 (declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
 (declare-fun |state_0| () |state_type|)
 (declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
-(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
+(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
 (declare-fun |tx_0| () |tx_type|)
 (declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int)))))
 (declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int))))))
@@ -60,6 +60,6 @@
 (declare-fun |expr_14_0| () Int)
 (declare-fun |expr_15_1| () Bool)
 
-(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1)))
+(assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1))
 (check-sat)
 "}},"sources":{"A":{"id":0}}}