Commit 1381c0cb authored by Léon Gondelman's avatar Léon Gondelman
Browse files

fix vcg_wp for binOp w.r.t. giving back mIn earlier

parent 8def411d
......@@ -133,21 +133,25 @@ Section vcg.
Fixpoint vcg_wp (E: known_locs) (m: denv) (de : dcexpr) (R : iProp Σ) (Φ : dval wp_expr) : wp_expr :=
match de with
| dCRet dv => Φ dv
| dCLoad de1 => vcg_wp E m de1 R (λ dv, IsLoc dv (λ l, MapstoStar l 1%Qp (λ w, MapstoWand l w ULvl 1%Qp (Φ w))))
| dCLoad de1 =>
vcg_wp E m de1 R (λ dv,
IsLoc dv (λ l, MapstoStar l (1/2)%Qp (λ w, MapstoWand l w ULvl (1/2)%Qp (Φ w))))
| dCStore de1 de2 =>
match vcg_sp E m de1 with
| Some (mIn, mOut, dv1) =>
IsLoc dv1 (λ dl,
mapsto_star_list m (mapsto_wand_list mIn (
vcg_wp E mIn de2 R (λ dv2, mapsto_wand_list mOut
(MapstoStar dl 1%Qp (λ _, (MapstoWand dl dv2 LLvl 1%Qp (Φ dv2))))))))
mapsto_star_list m
(mapsto_wand_list mIn
(vcg_wp E mIn de2 R (λ dv2, mapsto_wand_list mOut
(MapstoStar dl 1%Qp (λ _, (MapstoWand dl dv2 LLvl 1%Qp (Φ dv2))))))))
| None =>
match vcg_sp E m de2 with
| Some (mIn, mOut, dv2) =>
mapsto_star_list m (mapsto_wand_list mIn (
vcg_wp E mIn de1 R (λ dv1,
IsLoc dv1 (λ dl, mapsto_wand_list mOut
(MapstoStar dl 1%Qp (λ _, MapstoWand dl dv2 LLvl 1%Qp (Φ dv2)))))))
mapsto_star_list m
(mapsto_wand_list mIn
(vcg_wp E mIn de1 R (λ dv1,
IsLoc dv1 (λ dl, mapsto_wand_list mOut
(MapstoStar dl 1%Qp (λ _, MapstoWand dl dv2 LLvl 1%Qp (Φ dv2)))))))
| None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
end
end
......@@ -155,13 +159,15 @@ Section vcg.
(* TODO: LG: return the `mIn` resources early on *)
match vcg_sp E m de1 with
| Some (mIn, mOut, dv1) =>
mapsto_star_list m (vcg_wp E mIn de2 R (λ dv2,
mapsto_wand_list (denv_merge mIn mOut) (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
mapsto_star_list m
(mapsto_wand_list mIn (vcg_wp E mIn de2 R (λ dv2,
mapsto_wand_list mOut (IsSome (dbin_op_eval E op dv1 dv2) Φ))))
| None =>
match vcg_sp E m de2 with
| Some (mIn, mOut, dv2) =>
mapsto_star_list m (vcg_wp E mIn de1 R (λ dv1,
mapsto_wand_list (denv_merge mIn mOut) (IsSome (dbin_op_eval E op dv1 dv2) Φ)))
mapsto_star_list m
(mapsto_wand_list mIn (vcg_wp E mIn de1 R (λ dv1,
mapsto_wand_list mOut (IsSome (dbin_op_eval E op dv1 dv2) Φ))))
| None => Base (awp (dcexpr_interp E de) R (λ v, wp_interp E (Φ (dValUnknown v))))
end
end
......@@ -425,17 +431,18 @@ Section vcg_spec.
eauto 30 with iFrame. }
rewrite mapsto_star_list_spec.
iDestruct "H" as "[Henv Hde1]".
rewrite mapsto_wand_list_spec.
rewrite IHde1.
iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
iDestruct ("Hsp" with "Henv") as "[Hm1 Hde2]".
iSpecialize ("Hde1" with "Hm1").
iApply (a_bin_op_spec with "[$Hde1] [$Hde2]").
iNext. iIntros (? ?) "Hex".
iDestruct "Hex" as (? <-) "Hwp".
simplify_eq /=.
rewrite mapsto_wand_list_spec.
rewrite -denv_merge_interp.
iIntros "[-> H]".
iSpecialize ("Hwp" with "[$Hm1 $H]").
iSpecialize ("Hwp" with "[$H]").
simpl.
iDestruct "Hwp" as (w) "(% & Hwp)".
iExists (dval_interp E w).
......@@ -444,16 +451,17 @@ Section vcg_spec.
eauto with iFrame. }
rewrite mapsto_star_list_spec.
iDestruct "H" as "[Henv Hde2]".
rewrite mapsto_wand_list_spec.
rewrite IHde2.
iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
iDestruct ("Hsp" with "Henv") as "[Hm1 Hde1]".
iSpecialize ("Hde2" with "Hm1").
iApply (a_bin_op_spec with "[$Hde1] [$Hde2]").
iNext. iIntros (? ?) "(% & H) Hex".
iDestruct "Hex" as (? <-) "Hwp".
simplify_eq /=.
rewrite mapsto_wand_list_spec.
rewrite -denv_merge_interp.
iSpecialize ("Hwp" with "[$Hm1 $H]").
iSpecialize ("Hwp" with "[$H]").
simpl.
iDestruct "Hwp" as (w) "(% & Hwp)".
iExists (dval_interp E w).
......
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