Midgrad Unsorted Key Linked Lists.

The formalization follows closely the Midgard specification, i.e. lists are implemented using a token based approach. We provided our modelization of tokens in FMMidgard.Cardano.DataStructures.Tokens.ListImpl implemented using lists. While in Cardano, one just presents a token (i.e. presenting the right credentials to spend it), here one just presents a valid token Id of type TId.

Nodes composing a list structure comes from context, we do not have direct access to it when modifying it. In other words, to traverse or iterate through the elements of a linked list, we need to provide them explicitly.

We are still able to prove properties over the steps taken in the creation and manipulation of lists. But to go through its elements, we need to build the required context. We explore traversals in FMMidgard.DataStructures.List.Paths.