Commit 3761273c authored by Ralf Jung's avatar Ralf Jung
Browse files

auth: more precise comments

parent 685148ab
...@@ -2,16 +2,17 @@ From algebra Require Export auth. ...@@ -2,16 +2,17 @@ From algebra Require Export auth.
From program_logic Require Export invariants ghost_ownership. From program_logic Require Export invariants ghost_ownership.
Import uPred. Import uPred.
(* TODO: Once we switched to RAs, it is no longer necessary to remember that a
is constantly valid. *)
Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG { Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
auth_inG :> inG Λ Σ (authRA A); auth_inG :> inG Λ Σ (authRA A);
auth_identity :> CMRAIdentity A; auth_identity :> CMRAIdentity A;
(* TODO: Once we switched to RAs, this can be removed. *)
auth_timeless (a : A) :> Timeless a; auth_timeless (a : A) :> Timeless a;
}. }.
Section definitions. Section definitions.
Context `{authG Λ Σ A} (γ : gname). Context `{authG Λ Σ A} (γ : gname).
(* TODO: Once we switched to RAs, it is no longer necessary to remember that a
is constantly valid. *)
Definition auth_inv (φ : A iPropG Λ Σ) : iPropG Λ Σ := Definition auth_inv (φ : A iPropG Λ Σ) : iPropG Λ Σ :=
( a, ( a own γ ( a)) φ a)%I. ( a, ( a own γ ( a)) φ a)%I.
Definition auth_own (a : A) : iPropG Λ Σ := own γ ( a). Definition auth_own (a : A) : iPropG Λ Σ := own γ ( a).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment