Support new 'hardhat' `--user-assert-mode`

[cd1m0]

Scribble is sometimes used to instrument the code for local testing. When this is done in a Hardhat environment, people often use console.log(...) to print out various information. In this mode, it is more convenient to signal user assertion failures with console.log() instead of emitting events, so that users can just look at their terminal instead of go hunting through the logs. In this mode we would support a new option for the --user-assert-mode key as follows.

Given the below sample:

contract Foo {
        /// #if_succeeds {:msg "Property 0 fail"} x > 0;
        function foo(uint x) public {}
}

When we instrument it with scribble --user-assert-mode hardhat tmp.sol we would get the following code:

import "hardhat/console.sol";

contract Foo {
    function foo(uint x) public {
        _original_Foo_foo(x);
        if (!(x > 0)) {
            console.log("0: Property 0 fail");
            assert(false);
        }
    }

    function _original_Foo_foo(uint x) private {}
}

Debug events would also be converted to console.logs. So running scribble --user-assert-mode hardhat tmp.sol --debug-events would produce:

import "hardhat/console.sol";

contract Foo {
    function foo(uint x) public {
        _original_Foo_foo(x);
        if (!(x > 0)) {
            console.log("0: Property 0 fail");
            console.log("x:", x);
            assert(false);
        }
    }

    function _original_Foo_foo(uint x) private {}
}

Note that the console.log() functions in hardhat are limited to up to 4 arguments, so extra work needs to be done when we need to print more than 4 values.

[Melvillian]

The flag --user-assert-mode is now in the docs https://docs.scribble.codes/tool/cli-usage, should this Issue be closed?

[cd1m0]

Good question @Melvillian - I think I didn't give enough detail in the description. Currently --user-asert-mode supports two possible options - log and mstore. These control exactly how user assertion failres are signaled in the instrumentation.

The suggestion in this PR is to add a 3rd possible option for --user-assert-mode - hardhat. In that mode, when you specify --user-assert-mode hardhat, it would emit console.log(...) statements to signal user assert failures. console.log is supported under hardhat, and is useful for local debugging.

Thus, I think the issue should still remain open, as a potential idea for a quality-of-life improvement