Commit 24e8b235 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

simplifying vcg_wp_bin_op and pointing out some todos in the proof of binop.

parent 65da2295
......@@ -179,7 +179,8 @@ Section vcg.
(m : denv) (Φ : denv dval wp_expr) : wp_expr :=
match dbin_op_eval E op dv1 dv2 with
| dSome dw => Φ m dw
| mdw => mapsto_wand_list m $ IsSome mdw (Φ [])
| dUnknown (Some dw) => Φ m dw
| _ => Base False
end.
Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
......@@ -433,27 +434,30 @@ Section vcg_spec.
- admit.
- rewrite{1} /vcg_wp; fold vcg_wp.
destruct (vcg_sp E m [] de1) as [[[mIn mOut] dv1]|] eqn:Heqsp; last first.
{ destruct (vcg_sp E m [] de2) as [[[mIn mOut] dv2]|] eqn:Heqsp2; last first.
+ destruct (vcg_sp E m [] de2) as [[[mIn mOut] dv2]|] eqn:Heqsp2; last first.
{ iApply (vcg_wp_unknown_correct with "[$Hm] [$Hwp]"). }
iPoseProof (vcg_sp_correct _ _ _ _ _ _ R) as "Hsp". eassumption.
iDestruct ("Hsp" with "Hm") as "[Hm Hde2]". iClear "Hsp". clear Heqsp2 Heqsp.
rewrite IHde1. iSpecialize ("Hm" with "Hwp").
rewrite IHde1; last first.
{ simpl in Hwf. apply andb_prop_elim in Hwf. by destruct Hwf. }
iSpecialize ("Hm" with "Hwp").
iApply (a_bin_op_spec with "[$Hm] [$Hde2]"); fold dcexpr_interp.
iNext. iIntros (v1 v2) "Hex (-> & HmOut)".
iDestruct "Hex" as (E' dv1 m' Hpre <-) "(Hm' & Hwp)"; simplify_eq /=.
rewrite /vcg_wp_bin_op. destruct (dbin_op_eval E' b dv1 dv2) as [| dw |] eqn:Hbin.
- rewrite mapsto_wand_list_spec -denv_merge_interp.
iSpecialize ("Hwp" with "[HmOut Hm']"). iFrame.
admit.
by iDestruct "Hwp" as (?) "(% & _)".
- iExists (dval_interp E' dw); iSplit. iPureIntro.
simpl in Hwf. apply andb_prop_elim in Hwf. destruct Hwf.
specialize (dval_interp_mono E E' dv2). intros.
admit. (* apply dbin_op_eval_correct. by rewrite Hbin. *)
admit.
- admit.
- admit. }
admit.
rewrite /vcg_wp_bin_op.
destruct (dbin_op_eval E' b dv1 dv2) as [ | dw | dw ] eqn:Hbin; first done.
* iExists (dval_interp E' dw); iSplit.
{ iPureIntro. (*TODO: we need (dval_interp E dv2) = (dval_interp E' dv2) *) admit. }
iExists E', dw, (denv_merge mOut m').
rewrite -denv_merge_interp. iFrame. repeat (iSplit; first done).
(*TODO: we have to relate denv_interp and prefix_of *) admit.
* destruct dw as [dw1|] eqn:Hdw; last done.
iExists (dval_interp E' dw1); iSplit.
{ iPureIntro. (*TODO: we need (dval_interp E dv2) = (dval_interp E' dv2) *) admit. }
iExists E', dw1, (denv_merge mOut m').
rewrite -denv_merge_interp. iFrame. repeat (iSplit; first done).
(*TODO: we have to relate denv_interp and prefix_of *) admit.
+ admit.
- rewrite IHde; last done. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iDestruct "Hex" as (E' dv m' Hpre <-) "(Hm & Hwp)".
......
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