Commit 2c796ed4 authored by Léon Gondelman's avatar Léon Gondelman
Browse files

working on the sequence case for the correctness of the vcg_wp. That will...

working on the sequence case for the correctness of the vcg_wp. That will require to strenghten the statement of correctness
parent 6c615dc7
......@@ -415,7 +415,7 @@ Section vcg_spec.
awp (dcexpr_interp E de) R
(λ v, E' dv m', dval_interp E' dv = v denv_interp E' m' wp_interp E' (Φ E' m' dv)).
Proof.
revert Φ m. induction de; intros Φ m; iIntros "Hm Hwp".
revert Φ E m. induction de; intros Φ E m; iIntros "Hm Hwp".
- iApply awp_ret. wp_value_head. iExists E, d, m. iSplit; first done; iFrame.
- iApply (vcg_wp_unknown_correct with "Hm Hwp").
- rewrite IHde. iSpecialize ("Hm" with "Hwp"); simpl.
......@@ -424,8 +424,26 @@ Section vcg_spec.
iApply (vcg_wp_load_correct with "Hm Hwp").
- admit.
- admit.
- admit.
- admit.
- rewrite IHde. iApply a_un_op_spec. iSpecialize ("Hm" with "Hwp").
iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iDestruct "Hex" as (E' dv m' <-) "(Hm & Hwp)".
destruct (dun_op_eval E' u dv) as [| dw | dw] eqn:Hop; simpl.
+ iDestruct "Hwp" as (?) "[% _]"; simplify_eq /=.
+ iExists (dval_interp E' dw); iSplit.
iPureIntro. apply dun_op_eval_correct. by rewrite Hop.
eauto with iFrame.
+ iDestruct "Hwp" as (w) "[% Hwp]"; simplify_eq /=.
iExists (dval_interp E' w). iSplit. iPureIntro.
apply dun_op_eval_correct. by rewrite Hop.
eauto with iFrame.
- rewrite IHde1. iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
iApply (a_sequence_spec with "[Hm]"); fold dcexpr_interp.
{ exists (λ: <>, dcexpr_interp E de2)%V. by unlock. }
iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iDestruct "Hex" as (Enew dv m' <-) "(Hm & Hwp)". simpl. rewrite denv_unlock_interp.
iModIntro. rewrite IHde2. awp_seq. iSpecialize ("Hm" with "Hwp").
(* TODO: Need to make the main statement stronger by requiring that
E `prefix_of` E', just as in unknown case. *) admit.
- iApply (vcg_wp_unknown_correct with "Hm Hwp").
Admitted.
......
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