let mutable

Notes from a meeting with JK, Aseem, Nik and Jonathan about use-cases for let-mutable.

Reminder: as some point in the past, the following program worked:

module Mutable

//
open FStar.Int32
open FStar.ST
open TestLib

val main: Int32.t -> FStar.Buffer.buffer (FStar.Buffer.buffer C.char) ->
  ST.Stack Int32.t (fun _ -> true) (fun _ _ _ -> true)
let main argc argv =
  push_frame ();
  let open FStar.Int32 in
  let mutable x = 1l in
  x <- x +^ x;
  check x 2l;
  pop_frame ();
  C.exit_success

let mutable is desugared as let x = salloc 1l; x <- e1 is desugared as x := e1 and any reference to x is replaced by !x.

• Low*/KreMLin is about offering a carefully-crafted set of primitives that balance the need to get performance and to make proofs easy. In a sense, there's already a tradeoff with structs-as-values: they're great because they come with no proof obligations, but the performance is potentially bad (complete copy on the stack on x86, at least). You can opt-out and go for a buffer of size 1 and de facto pass the struct by reference, but then there's extra proof obligations.
• Immutable let-bindings are great because they come with no proof obligation. Therefore, starting from the following snippet:

int x = 0;
x = e1;
x = e2;

one can turn it into the following Low* program:

let x = 0 in
let x = e1 in
let x = e2 in

the KreMLin extraction pipeline will generate:

int x = 0;
int x1 = e1;
int x2 = e2;

which any decent compiler will optimize through SSA + register allocation. So, for these use-cases, the recommendation is to keep using immutable variables. A future optimization phase of KreMLin may recognize that i) the two variables have the same size ii) the latter shadows the former and iii) they live in the same scope (i.e. didn't go through a branching construct)... and then replace this with an assignment.

• Let mutable variables may thus be useful for loops, but we want them to be easy to use, i.e. show that they are left unchanged through a function call in the Stack effect. One early proposal was to use a meta argument and say that push_frame() takes a snapshot of the locally mutable variables, and that pop_frame() restores the snapshot. Using a meta-argument, since the callee could not possibly have the address of x (because all that exists is !x), it must be the case that push_frame() and pop_frame() can always be implemented as no-ops.

• A slightly better proposal is the following. We distinguish a sub-region of each stack frame, say, the carmine region (red is boring); then, every let-mutable variable is allocated in that region. The Stack effect is modified to say that it leaves the caller's carmine region unchanged. Then, F* should be able at every use-site of the Stack effect to prove this fact.

Implementation status: let mutable is currently broken and no longer extracts properly through Kremlin #725