Huff doesn't work

[PatrickAlphaC]

Describe the bug I am trying to symbolic execution/formal verification for a huff contract. When I run my halmos command:

halmos --function check_storeAndReadAreIdentical

I get the following error in my foundry project:

Running 1 tests for test/HorseStoreSymbolic.t.sol:HorseStoreSymbolic
[FAIL] check_storeAndReadAreIdentical(uint256) (paths: 0/2, time: 0.03s, bounds: [])
WARNING:Halmos:Encountered Unknown contract call: to = 0x0000000000000000000000000000000000000000; calldata = Concat(0xcdfead2e, p_randomNumber_uint256); callvalue = 0x0000000000000000000000000000000000000000000000000000000000000000
(see https://github.com/a16z/halmos/wiki/warnings#internal-error)

My test suite works great for foundry tests:

// SPDX-License-Identifier: MIT
pragma solidity 0.8.20;

import {HuffDeployer} from "foundry-huff/HuffDeployer.sol";
import {HorseStore} from "../src/HorseStore.sol";
import {HorseStoreYul} from "../src/HorseStoreYul.sol";
import {Test, console2} from "forge-std/Test.sol";

abstract contract Base_Test is Test {
    string public constant horseStoreLocation = "HorseStore";
    HorseStore horseStoreHuff;
    HorseStore horseStoreSol;

    function setUp() public virtual {
        horseStoreHuff = HorseStore(HuffDeployer.config().deploy(horseStoreLocation));
        horseStoreSol = new HorseStore();
    }
    
    function check_storeAndReadAreIdentical(uint256 randomNumber) public {
        horseStoreHuff.updateHorseNumber(randomNumber);
        horseStoreSol.updateHorseNumber(randomNumber);

        assert(horseStoreHuff.readNumberOfHorses() == randomNumber);
        assert(horseStoreSol.readNumberOfHorses() == randomNumber);
    }

It's a minimal contract that essentially stores a variable at storage slot 0, and has a function to read the value in that slot.

In solidity:

// SPDX-License-Identifier: MIT
pragma solidity 0.8.20;

contract HorseStore {
    uint256 numberOfHorses;

    function updateHorseNumber(uint256 newNumberOfHorses) external {
        numberOfHorses = newNumberOfHorses;
    }

    function readNumberOfHorses() external view returns (uint256) {
        return numberOfHorses;
    }
}

In huff:

/* Interface */
#define function updateHorseNumber(uint256) nonpayable returns ()
#define function readNumberOfHorses() view returns (uint256)

/* Storage Slots */
#define constant VALUE_LOCATION = FREE_STORAGE_POINTER()

/* Methods */
#define macro SET_VALUE() = takes (0) returns (0) {
    0x04 calldataload   // [value]
    [VALUE_LOCATION]    // [ptr, value]
    sstore              // []
    stop
}

#define macro GET_VALUE() = takes (0) returns (0) {
    // Load value from storage.
    [VALUE_LOCATION]   // [ptr]
    sload                // [value]

    // Store value in memory.
    0x00 mstore

    // Return value
    0x20 0x00 return
}

#define macro MAIN() = takes (0) returns (0) {
    // Identify which function is being called.
    0x00 calldataload 0xE0 shr
    // __FUNC_SIG("updateHorseNumber(uint256)")
    // cast sig "updateHorseNumber(uint256)"
    // dup1 0xcdfead2e eq set jumpi
    dup1 __FUNC_SIG(updateHorseNumber) eq updateJump jumpi
    
    // __FUNC_SIG("readNumberOfHorses()")
    // cast sig "readNumberOfHorses()"
    dup1 __FUNC_SIG(readNumberOfHorses) eq readJump jumpi

    updateJump:
        SET_VALUE()
    readJump:
        GET_VALUE()
}

To Reproduce

Clone and setup the repo:

1. git clone https://github.com/Cyfrin/10-horse-store-s23
2. cd 10-horse-store-s23
3. git checkout b097c2a

Rm lib cuz foundry weirdness

4. rm -r ./lib

Install dependencies, and run the halmos command.

5. forge install huff-language/foundry-huff --no-commit
6. forge build
7. halmos --function check_storeAndReadAreIdentical

Environment:

• OS: MacOS
• Python version: Python 3.10.6
• Halmos and other dependency versions:

halmos==0.1.9
z3-solver==4.12.2.0

Additional context Add any other context about the problem here.

We have solved it with a work around where we just etch the bytecode into a dummy contract.

// using deployment bytecode:
//      huffc src/HorseStore.huff --bytecode
bytes memory deployBytecode = hex"602b8060093d393df35f3560e01c8063cdfead2e1461001b578063e026c01714610022575b6004355f55005b5f545f5260205ff3";
address horseStoreHuffAddr;
assembly {
    horseStoreHuffAddr := create(0, add(deployBytecode, 0x20), mload(deployBytecode))
}
horseStoreHuff = HorseStore(horseStoreHuffAddr);