Human readable counterexamples

[aviggiano]

Is your feature request related to a problem? Please describe.

I would like to see clear, human-readable versions of Halmos counterexamples, such as in fuzzing tools like Foundry, Echidna, and Medusa.

Currently, Halmos counterexamples contains both symbolic and concrete values, which are harder to understand. Given that this information already exists on my contracts ABIs, it should be possible to convert the current output to something much cleaner for most cases.

For example, take the following output from this test

Counterexample: 
    halmos_block_timestamp_depth1_d16404c = 0x8000000000000000
    halmos_block_timestamp_depth2_9582fea = 0x8000000000000000
    halmos_msg_sender_0x00000000000000000000000000000000aaaa0002_7c584f7_02 = 0x30000
    halmos_msg_sender_0x00000000000000000000000000000000aaaa0009_0a81e90_48 = 0x30000
    halmos_msg_value_0x00000000000000000000000000000000aaaa0002_99477cc_03 = 0x00
    halmos_msg_value_0x00000000000000000000000000000000aaaa0009_eaeb5de_49 = 0x00
    p_amount_uint256_796aa27_51 = 0x2f86489e
    p_spender_address_3e99520_04 = 0xaaaa0009
    p_to_address_284592d_50 = 0x8000000000000000000000000000000000000000
    p_value_uint256_856fd78_05 = 0x4000000000000000000000000000000000000000000000000000000000000000
Sequence:
    CALL 0xaaaa0002::approve(Concat(p_spender_address_3e99520_04, p_value_uint256_856fd78_05)) (value: 
halmos_msg_value_0x00000000000000000000000000000000aaaa0002_99477cc_03) (caller: halmos_msg_sender_0x00000000000000000000000000000000aaaa0002_7c584f7_02)
        ...
    CALL 0xaaaa0009::deposit(Concat(p_to_address_284592d_50, p_amount_uint256_796aa27_51)) (value: 
halmos_msg_value_0x00000000000000000000000000000000aaaa0009_eaeb5de_49) (caller: halmos_msg_sender_0x00000000000000000000000000000000aaaa0009_0a81e90_48)
        ...

This could be translated to:

vm.warp(0x8000000000000000);
vm.prank(address(0x30000));
usdc.approve(address(token), 0x4000000000000000000000000000000000000000000000000000000000000000);
vm.warp(0x8000000000000000);
vm.prank(address(0x30000));
token.deposit(0x8000000000000000000000000000000000000000, 0x2f86489e);

Describe the solution you'd like

A more human readable formatting for logs

Describe alternatives you've considered

Manually doing what I just mentioned. See here

Additional context

N/A