This is a formalisation of the swap-or-not shuffling algorithm as used in Ethereum 2.0.
AbstractSwapOrNotShuffle.thy: definition of swap-or-not shuffle in terms of Abelian groups. We prove that under some mild assumptions about the input list, swap-or-not shuffle yields a permutation.
The proofs are compatible with Isabelle 2019
The next step will be to instantiate the abstract shuffle with the key and round functions used in Eth2, which are based on hashing and modulo arithmetic on integers.
Once that is complete, I hope to prove equivalence between the optimised implementation of the algorithm that we use in Lighthouse, and the one-at-a-time shuffling defined by the Ethereum 2 specification.