Fancy Update Has Later Credit Parameter Update

Fancy Updates with explicit has_lc parameters

Previously, the use of later credits hlc : has_lc for fancy updates was globally fixed by the instance of invGS_gen hlc Σ. When later credits are globally enabled, we cannot extract plain information from behind fancy updates. Sometimes, we want some fancy updates to not use later credits, and other fancy updates to have later credits. If this merge request is accepted, it will allow us to remove the coinductive machinery from the definition for logically atomic updates.

Thus, in this merge request we update Iris to have explicit has_lc parameters for fancy updates, allowing different kinds of fancy updates to coexist in the same definitions and proofs.

Since the logically atomic definitions will be reworked in a future merge request, this changes fix logically atomic definitions to use later credits in the hope to minimize changes to proofs using logical atomicity in this repository and the iris examples repo. In the succeeding merge request more dramatic changes will take place.

Changes to Fancy Updates

• Fancy updates in iris/bi/updates.v how have an explicit has_lc parameter.
• The notation for parameterized updates is |=⟨ hlc ⟩{ E1 , E2 }=> Q.
• The default notation |={E1,E2}=> Q denotes |=⟨ HasLc ⟩{ E1 , E2 }=> Q.
• |={ E1 , E2 }€=> Q denotes |=⟨ HasNoLc ⟩{ E1 , E2 }=> Q.
• Define a total order on has_lc called has_lc_less_than_eq_def such that HasNoLc < HasLc.
• Introduce a new proof rule for fancy updates:

  bi_fupd_mixin_fupd_has_lc_weaken_less_than E1 E2 (P : PROP) :
    (|={E1,E2}€=> P) ⊢ |={E1,E2}=> P

Changes to Proofmode

• Introduce a new type class HasLcLessThanEq for the total order on has_lc.
• Instances for ElimModal for fancy updates now allow one to iMod a hypothesis with a fancy update with a weaker has_lc than the goal (elim_modal_fupd_fupd).
• Instances for ElimAcc for fancy updates also allow one to iMod an accessor hypothesis with a fancy update with a weaker has_lc than the goal (elim_acc_fupd).
• Automation for envs_entails takes into account the general form |=⟨ _ ⟩{ _ }=> _.
• iApply "H" may no longer suffice in cases where "H" and the goal are fancy updates with different later credit options.

Changes to Base Logic

• The invGS_gen hlc Σ type class in iris/base_logic/lib/fancy_updates.v is replaced with just invGS Σ: this type class no longer fixes the global has_lc for all fancy updates.
• Invariants use fancy updates with no later credits in their definition.
• Many lemmas are how parametric with respect to has_lc. Occasionally, an explicit has_lc parameter is needed when invoking some lemmas, such as inv_alloc.

Changes to Program Logic

• irisGS_gen hlc Σ now fixes hlc : has_lc for all weakest preconditions.
• Logically atomic updates and triples just use HasLc for now.

Changes to Tests

• Tests for eliminations with ElimModal added when later credit option between the goal and hypothesis differ.
• Test output changed to account for explicit has_lc parameter.