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?

NS, DM, TR, JP:

• this is hard to enforce, probably want the user to state what kind of annotations they expect to see in the generated C code
• probably want a separate language of annotations to be checked by a hook of some sorts, like a tactic
• difficult to figure out what is the right design; for instance one could rely on the user to annotate parameters and local let-bindings with const (the C compiler checks it, or krml) -- or a variant, e.g. user annotates function parameters and kremlin checks const as needed

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

NS, DM, TR, JP:

• PCMs are general and it's hard to settle on any given PCM because they encode layout but also temporal invariants through the use of monotonicity
• it'd be nice to aim for something modular and reusable where someone can combine a shared, canonical layout PCM with a custom PCM for, say, the laws of a state machine, but we're not there yet -- would be nice to investigate
• type class of pointer which is what extraction specializes on, and allows multiple PCMs?
• it seems nice to allow everyone to agree on a distinguished PCM for low-level (concrete) programming while for reasoning over ghost refs could be done with arbitrary PCMs

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?

discussion:

• would be nice to enforce that the user hoists the closures themselves at the top-level, and we can probably reveal in Steel that the closures receive some heap-allocated data
• no surprises
• kremlin will transform a polymorphic fork-join into pthread_create along with suitable casts to void*
• user-facing API might need to be changed to reflect the thread handle as a pointer to a resource in memory

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.

About automating proofs that require unrolling/rolling of ressources definition in context

For instance you can view a struct as one reference to the whole struct or have a big star of all the fields of the struct. A tactic could do automatic recombining/exploding of the struct depending on what's expected. See heuristics of Mezzo to define a set of tactics to automate common pattern.

Objective => define a limited subset of things where there is very high automation support.

Various kinds of structures that we would like to express with ArrayStruct

Fractional permissions on arrays and their elements

Immutable arrays with splitting

Preorders on entire arrays

Prefix-freezable arrays (aka stash)

2d points, 3d points and pointers to fields thereof

Points constrained to evolve along some trajectory

Delayed initialization (initialized once, but not at allocation)

??