Commit 7a42ec17 authored by Hai Dang's avatar Hai Dang
Browse files

add AsFractional to graph specs

parent a45346ba
......@@ -398,12 +398,14 @@ Local Existing Instances
StackInv_Timeless
StackInv_Objective
StackInv_Fractional
StackInv_AsFractional
StackLocal_Persistent
StackLocalLite_Persistent
StackLocalLite_Timeless
ExchangerInv_Timeless
ExchangerInv_Objective
ExchangerInv_Fractional
ExchangerInv_AsFractional
ExchangerLocal_Persistent
ExchangerLocalLite_Persistent
ExchangerLocalLite_Timeless
......@@ -564,14 +566,6 @@ Proof.
iExists Vbx', _, _, _, _. by iFrame.
Qed.
(* TODO duplicated proofs *)
Instance StackInv_asfractional γb b q Gb :
AsFractional (StackInv stk γb b q Gb) (λ q, StackInv stk γb b q Gb) q.
Proof. constructor; [done|apply _]. Qed.
Instance ExchangerInv_asfractional γx q Gx :
AsFractional (ExchangerInv ex γx q Gx) (λ q, ExchangerInv ex γx q Gx) q.
Proof. constructor; [done|apply _]. Qed.
#[global] Instance StackSharedInv_fractional γg s G b γb γx γ Gb Gx T :
Fractional (λ q, StackSharedInv γg s q G b γb γx γ Gb Gx T).
Proof.
......
......@@ -48,6 +48,7 @@ Definition is_maybe_pop e : Prop :=
Local Notation EMPTY := 0 (only parsing).
Local Notation FAIL_RACE := (-1) (only parsing).
(* TODO: generalize these types for graph specs *)
Definition StackLocalT Σ : Type :=
gname loc graph logView vProp Σ.
Definition StackLocalNT Σ : Type :=
......@@ -195,21 +196,26 @@ Definition pop_spec' {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)}
Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (graphR sevent)}
{StackConsistent : graph Prop} := StackSpec {
(* operations *)
(** operations *)
new_stack : val;
try_push : val;
push : val;
try_pop : val;
pop : val;
(* predicates *)
(** predicates *)
StackLocal : StackLocalNT Σ;
StackLocalLite : StackLocalT Σ;
StackInv : StackInvT Σ;
(** predicates properties *)
StackInv_Objective : γg s q G, Objective (StackInv γg s q G) ;
StackInv_Timeless : γg s q G, Timeless (StackInv γg s q G) ;
StackInv_Fractional : γg s G, Fractional (λ q, StackInv γg s q G) ;
(* TODO: one might want exclusiveness for StackInv *)
StackInv_Fractional : γg s G, Fractional (λ q, StackInv γg s q G) ;
StackInv_AsFractional : γg s q G,
AsFractional (StackInv γg s q G) (λ q, StackInv γg s q G) q ;
StackInv_StackConsistent : γg s q G, StackInv γg s q G StackConsistent G ;
StackInv_graph_master_acc :
γg s q G, StackInv γg s q G
......
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