Merge branch 'jonas/map_swap_example'

theories/examples/basics.v

@@ -104,6 +104,18 @@ Definition prog_swap_twice : val := λ: <>,
   send "c" #11;; send "c" #11;;
   recv "c" + recv "c".
 
+Definition prog_swap_loop : val := λ: <>,
+  let: "c" := start_chan (λ: "c'",
+    let: "go" :=
+      rec: "go" <> :=
+        let: "x" := recv "c'" in send "c'" ("x" + #2);; "go" #() in
+    "go" #()) in
+  send "c" #18;;
+  send "c" #20;;
+  let: "x1" := recv "c" in
+  let: "x2" := recv "c" in
+  "x1" + "x2".
+
 Section proofs.
 Context `{heapG Σ, chanG Σ}.
 
@@ -171,6 +183,12 @@ Definition prot_swap_twice : iProto Σ :=
    <?> MSG #20;
    <?> MSG #(x+y); END)%proto.
 
+Definition prot_swap_loop : iProto Σ :=
+  (<! (x : Z)> MSG #x;
+   <! (y : Z)> MSG #y;
+   <?> MSG #(x+2);
+   <?> MSG #(y+2); prot_loop)%proto.
+
 (** Specs and proofs of the respective programs *)
 Lemma prog_spec : {{{ True }}} prog #() {{{ RET #42; True }}}.
 Proof.
@@ -318,4 +336,18 @@ Proof.
   - wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
     wp_pures. by iApply "HΦ".
 Qed.
+
+Lemma prog_loop_swap_spec : {{{ True }}} prog_swap_loop #() {{{ RET #42; True }}}.
+Proof.
+  iIntros (Φ) "_ HΦ". wp_lam.
+  wp_apply (start_chan_spec prot_loop); iIntros (c) "Hc".
+  - iAssert (∀ Ψ, WP (rec: "go" <> := let: "x" := recv c in
+      send c ("x" + #2) ;; "go" #())%V #() {{ Ψ }})%I with "[Hc]" as "H".
+    { iIntros (Ψ). iLöb as "IH". wp_recv (x) as "_". wp_send with "[//]".
+      wp_seq. by iApply "IH". }
+    wp_lam. wp_closure. wp_let. iApply "H".
+  - wp_send with "[//]". wp_send with "[//]". wp_recv as "_". wp_recv as "_".
+    wp_pures. by iApply "HΦ".
+Qed.
+
 End proofs.

theories/examples/subprotocols.v

 From actris.channel Require Import proofmode proto channel.
 From actris.logrel Require Import subtyping_rules.
 From iris.proofmode Require Import tactics.
+From actris.utils Require Import llist.
 
 Section basics.
   Context `{heapG Σ, chanG Σ}.
@@ -10,4 +11,33 @@ Section basics.
     (<! (l1 l2 : loc)> MSG (#l1, #l2) {{ l1 ↦ #20 ∗ l2 ↦ #22 }}; END) ⊑
     (<! (l1 : loc)> MSG (#l1, #l2') {{ l1 ↦ #20 }}; END).
   Proof. iIntros "Hl2'" (l1) "Hl1". iExists l1, l2'. by iFrame "Hl1 Hl2'". Qed.
+
+  Section program_reuse.
+    Context {T U R : Type}.
+    Context (IT : T -> val -> iProp Σ).
+    Context (ITR : (T * R) -> val -> iProp Σ).
+    Context (IU : U -> val -> iProp Σ).
+    Context (IUR : (U * R) -> val -> iProp Σ).
+    Context (IR : R -> iProp Σ).
+
+    Axiom HIT : ∀ v t r, ITR (t,r) v -∗ IT t v ∗ IR r.
+    Axiom HIU : ∀ v u r, (IU u v ∗ IR r) -∗ IUR (u,r) v.
+
+    Lemma example :
+      ⊢ (<! (v : val) (t : T)> MSG v {{ IT t v }};
+         <? (w : val) (u : U)> MSG w {{ IU u w }}; END) ⊑
+        (<! (v : val) (t : T) (r: R)> MSG v {{ ITR (t,r) v }};
+         <? (w : val) (u : U)> MSG w {{ IUR (u,r) w }}; END).
+    Proof.
+      iIntros (v t r) "HTR".
+      iDestruct (HIT with "HTR") as "[HT HR]".
+      iExists v, t. iFrame "HT".
+      iModIntro.
+      iIntros (w u) "HU".
+      iDestruct (HIU with "[$HR $HU]") as "HUR".
+      iExists w, u. iFrame "HUR".
+      eauto.
+    Qed.
+  End program_reuse.
+
 End basics.