iris.v 1.08 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
From iris.program_logic Require Export ghost_ownership language.
From iris.prelude Require Export coPset.
From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.

Class irisPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
  state_inG :> inG Σ (authUR (optionUR (exclR (stateC Λ))));
  invariant_inG :> inG Σ (authUR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
  enabled_inG :> inG Σ coPset_disjUR;
  disabled_inG :> inG Σ (gset_disjUR positive);
}.

Class irisG (Λ : language) (Σ : gFunctors) : Set := IrisG {
  iris_pre_inG :> irisPreG Λ Σ;
  state_name : gname;
  invariant_name : gname;
  enabled_name : gname;
  disabled_name : gname;
}.

20
Definition irisGF (Λ : language) : gFunctorList :=
21 22 23 24 25
  [GFunctor (constRF (authUR (optionUR (exclR (stateC Λ)))));
   GFunctor (authRF (gmapURF positive (agreeRF (laterCF idCF))));
   GFunctor (constRF coPset_disjUR);
   GFunctor (constRF (gset_disjUR positive))].

26
Instance inGF_barrierG `{H : inGFs Σ (irisGF Λ)} : irisPreG Λ Σ.
27 28 29
Proof.
  by destruct H as (?%inGF_inG & ?%inGF_inG & ?%inGF_inG & ?%inGF_inG & _).
Qed.