Hoare Triples in Iris-Lean

Stream: iris-lean

[Edwin Fernando]

Hi I was looking for an example of implementation of reasoning with Hoare triples, but realised that HeapLang is still not implemented. My goal is to implement a probabilistic separation logic for my masters project and I was hoping to use Iris Lean for this. I don't want to use the whole of Iris but just MoSeL.

I'm wondering if there are some common abstractions for supporting reasoning with wp/Hoare triples, that belong in Iris-lean rather than my instantiation of it. Any thoughts about that?

I'm also wondering whether there might be any obvious blockers to this kind of instantiation. I'm happy to contribute to the Iris-lean project directly as well!

[Shreyas Srinivas]

Currently not really. We are still getting iprop done

[Shreyas Srinivas]

I am implementing heaplang piece by piece but this is currently stalled. I can finish my first PR if it would help you

[Shreyas Srinivas]

It has been on the back burner

[Shreyas Srinivas]

But if you just want to use MoSeL and build your own abstraction that’s already viable in a repo downstream of iris-lean and mathlib. I believe @Markus de Medeiros has some ideas on how to do probabilistic verification

[Edwin Fernando]

Shreyas Srinivas said:

Currently not really. We are still getting iprop done

Could you elaborate what iprop is? Is it an Iris proposition? That's not relevant for MoSeL right?

[Markus de Medeiros]

Hi! Always cool to see people interested in Iris-Lean, I'm happy to help clear some things up.

• There is no common wp predicate defined yet. The Iris-Rocq project defines one, however, forks of the Iris project often re-define it for domain specific applications. For example, and since you mentioned probability here is how it is defined in the Eris (Rocq) logic.
• iProp is the type that Iris uses to instantiate the proof interface with (ie. the proof interface manipulates iProp expressions). You can instanstiate MoSeL this with a different type if you'd like. An example of doing this is the classical instance.
• The project Shreyas is referring to is KLR. KLR instanstiates MoSeL with UPred, which you can think of as a more basic form of iProp. The definition for a weakest precondition in KLR is here.
• Both KLR, Eris, and many other Iris-based logics define weakest preconditions internally, as in they first define a logic, and then they express what a weakest precondition means inside that logic. For this reason, the KLR and Eris weakest preconditions are very similar in their definition. If you wanted to work inside the Iris framework, your definition could be similar as well.

There is nothing stopping you from instantiating MoSeL with a different type, perhaps one which represents a weakest precondition externally. In that case, you're right that iProp will have nothing to do with your logic, and you can use MoSeL on its own!

[Edwin Fernando]

Thanks for the info and links! I believe according to this description that I would be defining wp internally to the logic. I aim to formalise Lilac by the way. And I plan to instantiate MoSeL with a different type (not iprop), since Iris has many things which I believe aren't required for the language and logic I want to formalise.

[Markus de Medeiros]

Oh excellent!!! You may be interested to see that the zkEVM people have started porting Bluebell (though I don't know how much is going on there). I've actually chatted with John Li about formalizing Lilac in Iris-Lean, not to put words in his mouth but I get the impression that it's well within the realm of possibility.

Probabilistic separation logic was the main reason I got into Iris-Lean so I'll be interested in hearing what comes of this! I'm hoping to port some parts of Eris when I have the time, maybe we can even share some work later on!

[Yoichi Hirai]

I'm roughly at the middle (of material before appendix) of BlueBell paper. It's getting more interesting as I follow the pages.