Independent testing of inner_test_validate_owner

[mariaKt]

inner_test_validate_owner is called from multiple tests, specifically the *multisig ones. This PR checks that this is not the source of any errors through two independent tests (multisig and no multisig).

Refactored version

Note that inner_test_validate_owner is designed to accept all parameters needed to computed the expected Result, as well as a Result parameter (utilized to provide the Result value already computed by another operation in our tests). During its execution, it computes the expected Result and asserts for equality with the actual Result. In order to be able to test it, I provided another, refactored version of it, that replicates it exactly but only computes the expected Result .

Proof correctness

I checked the split nodes of the proof for test_validate_owner_multisig to make sure that we explore the paths that we should. As expected, there are several branches for owner check, multisig checks, unsigned_exists result, signers_count result, multisig initialized, and many for the unsigned_exists closures. However, I found no branching for the signers_count closures.

I tested the exact same closures structure with the following small test, which passes

struct Wrapper {
    tag: u8,
    a: [[u8; 32]; 3],
}

fn main() {
    let c = Wrapper {
        tag: 42,
        a: [[1u8; 32], [2u8; 32], [3u8; 32]],
    };
    let d = Wrapper {
        tag: 84,
        a: [[1u8; 32], [3u8; 32], [5u8; 32]],
    };

    let equal_count = c.a
        .iter()
        .filter_map(|first| {
            d.a.iter().find(|second| {
                first == *second
            })
        })
        .count();

    assert!(equal_count == 2);

}

, so I am not concerned. My explanation is that this is due to the path conditions that are present when the signers_count is reached. Execution reaches this point only after evaluation of unsigned_exists, that needs to evaluate the same condition for the pairs of keys-signers. So, the path conditions placed to make the computation of unsigned_exists are enough to continue evaluation without branching. Please let me know what you think.

[mariaKt]

It would be good to eventually use the commented out version of this test (which calls the refactored function that only computes the result and then the one that uses it and calls inner_test_validate_owner, the one that is used by all the tests). This way, we would have a test that includes exactly the function called from the other tests.

Argument for: We should have a proof for this function if we plan to find a way to replace this call with a spec or a summary. I would like to have a discussion about this though, as I am not sure what is doable at this stage where we still modify the semantics.

Argument against: This changes the proof's time from ~10.5h to ~28.8h.

[mariaKt]

Using lemmas (for expected_validate_owner_result and inner_test_validate_owner), we can get the full test to execute in about 15min.