test: MBT for Part Streaming

[hvanz]

Part Streaming is the protocol utilised for block propagation in the Starknet app. When sending a block proposal to a set of peers, a node partitions the block into multiple parts and send each part to the peers in StreamMessages, which may arrive out of order. Then the peers must re-assemble the received parts into a block.

This is the implementation. And this is the Quint spec.

The goal is to write an MBT driver and tests for Part Streaming.

Tasks:

• Update and expand the documentation of the code and the spec, if needed.
• Extend the spec with new tests and invariants, if needed.
• Write in Rust the types and data structures that will be used to map the spec's state variables (example of State struct for consensus-core module)
• Write implementation of ItfRunner for ITF traces generated from the spec (for example, ConsensusRunner)
• Write MBT test, which generates ITF traces from the Quint spec and runs the traces as Rust tests (example for consensus-core)
• Integrate the new MBT tests in CI