Steel:wishlist

This page is a list of shortcomings of Low*v2 that we absolutely would like to address with STEEL, and in particular the redesign of the user programming model.

reinstate stack & heap

• what have we learned from the shortcomings of push/pop frame?
• can we have a more lexical discipline?
• a combinator, e.g. with_alloca 0ul 12ul (fun b -> ...) where the function receives a permission and must return it
• a meta-programmed combinator that takes a list of local variables, e.g.

with_locals [
  0ul, 12ul; // local variable int32_t x[12] = 0;
  false, 1ul; // local variable bool y[1] = { false };
] (fun x y ->
)

• can we minimize the amount of annotations?

const pointer done right

do we stand by the motto that every primitive concept in Low* has to be modeled as an abstract type in F*? do we really want to offer a specific library just for const pointers?

ghost references

do we want a primitive library of references? I would advocate arrays of size 1 only -- references should be a special case

kremlin could conceivably have a special treatment for arrays of units to eliminate them

size_t

The array type needs to have its length defined over an abstract module of size_t. size_t will be similar to a machine integer, in that it supports arithmetic operations. However, its maximum value will be unspecified.

Injections from machine integers will be made available, at the expense of generating static asserts in the generated C. We regroup all of the target assumptions in a module called Steel.Target which will expose:

module Steel.Target

val size_at_least16: bool
val size_at_least32: bool
val size_at_least64: bool

val little_endian: bool

These will be defined by hand using compiler macros.

// "Safe" version
val size_of_uint16: x:UInt16.t { Steel.Target.size_at_least16 } -> y:size_t { v y == v x }
// If Kremlin sees any occurrence of this one, it will generate at the beginning of the module: _Static_assert(sizeof size_t >= 2)
val size_of_uint16_assert: x:UInt16.t -> y:size_t { v y == v x }

Casts via magic wands

Oftentimes it's convenient to cast an array of integers to an array of bytes. The C standard comes with a strict aliasing restriction, meaning that we can only cast from uint_n* to char* and back to the exact same uint_n*; furthermore, for proof reasoning purposes, we don't want to allow arbitrary aliasing.

It would be nice to be able to define a magic wand, that takes an array of machine integers, casts it to an array of bytes, and when the user relinquishes the permission for the array of bytes, the permission for the original array is returned to the user.

For its functional specification, this operation would use Steel.Target to figure out whether the encoding is little or big-endian.

arraystruct

We want to revive Tahina's original ArrayStruct experiment. Seeing that we can define things built into the memory model, we will not run into the universe restriction that Tahina encountered earlier, and we should be able to define a type of paths to navigate a flat layout.

There are some C standard restrictions to be aware:

• no empty structs or unions (TBD -- most compilers actually accept them)
• non-zero arrays

For the latter point, there is actually a C feature where one can have this:

struct header {
  size_t len;
  char data[0];
} header_s;

char *tagged_array = malloc(sizeof header_s + MY_LEN);
((header_s *)tagged_array)->len = MY_LEN;

it would be really nice in terms of expressive power if we could model this with a magic wand.

concurrent toolkit

• https://en.wikipedia.org/wiki/Read-copy-update -- a primitive used pervasively in the linux kernel that would also be very useful for our userland implementation
• spinlocks, semaphores and threads: what is an API that is compilable to C?
  • underlying data structure (e.g. pthread_t) is by-address
  • passing data to initial thread creation requires the use of void* and cast; time to write Steel.Dyn? any way to make this safe?
  • shall we aim for generality (compiles to both windows & unix) or target one specific API (e.g. pthreads) and rely on winpthreads?

low-level data structures

a custom static allocator for embedded devices, where the outer allocator "owns" the unused slots + bookkeeping data at the beginning of each block, and client "owns" the payload of each allocated block

tricky issues of splitting ownership within a given struct

null pointer

There should be a null pointer value which has length 0, but also allow for other arrays (for instance splitted arrays) to have length 0. There should not be a lemma saying that any array of size 0 is the null pointer. Null pointer and other arrays of size 0 should be live (they should be in the ressource context) but you can only sub them, no indexing or update

The use of magic wands vs predicate refinements

The following situations are naturally encoded into magic wands:

• when you split an array, same thing it should give you the recombinable predicate as a magic wand, so that gluing back can just be an application of the magic wand rule
• same for sharing permissions. However this would pollute the ressource context with a lot of magic wand predicates, so we might want to do this a logical predicates in the refinements.