stdpp

Stream: iris-lean

[Bas Spitters]

What is the plan for porting the relevant parts of stdpp?
I understand it will depend on batteries, but not cslib. Does that seem correct?

[Markus de Medeiros]

There is currently no plan to port stdpp, we will evaluate what we need from stdpp on a case-by-case basis. For example, we did not port the gmap CMRA, we developed a CMRA for generic maps instead.

Iris-Lean does depend on batters but not cslib, yes. I can imagine writing a program logic for cslib languages at some point, but as of now I don't think that justifies another dependency.

[Bas Spitters]

So, you would expect cslib to make some duplication of the lean-iris-stdpp.

[Markus de Medeiros]

I'd like to avoid it if possible. As it stands it looks like there isn't much duplication in "core Iris". If down the road there is more substantial duplications, then we could either try to move it upstream to batteries (our common dependency) or downstream to an iris-lean-cslib.

[Markus de Medeiros]

The latter is the plan for Iris+mathlib stuff.

[Shreyas Srinivas]

Note that batteries is intended to morally serve the same role as stdpp

[Shreyas Srinivas]

So the right place to port something from stdpp is directly to batteries, after checking that the corresponding material doesn't already exist in some Data folder of mathlib. EDIT : or in the Lean/Std namespace of the main lean4 repository.

[Shreyas Srinivas]

Cslib is not playing quite the same role as stdpp. It's largely formalising CS curriculum stuff. It sits downstream of mathlib.

[Zongyuan Liu]

Is there a conclusion on what the correspondence of stdpp gmap is in Lean? I plan to port big_ops for maps, and am still not quite sure what I should use. Should I use the generic map API or a concrete map implementation?

[Markus de Medeiros]

Unless you really need something specific about gmaps, you should try to generalize the constructions to use the generic API.

[Michael Sammler]

I've been wondering about this question as well. My understanding is that ExtTreeMap is the closest analogue to gmap.
Is this the generic map API that you are referring to? At the moment this interface looks very minimal. Is it intended to be the equivalent of the FinMap interface of std++? (Note that there is discussion to get rid of FinMap in std++ since basically everyone uses gmap directly.)

[Markus de Medeiros]

I think it is good to use an interface (like the heap API you linked) rather than a specific type (like ExtTreeMap) wherever possible. In my work I have run into situations where the restrictions on gmap have been too restrictive (a countable type of keys, and having only finitely many elements allocated at once) and as a consequence I've had to redevelop all the theory on top of gmaps to use a different data structure.

The API is indeed relatively close to FinMap.

[Zongyuan Liu]

I actually prefer removing this layer of abstraction and just using the closest thing to gmap. A concrete map with a rich API simplifies and speeds up porting. IMHO, catching up with Iris-Rocq is more important at this project stage.

[Markus de Medeiros]

Do you have an example of somewhere that gmap is easier than using generic API? My experience with the heap_view CMRA is exactly the opposite

[Markus de Medeiros]

In Iris-Rocq they do some strange proofs by induction over the number of allocated keys in a gmap. I suspect that this is to avoid classical logic, so we could technically avoid this with gmaps as well, but I also haven't encountered a case where using a concrete type instead would give any benefit

[Michael Sammler]

I think the main benefit of using an existing definition is that one does not need to duplicate / reprove the API. For example, a quick look at the lemmas of ExtTreeMap suggests that there are around ~700 theorems that one would want to / need to duplicate. (The Std lib seems to indeed duplicate all these lemmas for the 4+ different maps using a process I do not understand.)

[Markus de Medeiros]

I could get behind that! I did not know much about Std.ExtTreeMap but the restrictions on the type seem pretty liberal which is good.

[Markus de Medeiros]

Do these tree maps have an analogue of "allocation" for maps with infinitely many unallocated values? I don't see any such thing.

[Markus de Medeiros]

Ah, I see there are a number of lemmas for finding keys of a certain size Std.ExtTreeMap.maxKey and this Std.ExtTreeMap.filterMap which I think is enough to simulate it.

I'd guess that the Ordering field is always able to be trivially instantiated, so I think the only way this is less general than the one we've implemented is about the universe levels of Ext(D)TreeMap with respect to the keys and values. But somehow I doubt this is a problem. I can give porting the old stuff to the Std maps a try sometime.

[Michael Sammler]

Indeed, I think giving Ext(D)TreeMap a try sounds like the best option to find out how well it works. If someone has experience with the different map types and their advantages and disadvantages, please chime in! I would be interested.

[Markus de Medeiros]

Ah--If I'm understanding the code correctly, Ext(D)TreeMaps can only represent maps that have a finite number of allocated elements. For example, I don't believe that there is a way to represent a heap with keys in the natural numbers that has every odd element allocated. Even if this sounds silly, this kind of thing is done in probability (splitting sources of randomness, for example) and I think it's important that we keep the library of Iris CMRA's as generalized as we reasonably can.

[Markus de Medeiros]

That said, the abstract heap interface only needs to be rich enough for internal clients, for example HeapView (already completed). I've added an issue iris-lean#105 to instantiate this interface with the Lean map types, so that external clients are free to use maps that have a more well-developed API if they want to do so. I also think we could use the Lean map types for IProp without any real loss of generality, and I agree with Zongyuan in this case that using a type closer to gmap could make the port go faster, so we should do it!

[Zongyuan Liu]

For example, I don't believe that there is a way to represent a heap with keys in the natural numbers that has every odd element allocated.

Does this imply a need for a generic interface based big_sepM for your heap points-tos? However, big_op for maps requires a rich API for the lemmas on its various operations.

[Markus de Medeiros]

Is there anything stopping us from having a generic interface? Big ops are just folds over finite data structures, whether you're folding to construct terms in the heap API or a concrete implementation seems immaterial.

I browsed big_ops.v and nothing jumped out to me as being missing, but I think you are more familiar than I am. Do you have examples of where using a specific map type would help?

[Michael Sammler]

Markus de Medeiros said:

Ah--If I'm understanding the code correctly, Ext(D)TreeMaps can only represent maps that have a finite number of allocated elements. For example, I don't believe that there is a way to represent a heap with keys in the natural numbers that has every odd element allocated. Even if this sounds silly, this kind of thing is done in probability (splitting sources of randomness, for example) and I think it's important that we keep the library of Iris CMRA's as generalized as we reasonably can.

How would you do this in Rocq? There also gmap also only represents finite maps. E.g. the ghost_map constructions are specific to gmap and cannot represent infinite maps. For me this has never been a problem, but I also never did any probablistic verification.

[Markus de Medeiros]

Yeah that's my problem exactly--I couldn't, without rewriting parts of the core Iris libraries.

[Markus de Medeiros]

Even though, mathematically, something like ghost map does (did) easily generalize beyond gmap.

[Michael Sammler]

I see, then it probably makes sense to define ghost_map over the generic interface as you already did. But I guess one would only use this interface if one actually needs this generality. For a concrete heap of like heaplang, one can still use ExtTreeMap and then just use the fact that it implements the generic interface. This means that the generic interface does not provide the full API of ExtTreeMap, but only what is necessary for ghost_map (which is hopefully a lot less).