Commit c3423d5a authored by Simon Friis Vindum's avatar Simon Friis Vindum

Refactor and cleanup proofs

parent 3a99baa4
......@@ -66,8 +66,8 @@ theories/logrel/F_mu_ref_conc/examples/queue/common.v
theories/logrel/F_mu_ref_conc/examples/queue/MS_queue.v
theories/logrel/F_mu_ref_conc/examples/queue/MS_queue_alt.v
theories/logrel/F_mu_ref_conc/examples/queue/CG_queue.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement_alt.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement_variant.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement_original.v
theories/logrel/F_mu_ref_conc/examples/fact.v
theories/logrel/heaplang/ltyping.v
......
......@@ -2,6 +2,9 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Import weakestpre.
From iris_examples.logrel.F_mu_ref_conc Require Import examples.lock.
From iris.program_logic Require Import adequacy ectxi_language.
From iris.proofmode Require Import tactics.
From iris.algebra Require Import list.
From iris.program_logic Require Export lifting.
From iris_examples.logrel.F_mu_ref_conc Require Export logrel_binary.
......@@ -17,13 +20,11 @@ Definition TNodeBody τ v := TMaybe (TProd (TMaybe τ.[ren (+1)]) (Tref (Tref v)
Definition TNode τ := TRec (TNodeBody τ (TVar 0)).
Definition MS_QueueType τ := Tref (Tref (TNode τ)).
Definition Node x out := Fold (some (Pair (some x) (Loc out))).
(* Get the value of a some and spin it the argument is a none. *)
Definition getValue (e : expr) : expr :=
(Case
e
(App (Rec (App (Var 0) Unit)) Unit)
(Var 0)
).
(Case e (App (Rec (App (Var 0) Unit)) Unit) (Var 0)).
(* Pseudo code for dequeue:
rec try() =>
......@@ -37,6 +38,7 @@ Definition getValue (e : expr) : expr :=
else (try ())
*)
(* The dequeue operation is the same for both variants of the queue. *)
Definition MS_dequeue :=
(Rec (* try(_) *)
(LetIn
......@@ -59,8 +61,9 @@ Definition MS_dequeue :=
).
(* Pseudo code for enqueue:
fun x =>
fun x =
let n = alloc (fold (some (some x), (alloc (alloc (fold none))))))
tt = !head
in
(rec try(c) =>
let t = !c
......@@ -71,10 +74,10 @@ Definition MS_dequeue :=
Right c' =>
try (snd c')
)
(snd (getValue (unfold !!head)))
(snd (getValue (unfold !t)))
*)
Definition MS_enqueue :=
Definition MS_enqueue_variant :=
(Lam (* x *)
(LetIn
(* n = *) (Alloc (Fold (some (Pair (some (Var 0 (* x *))) (Alloc (Alloc (Fold none)))))))
......@@ -107,14 +110,78 @@ Definition MS_enqueue :=
)
).
Definition MS_queue : expr :=
Definition MS_queue_variant : expr :=
TLam (* _ *)
(LetIn (* node = *) (Alloc (Fold (some (Pair (none) (Alloc (Alloc (Fold none)))))))
(LetIn
(* tail = *) (Alloc (Var 0 (* node *)))
(LetIn
(* head = *) (Alloc (Var 1 (* node *)))
(Pair MS_dequeue MS_enqueue_variant)
))).
(* The original MS-queue *)
(* Pseudo code for enqueue:
fun x =>
let n = alloc (fold (some (some x), (alloc (alloc (fold none))))))
in
(rec try(_) =>
let c = (snd (getValue (unfold !!tail)))
t = !c
in case (unfold !t) with
Left _ => if CAS c t n
then
tail <- n ;;
()
else try ()
Right c' => try ()
)
()
*)
Definition MS_enqueue_original :=
(Lam (* x. *)
(LetIn
(* n = *) (Alloc (Fold (some (Pair (some (Var 0 (* x *))) (Alloc (Alloc (Fold none)))))))
(App
(Rec (* try(_) *)
(LetIn
(* c = *) (Snd (getValue (Unfold (Load (Load (Var 5 (* tail *)))))))
(LetIn
(* t = *) (Load (Var 0 (* c *)))
(Case
(Unfold (Load (Var 0 (* t *))))
(* c = InjL ... Tail is nil, we can try to insert now *)
(If
(CAS (Var 2 (* c *)) (Var 1 (* t *)) (Var 5 (* n *)))
(* Insertion succeeded *)
(Seq
(* Update the tail pointer *)
(Store (Var 8 (* tail *)) (Var 5 (* n *)))
Unit)
(* Insertion failed, we try again*)
(App (Var 3 (* try *)) Unit)
)
(* c = InjR c' =>. We are not at the end yet, try again.*)
(App (Var 3 (* try *)) Unit)
)
)
)
)
Unit
)
)
).
Definition MS_queue_original : expr :=
TLam (* _ *)
(LetIn (* node = *) (Alloc (Fold (some (Pair (none) (Alloc (Alloc (Fold none)))))))
(LetIn
(* tail = *) (Alloc (Var 0 (* node *)))
(LetIn
(* head = *) (Alloc (Var 1 (* node *)))
(Pair MS_dequeue MS_enqueue)
(Pair MS_dequeue MS_enqueue_original)
))).
Section MS_queue.
......@@ -128,8 +195,33 @@ Section MS_queue.
intros ?. repeat econstructor. eassumption.
Qed.
Lemma MS_enqueue_type Γ τ :
typed (MS_QueueType τ :: MS_QueueType τ :: Γ) MS_enqueue (TArrow τ TUnit).
Lemma MS_dequeue_type Γ τ :
typed (MS_QueueType τ :: Γ) MS_dequeue (TArrow TUnit (TMaybe τ)).
Proof.
econstructor.
econstructor.
{ repeat econstructor. }
econstructor.
{ apply getValue_type.
eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
}
econstructor.
- eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
- repeat econstructor.
- econstructor.
+ econstructor.
2: { econstructor. reflexivity. }
* econstructor.
* econstructor. reflexivity.
* repeat econstructor.
+ repeat econstructor. asimpl. done.
+ repeat econstructor.
Qed.
Lemma MS_enqueue_variant_type Γ τ :
typed (MS_QueueType τ :: MS_QueueType τ :: Γ) MS_enqueue_variant (TArrow τ TUnit).
Proof.
econstructor.
econstructor.
......@@ -167,33 +259,60 @@ Section MS_queue.
* repeat econstructor.
Qed.
Lemma MS_dequeue_type Γ τ :
typed (MS_QueueType τ :: Γ) MS_dequeue (TArrow TUnit (TMaybe τ)).
Lemma MS_queue_variant_type Γ :
typed Γ MS_queue_variant
(TForall (TProd
(TArrow TUnit (TMaybe (TVar 0)))
(TArrow (TVar 0) TUnit)
)
).
Proof.
econstructor.
econstructor.
{ repeat econstructor. }
econstructor.
{ apply getValue_type.
eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
}
econstructor.
- eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
- econstructor.
apply (TFold _ _ (TNodeBody (TVar 0) (TVar 0))).
repeat econstructor.
- repeat econstructor.
- econstructor.
+ repeat econstructor.
+ econstructor.
2: { econstructor. reflexivity. }
* econstructor.
* econstructor. reflexivity.
* repeat econstructor.
+ repeat econstructor. asimpl. done.
+ repeat econstructor.
* econstructor.
-- apply MS_dequeue_type.
-- apply MS_enqueue_variant_type.
Qed.
Lemma MS_enqueue_original_type Γ τ :
typed (MS_QueueType τ :: MS_QueueType τ :: Γ) MS_enqueue_original (TArrow τ TUnit).
Proof.
econstructor. econstructor.
- econstructor.
apply (TFold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor. asimpl. done.
- econstructor.
2: { econstructor. }
econstructor. econstructor.
+ econstructor.
apply getValue_type.
apply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
+ asimpl.
econstructor.
* repeat constructor.
* econstructor.
-- apply (TUnfold _ _ (TNodeBody τ (TVar 0))). repeat constructor.
-- econstructor.
++ econstructor.
2: { by constructor. }
repeat econstructor.
repeat econstructor.
repeat econstructor.
++ repeat econstructor.
++ repeat econstructor.
-- repeat econstructor.
Qed.
Lemma MS_queue_type Γ :
typed Γ MS_queue
Lemma MS_queue_original_type Γ :
typed Γ MS_queue_original
(TForall (TProd
(TArrow TUnit (TMaybe (TVar 0)))
(TArrow (TVar 0) TUnit)
......@@ -211,7 +330,6 @@ Section MS_queue.
* repeat econstructor.
* econstructor.
-- apply MS_dequeue_type.
-- apply MS_enqueue_type.
-- apply MS_enqueue_original_type.
Qed.
End MS_queue.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import weakestpre.
From iris_examples.logrel.F_mu_ref_conc Require Import examples.lock.
From iris.algebra Require Import list.
From iris.program_logic Require Export lifting.
From iris_examples.logrel.F_mu_ref_conc Require Export logrel_binary.
From iris_examples.logrel.F_mu_ref_conc Require Import rules_binary.
Import uPred.
Definition TMaybe τ := (TSum TUnit τ).
Definition none := InjL Unit.
Definition some v := InjR v.
Definition TNodeBody τ v := TMaybe (TProd (TMaybe τ.[ren (+1)]) (Tref (Tref v))).
Definition TNode τ := TRec (TNodeBody τ (TVar 0)).
Definition MS_QueueType τ := Tref (Tref (TNode τ)).
(* Get the value of a some and spin it the argument is a none. *)
Definition getValue (e : expr) : expr :=
(Case e (App (Rec (App (Var 0) Unit)) Unit) (Var 0)).
(* Pseudo code for dequeue:
rec try() =>
let n = !head
c = getValue (unfold !n)
in case unfold !!(snd c) with
Nil => none
Cons x xs =>
if CAS head n !(snd c)
then some (getValue x)
else (try ())
*)
Definition MS_dequeue :=
(Rec (* try(_) *)
(LetIn
(* n = *) (Load (Var 2 (* head *)))
(LetIn
(* c = *) (getValue (Unfold (Load ((Var 0 (* n *))))))
(Case
(Unfold (Load (Load (Snd (Var 0 (* c *)))))) (* Get next node after sentinel *)
(* Snd n = InjL Unit => *)
none (* The queue is empty, return none *)
(* Snd n = InjR n' => *)
(If
(CAS (Var 5 (* head *)) (Var 2 (* n *)) (Load (Snd (Var 1 (* c *)))))
(some (getValue (Fst (Var 0 (* n' *)))))
(App (Var 3 (* try *)) Unit)
)
)
)
)
).
(* Pseudo code for enqueue:
fun x =>
let n = alloc (fold (some (some x), (alloc (alloc (fold none))))))
in
(rec try(_) =>
let c = (snd (getValue (unfold !!tail)))
t = !c
in case (unfold !t) with
Left _ => if CAS c t n
then
tail <- n ;;
()
else try ()
Right c' => try ()
)
()
*)
Definition MS_enqueue :=
(Lam (* x. *)
(LetIn
(* n = *) (Alloc (Fold (some (Pair (some (Var 0 (* x *))) (Alloc (Alloc (Fold none)))))))
(App
(Rec (* try(_) *)
(LetIn
(* c = *) (Snd (getValue (Unfold (Load (Load (Var 5 (* tail *)))))))
(LetIn
(* t = *) (Load (Var 0 (* c *)))
(Case
(Unfold (Load (Var 0 (* t *))))
(* c = InjL ... Tail is nil, we can try to insert now *)
(If
(CAS (Var 2 (* c *)) (Var 1 (* t *)) (Var 5 (* n *)))
(* Insertion succeeded *)
(Seq
(* Update the tail pointer *)
(Store (Var 8 (* tail *)) (Var 5 (* n *)))
Unit)
(* Insertion failed, we try again*)
(App (Var 3 (* try *)) Unit)
)
(* c = InjR c' =>. We are not at the end yet, try again.*)
(App (Var 3 (* try *)) Unit)
)
)
)
)
Unit
)
)
).
Definition MS_queue : expr :=
TLam (* _ *)
(LetIn (* node = *) (Alloc (Fold (some (Pair (none) (Alloc (Alloc (Fold none)))))))
(LetIn
(* tail = *) (Alloc (Var 0 (* node *)))
(LetIn
(* head = *) (Alloc (Var 1 (* node *)))
(Pair MS_dequeue MS_enqueue)
))).
Section MS_queue_alt.
Context `{heapIG Σ, cfgSG Σ}.
(* Check the types of the various functions. *)
Lemma getValue_type Γ τ e :
typed Γ e (TMaybe τ) typed Γ (getValue e) τ.
Proof.
intros ?. repeat econstructor. eassumption.
Qed.
Lemma MS_enqueue_type Γ τ :
typed (MS_QueueType τ :: MS_QueueType τ :: Γ) MS_enqueue (TArrow τ TUnit).
Proof.
econstructor. econstructor.
- econstructor.
apply (TFold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor. asimpl. done.
- econstructor.
2: { econstructor. }
econstructor. econstructor.
+ econstructor.
apply getValue_type.
apply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
+ asimpl.
econstructor.
* repeat constructor.
* econstructor.
-- apply (TUnfold _ _ (TNodeBody τ (TVar 0))). repeat constructor.
-- econstructor.
++ econstructor.
2: { by constructor. }
repeat econstructor.
repeat econstructor.
repeat econstructor.
++ repeat econstructor.
++ repeat econstructor.
-- repeat econstructor.
Qed.
Lemma MS_dequeue_type Γ τ :
typed (MS_QueueType τ :: Γ) MS_dequeue (TArrow TUnit (TMaybe τ)).
Proof.
econstructor.
econstructor.
{ repeat econstructor. }
econstructor.
{ apply getValue_type.
eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
}
econstructor.
- eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
- repeat econstructor.
- econstructor.
+ econstructor.
2: { econstructor. reflexivity. }
* econstructor.
* econstructor. reflexivity.
* repeat econstructor.
+ repeat econstructor. asimpl. done.
+ repeat econstructor.
Qed.
Lemma MS_queue_type Γ :
typed Γ MS_queue
(TForall (TProd
(TArrow TUnit (TMaybe (TVar 0)))
(TArrow (TVar 0) TUnit)
)
).
Proof.
econstructor.
econstructor.
- econstructor.
apply (TFold _ _ (TNodeBody (TVar 0) (TVar 0))).
repeat econstructor.
- econstructor.
+ repeat econstructor.
+ econstructor.
* repeat econstructor.
* econstructor.
-- apply MS_dequeue_type.
-- apply MS_enqueue_type.
Qed.
End MS_queue_alt.
......@@ -14,7 +14,7 @@ Ltac iExistsN := repeat iExists _.
(* Solve a goal that consists of introducing existentials, framing, and picking branches. *)
Ltac iExistsFrame :=
(repeat iExistsN || iFrame);
(repeat iExistsN || iFrame || iFrame "#");
(done || (iLeft; iExistsFrame) || (iRight; iExistsFrame) || fail "Could not solve goal").
Notation "◓ v" := ((1/2)%Qp, to_agree v) (at level 20).
......@@ -24,6 +24,7 @@ Section common.
Definition noneV := InjLV UnitV.
Definition someV v := InjRV v.
Definition nodeV x out := FoldV (someV (PairV (someV x) (LocV out))).
Definition locO := leibnizO loc.
Definition fracAgreeR : cmraT := prodR fracR (agreeR locO).
......@@ -62,8 +63,8 @@ Section common.
(* Lemmas related to nodes. *)
(* Expresses that ℓ points to a non-nil node. *)
Definition pointsToSome : iProp Σ :=
n x next, ↦ᵢ{-} (LocV n) n ↦ᵢ{-} FoldV (someV (PairV x next)).
Definition pointsToSome toN : iProp Σ :=
n x nOut, toN ↦ᵢ{-} (LocV n) n ↦ᵢ{-} FoldV (someV (PairV x nOut)).
(* Lemmas regarding fractional agreement. *)
......
......@@ -194,7 +194,7 @@ Section logrel.
properness; auto. apply (IHτ (_ :: _)).
- rewrite iter_up; destruct lt_dec as [Hl | Hl]; simpl.
{ by rewrite !lookup_app_l. }
(* FIXME: Ideally we wouldn't have to do this kinf of surgery. *)
(* FIXME: Ideally we wouldn't have to do this kind of surgery. *)
change (bi_ofeO (uPredI (iResUR Σ))) with (uPredO (iResUR Σ)).
rewrite !lookup_app_r; [|lia ..].
case EQ: (x - length Δ1) => [|n]; simpl.
......@@ -212,6 +212,12 @@ Section logrel.
Lemma interp_env_length Δ Γ vvs : Γ * Δ vvs length Γ = length vvs.
Proof. by iIntros "[% ?]". Qed.
Lemma interp_env_empty Δ vvs : [] * Δ vvs vvs = [].
Proof.
iIntros "HΓ".
iDestruct (interp_env_length with "HΓ") as %?. destruct vvs; done.
Qed.
Lemma interp_env_Some_l Δ Γ vvs x τ :
Γ !! x = Some τ Γ * Δ vvs vv, vvs !! x = Some vv τ Δ vv.
Proof.
......
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