Version 0.5.0: Division, nicer error spans, dual-interval domain

Eliminating the technical debt and getting the benefits. No breaking changes (hopefully).

I'm happy to announce that a new version of machine-check, 0.5.0, has been released!

For this version, I planned to keep the user-facing API as-is, but refactor the underlying implementation of the description translation (i.e. what is happening in the macro machine_description) and make the abstraction domains more flexible so that more domains could be introduced for faster and more powerful verification. While this took a lot of time, eliminating the technical debt allowed me to add new capabilities fairly easily.

On a related note, I have successfully defended my dissertation thesis on the techniques used in machine-check and was awarded a doctoral degree! This is just the end of the beginning: I hope to keep improving machine-check so it is practically useful and we can use it to build safer and more secure systems.

Important changes in version 0.5.0

• Division and remainder are now supported for both unsigned and signed bit-vectors. They are wrapping: panic on zero, but not on signed overflow.
• Errors that occur within machine_description now have correct spans. Multiple errors can now be shown at the same time.
• A new dual-interval abstraction domain, currently opt-in through the feature Zdual_interval.
• Added a system crate for verifying hardware systems in the Btor2 format.

Adding division and remainder was previously problematic since they can panic when the divisor is zero, and this also precluded me from publishing the hardware system verification crate. Without the baggage of the technical debt, we can now enjoy all basic operations with bit-vectors.

Improving the support for the abstraction domain was also indirectly made possible by the translation rewrite, allowing me to figure out what must be supported by each domain. The dual-interval domain is now implemented, but not yet enabled by default due to state space size issues due to the increased precision.

On a less positive note, the build times for the systems have regressed (seem to be longer up to 2x) due to the new translation, which seems to be mainly due to the Rust compiler passes on the generated code (now less compact). I think this is acceptable for now, and the generated code can be optimised in the future thanks to the more reasonable translation code.

What's next

While description translation was the weak point of machine-check prior to 0.5.0, the new weak point are properties and state-space generation/refinement strategies, which are closely linked: the generation and refinements are guided by the property we want to verify. One of my next goals is to process the properties as a subset of Rust using the same translation as for the systems (just at runtime). This will allow better generation and refinements, making the dual-interval domain and other upcoming domains (such as relational ones) useful.

I also think that support of parametric systems is necessary to be able to reason well about systems such as processors. Currently, the only way to have a part of a system (e.g. a processor peripheral) unimplemented in a machine-check system is to raise a panic when it is used. Parametric descriptions would allow us to proceed normally with verification of properties where the interaction with the part is irrelevant, only giving an indefinite verification result if the property depends on the parameter. As far as my understanding goes, this should be possible to do very nicely within the used abstraction refinement framework.

I anticipate the next release to be breaking, bringing new features to properties and systems while smoothing out previous bad design decisions (such as the machine_check::Input and machine_check::State marker traits).

Until next time!