nits

theories/coneris/error_rules.v

@@ -1297,10 +1297,9 @@ Qed.
     iPureIntro. rewrite fmap_app; by f_equal.
   Qed.
 
-  Lemma state_step_err_set_in_out (N : nat) (z : Z) (bad : gset nat) (ε εI εO : R) E α ns :
-    TCEq N (Z.to_nat z) →
-    (0<=εI)%R →
-    (0<=εO)%R →
+  Lemma state_step_err_set_in_out (N : nat) (bad : gset nat) (ε εI εO : R) E α ns :
+    (0 <= εI)%R →
+    (0 <= εO)%R →
     (∀ n, n ∈ bad -> n < S N) →
     (εI * (size bad) + εO * (N + 1 - size bad)  <= ε * (N + 1))%R →
     α ↪N (N; ns) -∗
@@ -1309,11 +1308,10 @@ Qed.
         ((⌜fin_to_nat x ∉ bad⌝ ∗ ↯ εO) ∨ (⌜fin_to_nat x ∈ bad⌝ ∗ ↯ εI)) ∗
           α ↪N (N; ns ++ [fin_to_nat x])).
   Proof.
-    iIntros (HN HineqI HineqO Hlen Hleq) "Htape Herr".
+    iIntros (HineqI HineqO Hlen Hleq) "Htape Herr".
     set (ε2 := (λ x : fin (S N), if bool_decide (fin_to_nat x ∈ bad) then εI else εO)).
     iMod (state_update_presample_exp _ _ _ _ (SeriesC (λ n : fin (S N), (1 / (N + 1) * ε2 n)%R)) ε2
            with "Htape [Herr]") as (x) "[Htape Herr]".
-    (* wp_apply (wp_couple_rand_adv_comp1 _ _ _  (SeriesC (λ n : fin (S N), (1 / (N + 1) * ε2 n)%R)) ε2 with "[Herr]"). *)
     { intros. rewrite /ε2. by case_bool_decide. }
     { rewrite S_INR. done. }
     { iApply ec_weaken; auto.

theories/coneris/examples/hash/con_hash_impl4.v

@@ -1,13 +1,11 @@
 From iris.base_logic.lib Require Import ghost_map.
 From clutch.coneris Require Import coneris.
 From clutch.coneris.lib Require Import map lock.
-From clutch.coneris.examples Require Import coll_free_hash_view_impl.
 Set Default Proof Using "Type*".
 
 Class con_hashG Σ `{conerisGS Σ} := {
   con_hash_lock :: lock.lock;
   con_hash_lockG : lockG Σ;
-  con_hash_hash_viewG : hvG1 Σ;
   con_hash_ghost_mapG1 :: ghost_mapG Σ nat loc;
   con_hash_ghost_mapG2 :: ghost_mapG Σ nat (option nat);
 }.
@@ -132,6 +130,8 @@ Section con_hash_impl.
        map_list ltm ((λ (α : loc), LitV (LitLbl α)) <$> tm) ∗
        ghost_map_auth γtm 1 tm ∗
        ghost_map_auth γvm 1 vm' ∗
+       (** [vm] is the physical value map, whereas [vm'] is the logical value map. In this way, the
+           points-to [k ↪[γv] None] represents a "permission" to write to the key [k]. *)
        ⌜∀ i v, vm !! i = Some v ↔ vm' !! i = Some (Some v)⌝.
 
   Lemma wp_init_hash_state max :
@@ -241,7 +241,7 @@ Section con_hash_impl.
   Proof.
     iIntros (Hmax Hsize Heps) "Hkey Herr".
     iDestruct "Hkey" as (α w) "(Hk & Hw & Hα & %)".
-    iMod (state_step_err_set_in_out _ val_size bad _ εI εO
+    iMod (state_step_err_set_in_out _ bad _ εI εO
            with "Hα Herr") as (n) "[Herr Htape] /=".
     { apply cond_nonneg. }
     { apply cond_nonneg. }