Looking for feedback on gmap generalization

Stream: iris-lean

[Markus de Medeiros]

I've been working on my heaps PR for a few days now and I'm hoping to get some feedback on it.

Algebra/heap.lean contains a general interface for data structures which behave like partial functions, and defines a CMRA over them analogous to the gmap CMRA from Rocq Iris. Doing it this way removes several restrictions imposed by the gmap type, namely:

• The restriction that the type of keys be countable
• The restriction that each heap can only have a finite number of allocated elements
  I've actually ran into both of these issues in my research. I wrote two models of this type, Algebra/Lib/ClassicalHeaps.lean and Algebra/Lib/FiniteHeaps.lean, the latter being closer to gmap.

I had to do a couple new tricks to get the general construction to work, and I'm wary of over-indexing on the few models I'm thinking about. Most of the heaps.lean file right now is a trainwreck but if anyone wants to look at the typeclasses at the top of that file and think of types that behave like a partial function but do not fit into this framework, it would be very helpful :)

[Markus de Medeiros]

Oh and just to point out another reason this may be of interest: the definition of iProp in Rocq uses the gmap CMRA to manage its dynamically allocated ghost state (the iProp CMRA is a gmap from gname to CMRA's). This heaps CMRA generalizes the Iris model as a whole.

[Shreyas Srinivas]

one small quibble as I skim the file. You have lines like this:

cases (Classical.em (k = k'))
    · rename_i H; rw [Store.get_set_eq H, Store.get_set_eq H]; exact Ht
    · rename_i H; rw [Store.get_set_ne H, Store.get_set_ne H]; exact Hv k'

I have two suggestions:

1. You can name the cases hypothesis like cases h : <something>. This is is better than using rename_i. I really wish we had the batteries import so you would get the matches style syntax with a code action.
2. I think in this instance you can simply use the by_cases tactic.

[Shreyas Srinivas]

(deleted)

[Markus de Medeiros]

Yeah no definitely. And there's no need to use classical there either. I will fix the proofs later.

[Markus de Medeiros]

At the moment I'm more interested in making sure the interface is right.

[Shreyas Srinivas]

There is an implementation of partial functions in mathlib to get some inspiration for API : https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/PFun.html#PFun never mind. I think it won't be useful here.

[Mario Carneiro]

I think RepFunStore isn't a good idea, that's baking in a validity predicate which will lead to some noncomputable code (which is fine but probably not necessary and will make some mess)

[Mario Carneiro]

Can you summarize the problem to be solved here?

[Mario Carneiro]

What's the API you can't change which grounds the typeclasses?

[Markus de Medeiros]

Yeah. RepFunStore (and IsoFunStore) is not actually necessary for the CMRA (and I don't think either of my models end up using it) but it's a necessary condition for getting a Leibniz OFE when the value types are Leibniz.

[Mario Carneiro]

instance Heap_COFE [Heap T K] [COFE V] : COFE (T V) where

I don't think this will actually work as a typeclass instance

[Markus de Medeiros]

What's the API you can't change which grounds the typeclasses?

gmap? The API here does not exist in Iris-Rocq.

[Markus de Medeiros]

Mario Carneiro said:

instance Heap_COFE [Heap T K] [COFE V] : COFE (T V) where

I don't think this will actually work as a typeclass instance

Really? I was able to write a CMRA so I assumed it was working

[Mario Carneiro]

I think it might only work when T is a constant or local variable

[Mario Carneiro]

I'm trying to figure out what requires a meta-typeclass like Heap in the first place. Why can't we just have a CMRA on a partial functions type?

[Mario Carneiro]

I suspect that the general thing you want is a type that can be mapped to the type of partial functions

[Markus de Medeiros]

gmap is not the same as a partial function, it's a partial function which internalizes the fact that its domain is finite.

On the other hand, I also have more complex data structures coming from my operational semantics in NML which aren't partial functions but do behave like it. It would be nice to directly get the heap-like CMRA on this structure without having to make a complicated model of it using many different pieces of ghost state.

[Mario Carneiro]

gmap is really just TreeMap IIUC

[Mario Carneiro]

but is the finiteness something the CMRA can detect?

[Mario Carneiro]

Mario Carneiro said:

I suspect that the general thing you want is a type that can be mapped to the type of partial functions

This is how I would expect to handle things like TreeMap and HashMap

[Markus de Medeiros]

Mario Carneiro said:

but is the finiteness something the CMRA can detect?

As in making partial functions with infinite allocated elements invalid? I do not want this, because I have applications where I do want to allocate an infinite number of cells.

[Mario Carneiro]

no I mean the opposite, just let things be infinite and does this cause a problem

[Markus de Medeiros]

It means that you can't define (a total) alloc function on your type

[Markus de Medeiros]

This is baked pretty deeply into a lot of Iris code

[Mario Carneiro]

Is it supposed to always be possible to alloc, or are unallocable heaps also relevant?

[Markus de Medeiros]

I do think I can define a general instance of the non-alloc classes for types which having a mapping into partial functions though!

[Mario Carneiro]

You could make that part of the validity predicate

[Mario Carneiro]

i.e. in a valid partial function there are always an infinite number of free slots

[Markus de Medeiros]

Unallocable heaps are relevant too (eg. finite key types). We want the CMRA to work for both models.

[Markus de Medeiros]

The CMRA itself doesn't actually depend on any of this though. I had to do some tricks to get around this.

[Mario Carneiro]

Does Heap need to be a predicate on a type function?

[Markus de Medeiros]

I initially tried class Heap (T K V : Type _) extends Store T K (Option V) but got stuck.

[Markus de Medeiros]

Though, that was on an early version. I could try that again if you think it's a better idea.

[Markus de Medeiros]

I don't recall exactly what went wrong.

[Mario Carneiro]

I see hmap being used, not sure what it is doing

[Markus de Medeiros]

Right. To get the CMRA constructions to work you need a definition of map which ensures that unallocated elements stay unallocated. That's the core of what makes all of the CMRA proofs work.

[Mario Carneiro]

but CMRA doesn't have map?

[Markus de Medeiros]

Yup. Its mainly for proofs involving inc/incN.

[Markus de Medeiros]

And the COFE.

[Markus de Medeiros]

In both of these cases you need to construct a heap, and the trick is that you can construct them by mapping out of one of the heaps you are given. The property you need to prove all of the CMRA properties is that unallocated elements stay unallocated.

[Markus de Medeiros]

They way they do this construction in Rocq-lean is specific to gmap, doing induction over the number of allocated elements. It's weird and definitely does not generalize to the infinitely allocated cases.

[Mario Carneiro]

can you point to the theorem name?

[Markus de Medeiros]

conv_compl in the COFE instance is one example,lookup_included/lookup_includedN are two more

[Markus de Medeiros]

here is the mapping trick used in the definition of compl.

[Mario Carneiro]

Markus de Medeiros said:

Unallocable heaps are relevant too (eg. finite key types). We want the CMRA to work for both models.

Are these always total functions?

[Markus de Medeiros]

It is for gmap (and in my finite heaps instance you can see that my hasRoom predicate is True). But in general no. My definition of fresh takes a hasRoom argument

[Markus de Medeiros]

I guess we could change it to return Option instead, and have another term that says fresh on heaps with hasRoom is some

[Markus de Medeiros]

Markus de Medeiros said:

I initially tried class Heap (T K V : Type _) extends Store T K (Option V) but got stuck.

@Mario Carneiro Just to check, would this formulation be better? Happy to try again if so!

[Mario Carneiro]

The main thing you will miss with that version of the class is hmap

[Mario Carneiro]

You could have a class for that though (this also has the advantage of giving you the universe generic map function)

[Mario Carneiro]

btw you could also write the hmap axiom as get (hmap f t) k = (get t k).bind (f k)

[Mario Carneiro]

also the match statement in get_merge should be extracted as a function, and it already exists as the aptly named Option.merge

[Markus de Medeiros]

Mario Carneiro said:

You could have a class for that though (this also has the advantage of giving you the universe generic map function)

Yeah okay. I think that I only need self-maps, so I may be able to get away with (something like) a [StoreMap T T K (Option V) (Option V)] instance, plus a predicate that that map obeys the hmap rule. I'll give it try. (Ignore this, it does not work & I am trying something else)

[Markus de Medeiros]

Updated everything with your suggestions so far and it seems much more right:

class Heap (T : Type _) (K V : outParam (Type _)) extends Store T K (Option V) where
  empty : T
  hmap (f : K → V → Option V) : T → T
  merge (op : V → V → V) : T → T → T
  get_empty : get empty k = none
  get_hmap : get (hmap f t) k = (get t k).bind (f k)
  get_merge : get (merge op t1 t2) k = Option.merge op (get t1 k) (get t2 k)