### change IntoVal so that it is easier to use in specs

parent bf9fd4f5
 ... ... @@ -32,6 +32,7 @@ Changes in Coq: - `cmra_opM_assoc_L` → `cmra_op_opM_assoc_L` - `cmra_opM_assoc'` → `cmra_opM_opM_assoc` * `namespaces` has been moved to std++. * Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`. ## Iris 3.1.0 (released 2017-12-19) ... ...
 ... ... @@ -82,7 +82,7 @@ Section proof. (λ v (_:()), l ↦ w)%I (λ _ _, #()%V). Proof. iIntros (<-%of_to_val Q Φ) "? AU". wp_let. wp_proj. wp_proj. iIntros (<- Q Φ) "? AU". wp_let. wp_proj. wp_proj. iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj. wp_store. iMod ("Hclose" \$! () with "H↦") as "HΦ". by iApply "HΦ". Qed. ... ... @@ -95,7 +95,7 @@ Section proof. (λ v (_:()), if decide (v = w1) then l ↦ w2 else l ↦ v)%I (λ v _, #(if decide (v = w1) then true else false)%V). Proof. iIntros (<-%of_to_val <-%of_to_val Q Φ) "? AU". wp_let. repeat wp_proj. iIntros (<- <- Q Φ) "? AU". wp_let. repeat wp_proj. iMod (aupd_acc with "AU") as (v) "[H↦ [_ Hclose]]"; first solve_ndisj. destruct (decide (v = w1)) as [Hv|Hv]; [wp_cas_suc|wp_cas_fail]; iMod ("Hclose" \$! () with "H↦") as "HΦ"; by iApply "HΦ". ... ...
 ... ... @@ -21,13 +21,13 @@ Context `{!heapG Σ, !spawnG Σ}. brought together. That is strictly stronger than first stripping a later and then merging them, as demonstrated by [tests/joining_existentials.v]. This is why these are not Texan triples. *) Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ) `{Hef : !IntoVal e (f1,f2)} : Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) e (f1 f2 : val) (Φ : val → iProp Σ) : IntoVal e (f1,f2) → WP f1 #() {{ Ψ1 }} -∗ WP f2 #() {{ Ψ2 }} -∗ (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗ WP par e {{ Φ }}. Proof. apply of_to_val in Hef as <-. iIntros "Hf1 Hf2 HΦ". iIntros (<-) "Hf1 Hf2 HΦ". rewrite /par /=. wp_let. wp_proj. wp_apply (spawn_spec parN with "Hf1"). iIntros (l) "Hl". wp_let. wp_proj. wp_bind (f2 _). ... ...
 ... ... @@ -44,10 +44,11 @@ Global Instance join_handle_ne n l : Proof. solve_proper. Qed. (** The main proofs. *) Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) `{Hef : !IntoVal e f} : Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) : IntoVal e f → {{{ WP f #() {{ Ψ }} }}} spawn e {{{ l, RET #l; join_handle l Ψ }}}. Proof. apply of_to_val in Hef as <-. iIntros (Φ) "Hf HΦ". rewrite /spawn /=. iIntros (<- Φ) "Hf HΦ". rewrite /spawn /=. wp_let. wp_alloc l as "Hl". wp_let. iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done. iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?". ... ...
 ... ... @@ -147,6 +147,9 @@ Qed. Lemma to_val_is_Some e : is_Some (to_val e) → is_Some (heap_lang.to_val (to_expr e)). Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed. Lemma expr_of_val e v : to_val e = Some v → of_val v = W.to_expr e. Proof. intros ?. apply of_to_val, to_val_Some. done. Qed. Fixpoint subst (x : string) (es : expr) (e : expr) : expr := match e with ... ... @@ -217,8 +220,8 @@ Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances. Ltac solve_into_val := match goal with | |- IntoVal ?e ?v => let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v); apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity let e' := W.of_expr e in change (of_val v = W.to_expr e'); apply W.expr_of_val; simpl; unfold W.to_expr; reflexivity end. Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances. ... ...
 ... ... @@ -160,7 +160,7 @@ Section language. (* This is a family of frequent assumptions for PureExec *) Class IntoVal (e : expr Λ) (v : val Λ) := into_val : to_val e = Some v. into_val : of_val v = e. Class AsVal (e : expr Λ) := as_val : is_Some (to_val e). (* There is no instance [IntoVal → AsVal] as often one can solve [AsVal] more ... ...
 ... ... @@ -94,7 +94,7 @@ Proof. iMod (fupd_intro_mask' E2 ∅) as "Hclose"; [set_solver|]. iIntros "!> !>". iMod "Hclose" as "_". iMod "H" as "(\$ & HΦ & \$)". destruct (to_val e2) eqn:?; last by iExFalso. by iApply wp_value. iApply wp_value; last done. by apply of_to_val. Qed. Lemma wp_lift_atomic_step {s E Φ} e1 : ... ...
 ... ... @@ -147,7 +147,7 @@ Section lifting. iNext; iIntros (e2 σ2 efs) "% Hσ". iDestruct ("H" \$! e2 σ2 efs with "[] [Hσ]") as "[HΦ \$]"; [by eauto..|]. destruct (to_val e2) eqn:?; last by iExFalso. by iMod "Hclose"; iApply wp_value; auto using to_of_val. iMod "Hclose"; iApply wp_value; last done. by apply of_to_val. Qed. Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs : ... ...
 ... ... @@ -54,7 +54,7 @@ Proof. iIntros "!>" (e2 σ2 efs) "%". iMod "Hclose" as "_". iMod ("H" \$! e2 σ2 efs with "[#]") as "(\$ & HΦ & \$)"; first by eauto. destruct (to_val e2) eqn:?; last by iExFalso. by iApply twp_value. iApply twp_value; last done. by apply of_to_val. Qed. Lemma twp_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs : ... ...
 ... ... @@ -342,14 +342,14 @@ Global Instance twp_mono' s E e : Proper (pointwise_relation _ (⊢) ==> (⊢)) (@twp Λ Σ _ s E e). Proof. by intros Φ Φ' ?; apply twp_mono. Qed. Lemma twp_value s E Φ e v `{!IntoVal e v} : Φ v -∗ WP e @ s; E [{ Φ }]. Proof. intros; rewrite -(of_to_val e v) //; by apply twp_value'. Qed. Lemma twp_value s E Φ e v : IntoVal e v → Φ v -∗ WP e @ s; E [{ Φ }]. Proof. intros <-. by apply twp_value'. Qed. Lemma twp_value_fupd' s E Φ v : (|={E}=> Φ v) -∗ WP of_val v @ s; E [{ Φ }]. Proof. intros. by rewrite -twp_fupd -twp_value'. Qed. Lemma twp_value_fupd s E Φ e v `{!IntoVal e v} : (|={E}=> Φ v) -∗ WP e @ s; E [{ Φ }]. Proof. intros. rewrite -twp_fupd -twp_value //. Qed. Lemma twp_value_inv s E Φ e v `{!IntoVal e v} : WP e @ s; E [{ Φ }] ={E}=∗ Φ v. Proof. intros; rewrite -(of_to_val e v) //; by apply twp_value_inv'. Qed. Lemma twp_value_fupd s E Φ e v : IntoVal e v → (|={E}=> Φ v) -∗ WP e @ s; E [{ Φ }]. Proof. intros ?. rewrite -twp_fupd -twp_value //. Qed. Lemma twp_value_inv s E Φ e v : IntoVal e v → WP e @ s; E [{ Φ }] ={E}=∗ Φ v. Proof. intros <-. by apply twp_value_inv'. Qed. Lemma twp_frame_l s E e Φ R : R ∗ WP e @ s; E [{ Φ }] -∗ WP e @ s; E [{ v, R ∗ Φ v }]. Proof. iIntros "[? H]". iApply (twp_strong_mono with "H"); auto with iFrame. Qed. ... ...
 ... ... @@ -292,15 +292,15 @@ Global Instance wp_mono' s E e : Proper (pointwise_relation _ (⊢) ==> (⊢)) (@wp Λ Σ _ s E e). Proof. by intros Φ Φ' ?; apply wp_mono. Qed. Lemma wp_value s E Φ e v `{!IntoVal e v} : Φ v ⊢ WP e @ s; E {{ Φ }}. Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed. Lemma wp_value s E Φ e v : IntoVal e v → Φ v ⊢ WP e @ s; E {{ Φ }}. Proof. intros <-. by apply wp_value'. Qed. Lemma wp_value_fupd' s E Φ v : (|={E}=> Φ v) ⊢ WP of_val v @ s; E {{ Φ }}. Proof. intros. by rewrite -wp_fupd -wp_value'. Qed. Lemma wp_value_fupd s E Φ e v `{!IntoVal e v} : (|={E}=> Φ v) ⊢ WP e @ s; E {{ Φ }}. Proof. intros. rewrite -wp_fupd -wp_value //. Qed. Lemma wp_value_inv s E Φ e v `{!IntoVal e v} : WP e @ s; E {{ Φ }} ={E}=∗ Φ v. Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value_inv'. Qed. Lemma wp_value_inv s E Φ e v : IntoVal e v → WP e @ s; E {{ Φ }} ={E}=∗ Φ v. Proof. intros <-. by apply wp_value_inv'. Qed. Lemma wp_frame_l s E e Φ R : R ∗ WP e @ s; E {{ Φ }} ⊢ WP e @ s; E {{ v, R ∗ Φ v }}. Proof. iIntros "[? H]". iApply (wp_strong_mono with "H"); auto with iFrame. Qed. ... ...
• Owner

Interestingly, this change (or rather, https://gitlab.mpi-sws.org/FP/iris-coq/compare/a2dab2fb4959...a4731f4c73b5) made `atomic_heap.v` and `par.v` almost double their compile time:

https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?orgId=1&from=1529316366080&to=1529324554450&var-metric=time&var-project=iris&var-branch=gen_proofmode&var-config=coq-8.8.0&var-group=(.*)

Zooming out shows that this is consistent and not just noise.

However, `heap_lang/lifting.v` (which uses `IntoVal` much more often!) is unaffected. What?!?

Edited by Ralf Jung
• Owner

And here is why:

``````Time rewrite /IntoVal; iIntros (<-). (* Finished transaction in 0.001 secs *)
Undo.
Time iIntros (<-). (* Finished transaction in 2.085 secs *)``````
• Maintainer

In the case of `par`, we are basically performing a rewrite on:

``IntoVal e (f1,f2)``

this thing is not directly an equality, so Coq's rewrite (which is used by the `<-` introduction pattern) somehow first tries to see if it can use this thing as a setoid relation.

If you enable `Typeclasses eauto := debug`, so see its awful attempt.

Edited by Robbert Krebbers
• Maintainer

IMHO, let's revert this whole change. The mount of porting it took to adapt existing developments was also not really worth the effort.

• Owner

Here's the slow TC trace: https://gitlab.mpi-sws.org/snippets/173

The fast one doesn't even trigger TC search.

• Owner

The mount of porting it took to adapt existing developments was also not really worth the effort.

Except that that work is already done.

• Maintainer

Except that that work is already done.

There are surely developments by other people that have not been ported.

Edited by Robbert Krebbers
• Maintainer

The fast one doesn't even trigger TC search.

The problem is, I think, that only `IntoVal e (f1,f2)` can be turned into a relation on the same type, namely `λ v1 v2, IntoVal e (v1, v2)`, whereas for the others, that is not the case.

• Owner

`IntoVal` doesn't even appear in that TC trace so I am wondering what the heck it is doing.

The problem is, I think, that only `IntoVal e (f1,f2)` can be turned into a relation on the same type, namely `λ v1 v2, IntoVal e (v1, v2)`, whereas for the others, that is not the case.

I don't think so, `atomic_heap` also got slower and it only uses `IntoVal e v`.

• Owner

On the other hand, it is looking for something about `rtc`?!???

``````4.1-1.2-2.1-1.1-3.1-2 : (subrelation (bi_entails ==> bi_entails)%signature
(rtc ?Goal0 --> flip ?r)%signature)``````

EDIT: Ah, here

``````Debug: 1.1-1.3-1.1-1.1-1 : (Reflexive ?r)
Debug: 1.1-1.3-1.1-1.1-1: looking for (Reflexive ?r) with backtracking
Debug: 1.1-1.3-1.1-1.1-1.1: simple apply @rtc_reflexive on (Reflexive ?r), 0 subgoal(s)``````

Should `Reflexive` have a `Hint Mode`?

Edited by Ralf Jung
• Owner

``Hint Mode Reflexive ! ! : typeclass_instances.``

The time is down from 2s to 0.4s.

• Owner

Ouch, but there is a use of `setoid_rewrite` which fails with that mode. Wtf.

EDIT: That `setoid_rewrite` indeed uses `rtc` for some intermediate result... that's probably discarded again later. That doesn't seem right.

Edited by Ralf Jung
• Owner

Interestingly,

``Remove Hints rtc_reflexive : typeclass_instances.``

also reduces the time to 0.4s. It then picks `iff_reflexive` instead which doesn't introduce a new evar, which seems to help. It may be worth reducing the priority of `rtc_reflexive`, not just for this case.

Edited by Ralf Jung
• Ralf Jung @jung

mentioned in merge request robbertkrebbers/coq-stdpp!38

·

mentioned in merge request robbertkrebbers/coq-stdpp!38

Toggle commit list
• Owner

https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38 decreased the time the rewrite takes from 2s to 0.38s.

• Maintainer

Good to hear this had an effect, but IMHO these rewrites should take something much closer to 0.

Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!