Cryptographic Hash Functions

Stream: Is there code for X?

[Leo Sin]

Hi everyone!

Are there libraries that provide cryptographic hash functions (e.g., MD5, SHA1)? Seems those are not in stdlib, batteries, nor mathlib4...

Or should I try to bring those in from something like OpenSSL via FFI?

[Kim Morrison]

Not that I am aware of.

An OpenSSL wrapper library would be very useful for many people! Native implementations would be great to have too, but for quite different purposes.

[Henrik Böving]

Note that OpenSSL is notorioulsy difficult to use correctly from the C API, if you plan to use this for anything serious you have to be really careful.

[Kim Morrison]

As a Saturday morning exercise in using Claude Code (fun, mostly impressive), we now have an md5 library written in Lean.

It provides String.md5 and ByteArray.md5, as well as command line interfaces lake exe md5 and lake exe md5sum reproducing all the options those standard tools provide.

[Kim Morrison]

(Oh, and a thorough test suite that does conformance testing against the command line tools. Claude is inexhaustible.)

[Kim Morrison]

It's 10x slower than my system binaries, but if anyone wants to improve on that, the test suite is there to catch you if you fall. :-)

[Aaron Liu]

How do you time it?

[Kim Morrison]

kim@carica lean-md5 % lake exe md5 -t
MD5 time trial. Digesting 10000 10000-byte blocks ... done
Digest = 0d0c9c4db6953fee9e03f528cafd7d3e
Time = 28.699000 seconds
Speed = 3484441.966619 bytes/second
kim@carica lean-md5 % md5 -t
MD5 time trial. Digesting 100000 10000-byte blocks ... done
Digest = 766a2bb5d24bddae466c572bcabca3ee
Time = 1.740423 seconds
Speed = 574572992.000000 bytes/second

[Leo Sin]

Kim Morrison said:

As a Saturday morning exercise in using Claude Code (fun, mostly impressive), we now have an md5 library written in Lean.

It provides String.md5 and ByteArray.md5, as well as command line interfaces lake exe md5 and lake exe md5sum reproducing all the options those standard tools provide.

Thanks for creating library, really appreciate it!

Btw just wondering are there any tips/prescriptions/best practices in terms of managing lean-toolchain versions to keep forward compatibility for third-party library maintainers?
Because some libraries with old toolchain version seems do not play well with new versions of batteries and/or mathlib...

[Kim Morrison]

The library has been renamed to lean-crypto-hash and now implements (and tests) the SHA1 and SHA2 algorithms. Claude Code is fun.

[Joachim Breitner]

(important discussion, maybe someone can move the last three messages to a new thread in #general or #lean4?)

[Kim Morrison]

Claude also had no problem with SHA3, so that's in the library too.