-
Notifications
You must be signed in to change notification settings - Fork 130
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
conflict_tests_from_alloy in miniscript/ms_tests.rs does not actually test for timelock mixing #514
Comments
Hi @benma, thanks for taking a look at 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.
EDIT: There is some error in conflict_tests_from_alloy because they implemented a simple algorithm for detecting timelock mixing. For example, Comments on alloy timelock test algorithm: sipa/miniscript#41 (comment) |
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. |
Thanks. It would be better if you could fix the tests to include timelock mixing though. Btw, what does |
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 😬. |
@benma the spec in Alloy that is discussed is here: https://github.com/dgpv/miniscript-alloy-spec (implemented in Alloy 5). You add a |
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 forafter
. It seems as if the test would check for that by the absence of thek
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 addk
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.
The text was updated successfully, but these errors were encountered: