SMTChecker: Add support for block.blobbasefee and blobhash()

Changelog.md

@@ -5,6 +5,7 @@ Language Features:
 
 Compiler Features:
  * Error Reporting: Errors reported during code generation now point at the location of the contract when more fine-grained location is not available.
+ * SMTChecker: Support `block.blobbasefee` and `blobhash`.
  * SMTChecker: Z3 is now a runtime dependency, not a build dependency (except for emscripten build).
  * Yul Parser: Make name clash with a builtin a non-fatal error.
 

docs/smtchecker.rst

@@ -931,9 +931,9 @@ the arguments.
 +-----------------------------------+--------------------------------------+
 |``addmod``, ``mulmod``             |Supported precisely.                  |
 +-----------------------------------+--------------------------------------+
-|``gasleft``, ``blockhash``,        |Abstracted with UF.                   |
-|``keccak256``, ``ecrecover``       |                                      |
-|``ripemd160``                      |                                      |
+|``gasleft``, ``blobhash``,         |Abstracted with UF.                   |
+|``blockhash``, ``keccak256``,      |                                      |
+|``ecrecover``, ``ripemd160``       |                                      |
 +-----------------------------------+--------------------------------------+
 |pure functions without             |Abstracted with UF                    |
 |implementation (external or        |                                      |

libsolidity/formal/BMC.cpp

@@ -664,6 +664,7 @@ void BMC::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ECRecover:
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
+	case FunctionType::Kind::BlobHash:
 	case FunctionType::Kind::BlockHash:
 	case FunctionType::Kind::AddMod:
 	case FunctionType::Kind::MulMod:

libsolidity/formal/CHC.cpp

@@ -641,6 +641,7 @@ void CHC::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ECRecover:
 	case FunctionType::Kind::SHA256:
 	case FunctionType::Kind::RIPEMD160:
+	case FunctionType::Kind::BlobHash:
 	case FunctionType::Kind::BlockHash:
 	case FunctionType::Kind::AddMod:
 	case FunctionType::Kind::MulMod:

libsolidity/formal/Predicate.cpp

@@ -489,22 +489,7 @@ std::map<std::string, std::string> Predicate::expressionSubstitution(smtutil::Ex
 
 std::map<std::string, std::optional<std::string>> Predicate::readTxVars(smtutil::Expression const& _tx) const
 {
-	std::map<std::string, Type const*> const txVars{
-		{"block.basefee", TypeProvider::uint256()},
-		{"block.chainid", TypeProvider::uint256()},
-		{"block.coinbase", TypeProvider::address()},
-		{"block.prevrandao", TypeProvider::uint256()},
-		{"block.gaslimit", TypeProvider::uint256()},
-		{"block.number", TypeProvider::uint256()},
-		{"block.timestamp", TypeProvider::uint256()},
-		{"blockhash", TypeProvider::array(DataLocation::Memory, TypeProvider::uint256())},
-		{"msg.data", TypeProvider::array(DataLocation::CallData)},
-		{"msg.sender", TypeProvider::address()},
-		{"msg.sig", TypeProvider::fixedBytes(4)},
-		{"msg.value", TypeProvider::uint256()},
-		{"tx.gasprice", TypeProvider::uint256()},
-		{"tx.origin", TypeProvider::address()}
-	};
+	std::map<std::string, Type const*> const txVars = transactionMemberTypes();
 	std::map<std::string, std::optional<std::string>> vars;
 	for (auto&& [i, v]: txVars | ranges::views::enumerate)
 		vars.emplace(v.first, expressionToString(_tx.arguments.at(i), v.second));

libsolidity/formal/SMTEncoder.cpp

@@ -679,6 +679,9 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::BlockHash:
 		defineExpr(_funCall, state().blockhash(expr(*_funCall.arguments().at(0))));
 		break;
+	case FunctionType::Kind::BlobHash:
+		visitBlobHash(_funCall);
+		break;
 	case FunctionType::Kind::AddMod:
 	case FunctionType::Kind::MulMod:
 		visitAddMulMod(_funCall);
@@ -893,6 +896,18 @@ void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
 		m_context.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
+void SMTEncoder::visitBlobHash(FunctionCall const& _funCall)
+{
+	constexpr unsigned BLOB_TRANSACTION_LIMIT = 9; // Since pectra
+	auto indexExpr = expr(*_funCall.arguments().at(0));
+	auto valueExpr = smtutil::Expression::ite(
+		indexExpr >= BLOB_TRANSACTION_LIMIT,
+		smtutil::Expression(u256(0)),
+		state().blobhash(indexExpr)
+	);
+	defineExpr(_funCall, std::move(valueExpr));
+}
+
 void SMTEncoder::visitAddMulMod(FunctionCall const& _funCall)
 {
 	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);

libsolidity/formal/SMTEncoder.h

@@ -229,6 +229,7 @@ class SMTEncoder: public ASTConstVisitor
 	void visitBytesConcat(FunctionCall const& _funCall);
 	void visitCryptoFunction(FunctionCall const& _funCall);
 	void visitGasLeft(FunctionCall const& _funCall);
+	void visitBlobHash(FunctionCall const& _funCall);
 	virtual void visitAddMulMod(FunctionCall const& _funCall);
 	void visitWrapUnwrap(FunctionCall const& _funCall);
 	void visitObjectCreation(FunctionCall const& _funCall);

libsolidity/formal/SymbolicState.cpp

@@ -96,6 +96,11 @@ smtutil::Expression SymbolicState::balance(smtutil::Expression _address) const
 	return smtutil::Expression::select(balances(), std::move(_address));
 }
 
+smtutil::Expression SymbolicState::blobhash(smtutil::Expression _blobIndex) const
+{
+	return smtutil::Expression::select(m_tx.member("blobhash"), std::move(_blobIndex));
+}
+
 smtutil::Expression SymbolicState::blockhash(smtutil::Expression _blockNumber) const
 {
 	return smtutil::Expression::select(m_tx.member("blockhash"), std::move(_blockNumber));
@@ -222,6 +227,7 @@ smtutil::Expression SymbolicState::txTypeConstraints() const
 	return
 		evmParisConstraints() &&
 		smt::symbolicUnknownConstraints(m_tx.member("block.basefee"), TypeProvider::uint256()) &&
+		smt::symbolicUnknownConstraints(m_tx.member("block.blobbasefee"), 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.prevrandao"), TypeProvider::uint256()) &&

libsolidity/formal/SymbolicState.h

@@ -65,8 +65,10 @@ class BlockchainVariable
  *   - array of address => bool representing whether an address is used by a contract
  *   - storage of contracts
  * - block and transaction properties, represented as a tuple of:
+ *   - blobhash
  *   - blockhash
  *   - block basefee
+ *   - block blobbasefee
  *   - block chainid
  *   - block coinbase
  *   - block gaslimit
@@ -148,6 +150,7 @@ class SymbolicState
 	smtutil::Expression txFunctionConstraints(FunctionDefinition const& _function) const;
 	smtutil::Expression txTypeConstraints() const;
 	smtutil::Expression txNonPayableConstraint() const;
+	smtutil::Expression blobhash(smtutil::Expression _blobIndex) const;
 	smtutil::Expression blockhash(smtutil::Expression _blockNumber) const;
 	smtutil::Expression evmParisConstraints() const;
 	//@}
@@ -236,27 +239,7 @@ class SymbolicState
 	/// and the element is a tuple containing the state variables of that contract.
 	std::unique_ptr<BlockchainVariable> m_state;
 
-	BlockchainVariable m_tx{
-		"tx",
-		{
-			{"block.basefee", smtutil::SortProvider::uintSort},
-			{"block.chainid", smtutil::SortProvider::uintSort},
-			{"block.coinbase", smt::smtSort(*TypeProvider::address())},
-			{"block.prevrandao", smtutil::SortProvider::uintSort},
-			{"block.gaslimit", smtutil::SortProvider::uintSort},
-			{"block.number", smtutil::SortProvider::uintSort},
-			{"block.timestamp", smtutil::SortProvider::uintSort},
-			{"blockhash", std::make_shared<smtutil::ArraySort>(smtutil::SortProvider::uintSort, smtutil::SortProvider::uintSort)},
-			// TODO gasleft
-			{"msg.data", smt::smtSort(*TypeProvider::bytesMemory())},
-			{"msg.sender", smt::smtSort(*TypeProvider::address())},
-			{"msg.sig", smtutil::SortProvider::uintSort},
-			{"msg.value", smtutil::SortProvider::uintSort},
-			{"tx.gasprice", smtutil::SortProvider::uintSort},
-			{"tx.origin", smt::smtSort(*TypeProvider::address())}
-		},
-		m_context
-	};
+	BlockchainVariable m_tx{"tx", transactionMemberSorts(), m_context};
 
 	BlockchainVariable m_crypto{
 		"crypto",

libsolidity/formal/SymbolicTypes.cpp

@@ -667,4 +667,41 @@ smtutil::Expression assignMember(smtutil::Expression const _tuple, std::map<std:
 	return smtutil::Expression::tuple_constructor(sortExpr, args);
 }
 
+std::map<std::string, frontend::Type const*> transactionMemberTypes()
+{
+	// TODO: gasleft
+	return {
+		{"block.basefee", TypeProvider::uint256()},
+		{"block.blobbasefee", TypeProvider::uint256()},
+		{"block.chainid", TypeProvider::uint256()},
+		{"block.coinbase", TypeProvider::address()},
+		{"block.prevrandao", TypeProvider::uint256()},
+		{"block.gaslimit", TypeProvider::uint256()},
+		{"block.number", TypeProvider::uint256()},
+		{"block.timestamp", TypeProvider::uint256()},
+		{"blobhash", TypeProvider::array(DataLocation::Memory, TypeProvider::uint256())},
+		{"blockhash", TypeProvider::array(DataLocation::Memory, TypeProvider::uint256())},
+		{"msg.data", TypeProvider::bytesCalldata()},
+		{"msg.sender", TypeProvider::address()},
+		{"msg.sig", TypeProvider::fixedBytes(4)},
+		{"msg.value", TypeProvider::uint256()},
+		{"tx.gasprice", TypeProvider::uint256()},
+		{"tx.origin", TypeProvider::address()}
+	};
+}
+
+std::map<std::string, SortPointer> transactionMemberSorts()
+{
+	// NOTE: `blockhash` and `blobhash` need proper `ArraySort`, `smtSort()` wraps array types into array+length pair
+	auto toSort = [&](auto const& entry) -> SortPointer
+	{
+		if (entry.first == "blockhash" || entry.first == "blobhash")
+			return std::make_shared<ArraySort>(SortProvider::uintSort, SortProvider::uintSort);
+		return smtSort(*entry.second);
+	};
+	auto types = transactionMemberTypes();
+	return types
+	| ranges::views::transform([&](auto const& entry) { return std::make_pair(entry.first, toSort(entry)); })
+	| ranges::to<std::map<std::string, SortPointer>>();
+}
 }

libsolidity/formal/SymbolicTypes.h

@@ -86,4 +86,6 @@ std::optional<smtutil::Expression> symbolicTypeConversion(frontend::Type const*
 smtutil::Expression member(smtutil::Expression const& _tuple, std::string const& _member);
 smtutil::Expression assignMember(smtutil::Expression const _tuple, std::map<std::string, smtutil::Expression> const& _values);
 
+std::map<std::string, frontend::Type const*> transactionMemberTypes();
+std::map<std::string, smtutil::SortPointer> transactionMemberSorts();
 }

scripts/error_codes.py

@@ -205,6 +205,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False):
         "7053", # Unimplemented feature error (parsing stage), currently has no tests
         "2339", # SMTChecker, covered by CL tests
         "6240", # SMTChecker, covered by CL tests
+        "2788", # SMTChecker: BMC: verification condition(s) could not be proved
         "1733", # AsmAnalysis: expecting bool expression (everything is implicitly bool without types in Yul)
         "9547", # AsmAnalysis: assigning incompatible types in Yul (whitelisted as there are currently no types)
     }