remove redundant Lens struct, make for_each_mut require &mut self

src/collections/arraymap.rs

@@ -0,0 +1,7 @@
+#![cfg(verification)]
+
+use arrayvec;
+
+struct ArrayMap<K, V> {
+    keys: arrayvec,
+}

src/collections/mod.rs

@@ -17,57 +17,49 @@ mod default {
     // TODO: HashMap during lookup can touch keys other than the passed one, thus it can dereference root key while searching
     // for other keys, thus creating a shared borrow in addition to mutable one
     // TODO
-    pub struct Lens<'a, 'b, K, V> {
+    // TODO there can be a trait that provides a method that returns id and a unique sequence that are guaranteed to be unique together
+    // I e Apply message can easily implement it, because transaction cant depend on itself thus Apply.txn_id
+    // and Apply.dependencies are guaranteed to be unique together
+    // TODO clarify that guards are needed because if these methods exist on Lens itself we must have shared reference as self parameter
+    // which is wrong because this way we'd be able to invoke several for_each_mut iterators inside of each other which would end
+    // up in multiple mutable references existing for the same memory location which violates safety
+    pub fn split<'a, 'b, K, V>(
         root_key: K,
         other_keys: &'a Set<K>,
         source: &'b mut Map<K, V>,
-    }
-
-    impl<'a, 'b, K, V> Lens<'a, 'b, K, V>
+    ) -> Option<(RootGuard<'b, K, V>, IterGuard<'a, 'b, K, V>)>
     where
         K: Eq + Hash,
     {
-        // TODO there can be a trait that provides a method that returns id and a unique sequence that are guaranteed to be unique together
-        // I e Apply message can easily implement it, because transaction cant depend on itself thus Apply.txn_id
-        // and Apply.dependencies are guaranteed to be unique together
-        // TODO clarify that guards are needed because if these methods exist on Lens itself we must have shared reference as self parameter
-        // which is wrong because this way we'd be able to invoke several for_each_mut iterators inside of each other which would end
-        // up in multiple mutable references existing for the same memory location which violates safety
-        pub fn zoom(
-            root_key: K,
-            other_keys: &'a Set<K>,
-            source: &'b mut Map<K, V>,
-        ) -> Option<(LensRootGuard<'b, K, V>, LensIterGuard<'a, 'b, K, V>)> {
-            if other_keys.contains(&root_key) {
-                return None;
-            }
-
-            let hash = source.hasher().hash_one(&root_key);
-            let root_bucket = source
-                .raw_table()
-                .find(hash, |(k, _)| k.equivalent(&root_key))
-                .expect("TODO");
-
-            Some((
-                LensRootGuard {
-                    bucket: root_bucket,
-                    _phantom: PhantomData,
-                },
-                LensIterGuard {
-                    other_keys,
-                    source,
-                    root_key,
-                },
-            ))
+        if other_keys.contains(&root_key) {
+            return None;
         }
+
+        let hash = source.hasher().hash_one(&root_key);
+        let root_bucket = source
+            .raw_table()
+            .find(hash, |(k, _)| k.equivalent(&root_key))
+            .expect("TODO");
+
+        Some((
+            RootGuard {
+                bucket: root_bucket,
+                _phantom: PhantomData,
+            },
+            IterGuard {
+                other_keys,
+                source,
+                root_key,
+            },
+        ))
     }
 
-    pub struct LensRootGuard<'a, K, V> {
+    pub struct RootGuard<'a, K, V> {
         bucket: Bucket<(K, V)>,
         _phantom: PhantomData<&'a ()>,
     }
 
-    impl<'b, K, V> LensRootGuard<'b, K, V>
+    impl<'b, K, V> RootGuard<'b, K, V>
     where
         K: Eq + Hash,
     {
@@ -79,16 +71,16 @@ mod default {
         }
     }
 
-    pub struct LensIterGuard<'a, 'b, K, V> {
+    pub struct IterGuard<'a, 'b, K, V> {
         root_key: K,
         other_keys: &'a Set<K>,
         source: &'b mut Map<K, V>,
     }
-    impl<'a, 'b, K, V> LensIterGuard<'a, 'b, K, V>
+    impl<'a, 'b, K, V> IterGuard<'a, 'b, K, V>
     where
         K: Eq + Hash,
     {
-        pub fn for_each_mut(&self, mut f: impl FnMut(&K, &mut V)) {
+        pub fn for_each_mut(&mut self, mut f: impl FnMut(&K, &mut V)) {
             for key in self.other_keys {
                 let hash = self.source.hasher().hash_one(key);
                 let entry = self
@@ -104,18 +96,24 @@ mod default {
             }
         }
 
-        pub fn exchange(self, other_keys: &'a Set<K>) -> Option<Self> {
+        pub fn exchange(self, other_keys: &'a Set<K>) -> Result<Self, Self> {
             if other_keys.contains(&self.root_key) {
-                return None;
+                return Err(self);
             }
 
-            Some(Self {
+            Ok(Self {
                 root_key: self.root_key,
                 other_keys,
                 source: self.source,
             })
         }
     }
+
+    impl<'a, 'b, K, V> std::fmt::Debug for IterGuard<'a, 'b, K, V> {
+        fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+            f.debug_struct("IterGuard").finish()
+        }
+    }
 }
 
 // #[cfg(test)]
@@ -129,48 +127,40 @@ mod verification {
     pub type Map<K, V> = VecMap<K, V>;
     pub type MapEntry<'a, K, V> = Entry<'a, K, V>;
 
-    pub struct Lens<'a, 'b, K, V> {
+    pub fn split<'a, 'b, K, V>(
         root_key: K,
         other_keys: &'a Set<K>,
         source: &'b mut Map<K, V>,
-    }
-
-    impl<'a, 'b, K, V> Lens<'a, 'b, K, V>
+    ) -> Option<(RootGuard<'b, K, V>, IterGuard<'a, 'b, K, V>)>
     where
         K: Eq,
     {
-        pub fn zoom(
-            root_key: K,
-            other_keys: &'a Set<K>,
-            source: &'b mut Map<K, V>,
-        ) -> Option<(LensRootGuard<'b, K, V>, LensIterGuard<'a, 'b, K, V>)> {
-            if other_keys.contains(&root_key) {
-                return None;
-            }
-
-            let root_position = source.position(&root_key).unwrap();
-            let root_ptr = unsafe { source.as_values_ptr().add(root_position) };
-
-            Some((
-                LensRootGuard {
-                    root_ptr,
-                    _phantom: PhantomData,
-                },
-                LensIterGuard {
-                    other_keys,
-                    source,
-                    root_key,
-                },
-            ))
+        if other_keys.contains(&root_key) {
+            return None;
         }
+
+        let root_position = source.position(&root_key).unwrap();
+        let root_ptr = unsafe { source.as_values_ptr().add(root_position) };
+
+        Some((
+            RootGuard {
+                root_ptr,
+                _phantom: PhantomData,
+            },
+            IterGuard {
+                other_keys,
+                source,
+                root_key,
+            },
+        ))
     }
 
-    pub struct LensRootGuard<'a, K, V> {
+    pub struct RootGuard<'a, K, V> {
         root_ptr: *const V,
         _phantom: PhantomData<&'a (K, V)>,
     }
 
-    impl<'b, K, V> LensRootGuard<'b, K, V>
+    impl<'b, K, V> RootGuard<'b, K, V>
     where
         K: Eq,
     {
@@ -183,16 +173,17 @@ mod verification {
         }
     }
 
-    pub struct LensIterGuard<'a, 'b, K, V> {
+    pub struct IterGuard<'a, 'b, K, V> {
         root_key: K,
         other_keys: &'a Set<K>,
         source: &'b mut Map<K, V>,
     }
-    impl<'a, 'b, K, V> LensIterGuard<'a, 'b, K, V>
+
+    impl<'a, 'b, K, V> IterGuard<'a, 'b, K, V>
     where
         K: Eq,
     {
-        pub fn for_each_mut(&self, mut f: impl FnMut(&K, &mut V)) {
+        pub fn for_each_mut(&mut self, mut f: impl FnMut(&K, &mut V)) {
             for key in self.other_keys {
                 let position = self.source.position(key).unwrap();
                 unsafe {
@@ -215,6 +206,12 @@ mod verification {
             })
         }
     }
+
+    impl<'a, 'b, K, V> std::fmt::Debug for IterGuard<'a, 'b, K, V> {
+        fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+            f.debug_struct("IterGuard").finish()
+        }
+    }
 }
 
 #[cfg(not(kani))]

src/protocol/replica.rs

@@ -1,7 +1,7 @@
 use std::cmp;
 
 use crate::{
-    collections::{Lens, LensIterGuard, Map, MapEntry, Set},
+    collections::{split, IterGuard, Map, MapEntry, Set},
     protocol::{
         messages::{Accept, AcceptOk, Apply, Commit, PreAccept, PreAcceptOk, Read, ReadOk},
         node::DataStore,
@@ -351,13 +351,13 @@ impl Replica {
         // TODO (feature) arm recovery timer
         let dummy = Set::new();
         let (mut root_guard, dummy_iter_guard) =
-            Lens::zoom(commit.txn_id, &dummy, &mut self.transactions).expect("TODO");
+            split(commit.txn_id, &dummy, &mut self.transactions).expect("TODO");
 
         root_guard.with_mut(|progress| {
             let stage_consensus = progress.as_mut_pre_accepted_or_accepted().expect("TODO");
             let stage_execution = StageExecution::from(stage_consensus);
 
-            let deps_waiting_guard = dummy_iter_guard
+            let mut deps_waiting_guard = dummy_iter_guard
                 .exchange(&stage_execution.dependencies_waiting)
                 .expect("TODO");
 
@@ -372,7 +372,7 @@ impl Replica {
 
     fn register_pending_dependencies(
         txn_id: TxnId,
-        deps_iter_guard: &mut LensIterGuard<TxnId, ReplicaTransactionProgress>,
+        deps_iter_guard: &mut IterGuard<TxnId, ReplicaTransactionProgress>,
     ) -> Map<TxnId, WaitingOn> {
         // Register this transaction in each of its dependencies so once they're
         // committed/applied this transaction can move forward too
@@ -425,7 +425,7 @@ impl Replica {
         data_store: &DataStore,
     ) -> Option<ReadOk> {
         let (mut root_guard, mut deps_iter_guard) =
-            Lens::zoom(read.txn_id, &read.dependencies, &mut self.transactions).expect("TODO");
+            split(read.txn_id, &read.dependencies, &mut self.transactions).expect("TODO");
 
         root_guard.with_mut(|progress| {
             let stage_committed = progress.as_mut_committed().expect("TODO");
@@ -461,7 +461,7 @@ impl Replica {
 
     fn propagate_apply_to_waiting_dependencies(
         txn_id: TxnId,
-        dependencies_waiting_iter_guard: LensIterGuard<'_, '_, TxnId, ReplicaTransactionProgress>,
+        mut dependencies_waiting_iter_guard: IterGuard<'_, '_, TxnId, ReplicaTransactionProgress>,
         res: &mut Vec<(NodeId, ReadOk)>,
         data_store: &mut DataStore,
     ) {
@@ -511,7 +511,7 @@ impl Replica {
         use ReplicaTransactionProgress::*;
 
         let (mut root_guard, mut pending_deps_iter_guard) =
-            Lens::zoom(apply.txn_id, &apply.dependencies, &mut self.transactions).expect("TODO");
+            split(apply.txn_id, &apply.dependencies, &mut self.transactions).expect("TODO");
 
         let mut res = vec![];