Inria Prosecco Admin (Karthik)
Inria Prosecco Admin (Karthik)
Is this based on Guillaume’s work? > On 4 Feb 2020, at 10:06, Benjamin Beurdouche wrote: > > Please do not touch this ! I'll merge it in _dev myself......
I am curious: is there a public RFC or other standard for merkle trees that the code is trying to meet? > On 30 Apr 2020, at 12:01, Christoph M....
This is the only public spec I see: https://tools.ietf.org/html/rfc6962#section-2.1 I don’t expect the F* code follows this though. > On 6 May 2020, at 11:03, Christoph M. Wintersteiger wrote: >...
There is perhaps a more general pattern to be explored here. I think we are describing datatypes t that have a “hasSize t” attribute. Something like: type sizetype = a:Type{hasSize...
Got the type of create wrong. Here’s another try type sizetype = a:Type{hasSize a} val sizeOf: sizetype -> Tot nat val create: a:sizetype -> b:buffer UInt8.t -> ST (buffer a)...
We should generate for all arrays/buffers etc: __attribute__ ((aligned (16))) b For all records/structs, we should generate "force_inline" functions by default, e.g.: static force_inline inline uint64_t *Hacl_Impl_Poly1305_64___proj__MkState__item__r(Hacl_Impl_Poly1305_64_poly1305_state projectee) { Hacl_Impl_Poly1305_64_poly1305_state...
A related ask is a macro for bounded sequences, of the form: ```bounded_sequence!(, , , )``` This is similar to the `array` macro but instead of declaring a type for...
warning: valecrypt does not seem to like 4.13.3 On Thu, Dec 26, 2024, 16:23 Jonathan Protzenko ***@***.***> wrote: > @mtzguido can you remind me what's up with > using the...