Version 0.7.0: Interpreted properties and descriptions, equality domain

More options and much improved compile time.

I am happy to release machine-check 0.7.0! This release solves a long-standing problem of long compilation times, adds more expressivity to properties, and allows support for new abstraction domains. An equality domain has been added behind a feature gate.

Previously, the macro machine_description only generated additional Rust code to be compiled: the abstract analogue of the system, used for stepping (generating the state space), and the refinement analogue, used to find the reasons for unknown verification results so that machine-check could figure out which refinements to make. In practice, the abstract analogue works very well, since it essentially executes almost the same code as the original, just adjusted to use abstract domains and to properly work with if-else conditions. The refinement analogue is a different story; it reasons "backwards" from the unknown result, while also taking the abstract values into account. This brought two big disadvantages:

• It was very hard to implement and change, since the produced code must be valid Rust.
• The generated code is fundamentally very complex, making a lot of problems for the Rust compiler optimisation passes. For machine-check-avr, compilation in release mode took 5+ minutes!

Another pain point was that properties are supplied when the verifier executable is running, so we do not have the compiler available. As such, the property format used completely separate handling for verification.

The solution? Leave the abstract analogues as-is, but replace both the refinement analogues and properties by intepretation of the supported Rust subset. After a lot of work, it turns out that this idea actually works very well: the verification logic is now easier, compilation time for machine-check-avr has improved to seconds, and new abstract domains can now be added much more easily, as evidenced by the new added equality domain.

Important changes in version 0.7.0

• Minimum Supported Rust Version has been raised to 1.88.
• Compilation times have improved dramatically, and the Rust compiler optimisations no longer overflow its stack for large systems (which forced managing RUST_MIN_STACK).
• Properties are now written in a subset of Rust similarly to systems. This also allows more advanced uses such as system hierarchy checking.
• A feature-gated equality domain has been added.

The good news is that everything that previously did not panic or produce errors should be completely backward-compatible. However, in version 0.7.0, checks for monotonicity of properties are no longer performed, as the expressions can now be arbitrarily complex. This means that you can now put verification into an infinite loop as simply as lfp![X, !X]. I do not consider this to be a soundness problem as valid (monotone) properties will still produce sound results. However, I am looking into how to cheaply detect breaking monotonicity during computation of the properties, which is not trivial for μ-calculus.

What's next

Since the compilation woes for large systems have been solved, the next thing on the list is to implement a simple RISC-V core. The obvious challenge is stepping up from an 8-bit microcontroller in machine-check-avr to a 32-bit one, which precludes verification even with a single failure to refine well (forcing 2³² new states). However, machine-check should be able to verify carefully crafted toy programs for RISC-V, and the ways the failures to verify occur should guide us to better abstraction and refinement choices.

All in all, I am now quite satisfied with the overall richness of abilities that machine-check offers. There is a lot of exciting avenues to enhance the performance and usability, but the fundamentals have been set.

Until next time.