Commit 166d10aa authored by Léon Gondelman's avatar Léon Gondelman
Browse files

progress on denv_wf

parent 47c2d451
......@@ -29,13 +29,23 @@ Section denv.
Definition penv_to_known_locs : penv known_locs := fmap penv_loc.
Fixpoint denv_wf (E: known_locs) (m: denv) : bool :=
Fixpoint denv_wf_val (E: known_locs) (m: denv) : bool :=
match m with
| [] => true
| Some (DenvItem _ _ dv) :: m' => dval_wf E dv && denv_wf E m'
| None :: m' => denv_wf E m'
| Some (DenvItem _ _ dv) :: m' => dval_wf E dv && denv_wf_val E m'
| None :: m' => denv_wf_val E m'
end.
Fixpoint denv_wf_len (E: known_locs) (m: denv) : bool :=
match E, m with
| _, [] => true
| _ :: E', _ :: m' => denv_wf_len E m'
| [], _ => false
end.
Definition denv_wf (E: known_locs) (m: denv) : bool :=
denv_wf_val E m && denv_wf_len E m.
Definition denv_item_opt_merge
(dio1 dio2 : option denv_item) : option denv_item :=
match dio1, dio2 with
......@@ -666,17 +676,46 @@ Section denv_spec.
- iIntros "[Hm Hms]". rewrite -denv_merge_interp. iFrame. by iApply "IH".
Qed.
(** ** Well-foundness of denv *)
(** ** Well-foundness of denv *)
Lemma denv_wf_len_mono E E' m :
denv_wf_len E m
E `prefix_of`E'
denv_wf_len E' m.
Proof.
revert E. induction m as [| x m']; intros.
- by destruct E'.
- destruct E', E; simplify_eq /=;
[ | by apply prefix_nil_not in H1 | | ]; by eauto.
Qed.
Lemma denv_wf_mono E E' m :
denv_wf E m E `prefix_of` E' denv_wf E' m.
Proof.
rewrite !andb_True.
induction m as [|[denv|] ms]; simpl; eauto.
destruct denv; simpl. intros. destruct_and!.
split_and. eapply dval_wf_mono; eauto. apply IHms; eauto.
Qed.
Lemma denv_wf_merge E m1 m2 :
denv_wf E m1 denv_wf E m2 denv_wf E (denv_merge m1 m2).
- intros [_ Hwf] Hpre; split; first done. by destruct E'.
- destruct denv. intros. destruct_and!.
split_and. rewrite andb_True. split.
eapply dval_wf_mono; eauto.
apply IHms; eauto.
+ split; first done; by destruct E.
+ destruct E, E'; simplify_eq /=; try done;
first by apply prefix_nil_not in H1.
destruct ms; simplify_eq /=; first done.
pose H1.
apply prefix_cons_inv_1 in p.
apply (denv_wf_len_mono (c::E)). done.
rewrite -p in H1. by rewrite -p.
- intros. destruct H0 as [Hwg1 He].
destruct E, E'; try done.
+ by apply prefix_nil_not in H1.
+ by apply IHms.
Qed.
Lemma denv_wf_merge_val (E : known_locs) (m1 m2 : denv) :
denv_wf_val E m1 denv_wf_val E m2 denv_wf_val E (denv_merge m1 m2).
Proof.
revert m2. induction m1 as [|doenv1 ms1]; simpl; intros m2.
- destruct m2; eauto.
......@@ -684,26 +723,60 @@ Section denv_spec.
destruct m2 as [|[denv2|] ms2]; try (destruct denv2); naive_solver.
Qed.
Lemma denv_wf_stack_merge ms E :
Forall (denv_wf E) ms
denv_wf E (denv_stack_merge ms).
Lemma denv_wf_merge_len (E : known_locs) (m1 m2 : denv) :
denv_wf_len E m1
denv_wf_len E m2
denv_wf_len E (denv_merge m1 m2).
Proof. Admitted.
Lemma denv_wf_merge E m1 m2 :
denv_wf E m1 denv_wf E m2 denv_wf E (denv_merge m1 m2).
Proof.
intros Hwf1 Hwf2.
unfold denv_wf in Hwf1; apply andb_True in Hwf1 as [Haux1 Hlen1].
unfold denv_wf in Hwf2; apply andb_True in Hwf2 as [Haux2 Hlen2].
specialize (denv_wf_merge_val E m1 m2 Haux1 Haux2) as Hwf.
specialize (denv_wf_merge_len E m1 m2 Hlen1 Hlen2) as Hlen.
unfold denv_wf. naive_solver.
Qed.
Lemma denv_wf_stack_merge ms E :
Forall (denv_wf E) ms
denv_wf E (denv_stack_merge ms).
Proof.
induction ms as [|m ms]; simpl; eauto.
- intros; unfold denv_wf; by destruct E.
- rewrite Forall_cons =>Hm. destruct Hm as [Hm Hms].
apply denv_wf_merge; eauto.
Qed.
Lemma denv_wf_val_unlock E m :
denv_wf_val E m denv_wf_val E (denv_unlock m).
Proof.
induction m as [|[denv|] ms]; simpl; eauto.
- destruct denv; simpl. intros. destruct_and!.
split_and. eapply dval_wf_mono; eauto. apply IHms; eauto.
Qed.
Lemma denv_wf_len_unlock E m :
denv_wf_len E m denv_wf_len E (denv_unlock m).
Proof.
induction ms as [|m ms]; simpl; eauto.
rewrite Forall_cons =>Hm. destruct Hm as [Hm Hms].
apply denv_wf_merge; eauto.
induction m; destruct E; naive_solver.
Qed.
Lemma denv_wf_unlock E m :
denv_wf E m denv_wf E (denv_unlock m).
Proof.
induction m as [|[denv|] ms]; simpl; eauto.
destruct denv; simpl. intros. destruct_and!.
split_and. eapply dval_wf_mono; eauto. apply IHms; eauto.
intros Hwf.
unfold denv_wf in Hwf; apply andb_True in Hwf as [Haux Hlen].
unfold denv_wf. apply andb_True; split.
by apply denv_wf_val_unlock.
by apply denv_wf_len_unlock.
Qed.
Lemma denv_delete_full_aux_wf E i m m' q dv :
denv_wf E m denv_delete_full_aux i m = Some (m', q, dv)
denv_wf E m' dval_wf E dv.
Lemma denv_delete_full_val_aux_wf E i m m' q dv :
denv_wf_val E m denv_delete_full_aux i m = Some (m', q, dv)
denv_wf_val E m' dval_wf E dv.
Proof.
revert i m'; induction m as [|[di|] m];
intros i m'; simpl; first naive_solver.
......@@ -720,6 +793,23 @@ Section denv_spec.
eapply IHm; eauto.
Qed.
Lemma denv_delete_full_len_aux_wf E i m m' q dv :
denv_wf_len E m denv_delete_full_aux i m = Some (m', q, dv)
denv_wf_len E m'.
Proof. Admitted.
Lemma denv_delete_full_aux_wf E i m m' q dv :
denv_wf E m denv_delete_full_aux i m = Some (m', q, dv)
denv_wf E m' dval_wf E dv.
Proof.
intros Hwf Hdel.
unfold denv_wf in Hwf; apply andb_True in Hwf as [Haux Hlen].
specialize (denv_delete_full_val_aux_wf E i m m' q dv Haux Hdel)
as [Hdel1 Hdel2]. split; last done.
unfold denv_wf. apply andb_True. split; first done.
by eapply denv_delete_full_len_aux_wf.
Qed.
Lemma denv_lookup_wf E i m q dv :
denv_wf E m denv_lookup i m = Some (q, dv) dval_wf E dv.
Proof.
......
......@@ -513,17 +513,22 @@ Section vcg_spec.
Proof.
revert ms ms' mNew dv. induction de;
intros ms ms' mNew dv Hwfms Hwfde Hsp; simplify_eq/=; eauto.
- split; first done. unfold denv_wf. split; last done. apply andb_True. by destruct E.
- destruct (vcg_sp E ms de) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
destruct dv1 as [|?|[i|?]|]; simplify_eq/=.
destruct (denv_delete_frac_2 i ms1 mNew1) as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
destruct (denv_delete_frac_2 i ms1 mNew1)
as [[[[ms2 mNew2] q] dv1]|] eqn:Hout1; simplify_eq/=.
destruct (IHde _ _ _ _ Hwfms Hwfde Hsp1) as (?&?&?).
eapply denv_wf_delete_frac_2 in Hout1; eauto.
destruct Hout1 as (?&?&?).
repeat split; eauto using denv_wf_insert.
- destruct (vcg_sp E ms de1) as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
- destruct (vcg_sp E ms de1)
as [[[ms1 mNew1] dv1]|] eqn:Hsp1; simplify_eq /=.
destruct dv1 as [?|?|[i|?]|]; simplify_eq/=.
destruct (vcg_sp E ms1 de2) as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2)) as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
destruct (vcg_sp E ms1 de2)
as [[[ms2 mNew2] dv2]|] eqn:Hsp2; simplify_eq /=.
destruct (denv_delete_full_2 i ms2 (denv_merge mNew1 mNew2))
as [[[ms3 mNew3] dv1]|] eqn:Hout1; simplify_eq/=.
apply andb_True in Hwfde. destruct Hwfde as [Hwfde1 Hwfde2].
destruct (IHde1 _ _ _ _ Hwfms Hwfde1 Hsp1) as (Hwfms1&HwfNew1&Hwfdv1).
destruct (IHde2 _ _ _ _ Hwfms1 Hwfde2 Hsp2) as (?&?&?).
......@@ -646,8 +651,9 @@ Section vcg_spec.
denv_interp E m -
vcg_wp_bin_op E b dv1 dv2 (denv_merge mOut m) Φ -
denv_interp E mOut -
w : val, cbin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w
vcg_wp_continuation E Φ w.
w : val,
cbin_op_eval b (dval_interp E dv1) (dval_interp E dv2) = Some w
vcg_wp_continuation E Φ w.
Proof.
iIntros (Hpre Hwf1 Hwf2 Hwf3) "Hm Hwp HmOut". rewrite /vcg_wp_bin_op.
destruct (dcbin_op_eval E b dv1 dv2) as [ | dw | dw ] eqn:Hbin.
......
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