Rewrite the difftest model in Quint

[p-offtermatt]

The current difftest model is hard to read, since it has quite a bit of infrastructure written in typescript.
It could improve the model if it was written in a more high-level language,
which should allow developers to interact with it more easily. We choose Quint for this high level language,
since it has support for model-checking and integration with MBT tooling on the way.

Closing Criterion:
The difftest model has been rewritten in Quint.

[p-offtermatt]

I will marked this blocked for now, see informalsystems/quint#1096.

[p-offtermatt]

I was told a workaround for this, so continuing work on this for now

[shaspitz]

Chiming in here, this issue is important from my perspective as I'll have to comment out diff tests to merge #1024.

Note the linked PR fails diff tests, even when they're just used as regression tests, since throttling v2 necessarily changes the consumer's behavior w.r.t how slash and vsc matured packets are sent to the provider.

[p-offtermatt]

After a spike, see https://github.com/cosmos/interchain-security/tree/ph/1177-rewrite-the-difftest-model-in-quint, it seems relatively hard to write the entire difftest model in Quint. For now, I think it looks much more reasonable to try and write a more high-level model first.

Thus, the plan for now is to take another spike to try to write a high level model that is maximally abstract, while being able to express interesting invariants from https://github.com/cosmos/ibc/tree/main/spec/app/ics-028-cross-chain-validation.
Then we can compare this to the TLA+ model for the same spec and see whether we get any benefit,
and in the next step actually connect the abstract model as a trace generator.