chore: Add Quint model of Interchain Security

tests/difference/core/quint_model/README.md

@@ -0,0 +1,37 @@
+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_statemachine.qnt: Contains the state machine layer 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.
+- libararies/*: 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.
+
+### Invariants
+
+The invariants I am checking are in ccv_statemachine.qnt.
+Check a single invariant by running
+`quint run --invariant INVARIANT_NAME ccv_statemachine.qnt --main CCVDefaultStateMachine`,
+or all invariants by running this command:
+
+Invariants are as follows:
+- ValidatorUpdatesArePropagated: When a validator power update is comitted on chain, a packet containing that change in voting power is sent to all running consumers.
+- ValidatorSetHasExistedInv: Every validator set on consumer chains is/was a validator set on the provider.
+- 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.
+- 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.