chore: Add Quint model of Interchain Security #1242

p-offtermatt · 2023-08-25T09:26:36Z

Description

Closes: #1239

This adds a quint model of interchain Security, based on the existing TLA+ model by @Kukovec.
There are a few notable differences:

Initializing is removed as a status - this is mostly because my goal is to use the model for MBT, and the initializing state is probably something we would skip past in the tests (also since the interactions with the initializing state aren't very meaningful in the model)
The actions the model exposes are slightly different, e.g. time advancement and chain status advancement are separate actions and don't happen simultaneously with other actions. This is because this makes the traces easier to test in Quint, i.e. more control over what happens when.
I model endBlocks for both provider and consumer chains. This is because I think this is a useful extra level of implementation details that will make test traces more meaningful.

Other than that, some implementation details are different. Some are my preference, some are just due to what is more natural to write in Quint, some are to (hopefully) make traces that are easier to use.

When this PR is merged, the model should also be added to the spec repo.

Author Checklist

All items are required. Please add a note to the item if the item is not applicable and
please add links to any relevant follow up issues.

I have...

Included the correct type prefix in the PR title
Targeted the correct branch (see PR Targeting)
Provided a link to the relevant issue or specification
Reviewed "Files changed" and left comments if necessary
Confirmed all CI checks have passed

Reviewers Checklist

All items are required. Please add a note if the item is not applicable and please add
your handle next to the items reviewed if you only reviewed selected items.

I have...

Confirmed the correct type prefix in the PR title
Confirmed all author checklist items have been addressed
Confirmed that this PR does not change production code

shaspitz

Great work! Very useful and well documented. I haven't taken too deep of a dive into model logic yet.

My two cents w.r.t the more broad conversation of using quint vs something like Rapid:

This model definitely seems readable, so readability of .qnt vs .go isn't an issue.
I'm still having trouble understanding why quint as a language is more succinct for writing models compared to other programming languages that're more widely known. There are global variables, types, functions, actions etc. defined, all composed together to create what we're referring to as a "model". These abstractions are all possible to encode with golang from my knowledge.
Can we use a debugger for .qnt like we could with .go files?
I'm not able to really validate the model logic until I take time to learn quint. This is mostly a me problem :)

shaspitz · 2023-09-05T18:16:04Z

tests/difference/core/quint_model/ccv.qnt

+
+
+    // set of identifiers of potential nodes
+    pure val Nodes: Set[Node] = 


Is this pretty much an example validator set? If so, why not define it as a ValidatorSet?

This is supposed to be the set of "potential" full nodes that could be validators, i.e. the validator set will be a subset of these (because some may not have any power=bonded tokens).

shaspitz · 2023-09-05T18:18:18Z

tests/difference/core/quint_model/ccv.qnt

+        Set("A", "B", "C", "D", "E", "F", "G", "H", "I", "J")
+
+    // the set of consumer chains
+    pure val ConsumerChains: Set[Chain] = 


Can these model parameters be changed? Ie. could we theoretically execute the model with 5 consumers for example

Yes, exactly, this can be changed.

shaspitz · 2023-09-05T18:27:39Z

tests/difference/core/quint_model/ccv.qnt

+            chain => chain.getCurrentValidatorSet().wasValidatorSetOnProvider()
+        )
+
+    // TESTS


Do tests over the model always have to be explicitly defined? My understanding is that quint somehow enables fuzzed or implicitly generated test cases

They do not need to be defined, Quint allows doing PBT in-built (checking that given invariants always hold).
This manual test case is mostly there for my benefit while writing the model to gradually check things I introduced, and can complement random testing.

p-offtermatt · 2023-09-06T07:51:48Z

Thanks for taking the time to review!

* This model definitely seems readable, so readability of .qnt vs .go isn't an issue.

That's great to hear!

* I'm still having trouble understanding why quint as a language is more succinct for writing models compared to other programming languages that're more widely known. There are global variables, types, functions, actions etc. defined, all composed together to create what we're referring to as a "model". These abstractions are all possible to encode with golang from my knowledge.

In principle, you are right, this can also be written in Golang. One big advantage is that Quint can be model-checked, which we would have a hard time doing with Golang (since it has more fine-grained concepts of e.g. memory, the state space blows up much faster).

* Can we use a debugger for .qnt like we could with .go files?

Something like it, there is a REPL that can serve the same purpose, though it is a bit different in the exact usage.

Thanks again for commenting, it's very helpful to hear different perspectives on this! If you find any of my responses unconvincing, please do let me know!

shaspitz · 2023-09-06T20:00:43Z

@p-offtermatt thanks for the responses! W.r.t One big advantage is that Quint can be model-checked, what do you mean by this? Is model checking the process of generating a large number of test traces over the described model? From my understanding Rapid has mechanisms which do this, although I admittedly do not have knowledge about the internals

p-offtermatt · 2023-09-07T07:27:47Z

@p-offtermatt thanks for the responses! W.r.t One big advantage is that Quint can be model-checked, what do you mean by this? Is model checking the process of generating a large number of test traces over the described model? From my understanding Rapid has mechanisms which do this, although I admittedly do not have knowledge about the internals

No, model-checking is more powerful. Intuitively, model-checking is an exhaustive way of checking all possible states of the model for given properties. Imagine for the Cosmos Hub, we want to ensure that token balances of wallets can never become negative. We could just try to show this e.g. via PBT by exhaustively generating test traces. Imagine there are 5 trillion possible states reachable over the course of the next 5 blocks (this is a vast underestimation of the state space for the Cosmos Hub that can be reached in 5 blocks), then exhaustively generating test traces can clearly never cover the whole state space in a reasonable time span. Model-checking in this context would mean checking all 5 trillion possible states, and we could conclusively say that in none of them is a wallet balance negative.

The problem is that model-checking a "full programming language" is very hard and slow, but for Quint it's possible. The proposed workflow then is to write a Quint model -> Model-check the Quint model to confirm it fulfills desirable safety properties -> use model-based testing to confirm the code behaves like the model, thus the code fulfills the desirable properties.

mpoke

Partial review before going into the model actions. See my comments below.

tests/difference/core/quint_model/ccv.qnt

mpoke · 2023-09-07T10:07:31Z

tests/difference/core/quint_model/ccv.qnt

+
+
+    // UTILITY FUNCTIONS & ACTIONS
+    def wasValidatorSetOnProvider(validatorSet: ValidatorSet): bool = {


Splitting the model into functional and SM would make these functions pure. For example, just define a type VotingPowerHistories and pass it to the function. I believe this would make the logic much easier to understand and maintain.

mpoke · 2023-09-07T10:12:34Z

tests/difference/core/quint_model/ccv.qnt

+    def getCurrentValidatorSet(chain: Chain): ValidatorSet = 
+        votingPowerHistories.get(chain).head()
+
+    def getUpdatedValidatorSet(oldValidatorSet: ValidatorSet, validator: Node, newVotingPower: int): ValidatorSet =


This should be a pure function.

mpoke · 2023-09-07T10:19:20Z

tests/difference/core/quint_model/ccv.qnt

+    def consumerTimedOut(consumer: Chain): bool =
+        any {
+            // either a package from provider to consumer has timed out
+            outstandingPacketsToConsumer.get(consumer).select(


Wouldn't this be more efficient to just look at the oldest packet in the list? Or we do not remove packets once they arrive?

mpoke · 2023-09-07T10:24:18Z

tests/difference/core/quint_model/ccv.qnt

+            // among those, get packets where inactivity timeout has passed
+            packetsWithoutResponse.filter(
+                packet => 
+                val sentAt = curChainTimes.get(ProviderChain) - PacketTimeout // compute when the packet was sent


Why was the packet sent at the current time on the provider minus the packet timeout?

mpoke · 2023-09-07T10:25:47Z

tests/difference/core/quint_model/ccv.qnt

+    // utility action that leaves all provider state untouched
+    action PROVIDER_NOOP(): bool = 
+        all {
+            receivedMaturations' = receivedMaturations,


What about sentVSCPackets and providerValidatorSetChangedInThisBlock?

mpoke

Some more comments.

mpoke · 2023-09-07T11:12:44Z

tests/difference/core/quint_model/ccv.qnt

+
+    // the power of a validator on the provider chain is changed to the given amount. We do not care how this happens,
+    // e.g. via undelegations, or delegations, ...
+    action votingPowerChange(validator: Node, amount: int): bool =


Why is it relevant to have an action that changes the power of a single validator. Wouldn't make more sense to have an action that changes the powers of a subset of the nodes? Like this, a change of powers for three validators can be done in one step instead of three.

mpoke · 2023-09-07T11:19:08Z

tests/difference/core/quint_model/ccv.qnt

+
+    // deliver the next outstanding packet from the consumer to the provider.
+    // since this model assumes a single provider chain, this just takes a single chain as argument.
+    action recvPacketOnProvider(consumer: Chain): bool = all {


ditto: more efficient to receive an arbitrary number of packets

mpoke · 2023-09-07T11:24:08Z

tests/difference/core/quint_model/ccv.qnt

+        val newOutstandingPackets = outstandingPacketsToConsumer.set(consumer, newPacketQueue)
+        RegisterNewOutstandingPackets(newOutstandingPackets),
+        val packet = outstandingPacketsToConsumer.get(consumer).head()
+        all {


Why is the all keyword needed here?

mpoke · 2023-09-07T11:26:22Z

tests/difference/core/quint_model/ccv.qnt

+
+    // deliver the next outstanding packet from the provider to the consumer.
+    // since this model assumes a single provider chain, this just takes a single chain as argument.
+    action recvPacketOnConsumer(consumer: Chain): bool = all {


ditto: arbitrary number of packets

mpoke · 2023-09-07T11:32:05Z

tests/difference/core/quint_model/ccv.qnt

+    action endAndBeginBlock(chain: Chain): bool = any {
+        all {
+          chain == ProviderChain,
+          endAndBeginBlockForProvider,
+        },
+        all {
+            chain != ProviderChain,
+            endAndBeginBlockForConsumer(chain),
+        }
+    }


This construction looks weird. Isn't any other way to do an if-else within an action?

mpoke · 2023-09-07T12:20:59Z

tests/difference/core/quint_model/ccv.qnt

+        },
+        PROVIDER_NOOP,
+        // no packets are sent to consumer or received by it
+        RegisterNewOutstandingPackets(outstandingPacketsToConsumer),


outstandingPacketsToConsumer remains unchanged. Why calling RegisterNewOutstandingPackets?

mpoke · 2023-09-07T12:22:12Z

tests/difference/core/quint_model/ccv.qnt

+    action AdvanceTime(): bool = 
+            val advanceAmounts = curChainTimes.keys().mapBy(
+                chain =>    
+                nondet amount = oneOf(1.to(10))


Why 1 to 10? What's the scale of time?

Also, is there a limit for the difference in time between two chains?

mpoke · 2023-09-07T12:23:48Z

tests/difference/core/quint_model/ccv.qnt

+
+    // advance timestamps for maps nondeterministically
+    action AdvanceTime(): bool = 
+            val advanceAmounts = curChainTimes.keys().mapBy(


Why not use chains.mabBy()?

mpoke · 2023-09-07T12:25:34Z

tests/difference/core/quint_model/ccv.qnt

+            AdvanceTimeByMap(advanceAmounts)
+
+    // the timestamp for each chain is advanced by the given amount
+    action AdvanceTimeByMap(advancementAmount: Chain -> int): bool = all


Why is this a different function than AdvanceTime()?

mpoke · 2023-09-07T12:33:49Z

tests/difference/core/quint_model/ccv.qnt

+    // some events may necessitate a transition, e.g. timeouts.
+    // shouldAdvance gives, for each consumer chain, whether it should advance if possible.
+    // if a chain has to advance, e.g. due to timeouts, or may not advance, the value will have no effect.
+    action AdvanceConsumers(shouldAdvance: Chain -> bool): bool = 


shouldAdvance is not clear.

p-offtermatt · 2023-09-07T13:25:56Z

Converting this to draft to make major changes after discussing with Marius - please hold on reviewing this for the new version!

Notes to myself:

curTimes are unnecessary - timestamps should be per block, and time advancement happens just in endBlock. same for consumer status
more realistic constant values
Split functional and state machine parts

This reverts commit 1320b95.

p-offtermatt · 2023-09-29T14:19:39Z

Just to keep it cleaner, I will close this PR and open a new one with the new model.
The model is rewritten from scratch anyways, so the old comments will not be very relevant.

p-offtermatt added 4 commits August 17, 2023 15:48

Start new attempt on Quint model of ICS

e2b6407

Advance quint model

283dc0a

Add first finished draft of model

2155a4f

Add test run to model

6ca6510

github-actions bot added the C:Testing Assigned automatically by the PR labeler label Aug 25, 2023

p-offtermatt added 2 commits August 25, 2023 15:20

Rename model, add test, use powerset for nondeterminism

e27e74b

Reintroduce vsc changed tracking variables

50fae34

p-offtermatt changed the title ~~Ph/quint model v2~~ chore: Add Quint model of Interchain Security Aug 25, 2023

p-offtermatt added 3 commits August 25, 2023 18:05

Add text with what expliticly is modelled

78e890a

Add bluespec to ccv.qnt

a1d57ef

Add bluespec to expraSpells.qnt

6c91866

p-offtermatt marked this pull request as ready for review August 25, 2023 20:01

p-offtermatt requested a review from a team as a code owner August 25, 2023 20:01

Add docstring to extraSpells module

2126eac

shaspitz reviewed Sep 5, 2023

View reviewed changes

mpoke reviewed Sep 7, 2023

View reviewed changes

p-offtermatt marked this pull request as draft September 7, 2023 13:59

p-offtermatt force-pushed the ph/quint-model-v2 branch from cdebe89 to 2126eac Compare September 18, 2023 14:11

p-offtermatt added 6 commits September 18, 2023 18:23

Start rewriting model

1320b95

Revert "Start rewriting model"

5fa449c

This reverts commit 1320b95.

Start rewriting quint model

c05d9e6

Continue seperating logic in Quint model

4bbe033

Start debugging cryptic error message

5ebab39

Start adding endAndBeginBlock defs

5bca6fc

p-offtermatt added 19 commits September 21, 2023 10:10

Diagnose Quint parser bug

4f77d68

Fix type in Quint

fa233d6

Add endBlock actions

66663bf

Start adding state machine module

7b489fe

Save status with crashing effect checker

b992f8c

Resolve issue by removing undefined field

baaddb7

Remove add

2c1341d

Fix init

e09968d

Snapshot spec with parser crasher

55ab595

Snapshot model

0897e8c

Start debugging tests

d227aee

Finish test for quint model

09b1b87

Add README and improve folder structure

96c101f

Fix import

aa2989e

Add some invariants

c291303

Refactor Consumer advancement

94a0acb

Snapshot error

8818531

Make time module upper case

633f8bb

Add invariants

f28d074

p-offtermatt closed this Sep 29, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: Add Quint model of Interchain Security #1242

chore: Add Quint model of Interchain Security #1242

p-offtermatt commented Aug 25, 2023 •

edited

Loading

shaspitz left a comment

shaspitz Sep 5, 2023

p-offtermatt Sep 6, 2023

shaspitz Sep 5, 2023

p-offtermatt Sep 6, 2023

shaspitz Sep 5, 2023

p-offtermatt Sep 6, 2023

shaspitz Sep 6, 2023

p-offtermatt commented Sep 6, 2023 •

edited

Loading

shaspitz commented Sep 6, 2023

p-offtermatt commented Sep 7, 2023 •

edited

Loading

mpoke left a comment

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke left a comment

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

mpoke Sep 7, 2023

p-offtermatt commented Sep 7, 2023 •

edited

Loading

p-offtermatt commented Sep 29, 2023



		// set of identifiers of potential nodes
		pure val Nodes: Set[Node] =



		// UTILITY FUNCTIONS & ACTIONS
		def wasValidatorSetOnProvider(validatorSet: ValidatorSet): bool = {

chore: Add Quint model of Interchain Security #1242

chore: Add Quint model of Interchain Security #1242

Conversation

p-offtermatt commented Aug 25, 2023 • edited Loading

Description

Author Checklist

Reviewers Checklist

shaspitz left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

p-offtermatt commented Sep 6, 2023 • edited Loading

shaspitz commented Sep 6, 2023

p-offtermatt commented Sep 7, 2023 • edited Loading

mpoke left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mpoke left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

p-offtermatt commented Sep 7, 2023 • edited Loading

p-offtermatt commented Sep 29, 2023

p-offtermatt commented Aug 25, 2023 •

edited

Loading

p-offtermatt commented Sep 6, 2023 •

edited

Loading

p-offtermatt commented Sep 7, 2023 •

edited

Loading

p-offtermatt commented Sep 7, 2023 •

edited

Loading