Stream: hs-to-coq devs & users

Topic: A talk on hs-to-coq

Yao Li (Sep 02 2020 at 18:34):

I have recently given a talk on how we verify parts of GHC using hs-to-coq. The video of my talk is available at https://youtu.be/1NA6yV3cxNY :smile:

Bas Spitters (Sep 02 2020 at 19:58):

Nice! do you have the slides available too?

Yao Li (Sep 02 2020 at 20:06):

Sure! Slides available here: https://drive.google.com/file/d/1Cj7ax-b-BsWZeZ-fRFTu3BMdLUsWNfos/view?usp=sharing

Bas Spitters (Sep 02 2020 at 20:10):

Very nice. Did you get any response from the haskell community?

Bas Spitters (Sep 02 2020 at 20:13):

BTW what is the current thinking about Equations. E.g.
https://github.com/antalsz/hs-to-coq/issues/138

Karl Palmskog (Sep 02 2020 at 20:34):

@Yao Li maybe this is a long shot, but any thoughts/hope for formalizing the core GHC language and connecting it to hs-to-coq? This (GHC core, https://github.com/ghc/ghc/tree/master/docs/core-spec) seems to be the closest Haskell has to any formal specification - it's in the Ott language, which can be used to generate a Coq definition with proper annotations

Yao Li (Sep 02 2020 at 20:54):

@Bas Spitters Yes. Some nice responses from the Haskell community. Most responses I've got are about how we translate Haskell to Coq (e.g. how do we handle laziness?). Simon PJ is also interested in if formalization can help write better code, which I'm also interested in but I haven't had a good answer to it.

If anyone has some interesting Haskell programs that they want to verify, or if any other ways of using hs-to-coq, I would love to hear about it!

Yao Li (Sep 02 2020 at 20:55):

As for Equations, I haven't heard much about the updates, either.

Yao Li (Sep 02 2020 at 21:04):

@Karl Palmskog Good question! And it is indeed something that we are trying to verify. For example, here is the Coq translation of the CoreSyn module (together with a few other modules that CoreSyn has mutual dependencies with) in GHC 8.4.3: https://github.com/antalsz/hs-to-coq/blob/master/examples/ghc/lib/Core.v You can find the Expr data type on L651. And what we have proved is some properties about well-scopedness of term substitution, etc.
However, I don't think we can give a complete specification of Core and verify it because that is a lot of work.

Karl Palmskog (Sep 02 2020 at 21:06):

ah, nice, thanks for the pointer

Paolo Giarrusso (Sep 02 2020 at 22:10):

Is this the same formalization as the Deep Spec one? https://deepspec.org/entry/Project/Haskell.20CoreSpec

Paolo Giarrusso (Sep 02 2020 at 22:12):

Ah, guess yes — Antal Spector-Zabusky is involved in both :-)

Yao Li (Sep 02 2020 at 22:28):

Yes it's the same one :)

Bas Spitters (Sep 03 2020 at 07:10):

Any thoughts on the interaction with liquidhaskell (we discussed it before in the issues), but LH seems to be gaining some traction now.

Karl Palmskog (Sep 03 2020 at 09:58):

@Bas Spitters do you know how Liquid Haskell is connected to Haskell semantics, if at all? There are many claims to this effect in the Liquid Haskell papers, along the lines of "Liquid Haskell proves termination of a [Haskell function]", but from what I can tell what language you are verifying and whether this is something resembling Haskell is something that has to be taken by faith.

What worries me in particular is that there seems to be many Haskell functions which are known to not be verifiable by Liquid Types, even on pen and paper (see ICFP '14 paper).

Bas Spitters (Sep 03 2020 at 11:20):

They have a totality checker in LH, at that point the semantics is the same as for hs2coq.
Famously, haskell does not have a formal semantics, but one can more or less trust the total part.

Karl Palmskog (Sep 03 2020 at 14:37):

I would disagree that just Haskell + totality gives you something reasonable, in the presence of the IO monad and the like. What I think LH should have done is to define an explicit Haskell fragment where they are sound. "Projecting" Coq functions to/from a messy language is at least a process that is amenable to inspection/analysis, and you can always fall back on Coq to fully define everything.

Bas Spitters (Sep 03 2020 at 14:51):

"total haskell is reasonable coq" is the premise of hs2coq.
https://arxiv.org/abs/1711.09286
I don't know how LH interacts with IO, I guess there is more in either the book, or in Niki's thesis.
https://ucsd-progsys.github.io/liquidhaskell-tutorial/
Did you check?

Karl Palmskog (Sep 03 2020 at 15:34):

this looks like the closest on soundness there is: http://goto.ucsd.edu/~nvazou/thesis/main.pdf#page=143 (but not clear to me what the connection to Haskell/GHC is)

Karl Palmskog (Sep 03 2020 at 15:49):

but more practically, perhaps @Yao Li could comment on whether Liquid Haskell devs have shown any interest in the Haskell Core Spec work? To me, a connection to something like this would be the obvious way to achieve trustworthiness for LH.

Yao Li (Sep 03 2020 at 16:27):

I haven't been in any discussion on that topic with the LH team. I think there might be some challenges of making connections between LH and CoreSpec: (1) a complete verification of Core is a lot of work, and (2) GHC is constantly evolving (even the parts relevant to Core). I would be concerned that a small team of hs-to-coq devs might not be able to verify enough Core to actually help make LH more trustworthy.

Yao Li (Sep 03 2020 at 16:29):

@Bas Spitters And what sort of connection do you have in mind? (Sorry I do not recall the earlier discussion. Maybe I didn't join the discussion.)

Bas Spitters (Sep 03 2020 at 18:16):

@Yao Li I just checked, it was an email discussion with some hs2coq developers.
In any case, then we saw two main hurdles:

• hs-to-coq uses GHC to parse and resolve names; but Liquid Haskell is not built into this machinery, and parses the LH annotations separately. So a non-trivial amount of plumbing would be needed to get our hands on the information we need.
• LH puts all the refinement type obligations of a Haskell function into a single SMT task. This may allow for more interaction between the equations than Program mode, where each occurrence of a refinement type would have to be solved individually.

Karl Palmskog (Sep 03 2020 at 21:07):

thanks for the summary, this in my mind means that anyone who is "foundationally conscious" would focus on primarily using hs-to-coq for practical Haskell verification at the moment

Karl Palmskog (Sep 03 2020 at 21:10):

I think it was nice what the VeriFast developers did, they basically carved out minimalistic fragment of their system and verified it end-to-end: https://people.cs.kuleuven.be/~bart.jacobs/fvf/ --- something like this should be within reach with CoreSpec + LH.

Bas Spitters (Sep 04 2020 at 05:51):

Yes, I was thinking along the same lines, but then I was told about the two hurdles above.

Paolo Giarrusso (Sep 04 2020 at 07:42):

On the first hurdle, things might be easier now because LH is more integrated into GHC (but I haven’t watched the talk): https://icfp20.sigplan.org/details/hiw-2020-papers/1/Liquid-Haskell-as-a-GHC-Plugin

Last updated: Feb 06 2023 at 05:03 UTC