SHA3 -- Keccack256 Hash functions.

Stream: Is there code for X?

[Martin Ceresa]

Hi everyone! I am formalizing/implementing some of our ideas[0] and ideally we would want to have some hashing functions á la Etherum. Is there any code implementing Keccack256 hash functions? No proofs, just their implementations would be enough.

In general, I am formalizing some theorems we have unsing Merkle Tree membership queries. That's almost done, but I want to write an interactive demo. I built my library ignoring certain aspects hehe, but now I want to go as real (again, not at the proof level) as I can :muscle: .

[0] : My name is Martin Ceresa and I am working at IMDEA Software Institute under the supervision of Cesar Sanchez :muscle: .

[Johan Commelin]

I'm not aware of a Keccak implementation in Lean

[Martin Ceresa]

Thanks! I have some IO interactions, so I will push this outside of Lean. I may implement it some day.