Commit 5c1f67f1 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

gc library: definitions

parent c3aaa5db
Pipeline #17713 failed with stage
From iris.algebra Require Import auth excl gmap.
From iris.base_logic.lib Require Export own invariants.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Export lang locations lifting.
Set Default Proof Using "Type".
Import uPred.
Definition gc_mapUR : ucmraT := gmapUR loc $ optionR $ exclR $ leibnizC val.
Definition to_gc_map (gcm: gmap loc val) : gc_mapUR :=
fmap (λ v, Some (Excl (v : leibnizC val))) gcm.
Class gc_mapG (Σ : gFunctors) := Gc_mapG {
gc_map_inG :> inG Σ (authR (gc_mapUR));
}.
Definition gc_mapΣ : gFunctors :=
#[ GFunctor (authR (gc_mapUR)) ].
Instance subG_gc_mapG {Σ} : subG gc_mapΣ Σ gc_mapG Σ.
Proof. solve_inG. Qed.
Section defs.
Context `{!invG Σ, !heapG Σ, !gc_mapG Σ} (γ: gname)(N: namespace).
Definition gc_inv : iProp Σ :=
(inv N ((gcm: gmap loc val), own γ ( to_gc_map gcm) ([ map] l v gcm, (l v)) ) )%I.
Definition gc_mapsto (l: loc) (v: val) : iProp Σ := own γ ( {[l := Some $ Excl $ v]}).
Definition is_gc_loc (l: loc) : iProp Σ := own γ ( {[l := None]}).
End defs.
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