Commit ce28da7a authored by Hai Dang's avatar Hai Dang
Browse files

Minor cleanup in stack hist spec

parent 5c4b39ff
...@@ -31,7 +31,7 @@ Section Stack. ...@@ -31,7 +31,7 @@ Section Stack.
Hypothesis qu : queue_per_elem_spec Σ. Hypothesis qu : queue_per_elem_spec Σ.
(** Assuming history-based Stack spec *) (** Assuming history-based Stack spec *)
Hypothesis stk : a_stack_spec Σ. Hypothesis stk : stack_spec Σ.
Definition prog : expr := Definition prog : expr :=
let: "s" := stk.(new_stack) [] in let: "s" := stk.(new_stack) [] in
......
...@@ -2588,8 +2588,8 @@ Proof. ...@@ -2588,8 +2588,8 @@ Proof.
Qed. Qed.
End proof. End proof.
Program Definition treiber_stack_impl `{!noprolG Σ, !tstackG Σ, !atomicG Σ} Definition treiber_stack_impl `{!noprolG Σ, !tstackG Σ, !atomicG Σ}
: a_stack_spec Σ := {| : stack_spec Σ := {|
spec_history.StackInv_Objective := StackInv_objective ; spec_history.StackInv_Objective := StackInv_objective ;
spec_history.StackInv_StackLinearizability := StackInv_StackLinearizability_instance ; spec_history.StackInv_StackLinearizability := StackInv_StackLinearizability_instance ;
spec_history.StackInv_history_master_acc := StackInv_history_master_acc_instance ; spec_history.StackInv_history_master_acc := StackInv_history_master_acc_instance ;
......
...@@ -231,7 +231,6 @@ Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)} := StackSpec { ...@@ -231,7 +231,6 @@ Record stack_spec {Σ} `{!noprolG Σ, !inG Σ (historyR sevent)} := StackSpec {
Arguments stack_spec _ {_ _}. Arguments stack_spec _ {_ _}.
Existing Instances StackInv_Objective StackInv_Timeless StackLocal_Persistent. Existing Instances StackInv_Objective StackInv_Timeless StackLocal_Persistent.
Definition a_stack_spec Σ `{!noprolG Σ, !inG Σ (historyR sevent)} := stack_spec Σ.
(** Properties of stack spec *) (** Properties of stack spec *)
......
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