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.

Sign up for GitHub

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

Jump to bottom

Add Quint model of Interchain Security #1336

Merged
merged 81 commits into from
Oct 19, 2023
Merged

Add Quint model of Interchain Security #1336

merged 81 commits into from
Oct 19, 2023

Conversation

p-offtermatt
Copy link
Contributor

@p-offtermatt p-offtermatt commented Sep 29, 2023 •
edited
Loading

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 happen only during EndBlocks/BeginBlocks 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.

How to review:

  • Read README.md for some cursory explanations
  • Run tests and sanity checks using the commands from the README. Running the invariant checks is probably too time consuming and not necessary.
  • Read through ccv.qnt. Reading top-down is probably fine. What to pay attention to here: Does the code match the intention of the CCV protocol as specified here https://github.com/cosmos/ibc/tree/main/spec/app/ics-028-cross-chain-validation?
  • Read through ccv_test.qnt. What to pay attention to here: Do the test traces make sense and provide fine coverage? These are supposed to be unit tests.
  • Read through ccv_statemachine.qnt. This needs to not be looked at as thoroughly as the core logic in ccv.qnt, except: the INVARIANT CHECKS are important to look at. What to pay attention to: Are there more invariants that you think should be expressed here? Just generally, this would be any properties that you assume hold true for the interchain security protocol when you reason about it.

p-offtermatt and others added 30 commits August 17, 2023 15:48
@p-offtermatt
Start new attempt on Quint model of ICS
e2b6407
@p-offtermatt
Advance quint model
283dc0a
@p-offtermatt
Add first finished draft of model
2155a4f
@p-offtermatt
Add test run to model
6ca6510
@p-offtermatt
Rename model, add test, use powerset for nondeterminism
e27e74b
@p-offtermatt
Reintroduce vsc changed tracking variables
50fae34
@p-offtermatt
Add text with what expliticly is modelled
78e890a
@p-offtermatt
Add bluespec to ccv.qnt
a1d57ef
@p-offtermatt
Add bluespec to expraSpells.qnt
6c91866
@p-offtermatt
Add docstring to extraSpells module
2126eac
@p-offtermatt
Start rewriting model
1320b95
@p-offtermatt
Revert "Start rewriting model"
5fa449c 
This reverts commit 1320b95.
@p-offtermatt
Start rewriting quint model
c05d9e6
@p-offtermatt
Continue seperating logic in Quint model
4bbe033
@p-offtermatt
Start debugging cryptic error message
5ebab39
@p-offtermatt
Start adding endAndBeginBlock defs
5bca6fc
@p-offtermatt
Diagnose Quint parser bug
4f77d68
@p-offtermatt
Fix type in Quint
fa233d6
@p-offtermatt
Add endBlock actions
66663bf
@p-offtermatt
Start adding state machine module
7b489fe
@p-offtermatt
Save status with crashing effect checker
b992f8c
@p-offtermatt
Resolve issue by removing undefined field
baaddb7
@p-offtermatt
Remove add
2c1341d
@p-offtermatt
Fix init
e09968d
@p-offtermatt
Snapshot spec with parser crasher
55ab595
@p-offtermatt
Snapshot model
0897e8c
@p-offtermatt
Start debugging tests
d227aee
@p-offtermatt
Finish test for quint model
09b1b87
@p-offtermatt
Add README and improve folder structure
96c101f
@p-offtermatt
Fix import
aa2989e
@p-offtermatt @insumity
Update tests/difference/core/quint_model/README.md
53d5bff 
Co-authored-by: insumity <insumity@users.noreply.github.com>
insumity
insumity reviewed Oct 12, 2023
View reviewed changes
tests/difference/core/quint_model/ccv_test.qnt
)
)
).with(
// put an entry into sentVscPacket on the provider that corresponds to the packet we put on the consumer
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
// put an entry into sentVscPacket on the provider that corresponds to the packet we put on the consumer
// put an entry into sentVscPacketsToConsumer on the provider that corresponds to the packet we put on the consumer

I guess the packet put on the consumer is the maturation packet?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

the VSC packet is sent to the consumer, the consumer responds with a VSCMatured packet

insumity
insumity approved these changes Oct 12, 2023
View reviewed changes
Copy link
Contributor

@insumity insumity left a comment •
edited
Loading

Choose a reason for hiding this comment

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

Great work!

It might make sense to ask someone from the Quint team to also review this for Quint style, potential simplifications, etc.

bermuell
bermuell reviewed Oct 13, 2023
View reviewed changes
tests/difference/core/quint_model/ccv.qnt Show resolved Hide resolved
tests/difference/core/quint_model/ccv.qnt Show resolved Hide resolved
tests/difference/core/quint_model/ccv.qnt Outdated Show resolved Hide resolved
tests/difference/core/quint_model/ccv.qnt Show resolved Hide resolved
tests/difference/core/quint_model/ccv.qnt Show resolved Hide resolved
tests/difference/core/quint_model/ccv.qnt Show resolved Hide resolved
tests/difference/core/quint_model/ccv.qnt
val newConsumerStatus = res1._1
val err1 = res1._2
val res2 = newConsumerStatus.stopConsumers(consumersToStop, consumersToTimeout)
val err2 = res2._2
Copy link
Contributor

Choose a reason for hiding this comment

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

no need to run stopConsumers in case of error on startConsumers, right?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Technically not, no, but it doesn't hurt and I think it's slightly more readable like this. (Performance is not really an issue for models, we should likely radically prefer readability unless we have evidence certain things need to be faster). If you think it's currently less readable than the alternative, lmk and I will adjust

Copy link
Contributor

Choose a reason for hiding this comment

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

Not just performance but alos readability. With constructs like this it means to me that other steps have to be executed until you return, but maybe it's just me. Up to you as it's not an issue.

konnov
konnov reviewed Oct 16, 2023
View reviewed changes
Copy link

@konnov konnov left a comment

Choose a reason for hiding this comment

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

This looks nice! Obviously, I did not try to understand the logic of CCV, but only looked at the Quint side of things.

tests/difference/core/quint_model/README.md 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_statemachine.qnt Outdated Show resolved Hide resolved
@p-offtermatt p-offtermatt merged commit 3989e17 into main Oct 19, 2023
14 checks passed
@p-offtermatt p-offtermatt deleted the ph/quint-model-v2 branch October 19, 2023 07:48
MSalopek pushed a commit that referenced this pull request Dec 1, 2023
@p-offtermatt @insumity @MSalopek
Add Quint model of Interchain Security (#1336)
18a1742 
* Start new attempt on Quint model of ICS

* Advance quint model

* Add first finished draft of model

* Add test run to model

* Rename model, add test, use powerset for nondeterminism

* Reintroduce vsc changed tracking variables

* Add text with what expliticly is modelled

* Add bluespec to ccv.qnt

* Add bluespec to expraSpells.qnt

* Add docstring to extraSpells module

* Start rewriting model

* Revert "Start rewriting model"

This reverts commit 1320b95.

* Start rewriting quint model

* Continue seperating logic in Quint model

* Start debugging cryptic error message

* Start adding endAndBeginBlock defs

* Diagnose Quint parser bug

* Fix type in Quint

* Add endBlock actions

* Start adding state machine module

* Save status with crashing effect checker

* Resolve issue by removing undefined field

* Remove add

* Fix init

* Snapshot spec with parser crasher

* Snapshot model

* Start debugging tests

* Finish test for quint model

* Add README and improve folder structure

* Fix import

* Add some invariants

* Refactor Consumer advancement

* Snapshot error

* Make time module upper case

* Add invariants

* Clean up invariants

* Add script to run many invariants

* Update model

* Update model for bug reporting]

* Remove sanity check script

* Fix model and randomly run invariant checks

* Remove trace

* Add model checking to README

* Add bluespec

* Try fixed bluespec

* Fix bluespec definitions

* Update tests/difference/core/quint_model/README.md

Co-authored-by: insumity <insumity@users.noreply.github.com>

* Update tests/difference/core/quint_model/README.md

Co-authored-by: insumity <insumity@users.noreply.github.com>

* Fix minor issues

* Update tests/difference/core/quint_model/README.md

Co-authored-by: insumity <insumity@users.noreply.github.com>

* Update tests/difference/core/quint_model/README.md

Co-authored-by: insumity <insumity@users.noreply.github.com>

* Update tests/difference/core/quint_model/README.md

Co-authored-by: insumity <insumity@users.noreply.github.com>

* Correct verify command by adding \

* Add Inv to ValidatorUpdatesArePropagated

* Update tests/difference/core/quint_model/README.md

Co-authored-by: insumity <insumity@users.noreply.github.com>

* Apply comments

* Rename VSC to Vsc

* Return plain ProtocolState in cases where no error is returned anyways

* Remove unused defs

* Fix indentation

* Rename to isRunningConsumer

* Unify naming for extraSpells

* Remove HasSubsequence

* Run tests before running invariants

* Rename modules to have same name as files

* Adjust module name in README and invariant script

* Fix voting power change behaviour around 0

* Adjust error message in test

* Remove special treatment of 0 voting power

* Rename sentVscPackets to sentVscPacketsToConsumer

* Update tests/difference/core/quint_model/README.md

Co-authored-by: insumity <insumity@users.noreply.github.com>

* Resolve comments

* Adjust comment to fit actual time advancement

* Remove hasError field and make it a function

* Adjust docstring

* Remove unused timedout val

* Update doc

* Rename statemachine to model

* Use ... syntax

* Change Error type to string

---------

Co-authored-by: insumity <insumity@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@konnov konnov konnov left review comments

@insumity insumity insumity approved these changes

@bermuell bermuell bermuell approved these changes

Assignees
No one assigned
Labels
C:Testing Assigned automatically by the PR labeler
Projects
None yet
Milestone
No milestone
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)
4 participants
@p-offtermatt @konnov @insumity @bermuell