Library iris.bi.sbi

The Step-indexed BI (SBI) interface describes BIs with a step-indexed structure. An SBI has an operation si_pure : siProp → PROP that embeds an siProp (a pure step-indexed proposition, think of siProp ≈ nat → Prop) into the logic while preserving the step-index, and si_emp_valid : PROP → siProp expresses that a proposition is valid (under assumption emp) at a given step-index. One should think of si_pure as a step-indexed version of bi_pure and si_emp_valid as a step-indexed version of bi_emp_valid, in both cases with siProp instead of Prop. Note that typically, all bi instances with a non-trivial ▷ operator should have an Sbi instance. However, it is possible to omit Sbi and just prove BiLöb directly if one does not need the additional results provided by Sbi. This may change in the future, and ▷ might be moved to Sbi.

Derived definitions/results

For any SBI we obtain the following results:

• "Internal equality" x ≡ y, which compares x, y : A for A : ofe, by internalizing dist n x y into the logic. This notion is defined as x ≡ y := <si_pure> siProp_internal_eq P Q, see iris.bi.internal_eq.
• "Internal validity" ✓ x, which expresses validity of x : A for A : cmra by internalizing cmra_validN n x into the logic. This notion is defined as ✓ x := <si_pure> siProp_cmra_valid x, see iris.bi.cmra.
• The "plainly modality" ■ P, which says that a proposition P holds without depending on any resources (but preserving the step-index). It is different from the persistence modality (<pers>/□), which says that the proposition only depends on non-exclusive resources (also preserving the step-index). The plainly modality is defined as ■ P := <si_pure> <si_emp_valid> P, see iris.bi.plainly.
• The class of "plain" propositions, which is defined as Plain P := P ⊢ ■ P, see iris.bi.plainly.
• Generic soundness theorems (which follow from soundness of siProp): + pure_soundness : (⊢ ⌜ φ ⌝) → φ + later_soundness : (⊢ ▷ P) → ⊢ P + internal_eq_soundness : (⊢ x ≡ y) → x ≡ y
• Internal characterizations of NonExpansive and Contractive: + ne_internal_eq : NonExpansive f ↔ ∀ x1 x2, x1 ≡ x2 ⊢ f x1 ≡ f x2 + contractive_internal_eq : Contractive f ↔ ∀ x1 x2, ▷ (x1 ≡ x2) ⊢ f x1 ≡ f x2
• Later is contractive sbi_later_contractive, which in turn gives Löb induction, i.e., an instance of BiLöb (allowing one to use the iLöb tactic).

Prototypical instance

For uPred M ≈ nat → M → Prop, we define (recall siProp ≈ nat → Prop): si_pure (φ : siProp) : uPred M := λ n r, φ n si_emp_valid (P : uPred M) : siProp := λ n, P n ε In an affine BI like uPred we could have equivalently defined si_emp_valid as λ n, ∀ x, ✓{n} x → P n x. However, for a linear version of uPred (without monotonicity condition on M), one really needs ε. Otherwise the law si_emp_valid_affinely_2 does not hold, i.e., si_emp_valid P does not say P holds under <affine>.

Sbi versus siProp

End-users should always use the generic SBI definitions, instead of siProp, even when using siProp itself. In particular, one should always use ≡/✓ instead of siProp_internal_eq/siProp_cmra_valid. The latter definitions are used privately to define ≡/✓ and are not meant for end-users. Lemmas about internal equality and validity are stated universally over any SBI. For example, we have: internal_eq_sym `{!Sbi PROP} {A : ofe} (a b : A) : a ≡ b ⊢@{PROP} b ≡ a prod_includedI `{!Sbi PROP}{A B : cmra} (x y : A * B) : x ≼ y ⊣⊢ x.1 ≼ y.1 ∧ x.2 ≼ y.2 instead of versions specialized to siProp (using siProp_internal_eq). The reason we state lemmas generically is that one can directly use them in any SBI without having to distribute si_pure, making proofs in user-space much easier.

Proving SBI lemmas for custom OFEs and CMRAs

To prove lemmas such as prod_includedI, we typically want to drop down to the model of siProp and lift the corresponding step-indexed lemmas on OFEs/CMRAs. This is done using the tactic sbi_unfold, see iris.bi.sbi_unfold. Consider the example prod_includedI discussed above, calling sbi_unfold gives: ∀ n : nat, x ≼{n} y ↔ x.1 ≼{n} y.1 ∧ x.2 ≼{n} y.2 This is exactly the step-indexed lemma prod_includedN. See iris.bi.algebra how step-indexed lemmas about OFEs and CMRAs are lifted to SBIs.

si_pure and si_emp_valid are non-expansive and monotone

si_emp_valid is a left inverse for si_pure

The other way around does not hold, i.e., <si_pure> <si_emp_valid> P is not equivalent to P. This is easy to see in the prototypical model (uPred above) as the conversion erases the resources. (In other words, plainly is not the identity.) The best we get is that if <si_pure> <si_emp_valid> P (i.e., P holds under then empty resource), then P holds persistently. Note that this is ■ P ⊢ <pers> P (the usual elimination rule for plainly) but that notation is defined as a derived notion on top of this interface.

si_pure commutes with implication, universal quantification, and later. The commuting rules for other connectives (and other directions) are derived.

si_pure is absorbing (i.e., we have P ∗ <si_pure> φ ⊢ <si_pure> φ. This is similar to bi_pure being absorbing.

si_emp_valid commutes with later. The commuting rules for other connectives (and other directions) are derived.

The following rule expresses that si_emp_valid actually ensures P holds with the empty resource, i.e., under the affinely modality.

There is one more law we would like to include in Sbi, and that is: ∀ P Q : PROP, <si_emp_valid> (P ∗-∗ Q) ⊢@{siPropI} P ≡ Q However, this law cannot be part of the mixin above since it uses ≡ which is defined in terms of Sbi. So instead we state the law using lower-level primitives such as siProp_internal_eq. However, we want to avoid users having to see this low-level form, so we make this law a separate mixin that users are not expected to construct directly, but instead using the sbi_prop_ext_mixin smart constructor (see iris.bi.internal_eq). This is separate from SbiMixin since it is easier to have a smart constructor for a single law than for all laws. Similarly, when using the Sbi class, end-users should not use the field of the mixin, but rather one of the following lemmas: prop_ext_2 : ■ (P ∗-∗ Q) ⊢@{PROP} P ≡ Q prop_ext_si_emp_valid_2 : <si_emp_valid> (P ∗-∗ Q) ⊢@{siPropI} P ≡ Q

SbiEmpValidExist generalizes that plainly ■ commutes with existentials and disjunction (in both directions), see plainly_exist and plainly_or. This law does not hold for every SBI. For instance, for monPred I PROP it only holds if I has a bottom element: Assume that I uses equality as its order, and PROP:=siProp, then <si_emp_valid> P means that P holds for any i. So on the LHS we can have a different x for each i, while on the RHS we need one i for any x. However, if I has a bottom element, we can obtain the witness x for the bottom element on the LHS, and use monotonicy to conclude it holds for any i on the RHS. See also monPred_sbi_emp_valid_exist.

BiPersistentlyImplSiPure generalizes that persistent propositions are closed under implication and wand (subject to other conditions), see impl_persistent and wand_persistent. This property does not hold for every BI, take monPred I PROP, where it only holds if I has a bottom element. See monPred_bi_persistently_impl_si_pure.

siProp is an SBI by taking <si_pure> and <si_emp_valid> to be the identity. Although this instance is trivial, it is a very useful one. It means that all lemmas and instances about internal equality ≡ and internal validity ✓ also apply to siProp (and we do not need to state specialized versions).

The primitive laws

The derived laws

Commuting rules of <si_pure>

Version of primitive si_pure_si_emp_valid for Absorbing P and with <affine> added.

Commuting rules of <si_emp_valid>

Relating ⊢ in siProp to ⊢ in PROP

Soundness lemmas The version for internal equality internal_eq_soundness can be found in iris.bi.internal_eq.