Comment by Jweb_Guru | Hacker News Reader

Comment by Jweb_Guru | Hacker News Reader

In addition to the project itself being very cool and useful (you can count the number of verified SAT solvers that can solve most problems in modern SAT competitions on two fingers!), it's also an impressive demonstration of its toolchain, which essentially exploits the fact that the purely safe fragment of Rust (augmented with a handful of types that use unsafe code like Vec, which I believe have been proven compatible with the rest of Creusot in another recent paper) behaves like a functional language. This allows borrow-checked Rust code to be treated purely functionally in safe contexts, which allows exploiting the large amount of existing software tailored to proving purely functional specifications, without having to worry about memory-related side conditions, separation logic, etc.

This has always been the hope for Rust verification tools (that Rust would scale to these kinds of large proofs better than other industrial imperative languages due to the restrictions of the borrow checker), and I think this is the first real practical indication that that is indeed the case. Both in terms of verification time and additional verification code, it weighs in at a small fraction of that of the only other verified solver with comparable performance on SAT benchmarks (IsaSAT), which is extracted using code generation from Isabelle (which is a full proof assistant), while other attempts to produce verified SAT solvers directly from imperative code fall far short of its performance because they do not implement any of the difficult optimizations (presumably due to the amount of extra proof effort required).

Incidentally, another paper has come out at basically the same time making a similar observation, Aeneas: https://arxiv.org/abs/2206.07185, which uses a resizable hash map as its case study. Since it just came out, it does not have any larger proof developments yet that could be used as comparison, and it has somewhat different goals, but overall I am also excited about it and am very hopeful for the future of verification tools that integrate directly with Rust code like these two, as I think they are one of the more promising avenues towards the regular integration of verified code with more "ordinary" projects.

Does the proof encompass some sort of proof of amount of RAM consumption in it, presumably bounded by some characteristic of the problem presented?

Regardless, this is very impressive, and one of the first things to raise my eyebrows w.r.t. formal proofs being possibly useful in the real world in a long time. If safe Rust can function as the bridge between the "practical" world and the world of proofs, that alone would be enough to justify Rust's existence.

No, it does not. This is mentioned as a limitation in the paper (it does, however, handle things like integer overflows correctly). I believe with some suitable extensions, it would be possible to prove invariants like this as well, but IMO functional correctness is a pretty good start!

It does assume enough RAM, as it has no way of knowing how much RAM the target machine will have. It is thus correct with regards to the model specified by Rust, but a program which is proven correct in Creusot may get an OOM-error. A note here is that it will not provide the wrong answer due to insufficient memory, but it will crash.

Proving some upper bound on the amount of memory used (and potentially gracefully exiting) should be possible, but I have not prioritised it, as OOM has not been an issue.

"has no way of knowing how much RAM the target machine will have"

That's why I phrased it in terms of a bound based on some characteristic of the problem.

But I was just asking for information. I know it's a well-known problem. To be honest the fact that we're even seriously discussing this as something that may be doable is a huge step forward. AIUI, previous state of the art on real languages would have this as hopelessly pie-in-the-sky.

I think in many cases memory bound is uninteresting; one could examine a vector implementation and be satisfied that it won't explode unnecessarily. After all, we do exactly that on non-proved implementations without too much fear all the time. SAT just came to mind as a problem where that could be an interesting thing to be able to prove.

That's analogous to the halting problem.

It would be cool if the unsafe aspects of Rust that are necessary (like Vec) could themselves be formally verified, like when each edition of the language gets compiled or something. I know some languages include proof tools but they're not super popular, and Rust's compiler helps a lot. Still, it would be really cool to know, or at least know that you can't know. LinkedList is another example. There's no way to really write a linked list in the rust friendly way, so you have to use some boxing. All of that is fine, it probably works, but what if I forgot later, and changed something about the implementation, introducing bugs around edge cases or what not.

This process is actually already underway, notably with the RustBelt project: https://plv.mpi-sws.org/rustbelt/. It has not yet achieved the kind of tight integration with the source language that stuff like Creusot has, but everyone would like it to move in that direction :)

For the specific case of Vec (and a few other types--e.g. Cell, Mutex, etc.), as I mentioned, a recent paper by xavxav actually proves that the important parts of the unsafe implementation of Vec do actually fulfill the signatures that are used by the CreuSAT proof. This is part of https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper..., which I believe won the distinguished paper award at this year's PLDI!

This discussion is also interesting wrt the rust verification: https://news.ycombinator.com/item?id=30174827 . Creusot author did comment on it.

Seems like there finally will be alternatives to Ada SPARK.

Oh wow. So efforts like this can actually eventually trickle down to more regular programming?

Well, that's the research question! So far signs are promising, IMO. I think this is at least the best chance formal methods have ever had at being relatively easy to integrate into larger codebases--Rust's type system is strong enough to support nontrivial verification conditions, and effectively encapsulate them, without needing to directly deal with "exotic" logic, heavyweight encodings, pointer obligations that need to be manually discharged, or linking to code generated by some external language (a feature it shares with functional programming languages, as well as "hybrid" linear/dependently typed lanugages, like Dafny or ATS). Unlike functional or dependently typed programming languages, however, Rust has a lot of adoption independently of its suitability for formal methods, meaning that ease of integration has a good chance of benefiting projects that don't have correctness as a principle requirement. For example, assuming that a useful crate can be extracted from this project, it would be quite easy to integrate into a video game like Veloren (e.g. to help improve some of its AI heuristics), which is about as far from traditional high-assurance software as you can get!

If we can make using high-assurance software as easy (or almost as easy) as non-high-assurance software, without sacrificing huge amounts of performance to do so, it will be a major step in making software more reliable for everyday programmers, rather than restricting these kinds of techniques to critical libraries like cryptographic primitives where correctness and performance justify pretty much any number of proof engineering hours. This doesn't mean everything would be verified, but with more and more verified "building blocks," less and less engineering time would be spent debugging third party code (which at least IME, is usually much more painful than verifying code at the top level). We have a long way to go to get there, but projects like this are an excellent start.

Why are verified SAT solvers interesting?

SAT solvers often form (part of) the backbone of other proof assistants and verified software and hardware, which makes them producing correct output quite critical. At the same time, production SAT solvers (the ones people actually use on the critical path of these proof assistants) are very performance-sensitive, which means tons of optimizations that are nonobvious, subtle, and in some cases not obviously memory safe. This makes them ideal candidates for formal verification.

Unfortunately, in the past, the proof effort required to produce a competitive SAT solver was so high that this was considered infeasible, so instead the industry has been focused on non-verified SAT solvers that produce efficiently verifiable certificates for their solution that can be checked by an independent verifier. This was an important improvement that has allowed SAT solvers to continue to evolve, but (as mentioned downthread) they have disadvantages compared to a solver that can be fully trusted without producing a certificate, including in "forcing" people to use techniques that produce proofs which we know how to efficiently verify.

What this project promises is an order of magnitude reduction in proof effort to achieve and maintain an extensible, competitive, verified solver, which may help change the above calculus to favor verified solvers. IMO, it is quite an exciting development, even if it does not pan out!

Maybe I'm missing something blindingly obvious, but why is "trusting" a SAT solver necessary in the first place? The solution itself either satisfies the constraints or it does not. Are there situations where we can't even tell whether the solution is correct by looking at the problem instance?

For positive solutions, you are correct--verifying the solution is incredibly easy. For negative solutions (UNSAT), however, this is not the case--UNSAT is in Co-NP, not NP. Finding an efficiently verifiable representation of the UNSAT proof can be very challenging, which is part of why solvers are given much more time to produce and verify certificates than they are to solve the problem in the first place.

Ahh, I see now what you mean. Thanks, that makes much more sense to me now.

Right, unsat is the interesting case where you especially want a proof of the SAT solver.

Unsat can be used, in turn, to prove other things. If you want to prove that some condition C is always true in a set of expressions, just ask the SAT solver to solve for "not C". If the answer is UNSAT, then C is always true... if the answer UNSAT is actually correct.

Thanks. Do you have a link or reference to more material on the certificates. I dont understand a bit, but I want to learn more.

I will just steal from the paper's author (Sarek) and point you to the first two talks and lecture notes by Randy Bryant at this link: https://fm.csl.sri.com/SSFT22/#splogic.

> on two fingers

In which base? Can I use my knuckles?

Base 1, no knuckles required :)

Reply on news.ycombinator.com