cryptography

Stream: new members

[cmlsharp]

Hello everyone, I’m a PhD student (hopefully not a student for much longer) in cryptography. I’ve recently become interested in formal verification/type theory etc which brought me here.

I’m generally interested in using Lean to build dependent-typed DSLs for cryptographic applications (such as SNARKs for example). I’m interested in lean both as a theorem prover but also potentially as a somewhat more general purpose programming language for cryptographic implementations. As such, I’m very interested in learning more about writing performant code in Lean. Glad to meet you all!

[Wrenna Robson]

Hey! Great to see more cryptographers interested in Lean.

[Wrenna Robson]

Are you aware of https://www.hacs-workshop.org?

[Tanner Duve]

if you haven’t seen it, there’s ArkLib, clean, zkLean

[cmlsharp]

@Wrenna Robson I am, thank you! I will be at RWC this year, so I did apply to attend this workshop

[Wrenna Robson]

I'll see you there

[cmlsharp]

Tanner Duve said:

if you haven’t seen it, there’s ArkLib, clean, zkLean

I was aware of Galois' zk dsl, but I was not aware of 'clean', that looks really interesting, thank you!

[Yoichi Hirai]

I've been contributing to the clean project for a while. There's also cryptography involving reduction proofs. I formalized a recent FRI round-by-round soundness proof (by a colleague and his coauthors) with the help of Harmonic's Aristotle: https://blog.zksecurity.xyz/posts/simple-rbr-fri/

[cmlsharp]

Wrenna Robson said:

I'll see you there

Alas, they did not accept my self nomination, but perhaps I'll see you at RWC itself!