[do not merge] lc + receipts + num_laters_per_step in eris

.github/workflows/build.yml

@@ -39,10 +39,14 @@ jobs:
             startGroup "Install dependencies"
               opam install odoc -y
               apt-get install rsync -y
+              opam pin add -y rocq-stdpp 1.13.0
+              opam pin add -y rocq-iris.dev  git+https://gitlab.mpi-sws.org/iris/iris.git#93c7df745a0485cebcb97ca77e7d263e5c920d4f --ignore-constraints-on=rocq-stdpp
               opam pin add -n -y -k path $PACKAGE $WORKDIR
               opam update -y
               opam reinstall --forget-pending --yes
-              opam install --confirm-level=unsafe-yes -j 2 $PACKAGE --deps-only --with-doc
+              opam install --confirm-level=unsafe-yes -j 2 rocq-stdpp.1.13.0
+              opam install --confirm-level=unsafe-yes -j 2 \
+                --ignore-constraints-on=rocq-stdpp $PACKAGE --deps-only --with-doc
             endGroup
           script: |
             startGroup Build

dune-project

@@ -2,9 +2,9 @@
 
 (using rocq 0.11)
 
-; (name clutch)
+(name rocq-clutch)
 
-(generate_opam_files true)
+(generate_opam_files false)
 
 (source (github logsem/clutch))
 
@@ -33,7 +33,7 @@
   ; at least rocq 9.1 is needed to work with dune's rocq-lang feature
   (rocq-core (and (>= 9.1.1) (< "9.2~")))
   (rocq-stdlib (and (>= 9.0.0) (< "9.2~")))
-  (rocq-iris (= "4.5.0"))
+  (rocq-iris (= "dev"))
   (rocq-stdpp (= "1.13.0"))
   (coq-coquelicot (= "3.4.4"))
   (coq-autosubst (= "dev"))

rocq-clutch.opam

@@ -1,4 +1,3 @@
-# This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 synopsis: "Higher-order probabilistic separation logics"
 maintainer: ["Simon Oddershede Gregersen <s.gregersen@nyu.edu>"]
@@ -20,7 +19,11 @@ depends: [
   "ocaml" {>= "5.4.0" & < "5.5~"}
   "rocq-core" {>= "9.1.1" & < "9.2~"}
   "rocq-stdlib" {>= "9.0.0" & < "9.2~"}
-  "rocq-iris" {= "4.5.0"}
+  # NOTE: Mainline iris pinned to the merge of MR 1217.
+  # main iris opam declares a strict stdpp dev constraint, but its
+  # Rocq source is compatible with stdpp 1.13.0.
+  # Install with: [opam install . --ignore-constraints-on=rocq-stdpp]
+  "rocq-iris" {= "dev"}
   "rocq-stdpp" {= "1.13.0"}
   "coq-coquelicot" {= "3.4.4"}
   "coq-autosubst" {= "dev"}

theories/approxis/primitive_laws.v

@@ -47,7 +47,7 @@ Definition tapes_auth `{approxisGS Σ} :=
 
 Global Instance approxisGS_irisGS `{!approxisGS Σ} : approxisWpGS prob_lang Σ := {
   approxisWpGS_invGS := approxisGS_invG;
-  state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes))%I;
+  state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes))%I;
   err_interp := ec_supply;
 }.
 

theories/caliper/primitive_laws.v

@@ -46,7 +46,7 @@ Definition tapes_auth `{caliperG δ Σ} :=
 #[export] Instance caliperG_caliperWpG `{caliperG δ Σ} : caliperWpG δ prob_lang Σ := {
   caliperWpG_invGS := caliperG_invG;
 
-  state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes))%I;
+  state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes))%I;
 }.
 
 (** Heap *)

theories/clutch/examples/keyed_hash.v

@@ -294,13 +294,13 @@ Section keyed_hash.
   Definition keyed_hash_auth (γ : gname) (f : val) : iProp Σ :=
     ∃ (f0 : val) (mphys : gmap nat bool) (mghost : gmap fin_hash_dom_space (option bool)),
       keyed_hash_auth_pure f f0 mphys mghost ∗
-      ghost_map_auth γ 1 mghost ∗
+      ghost_map_auth γ (DfracOwn 1) mghost ∗
       hashfun' MAX_HASH_DOM f0 mphys.
 
   Definition skeyed_hash_auth (γ : gname) (f : val) : iProp Σ :=
     ∃ (f0 : val) (mphys : gmap nat bool) (mghost : gmap fin_hash_dom_space (option bool)),
       keyed_hash_auth_pure f f0 mphys mghost ∗
-      ghost_map_auth γ 1 mghost ∗
+      ghost_map_auth γ (DfracOwn 1) mghost ∗
       shashfun' MAX_HASH_DOM f0 mphys.
 
   Section timeless_spec.

theories/clutch/primitive_laws.v

@@ -43,7 +43,7 @@ Definition tapes_auth `{clutchGS Σ} :=
 
 #[global] Instance clutchGS_clutchWpGS `{!clutchGS Σ} : clutchWpGS prob_lang Σ := {
   clutchWpGS_invGS := clutchGS_invG;
-  state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes))%I;
+  state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes))%I;
 }.
 
 (** Heap *)

theories/con_prob_lang/spec/spec_ra.v

@@ -66,11 +66,11 @@ Qed.
 Section resources.
   Context `{!specG_con_prob_lang Σ}.
   Definition spec_prog_auth :=
-    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_prog specG_con_prob_lang_prog_name 1.
+    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_prog specG_con_prob_lang_prog_name (DfracOwn 1).
   Definition spec_heap_auth :=
-    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_heap specG_con_prob_lang_heap_name 1.
+    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_heap specG_con_prob_lang_heap_name (DfracOwn 1).
   Definition spec_tapes_auth  :=
-    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_tapes specG_con_prob_lang_tapes_name 1.
+    @ghost_map_auth _ _ _ _ _ specG_con_prob_lang_tapes specG_con_prob_lang_tapes_name (DfracOwn 1).
 
   Definition spec_auth (ρ : cfg) : iProp Σ :=
     spec_prog_auth (to_tpool ρ.1) ∗

theories/coneris/examples/con_two_add.v

@@ -98,7 +98,7 @@ Section complex'.
      form of the paper *)
 
   Definition parallel_add_inv' (γ1 γ2: gname) l: iProp Σ :=
-    ∃ (s1 s2 : T), ghost_var γ1 (1/2) s1 ∗ ghost_var γ2 (1/2) s2 ∗
+    ∃ (s1 s2 : T), ghost_var γ1 (DfracOwn (1/2)) s1 ∗ ghost_var γ2 (DfracOwn (1/2)) s2 ∗
       (((l ↦ #0 ∗ ⌜ no_thread_added s1 s2 ⌝) ∨
          (∃ n : nat, l ↦ #n ∗ ⌜ one_thread_added n s1 s2 ⌝) ∨
          (∃ n : nat, l ↦ #n ∗ ⌜ n > 0 ⌝ ∗ ⌜ both_threads_added n s1 s2 ⌝)) ∗
@@ -138,9 +138,9 @@ Section complex'.
   Qed.
 
   Lemma rand_step γ1 γ2 l:
-    {{{ inv nroot (parallel_add_inv' γ1 γ2 l) ∗ ghost_var γ1 (1/2) S0 }}}
+    {{{ inv nroot (parallel_add_inv' γ1 γ2 l) ∗ ghost_var γ1 (DfracOwn (1/2)) S0 }}}
       rand #3
-      {{{ (n: nat), RET #n; ghost_var γ1 (1/2) (S1 n) }}}.
+      {{{ (n: nat), RET #n; ghost_var γ1 (DfracOwn (1/2)) (S1 n) }}}.
   Proof.
     iIntros (Φ) "(#I&Hfrag1) HΦ".
     iInv "I" as ">(%s1&%s2&Hauth1&Hauth2&Hstate&Hsamp)".
@@ -194,9 +194,9 @@ Section complex'.
   Qed.
 
   Lemma faa_step γ1 γ2 l (n: nat) :
-    {{{ inv nroot (parallel_add_inv' γ1 γ2 l) ∗ ghost_var γ1 (1/2) (S1 n) }}}
+    {{{ inv nroot (parallel_add_inv' γ1 γ2 l) ∗ ghost_var γ1 (DfracOwn (1/2)) (S1 n) }}}
       FAA #l #n
-    {{{ (v : val), RET v; ghost_var γ1 (1/2) (S2 n) }}}.
+    {{{ (v : val), RET v; ghost_var γ1 (DfracOwn (1/2)) (S2 n) }}}.
   Proof.
     iIntros (Φ) "(#I&Hfrag1) HΦ".
     iInv "I" as ">(%s1&%s2&Hauth1&Hauth2&Hstate&Hsamp)".
@@ -272,8 +272,8 @@ Section complex'.
       { iPureIntro. left. by eauto. }
       { iLeft. iFrame. }
     }
-    wp_apply (wp_par (λ _, ∃ (n:nat), ghost_var γ1 (1/2) (S2 n))%I
-                (λ _, ∃ (n:nat), ghost_var γ2 (1/2) (S2 n))%I with "[Hfrag1][Hfrag2]").
+    wp_apply (wp_par (λ _, ∃ (n:nat), ghost_var γ1 (DfracOwn (1/2)) (S2 n))%I
+                (λ _, ∃ (n:nat), ghost_var γ2 (DfracOwn (1/2)) (S2 n))%I with "[Hfrag1][Hfrag2]").
     - wp_apply (rand_step with "[$]").
       iIntros (n) "Hfrag1".
       wp_apply (faa_step with "[$]").
@@ -305,7 +305,7 @@ Section complex'.
   Qed.
 
   Definition gs γ1 γ2 P : iProp Σ :=
-    ∃ (s1 s2 : T), ghost_var γ1 (1/2/2) s1 ∗ ghost_var γ2 (1/2/2) s2 ∗ ⌜ P s1 s2 ⌝.
+    ∃ (s1 s2 : T), ghost_var γ1 (DfracOwn (1/2/2)) s1 ∗ ghost_var γ2 (DfracOwn (1/2/2)) s2 ∗ ⌜ P s1 s2 ⌝.
 
   (* In the paper we do not have leading existentials in the descriptions of the invariant.
      This alternate version matching the paper is defined next . It is equivalent to what
@@ -327,7 +327,7 @@ Section complex'.
          (∃ n : nat, l ↦ #n ∗ gs γ1 γ2 (one_thread_added n)) ∨
          (∃ n : nat, l ↦ #n ∗ ⌜ n > 0 ⌝ ∗ gs γ1 γ2 (both_threads_added n)))
    -∗
-    ∃ (s1 s2 : T), ghost_var γ1 (1/2/2) s1 ∗ ghost_var γ2 (1/2/2) s2 ∗
+    ∃ (s1 s2 : T), ghost_var γ1 (DfracOwn (1/2/2)) s1 ∗ ghost_var γ2 (DfracOwn (1/2/2)) s2 ∗
       (((l ↦ #0 ∗ ⌜ no_thread_added s1 s2 ⌝) ∨
          (∃ n : nat, l ↦ #n ∗ ⌜ one_thread_added n s1 s2 ⌝) ∨
          (∃ n : nat, l ↦ #n ∗ ⌜ n > 0 ⌝ ∗ ⌜ both_threads_added n s1 s2 ⌝))).
@@ -342,7 +342,7 @@ Section complex'.
      (↯(1) ∗ gs γ1 γ2 (λ _ _, True : Prop)) ∨
      (↯(0) ∗ gs γ1 γ2 at_least_one_thread_sampled_non_zero))
    -∗
-    ∃ (s1 s2 : T), ghost_var γ1 (1/2/2) s1 ∗ ghost_var γ2 (1/2/2) s2 ∗
+    ∃ (s1 s2 : T), ghost_var γ1 (DfracOwn (1/2/2)) s1 ∗ ghost_var γ2 (DfracOwn (1/2/2)) s2 ∗
        ((↯(1/16) ∗ ⌜ no_thread_sampled s1 s2 ⌝) ∨
          (↯(1/4) ∗ ⌜ one_thread_sampled_zero s1 s2 ⌝) ∨
          (↯(1) (* both_thread_sampled_zero *)) ∨

theories/coneris/examples/hash/con_hash_impl1.v

@@ -24,7 +24,7 @@ Section con_hash_impl1.
 
 
   Definition hash_set_frag v (γ:gname) :=(v ↪[γ]□ ())%I.
-  Definition hash_set s γ:=(ghost_map_auth γ 1 (gset_to_gmap () s) ∗
+  Definition hash_set s γ:=(ghost_map_auth γ (DfracOwn 1) (gset_to_gmap () s) ∗
                               ⌜ ∀ x, x∈s-> (x < S val_size)%nat⌝ ∗
                                      [∗ set] x∈s, hash_set_frag x γ
                              )%I.

theories/coneris/examples/hash/con_hash_impl2.v

@@ -24,7 +24,7 @@ Section con_hash_impl2.
 
   Definition hash_set_frag v γ_set γ_set' := (hash_set_frag1 v γ_set∗ (v ↪[γ_set'] ()))%I.
   Definition hash_set n γ γ':=
-    (∃ s, ⌜size s = n⌝ ∗ hash_set1 s γ ∗ ghost_map_auth γ' 1 (gset_to_gmap () s))%I.
+    (∃ s, ⌜size s = n⌝ ∗ hash_set1 s γ ∗ ghost_map_auth γ' (DfracOwn 1) (gset_to_gmap () s))%I.
 
   Definition hash_auth m γ1 γ2 γ4 γ5:=
     (hv_auth (L:=Hhv) m γ4 ∗

theories/coneris/examples/hash/con_hash_impl4.v

@@ -124,7 +124,7 @@ Section con_hash_impl.
 
   Definition hashfunI (γs : gname * gname * gname) (val_size : nat) : iProp Σ :=
     ∃ (m : gmap nat (option nat)),
-      ghost_map_auth γs.1.1 1 m ∗
+      ghost_map_auth γs.1.1 (DfracOwn 1) m ∗
       [∗ map] k ↦ o ∈ m,
         ∃ α : loc, k ↪[γs.1.2]□ α ∗
            if o is Some n then α ↪N (val_size; [n]) ∨ k ↪[γs.2]□ n
@@ -140,8 +140,8 @@ Section con_hash_impl.
        ⌜f = compute_hash_specialized #val_size #lvm #ltm ⌝ ∗
        map_list lvm ((λ (n : nat), LitV (LitInt n)) <$> vm) ∗
        map_list ltm ((λ (α : loc), LitV (LitLbl α)) <$> tm) ∗
-       ghost_map_auth γs.1.2 1 tm ∗
-       ghost_map_auth γs.2   1 vm ∗
+       ghost_map_auth γs.1.2 (DfracOwn 1) tm ∗
+       ghost_map_auth γs.2   (DfracOwn 1) vm ∗
        ([∗ map] k ↦ n ∈ vm, k ↪[γs.1.1]□ (Some n)).
 
   Lemma wp_init_hash_state N val_size max :

theories/coneris/examples/hash/hash_view_impl.v

@@ -9,7 +9,7 @@ Section hash_view_impl.
   Context `{Hcon:conerisGS Σ,
               HinG: ghost_mapG Σ nat nat}.
 
-  Definition hash_view_auth m γ := (ghost_map_auth γ 1 m ∗
+  Definition hash_view_auth m γ := (ghost_map_auth γ (DfracOwn 1) m ∗
                                    [∗ map] k↦v ∈m, (k ↪[γ]□ v))%I
   .
   Definition hash_view_frag k v γ := (k ↪[γ]□ v)%I.

theories/coneris/examples/lazy_rand/lazy_rand_impl.v

@@ -69,7 +69,7 @@ Section impl.
     end.
 
   Definition rand_auth (n:option (nat*nat)) γ :=
-    (ghost_map_auth γ 1 (option_to_gmap n) ∗
+    (ghost_map_auth γ (DfracOwn 1) (option_to_gmap n) ∗
      option_duplicate n γ ∗
      ⌜option_valid n⌝)%I.
 

theories/coneris/lib/abstract_tape.v

@@ -15,7 +15,7 @@ Notation "α ◯↪N ( M ; ns ) @ γ":= (α ↪[ γ ] (M,ns))%I
                                     (at level 20, format "α ◯↪N ( M ; ns ) @ γ") : bi_scope.
 
 #[warning="-notation-incompatible-prefix"]
-Notation "● m @ γ" := (ghost_map_auth γ 1 m) (at level 20) : bi_scope.
+Notation "● m @ γ" := (ghost_map_auth γ (DfracOwn 1) m) (at level 20) : bi_scope.
 
 Section tapes_lemmas.
   Context `{!conerisGS Σ, !abstract_tapesGS Σ}.

theories/coneris/lib/hocap_rand_alt.v

@@ -117,7 +117,7 @@ Section impl1.
   (* (** Instantiate rand *) *)
   Local Definition rand_inv_pred1  (γ:gname*gname) : iProp Σ:=
     (∃ (m:gmap val (list nat)),
-        (ghost_map_auth γ.1 1 ((λ _, ())<$>m)) ∗
+        (ghost_map_auth γ.1 (DfracOwn 1) ((λ _, ())<$>m)) ∗
         ● ((λ x, (tb, x))<$>m)@ γ.2 ∗
         [∗ map] α ↦ns∈m, (∃ α', ⌜α = #lbl:α'⌝ ∗ (α' ↪N (tb; ns) ))
     )%I.
@@ -241,7 +241,7 @@ Section impl2.
   (** simulating a rand 3 with two flips *)
   Local Definition rand_inv_pred2  (γ:gname*gname) : iProp Σ:=
     (∃ (m:gmap val (list nat)),
-        (ghost_map_auth γ.1 1 ((λ _, ())<$>m)) ∗
+        (ghost_map_auth γ.1 (DfracOwn 1) ((λ _, ())<$>m)) ∗
         ● ((λ x, (1, x))<$>m)@ γ.2 ∗
         [∗ map] α ↦ns∈m, (∃ α', ⌜α = #lbl:α'⌝ ∗ (α' ↪N (1; ns) ))
     )%I.
@@ -442,7 +442,7 @@ Section impl3.
   (* (** Instantiate rand *) *)
   Local Definition rand_inv_pred3  (γ:gname*gname) : iProp Σ:=
     (∃ (m:gmap val (list nat)),
-        (ghost_map_auth γ.1 1 ((λ _, ())<$>m)) ∗
+        (ghost_map_auth γ.1 (DfracOwn 1) ((λ _, ())<$>m)) ∗
         ● ((λ x, (S tb, x))<$>m)@ γ.2 ∗
         [∗ map] α ↦ns∈m, (∃ α', ⌜α = #lbl:α'⌝ ∗ (α' ↪N (S tb; ns) ))
     )%I.

theories/coneris/primitive_laws.v

@@ -34,7 +34,7 @@ Definition tapes_auth `{conerisGS Σ} :=
 
 Global Instance conerisGS_conerisWpGS `{!conerisGS Σ} : conerisWpGS con_prob_lang Σ := {
   conerisWpGS_invGS := conerisGS_invG;
-    state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes))%I;
+    state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes))%I;
     fork_post := (λ _, True%I);
     err_interp ε := (ec_supply ε);
 
@@ -112,15 +112,15 @@ Section tape_interface.
   Qed.
 
   Lemma tapeN_lookup α N ns m: 
-    tapes_auth 1 m -∗ α ↪N (N; ns) -∗ ⌜∃ ns', m!!α = Some (N; ns') /\ fin_to_nat <$> ns' = ns⌝.
+    tapes_auth (DfracOwn 1) m -∗ α ↪N (N; ns) -∗ ⌜∃ ns', m!!α = Some (N; ns') /\ fin_to_nat <$> ns' = ns⌝.
   Proof.
     iIntros "? (%&%&?)".
     iDestruct (ghost_map_lookup with "[$][$]") as "%".
     iPureIntro. naive_solver.
   Qed.
 
   Lemma tapeN_update_append α N ns m (x : fin (S N)):
-    tapes_auth 1 m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth 1 (<[α:=(N; ns ++ [x])]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ [fin_to_nat x]).
+    tapes_auth (DfracOwn 1) m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth (DfracOwn 1) (<[α:=(N; ns ++ [x])]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ [fin_to_nat x]).
   Proof.
     iIntros "? (%&%&?)".
     iMod (ghost_map_update with "[$][$]") as "[??]".
@@ -129,7 +129,7 @@ Section tape_interface.
   Qed. 
 
   Lemma tapeN_update_append' α N m (ns ns':list (fin (S N))):
-    tapes_auth 1 m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth 1 (<[α:=(N; ns ++ ns')]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ (fin_to_nat <$> ns')).
+    tapes_auth (DfracOwn 1) m -∗ α ↪N (N; fin_to_nat <$> ns) ==∗ tapes_auth (DfracOwn 1) (<[α:=(N; ns ++ ns')]> m) ∗ α ↪N (N; (fin_to_nat <$> ns) ++ (fin_to_nat <$> ns')).
   Proof.
     iIntros "? (%&%&?)".
     iMod (ghost_map_update with "[$][$]") as "[??]".

theories/diffpriv/examples/report_noisy_max_lemmas.v

@@ -791,12 +791,12 @@ Section coupling_rule.
     length zs' = length xιs ->
     ls = zip (zip xιs.*2 xιs.*1) (replicate (length xιs) []) ->
     ls' =zip (zip xιs'.*2 xιs'.*1) (replicate (length xιs) []) ->
-    tapes_laplace_auth 1 (tapes_laplace σ) -∗
+    tapes_laplace_auth (DfracOwn 1) (tapes_laplace σ) -∗
     spec_tapes_laplace_auth (tapes_laplace σ') -∗
     ([∗ list] '(x, ι);'(x', ι') ∈ xιs;xιs', ι ↪L (num,2 * den,x; []) ∗
             ι' ↪Lₛ (num,2 * den,x'; []) ∗ ⌜(Rabs (IZR (x - x')) <= 1)%R⌝)
     ==∗
-    (tapes_laplace_auth 1 (tapes_laplace (replace_laplace_tape num (2 * den) σ (zip ls zs)))) ∗
+    (tapes_laplace_auth (DfracOwn 1) (tapes_laplace (replace_laplace_tape num (2 * den) σ (zip ls zs)))) ∗
      spec_tapes_laplace_auth (tapes_laplace (replace_laplace_tape num (2 * den) σ' (zip ls' zs'))) ∗
     ([∗ list] k↦'(x, ι);'(x', ι') ∈ xιs;xιs', ι ↪L (num,2 * den,x; [
                                                     zs !!! k]) ∗ ι' ↪Lₛ (num,2 * den,x'; [zs' !!! k]) ∗ ⌜(Rabs (IZR (x - x')) <= 1)%R⌝).

theories/diffpriv/primitive_laws.v

@@ -60,7 +60,7 @@ Definition add_ec_supply `{diffprivGS Σ} :=
 
 Global Instance diffprivGS_irisGS `{!diffprivGS Σ} : diffprivWpGS prob_lang Σ := {
   diffprivWpGS_invGS := diffprivGS_invG;
-  state_interp σ := (heap_auth 1 σ.(heap) ∗ tapes_auth 1 σ.(tapes) ∗ tapes_laplace_auth 1 σ.(tapes_laplace))%I;
+  state_interp σ := (heap_auth (DfracOwn 1) σ.(heap) ∗ tapes_auth (DfracOwn 1) σ.(tapes) ∗ tapes_laplace_auth (DfracOwn 1) σ.(tapes_laplace))%I;
   err_interp ε δ := ((mult_ec_supply ε) ∗ (add_ec_supply δ))%I;
 }.
 

theories/elton/examples/generic_group.v

@@ -574,7 +574,7 @@ Section prog.
           ⌜dom m = set_seq 0 k⌝ ∗
           ⌜map_Forall (λ _ x, base_lit_type_check x = Some BLTInt) m⌝ ∗
           ⌜is_valid_urn (urn_unif s)⌝ ∗
-          mono_nat_auth_own γ2 1 (k-1) ∗
+          mono_nat_auth_own γ2 (DfracOwn 1) (k-1) ∗
           ⌜dom m = dom m'⌝ ∗ 
           ⌜map_Forall (λ _ x, 0<=x.1<p/\0<=x.2<p) m'⌝ ∗
           ⌜map_match m m' l⌝  ∗
@@ -634,8 +634,8 @@ Section prog.
         wp_pures.
 
 
-        iDestruct (mono_nat_lb_own_valid with "[$][$Hfrag1]") as "%".
-        iDestruct (mono_nat_lb_own_valid with "[$][$Hfrag2]") as "%".
+        iDestruct (mono_nat_auth_lb_own_valid with "[$][$Hfrag1]") as "%".
+        iDestruct (mono_nat_auth_lb_own_valid with "[$][$Hfrag2]") as "%".
         assert (n1 ∈ dom m) as Hlookup1.
         { rewrite Hdom. rewrite elem_of_set_seq. destruct!/=; simpl in *.
           lia. }
@@ -921,7 +921,7 @@ Section prog.
         wp_pures.
 
 
-        iDestruct (mono_nat_lb_own_valid with "[$][$Hfrag']") as "%".
+        iDestruct (mono_nat_auth_lb_own_valid with "[$][$Hfrag']") as "%".
         assert (n ∈ dom m) as Hlookup.
         { rewrite Hdom. rewrite elem_of_set_seq. destruct!/=; simpl in *.
           lia. }
@@ -1181,8 +1181,8 @@ Section prog.
         iInv "Hinv" as ">(%m&%k&%s'&%m'&Hurn&%Hs&Harr&%&Htries&Hm&%Hdom&%Hforall&%&Hauth&%Hdom'&%Hforall2&%Hmatch&Hor)" "Hclose".
 
 
-        iDestruct (mono_nat_lb_own_valid with "[$][$Hfrag1]") as "%".
-        iDestruct (mono_nat_lb_own_valid with "[$][$Hfrag2]") as "%".
+        iDestruct (mono_nat_auth_lb_own_valid with "[$][$Hfrag1]") as "%".
+        iDestruct (mono_nat_auth_lb_own_valid with "[$][$Hfrag2]") as "%".
         assert (n1 ∈ dom m) as Hlookup1.
         { rewrite Hdom. rewrite elem_of_set_seq. destruct!/=; simpl in *.
           lia. }