Rasmus Holdsbjerg-Larsen

Thanks for the response : ) If it makes things easier, we can set up a meeting to discuss how to best go about merging this when you have time;...

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

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

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

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

Thanks! Adding the (* ?R) frame to the postcondition in the function specification solved the problem. I am not entirely sure about the purpose of this R variable though. As...

@JasonGross @andres-erbsen @jadephilipoom @bshvass?

Yes, the SOS method does indeed refer to the same method of that paper; I am not sure what "Comba" refers to here (perhaps @dfaranha can clarify?). With respect to...

Thanks for the response! The split_distr lemma was indeed written to help with stack allocation; I had some problems getting stragihtline_stackalloc to work, but now, having experimented a bit more...

New notation looks nice : ) The functions generated by Fiat-Crypto seem to work regardless of aliasing; although they are a lot more complicated. I have tried doing something similar...