From 98da017c4d752289c3b6b6b4c3a254abb88d58c8 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 21 Sep 2020 13:58:39 +0200
Subject: [PATCH] Review comments for compute example
---
theories/logrel/examples/compute_list_par.v | 97 +++++++--------------
1 file changed, 33 insertions(+), 64 deletions(-)
diff --git a/theories/logrel/examples/compute_list_par.v b/theories/logrel/examples/compute_list_par.v
index f6490f7..78a5b79 100644
--- a/theories/logrel/examples/compute_list_par.v
+++ b/theories/logrel/examples/compute_list_par.v
@@ -1,21 +1,19 @@
-From actris.channel Require Import proofmode proto channel.
-From actris.logrel Require Import session_types subtyping_rules
- term_typing_judgment term_typing_rules session_typing_rules
- environments telescopes napp.
+From iris.algebra Require Import frac.
+From iris.heap_lang Require Import metatheory.
From actris.utils Require Import llist.
+From actris.channel Require Import proofmode proto channel.
+From actris.logrel Require Import term_typing_rules session_typing_rules
+ subtyping_rules napp.
From actris.logrel.lib Require Import par_start.
-From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import metatheory.
-From iris.algebra Require Import frac.
Definition cont : Z := 1.
Definition stop : Z := 2.
Definition compute_service : val :=
rec: "go" "c":=
- (branch [cont;stop]) "c"
+ branch [cont;stop] "c"
(λ: "c", let: "v" := recv "c" in
- send "c" ("v" #());; "go" "c")
+ send "c" ("v" #());; "go" "c")
(λ: "c", #()).
Definition send_all_par : val :=
@@ -26,19 +24,21 @@ Definition send_all_par : val :=
acquire "lk";;
select "c" #cont;; send "c" (lpop "xs");;
"counter" <- !"counter"+#1;;
- release "lk";; "go" "c" "xs" "lk" "counter".
+ release "lk";;
+ "go" "c" "xs" "lk" "counter".
Definition recv_all_par : val :=
rec: "go" "c" "ys" "n" "lk" "counter" :=
if: "n" = #0 then #() else
acquire "lk";;
- if: (#0 = !"counter")
- then release "lk";; "go" "c" "ys" "n" "lk" "counter"
+ if: (#0 = !"counter") then
+ release "lk";; "go" "c" "ys" "n" "lk" "counter"
else
let: "x" := recv "c" in
"counter" <- !"counter"-#1;;
release "lk";;
- "go" "c" "ys" ("n"-#1) "lk" "counter";; lcons "x" "ys".
+ "go" "c" "ys" ("n"-#1) "lk" "counter";;
+ lcons "x" "ys".
Definition compute_client : val :=
λ: "xs" "c",
@@ -63,15 +63,15 @@ Section compute_example.
Context `{!inG Σ fracR}.
Definition compute_type_service_aux (rec : lsty Σ) : lsty Σ :=
- lty_branch
- (<[cont := (<?? A> TY () ⊸ A; <!!> TY A ; rec)%lty]>
- (<[stop := END%lty]>∅)).
+ lty_branch $ <[cont := (<?? A> TY () ⊸ A; <!!> TY A ; rec)%lty]> $
+ <[stop := END%lty]> $ ∅.
Instance mapper_type_rec_service_contractive :
Contractive (compute_type_service_aux).
Proof. solve_proto_contractive. Qed.
Definition compute_type_service : lsty Σ :=
lty_rec (compute_type_service_aux).
+ (** This judgement is checked only with the typing rules of the type system *)
Lemma ltyped_compute_service Γ :
⊢ Γ ⊨ compute_service : lty_chan compute_type_service ⊸ () ⫤ Γ.
Proof.
@@ -95,8 +95,7 @@ Section compute_example.
pose proof (ltys_O_inv Ys') as HYs'.
rewrite HYs HYs' /=.
iApply ltyped_seq.
- { iApply (ltyped_send _
- [EnvItem "v" _; EnvItem "c" _; EnvItem "go" _]);
+ { iApply (ltyped_send _ [EnvItem "v" _; EnvItem "c" _; EnvItem "go" _]);
[ done | ].
iApply ltyped_app; [ by iApply ltyped_unit | ]=> /=.
by iApply ltyped_var. }
@@ -116,8 +115,8 @@ Section compute_example.
Qed.
Definition compute_type_client_aux (A : ltty Σ) (rec : lsty Σ) : lsty Σ :=
- lty_select (<[cont := (<!!> TY () ⊸ A; <??> TY A ; rec)%lty]>
- (<[stop := END%lty]>∅)).
+ lty_select $ <[cont := (<!!> TY () ⊸ A; <??> TY A ; rec)%lty]> $
+ <[stop := END%lty]>∅.
Instance compute_type_rec_client_contractive A :
Contractive (compute_type_client_aux A).
Proof. solve_proto_contractive. Qed.
@@ -125,7 +124,7 @@ Section compute_example.
lty_rec (compute_type_client_aux A).
Global Instance compute_type_client_unfold A :
ProtoUnfold (lsty_car (compute_type_client A))
- (lsty_car ((compute_type_client_aux A) (compute_type_client A))).
+ (lsty_car (compute_type_client_aux A (compute_type_client A))).
Proof. apply proto_unfold_eq, (fixpoint_unfold (compute_type_client_aux A)). Qed.
Definition list_pred (A : ltty Σ) : val → val → iProp Σ :=
@@ -167,9 +166,9 @@ Section compute_example.
(<??> TY A ; END)%lty.
Definition compute_type_invariant
- γ (A : ltty Σ) (c : val) counter : iProp Σ :=
- (∃ (n : nat) b,
- ((⌜b = trueâŒ) ∨ (own γ 1%Qp ∗ ⌜b = falseâŒ)) ∗
+ γ (A : ltty Σ) (c : val) (counter : loc) : iProp Σ :=
+ (∃ (n : nat) (b : bool),
+ (if b then True else own γ 1%Qp) ∗
counter ↦ #n ∗
c ↣ (lsty_car (lty_napp (recv_type A) n <++>
(if b then compute_type_client A else END)%lty)))%I.
@@ -250,7 +249,7 @@ Section compute_example.
rewrite /select.
wp_apply (acquire_spec with "Hlk").
iIntros "[Hlocked HI]".
- iDestruct "HI" as (n b) "([-> | [Hf' _]] & Hcounter & Hc)"; last first.
+ iDestruct "HI" as (n [ | ]) "(Hf' & Hcounter & Hc)"; last first.
{ by iDestruct (own_valid_2 with "Hf Hf'") as %[]. }
iDestruct (iProto_mapsto_le with "Hc []") as "Hc".
{ iApply iProto_le_trans.
@@ -264,16 +263,13 @@ Section compute_example.
wp_apply (release_spec with "[-HΦ Hl]").
{ iFrame "Hlk Hlocked".
iExists n, false.
- iSplitL "Hf".
- - iRight. iFrame "Hf". done.
- - rewrite lookup_total_insert.
- rewrite -lsty_car_app lty_app_end_l lty_app_end_r.
- iFrame "Hcounter Hc". }
+ rewrite lookup_total_insert -lsty_car_app lty_app_end_l lty_app_end_r.
+ iFrame "Hf Hcounter Hc". }
iIntros "_". wp_pures. iApply "HΦ". iFrame "Hl Hlk Hsf". }
wp_lam. wp_apply (lisnil_spec with "Hl"); iIntros "Hl".
wp_apply (acquire_spec with "Hlk").
iIntros "[Hlocked HI]".
- iDestruct "HI" as (n b) "([-> | [Hf' _]] & Hcounter & Hc)"; last first.
+ iDestruct "HI" as (n [ | ]) "(Hf' & Hcounter & Hc)"; last first.
{ by iDestruct (own_valid_2 with "Hf Hf'") as %[]. }
iDestruct (iProto_mapsto_le with "Hc []") as "Hc".
{ iApply iProto_le_trans.
@@ -303,7 +299,6 @@ Section compute_example.
rewrite -lty_napp_S_r.
rewrite Nat.add_succ_r.
rewrite -plus_n_O.
- iSplitR; [ by iLeft | ].
replace (Z.of_nat n + 1)%Z with (Z.of_nat (S n)) by lia.
iFrame "Hc Hcounter". }
iIntros "_". wp_pures.
@@ -321,14 +316,14 @@ Section compute_example.
Proof.
iIntros (Φ) "(Hl & #Hlk) HΦ".
iLöb as "IH" forall (n Φ).
- destruct n.
+ destruct n as [ | n ].
{ wp_lam. wp_pures. iApply "HΦ". by iFrame "Hl Hlk". }
wp_lam.
wp_apply (acquire_spec with "Hlk").
iIntros "[Hlocked HI]".
iDestruct "HI" as (m b) "(Hb & Hcounter & Hc)".
wp_load.
- destruct m.
+ destruct m as [ | m ].
{ wp_apply (release_spec with "[$Hlocked $Hlk Hb Hcounter Hc]").
{ iExists 0, b. iFrame "Hb Hcounter Hc". }
iIntros "_". wp_pures. iApply ("IH" with "Hl").
@@ -342,7 +337,7 @@ Section compute_example.
iExists m, b. iFrame "Hb Hcounter Hc". }
iIntros "_".
wp_pures.
- replace ((Z.of_nat (S n)) - 1)%Z with (Z.of_nat (n)) by lia.
+ replace (Z.of_nat (S n) - 1)%Z with (Z.of_nat (n)) by lia.
wp_apply ("IH" with "Hl").
iIntros (ys). iDestruct 1 as (Heq) "(Hl & Hc)".
wp_apply (lcons_spec with "[$Hl $Hw//]").
@@ -377,32 +372,7 @@ Section compute_example.
iApply ltyped_val_lam=> //.
iApply ltyped_post_nil.
iApply (ltyped_lam [EnvItem "xs" _]).
- iIntros "!>" (vs) "HΓ". simpl.
- rewrite (lookup_delete_ne _ "lk" "c")=> //.
- rewrite (lookup_delete_ne _ "lk" "xs")=> //.
- rewrite (lookup_delete_ne _ "lk" "counter")=> //.
- rewrite (lookup_delete_ne _ "lk" "n")=> //.
- rewrite (lookup_delete_ne _ "lk" "ys")=> //.
- rewrite (lookup_delete_ne _ "ys" "c")=> //.
- rewrite (lookup_delete_ne _ "ys" "xs")=> //.
- rewrite (lookup_delete_ne _ "ys" "counter")=> //.
- rewrite (lookup_delete_ne _ "ys" "n")=> //.
- rewrite (lookup_delete_ne _ "counter" "c")=> //.
- rewrite (lookup_delete_ne _ "counter" "xs")=> //.
- rewrite (lookup_delete_ne _ "counter" "n")=> //.
- rewrite (lookup_delete_ne _ "n" "c")=> //.
- rewrite (lookup_delete_ne _ "n" "xs")=> //.
- rewrite (delete_commute _ "lk" "ys")=> //.
- rewrite (lookup_delete_ne _ "ys" "lk")=> //.
- rewrite (delete_commute _ "lk" "counter")=> //.
- rewrite (lookup_delete_ne _ "counter" "lk")=> //.
- rewrite (delete_commute _ "lk" "n")=> //.
- rewrite (lookup_delete_ne _ "n" "lk")=> //.
- rewrite (delete_commute _ "ys" "counter")=> //.
- rewrite (lookup_delete_ne _ "counter" "ys")=> //.
- rewrite (delete_commute _ "counter" "n")=> //.
- rewrite (lookup_delete_ne _ "n" "counter")=> //.
- rewrite !lookup_delete=> //.
+ iIntros "!>" (vs) "HΓ". simplify_map_eq.
iDestruct (env_ltyped_cons _ _ "c" with "HΓ") as (vc ->) "[Hc HΓ]".
iDestruct (env_ltyped_cons _ _ "xs" with "HΓ") as (vlxs ->) "[Hlxs HΓ]".
iDestruct "Hlxs" as (l' v ->) "[Hlxs Hv]".
@@ -415,8 +385,7 @@ Section compute_example.
iMod (own_alloc 1%Qp) as (γf) "Hf"; [ done | ].
wp_apply (newlock_spec (compute_type_invariant γf A vc counter)
with "[Hcounter Hc]").
- { iExists 0, true. simpl. rewrite left_id. iSplitR; [ by iLeft | ].
- iFrame. }
+ { iExists 0, true. repeat rewrite left_id. iFrame "Hcounter Hc". }
iIntros (lk γ) "#Hlk".
wp_apply (par_spec
(λ v, ⌜v = #()âŒ)%I
@@ -431,7 +400,7 @@ Section compute_example.
iDestruct "Hw2" as (ys) "(-> & Hlys)".
iIntros "!>".
wp_pures. iFrame "HΓ".
- by iApply llist_lty_list.
+ by iApply llist_lty_list.
Qed.
Lemma lty_le_compute_type_dual A :
--
GitLab