Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: Add Quint model of Interchain Security #1242

Closed
wants to merge 35 commits into from

Conversation

p-offtermatt
Copy link
Contributor

@p-offtermatt p-offtermatt commented Aug 25, 2023

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

@github-actions github-actions bot added the C:Testing Assigned automatically by the PR labeler label Aug 25, 2023
@p-offtermatt p-offtermatt changed the title Ph/quint model v2 chore: Add Quint model of Interchain Security Aug 25, 2023
@p-offtermatt p-offtermatt marked this pull request as ready for review August 25, 2023 20:01
@p-offtermatt p-offtermatt requested a review from a team as a code owner August 25, 2023 20:01
Copy link
Contributor

@shaspitz shaspitz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 :)



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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Set("A", "B", "C", "D", "E", "F", "G", "H", "I", "J")

// the set of consumer chains
pure val ConsumerChains: Set[Chain] =
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, exactly, this can be changed.

chain => chain.getCurrentValidatorSet().wasValidatorSetOnProvider()
)

// TESTS
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice!

@p-offtermatt
Copy link
Contributor Author

p-offtermatt commented Sep 6, 2023

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
Copy link
Contributor

shaspitz commented Sep 6, 2023

@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
Copy link
Contributor Author

p-offtermatt commented Sep 7, 2023

@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.

Copy link
Contributor

@mpoke mpoke left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

tests/difference/core/quint_model/ccv.qnt Outdated Show resolved Hide resolved
tests/difference/core/quint_model/ccv.qnt Outdated Show resolved Hide resolved
tests/difference/core/quint_model/ccv.qnt Outdated Show resolved Hide resolved
tests/difference/core/quint_model/ccv.qnt Outdated Show resolved Hide resolved
tests/difference/core/quint_model/ccv.qnt Outdated Show resolved Hide resolved


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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

def getCurrentValidatorSet(chain: Chain): ValidatorSet =
votingPowerHistories.get(chain).head()

def getUpdatedValidatorSet(oldValidatorSet: ValidatorSet, validator: Node, newVotingPower: int): ValidatorSet =
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be a pure function.

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What about sentVSCPackets and providerValidatorSetChangedInThisBlock?

Copy link
Contributor

@mpoke mpoke left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some more comments.


// 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 =
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


// 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 {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ditto: more efficient to receive an arbitrary number of packets

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is the all keyword needed here?


// 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 {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ditto: arbitrary number of packets

Comment on lines 294 to 303
action endAndBeginBlock(chain: Chain): bool = any {
all {
chain == ProviderChain,
endAndBeginBlockForProvider,
},
all {
chain != ProviderChain,
endAndBeginBlockForConsumer(chain),
}
}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

outstandingPacketsToConsumer remains unchanged. Why calling RegisterNewOutstandingPackets?

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not use chains.mabBy()?

AdvanceTimeByMap(advanceAmounts)

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this a different function than AdvanceTime()?

// 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 =
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

shouldAdvance is not clear.

@p-offtermatt
Copy link
Contributor Author

p-offtermatt commented Sep 7, 2023

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

@p-offtermatt p-offtermatt marked this pull request as draft September 7, 2023 13:59
@p-offtermatt p-offtermatt marked this pull request as draft September 7, 2023 13:59
@p-offtermatt
Copy link
Contributor Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
C:Testing Assigned automatically by the PR labeler
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Rewrite the TLA+ ICS model in Quint (see https://github.com/cosmos/ibc/pull/911)
3 participants