Commit 19fba43f authored by Léon Gondelman's avatar Léon Gondelman

started working on alloc case for vcg_wp. In the subsequent commit, I will turn admits into lemmas.

parent 3eb3006a
......@@ -37,9 +37,9 @@ Section tests_vcg.
k C #10 - awp (alloc 11 = ∗ᶜ♯k + 2) True (λ v, True).
Proof.
iIntros "Hk". vcg_solver.
iIntros "Hk". iApply a_alloc_spec. awp_ret_value.
(* iIntros "Hk". iApply a_alloc_spec. awp_ret_value.
iIntros (l) "Hl". vcg_continue.
eauto 42 with iFrame.
eauto 42 with iFrame. *)
Qed.
(*
......
......@@ -198,6 +198,9 @@ Section vcg.
| dCSeq de1 de2 =>
vcg_wp E m de1 R (λ E m _,
U (vcg_wp E (denv_unlock m) de2 R Φ))
| dCAlloc de =>
vcg_wp E m de R (λ E m' dv,
l : loc, Φ (E++[l]) (denv_insert (length E) ULvl 1 dv m') (dLitV $ dLitLoc (dLoc (length E))))
| _ => vcg_wp_unknown R E de m Φ
end%I.
End vcg.
......@@ -576,10 +579,24 @@ Section vcg_spec.
revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp".
- iApply awp_ret. wp_value_head.
iExists E, d, m. iSplit; first done; by iFrame.
- by iApply (vcg_wp_unknown_correct with "Hm Hwp").
- rewrite IHde //. iRename "Hm" into "Hawp".
iSpecialize ("Hawp" with "Hwp"); simpl.
iApply a_alloc_spec. iApply (awp_wand with "Hawp").
iIntros (v) "Hpost". iDestruct "Hpost" as (E' dv m' -> Hwf0 Hm'wf Hwf2) "(Hm & Hwp)".
iIntros (l) "Hl". iSpecialize ("Hwp" $! l).
unfold vcg_wp_postcondition.
iExists (E' ++ [l]), (dLitV (dLitLoc (dLoc (length E')))), (denv_insert (length E') ULvl 1 dv m').
iSplit. admit. (*TODO: this will require a special lemma *)
iSplit. iPureIntro. trans E'; first done. by apply prefix_app_r.
iSplit. admit. (*TODO: this will require another denv_wf monotonicity lemma *)
iSplit. (*TODO: this will require a special lemma *) admit.
iFrame. rewrite -denv_insert_interp.
iSplitL "Hm". iApply (denv_interp_mono with "Hm"); first done.
trans E'; first done. by apply prefix_app_r.
(*TODO: this will require a special lemma *) admit.
- rewrite IHde //. iRename "Hm" into "Hawp".
iSpecialize ("Hawp" with "Hwp"); simpl.
iApply (a_load_spec_exists_frac with "[Hawp]"). iApply (awp_wand with "Hawp").
iApply (a_load_spec_exists_frac with "[Hawp]"). iApply (awp_wand with "Hawp").
iIntros (v) "H". unfold vcg_wp_postcondition.
iDestruct "H" as (E' dv m' Heq Hwf0 Hm'wf Hwf2) "(Hm & Hwp)".
iPoseProof (vcg_wp_load_correct E' m' with "Hm Hwp") as "Hload"; first done.
......@@ -692,7 +709,7 @@ Section vcg_spec.
iFrame. iPureIntro; done. eapply dcexpr_wf_mono in Hwf2.
done. done. by apply denv_wf_unlock.
- by iApply (vcg_wp_unknown_correct with "Hm Hwp").
Qed.
Admitted.
Lemma tac_vcg_sound Γs_in Γs_out Γls Γp m c e R Φ E de :
MapstoListFromEnv Γs_in Γs_out Γls
......
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