Zulip Chat Archive

Stream: general

Topic: Cryptography


Bas Spitters (Dec 23 2021 at 11:17):

We're having a bit of fun in Coq on a pipeline from the hacspec specification language to optimized verified implementations in C, rust, ... using the bedrock/fiat-cryptography libraries in Coq.
https://cs.au.dk/~spitters/CoqPL22.pdf

hacspec provides backends for F*,Easycrypt and Coq. Lean is missing...

Mac (Dec 23 2021 at 11:43):

Considering that Lean 4 has its own already rather optimized codegen (that can in some cases be faster and safer than Rust) this seems like an odd project for Lean.. Maybe it might be reasonable for Lean 3, but it seems like a bit of a time sink. Especially since there is the potentially more interesting work of just translating the specific language directly to Lean 4 (and seeing how optimized and verified it could be made with just that).

Mario Carneiro (Dec 23 2021 at 11:59):

Isn't that what Bas is suggesting? A translation from hacspec language to lean [3/4]

Bas Spitters (Dec 23 2021 at 15:14):

@Mario Carneiro Indeed!
@Mac it would be interesting to see whether lean codegen is competitive with fiat-cryptography for cryptographic primitives.

Mario Carneiro (Dec 23 2021 at 15:19):

@Bas Spitters Is there a way to get hacspec in an easily parsed format (say, json or sexprs), or one with a simple (documented!) spec?

Bas Spitters (Dec 23 2021 at 15:38):

The Coq backend was added in this PR, something similar should be
possible for lean, as the coq backend was an adaptation of the F*
backend.
https://github.com/hacspec/hacspec/pull/144

Mario Carneiro (Dec 23 2021 at 15:53):

At least with lean 4, it is much easier and more reliable to write an importer than an exporter that produces lean text directly. (I've done this before with lean 3 and there are a lot of drawbacks to producing lean source text without lean guiding the process.) So it would be best to have the hacspec compiler just spit out an AST in some format (preferably json since we already have a good json parsing framework) and then import from there.

Mario Carneiro (Dec 23 2021 at 15:55):

This is also how the current lean 3 -> lean 4 source-to-source translator works: lean 3 runs and produces AST in a JSON format, and a lean 4 program reads the json, translates to lean 4 data structures and pretty prints it as type correct lean 4 text.

Mario Carneiro (Dec 23 2021 at 16:04):

Ah, it looks like there is already a json exporter. You should really mention that on the list of backends

Joe Hendrix (Dec 23 2021 at 16:51):

@Mario Carneiro Do you have a recommendation for a good entry point on learning how to generate Lean source within Lean? The haspec translation seems like it could be an interesting project when the underlying Lean 4 libraries for expressive cryptographic primitive operations are more mature.

Mario Carneiro (Dec 23 2021 at 21:15):

@Joe Hendrix mathport seems like a good example to follow. The idea is pretty simple: translate Json to HacspecAST to Syntax, then use parenthesize and format on the resulting syntax and print the format.

Joe Hendrix (Dec 23 2021 at 22:13):

Yes, I think the interesting bits would more be using the result for something interesting such as verifying properties or using verified simplification rules to optimize the specification. Once there is more sophisticated automation, I may revisit this unless somebody else tries working on it.

Mario Carneiro (Dec 23 2021 at 22:17):

An alternative translation which would make sense for lean 4 is to go from HacspecAST to Syntax representing elements of a hacspec syntax category, so that the final result is written in a hacspec internal DSL. That form might be better for proving properties than a shallow embedding

Bas Spitters (Aug 13 2022 at 13:55):

@Joe Hendrix Nice work here: https://github.com/joehendrix/lean-crypto
I see you're looking for specifications. One for AES is available in hacspec already

Joe Hendrix (Aug 13 2022 at 16:52):

@Bas Spitters Thanks for reminding me about this thread. I was thinking about making an AES spec from Cryptol sources, but it'd probably be interesting to at least experiment with the HASpec to JSON to Lean Syntax route.

I have a moderately large collection of bit vector and polymorphic vector operations for the Classic Mceliece spec, and I think that they should probably be polished and pulled into their own library (perhaps Mathlib already has many of these also).

Bas Spitters (Aug 13 2022 at 17:34):

There's some interest in connecting hacspec to cryptol.
So, this may be an excuse for another push...
https://hacspec.zulipchat.com/#narrow/stream/271596-crux-mir/topic/Running.20Crux-mir

Wrenna Robson (Aug 24 2022 at 01:23):

@Joe Hendrix our bitvector stuff in mathlib exists but is imo limited in some ways. I would be interested in helping with a project to port your lemmas.

Bas Spitters (Apr 12 2023 at 09:08):

There was some further discussion on a lean backend for hacspec at HACS, the tool is gaining quite a bit of traction.
@Joe Hendrix Regarding AES, we've connected the hacspec spec with the jasmin efficient implementation going via SSProve.
https://eprint.iacr.org/2023/185

Joe Hendrix (Apr 12 2023 at 20:09):

@Bas Spitters Thank you for the pointer. I've needed to focus on other things for a while (too long), but would love to resume looking at crypto in Lean in the next month.


Last updated: Dec 20 2023 at 11:08 UTC