Commit 0f0cba76 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

work in progress on vcg_sp and vcg_wp w.r.t. fractions and levels

parent 823e05c0
......@@ -5,13 +5,22 @@ 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.
(*TODO:
Understand how to correctly deal with levels and fractions in
- exhale_list, i.e., what are levels and fractions of those ressources that
are given in the very end to the postcondition
- computations of vcg_sp, i.e. what are levels and fractions given back
by vcg_sp in case of load and store *)
Section vcg.
Context `{amonadG Σ}.
Inductive wp_expr :=
| Base : iProp Σ wp_expr
| Inhale : dloc (dval wp_expr) wp_expr
| Exhale : dloc dval level wp_expr wp_expr
| Inhale : dloc frac (dval wp_expr) wp_expr
| Exhale : dloc dval frac level wp_expr wp_expr
| IsSome {A} : doption A (A wp_expr) wp_expr
| IsLoc : dval (dloc wp_expr) wp_expr
| UMod : wp_expr wp_expr
......@@ -21,13 +30,13 @@ Section vcg.
(dval dval wp_expr) wp_expr.
Arguments Base _%I.
Fixpoint wp_interp (E : list loc) (a : wp_expr) : iProp Σ :=
Fixpoint wp_interp (E : env_locs) (a : wp_expr) : iProp Σ :=
match a with
| Base P => P
| Inhale dl Φ =>
dv, dloc_interp E dl U dval_interp E dv wp_interp E (Φ dv)
| Exhale dl dv x Φ =>
dloc_interp E dl [x] dval_interp E dv - wp_interp E Φ
| Inhale dl q Φ =>
dv, dloc_interp E dl U{q} dval_interp E dv wp_interp E (Φ dv)
| Exhale dl dv q x Φ =>
mapsto (dloc_interp E dl) x q (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)
......@@ -36,15 +45,15 @@ Section vcg.
wp_interp E (P1 Ψ1)
wp_interp E (P2 Ψ2)
(v1 v2 : val), Ψ1 v1 - Ψ2 v2 - wp_interp E (P3 (dValUnknown v1) (dValUnknown v2))
end%I.
end%I.
Fixpoint wp_interp_sane (E : list loc) (a : wp_expr) : iProp Σ :=
Fixpoint wp_interp_sane (E : env_locs) (a : wp_expr) : iProp Σ :=
match a with
| Base Φ => Φ
| Inhale dl Φ =>
v, dloc_interp E dl U v wp_interp_sane E (Φ (dValUnknown v))
| Exhale dl dv x Φ =>
dloc_interp E dl [x] dval_interp E dv - wp_interp_sane E Φ
| Inhale dl q Φ =>
v, dloc_interp E dl U{q} v wp_interp_sane E (Φ (dValUnknown v))
| Exhale dl dv q x Φ =>
mapsto (dloc_interp E dl) x q (dval_interp E dv) - wp_interp_sane E Φ
| IsSome dmx Φ =>
x, doption_interp dmx = Some x wp_interp_sane E (Φ x)
| IsLoc dv Φ =>
......@@ -78,10 +87,116 @@ Section vcg.
iApply ("HΦ" with "Hv1 Hv2").
Qed.
Fixpoint vcg_wp (E: list loc) (s: list (nat * (frac * dval))) (de : dcexpr) (Φ: dval wp_expr) : wp_expr :=
Definition env_ps_dv := list (nat * (frac * dval)).
Fixpoint exhale_list (ps : env_ps_dv) (Φ : wp_expr) : wp_expr :=
match ps with
| (i, (q, dv)) :: s' =>
Exhale (dLoc i) dv q ULvl (*TODO: think whether it is correct *)
(exhale_list s' Φ)
| [] => Φ
end.
(*TODO: fix the levels: Sure it is ULvl *)
Definition exhale_list_interp E (ps : env_ps_dv) : iProp Σ :=
([ list] lw ps, dloc_interp E (dLoc lw.1) U{lw.2.1} dval_interp E lw.2.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 [q w]] s']; simpl.
- by iIntros "$ _".
- iIntros "H [H1 H2]".
iSpecialize ("H" with "H1"). iApply (IHs' with "H H2").
Qed.
Fixpoint is_dloc (E: env_locs) (dv: dval) : option nat :=
match dv with
| dLitV (dLitLoc (dLoc i)) => Some i
| _ => None
end.
Fixpoint find_and_remove (ps: env_ps_dv) (dl: dloc) :
option (env_ps_dv * (frac * dval)) :=
match ps with
| [] => None
| (i, (q, dv)) :: ps' =>
if (bool_decide (dl = dLoc i))
then Some (ps', (q, dv))
else match find_and_remove ps' dl with
| None => None
| Some (rs, w) => Some ((i,(q, dv)) :: rs, w)
end
end.
Lemma find_and_remove_dLocUnknown ps l :
find_and_remove ps (dLocUnknown l) = None.
Proof. induction ps as [|[? [? ?]] ?]; eauto; simpl; by rewrite IHps. Qed.
Lemma find_and_remove_dLocKnown ps ps' d w' :
find_and_remove ps d = Some (ps', w') i, d = dLoc i.
Proof.
case d; eauto; intros ?; rewrite find_and_remove_dLocUnknown; inversion 1.
Qed.
Lemma find_and_remove_big_sepL ps i ps' w' (Φ : nat * (frac * dval) iProp Σ) :
find_and_remove ps (dLoc i) = Some (ps', w')
([ list] lw ps, Φ lw)%I (([ list] lw ps', Φ lw) Φ (i, w'))%I.
Proof.
iIntros (Hfind). iInduction ps as [|[j [q dw] ] ts] "IH" forall (ps' Hfind);
simpl; iSplit; try (done || simpl in H0; case_bool_decide;
simplify_eq /=; iIntros "[H1 H2]"; iFrame); simpl in Hfind;
iIntros "[HΦ Hlst]"; case_bool_decide; simplify_eq /=; [iFrame| |iFrame|].
- destruct (find_and_remove ts (dLoc i)); simplify_eq /=.
destruct p; simplify_eq /=. iFrame. by iApply "IH".
- destruct (find_and_remove ts (dLoc i)); simplify_eq /=.
destruct p; simplify_eq /=. iDestruct "HΦ" as "[HΦ Hl]".
iFrame. iApply ("IH" $! e); first done. iFrame.
Qed.
Fixpoint vcg_sp (E: env_locs) (s: env_ps_dv) (de : dcexpr) :
option ( env_ps_dv * env_ps_dv * dval) :=
match de with
| dCVal dv => Some (nil, nil, dv)
| dCLoad de1 =>
''(s1, s2, dv) vcg_sp E s de1;
i is_dloc E dv;
''(s1', (q, dvi)) find_and_remove s (dLoc i);
Some ((i, ((q/2)%Qp, dvi)) :: s1', (i, ((q%Qp, dvi))) :: s2, dvi)
| dCStore de1 de2 =>
''(s1, s2, dv1) vcg_sp E s de1;
''(s1', s2', dv2) vcg_sp E s1 de2;
i is_dloc E dv1;
''(s3, (q%Qp, dvi)) find_and_remove s (dLoc i);
if (bool_decide (q = 1%Qp))
then Some (s3, (i, (1%Qp, dvi)) :: s2 ++ s2', dv2)
else None
| dCBinOp op de1 de2 =>
''(s1, s2, dv1) vcg_sp E s de1;
''(s1', s2', dv2) vcg_sp E s1 de2;
match dbin_op_eval E op dv1 dv2 with
| dSome dv | dUnknown (Some dv) => Some (s1', s2 ++ s2', dv)
| dNone | dUnknown None => None
end
end.
(* TODO: fix the Qp's correctly using vcg_sp *)
Fixpoint vcg_wp (E: list loc) (s: env_ps_dv) (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))))
| dCLoad de1 => vcg_wp E s de1 (λ dv, IsLoc dv (λ l, Inhale l 1%Qp (λ w, Exhale l w 1%Qp ULvl (Φ w))))
| dCBinOp op de1 de2 =>
match vcg_sp E s de1 with
| Some (s1, s2, dv1) =>
vcg_wp E s1 de2 (λ dv2,
exhale_list s2 (IsSome (dbin_op_eval E op dv1 dv2) Φ))
| None => Φ (dValUnknown #())
end
| _ => Φ (dValUnknown #())
end.
......
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