fix(BV): Do not lose explanations in bvmul #1170
Conversation
The implementation of bvmul from OCamlPro#1144 introduced a soundness bug: when we do not know anything about the result, the explanation is dropped. This is because the implementation was performing mixing bitlist computation and creation of raw bitlist values. This patch fixes the implementation by performing all computations in [Z] and only adding the explanation at the end.
bclement-ocp
force-pushed
the
bvmul-soundness
branch
from
0eb8e50 to
7ce7868
Compare
|
Can you add a test that caught the soundness bug in the previous code? |
|
Yes and no — I don't have a reproducer on next. I have one on #1152 where it was found, but the propagators run in a different order on I can add the reproducer that breaks on #1152 even though i don't think it is very robust to changes in propagation strategy. Now that I understand the issue I will see if I can make a more robust test |
|
Sure, if the test is not robust we shouldn't add it. |
|
Thinking about it more, I think the test is actually fairly robust but very hard to trigger on I have added the test. |
* fix(BV): Do not lose explanations in bvmul The implementation of bvmul from OCamlPro#1144 introduced a soundness bug: when we do not know anything about the result, the explanation is dropped. This is because the implementation was performing mixing bitlist computation and creation of raw bitlist values. This patch fixes the implementation by performing all computations in [Z] and only adding the explanation at the end. * Add a test
The implementation of bvmul from #1144 introduced a soundness bug: when we do not know anything about the result, the explanation is dropped.
This is because the implementation was performing mixing bitlist computation and creation of raw bitlist values. This patch fixes the implementation by performing all computations in [Z] and only adding the explanation at the end.