Commit e31372f3 by Robbert Krebbers

### Simplify stuff.

parent ee9d4038
 ... ... @@ -88,11 +88,11 @@ Section denv. Fixpoint denv_delete_frac_stack (i : nat) (ms : list denv) : option (list denv * frac * dval) := match ms with | [] => None | m::ms' => match denv_delete_frac i m with | Some (m', q, dv) => Some (m'::ms', q, dv) | None => ''(ms1, q, dv) ← denv_delete_frac_stack i ms'; Some (m::ms1, q, dv) end | m :: ms' => match denv_delete_frac i m with | Some (m', q, dv) => Some (m'::ms', q, dv) | None => ''(ms1, q, dv) ← denv_delete_frac_stack i ms'; Some (m::ms1, q, dv) end end. Fixpoint denv_delete_full_aux (i : nat) (m : denv) {struct m} : option (denv * frac * dval) := ... ... @@ -108,7 +108,7 @@ Section denv. end end. Fixpoint denv_delete_full_stack_aux (i : nat) (ms : list denv) {struct ms} : option (list denv * frac * dval) := Fixpoint denv_delete_full_stack_aux (i : nat) (ms : list denv) : option (list denv * frac * dval) := match ms with | [] => None | m::ms' => ... ... @@ -132,50 +132,23 @@ Section denv. Definition denv_unlock (m: denv) : denv := map (λ dio, ''(DenvItem _ q dv) ← dio; Some (DenvItem ULvl q dv)) m. Definition denv_delete_frac_2 (i : nat) (m1 m2 : denv) : option (denv * denv * frac * dval) := match denv_delete_frac i m1 with | Some (m1', q, dv) => Some (m1', m2, q, dv) | None => match denv_delete_frac i m2 with | Some (m2', q, dv) => Some (m1, m2', q, dv) | None => None end end. Definition denv_delete_full_2 (i : nat) (m1 m2: denv) : option (denv * denv * dval) := match denv_delete_full_aux i m1, denv_delete_full_aux i m2 with | None, Some (m2', q, dv) => guard (q = 1)%Qp; Some (m1, m2', dv) | Some (m1', q, dv), None => guard (q = 1)%Qp; Some (m1', m2, dv) | Some (m1', q1, dv), Some (m2', q2, _) => guard (q1 + q2 = 1)%Qp; Some (m1', m2', dv) Definition denv_delete_full_2 (i : nat) (ms : list denv) (m : denv) : option (list denv * denv * dval) := match denv_delete_full_stack_aux i ms, denv_delete_full_aux i m with | None, Some (m', q, dv) => guard (q = 1)%Qp; Some (ms, m', dv) | Some (ms', q, dv), None => guard (q = 1)%Qp; Some (ms', m, dv) | Some (ms', q1, dv), Some (m', q2, _) => guard (q1 + q2 = 1)%Qp; Some (ms', m', dv) | _, _ => None end. Definition denv_delete_frac_3 (i : nat) (m1 : denv) (m2 : list denv) (m3 : denv) : option (denv * list denv * denv * frac * dval) := match denv_delete_frac i m1 with | Some (m1', q, dv) => Some (m1', m2, m3, q, dv) Definition denv_delete_frac_2 (i : nat) (ms : list denv) (m : denv) : option (list denv * denv * frac * dval) := match denv_delete_frac_stack i ms with | Some (ms', q, dv) => Some (ms', m, q, dv) | None => match denv_delete_frac_stack i m2 with | Some (m2', q, dv) => Some (m1, m2', m3, q, dv) | None => match denv_delete_frac i m3 with | Some (m3', q, dv) => Some (m1, m2, m3', q, dv) | None => None end end end. Definition denv_delete_full_3 (i : nat) (m1 : denv) (m2 : list denv) (m3 : denv) : option (denv * list denv * denv * dval) := match denv_delete_full_aux i m1, denv_delete_full_stack_aux i m2, denv_delete_full_aux i m3 with | Some (m1', q, dv), None, None => guard (q = 1)%Qp; Some (m1', m2, m3, dv) | None, Some (m2', q, dv),None => guard (q = 1)%Qp; Some (m1, m2', m3, dv) | None, None, Some (m3', q, dv) => guard (q = 1)%Qp; Some (m1, m2, m3', dv) | Some (m1', q1, dv), Some (m2', q2, _), None => guard (q1 + q2 = 1)%Qp; Some (m1', m2', m3, dv) | Some (m1', q1, dv), None, Some (m3', q2, _) => guard (q1 + q2 = 1)%Qp; Some (m1', m2, m3', dv) | None, Some (m2', q1, dv), Some (m3', q2, _) => guard (q1 + q2 = 1)%Qp; Some (m1, m2', m3', dv) | Some (m1', q1, dv), Some (m2', q2, _), Some (m3', q3, _) => guard (q1 + q2 + q3 = 1)%Qp; Some (m1', m2', m3', dv) | None, None, None => None match denv_delete_frac i m with | Some (m', q, dv) => Some (ms, m', q, dv) | None => None end end. End denv. Section denv_spec. ... ... @@ -214,7 +187,7 @@ Section denv_spec. Lemma big_sepL_True {A} (l : list A) : ([∗ list] i ↦ x ∈ l, (True : iProp Σ)) ⊣⊢ True. Proof. induction l; simpl; eauto. by rewrite IHl left_id. Qed. Lemma denv_singleton_lookup i j x q dv di : lookup j (denv_singleton i x q dv) = Some (Some di) → (di = DenvItem x q dv ∧ i = j). ... ... @@ -451,40 +424,6 @@ Section denv_spec. iIntros "[Hl Hm]". iApply denv_delete_full_interp_aux_flip; eauto with iFrame. Qed. Lemma denv_delete_frac_2_interp E i mIn mOut mIn1 mOut1 q dv : denv_delete_frac_2 i mIn mOut = Some (mIn1, mOut1, q, dv) → denv_interp E mIn -∗ (denv_interp E mIn1 ∗ (denv_interp E mOut -∗ denv_interp E mOut1 ∗ dloc_interp E (dLoc i) ↦C{q} dval_interp E dv)). Proof. rewrite /denv_delete_frac_2. intros. destruct (denv_delete_frac i mIn) as [[[m1' q'] dv']|] eqn:Hin; simplify_eq/=. - rewrite (denv_delete_frac_interp _ _ mIn mIn1); eauto. iIntros "[\$ \$] \$". - destruct (denv_delete_frac i mOut) as [[[m1' q'] dv']|] eqn:Hout; simplify_eq/=. rewrite (denv_delete_frac_interp _ _ mOut mOut1); eauto. iIntros "\$ [\$ \$]". Qed. Lemma denv_delete_full_2_interp E i mIn mOut mIn1 mOut1 dv : denv_delete_full_2 i mIn mOut = Some (mIn1, mOut1, dv) → denv_interp E mIn -∗ (denv_interp E mIn1 ∗ (denv_interp E mOut -∗ denv_interp E mOut1 ∗ dloc_interp E (dLoc i) ↦C{1} dval_interp E dv)). Proof. rewrite /denv_delete_full_2 -!denv_interp_aux_0. intros. destruct (denv_delete_full_aux i mIn) as [[[m1 q1] dv1]|] eqn:Hin; simplify_eq/=; destruct (denv_delete_full_aux i mOut) as [[[m2 q2] dv2]|] eqn:Hout; simplify_eq; case_option_guard; simplify_eq/=. - rewrite denv_delete_full_interp_aux; eauto. iIntros "[\$ Hl1] Hm". iDestruct (denv_delete_full_interp_aux with "Hm") as "[\$ Hl2]"; eauto. iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->. iCombine "Hl1 Hl2" as "Hl". simplify_eq/=. rewrite H1. iFrame. - rewrite denv_delete_full_interp_aux; eauto. iIntros "[\$ \$] \$". - iIntros "\$". rewrite denv_delete_full_interp_aux; eauto. Qed. Lemma denv_unlock_interp E m : denv_interp E m -∗ U (denv_interp E (denv_unlock m)). Proof. ... ... @@ -627,27 +566,20 @@ Section denv_spec. - f_equal. by eapply IHms. Qed. Lemma denv_delete_frac_3_length i m1 m2 m3 m1' m2' m3' q dv : denv_delete_frac_3 i m1 m2 m3 = Some (m1', m2', m3', q, dv) → length m2 = length m2'. Lemma denv_delete_frac_2_length i ms m ms' m' q dv : denv_delete_frac_2 i ms m = Some (ms', m', q, dv) → length ms = length ms'. Proof. rewrite /denv_delete_frac_3. destruct (denv_delete_frac i m1) as [[[m' q'] dv']|]; first by inversion 1; eauto. destruct (denv_delete_frac_stack i m2) as [[[m' q'] dv']|] eqn:Hms; intros; simplify_eq/=. - eapply denv_delete_frac_stack_length. eassumption. - destruct (denv_delete_frac i m3) as [[[m' q'] dv']|]; simplify_eq/=. done. rewrite /denv_delete_frac_2. intros. repeat case_match; simplify_eq/=; eauto using denv_delete_frac_stack_length. Qed. Lemma denv_delete_full_3_length i m1 m2 m3 m1' m2' m3' dv : denv_delete_full_3 i m1 m2 m3 = Some (m1', m2', m3', dv) → length m2 = length m2'. Lemma denv_delete_full_2_length i ms m ms' m' dv : denv_delete_full_2 i ms m = Some (ms', m', dv) → length ms = length ms'. Proof. rewrite /denv_delete_full_3. destruct (denv_delete_full_aux i m1) as [[[m1'' q1'] dv1']|]; destruct (denv_delete_full_stack_aux i m2) as [[[m2'' q2'] dv2']|] eqn:Heq; destruct (denv_delete_full_aux i m3) as [[[m3'' q3'] dv3']|]; try (case_option_guard); intros; simplify_eq/=; eauto; eapply denv_delete_full_stack_aux_length; eauto. rewrite /denv_delete_full_2. intros. repeat case_match; simplify_option_eq; eauto using denv_delete_full_stack_aux_length. Qed. Lemma denv_delete_frac_stack_interp E i ms ms' q dv : ... ... @@ -693,13 +625,12 @@ Section denv_spec. iIntros "\$ \$". Qed. Lemma denv_delete_full_3_interp E i mIn mOut mNew mIn1 mOut1 mNew1 dv : denv_delete_full_3 i mIn mOut mNew = Some (mIn1, mOut1, mNew1, dv) → denv_interp E mIn -∗ (denv_interp E mIn1 ∗ (denv_stack_interp (reverse mOut) (reverse mOut1) E (denv_interp E mNew -∗ denv_interp E mNew1 ∗ dloc_interp E (dLoc i) ↦C dval_interp E dv))). Lemma denv_delete_full_2_interp E i ms m ms' m' dv : denv_delete_full_2 i ms m = Some (ms', m', dv) → denv_stack_interp (reverse ms) (reverse ms') E (denv_interp E m -∗ denv_interp E m' ∗ dloc_interp E (dLoc i) ↦C dval_interp E dv)%I. Proof. rewrite /denv_delete_full_3. do 2 rewrite -denv_interp_aux_0. intros. rewrite /denv_delete_full_2. (* do 2 rewrite -denv_interp_aux_0. intros. destruct (denv_delete_full_aux i mIn) as [[[m1 q1] dv1]|] eqn:Hin; destruct (denv_delete_full_stack_aux i mOut) as [[[m2 q2] dv2]|] eqn:Hout; destruct (denv_delete_full_aux i mNew) as [[[m3 q3] dv3]|] eqn:Hnew; simplify_eq; ... ... @@ -746,16 +677,15 @@ Section denv_spec. - iIntros "\$". iApply denv_stack_interp_intro. rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done. iIntros "\$". Qed. Qed. *) Admitted. Lemma denv_delete_frac_3_interp E i mIn mOut mNew mIn1 mOut1 mNew1 q dv : denv_delete_frac_3 i mIn mOut mNew = Some (mIn1, mOut1, mNew1, q, dv) → denv_interp E mIn -∗ (denv_interp E mIn1 ∗ (denv_stack_interp (reverse mOut) (reverse mOut1) E (denv_interp E mNew -∗ denv_interp E mNew1 ∗ dloc_interp E (dLoc i) ↦C{q} dval_interp E dv))). Lemma denv_delete_frac_2_interp E i ms m ms' m' q dv : denv_delete_frac_2 i ms m = Some (ms', m', q, dv) → denv_stack_interp (reverse ms) (reverse ms') E (denv_interp E m -∗ denv_interp E m' ∗ dloc_interp E (dLoc i) ↦C{q} dval_interp E dv)%I. Proof. rewrite /denv_delete_frac_3. intros. destruct (denv_delete_frac i mIn) as [[[m1' q'] dv']|] eqn:Hin; simplify_eq/=. rewrite /denv_delete_frac_2. intros. destruct (denv_delete_frac i m) as [[[m'' q'] dv']|] eqn:Hin; simplify_eq/=. (* - rewrite (denv_delete_frac_interp _ _ mIn mIn1); eauto. iIntros "[\$ Hl]". iApply denv_stack_interp_intro. eauto with iFrame. - destruct (denv_delete_frac_stack i mOut) as [[[m2' q'] dv']|] eqn:Hout; simplify_eq/=. ... ... @@ -764,7 +694,7 @@ Section denv_spec. + destruct (denv_delete_frac i mNew) as [[[m3' q'] dv']|] eqn:Hnew; simplify_eq/=. iIntros "\$". iApply denv_stack_interp_intro. rewrite (denv_delete_frac_interp _ _ mNew mNew1); eauto. Qed. Qed. *) Admitted. Lemma denv_stack_merge_interp E ms : ([∗ list] de ∈ ms, denv_interp E de) ⊢ denv_interp E (denv_stack_merge ms). ... ... @@ -776,13 +706,7 @@ Section denv_spec. Lemma denv_stack_reverse E ms : ([∗ list] de ∈ (reverse ms), denv_interp E de) ⊢ ([∗ list] de ∈ ms, denv_interp E de). Proof. iInduction ms as [|m ms] "IH"; simpl. - iIntros "_". rewrite /denv_interp //. - rewrite reverse_cons big_sepL_app big_sepL_singleton. iIntros "[Hms \$]". by iApply "IH". Qed. Proof. by rewrite reverse_Permutation. Qed. (** ** Well-foundness of denv *) Lemma denv_wf_mono E E' m : ... ... @@ -814,26 +738,21 @@ Section denv_spec. denv_interp E m -∗ denv_interp E' m. Proof. Admitted. Lemma denv_wf_delete_frac_3 mIn mOut mNew mIn' mOut' mNew' i E q dv : denv_wf E mIn → Forall (denv_wf E) mOut → denv_wf E mNew → denv_delete_frac_3 i mIn mOut mNew = Some (mIn', mOut', mNew', q, dv) → denv_wf E mIn' ∧ Forall (denv_wf E) mOut' ∧ denv_wf E mNew' ∧ Lemma denv_wf_delete_frac_2 ms m ms' m' i E q dv : Forall (denv_wf E) ms → denv_wf E m → denv_delete_frac_2 i ms m = Some (ms', m', q, dv) → Forall (denv_wf E) ms' ∧ denv_wf E m' ∧ dval_wf E dv. Proof. Admitted. Lemma denv_wf_delete_full_3 mIn mOut mNew mIn' mOut' mNew' i E dv : denv_wf E mIn → Forall (denv_wf E) mOut → denv_wf E mNew → denv_delete_full_3 i mIn mOut mNew = Some (mIn', mOut', mNew', dv) → denv_wf E mIn' ∧ Forall (denv_wf E) mOut' ∧ denv_wf E mNew' ∧ Lemma denv_wf_delete_full_2 ms m ms' m' i E dv : Forall (denv_wf E) ms → denv_wf E m → denv_delete_full_2 i ms m = Some (ms', m', dv) → Forall (denv_wf E) ms' ∧ denv_wf E m' ∧ dval_wf E dv. Proof. Admitted. End denv_spec.
 ... ... @@ -84,42 +84,46 @@ Section vcg. | m::ms => Some (ms, m) end. Fixpoint vcg_sp (E: known_locs) (mIn : denv) (mOut : list denv) (de : dcexpr) : option (denv * list denv * denv * dval) := Fixpoint vcg_sp (E: known_locs) (ms : list denv) (de : dcexpr) : option (list denv * denv * dval) := match de with | dCRet dv => Some (mIn, mOut, [], dv) | dCRet dv => Some (ms, [], dv) | dCLoad de1 => ''(mIn1, mOut1, mNew, dl) ← vcg_sp E mIn mOut de1; i ← is_dloc E dl; ''(mIn2, mOut2, mNew2, q, dv) ← denv_delete_frac_3 i mIn1 mOut1 mNew; Some (mIn2, mOut2, denv_insert i ULvl q dv mNew2, dv) ''(ms1, mNew, dl) ← vcg_sp E ms de1; 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 => ''(mIn1, mOut1, mNew1, dl) ← vcg_sp E mIn mOut de1; i ← is_dloc E dl; ''(mIn2, mOut2, mNew2, dv) ← vcg_sp E mIn1 mOut1 de2; ''(mIn3, mOut3, mNew3, _) ← denv_delete_full_3 i mIn2 mOut2 (denv_merge mNew1 mNew2); Some (mIn3, mOut3, denv_insert i LLvl 1 dv mNew3, dv) ''(ms1, mNew1, dl) ← vcg_sp E ms de1; i ← is_dloc E dl; ''(ms2, mNew2, dv) ← vcg_sp E ms1 de2; ''(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 => ''(mIn1, mOut1, mNew1, dv1) ← vcg_sp E mIn mOut de1; ''(mIn2, mOut2, mNew2, dv2) ← vcg_sp E mIn1 mOut1 de2; ''(ms1, mNew1, dv1) ← vcg_sp E ms de1; ''(ms2, mNew2, dv2) ← vcg_sp E ms1 de2; match dbin_op_eval E op dv1 dv2 with | dSome dv => Some (mIn2, mOut2, denv_merge mNew1 mNew2, dv) | dSome dv => Some (ms2, denv_merge mNew1 mNew2, dv) | dNone | dUnknown _ => None end | dCUnOp op de => ''(mIn1, mOut1, mNew1, dv) ← vcg_sp E mIn mOut de; ''(ms1, mNew1, dv) ← vcg_sp E ms de; match dun_op_eval E op dv with | dSome dv' => Some (mIn1, mOut1, mNew1, dv') | dSome dv' => Some (ms1, mNew1, dv') | dNone | dUnknown _ => None end | dCSeq de1 de2 => ''(mIn1, mOut1, mNew1, _) ← vcg_sp E mIn mOut de1; ''(mIn2, mOut2, mNew2, dv2) ← vcg_sp E mIn1 (denv_unlock mNew1::mOut1) de2; ''(mOut3, mNew3) ← popstack mOut2; Some (mIn2, mOut3, denv_merge mNew2 mNew3, dv2) ''(ms1, mNew1, _) ← vcg_sp E ms de1; ''(ms2, mNew2, dv2) ← vcg_sp E (denv_unlock mNew1 :: ms1) de2; ''(ms3, mNew3) ← popstack ms2; Some (ms3, denv_merge mNew2 mNew3, dv2) | dCAlloc _ | dCUnknown _ => None end. Definition vcg_sp' (E: known_locs) (m : denv) (de : dcexpr) : option (denv * denv * dval) := ''(ms,mNew,dv) ← vcg_sp E [m] de; ''(_, m') ← popstack ms; Some (m', mNew, dv). Definition vcg_wp_unknown (R : iProp Σ) (E: known_locs) (de: dcexpr) (m: denv) (Φ : known_locs → denv → dval → wp_expr) : wp_expr := ... ... @@ -181,28 +185,28 @@ Section vcg. | dCLoad de1 => vcg_wp E m de1 R (λ E m' dv, vcg_wp_load E dv m' (Φ E)) | dCStore de1 de2 => match vcg_sp E m [] de1 with | Some (mIn, mOut, mNew, dv1) => vcg_wp E mIn de2 R (λ E mIn dv2, vcg_wp_store E dv1 dv2 (denv_merge (denv_merge mNew (denv_stack_merge mOut)) mIn) (Φ E)) 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'') (Φ E)) | None => match vcg_sp E m [] de2 with | Some (mIn, mOut, mNew, dv2) => vcg_wp E mIn de1 R (λ E mIn dv1, vcg_wp_store E dv1 dv2 (denv_merge mNew (denv_merge (denv_stack_merge mOut) mIn)) (Φ E)) 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'') (Φ E)) | None => vcg_wp_unknown R E de m Φ end end | dCBinOp op de1 de2 => match vcg_sp E m [] de1 with | Some (mIn, mOut, mNew, dv1) => vcg_wp E mIn de2 R (λ E mIn dv2, vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew (denv_merge (denv_stack_merge mOut) mIn)) (Φ E)) 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'') (Φ E)) | None => match vcg_sp E m [] de2 with | Some (mIn, mOut, mNew, dv2) => vcg_wp E mIn de1 R (λ E mIn dv1, vcg_wp_bin_op E op dv1 dv2 (denv_merge mNew (denv_merge (denv_stack_merge mOut) mIn)) (Φ E)) 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'') (Φ E)) | None => vcg_wp_unknown R E de m Φ end end ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!