Next milestone: Iris 0.5 ("Monoids are all you need!")

Stream: iris-lean

[Markus de Medeiros]

The last week has seen a ton of work so far! Thank you to everyone who is contributing. I figured it would be wise to post an update with the status of the project, and write down how all of the pending PR's relate to each other.

Where we are going

We are within striking distance of being able to develop program logics with fixed, first-order ghost state for sequential languages in iris-lean. I'm personally calling this version of the logic Iris 0.5 (because it can sort-of support half of the famous Iris tagline) even though the features we have ported don't exactly linearize into the Iris genealogy. For example, Iris 0.5 won't be able to express invariants yet, but it will have enough to define a weakest precondition inside the logic itself which is one of the super powerful concepts introduced in Iris 3.

Where we are now

To get to Iris 0.5, we need the following features, which are in varying states of done-ness:

• The agree CMRA (iris-lean#41, @Leo Stefanesco, done).
• Löb induction (iris-lean#50, @Markus de Medeiros, done).
• BI derived connectives (iris-lean#44, depends on iris-lean#50, @Markus de Medeiros, done).
• COFE fixpoints (iris-lean#45, @Markus de Medeiros, done).
• UPred soundness (iris-lean#46, @Markus de Medeiros, done).
• OwnM lemmas (also iris-lean #46, @Markus de Medeiros, done).
• Local updates (iris-lean#49, @suhr, done).
• Updates (iris-lean#61, depends on iris-lean#49, @suhr, done).
• Frac CMRA (iris-lean#56. @Shreyas Srinivas and @Markus de Medeiros. Depends on iris-lean#61. done.)
• Discardable fractions (iris-lean#59, depends on iris-lean#56, @Markus de Medeiros , done).
• Views (iris-lean#60, depends on iris-lean#59. @Markus de Medeiros, in progress).
• Heap CMRA, generalizes gmap (iris-lean#63, depends on iris-lean#60, @Markus de Medeiros, in progress).
• Heap ghost state (iris-lean#64, depends on iris-lean#63, @Markus de Medeiros, in progress).

The following PR, though not technically necessary, should also be merged

• Exclusive CMRA (iris-lean#48, @Oliver Soeser, done).

What we need to do next

Mario does not have time to refactor and review all of these PR's, so even for the PR's that are done, we need to make sure they are high quality. This means minimizing the proofs and using consistent names (I'm super bad about this). You can look at Mario's commit history to see the kind of changes he usually makes.

If you want to help clean up any of the proofs, please make a PR into the appropriate branch. I'll deal with rebasing all of the downstream PR's and making sure everything works together.

Thanks again for everyone who is helping with the project! To end here is a cool picture that is downstream of almost everyone who has contributed: the definition for the points-to connective using Iris ghost state:
heprop.png

[Notification Bot]

Markus de Medeiros has marked this topic as resolved.

[Shreyas Srinivas]

I seem to have a few proofs stuck on typeclass inference. I’ll ping you when iris-lean#62 is done. I plan to repurpose my earlier PR for numbers

[Shreyas Srinivas]

Also if you are posting task lists to track stuff, you might want to use tagged issues or even a project dashboard.

[Markus de Medeiros]

Yeah, maybe one day!

[suhr]

How much of Iris is necessary to start porting the first two chapters of https://github.com/logsem/iris-tutorial?

[Markus de Medeiros]

The first two chapters are very simple and just use the proofmode, nothing about the instance. So could almost be done now.

[Markus de Medeiros]

They cannot be ported 1-1 because we don't have the iApply tactic yet. In iris-lean#43 I started playing around with that but there are some differences between Rocq and Lean typeclass search that need more careful thought.

[Oliver Soeser]

I've been looking into porting iApply and some of the other missing tactics, I'll keep you all updated

[Markus de Medeiros]

That would be super useful!

[Oliver Soeser]

For the existing (done) PRs, am I good to have a go at reviewing/refactoring some so we can get closer to having them merged?

[suhr]

I would really appreciate fixing naming in my PRs.

[Notification Bot]

Shreyas Srinivas has marked this topic as unresolved.

[Shreyas Srinivas]

I'll work on my typeclass instance issues and finish mine. Maybe I can also recast DFrac along the way

[Markus de Medeiros]

@Oliver Soeser Definitely, and it would be super helpful! If you make a PR into the appropriate branch, I will merge and rebase all the dependent PR's.

[Markus de Medeiros]

@Shreyas Srinivas Happy to help with the typeclasses if you want it, it would be nice to wrap this up sometime soon since some of my proofs depend on the details of the Fractional typeclass.

[Shreyas Srinivas]

I'll get back to you in 1.5 hours EDIT : 3 hours, thanks to some office food stuff.

[Markus de Medeiros]

No stress haha

[Shreyas Srinivas]

I am back to take down some sorry proofs

[Shreyas Srinivas]

last one to knock out

[Shreyas Srinivas]

@Markus de Medeiros : Frac.lean can be reviewed

[Shreyas Srinivas]

Given the current PR structure, it might be easier to merge my PR into your PR, merge your PR into master, and then merge master into the DFrac PR

[Shreyas Srinivas]

Keeps the commit history clean

[Oliver Soeser]

suhr said:

I would really appreciate fixing naming in my PRs.

Made a PR for local-update

[Oliver Soeser]

Likewise for updates

[Markus de Medeiros]

FYI: I tweaked the dependencies between PR's so that Suhr's update PR's are on the bottom (I skipped porting updates in some later PR's just due to dependency order).

[Markus de Medeiros]

I also sorry'd out a bunch of lemmas this weekend in the heaps/views PR's, I'll get to them eventually but they're not a very high priority for me atm.

[Shreyas Srinivas]

Has dfrac already been updated to the version of frac I wrote?

[Markus de Medeiros]

Finally, I made a branch in my personal repo that merges all of the changes from all of the above. If you want to play around with a prototype, before waiting for Mario to merge stuff, I'll periodically cut these type of branches.

[Shreyas Srinivas]

If yes then I will move on to numbers

[Markus de Medeiros]

Shreyas Srinivas said:

Has dfrac already been updated to the version of frac I wrote?

Yep! I think there are a couple new sorrys's and there's some refinement to do but the changes have been propagated everywhere.

[suhr]

Some commits like More lemmas could be squashed I think.

[Markus de Medeiros]

Yeah, don't worry about that. Each PR will get squashed before merging into main.

[Mario Carneiro]

PS, I'm hoping to do a big merge pass some time this week. Please make sure all the ready for merge PRs are clearly marked

[Markus de Medeiros]

Will do!

[suhr]

I edited history of my PRs quite a bit. Prod and unit cmras are now in a separate PR.

[suhr]

PS: dealing with conflicts in git can be rather painful. Check out jj, it's compatible with git but makes dealing with conflicts and lots of branches much easier.

Here's some tutorial: https://steveklabnik.github.io/jujutsu-tutorial/introduction/introduction.html

[suhr]

PPS: Don't forget --colocate

[Markus de Medeiros]

@suhr please merge the PR I made your prod-cmra branch (some lemmas got lost in your split and I need to rebase all the downstream PR's) Actually, don't worry about this, I'll just make a new PR with your changes since I need to rebase everything on top of this change anyways.

[Markus de Medeiros]

By the way, there is no need to squash your commits yourself, all this does is add extra work for maintaining the dependent PR's. Commits get squashed when merged to main.

[suhr]

These lemmas are a part of Add Updates commit.

[suhr]

I forgot that this commit also adds some CMRA lemmas (very few though).

[suhr]

Neither updates nor local updates are actually used in your PRs. That's why I moved CMRA lemmas in a separate PR.

[Markus de Medeiros]

Thanks for letting me know! I appreciate the effort to make things cleaner but in this case it's just extra work to update all the downstream PR's.

[suhr]

Yeah, I see. I just forgot that rebasing stuff with git is painful.

[Markus de Medeiros]

All good :) I'm still going to close your PRs and make new ones from a branch in iris-lean to make my life easier (they need to be rebased on top of the lean update last week, for example).

[Shreyas Srinivas]

I will soon be finishing the numbers Cmra. I am beginning to get comfortable with CMRAs. Are there other areas where I can assist in the porting next? Tactics for example?

[Markus de Medeiros]

I can definitely cut some more issues tomorrow!

[Markus de Medeiros]

So, a lot of the most important upcoming features are dependent on this big chain of PR's getting merged. Namely, there are quite a few example where we've implemented a CMRA but we're missing A) their updates or B) their functors. The Auth CMRA (and the related CMRA's in algebra/lib/*_auth) also open up once the chain of PR's is merged.

There is also the CSum CMRA, the STS CMRA, the list CMRA... these are examples of CMRA's which have no dependencies (aside from updates whose lemmas can be skipped) and which aren't strictly necessary but would be nice to port.

As for a more substantial task: someone could take on generalizing step indexing. This will break a lot of stuff so it's probably better to deal with that soon, but porting stepindex.v and stepindex_finite.v are non-breaking and a good first step.

[Shreyas Srinivas]

I looked at their step indexing. Essentially they define a step index as a type which has a well-ordering and a successor operation

[Shreyas Srinivas]

I have no idea why they define their carrier type as a field and why they define a structure instead of a class

[Markus de Medeiros]

Iris uses canonical structures in Rocq instead of typeclasses for performance reasons. We don't have to do that.

[Shreyas Srinivas]

I can PR this file. But I think we should consider the possibility that we are repeatedly defining common typeclasses. Like I have total ordering in numbers. Should I factor the common stuff out into a utils folder?

[Shreyas Srinivas]

It also seems sensible to keep cmra files limited to instance definitions and lemmas

[Mario Carneiro]

I speed-ran the queue, and reviewed/merged iris-lean#41, iris-lean#42, iris-lean#50, iris-lean#44, iris-lean#45, iris-lean#47, iris-lean#48, iris-lean#70, iris-lean#71, iris-lean#72, iris-lean#56, iris-lean#59, iris-lean#73. The queue of awaiting-review PRs is now empty :tada:

[Markus de Medeiros]

Check it out! I've started putting together a program logic for my work, and today I proved a base case for our adequacy theorem :)
Screenshot 2025-07-10 at 7.05.33 PM.png
Screenshot 2025-07-10 at 7.05.38 PM.png

You can see there's a lot of going in and out of proofmode even in this very simple proof to manually alter the proof state, which will quickly be a big problem for larger proofs. But simple "real" Iris proofs are becoming possible :)

[Markus de Medeiros]

I've finished porting gmap_view and (our generalization of) gmaps. My PR's need some refactoring but "Iris 0.5" is sorry-free!

[Markus de Medeiros]

Time to think of the next milestone, I suppose :)