New approach to sentinel invariant

theories/logrel/F_mu_ref_conc/examples/queue/CG_queue.v

+From Coq.Lists Require Import List.
 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.
@@ -15,9 +16,13 @@ Import uPred.
 
 Definition TMaybe τ := (TSum TUnit τ).
 
-Definition nil := Fold (InjL Unit).
+Definition Nil := Fold (InjL Unit).
 Definition cons val tail := Fold (InjR (Pair val tail)).
 
+Definition none := InjL Unit.
+Definition noneV := InjLV UnitV.
+Definition someV v := InjRV v.
+
 Definition TListBody τ v := TMaybe (TProd τ.[ren (+1)] v).
 Definition TList τ := TRec (TListBody τ (TVar 0)).
 Definition CG_QueueType τ := Tref (TList τ).
@@ -45,8 +50,8 @@ Definition CG_enqueue_body head :=
           (Rec (* try(c) *)
              (Case
                 (Var 1 (* c *)) (* Check the current element *)
-                (* c = nil. We've arrived at the end of the list *)
-                (cons (Var 3 (* x *)) nil)
+                (* c = Nil. We've arrived at the end of the list *)
+                (cons (Var 3 (* x *)) Nil)
                 (* c = cons ... The next element is a cons *)
                 (cons (Fst (Var 0)) (App (Var 1 (* try *)) (Unfold (Snd (Var 0 (* c *)))))
                 )
@@ -64,7 +69,7 @@ Definition CG_queue : expr :=
     (LetIn
        (* lock = *) newlock
        (LetIn
-          (* head = *) (Alloc nil) (* Allocate nil *)
+          (* head = *) (Alloc Nil) (* Allocate nil *)
           (Pair (CG_dequeue (Var 0) (Var 1)) (CG_enqueue (Var 0) (Var 1)))
        )
     ).
@@ -167,6 +172,136 @@ Section CG_queue.
   (*   iApply wp_pure_step_later; auto. iNext. *)
   (* Abort. *)
 
+  (* Representation predicate for the course grained queue. *)
+  Fixpoint isCGQueue_go (xs : list val) : val :=
+    match xs with
+    | nil => FoldV noneV
+    | x :: xs' => FoldV (InjRV (PairV x (isCGQueue_go xs')))
+    end.
+
+  Definition isCGQueue (ℓ : loc) (xs : list val) : iProp Σ :=
+    ℓ ↦ₛ (isCGQueue_go xs).
+
+    Lemma steps_CG_dequeue_cons E j K x xs ℓ ℓlock :
+    nclose specN ⊆ E →
+    spec_ctx ∗ j ⤇ fill K (App (CG_dequeue (Loc ℓ) (Loc ℓlock)) Unit)
+             ∗ isCGQueue ℓ (x :: xs)
+             ∗ ℓlock ↦ₛ (#♭v false)
+             ⊢ |={E}=> j ⤇ fill K (InjR (of_val x))
+                         ∗ isCGQueue ℓ (xs)
+                         ∗ ℓlock ↦ₛ (#♭v false).
+  Proof.
+    iIntros (HNE) "(#spec & Hj & isQueue & lofal)".
+    rewrite /isCGQueue /CG_dequeue. simpl.
+    iMod (steps_with_lock _ _ _ _ _ (ℓ ↦ₛ FoldV (InjRV (PairV x _)))%I
+                          _ (InjRV x) UnitV
+            with "[$Hj $isQueue $lofal]") as "Hj"; eauto.
+    iIntros (K') "(#Hspec & isQueue & Hj)".
+    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
+    iMod (step_load _ _ (UnfoldCtx :: CaseCtx _ _ :: K')  with "[Hj $isQueue]")
+      as "[Hj isQueue]"; eauto.
+    simpl.
+    iMod (do_step_pure _ _ (CaseCtx _ _ :: K') with "[$Hj]") as "Hj"; eauto.
+    simpl.
+    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
+    simpl.
+    iMod (do_step_pure _ _ (StoreRCtx (LocV _) :: SeqCtx _ :: K') with "[$Hj]") as "Hj"; eauto.
+    simpl.
+    iMod (step_store _ _ (SeqCtx _ :: K') with "[$Hj $isQueue]") as "[Hj isQueue]"; eauto.
+    { rewrite /= !to_of_val //. }
+    simpl.
+    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
+    iMod (do_step_pure _ _ (InjRCtx :: K') with "[$Hj]") as "Hj"; eauto.
+    iModIntro. iFrame.
+  Qed.
+
+  Lemma steps_CG_dequeue_nil E j K ℓ ℓlock :
+    nclose specN ⊆ E →
+    spec_ctx ∗ j ⤇ fill K (App (CG_dequeue (Loc ℓ) (Loc ℓlock)) Unit)
+             ∗ isCGQueue ℓ []
+             ∗ ℓlock ↦ₛ (#♭v false)
+             ⊢ |={E}=> j ⤇ fill K (none)
+                         ∗ isCGQueue ℓ []
+                         ∗ ℓlock ↦ₛ (#♭v false).
+  Proof.
+    iIntros (HNE) "(#spec & Hj & isQueue & lofal)".
+    rewrite /isCGQueue /CG_dequeue. simpl.
+    iMod (steps_with_lock _ _ _ _ _ (ℓ ↦ₛ FoldV (noneV))%I
+                          _ (noneV) UnitV
+            with "[$Hj $isQueue $lofal]") as "Hj"; eauto.
+    iIntros (K') "(#Hspec & isQueue & Hj)".
+    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
+    iMod (step_load _ _ (UnfoldCtx :: CaseCtx _ _ :: K')  with "[Hj $isQueue]")
+      as "[Hj isQueue]"; eauto.
+    simpl.
+    iMod (do_step_pure _ _ (CaseCtx _ _ :: K') with "[$Hj]") as "Hj"; eauto.
+    simpl.
+    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
+    simpl.
+    iModIntro. iFrame.
+  Qed.
+
+  Definition inner x xs := (App
+                 (Rec
+                    (Case (ids 1)
+                       (Fold
+                          (InjR
+                             (Pair (of_val x).[ren (+3)] (Fold (InjL Unit)))))
+                       (Fold
+                          (InjR
+                             (Pair (Fst (ids 0))
+                                (App (ids 1) (Unfold (Snd (ids 0)))))))))
+                 (Unfold (of_val (isCGQueue_go xs)))).
+
+  Lemma steps_CG_enqueue_body E j K x xs :
+    nclose specN ⊆ E →
+    spec_ctx ∗ j ⤇ fill K (inner x xs)
+             ⊢ |={E}=> j ⤇ fill K (of_val (isCGQueue_go (xs ++ [x]))).
+  Proof.
+    iIntros (HNE) "(#spec & Hj)".
+    iInduction xs as [|x' xs'] "IH" forall (K).
+    - rewrite /inner. simpl.
+      iMod (do_step_pure _ _ (AppRCtx (RecV _) :: K) with "[$Hj]") as "Hj"; eauto.
+      simpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; eauto.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl.
+      iModIntro. iFrame.
+    - rewrite /inner. simpl.
+      iMod (do_step_pure _ _ (AppRCtx (RecV _) :: K) with "[$Hj]") as "Hj"; eauto.
+      simpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl.
+      iMod (do_step_pure _ _ (PairLCtx _ :: InjRCtx :: FoldCtx :: K) with "[$Hj]") as "Hj"; eauto.
+      simpl.
+      iMod (do_step_pure _ _ (UnfoldCtx :: AppRCtx (RecV _) :: PairRCtx _ :: InjRCtx :: FoldCtx :: K) with "[$Hj]") as "Hj"; eauto.
+      simpl.
+      iMod ("IH" $! (PairRCtx _ :: InjRCtx :: FoldCtx :: K) with "[$Hj]") as "Hj"; eauto.
+  Qed.
+
+  Lemma steps_CG_enqueue E j K x xs ℓ ℓlock :
+    nclose specN ⊆ E →
+    spec_ctx ∗ j ⤇ fill K (App (CG_enqueue (Loc ℓ) (Loc ℓlock)) (of_val x))
+             ∗ isCGQueue ℓ (xs)
+             ∗ ℓlock ↦ₛ (#♭v false)
+             ⊢ |={E}=> j ⤇ fill K (Unit)
+                         ∗ isCGQueue ℓ (xs ++ [x])
+                         ∗ ℓlock ↦ₛ (#♭v false).
+  Proof.
+    iIntros (HNE) "(#spec & Hj & isQueue & lofal)".
+    iMod (steps_with_lock _ _ _ _ _ (isCGQueue _ _)
+                          _ UnitV x
+            with "[$Hj $isQueue $lofal]") as "Hj"; eauto.
+    iIntros (K') "(#Hspec & isQueue & Hj)".
+    iMod (do_step_pure with "[$Hj]") as "Hj"; eauto. iAsimpl.
+    rewrite /isCGQueue.
+    iMod (step_load _ _ (UnfoldCtx :: AppRCtx (RecV _) :: StoreRCtx (LocV _) :: K')  with "[Hj $isQueue]")
+      as "[Hj isQueue]"; eauto.
+    simpl.
+    iMod (steps_CG_enqueue_body _ j (StoreRCtx (LocV _) :: K') with "[$Hj]") as "Hj"; eauto.
+    iMod (step_store _ j K' with "[$Hj isQueue]") as "[Hj Hx]"; eauto.
+    { rewrite /= !to_of_val //. }
+    iModIntro. iFrame.
+  Qed.
 End CG_queue.
 
 Hint Rewrite CG_dequeue_body_subst : autosubst.