HuffDeployer is not supported

[karmacoma-eth]

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

[karmacoma-eth]

These bytes are coming from the following function in HuffConfig:

    function bytes32ToString(bytes32 x) internal pure returns (string memory) {
        string memory result;
        for (uint256 j = 0; j < x.length; j++) {
            result = string.concat(result, string(abi.encodePacked(uint8(x[j]) % 26 + 97)));
        }
        return result;
    }

HuffConfig:

• executes rand_bytes.sh
• keccak's them
• passes the hash to bytes32ToString to obtain rand_bytes
• uses these rand_bytes to create a temporary file name tempFile = string.concat("__TEMP__", rand_bytes, tempFile)
• uses this tempFile name in another ffi command:

        // Paste the code in a new temp file
        string[] memory create_cmds = new string[](3);
        // TODO: create_cmds[0] = "$(find . -name \"file_writer.sh\")";
        create_cmds[0] = "./lib/foundry-huff/scripts/file_writer.sh";
        create_cmds[1] = string.concat("src/", tempFile, ".huff");
        create_cmds[2] = string.concat(code, "\n");
        vm.ffi(create_cmds);

I think it's during that last ffi command that we encounter the concretization failure