Extracting hacspec-compatible code from larger Rust projects about hacspec HOT 10 OPEN

@denismerigoux is working on a concrete equivalence proof in F*, so he may have insights on how to structure this.

from hacspec.

Pie-in-the-sky idea:

Annotate functions with the information needed to generate an equivalence proof with some reference implementation contained within the same repo.

#[hacspec(prove_equivalence_to = "specs/SBox.cry")]
fn sub_bytes(...) {
   [...]
}

from hacspec.

I really like the idea! Both actually, the first one is a little more realistic at this point though 😉
One question would be about the semantics of a #[hacspec] attribute. Running the typechecker only on annotated functions is probably the easiest and is definitely doable. But it's also a little limited in its usefulness. Any generated code would probably need quite a bit of work to make it useful as verification target.
I guess this is where your second idea comes in.
But the basic attribute might already be useful to people.

It would also be nice if we could have better integration.
Taking your example, I could imagine having a full AES implementation in hacspec with the same SBox function. It would be nice if we could pick a function like the SBox from there to use in the RustCrypto code without having to keep two copies of it.

from hacspec.

To get started on something like #55, it might be easiest to do as you suggest and extract the hacspec-compatible portions into their own modules and potentially even upstream those modules to this repo. I'll leave a note about it on that issue.

from hacspec.

About the pie-in-the-sky idea. For concreteness, let's consider equivalence in, say, easycrypt.
Are you proposing to have a link to an EC file containing such a proof?
I don't think we should expect such proofs to be automatically generated.

from hacspec.

I was mostly spitballing, but yeah, that's the general idea: have a reference implementation which is expected to be functionally equivalent checked in somewhere in the same directory structure, and some sort of runner tool which looks for these attributes and runs some sort of prover.

from hacspec.

Thanks Tony and Bas for the discussion. You're right, this is indeed we we're doing in F* with #54. The complete Hacspec crate is translated to an F* file, then we have another F* file in which we write the equivalence proof with the existing HACL* spec.

However, I'm skeptical about the #[hacspec] tag. Indeed, one function annotated using the #[hacspec] tag is likely going to use multiple type definitions and functions from this crate and other crates, which we also need to translate to F* if we want to make sense of the thing. Hence, the Hacspec/non-Hacspec separation involves usually more Hacspec than what you think and annotating everything that needs to be translated with #[hacspec] is cumbersome.

Then there are engineering difficulties in the Rust->Hacspec->F* compiler to keep track of what's being annotated, do dependency analysis, match Rust's crate semantics with F*/EC module semantics, being able to handle imports from other crates, etc. Those engineering difficulties are for instance the reason why currently Hacspec crates can only be single-file.

To come back to your AES example, currently you can define multiple SBoxes inside a Hacspec "sbox" crate, and then use any of those Sboxes with use in your regular RustCrypto AES crate.

from hacspec.

Assuming hacspec crates adopt the multi-file rust module system, maybe one needs an alternative top level build target, meaning hacspec.rs replaces lib.rs and then uses modules being verified.

As an aside, there are many applications like merkle trees for which hash functions naturally have a purely functional interface, but increasingly there exist applications for which only a mutable transcript interface like merlin makes more sense. As a rule, one implements transcript interfaces via extension traits, so they could be instantiated with a functional implementation underneath modulo rust-lang/rfcs#1403 or perhaps mutable borrows already make the interface suitable. Almost everything doing transcripts winds up in IPPs, FFTs, etc. fairly quickly, so maybe not verification targets this decade, but a transcript model makes even simple signatures less error prone.

from hacspec.

@burdges could elaborate on how this differs from persistent data structures? The concepts seems similar.

from hacspec.

I'd think transcripts are easier than arbitrary persistent data, but rust code should always access them via mutable borrows. I've not yet looked at how F* handles persistent data, but likely a non-issue. If an issue appears then indicates the translation does not interpret borrows correctly.

from hacspec.