conflict_tests_from_alloy in miniscript/ms_tests.rs does not actually test for timelock mixing

[benma]

File: https://github.com/rust-bitcoin/rust-miniscript/blob/a0648b3a4d63abbe53f621308614f97f04a04096/src/miniscript/ms_tests.rs (the file is too large to link directly to the test function).

It seems the test vectors in the conflict_tests_from_alloy test all contain timelock mixing for after. It seems as if the test would check for that by the absence of the k type property in the expected types, but this property is never added, even for expressions that do not contain any timelock mixing.

It seems to me that that impl fmt::Display for TestType should add k if there is no timelock mixing and add this type property to all tests in the file where it applies.

Maybe I misunderstand this test - if so, please let me know.

[sanket1729]

It seems to me that that impl fmt::Display for TestType should add k if there is no timelock mixing and add this type property to all tests in the file where it applies.

Hi @benma, thanks for taking a look at rust-miniscript. Indeed the property for k is not printed for TestType.

Those test vectors were obtained from another contributor's work and did not include "k" property. You are right that the test is not actually checking for timelock mixing. I will create a quick fix for it.

All of the tests in conflict_tests_from_alloy should have timelock mixes.

EDIT: There is some error in conflict_tests_from_alloy because they implemented a simple algorithm for detecting timelock mixing. For example, or(after(HEIGHT), after(TIME)) is not an issue because they both cannot be executed together. Only when we have a and of two mixes is there an issue. This is why we could not use the test vectors directly to check the k property from alloy implementation.

Comments on alloy timelock test algorithm: sipa/miniscript#41 (comment)

[sanket1729]

Opened #516 clarifying it. As mentioned above because of the other algorithm used in alloy test vectors, we could not test it. I remember cross testing this across bitcoin core implementation to see that timelock mixing worked correctly, but I don't have test vectors for those here.

[benma]

Thanks. It would be better if you could fix the tests to include timelock mixing though.

Btw, what does alloy mean, and how were this tests generated? Would be nice to have some documentation on it. I am interested in reusing the tests.

[apoelstra]

I believe this is Alloy: https://haslab.github.io/formal-software-design/overview/index.html

It is some sort of formal verification tool. @dgpv implemented Miniscript in this a couple years ago and was able to find a bug -- it looks like Sanket pulled in his test cases in #254. I believe at the time we all agreed "gee, this is spectacular, I should learn Alloy and figure out how he did this" but AFAIK none of us actually did 😬.

[dgpv]

@benma the spec in Alloy that is discussed is here: https://github.com/dgpv/miniscript-alloy-spec (implemented in Alloy 5). You add a check into miniscript.als that would constitute the configuration of your interest, and then execute this check in Alloy to find an example of the miniscript with this configuration (or if you want to check that the spec doesn't allow particular configurations, you run the check and expect Alloy to not find any examples). The test cases in question were generated by automating the Alloy GUI (with pyautogui AFAIR) to generate examples, save it to .dot file, generate next example, etc. Then .dot files were converted with parse_miniscript_dot.py to miniscript. (Note that Alloy can be automated with Java plugins IIRC, but gui automation was the easy option)