Caps constant names

cosmos · Oct 31, 2022 · 59e81fc · 59e81fc
1 parent 9481d3d
commit 59e81fc
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 12 deletions.
diff --git a/x/ccv/provider/keeper/keymap_api.cfg b/x/ccv/provider/keeper/keymap_api.cfg
@@ -1,7 +1,10 @@
 CONSTANTS
     STORAGE_CONSTANT = 2
-    ProviderKeys = {0, 1, 2, 3}
-    ConsumerKeys = {0, 1, 2, 3, 4, 5, 6, 7, 8}
+(*
+Could be improved by using model value symmetries.
+*)
+    PROVIDER_KEYS = {0, 1, 2, 3}
+    CONSUMER_KEYS = {0, 1, 2, 3, 4, 5, 6, 7, 8}
 INIT Init
 NEXT Next
 INVARIANT Invariant

diff --git a/x/ccv/provider/keeper/keymap_api.tla b/x/ccv/provider/keeper/keymap_api.tla
@@ -4,8 +4,8 @@ EXTENDS  Integers, Naturals, FiniteSets, Sequences, TLC
 
 CONSTANTS
     STORAGE_CONSTANT,
-    ProviderKeys,
-    ConsumerKeys
+    PROVIDER_KEYS,
+    CONSUMER_KEYS
 
 VARIABLES
     assignments,
@@ -26,9 +26,9 @@ VARIABLES
 
 Init ==
     \* Store the genesis assignment, and the current assignment
-    /\ assignments = [vscid \in 1..2 |-> [key \in ProviderKeys |-> key]]
+    /\ assignments = [vscid \in 1..2 |-> [key \in PROVIDER_KEYS |-> key]]
     \* One valset has been committed (genesis)
-    /\ \E valset \in SUBSET ProviderKeys: 
+    /\ \E valset \in SUBSET PROVIDER_KEYS: 
        providerValSets = [vscid \in {1} |-> valset]
     \* Genesis block is committed
     /\ committedProviderVSCID = 1
@@ -43,7 +43,7 @@ Init ==
 (***************************************)
 
 AssignKey == 
-    \E providerKey \in ProviderKeys, consumerKey \in ConsumerKeys:
+    \E providerKey \in PROVIDER_KEYS, consumerKey \in CONSUMER_KEYS:
     \* consumerKey is not in use
     /\ ~(\E i \in DOMAIN assignments: \E k \in DOMAIN assignments[i] : assignments[i][k] = consumerKey)
     \* Do assignment
@@ -59,7 +59,7 @@ AssignKey ==
 (***************************************)
 
 ProviderEndAndCommitBlock ==
-    \E valset \in SUBSET ProviderKeys:
+    \E valset \in SUBSET PROVIDER_KEYS:
     \* Create a new assignment entry
     /\ assignments' = assignments @@ [vscid \in {committedProviderVSCID+2} |-> assignments[committedProviderVSCID]]
     \* Get a new validator set from changes in voting power
@@ -108,7 +108,7 @@ queryable.
 True by construction: 'how' not explicitly modelled.
 *)
 AssignmentIsDefined == 
-    \A k \in ProviderKeys:
+    \A k \in PROVIDER_KEYS:
     LET ConsumerKey == assignments[committedProviderVSCID + 1][k]
     IN TRUE
 
@@ -139,7 +139,7 @@ UniqueReverseQueryResultIsDefined ==
     ConsumerValset == {assignments[i][k] : k \in providerValSets[i]}
     \* All the keys that are assigned to the consumerKey in stored assignments
     Assigned(consumerKey) == {
-            providerKey \in ProviderKeys :
+            providerKey \in PROVIDER_KEYS :
             \E j \in DOMAIN assignments : assignments[j][providerKey] = consumerKey
         }
     \* The query for the providerKey is successful and the result is unique.
@@ -148,7 +148,7 @@ UniqueReverseQueryResultIsDefined ==
 (*
 Storage cost grows linearly with committedProviderVSCID - maturedConsumerVSCID
 *)
-BoundedStorage ==
+StorageIsBounded ==
     Cardinality(DOMAIN(assignments)) <= STORAGE_CONSTANT * (1 + (committedProviderVSCID - maturedConsumerVSCID))
 
 
@@ -166,7 +166,12 @@ Sanity == LET
     /\ Sanity3
     /\ Sanity4
 
-Invariant == Sanity /\ BoundedStorage /\ UniqueReverseQuery
+Invariant == 
+    /\ Sanity
+    /\ AssignmentIsDefined
+    /\ ConsumerValidatorSetIsDefined
+    /\ UniqueReverseQueryResultIsDefined
+    /\ StorageIsBounded
 
 (***************************************************************************)