From 0989c28c0b941fb7a570cecfbb97153117c6c202 Mon Sep 17 00:00:00 2001
From: Jean-Paul Calderone <exarkun@twistedmatrix.com>
Date: Mon, 7 Feb 2022 13:51:32 -0500
Subject: [PATCH] assert the count_unblinded_tokens invariant in the stateful
hypothesis test
---
src/_zkapauthorizer/tests/test_model.py | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/src/_zkapauthorizer/tests/test_model.py b/src/_zkapauthorizer/tests/test_model.py
index f72c463..2f74057 100644
--- a/src/_zkapauthorizer/tests/test_model.py
+++ b/src/_zkapauthorizer/tests/test_model.py
@@ -534,6 +534,18 @@ class UnblindedTokenStateMachine(RuleBasedStateMachine):
self.available += len(self.using)
del self.using[:]
+
+ @invariant()
+ def unblinded_token_count(self):
+ """
+ ``VoucherStore.count_unblinded_tokens`` returns the number of tokens
+ available to be spent.
+ """
+ self.case.assertThat(
+ self.configless.store.count_unblinded_tokens(),
+ Equals(self.available),
+ )
+
@invariant()
def report_state(self):
note(
--
GitLab