Spike: Prototype Partial Set Security in Quint

[p-offtermatt]

Problem

We want to get familiar with doing spike implementations in Quint, in particular we want to assess whether it is even
viable. Therefore, we should model partial set security in Quint first, and pay attention to whether this is useful during later implementation stages.

Closing criteria

Partial set security has been added to the Quint model of CCV.

Problem details

These are the steps to spiking partial set security in the CCV Quint model:

• Add data structures that are necessary for partial set security to ProviderState/ConsumerState
• Implement Partial Set Security API. Some incomplete suggestions:
  • Add new consumer chain as top-n
  • Add new consumer chain permissionlessly
  • Adjust top-n percentage
  • Validator opts in to a chain (either with inclusive top-n or into a permissionless consumer chain)
  • Validator opts out of a chain
  • ...more?
• Adjust logic in existing model. Some incomplete suggestions:
  • Different VSCPackets should be sent to different chains, depending on opted-in validators
  • When blocks end and the validator set changes, who is top-n forced to what chain needs to change

TODO: this might become an epic and need to be split, but for now I think it's probably not big enough for an epic