Commit 84d87469 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Kill doption and do some clean up.

parent 166d10aa
......@@ -31,22 +31,6 @@ Inductive dval : Type :=
Global Instance dval_EqDecision : EqDecision dval.
Proof. solve_decision. Defined.
Inductive doption (A : Type) : Type :=
| dNone : doption A
| dSome : A doption A
| dUnknown : option A doption A.
Arguments dNone {_}.
Arguments dSome {_} _.
Arguments dUnknown {_} _.
Global Instance doption_fmap : FMap doption := λ A B f m,
match m with
| dNone => dNone
| dSome x => dSome (f x)
| dUnknown o => dUnknown (f <$> o)
end.
Definition dloc_interp (E : known_locs) (dl : dloc) : cloc :=
match dl with
| dLoc i => default inhabitant (E !! i)
......@@ -69,13 +53,6 @@ Fixpoint dval_interp (E : known_locs) (v : dval) : val :=
| dValUnknown v => v
end.
Fixpoint doption_interp {A} (mx : doption A) : option A :=
match mx with
| dNone => None
| dSome x => Some x
| dUnknown mx => mx
end.
Definition dbin_op_eval_int (op : bin_op) (n1 n2 : Z) : dbase_lit :=
match op with
| PlusOp => dLitInt (n1 + n2)
......@@ -98,158 +75,112 @@ Lemma dbin_op_eval_int_correct E op n1 n2 :
Proof. by destruct op. Qed.
Definition dbin_op_eval_bool
(op : bin_op) (b1 b2 : bool) : doption dbase_lit :=
(op : bin_op) (b1 b2 : bool) : option dbase_lit :=
match op with
| PlusOp | MinusOp | MultOp | QuotOp | RemOp => dNone (* Arithmetic *)
| AndOp => dSome (dLitBool (b1 && b2))
| OrOp => dSome (dLitBool (b1 || b2))
| XorOp => dSome (dLitBool (xorb b1 b2))
| ShiftLOp | ShiftROp => dNone (* Shifts *)
| LeOp | LtOp => dNone (* InEquality *)
| EqOp => dSome (dLitBool (bool_decide (b1 = b2)))
| PlusOp | MinusOp | MultOp | QuotOp | RemOp => None (* Arithmetic *)
| AndOp => Some (dLitBool (b1 && b2))
| OrOp => Some (dLitBool (b1 || b2))
| XorOp => Some (dLitBool (xorb b1 b2))
| ShiftLOp | ShiftROp => None (* Shifts *)
| LeOp | LtOp => None (* InEquality *)
| EqOp => Some (dLitBool (bool_decide (b1 = b2)))
end.
Lemma dbin_op_eval_bool_correct E op b1 b2 w :
dbin_op_eval_bool op b1 b2 = dSome w
dbin_op_eval_bool op b1 b2 = Some w
bin_op_eval_bool op b1 b2 = Some (dbase_lit_interp E w).
Proof. destruct op; simpl; try by inversion 1. Qed.
Definition dbin_op_eval
(E : known_locs) (op : bin_op) (dv1 dv2 : dval) : doption dval :=
(E : known_locs) (op : bin_op) (dv1 dv2 : dval) : option dval :=
match dv1,dv2 with
| dPairV _ _, _ | _, dPairV _ _ => dNone
| dValUnknown _, _ | _,dValUnknown _ =>
dUnknown
(dValUnknown <$> bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
| dLitV l1, dLitV l2 =>
if decide (op = EqOp)
then dSome $ dLitV $ dLitBool
$ bool_decide (dbase_lit_interp E l1 = dbase_lit_interp E l2)
then Some $ dLitV $ dLitBool
$ bool_decide (dbase_lit_interp E l1 = dbase_lit_interp E l2)
else match l1, l2 with
| (dLitInt n1), (dLitInt n2) =>
dSome $ dLitV $ dbin_op_eval_int op n1 n2
| (dLitBool b1), (dLitBool b2) =>
dLitV <$> dbin_op_eval_bool op b1 b2
| dLitUnknown _, _ | _, dLitUnknown _ =>
dUnknown (dValUnknown <$>
bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
| _, _ => dNone
| dLitInt n1, dLitInt n2 => Some $ dLitV $ dbin_op_eval_int op n1 n2
| dLitBool b1, dLitBool b2 => dLitV <$> dbin_op_eval_bool op b1 b2
| _, _ => None
end
| _, _ => dNone
| _, _ => None
end.
Definition dptr_plus_eval (E: known_locs) (dv1 dv2 : dval) : doption dval :=
Definition dptr_plus_eval (E: known_locs) (dv1 dv2 : dval) : option dval :=
match dv1,dv2 with
| dLocV (dLoc i), dLitV (dLitInt o) =>
(* DF: TODO: THIS MAY VERY BLOCK SIMPLIFICATION *)
(* TO PROPERLY HANDLE THIS CASE PLEASE DEEPLY EMBED THE NATURALS *)
match offset_of_val (LitV (LitInt o)) with
| None => dNone
| None => None
| Some n =>
dSome (dLocV (dLocUnknown (cloc_add (dloc_interp E (dLoc i)) n)))
Some $ dLocV $ dLocUnknown $ cloc_add (dloc_interp E (dLoc i)) n
end
| dValUnknown _,dValUnknown _ =>
dUnknown (dValUnknown <$>
cbin_op_eval PtrPlusOp (dval_interp E dv1) (dval_interp E dv2))
| _,_ => dNone
| _,_ => None
end.
Lemma dptr_plus_eval_correct E dv1 dv2 w :
doption_interp (dptr_plus_eval E dv1 dv2) = Some w
cbin_op_eval PtrPlusOp (dval_interp E dv1) (dval_interp E dv2)
= Some (dval_interp E w).
dptr_plus_eval E dv1 dv2 = Some w
cbin_op_eval PtrPlusOp (dval_interp E dv1) (dval_interp E dv2) = Some (dval_interp E w).
Proof.
destruct dv1 as [?|??|[]|u1],dv2 as [[]|??|?|u2]; try naive_solver.
- cbn-[cbin_op_eval]. case_option_guard; inversion 1.
simplify_eq/=. repeat (case_option_guard; last omega).
simpl. repeat f_equal. rewrite Nat2Z.id.
(* TODO: WTF? *)
destruct (default (1%positive, 0%nat) (E !! n)) as [? ?] eqn:lol.
by rewrite lol.
- cbn-[cbin_op_eval].
destruct (cbin_op_eval PtrPlusOp u1 u2) as [w1|] eqn:Hw1;
intros; simplify_eq/=. done.
rewrite /cbin_op_eval /=. case_option_guard; inversion 1.
simplify_eq/=. repeat (case_option_guard; last omega).
simpl. repeat f_equal. rewrite Nat2Z.id.
(* TODO: WTF? *)
destruct (default (1%positive, 0%nat) (E !! n)) as [? ?] eqn:lol.
by rewrite lol.
Qed.
Definition dcbin_op_eval (E: known_locs) (op : cbin_op) (dv1 dv2 : dval) : doption dval :=
Definition dcbin_op_eval (E: known_locs) (op : cbin_op) (dv1 dv2 : dval) : option dval :=
match op with
| CBinOp op' => dbin_op_eval E op' dv1 dv2
| PtrPlusOp => dptr_plus_eval E dv1 dv2
| PtrLtOp =>
dUnknown (dValUnknown <$> cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
| PtrLtOp => None
end.
Lemma dbin_op_eval_correct E op dv1 dv2 w :
doption_interp (dbin_op_eval E op dv1 dv2) = Some w
dbin_op_eval E op dv1 dv2 = Some w
bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) =
Some (dval_interp E w).
Proof.
destruct dv1 as [dl1 | |v1|]=> //.
- destruct dv2 as [dl2 | |v2|]=> //.
+ unfold bin_op_eval. simpl. case_decide; simplify_eq/=.
{ inversion 1. rewrite /bin_op_eval /=. f_equal. simplify_eq /=.
do 2 case_bool_decide; simplify_eq /=; eauto. destruct H0. done. }
{ rewrite /bin_op_eval; intros; destruct dl1, dl2;
rewrite /bin_op_eval_int /bin_op_eval_bool; simplify_eq /=; f_equal;
try (destruct op; done); simpl.
- rewrite /bin_op_eval in H0; case_decide; first done.
destruct b; simplify_eq /=; f_equal.
- destruct op; simplify_eq /=; try done.
- case_decide; first done. destruct b0; simplify_eq /=; f_equal.
destruct op; simplify_eq /=; try done.
- case_decide; first done. destruct b; simplify_eq /=; f_equal.
- case_decide; first done; destruct b; simplify_eq /=; f_equal;
destruct op; simplify_eq /=; try done.
- case_decide; first done; destruct b; simplify_eq /=; f_equal.
- case_decide; first done; destruct b,b0; simplify_eq /=; f_equal.
destruct op; simplify_eq /=; try done. }
+ simpl; destruct (bin_op_eval op #(dbase_lit_interp E dl1) _);
try by inversion 1.
- simpl; destruct (bin_op_eval op _ (dval_interp E dv2)), dv2;
try by inversion 1.
- simpl; destruct (bin_op_eval op _ (dval_interp E dv2)), dv2;
try by inversion 1.
destruct dv2 as [dl2 | |v2|]=> //.
unfold bin_op_eval. simpl. case_decide; simplify_eq/=.
{ inversion 1. rewrite /bin_op_eval /=. f_equal. simplify_eq /=.
do 2 case_bool_decide; simplify_eq /=; eauto. destruct H0. done. }
{ destruct dl1, dl2, op; simpl; intros; simplify_eq/=; auto. }
Qed.
Lemma dcbin_op_eval_correct E op dv1 dv2 w :
doption_interp (dcbin_op_eval E op dv1 dv2) = Some w
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'| |].
destruct op as [op'| |]=> //.
- apply dbin_op_eval_correct.
- apply dptr_plus_eval_correct.
- 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 :=
(E : known_locs) (op : un_op) (dv : dval) : option dval :=
match dv with
| dPairV _ _ => dNone
| dValUnknown _ => dUnknown (dValUnknown <$> un_op_eval op (dval_interp E dv))
| dLitV dl =>
match op, dl with
| NegOp, dLitBool b => dSome $ dLitV $ dLitBool (negb b)
| NegOp, dLitInt n => dSome $ dLitV $ dLitInt (Z.lnot n)
| MinusUnOp, dLitInt n => dSome $ dLitV $ dLitInt (- n)
| _, dLitUnknown l =>
dUnknown (dValUnknown <$> un_op_eval op (dval_interp E dv))
| _,_ => dNone
| NegOp, dLitBool b => Some $ dLitV $ dLitBool (negb b)
| NegOp, dLitInt n => Some $ dLitV $ dLitInt (Z.lnot n)
| MinusUnOp, dLitInt n => Some $ dLitV $ dLitInt (- n)
| _,_ => None
end
| dLocV _ => dNone
| _ => None
end.
Lemma dun_op_eval_correct E op dv w :
doption_interp (dun_op_eval E op dv) = Some w
dun_op_eval E op dv = Some w
un_op_eval op (dval_interp E dv) = Some (dval_interp E w).
Proof.
destruct dv as [dl | |v|]=> //=; last first.
- destruct (un_op_eval op v); simpl; by inversion 1.
- destruct op.
+ destruct dl; simpl; try by inversion 1.
destruct b; by inversion 1.
+ destruct dl; simpl; try by inversion 1.
destruct b; by inversion 1.
destruct dv as [dl | |v|]=> //=.
destruct op, dl; intros; simplify_eq/=; auto.
Qed.
(** DCexpr *)
......@@ -321,24 +252,20 @@ Lemma dcexpr_wf_mono (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_wf E' de.
Proof. induction de; simplify_eq /=; [apply dval_wf_mono|..]; naive_solver. Qed.
Lemma dun_op_eval_dSome_wf E dv u dw:
dval_wf E dv dun_op_eval E u dv = dSome dw dval_wf E dw.
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
Lemma dun_op_eval_dUnknown_wf E dv u w:
dval_wf E dv dun_op_eval E u dv = dUnknown (Some w) dval_wf E w.
Lemma dun_op_eval_Some_wf E dv u dw:
dval_wf E dv dun_op_eval E u dv = Some dw dval_wf E dw.
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
Lemma dbin_op_eval_dSome_wf E dv1 dv2 op dw:
Lemma dbin_op_eval_Some_wf E dv1 dv2 op dw:
dval_wf E dv1 dval_wf E dv2
dbin_op_eval E op dv1 dv2 = dSome dw dval_wf E dw.
dbin_op_eval E op dv1 dv2 = Some 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:
Lemma dcbin_op_eval_Some_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.
dcbin_op_eval E op dv1 dv2 = Some dw dval_wf E dw.
Proof.
destruct op; first eauto using dbin_op_eval_dSome_wf; try naive_solver.
destruct op; first eauto using dbin_op_eval_Some_wf; try naive_solver.
simpl. unfold dptr_plus_eval. repeat case_match; naive_solver.
Qed.
......
......@@ -42,11 +42,11 @@ Section memcpy.
- assert (ls1 = []) as -> by (destruct ls1; naive_solver).
simplify_eq/=. rewrite Nat.add_0_r.
iApply a_while_spec'.
iNext. vcg_solver. iExists #false. iSplit.
iNext. vcg_solver. iIntros "??". iExists #false. iSplit.
{ iPureIntro. case_option_guard; last omega; simpl.
do 3 f_equal. rewrite /cloc_lt.
rewrite bool_decide_true // bool_decide_false //. omega. }
rewrite Qp_half_half. iIntros "? ?".
rewrite Qp_half_half.
vcg_continue. iIntros "Hpp Hqq". iRight. iSplit; first done.
iApply a_seq_spec. iModIntro. simplify_eq/=.
iFrame.
......@@ -57,12 +57,12 @@ Section memcpy.
rewrite {1}/(cloc_add p). etaprod p.
rewrite {1}/(cloc_add q). etaprod q.
iApply a_while_spec'.
iNext. vcg_solver. iExists #true. iSplit.
iNext. vcg_solver. iIntros "????". iExists #true. iSplit.
{ iPureIntro. repeat (case_option_guard; last omega; simpl).
repeat f_equal. rewrite /cloc_lt /=.
rewrite !bool_decide_true; auto. apply Z2Nat.inj_lt; eauto.
apply Nat2Z.inj_lt. omega. }
rewrite Qp_half_half. iIntros "? ? ? ?".
rewrite Qp_half_half.
vcg_continue. iIntros "Hqq Hpp Hw Hy". iLeft; iSplit; first done.
(* TODO: DF: vcgen doesnt do anything here *)
vcg_solver. iIntros "Hy Hw Hpp Hqq".
......
......@@ -46,25 +46,19 @@ Section vcg.
| dCBinOp op de1 de2 =>
''(ms1, mNew1, dv1) vcg_sp E ms de1;
''(ms2, mNew2, dv2) vcg_sp E ms1 de2;
match dcbin_op_eval E op dv1 dv2 with
| dSome dv => Some (ms2, denv_merge mNew1 mNew2, dv)
| dNone | dUnknown _ => None
end
dv dcbin_op_eval E op dv1 dv2;
Some (ms2, denv_merge mNew1 mNew2, dv)
| dCPreBinOp op de1 de2 =>
''(ms1, mNew1, dl) vcg_sp E ms de1;
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 dcbin_op_eval E op dv dv2 with
| dSome dv3 => Some (ms3, denv_insert i LLvl 1 dv3 mNew3, dv)
| dNone | dUnknown _ => None
end
dv3 dcbin_op_eval E op dv dv2;
Some (ms3, denv_insert i LLvl 1 dv3 mNew3, dv)
| dCUnOp op de =>
''(ms1, mNew1, dv) vcg_sp E ms de;
match dun_op_eval E op dv with
| dSome dv' => Some (ms1, mNew1, dv')
| dNone | dUnknown _ => None
end
dv' dun_op_eval E op dv;
Some (ms1, mNew1, dv')
| dCSeq de1 de2 =>
''(ms1, mNew1, _) vcg_sp E ms de1;
''(ms2, mNew2, dv2) vcg_sp E (denv_unlock mNew1 :: ms1) de2;
......@@ -115,10 +109,10 @@ Section vcg.
(dloc_interp E (dLoc i) C[ULvl]{q} dval_interp E (dValUnknown v) -
vcg_wp_continuation E Φ v))
end
| _ =>
mapsto_wand_list E m ( (cl : cloc) q v,
dval_interp E dv = cloc_to_val cl
cl C{q} v (cl C{q} v - vcg_wp_continuation E Φ v))%I
| None =>
mapsto_wand_list E m ( (cl : cloc) q v,
dval_interp E dv = cloc_to_val cl
cl C{q} v (cl C{q} v - vcg_wp_continuation E Φ v))%I
end%I.
Definition vcg_wp_store (E : known_locs) (dv1 dv2 : dval) (m : denv)
......@@ -128,12 +122,12 @@ Section vcg.
match denv_delete_full i m with
| Some (m', dw) => Φ E (denv_insert i LLvl 1 dv2 m') dv2
| None =>
mapsto_wand_list E m ( v : val,
dloc_interp E (dLoc i) C v
(dloc_interp E (dLoc i) C[LLvl] dval_interp E dv2 -
vcg_wp_continuation E Φ (dval_interp E dv2)))
mapsto_wand_list E m ( v : val,
dloc_interp E (dLoc i) C v
(dloc_interp E (dLoc i) C[LLvl] dval_interp E dv2 -
vcg_wp_continuation E Φ (dval_interp E dv2)))
end
| _ =>
| None =>
mapsto_wand_list E m ( (cl : cloc) (v : val),
dval_interp E dv1 = cloc_to_val cl
cl C v
......@@ -145,9 +139,21 @@ Section vcg.
Definition vcg_wp_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval)
(m : denv) (Φ : known_locs denv dval iProp Σ) : iProp Σ :=
match dcbin_op_eval E op dv1 dv2 with
| dSome dw => Φ E m dw
| mdw => v, dval_interp E <$> (doption_interp mdw) = Some v
mapsto_wand_list E m (vcg_wp_continuation E Φ v)
| Some dw => Φ E m dw
| None =>
mapsto_wand_list E m ( v,
cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some v
vcg_wp_continuation E Φ v)
end%I.
Definition vcg_wp_un_op (E : known_locs) (op : un_op) (dv : dval)
(m : denv) (Φ : known_locs denv dval iProp Σ) : iProp Σ :=
match dun_op_eval E op dv with
| Some dw => Φ E m dw
| None =>
mapsto_wand_list E m ( w,
un_op_eval op (dval_interp E dv) = Some w
vcg_wp_continuation E Φ w)
end%I.
Definition vcg_wp_pre_bin_op (E : known_locs) (op : cbin_op) (dv1 dv2 : dval)
......@@ -157,18 +163,19 @@ Section vcg.
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))
| Some dw' => Φ E (denv_insert i LLvl 1 dw' m') dw
| None =>
mapsto_wand_list E m' $ w',
cbin_op_eval op (dval_interp E dw) (dval_interp E dv2) = Some w'
(dloc_interp E (dLoc i) C[LLvl] w' - 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))
| 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
| _ =>
| None =>
mapsto_wand_list E m ( (cl : cloc) (v w : val),
dval_interp E dv1 = cloc_to_val cl
cl C v
......@@ -234,12 +241,7 @@ Section vcg.
| None => vcg_wp_awp_continuation R E de m Φ
end
end
| dCUnOp op de =>
vcg_wp E m de R (λ E m dv,
match dun_op_eval E op dv with
| dSome dw => Φ E m dw
| mdw => dw, doption_interp mdw = Some dw Φ E m dw
end)
| dCUnOp op de => vcg_wp E m de R (λ E m dv, vcg_wp_un_op E op dv m Φ)
| dCSeq de1 de2 =>
vcg_wp E m de1 R (λ E m _,
U (vcg_wp E (denv_unlock m) de2 R Φ))
......@@ -257,8 +259,8 @@ Section vcg.
end
end
| dCInvoke ef de1 => vcg_wp E m de1 R (λ E m dv,
(vcg_wp_awp_continuation R E
(dCUnknown (ef (dval_interp E dv))) m Φ))
vcg_wp_awp_continuation R E
(dCUnknown (ef (dval_interp E dv))) m Φ)
| _ => vcg_wp_awp_continuation R E de m Φ
end%I.
End vcg.
......@@ -545,7 +547,7 @@ Section vcg_spec.
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
repeat split; eauto. apply denv_wf_merge; eauto.
eapply (dcbin_op_eval_dSome_wf _ dv1 dv2); eauto.
eapply (dcbin_op_eval_Some_wf _ dv1 dv2); eauto.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1;
simplify_eq/=.
destruct dv1 as [|?|d|]; simplify_eq/=.
......@@ -562,14 +564,13 @@ Section vcg_spec.
destruct Hout1 as (?&?&?).
repeat split; eauto using denv_wf_insert, denv_wf_merge.
eapply denv_wf_insert; eauto.
eapply (dcbin_op_eval_dSome_wf _ dv dv2); eauto.
eapply (dcbin_op_eval_Some_wf _ dv dv2); eauto.
by eapply denv_wf_merge.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (dun_op_eval E u dv1) as [|?|?] eqn:Hop; simplify_eq/=.
destruct (dun_op_eval E u dv1) as [?|] eqn:Hop; simplify_eq/=.
repeat split; eauto.
eapply dun_op_eval_dSome_wf; eauto.
eapply dun_op_eval_Some_wf; eauto.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq/=.
destruct (vcg_sp E (denv_unlock mNew1 :: ms1) de2)
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq/=.
......@@ -645,6 +646,25 @@ Section vcg_spec.
iExists l, q, v'. iSplit; first done. iFrame.
Qed.
Lemma vcg_wp_un_op_correct E m dv b Φ :
dval_wf E dv
denv_wf E m
denv_interp E m -
vcg_wp_un_op E b dv m Φ -
w : val,
un_op_eval b (dval_interp E dv) = Some w
vcg_wp_continuation E Φ w.
Proof.
iIntros (Hwf Hwf2) "Hm Hwp". rewrite /vcg_wp_un_op.
destruct (dun_op_eval E b dv) as [dw|] eqn:Hbin.
* iExists (dval_interp E dw); iSplit.
{ iPureIntro. apply dun_op_eval_correct. by rewrite Hbin. }
iExists E, dw, m.
apply dun_op_eval_Some_wf in Hbin; try done. eauto with iFrame.
* rewrite mapsto_wand_list_spec.
iDestruct ("Hwp" with "Hm") as (w0 Hopt) "Hcont"; eauto.
Qed.
Lemma vcg_wp_bin_op_correct E0 E m mOut dv1 dv2 b Φ :
E0 `prefix_of` E dval_wf E dv1 dval_wf E dv2
denv_wf E (denv_merge mOut m)
......@@ -656,21 +676,15 @@ Section vcg_spec.
vcg_wp_continuation E Φ w.
Proof.
iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
destruct (dcbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin.
* iDestruct "Hwp" as (dw Hopt) "Hcont"; simplify_eq.
destruct (dcbin_op_eval E b dv1 dv2) as [dw|] eqn:Hbin.
* iExists (dval_interp E dw); iSplit.
{ iPureIntro. apply dcbin_op_eval_correct. by rewrite Hbin. }
iExists E, dw, (denv_merge mOut m).
apply dcbin_op_eval_dSome_wf in Hbin; try done.
apply dcbin_op_eval_Some_wf in Hbin; try done.
rewrite -denv_merge_interp //. eauto with iFrame.
* iDestruct "Hwp" as (w0 Hopt) "Hcont"; simplify_eq.
destruct dw as [dw1|] eqn:Hdw; last done.
iCombine "HmOut Hm" as "Hm". rewrite denv_merge_interp.
rewrite mapsto_wand_list_spec. iSpecialize ("Hcont" with "Hm").
iExists w0; iSplit; last done.
iPureIntro. rewrite -Hbin in Hopt.
destruct (doption_interp (dcbin_op_eval E b dv1 dv2)) as [dw0|] eqn:Hdw0; simplify_eq/=.
apply dcbin_op_eval_correct. by rewrite Hdw0.
* iCombine "HmOut Hm" as "Hm". rewrite denv_merge_interp.
rewrite mapsto_wand_list_spec.
iDestruct ("Hwp" with "Hm") as (w0 Hopt) "Hcont"; eauto.
Qed.
Lemma vcg_wp_pre_bin_op_correct E m op dv1 dv2 Φ :
......@@ -694,32 +708,22 @@ Section vcg_spec.
iExists (dloc_interp E (dLoc i)),v,w. iFrame. eauto.
- iDestruct (denv_delete_full_interp E with "Hm")