Commit 823e05c0 authored by Dan Frumin's avatar Dan Frumin

Basic infrastructure for the new vcgen

parent 1e024dfb
......@@ -10,6 +10,7 @@ theories/c_translation/proofmode.v
theories/c_translation/translation.v
theories/c_translation/derived.v
theories/vcgen/dcexpr.v
theories/vcgen/splitenv.v
theories/vcgen/vcgen.v
# theories/vcgen/test.v
# theories/heap_lang_vcgen/dval.v
......
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.
(** ** LocLookup *)
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.
(** ** BaseLitQuote *)
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.
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
From iris_c.vcgen Require Import dcexpr.
From iris_c.lib Require Import U locking_heap.
From iris_c.c_translation Require Import monad.
From iris.algebra Require Import frac.
Section splitenv.
Context `{amonadG Σ}.
Definition env_locs := list loc.
Definition env_ps := list (loc * (frac * val)).
Definition ps_loc (p : loc * (frac * val)) : loc := p.1.
Definition ps_frac (p : loc * (frac * val)) : frac := p.2.1.
Definition ps_val (p : loc * (frac * val)) : val := p.2.2.
Definition env_ps_interp (ps : env_ps) : iProp Σ :=
([ list] p ps, ps_loc p U{ps_frac p} ps_val p)%I.
Definition env_to_known_locs (Γls : env_ps) : env_locs := map fst Γls.
Class MapstoListFromEnv (Γin Γout : env (iProp Σ)) (Γls : env_ps) := {
mapsto_list_from_env :
[] Γin [] Γout env_ps_interp Γls;
mapsto_list_from_env_wf : env_wf Γin env_wf Γout;
mapsto_list_from_env_lookup_None i: Γin !! i = None Γout !! i = None
}.
Global Instance mapsto_list_from_env_nil : MapstoListFromEnv Enil Enil nil.
Proof. split; unfold env_ps_interp; eauto. Qed.
Global Instance mapsto_list_from_env_snoc_Γout Γin Γout Γls i P :
MapstoListFromEnv Γin Γout Γls
MapstoListFromEnv (Esnoc Γin i P) (Esnoc Γout i P) Γls | 100.
Proof.
destruct 1; split; simpl.
- rewrite mapsto_list_from_env0. iIntros "(H1 & H2 & H3)". iFrame.
- intro Hwf. inversion Hwf; subst. apply mapsto_list_from_env_wf0 in H4.
apply Esnoc_wf; last done. by apply mapsto_list_from_env_lookup_None0.
- intros j Hj. destruct (ident_beq j i); simplify_eq /=.
by apply mapsto_list_from_env_lookup_None0.
Qed.
Global Instance mapsto_list_from_env_snoc_Γls Γin Γout Γls i l q v :
MapstoListFromEnv Γin Γout Γls
MapstoListFromEnv (Esnoc Γin i (l U{q} v)) Γout ((l,(q,v))::Γls).
Proof.
destruct 1.
split.
- iIntros "H". simpl. iDestruct "H" as "[H1 H2]". iFrame.
by rewrite mapsto_list_from_env0.
- intros Heq. inversion Heq; simplify_eq /=. by apply mapsto_list_from_env_wf0.
- intros j Hsnoc. apply mapsto_list_from_env_lookup_None0.
destruct (decide (i = j)) as [->|]. simplify_eq /=. by destruct (ident_beq j j ).
by rewrite env_lookup_snoc_ne in Hsnoc.
Qed.
Definition exhale_list_interp E (ps : list (nat * (frac * dval))) : iProp Σ :=
([ list] lw ps, dloc_interp E (dLoc lw.1) U{lw.2.1} dval_interp E lw.2.2)%I.
Class ListOfMapsto (Γls : env_ps) (E : env_locs) (ps : list (nat * (frac * dval))) :=
list_of_mapsto : env_ps_interp Γls exhale_list_interp E ps.
Global Instance list_of_mapsto_Nil E : ListOfMapsto [] E [].
Proof. unfold ListOfMapsto. simpl. eauto. Qed.
Global Instance list_of_mapsto_cons_dLitV E Γls ps lit dlit i l q :
BaseLitQuote E lit dlit
LocLookup E l i
ListOfMapsto Γls E ps
ListOfMapsto ((l,(q,LitV lit))::Γls) E ((i,(q,dLitV dlit))::ps).
Proof.
rewrite /BaseLitQuote /LocLookup => Hlit Hi.
rewrite /ListOfMapsto => HΓls /=.
iDestruct 1 as "[Hl H]". cbn.
rewrite Hi Hlit. unfold env_ps_interp in *. rewrite HΓls. iFrame.
Qed.
Global Instance list_of_mapsto_cons_dValUnknown E Γls ps v i l q :
LocLookup E l i
ListOfMapsto Γls E ps
ListOfMapsto ((l,(q,v))::Γls) E ((i,(q,dValUnknown v))::ps) | 100.
Proof.
rewrite /BaseLitQuote /LocLookup => Hi.
rewrite /ListOfMapsto => HΓls /=.
iDestruct 1 as "[Hl H]". cbn.
unfold env_ps_interp in *. rewrite Hi HΓls. iFrame.
Qed.
Lemma tac_envs_split_mapsto Γs_in Γs_out Γls Γp c ps P:
MapstoListFromEnv Γs_in Γs_out Γls
ListOfMapsto Γls (env_to_known_locs Γls) ps
envs_entails (Envs Γp Γs_out c) (exhale_list_interp (env_to_known_locs Γls) ps - P)%I
envs_entails (Envs Γp Γs_in c) P.
Proof.
intros Hsplit. rewrite /ListOfMapsto coq_tactics.envs_entails_eq=> Hexhale.
unfold of_envs. simpl.
rewrite mapsto_list_from_env. intros Hz.
iIntros "(Hwf & #Hp & Hs & Hls)". iDestruct "Hwf" as %Hwf.
iApply (Hz with "[Hs]").
- iFrame "Hp Hs". iPureIntro.
split; eauto.
+ apply Hwf.
+ apply Hsplit. apply Hwf.
+ intros i. simpl. destruct (envs_disjoint _ Hwf i) as [Hp | Hp]; simpl in Hp.
* by left.
* right. by apply Hsplit.
- by iApply Hexhale.
Qed.
End splitenv.
<
From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr.
From iris_c.vcgen Require Import dcexpr splitenv.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.lib Require Import locking_heap U.
Section vcg.
Context `{amonadG Σ}.
Inductive wp_expr :=
| Base : iProp Σ wp_expr
| Inhale : dloc (dval wp_expr) wp_expr
......@@ -16,10 +16,10 @@ Section vcg.
| IsLoc : dval (dloc wp_expr) wp_expr
| UMod : wp_expr wp_expr
| Par :
((dval iProp Σ) wp_expr)
((dval iProp Σ) wp_expr)
((val iProp Σ) wp_expr)
((val iProp Σ) wp_expr)
(dval dval wp_expr) wp_expr.
Arguments Base _%I.
Arguments Base _%I.
Fixpoint wp_interp (E : list loc) (a : wp_expr) : iProp Σ :=
match a with
......@@ -32,10 +32,10 @@ Section vcg.
| IsLoc dv Φ =>
dl : dloc, dval_interp E dv = #(dloc_interp E dl) wp_interp E (Φ dl)
| UMod P => U (wp_interp E P)
| Par P1 P2 P3 => (Ψ1 Ψ2 : dval iProp Σ),
| Par P1 P2 P3 => (Ψ1 Ψ2 : val iProp Σ),
wp_interp E (P1 Ψ1)
wp_interp E (P2 Ψ2)
(dv1 dv2 : dval), Ψ1 dv1 - Ψ2 dv2 - wp_interp E (P3 dv1 dv2)
(v1 v2 : val), Ψ1 v1 - Ψ2 v2 - wp_interp E (P3 (dValUnknown v1) (dValUnknown v2))
end%I.
Fixpoint wp_interp_sane (E : list loc) (a : wp_expr) : iProp Σ :=
......@@ -51,19 +51,11 @@ Section vcg.
l : loc, dval_interp E dv = #l wp_interp_sane E (Φ (dLocUnknown l))
| UMod P => U (wp_interp_sane E P)
| 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)))
wp_interp_sane E (P1 Ψ1)
wp_interp_sane E (P2 Ψ2)
v1 v2, Ψ1 v1 - Ψ2 v2 - wp_interp_sane E (P3 (dValUnknown v1) (dValUnknown v2))
end%I.
Fixpoint vcg_wp (E: list loc) (s: list (nat * dval)) (de : dcexpr) (t: dval wp_expr) : wp_expr :=
match de with
| dCVal dv => t dv
| dCLoad de1 => vcg_wp E s de1 (λ dv, IsLoc dv (λ l, Inhale l (λ w, Exhale l w ULvl (t w))))
| _ => t (dValUnknown #())
end.
Lemma wp_interp_sane_sound E a : wp_interp_sane E a wp_interp E a.
Proof.
generalize dependent E.
......@@ -79,394 +71,42 @@ Section vcg.
- simpl. intros E. by apply U_mono.
- simpl. intros E.
iDestruct 1 as (Ψ1 Ψ2) "(HΨ1 & HΨ2 & HΦ)".
iExists (λ dv, Ψ1 (dval_interp E dv)), (λ dv, Ψ2 (dval_interp E dv)).
iExists _,_.
iSplitL "HΨ1". by iApply H0.
iSplitL "HΨ2". by iApply H1.
iIntros (dv1 dv2) "Hv1 Hv2". iApply H2.
admit.
Admitted.
(* No need for those classes any more)
Class AWpQuote (E : list loc) (e : expr) (R : iProp Σ) (Φ : dval → wp_expr) (t : wp_expr) :=
wp_quote :
wp_interp E t ⊢
awp e R (λ v, ∃ dv, ⌜ dval_interp E dv = v ⌝ ∧ wp_interp E (Φ dv)).
Global Instance awp_quote_default E e R Φ :
AWpQuote E e R Φ (Base (awp e R (λ v, wp_interp E (Φ (dValUnknown v))))) | 1000.
Proof.
rewrite /AWpQuote /=. iIntros "H". iApply (awp_wand with "H").
iIntros (v) "H". iExists (dValUnknown v); auto.
Qed.
(* TODO: awp ret for a general expression *)
Instance awp_quote_ret E e dv R Φ :
IntoDVal E e dv → AWpQuote E (a_ret e) R Φ (Φ dv).
Proof.
rewrite /AWpQuote. iIntros (->) "H".
iApply awp_ret. iApply wp_value. eauto.
Qed.
Global Instance awp_quote_load E e R Φ t :
AWpQuote E e R (λ dv, IsLoc dv (λ l, Inhale l (λ w, Exhale l w ULvl (Φ w)))) t →
AWpQuote E (a_load e) R Φ t.
Proof.
rewrite /AWpQuote /= => ->. iIntros "H".
awp_apply (a_wp_awp with "H").
iIntros (a) "Ha".
iApply a_load_spec.
iApply (awp_wand with "Ha").
iIntros (?). iDestruct 1 as (dv <- l -> w) "[Hl H]".
iExists _, _; iSplit; eauto. iFrame "Hl".
iIntros "Hl". iExists _; iSplit; eauto.
by iApply "H".
Qed.
Global Instance wp_quote_store E e1 e2 R Φ (t1 t2 : ((dval → iProp Σ) → wp_expr)) :
(∀ Ψ1 : dval → iProp Σ, AWpQuote E e1 R (λ v1, IsLoc v1 (λ l, Base (Ψ1 (dValUnknown #(dloc_interp E l)))))
(t1 Ψ1)) →
(∀ Ψ2 : dval → iProp Σ, AWpQuote E e2 R (λ v, Base (Ψ2 (dValUnknown (dval_interp E v))))
(t2 Ψ2)) →
AWpQuote E (a_store e1 e2) R Φ
(Par t1 t2 (λ v1 v2, IsLoc v1 (λ l, Inhale l (λ _, Exhale l v2 LLvl (Φ v2))))).
Proof.
rewrite /AWpQuote /= => He1 He2.
iDestruct 1 as (Ψ1 Ψ2) "(HΨ1 & HΨ2 & HΦ)".
iApply (a_store_spec _ _ (λ l, Ψ1 (dValUnknown #l))
(λ v, Ψ2 (dValUnknown v)) with "[HΨ1] [HΨ2]").
- iPoseProof (He1 with "HΨ1") as "H".
iApply (awp_wand with "H"). iIntros (?).
iDestruct 1 as (dv <- dl ?) "HΨ1". iExists _.
iSplit; eauto.
- iPoseProof (He2 with "HΨ2") as "H".
iApply (awp_wand with "H"). iIntros (?).
iDestruct 1 as (dv <-) "$".
- iNext. iIntros (l w) "HΨ1 HΨ2".
iDestruct ("HΦ" with "HΨ1 HΨ2") as (dl ?) "H".
iDestruct "H" as (dv) "[Hl H]". simplify_eq/=.
iExists _; iFrame. iIntros "Hl".
iExists (dValUnknown w); iSplit; eauto. 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_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 ULvl (exhale_list s' Φ)
| [] => Φ
end.
Definition exhale_list_interp E (pl : list (nat * dval)) : iProp Σ :=
([ list] lw pl, dloc_interp E (dLoc lw.1) U 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.
iIntros (v1 v2) "Hv1 Hv2". iApply H2.
iApply ("HΦ" with "Hv1 Hv2").
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 ULvl Φ =>
if mem s i then Base False
else optimize ((i,w) :: s) Φ
| Exhale (dLoc i) w LLvl Φ => Exhale (dLoc i) w LLvl (optimize s Φ)
| Exhale (dLocUnknown l) w x Φ => Exhale (dLocUnknown l) w x (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
| UMod P => UMod (optimize s P)
| Par P1 P2 P3 => Par (λ Ψ1, optimize s (P1 Ψ1))
(λ Ψ2, optimize s (P2 Ψ2))
(λ v1 v2, optimize s (P3 v1 v2))
Fixpoint vcg_wp (E: list loc) (s: list (nat * (frac * dval))) (de : dcexpr) (Φ: dval wp_expr) : wp_expr :=
match de with
| dCVal dv => Φ dv
| dCLoad de1 => vcg_wp E s de1 (λ dv, IsLoc dv (λ l, Inhale l (λ w, Exhale l w ULvl (Φ w))))
| _ => Φ (dValUnknown #())
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.