Compile buffers and structs which lengths are known to more precise types ?

[jkzinzindohoue]

What would be a good way to make it so that I can write a type type state = b:buffer uint32{length b = 16} and that gets compile to typedef uint32[16] state ?

The usecase is the following: I have an algorithm that relies on a state with an "init", an "update" and a "finish" function. To run the algorithm I would call init the initialize the state, and then update a certain number of times, and then finish to cleanup to the state and return some value. This is very typical in cryptography.

In F* what I would do it that init would be in the StackInline effect, so that one calling the function gets in return a properly formatted, pre-filled state.
However at the C level this function will have been inline and thus will not be available. Which forces me to decouple the allocation of the state from its initialization (because it is stack-based so no mallocs).
Unfortunately I can't do state st; init(st, key) because state will just have been compiled to a pointer and not an array with a statically defined length. If the state is a complicated structure, this is even more painful because the C user need to allocated each element on the stack and then fill the struct that only contains pointers.

Is there a way to easily solve that ? I still want to complain about the lack of a mechanism to translate more information from the Core AST to the extracted AST (like the length of the buffers).

[prosecco]

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 a} val sizeOf: sizetype -> Tot nat val create: a:sizetype -> b:buffer UInt8.t {length b = sizeOf a} -> ST a In the generated C code, we automatically generate sizeOf and create for a variety of known datatypes, and calling C code can allocate a local buffer and “cast” it to a using create. What do you think? -Karthik

…

On 12 Feb 2017, at 13:11, Jean-Karim Zinzindohoué ***@***.***> wrote: What would be a good way to make it so that I can write a type type state = b:buffer uint32{length b = 16} and that gets compile to typedef uint32[16] state ? The usecase is the following: I have an algorithm that relies on a state with an "init", an "update" and a "finish" function. To run the algorithm I would call init the initialize the state, and then update a certain number of times, and then finish to cleanup to the state and return some value. This is very typical in cryptography. In F* what I would do it that init would be in the StackInline effect, so that one calling the function gets in return a properly formatted, pre-filled state. However at the C level this function will have been inline and thus will not be available. Which forces me to decouple the allocation of the state from its initialization (because it is stack-based so no mallocs). Unfortunately I can't do state st; init(st, key) because state will just have been compiled to a pointer and not an array with a statically defined length. If the state is a complicated structure, this is even more painful because the C user need to allocated each element on the stack and then fill the struct that only contains pointers. Is there a way to easily solve that ? I still want to complain about the lack of a mechanism to translate more information from the Core AST to the extracted AST (like the length of the buffers). — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#33>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AEYAnqXSOc85cHoQgGotpbbru60dpqvYks5rbvcBgaJpZM4L-eDo>.

[prosecco]

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) (requires (fun h -> live h0 b /\ length b = sizeOf a)) (ensures (fun h0 r h1 -> live h1 r /\ length r = 1 /\ modifies_1 r h0 h1)) In other words, create consumes b (does not guarantee that b is live afterwards) and promises that r is the only reference that has been modified in the heap. Whether we can implement this soundly remains open. One can aim for even more generality by going up to canSerialize: -- type serializable = a:Type{canSerialize a} val repr: a:serializable -> d:a -> GTot (seq UInt8.t) val serialize: a:serializable -> d:a -> b:buffer UInt8.t -> ST unit (requires (fun h -> live h0 b /\ length b = repr a d)) (ensures (fun h0 r h1 -> live h1 b /\ modifies_1 b h0 h1 /\ as_seq h1 b == repr a d)) val parse: … -- I am guessing serialization may already have been discussed before for Kremlin? We certainly thought about it a bunch for TLS message parsing. But this is probably a digression. I am still pushing the “sizeof” style for JK’s problem?

…

In the generated C code, we automatically generate sizeOf and create for a variety of known datatypes, and calling C code can allocate a local buffer and “cast” it to a using create. What do you think? -Karthik > On 12 Feb 2017, at 13:11, Jean-Karim Zinzindohoué ***@***.*** ***@***.***>> wrote: > > What would be a good way to make it so that I can write a type type state = b:buffer uint32{length b = 16} and that gets compile to typedef uint32[16] state ? > > The usecase is the following: I have an algorithm that relies on a state with an "init", an "update" and a "finish" function. To run the algorithm I would call init the initialize the state, and then update a certain number of times, and then finish to cleanup to the state and return some value. This is very typical in cryptography. > > In F* what I would do it that init would be in the StackInline effect, so that one calling the function gets in return a properly formatted, pre-filled state. > However at the C level this function will have been inline and thus will not be available. Which forces me to decouple the allocation of the state from its initialization (because it is stack-based so no mallocs). > Unfortunately I can't do state st; init(st, key) because state will just have been compiled to a pointer and not an array with a statically defined length. If the state is a complicated structure, this is even more painful because the C user need to allocated each element on the stack and then fill the struct that only contains pointers. > > Is there a way to easily solve that ? I still want to complain about the lack of a mechanism to translate more information from the Core AST to the extracted AST (like the length of the buffers). > > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub <#33>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AEYAnqXSOc85cHoQgGotpbbru60dpqvYks5rbvcBgaJpZM4L-eDo>. >