Комментарии 2
Возможно запускать SMTChecker из под Foundry? Я знаю, что Foundry использует под капотом solc для компиляции. Это было бы более удобно, потому что в разработке смарт-контрактов вряд ли кто-то компилирует через solc.
Привет! Да, можно, ведь, как вы правильно сказали, Foundry использует solc, а SMTChecker является его частью, но в Foundry он не включен по-умолчанию, и не отображает результаты чекера в forge test .
Вот, что написано об этом в файле Readme у Foundry:
то есть нужно подключать самостоятельно:
Необходимо добавить соответствующую директиву в ваш смарт-контракт
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
pragma experimental SMTChecker;
Также нужно в файле foundry.toml активировать SMTChecker (передать solc аргументы)
[profile.default] solc_args = ["--model-checker-engine", "all", "--model-checker-timeout", "20000"]
Напрямую Foundry ответ SMTChecker не отдает, но при запуске
forge build
выпадут варнинги, которые SMTChecker отдал для проваленных утверждений (аssertions)
Но лучше посмотреть полный отчет, а для этого все-таки скомпилировать напрямую с solc
solc --model-checker-engine all --model-checker-timeout 20000 MyContract.sol
Формальная верификация смарт-контрактов Solidity: SMTChecker