SMTChecker: Support block.slotnum

Changelog.md

@@ -11,6 +11,7 @@ Compiler Features:
 * General: Improve performance throughout the compiler using Boost's flat versions of unordered set and map.
 * General: Remove support for the experimental Generic Solidity prototype (`pragma experimental solidity`).
 * SMTChecker: Emit a deprecation warning for the BMC engine.
+* SMTChecker: Support `block.slotnum`.
 
 Bugfixes:
 * Code Generator: Fix ICE on parenthesized custom error construction in require statement.

libsolidity/formal/SMTEncoder.cpp

@@ -1412,16 +1412,6 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 
 	if (exprType->category() == Type::Category::Magic)
 	{
-		auto defineTxMember = [&](std::string const& _fullName) {
-			if (state().hasTxMember(_fullName))
-				defineExpr(_memberAccess, state().txMember(_fullName));
-			else
-				m_unsupportedErrors.warning(
-					2350_error,
-					_memberAccess.location(),
-					"Assertion checker does not yet support this expression."
-				);
-		};
 		if (auto const* identifier = dynamic_cast<Identifier const*>(&memberExpr))
 		{
 			auto const& name = identifier->name();
@@ -1432,16 +1422,16 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 			if (name == "block" && memberName == "difficulty")
 				memberName = "prevrandao";
 
-			defineTxMember(name + "." + memberName);
+			defineExpr(_memberAccess, state().txMember(name + "." + memberName));
 		}
 		else if (auto magicType = dynamic_cast<MagicType const*>(exprType))
 		{
 			if (magicType->kind() == MagicType::Kind::Block)
-				defineTxMember("block." + _memberAccess.memberName());
+				defineExpr(_memberAccess, state().txMember("block." + _memberAccess.memberName()));
 			else if (magicType->kind() == MagicType::Kind::Message)
-				defineTxMember("msg." + _memberAccess.memberName());
+				defineExpr(_memberAccess, state().txMember("msg." + _memberAccess.memberName()));
 			else if (magicType->kind() == MagicType::Kind::Transaction)
-				defineTxMember("tx." + _memberAccess.memberName());
+				defineExpr(_memberAccess, state().txMember("tx." + _memberAccess.memberName()));
 			else if (magicType->kind() == MagicType::Kind::MetaType)
 			{
 				auto const& memberName = _memberAccess.memberName();

libsolidity/formal/SymbolicState.cpp

@@ -233,6 +233,7 @@ smtutil::Expression SymbolicState::txTypeConstraints() const
 		smt::symbolicUnknownConstraints(m_tx.member("block.prevrandao"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.gaslimit"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.number"), TypeProvider::uint256()) &&
+		smt::symbolicUnknownConstraints(m_tx.member("block.slotnum"), TypeProvider::uint(64)) &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.timestamp"), TypeProvider::uint256()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("msg.sender"), TypeProvider::address()) &&
 		smt::symbolicUnknownConstraints(m_tx.member("msg.value"), TypeProvider::uint256()) &&

libsolidity/formal/SymbolicState.h

@@ -45,8 +45,6 @@ class BlockchainVariable
 
 	/// @returns the symbolic _member.
 	smtutil::Expression member(std::string const& _member) const;
-	/// @returns true if _member is part of this tuple.
-	bool hasMember(std::string const& _member) const { return m_componentIndices.count(_member) > 0; }
 	/// Generates a new tuple where _member is assigned _value.
 	smtutil::Expression assignMember(std::string const& _member, smtutil::Expression const& _value);
 
@@ -76,6 +74,7 @@ class BlockchainVariable
  *   - block gaslimit
  *   - block number
  *   - block prevrandao
+ *   - block slotnum
  *   - block timestamp
  *   - TODO gasleft
  *   - msg data
@@ -149,7 +148,6 @@ class SymbolicState
 	smtutil::SortPointer const& txSort() const { return m_tx.sort(); }
 	void newTx() { m_tx.newVar(); }
 	smtutil::Expression txMember(std::string const& _member) const;
-	bool hasTxMember(std::string const& _member) const { return m_tx.hasMember(_member); }
 	smtutil::Expression txFunctionConstraints(FunctionDefinition const& _function) const;
 	smtutil::Expression txTypeConstraints() const;
 	smtutil::Expression txNonPayableConstraint() const;

libsolidity/formal/SymbolicTypes.cpp

@@ -679,6 +679,7 @@ std::map<std::string, frontend::Type const*> transactionMemberTypes()
 		{"block.prevrandao", TypeProvider::uint256()},
 		{"block.gaslimit", TypeProvider::uint256()},
 		{"block.number", TypeProvider::uint256()},
+		{"block.slotnum", TypeProvider::uint(64)},
 		{"block.timestamp", TypeProvider::uint256()},
 		{"blobhash", TypeProvider::array(DataLocation::Memory, TypeProvider::uint256())},
 		{"blockhash", TypeProvider::array(DataLocation::Memory, TypeProvider::uint256())},

scripts/error_codes.py

@@ -211,10 +211,6 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
         "5026", # ContractLevelChecker: too difficult to exceed transient storage max size due to only value types supported.
         "1049", # AsmAnalysis: SLOTNUM only available for Amsterdam-compatible VMs. Only reachable once Amsterdam
                 # becomes the default EVM version.
-        "2350", # SMTEncoder: block/msg/tx member not yet known to the SMTChecker (e.g. block.slotnum before the
-                # formal/ support for it lands). Covered by CL test model_checker_unsupported_block_slotnum;
-                # unreachable via smtCheckerTests since SMTCheckerTest hardcodes EVMVersion{} and slotnum
-                # requires Amsterdam.
     }
     assert len(test_ids & white_ids) == 0, "The sets are not supposed to intersect"
     test_ids |= white_ids

test/cmdlineTests/model_checker_print_query_bmc/err

@@ -6,7 +6,7 @@ Info: BMC: Requested query:
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
 (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| (|blobhash| (Array Int Int)) (|block.basefee| Int) (|block.blobbasefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| 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| (|blobhash| (Array Int Int)) (|block.basefee| Int) (|block.blobbasefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.slotnum| 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))))))
@@ -21,7 +21,7 @@ Info: BMC: Requested query:
 (declare-fun |expr_9_0| () Int)
 (declare-fun |expr_10_0| () Int)
 (declare-fun |expr_11_1| () Bool)
-(assert (and (and (and true true) (and (= expr_11_1 (= expr_9_0 expr_10_0)) (and (=> (and true true) true) (and (= expr_10_0 0) (and (=> (and true true) (and (>= expr_9_0 0) (<= expr_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_0 x_5_1) (and (ite (and true true) (= x_5_1 expr_6_0) (= x_5_1 x_5_0)) (and (=> (and true true) true) (and (= expr_6_0 0) (and (= x_5_0 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.blobbasefee| tx_0) 0) (<= (|block.blobbasefee| 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.prevrandao| tx_0) 0) (<= (|block.prevrandao| 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) 638722032)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 38)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 18)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 31)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 240)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_11_1)))
+(assert (and (and (and true true) (and (= expr_11_1 (= expr_9_0 expr_10_0)) (and (=> (and true true) true) (and (= expr_10_0 0) (and (=> (and true true) (and (>= expr_9_0 0) (<= expr_9_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_9_0 x_5_1) (and (ite (and true true) (= x_5_1 expr_6_0) (= x_5_1 x_5_0)) (and (=> (and true true) true) (and (= expr_6_0 0) (and (= x_5_0 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (> (|block.prevrandao| tx_0) 18446744073709551616) (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.blobbasefee| tx_0) 0) (<= (|block.blobbasefee| 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.prevrandao| tx_0) 0) (<= (|block.prevrandao| 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.slotnum| tx_0) 0) (<= (|block.slotnum| tx_0) 18446744073709551615))) (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) 638722032)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 38)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 18)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 31)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 240)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_11_1)))
 (declare-const |EVALEXPR_0| Int)
 (assert (= |EVALEXPR_0| x_5_1))
 (check-sat)