Commit 77fb65ef authored by Dan Frumin's avatar Dan Frumin

add `dbin_op_eval`

parent d68e6434
......@@ -18,6 +18,9 @@ Section vcg.
| dLitLoc : dloc dbase_lit
| dLitUnknown : base_lit dbase_lit.
Global Instance dlit_decision : EqDecision dbase_lit.
Proof. solve_decision. Defined.
Inductive dval : Type :=
| dLitV : dbase_lit dval
| dValUnknown : val dval.
......@@ -31,6 +34,13 @@ Section vcg.
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.
Inductive wp_expr :=
| Base : iProp Σ wp_expr
| Inhale : dloc (dval wp_expr) wp_expr
......@@ -67,6 +77,74 @@ Section vcg.
| dUnknown mx => mx
end.
Definition dbin_op_eval_int (op : bin_op) (n1 n2 : Z) : dbase_lit :=
match op with
| PlusOp => dLitInt (n1 + n2)
| MinusOp => dLitInt (n1 - n2)
| MultOp => dLitInt (n1 * n2)
| QuotOp => dLitInt (n1 `quot` n2)
| RemOp => dLitInt (n1 `rem` n2)
| AndOp => dLitInt (Z.land n1 n2)
| OrOp => dLitInt (Z.lor n1 n2)
| XorOp => dLitInt (Z.lxor n1 n2)
| ShiftLOp => dLitInt (n1 n2)
| ShiftROp => dLitInt (n1 n2)
| LeOp => dLitBool (bool_decide (n1 n2))
| LtOp => dLitBool (bool_decide (n1 < n2))
| EqOp => dLitBool (bool_decide (n1 = n2))
end.
Lemma dbin_op_eval_int_correct E op n1 n2 :
bin_op_eval_int op n1 n2 = dbase_lit_interp E (dbin_op_eval_int op n1 n2).
Proof. by destruct op. Qed.
Definition dbin_op_eval_bool (op : bin_op) (b1 b2 : bool) : doption 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)))
end.
Lemma dbin_op_eval_bool_correct E op b1 b2 w :
dbin_op_eval_bool op b1 b2 = dSome 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 : list loc) (op : bin_op) (dv1 dv2 : dval) : doption dval :=
match dv1,dv2 with
| 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 (l1 = 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
end
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) = 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 /=. admit. }
{ admit. }
+ simpl. destruct (bin_op_eval op #(dbase_lit_interp E dl1) v2); try by inversion 1.
- simpl. destruct (bin_op_eval op v1 (dval_interp E dv2)); try by inversion 1.
Admitted.
Fixpoint wp_interp (E : list loc) (a : wp_expr) : iProp Σ :=
match a with
| Base Φ => Φ
......@@ -131,6 +209,7 @@ Section vcg.
Class BaseLitQuote (E : list loc) (l : base_lit) (dl : dbase_lit) :=
base_lit_quote : l = dbase_lit_interp E dl.
(** BaseLitQuote for locs *)
Global Instance base_lit_quote_loc E l i :
LocLookup E l i BaseLitQuote E (LitLoc l) (dLitLoc (dLoc i)) | 1.
Proof. by rewrite /LocLookup /BaseLitQuote /= => ->. Qed.
......@@ -139,6 +218,11 @@ Section vcg.
BaseLitQuote E (LitLoc l) (dLitLoc (dLocUnknown l)) | 10.
Proof. done. Qed.
(** BaseLitQuote for constants *)
Global Instance base_lit_quote_int E i :
BaseLitQuote E (LitInt i) (dLitInt i).
Proof. by rewrite /BaseLitQuote /=. Qed.
Global Instance base_lit_quote_default E l :
BaseLitQuote E l (dLitUnknown l) | 1000.
Proof. done. Qed.
......@@ -168,9 +252,11 @@ Section vcg.
Qed.
Global Instance wp_quote_bin_op E op e1 e2 Φ Ψ t :
( dv1, WpQuote E e2 (λ dv2,
IsSome (dUnknown (bin_op_eval op (dval_interp E dv1) (dval_interp E dv2)))
(λ v, Φ (dValUnknown v))) (Ψ dv1))
( dv1, WpQuote E e2
(λ dv2, IsSome (dbin_op_eval E op dv1 dv2) Φ) (Ψ dv1))
(* IsSome (dUnknown (bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))) *)
(* (λ v, Φ (dValUnknown v))) (Ψ dv1)) → *)
WpQuote E e1 Ψ t
WpQuote E (BinOp op e1 e2) Φ t.
Proof.
......@@ -179,7 +265,9 @@ Section vcg.
iDestruct 1 as (dv <-) "H". rewrite He2.
wp_apply (wp_wand with "H"); iIntros (v2).
iDestruct 1 as (dv' <- w ?) "H".
wp_op. iExists (dValUnknown w); auto.
wp_op.
- by apply dbin_op_eval_correct.
- iExists w. auto.
Qed.
Global Instance wp_quote_store E e1 e2 Φ Ψ t :
......@@ -236,18 +324,6 @@ Section vcg.
end
end.
(* Lemma vcg_sound e Φ: *)
(* wp_interp (vcg e (λ v, Base (Φ v))) ⊢ WP e {{v, Φ v}}. *)
(* Proof. *)
(* Admitted. *)
(* Lemma tac_vcg_sound Δ e Φ : *)
(* envs_entails Δ (wp_interp (vcg e (λ v, Base (Φ v)))) → *)
(* envs_entails Δ (WP e {{ Φ }}). *)
(* Proof. *)
(* rewrite /envs_entails. intros. by rewrite - (vcg_sound e Φ). *)
(* Qed. *)
Definition exhale_
(E : list loc) (s : option (nat * dval)) (P : iProp Σ) : iProp Σ :=
match s with
......@@ -319,7 +395,8 @@ Section Tests_vcg.
Proof.
iIntros.
(* --- PROOF BY VCG ---*)
vcg_opt (@nil loc). simpl. eauto.
vcg_opt (@nil loc). simpl.
done.
(* --- PROOF BY WP --- *)
(* wp_op. *)
Qed.
......@@ -330,6 +407,10 @@ Section Tests_vcg.
iIntros "H".
(* --- PROOF BY VCG --- *)
vcg_opt [l]. simpl.
(* ∃ x : val, ⌜bin_op_eval PlusOp #21 #21 = Some x⌝ ∧ ⌜x = #42⌝ *)
(* ∃ v : val, l ↦ v
∗ (∃ x : val, ⌜bin_op_eval PlusOp v #21 = Some x⌝
∧ (l ↦ v -∗ l ↦ #21 ∧ ⌜x = #42⌝)) *)
eauto 42 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. wp_op. eauto. *)
......@@ -350,6 +431,9 @@ Section Tests_vcg.
iIntros "H".
(* --- PROOF BY VCG --- *)
vcg_opt [l]. simpl.
(* ∃ v : val, l ↦ v
∗ (∃ x : val, ⌜bin_op_eval PlusOp v v = Some x⌝
∧ (l ↦ v -∗ ⌜x = #(n + n)⌝ ∧ l ↦ #n)) *)
eauto 17 with iFrame.
(* --- PROOF BY WP --- *)
(* wp_load. wp_load. wp_op. eauto. *)
......@@ -380,19 +464,18 @@ Section Tests_vcg.
(* (* do 2 wp_load. wp_op. eauto with iFrame. *) *)
(* Qed. *)
(* Lemma test7 (l1 l2: loc) (n m: Z) : *)
(* l1 ↦ #n -∗ l2 ↦ #m -∗ WP (!#l1 + !#l2 + !#l1) {{ v, ⌜v = #(n + m)⌝ ∧ l1 ↦ #n ∗ l2 ↦ #m }}. *)
(* Proof. *)
(* iIntros "Hl1 Hl2". *)
(* (* --- PROOF BY VCG --- *) wp_opt_vcg. *)
(* - by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[]. *)
(* - eauto 42 with iFrame. *)
(* iExists l1, #n. iSplit; first done. *)
(* iSplitL "Hl1"; first done. *)
(* eauto 15 with iFrame. *)
(* (* --- PROOF BY WP --- *) *)
(* (* do 2 wp_load. wp_op. eauto with iFrame. *) *)
(* Qed. *)
Lemma test7 (l1 l2: loc) (n m: Z) :
l1 #n - l2 #m - WP (!#l1 + !#l2 + !#l1) {{ v, v = #(n + m + n) l1 #n l2 #m }}.
Proof.
iIntros "Hl1 Hl2".
(* --- PROOF BY VCG --- *)
vcg_opt [l1;l2]. simpl.
iExists #n. iFrame "Hl1".
iIntros "Hl1".
iExists #m.
iFrame "Hl2".
eauto 150 with iFrame.
Qed.
Lemma test8 (l k : loc) (n: Z) :
l #k - k #n - WP (! !#l) {{ v, v = #n }}.
......
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