Rust Implementation Request for Comments

[Kevin Milner]

Hi all,

The last while I have been working on (with the help of LLMs) a rust port of tamarin. It is obviously not ready for any adoption but I'd like to submit it for anyone interested to evaluate. It is stable but does not currently implement accountability or diff equivalence modes. However, almost every other feature should work correctly.

Why try it: it is much much faster and lighter than the Haskell code, even after the Haskell optimisations I've implemented over the last couple months, and generates identical proofs across every applicable example in the tamarin repository. You can for example try autoproving or using the interface in the rust and then validate the proof with the Haskell version. If you find a mismatch please send me the file so I can investigate!

You can find the code and build instructions here: https://github.com/kmilner/tamarin-prover/tree/rust-port/rust

Some performance numbers for comparison are included in the README at that link. In general it is at least ~4x faster (ranging from about 2-37x, yes that's 37x, depending on the theory and core count) and typically uses about a quarter as much memory (ranging from about 2-26x less, and again 26x is not a typo, depending on the theory and core count). It generally scales better across multiple cores as well.

This is a work in progress, and absolutely nowhere close to supplanting the Haskell, not the least because far far too much of this code was written and reviewed by LLMs (albeit with a very extensive grounding framework against the exact proof system of the Haskell at each step). But I believe it's now in a state where it is close enough that some folks working on larger theories might find it useful to try out, on the basis that it will be faster in many cases to prove on the rust and validate the proof with the Haskell than it is to prove on the Haskell directly, or to (for example) use the rust locally to try their tactics etc and then hand off to a server with much more memory to generate the real proofs.

This comes with two minor caveats:
- Tamarin has two outstanding issues preventing proofs from being revalidated in certain limited cases, https://github.com/tamarin-prover/tamarin-prover/pull/872 and https://github.com/tamarin-prover/tamarin-prover/pull/882, so nothing can be done in those cases at the moment. However the proofs for affected files are identical in rust to what they would be if those fixes were in place in Haskell.

- Some variable numberings are slightly different, because of the way queries are submitted to Maude. This *should* never affect a proof, the only time you should ever see it is if you look at the full proof system (e.g. in interactive mode) and compare it between the rust and the Haskell, you will sometimes find that variables are numbered slightly differently.

Do let me know your thoughts and suggestions! This started as a small hobby project, and the process of getting it working and grounding the development against real tamarin helped me find a wide variety of optimisations and minor bugs in real tamarin, which I think of as arguably the main output of the project. But the result did end up being much faster and lighter as well, so it might be useful on its own to people. I'll look at moving it out into its own repository with extensive notes in the future if it is.

Cheers,

Kevin