Commit 1ab5c71b authored by Léon Gondelman's avatar Léon Gondelman
Browse files

delete heap_lang_vcgen

parent 719be114
From iris.heap_lang Require Export proofmode notation.
From iris.bi Require Import big_op.
Inductive dloc :=
| dLoc : nat dloc
| dLocUnknown : loc dloc.
Global Instance dloc_decision : EqDecision dloc.
Proof. solve_decision. Defined.
Inductive dbase_lit : Type :=
| dLitInt : Z dbase_lit
| dLitBool : bool dbase_lit
| dLitUnit : dbase_lit
| 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.
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 : list loc) (dl : dloc) : loc :=
match dl with
| dLoc i => from_option id inhabitant (E !! i)
| dLocUnknown l => l
end.
Definition dbase_lit_interp (E : list loc) (l : dbase_lit) : base_lit :=
match l with
| dLitInt x => LitInt x
| dLitBool b => LitBool b
| dLitUnit => LitUnit
| dLitLoc dl => LitLoc (dloc_interp E dl)
| dLitUnknown l => l
end.
Definition dval_interp (E : list loc) (v : dval) : val :=
match v with
| dLitV l => LitV (dbase_lit_interp E l)
| 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)
| 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 (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
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 /=. 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; 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) v2);
try by inversion 1.
- simpl; destruct (bin_op_eval op v1 (dval_interp E dv2));
try by inversion 1.
Qed.
From iris.heap_lang Require Export proofmode notation.
From iris.bi Require Import big_op.
From iris_c Require Import dval vcgen.
Hint Extern 50 (WpQuote _ _ _ _) =>
notypeclasses refine (wp_quote_value _ _ _ _ _) : typeclass_instances.
Ltac vcg_opt :=
eapply tac_vcg_opt_list_sound;
[ apply _
| compute; reflexivity
| apply _
| apply _
| simpl ].
Section Tests_vcg.
Context `{heapG Σ}.
Lemma test1: WP #21 + #21 {{ v, v = #42 }}%I.
Proof. iIntros. vcg_opt. try eauto with iFrame. Qed.
Lemma test2 (l: loc) :
l #21 - WP (!#l + #21) {{ v, l #21 v = #42}}.
Proof. iIntros. vcg_opt. try eauto with iFrame. Qed.
Lemma test3 (l: loc) (n: Z) :
l #n - WP (#l <- !#l + #1) {{ _, l #(n + 1) }}.
Proof. iIntros. vcg_opt. simpl. try eauto with iFrame. Qed.
Lemma test4 (l: loc) (n: Z) :
l #n - WP (!#l + !#l) {{ v, v = #(n + n) l #n }}.
Proof. iIntros. vcg_opt. try eauto with iFrame. Qed.
Lemma test5 (l1 l2: loc) (n m: Z) :
l1 #n - l2 #m - WP (!#l1 + !#l2 + !#l1 + !#l2) {{ _, l1 #n l2 #m }}.
Proof. iIntros. vcg_opt. try eauto with iFrame. Qed.
Lemma test6 (l k : loc) (n: Z) :
l #k - k #n - WP (! !#l) {{ v, v = #n }}.
Proof. iIntros. vcg_opt. try eauto with iFrame. Qed.
Lemma test7 (l: loc) Hp Hs1 Hs2 :
Hp Hs1 - l #21 - Hs2 - WP (!#l + #21) {{ v, l #21 v = #42}}.
Proof. iIntros (h) "H1 H2 H3". vcg_opt. try eauto with iFrame. Qed.
Lemma test8_swap (l1 l2 l3: loc) (n1 n2: Z) :
l1 #n1 - l2 #n2 - l3 #0 -
WP (#l3 <- !#l1 ;; #l1 <- !#l2 ;; #l2 <- !#l3) {{ _, l1 #n2 l2 #n1 }}.
Proof. iIntros. vcg_opt. eauto with iFrame. Qed.
Lemma test9 (l1 l2 l3: loc) (n1 n2: Z) :
l1 #n1 - l2 #n2 - l3 #0 -
WP (#l3 <- !#l1 + !#l1 ;;
#l1 <- !#l2 + !#l2 ;;
#l2 <- !#l3 ;;
!#l1 + !#l2)
{{ v, v = #(n2 + n2 + (n1 + n1)) l1 #(n2 + n2) l2 #(n1 + n1) }}.
Proof. iIntros. vcg_opt. eauto with iFrame. Qed.
Lemma test10 (l : loc) (n : Z) :
l #n - WP (#21 + #21 ;; #l <- !#l) ;; #0 ;; !#l {{ v, v = #n l #n }}.
Proof. iIntros. vcg_opt. eauto with iFrame. Qed.
Lemma test11_bad_store (l : loc) (n : Z) :
False -
l #n - WP (#21 + #21 ;; #l <- !#l) ;; #0 <- #0 ;; !#l {{ v, v = #n l #n }}.
Proof.
iIntros. vcg_opt. done. Qed.
End Tests_vcg.
From iris.heap_lang Require Export proofmode notation.
From iris.bi Require Import big_op.
From iris_c Require Import dval.
Section vcg.
Context `{heapG Σ}.
Inductive wp_expr :=
| Base : iProp Σ wp_expr
| Inhale : dloc (dval wp_expr) wp_expr
| Exhale : dloc dval wp_expr wp_expr
| IsSome {A} : doption A (A wp_expr) wp_expr
| IsLoc : dval (dloc wp_expr) wp_expr
| Par :
((dval iProp Σ) wp_expr)
((dval iProp Σ) wp_expr)
(dval dval wp_expr) wp_expr.
Arguments Base _%I.
Fixpoint wp_interp (E : list loc) (a : wp_expr) : iProp Σ :=
match a with
| Base P => P
| Inhale dl Φ =>
dv, dloc_interp E dl dval_interp E dv wp_interp E (Φ dv)
| Exhale dl dv Φ =>
dloc_interp E dl dval_interp E dv - wp_interp E Φ
| IsSome dmx Φ => x, doption_interp dmx = Some x wp_interp E (Φ x)
| IsLoc dv Φ =>
dl : dloc, dval_interp E dv = #(dloc_interp E dl) wp_interp E (Φ dl)
| Par P1 P2 P3 => Ψ1 Ψ2,
wp_interp E (P1 Ψ1)
wp_interp E (P2 Ψ2)
v1 v2, Ψ1 v1 - Ψ2 v2 - wp_interp E (P3 v1 v2)
end%I.
Fixpoint wp_interp_sane (E : list loc) (a : wp_expr) : iProp Σ :=
match a with
| Base Φ => Φ
| Inhale dl Φ =>
v, dloc_interp E dl v wp_interp_sane E (Φ (dValUnknown v))
| Exhale dl dv Φ =>
dloc_interp E dl dval_interp E dv - wp_interp_sane E Φ
| IsSome dmx Φ =>
x, doption_interp dmx = Some x wp_interp_sane E (Φ x)
| IsLoc dv Φ =>
l : loc, dval_interp E dv = #l wp_interp_sane E (Φ (dLocUnknown l))
| Par P1 P2 P3 => Ψ1 Ψ2 : val iProp Σ,
wp_interp_sane E (P1 (λ dv, Ψ1 (dval_interp E dv)))
wp_interp_sane E (P2 (λ dv, Ψ2 (dval_interp E dv)))
v1 v2, Ψ1 v1 - Ψ2 v2 - wp_interp_sane E (P3 (dValUnknown v1) (dValUnknown v2))
end%I.
Lemma wp_interp_sane_sound E a : wp_interp_sane E a wp_interp E a.
Proof. (*
generalize dependent E.
induction a.
- done.
- simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
iExists (dValUnknown v). simpl. iFrame. by iApply H0.
- simpl. iIntros (E) "He H". iApply IHa. by iApply "He".
- simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
iExists v. iFrame. by iApply H0.
- simpl. iIntros (E) "He". iDestruct "He" as (l) "[H1 H2]".
iExists (dLocUnknown l). simpl. iFrame. by iApply H0.
Qed. *) Admitted.
Class WpQuote (E : list loc) (e : expr) (Φ : dval wp_expr) (t : wp_expr) :=
wp_quote :
wp_interp E t
WP e {{ v, dv, dval_interp E dv = v wp_interp E (Φ dv) }}.
Global Instance wp_quote_default E e Φ :
WpQuote E e Φ (Base (WP e {{ v, wp_interp E (Φ (dValUnknown v)) }})) | 1000.
Proof.
rewrite /WpQuote /=. apply wp_mono=> v.
iIntros "H". iExists (dValUnknown v); auto.
Qed.
Class LocLookup (E : list loc) (l : loc) (i : nat) :=
loc_lookup : E !! i = Some l.
Global Instance loc_lookup_here l E : LocLookup (l :: E) l 0.
Proof. done. Qed.
Global Instance loc_lookup_there l l' E i :
LocLookup E l i LocLookup (l' :: E) l (S i).
Proof. done. Qed.
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.
Global Instance base_lit_quote_loc_unknown E l :
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.
Class IntoDVal (E : list loc) (e : expr) (dv : dval) :=
into_dval : e = of_val (dval_interp E dv).
Global Instance into_dval_loc E l dl :
BaseLitQuote E l dl IntoDVal E (Lit l) (dLitV dl).
Proof. by rewrite /BaseLitQuote /IntoDVal=> ->. Qed.
Global Instance into_dval_default E e v :
IntoVal e v IntoDVal E e (dValUnknown v) | 1000.
Proof. by rewrite /IntoVal /IntoDVal=> /of_to_val ->. Qed.
Instance wp_quote_value E e dv Φ :
IntoDVal E e dv WpQuote E e Φ (Φ dv).
Proof. rewrite /WpQuote. iIntros (->) "H". iApply wp_value. eauto. Qed.
Global Instance wp_quote_load E e Φ t :
WpQuote E e (λ dv, IsLoc dv (λ l, Inhale l (λ w, Exhale l w (Φ w)))) t
WpQuote E (Load e) Φ t.
Proof.
rewrite /WpQuote /= => ->. iIntros "H". wp_apply (wp_wand with "H").
iIntros (?). iDestruct 1 as (dv <- l -> w) "[Hl H]".
wp_load. iExists w; iSplit; first done. by iApply "H".
Qed.
Global Instance wp_quote_bin_op E op e1 e2 Φ Ψ t :
( dv1, WpQuote E e2 (λ dv2, IsSome (dbin_op_eval E op dv1 dv2) Φ) (Ψ dv1))
WpQuote E e1 Ψ t WpQuote E (BinOp op e1 e2) Φ t.
Proof.
rewrite /WpQuote /= => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"); iIntros (v1).
iDestruct 1 as (dv <-) "H". rewrite He2.
wp_apply (wp_wand with "H"); iIntros (v2).
iDestruct 1 as (dv' <- w ?) "H".
wp_op.
- by apply dbin_op_eval_correct.
- iExists w. auto.
Qed.
Global Instance wp_quote_store E e1 e2 Φ t1 t2 :
( Ψ1, WpQuote E e1 (Base Ψ1) (t1 Ψ1))
( Ψ2, WpQuote E e2 (Base Ψ2) (t2 Ψ2))
WpQuote E (Store e1 e2) Φ (Par t1 t2 (λ v1 v2, IsLoc v1 (λ l, Inhale l (λ _, Exhale l v2 (Φ v2))))).
Proof.
rewrite /WpQuote /= => He1 He2. (* => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"); iIntros (v1).
iDestruct 1 as (dl <- l ->) "H".
rewrite He2. wp_apply (wp_wand with "H"); iIntros (v2).
iDestruct 1 as (dv <- w) "[Hl H]". wp_store.
iExists (dLitV dLitUnit). iSplit; first done. by iApply "H".
Qed. *) Admitted.
Global Instance wp_quote_seq E e1 e2 Φ Ψ t `{Closed [] e2}:
WpQuote E e2 Φ Ψ
WpQuote E e1 (λ _, Ψ) t
WpQuote E (e1 ;; e2) Φ t.
Proof.
rewrite /WpQuote /= => He2 ->. iIntros "H".
wp_apply (wp_wand with "H"). iIntros (v1).
iDestruct 1 as (dv1 <-) "H". wp_seq.
by rewrite He2.
Qed.
Fixpoint exhale_list (s : list (nat * dval)) (Φ : wp_expr) : wp_expr :=
match s with
| (i, v) :: s' => Exhale (dLoc i) v (exhale_list s' Φ)
| [] => Φ
end.
Definition exhale_list_interp E (pl : list (nat * dval)) : iProp Σ :=
([ list] lw pl, dloc_interp E (dLoc lw.1) dval_interp E lw.2)%I.
Lemma vcg_exhale_list_sound' E s t :
wp_interp E (exhale_list s t) - exhale_list_interp E s - wp_interp E t.
Proof.
unfold exhale_list_interp.
induction s as [| [i w] s']; simpl.
- by iIntros "$ _".
- iIntros "H [H1 H2]".
iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
Qed.
Fixpoint find_and_remove (pl: list (nat * dval)) (dl: dloc) :
option (list (nat * dval) * dval) :=
match pl with
| [] => None
| (i,v) :: pl' =>
if (bool_decide (dl = dLoc i)) then Some (pl', v)
else match find_and_remove pl' dl with
| None => None
| Some (rl, w) => Some ((i,v) :: rl, w)
end
end.
Lemma find_and_remove_dLocUnknown pl l :
find_and_remove pl (dLocUnknown l) = None.
Proof. induction pl as [|[? ?] ?]; eauto; simpl; by rewrite IHpl. Qed.
Lemma find_and_remove_dLocKnown pl pl' d w' :
find_and_remove pl d = Some (pl', w') i, d = dLoc i.
Proof.
case d; eauto; intros ?; rewrite find_and_remove_dLocUnknown; inversion 1.
Qed.
Lemma find_and_remove_big_sepL pl i pl' w' (Φ : nat * dval iProp Σ) :
find_and_remove pl (dLoc i) = Some (pl', w')
([ list] lw pl, Φ lw)%I (([ list] lw pl', Φ lw) Φ (i, w'))%I.
Proof.
iIntros (Hfind). iInduction pl as [|hd tl] "IH" forall (pl' Hfind);
simpl; iSplit; try (done || simpl in H0; case_bool_decide;
simplify_eq /=; iIntros "[H1 H2]"; iFrame); simpl in Hfind; destruct hd;
iIntros "[HΦ Hlst]"; case_bool_decide; simplify_eq /=; [iFrame| |iFrame|].
- destruct (find_and_remove tl (dLoc i)); simplify_eq /=.
destruct p; simplify_eq /=. iFrame. by iApply "IH".
- destruct (find_and_remove tl (dLoc i)); simplify_eq /=.
destruct p; simplify_eq /=. iDestruct "HΦ" as "[HΦ Hl]".
iFrame. iApply ("IH" $! l); first done. iFrame.
Qed.
Fixpoint mem (s : list (nat * dval)) (i: nat) : bool :=
match s with
| [] => false
| (j, _) :: s' => if (bool_decide (i = j)) then true else mem s' i
end.
Lemma mem_no_dup s i : false = mem s i i s.*1.
Proof.
induction s; intros Hf.
- by apply not_elem_of_nil.
- apply not_elem_of_cons. simpl in Hf. destruct a as [i' ?].
case_bool_decide; first done. naive_solver.
Qed.
Fixpoint optimize (s : list (nat * dval)) (Φ : wp_expr) : wp_expr :=
match Φ with
| Base Φ1 => exhale_list s Φ
| Inhale dl Φ1 =>
match find_and_remove s dl with
| None => Inhale dl (λ v, optimize s (Φ1 v))
| Some (s', w) => optimize s' (Φ1 w)
end
| Exhale (dLoc i) w Φ =>
if mem s i then Base False
else optimize ((i,w) :: s) Φ
| Exhale (dLocUnknown l) w Φ => Exhale (dLocUnknown l) w (optimize s Φ)
| IsSome dmx Φ1 =>
match dmx with
| dNone => Base False
| dSome x => optimize s (Φ1 x)
| _ => IsSome dmx (λ v, optimize s (Φ1 v))
end
| IsLoc dv Φ1 =>
match dv with
| dLitV (dLitLoc l) => optimize s (Φ1 l)
| dLitV (dLitUnknown _) | dValUnknown _ =>
IsLoc dv (λ v, optimize s (Φ1 v))
| _ => Base False
end
| Par P1 P2 P3 => Par (λ Ψ1, optimize s (P1 Ψ1))
(λ Ψ2, optimize s (P2 Ψ2))
(λ v1 v2, optimize s (P3 v1 v2))
end.
Lemma vcg_opt_list_sound' (E: list loc) (pl: list (nat * dval)) (Φ: wp_expr) :
wp_interp E (optimize pl Φ) -
exhale_list_interp E pl - (wp_interp E Φ).
Proof. (*
generalize dependent pl.
induction Φ; simpl.
- intros. eapply vcg_exhale_list_sound'.
- intros pl.
remember (find_and_remove pl d) as far. destruct far.
+ iIntros "Hw He".
destruct d; last by rewrite find_and_remove_dLocUnknown in Heqfar.
unfold exhale_list_interp. symmetry in Heqfar. destruct p.
apply find_and_remove_big_sepL
with (Φ := λ lw, (dloc_interp E (dLoc lw.1) ↦ dval_interp E lw.2)%I)
in Heqfar. rewrite Heqfar.
iDestruct "He" as "[Hlst Hp]".
iExists d. iFrame. rewrite H0. by iApply "Hw".
+ iIntros "Hwp Hexh". simplify_eq /=.
iDestruct "Hwp" as (d0) "[Hp Hwp]". rewrite H0.
iExists d0. iFrame. by iApply "Hwp".
- intros pl.
destruct d as [i|l].
+ remember (mem pl i) as msi. destruct msi.
{ iIntros "?"; done. }
iIntros "Hwp Hl Hi". rewrite IHΦ /exhale_list_interp.