halmos icon indicating copy to clipboard operation
halmos copied to clipboard

HuffDeployer is not supported

Open 0xkarmacoma opened this issue 1 year ago • 1 comments

Describe the bug

The huff deployer from foundry-huff does a lot of things under the hood and we don't support it atm.

To Reproduce

  • install foundry-huff
  • use the following test
// SPDX-License-Identifier: MIT
pragma solidity 0.8.20;

import {HuffDeployer} from "foundry-huff/HuffDeployer.sol";

contract HuffDeployerTest {
    function check_huff_deploy() public {
        address horseStoreHuffAddr = HuffDeployer.config().deploy("BeepBoop");
    }
}
  • run halmos --function check_huff_deploy --debug --ffi

It fails with:

[FAIL] check_huff_deploy() (paths: 0/1, time: 2.45s, bounds: [])
WARNING:Halmos:Encountered expected concrete value but got: Concat(35729062061041830401508663135,
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(255, 248, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(247, 240, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(239, 232, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(231, 224, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(223, 216, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(215, 208, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(207, 200, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(199, 192, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(191, 184, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(183, 176, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(175, 168, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(167, 160, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(159, 152, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(151, 144, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(143, 136, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(135, 128, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(127, 120, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(119, 112, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(111, 104, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(103, 96, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(95, 88, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(87, 80, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(79, 72, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(71, 64, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(63, 56, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(55, 48, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(47, 40, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(39, 32, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(31, 24, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(23, 16, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(15, 8, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       97 + Extract(7, 0, evm_bvurem(Concat(0, Extract(7, 0, sha3_256(72560991576473913183248421186648683548549615480347232343958955200863790956544))), 26)),
       5260439343571744160932091487846)
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)
Symbolic test result: 0 passed; 1 failed; time: 2.45s

0xkarmacoma avatar Oct 31 '23 15:10 0xkarmacoma