From 94a7036f0ee7a7c17a3cd5e7486325a4b685cd4f Mon Sep 17 00:00:00 2001 From: Daniel Date: Mon, 31 Oct 2022 18:57:10 +0000 Subject: [PATCH] Checkpoint --- x/ccv/provider/keeper/keymap_api.cfg | 6 +- x/ccv/provider/keeper/keymap_api.tla | 84 +++++++++++++++++++--------- 2 files changed, 63 insertions(+), 27 deletions(-) diff --git a/x/ccv/provider/keeper/keymap_api.cfg b/x/ccv/provider/keeper/keymap_api.cfg index 4041534018..00f0d904b9 100644 --- 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 index be9acf0c2e..31fb5fcc85 100644 --- a/x/ccv/provider/keeper/keymap_api.tla +++ b/x/ccv/provider/keeper/keymap_api.tla @@ -2,60 +2,69 @@ 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 <> 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 <> Next == \/ AssignKey @@ -63,20 +72,39 @@ Next == \/ 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 + +(***************************************************************************) + ==== \ No newline at end of file