coinage-layer Phase 7 (part 13): coin/entry_count_in_purse total aggregators

Adds total-count aggregators that don't filter by state:

  coin_count_in_purse(p)  -> usize  // all coins regardless of state
  entry_count_in_purse(p) -> usize  // all entries regardless of state

Complement the state-filtered count primitives (coin_count_available,
entry_count_selectable). Useful for diagnostics ("how cluttered is
this purse"), test assertions, and pre-flight checks before purse
maintenance ops that don't care about state.

204 verified, 0 errors.

Author: TorstenStueber

rust/crates/coinage-layer/src/lib.rs

@@ -4689,6 +4689,57 @@ impl State {
         c
     }
 
+    /// Count of all coins (any state) in purse `p`. Useful diagnostic
+    /// for "how cluttered is this purse?". Distinguish from
+    /// coin_count_available which excludes locked/spent/pending.
+    pub fn coin_count_in_purse(&self, p: PurseId) -> (count: usize)
+        requires
+            self.invariant(),
+        ensures
+            count <= self.coins@.len(),
+    {
+        let mut c: usize = 0;
+        let mut j: usize = 0;
+        while j < self.coins.len()
+            invariant
+                0 <= j <= self.coins.len(),
+                c <= j,
+                self.invariant(),
+            decreases self.coins.len() - j,
+        {
+            if self.coins[j].purse == p {
+                c = c + 1;
+            }
+            j = j + 1;
+        }
+        c
+    }
+
+    /// Count of all entries (any state) in purse `p`. Entry parallel
+    /// of `coin_count_in_purse`.
+    pub fn entry_count_in_purse(&self, p: PurseId) -> (count: usize)
+        requires
+            self.invariant(),
+        ensures
+            count <= self.entries@.len(),
+    {
+        let mut c: usize = 0;
+        let mut j: usize = 0;
+        while j < self.entries.len()
+            invariant
+                0 <= j <= self.entries.len(),
+                c <= j,
+                self.invariant(),
+            decreases self.entries.len() - j,
+        {
+            if self.entries[j].purse == p {
+                c = c + 1;
+            }
+            j = j + 1;
+        }
+        c
+    }
+
     /// Count of `Available` coins in purse `p`. Used by maintenance
     /// triggers — e.g. "if coin_count_available(p) > threshold, run
     /// rebalance to consolidate into fewer larger coins".