Commit 70b3eb82 by Dan Frumin

### Merge the new vcg_sp stuff

parent b76e5de6
 ... ... @@ -175,7 +175,7 @@ Section properties. iDestruct (mapsto_agree with "Hl1 Hl2") as %->. done. Qed. Lemma mapsto_combine l x x' q q' v : l ↦C[x]{q} v -∗ l ↦C[x']{q'} v -∗ l ↦C[x ⋅ x']{q+q'} v. Lemma mapsto_combine x x' l q q' v : l ↦C[x]{q} v -∗ l ↦C[x']{q'} v -∗ l ↦C[x ⋅ x']{q+q'} v. Proof. rewrite mapsto_eq /mapsto_def. iDestruct 1 as (b1 Hb1) "[Hl1 Ho1]". ... ...
 ... ... @@ -43,6 +43,9 @@ Section denv. | dio1 :: m1', dio2 :: m2' => denv_item_opt_merge dio1 dio2 :: denv_merge m1' m2' end. Definition denv_stack_merge (ms : list denv) : denv := foldr denv_merge [] ms. Fixpoint denv_singleton (i : nat) (lv : lvl) (q : frac) (dv : dval) : denv := match i with | O => [Some (DenvItem lv q dv)] ... ... @@ -75,6 +78,16 @@ Section denv. end end. 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 end. Fixpoint denv_delete_full_aux (i : nat) (m : denv) {struct m} : option (denv * frac * dval) := match m with | [] => None ... ... @@ -88,6 +101,18 @@ Section denv. end end. Fixpoint denv_delete_full_stack_aux (i : nat) (ms : list denv) {struct ms} : option (list denv * frac * dval) := match ms with | [] => None | m::ms' => match denv_delete_full_aux i m,denv_delete_full_stack_aux i ms' with | None, None => None | None, Some (ms1, q1, dv1) => Some (m::ms1, q1, dv1) | Some (m1, q2, dv2), None => Some (m1::ms', q2, dv2) | Some (m1, q2, dv2), Some (ms1, q1, dv1) => Some (m1::ms1, (q1+q2)%Qp, dv2) end end. Definition denv_lookup (i : nat) (m : denv) : option (frac * dval) := ''(m', q, dv) ← denv_delete_full_aux i m; Some (q, dv). ... ... @@ -117,6 +142,33 @@ Section denv. | Some (m1', q1, dv), Some (m2', q2, _) => guard (q1 + q2 = 1)%Qp; Some (m1', m2', 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) | 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 end. End denv. Section denv_spec. ... ... @@ -130,6 +182,13 @@ Section denv_spec. from_option (λ '(DenvItem lv q dv), dloc_interp L (dLoc i) ↦C[lv]{q} dval_interp L dv) True dio)%I. Fixpoint denv_stack_interp (mOut mOut' : list denv) E (P : iProp Σ) := match mOut,mOut' with | m::ms,m'::ms' => (denv_interp E m -∗ denv_interp E m' ∗ (denv_stack_interp ms ms' E P))%I | ms,[] => (([∗ list] de ∈ ms, denv_interp E de) -∗ P)%I | [],ms' => (([∗ list] de ∈ ms', denv_interp E de) ∗ P)%I end. Definition penv_interp (m : penv) : iProp Σ := ([∗ list] p ∈ m, penv_loc p ↦C[penv_level p]{penv_frac p} penv_val p)%I. ... ... @@ -475,6 +534,293 @@ Section denv_spec. denv_interp E m -∗ denv_interp E' m. Proof. Admitted. (** / well-foundness of denv *) (** / well-foundness of denv *) (** stack interp properties *) Lemma denv_stack_interp_nil_r ms E P : denv_stack_interp ms [] E P ⊣⊢ (([∗ list] de ∈ ms, denv_interp E de) -∗ P). Proof. induction ms as [|m ms]; simpl; eauto. Qed. Lemma denv_stack_interp_nil_l ms E P : denv_stack_interp [] ms E P ⊣⊢ (([∗ list] de ∈ ms, denv_interp E de) ∗ P). Proof. induction ms as [|m ms]; simpl; eauto. by rewrite !left_id. Qed. (** Monadic properties *) Lemma denv_stack_interp_mono ms1 ms2 E P Q : denv_stack_interp ms1 ms2 E P -∗ (P -∗ Q) -∗ denv_stack_interp ms1 ms2 E Q. Proof. iIntros "HP Hw". iInduction (ms1) as [|m1 ms1] "IH1" forall (ms2); simpl. - destruct ms2. iIntros "_". iApply "Hw". by iApply "HP". iDestruct "HP" as "[\$ HP]". by iApply "Hw". - destruct ms2. + iIntros "Hm". iApply "Hw". by iApply "HP". + iIntros "Hm1". iDestruct ("HP" with "Hm1") as "[\$ HP]". iApply ("IH1" with "HP Hw"). Qed. Lemma denv_stack_interp_frame ms1 ms2 E P Q : denv_stack_interp ms1 ms2 E P -∗ Q -∗ denv_stack_interp ms1 ms2 E (P∗Q). Proof. iIntros "HP HQ". iInduction ms1 as [|m1' ms1] "IH" forall (ms2); simpl; destruct ms2; iFrame. iIntros "Hm1'". iDestruct ("HP" with "Hm1'") as "[\$ HP]". iApply ("IH" with "HP HQ"). Qed. Lemma denv_stack_interp_intro ms1 E P : P -∗ denv_stack_interp ms1 ms1 E P. Proof. iIntros "HP". iInduction ms1 as [|m1' ms1] "IH"; simpl; first by iFrame. iIntros "\$". by iApply "IH". Qed. (* DF: does not hold *) (* Lemma denv_stack_interp_trans ms1 ms2 ms3 E P : *) (* denv_stack_interp ms1 ms2 E (denv_stack_interp ms2 ms3 E P) -∗ *) (* denv_stack_interp ms1 ms3 E P. *) (* todo: how to get rid of the silly asserts? *) Lemma denv_stack_interp_trans ms1 ms2 ms3 E P Q : denv_stack_interp ms1 ms2 E P -∗ denv_stack_interp ms2 ms3 E Q -∗ denv_stack_interp ms1 ms3 E (P∗Q). Proof. iIntros "HP HQ". iInduction ms1 as [|m1 ms1] "IH1" forall (ms2 ms3); simpl. - iInduction ms2 as [|m2 ms2] "IH2" forall (ms3); simpl. + iSpecialize ("HP" with "[]"); first done. destruct ms3; simpl; by iFrame. + destruct ms3; simpl. * iDestruct "HP" as "[Hm \$]". iIntros "_". by iApply "HQ". * iDestruct "HP" as "[[Hm2 Hms2] HP]". iDestruct ("HQ" with "Hm2") as "[\$ HQ]". iAssert (∀ ms3, ([∗ list] de ∈ ms2, denv_interp E de) ∗ P -∗ denv_stack_interp ms2 ms3 E Q -∗ ([∗ list] de ∈ ms3, denv_interp E de) ∗ P ∗ Q)%I as "IH". { iIntros (ms0). destruct ms2,ms0 as [|m0 ms0]; simpl. - iIntros "[_ \$] HQ". by iApply "HQ". - iIntros "[_ \$] [\$ \$]". - iIntros "[H \$] HQ". by iApply "HQ". - iIntros "HP HQ". iSpecialize ("IH2" \$! (m0::ms0) with "HP"). simpl. by iApply "IH2". } iApply ("IH" with "[Hms2 HP] HQ"). iFrame. - iInduction ms2 as [|m2 ms2] "IH2" forall (ms3); simpl. + destruct ms3; simpl. { iSpecialize ("HQ" with "[]"); first done. iIntros "H". iFrame. by iApply "HP". } iIntros "H". iDestruct "HQ" as "[[\$ Hms3] HQ]". iApply ("IH1" \$! [] with "[H HP]"). { iApply denv_stack_interp_nil_r. iIntros "H2". iApply "HP". iFrame. } { iApply denv_stack_interp_nil_l. iFrame. } + destruct ms3 as [|m3 ms3]; simpl. * iIntros "[Hm1 Hms1]". iDestruct ("HP" with "Hm1") as "[Hm2 HP]". iSpecialize ("IH1" \$! ms2 []). simpl. rewrite !denv_stack_interp_nil_r. iApply ("IH1" with "HP [HQ Hm2] Hms1"). iIntros "H". iApply "HQ". iFrame. * iIntros "Hm1". iDestruct ("HP" with "Hm1") as "[Hm2 HP]". iDestruct ("HQ" with "Hm2") as "[\$ HQ]". iApply ("IH1" with "HP HQ"). Qed. (* The property that we need *) Lemma denv_stack_interp_snoc m1 m2 ms1 ms2 E P : length ms1 = length ms2 → denv_stack_interp ms1 ms2 E (denv_interp E m1 -∗ denv_interp E m2 ∗ P) ⊣⊢ denv_stack_interp (ms1++[m1]) (ms2++[m2]) E P. Proof. revert ms2. induction ms1 as [|m1' ms1]; intros ms2; simpl. - destruct ms2. + simpl. rewrite !left_id. eauto. + inversion 1. - destruct ms2 as [|m2' ms2]. + inversion 1. + intros ?. rewrite IHms1; eauto. Qed. Lemma denv_delete_frac_stack_length i ms ms' q dv : denv_delete_frac_stack i ms = Some (ms', q, dv) → length ms = length ms'. Proof. revert ms'; induction ms; intros ms'; first by inversion 1. simpl. destruct (denv_delete_frac i a) as [[[m' q'] dv']|]; first by inversion 1; eauto. destruct (denv_delete_frac_stack i ms) as [[[m' q'] dv']|] eqn:Hms; last by inversion 1. intros; simplify_eq/=. f_equal. by apply IHms. Qed. Lemma denv_delete_full_stack_aux_length i ms ms' q dv : denv_delete_full_stack_aux i ms = Some (ms', q, dv) → length ms = length ms'. Proof. revert ms' q dv; induction ms; intros ms' q dv; first by inversion 1. simpl. destruct (denv_delete_full_aux i a) as [[[m' q'] dv']|]; destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] ?]|] eqn:Hms; intros Hdel; simplify_eq/=. - f_equal. by eapply IHms. - by f_equal. - 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'. 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. 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'. 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. Qed. Lemma denv_delete_frac_stack_interp E i ms ms' q dv : denv_delete_frac_stack i ms = Some (ms', q, dv) → denv_stack_interp (reverse ms) (reverse ms') E (dloc_interp E (dLoc i) ↦C{q} dval_interp E dv)%I. Proof. iInduction ms as [|m ms] "IH" forall (ms'); iIntros (Hdel); simplify_eq/=. destruct (denv_delete_frac i m) as [[[m' q'] dv']|] eqn:Hm; simplify_eq/=. - rewrite !reverse_cons -denv_stack_interp_snoc; last done. iApply denv_stack_interp_intro. iIntros "Hm". by iApply denv_delete_frac_interp. - destruct (denv_delete_frac_stack i ms) as [[[m' q'] dv']|] eqn:Hms; simplify_eq/=. rewrite !reverse_cons -denv_stack_interp_snoc; last first. { rewrite !reverse_length. eapply denv_delete_frac_stack_length. eassumption. } iSpecialize ("IH" with "[]"). eauto. iApply (denv_stack_interp_mono with "IH"). iIntros "\$ \$". Qed. Lemma denv_delete_full_stack_interp E i ms ms' q dv : denv_delete_full_stack_aux i ms = Some (ms', q, dv) → denv_stack_interp (reverse ms) (reverse ms') E (dloc_interp E (dLoc i) ↦C{q} dval_interp E dv)%I. Proof. iInduction ms as [|m ms] "IH" forall (ms' q dv); iIntros (Hdel); simplify_eq/=. destruct (denv_delete_full_aux i m) as [[[m' q'] dv']|] eqn:Hm; simplify_eq/=. - destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] ?]|] eqn:Hms; simplify_eq/=. + rewrite !reverse_cons -denv_stack_interp_snoc; last first. { rewrite !reverse_length. by eapply denv_delete_full_stack_aux_length. } iSpecialize ("IH" with "[]"). eauto. iApply (denv_stack_interp_mono with "IH"). iIntros "Hl Hm". rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux /=; last done. iDestruct "Hm" as "[\$ Hl2]". iDestruct (mapsto_value_agree with "Hl Hl2") as %->. iCombine "Hl Hl2" as "\$". + rewrite !reverse_cons -denv_stack_interp_snoc; last done. iApply denv_stack_interp_intro. iIntros "Hm". rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done. iDestruct "Hm" as "[\$ \$]". - destruct (denv_delete_full_stack_aux i ms) as [[[ms1 q1] ?]|] eqn:Hms; simplify_eq/=. rewrite !reverse_cons -denv_stack_interp_snoc; last first. { rewrite !reverse_length. by eapply denv_delete_full_stack_aux_length. } iSpecialize ("IH" with "[]"). eauto. iApply (denv_stack_interp_mono with "IH"). 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))). Proof. rewrite /denv_delete_full_3. 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; case_option_guard; simplify_eq/=. - rewrite denv_delete_full_interp_aux; eauto. iIntros "[\$ Hl1] /=". iPoseProof denv_delete_full_stack_interp as "H"; first eassumption. iApply (denv_stack_interp_mono with "H"). iIntros "Hl2". rewrite -!denv_interp_aux_0. rewrite denv_delete_full_interp_aux; last done. iIntros "[\$ Hl3]". iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->. iDestruct (mapsto_value_agree with "Hl2 Hl3") as %->. iCombine "Hl1 Hl2 Hl3" as "Hl". (* STUPID: cannnot rewrite by associativity in BI *) assert ((q1 + (q2 + q3))%Qp = 1%Qp) as ->. { transitivity (q1+q2+q3)%Qp; last done. by rewrite (assoc Qp_plus q1 q2 q3). } iFrame. - rewrite denv_delete_full_interp_aux; eauto. iIntros "[\$ Hl1] /=". iPoseProof denv_delete_full_stack_interp as "H"; first eassumption. iApply (denv_stack_interp_mono with "H"). iIntros "Hl2". rewrite -!denv_interp_aux_0. iIntros "\$". iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->. iCombine "Hl1 Hl2" as "Hl". rewrite H1. done. - rewrite denv_delete_full_interp_aux; last done. iIntros "[\$ Hl1] /=". iApply denv_stack_interp_intro. rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done. iIntros "[\$ Hl2]". iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->. iCombine "Hl1 Hl2" as "Hl". rewrite H1. done. - rewrite denv_delete_full_interp_aux; last done. iIntros "[\$ Hl2]". iApply denv_stack_interp_intro. iIntros "\$". iFrame. - iIntros "\$". iPoseProof denv_delete_full_stack_interp as "H"; first eassumption. iApply (denv_stack_interp_mono with "H"). iIntros "Hl1". rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done. iIntros "[\$ Hl2]". iDestruct (mapsto_value_agree with "Hl1 Hl2") as %->. iCombine "Hl1 Hl2" as "Hl". rewrite H1. done. - iIntros "\$". iPoseProof denv_delete_full_stack_interp as "H"; first eassumption. iApply (denv_stack_interp_mono with "H"). iIntros "\$ \$". - iIntros "\$". iApply denv_stack_interp_intro. rewrite -!denv_interp_aux_0 denv_delete_full_interp_aux; last done. iIntros "\$". Qed. 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))). 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_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/=. + iIntros "\$". iPoseProof (denv_delete_frac_stack_interp) as "H"; first eassumption. iApply (denv_stack_interp_mono with "H"). iIntros "\$ \$". + 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. Lemma denv_stack_merge_interp E ms : ([∗ list] de ∈ ms, denv_interp E de) ⊢ denv_interp E (denv_stack_merge ms). Proof. iInduction ms as [|m ms] "IH"; simpl. - iIntros "_". rewrite /denv_interp //. - iIntros "[Hm Hms]". rewrite -denv_merge_interp. iFrame. by iApply "IH". Qed. 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. (** / stack interp properties *) End denv_spec.
 ... ... @@ -15,7 +15,7 @@ Section tests_vcg. (a_store (a_ret #s) (a_ret #4))) True (λ v, ⌜v = #6⌝ ∧ s ↦C[LLvl] #4 ∗ l ↦C[LLvl] #1). Proof. iIntros "Hs Hl". vcg_solver. iModIntro. eauto with iFrame. vcg_solver. eauto with iFrame. Qed. Lemma test_seq2 (s l : loc) : ... ... @@ -37,6 +37,81 @@ Section tests_vcg. iIntros "Hl". vcg_solver. iModIntro. eauto with iFrame. Qed. Lemma test_seq4 (l k : loc) : l ↦C #0 -∗ k ↦C #0 -∗ awp (a_bin_op PlusOp (a_store (a_ret #l) (a_ret #2);;;; a_bin_op PlusOp (a_ret #1) (a_store (a_ret #l) (a_ret #1))) (a_store (a_ret #k) (a_ret #2);;;; a_bin_op PlusOp (a_ret #1) (a_store (a_ret #k) (a_ret #1)))) True (λ v, ⌜v = #4⌝ ∧ l ↦C[LLvl] #1 ∗ k ↦C[LLvl] #1). Proof. iIntros "Hl Hk". vcg_solver. iModIntro. by eauto with iFrame. Qed. Definition stupid (l : loc) := a_store (a_ret #l) (a_ret #1);;;;(a_ret #0). Lemma test_seq_fail (l : loc) : l ↦C[ULvl] #0 -∗ awp (a_bin_op PlusOp (a_bin_op PlusOp (stupid l) (stupid l)) (a_ret #0)) True (λ v, l ↦C #1). Proof. iIntros "Hl". vcg_solver. Fail by eauto with iFrame. Abort. Lemma test_seq5 (l k : loc) : l ↦C #0 -∗ k ↦C #0 -∗ awp (a_bin_op PlusOp (a_ret #0) ((a_store (a_ret #l) (a_ret #1));;;; (a_store (a_ret #k) (a_ret #2));;;; (a_ret #0))) True (λ v, ⌜v = #0⌝ ∗ l ↦C #1 ∗ k ↦C #2). Proof. iIntros "Hl Hk". vcg_solver. repeat iModIntro. by eauto with iFrame. Qed. Lemma test_sp1 (l k : loc) : l ↦C #0 -∗ k ↦C #0 -∗ awp (a_bin_op PlusOp (a_ret #1) ((a_store (a_ret #l) (a_ret #1));;;; (a_bin_op PlusOp (a_store (a_ret #k) (a_ret #2)) (a_load (a_ret #l)));;;; (a_bin_op PlusOp (a_load (a_ret #k)) (a_store (a_ret #l) (a_ret #2))))) True (λ v, ⌜v = #5⌝ ∗ l ↦C[LLvl] #2 ∗ k ↦C #2). Proof. iIntros "Hl Hk". vcg_solver. repeat iModIntro. rewrite ?Qp_half_half. eauto with iFrame. Qed. Lemma test_sp2 (l : loc) : l ↦C #0 -∗ awp (a_bin_op PlusOp (a_ret #1) ((a_store (a_ret #l) (a_ret #1));;;; (a_bin_op PlusOp (a_load (a_ret #l)) (a_load (a_ret #l)));;;; (a_store (a_ret #l) (a_ret #2)))) True (λ v, ⌜v = #3⌝ ∗ l ↦C[LLvl] #2). Proof. iIntros "Hl". vcg_solver. repeat iModIntro. rewrite ?Qp_half_half. eauto with iFrame. Qed. Lemma store_load (s l : loc) R : s ↦C #0 -∗ l ↦C #1 -∗ awp (a_store (a_ret #s) (a_load (a_ret #l))) R (λ _, s ↦C[LLvl] #1 ∗ l ↦C #1). ... ...
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!