Commit d21da3ed authored by Ralf Jung's avatar Ralf Jung

equip remaining specs with the fact that names are countable (just in case)

parent e72057ce
Pipeline #17369 passed with stage
in 6 minutes and 23 seconds
......@@ -27,6 +27,8 @@ Record hocap_stack {Σ} `{!heapG Σ} := AtomicStack {
pop : val;
(* -- other data -- *)
name : Type;
name_eqdec : EqDecision name;
name_countable : Countable name;
(* -- predicates -- *)
is_stack (N : namespace) (γs : name) (v : val) : iProp Σ;
stack_content_frag (γs : name) (l : list val) : iProp Σ;
......@@ -61,9 +63,9 @@ Record hocap_stack {Σ} `{!heapG Σ} := AtomicStack {
}.
Arguments hocap_stack _ {_}.
Existing Instance is_stack_persistent.
Existing Instance stack_content_frag_timeless.
Existing Instance stack_content_auth_timeless.
Existing Instances
is_stack_persistent stack_content_frag_timeless stack_content_auth_timeless
name_eqdec name_countable.
(** Show that our way of writing the [pop_spec] is equivalent to what is done in
[concurrent_stack.spec]. IOW, the conjunction-vs-match doesn't matter. Fixing
......
......@@ -11,6 +11,8 @@ Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack {
pop : val;
(* -- other data -- *)
name : Type;
name_eqdec : EqDecision name;
name_countable : Countable name;
(* -- predicates -- *)
is_stack (N : namespace) (γs : name) (v : val) : iProp Σ;
stack_content (γs : name) (l : list val) : iProp Σ;
......@@ -36,5 +38,6 @@ Record atomic_stack {Σ} `{!heapG Σ} := AtomicStack {
}.
Arguments atomic_stack _ {_}.
Existing Instance is_stack_persistent.
Existing Instance stack_content_timeless.
Existing Instances
is_stack_persistent stack_content_timeless
name_countable name_eqdec.
......@@ -17,6 +17,8 @@ Record atomic_snapshot {Σ} `{!heapG Σ} := AtomicSnapshot {
readPair : val;
(* other data *)
name: Type;
name_eqdec : EqDecision name;
name_countable : Countable name;
(* predicates *)
is_pair (N : namespace) (γ : name) (p : val) : iProp Σ;
pair_content (γ : name) (a: val * val) : iProp Σ;
......@@ -48,3 +50,7 @@ Record atomic_snapshot {Σ} `{!heapG Σ} := AtomicSnapshot {
<<< pair_content γ (v1, v2), RET (v1, v2) >>>;
}.
Arguments atomic_snapshot _ {_}.
Existing Instances
is_pair_persistent pair_content_timeless
name_countable name_eqdec.
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