Library iris.base_logic.lib.later_credits

This file implements later credits, in particular the later-elimination update. That update is used internally to define the Iris fupd; it should not usually be directly used unless you are defining your own fupd.

The hlc : has_lc parameter indicates whether later credits are enabled or not. From a user's point of view there are two differences:

• If later credits are enabled (hlc = HasLc), we obtain the rule lc_le_upd_elim_later : £ 1 -∗ (▷ P) -∗ |==£> P, which allows us strip a later by spending a credit. This rule is used to prove the similar rule for the fancy update modality.
• If later credits are disabled (hlc = HasNoLc), we obtain the rule le_upd_keep : (|==£|> P) ∧ (P -∗ |==£> Q) ⊢ |==£> Q without the side-condition that P should be timeless (the "finally" modality |==£|> is described further below in this file). This rule is used to derive the plain interaction rules BiFUpdSbi of the fancy update modality.

In the model, if later credits are disabled (hlc = HasNoLc), we simply define the credit £ n as True and the supply lc_supply n as n = 0. This choice gives uniform proofs, where we do not have to case split on hlc for nearly all rules.

The ghost state for later credits

The user-facing credit resource, denoting ownership of n credits (but only if later credits are enabled).

The internal authoritative part of the credit ghost state, tracking how many credits are available in total. Users should not directly interface with this.

The splitting rules for £ hold regardless of whether later credits are enabled. If later credits are disabled (hlc = HasNoLc, these rules are not useful on their own, but they can be used to write adequacy/soundness proof that are generic in the choice of hlc.

Make sure that the rule for + is used before S, otherwise Coq's unification applies the S hint too eagerly. See Iris issue 470.

When combining later credits with iCombine, the priorities are reversed when compared to FromSep and IntoSep. This causes £ n and £ 1 to be combined as £ (S n), not as £ (n + 1).

The (internal) lc_supply rules are only vald if later credits are enabled.

The later-elimination update Let users import the above without also getting the below laws. This should only be imported by the internal development of fancy updates.

Case 1: Generalization of except-0 ◇, needed for proving the rule le_upd_keep. There we obtain ▷^n ◇ P for a timeless P, and need to eliminate n laters and one except-0, which can be done by having a disjunct ▷^(S n) False in the goal.

Case 2: No credits are spent.

Case 3: Eliminate a later by decreasing the credit supply (which means at least one credit needs to be spent). This case is impossible if later credits are disabled (HasNoLc), because m < 0 is false.

If later credits are disabled, this lemma shows that le_upd is just the basic update + except-0 modality, i.e., fancy updates are like Iris 3.0.

Rules for the later elimination update

Derived lemmas

A safety check that later-elimination updates can replace basic updates We do not use this to build an instance, because it would conflict with the basic updates.

Proof mode class instances internally needed for people defining their fupd with le_upd.

You probably do NOT want to use these lemmas; use lc_soundness if you want to actually use le_upd!

Flexible soundness theorem through "finally" modality. The later-elimination finally modality le_upd_finally is used internally in the finally modality for fancy updates (fupd_finally). It should not be used directly by end-users. See the file fancy_updates for documentation how to prove soundness/adequacy results using the user-facing finally modality. Compared to the later-elimination modality le_upd itself, this modality only consumes the supply lc_supply, but does not give it back. This change allows us to prove the rules le_upd_finally_later, le_upd_finally_keep, and le_upd_finally_forall, which cannot be proven for le_upd. For instance, to prove le_upd_finally_forall the goal is ▷^m ◇ ■ ∀ x, Φ x where we can just commute out the ∀. Such a proof does not work for a corresponding lemma for le_upd because we cannot commute out the ∀. Due to the plain modality ■, we can perform basic updates around le_upd_finally (we have (|==> ■ P) ⊣⊢ ■ P). This fact is exposed by the rule le_upd_le_upd_finally combined with the rule bupd_le_upd.

Commute a later out of the modality. This only works if the proposition below the later can be turned into an except-0 ◇.

Add a later credit by removing a later below the modality. This only works if the proposition below the later can be turned into an except-0 ◇.

Derived rules Since the modality is used only internally in the version for fancy updates, we do not provide instances of the proof mode classes.