From 98432a2e8d94fe2439f50ce48f5c4fc0a48cc832 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Mon, 2 Jul 2018 13:31:20 +0200 Subject: [PATCH] Uniform treatment of ML binops and C-level pointer operations --- theories/c_translation/derived.v | 4 +- theories/c_translation/translation.v | 291 +++++++++++++++++---------- theories/lib/locking_heap.v | 2 +- theories/vcgen/dcexpr.v | 28 ++- theories/vcgen/tests/memcpy.v | 54 +++-- theories/vcgen/tests/test.v | 4 +- theories/vcgen/vcgen.v | 94 ++++----- 7 files changed, 292 insertions(+), 185 deletions(-) diff --git a/theories/c_translation/derived.v b/theories/c_translation/derived.v index 558be1f..c0b964c 100644 --- a/theories/c_translation/derived.v +++ b/theories/c_translation/derived.v @@ -58,7 +58,7 @@ Section derived. Lemma awp_bin_op_load_load op (l r : cloc) (v1 v2: val) R Φ : l ↦C v1 -∗ r ↦C v2 -∗ - (l ↦C v1 -∗ r ↦C v2 -∗ ∃ w : val, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w) -∗ + (l ↦C v1 -∗ r ↦C v2 -∗ ∃ w : val, ⌜cbin_op_eval op v1 v2 = Some w⌝ ∧ Φ w) -∗ awp (a_bin_op op (a_load (a_ret (cloc_to_val l))) (a_load (a_ret (cloc_to_val r)))) R Φ. Proof. iIntros "Hl Hr HΦ". @@ -75,7 +75,7 @@ Section derived. l ↦C v -∗ AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗ ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ⌜v1 = cloc_to_val l⌝ ∗ - ∃ w, ⌜bin_op_eval op v v2 = Some w⌝ + ∃ w, ⌜cbin_op_eval op v v2 = Some w⌝ ∗ (l ↦C[LLvl] w -∗ Φ v)) -∗ AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}. Proof. diff --git a/theories/c_translation/translation.v b/theories/c_translation/translation.v index 682b012..61c3d69 100644 --- a/theories/c_translation/translation.v +++ b/theories/c_translation/translation.v @@ -75,30 +75,6 @@ Definition a_un_op (op : un_op) : val := λ: "x", "v" ←ᶜ "x" ;;ᶜ a_ret (UnOp op "v"). -(*Definition a_pre_un_op (op : un_op) : val := λ: "x", - "l" ←ᶜ "x" ;;ᶜ - a_atomic (λ: <>, a_store (a_ret "l") (a_un_op op (∗ᶜ (a_ret "l")))).*) - -Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2", - "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ - a_ret (BinOp op (Fst "vv") (Snd "vv")). -Notation "e1 +ᶜ e2" := (a_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope. -Notation "e1 -ᶜ e2" := (a_bin_op MinusOp e1%E e2%E) (at level 80) : expr_scope. -Notation "e1 *ᶜ e2" := (a_bin_op MultOp e1%E e2%E) (at level 80) : expr_scope. -Notation "e1 ≤ᶜ e2" := (a_bin_op LeOp e1%E e2%E) (at level 80) : expr_scope. -Notation "e1 <ᶜ e2" := (a_bin_op LtOp e1%E e2%E) (at level 80) : expr_scope. -Notation "e1 ==ᶜ e2" := (a_bin_op EqOp e1%E e2%E) (at level 80) : expr_scope. -Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op EqOp e1%E e2%E)) (at level 80): expr_scope. -Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope. - -Definition a_pre_bin_op (op : bin_op) : val := λ: "x" "y", - "lv" ←ᶜ ("x" |||ᶜ "y");;ᶜ - a_atomic (λ: <>, - "ov" ←ᶜ ∗ᶜ (a_ret (Fst "lv"));;ᶜ - a_ret (Fst "lv") =ᶜ a_bin_op op (a_ret "ov") (a_ret (Snd "lv"));;ᶜ - a_ret "ov"). -Notation "e1 +=ᶜ e2" := (a_pre_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope. - (* M () *) (* The eta expansion is used to turn it into a value *) Definition a_seq : val := λ: <>, @@ -135,6 +111,77 @@ Notation "'callᶜ' ( f , a )" := (at level 100, a at level 200, format "'callᶜ' ( f , a )") : expr_scope. +Inductive cbin_op := + | CBinOp : bin_op → cbin_op + | PtrPlusOp : cbin_op + | PtrLtOp : cbin_op. + +(* TODO: move to locking_heap.v ?*) +Definition cloc_add_Z (l : loc) (o : Z) (o' : Z) : option cloc := + match o,o' with + | Z0,Z0 => Some (l, O) + | Z0,Zpos k => Some (l, Pos.to_nat k) + | Zpos k,Z0 => Some (l, Pos.to_nat k) + | Zpos k1,Zpos k2 => Some (l, Pos.to_nat k1 + Pos.to_nat k2)%nat + | _,_ => None + end. + +Lemma cloc_add_Z_spec l o o' cl : + cloc_add_Z l o o' = Some cl → + cl.1 = l ∧ ∃ n n', cl.2 = (n + n')%nat ∧ Z.of_nat n = o ∧ Z.of_nat n' = o'. +Proof. + destruct o as [|o|], o' as [|o'|]; intros; simplify_eq/=; (split; first done). + naive_solver. + - exists 0%nat, (Pos.to_nat o'). eauto using positive_nat_Z. + - exists (Pos.to_nat o),0%nat. eauto using positive_nat_Z. + - exists (Pos.to_nat o),(Pos.to_nat o'). eauto using Pos2Nat.inj_add, positive_nat_Z. +Qed. + +Definition cloc_lt_Z (l1 : loc) (o1 : Z) (l2 : loc) (o2 : Z) : option bool := + match o1,o2 with + | Z0,Z0 => Some false + | Z0,Zpos k => Some (bool_decide (l1 = l2)) + | Zpos k,Z0 => Some false + | Zpos k1,Zpos k2 => Some (bool_decide (l1 = l2) && bool_decide (Pos.to_nat k1 < Pos.to_nat k2)%nat) + | _,_ => None + end. + +Lemma cloc_lt_Z_spec l1 o1 l2 o2 b : + cloc_lt_Z l1 o1 l2 o2 = Some b → + ∃ n1 n2, Z.of_nat n1 = o1 ∧ Z.of_nat n2 = o2 ∧ cloc_lt (l1,n1) (l2,n2) = b. +Proof. + rewrite /cloc_lt /=. + destruct o1 as [|o1|], o2 as [|o2|]; intros; simplify_eq/=. + - exists 0%nat,0%nat. repeat split; try done. + repeat case_bool_decide; try done. inversion H0. + - exists 0%nat, (Pos.to_nat o2). + repeat split; try done; first eauto using positive_nat_Z. + repeat case_bool_decide; try done. exfalso. eauto using Pos2Nat.is_pos. + - exists (Pos.to_nat o1),0%nat. + repeat split; try done; first eauto using positive_nat_Z. + repeat case_bool_decide; try done. exfalso. inversion H0. + - exists (Pos.to_nat o1),(Pos.to_nat o2). + repeat split; eauto using positive_nat_Z. +Qed. + +Definition cbin_op_eval (op : cbin_op) (v1 v2 : val) : option val := + match op with + | CBinOp op' => bin_op_eval op' v1 v2 + | PtrPlusOp => + match v1,v2 with + | (LitV (LitLoc pl),LitV (LitInt po))%V,LitV (LitInt z) => + cloc_to_val <$> cloc_add_Z pl po z + | _, _ => None + end + | PtrLtOp => + match v1,v2 with + | (LitV (LitLoc pl),LitV (LitInt po))%V, + (LitV (LitLoc ql),LitV (LitInt qo))%V => + (LitV ∘ LitBool) <$> cloc_lt_Z pl po ql qo + | _, _ => None + end + end. + Definition a_ptr_add : val := λ: "x" "y", "lo" ←ᶜ ("x" |||ᶜ "y");;ᶜ let: "o'" := Snd (Fst "lo") + Snd "lo" in @@ -145,8 +192,37 @@ Definition a_ptr_lt : val := λ: "x" "y", let: "p" := Fst "pq" in let: "q" := Snd "pq" in if: Fst "p" = Fst "q" then a_ret (Snd "p" < Snd "q") else a_ret #false. -Notation "e1 +∗ᶜ e2" := (a_ptr_add e1%E e2%E) (at level 80) : expr_scope. -Notation "e1 <∗ᶜ e2" := (a_ptr_lt e1%E e2%E) (at level 80) : expr_scope. + +Definition a_bin_op (op : cbin_op) : val := + match op with + | CBinOp op' => + λ: "x1" "x2", + "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ + a_ret (BinOp op' (Fst "vv") (Snd "vv")) + | PtrPlusOp => a_ptr_add + | PtrLtOp => a_ptr_lt + end. + +Notation "e1 +ᶜ e2" := (a_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope. +Notation "e1 -ᶜ e2" := (a_bin_op (CBinOp MinusOp) e1%E e2%E) (at level 80) : expr_scope. +Notation "e1 *ᶜ e2" := (a_bin_op (CBinOp MultOp) e1%E e2%E) (at level 80) : expr_scope. +Notation "e1 ≤ᶜ e2" := (a_bin_op (CBinOp LeOp) e1%E e2%E) (at level 80) : expr_scope. +Notation "e1 <ᶜ e2" := (a_bin_op (CBinOp LtOp) e1%E e2%E) (at level 80) : expr_scope. +Notation "e1 ==ᶜ e2" := (a_bin_op (CBinOp EqOp) e1%E e2%E) (at level 80) : expr_scope. +Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op (CBinOp EqOp) e1%E e2%E)) (at level 80): expr_scope. +Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope. + +Notation "e1 +∗ᶜ e2" := (a_bin_op PtrPlusOp e1%E e2%E) (at level 80) : expr_scope. +Notation "e1 <∗ᶜ e2" := (a_bin_op PtrLtOp e1%E e2%E) (at level 80) : expr_scope. + +Definition a_pre_bin_op (op : cbin_op) : val := λ: "x" "y", + "lv" ←ᶜ ("x" |||ᶜ "y");;ᶜ + a_atomic (λ: <>, + "ov" ←ᶜ ∗ᶜ (a_ret (Fst "lv"));;ᶜ + a_ret (Fst "lv") =ᶜ a_bin_op op (a_ret "ov") (a_ret (Snd "lv"));;ᶜ + a_ret "ov"). +Notation "e1 +=ᶜ e2" := (a_pre_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope. +Notation "e1 +∗=ᶜ e2" := (a_pre_bin_op PtrPlusOp e1%E e2%E) (at level 80) : expr_scope. Section proofs. Context `{amonadG Σ}. @@ -256,82 +332,6 @@ Section proofs. iApply awp_ret. by wp_op. Qed. - (* - Lemma a_pre_un_op_spec R Φ e op : - AWP e @ R {{ vl, R -∗ ∃ l v w, l ↦C v ∗ ⌜vl = #l⌝ - ∗ ⌜un_op_eval op v = Some w⌝ - ∗ (l ↦C[LLvl] w -∗ R ∗ Φ w) }} -∗ - AWP a_pre_un_op op e @ R {{ Φ }}. - Proof. - iIntros "He". rewrite /a_pre_un_op. - awp_apply (a_wp_awp with "He"); iIntros (?) "HΦ"; awp_lam. - iApply awp_bind. iApply (awp_wand with "HΦ"). - iIntros (vl) "H". awp_lam. - iApply awp_atomic. iNext. - iIntros "R". iDestruct ("H" with "R") as (l v w) "(Hl & % & % & HΦ)". - simplify_eq/=. - iExists True%I. rewrite left_id. awp_lam. - iApply (a_store_spec _ _ (λ v', ⌜v' = #l⌝)%I - (λ v', ⌜v' = w⌝ ∗ l ↦C v)%I - with "[] [Hl] [-]"). - - iApply awp_ret. by wp_value_head. - - iApply a_un_op_spec. iApply a_load_spec. - iApply awp_ret. wp_value_head. - iExists _,_; iFrame. iSplit; eauto. - - iNext. iIntros (? ? ->) "[% Hl]". simplify_eq/=. - iExists _,_; iFrame. iSplit; eauto. - iIntros "? _". by iApply "HΦ". - Qed. - *) - - Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) : - AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗ - ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ w, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w) -∗ - AWP a_bin_op op e1 e2 @ R {{ Φ }}. - Proof. - iIntros "H1 H2 HΦ". - awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam. - awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2". awp_lam. - iApply awp_bind. - iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2"). - iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst. - iNext. awp_lam. iApply awp_ret. do 2 wp_proj. - iSpecialize ("HΦ" with "HΨ1 HΨ2"). - iDestruct "HΦ" as (w0) "[% H]". by wp_pure _. - Qed. - - Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op : - AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗ - ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ R -∗ - ∃ cl v w, ⌜ v1 = cloc_to_val cl ⌝ ∧ - cl ↦C v ∗ - ⌜ bin_op_eval op v v2 = Some w ⌝ ∗ - (cl ↦C[LLvl] w -∗ R ∗ Φ v)) -∗ - AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}. - Proof. - iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op. - awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam. - awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam. - iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext. - iIntros (v1 v2) "Hv1 Hv2 !>". awp_let. - iApply awp_atomic. iNext. - iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (cl v w ->) "(Hl & % & HΦ)". - simplify_eq/=. iExists True%I. rewrite left_id. awp_lam. - iApply awp_bind. awp_proj. iApply a_load_spec. iApply awp_ret. wp_value_head. - iExists cl, v; iFrame. iSplit; first done. - iIntros "Hl". awp_let. iApply awp_bind. - iApply (a_store_spec _ _ - (λ v', ⌜v' = cloc_to_val cl⌝)%I (λ v', ⌜v' = w⌝)%I with "[] [] [-]"). - - awp_proj. iApply awp_ret; by wp_value_head. - - iApply (a_bin_op_spec _ _ (λ v', ⌜v' = v⌝)%I (λ v', ⌜v' = v2⌝)%I); - try (try awp_proj; iApply awp_ret; by wp_value_head). - iNext. iIntros (? ? -> ->). eauto. - - iNext. iIntros (? ? -> ->). - iExists _, _; iFrame. iSplit; first done. - iIntros "?". awp_seq. iApply awp_ret; wp_value_head. - iIntros "_". by iApply "HΦ". - Qed. - Lemma a_seq_spec R Φ : U (Φ #()) -∗ AWP (a_seq #()) @ R {{ Φ }}. @@ -497,13 +497,84 @@ Section proofs. do 2 (awp_proj; awp_let). do 2 awp_proj. unfold cloc_lt; simpl. case_bool_decide as Hp; awp_op. - destruct Hp as [-> ?%Nat2Z.inj_lt]. - rewrite bool_decide_true //. awp_if. do 2 awp_proj. - iApply awp_ret. wp_op. rewrite bool_decide_true //. - - apply not_and_l_alt in Hp as [?|[? ->]]. - + rewrite bool_decide_false; last congruence. - awp_if. iApply awp_ret. by iApply wp_value. - + rewrite bool_decide_true //. awp_if. iApply awp_ret. do 2 wp_proj. - wp_op. by rewrite bool_decide_false; last lia. + rewrite (bool_decide_true (LitV pl = LitV pl)) //. awp_if. do 2 awp_proj. + iApply awp_ret. wp_op. + rewrite (bool_decide_iff (pi < qi)%nat (pi < qi)); eauto using Nat2Z.inj_lt. + - rewrite bool_decide_false; last congruence. + awp_if. iApply awp_ret. by iApply wp_value. + Qed. + + Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : cbin_op) (e1 e2: expr) : + AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗ + ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ w, ⌜cbin_op_eval op v1 v2 = Some w⌝ ∧ Φ w) -∗ + AWP a_bin_op op e1 e2 @ R {{ Φ }}. + Proof. + iIntros "H1 H2 HΦ". + destruct op as [op'| |]. + - awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam. + awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2". awp_lam. + iApply awp_bind. + iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2"). + iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst. + iNext. awp_lam. iApply awp_ret. do 2 wp_proj. + iSpecialize ("HΦ" with "HΨ1 HΨ2"). + iDestruct "HΦ" as (w0) "[% H]". by wp_pure _. + - iApply (a_ptr_add_spec with "H2"). + iApply (awp_wand with "H1"). + iIntros (v1) "HΨ1". iNext. + iIntros (v2) "HΨ2". iDestruct ("HΦ" with "HΨ1 HΨ2") as (w hop) "HΦ". + destruct v1 as [ | |v11 v12| |],v2 as [|vl| | |]; simplify_eq/=; + destruct v11 as [|[]| | |],v12 as [|[o| | |]| | |]; simplify_eq/=. + destruct vl as [o'| | |]; simplify_eq/=. + destruct (cloc_add_Z l o o') as [cl|] eqn:Hcl; simplify_eq/=. + apply cloc_add_Z_spec in Hcl. + destruct Hcl as [Hcl1 (n & n' & Hcl2 & Hn & Hn')]. simplify_eq/=. + iExists (cl.1,n), n'. repeat iSplit; eauto. + compute [cloc_add]. simpl. rewrite -Hcl2. iApply "HΦ". + - iApply (a_ptr_lt_spec with "H1"). + iApply (awp_wand with "H2"). + iIntros (v2) "HΨ2". iNext. + iIntros (v1) "HΨ1". iDestruct ("HΦ" with "HΨ1 HΨ2") as (w hop) "HΦ". + simpl in hop. + destruct v1 as [ | |v11 v12| |],v2 as [| |v21 v22 | |]; simplify_eq; + destruct v11 as [|[| | |l1]| | |],v12 as [|[o1| | |]| | |]; simplify_eq. + destruct v21 as [|[| | |l2]| | |],v22 as [|[o2| | |]| | |]; simplify_eq/=. + destruct (cloc_lt_Z l1 o1 l2 o2) as [b|] eqn:Hcl; simplify_eq/=. + apply cloc_lt_Z_spec in Hcl. + destruct Hcl as (n1 & n2 & Hn1 & Hn2 & Hlt). simplify_eq/=. + iExists (l1,n1),(l2,n2). eauto. + Qed. + + Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op : + AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗ + ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ R -∗ + ∃ cl v w, ⌜ v1 = cloc_to_val cl ⌝ ∧ + cl ↦C v ∗ + ⌜ cbin_op_eval op v v2 = Some w ⌝ ∗ + (cl ↦C[LLvl] w -∗ R ∗ Φ v)) -∗ + AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}. + Proof. + iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op. + awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam. + awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam. + iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext. + iIntros (v1 v2) "Hv1 Hv2 !>". awp_let. + iApply awp_atomic. iNext. + iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (cl v w ->) "(Hl & % & HΦ)". + simplify_eq/=. iExists True%I. rewrite left_id. awp_lam. + iApply awp_bind. awp_proj. iApply a_load_spec. iApply awp_ret. wp_value_head. + iExists cl, v; iFrame. iSplit; first done. + iIntros "Hl". awp_let. iApply awp_bind. + iApply (a_store_spec _ _ + (λ v', ⌜v' = cloc_to_val cl⌝)%I (λ v', ⌜v' = w⌝)%I with "[] [] [-]"). + - awp_proj. iApply awp_ret; by wp_value_head. + - iApply (a_bin_op_spec _ _ (λ v', ⌜v' = v⌝)%I (λ v', ⌜v' = v2⌝)%I); + try (try awp_proj; iApply awp_ret; by wp_value_head). + iNext. iIntros (? ? -> ->). eauto. + - iNext. iIntros (? ? -> ->). + iExists _, _; iFrame. iSplit; first done. + iIntros "?". awp_seq. iApply awp_ret; wp_value_head. + iIntros "_". by iApply "HΦ". Qed. Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} : @@ -528,4 +599,4 @@ End proofs. (* Make sure that we only use the provided rules and don't break the abstraction *) Typeclasses Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke. -Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke a_ret. +Global Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke a_ret. diff --git a/theories/lib/locking_heap.v b/theories/lib/locking_heap.v index 7adf9f1..7dae134 100644 --- a/theories/lib/locking_heap.v +++ b/theories/lib/locking_heap.v @@ -92,7 +92,7 @@ Section definitions. (** Pointer arithmetic *) Definition cloc_lt (p q : cloc) : bool := - bool_decide (p.1 = q.1 ∧ p.2 < q.2). + bool_decide (p.1 = q.1) && bool_decide (p.2 < q.2)%nat. Definition cloc_add (cl : cloc) (i : nat) : cloc := (cl.1, cl.2 + i). Definition cloc_to_val (cl : cloc) : val := (#cl.1, #cl.2). diff --git a/theories/vcgen/dcexpr.v b/theories/vcgen/dcexpr.v index 222da92..94a6e2f 100644 --- a/theories/vcgen/dcexpr.v +++ b/theories/vcgen/dcexpr.v @@ -138,6 +138,14 @@ Definition dbin_op_eval | _, _ => dNone end. + +Definition dcbin_op_eval (E: known_locs) (op : cbin_op) (dv1 dv2 : dval) : doption dval := + match op with + | CBinOp op' => dbin_op_eval E op' dv1 dv2 + | PtrPlusOp | PtrLtOp => + dUnknown (dValUnknown <$> cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2)) + end. + Lemma dbin_op_eval_correct E op dv1 dv2 w : doption_interp (dbin_op_eval E op dv1 dv2) = Some w → bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = @@ -170,6 +178,17 @@ Proof. try by inversion 1. Qed. +Lemma dcbin_op_eval_correct E op dv1 dv2 w : + doption_interp (dcbin_op_eval E op dv1 dv2) = Some w → + cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = + Some (dval_interp E w). +Proof. + destruct op as [op'| |]. + - apply dbin_op_eval_correct. + - cbn-[cbin_op_eval]. destruct (cbin_op_eval PtrPlusOp (dval_interp E dv1) (dval_interp E dv2)); naive_solver. + - cbn-[cbin_op_eval]. destruct (cbin_op_eval PtrLtOp (dval_interp E dv1) (dval_interp E dv2)); naive_solver. +Qed. + Definition dun_op_eval (E : known_locs) (op : un_op) (dv : dval) : doption dval := match dv with @@ -206,8 +225,8 @@ Inductive dcexpr : Type := | dCAlloc : dcexpr → dcexpr | dCLoad : dcexpr → dcexpr | dCStore : dcexpr → dcexpr → dcexpr - | dCBinOp : bin_op → dcexpr → dcexpr → dcexpr - | dCPreBinOp : bin_op → dcexpr → dcexpr → dcexpr + | dCBinOp : cbin_op → dcexpr → dcexpr → dcexpr + | dCPreBinOp : cbin_op → dcexpr → dcexpr → dcexpr | dCUnOp : un_op → dcexpr → dcexpr | dCSeq : dcexpr → dcexpr → dcexpr | dCPar : dcexpr → dcexpr → dcexpr @@ -286,6 +305,11 @@ Lemma dbin_op_eval_dSome_wf E dv1 dv2 op dw: dbin_op_eval E op dv1 dv2 = dSome dw → dval_wf E dw. Proof. destruct op, dv1,dv2; simpl; repeat case_match; naive_solver. Qed. +Lemma dcbin_op_eval_dSome_wf E dv1 dv2 op dw: + dval_wf E dv1 → dval_wf E dv2 → + dcbin_op_eval E op dv1 dv2 = dSome dw → dval_wf E dw. +Proof. destruct op; first eauto using dbin_op_eval_dSome_wf; naive_solver. Qed. + (** / Well-foundness of dcexpr w.r.t. known_locs *) Lemma dval_interp_mono (E E': known_locs) (dv: dval) : diff --git a/theories/vcgen/tests/memcpy.v b/theories/vcgen/tests/memcpy.v index 9a640e8..d3e863d 100644 --- a/theories/vcgen/tests/memcpy.v +++ b/theories/vcgen/tests/memcpy.v @@ -18,7 +18,16 @@ Section memcpy. let: "n" := Snd (Snd "arg") in "pend" ←ᶜ ∗ᶜ(a_ret "p") +∗ᶜ (a_ret "n");;ᶜ whileᶜ (∗ᶜ(a_ret "p") <∗ᶜ (a_ret "pend")) - { ((a_ret "p")+=ᶜ♯1) =ᶜ ∗ᶜ((a_ret "q")+=ᶜ♯1) }. + { ((a_ret "p")+∗=ᶜ♯1) =ᶜ ∗ᶜ((a_ret "q")+∗=ᶜ♯1) }. + + (* TODO: move somewhere *) + Lemma cloc_lt_Z_eq l1 (o1 : nat) l2 (o2 : nat) : + cloc_lt_Z l1 o1 l2 o2 = Some (cloc_lt (l1,o1) (l2,o2)). + Proof. Admitted. + + Lemma cloc_add_Z_eq l1 (o1 o2 : nat) : + cloc_add_Z l1 o1 o2 = Some (cloc_add (l1,o1) o2). + Proof. Admitted. Lemma memcpy_body_spec (i: nat) (pp p q : cloc) (n : nat) (ls1 ls2 : list val) R : length ls1 = n → @@ -28,28 +37,25 @@ Section memcpy. q ↦C∗ ls2 -∗ pp ↦C (#p.1, #(p.2+i)%nat) -∗ AWP whileᶜ (∗ᶜ (a_ret (#pp.1, #pp.2)) <∗ᶜ a_ret (#p.1, #(p.2 + n)%nat)) - { (a_ret (#pp.1, #pp.2) +=ᶜ ♯1) =ᶜ ∗ᶜ (a_ret (#q.1, #q.2) +=ᶜ ♯1) } + { (a_ret (#pp.1, #pp.2) +∗=ᶜ ♯1) =ᶜ ∗ᶜ (a_ret (#q.1, #q.2) +∗=ᶜ ♯1) } @ R {{ _, p ↦C∗ ls2 ∗ q ↦C∗ ls2 }}. Proof. iIntros (? ?) "Htake Hp Hq Hpp". iLöb as "IH" forall (i). iDestruct "Htake" as %Htake. iApply a_while_spec'. - iNext. - - iApply (a_ptr_lt_spec _ _ (λ v, ⌜v = (#p.1, #(p.2+i)%nat)%V⌝ ∗ pp ↦C (#p.1, #(p.2+i)%nat))%I with "[Hpp]"). - { vcg_solver. eauto. } - - vcg_solver. iNext. iIntros (?) "[% Hpp]"; simplify_eq/=. - iExists (p.1,p.2+i)%nat,(p.1,p.2+length ls1)%nat; repeat iSplit; eauto. + iNext. vcg_solver. simpl. destruct (decide (i < length ls1)%nat). - - iLeft. iSplit. - { iPureIntro. compute[cloc_lt]. f_equal. simpl. - rewrite bool_decide_true; auto. split; auto. omega. } + - iExists (dValUnknown #true). iSplit. + { iPureIntro. rewrite cloc_lt_Z_eq /= /cloc_lt. do 3 f_equal. simpl. + rewrite !bool_decide_true; auto. omega. } + vcg_continue. iLeft; iSplit; first done. + (* vcg_solver DF: doesnt do anything *) admit. - - iRight. iSplit. - { iPureIntro. compute[cloc_lt]. f_equal. simpl. - rewrite bool_decide_false; auto. intros [? ?]. omega. } - iApply a_seq_spec. iModIntro. + - iExists (dValUnknown #false). iSplit. + { iPureIntro. rewrite cloc_lt_Z_eq /= /cloc_lt. do 3 f_equal. simpl. + rewrite bool_decide_true // bool_decide_false //. omega. } + vcg_continue. iRight; iSplit; first done. + iApply a_seq_spec. iModIntro. simplify_eq/=. assert (ls1 = ls2) as ->. { generalize dependent i. generalize dependent ls2. induction ls1; simpl; eauto. - intros ls2 ->%nil_length_inv. done. @@ -77,11 +83,17 @@ Section memcpy. iNext. iIntros (? ->). iExists 1%nat. iSplit; eauto. iIntros (pp) "[Hpp _]". rewrite {3}/cloc_add. etaprod pp. repeat awp_pure _. iApply awp_bind. - iApply (a_ptr_add_spec _ _ (λ v, ⌜v = #n⌝))%I; first by (iApply awp_ret; wp_value_head). - vcg_solver. iIntros "Hpp". - iNext. iIntros (? ->). iExists p,n; repeat iSplit; eauto. - awp_let. iApply (memcpy_body_spec 0 with "[] Hp Hq [Hpp]"); eauto. - by rewrite Nat.add_0_r. + (* DF: TODO!! if we run vcg_solver here then we loose pp ↦ - + some problem with vcgen for pre_op? + *) + iApply (a_bin_op_spec _ _ (λ v, ⌜v = cloc_to_val p⌝ ∗ pp ↦C (#p.1, #p.2)) (λ v, ⌜v = #n⌝) with "[Hpp]")%I. + - vcg_solver. eauto. + - by vcg_solver. + - iNext. iIntros (? ?) "[% Hpp] %". simplify_eq/=. + iExists (cloc_to_val (p.1,p.2+length ls1))%nat; repeat iSplit; eauto. + { rewrite cloc_add_Z_eq. done. } + awp_let. iApply (memcpy_body_spec 0 with "[] Hp Hq [Hpp]"); eauto. + by rewrite Nat.add_0_r. Qed. End memcpy. diff --git a/theories/vcgen/tests/test.v b/theories/vcgen/tests/test.v index 8ff83ff..6a5e085 100644 --- a/theories/vcgen/tests/test.v +++ b/theories/vcgen/tests/test.v @@ -48,8 +48,8 @@ Section tests_vcg. Lemma test_seq_fail l : l ↦C[ULvl] #0 -∗ - awp (a_bin_op PlusOp (a_bin_op PlusOp (stupid l) (stupid l)) (a_ret #0)) - True (λ v, l ↦C #1). + AWP ((stupid l) +ᶜ (stupid l)) +ᶜ (a_ret #0) @ + True {{ v, l ↦C #1 }}. Proof. iIntros "Hl". vcg_solver. Fail by eauto with iFrame. Abort. diff --git a/theories/vcgen/vcgen.v b/theories/vcgen/vcgen.v index ed01bbf..1fab3fe 100644 --- a/theories/vcgen/vcgen.v +++ b/theories/vcgen/vcgen.v @@ -46,7 +46,7 @@ Section vcg. | dCBinOp op de1 de2 => ''(ms1, mNew1, dv1) ← vcg_sp E ms de1; ''(ms2, mNew2, dv2) ← vcg_sp E ms1 de2; - match dbin_op_eval E op dv1 dv2 with + match dcbin_op_eval E op dv1 dv2 with | dSome dv => Some (ms2, denv_merge mNew1 mNew2, dv) | dNone | dUnknown _ => None end @@ -55,7 +55,7 @@ Section vcg. i ← is_dloc E dl; ''(ms2, mNew2, dv2) ← vcg_sp E ms1 de2; ''(ms3, mNew3, dv) ← denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2); - match dbin_op_eval E op dv dv2 with + match dcbin_op_eval E op dv dv2 with | dSome dv3 => Some (ms3, denv_insert i LLvl 1 dv3 mNew3, dv) | dNone | dUnknown _ => None end @@ -74,7 +74,7 @@ Section vcg. ''(ms1, mNew1, dv1) ← vcg_sp E ms de1; ''(ms2, mNew2, dv2) ← vcg_sp E ms1 de2; Some (ms2, denv_merge mNew1 mNew2, (dPairV dv1 dv2)) - | dCAlloc _ | dCUnknown _ | dCInvoke _ _ => None + | dCAlloc _ | dCUnknown _ | dCInvoke _ _ => None end. Definition vcg_sp' @@ -135,39 +135,39 @@ Section vcg. vcg_wp_continuation E Φ (dval_interp E dv2)))%I end%I. - Definition vcg_wp_bin_op (E : known_locs) (op : bin_op) (dv1 dv2 : dval) + (* DF: the handling of pointer operations is uniform wrt other binary operations, but it doesnt work very well because of the deep embedding of cbin_op_eval *) + Definition vcg_wp_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := - match dbin_op_eval E op dv1 dv2 with + match dcbin_op_eval E op dv1 dv2 with | dSome dw => Φ E m dw | mdw => ∃ dw, ⌜ doption_interp mdw = Some dw ⌝ ∧ - vcg_wp_continuation E Φ (dval_interp E dw) + vcg_wp_continuation E Φ (dval_interp E dw) end%I. - Definition vcg_wp_pre_bin_op (E : known_locs) (op : bin_op) (dv1 dv2 : dval) + Definition vcg_wp_pre_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval) (m : denv) (Φ : known_locs → denv → dval → iProp Σ) : iProp Σ := match is_dloc E dv1 with | Some i => - match denv_delete_full i m with - | Some (m', dw) => - match dbin_op_eval E op dw dv2 with - | dSome dw' => Φ E (denv_insert i LLvl 1 dw' m') dw - | mdw => ∃ dw', ⌜doption_interp mdw = Some dw'⌝ ∧ - mapsto_wand_list E (denv_insert i LLvl 1 dw' m') - (vcg_wp_continuation E Φ (dval_interp E dw)) - end - | None => mapsto_wand_list E m (∃ (v w : val), - dloc_interp E (dLoc i) ↦C v ∗ - ⌜bin_op_eval op v (dval_interp E dv2) = Some w⌝ ∗ - (dloc_interp E (dLoc i) ↦C[LLvl] w -∗ - vcg_wp_continuation E Φ v)) - end + match denv_delete_full i m with + | Some (m', dw) => + match dcbin_op_eval E op dw dv2 with + | dSome dw' => Φ E (denv_insert i LLvl 1 dw' m') dw + | mdw => ∃ dw', ⌜doption_interp mdw = Some dw'⌝ ∧ + mapsto_wand_list E (denv_insert i LLvl 1 dw' m') + (vcg_wp_continuation E Φ (dval_interp E dw)) + end + | None => mapsto_wand_list E m (∃ (v w : val), + dloc_interp E (dLoc i) ↦C v ∗ + ⌜cbin_op_eval op v (dval_interp E dv2) = Some w⌝ ∗ + (dloc_interp E (dLoc i) ↦C[LLvl] w -∗ + vcg_wp_continuation E Φ v)) + end | _ => - mapsto_wand_list E m (∃ (cl : cloc) (v w : val), - ⌜dval_interp E dv1 = cloc_to_val cl⌝ ∗ - cl ↦C v ∗ - ⌜bin_op_eval op v (dval_interp E dv2) = Some w⌝ ∗ - (cl ↦C[LLvl] w -∗ - vcg_wp_continuation E Φ v)) + mapsto_wand_list E m (∃ (cl : cloc) (v w : val), + ⌜dval_interp E dv1 = cloc_to_val cl⌝ ∗ + cl ↦C v ∗ + ⌜cbin_op_eval op v (dval_interp E dv2) = Some w⌝ ∗ + (cl ↦C[LLvl] w -∗ vcg_wp_continuation E Φ v)) end%I. Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr) @@ -295,7 +295,7 @@ Section vcg_spec. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=. - destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=. + destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. transitivity (length ms1); eauto. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hde1; simplify_eq/=. destruct dv1 as [?|?|?|dv1]; try destruct dv1; simplify_eq/=. @@ -304,7 +304,7 @@ Section vcg_spec. simplify_eq/=. destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=. - destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=. + destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. transitivity (length ms1); eauto. transitivity (length ms2); eauto using denv_delete_full_2_length. - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hde; simplify_eq/=. @@ -376,7 +376,7 @@ Section vcg_spec. destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=. specialize (IHde2 ms1). destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=. - destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=. + destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. iPoseProof IHde1 as "Hawp1"; first done. iPoseProof IHde2 as "Hawp2"; first done. iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp". @@ -385,7 +385,7 @@ Section vcg_spec. iApply (a_bin_op_spec with "Hawp1 Hawp2"). iNext. iIntros (? ?) "[% HmNew1] [% HmNew2]"; simplify_eq/=. iExists (dval_interp E dv). repeat iSplit; eauto. - + iPureIntro. apply dbin_op_eval_correct. by rewrite Hboe. + + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe. + rewrite -denv_merge_interp. iFrame. - specialize (IHde1 ms). destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|]; simplify_eq /=. @@ -395,7 +395,7 @@ Section vcg_spec. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|]; simplify_eq /=. destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv'] |] eqn:Hfar; simplify_eq/=. - destruct (dbin_op_eval E b dv' dv2) eqn:Hboe; simplify_eq/=. + destruct (dcbin_op_eval E c dv' dv2) eqn:Hboe; simplify_eq/=. iPoseProof IHde1 as "Hawp1"; first done. iPoseProof IHde2 as "Hawp2"; first done. iPoseProof denv_delete_full_2_interp as "Hl"; first done. @@ -409,7 +409,7 @@ Section vcg_spec. iExists (dloc_interp E (dLoc i)), (dval_interp E dv), (dval_interp E d). iDestruct ("Hl" with "HmNew") as "[HmNew $]". repeat iSplit; eauto. - + iPureIntro. apply dbin_op_eval_correct. by rewrite Hboe. + + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hboe. + iIntros "Hl". iFrame. iSplit; first done. rewrite -denv_insert_interp. by iFrame. - specialize (IHde ms). @@ -516,12 +516,12 @@ Section vcg_spec. simplify_eq/=. destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=. - destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=. + destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). repeat split; eauto. apply denv_wf_merge; eauto. - eapply (dbin_op_eval_dSome_wf _ dv1 dv2); eauto. + eapply (dcbin_op_eval_dSome_wf _ dv1 dv2); eauto. - destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=. destruct dv1 as [|?|d|]; simplify_eq/=. @@ -531,14 +531,14 @@ Section vcg_spec. destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=. apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2]. - destruct (dbin_op_eval E b dv1 dv2) eqn:Hboe; simplify_eq/=. + destruct (dcbin_op_eval E c dv1 dv2) eqn:Hboe; simplify_eq/=. destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1). destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?). eapply denv_wf_delete_full_2 in Hout1; try eassumption. destruct Hout1 as (?&?&?). repeat split; eauto using denv_wf_insert, denv_wf_merge. eapply denv_wf_insert; eauto. - eapply (dbin_op_eval_dSome_wf _ dv dv2); eauto. + eapply (dcbin_op_eval_dSome_wf _ dv dv2); eauto. by eapply denv_wf_merge. - destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=. @@ -627,21 +627,21 @@ Section vcg_spec. denv_interp E m -∗ vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) Φ -∗ denv_interp E mOut -∗ - ∃ w : val, ⌜bin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w⌝ ∧ + ∃ w : val, ⌜cbin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w⌝ ∧ vcg_wp_continuation E Φ w. Proof. iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op. - destruct (dbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin. + destruct (dcbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin. * iDestruct "Hwp" as (dw Hopt) "Hcont"; simplify_eq. * iExists (dval_interp E dw); iSplit. - { iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin. } + { iPureIntro. apply dcbin_op_eval_correct. by rewrite Hbin. } iExists E, dw, (denv_merge mOut m). - apply dbin_op_eval_dSome_wf in Hbin; try done. + apply dcbin_op_eval_dSome_wf in Hbin; try done. rewrite -denv_merge_interp //. eauto with iFrame. * iDestruct "Hwp" as (dw0 Hopt) "Hcont"; simplify_eq. destruct dw as [dw1|] eqn:Hdw; last done. iExists (dval_interp E dw0); iSplit; last done. - iPureIntro. apply dbin_op_eval_correct. by rewrite Hbin. + iPureIntro. apply dcbin_op_eval_correct. by rewrite Hbin. Qed. Lemma vcg_wp_pre_bin_op_correct E m op dv1 dv2 Φ : @@ -650,7 +650,7 @@ Section vcg_spec. denv_interp E m -∗ vcg_wp_pre_bin_op E op dv1 dv2 m Φ -∗ ∃ l v w, l ↦C v ∗ ⌜dval_interp E dv1 = cloc_to_val l⌝ ∗ - ⌜bin_op_eval op v (dval_interp E dv2) = Some w⌝ ∗ + ⌜cbin_op_eval op v (dval_interp E dv2) = Some w⌝ ∗ (l ↦C[LLvl] w -∗ vcg_wp_continuation E Φ v). Proof. iIntros (? ?) "Hm Hwp". rewrite /vcg_wp_pre_bin_op. @@ -665,7 +665,7 @@ Section vcg_spec. iExists (dloc_interp E (dLoc i)),v,w. iFrame. eauto. - iDestruct (denv_delete_full_interp E with "Hm") as "[Hm' Hl]"; first eassumption. - destruct (dbin_op_eval E op dw dv2) as [|dw'|] eqn:Hop. + destruct (dcbin_op_eval E op dw dv2) as [|dw'|] eqn:Hop. { iDestruct "Hwp" as (dw') "[% Hwp]". iExists (dloc_interp E (dLoc i)), (dval_interp E dw), (dval_interp E dw'). iFrame. @@ -675,17 +675,17 @@ Section vcg_spec. { iExists (dloc_interp E (dLoc i)), (dval_interp E dw), (dval_interp E dw'). iFrame. repeat iSplit; eauto; try iPureIntro. - - apply dbin_op_eval_correct. by rewrite Hop. + - apply dcbin_op_eval_correct. by rewrite Hop. - iIntros "Hl". iCombine "Hm' Hl" as "Hm'". rewrite denv_insert_interp. rewrite /vcg_wp_continuation. iExists E,dw,_. iFrame. eapply denv_wf_delete_full in Hdel; eauto. destruct_and!. - apply dbin_op_eval_dSome_wf in Hop; eauto. + apply dcbin_op_eval_dSome_wf in Hop; eauto. repeat iSplit; eauto using denv_wf_insert. } { iDestruct "Hwp" as (dw') "[% Hwp]". iExists (dloc_interp E (dLoc i)), (dval_interp E dw), (dval_interp E dw'). iFrame. repeat iSplit; eauto. - - iPureIntro. apply dbin_op_eval_correct. by rewrite Hop. + - iPureIntro. apply dcbin_op_eval_correct. by rewrite Hop. - iIntros "Hl". iCombine "Hm' Hl" as "Hm'". rewrite denv_insert_interp. rewrite mapsto_wand_list_spec. by iApply "Hwp". } Qed. -- GitLab