Steady progress towards fully type-checked machine-check.
Last few months, I have been working on proper machine-check typechecking. Although this has been harder than anticipated, I was able to build a context-based framework where types are tracked using type ids. The progress is as follows, going between the contexts that contain definitions and types:
- The syn items describing the Rust code are converted to the internal representation where all names are expanded to their full forms, and representation internal to machine-check is built for everything except the function bodies.
- The internal representation of function bodies is built; it can contain variables and calls where type inference is needed.
- A type inference algorithm runs and produces an error if proper inference could not be made.
- The fully typed context is lowered to a version that only uses primitives that machine-check can abstract (bitvectors and bitvector arrays).
- The lowered version is used to construct the Rust-code version for forward computation that will be compiled for better speed (only for descriptions, not for properties) and a universal Intermediate Representation version that is used interpreted.
Nicely, I was able to make property and description creation much more similar to each other than before, deduplicating or simplifying code. I still need to work on a lot of internal details, including the proper inference, converting hard-coded functions for basic primitives into non-hard-coded versions where their signature is used normally for purposes such as inference, basic lifetime typechecking, and re-adding support for all previously available features. That said, the main groundwork is done and seems reasonable.
Aside from my work on machine-check, our new paper on Roole and Roolean Lean Certified Bitvector Solving without Bitblasting has been accepted and I will present it at the conference FMCAD 2026.
Until next time!