This is my attempt at formalizing the foundations of the LOCAL model using Lean. The definitions and theorems are based on the book of Distributed Algorithms course here at Aalto University.
- Port-numbered network (
PNNetwork
) - Covering maps (
CoveringMap
) - PN algorithms (
PNAlgorithm
) - PN algorithms cannot distinguish covering maps (
PNAlgorithm.covering_map_indistinguishable
) - Define LOCAL model