interface spec of random counter

logsem · Sep 26, 2024 · 4dbc843 · 4dbc843
1 parent ef8d71f
commit 4dbc843
Show file tree

Hide file tree

Showing 2 changed files with 109 additions and 129 deletions.
diff --git a/theories/coneris/examples/random_counter/random_counter.v b/theories/coneris/examples/random_counter/random_counter.v
@@ -1,133 +1,114 @@
-(* From clutch.coneris Require Import coneris. *)
+From clutch.coneris Require Import coneris.
 
-(* Set Default Proof Using "Type*". *)
+Set Default Proof Using "Type*".
 
-(* Class random_counter `{!conerisGS Σ} := RandCounter *)
-(* { *)
-(*   (** * Operations *) *)
-(*   new_counter : val; *)
-(*   (* incr_counter : val; *) *)
-(*   allocate_tape : val; *)
-(*   incr_counter_tape : val; *)
-(*   read_counter : val; *)
-(*   (** * Ghost state *) *)
-(*   (** The assumptions about [Σ] *) *)
-(*   counterG : gFunctors → Type; *)
-(*   (** [name] is used to associate [locked] with [is_lock] *) *)
-(*   error_name : Type; *)
-(*   tape_name: Type; *)
-(*   counter_name: Type; *)
-(*   (** * Predicates *) *)
-(*   is_counter {L : counterG Σ} (N:namespace) (counter: val) *)
-(*     (γ1: error_name) (γ2: tape_name) (γ3: counter_name): iProp Σ; *)
-(*   counter_error_auth {L : counterG Σ} (γ: error_name) (x:R): iProp Σ; *)
-(*   counter_error_frag {L : counterG Σ} (γ: error_name) (x:R): iProp Σ; *)
-(*   counter_tapes_auth {L : counterG Σ} (γ: tape_name) (m:gmap loc (list nat)): iProp Σ; *)
-(*   counter_tapes_frag {L : counterG Σ} (γ: tape_name) (α:loc) (ns:list nat): iProp Σ; *)
-(*   counter_content_auth {L : counterG Σ} (γ: counter_name) (z:nat): iProp Σ; *)
-(*   counter_content_frag {L : counterG Σ} (γ: counter_name) (f:frac) (z:nat): iProp Σ; *)
-(*   (** * General properties of the predicates *) *)
-(*   #[global] is_counter_persistent {L : counterG Σ} N c γ1 γ2 γ3 :: *)
-(*     Persistent (is_counter (L:=L) N c γ1 γ2 γ3); *)
-(*   #[global] counter_error_auth_timeless {L : counterG Σ} γ x :: *)
-(*     Timeless (counter_error_auth (L:=L) γ x); *)
-(*   #[global] counter_error_frag_timeless {L : counterG Σ} γ x :: *)
-(*     Timeless (counter_error_frag (L:=L) γ x); *)
-(*   #[global] counter_tapes_auth_timeless {L : counterG Σ} γ m :: *)
-(*     Timeless (counter_tapes_auth (L:=L) γ m); *)
-(*   #[global] counter_tapes_frag_timeless {L : counterG Σ} γ α ns :: *)
-(*     Timeless (counter_tapes_frag (L:=L) γ α ns); *)
-(*   #[global] counter_content_auth_timeless {L : counterG Σ} γ z :: *)
-(*     Timeless (counter_content_auth (L:=L) γ z); *)
-(*   #[global] counter_content_frag_timeless {L : counterG Σ} γ f z :: *)
-(*     Timeless (counter_content_frag (L:=L) γ f z); *)
-
-(*   counter_error_auth_exclusive {L : counterG Σ} γ x1 x2: *)
-(*     counter_error_auth (L:=L) γ x1 -∗ counter_error_auth (L:=L) γ x2 -∗ False; *)
-(*   counter_error_frag_split {L : counterG Σ} γ (x1 x2:nonnegreal): *)
-(*   counter_error_frag (L:=L) γ x1 ∗ counter_error_frag (L:=L) γ x2 ⊣⊢ *)
-(*   counter_error_frag (L:=L) γ (x1+x2)%R ; *)
-(*   counter_error_auth_valid {L : counterG Σ} γ x: *)
-(*     counter_error_auth (L:=L) γ x -∗ ⌜(0<=x<1)%R⌝; *)
-(*   counter_error_frag_valid {L : counterG Σ} γ x: *)
-(*     counter_error_frag (L:=L) γ x -∗ ⌜(0<=x<1)%R⌝; *)
-(*   counter_error_ineq {L : counterG Σ} γ x1 x2: *)
-(*     counter_error_auth (L:=L) γ x1 -∗ counter_error_frag (L:=L) γ x2 -∗ ⌜(x2<=x1)%R ⌝; *)
-(*   counter_error_decrease {L : counterG Σ} γ (x1 x2:nonnegreal): *)
-(*      counter_error_auth (L:=L) γ (x1 + x2)%NNR -∗ counter_error_frag (L:=L) γ x1 ==∗ counter_error_auth (L:=L) γ x2; *)
-(*   counter_error_increase {L : counterG Σ} γ (x1 x2:nonnegreal): *)
-(*     (x1+x2<1)%R -> ⊢ counter_error_auth (L:=L) γ x1 ==∗ *)
-(*     counter_error_auth (L:=L) γ (x1+x2) ∗ counter_error_frag (L:=L) γ x2; *)
+Class random_counter `{!conerisGS Σ} := RandCounter
+{
+  (** * Operations *)
+  new_counter : val;
+  (* incr_counter : val; *)
+  allocate_tape : val;
+  incr_counter_tape : val;
+  read_counter : val;
+  (** * Ghost state *)
+  (** The assumptions about [Σ] *)
+  counterG : gFunctors → Type;
+  (** [name] is used to associate [locked] with [is_lock] *)
+  tape_name: Type;
+  counter_name: Type;
+  (** * Predicates *)
+  is_counter {L : counterG Σ} (N:namespace) (counter: val)
+    (γ1: tape_name) (γ2: counter_name): iProp Σ;
+  counter_tapes_auth {L : counterG Σ} (γ: tape_name) (m:gmap loc (list nat)): iProp Σ;
+  counter_tapes_frag {L : counterG Σ} (γ: tape_name) (α:loc) (ns:list nat): iProp Σ;
+  counter_content_auth {L : counterG Σ} (γ: counter_name) (z:nat): iProp Σ;
+  counter_content_frag {L : counterG Σ} (γ: counter_name) (f:frac) (z:nat): iProp Σ;
+  (** * General properties of the predicates *)
+  #[global] is_counter_persistent {L : counterG Σ} N c γ1 γ2 ::
+    Persistent (is_counter (L:=L) N c γ1 γ2);
+  #[global] counter_tapes_auth_timeless {L : counterG Σ} γ m ::
+    Timeless (counter_tapes_auth (L:=L) γ m);
+  #[global] counter_tapes_frag_timeless {L : counterG Σ} γ α ns ::
+    Timeless (counter_tapes_frag (L:=L) γ α ns);
+  #[global] counter_content_auth_timeless {L : counterG Σ} γ z ::
+    Timeless (counter_content_auth (L:=L) γ z);
+  #[global] counter_content_frag_timeless {L : counterG Σ} γ f z ::
+    Timeless (counter_content_frag (L:=L) γ f z);
 
-(*   counter_tapes_auth_exclusive {L : counterG Σ} γ m m': *)
-(*   counter_tapes_auth (L:=L) γ m -∗ counter_tapes_auth (L:=L) γ m' -∗ False; *)
-(*   counter_tapes_frag_exclusive {L : counterG Σ} γ α ns ns': *)
-(*   counter_tapes_frag (L:=L) γ α ns -∗ counter_tapes_frag (L:=L) γ α ns' -∗ False; *)
-(*   counter_tapes_agree {L : counterG Σ} γ α m ns: *)
-(*     counter_tapes_auth (L:=L) γ m -∗ counter_tapes_frag (L:=L) γ α ns -∗ ⌜ m!! α = Some (ns) ⌝; *)
-(*   counter_tapes_update {L : counterG Σ} γ α m ns n: *)
-(*     counter_tapes_auth (L:=L) γ m -∗ counter_tapes_frag (L:=L) γ α ns ==∗ *)
-(*     counter_tapes_auth (L:=L) γ (<[α := (ns ++[n])]> m) ∗ counter_tapes_frag (L:=L) γ α (ns ++ [n]); *)
+  counter_tapes_auth_exclusive {L : counterG Σ} γ m m':
+  counter_tapes_auth (L:=L) γ m -∗ counter_tapes_auth (L:=L) γ m' -∗ False;
+  counter_tapes_frag_exclusive {L : counterG Σ} γ α ns ns':
+  counter_tapes_frag (L:=L) γ α ns -∗ counter_tapes_frag (L:=L) γ α ns' -∗ False;
+  counter_tapes_agree {L : counterG Σ} γ α m ns:
+  counter_tapes_auth (L:=L) γ m -∗ counter_tapes_frag (L:=L) γ α ns -∗ ⌜ m!! α = Some (ns) ⌝;
+  counter_tapes_valid {L : counterG Σ} γ α ns:
+    counter_tapes_frag (L:=L) γ α ns -∗ ⌜Forall (λ n, n<=3)%nat ns⌝;
+  counter_tapes_update {L : counterG Σ} γ α m ns ns':
+    Forall (λ x, x<=3%nat) ns'->
+    counter_tapes_auth (L:=L) γ m -∗ counter_tapes_frag (L:=L) γ α ns ==∗
+    counter_tapes_auth (L:=L) γ (<[α := ns']> m) ∗ counter_tapes_frag (L:=L) γ α (ns');
 
-(*   counter_content_auth_exclusive {L : counterG Σ} γ z1 z2: *)
-(*     counter_content_auth (L:=L) γ z1 -∗ counter_content_auth (L:=L) γ z2 -∗ False; *)
-(*   counter_content_less_than {L : counterG Σ} γ z z' f: *)
-(*   counter_content_auth (L:=L) γ z -∗ counter_content_frag (L:=L) γ f z' -∗ ⌜(z'<=z)%nat ⌝; *)
-(*   counter_content_frag_combine {L:counterG Σ} γ f f' z z': *)
-(*     (counter_content_frag (L:=L) γ f z ∗ counter_content_frag (L:=L) γ f' z')%I ≡ *)
-(*     counter_content_frag (L:=L) γ (f+f')%Qp (z+z')%nat; *)
-(*   counter_content_agree {L : counterG Σ} γ z z': *)
-(*     counter_content_auth (L:=L) γ z -∗ counter_content_frag (L:=L) γ 1%Qp z' -∗ ⌜(z'=z)%nat ⌝; *)
-(*   counter_content_update {L : counterG Σ} γ f z1 z2 z3: *)
-(*     counter_content_auth (L:=L) γ z1 -∗ counter_content_frag (L:=L) γ f z2 ==∗ *)
-(*     counter_content_auth (L:=L) γ (z1+z3)%nat ∗ counter_content_frag (L:=L) γ f (z2+z3)%nat; *)
+  counter_content_auth_exclusive {L : counterG Σ} γ z1 z2:
+    counter_content_auth (L:=L) γ z1 -∗ counter_content_auth (L:=L) γ z2 -∗ False;
+  counter_content_less_than {L : counterG Σ} γ z z' f:
+  counter_content_auth (L:=L) γ z -∗ counter_content_frag (L:=L) γ f z' -∗ ⌜(z'<=z)%nat ⌝;
+  counter_content_frag_combine {L:counterG Σ} γ f f' z z':
+    (counter_content_frag (L:=L) γ f z ∗ counter_content_frag (L:=L) γ f' z')%I ≡
+    counter_content_frag (L:=L) γ (f+f')%Qp (z+z')%nat;
+  counter_content_agree {L : counterG Σ} γ z z':
+    counter_content_auth (L:=L) γ z -∗ counter_content_frag (L:=L) γ 1%Qp z' -∗ ⌜(z'=z)%nat ⌝;
+  counter_content_update {L : counterG Σ} γ f z1 z2 z3:
+    counter_content_auth (L:=L) γ z1 -∗ counter_content_frag (L:=L) γ f z2 ==∗
+    counter_content_auth (L:=L) γ (z1+z3)%nat ∗ counter_content_frag (L:=L) γ f (z2+z3)%nat;
 
-(*   (** * Program specs *) *)
-(*   new_counter_spec {L : counterG Σ} E ε N: *)
-(*   {{{ ↯ ε }}} new_counter #() @E *)
-(*     {{{ c, RET c; ∃ γ1 γ2 γ3, is_counter (L:=L) N c γ1 γ2 γ3 ∗ *)
-(*                               counter_error_frag (L:=L) γ1 ε ∗ *)
-(*                               counter_content_frag (L:=L) γ3 1%Qp 0%nat *)
-(*     }}}; *)
-(*   allocate_tape_spec {L: counterG Σ} N E c γ1 γ2 γ3: *)
-(*     ↑N ⊆ E-> *)
-(*     {{{ is_counter (L:=L) N c γ1 γ2 γ3 }}} *)
-(*       allocate_tape #() @ E *)
-(*       {{{ (v:val), RET v; *)
-(*           ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ counter_tapes_frag (L:=L) γ2 α [] *)
-(*       }}}; *)
-(*   incr_counter_tape_spec_some {L: counterG Σ} N E c γ1 γ2 γ3 (P: iProp Σ) (Q:nat->iProp Σ) (α:loc) (n:nat) ns: *)
-(*     ↑N⊆E ->  *)
-(*     {{{ is_counter (L:=L) N c γ1 γ2 γ3 ∗ *)
-(*         □ (∀ (z:nat), P ∗ counter_content_auth (L:=L) γ3 z ={E∖↑N}=∗ *)
-(*                           counter_content_auth (L:=L) γ3 (z+n)%nat ∗ Q z) ∗ *)
-(*         P ∗ counter_tapes_frag (L:=L) γ2 α (n::ns) *)
-(*     }}} *)
-(*       incr_counter_tape c #lbl:α @ E *)
-(*                                  {{{ (z:nat), RET (#z, #n); Q z ∗ counter_tapes_frag (L:=L) γ2 α ns}}}; *)
-(*   counter_presample_spec {L: counterG Σ} NS E ns α *)
-(*      (ε2 : R -> nat -> R) *)
-(*     (P : iProp Σ) T γ1 γ2 γ3 c: *)
-(*     ↑NS ⊆ E -> *)
-(*     (∀ ε n, 0<= ε -> 0<=ε2 ε n)%R -> *)
-(*     (∀ (ε:R), 0<= ε ->SeriesC (λ n, if (bool_decide (n≤3%nat)) then 1 / (S 3%nat) * ε2 ε n else 0%R)%R <= ε)%R-> *)
-(*     is_counter (L:=L) NS c γ1 γ2 γ3 -∗ *)
-(*     (□∀ (ε ε':nonnegreal) n, (P ∗ counter_error_auth (L:=L) γ1 (ε')%R) ={E∖↑NS}=∗ *)
-(*         (⌜(1<=ε2 ε n)%R⌝ ∨ (counter_error_auth (L:=L) γ1 (ε' + )%R  ∗ T (n))))  *)
-(*         -∗ *)
-(*     P -∗ counter_tapes_frag (L:=L) γ2 α ns-∗ *)
-(*         wp_update E (∃ n, T (n) ∗ counter_tapes_frag (L:=L) γ2 α (ns++[n])); *)
-(*   read_counter_spec {L: counterG Σ} N E c γ1 γ2 γ3 P Q: *)
-(*     ↑N ⊆ E -> *)
-(*     {{{  is_counter (L:=L) N c γ1 γ2 γ3  ∗ *)
-(*         □ (∀ (z:nat), P ∗ counter_content_auth (L:=L) γ3 z ={E∖↑N}=∗ *)
-(*                     counter_content_auth (L:=L) γ3 z∗ Q z) *)
-(*          ∗ P *)
-(*     }}} *)
-(*       read_counter c @ E *)
-(*       {{{ (n':nat), RET #n'; Q n' *)
-(*       }}} *)
-(* }. *)
+  (** * Program specs *)
+  new_counter_spec {L : counterG Σ} E N:
+  {{{ True }}} new_counter #() @E
+    {{{ c, RET c; ∃ γ1 γ2, is_counter (L:=L) N c γ1 γ2 ∗
+                           counter_content_frag (L:=L) γ2 1%Qp 0%nat
+    }}};
+  allocate_tape_spec {L: counterG Σ} N E c γ1 γ2:
+    ↑N ⊆ E->
+    {{{ is_counter (L:=L) N c γ1 γ2 }}}
+      allocate_tape #() @ E
+      {{{ (v:val), RET v;
+          ∃ (α:loc), ⌜v=#lbl:α⌝ ∗ counter_tapes_frag (L:=L) γ1 α []
+      }}};
+  incr_counter_tape_spec_some {L: counterG Σ} N E c γ1 γ2 (P: iProp Σ) (Q:nat->iProp Σ) (α:loc) (n:nat) ns:
+    ↑N⊆E ->
+    {{{ is_counter (L:=L) N c γ1 γ2 ∗
+        □ (∀ (z:nat), counter_content_auth (L:=L) γ2 z ∗ P ={E∖ ↑N, ∅}=∗
+                    counter_tapes_frag (L:=L) γ1 α (n::ns) ∗
+                    (counter_tapes_frag (L:=L) γ1 α ns ={∅, E∖↑N}=∗
+                     counter_content_auth (L:=L) γ2 (z+n) ∗ Q z)
+          ) ∗ P
+    }}}
+      incr_counter_tape c #lbl:α @ E
+                                 {{{ (z:nat), RET (#z, #n); Q z}}}; 
+  counter_presample_spec {L: counterG Σ} NS E ns α
+     (ε2 : list nat -> R)
+    (P : iProp Σ) T γ1 γ2 c num ε:
+    ↑NS ⊆ E ->
+    (∀ n, 0<=ε2 n)%R ->
+    (SeriesC (λ l, if bool_decide (l∈fmap (λ x, fmap (FMap:=list_fmap) fin_to_nat x) (enum_uniform_fin_list 3%nat num)) then ε2 l else 0%R) / (4^num) <= ε)%R->
+    is_counter (L:=L) NS c γ1 γ2 -∗
+    □(P ={E∖↑NS,∅}=∗ ↯ ε ∗ counter_tapes_frag (L:=L) γ1 α ns ∗
+      (∀ ns', ⌜length ns' = num⌝ ∗ ↯ (ε2 ns') ∗ counter_tapes_frag (L:=L) γ1 α (ns++ns')={∅,E∖↑NS}=∗
+              T ns'
+      ))-∗
+    P -∗ 
+        wp_update E (∃ n, T n); 
+  read_counter_spec {L: counterG Σ} N E c γ1 γ2 P Q:
+    ↑N ⊆ E ->
+    {{{  is_counter (L:=L) N c γ1 γ2 ∗
+        □ (∀ (z:nat), P ∗ counter_content_auth (L:=L) γ2 z ={E∖↑N}=∗
+                    counter_content_auth (L:=L) γ2 z∗ Q z)
+         ∗ P
+    }}}
+      read_counter c @ E
+      {{{ (n':nat), RET #n'; Q n'
+      }}}
+}.
 
 
 (* Section lemmas. *)
@@ -165,7 +146,7 @@
 (*     {{{ is_counter (L:=L) N c γ1 γ2 γ3 ∗ *)
 (*         counter_error_frag (L:=L) γ1 ε ∗ *)
 (*         counter_tapes_frag (L:=L) γ2 α [] ∗ *)
-(*         counter_content_frag (L:=L) γ3 q z  *)
+(*         counter_content_frag (L:=L) γ3 q z *)
 (*     }}} *)
 (*       incr_counter_tape c #lbl:α @ E *)
 (*                                  {{{ (z':nat) (n:nat), *)
@@ -197,7 +178,7 @@
 (*         iDestruct (counter_error_auth_valid with "[$]") as "%". *)
 (*         iDestruct (counter_error_frag_valid with "[$]") as "%". *)
 (*         unshelve iMod (counter_error_update _ _ _ (mknonnegreal (ε2' ε n) _) with "[$][$]") as "[$$]". *)
-(*         { rewrite /ε2' H.  *)
+(*         { rewrite /ε2' H. *)
 (*           naive_solver. } *)
 (*         iPureIntro. split; first lia. *)
 (*         apply leb_complete in H. lia. *)

diff --git a/theories/coneris/lib/hocap_rand.v b/theories/coneris/lib/hocap_rand.v
@@ -35,8 +35,7 @@ Class rand_spec `{!conerisGS Σ} := RandSpec
   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 Σ} γ2 α tb ns:
-    rand_tapes_frag (L:=L) γ2 α (tb, ns) -∗
-    ⌜Forall (λ n, n<=tb)%nat ns⌝ ;
+    rand_tapes_frag (L:=L) γ2 α (tb, ns) -∗ ⌜Forall (λ n, n<=tb)%nat ns⌝ ;
   rand_tapes_update {L : randG Σ} γ α m ns ns':
   Forall (λ x, x<=ns'.1) ns'.2 ->
     rand_tapes_auth (L:=L) γ m -∗ rand_tapes_frag (L:=L) γ α ns ==∗