Rewrite mutating methods to only locally mutate.

informalsystems · Apr 20, 2021 · 858da86 · 858da86
1 parent 7093d06
commit 858da86
Showing 1 changed file with 19 additions and 16 deletions.
diff --git a/stainless/src/lib.rs b/stainless/src/lib.rs
@@ -145,22 +145,23 @@ impl<T: Clone> PeerList<T> {
     /// ## Precondition
     /// - The given peer id must not be the primary peer id.
     /// - The given peer must be in the witness list
-    #[pre(faulty_witness != self.primary && self.witnesses.contains(&faulty_witness))]
-    #[post(Self::invariant(&self))]
-    pub fn replace_faulty_witness(&mut self, faulty_witness: PeerId) -> Option<PeerId> {
+    #[pre(&faulty_witness != &self.primary && self.witnesses.contains(&faulty_witness))]
+    #[post(Self::invariant(&ret.0))]
+    pub fn replace_faulty_witness(self, faulty_witness: PeerId) -> (Self, Option<PeerId>) {
+        let mut new_list = self;
         let mut result = None;
 
-        self.witnesses.remove(&faulty_witness);
+        new_list.witnesses = new_list.witnesses.remove(&faulty_witness);
 
-        if let Some(new_witness) = self.full_nodes.iter().next().copied() {
-            self.witnesses.add(new_witness);
-            self.full_nodes.remove(&new_witness);
+        if let Some(new_witness) = new_list.full_nodes.iter().next().copied() {
+            new_list.witnesses = new_list.witnesses.add(new_witness);
+            new_list.full_nodes = new_list.full_nodes.remove(&new_witness);
             result = Some(new_witness);
         }
 
-        self.faulty_nodes.add(faulty_witness);
+        new_list.faulty_nodes = new_list.faulty_nodes.add(faulty_witness);
 
-        result
+        (new_list, result)
     }
 
     /// Mark the primary as faulty and swap it for the next available witness, if any.
@@ -170,15 +171,17 @@ impl<T: Clone> PeerList<T> {
     /// - If there are no witness left, returns `ErrorKind::NoWitnessLeft`.
     #[post(ret.is_ok().implies(Self::invariant(&self)))]
     pub fn replace_faulty_primary(
-        &mut self,
+        self,
         primary_error: Option<Error>,
-    ) -> Result<PeerId, Error> {
-        self.faulty_nodes.add(self.primary);
+    ) -> Result<(Self, PeerId), Error> {
+        let mut new_list = self;
 
-        if let Some(new_primary) = self.witnesses.iter().next().copied() {
-            self.primary = new_primary;
-            self.witnesses.remove(&new_primary);
-            Ok(new_primary)
+        new_list.faulty_nodes = new_list.faulty_nodes.add(new_list.primary);
+
+        if let Some(new_primary) = new_list.witnesses.iter().next().copied() {
+            new_list.primary = new_primary;
+            new_list.witnesses = new_list.witnesses.remove(&new_primary);
+            Ok((new_list, new_primary))
         } else if let Some(err) = primary_error {
             bail!(ErrorKind::NoWitnessLeft { context: Some(err) })
         } else {