Commit 0bc5d071 authored by Léon Gondelman 's avatar Léon Gondelman
Browse files

wip (a simple test work)

parent 14a6fe83
......@@ -243,23 +243,23 @@ Fixpoint dval_wf (E: known_locs) (dv : dval) : bool :=
| _ => true
end.
Fixpoint dexpr_wf (X: list string) (E: known_locs) (de: dexpr) : bool :=
Fixpoint dexpr_wf (E: known_locs) (de: dexpr) : bool :=
match de with
| dEVal dv => dval_wf E dv
| dEVar x => bool_decide (x X)
| dEFst de | dESnd de => dexpr_wf X E de
| dEPair de1 de2 => dexpr_wf X E de1 && dexpr_wf X E de2
| dEVar x => true
| dEFst de | dESnd de => dexpr_wf E de
| dEPair de1 de2 => dexpr_wf E de1 && dexpr_wf E de2
| dEUnknown _ => true
end.
Fixpoint dcexpr_wf (X: list string) (E: known_locs) (de: dcexpr) : bool :=
Fixpoint dcexpr_wf (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
| dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf X E de1
| dCRet de => dexpr_wf E de
| dCBind x de1 de2 => dcexpr_wf E de1 && dcexpr_wf E de2
| dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf E de1
| dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
| dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
dcexpr_wf X E de1 && dcexpr_wf X E de2
dcexpr_wf E de1 && dcexpr_wf E de2
| dCUnknown _ => true
end.
......@@ -279,14 +279,13 @@ Proof.
* specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
Qed.
Lemma dexpr_wf_mono (X: list string) (E E': known_locs) (de: dexpr) :
dexpr_wf X E de E `prefix_of` E' dexpr_wf X E' de.
Lemma dexpr_wf_mono (E E': known_locs) (de: dexpr) :
dexpr_wf E de E `prefix_of` E' dexpr_wf E' de.
Proof. induction de; simplify_eq /=; [apply dval_wf_mono|..]; naive_solver. Qed.
Lemma dcexpr_wf_mono (X: list string) (E E': known_locs) (de: dcexpr) :
dcexpr_wf X E de E `prefix_of` E' dcexpr_wf X E' de.
Lemma dcexpr_wf_mono (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_wf E' de.
Proof.
revert X.
induction de; intros X; simplify_eq /=; [try apply dexpr_wf_mono|..];
naive_solver.
Qed.
......@@ -346,8 +345,8 @@ Proof.
* specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
Qed.
Lemma dexpr_interp_mono (X: list string) (E E': known_locs) (de: dexpr) :
dexpr_wf X E de E `prefix_of` E' dexpr_interp E de = dexpr_interp E' de.
Lemma dexpr_interp_mono (E E': known_locs) (de: dexpr) :
dexpr_wf E de E `prefix_of` E' dexpr_interp E de = dexpr_interp E' de.
Proof.
induction de; simplify_eq /=; intros H Hpre;
try (by rewrite IHde ) ||
......@@ -357,16 +356,16 @@ Proof.
by rewrite (dval_interp_mono E E').
Qed.
Lemma dcexpr_interp_mono (X: list string) (E E': known_locs) (de: dcexpr) :
dcexpr_wf X E de E `prefix_of` E' dcexpr_interp E de = dcexpr_interp E' de.
Lemma dcexpr_interp_mono (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_interp E de = dcexpr_interp E' de.
Proof.
induction de; simplify_eq /=; intros H Hpre;
try (by rewrite IHde ) ||
(apply andb_prop_elim in H as [H1 H2];
rewrite IHde2; [rewrite IHde1; done | done | done ];
by rewrite (IHde1 H1 Hpre (dcexpr_interp E de1))) || eauto.
by rewrite (dexpr_interp_mono X E E').
Admitted.
by rewrite (dexpr_interp_mono E E').
Qed.
(*
Global Instance dexpr_closed E de : Closed [] (dexpr_interp E de).
......@@ -460,13 +459,17 @@ Proof. done. Qed.
(** ** IntoDExpr *)
Class IntoDExpr (E: known_locs) (e: expr) (de: dexpr) :=
{ into_dexpr : e = dexpr_interp E de;
into_dexpr_wf : dexpr_wf [] E de }.
into_dexpr_wf : dexpr_wf E de }.
Global Instance into_dexpr_val E e dv :
ExprIntoDVal E e dv
IntoDExpr E e (dEVal dv) | 5.
Proof. intros [-> ?]; split; auto. Qed.
Global Instance into_dexpr_var E x :
IntoDExpr E (Var x) (dEVar x) | 5.
Proof. split; auto. Qed.
Global Instance into_dexpr_pair E e1 e2 de1 de2 :
IntoDExpr E e1 de1 IntoDExpr E e2 de2
IntoDExpr E (Pair e1 e2) (dEPair de1 de2).
......@@ -489,13 +492,20 @@ Proof. done. Qed.
(** ** IntoDCExpr *)
Class IntoDCExpr (E: known_locs) (e: expr) (de: dcexpr) :=
{ into_dcexpr : e = dcexpr_interp E de;
into_dcexpr_wf : dcexpr_wf [] E de }.
into_dcexpr_wf : dcexpr_wf E de }.
Global Instance into_dcexpr_ret E e de:
IntoDExpr E e de
IntoDCExpr E (a_ret e) (dCRet de).
Proof. intros [-> ?]; split; auto. Qed.
Global Instance into_dcexpr_bind E x e1 e2 de1 de2:
IntoDCExpr E e1 de1
IntoDCExpr E e2 de2
IntoDCExpr E (BNamed x ←ᶜ e1 ;; e2) (dCBind x de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Global Instance into_dcexpr_alloc E e1 e2 de1 de2 :
IntoDCExpr E e1 de1 IntoDCExpr E e2 de2
IntoDCExpr E (a_alloc e1 e2) (dCAlloc de1 de2).
......
......@@ -36,7 +36,7 @@ Section vcg_continue.
denv_wf (penv_to_known_locs Γls) m
envs_entails (Envs Γp Γs_out c)
(vcg_wp E m de R (λ E m dv,
mapsto_wand_list E m (Φ (dval_interp E dv))))
mapsto_wand_list E m (Φ (dval_interp E dv))) 1024 (*TODO: Fix this*))
envs_entails (Envs Γp Γs_in c) (awp e R Φ).
Proof.
intros Hsplit ->.
......
......@@ -55,56 +55,97 @@ Section vcg.
| dEUnknown _ => None
end.
(** substitution *)
Fixpoint de_subst (x: string) (dv : dval) (de: dexpr) : dexpr :=
match de with
| dEVal _ => de
| dEVar y => if decide (x = y) then dEVal dv else de
| dEPair de1 de2 => dEPair (de_subst x dv de1) (de_subst x dv de2)
| dEFst de1 => dEFst (de_subst x dv de1)
| dESnd de1 => dESnd (de_subst x dv de1)
| dEUnknown _ => de
end.
Fixpoint dce_subst (x: string) (dv : dval) (dce : dcexpr) : dcexpr :=
match dce with
| dCRet de1 => dCRet (de_subst x dv de1)
| dCBind y de1 de2 =>
if decide (x = y)
then dCBind y (dce_subst x dv de1) de2
else dCBind y (dce_subst x dv de1) (dce_subst x dv de2)
| dCAlloc de1 de2 => dCAlloc (dce_subst x dv de1) (dce_subst x dv de2)
| dCLoad de1 => dCLoad (dce_subst x dv de1)
| dCStore de1 de2 => dCStore (dce_subst x dv de1) (dce_subst x dv de2)
| dCBinOp op de1 de2 =>
dCBinOp op (dce_subst x dv de1) (dce_subst x dv de2)
| dCPreBinOp op de1 de2 =>
dCPreBinOp op (dce_subst x dv de1) (dce_subst x dv de2)
| dCUnOp op de1 => dCUnOp op (dce_subst x dv de1)
| dCSeq de1 de2 => dCSeq (dce_subst x dv de1) (dce_subst x dv de2)
| dCPar de1 de2 => dCPar (dce_subst x dv de1) (dce_subst x dv de2)
| dCInvoke v de1 => dCInvoke v (dce_subst x dv de1)
| dCUnknown _ => dce
end.
(** Computes the framing for the resources, necessary for the safety of the
expression, and simulatenously computes the strongest postcondition based on that.
See `vcg_sp_correct` and `vcg_sp'_correct`. *)
Fixpoint vcg_sp (E: known_locs) (ms : list denv) (de : dcexpr)
: option (list denv * denv * dval) :=
match de with
| dCRet de => dv vcg_eval_dexpr de; Some (ms, [], dv)
| dCBind _ _ _ => None
| dCLoad de1 =>
''(ms1, mNew, dl) vcg_sp E ms de1;
Fixpoint vcg_sp (E: known_locs) (ms : list denv) (de : dcexpr) (n: nat)
{ struct n }: option (list denv * denv * dval) :=
match de, n with
| dCRet de, _ => dv vcg_eval_dexpr de; Some (ms, [], dv)
| dCBind x de1 de2, S p =>
''(ms1, mNew1, dv1) vcg_sp E ms de1 p;
''(ms2, mNew2, dv2)
vcg_sp E (mNew1 :: ms1) (dce_subst x dv1 de2) p;
''(ms3, mNew3) popstack ms2;
Some (ms3, denv_merge mNew2 mNew3, dv2)
| dCLoad de1, S p =>
''(ms1, mNew, dl) vcg_sp E ms de1 p;
i is_dloc E dl;
''(ms2, mNew2, q, dv) denv_delete_frac_2 i ms1 mNew;
Some (ms2, denv_insert i ULvl q dv mNew2, dv)
| dCStore de1 de2 =>
''(ms1, mNew1, dl) vcg_sp E ms de1;
| dCStore de1 de2, S p =>
''(ms1, mNew1, dl) vcg_sp E ms de1 p;
i is_dloc E dl;
''(ms2, mNew2, dv) vcg_sp E ms1 de2;
''(ms2, mNew2, dv) vcg_sp E ms1 de2 p;
''(ms3, mNew3, _) denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
Some (ms3, denv_insert i LLvl 1 dv mNew3, dv)
| dCBinOp op de1 de2 =>
''(ms1, mNew1, dv1) vcg_sp E ms de1;
''(ms2, mNew2, dv2) vcg_sp E ms1 de2;
| dCBinOp op de1 de2, S p =>
''(ms1, mNew1, dv1) vcg_sp E ms de1 p;
''(ms2, mNew2, dv2) vcg_sp E ms1 de2 p;
dv dcbin_op_eval E op dv1 dv2;
Some (ms2, denv_merge mNew1 mNew2, dv)
| dCPreBinOp op de1 de2 =>
''(ms1, mNew1, dl) vcg_sp E ms de1;
| dCPreBinOp op de1 de2, S p =>
''(ms1, mNew1, dl) vcg_sp E ms de1 p;
i is_dloc E dl;
''(ms2, mNew2, dv2) vcg_sp E ms1 de2;
''(ms2, mNew2, dv2) vcg_sp E ms1 de2 p;
''(ms3, mNew3, dv) denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2);
dv3 dcbin_op_eval E op dv dv2;
Some (ms3, denv_insert i LLvl 1 dv3 mNew3, dv)
| dCUnOp op de =>
''(ms1, mNew1, dv) vcg_sp E ms de;
| dCUnOp op de, S p =>
''(ms1, mNew1, dv) vcg_sp E ms de p ;
dv' dun_op_eval E op dv;
Some (ms1, mNew1, dv')
| dCSeq de1 de2 =>
''(ms1, mNew1, _) vcg_sp E ms de1;
''(ms2, mNew2, dv2) vcg_sp E (denv_unlock mNew1 :: ms1) de2;
| dCSeq de1 de2, S p =>
''(ms1, mNew1, _) vcg_sp E ms de1 p;
''(ms2, mNew2, dv2) vcg_sp E (denv_unlock mNew1 :: ms1) de2 p;
''(ms3, mNew3) popstack ms2;
Some (ms3, denv_merge mNew2 mNew3, dv2)
| dCPar de1 de2 =>
''(ms1, mNew1, dv1) vcg_sp E ms de1;
''(ms2, mNew2, dv2) vcg_sp E ms1 de2;
| dCPar de1 de2, S p =>
''(ms1, mNew1, dv1) vcg_sp E ms de1 p;
''(ms2, mNew2, dv2) vcg_sp E ms1 de2 p;
Some (ms2, denv_merge mNew1 mNew2, (dPairV dv1 dv2))
| dCAlloc _ _ | dCUnknown _ | dCInvoke _ _ => None
| dCAlloc _ _, _ | dCUnknown _, _ | dCInvoke _ _, _ => None
| _, O => None
end.
Definition vcg_sp'
(E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) :=
''(ms,mNew,dv) vcg_sp E [m] de;
''(ms,mNew,dv) vcg_sp E [m] de 1024
(*TODO: add some better measure than a constant :) *);
''(_, m') popstack ms;
Some (m', mNew, dv).
Global Arguments vcg_sp' _ _ !_ /.
......@@ -215,89 +256,105 @@ Section vcg.
(cl C[LLvl] w - vcg_wp_continuation E Φ v))
end%I.
Definition vcg_wp_bind (E : known_locs) (dv: dval) (m : denv)
(Φ : known_locs denv dval iProp Σ) : iProp Σ :=
mapsto_wand_list E m (vcg_wp_continuation E Φ ((dval_interp E dv)))%I.
Fixpoint vcg_wp (E : known_locs) (m : denv) (de : dcexpr)
(R : iProp Σ) (Φ : known_locs denv dval iProp Σ) : iProp Σ :=
match de with
| dCRet de' =>
(R : iProp Σ) (Φ : known_locs denv dval iProp Σ) (n: nat) {struct n}: iProp Σ :=
match de, n with
| dCRet de', _ =>
match vcg_eval_dexpr de' with
| Some dv => Φ E m dv
| None => vcg_wp_awp_continuation R E de m Φ
end
| dCAlloc de1 de2 =>
| dCBind x de1 de2, S p =>
match vcg_sp' E m de1 with
| Some (m', mNew, dv1) =>
vcg_wp E m' (dce_subst x dv1 de2) R (λ E m'' dv2,
vcg_wp_bind E dv2 (denv_merge mNew m'') Φ) p
| None =>
vcg_wp E m de1 R (λ E m' dv1,
vcg_wp E m' (dce_subst x dv1 de2) R (λ E m'' dv2,
vcg_wp_bind E dv2 m'' Φ) p) p
end
| dCAlloc de1 de2, S p =>
match vcg_sp' E m de1 with
| Some (m', mNew, dv1) =>
vcg_wp E m' de2 R (λ E m'' dv2,
vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ)
vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ) p
| None =>
match vcg_sp' E m de2 with
| Some (m', mNew, dv2) =>
vcg_wp E m' de1 R (λ E m'' dv1,
vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ)
vcg_wp_alloc E dv1 dv2 (denv_merge mNew m'') Φ) p
| None => vcg_wp_awp_continuation R E de m Φ
end
end
| dCLoad de1 =>
vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' Φ)
| dCStore de1 de2 =>
| dCLoad de1, S p =>
vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' Φ) p
| dCStore de1 de2, S p =>
match vcg_sp' E m de1 with
| Some (m', mNew, dv1) =>
vcg_wp E m' de2 R (λ E m'' dv2,
vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ)
vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ) p
| None =>
match vcg_sp' E m de2 with
| Some (m', mNew, dv2) =>
vcg_wp E m' de1 R (λ E m'' dv1,
vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ)
vcg_wp_store E dv1 dv2 (denv_merge mNew m'') Φ) p
| None => vcg_wp_awp_continuation R E de m Φ
end
end
| dCBinOp op de1 de2 =>
| dCBinOp op de1 de2, S p =>
match vcg_sp' E m de1 with
| Some (m', mNew, dv1) =>
vcg_wp E m' de2 R (λ E m'' dv2,
vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
| None =>
match vcg_sp' E m de2 with
| Some (m', mNew, dv2) =>
vcg_wp E m' de1 R (λ E m'' dv1,
vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
| None => vcg_wp_awp_continuation R E de m Φ
end
end
| dCPreBinOp op de1 de2 =>
| dCPreBinOp op de1 de2, S p =>
match vcg_sp' E m de1 with
| Some (m', mNew, dv1) =>
vcg_wp E m' de2 R (λ E m'' dv2,
vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
| None =>
match vcg_sp' E m de2 with
| Some (m', mNew, dv2) =>
vcg_wp E m' de1 R (λ E m'' dv1,
vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ)
vcg_wp_pre_bin_op E op dv1 dv2 (denv_merge mNew m'') Φ) p
| None => vcg_wp_awp_continuation R E de m Φ
end
end
| dCUnOp op de => vcg_wp E m de R (λ E m dv, vcg_wp_un_op E op dv m Φ)
| dCSeq de1 de2 =>
| dCUnOp op de, S p => vcg_wp E m de R (λ E m dv, vcg_wp_un_op E op dv m Φ) p
| dCSeq de1 de2, S p =>
vcg_wp E m de1 R (λ E m _,
U (vcg_wp E (denv_unlock m) de2 R Φ))
| dCPar de1 de2 =>
U (vcg_wp E (denv_unlock m) de2 R Φ p)) p
| dCPar de1 de2, S p =>
match vcg_sp' E m de1 with
| Some (m', mNew, dv1) =>
vcg_wp E m' de2 R (λ E m'' dv2,
(Φ E (denv_merge mNew m'') (dPairV dv1 dv2)))
(Φ E (denv_merge mNew m'') (dPairV dv1 dv2))) p
| None =>
match vcg_sp' E m de2 with
| Some (m', mNew, dv2) =>
vcg_wp E m' de1 R (λ E m'' dv1,
(Φ E (denv_merge mNew m'') (dPairV dv1 dv2)))
(Φ E (denv_merge mNew m'') (dPairV dv1 dv2))) p
| None => vcg_wp_awp_continuation R E de m Φ
end
end
| dCInvoke ef de1 => vcg_wp E m de1 R (λ E m dv,
| 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 Φ)
| _ => vcg_wp_awp_continuation R E de m Φ
(dCUnknown (ef (dval_interp E dv))) m Φ) p
| _, S p => vcg_wp_awp_continuation R E de m Φ
| _, O => False
end%I.
End vcg.
......@@ -329,11 +386,12 @@ Section vcg_spec.
iIntros "H1 H2". iApply (mapsto_wand_list_aux_spec with "H1 H2").
Qed.
Lemma vcg_sp_length E de ms ms' mNew dv :
vcg_sp E ms de = Some (ms', mNew, dv)
Lemma vcg_sp_length E de ms ms' mNew dv n:
vcg_sp E ms de n = Some (ms', mNew, dv)
length ms = length ms'.
Proof.
revert ms ms' mNew dv. induction de;
Admitted.
(* revert ms ms' mNew dv. induction de;
intros ms ms' mNew dv Hsp; simplify_eq/=; eauto.
- by simplify_option_eq.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hout; simplify_eq /=.
......@@ -378,7 +436,7 @@ Section vcg_spec.
destruct (vcg_sp E ms1 de2)
as [[[ms2 mNew2] dv2]|] eqn:Hde2; simplify_eq/=.
transitivity (length ms1); eauto.
Qed.
Qed. *)
Lemma vcg_eval_dexpr_correct E de dv :
vcg_eval_dexpr de = Some dv
......@@ -404,7 +462,7 @@ Section vcg_spec.
Lemma vcg_eval_dexpr_wf E de dv :
vcg_eval_dexpr de = Some dv
dexpr_wf [] E de dval_wf E dv.
dexpr_wf E de dval_wf E dv.
Proof.
generalize dependent dv. induction de; intros dv Hdv; simplify_eq/=; eauto.
- simplify_option_eq. naive_solver.
......@@ -419,12 +477,13 @@ Section vcg_spec.
(* THIS IS UGLY AF ^ *) simpl in IHde.
destruct_and!. auto.
Qed.
Lemma vcg_sp_correct' E de ms ms' mNew dv R :
vcg_sp E ms de = Some (ms', mNew, dv)
Lemma vcg_sp_correct' E de ms ms' mNew dv R n :
vcg_sp E ms de n = Some (ms', mNew, dv)
(denv_stack_interp ms ms' E
(awp (dcexpr_interp E de) R
(λ v, v = dval_interp E dv denv_interp E mNew)))%I.
Proof.
Admitted. (*
revert ms ms' mNew dv. induction de;
iIntros (ms ms' mNew dv Hsp); simplify_eq/=.
- simplify_option_eq.
......@@ -531,7 +590,7 @@ Section vcg_spec.
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply a_sequence_spec'.
Admitted. (* iNext. iApply (awp_wand with "Hawp1").
iNext. iApply (awp_wand with "Hawp1").
iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
rewrite (denv_unlock_interp E mNew1).
iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
......@@ -552,8 +611,8 @@ Section vcg_spec.
rewrite -denv_merge_interp. iFrame.
Qed. *)
Lemma vcg_sp_correct E de m ms mNew dv R :
vcg_sp E [m] de = Some (ms, mNew, dv)
Lemma vcg_sp_correct E de m ms mNew dv R n:
vcg_sp E [m] de n = Some (ms, mNew, dv)
denv_interp E m -
denv_interp E (denv_stack_merge ms)
awp (dcexpr_interp E de) R
......@@ -561,7 +620,7 @@ Section vcg_spec.
Proof.
iIntros (Hsp) "Hm".
iPoseProof vcg_sp_correct' as "Hawp"; first eassumption.
pose (vcg_sp_length _ _ _ _ _ _ Hsp) as Hlen.
pose (vcg_sp_length _ _ _ _ _ _ _ Hsp) as Hlen.
assert ( m', ms = [m']) as [m' ->]=>/=.
{ destruct ms as [|m' [|m'' ms'']]; eauto; inversion Hlen. }
rewrite denv_merge_nil_r. iDestruct ("Hawp" with "Hm") as "[$ $]".
......@@ -573,8 +632,8 @@ Section vcg_spec.
denv_interp E m'
awp (dcexpr_interp E de) R
(λ v, v = dval_interp E dv denv_interp E mNew).
Proof.
rewrite /vcg_sp'.
Proof. Admitted.
(* rewrite /vcg_sp'.
iIntros (Hsp') "Hm".
destruct (vcg_sp E [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq/=.
destruct ms as [|?m' ms]; simplify_eq/=.
......@@ -582,15 +641,15 @@ Section vcg_spec.
assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen).
rewrite vcg_sp_correct; last eassumption. simpl.
rewrite denv_merge_nil_r. iFrame.
Qed.
Qed. *)
Lemma vcg_sp_wf' E de ms ms' mNew dv :
Lemma vcg_sp_wf' E de ms ms' mNew dv n:
Forall (denv_wf E) ms
dcexpr_wf [] E de
vcg_sp E ms de = Some (ms', mNew, dv)
dcexpr_wf E de
vcg_sp E ms de n = Some (ms', mNew, dv)
Forall (denv_wf E) ms' denv_wf E mNew dval_wf E dv .
Proof.
revert ms ms' mNew dv. induction de;
Proof. Admitted.
(* revert ms ms' mNew dv. induction de;
intros ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
- simplify_option_eq. split_and?; auto; first by destruct E.
by eapply vcg_eval_dexpr_wf.
......@@ -666,15 +725,15 @@ Section vcg_spec.
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
repeat split; eauto. apply denv_wf_merge; eauto.
Qed.
Qed. *)
Lemma vcg_sp'_wf E de m m' mNew dv :
denv_wf E m
dcexpr_wf [] E de
dcexpr_wf E de
vcg_sp' E m de = Some (m', mNew, dv)
denv_wf E m' denv_wf E mNew dval_wf E dv .
Proof.
rewrite /vcg_sp'. intros Hm Hde Hsp'.
Proof. Admitted.
(* rewrite /vcg_sp'. intros Hm Hde Hsp'.
assert (Forall (denv_wf E) [m]) as Hms by (econstructor; eauto).
destruct (vcg_sp E [m] de) as [[[ms ?mNew] ?dv]|] eqn:Hsp; simplify_eq/=.
destruct ms as [|?m' ms]; simplify_eq/=.
......@@ -682,7 +741,7 @@ Section vcg_spec.
assert (ms = []) as -> by (destruct ms; eauto; inversion Hlen).
destruct (vcg_sp_wf' E de [m] [m'] mNew _ Hms Hde Hsp) as (Hm'&?&?).
repeat split; eauto. by inversion Hm'.
Qed.
Qed. *)
Lemma vcg_wp_awp_continuation_correct R E m de Φ :
denv_wf E m
......@@ -842,10 +901,10 @@ Section vcg_spec.
Qed.
Lemma vcg_wp_correct R E m de Φ :
dcexpr_wf [] E de
dcexpr_wf E de
denv_wf E m
denv_interp E m -
vcg_wp E m de R Φ -
vcg_wp E m de R Φ 1024 (*TODO: Fix this *) -
awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ).
Proof.
Admitted. (*
......@@ -1078,3 +1137,4 @@ Arguments vcg_wp_store _ _ _ _ _ _ _ /.
Arguments vcg_wp_bin_op _ _ _ _ _ _ _ _ /.
Arguments vcg_wp_un_op _ _ _ _ _ _ _ /.
Arguments vcg_wp_pre_bin_op _ _ _ _ _ _ _ _ /.
Arguments vcg_wp_bind _ _ _ _ _ _ /.
\ No newline at end of file