coinage-layer Phase 7 (part 14): op_count_in_flight diagnostic

Adds an aggregator over non-terminal operations:

  op_count_in_flight() -> usize

Counts operations with status in {Preparing, Submitted, InBlock,
Finalized, Waiting(_)}. Useful for "how many ops are pending" UI
and for tests asserting no in-flight ops remain after a cancellation
sweep.

(An earlier attempt at op_count_by_kind hit Verus's restriction on
deriving PartialEq for enums with payloads. Future work: add an
assume_specification for OpKind equality, or refactor to use match
arms.)

206 verified, 0 errors.

Author: TorstenStueber

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

@@ -4689,6 +4689,36 @@ impl State {
         c
     }
 
+    /// Count of operations currently in-flight (non-terminal status).
+    pub fn op_count_in_flight(&self) -> (count: usize)
+        requires
+            self.invariant(),
+        ensures
+            count <= self.operations@.len(),
+    {
+        let mut c: usize = 0;
+        let mut j: usize = 0;
+        while j < self.operations.len()
+            invariant
+                0 <= j <= self.operations.len(),
+                c <= j,
+                self.invariant(),
+            decreases self.operations.len() - j,
+        {
+            let op = &self.operations[j];
+            let is_terminal = match op.status {
+                OpStatus::Done => true,
+                OpStatus::Failed => true,
+                _ => false,
+            };
+            if !is_terminal {
+                c = c + 1;
+            }
+            j = j + 1;
+        }
+        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.