Commit bf3aca9a authored by Dan Frumin's avatar Dan Frumin

Strengthen `related_bind`

We define a stronger rule `related_bind_up`, in which there is a baked
in semantic type `R`. The idea here is that we don't actually require
the expressions that we bind to have the same syntactic type.

```
  {E;R::Δ;⤉Γ} ⊨ e1 ≤log≤ e2 : τ
∗ (∀ vv, ⟦ τ ⟧ (R::Δ) vv -∗ {E;Δ;Γ} ⊨ K[v1] ≤log≤ K'[v2] : τ')
____________________________________________________________
  {E;Δ;Γ} ⊨ K[e1] ≤log≤ K'[e2] : τ'
```

We can then use `bin_log_related_weaken_2` to prove the original
binding rule.

The advantages of the new rule is that it allows us to prove the
following compatibility rule for seq:

```
{E;(R::Δ);⤉Γ} ⊨ e1 ≤log≤ e1' : τ1 -∗
{E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ2 -∗
{E;Δ;Γ} ⊨ (e1;; e2) ≤log≤ (e1';; e2') : τ2.
```

The idea here is that we can also pick any *semantic* type to related
e1 and e1'. For instance, if both e1 and e1' are expressions of type
Nat then it is not necessarily the case that we can relate them at
that type -- they might reduce to two different numerals -- but
it *should* be the case that we can relate their effects, if it makes
sense. E.g.

((#l <- #1;; #0) ;; e) ≤ ((#l <- #1;; #1) ;; e)
parent 751f6d75
......@@ -77,7 +77,7 @@ Section refinement.
rel_arrow.
iIntros "!#" (f1 f2) "#Hf".
rel_let_l; rel_let_r.
iApply bin_log_related_seq; auto.
iApply bin_log_related_seq'; auto.
- iApply (bin_log_related_app with "Hf").
iApply bin_log_related_unit.
- rel_load_l_atomic;
......
......@@ -24,7 +24,7 @@ Section refinement.
iMod (inv_alloc (nroot.@"xinv") _ (x ↦ᵢ #1)%I with "Hx") as "#Hinv".
iApply bin_log_related_rec; auto.
iAlways. cbn.
iApply (bin_log_related_seq); auto.
iApply (bin_log_related_seq'); auto.
- iApply bin_log_related_app; last by iApply bin_log_related_unit.
iApply bin_log_related_var.
apply lookup_insert.
......@@ -51,7 +51,7 @@ Section refinement.
iApply bin_log_related_arrow; auto.
iIntros "!#" (f1 f2) "Hf".
rel_let_l. rel_let_r.
iApply (bin_log_related_seq with "[Hf]"); auto.
iApply (bin_log_related_seq' with "[Hf]"); auto.
- iApply (bin_log_related_app with "Hf").
by rel_vals.
- rel_load_l_atomic.
......@@ -112,7 +112,7 @@ Section refinement.
- iMod (shoot γ with "Hp") as "#Hs".
iMod ("Hcl" with "[$Hy Hx]") as "_".
{ iNext. iRight. by iFrame. }
iApply (bin_log_related_seq with "[Hf]"); auto.
iApply (bin_log_related_seq' with "[Hf]"); auto.
+ iApply (bin_log_related_app with "Hf").
by rel_vals.
+ rel_load_l_atomic.
......@@ -126,7 +126,7 @@ Section refinement.
iApply bin_log_related_nat.
- iMod ("Hcl" with "[$Hy Hx]") as "_".
{ iNext. iRight. by iFrame. }
iApply (bin_log_related_seq with "[Hf]"); auto.
iApply (bin_log_related_seq' with "[Hf]"); auto.
+ iApply (bin_log_related_app with "Hf").
by rel_vals.
+ rel_load_l_atomic.
......@@ -163,7 +163,7 @@ Section refinement.
- iMod (shoot γ with "Hp") as "#Hs".
iMod ("Hcl" with "[Hx]") as "_".
{ iNext. iRight. by iFrame. }
iApply (bin_log_related_seq with "[Hf]"); auto.
iApply (bin_log_related_seq' with "[Hf]"); auto.
+ iApply (bin_log_related_app with "Hf").
rel_finish.
+ iInv shootN as "[[>Hx >Hp] | [>Hx _]]" "Hcl";
......@@ -174,7 +174,7 @@ Section refinement.
rel_finish.
- iMod ("Hcl" with "[Hx]") as "_".
{ iNext. iRight. by iFrame. }
iApply (bin_log_related_seq with "[Hf]"); auto.
iApply (bin_log_related_seq' with "[Hf]"); auto.
+ iApply (bin_log_related_app with "Hf").
rel_finish.
+ iInv shootN as "[[>Hx >Hp] | [>Hx _]]" "Hcl";
......@@ -243,7 +243,7 @@ Section refinement.
rel_load_r. rel_let_r.
iMod ("Hcl" with "[Hb Hb']") as "_".
{ iNext. iRight. iFrame. }
iApply (bin_log_related_seq with "[Hf]"); auto.
iApply (bin_log_related_seq' with "[Hf]"); auto.
{ iApply (bin_log_related_app with "Hf").
iApply bin_log_related_unit. }
rel_load_l.
......@@ -298,15 +298,15 @@ Section refinement.
iIntros "Hlocked". iDestruct 1 as (n m) "[Hx Hy]".
rel_seq_l.
rel_store_l. rel_seq_l.
iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit with "[Hf]"); auto.
iApply (bin_log_related_seq' _ _ _ _ _ _ _ TUnit with "[Hf]"); auto.
{ iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hf]").
iApply (related_ret ). iApply interp_ret; eauto using to_of_val.
iApply bin_log_related_val; eauto using to_of_val.
iApply bin_log_related_unit. }
rel_store_l. rel_seq_l.
rel_store_r. rel_seq_r.
iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit with "[Hf]"); auto.
iApply (bin_log_related_seq' _ _ _ _ _ _ _ TUnit with "[Hf]"); auto.
{ iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hf]").
iApply (related_ret ). iApply interp_ret; eauto using to_of_val.
iApply bin_log_related_val; eauto using to_of_val.
iApply bin_log_related_unit. }
rel_load_l.
rel_let_l.
......@@ -344,7 +344,7 @@ Section refinement.
rel_alloc_l as y "Hy". rel_let_l.
rel_alloc_r as x' "Hx'". rel_let_r.
rel_alloc_r as y' "Hy'". rel_let_r.
iApply (bin_log_related_seq with "[Hf]"); eauto.
iApply (bin_log_related_seq' with "[Hf]"); eauto.
{ iApply (bin_log_related_app with "Hf").
iApply bin_log_related_unit. }
rel_load_l. rel_load_r.
......@@ -372,6 +372,26 @@ Section refinement.
( (n : nat),
(c1 ↦ᵢ #n c2 ↦ₛ #n pending γ)
(c1 ↦ᵢ #(S n) c2 ↦ₛ #n shot γ own γ' (Excl ())))%I.
Program Definition TRV : D := λne _, True%I.
Lemma bin_log_related_FG_increment_r Δ Γ K E1 E2 t τ (x : loc) (n : nat) :
nclose specN E1
(x ↦ₛ # n -
(x ↦ₛ # (S n) -
({E1,E2;Δ;Γ} t log fill K #() : τ)) -
{E1,E2;Δ;Γ} t log fill K ((FG_increment $/ (LitV (Loc x))) #()) : τ)%I.
Proof.
iIntros (?) "Hx Hlog".
unlock FG_increment. simpl_subst/=.
rel_rec_r.
rel_load_r.
rel_rec_r. rel_op_r.
rel_cas_suc_r.
rel_if_r.
by iApply "Hlog".
Qed.
Lemma profiled_g `{oneshotG Σ} `{inG Σ (exclR unitR)} γ γ' c1 c2 g1 g2 Δ Γ :
inv shootN (i6 c1 c2 γ γ') -
τg Δ (g1, g2) -
......@@ -381,9 +401,9 @@ Section refinement.
(FG_increment #c2 #() ;; g2 #()) : TUnit.
Proof.
iIntros "#Hinv #Hg".
iApply (bin_log_related_seq); auto; last first.
iApply (bin_log_related_seq _ TRV _ _ _ _ _ _ (TVar 0)); auto; last first.
{ iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit).
iApply (related_ret ). iApply interp_ret; eauto using to_of_val.
iApply bin_log_related_val; eauto using to_of_val.
iApply bin_log_related_unit. }
rel_rec_l.
rel_apply_l (bin_log_FG_increment_logatomic _
......@@ -401,27 +421,18 @@ Section refinement.
rewrite minus_Sn_m // /= -minus_n_O.
iFrame. }
{ iIntros (m) "[Hc1 Hc] _".
iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
- unlock FG_increment. simpl.
rel_rec_r. rel_rec_r.
rel_load_r. rel_rec_r.
rel_op_r.
rel_cas_suc_r.
rel_if_r.
iMod ("Hcl" with "[-]") as "_".
iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]";
rel_rec_r;
(rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj);
iIntros "Hc2".
- iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists (S m). iFrame. iLeft; iFrame. }
iApply bin_log_related_unit.
- unlock FG_increment. simpl.
rel_rec_r. rel_rec_r.
rel_load_r. rel_rec_r.
rel_op_r.
rel_cas_suc_r.
rel_if_r.
iMod ("Hcl" with "[-]") as "_".
rel_finish.
- iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists m.
rewrite minus_Sn_m // /= -minus_n_O.
iFrame. iRight; iFrame. }
iApply bin_log_related_unit. }
rel_finish. }
- iSplitL "Hc2 Ht".
{ rewrite /= -minus_n_O. iRight. iFrame.
iDestruct "Ht" as "[$ $]".
......@@ -434,27 +445,18 @@ Section refinement.
rewrite minus_Sn_m // /= -minus_n_O.
iFrame. }
{ iIntros (m) "[Hc1 Hc] _".
iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]".
- unlock FG_increment. simpl.
rel_rec_r. rel_rec_r.
rel_load_r. rel_rec_r.
rel_op_r.
rel_cas_suc_r.
rel_if_r.
iMod ("Hcl" with "[-]") as "_".
iDestruct "Hc" as "[[Hc2 Ht] | [Hc2 [Ht [Ht' %]]]]";
rel_rec_r;
(rel_apply_r (bin_log_related_FG_increment_r with "Hc2"); first solve_ndisj);
iIntros "Hc2".
- iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists (S m). iFrame. iLeft; iFrame. }
iApply bin_log_related_unit.
- unlock FG_increment. simpl.
rel_rec_r. rel_rec_r.
rel_load_r. rel_rec_r.
rel_op_r.
rel_cas_suc_r.
rel_if_r.
iMod ("Hcl" with "[-]") as "_".
rel_finish.
- iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists m.
rewrite minus_Sn_m // /= -minus_n_O.
iFrame. iRight; iFrame. }
iApply bin_log_related_unit. }
rel_finish. }
Qed.
Lemma profiled_g' `{oneshotG Σ} `{inG Σ (exclR unitR)} γ γ' c1 c2 g1 g2 Δ Γ :
......@@ -506,14 +508,14 @@ Section refinement.
iMod (shoot γ with "Hp") as "#Hs".
iMod ("Hcl" with "[-]") as "_".
{ iNext. iExists m. iRight. iFrame. done. }
iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
iApply (bin_log_related_seq' _ _ _ _ _ _ _ TUnit); auto.
{ iApply (bin_log_related_app _ _ _ _ _ _ _ TUnit TUnit with "[Hg]").
iApply (related_ret ). iApply interp_ret; eauto using to_of_val.
iApply bin_log_related_val; eauto using to_of_val.
iApply bin_log_related_unit. }
iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
iApply (bin_log_related_seq' _ _ _ _ _ _ _ TUnit); auto.
{ iApply (bin_log_related_app _ _ _ _ _ _ _ τg TUnit with "[Hf]").
iApply (related_ret ). iApply interp_ret; eauto using to_of_val.
by iApply profiled_g'. }
iApply bin_log_related_val; eauto using to_of_val.
by iApply profiled_g'. }
rel_seq_l. rel_seq_r.
rel_load_l_atomic. clear m.
iInv shootN as (m) ">[(Hc1 & Hc2 & Ht) | (Hc1 & Hc2 & Ht & Ht')]" "Hcl";
......@@ -566,10 +568,10 @@ Section refinement.
rel_let_l. rel_let_r.
rel_proj_l. rel_proj_r.
rel_let_l. rel_let_r.
iApply (bin_log_related_seq _ _ _ _ _ _ _ TUnit); auto.
iApply (bin_log_related_seq' _ _ _ _ _ _ _ TUnit); auto.
{ iApply (bin_log_related_app _ _ _ _ _ _ _ τg TUnit with "[Hf]").
iApply (related_ret ). iApply interp_ret; eauto using to_of_val.
iApply profiled_g'; eauto. }
iApply bin_log_related_val; eauto using to_of_val.
by iApply profiled_g'. }
rel_seq_l.
rel_bind_l (FG_increment _). rel_rec_l.
rel_apply_l (bin_log_FG_increment_logatomic _
......
......@@ -197,22 +197,33 @@ Section masked.
iApply ("Ht" with "Hj").
Qed.
Lemma bin_log_related_seq Δ Γ e1 e2 e1' e2' τ1 τ2 `{Closed e2} `{Closed e2'} :
Lemma bin_log_related_seq R Δ Γ e1 e2 e1' e2' τ1 τ2 `{Closed e2} `{Closed e2'} :
logrelN E
{E;Δ;Γ} e1 log e1' : τ1 -
{E;(R::Δ);Γ} e1 log e1' : τ1 -
{E;Δ;Γ} e2 log e2' : τ2 -
{E;Δ;Γ} (e1;; e2) log (e1';; e2') : τ2.
Proof.
iIntros (?) "He1 He2".
rel_bind_l e1.
rel_bind_r e1'.
iApply (related_bind with "He1 [He2]").
iApply (related_bind_up _ _ R with "He1 [He2]").
iIntros (?) "? /=".
rel_rec_l.
rel_rec_r.
done.
Qed.
Lemma bin_log_related_seq' Δ Γ e1 e2 e1' e2' τ1 τ2 `{Closed e2} `{Closed e2'} :
logrelN E
{E;Δ;Γ} e1 log e1' : τ1 -
{E;Δ;Γ} e2 log e2' : τ2 -
{E;Δ;Γ} (e1;; e2) log (e1';; e2') : τ2.
Proof.
iIntros (?) "He1 He2".
iApply (bin_log_related_seq (λne _, True%I) _ _ _ _ _ _ τ1.[ren (+1)] with "[He1]"); auto.
by iApply bin_log_related_weaken_2.
Qed.
Lemma bin_log_related_injl Δ Γ e e' τ1 τ2 :
logrelN E
{E;Δ;Γ} e log e' : τ1 -
......
......@@ -248,16 +248,17 @@ Section monadic.
by iMod ("Hτ" with "Hj") as "Hτ".
Qed.
Lemma related_bind E Δ Γ (e1 e2 : expr) (τ τ' : type) (K K' : list ectx_item) :
({E;Δ;Γ} e1 log e2 : τ) -
( vv, τ Δ vv - {E;Δ;Γ} fill K (of_val (vv.1)) log fill K' (of_val (vv.2)) : τ') -
Lemma related_bind_up E Δ R Γ (e1 e2 : expr) (τ τ' : type) (K K' : list ectx_item) :
({E;R::Δ;Γ} e1 log e2 : τ) -
( vv, τ (R::Δ) vv - {E;Δ;Γ} fill K (of_val (vv.1)) log fill K' (of_val (vv.2)) : τ') -
({E;Δ;Γ} fill K e1 log fill K' e2 : τ').
Proof.
iIntros "Hm Hf".
rewrite bin_log_related_eq /bin_log_related_def.
iIntros (vvs ρ) "#Hs #HΓ".
iIntros (j L) "Hj /=".
iSpecialize ("Hm" with "Hs HΓ").
iSpecialize ("Hm" with "Hs [HΓ]").
{ by rewrite interp_env_ren. }
rewrite /env_subst !fill_subst -fill_app.
iMod ("Hm" with "Hj") as "Hm /=".
iModIntro.
......@@ -272,8 +273,9 @@ Section monadic.
rewrite -!fill_subst.
iApply fupd_wp. iApply (fupd_mask_mono E); eauto.
iMod ("Hf" with "Hvv Hs HΓ Hj") as "Hf /=".
done.
by rewrite fill_subst Closed_subst_p_id.
Qed.
End monadic.
Typeclasses Opaque interp_env.
......@@ -88,7 +88,19 @@ Section properties.
Qed.
(** ** Monadic rules *)
(* TODO this is not actually primitive; insert the monadic rules here *)
Lemma related_bind E Δ Γ (e1 e2 : expr) (τ τ' : type) (K K' : list ectx_item) :
({E;Δ;Γ} e1 log e2 : τ) -
( vv, τ Δ vv - {E;Δ;Γ} fill K (of_val (vv.1)) log fill K' (of_val (vv.2)) : τ') -
({E;Δ;Γ} fill K e1 log fill K' e2 : τ').
Proof.
iIntros "Hm Hf".
iApply (related_bind_up _ _ (λne _, True%I) _ _ _ (τ.[ren (+1)]) with "[Hm] [Hf]").
- iApply (bin_log_related_weaken_2 with "Hm").
- iIntros (vv) "Hvv /=".
rewrite -interp_ren.
by iApply "Hf".
Qed.
Lemma bin_log_related_val Δ Γ E e e' τ v v' :
to_val e = Some v
to_val e' = Some v'
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment