GitLab

For Perennial, @jtassaro developed a notion of "fancy updates" that satisfies all the laws we have in Iris, plus way more. Unfortunately this means we cannot directly use anything from base_logc/lib and above, even though all these proofs do go through unchanged.

This change is likely not canonical enough to be upstreamable, and I see no way to make our notion of fancy updates itself general enough that @jtassaro's update are an instance of them. The design space is very wide open here.

It would thus be useful if we could parameterize the definition of WP by the notion of fancy update, and similar for some of the things in base_logic/lib -- everything that mentions fancy updates, basically (or at least anything useful; I don't think it is worth doing this with STS and auth). Maybe some things can be changed to use basic updates instead of fancy updates, which would avoid the need for parameterization.

Even semantic invariants themselves can be defined generally for any fancy update; the only thing that each update would need to prove is the allocation lemma(s).

@robbertkrebbers what do you think?