From 4dbc843d23c24d7f34c70acecc13cd63071888c6 Mon Sep 17 00:00:00 2001 From: Hei Li Date: Thu, 26 Sep 2024 10:21:02 +0200 Subject: [PATCH] interface spec of random counter --- .../examples/random_counter/random_counter.v | 235 ++++++++---------- theories/coneris/lib/hocap_rand.v | 3 +- 2 files changed, 109 insertions(+), 129 deletions(-) diff --git a/theories/coneris/examples/random_counter/random_counter.v b/theories/coneris/examples/random_counter/random_counter.v index 2491e18c..e4c28cbd 100644 --- 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 index 0fca693b..83211ce5 100644 --- 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 ==∗