We have an idea and want to ask if that makes sense.
To formally verify Cairo programs, a possible approach is to translate the Cairo code to identical Rust and then use the existing formal verification tools for Rust.
Using Rust as a backend has the advantage of reusing a lot of work done on formal verification tooling. It is also a language similar to Cairo, so there is not much loss of information/noise in the translation.
Does this sound technically possible? Would there be an interest in this development?
My intuition is that a fully fledged compiler is far from simple and is probably overkill. The main potential issues I can think of are:
While the languages are similar, there are some nontrivial differences (e.g. traits/impls, some Cairo-specific types, arrays being write once)
The smart contract syntax, which is usually the source of interest in the context of formal verification, is something you’ll have to define in Rust
I’m mostly concerned about 2. As a side note, there is an effort for the other direction (LLVM–>Cairo); see Hieratika, though it’s not maintained at the moment.
The way traits are inferred can be a source of trouble indeed, as this is generally a fragile mechanism in programming languages. For Cairo-specific types/functions, I guess they can be defined on the Rust side also. For the “write-once” aspect of data structure, I guess that if Rust is less restrictive, then it should always type-check Cairo programs, but we need to look more into it.
OK, I need to understand how it works in detail. If the smart contract attributes are macros, then it is fine, as we can expand them, as it is “just” regular syntax, but more verbose. If they are built-ins, then we need to represent them somehow on the other side. My intuition is that, anyway, we would need to represent these constructs in a formal language if we want to verify Cairo, and it would be as much of an effort as representing them in Rust.
OK, thanks for the link to Hieratika; that also sounds very interesting!
