Cryptography

Stream: general

[Bas Spitters]

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]

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]

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

[Bas Spitters]

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

[Mario Carneiro]

@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]

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]

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]

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]

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

[Joe Hendrix]

@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]

@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]

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]

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]

@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]

@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]

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]

@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]

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]

@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.