Commit 0f2dec86 authored by Léon Gondelman 's avatar Léon Gondelman

work in progress on vcg_sp correctness

parent 231c868e
......@@ -254,7 +254,7 @@ Fixpoint dexpr_wf (X: list string) (E: known_locs) (de: dexpr) : bool :=
Fixpoint dcexpr_wf (X: list string) (E: known_locs) (de: dcexpr) : bool :=
match de with
| dCRet de => dexpr_wf X E de
| dCBind x de1 de2 => dcexpr_wf (x :: X) E de1 && dcexpr_wf X E de2
| dCBind x de1 de2 => dcexpr_wf X E de1 && dcexpr_wf (x :: X) E de2
| dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf X E de1
| dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
| dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
......@@ -371,17 +371,23 @@ Proof.
by rewrite (dexpr_interp_mono X E E').
Admitted.
(*
Global Instance dexpr_closed E de : Closed [] (dexpr_interp E de).
Proof. induction de; simpl; try solve_closed. Qed.
Global Instance dcexpr_closed E de : Closed [] (dcexpr_interp E de).
Global Instance dexpr_closed X E de :
dexpr_wf X E de
Closed X (dexpr_interp E de).
Proof.
induction de; simpl; try solve_closed. rewrite /Closed /=.
split_and. change (Closed [] a_ret). solve_closed. apply (dexpr_closed E d).
revert X. induction de; simpl; intros; unfold Closed; simpl; eauto using is_closed_of_val;
try by apply IHde.
destruct_and!. by split_and; [apply IHde1 | apply IHde2].
by apply W.is_closed_correct.
Qed.
*)
Global Instance dcexpr_closed X E de :
dcexpr_wf X E de
Closed X (cdexpr_interp E de).
Proof. Admitted.
(* induction de; simpl; try solve_closed. rewrite /Closed /=.
split_and. change (Closed [] a_ret). solve_closed. apply (dexpr_closed E d).
Qed. *)
(** * Reification of C syntax *)
(** ** LocLookup *)
......@@ -462,7 +468,7 @@ Global Instance into_dval_default E v : IntoDVal E v (dValUnknown v) | 1000.
Proof. done. Qed.
(** ** IntoDExpr *)
Class IntoDExpr (E: known_locs) (e: expr) (de: dexpr) :=
Class IntoDExpr (E: known_locs) (e: expr) (de: dexpr) :=
into_dexpr : e = dexpr_interp E de.
Global Instance into_dexpr_val E e dv :
......
......@@ -33,6 +33,7 @@ Section vcg_continue.
E = penv_to_known_locs Γls
ListOfMapsto Γls E m
IntoDCExpr E e de
dcexpr_wf [] E de
denv_wf (penv_to_known_locs Γls) m
envs_entails (Envs Γp Γs_out c)
(vcg_wp E m de R (λ E m dv,
......@@ -89,6 +90,7 @@ Ltac vcg_solver :=
| simpl; reflexivity (* Compute the known locations *)
| apply _ (* Compute the symbolic environment based on known locations *)
| apply _ (* Reify the expression *)
| vm_compute[reflexivity]; try done
| done (* Prove that the environment is well-formed *)
| simpl ].
......
......@@ -64,7 +64,11 @@ Section vcg.
| dEPair de1 de2 => dEPair (de_subst E x dv de1) (de_subst E x dv de2)
| dEFst de1 => dEFst (de_subst E x dv de1)
| dESnd de1 => dESnd (de_subst E x dv de1)
| dEUnknown e => dEUnknown (subst x (dval_interp E dv) e)
| dEUnknown we =>
dEUnknown (W.subst x
(W.Val (dval_interp E dv)
(of_val (dval_interp E dv))
(to_of_val _ )) we)
end.
......@@ -87,7 +91,9 @@ Section vcg.
| dCSeq de1 de2 => dCSeq (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCPar de1 de2 => dCPar (dce_subst E x dv de1) (dce_subst E x dv de2)
| dCInvoke v de1 => dCInvoke v (dce_subst E x dv de1)
| dCUnknown e => dCUnknown (subst x (dval_interp E dv) e)
| dCUnknown we => dCUnknown (W.subst x (W.Val (dval_interp E dv)
(of_val (dval_interp E dv))
(to_of_val _ )) we)
end.
......@@ -342,7 +348,7 @@ Section vcg.
end
| dCInvoke ef de1, S p => vcg_wp E m de1 R (λ E m dv,
vcg_wp_awp_continuation R E
(dCUnknown (ef (dval_interp E dv))) m Φ) p
(dCUnknown (W.ClosedExpr (ef (dval_interp E dv)))) m Φ) p
| _, S p => vcg_wp_awp_continuation R E de m Φ
| _, O => False
end%I.
......@@ -355,12 +361,18 @@ Section vcg_spec.
Lemma de_subst_subst_comm E x de dv :
(dexpr_interp E (de_subst E x dv de)) =
(subst x (dval_interp E dv) (dexpr_interp E de)).
subst x (dval_interp E dv) (dexpr_interp E de).
Proof.
induction de; simplify_eq /=; simpl_subst;
try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst);
by destruct (decide (x = s)).
induction de; simplify_eq /=.
- by simpl_subst.
- by destruct (decide (x = s)).
- try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst).
- try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst).
- try (repeat match goal with | [ H: _ = subst _ _ _ |- _ ] => rewrite H
end; by simpl_subst).
- by rewrite! W.to_expr_subst.
Qed.
Lemma dce_subst_subst_comm E (x: string) (de: dcexpr) (dv: dval) :
......@@ -376,13 +388,19 @@ Section vcg_spec.
+ rewrite IHde2 decide_True; naive_solver.
Qed.
Lemma dce_subst_dcexpr_wf E s dv1 de2 :
dval_wf E dv1
dcexpr_wf [s] E de2
dcexpr_wf [] E (dce_subst E s dv1 de2).
Proof. Admitted.
Arguments subst : simpl never.
Lemma mapsto_wand_list_aux_spec E m Φ (k : nat) :
mapsto_wand_list_aux E m Φ k -
([ list] ndio m, from_option
(λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
dloc_interp E (dLoc (k + n) 0) C[lv]{q} dval_interp E dv) True dio) - Φ.
(λ '{| denv_level := lv; denv_frac := q; denv_dval := dv |},
dloc_interp E (dLoc (k + n) 0) C[lv]{q} dval_interp E dv) True dio) - Φ.
Proof.
iIntros "H".
iInduction m as [|[[x q dv]|]] "IH" forall (k); simpl; first auto.
......@@ -516,21 +534,26 @@ Section vcg_spec.
destruct_and!. auto.
Qed.
Lemma vcg_sp_dval_wf E de ms ms' mNew dv n :
vcg_sp E ms de n = Some (ms', mNew, dv)
dval_wf E dv.
Proof. Admitted.
Lemma vcg_sp_correct' E de ms ms' mNew dv R n :
vcg_sp E ms de n = Some (ms', mNew, dv)
dcexpr_wf [] E de (*where free_vars de ⊆ X*) *)
dcexpr_wf [] E de
(denv_stack_interp ms ms' E
(awp (dcexpr_interp E de) R
(λ v, v = dval_interp E dv denv_interp E mNew)))%I.
Proof.
revert de ms ms' mNew dv. induction n as [|n IH].
(* Base Case *)
- iIntros (de ms ms' mNew dv Hsp); simplify_eq/=.
- iIntros (de ms ms' mNew dv Hsp Hwf); simplify_eq/=.
destruct de; simplify_option_eq.
iApply denv_stack_interp_intro.
iApply awp_ret. iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
iIntros (? ->). iSplit; eauto. rewrite /denv_interp //.
- iIntros (de ms ms' mNew dv Hsp).
- iIntros (de ms ms' mNew dv Hsp Hwf).
destruct de; simplify_option_eq.
+ iApply denv_stack_interp_intro; iApply awp_ret;
iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
......@@ -541,13 +564,16 @@ Section vcg_spec.
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
unfold popstack in Hsp.
destruct ms2 as [|t ms2'] eqn:Houteq; simplify_eq/=.
iPoseProof (IHn de1 ms) as "Hawp1"; first done.
iPoseProof (IHn (dce_subst E s dv1 de2) (mNew1 :: ms1))
apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
iPoseProof (IH de1 ms) as "Hawp1"; first done. done.
iPoseProof (IH (dce_subst E s dv1 de2) (mNew1 :: ms1))
as "Hawp2"; first done.
apply dce_subst_dcexpr_wf. eapply vcg_sp_dval_wf. eassumption. done.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
assert (Closed (s:b:[]) (dcexpr_interp E de2)). admit.
assert (Closed ( [s]) (dcexpr_interp E de2)).
{ apply dcexpr_closed. apply Hwf2. }
iApply awp_bind.
* exists (λ: s, dcexpr_interp E de2)%V. by unlock.
* iApply (awp_wand with "Hawp1").
......@@ -563,8 +589,8 @@ Section vcg_spec.
as [i|] eqn:Hdl; try apply is_dloc_Some in Hdl as ->; simplify_eq/=.
destruct (denv_delete_frac_2 i ms1 mNew1)
as [[[[ms2 mNew2] q] dv1]|] eqn:Hfar; simplify_eq/=.
specialize (IHn de ms).
iPoseProof IHn as "Hawp"; first done.
specialize (IH de ms).
iPoseProof IH as "Hawp"; first done. done.
iPoseProof denv_delete_frac_2_interp as "Hm"; first eassumption.
iDestruct (denv_stack_interp_trans with "Hawp Hm") as "Hawp'".
iClear "Hawp Hm".
......
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