Add Quint model of Interchain Security (#1336)

* 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 <[email protected]>

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

Co-authored-by: insumity <[email protected]>

* Fix minor issues

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

Co-authored-by: insumity <[email protected]>

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

Co-authored-by: insumity <[email protected]>

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

Co-authored-by: insumity <[email protected]>

* Correct verify command by adding \

* Add Inv to ValidatorUpdatesArePropagated

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

Co-authored-by: insumity <[email protected]>

* 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 <[email protected]>

* 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 <[email protected]>

tests/difference/core/quint_model/README.md

@@ -0,0 +1,72 @@
+This folder contains a Quint model for the core logic of Cross-Chain Validation (CCV).
+
+### File structure
+The files are as follows:
+- ccv.qnt: Contains the type definitions, data structures, functional logic for CCV.
+The core of the protocol.
+- ccv_model.qnt: Contains the stateful part of the model for CCV. Very roughly speaking, this could be seen as "e2e tests".
+Also contains invariants.
+- ccv_test.qnt: Contains unit tests for the functional layer of CCV.
+- libraries/*: Libraries that don't belong to CCV, but are used by it.
+
+### Model details
+
+To see the data structures used in the model, see the `ProtocolState` type in ccv.qnt.
+
+The "public" endpoints of the model are those functions that take as an input the protocol state, and return a `Result`.
+Other functions are for utility.
+
+The parameters of the protocol are defined as consts in [ccv.qnt](ccv.qnt).
+
+### Tests
+
+To run unit tests, run 
+```
+quint test ccv_test.qnt
+```
+and 
+```
+quint test ccv_model.qnt
+```
+
+### Invariants
+
+The invariants to check are in [ccv_model.qnt](ccv_model.qnt).
+Check a single invariant by running
+`quint run --invariant INVARIANT_NAME ccv_model.qnt`,
+or all invariants one after another with the help of the script `run_invariants.sh`.
+Each invariant takes about a minute to run.
+
+Invariants are as follows:
+- [X] ValidatorUpdatesArePropagatedInv: When a validator power update is comitted on chain, a packet containing that change in voting power is sent to all running consumers.
+- [X] ValidatorSetHasExistedInv: Every validator set on consumer chains is/was a validator set on the provider.
+- [X] SameVscPacketsInv: Ensure that consumer chains receive the same VscPackets in the same order.
+Because of nuances with starting/stopping consumers, this invariant is not as simple as it sounds. In detail:
+For consumer chains c1, c2, if both c1 and c2 received a packet p1 sent at t1 and a packet p2 sent at t2,
+then both have received ALL packets that were sent between t1 and t2 in the same order.
+- [X] MatureOnTimeInv: For every ValidatorSetChangePacket received by a consumer chain at 
+time t, a MaturedVscPacket is sent back to the provider in the first block 
+with a timestamp >= t + UnbondingPeriod on that consumer.
+- [X] EventuallyMatureOnProviderInv: If we send a VscPacket, this is eventually responded to by all consumers
+that were running at the time the packet was sent (and are still running).
+
+Invariants can also be model-checked by Apalache, using this command:
+```
+quint verify --invariant ValidatorUpdatesArePropagatedInv,ValidatorSetHasExistedInv,SameVscPacketsInv,MatureOnTimeInv,EventuallyMatureOnProviderInv \
+ ccv_model.qnt
+```
+
+### Sanity Checks
+
+Sanity checks verify that certain patterns of behaviour can appear in the model.
+In detail, they are invariant checks that we expect to fail.
+They usually negate the appearance of some behaviour, i.e. `not(DesirableBehaviour)`.
+Then, a counterexample for this is an example trace exhibiting the behaviour.
+
+They are run like invariant checks, i.e. `quint run --invariant SANITY_CHECK_NAME ccv_model.qnt`.
+The available sanity checks are:
+- CanRunConsumer
+- CanStopConsumer
+- CanTimeoutConsumer
+- CanSendVscPackets
+- CanSendVscMaturedPackets