Just to clarify, Bose et al.'s paper was incorrect due to an incorrect definition of Stirling numbers of the second kind (some of their expressions used the wro

Just to clarify, Bose et al.'s paper was incorrect due to an incorrect definition of Stirling numbers of the second kind (some of their expressions used the wrong exponents). In our certified work, in light of this error, we ended up deriving the expression for Stirling numbers of the second kind from first principles[1], eliding it as a source of errors. As such, the main definition that needs to be human-verified in our work is the actual implementation of the Bloomfilter[2], which is fairly simple and easy to check as being correct. [1] https://github.com/certichain/ceramist/blob/fd5e522f2c381f7dbd5b8e38b48041dfd4bd261a/Utils/stirling.v#L341 https://github.com/certichain/ceramist/blob/fd5e522f2c381f7d... [2] https://github.com/certichain/ceramist/blob/fd5e522f2c381f7dbd5b8e38b48041dfd4bd261a/Structures/BloomFilter/BloomFilter_Definitions.v#L98 https://github.com/certichain/ceramist/blob/fd5e522f2c381f7d...