Upstream simplified Optimism test

[palinatolmach]

Closes #366.

This PR upstreams a simplified Optimism test PortalTest that can be used for performance profiling:

/// @custom:kontrol-array-length-equals _withdrawalProof: 1,
/// @custom:kontrol-bytes-length-equals _withdrawalProof: 32,
function test_withdrawal_paused(
    Types.WithdrawalTransaction memory _tx,
    uint256 _l2OutputIndex,
    Types.OutputRootProof calldata _outputRootProof,
    bytes[] calldata _withdrawalProof
)
    external
{
    vm.expectRevert();
    portalContract.proveWithdrawalTransaction(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
}

It also adds a set of lemmas needed for this test (pausability-lemmas.k), and renames an existing file with lemmas for the sumToN test (sum-to-n-lemmas.k).

The execution of this test on my machine takes:

• 5m19s using latest (v0.1.204) Kontrol
• 7m40s using v0.1.178
• 15m15s using v0.1.176
• 11m40s using v0.1.176 with booster overwritten to d299753 (with simplifier cache enabled)

[palinatolmach]

The CI job with a new test got killed (https://github.com/runtimeverification/kontrol/actions/runs/7898491231/attempts/1?pr=369, and then timed out in 2 hours), and on my machine it also takes > 1 hour — I'll look into how it can be further minimized while still being illustrative of the performance changes.

[palinatolmach]

The following test (which is too simple to be illustrative of the performance difference between backend versions):

    /// @custom:kontrol-length-equals _withdrawalProof: 3,
    /// @custom:kontrol-length-equals data: 32,
    /// @custom:kontrol-length-equals _withdrawalProof[]: 32,
    function test_withdrawal_paused(
        Types.WithdrawalTransaction calldata _tx,
        uint256 _l2OutputIndex,
        Types.OutputRootProof calldata _outputRootProof,
        bytes[] calldata _withdrawalProof
    )
        external
    {
        portalContract.pause();
        vm.expectRevert();
        portalContract.proveWithdrawalTransaction(_tx, _l2OutputIndex, _outputRootProof, _withdrawalProof);
    }
}

takes ~6 minutes to run locally on my machine and ~8 minutes — on CI when executed by a faster runner. It seems that we're getting very different execution time on booster tests depending on the runner, e.g.,

• github-runner-2 consistently took more than 2 hours to run a job: https://github.com/runtimeverification/kontrol/actions/runs/7914368796/job/21642139595, while
• github-runner-36 finished it in 1h8m: https://github.com/runtimeverification/kontrol/actions/runs/7927923233/job/21645283356

Making the test more challenging (and lemma-dependent) is needed to ensure that we can observe the difference in performance, however, it seems that it would also cause time outs in many CI runs. With @JuanCoRo, we've also realised that a cleanup of lemmas used to run this test is needed, and it seems that removing some of the lemmas improves the execution time w/o causing any issues — that's what I'm looking into now.

Update: while updating lemmas file and the test, both @JuanCoRo and I are encountering the following issue with Kontrol hanging at the end of the execution while seemingly being unable to stop the server: #375.

[palinatolmach]

I've pushed an updated test as well as contracts (OptimismPortal, Types) it's calling. The test demonstrates ~10% performance diffs between Kontrol/backend versions taking

• 12m using latest (v0.1.178) Kontrol
• 10m50s using v0.1.176 (before the recent performance regression got introduced)
• 9m55s using v0.1.176 with booster overwritten to use and update simplifier cache while checking rewrite rule conditions hs-backend-booster#503 (with simplifier cache enabled)

However, the test is the current format uses a different solc version from the rest of the test suite (0.8.15) and can be minimized further. These changes (like any other changes to the Solidity code) require modification of the copy-memory-to-memory lemma, that includes the following steps (instruction courtesy of @PetarMax):

• when hitting the first branching, get to 200 steps or so backward
• execute with --break-every-step for ~200 iterations, which should reveal the copying loop
• update the rule according to where the loop starts, where it ends, and what is the word stack structure at both of those points

[ehildenb]

@palinatolmach not sure, but can we get this merged? One of the next tasks for Qian is to investigate loop invariant inference using the merge-nodes functionality, so perhaps having this merged will make it easier for her. #448

[palinatolmach]

@ehildenb ok! I'll get it up to date and will merge in the morning. I think I can also remove the lemma that's causing a rewrite in another contract. I agree that it's probably good to merge it now, it would hopefully also help us avoid performance regressions while #442 is being investigated.

[palinatolmach]

Temporarily removed automerge to let #355 go through first.

I couldn't remove the lemmas causing the rewrite in another contract w/o affecting PortalTest performance, but the related investigation is factored out into #442. Otherwise, it's ready to be merged.