NIT

logsem · Sep 26, 2024 · fb3f8f7 · fb3f8f7
1 parent 690707a
commit fb3f8f7
Showing 1 changed file with 12 additions and 11 deletions.
diff --git a/theories/coneris/examples/random_counter/random_counter.v b/theories/coneris/examples/random_counter/random_counter.v
@@ -74,28 +74,29 @@ Class random_counter `{!conerisGS Σ} := RandCounter
       {{{ (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 (Q:nat->iProp Σ) (α:loc) (n:nat) ns:
+  incr_counter_tape_spec_some {L: counterG Σ} N E c γ1 γ2 (Q:nat->nat->list nat->iProp Σ) (α:loc) :
     ↑N⊆E ->
     {{{ is_counter (L:=L) N c γ1 γ2 ∗
         (∀ (z:nat), counter_content_auth (L:=L) γ2 z ={E∖ ↑N, ∅}=∗
-                    counter_tapes_frag (L:=L) γ1 α (n::ns) ∗
+                   ∃ n ns, 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)
+                     counter_content_auth (L:=L) γ2 (z+n) ∗ Q z n ns)
           ) 
     }}}
       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) T γ1 γ2 c num ε:
+                                 {{{ (z n:nat), RET (#z, #n); ∃ ns, Q z n ns}}}; 
+  counter_presample_spec {L: counterG Σ} NS E T γ1 γ2 c:
     ↑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 -∗
-    ( |={E∖↑NS,∅}=> ↯ ε ∗ counter_tapes_frag (L:=L) γ1 α ns ∗
+    ( |={E∖↑NS,∅}=>
+        ∃ ε α ε2 num ns,
+        ↯ ε ∗ counter_tapes_frag (L:=L) γ1 α ns ∗
+        ⌜(∀ 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⌝ ∗
       (∀ ns', ⌜length ns' = num⌝ ∗ ↯ (ε2 ns') ∗ counter_tapes_frag (L:=L) γ1 α (ns++ns')={∅,E∖↑NS}=∗
-              T ns'
+              T ε α ε2 num ns ns'
       ))-∗ 
-        wp_update E (∃ n, T n); 
+        wp_update E (∃ ε α ε2 num ns ns', T ε α ε2 num ns ns'); 
   read_counter_spec {L: counterG Σ} N E c γ1 γ2 Q:
     ↑N ⊆ E ->
     {{{  is_counter (L:=L) N c γ1 γ2 ∗