Some valid Low* constructs¶

Low*’s base types are machine integers.

let square (x: UInt32.t): UInt32.t =
  let open FStar.UInt32 in
  x *%^ x

uint32_t square(uint32_t x)
{
  return x * x;
}

Classic control-flow is, naturally, supported. One may use recursive functions if they wish to do so, modern versions of GCC are generally quite good at performing tail-call optimizations.

let abs (x: Int32.t): Pure Int32.t
  (requires Int32.v x <> Int.min_int 32)
  (ensures fun r -> Int32.v r >= 0)
=
  let open FStar.Int32 in
  if x >=^ 0l then
    x
  else
    0l -^ x

int32_t abs(int32_t x)
{
  if (x >= (int32_t)0)
    return x;
  else
    return (int32_t)0 - x;
}

Low* models stack allocation, which is covered in The buffer library below.

let on_the_stack (): Stack UInt64.t (fun _ -> True) (fun _ _ _ -> True) =
  push_frame ();
  let b = B.alloca 0UL 64ul in
  b.(0ul) <- 32UL;
  let r = b.(0ul) in
  pop_frame ();
  r

uint64_t on_the_stack()
{
  uint64_t b[64U] = { 0U };
  b[0U] = (uint64_t)32U;
  uint64_t r = b[0U];
  return r;
}

Similarly, Low* supports heap allocation.

let on_the_heap (): St UInt64.t =
  let b = B.malloc HyperStack.root 0UL 64ul in
  b.(0ul) <- 32UL;
  let r = b.(0ul) in
  B.free b;
  r

uint64_t on_the_heap()
{
  uint64_t *b = KRML_HOST_CALLOC((uint32_t)64U, sizeof (uint64_t));
  b[0U] = (uint64_t)32U;
  uint64_t r = b[0U];
  KRML_HOST_FREE(b);
  return r;
}

Flat records are part of the original paper formalization, and are translated as regular C structs.

type uint128 = {
  low: UInt64.t;
  high: UInt64.t
}

typedef struct uint128_s
{
  uint64_t low;
  uint64_t high;
}
uint128;

In the original paper, structs may be allocated within buffers.

let uint128_alloc (h l: UInt64.t): St (B.buffer uint128) =
  B.malloc HyperStack.root ({ low = l; high = h }) 1ul

uint128 *uint128_alloc(uint64_t h, uint64_t l)
{
  KRML_CHECK_SIZE(sizeof (uint128), (uint32_t)1U);
  uint128 *buf = KRML_HOST_MALLOC(sizeof (uint128));
  buf[0U] = ((uint128){ .low = l, .high = h });
  return buf;
}

Still in the original paper, one may access a buffer index, then select a number of fields.

let uint128_high (x: B.buffer uint128): Stack UInt64.t
  (requires fun h -> B.live h x /\ B.length x = 1)
  (ensures fun h0 _ h1 -> B.live h1 x)
=
  (x.(0ul)).high

uint64_t uint128_high(uint128 *x)
{
  return x->high;
}

One may define global constants too, as long as they evaluate to C constants. As a rough approximation, arithmetic expressions and addresses of other globals are C constants, but as always, the C11 standard is the ultimate source of truth.

let min_int32 = FStar.Int32.(0l -^ 0x7fffffffl -^ 1l)

// Meta-evaluated by F*
int32_t min_int32 = (int32_t)-2147483648;

Some extensions to Low*¶

KreMLin supports a number of programming patterns beyond the original paper formalization, which aim to maximize programmer productivity. We now review the main ones.

One can rely on KreMLin to compile F*’s structural equality (the (=) operator) to C functions specialized to each type. Furthermore, the function below demonstrates the use of a struct type as a value, which is straightforwardly compiled to a C structure passed by value. Be aware that doing so has performance implications (see ??).

let uint128_equal (x y: uint128) =
  x = y

static bool __eq__LowStar_uint128(uint128 y, uint128 x)
{
  return true && x.low == y.low && x.high == y.high;
}

bool uint128_equal(uint128 x, uint128 y)
{
  return __eq__LowStar_uint128(x, y);
}

One may also use F* inductives, knowing that KreMLin will compile them as tagged unions, with a variety of optimized compilation schemes to make the generated code as palatable as possible.

noeq
type key =
  | Algorithm1: B.buffer UInt32.t -> key
  | Algorithm2: B.buffer UInt64.t -> key

typedef enum { Algorithm1, Algorithm2 } key_tags;

typedef struct key_s
{
  key_tags tag;
  union {
    uint32_t *case_Algorithm1;
    uint64_t *case_Algorithm2;
  }
  ;
}
key;

Generally, KreMLin performs a whole-program monomorphization of parameterized data types. The example below demonstrates this, along with a “pretty” compilation scheme for the option type that does not involves an anonymous union.

let abs2 (x: Int32.t): option Int32.t =
  let open FStar.Int32 in
  if x = min_int32 then
    None
  else if x >=^ 0l then
    Some x
  else
    Some (0l -^ x)

typedef enum { FStar_Pervasives_Native_None, FStar_Pervasives_Native_Some }
FStar_Pervasives_Native_option__int32_t_tags;

typedef struct FStar_Pervasives_Native_option__int32_t_s
{
  FStar_Pervasives_Native_option__int32_t_tags tag;
  int32_t v;
}
FStar_Pervasives_Native_option__int32_t;

FStar_Pervasives_Native_option__int32_t abs2(int32_t x)
{
  if (x == min_int32)
    return ((FStar_Pervasives_Native_option__int32_t){ .tag = FStar_Pervasives_Native_None });
  else if (x >= (int32_t)0)
    return
      ((FStar_Pervasives_Native_option__int32_t){ .tag = FStar_Pervasives_Native_Some, .v = x });
  else
    return
      (
        (FStar_Pervasives_Native_option__int32_t){
          .tag = FStar_Pervasives_Native_Some,
          .v = (int32_t)0 - x
        }
      );
}

Inductives are compiled by KreMLin, and so are pattern matches. Note that for a series of cascading if-then-elses, KreMLin has to insert a fallback else statement, both because the original F* code may be unverified and the pattern-matching may be incomplete, but also because the C compiler may trigger an error.

let fail_if #a #b (package: a * (a -> option b)): St b =
  let open C.Failure in
  let open C.String in
  let x, f = package in
  match f x with
  | None -> failwith !$"invalid argument: fail_if"
  | Some x -> x

int32_t
fail_if__int32_t_int32_t(
  K___int32_t_int32_t____FStar_Pervasives_Native_option__int32_t package
)
{
  int32_t x = package.fst;
  FStar_Pervasives_Native_option__int32_t (*f)(int32_t x0) = package.snd;
  FStar_Pervasives_Native_option__int32_t scrut = f(x);
  if (scrut.tag == FStar_Pervasives_Native_None)
    return C_Failure_failwith__int32_t("invalid argument: fail_if");
  else if (scrut.tag == FStar_Pervasives_Native_Some)
  {
    int32_t x1 = scrut.v;
    return x1;
  }
  else
  {
    KRML_HOST_PRINTF("KreMLin abort at %s:%d\n%s\n",
      __FILE__,
      __LINE__,
      "unreachable (pattern matches are exhaustive in F*)");
    KRML_HOST_EXIT(255U);
  }
}

Higher order is, to a certain extent, possible. The sample above demonstrates a block-scope function pointer. The fail_if function has been specialized on K__int32_t_int32_t, which is itself a specialization of the polymorphic pair type of F*. Below is a sample caller of fail_if__int32_t_int32_t, which relies on passing a pair of a function pointer and its argument.

let abs3 (x: Int32.t): St Int32.t =
  fail_if (x, abs2)

int32_t abs3(int32_t x)
{
  return
    fail_if__int32_t_int32_t((
        (K___int32_t_int32_t____FStar_Pervasives_Native_option__int32_t){ .fst = x, .snd = abs2 }
      ));
}

Local closures are not supported, as they do not have a natural compilation scheme to C. We will, however, show in (??) how to rely on F*’s meta-programming capabilities to normalize these closures away before passing them to KreMLin.

let pow4 (x: UInt32.t): UInt32.t =
  let open FStar.UInt32 in
  [@ inline_let ]
  let pow2 (y: UInt32.t) = y *%^ y in
  pow2 (pow2 x)

uint32_t pow4(uint32_t x)
{
  uint32_t x0 = x * x;
  return x0 * x0;
}

In the case that the user defines a global variable that does not compile to a C11 constant, KreMLin generates a “static initializer” in the special kremlinit_globals function. If the program has a main, KreMLin automatically prepends a call to kremlinit_globals in the main. If the program does not have a main and is intended to be used as a library, KreMLin emits a warning, which is fatal by default.

let uint128_zero (): Tot uint128 =
  { high = 0UL; low = 0UL }

let zero = uint128_zero ()

$ krml -skip-linking -no-prefix LowStar LowStar.fst
(...)
Warning 9: : Some globals did not compile to C values and must be
initialized before starting main(). You did not provide a main function,
so users of your library MUST MAKE SURE they call kremlinit_globals();
(see kremlinit.c).

$ cat kremlinit.c
(...)
void kremlinit_globals()
{
  zero = uint128_zero();
}

Some non-Low* code¶

We now review some classic programming patterns that are not supported in Low*.

The example below cannot be compiled for the following reasons:

• local recursive let-bindings are not Low*;

• local closure captures variable in scope (KreMLin does not do closure conversion)

• the list type is not Low*.

let filter_map #a #b (f: a -> option b) (l: list a): list b =
  let rec aux (acc: list b) (l: list a): Tot (list b) (decreases l) =
    match l with
    | hd :: tl ->
        begin match f hd with
        | Some x -> aux (x :: acc) tl
        | None -> aux acc tl
        end
    | [] ->
        List.rev acc
  in
  aux [] l

Trying to compile the snippet above will generate a warning when calling F* to generate a .krml file.

$ krml -skip-compilation -verbose LowStar.fst
⚙ KreMLin auto-detecting tools.
(...)
✔ [F*,extract]
<dummy>(0,0-0,0): (Warning 250) Error while extracting LowStar.filter_map
to KreMLin (Failure("Internal error: name not found aux\n"))

To explain why the list type cannot be compiled to C, consider the snippet below. Data types are compiled as flat structures in C, meaning that the list type would have infinite size in C. This is compiled by KreMLin but rejected by the C compiler. See ?? for an example of a linked list.

type list_int32 =
| Nil: list_int32
| Cons: hd:Int32.t -> tl:list_int32 -> list_int32

let mk_list (): St list_int32 =
  Cons 0l Nil

Trying to compile the snippet above will generate an error when calling the C compiler to generate a .o file.

$ krml -skip-linking -verbose LowStar.fst
⚙ KreMLin auto-detecting tools.
(...)
✘ [CC,./LowStar.c]
In file included from ./LowStar.c:8:0:
./LowStar.h:95:22: error: field ‘tl’ has incomplete type
   LowStar_list_int32 tl;

Polymorphic assumes are also not compiled. KreMLin could generate one C extern declaration per monomorphic use, but this would require the user to provide a substantial amount of manually-written code, so instead we refuse to compile the definition below.

// Cannot be compiled: polymorphic assume val; solution: make the function
// monomorphic, or provide a C macro
assume val pair_up: #a:Type -> #b:Type -> a -> b -> a * b

Trying to compile the snippet above will generate a warning when calling F* to generate a .krml file.

$ krml -skip-compilation -verbose LowStar.fst
⚙ KreMLin auto-detecting tools.
(...)
✔ [F*,extract]
Not extracting LowStar.pair_up to KreMLin (polymorphic assumes are not supported)

One point worth mentioning is that indexed types are by default not supported. See section ?? for an unofficial KreMLin extension that works in some very narrow cases, or rewrite your code to make t an inductive. KreMLin currently does not have support for untagged unions, i.e. automatically making t a C union.

type alg = | Alg1 | Alg2
let t (a: alg) =
  match a with
  | Alg1 -> UInt32.t
  | Alg2 -> uint128

let default_t (a: alg): t a =
  match a with
  | Alg1 -> 0ul
  | Alg2 -> zero

Trying to compile the snippet above will generate invalid C code.

void *default_t(alg a)
{
  switch (a)
  {
    case Alg1:
      {
        return (void *)(uint32_t)0U;
      }
    case Alg2:
      {
        return (void *)zero
      }
    default:
      {
        KRML_HOST_PRINTF("KreMLin incomplete match at %s:%d\n", __FILE__, __LINE__);
        KRML_HOST_EXIT(253U);
      }
  }
}

If you are lucky, the C compiler may generate an error:

$ krml -skip-linking LowStar.fst -add-include '"kremstr.h"' -no-prefix LowStar -warn-error +9

✘ [CC,./LowStar.c]
./LowStar.c: In function ‘default_t’:
./LowStar.c:291:9: error: cannot convert to a pointer type
         return (void *)zero;

The memory model¶

Beyond the language subset, one defining component of Low* is how it models the C memory.

module ST = FStar.HyperStack.ST
module HS = FStar.HyperStack

let root: HS.rid = HS.root

let _ =
  //AR: TODO: FIXME: temporary until I fix it in the memory model
  HS.root_is_not_freeable ();
  assert (ST.is_eternal_region root /\ ~ (Monotonic.HyperStack.is_stack_region root))

let equal_domains (m0 m1: HS.mem) =
  (HS.get_tip m0) == (HS.get_tip m1) /\
  Set.equal (Map.domain (HS.get_hmap m0)) (Map.domain (HS.get_hmap m1)) /\
  ST.same_refs_in_all_regions m0 m1

let f (x: UInt32.t): Stack UInt32.t (fun _ -> True) (fun _ _ _ -> True) =
  FStar.UInt32.( x *%^ x )

[@ expect_failure ]
let g (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
  let b = B.alloca 0ul 8ul in
  ()

[@ expect_failure ]
let g2 (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
  push_frame ();
  let b = B.alloca 0ul 8ul in
  ()

let g3 (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
  push_frame ();
  let b = B.alloca 0ul 8ul in
  pop_frame ();
  ()

void g3()
{
  uint32_t b[8U] = { 0U };
}

let g4 (): ST unit (fun _ -> True) (fun _ _ _ -> True) =
  push_frame ();
  let b = B.malloc HS.root 0ul 8ul in
  pop_frame ();
  ()

effect St (a:Type) = ST a (fun _ -> True) (fun _ _ _ -> True)

let test_st_get (): St unit =
  push_frame ();
  let m = ST.get () in
  assert (Monotonic.HyperStack.is_stack_region (HS.get_tip m));
  pop_frame ()

Machine integers¶

Machine integers are modeled as natural numbers that fit within a certain number of bits. This model is dropped by KreMLin, in favor of C’s fixed-width types.

Fixed-width integers are found in FStar.UInt{16,32,64,128}.fst and FStar.Int{16,32,64,128}. The FStar.Int.Cast.Full.fst module offers conversion functions between these integer types.

Machine integers offer the classic set of arithmetic operations. Like in C, unsigned integers have wraparound overflow semantics, exposed via the add_mod function. Signed integers offer no such function. Other undefined behaviors of C are ruled out at the F* level, such as shifting an integer by the bit width.

Machine integers modules also define operators, suffixed with ^. For instance, the + operation for UInt32 is +^. Wraparound variants have an extra % character, such as +%^, when available.

Operators follow the standard precedence rules of F*, which are outlined on its wiki. Operators are resolved in the current scope; we recommend the use of module abbreviations and the let-open notation M.( ... ).

module U32 = FStar.UInt32

let z = U32.(16ul -^ 8ul )

Machine integers can be reflected as natural numbers of type nat using the v function. It is generally more convenient to perform proofs on natural numbers.

let test_v (): unit =
  let x = 0ul in
  assert (U32.v x = 0)

The buffer library¶

LowStar.Buffer is the workhorse of Low*, and allows modeling C arrays on the stack and in the heap. LowStar.Buffer models C arrays as follows:

let lseq (a: Type) (l: nat) : Type =
  (s: Seq.seq a { Seq.length s == l } )

noeq
type buffer (a:Type) =
  | MkBuffer: max_length:UInt32.t
    -> content:reference (lseq a (U32.v max_length))
    -> idx:UInt32.t
    -> length:UInt32.t{U32.(v idx + v length <= v max_length)}
    -> buffer a

In other words, buffers are modeled as a reference to a sequence, along with a starting index idx, and a length, which captures how much of an allocation slice one is currently pointing to.

This is a model: at compilation-time, KreMLin implements buffers using C arrays.

The length is available in ghost (proof) code only: just like in C, one cannot compute the length of a buffer at run-time. Therefore, a typical pattern is to use refinements to tie together a buffer and its length, as we saw with the initial memcpy example.

let do_something (x: B.buffer UInt64.t) (l: U32.t { U32.v l = B.length x }): St unit =
  ()

Allocating a buffer on the stack is done using the alloca function, which takes an initial value and a length. alloca requires that the top of the stack be a valid stack frame.

let test_alloc_stack (): Stack unit (fun _ -> True) (fun _ _ _ -> True) =
  push_frame ();
  let b = B.alloca 0UL 8ul in
  pop_frame ();
  ()

Allocating a buffer on the heap is done using the malloc function, which takes a region, an initial value and a length. The region is purely for proof and separation purposes, and has no effect on the generated code. A buffer created with malloc can be freed with free.

let test_alloc (): St unit =
  let b = B.malloc HS.root 0UL 8ul in
  B.free b

Pointer arithmetic is performed by the means of the sub function. Under the hood, the sub function returns a buffer that points to the same underlying reference, but has different idx and length fields.

let test_sub (): St unit =
  let b = B.malloc HS.root 0UL 8ul in
  let b_l = B.sub b 0ul 4ul in // idx = 0; length = 4
  let b_r = B.sub b 4ul 4ul in // idx = 4; length = 4
  B.free b

Just like in C, one can only free the base pointer, i.e. this is an error:

[@ expect_failure ]
let test_sub_error (): St unit =
  let b = B.malloc HS.root 0UL 8ul in
  let b_l = B.sub b 0ul 4ul in // idx = 0; length = 4
  B.free b_l

Reading and modifying a buffer is performed by means of the index and upd functions. These are exposed as the .() and .()<- operators respectively, defined in LowStar.BufferOps. This latter module module only contains those operators, and is meant to be used with open to bring operators into scope without further polluting the context with any definition from LowStar.Buffer.

let test_index (): St unit =
  let b = B.malloc HS.root 0UL 8ul in
  b.(0ul) <- UInt64.add_mod b.(0ul) b.(0ul);
  B.free b

Buffers are reflected at the proof level using sequences, via the as_seq function, which returns the contents of a given buffer in a given heap, i.e. a sequence slice ranging over the interval [idx; idx + length).

let test_as_seq (): St unit =
  let b = B.malloc HS.root 0UL 1ul in
  let h = ST.get () in
  assert (Seq.equal (B.as_seq h b) (Seq.cons 0UL Seq.createEmpty));
  B.free b

B.get is an often-convenient shorthand to index the value of a given buffer in a given heap.

let test_get (): St unit =
  let b = B.malloc HS.root 0UL 1ul in
  let h = ST.get () in
  assert (B.get h b 0 = 0UL);
  B.free b

C NULL pointers

LowStar.Buffer also exposes a model of the C NULL pointer, null – this is what you should use if you need zero-length buffers. The NULL pointer is always live, and always has length 0. The pointer and pointer_or_null functions define convenient aliases, while the (!*) operator (defined in LowStar.BufferOps) guarantees that the dereference will be pretty-printed with a * C dereference, as opposed to an access at array index 0. Pointers can always be tested for nullity via the is_null p function, which is guaranteed to be pretty-printed as p != NULL.

The modifies clauses library¶

The current heap model of F* is based on a select-update theory: the heap is reflected as a map, allocation adds a key in the map, assignment updates the map, and reading selects from the map.

Proving properties of programs therefore requires the programmer to reason about the heap model. However, stating precise post-conditions that refer to a particular heap after a particular update does not scale up to large programs: we want to reason abstractly about modifications, and use a library of composable predicates that allow one to generically reason about a given modification to the heap.

This is where the LowStar.Modifies library comes in handy. The modifies clauses library allows one to reason about allocation, de-allocation, modifications using a single unified modifies clause. An abstract notion of a memory location allows composing predicates, and deriving properties such as: “if I modify a location l1 disjoint from l2, then the contents of the memory at address l2 remain unchanged”.

Abstract memory locations

The LowStar.Modifies library abstracts over memory locations. Memory locations have type loc. Locations form a monoid, where loc_none is the empty location and loc_union combines two location to form the union of the two.

Several injections exist to create locations; for now, we will mostly use loc_buffer, which injects a LowStar.Buffer.t into an abstract location.

Inclusion and disjointness

The LowStar.Modifies module provides an inclusion relation, via loc_includes. This allows the programmer to state, for instance, that the location of a stack-allocated buffer is included in its stack frame.

Perhaps more useful is the loc_disjoint predicates, which allows the programmer to state that two memory locations do not overlap.

The modifies clause

The modifies clause is of the form modifies l h0 h1 where l is an abstract memory location, h0 is the initial heap and h1 is the resulting heap. Here is an example:

module M = LowStar.Modifies

let example_modifies_callee (b1 b2: B.buffer UInt32.t) : Stack unit
  (requires (fun h -> B.live h b1 /\ B.live h b2 /\ B.length b1 == 1 /\ B.length b2 == 1 /\ B.disjoint b1 b2))
  (ensures (fun h _ h' ->
    M.modifies (M.loc_union (M.loc_buffer b1) (M.loc_buffer b2)) h h' /\
    B.live h' b1 /\ B.live h' b2 /\
    B.get h' b1 0 == 18ul /\ B.get h' b2 0 == 42ul
  ))
= b2.(0ul) <- 42ul;
  b1.(0ul) <- 18ul

The pre- and post-conditions of the example_modifies_callee function state that, if b1 and b2 are two disjoint live buffers of length 1, then example_modifies changes their contents to 18ul and 42ul, respectively. In itself, the modifies clause tells nothing, but it starts becoming useful when the example_modifies_callee function is called by another function:

let example_modifies_caller (b0: B.buffer UInt32.t) : Stack unit
  (requires (fun h -> B.live h b0 /\ B.length b0 == 3))
  (ensures (fun h _ h' ->
    M.modifies (M.loc_buffer b0) h h' /\
    B.live h' b0 /\
    B.get h' b0 0 == B.get h b0 0
  ))
= let b1 = B.sub b0 1ul 1ul in
  let b2 = B.sub b0 2ul 1ul in
  example_modifies_callee b1 b2;
  assert (forall h . B.get h b0 0 == B.get h (B.gsub b0 0ul 1ul) 0)

This function takes a buffer b0 of length 3, and from it, extracts two disjoint buffers, b1 and b2, as the sub-buffers of b0 of length 1 at offsets 1 and 2, respectively. Since they are both live and disjoint, they can then be passed to example_modifies_callee. Then, the post-condition of example_modifies_caller about the contents of the cell of b0 at offset 0 is due to the fact that that cell of b0 is disjoint from both b1 and b2 (because it is the cell of the sub-buffer of b0 at offset 0, as suggested by the assert), and so, by virtue of the modifies clause of example_modifies_callee, its value is preserved.

C standard library¶

The C.fst module, found in the kremlib directory, exposes a hodgepodge of C functions.

From the C header <stdlib.h>:

• rand and srand; note that this makes the assumption that sizeof int == 4, which is true of most modern platforms

• exit, which is not polymorphic, per the reasons exposed earlier in The Low* subset of F*, see C.Failure below instead

• the stdout, stderr and fflush functions

• the EXIT_SUCCESS and EXIT_FAILURE macros; these are defined as an inductive; since C.fst is not extracted, the code is left with references that resolve to the underlying C macros

From the C header <time.h>:

• clock_t and clock – the post-condition is not very good and needs to be fixed

Other:

• a variety of endian-ness conversion macros that are implemented using host-specific instructions to maximize efficiency

• a C.char type, which is interconvertible with uint8 through a variety of coercions; the C standard states that char is the only type that is not equal to its signed or unsigned variants, meaning that we can neither expose type char = UInt8.t or type char = Int8.t.

Test helpers¶

The TestLib.fsti module provides a couple helper functions, including print_clock_diff to deal with clock_t above.

C string literals¶

The C.String.fst module exposes a bare-bones model of C string literals, i.e. const char *s = "my string literal";. This relies on a syntactic check that the argument to of_literal is a constant string literal in the original F* source. Such strings are zero-terminated, and their length can be computed (TODO). They can be printed on the standard output via C.String.print.

From the F* typing perspective, these strings are values that have an eternal lifetime and are immutable. This corresponds exactly to the semantics of a C string literal placed in the RODATA section of an ELF executable.

Operations such as mutation or concatenation cannot be implemented on C.String.t. The former is not possible given the value semantics of C.String.t, and the latter would require allocations that would never be freed. Instead, one should allocate a C character array and blit string literals into it to achieve concatenation, hence properly tracking mutation and the underlying allocation. See test/Server.fst for an incomplete, work-in-progress model of dealing with mutable string buffers.

A polymorphic exit¶

The C.Failure.fst exposes a single failwith function that properly has a polymorphic return type. This uses a recursion hack in combination with KreMLin’s monomorphization, and will require you to disable compiler warnings for infinite recursion.