5 ms·

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 compet

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 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.

jerf 4y ago
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.
- Jweb_Guru 4y ago
  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!
- Sarek 4y ago
  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.
  - jerf 4y ago
    "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.
- viccuad 4y ago
  That's analogous to the halting problem.
riedel 4y ago
This discussion is also interesting wrt the rust verification: https://news.ycombinator.com/item?id=30174827 https://news.ycombinator.com/item?id=30174827 . Creusot author did comment on it. Seems like there finally will be alternatives to Ada SPARK.
ithkuil 4y ago
> on two fingers In which base? Can I use my knuckles?
- Jweb_Guru 4y ago
  Base 1, no knuckles required :)
andi999 4y ago
Why are verified SAT solvers interesting?
- Jweb_Guru 4y ago
  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!
  - jhgb 4y ago
    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?
    - Jweb_Guru 4y ago
      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.
avgcorrection 4y ago
Oh wow. So efforts like this can actually eventually trickle down to more regular programming?
- Jweb_Guru 4y ago
  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.
asimpletune 4y ago
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.
- Jweb_Guru 4y ago
  This process is actually already underway, notably with the RustBelt project: https://plv.mpi-sws.org/rustbelt/ 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.pdf https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper..., which I believe won the distinguished paper award at this year's PLDI!

jerf 4y ago

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.

Jweb_Guru 4y ago
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!
Sarek 4y ago
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.
- jerf 4y ago
  "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.
viccuad 4y ago
That's analogous to the halting problem.

riedel 4y ago

This discussion is also interesting wrt the rust verification: https://news.ycombinator.com/item?id=30174827 https://news.ycombinator.com/item?id=30174827 . Creusot author did comment on it. Seems like there finally will be alternatives to Ada SPARK.

ithkuil 4y ago

> on two fingers In which base? Can I use my knuckles?

Jweb_Guru 4y ago
Base 1, no knuckles required :)

andi999 4y ago

Why are verified SAT solvers interesting?

Jweb_Guru 4y ago
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!
- jhgb 4y ago
  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?
  - Jweb_Guru 4y ago
    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.

avgcorrection 4y ago

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

Jweb_Guru 4y ago
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.

asimpletune 4y ago

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.

Jweb_Guru 4y ago
This process is actually already underway, notably with the RustBelt project: https://plv.mpi-sws.org/rustbelt/ 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.pdf https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper..., which I believe won the distinguished paper award at this year's PLDI!