Stream: Coq users

Topic: Alternatives to VST

Huỳnh Trần Khanh (Jul 27 2022 at 02:47):

I want to formalize imperative programs. I considered VST, but I don't like the licenses. Now I'd love to hear about alternatives. I do not need to formalize C programs, I just need to formalize programs written in some imperative language that's decently low level. Anything that fits the bill?

Paolo Giarrusso (Jul 27 2022 at 02:59):

https://iris-project.org/ +... some of their supported languages — HeapLang, RustBelt, (and maybe OCaml, Go), RefinedC?

Yannick Forster (Jul 27 2022 at 07:37):

I think more context would be helpful :) If you are an expert user with a concrete project idea, that's a different situation than being a more novice user who wants to learn the basics of imperative program verification first (where my answer would have been "Software Foundations volume 2")

Huỳnh Trần Khanh (Jul 27 2022 at 09:21):

I know how to make a little imperative language within Coq using inductive predicates. I don't have a project. On each contest, I'll make a new Coq project and write formalized code, then when I'm confident the code is correct, I submit the code to the online judge. If I want to take the DIY route, I could define an imperative language myself and then write a function to convert that language to C++ or some other mainstream language, and submit the generated C++ to the online judge to increase my rating.

Huỳnh Trần Khanh (Jul 27 2022 at 09:21):

I'm doing competitive programming!

Huỳnh Trần Khanh (Jul 27 2022 at 09:24):

The generated code still needs to meet minimum readability standards because it's considered cheating to submit unreadable code.

Yannick Forster (Jul 27 2022 at 09:39):

Have you also verified programs in these little imperative languages using techniques like Hoare logic or separation logic? :) I guess my general stance, not necessarily applicable to you, can be summarised as: Start at the beginning. If you feel like you don't know all or most of the relevant material explained in books like SF, overall your fastest path to verifying complex imperative code will be to first work through relevant parts of SF.

Yannick Forster (Jul 27 2022 at 09:40):

Independent of that, you might be interested at having a look what tools people used to solve the Proof Ground challenges in the last years: https://www21.in.tum.de/~wimmers/proofground/

Paolo Giarrusso (Jul 27 2022 at 09:44):

For imperative programming I'd consider software foundations volume 5...

Paolo Giarrusso (Jul 27 2022 at 09:49):

Re "convert to C++", what you propose risks adding C/C++/Rust undefined behavior (background: https://www.ralfj.de/blog/2018/07/24/pointers-and-bytes.html); I won't speculate how likely actual miscompilation is.
Going from RustBelt to Rust might reduce the chances (but I'm no expert!)

Huỳnh Trần Khanh (Jul 27 2022 at 11:11):

You are indeed correct, I only formalized imperative programs with inductive predicates, I haven't done any Hoare logic/separation logic yet, but I expect this stuff to be simple. I'll read Software Foundations.

Huỳnh Trần Khanh (Jul 27 2022 at 11:15):

I'm still afraid of reading chapter 5. It's VST stuff and I'm afraid I'll get addicted to it! And because I intend to make my code publicly available under CC0 after the contest, this constitutes commercial use.

Huỳnh Trần Khanh (Jul 27 2022 at 11:15):

But the basics should still be the same regardless of toolchain right?

Karl Palmskog (Jul 27 2022 at 11:17):

One key problem with these deeply embedded imperative languages like HeapLang, RustBelt is that even proving pure functions correct has a lot of overhead. From what I remember, frameworks like CFML (http://www.chargueraud.org/softs/cfml/) actually allow reasoning directly about pure functions in the usual way together with imperative parts in separation logic. The state of the art for this is arguably CakeML, but only in the HOL4 proof assistant (although people are seemingly working on porting CakeML semantics to Coq)

Huỳnh Trần Khanh (Jul 27 2022 at 11:25):

I assume by "overhead" you mean the goals are way too long and cantankerous, not the resulting program is too slow, right?

Karl Palmskog (Jul 27 2022 at 11:36):

"proving correct" is nearly always completely separate from execution, regardless of the framework

Karl Palmskog (Jul 27 2022 at 11:37):

one example that Paolo may be able to corroborate: if I want to prove something about a pure function in C++, I will still have in my correctness statement a bunch of stuff about the heap and the stack and memory in general

Karl Palmskog (Jul 27 2022 at 11:38):

I don't think most of these imperative proof environments even have a notion of what pure function is (C++ const doesn't give the full notion)

Karl Palmskog (Jul 27 2022 at 11:40):

one exception is Dafny, since it was consciously designed to have a pure part and an imperative part. But Dafny semantics is pretty opaque.

Huỳnh Trần Khanh (Jul 27 2022 at 11:41):

(deleted)

Paolo Giarrusso (Jul 27 2022 at 11:59):

@Karl Palmskog

a bunch of stuff about the heap and the stack and memory in general

I'm not too familiar with those frameworks, but between the frame rule and abstraction, it should be possible for such a framework to "hide away" quite a bit of that. For instance, the spec for a int square(int n) function might look like \with n \arg "n" (Vint n) \let n2 := n * n \require in_bounds Tint n2 \post[Vint n2] — this is essentially what we write at Bedrock with Brick (and VST specs look similar?). A proof will involve some separation logic, but most of it could be automated in principle, and in practice with enough effort.

Karl Palmskog (Jul 27 2022 at 12:07):

but I think we see the problems with this kind of spec: all your regular numbers are now Tints/Vints, and you need new variants of lia tactics to reason about them. Sure, you can do the proof mode stuff, but it's not like that will work for everything

Paolo Giarrusso (Jul 27 2022 at 12:09):

the numbers are wrapped, but they're still numbers — Vint : Z -> val. And we do use lia, ultimately. I agree there's _LOTS_ of proof automation work to get there :sweat_smile:

Karl Palmskog (Jul 27 2022 at 12:10):

if you do the Isabelle-style reasoning about C programs (AutoCorres or whatever it's called), at least you can reason on regular pure functions in the end (at least that's my current understanding). Basically, the tool takes a C program and generates a bunch of pure functions for you.

Paolo Giarrusso (Jul 27 2022 at 12:14):

Happy to take your word for it, I mostly work in a different fragment... but so if the tool cannot prove the function is externally pure, the translation will just fail?

Paolo Giarrusso (Jul 27 2022 at 12:17):

But I should warn you: for an academic I'm extremely ignorant of <non-Iris separation logics>, as my academic background is elsewhere :-).

Karl Palmskog (Jul 27 2022 at 12:20):

I think what happens in AutoCorres is that it goes through a simple imperative language in isabelle, and then any program in this language can be interpreted as a pure function [monadic stuff, possibly?]

Karl Palmskog (Jul 27 2022 at 12:21):

but even with all the fancy automation, can you rewrite with C++ programs in other C++ programs?

Karl Palmskog (Jul 27 2022 at 12:22):

I think that's the usual argument to keep pure things pure, you're not constrained by the frame rule and other imperative boilerplate

Karl Palmskog (Jul 27 2022 at 12:30):

I guess one Coq alternative to CFML and CakeML would be to use a combination of CertiCoq and VST - write as much as possible in CertiCoq-friendly Gallina, then the rest in Clight, do reasoning about both things [manual Clight and CertiCoq-generated Clight] together in VST

Karl Palmskog (Jul 27 2022 at 12:31):

not sure this is possible technically right now (and it's probably not proven to ISA level), but it should possible in principle

Paolo Giarrusso (Jul 27 2022 at 13:28):

okay, https://trustworthy.systems/projects/TS/autocorres/ and https://trustworthy.systems/publications/nicta_full_text/7629.pdf are helpful. max' in Figure 2 seems something nice to reason about. OTOH, their results in Figure 5 still seem extremely painful — I don't see a proof that this swap function actually swaps disjoint inputs.

Paolo Giarrusso (Jul 27 2022 at 13:32):

Separately, AFAICT the seL4 model of the C standard is not suitable for use in a TCB. That's why seL4 does _not_ trust their C semantics and uses translation validation instead.

Karl Palmskog (Jul 27 2022 at 13:33):

I meant that substituting equals for equals is a fundamental mechanism for productivity in program correctness proofs. If your structures are all wrapped, and you have to reason about a deeply embedded language in a deeply embedded proof system, you're most of the time not going to get the same general algebraic reasoning tools

Paolo Giarrusso (Jul 27 2022 at 13:34):

I see. Yeah, that's the advantage of functional specifications — which one can use in separation logic (and VST advocates). I think I agree that, if your program does _not_ use dynamic memory allocation/pointers/aliasing, AutoCorres seems nice.

Karl Palmskog (Jul 27 2022 at 13:36):

for example, let's say that Xavier had started to write CompCert using HeapLang in Iris, would he have gotten as far as purely-functional-CompCert is now in the same time?

Karl Palmskog (Jul 27 2022 at 13:37):

indeed, translation validation may eat our lunches in the end, it's yet another nearly-orthogonal program verification approach

Paolo Giarrusso (Jul 27 2022 at 13:37):

HeapLang's target is 10-line concurrent programs that take a PhD to verify, so this isn't the most interesting question :-)

Paolo Giarrusso (Jul 27 2022 at 13:39):

in any case, we're talking about very different questions :-)

Paolo Giarrusso (Jul 27 2022 at 13:40):

yes, (nearly) functional programs can be verified using reasoning that is less expressive and is easier to automate.

Paolo Giarrusso (Jul 27 2022 at 13:42):

if you _need_ a program outside that fragment, that doesn't help you. Whether you need that is of course up for discussion :-)

Karl Palmskog (Jul 27 2022 at 13:43):

ah, but then, isn't it often that you can partition your program into a purely functional part and one must-be-imperative part (compare partitioning for concurrency), and link them together

Karl Palmskog (Jul 27 2022 at 13:44):

at least, this is what I argued above, and I believe CFML, CertiCoq+VST, CakeML can support that style.

Paolo Giarrusso (Jul 27 2022 at 13:48):

Hence "different questions": I'll bet there exist programs where that makes sense. My bias comes from "we're verifying an hypervisor" — even if you could extract pure programs even there, that's probably a smaller fraction

Paolo Giarrusso (Jul 27 2022 at 13:48):

in any case, I understand your point better, thanks.

Yannick Forster (Jul 27 2022 at 14:30):

Paolo Giarrusso said:

For imperative programming I'd consider software foundations volume 5...

Well yes, but 2 first, for the operational semantics and the Hoare logic, and 1 before that, for the basics

Alexander Gryzlov (Jul 27 2022 at 23:31):

Karl Palmskog said:

One key problem with these deeply embedded imperative languages like HeapLang, RustBelt is that even proving pure functions correct has a lot of overhead. From what I remember, frameworks like CFML (http://www.chargueraud.org/softs/cfml/) actually allow reasoning directly about pure functions in the usual way together with imperative parts in separation logic. The state of the art for this is arguably CakeML, but only in the HOL4 proof assistant (although people are seemingly working on porting CakeML semantics to Coq)

HTT is also a shallowly embedded separation logic :)

Last updated: Oct 03 2023 at 21:01 UTC