The Poseidon hash function.
Poseidon is a framework for defining cryptographic hash functions that are designed to operate on elements of a large prime field in a way that is efficient in a zero-knowledge circuit.
Poseidon is described on this web site, which links to the research paper that defines the hash function; that paper refers to the HADES paper.
In this library we formalize the main parameterized Poseidon algorithm and formalize the parameters that instantiate the algorithm into a specific hash function.
Then we model a number of specific instantiations of Poseidon that are in use in the wild.
At this time we do not model the security checks that should be done on any new instantiation before using it in production.