Making system descriptions and Graphical User Interface nicer to use.
I am happy to state that machine-check has been selected
for a grant to enhance its usability by the NLnet foundation.
My hope is that by the start of 2027, machine-check will be much nicer to use, especially when writing systems and properties.
Let's demonstrate on an example of how to convert a four-bit bitvector to an eight-bit one by adding zeros to the left.
Currently, it must be done in a very cumbersome way (and this is after importing Bitvector, Into, etc. to scope):
// a four-bit bitvector with the value 9 (1001 in binary)
let var1 = Bitvector::<4>::new(9);
// convert it into a four-bit bitvector behaving as unsigned
let var2 = Into::<Unsigned<4>>::into(var1);
// extend it to 8 bits
let var3 = Ext::<8>::ext(var2);
// stop it from behaving as unsigned
let var4 = Into::<Bitvector<8>>::into(var3);
// var4 is now an eight-bit bitvector with the value 9 (00001001 in binary)
This is incredibly annoying to deal with when writing processors where this needs to be done dozens of times (ugh!).
Let's consider just the width extension for now. What we would like is to write something like:
// we have var2, a bitvector behaving as unsigned, extend it to 8 bits
let var3: Unsigned<8> = var2.ext();
Unfortunately, method calls are currently not supported by machine-check since this requires precise information about types and visibility to decide which actual function to call.
While it would be possible to somehow integrate machine-check with the Rust compiler to get precise type information, I have decided against this early on as it brings a dependency on the whole Rust compiler toolchain which is large, complicated, and under active development.
Instead, I decided to implement a sound type and borrow checker for the supported subset of Rust, which doesn't include complicated things such as function pointers, lambdas, etc. This is doable, but still hard, as Rust includes type inference based on the Hindley-Milner type system with a lot of customisation. Not the easiest thing around. And after this is implemented, borrow checking must be implemented as well! Fortunately, unlike the Rust compiler, this doesn't need to be very fast, as the machine descriptions tend to be much smaller than normal Rust programs with their all dependencies.
Once type- and borrow-checking is implemented, I want to also add better support for other important part of Rust such as tuples, enumerations etc., and generally make things nicer for the user. For example, there could be a function on basic bitvectors to do a zero-extension:
// a four-bit bitvector with the value 9 (1001 in binary)
let var1 = Bitvector::<4>::new(9);
let var2: Bitvector<8> = var1.zero_ext();
// var2 is now an eight-bit bitvector with the value 9 (00001001 in binary)
This year, I also want to focus on better automation and a nicer Graphical User Interface. Unlike the vast majority of verification tools, machine-check has a GUI since the last year and it has helped me in figuring things out many times already. However, it leaves lots to be desired. Good visualisation is the core of understanding, so the need for improvements can't be underestimated.
One thing I didn't touch on in this post yet was the performance of the model checking itself. This is something I am working on (in a bit of a roundabout way) in my position at the University of Freiburg. I will have another blogpost ready about that in a few weeks. Until next time!