Add a network model to allow for reasoning about global protocols in the formal specification

[WhatisRT]

Most interesting properties of Leios are global, meaning that they are of the form all honest nodes eventually .... To even express statements like this, we need a notion of network, nodes, honesty, etc. while we're currently only modelling single nodes.

• Add a network layer that has honest and byzantine nodes
• Allow for tracking meta information in the network state
• If time permits, prove some basic properties

Acceptance criteria

The code type checks in CI

[will-break-it]

Can you please add more to the acceptance criteria as it's not clear what is completed if types are compiling. That's not really a deliverable. Thank you.

[WhatisRT]

This is just how expressing and reasoning properties works in Agda and other proof assistants. See also #52 where we had the same criteria, except that we don't care about the network being executable because that's not particularly useful for any kind of testing.

So in this case, type correct code is the actual deliverable. We could say something like 'the proofs are checked for correctness by CI', but that's exactly the same thing worded differently. If you think this is helpful I could rephrase it or include an explanation.