Merge branch 'master' of gitlab.mpi-sws.org:jihgfee/osiris

theories/channel/proto_channel.v

@@ -52,48 +52,74 @@ Instance: Params (@iProto_message) 3.
 
 Notation "< a > x1 .. xn , 'MSG' v {{ P }}; p" :=
   (iProto_message
-    (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
     a
     (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
   (at level 20, a at level 10, x1 binder, xn binder, v at level 20, P, p at level 200) : proto_scope.
 Notation "< a > x1 .. xn , 'MSG' v ; p" :=
   (iProto_message
-    (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
     a
     (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
   (at level 20, a at level 10, x1 binder, xn binder, v at level 20, p at level 200) : proto_scope.
+Notation "< a > 'MSG' v {{ P }}; p" :=
+  (iProto_message
+    a
+    (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
+  (at level 20, a at level 10, v at level 20, P, p at level 200) : proto_scope.
+Notation "< a > 'MSG' v ; p" :=
+  (iProto_message
+    a
+    (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
+  (at level 20, a at level 10, v at level 20, p at level 200) : proto_scope.
 
 Notation "<!> x1 .. xn , 'MSG' v {{ P }}; p" :=
   (iProto_message
-    (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
     Send
     (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
   (at level 20, x1 binder, xn binder, v at level 20, P, p at level 200) : proto_scope.
 Notation "<!> x1 .. xn , 'MSG' v ; p" :=
   (iProto_message
-    (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
     Send
     (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
   (at level 20, x1 binder, xn binder, v at level 20, p at level 200) : proto_scope.
+Notation "<!> 'MSG' v {{ P }}; p" :=
+  (iProto_message
+    (TT:=TeleO)
+    Send
+    (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
+  (at level 20, v at level 20, P, p at level 200) : proto_scope.
+Notation "<!> 'MSG' v ; p" :=
+  (iProto_message
+    (TT:=TeleO)
+    Send
+    (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
+  (at level 20, v at level 20, p at level 200) : proto_scope.
 
 Notation "<?> x1 .. xn , 'MSG' v {{ P }}; p" :=
   (iProto_message
-    (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
     Receive
     (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, (v%V,P%I,p%proto)) ..))
   (at level 20, x1 binder, xn binder, v at level 20, P, p at level 200) : proto_scope.
 Notation "<?> x1 .. xn , 'MSG' v ; p" :=
   (iProto_message
-    (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
     Receive
     (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
                        λ x1, .. (λ xn, (v%V,True%I,p%proto)) ..))
   (at level 20, x1 binder, xn binder, v at level 20, p at level 200) : proto_scope.
+Notation "<?> 'MSG' v {{ P }}; p" :=
+  (iProto_message
+    Receive
+    (tele_app (TT:=TeleO) (v%V,P%I,p%proto)))
+  (at level 20, v at level 20, P, p at level 200) : proto_scope.
+Notation "<?> 'MSG' v ; p" :=
+  (iProto_message
+    Receive
+    (tele_app (TT:=TeleO) (v%V,True%I,p%proto)))
+  (at level 20, v at level 20, p at level 200) : proto_scope.
 
 Notation "'END'" := iProto_end : proto_scope.
 

theories/examples/list_sort.v

@@ -4,20 +4,14 @@ From iris.heap_lang Require Import proofmode notation.
 From osiris.utils Require Import list.
 
 Definition lmerge : val :=
-  rec: "go" "cmp" "hys" "hzs" :=
-    match: "hys" with
-      NONE => "hzs"
-    | SOME "_" =>
-      match: "hzs" with
-        NONE => "hys"
-      | SOME "_" =>
-        let: "y" := lhead "hys" in
-        let: "z" := lhead "hzs" in
-        if: "cmp" "y" "z"
-        then lcons "y" ("go" "cmp" (ltail "hys") "hzs")
-        else lcons "z" ("go" "cmp" "hys" (ltail "hzs"))
-      end
-    end.
+  rec: "go" "cmp" "ys" "zs" :=
+    if: lisnil "ys" then "zs" else
+    if: lisnil "zs" then "ys" else
+    let: "y" := lhead "ys" in
+    let: "z" := lhead "zs" in
+    if: "cmp" "y" "z"
+    then lcons "y" ("go" "cmp" (ltail "ys") "zs")
+    else lcons "z" ("go" "cmp" "ys" (ltail "zs")).
 
 Definition list_sort_service : val :=
   rec: "go" "c" :=
@@ -70,12 +64,12 @@ Section list_sort.
     {{{ ws, RET val_encode ws; [∗ list] x;v ∈ list_merge R xs1 xs2;ws, I x v }}}.
   Proof.
     iIntros "#Hcmp" (Ψ) "!> [HI1 HI2] HΨ". iLöb as "IH" forall (xs1 xs2 vs1 vs2 Ψ).
-    destruct xs1 as [|x1 xs1], vs1 as [|v1 vs1]; simpl; try done.
-    { wp_lam. wp_pures. iApply "HΨ". by rewrite list_merge_nil_l. }
-    wp_lam; wp_pures.
-    destruct xs2 as [|x2 xs2], vs2 as [|v2 vs2]; simpl; try done.
-    { wp_pures. iApply "HΨ". iFrame. }
-    wp_pures.
+    wp_lam. wp_apply (lisnil_spec (A:=val) with "[//]"); iIntros (_).
+    destruct xs1 as [|x1 xs1], vs1 as [|v1 vs1]; simpl; done || wp_pures.
+    { iApply "HΨ". by rewrite list_merge_nil_l. }
+    wp_apply (lisnil_spec (A:=val) with "[//]"); iIntros (_).
+    destruct xs2 as [|x2 xs2], vs2 as [|v2 vs2]; simpl; done || wp_pures.
+    { iApply "HΨ". iFrame. }
     wp_apply (lhead_spec (A:=val) with "[//]"); iIntros (_).
     wp_apply (lhead_spec (A:=val) with "[//]"); iIntros (_).
     iDestruct "HI1" as "[HI1 HI1']"; iDestruct "HI2" as "[HI2 HI2']".

theories/examples/list_sort_instances.v

@@ -4,45 +4,42 @@ From iris.heap_lang Require Import proofmode notation.
 From osiris.utils Require Import list.
 From osiris.examples Require Import list_sort.
 
+Definition cmpZ : val :=
+  λ: "x" "y", "x" ≤ "y".
+
 Section list_sort_instances.
   Context `{!heapG Σ, !proto_chanG Σ} (N : namespace).
 
   (* Example: Sort of integers *)
-  Definition IZ (x : Z) (v : val) : iProp Σ :=
-    ⌜∃ w, v = LitV $ LitInt w ∧ x = w⌝%I.
-
-  Definition compareZ : val :=
-    λ: "x" "y", "x" ≤ "y".
+  Definition IZ (x : Z) (v : val) : iProp Σ := ⌜v = #x⌝%I.
 
-  Lemma compareZ_spec : cmp_spec IZ (≤) compareZ.
+  Lemma cmpZ_spec : cmp_spec IZ (≤) cmpZ.
   Proof.
-    iIntros (x x' v v' Φ) "!>".
-    iIntros ([[w [-> ->]] [w' [-> ->]]]) "HΦ".
-    wp_lam. wp_pures. iApply "HΦ". eauto 10 with iFrame.
+    rewrite /IZ. iIntros (x x' v v' Φ [-> ->]) "!> HΦ".
+    wp_lam. wp_pures. by iApply "HΦ".
   Qed.
-  
+
   Local Arguments val_encode _ _ !_ /.
 
   Lemma list_sort_client_le_spec l (xs : list Z) :
     {{{ l ↦ val_encode xs }}}
-      list_sort_client compareZ #l
+      list_sort_client cmpZ #l
       {{{ ys, RET #(); ⌜Sorted (≤) ys⌝ ∗ ⌜ ys ≡ₚ xs⌝ ∗ l ↦ val_encode ys }}}.
   Proof.
     assert (∀ zs : list Z, val_encode zs = val_encode (LitV ∘ LitInt <$> zs)) as Henc.
     { intros zs. induction zs; f_equal/=; auto with f_equal. }
     iIntros (Φ) "Hl HΦ".
     iApply (list_sort_client_spec N IZ (≤) _ _ (LitV ∘ LitInt <$> xs) xs with "[] [Hl] [HΦ]").
-    { iApply compareZ_spec. }
+    { iApply cmpZ_spec. }
     { rewrite -Henc. iFrame "Hl".
       iInduction xs as [|x xs] "IH"; csimpl; first by iFrame.
-      iFrame "IH". by iExists x. }
+      by iFrame "IH". }
     iIntros "!>" (ys ws) "(?&?&?&HI)".
     iAssert ⌜ ws = (LitV ∘ LitInt) <$> ys ⌝%I with "[HI]" as %->.
     { iInduction ys as [|y ys] "IH" forall (ws);
       destruct ws as [|w ws]; csimpl; try done.
-      iDestruct "HI" as "[HI1 HI2]"; iDestruct "HI1" as %(?&->&->).
+      iDestruct "HI" as "[-> HI2]".
       by iDestruct ("IH" with "HI2") as %->. }
     rewrite -Henc. iApply ("HΦ" $! ys with "[$]").
   Qed.
-
 End list_sort_instances.

theories/utils/list.v

@@ -14,6 +14,12 @@ Instance list_val_enc `{ValEnc A} : ValEnc (list A) :=
 Definition lnil : val := λ: <>, NONEV.
 Definition lcons : val := λ: "x" "l", SOME ("x", "l").
 
+Definition lisnil : val := λ: "l",
+  match: "l" with
+    SOME "p" => #false
+  | NONE => #true
+  end.
+
 Definition lhead : val := λ: "l",
   match: "l" with
     SOME "p" => Fst "p"
@@ -106,6 +112,12 @@ Lemma lcons_spec x xs :
   {{{ RET val_encode (x :: xs); True }}}.
 Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.
 
+Lemma lisnil_spec xs:
+  {{{ True }}}
+    lisnil (val_encode xs)
+  {{{ RET #(if xs is [] then true else false); True }}}.
+Proof. iIntros (Φ _) "HΦ". wp_lam. destruct xs; wp_pures; by iApply "HΦ". Qed.
+
 Lemma lhead_spec x xs:
   {{{ True }}} lhead (val_encode (x::xs)) {{{ RET val_encode x; True }}}.
 Proof. iIntros (Φ _) "HΦ". wp_lam. wp_pures. by iApply "HΦ". Qed.