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.

[Edwin Fernando]

I'm confused on how contexts and environments work in Iris-lean and I thought I'd ask here.
I'm used to semantics of assertions being given in the form s, h ⊨ P. My confusion is in figuring out how to model s, which is not present in the classical instantiation for example.
1) I've noticed a difference between the MoSeL paper + rocq implementation vs the lean implementation in how quantification works.
bi_forall : ∀ A, (A → PROP) → PROP (in rocq)
sForall : (PROP → Prop) → PROP (in lean)

2) I believe the rocq implementation atleast, supports environments as a maps from strings to a fixed type A. (I understand this as working in an untyped calculus). But I would really like to work with environments which allow mapping an index to some type in a type family (β : α → Type u) where α is the syntax of a type in the language and Type u is the donation of the type, in Lean. I understand this as working with strongly typed environments. I'm making guesses here but was the change in 1) perhaps meant to enable 2)

3) Could you explain which parts of the lean code I should look at to see, how environments now work. Environments.lean is not there. I'm guessing the comments/proofmode.md are a little out of date. There is mention of an EnvsEntail function here, which I couldn't find, which I thought might be important for me.

I also wanted to note that lilac assertions have two intuitionistic contexts, one for deterministic and the other for random variables (so I'm trying to figure out how to represent that with this question).

[Markus de Medeiros]

Happy to try and help!
1) See #iris-lean > Why are sForall and sExists defined the way they are?
2) This I'm not too sure of. Iris-Rocq does have the ability to combine multiple different BI instances: we haven't tested this in Iris-Lean and I'm not 100% sure what you describe is well-supported in Iris-Rocq either. Could you maybe describe this in more detail? It's common in Iris to define the denotation of a type using a logical relation, you can do this as long as all of your denotations live in the same BI instance.
3) The representation the proofmode uses is [*] [spatial context] * pers [^] [Intuitionistic context]. Names are attached to each term in this expression at the meta-level, and the tactics parse this form into the Hyps data structure from Expr.lean. That's probably where you want to look, though you might also want to just look through some of the tactic implementations to see which metaprograms are used to manipulate Hyps.

And re. your last note: I don't think there are any plans to support multiple intuitionistic contexts, though I'd guess you can simulate this inside one context, no?

[Michael Sammler]

The representation the proofmode uses is [*] [spatial context] * pers [^] [Intuitionistic context].

I would like to clarify that Iris Lean does not use this representation (this is used by Iris Rocq). Instead, Iris Lean uses the Hyps data structure that represents the context as a tree where each node can be persistent or not. I am also currently working on refactoring the proof mode so this might change in the future.

[Markus de Medeiros]

Oh whoops, yeah this is right. It has this representation logically (as in that's what hyps represents in terms of BI), and it has the capability to go back and forth between hyps and this representation (with the istop and istart tactics), but it's not this representation literally. Thanks for chiming in Michael!

[Edwin Fernando]

Sorry for the confusing previous question. Thanks, for the answers! I was using the wrong terminology I think, and didn't really want to refer to the spatial or intuitionistic contexts. I wanted to refer to the s in the s, h ⊨ P used to give semantics to assertions in a classical separation logic, through the satisfiability relation.
I think there is no need for an s (program variable environment) in classical instance provided as an example by Iris-lean. I would expect it to be seen only when HeapLang is introduced and when reasoning about HeapLang programs. I think I should perhaps port HeapLang, to understand things better? Particularly the definition of the PROP parameter of BI and BIBase. Would it be of the form PROP := Store → Heap → Prop? Would this shape for PROP be standard?

And following on from the previous suggested shape from PROP, question 2), was about the type Store (which is a typing context Γ, hence my use of the word context). I don't at the moment have a question about this anymore since I wanted to think about it more first, particularly about logical relations. For more context, in the Lilac paper it is given like so:

Γ ::= · | Γ, 𝑥 : 𝑆     (𝑆 for Set)
⟦𝑥1 : 𝑆1, . . . , 𝑥𝑛 : 𝑆𝑛 ⟧ = 𝑆1 × · · · × 𝑆𝑛

example usage in an inference rule for defining probability specific SL connective Own E

𝐸 ∈ ⟦Γ⟧ → ⟦Δ⟧ -m→ 𝐴    (-m→ is measurable function, Δ is the typing context for random variables)
---------------------------
Γ; Δ ⊢ own 𝐸

[Michael Sammler]

Edwin Fernando said:

Would it be of the form PROP := Store → Heap → Prop? Would this shape for PROP be standard?

Yes, I think this would be the way to get a standard separation logic. See here for an example that does this in Iris Rocq.
I do not understand Liliac / what you are trying to do enough to say something there. Maybe you can give it a try and see what issues you run into?