Mimc
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.
