first attempt with hocap rand

theories/coneris/lib/hocap.v

@@ -1,7 +1,7 @@
 (** * Hocap specs *)
 From stdpp Require Import namespaces.
 From iris Require Import excl_auth invariants list.
-From clutch.coneris Require Import coneris flip.
+From clutch.coneris Require Import coneris.
 
 Set Default Proof Using "Type*".
 
@@ -94,14 +94,16 @@ Section error_lemmas.
   Qed.
 
   Lemma hocap_error_decrease γ (b' b:nonnegreal) :
-     (●↯ (b+b') @ γ) -∗ (◯↯ b @ γ) ==∗ (●↯ b' @ γ).
+     (●↯ (b) @ γ) -∗ (◯↯ b' @ γ) ==∗ (●↯ (b-b') @ γ).
   Proof.
     iIntros "H1 H2".
     simpl.
+    iDestruct (hocap_error_ineq with "[$][$]") as "%".
     iDestruct "H1" as "[% [% H1]]".
     iDestruct "H2" as "[% [% H2]]".
     iMod (own_update_2 with "H1 H2") as "Hown".
-    { eapply (auth_update_dealloc _ _ b'), nonnegreal_local_update.
+    { unshelve eapply (auth_update_dealloc _ _ ((b-b') _)%NNR), nonnegreal_local_update.
+      - lra.
       - apply cond_nonneg.
       - apply nnreal_ext =>/=. lra. }
     iFrame. by iPureIntro.
@@ -123,11 +125,17 @@ Section error_lemmas.
     - done.
   Qed.
 
-  Lemma hocap_error_irrel γ (b c:R) :
+  Lemma hocap_error_auth_irrel γ (b c:R) :
     (b=c)%R -> (●↯ b @ γ) -∗ (●↯ c @ γ).
   Proof.
     iIntros (->) "$".
   Qed.
+
+  Lemma hocap_error_frag_irrel γ (b c:R) :
+    (b=c)%R -> (◯↯ b @ γ) -∗ (◯↯ c @ γ).
+  Proof.
+    iIntros (->) "$".
+  Qed.
 
 End error_lemmas.
 

theories/coneris/lib/hocap_rand.v

@@ -0,0 +1,107 @@
+(** * Hocap rand specs *)
+From clutch.coneris Require Import coneris hocap.
+
+Set Default Proof Using "Type*".
+
+
+Class rand_spec `{!conerisGS Σ} := RandSpec
+{
+  (** * Operations *)
+  rand_allocate_tape : val;
+  rand_tape : val;
+  (** * Ghost state *)
+  (** The assumptions about [Σ] *)
+  randG : gFunctors → Type;
+
+  rand_error_name : Type;
+  rand_tape_name: Type;
+  (** * Predicates *)
+  is_rand {L : randG Σ} (N:namespace)
+    (γ1: rand_error_name) (γ2: rand_tape_name): iProp Σ;
+  rand_error_auth {L : randG Σ} (γ: rand_error_name) (x:R): iProp Σ;
+  rand_error_frag {L : randG Σ} (γ: rand_error_name) (x:R): iProp Σ;
+  rand_tapes_auth {L : randG Σ} (γ: rand_tape_name) (m:gmap loc (nat * list nat)): iProp Σ;
+  rand_tapes_frag {L : randG Σ} (γ: rand_tape_name) (α:loc) (ns: (nat * list nat)): iProp Σ;
+  (** * General properties of the predicates *)
+  #[global] is_rand_persistent {L : randG Σ} N γ1 γ2 ::
+    Persistent (is_rand (L:=L) N γ1 γ2);
+  #[global] rand_error_auth_timeless {L : randG Σ} γ x ::
+    Timeless (rand_error_auth (L:=L) γ x);
+  #[global] rand_error_frag_timeless {L : randG Σ} γ x ::
+    Timeless (rand_error_frag (L:=L) γ x);
+  #[global] rand_tapes_auth_timeless {L : randG Σ} γ m ::
+    Timeless (rand_tapes_auth (L:=L) γ m);
+  #[global] rand_tapes_frag_timeless {L : randG Σ} γ α ns ::
+    Timeless (rand_tapes_frag (L:=L) γ α ns);
+  #[global] rand_error_name_inhabited::
+    Inhabited rand_error_name;
+  #[global] rand_tape_name_inhabited::
+    Inhabited rand_tape_name;
+
+  rand_error_auth_exclusive {L : randG Σ} γ x1 x2:
+    rand_error_auth (L:=L) γ x1 -∗ rand_error_auth (L:=L) γ x2 -∗ False;
+  rand_error_frag_split {L : randG Σ} γ (x1 x2:nonnegreal):
+  rand_error_frag (L:=L) γ x1 ∗ rand_error_frag (L:=L) γ x2 ⊣⊢
+  rand_error_frag (L:=L) γ (x1+x2)%R ;
+  rand_error_auth_valid {L : randG Σ} γ x:
+    rand_error_auth (L:=L) γ x -∗ ⌜(0<=x<1)%R⌝;
+  rand_error_frag_valid {L : randG Σ} γ x:
+    rand_error_frag (L:=L) γ x -∗ ⌜(0<=x<1)%R⌝;
+  rand_error_ineq {L : randG Σ} γ x1 x2:
+    rand_error_auth (L:=L) γ x1 -∗ rand_error_frag (L:=L) γ x2 -∗ ⌜(x2 <= x1)%R ⌝;
+  rand_error_decrease {L : randG Σ} γ (x1 x2:nonnegreal):
+     rand_error_auth (L:=L) γ x1 -∗ rand_error_frag (L:=L) γ x2 ==∗ rand_error_auth (L:=L) γ (x2-x1)%R;
+  rand_error_increase {L : randG Σ} γ (x1 x2:nonnegreal):
+    (x1+x2<1)%R -> ⊢ rand_error_auth (L:=L) γ x1 ==∗
+    rand_error_auth (L:=L) γ (x1+x2) ∗ rand_error_frag (L:=L) γ x2;
+
+  rand_tapes_auth_exclusive {L : randG Σ} γ m m':
+  rand_tapes_auth (L:=L) γ m -∗ rand_tapes_auth (L:=L) γ m' -∗ False;
+  rand_tapes_frag_exclusive {L : randG Σ} γ α ns ns':
+  rand_tapes_frag (L:=L) γ α ns -∗ rand_tapes_frag (L:=L) γ α ns' -∗ False;
+  rand_tapes_agree {L : randG Σ} γ α m ns:
+  rand_tapes_auth (L:=L) γ m -∗ rand_tapes_frag (L:=L) γ α ns -∗ ⌜ m!! α = Some (ns) ⌝;
+  rand_tapes_valid {L : randG Σ} γ1 γ2 α N E tb ns:
+    ⌜↑N⊆E⌝ ∗ is_rand (L:=L) N γ1 γ2 ∗ rand_tapes_frag (L:=L) γ2 α (tb, ns) ={E}=∗
+    ⌜Forall (λ n, n<=tb)%nat ns⌝;
+  rand_tapes_update {L : randG Σ} γ α m ns ns':
+    rand_tapes_auth (L:=L) γ m -∗ rand_tapes_frag (L:=L) γ α ns ==∗
+    rand_tapes_auth (L:=L) γ (<[α := ns']> m) ∗ rand_tapes_frag (L:=L) γ α ns';
+
+  (** * Program specs *)
+  rand_inv_create_spec {L : randG Σ} N E ε:
+  ↯ ε -∗
+  wp_update E (∃ γ1 γ2, is_rand (L:=L) N γ1 γ2 ∗
+                        rand_error_frag (L:=L) γ1 ε);
+
+  rand_allocate_tape_spec {L: randG Σ} N E (tb:nat) γ1 γ2:
+    ↑N ⊆ E->
+    {{{ is_rand (L:=L) N γ1 γ2 }}}
+      rand_allocate_tape #tb @ E
+      {{{ (v:val), RET v;
+          ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ rand_tapes_frag (L:=L) γ2 α (tb, [])
+      }}};
+  rand_tape_spec_some {L: randG Σ} N E γ1 γ2 (P: iProp Σ) (Q:iProp Σ) (α:loc) (n:nat) (tb:nat) ns:
+    ↑N⊆E ->
+    {{{ is_rand (L:=L) N γ1 γ2 ∗
+        □ (∀ (m:gmap loc (nat * list nat)), P ∗
+           rand_tapes_auth (L:=L) γ2 m
+            ={E∖↑N}=∗ ⌜m!!α=Some (tb, n::ns)⌝ ∗ Q ∗ rand_tapes_auth (L:=L) γ2 (<[α:=(tb, ns)]> m)) ∗
+        P
+    }}}
+      rand_tape #lbl:α #tb @ E
+                       {{{ RET #n; Q }}}; 
+  rand_presample_spec {L: randG Σ} N E ns α (tb:nat)
+     (ε2 : list (fin (S tb)) -> R)
+    (P : iProp Σ) num T γ1 γ2 ε :
+    ↑N ⊆ E ->
+    (∀ l, length l = num ->  0<= ε2 l)%R ->
+    (SeriesC (λ l, if bool_decide (l ∈ enum_uniform_fin_list tb num) then ε2 l else 0) /((S tb)^num) <= ε)%R->
+    is_rand (L:=L) N γ1 γ2 -∗
+    (□∀ (ε':R) ns', (P ∗ rand_error_auth (L:=L) γ1 (ε')%R ∗ ⌜length ns' = num⌝) ={E∖↑N}=∗
+                  ∃ diff: R, ⌜(0<=diff)%R⌝ ∗ ⌜(ε' = ε+diff)%R⌝ ∗  
+        (⌜(1<=ε2 ns' + diff)%R⌝ ∨ (rand_error_auth (L:=L) γ1 (ε2 ns' + diff)%R ∗ T ns')))
+        -∗
+    P -∗ rand_tapes_frag (L:=L) γ2 α (tb, ns)-∗
+        wp_update E (∃ n, T n ∗ rand_tapes_frag (L:=L) γ2 α (tb, ns++(fin_to_nat <$> n)))
+}.

theories/coneris/primitive_laws.v

@@ -137,6 +137,17 @@ Section tape_interface.
     by rewrite fmap_app.
   Qed. 
 
+  Lemma tapeN_ineq α N ns:
+    α↪N (N; ns) -∗ ⌜Forall (λ n, n<=N)%nat ns⌝.
+  Proof.
+    iIntros "(% & <- & H)".
+    iPureIntro.
+    eapply Forall_impl.
+    - apply fin.fin_forall_leq.
+    - simpl. intros.
+      lia.
+  Qed.
+
   (*
   Lemma spec_tapeN_to_empty l M :
     (l ↪ₛN ( M ; [] ) -∗ l ↪ₛ ( M ; [] )).

theories/prob/countable_sum.v

@@ -2,7 +2,7 @@ From Coq Require Import Reals Psatz.
 From Coquelicot Require Import Series Hierarchy Lim_seq Rbar Lub.
 From stdpp Require Import option.
 From stdpp Require Export countable finite gmap.
-From clutch.prelude Require Import base Reals_ext Coquelicot_ext Series_ext stdpp_ext classical fin.
+From clutch.prelude Require Import base Reals_ext Coquelicot_ext Series_ext stdpp_ext classical fin uniform_list.
 Set Default Proof Using "Type*".
 Import Hierarchy.
 
@@ -710,12 +710,20 @@ Section filter.
 
 End filter.
 
-Lemma ex_seriesC_list_length `{Countable A} (f:list A -> R) num:
-  (forall x, (0<f x)%R -> length x = num) ->
+Lemma ex_seriesC_list_length `{Finite A} (f:list A -> R) num:
+  (forall x, (0≠f x)%R -> length x = num) ->
   ex_seriesC f.
 Proof.
   intros.
-Admitted.
+  eapply (ex_seriesC_ext (λ x, if bool_decide(x∈enum_uniform_list num) then f x else 0))%R.
+  - intros n.
+    case_bool_decide as K; first done.
+    destruct (Req_dec (f n) 0); first done.
+    exfalso.
+    apply K. apply elem_of_enum_uniform_list.
+    naive_solver.
+  - apply ex_seriesC_list.
+Qed.
 
 Lemma SeriesC_Series_nat (f : nat → R)  :
   SeriesC f = Series f.