Virtual machine in Rust type system

tutorials
1

Hello!

I wrote a virtual machine in the Rust type system! (Why not.)

This is a follow-up to a CTF challenge I wrote. It is a small proof-of-concept virtual machine embedded in the Rust type system, which uses trait resolution and in particular associated types to "execute" a program, represented as a type, to its final state. (The "execution" happens during Rust compilation.)

The VM architecture is simple: two 8-bit registers, a stack, a small number of instructions, including conditional control flow. However, other than patience and hitting the recursion limits, more useful/realistic architectures could be embedded as well.

I wrote a blog post that goes into more depth about how this was developed and how it all works: thenet / Virtual machine in Rust type resolution

The repository with all the (cleaned-up) code is here: GitHub - Aurel300/type-system-vm: VM in the Rust type system.

6 Likes
2

Nice read!
Rust unhinged got to the next level, and now rust has an insane performance stress test for its trait resolver. :grin:

1 Like
3

Amazing. Totally nuts but brilliant. Clearly I have some things to learn about Rust from this...

2 Likes
4

So have you ran across trait resolver bugs like the one in cve-rs? Associated types look a bit scary, on a bug they could unify to anything.

5

I assume the end state would be running doom

It took typescript 177TB of types, so maybe stock up on RAM.

3 Likes
6

No, I didn't really run into (scary) bugs. The issue that was solved with -Znext-solver was the result of compiler checking some impl blocks too eagerly, even though they were not actually candidates for selection (if I understand it correctly). This is technically fine: it just disallows some programs that should actually type check, i.e., it is a completeness issue, not a soundness one.

Apart from that I thought I found a problem that caused the compiler to hang indefinitely, but as I note in the blog post, I think it's actually just that the time to perform the error reporting scales really badly with the number of (related) impl blocks.

Also cve-rs does not seem to be related to trait resolution, right?

1 Like
7

You can control order of evaluation of associated types by using GATs

For example, I used it to great effect to embed lambda calculus into the type system.

This way I could iteratively reduce until I got a normal form, and stop. Instead of the Rust type system just unfolding infinitely.