branding examples

_CoqProject

@@ -80,6 +80,8 @@ 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/arrays.v
+theories/logrel_heaplang/lib/vectors.v
 
 theories/hocap/abstract_bag.v
 theories/hocap/cg_bag.v

theories/logrel_heaplang/lib/arrays.v

+From iris.algebra Require Import auth agree.
+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 Require Import ltyping ltyping_safety.
+
+
+(* utility stuff *)
+Ltac bool_decide H :=
+  match goal with
+  | [ |- context[@bool_decide ?P ?d]] =>
+    destruct d as [H|H];
+    [rewrite  bool_decide_true; [|exact H]|rewrite  bool_decide_false; [|exact H]]
+  end.
+
+Lemma Z_to_nat n: n >= 0 -> ∃ m: nat, n = m.
+Proof.
+  intros; exists (Z.to_nat n); rewrite Z2Nat.id; lia. 
+Qed.
+
+
+
+(** 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}.
+
+
+  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.
+
+  
+  Lemma big_opR_empty m n ϕ:
+    n <= m -> (([∗ range] m <= i < n, ϕ i) ⊣⊢ emp)%I.
+  Proof.
+   intros; rewrite range_empty; try lia. reflexivity. 
+  Qed.
+
+
+  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.
+
+  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.
+
+  Lemma big_opR_singleton k ϕ:
+    (([∗ range] k <= i < k + 1, ϕ i) ⊣⊢ ϕ k)%I.
+  Proof.
+    rewrite range_step; try lia. rewrite range_empty; try lia.
+    now rewrite big_sepL_singleton. 
+  Qed.
+
+  Lemma big_opR_shift k m n ϕ:
+    (([∗ range] (k + m) <= i < (k + n), ϕ i) ⊣⊢ ([∗ range] m <= i < n, ϕ (k + i)))%I.
+  Proof.
+    rewrite range_shift. induction (range m n); cbn; eauto.
+    now rewrite IHl. 
+  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.
+  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. 
+  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.
+  Proof.
+    intros H; rewrite big_opR_split -?big_opR_step; eauto; lia. 
+  Qed.
+
+  Lemma big_opR_acc n m k ϕ:
+    n <= k < m -> ([∗ range] n <= i < m, ϕ i) ⊣⊢ ϕ k ∗ (ϕ k -∗ [∗ range] n <= i < m, ϕ i).
+  Proof.
+    intros H; rewrite big_opR_split_three; eauto. iSplit.
+    - iIntros "(H1 & H2 & H3)". iFrame. eauto.
+    - iIntros "(H1 & H2)". iApply "H2". iFrame.
+  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.
+  Proof.
+    iIntros "#I". rewrite Inv_eq. iIntros (E H).
+    iPoseProof (inv_open with "I") as "H"; eauto.
+  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).
+  Proof.
+    rewrite Inv_eq /IntoAcc /accessor bi.exist_unit. 
+    iIntros (?) "#Hinv _". iApply "Hinv"; done.
+  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.
+  Proof.
+    iIntros "#I". iApply Inv_acc; eauto.
+    iModIntro. iIntros "[$ Q] P"; iFrame.
+  Qed.
+
+  Lemma Inv_proj_r M P Q: Inv M (P ∗ Q) -∗ Inv M Q.
+  Proof.
+    rewrite (bi.sep_comm P Q). eapply Inv_proj_l. 
+  Qed.
+
+  
+  Lemma Inv_split M P Q: Inv M (P ∗ Q) -∗ Inv M P ∗ Inv M Q.
+  Proof.
+    iIntros "#H".
+    iPoseProof (Inv_proj_l with "H") as "$".
+    iPoseProof (Inv_proj_r with "H") as "$".
+  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 _ _).
+    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.
+  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 }}}.
+  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.
+    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 }}}.
+  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.
+    now iApply "Post".
+  Qed.
+
+
+
+  (** Semantic Types *)
+  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).
+
+  Lemma typing_arr: ∅ ⊨ arr : lty_int → Option Array.
+  Proof.
+    iIntros (s) "!# _ /=". iApply wp_value.
+    iIntros (v1) "!#". iDestruct 1 as (z) "->".
+    unfold arr. wp_pures.
+    bool_decide H; wp_pures.
+    - iLeft. eauto.
+    - wp_apply wp_fupd.
+      wp_apply (unsafe_arr_spec); eauto with lia.
+      iIntros (l) "A".
+      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.
+  Qed.
+
+  Lemma typing_get: ∅ ⊨ get : Array → lty_int → Option lty_int.
+  Proof.
+    iIntros (s) "!# _ /=". iApply wp_value.
+    iIntros (v) "!#". iDestruct 1 as (a m) "[#I ->]".
+    unfold get. wp_pures.
+    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_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. 
+  Qed.
+
+
+  Lemma typing_set: ∅ ⊨ set : Array → lty_int → lty_int → lty_unit.
+  Proof.
+    iIntros (s) "!# _ /=". iApply wp_value.
+    iIntros (v) "!#". iDestruct 1 as (a m) "[#I ->]".
+    unfold set. wp_pures.
+    iIntros (v) "!#". iDestruct 1 as (i) "->".
+    wp_pures.
+    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_pures. wp_apply (unsafe_set_spec); first iSplit; eauto with lia.
+      + now wp_pures.  
+    - now wp_pures.  
+  Qed.
+  
+  
+
+  (** Copying Arrays *)
+  Definition copy_rec : val :=
+    rec: "f" "old" "new" "n" :=
+      if: #0 < "n" then ("new" + #1) <- !("old" + #1);; "f" ("old" + #1) ("new" + #1) ("n" - #1)
+      else #().
+
+  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⌝ }}}
+      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.                                                   
+    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; iApply "Post"; eauto.
+  Qed.
+
+
+  Lemma copy_spec (a: loc) (m n: Z):
+    {{{ 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.
+  Qed.
+     
+  
+End Arrays.
+

theories/logrel_heaplang/lib/vectors.v

+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.
+
+Set Default Proof Using "Type".
+
+
+
+ 
+ Section Vectors.
+
+  (* vec = ref array *) 
+
+  (* API *)
+  Definition use : val :=
+    λ: <> "a" "f" ,
+    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
+      let: "b" := copy "a" (!"a" + #1) in
+      "b" + !"a" + #1 <- "x";;
+      if: CAS "v" "a" "b" then #() else "f" "v" "x".
+
+
+  Context `{!heapG Σ,
+            !inG Σ (authR mnatUR), (* maximum length *)
+            !inG Σ (authR (gmapUR loc (agreeR (leibnizC nat)))) (* 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.  
+  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. 
+  Qed.
+
+  Lemma auth_mnat_agree γ (m n : mnat):
+    own γ (● m) -∗ own γ (◯ n) -∗ ⌜n <= m⌝.
+  Proof.
+    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.