Path Module

Module dedicated to defining paths over Midgard lists. The initial idea was to verify that lists are always connected, i.e. there is a path from root to all nodes.

The main goal is to avoid dandling nodes in lists, or more general, to avoid ways of spliting the list.

Midgard employs lists to keep the state and the operator directories. Dandling nodes are nodes that cannot be removed, and thus, malicious operators can force honest to become dandling nodes, locking their funds forever.

Instead of proving all the required properties, we opted to use the property-based testing library (Plausible)[https://github.com/leanprover-community/plausible]. Fully proving all these properties would take a lot of time and effort, and we will not get a lot of useful results since Midgard is a moving target. See ./Tests/Lists.lean.