A formal specification of the MiMC hash function as used by Semaphore.

The MIMC library includes a formal specification of the MiMC hash function, as used by Semaphore.

MiMC is defined in the paper MiMC: Efficient Encryption and Cryptographic Hashing with Minimal Multiplicative Complexity.

The following `include-book` command may be helpful to bring in the library:

(include-book "kestrel/crypto/mimc/mimcsponge" :dir :system)

The interface functions are:

`(mimcsponge m n inputs field-order constants exponent nrounds)`

Absorbs the`m`field element inputs contained in the list`inputs`and produces`n`field element outputs. Each input and output is a field element in the finite field of size`field-order`. The round constants in`constants`are also field elements.`exponent`is the power to which intermediate values are raised.`nrounds`is the number of rounds, which must match the length of`constants`.`(mimcsponge-semaphore m n inputs)`

Calls`mimcsponge`with the field order`(zksemaphore::baby-jubjub-prime)`(which is the same as`(primes::bn-254-group-prime)`), the constants in`(mimc-feistel-220-constants)`, the exponent`5`, and the number of rounds`220`.

See the comments in the source file for more information on the MiMC specification including the variations chosen.

The library also includes some concrete tests.