Commit 65da2295 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

working on bin_op case

parent 6b9ef14e
......@@ -431,7 +431,29 @@ Section vcg_spec.
iSpecialize ("Hwp" with "Hl"). iDestruct "Hwp" as (Ef dvf mf Hpre' <-) "(Hmf & Hwp)".
iExists Ef, dvf, mf. iFrame. by iSplit; first by iPureIntro; trans E'; done.
- admit.
- 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.
{ 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").
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 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