Use of return values in synthesized Bedrock2 functions

[RasmusHoldsbjergCSAU]

I noticed that the Bedrock2 synthesis pipeline generates Bedrock2 functions that do not make use of return values, a functionality that is supported by Bedrock2 as far as I can tell.

Is there a good reason for this, or would it be straightforward to modify the pipeline (as discussed in #944) to have the synthesized functions use return values as opposed to accepting an "out" pointer as one of its arguments? @jadephilipoom

This is of interest to me, as I am trying to have Bedrock2 functions printed to Rust, similarly to how C functions are printed. I have been fighting the strict borrow checker of safe Rust, and believe that much of this can be mediated by having functions use return values instead.

[JasonGross]

I believe the primary issue is that we want the bedrock2 C code to have the same signature as the non-bedrock2 C code, so that it can be used directly in BoringSSL. I've not yet adapted the stringification code to handle return values, but it's on my to-do list. In the meantime, I'm happy to have an option controlling whether or not bedrock2 returns things or not. You may in fact find the code to have bedrock2 make use of returns in git history, since I believe it originally returned values.

[jadephilipoom]

I'm not sure it will be so straightforward; if I recall correctly, bedrock2 does not support returning arrays or multiple values, so you'd have to return a pointer. Introducing memory allocation in which to store the result would likely be significant work. However, you could just modify the code to continue taking the pointer as an argument and then return the same pointer, if that would make the borrow checker happy.

[RasmusHoldsbjergCSAU]

There is an example of a bedrock2 function with multiple return values here: https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/bedrock2Examples/MultipleReturnValues.v

Do you mean that it is not possible to prove properties of such a function?

Also I'm afraid that returning the argument pointer will not help much; since values are stored into the address of this pointer, a mutable reference is needed. But since typing information is not in bedrock2, it would be better if all arguments were passed as immutable references.

[jadephilipoom]

Do you mean that it is not possible to prove properties of such a function?

I just misremembered; it was a couple of years ago :) After a closer look, it should be possible to adapt the synthesis engine so that it returns a tuple with each part of the field element, which the caller can store as they please. I'm not sure it will be easy, but it should be doable.

This is the definition that creates bedrock2 functions from fiat-crypto's IR: https://github.com/mit-plv/fiat-crypto/blob/f1951b3d80f1d0e402a832682875667ae52e8028/src/Bedrock/Field/Translation/Func.v#L55

You will be able to get away with not modifying anything in Cmd.v or Expr.v, the lower-level layers of the compiler; they operate by treating lists as collections local variables, so Func.v (and Flatten.v) has all the code that deals with storing those return-value local variables to lists. You could either make an alternate version of Func.v that has no argument pointers and uses local return values exclusively, or just add support for local return values in addition to argument pointers (I'd recommend the latter). Either way, you'd then use an option at synthesis time to decide which representation to use. If you'd like, we can schedule a call and I can talk you through it in more detail.

[RasmusHoldsbjergCSAU]

Sorry for the late reply; a meeting to talk about the details sounds like a good idea. On a related note, I have been working on having the new Bedrock2 synthesis pipeline generate word-by-word Montgomery field operations, we could also discuss the approach I have taken there and how to integrate it into the pipeline.

wrt. return values; it is not necessary that a tuple containing parts of the field element is returned. A pointer to an array contining these parts should be sufficient; I imagine that this is easier to achieve?

The difference between using return values and not is more subtle in this case, but having a pointer returned would remove the need for arguments to be mutably borrowed when translating the Bedrock2 functions to safe Rust.

I suggest meeting on Sunday, Monday or Tuesday if any of those days work for you?

[jadephilipoom]

An array is not necessarily easier to achieve; that would involve introducing stack allocation to the translation pipeline, which could be tricky. Then again, maybe not; when the pipeline was first written stack allocation didn't really exist in bedrock2, but now it does, so it might be worth a try.

Unfortunately I'm on vacation for the next week -- does sometime the week of September 27 work for you? Alternatively I could do tomorrow/Friday.

[RasmusHoldsbjergCSAU]

I see the issue. Friday works for me, you can just pick a time : )

[jadephilipoom]

Sounds good. Let's arrange the rest over email.

[RasmusHoldsbjergCSAU]

Yes, I cannot find your email address, but you can write me on [email protected]

[jadephilipoom]

Hmm, I did email that address -- if you don't see my email, you can find my address on the HACS attendee list.