-
Notifications
You must be signed in to change notification settings - Fork 235
Mutable structures in Low*
Besides homogeneous buffers, the F* standard library provides mutable structures based on heterogeneous dependent maps. This wiki page presents the formalization and implementation as of February 27th 2017.
The FStar.DependentMap module provides a library for pure heterogeneous maps.
A type key for element names shall be provided. keys shall have decidable equality. Then, the type of each element of the map shall be given by a function value: (f: field_name) -> Tot Type.
Based on those, to create a heterogeneous map, the user shall provide a function initial_values: (k: key) -> value k. Then, FStar.DependentMap.create #key #value initial_values will create a map of type FStar.DependentMap.t key value.
Then, given a map m: FStar.DependentMap.t keys value_types and a key k: key, FStar.DependentMap.sel m k will retrieve the element associated to the key k.
Then, given a map m: FStar.DependentMap.t keys value_types, a key k: key and a value v: value k, FStar.DependentMap.upd m k v will retrieve the new map with the key k now associated to v and others unchanged.
Based on this library for heterogeneous maps, we can define mutable structures. The FStar.Struct library provides a way to define mutable structures, and pointers to their fields.
If init is a dependent map, of some type DependentMap.t key value containing the initial values of the fields of a structure, then FStar.Struct.screate #(FStar.DependentMap.t key value) init allocates a new structure into the stack, with those initial values. The structure is of type FStar.Struct.struct_ptr (FStar.DependentMap.t key value). This is an effectful operation (similar to FStar.Buffer.create for buffers.)
Similarly, for an eternal region r, FStar.Struct.ecreate #(FStar.DependentMap.t key value) r init will allocate the structure into the region r instead of the stack. This is also an effectful operation (similar to FStar.Buffer.rcreate for buffers.)
In both cases, the result is live (FStar.Struct.live) in the post memory state.
In fact, it is also possible to create a reference-like pointer to a value of type t where t is any type (not necessarily a FStar.DependentMap.t). In that case, the notion of field is not defined.
If s is a mutable structure, of type FStar.Struct.struct_ptr (FStar.DependentMap.t key value), and f: key is a field, then FStar.Struct.field s f returns a pointer to the field f in s, of type (FStar.Struct.struct_ptr (value f)). This is an effectful operation.
This operation has a ghost counterpart, for use in specifications: FStar.Struct.gfield.
The type value f can itself be FStar.DependentMap.t, thus providing a way to nest a structure into s.
Both operations are similar to FStar.Buffer.sub for buffers.
If s is a structure, or a pointer to a field (or other kind of pointer), of type FStar.Struct.struct_ptr t, then FStar.Struct.read s reads the value stored in s, thus returning a value of type t. This is an effectful operation (similar to FStar.Buffer.index for buffers.)
This operation has a ghost counterpart, for use in specifications: FStar.Struct.as_value (similar to FStar.Buffer.as_seq for buffers.)
If s is a structure, or a pointer to a field, of type FStar.Struct.struct_ptr t, and v is a value of type t, then FStar.Struct.write s v write the value v into s. This is an effectful operation (similar to FStar.Buffer.upd for buffers.)
It is possible to nest a structure into a buffer without any indirection. To this end, it suffices to create a buffer of dependent maps, thus of type FStar.Buffer.buffer (FStar.DependentMap.t key value).
Then, if b is such a buffer, then it is possible to obtain a pointer to its cell i, by the operation FStar.Struct.from_buffer_index b i, thus yielding a (pointer to a) mutable structure, of type FStar.Struct.struct_ptr (FStar.DependentMap.t key value), thus making it possible to take a pointer to one of its fields. This is an effectful operation (requiring b to be live.)
This operation has a ghost counterpart: FStar.Struct.gfrom_buffer_index
However useful, this operation is possible if the buffer data is of any type t (not necessarily a FStar.DependentMap.t), thus yielding a reference-like pointer to a value of type t; of course, there, the notion of field is no longer defined.
Structures can be nested. Currently, structures are built on top of buffers, but buffers cannot be nested into structures without any indirection.
It would be nice to fully allow nesting them so that arrays can be flatly stored as structure fields with no indirection.
Then, we would reimplement buffers as a special case of structs.
What if we want structures with fields whose types depend on each other's values?
A possible implementation could be based on the following telescope type:
noeq type telescope:
(field: eqtype) ->
(repr: Type) ->
Type =
| TNil:
(field: eqtype { ~ field } ) ->
telescope field unit
| TCons:
(field: eqtype) ->
(f: field) ->
(repr:Type) ->
(tele: telescope (f': field {f' <> f}) repr) ->
(v: (repr -> Tot Type)) ->
telescope field ((x: repr) & v x)
(UPDATE: does not work very well with unification in practice. Maybe we should have a separate list of fields, consume it in the telescope, and have the two totality and non-duplication conditions separately on the list.)