Better spec for lock example, and polish

theories/examples/pizza.v

@@ -12,29 +12,30 @@ Section example.
 
   Definition pizza_to_val (p : pizza) :=
     match p with
-    | Margherita => #true
-    | Calzone => #false
+    | Margherita => #0
+    | Calzone => #1
     end.
 
-  Fixpoint list_to_val {T} (f : T -> val) (xs : list T) :=
+  Fixpoint list_to_val {T} (f : T → val) (xs : list T) :=
     match xs with
     | [] => NONEV
-    | x::xs => SOMEV (PairV (f x) (list_to_val f xs))
+    | x::xs => SOMEV ((f x), (list_to_val f xs))%V
     end.
 
-  Definition pizza_list_to_val := list_to_val pizza_to_val.
+  Notation pizza_list_to_val := (list_to_val pizza_to_val).
 
-  Fixpoint is_list {T} (f : T -> val) (v : val) (ws : list T) : iProp Σ :=
+  Fixpoint is_list {T} (f : T → val) (v : val) (ws : list T) : iProp Σ :=
     match ws with
     | []    => ⌜v = NONEV⌝
-    | w::ws => ∃ (v' : val), ⌜v = SOMEV (PairV (f w) v')⌝ ∗ is_list f v' ws
+    | w::ws => ∃ (v' : val), ⌜v = SOMEV ((f w), v')%V⌝ ∗ is_list f v' ws
   end.
 
-  Definition is_int_list : val → list Z → iProp Σ :=
-    is_list (λ v, LitV $ LitInt $ v).
+  Notation is_int_list := (is_list (λ v, LitV $ LitInt $ v)).
+  Notation is_pizza_list := (is_list pizza_to_val).
 
-  Definition is_pizza_list : val → list pizza → iProp Σ :=
-    is_list pizza_to_val.
+  Lemma is_pizza_list_pizzas pizzas :
+    ⊢ is_pizza_list (pizza_list_to_val pizzas) pizzas.
+  Proof. induction pizzas; [eauto | iExists _; eauto]. Qed.
 
   Fixpoint int_list_sum (xs : list Z) : Z :=
     match xs with
@@ -52,7 +53,7 @@ Section example.
   Lemma sum_list_spec v xs :
     {{{ is_int_list v xs }}}
       sum_list v
-    {{{ RET #(int_list_sum xs)%Z; True }}}.
+    {{{ RET #(int_list_sum xs); True }}}.
   Proof.
     unfold is_int_list.
     iIntros (Φ) "Hxs HΦ".
@@ -67,9 +68,9 @@ Section example.
       by iApply "HΦ".
   Qed.
 
-  Definition order_pizza : val :=
+  Definition order_pizza (pizzas : list pizza) : val :=
     λ: "cc" "c",
-    send "c" (pizza_list_to_val [Margherita; Calzone]);;
+    send "c" (pizza_list_to_val pizzas);;
     send "c" "cc";;
     let: "receipt" := recv "c" in
     (sum_list "receipt", !"cc").
@@ -90,17 +91,17 @@ Section example.
     ProtoUnfold pizza_prot (pizza_prot_aux pizza_prot).
   Proof. apply proto_unfold_eq, (fixpoint_unfold _). Qed.
 
-  Lemma order_pizza_spec c cc (x : Z) :
-    {{{ c ↣ pizza_prot ∗ cc ↦ #x }}}
-      order_pizza #cc c
-    {{{ (y x2 : Z), RET PairV #y #x2;
-        c ↣ pizza_prot ∗ cc ↦ #x2 ∗ ⌜x2 = (x - y)%Z⌝ }}}.
+  Lemma order_pizza_spec pizzas c cc (x1 : Z) :
+    {{{ c ↣ pizza_prot ∗ cc ↦ #x1 }}}
+      order_pizza pizzas #cc c
+    {{{ (x2 : Z), RET (#x2, #(x1 - x2))%V;
+        c ↣ pizza_prot ∗ cc ↦ #(x1 - x2)%Z }}}.
   Proof.
     iIntros (Φ) "[Hc Hcc] HΦ".
     wp_lam.
-    wp_send (_ [Margherita; Calzone]) with "[]".
-    { unfold is_pizza_list. simpl. eauto. }
-    wp_send with "[Hcc]"=> //.
+    wp_send (_ pizzas) with "[]".
+    { iApply is_pizza_list_pizzas. }
+    wp_send with "[Hcc //]".
     wp_recv (v2 xs2) as "[Hxs2 [_ Hcc]]".
     wp_load.
     wp_apply (sum_list_spec with "Hxs2").
@@ -111,57 +112,62 @@ Section example.
     eauto with iFrame.
   Qed.
 
-
   Definition lock_example : val :=
-    λ: "c",
+    λ: "jesper_cc" "robbert_cc" "c",
     let: "lk" := newlock #() in
     (
-      (let: "jesper_cc" := ref #0 in
-       acquire "lk";;
-       send "c" (pizza_list_to_val [Margherita]);;
-       send "c" "jesper_cc";;
-       let: "jesper_receipt" := recv "c" in
-       "jesper_receipt")
+      (acquire "lk";;
+       let: "v1" := order_pizza [Margherita] "jesper_cc" "c" in
+       release "lk";;
+       "v1")
       |||
-      (let: "robbert_cc" := ref #0 in
-       acquire "lk";;
-       send "c" (pizza_list_to_val [Calzone]);;
-       send "c" "robbert_cc";;
-       let: "robbert_receipt" := recv "c" in
-       "robbert_receipt")
+      (acquire "lk";;
+       let: "v2" := order_pizza [Calzone] "robbert_cc" "c" in
+       release "lk";;
+       "v2")
     ).
 
-  Lemma lock_example_spec c :
-    {{{ c ↣ pizza_prot }}}
-      lock_example c
-    {{{ v, RET v; True }}}.
+  Lemma lock_example_spec jcc rcc c (x1 y1 : Z) :
+    {{{ c ↣ pizza_prot ∗ jcc ↦ #x1 ∗ rcc ↦ #y1 }}}
+      lock_example #jcc #rcc c
+    {{{ (x2 y2 : Z), RET ((#x2, #(x1 - x2)), (#y2, #(y1 - y2)))%V;
+        jcc ↦ #(x1 - x2) ∗ rcc ↦ #(y1 - y2) }}}.
   Proof.
-    iIntros (Φ) "Hc HΦ".
-    wp_lam.
+    iIntros (Φ) "[Hc [Hjcc Hrcc]] HΦ".
+    wp_lam. wp_pures.
     wp_apply (newlock_spec with "Hc").
     iIntros (lk γ) "#Hlk".
     wp_pures.
-    wp_apply wp_par.
-    - wp_alloc cc as "Hcc".
-      wp_pures.
+    wp_apply (wp_par (λ v, ∃ (x2:Z), ⌜v = (#x2, #(x1 - x2))%V⌝ ∗
+                                     jcc ↦ #(x1 - x2)%Z)%I
+                     (λ v, ∃ (y2:Z), ⌜v = (#y2, #(y1 - y2))%V⌝ ∗
+                                     rcc ↦ #(y1 - y2)%Z)%I
+                with "[Hjcc] [Hrcc]").
+    - wp_pures.
       wp_apply (acquire_spec with "Hlk").
       iIntros "[Hlocked Hc]".
-      wp_send (_ [Margherita]) with "[]".
-      { eauto. }
-      wp_send with "[Hcc]"=> //.
-      wp_recv (v2 xs2) as "[Hxs2 [_ Hcc]]".
-      wp_pures. eauto.
-    - wp_alloc cc as "Hcc".
+      wp_pures. wp_apply (order_pizza_spec with "[$Hc $Hjcc]").
+      iIntros (x2) "[Hc Hjcc]".
+      wp_pures.
+      wp_apply (release_spec with "[$Hlk $Hlocked $Hc]").
+      iIntros "_".
       wp_pures.
+      eauto.
+    - wp_pures.
       wp_apply (acquire_spec with "Hlk").
       iIntros "[Hlocked Hc]".
-      wp_send (_ [Calzone]) with "[]".
-      { eauto. }
-      wp_send with "[Hcc]"=> //.
-      wp_recv (v2 xs2) as "[Hxs2 [_ Hcc]]".
-      wp_pures. eauto.
-    - iIntros (v1 v2) "[_ _]".
-      by iApply "HΦ".
+      wp_pures. wp_apply (order_pizza_spec with "[$Hc $Hrcc]").
+      iIntros (y2) "[Hc Hrcc]".
+      wp_pures.
+      wp_apply (release_spec with "[$Hlk $Hlocked $Hc]").
+      iIntros "_".
+      wp_pures.
+      eauto.
+    - iIntros (v1 v2) "[HΨ1 HΨ2]".
+      iIntros "!>".
+      iDestruct "HΨ1" as (x2) "[-> HΨ1]".
+      iDestruct "HΨ2" as (y2) "[-> HΨ2]".
+      iApply ("HΦ" with "[$HΨ1 $HΨ2]").
   Qed.
 
 End example.