Commit 14a6fe83 authored by Léon Gondelman 's avatar Léon Gondelman

wip

parent 4f047167
......@@ -180,6 +180,7 @@ Qed.
(** Dexpr *)
Inductive dexpr : Type :=
| dEVal : dval dexpr
| dEVar : string dexpr
| dEPair : dexpr dexpr dexpr
| dEFst : dexpr dexpr
| dESnd : dexpr dexpr
......@@ -188,6 +189,7 @@ Inductive dexpr : Type :=
Fixpoint dexpr_interp (E: known_locs) (de: dexpr) : expr :=
match de with
| dEVal dv => dval_interp E dv
| dEVar x => Var x
| dEPair de1 de2 => (dexpr_interp E de1, dexpr_interp E de2)
| dEFst de => Fst (dexpr_interp E de)
| dESnd de => Snd (dexpr_interp E de)
......@@ -197,6 +199,7 @@ Fixpoint dexpr_interp (E: known_locs) (de: dexpr) : expr :=
(** DCexpr *)
Inductive dcexpr : Type :=
| dCRet : dexpr dcexpr
| dCBind : string dcexpr dcexpr dcexpr
| dCAlloc : dcexpr dcexpr dcexpr
| dCLoad : dcexpr dcexpr
| dCStore : dcexpr dcexpr dcexpr
......@@ -211,6 +214,7 @@ Inductive dcexpr : Type :=
Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
match de with
| dCRet de => a_ret (dexpr_interp E de)
| dCBind x de1 de2 => x ←ᶜ (dcexpr_interp E de1) ;; (dcexpr_interp E de2)
| dCAlloc de1 de2 => a_alloc (dcexpr_interp E de1) (dcexpr_interp E de2)
| dCLoad de1 => a_load (dcexpr_interp E de1)
| dCStore de1 de2 => a_store (dcexpr_interp E de1) (dcexpr_interp E de2)
......@@ -239,21 +243,23 @@ Fixpoint dval_wf (E: known_locs) (dv : dval) : bool :=
| _ => true
end.
Fixpoint dexpr_wf (E: known_locs) (de: dexpr) : bool :=
Fixpoint dexpr_wf (X: list string) (E: known_locs) (de: dexpr) : bool :=
match de with
| dEVal dv => dval_wf E dv
| dEFst de | dESnd de => dexpr_wf E de
| dEPair de1 de2 => dexpr_wf E de1 && dexpr_wf E de2
| 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
| dEUnknown _ => true
end.
Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
Fixpoint dcexpr_wf (X: list string) (E: known_locs) (de: dcexpr) : bool :=
match de with
| dCRet de => dexpr_wf E de
| dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf E de1
| 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
| dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
| dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
dcexpr_wf E de1 && dcexpr_wf E de2
dcexpr_wf X E de1 && dcexpr_wf X E de2
| dCUnknown _ => true
end.
......@@ -273,13 +279,17 @@ Proof.
* specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
Qed.
Lemma dexpr_wf_mono (E E': known_locs) (de: dexpr) :
dexpr_wf E de E `prefix_of` E' dexpr_wf E' de.
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.
Proof. induction de; simplify_eq /=; [apply dval_wf_mono|..]; naive_solver. Qed.
Lemma dcexpr_wf_mono (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_wf E' de.
Proof. induction de; simplify_eq /=; [apply dexpr_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.
Proof.
revert X.
induction de; intros X; simplify_eq /=; [try apply dexpr_wf_mono|..];
naive_solver.
Qed.
Lemma dun_op_eval_Some_wf E dv u dw:
dval_wf E dv dun_op_eval E u dv = Some dw dval_wf E dw.
......@@ -336,8 +346,8 @@ Proof.
* specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
Qed.
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.
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.
Proof.
induction de; simplify_eq /=; intros H Hpre;
try (by rewrite IHde ) ||
......@@ -347,17 +357,18 @@ Proof.
by rewrite (dval_interp_mono E E').
Qed.
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.
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.
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 E E').
Qed.
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.
......@@ -366,6 +377,7 @@ Proof.
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 *)
......@@ -448,7 +460,7 @@ 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
......@@ -477,7 +489,7 @@ 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
......
......@@ -35,6 +35,7 @@ Section vcg.
Fixpoint vcg_eval_dexpr (de : dexpr) : option dval :=
match de with
| dEVal dv => Some dv
| dEVar x => None
| dEPair de1 de2 =>
dv1 vcg_eval_dexpr de1;
dv2 vcg_eval_dexpr de2;
......@@ -61,6 +62,7 @@ Section vcg.
: 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;
i is_dloc E dl;
......@@ -402,7 +404,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.
......@@ -417,7 +419,6 @@ 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)
(denv_stack_interp ms ms' E
......@@ -529,7 +530,8 @@ Section vcg_spec.
iDestruct (denv_stack_interp_trans with "Hawp1 Hawp2") as "Hawp".
iClear "Hawp1 Hawp2".
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply a_sequence_spec'. iNext. iApply (awp_wand with "Hawp1").
iApply a_sequence_spec'.
Admitted. (* 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]".
......@@ -548,7 +550,7 @@ Section vcg_spec.
iNext. iIntros (? ?) "[% HmNew1] [% HmNew2] !>";
simplify_eq/=; iSplit; eauto.
rewrite -denv_merge_interp. iFrame.
Qed.
Qed. *)
Lemma vcg_sp_correct E de m ms mNew dv R :
vcg_sp E [m] de = Some (ms, mNew, dv)
......@@ -584,7 +586,7 @@ Section vcg_spec.
Lemma vcg_sp_wf' E de ms ms' mNew dv :
Forall (denv_wf E) ms
dcexpr_wf E de
dcexpr_wf [] E de
vcg_sp E ms de = Some (ms', mNew, dv)
Forall (denv_wf E) ms' denv_wf E mNew dval_wf E dv .
Proof.
......@@ -668,7 +670,7 @@ Section vcg_spec.
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.
......@@ -840,12 +842,13 @@ 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 Φ -
awp (dcexpr_interp E de) R (vcg_wp_continuation E Φ).
Proof.
Admitted. (*
revert Φ E m. induction de; intros Φ E m Hwf; iIntros (Hmwf) "Hm Hwp".
- simpl. case_match.
+ iApply awp_ret. iApply wp_wand; first by iApply vcg_eval_dexpr_correct.
......@@ -1065,7 +1068,7 @@ Section vcg_spec.
rewrite (vcg_wp_continuation_mono E) //.
iFrame.
- by iApply (vcg_wp_awp_continuation_correct with "Hm Hwp").
Qed.
Qed.*)
End vcg_spec.
Arguments vcg_wp_awp_continuation _ _ _ _ _ _ _ /.
......
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