From c56b93abbdfcebd07f8669e8176ea03912ee0023 Mon Sep 17 00:00:00 2001 From: Simon Spies Date: Thu, 19 Sep 2019 11:49:49 +0200 Subject: [PATCH] refactor to use iris arrays more and move semantic invariants out --- _CoqProject | 1 + theories/logrel_heaplang/lib/arrays.v | 470 +++++++--------------- theories/logrel_heaplang/lib/invariants.v | 197 +++++++++ theories/logrel_heaplang/lib/vectors.v | 190 +++++---- 4 files changed, 433 insertions(+), 425 deletions(-) create mode 100644 theories/logrel_heaplang/lib/invariants.v diff --git a/_CoqProject b/_CoqProject index 467617a..e4b2936 100644 --- a/_CoqProject +++ b/_CoqProject @@ -80,6 +80,7 @@ theories/logrel/F_mu_ref_conc/examples/fact.v theories/logrel_heaplang/ltyping.v theories/logrel_heaplang/ltyping_safety.v theories/logrel_heaplang/lib/symbol_adt.v +theories/logrel_heaplang/lib/invariants.v theories/logrel_heaplang/lib/arrays.v theories/logrel_heaplang/lib/vectors.v diff --git a/theories/logrel_heaplang/lib/arrays.v b/theories/logrel_heaplang/lib/arrays.v index 03d0e65..a643581 100644 --- a/theories/logrel_heaplang/lib/arrays.v +++ b/theories/logrel_heaplang/lib/arrays.v @@ -3,6 +3,7 @@ From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Export lifting metatheory. From iris.heap_lang Require Import notation proofmode. +From iris_examples.logrel_heaplang.lib Require Import invariants. From iris_examples.logrel_heaplang Require Import ltyping ltyping_safety. @@ -16,328 +17,162 @@ Ltac bool_decide H := Lemma Z_to_nat n: n >= 0 -> ∃ m: nat, n = m. Proof. - intros; exists (Z.to_nat n); rewrite Z2Nat.id; lia. + intros; exists (Z.to_nat n); rewrite Z2Nat.id; lia. Qed. +(** Arrays *) +Section Arrays. + Context `{! heapG Σ}. + (* Arrays have the following memory layout: |n|x_0|...|x_{n-1}| *) -(** range function on integers *) -Definition range (m n: Z) := map (fun x: nat => x + m) (seq 0 (Z.to_nat (n - m))). -Arguments range : simpl never. - -Lemma range_induct n P: - (forall m, n <= m -> P n m) -> (forall m, m < n -> P n (m + 1) -> P n m) -> forall m, P n m. -Proof. - intros H IH m. remember (Z.to_nat (n - m)) as k. revert m Heqk. - induction k. - - intros; enough (n <= m) by eauto. eapply Zle_0_minus_le. - destruct (n - m) eqn: E; try lia. rewrite Z2Nat.inj_pos in Heqk. - lia. - - intros; eapply IH. eapply Zlt_0_minus_lt, Z_to_nat_neq_0_pos; lia. - eapply IHk. replace (n - (m + 1)) with (Z.pred (n - m)) by lia. - rewrite Z2Nat.inj_pred. now rewrite <-Heqk. -Qed. - - -Lemma range_empty m n: n <= m -> range m n = []. -Proof. - intros H. unfold range. - assert (n - m <= 0) as -> % Z_to_nat_nonpos by lia. - reflexivity. -Qed. - -Lemma range_step m n: - (m < n) -> range m n = m :: range (m + 1) n. -Proof. - unfold range. intros H. assert (0 < n - m) by lia. - apply Z2Nat.inj_lt in H0 as H1; try lia. - rewrite Z2Nat.inj_0 in H1. destruct (Z.to_nat (n - m)) as [|k] eqn: Eq. - lia. cbn. replace (0%nat + m) with m by lia. - replace (n - (m + 1)) with (Z.pred (n - m)) by lia. - rewrite Z2Nat.inj_pred Eq. - rewrite <-seq_shift. rewrite map_map. - erewrite map_ext. reflexivity. - intros; lia. -Qed. - - -Lemma range_shift k m n: range (k + m) (k + n) = map (Z.add k) (range m n). -Proof. - induction n, m using range_induct. - - rewrite !range_empty; eauto; lia. - - rewrite range_step; try lia. replace (k + m + 1) with (k + (m + 1)) by lia. - rewrite IHm. setoid_rewrite range_step at 2; now try lia. -Qed. - -Lemma range_split k m n: m <= k < n -> range m n = range m k ++ range k n. -Proof. - induction k, m using range_induct. - - intros; assert (k = m) as -> by lia. rewrite (range_empty m m); eauto. - - intros. rewrite range_step; try lia. rewrite IHm; try lia. - rewrite app_comm_cons. now rewrite <-range_step. -Qed. - - -Lemma range_step_top m n: m <= n -> range m (n + 1) = range m n ++ [n]. -Proof. - intros; rewrite (range_split n); try lia. - f_equal. rewrite range_step; try lia. - rewrite range_empty; now try lia. -Qed. - - -(** big range operation *) -Section BigOpRange. - Context {Σ : gFunctors}. + (* to create an array, unsafe *) + Definition unsafe_arr : val := + λ: "n", let: "a" := AllocN ("n" + #1) #0 in "a" <- "n" ;; "a". + Definition unsafe_set : val := + λ: "a" "i" "x", ("a" + "i" + #1) <- "x". - Implicit Types (m n k: Z) (ϕ: Z -> iProp Σ). - - Notation "'[∗' 'range]' m '<=' i '<' n ',' P" := - ([∗ list] i ∈ range m n, P)%I - (at level 200, m at level 30, i at level 30, n at level 30, - right associativity, format "[∗ range] m <= i < n , P") : bi_scope. + Definition unsafe_get : val := + λ: "a" "i", !("a" + "i" + #1). - - Lemma big_opR_empty m n ϕ: - n <= m -> (([∗ range] m <= i < n, ϕ i) ⊣⊢ emp)%I. - Proof. - intros; rewrite range_empty; try lia. reflexivity. - Qed. + Definition arr : val := + λ: "n", if: "n" < #0 then NONE else SOME (unsafe_arr "n"). + Definition get : val := + λ: "a" "i", if: ((#-1) < "i") && ("i" < !"a") then SOME (unsafe_get "a" "i") else NONE. - Lemma big_opR_step m n ϕ: - m < n -> (([∗ range] m <= i < n, ϕ i) ⊣⊢ ϕ m ∗ ([∗ range] (m + 1) <= i < n, ϕ i))%I. - Proof. - intros; now rewrite range_step. - Qed. + Definition set : val := + λ: "a" "i" "x", if: ((#-1) < "i") && ("i" < !"a") then (unsafe_set "a" "i" "x") else #(). - Lemma big_opR_split n m k ϕ: - n <= k < m -> (([∗ range] n <= i < m, ϕ i) ⊣⊢ (([∗ range] n <= i < k, ϕ i) ∗ ([∗ range] k <= i < m, ϕ i)))%I. - Proof. - intros; rewrite (range_split k); try lia. now rewrite big_sepL_app. - Qed. + (* Verification *) - Lemma big_opR_singleton k ϕ: - (([∗ range] k <= i < k + 1, ϕ i) ⊣⊢ ϕ k)%I. + Variable (N: namespace). + Definition array (n: Z) (l: loc) : iProp Σ := + (∃ zs: list Z, ⌜n = length zs⌝ ∗ l ↦∗ (#n :: ((LitV ∘ LitInt) <$> zs)))%I. + Definition body (n: Z) (l: loc) : iProp Σ := + (∃ zs: list Z, ⌜n = length zs⌝ ∗ (l +ₗ 1) ↦∗ ((LitV ∘ LitInt) <$> zs))%I. + Definition entry (l: loc) (i: Z) : iProp Σ := + (∃ z: Z, (l +ₗ i +ₗ1) ↦ #z)%I. + + Lemma body_decompose n l: + ⌜n > 0⌝ -∗ body n l -∗ entry l 0 ∗ body (n - 1) (loc_add l 1). Proof. - rewrite range_step; try lia. rewrite range_empty; try lia. - now rewrite big_sepL_singleton. + iIntros "%". iDestruct 1 as (vs) "[% H]". subst n. destruct vs as [|v vs]; simpl in *; try lia. + cbn; iDestruct "H" as "[He H]". iSplitL "He". + { iExists _; replace (0%nat : Z) with 0 by lia; by rewrite !loc_add_0. } + iExists vs; simpl. iSplitR; first (iPureIntro; lia). + unfold array.array. iApply big_sepL_mono'; eauto. + intros n v'; rewrite !loc_add_assoc. simpl. + by replace (1 + S n) with (1 + (1 + n)) by lia. Qed. - Lemma big_opR_shift k m n ϕ: - (([∗ range] (k + m) <= i < (k + n), ϕ i) ⊣⊢ ([∗ range] m <= i < n, ϕ (k + i)))%I. + Lemma body_compose n l: + entry l 0 -∗ body (n - 1) (loc_add l 1) -∗ body n l. Proof. - rewrite range_shift. induction (range m n); cbn; eauto. - now rewrite IHl. + iDestruct 1 as (v) "E"; rewrite !loc_add_0. + iDestruct 1 as (vs) "[% B]". iExists (v::vs). iSplit. + { iPureIntro; simpl; lia. } + rewrite array_cons; iFrame. Qed. - Lemma big_opR_ext m n ϕ ψ: - (forall i, m <= i < n -> ϕ i ⊣⊢ ψ i) -> ([∗ range] m <= i < n, ϕ i) ⊣⊢ ([∗ range] m <= i < n, ψ i). - Proof. - intros H. induction n, m using range_induct. - - rewrite !big_opR_empty; eauto. - - rewrite big_opR_step ?IHm ?H. now rewrite <-big_opR_step. - all: intros; try lia. - eapply H. lia. - Qed. - - Lemma big_opR_shift_succ m n ϕ: - (([∗ range] (m + 1) <= i < (n + 1), ϕ i) ⊣⊢ ([∗ range] m <= i < n, ϕ (i + 1)))%I. + Lemma body_entry_acc i n l: + ⌜0 ≤ i < n⌝ -∗ body n l -∗ entry l i ∗ (entry l i -∗ body n l). Proof. - replace (m + 1) with (1 + m) by lia. replace (n + 1) with (1 + n) by lia. - rewrite range_shift. induction (range m n); cbn; eauto. rewrite IHl. - now replace (1 + a) with (a + 1) by lia. + iIntros ([H1 H2]) "B". edestruct (Z_to_nat i) as [j ->]; first lia. + edestruct (Z_to_nat n) as [m ->]; first lia. clear H1. + iInduction m as [|m] "IH" forall (l j H2); first lia. destruct j as [|j]. + all: iDestruct (body_decompose with "[] B") as "[E B]"; first (iPureIntro; lia). + - replace (0%nat : Z) with 0 by lia. + iFrame. iIntros "E". iApply (body_compose with "E B"). + - replace (S m - 1) with (m: Z) by lia. + iDestruct ("IH" $! _ j with "[] B") as "[E2 Bclose]"; first (iPureIntro; lia). + iSplitL "E2". + { unfold entry. rewrite !loc_add_assoc. by replace (S j + 1) with (1 + (j + 1)) by lia. } + iIntros "E2". iApply (body_compose with "E"). replace (S m - 1) with (m: Z) by lia. + iApply "Bclose". + { unfold entry. rewrite !loc_add_assoc. by replace (S j + 1) with (1 + (j + 1)) by lia. } Qed. - Lemma big_opR_step_top m n ϕ: - (m <= n) -> (([∗ range] m <= i < n + 1, ϕ i) ⊣⊢ ([∗ range] m <= i < n, ϕ i) ∗ ϕ n)%I. - Proof. - intros. rewrite -big_opR_singleton -(big_opR_split); eauto; lia. - Qed. - - Lemma big_opR_split_three n m k ϕ: - n <= k < m -> - (([∗ range] n <= i < m, ϕ i) ⊣⊢ (([∗ range] n <= i < k, ϕ i) ∗ ϕ k ∗ ([∗ range] (k + 1) <= i < m, ϕ i)))%I. + Lemma array_body_acc n l: + array n l -∗ body n l ∗ (body n l -∗ array n l). Proof. - intros H; rewrite big_opR_split -?big_opR_step; eauto; lia. + iDestruct 1 as (vs) "[% A]"; rewrite array_cons. iDestruct "A" as "[L B]". + iSplitL "B"; first (iExists vs ; by iSplit). + iDestruct 1 as (vs') "[% B]". iExists vs'. rewrite array_cons. iFrame. by iPureIntro. Qed. - Lemma big_opR_acc n m k ϕ: - n <= k < m -> ([∗ range] n <= i < m, ϕ i) ⊣⊢ ϕ k ∗ (ϕ k -∗ [∗ range] n <= i < m, ϕ i). + Lemma array_entry_acc i n l: + ⌜0 ≤ i < n⌝ -∗ array n l -∗ entry l i ∗ (entry l i -∗ array n l). Proof. - intros H; rewrite big_opR_split_three; eauto. iSplit. - - iIntros "(H1 & H2 & H3)". iFrame. eauto. - - iIntros "(H1 & H2)". iApply "H2". iFrame. + iIntros "H A". iDestruct (array_body_acc with "A") as "[B Bclose]". + iDestruct (body_entry_acc with "H B") as "[E Eclose]". iFrame. + iIntros "E". iApply "Bclose". by iApply "Eclose". Qed. - -End BigOpRange. - -Notation "'[∗' 'range]' m '<=' i '<' n ',' P" := - ([∗ list] i ∈ range m n, P)%I - (at level 200, m at level 30, i at level 30, n at level 30, - right associativity, format "[∗ range] m <= i < n , P") : bi_scope. - - - - -(* A more semantic notion of an invariant, using the accessor pattern *) -Section SemanticInvariants. - - Context `{!invG Σ}. - - Definition Inv_def (N: namespace) (P: iProp Σ) : iProp Σ := - (□ (∀ E, ⌜↑N ⊆ E⌝ → True ={E,E ∖ ↑N}=∗ ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True)))%I. - - Definition Inv_aux : seal (@Inv_def). by eexists. Qed. - Definition Inv := Inv_aux.(unseal). - Definition Inv_eq : @Inv = @Inv_def := Inv_aux.(seal_eq). - - - Global Instance inv_contractive N : Contractive (Inv N). - Proof. rewrite Inv_eq. solve_contractive. Qed. - - Global Instance inv_ne N : NonExpansive (Inv N). - Proof. apply contractive_ne, _. Qed. - - Global Instance Inv_proper N: Proper (equiv ==> equiv) (Inv N). - Proof. apply ne_proper, _. Qed. - - Global Instance Inv_persist M P: Persistent (Inv M P). - Proof. rewrite Inv_eq. typeclasses eauto. Qed. - - - Lemma inv_to_Inv M P: inv M P -∗ Inv M P. + Lemma array_length_acc n l: + array n l -∗ l ↦ #n ∗ (l ↦ #n -∗ array n l). Proof. - iIntros "#I". rewrite Inv_eq. iIntros (E H). - iPoseProof (inv_open with "I") as "H"; eauto. + iDestruct 1 as (zs) "[H1 H2]"; cbn; iDestruct "H2" as "[Hl H2]". + rewrite loc_add_0. iFrame. iIntros "Hl". iExists _. iFrame "H1". + cbn; iFrame. by rewrite loc_add_0. Qed. - - Global Instance into_inv_Inv N P : IntoInv (Inv N P) N := {}. - - Global Instance into_acc_Inv N P E: - IntoAcc (Inv N P) (↑N ⊆ E) True (fupd E (E ∖ ↑N)) (fupd (E ∖ ↑N) E) (λ _ : (), (▷ P)%I) (λ _ : (), (▷ P)%I) (λ _ : (), None). + Lemma body_entry_inv i n l: + ⌜0 ≤ i < n⌝ -∗ inv N (body n l) -∗ inv N (entry l i). Proof. - rewrite Inv_eq /IntoAcc /accessor bi.exist_unit. - iIntros (?) "#Hinv _". iApply "Hinv"; done. + iIntros "% #I". iApply inv_acc; eauto. iNext. iModIntro. by iApply body_entry_acc. Qed. - - Lemma Inv_acc N P Q: - Inv N P -∗ □ (P -∗ Q ∗ (Q -∗ P)) -∗ Inv N Q. - Proof. - iIntros "#I #Acc". rewrite Inv_eq. - iModIntro. iIntros (E H) "T". - iSpecialize ("I" $! E H with "T"). - iApply fupd_wand_r. iFrame. - iIntros "(P & Hclose)". iSpecialize ("Acc" with "P"). - iDestruct "Acc" as "[Q CB]". iFrame. - iIntros "Q". iApply "Hclose". now iApply "CB". - Qed. - - Lemma Inv_proj_l M P Q: Inv M (P ∗ Q) -∗ Inv M P. + Lemma array_entry_inv i n l: + ⌜0 ≤ i < n⌝ -∗ inv N (array n l) -∗ inv N (entry l i). Proof. - iIntros "#I". iApply Inv_acc; eauto. - iModIntro. iIntros "[$ Q] P"; iFrame. + iIntros "% #I". iApply inv_acc; eauto. iNext. iModIntro. by iApply array_entry_acc. Qed. - Lemma Inv_proj_r M P Q: Inv M (P ∗ Q) -∗ Inv M Q. + Lemma array_body_inv n l: + inv N (array n l) -∗ inv N (body n l). Proof. - rewrite (bi.sep_comm P Q). eapply Inv_proj_l. + iIntros "#I". iApply inv_acc; eauto. iNext. iModIntro. by iApply array_body_acc. Qed. - - Lemma Inv_split M P Q: Inv M (P ∗ Q) -∗ Inv M P ∗ Inv M Q. + Lemma array_length_inv n l: + inv N (array n l) -∗ inv N (l ↦ #n). Proof. - iIntros "#H". - iPoseProof (Inv_proj_l with "H") as "$". - iPoseProof (Inv_proj_r with "H") as "$". + iIntros "#I". iApply inv_acc; eauto. iNext. iModIntro. by iApply array_length_acc. Qed. - -End SemanticInvariants. - - - - -(** Arrays *) -Section Arrays. - - Context `{! heapG Σ}. - (* Arrays have the following memory layout: |n|x_0|...|x_{n-1}| *) - - (* to create an array, unsafe *) - Definition unsafe_arr : val := - λ: "n", let: "a" := AllocN ("n" + #1) #0 in "a" <- "n" ;; "a". - - Definition unsafe_set : val := - λ: "a" "i" "x", ("a" + "i" + #1) <- "x". - - Definition unsafe_get : val := - λ: "a" "i", !("a" + "i" + #1). - - Definition arr : val := - λ: "n", if: "n" < #0 then NONE else SOME (unsafe_arr "n"). - - Definition get : val := - λ: "a" "i", if: ((#-1) < "i") && ("i" < !"a") then SOME (unsafe_get "a" "i") else NONE. - - Definition set : val := - λ: "a" "i" "x", if: ((#-1) < "i") && ("i" < !"a") then (unsafe_set "a" "i" "x") else #(). - - (* Verification *) - - Variable (N: namespace). - Definition body n (l: loc) : iProp Σ := - ([∗ range] 0 <= i < n, ∃ x: Z, (l +ₗ (i + 1)) ↦ #x)%I. - Definition array (n: Z) (l: loc) : iProp Σ := (l ↦ #n ∗ body n l)%I. - - (** ** Specs *) Lemma unsafe_arr_spec n: {{{ ⌜n >= 0⌝ }}} unsafe_arr #n {{{ (l: loc), RET #l; array n l }}}. Proof. - iIntros (phi) "% Post". wp_lam. wp_pures. wp_bind (AllocN _ _). + iIntros (ϕ) "% Post". wp_lam. wp_pures. wp_bind (AllocN _ _). wp_apply (wp_allocN); eauto. lia. - iIntros (l) "A". wp_pures. replace (n + 1) with (Z.succ n) by lia. - rewrite Z2Nat.inj_succ; try lia. cbn. - iDestruct "A" as "[[Hl R'] R]". rewrite loc_add_0. - wp_store. iApply "Post". iClear "R". - iFrame. unfold body. - assert (n = Z.to_nat n) as -> by (rewrite Z2Nat.id; lia). rewrite Nat2Z.id. clear a. - iInduction (Z.to_nat n) as [|m] "IH" forall (l); cbn; eauto. - rewrite big_opR_step; try lia. - iDestruct "R'" as "[Hl R']". iSplitL "Hl"; eauto. - replace (S m: Z) with (m + 1) by lia. rewrite big_opR_shift_succ. - iApply big_opR_ext. 2: iApply ("IH" with "[R']"). - intros. cbn. now rewrite Z.add_comm -loc_add_assoc. - setoid_rewrite loc_add_assoc. erewrite big_opL_ext. iExact "R'". - cbn. intros. now replace (1 + S k) with (S (S k) : Z) by lia. + iIntros (l) "[A _]". wp_pures. replace (n + 1) with (Z.succ n) by lia. + rewrite Z2Nat.inj_succ; try lia. + iPoseProof (@update_array _ _ _ _ 0%nat with "[$A]") as "[Hl B]"; first reflexivity. + rewrite loc_add_0. wp_store. iApply "Post". iSpecialize ("B" with "[$Hl]"). simpl. + iExists (replicate (Z.to_nat n) 0). iSplit; eauto. + { iPureIntro. rewrite replicate_length. symmetry. apply Z2Nat.id. lia. } + by rewrite fmap_replicate. Qed. Lemma unsafe_get_spec n a i: - {{{ Inv N (array n a) ∗ ⌜0 ≤ i < n⌝ }}} unsafe_get #a #i {{{ (x: Z), RET #x; True }}}. + {{{ inv N (array n a) ∗ ⌜0 ≤ i < n⌝ }}} unsafe_get #a #i {{{ (x: Z), RET #x; True }}}. Proof. - iIntros (phi) "[#A %] Post". - unfold unsafe_get. wp_pures. - iInv "A" as "[Hl B]" "Hclose". rewrite /body (big_opR_acc); last eauto. - iDestruct "B" as "(B1 & B2)". iDestruct "B1" as (x) "B1". rewrite loc_add_assoc. wp_load. - iMod ("Hclose" with "[Hl B1 B2]") as "_"; eauto. - iNext. iFrame. iApply "B2". now iExists x. + iIntros (ϕ) "[#A %] Post". unfold unsafe_get. wp_pures. + iPoseProof (array_entry_inv with "[] A") as "E"; eauto. + iInv "E" as ">HE" "Hclose". iDestruct "HE" as (v) "He". + wp_load. iMod ("Hclose" with "[He]") as "_"; first by iExists _. now iApply "Post". Qed. - Lemma unsafe_set_spec n a i (x: Z): - {{{ Inv N (array n a) ∗ ⌜0 ≤ i < n⌝ }}} unsafe_set #a #i #x {{{ RET #(); True }}}. + {{{ inv N (array n a) ∗ ⌜0 ≤ i < n⌝ }}} unsafe_set #a #i #x {{{ RET #(); True }}}. Proof. - iIntros (phi) "[#A %] Post". - unfold unsafe_set. wp_pures. - iInv "A" as "[Hl B]" "Hclose". rewrite /body (big_opR_acc); last eauto. - iDestruct "B" as "(B1 & B2)". iDestruct "B1" as (y) "B1". rewrite loc_add_assoc. wp_store. - iMod ("Hclose" with "[Hl B1 B2]") as "_"; eauto. - iNext. iFrame. iApply "B2". now iExists x. + iIntros (ϕ) "[#A %] Post". unfold unsafe_set. wp_pures. + iPoseProof (array_entry_inv with "[] A") as "E"; eauto. + iInv "E" as ">HE" "Hclose". iDestruct "HE" as (v) "He". + wp_store. iMod ("Hclose" with "[He]") as "_"; first by iExists _. now iApply "Post". Qed. @@ -347,7 +182,7 @@ Section Arrays. Definition Option (S: lty Σ) : lty Σ := Lty (fun v => (□ ⌜v = NONEV⌝ ∨ ∃ s, S s ∗ ⌜v = SOMEV s⌝)%I). Definition Array : lty Σ := - Lty (fun v => (□ ∃ (a: loc) (m: mnat), Inv N (array m a) ∗ ⌜v = #a⌝)%I). + Lty (fun v => (□ ∃ (a: loc) (m: mnat), inv N (array m a) ∗ ⌜v = #a⌝)%I). Lemma typing_arr: ∅ ⊨ arr : lty_int → Option Array. Proof. @@ -359,12 +194,12 @@ Section Arrays. - wp_apply wp_fupd. wp_apply (unsafe_arr_spec); eauto with lia. iIntros (l) "A". - edestruct (Z_to_nat z) as [m ->]; try lia. + edestruct (Z_to_nat z) as [m ->]; try lia. wp_pures. iMod (inv_alloc N _ (array m l) with "[$A]") as "#I". iModIntro. iRight. - iExists #l. iSplit; eauto. - iExists l, m. iModIntro; iSplit; eauto; now iApply inv_to_Inv. + iExists #l. iSplit; eauto. + iExists l, m. iModIntro. by iSplit. Qed. Lemma typing_get: ∅ ⊨ get : Array → lty_int → Option lty_int. @@ -375,12 +210,13 @@ Section Arrays. iIntros (v) "!#". iDestruct 1 as (i) "->". wp_pures. bool_decide H; wp_pures. - - wp_bind (! _)%E. iInv "I" as "[Ha Aa]" "Hclose". wp_load. - iMod("Hclose" with "[$Ha $Aa]") as "_". iModIntro. wp_pures. bool_decide H'. + - wp_bind (! _)%E. iPoseProof (array_length_inv with "I") as "L". + iInv "L" as "Hl" "Hclose". wp_load. + iMod("Hclose" with "Hl") as "_". iModIntro. wp_pures. bool_decide H'. + wp_pures. wp_apply (unsafe_get_spec); first iSplit; eauto with lia. iIntros (x) "_". wp_pures. iRight. iExists #x. iSplit; eauto. - + wp_pures. now iLeft. - - wp_pures. now iLeft. + + wp_pures. now iLeft. + - wp_pures. now iLeft. Qed. @@ -394,14 +230,15 @@ Section Arrays. iIntros (v) "!#". iDestruct 1 as (x) "->". wp_pures. bool_decide H; wp_pures. - - wp_bind (! _)%E. iInv "I" as "[Ha Aa]" "Hclose". wp_load. - iMod("Hclose" with "[$Ha $Aa]") as "_". iModIntro. wp_pures. bool_decide H'. + - wp_bind (! _)%E. iPoseProof (array_length_inv with "I") as "L". + iInv "L" as "Hl" "Hclose". wp_load. + iMod("Hclose" with "Hl") as "_". iModIntro. wp_pures. bool_decide H'. + wp_pures. wp_apply (unsafe_set_spec); first iSplit; eauto with lia. - + now wp_pures. - - now wp_pures. + + now wp_pures. + - now wp_pures. Qed. - - + + (** Copying Arrays *) Definition copy_rec : val := @@ -411,68 +248,49 @@ Section Arrays. Definition copy : val := λ: "a" "n", let: "b" := unsafe_arr "n" in copy_rec "a" "b" (!"a");; "b". - Lemma copy_rec_spec (a1 a2: loc) (n1 n2 n: Z): - {{{ Inv N (body n1 a1) ∗ body n2 a2 ∗ ⌜n <= n1⌝ ∗ ⌜n <= n2⌝ }}} + {{{ inv N (body n1 a1) ∗ body n2 a2 ∗ ⌜n <= n1⌝ ∗ ⌜n <= n2⌝ }}} copy_rec #a1 #a2 #n {{{ RET #(); body n2 a2 }}}. Proof. iIntros (ϕ) "(#I & B & % & %) Post". iLöb as "IH" forall (a1 a2 n n1 n2 H H0) "I". - unfold copy_rec. wp_pures. fold copy_rec. + unfold copy_rec. wp_pures. fold copy_rec. bool_decide H1. - - wp_pures. unfold body. - wp_bind(! _)%E. iInv "I" as "B2" "Hclose". - setoid_rewrite big_opR_acc with (k := 0) at 5; try lia. - iDestruct "B2" as "[H1 H2]". iDestruct "H1" as (x) "H1". - wp_load. iMod ("Hclose" with "[H1 H2]") as "_". iApply "H2"; eauto. iModIntro. wp_pures. - setoid_rewrite big_opR_acc with (k := 0) at 3; try lia. - iDestruct "B" as "[H1 H2]". iDestruct "H1" as (y) "H1". - wp_store. wp_pures. iSpecialize ("H2" with "[H1]"); eauto. - setoid_rewrite big_opR_step at 4; try lia. - replace n2 with (n2 - 1 + 1) at 2 by lia. - rewrite big_opR_shift_succ. iDestruct "H2" as "[H1 H2]". - wp_apply ("IH" $! _ _ _ (n1 - 1) (n2 - 1) with "[] [] [H2] [H1 Post]"). - 1 - 2: iPureIntro; lia. - + setoid_rewrite big_opR_ext at 3. iFrame. - intros. cbn; rewrite loc_add_assoc. - now replace (i + 1 + 1) with (1 + (i + 1)) by lia. - + iNext. iIntros "H". iApply "Post". - setoid_rewrite big_opR_step at 4; try lia. - replace n2 with (n2 - 1 + 1) at 2 by lia. - rewrite big_opR_shift_succ. iFrame. - setoid_rewrite big_opR_ext at 3. iFrame. - intros; cbn. rewrite loc_add_assoc. - now replace (1 + (i + 1)) with (i + 1 + 1) by lia. - + iModIntro. - setoid_rewrite big_opR_step at 2; try lia. - replace n1 with (n1 - 1 + 1) at 1 by lia. - rewrite big_opR_shift_succ. iFrame. - setoid_rewrite big_opR_ext at 3. - iPoseProof (Inv_split with "I") as "[_ I']". iExact "I'". - intros; cbn. rewrite loc_add_assoc. - now replace (1 + (i + 1)) with (i + 1 + 1) by lia. + - wp_pures. iPoseProof (body_entry_inv 0 with "[] I") as "E"; first (iPureIntro; split; lia). + wp_bind(! _)%E. iInv "E" as (v) "E" "Hclose". rewrite loc_add_0. + wp_load. iMod ("Hclose" with "[E]") as "_"; first (iExists _; by rewrite loc_add_0). + iModIntro. wp_pures. iPoseProof (body_entry_acc 0 with "[] B") as "[E Eclose]"; first (iPureIntro; split; lia). + wp_bind(_ <- _)%E. iDestruct "E" as (v') "E". rewrite loc_add_0. + wp_store. wp_pures. iDestruct ("Eclose" with "[E]") as "B"; first (iExists _; by rewrite loc_add_0). + iDestruct (body_decompose with "[] B") as "[E B]"; first (iPureIntro; lia). + wp_apply ("IH" $! _ _ _ (n1 - 1) (n2 - 1) with "[] [] B [E Post]"). + 1 - 2: iPureIntro; lia. + + iNext. iIntros "B". iApply "Post". iApply (body_compose with "E B"). + + iModIntro. iApply inv_acc; eauto. iNext. iModIntro. + iIntros "B". iPoseProof (body_decompose with "[] B") as "[E B]"; first (iPureIntro; lia). + iFrame. iIntros "B". iApply (body_compose with "E B"). - wp_pures; iApply "Post"; eauto. Qed. Lemma copy_spec (a: loc) (m n: Z): - {{{ Inv N (array m a) ∗ ⌜0 <= m <= n⌝}}} + {{{ inv N (array m a) ∗ ⌜0 <= m <= n⌝}}} copy #a #n {{{ (b: loc), RET #b; array n b }}}. Proof. iIntros (ϕ) "[#H %] Post". unfold copy. wp_pures. wp_apply (unsafe_arr_spec); first (iPureIntro; lia). - iIntros (l) "[Hb Ab]". wp_pures. - wp_bind (! _)%E. iInv "H" as "[Ha Aa]" "Hclose". - wp_load. iMod("Hclose" with "[$Ha $Aa]") as "_". iModIntro. - wp_apply (copy_rec_spec with "[$Ab]"). - repeat iSplit; eauto with lia. iApply Inv_proj_r; eauto. - iIntros "Ab". wp_pures. iApply "Post". iFrame. + iIntros (l) "A". wp_pures. wp_bind (! _)%E. + iPoseProof (array_length_inv with "H") as "I". + iInv "I" as "Ha" "Hclose". wp_load. iMod("Hclose" with "Ha") as "_". iModIntro. + iPoseProof (array_body_acc with "A") as "[B Bclose]". + wp_apply (copy_rec_spec with "[$B]"). + { repeat iSplit; eauto with lia. iApply array_body_inv; eauto. } + iIntros "?". wp_pures. iApply "Post". by iApply "Bclose". Qed. - - -End Arrays. + +End Arrays. diff --git a/theories/logrel_heaplang/lib/invariants.v b/theories/logrel_heaplang/lib/invariants.v new file mode 100644 index 0000000..f4e0f90 --- /dev/null +++ b/theories/logrel_heaplang/lib/invariants.v @@ -0,0 +1,197 @@ +(* TODO: merge this into iris *) +From iris.base_logic.lib Require Export fancy_updates. +From stdpp Require Export namespaces. +From iris.base_logic.lib Require Import wsat. +From iris.algebra Require Import gmap. +From iris.proofmode Require Import tactics. +Set Default Proof Using "Type". +Import uPred. + + +Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ (↑N:coPset). +Proof. + exists (coPpick (↑ N ∖ gset_to_coPset E)). + rewrite -elem_of_gset_to_coPset (comm and) -elem_of_difference. + apply coPpick_elem_of=> Hfin. + eapply nclose_infinite, (difference_finite_inv _ _), Hfin. + apply gset_to_coPset_finite. +Qed. + + +(** * Invariants *) +Section inv. + Context `{!invG Σ}. + + (** Internal backing store of invariants *) + Definition internal_inv_def (N : namespace) (P : iProp Σ) : iProp Σ := + (∃ i P', ⌜i ∈ (↑N:coPset)⌝ ∧ ▷ □ (P' ↔ P) ∧ ownI i P')%I. + Definition internal_inv_aux : seal (@internal_inv_def). by eexists. Qed. + Definition internal_inv := internal_inv_aux.(unseal). + Definition internal_inv_eq : @internal_inv = @internal_inv_def := internal_inv_aux.(seal_eq). + Typeclasses Opaque internal_inv. + + Global Instance internal_inv_persistent N P : Persistent (internal_inv N P). + Proof. rewrite internal_inv_eq /internal_inv; apply _. Qed. + + Lemma internal_inv_open E N P : + ↑N ⊆ E → internal_inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True). + Proof. + rewrite internal_inv_eq /internal_inv_def uPred_fupd_eq /uPred_fupd_def. + iDestruct 1 as (i P') "(Hi & #HP' & #HiP)". + iDestruct "Hi" as % ?%elem_of_subseteq_singleton. + rewrite {1 4}(union_difference_L (↑ N) E) // ownE_op; last set_solver. + rewrite {1 5}(union_difference_L {[ i ]} (↑ N)) // ownE_op; last set_solver. + iIntros "(Hw & [HE $] & $) !> !>". + iDestruct (ownI_open i with "[$Hw $HE $HiP]") as "($ & HP & HD)". + iDestruct ("HP'" with "HP") as "$". + iIntros "HP [Hw $] !> !>". iApply (ownI_close _ P'). iFrame "HD Hw HiP". + iApply "HP'". iFrame. + Qed. + + Lemma internal_inv_alloc N E P : ▷ P ={E}=∗ internal_inv N P. + Proof. + rewrite internal_inv_eq /internal_inv_def uPred_fupd_eq. iIntros "HP [Hw $]". + iMod (ownI_alloc (∈ (↑N : coPset)) P with "[$HP $Hw]") + as (i ?) "[$ ?]"; auto using fresh_inv_name. + do 2 iModIntro. iExists i, P. rewrite -(iff_refl True%I). auto. + Qed. + + Lemma internal_inv_alloc_open N E P : + ↑N ⊆ E → (|={E, E∖↑N}=> internal_inv N P ∗ (▷P ={E∖↑N, E}=∗ True))%I. + Proof. + rewrite internal_inv_eq /internal_inv_def uPred_fupd_eq. iIntros (Sub) "[Hw HE]". + iMod (ownI_alloc_open (∈ (↑N : coPset)) P with "Hw") + as (i ?) "(Hw & #Hi & HD)"; auto using fresh_inv_name. + iAssert (ownE {[i]} ∗ ownE (↑ N ∖ {[i]}) ∗ ownE (E ∖ ↑ N))%I + with "[HE]" as "(HEi & HEN\i & HE\N)". + { rewrite -?ownE_op; [|set_solver..]. + rewrite assoc_L -!union_difference_L //. set_solver. } + do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw". + iSplitL "Hi". + { iExists i, P. rewrite -(iff_refl True%I). auto. } + iIntros "HP [Hw HE\N]". + iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[$ HEi]". + do 2 iModIntro. iSplitL; [|done]. + iCombine "HEi HEN\i HE\N" as "HEN". + rewrite -?ownE_op; [|set_solver..]. + rewrite assoc_L -!union_difference_L //; set_solver. + Qed. + + (** Invariants API *) + Definition inv_def (N: namespace) (P: iProp Σ) : iProp Σ := + (□ (∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True)))%I. + Definition inv_aux : seal (@inv_def). by eexists. Qed. + Definition inv := inv_aux.(unseal). + Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq). + Typeclasses Opaque inv. + + (** Properties about invariants *) + Global Instance inv_contractive N: Contractive (inv N). + Proof. rewrite inv_eq. solve_contractive. Qed. + + Global Instance inv_ne N : NonExpansive (inv N). + Proof. apply contractive_ne, _. Qed. + + Global Instance inv_proper N: Proper (equiv ==> equiv) (inv N). + Proof. apply ne_proper, _. Qed. + + Global Instance inv_persistent M P: Persistent (inv M P). + Proof. rewrite inv_eq. typeclasses eauto. Qed. + + Lemma inv_acc N P Q: + inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q. + Proof. + iIntros "#I #Acc". rewrite inv_eq. + iModIntro. iIntros (E H). iDestruct ("I" $! E H) as "#I'". + iApply fupd_wand_r. iFrame "I'". + iIntros "(P & Hclose)". iSpecialize ("Acc" with "P"). + iDestruct "Acc" as "[Q CB]". iFrame. + iIntros "Q". iApply "Hclose". now iApply "CB". + Qed. + + Lemma inv_iff N P Q : ▷ □ (P ↔ Q) -∗ inv N P -∗ inv N Q. + Proof. + iIntros "#HPQ #I". iApply (inv_acc with "I"). + iNext. iIntros "!# P". iSplitL "P". + - by iApply "HPQ". + - iIntros "Q". by iApply "HPQ". + Qed. + + Lemma inv_to_inv M P: internal_inv M P -∗ inv M P. + Proof. + iIntros "#I". rewrite inv_eq. iIntros (E H). + iPoseProof (internal_inv_open with "I") as "H"; eauto. + Qed. + + Lemma inv_alloc N E P : ▷ P ={E}=∗ inv N P. + Proof. + iIntros "P". iPoseProof (internal_inv_alloc N E with "P") as "I". + iApply fupd_mono; last eauto. + iApply inv_to_inv. + Qed. + + Lemma inv_alloc_open N E P : + ↑N ⊆ E → (|={E, E∖↑N}=> inv N P ∗ (▷P ={E∖↑N, E}=∗ True))%I. + Proof. + iIntros (H). iPoseProof (internal_inv_alloc_open _ _ _ H) as "H". + iApply fupd_mono; last eauto. + iIntros "[I H]"; iFrame; by iApply inv_to_inv. + Qed. + + Lemma inv_open E N P : + ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True). + Proof. + rewrite inv_eq /inv_def; iIntros (H) "#I". by iApply "I". + Qed. + + Lemma inv_open_strong E N P : + ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ ∀ E', ▷ P ={E',↑N ∪ E'}=∗ True. + Proof. + iIntros (?) "Hinv". iPoseProof (inv_open (↑ N) N P with "Hinv") as "H"; first done. + rewrite difference_diag_L. + iPoseProof (fupd_mask_frame_r _ _ (E ∖ ↑ N) with "H") as "H"; first set_solver. + rewrite left_id_L -union_difference_L //. iMod "H" as "[$ H]"; iModIntro. + iIntros (E') "HP". + iPoseProof (fupd_mask_frame_r _ _ E' with "(H HP)") as "H"; first set_solver. + by rewrite left_id_L. + Qed. + + Global Instance into_inv_inv N P : IntoInv (inv N P) N := {}. + + Global Instance into_acc_inv N P E: + IntoAcc (X := unit) (inv N P) + (↑N ⊆ E) True (fupd E (E ∖ ↑N)) (fupd (E ∖ ↑N) E) + (λ _ : (), (▷ P)%I) (λ _ : (), (▷ P)%I) (λ _ : (), None). + Proof. + rewrite inv_eq /IntoAcc /accessor bi.exist_unit. + iIntros (?) "#Hinv _". iApply "Hinv"; done. + Qed. + + Lemma inv_open_timeless E N P `{!Timeless P} : + ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ P ∗ (P ={E∖↑N,E}=∗ True). + Proof. + iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto. + iIntros "!> {$HP} HP". iApply "Hclose"; auto. + Qed. + + (* Weakening of semantic invariants *) + Lemma inv_proj_l N P Q: inv N (P ∗ Q) -∗ inv N P. + Proof. + iIntros "#I". iApply inv_acc; eauto. + iNext. iIntros "!# [$ Q] P"; iFrame. + Qed. + + Lemma inv_proj_r N P Q: inv N (P ∗ Q) -∗ inv N Q. + Proof. + rewrite (bi.sep_comm P Q). eapply inv_proj_l. + Qed. + + Lemma inv_split N P Q: inv N (P ∗ Q) -∗ inv N P ∗ inv N Q. + Proof. + iIntros "#H". + iPoseProof (inv_proj_l with "H") as "$". + iPoseProof (inv_proj_r with "H") as "$". + Qed. + +End inv. + diff --git a/theories/logrel_heaplang/lib/vectors.v b/theories/logrel_heaplang/lib/vectors.v index 5cbf420..22e8f88 100644 --- a/theories/logrel_heaplang/lib/vectors.v +++ b/theories/logrel_heaplang/lib/vectors.v @@ -1,18 +1,14 @@ From iris.heap_lang Require Export lifting metatheory. -From iris.base_logic.lib Require Import invariants. From iris.heap_lang Require Import notation proofmode. From iris_examples.logrel_heaplang Require Import ltyping ltyping_safety. From iris.algebra Require Import gmap auth agree. -From iris_examples.logrel_heaplang.lib Require Import arrays. +From iris_examples.logrel_heaplang.lib Require Import invariants arrays. Set Default Proof Using "Type". - - - Section Vectors. - (* vec = ref array *) + (* vec = ref array *) (* API *) Definition use : val := @@ -20,17 +16,15 @@ Set Default Proof Using "Type". let: "b" := copy "a" (!"a") in let: "v" := ref "b" in "f" #() "v". - Definition idx : val := λ: <> "v" "i", if: ((#-1) < "i") && ("i" < !(!"v")) then SOME "i" else NONE. - Definition get : val := λ: <> "v" "i", unsafe_get (!"v") "i". Definition set : val := λ: <> "v" "i" "x", (unsafe_set (!"v") "i") "x". - + Definition app : val := λ: <> , rec: "f" "v" "x" := let: "a" := !"v" in @@ -39,28 +33,34 @@ Set Default Proof Using "Type". if: CAS "v" "a" "b" then #() else "f" "v" "x". + (* History *) + Definition Hist := gmap loc nat. + Definition HistUR := gmapUR loc (agreeR (leibnizO nat)). + Definition hist : Hist → HistUR := fmap (λ v: nat, to_agree (v : leibnizO nat)). + Implicit Types (h : Hist) (a: loc). + Context `{!heapG Σ, !inG Σ (authR mnatUR), (* maximum length *) - !inG Σ (authR (gmapUR loc (agreeR (leibnizC nat)))) (* history *) + !inG Σ (authR HistUR) (* history *) }. (* Maximum Length *) Global Instance auth_mnat_persistent (n: mnat) γ: Persistent (own γ (◯ n)). Proof. - eapply own_core_persistent, auth_frag_core_id, mnat_core_id. + eapply own_core_persistent, auth_frag_core_id, mnat_core_id. Qed. - + Lemma auth_mnat_alloc (n: mnat) : (|==> ∃ γ, own γ (● n) ∗ own γ (◯ n))%I. Proof. iMod (own_alloc (● n ⋅ ◯ n)) as (γ) "[??]". eapply auth_both_valid_2; done. - eauto with iFrame. + eauto with iFrame. Qed. Lemma auth_mnat_agree γ (m n : mnat): own γ (● m) -∗ own γ (◯ n) -∗ ⌜n <= m⌝. Proof. - iIntros "Hγ● Hγ◯". + iIntros "Hγ● Hγ◯". iDestruct (own_valid_2 with "Hγ● Hγ◯") as "%". eapply auth_both_valid in H as [H _]. iPureIntro. eapply mnat_included in H. lia. @@ -79,64 +79,59 @@ Set Default Proof Using "Type". Proof. intros H. eapply own_mono. eapply (auth_frag_mono n m), mnat_included. lia. Qed. - + Lemma auth_mnat_update γ (n p: mnat): n <= p -> own γ (● n) ==∗ own γ (● p). Proof. iIntros (H) "Hγ●". - iMod (auth_mnat_fork with "Hγ●") as "[Hγ● Hγ◯]"; eauto. + iMod (auth_mnat_fork with "Hγ●") as "[Hγ● Hγ◯]"; eauto. iMod (own_update_2 _ _ _ (● p ⋅ ◯ p) with "Hγ● Hγ◯") as "[$ _]"; eauto. eapply auth_update, mnat_local_update; lia. Qed. - (* History *) - Definition Hist := gmap loc nat. - Definition HistUR := gmapUR loc (agreeR (leibnizC nat)). - Definition hist: Hist -> HistUR := fmap (λ v, to_agree (v : leibnizC nat)). - Implicit Types (h : Hist) (a: loc). + Section hist. (** Conversion to hists and back *) Lemma hist_valid h : ✓ hist h. Proof. intros l. rewrite lookup_fmap. by case (h !! l). Qed. - + Lemma lookup_hist_None h a : h !! a = None → hist h !! a = None. Proof. by rewrite /hist lookup_fmap=> ->. Qed. - + Lemma hist_singleton_included h a m : {[a := to_agree m]} ≼ hist h → h !! a = Some m. Proof. rewrite singleton_included=> -[a' []]. - rewrite /hist lookup_fmap fmap_Some_equiv => -[m' [-> H]]. rewrite H. + rewrite /hist lookup_fmap fmap_Some_equiv => -[m' [-> H]]. rewrite H. move=> /Some_included_total /to_agree_included /leibniz_equiv_iff -> //. Qed. - + Lemma hist_insert h a m : - hist (<[a:=m]> h) = <[a:= to_agree (m: leibnizC nat)]> (hist h). + hist (<[a:=m]> h) = <[a:= to_agree (m: leibnizO nat)]> (hist h). Proof. by rewrite /hist fmap_insert. Qed. - + Lemma hist_delete a h : hist (delete a h) = delete a (hist h). Proof. by rewrite /hist fmap_delete. Qed. End hist. - Definition hist_all γ h : iProp Σ := - (own γ (● (hist h)))%I. + Definition hist_all γ h : iProp Σ := (own γ (● (hist h)))%I. Definition hist_entry γ a m : iProp Σ := - (own γ (◯ {[ a := to_agree (m : leibnizC nat)]}))%I. - + (own γ (◯ {[ a := to_agree (m : leibnizO nat)]}))%I. + Global Instance hist_persistent a m γ: Persistent (hist_entry γ a m). Proof. eapply _. Qed. - + Lemma hist_alloc: (|==> ∃ γ, hist_all γ ∅)%I. Proof. iMod (own_alloc (● (hist ∅))) as (γ) "H". - eapply auth_auth_valid, hist_valid. + eapply auth_auth_valid, hist_valid. eauto with iFrame. Qed. - + Lemma hist_update γ h a m: (h !! a = None) -> hist_all γ h ==∗ hist_all γ (<[a := m]> h) ∗ hist_entry γ a m. @@ -156,7 +151,7 @@ Set Default Proof Using "Type". f_equiv. rewrite auth_frag_valid /=. rewrite op_singleton singleton_valid. by intros ?%agree_op_invL'. Qed. - + Lemma hist_agree γ h a m: hist_all γ h -∗ hist_entry γ a m -∗ ⌜h !! a = Some m⌝. Proof. @@ -167,11 +162,11 @@ Set Default Proof Using "Type". Qed. - - + + Variable (N: namespace). - + Definition Vec_inv γ1 γ2 (l: loc) : iProp Σ := (∃ (h: Hist) (a: loc) (m: mnat), l ↦ #a ∗ @@ -185,18 +180,17 @@ Set Default Proof Using "Type". Lemma Vec_project_array γ1 γ2 a m l: - hist_entry γ2 a m -∗ Vec γ1 γ2 l -∗ Inv N (array m a). + hist_entry γ2 a m -∗ Vec γ1 γ2 l -∗ inv N (array m a). Proof. - iIntros "#E #V". iPoseProof (inv_to_Inv with "V") as "Vec". - iApply Inv_acc; eauto. - iModIntro. iDestruct 1 as (h b n) "(Hl & Hγ1● & Hγ2● & Hγ2◯ & Hst)". + iIntros "#E #V". iApply inv_acc; eauto. + iNext. iModIntro. iDestruct 1 as (h b n) "(Hl & Hγ1● & Hγ2● & Hγ2◯ & Hst)". iAssert (⌜h !! a = Some m⌝)%I with "[Hγ2●]" as "#H". { iApply (hist_agree with "[Hγ2●]"); eauto. } iAssert ((array m a ∗ (array m a -∗ [∗ map] a ↦ m ∈ h, array (Z.of_nat m) a)))%I with "[Hst]" as "(Ha & Hst)". { iDestruct "H" as %H1. now iApply (big_sepM_lookup_acc with "Hst"). } - iFrame. iIntros "Ha". + iFrame. iIntros "Ha". iExists h, b, n. iFrame. now iApply "Hst". Qed. @@ -204,31 +198,31 @@ Set Default Proof Using "Type". (* Function Verification *) Definition ι γ1 γ2 : val := PairV (#(Z.pos γ1)) (#(Z.pos γ2)). - + Definition β γ1 γ2 : lty Σ := Lty (fun v => ⌜v = ι γ1 γ2⌝)%I. - + Definition Index (S: lty Σ) : lty Σ := Lty (fun v => (□ ∃ γ1 γ2 (i: mnat), (∀ v, S v ∗-∗ β γ1 γ2 v) ∗ ⌜v = #i⌝ ∗ Idx γ1 i)%I). Definition Vector (S: lty Σ) : lty Σ := Lty (fun v => (□ ∃ γ1 γ2 (l: loc), (∀ v, S v ∗-∗ β γ1 γ2 v) ∗ ⌜v = #l⌝ ∗ Vec γ1 γ2 l)%I). - + Lemma typing_use: ∅ ⊨ use : ∀ T, Array N → (∀ S, Vector S → T) → T. - Proof. unfold use. - iIntros (s) "!# #T /=". + Proof. unfold use. + iIntros (s) "!# #T /=". iApply wp_value. - iIntros (S) "!#". wp_pures. + iIntros (S) "!#". wp_pures. iIntros (v1) "!# #Array". wp_pures. iIntros (v2) "!# #Cont". wp_pures. - iDestruct "Array" as (a m) "[Array ->]". - wp_bind (! #a)%E. - iInv "Array" as "[Ha Hl]" "Hclose". wp_load. iMod ("Hclose" with "[$Ha $Hl]") as "_". + iDestruct "Array" as (a m) "[Array ->]". + wp_bind (! #a)%E. iPoseProof (array_length_inv with "Array") as "L". + iInv "L" as "Ha" "Hclose". wp_load. iMod ("Hclose" with "Ha") as "_". iModIntro. wp_apply (copy_spec); eauto with lia. iIntros (b) "B". wp_pures. wp_bind (ref _)%E. wp_apply wp_fupd. wp_alloc l as "Hl". iMod (auth_mnat_alloc m) as (γ1) "[Hγ1● _]". iMod (hist_alloc) as (γ2) "Hγ2●". - iMod (hist_update γ2 ∅ b m with "[Hγ2●]") as "[Hγ2● #Hγ2◯]"; eauto. + iMod (hist_update γ2 ∅ b m with "[Hγ2●]") as "[Hγ2● #Hγ2◯]"; eauto. iMod (inv_alloc N _ (Vec_inv γ1 γ2 l) with "[Hγ1● Hγ2● Hl B]") as "#I". - iNext. iExists {[ b := m ]}, b, m. iFrame. iSplit; eauto. now rewrite big_sepM_singleton. @@ -239,14 +233,14 @@ Set Default Proof Using "Type". Qed. - + Lemma typing_idx: ∅ ⊨ idx : (∀ S, Vector S → lty_int → Option (Index S)). Proof. unfold idx. iIntros (s) "!# T /=". iApply wp_value. iIntros (S) "!#". wp_pures. - iIntros (v1) "!# #Vec". wp_pures. + iIntros (v1) "!# #Vec". wp_pures. iIntros (v2) "!# #Int". wp_pures. - iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & V)". + iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & V)". iDestruct "Int" as (n) "->". wp_pures. bool_decide H; last (wp_pures; now iLeft). wp_pures. wp_bind (! #l)%E. iInv "V" as (h a m) "(H1 & H2 & H3 & #Ha & H4)" "Hclose". @@ -254,14 +248,15 @@ Set Default Proof Using "Type". iMod("Hclose" with "[H1 H2 H3 H4]") as "_". iNext; iExists h, a, m; iFrame; eauto. iModIntro. iPoseProof (Vec_project_array with "Ha V") as "I". - wp_bind (! _)%E. iInv "I" as "[Hb Aa]" "Hclose". wp_load. - iMod("Hclose" with "[$Hb $Aa]") as "_". iModIntro. wp_pures. + wp_bind (! _)%E. iPoseProof (array_length_inv with "I") as "L". + iInv "L" as "H" "Hclose". wp_load. iMod ("Hclose" with "H") as "_". + iModIntro. wp_pures. bool_decide H'; last (wp_pures; now iLeft). wp_pures. iRight. iExists #n. iSplit; eauto. destruct (Z_to_nat n) as [k ->]; first lia. iExists γ1, γ2, k. iModIntro. repeat iSplit; eauto. - iApply auth_mnat_previous; eauto. lia. + iApply auth_mnat_previous; eauto. lia. Qed. @@ -269,97 +264,94 @@ Set Default Proof Using "Type". Proof. unfold get. iIntros (s) "!# T /=". iApply wp_value. iIntros (S) "!#". wp_pures. - iIntros (v1) "!# #Vec". wp_pures. + iIntros (v1) "!# #Vec". wp_pures. iIntros (v2) "!# #Idx". wp_pures. - iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & V)". + iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & V)". iDestruct "Idx" as (γ1' γ2' i) "(EQ' & -> & I)". iAssert (β γ1 γ2 (ι γ1' γ2'))%I as "%". { iApply "EQ". iApply "EQ'". now iPureIntro. } - injection H as -> ->. + injection H as -> ->. wp_bind (! _)%E. iInv "V" as (h a m) "(H1 & H2 & H3 & #Ha & H4)" "Hclose". wp_load. iDestruct (auth_mnat_agree with "H2 I") as %H. - iMod("Hclose" with "[H1 H2 H3 H4]") as "_". + iMod("Hclose" with "[H1 H2 H3 H4]") as "_". iNext; iExists h, a, m; iFrame; eauto. iModIntro. wp_apply (unsafe_get_spec); eauto. iSplit. - iApply Vec_project_array; eauto. iPureIntro; lia. + iApply Vec_project_array; eauto. iPureIntro; lia. Qed. - + Lemma typing_set: ∅ ⊨ set : (∀ S, Vector S → Index S → lty_int → lty_unit). Proof. unfold set. iIntros (s) "!# T /=". iApply wp_value. iIntros (S) "!#". wp_pures. - iIntros (v1) "!# #Vec". wp_pures. + iIntros (v1) "!# #Vec". wp_pures. iIntros (v2) "!# #Idx". wp_pures. - iIntros (v3) "!# #Int". wp_pures. - iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & V)". + iIntros (v3) "!# #Int". wp_pures. + iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & V)". iDestruct "Idx" as (γ1' γ2' i) "(EQ' & -> & I)". iDestruct "Int" as (n) "->". iAssert (β γ1 γ2 (ι γ1' γ2'))%I as "%". { iApply "EQ". iApply "EQ'". now iPureIntro. } - injection H as -> ->. + injection H as -> ->. wp_bind (! _)%E. iInv "V" as (h a m) "(H1 & H2 & H3 & #Ha & H4)" "Hclose". wp_load. iDestruct (auth_mnat_agree with "H2 I") as %H. - iMod("Hclose" with "[H1 H2 H3 H4]") as "_". + iMod("Hclose" with "[H1 H2 H3 H4]") as "_". iNext; iExists h, a, m; iFrame; eauto. iModIntro. wp_apply (unsafe_set_spec); eauto. iSplit. - iApply Vec_project_array; eauto. iPureIntro; lia. + iApply Vec_project_array; eauto. iPureIntro; lia. Qed. Lemma typing_app: ∅ ⊨ app : (∀ S, Vector S → lty_int → lty_unit). Proof. iIntros (s) "!# #T /=". - unfold app. + unfold app. iApply wp_value. iIntros (S) "!#". wp_pures. - iIntros (v1) "!# #Vec". wp_pures. + iIntros (v1) "!# #Vec". wp_pures. iIntros (v2) "!# #Int". wp_pures. fold app. iLöb as "IH" forall (v1 v2) "Vec Int". - iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & Vec)". + iDestruct "Vec" as (γ1 γ2 l) "(EQ & -> & Vec)". iDestruct "Int" as (n) "->". wp_bind (! #l)%E. iInv "Vec" as (h a m) "(Hl & Hγ1● & Hγ2 & #Ha & Hst)" "Hclose". wp_load. iMod ("Hclose" with "[Hl Hγ1● Hγ2 Hst]") as "_". iNext. iExists h, a, m. iFrame; eauto. - clear h. iModIntro. iPoseProof (Vec_project_array with "Ha Vec") as "#HA". - wp_pures. wp_bind (! #a)%E. - iInv "HA" as "[Hal A]" "Hclose". wp_load. iMod ("Hclose" with "[$Hal $A]") as "_". + clear h. iModIntro. iPoseProof (Vec_project_array with "Ha Vec") as "#HA". + wp_pures. wp_bind (! #a)%E. iPoseProof (array_length_inv with "HA") as "L". + iInv "L" as "H" "Hclose". wp_load. iMod ("Hclose" with "H") as "_". iModIntro. wp_pures. wp_apply (copy_spec with "[]"); first eauto with lia. iIntros (b) "A". wp_pures. - wp_bind (! #a)%E. iInv "HA" as "[Hb Aa]" "Hclose". wp_load. - iMod("Hclose" with "[$Hb $Aa]") as "_". iModIntro. wp_pures. - iDestruct "A" as "[Hb Hst]". rewrite /body big_opR_acc. - iDestruct "Hst" as "[Hbm Hst]". - iDestruct "Hbm" as (v') "Hbm". rewrite loc_add_assoc. - wp_store. 2: lia. - iSpecialize ("Hst" with "[Hbm]"); eauto. iCombine "Hb Hst" as "Hb". - wp_bind (CAS _ _ _). + wp_bind (! #a)%E. iInv "L" as "Hb" "Hclose". wp_load. + iMod("Hclose" with "Hb") as "_". iModIntro. wp_pures. + iPoseProof (array_entry_acc m with "[] A") as "[E A]"; first (iPureIntro; lia). + iDestruct "E" as (v) "E". wp_store. iSpecialize ("A" with "[E]"); first by iExists _. + wp_bind (CmpXchg _ _ _). iInv "Vec" as (h a' m') "(Hl & Hγ1● & Hγ2 & #Ha' & Hst)" "Hclose". - wp_cas as H|H. + wp_cmpxchg as H|H. - injection H as ?; subst. iPoseProof (entry_agree with "Ha Ha'") as "%"; subst m'. - iMod (auth_mnat_update _ _ (m + 1)%nat with "Hγ1●") as "Hγ1●"; try lia. - iAssert (⌜h !! b = None⌝)%I with "[Hb Hst]" as "%". - { destruct (h !! b) eqn: H; eauto. - iPoseProof (big_sepM_insert_acc with "Hst") as "Hst"; eauto. - iDestruct "Hb" as "[H1?]". iDestruct "Hst" as "[[H2?]?]". - iPoseProof (mapsto_valid_2 with "H1 H2") as "%". - exfalso. + iMod (auth_mnat_update _ _ (m + 1)%nat with "Hγ1●") as "Hγ1●"; try lia. + iAssert (⌜h !! b = None⌝)%I with "[A Hst]" as "%". + { destruct (h !! b) eqn: H; eauto. + iPoseProof (big_sepM_insert_acc with "Hst") as "[Hst _]"; eauto. + iPoseProof (array_length_acc with "A") as "[H1 _]". + iPoseProof (array_length_acc with "Hst") as "[H2 _]". + iPoseProof (mapsto_valid_2 with "H1 H2") as "%". exfalso. destruct (frac.frac_valid' 2%Qp) as [H1 _]. eapply H1 in H0. now eapply Qp_not_plus_q_ge_1 in H0. } - iMod (hist_update _ _ _ (m + 1)%nat with "Hγ2") as "[Hγ2 #Hb_ent]"; eauto. - iMod ("Hclose" with "[Hl Hγ1● Hγ2 Hb Hst]") as "_". + iMod (hist_update _ _ _ (m + 1)%nat with "Hγ2") as "[Hγ2 #Hb_ent]"; eauto. + iMod ("Hclose" with "[Hl Hγ1● Hγ2 A Hst]") as "_". iNext. iExists (<[b:=(m + 1)%nat]> h), b, ((m + 1)%nat). iFrame. iSplit; eauto. rewrite big_sepM_insert; eauto; iFrame. replace ((m + 1)%nat : Z) with (m + 1) by lia. - iFrame. iModIntro. wp_pures. done. - - iMod ("Hclose" with "[Hl Hγ1● Hγ2 Hb Hst]") as "_". + iFrame. iModIntro. wp_pures. done. + - iMod ("Hclose" with "[Hl Hγ1● Hγ2 A Hst]") as "_". iNext. iExists h, a', m'. iFrame; eauto. iModIntro. wp_pures. iApply "IH". iModIntro. iExists γ1, γ2, l. repeat iSplit; eauto. - iModIntro. iExists n. done. + iModIntro. iExists n. done. Qed. -End Vectors. \ No newline at end of file +End Vectors. -- GitLab