Checkpoint

cosmos · Oct 31, 2022 · 94a7036 · 94a7036
1 parent 37fab45
commit 94a7036
Show file tree

Hide file tree

Showing 2 changed files with 63 additions and 27 deletions.
diff --git a/x/ccv/provider/keeper/keymap_api.cfg b/x/ccv/provider/keeper/keymap_api.cfg
@@ -1,4 +1,8 @@
+CONSTANTS
+    STORAGE_CONSTANT = 2
+    ProviderKeys = {0, 1, 2, 3}
+    ConsumerKeys = {0, 1, 2, 3, 4, 5, 6, 7, 8}
 INIT Init
 NEXT Next
-INVARIANT Inv
+INVARIANT Invariant
 
diff --git a/x/ccv/provider/keeper/keymap_api.tla b/x/ccv/provider/keeper/keymap_api.tla
@@ -2,81 +2,109 @@
 
 EXTENDS  Integers, Naturals, FiniteSets, Sequences, TLC
 
-Validators == 0..2
-ProviderKeys == 0..2
-ConsumerKeys == 0..8
+CONSTANTS
+    STORAGE_CONSTANT,
+    ProviderKeys,
+    ConsumerKeys
 
 VARIABLES
     assignments,
     providerValSets,
     committedProviderVSCID,
     committedConsumerVSCID,
-    greatestConsumerVSCIDMatured
+    maturedConsumerVSCID
 
 Init ==
     \* Store the genesis assignment, and the current assignment
-    /\ assignments = [1 |-> [key \in ProviderKeys |-> key],
-                      2 |-> [key \in ProviderKeys |-> key]]
+    /\ assignments = [vscid \in 1..2 |-> [key \in ProviderKeys |-> key]]
     \* One valset has been committed (genesis)
-    /\ \E valset \in SUBSET Validators: 
-       providerValSets = [1 |-> valset]
+    /\ \E valset \in SUBSET ProviderKeys: 
+       providerValSets = [vscid \in {1} |-> valset]
     \* Genesis block is committed
     /\ committedProviderVSCID = 1
     \* on consumer too.
     /\ committedConsumerVSCID = 1
     \* Nothing has matured yet.
-    /\ greatestConsumerVSCIDMatured = 0
+    /\ maturedConsumerVSCID = 0
 
 AssignKey == 
     \E providerKey \in ProviderKeys, consumerKey \in ConsumerKeys:
     \* consumerKey is not in use
-    /\ ~(k \in DOMAIN assignments : assignments[k][providerKey] = consumerKey)
+    /\ ~(\E i \in DOMAIN assignments: \E k \in DOMAIN assignments[i] : assignments[i][k] = consumerKey)
     \* Do assignment
-    /\ assignments' = [assignments EXCEPT ![committedProviderVSCID + 1] = [@ EXCEPT ![providerKey] = consumerKey] ]
+    /\ assignments' = [
+        assignments EXCEPT ![committedProviderVSCID + 1] = 
+        [@ EXCEPT ![providerKey] = consumerKey] ]
     \* The rest...
-    /\ UNCHANGED << providerValSets, committedProviderVSCID, committedConsumerVSCID, greatestConsumerVSCIDMatured >>
+    /\ UNCHANGED << providerValSets, committedProviderVSCID, committedConsumerVSCID, maturedConsumerVSCID >>
 
 ProviderEndAndCommitBlock ==
-    \E valset \in SUBSET Validators:
+    \E valset \in SUBSET ProviderKeys:
     \* Create a new assignment entry
-    /\ assignments' = assignments @@ [committedProviderVSCID' |-> assignments[committedProviderVSCID]]
+    /\ assignments' = assignments @@ [vscid \in {committedProviderVSCID+2} |-> assignments[committedProviderVSCID]]
     \* Get a new validator set from changes in voting power
-    /\ providerValSets' = providerValSets @@ [committedProviderVSCID' |-> valset]
+    /\ providerValSets' = providerValSets @@ [vscid \in {committedProviderVSCID+1} |-> valset]
     \* Increment vscid
     /\ committedProviderVSCID' = committedProviderVSCID + 1
     \* The rest...
-    /\ UNCHANGED << committedConsumerVSCID, greatestConsumerVSCIDMatured >>
+    /\ UNCHANGED << committedConsumerVSCID, maturedConsumerVSCID >>
 
 ConsumerDeliverUpdates == 
     \* Fast forward the consumer
     \E vscid \in (committedConsumerVSCID + 1)..committedProviderVSCID:
     committedConsumerVSCID' = vscid
+    \* The rest...
+    /\ UNCHANGED <<committedProviderVSCID, assignments, providerValSets, maturedConsumerVSCID >>
 
 ProviderDeliverMaturities == 
     \* Fast forward the consumer maturities, and notify provider
-    \E vscid \in (greatestConsumerVSCIDMatured + 1)..committedConsumerVSCID:
-    greatestConsumerVSCIDMatured' = vscid
+    \E vscid \in (maturedConsumerVSCID + 1)..committedConsumerVSCID:
+    /\ maturedConsumerVSCID' = vscid
+    /\ assignments' = [i \in {
+            j \in DOMAIN assignments : vscid < j \/ committedProviderVSCID <= j
+        } |-> assignments[i]]
+    \* The rest...
+    /\ UNCHANGED <<committedConsumerVSCID, committedProviderVSCID, providerValSets>>
 
 Next ==
     \/ AssignKey
     \/ ProviderEndAndCommitBlock
     \/ ConsumerDeliverUpdates
     \/ ProviderDeliverMaturities
 
-ReverseQueries == 
-    LET Query(consumerKey) == {providerKey \in ProviderKeys : 
-    \E ix \in assignments
-    assignments[Len(assignments)][providerKey] = consumerKey}
+(***************************************************************************)
+(** Invariants *************************************************************)
+(***************************************************************************)
+(***************************************************************************)
 
+(*
+Storage cost grows bigO(committedProviderVSCID - maturedConsumerVSCID)
+*)
+BoundedStorage ==
+    Cardinality(DOMAIN(assignments)) <= STORAGE_CONSTANT * (1 + (committedProviderVSCID - maturedConsumerVSCID))
 
-    \A ix \in (greatestConsumerVSCIDMatured+1)..consumerVSCID:
-      \A consumerKey \in {assignments[ix][key] : key \in providerValSets[ix]}:
-
+(*
+It's always possible to retrieve a unique provider key, for any consumer key
+known to the consumer.
+*)
+UniqueReverseQuery == 
+    \A i \in (maturedConsumerVSCID + 1)..committedConsumerVSCID : 
+    LET
+    \* The valset known to the consumer
+    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 :
+            \E j \in DOMAIN assignments : assignments[j][providerKey] = consumerKey
+        }
+    \* The query for the providerKey is successful and the result is unique.
+    IN \A consumerKey \in ConsumerValset : Cardinality(Assigned(consumerKey)) = 1
 
 
+(*Check that the spec is written correctly.*)
 Sanity == LET
     Sanity0 == committedConsumerVSCID <= committedProviderVSCID
-    Sanity1 == greatestConsumerVSCIDMatured <= committedConsumerVSCID
+    Sanity1 == maturedConsumerVSCID <= committedConsumerVSCID
     Sanity2 == committedProviderVSCID \in DOMAIN assignments
     Sanity3 == committedProviderVSCID + 1 \in DOMAIN assignments
     Sanity4 == committedProviderVSCID \in DOMAIN providerValSets
@@ -87,4 +115,8 @@ Sanity == LET
     /\ Sanity3
     /\ Sanity4
 
+Invariant == Sanity /\ BoundedStorage /\ UniqueReverseQuery
+
+(***************************************************************************)
+
 ====