This is an experimental formalisation of the network model introduced in my thesis.
This project is a learning ground, questionable code lies ahead.
- listidx.v adds a
indexOf ltype that let us easily work with indexes of listl - sequences.v defines the types of coinductive lists, or equivalently, streams thay may be finite. It also defines the
indexOf stype for a sequences. - network.v is the main files, which will be broken up in the future. Currently implemented:
- Types for protocols, modules
- associated events, executions as sequences of events, nodes states and IO during execution
- admissibility predicates for : modules admissibilty predicates, execution of the protocol by honest nodes, corruption structures
- satisfication of module specification by a protocol
- the 'asynchronous network' module
- reductions between modules