Mutable Arrays

In this chapter, we will learn about mutable arrays in Pulse. An array is a contiguous collection of values of the same type. Similar to ref, arrays in Pulse can be allocated in the stack frame of the current function or in the heap—while the stack allocated arrays are reclaimed automatically (e.g., when the function returns), heap allocated arrays are explicitly managed by the programmer.

Pulse provides two array types: Pulse.Lib.Array.array t as the basic array type and Pulse.Lib.Vec.vec t for heap allocated arrays. To provide code reuse, functions that may operate over both stack and heap allocated arrays can be written using Pulse.Lib.Array.array t—the Pulse.Lib.Vec library provides back-and-forth coercions between vec t and array t.

`array t`

We illustrate the basics of array t with the help of the following example that reads an array:

fn read_i #t (arr:array t) (#p:perm) (#s:erased (Seq.seq t)) (i:SZ.t { SZ.v i < Seq.length s })
  requires pts_to arr #p s
  returns x:t
  ensures pts_to arr #p s ** pure (x == Seq.index s (SZ.v i))
{
  arr.(i)
}

The library provides a points-to predicate pts_to arr #p s with the interpretation that in the current memory, the contents of arr are same as the (functional) sequence s:FStar.Seq.seq t. Like the pts_to predicate on reference, it is also indexed by an implicit fractional permission p, which distinguished shared, read-only access from exclusive read/write access.

In the arguments of read_i, the argument `s is erased, since it is for specification only.

Arrays can be read and written-to using indexes of type FStar.SizeT.t, a model of C size_t 1 in F*, provided that the index is within the array bounds—the refinement SZ.v i < Seq.length s enforces that the index is in bounds, where module SZ = FStar.SizeT. The function returns the i-th element of the array, the asserted by the postcondition vprop pure (x == Seq.index s (SZ.v i)). The body of the function uses the array read operator arr.(i).

As another example, let’s write to the i-th element of an array:

fn write_i #t (arr:array t) (#s:erased (Seq.seq t)) (x:t) (i:SZ.t { SZ.v i < Seq.length s })
  requires pts_to arr s
  ensures pts_to arr (Seq.upd s (SZ.v i) x)
{
  arr.(i) <- x
}

The function uses the array write operator arr(i) <- x and the postcondition asserts that in the state when the function returns, the contents of the array are same as the sequence s updated at the index i.

While any permission suffices for reading, writing requires full_perm. For example, implementing write_i without full_perm is rejected, as shown below.

[@@ expect_failure]
```pulse
fn write_ip #t (arr:array t) (#p:perm) (#s:erased _) (x:t) (i:SZ.t { SZ.v i < Seq.length s })
  requires pts_to arr #p s
  ensures pts_to arr #p (Seq.upd s (SZ.v i) x)
{
  arr.(i) <- x
}
```

The library contains share and gather functions, similar to those for references, to divide and combine permissions on arrays.

We now look at a couple of examples that use arrays with conditionals, loops, existentials, and invariants, using many of the Pulse constructs we have seen so far.

1: size_t in C is an unsigned integer type that is at least 16 bits wide. The upper bound of size_t is platform dependent. FStar.SizeT.size_t models this type and is extracted to the primitive size_t type in C, similar to the other bounded integer types discussed previously.

Compare

Let’s implement a function that compares two arrays for equality:

fn compare (#t:eqtype) #p1 #p2 (a1 a2:A.array t) (l:SZ.t) 
  requires (
    A.pts_to a1 #p1 's1 **
    A.pts_to a2 #p2 's2 **
    pure (Seq.length 's1 == Seq.length 's2 /\ Seq.length 's2 == SZ.v l)
  )
  returns res:bool
  ensures (
    A.pts_to a1 #p1 's1 **
    A.pts_to a2 #p2 's2 **
    pure (res <==> Seq.equal 's1 's2)
  )

The function takes two arrays a1 and a2 as input, and returns a boolean. The postcondition pure (res <==> Seq.equal 's1 's2) specifies that the boolean is true if and only if the sequence representations of the two arrays are equal. Since the function only reads the arrays, it is parametric in the permissions p1 and p2 on the two arrays. Note that the type parameter t has type eqtype, requiring that values of type t support decidable equality.

One way to implement compare is to use a while loop, reading the two arrays using a mutable counter and checking that the corresponding elements are equal.

{
  let mut i = 0sz;
  while (
    let vi = !i;
    if (vi <^ l) {
      let v1 = a1.(vi);
      let v2 = a2.(vi);
      (v1 = v2)
    } else {
      false
    }
  )
  invariant b.
  exists* vi. ( 
    R.pts_to i vi **
    A.pts_to a1 #p1 's1 **
    A.pts_to a2 #p2 's2 **
    pure (
      SZ.v vi <= SZ.v l /\
      (b == (SZ.v vi < SZ.v l && Seq.index 's1 (SZ.v vi) = Seq.index 's2 (SZ.v vi))) /\
      (forall (i:nat). i < SZ.v vi ==> Seq.index 's1 i == Seq.index 's2 i)
    )
  )
  {
    let vi = !i; 
    i := vi +^ 1sz
  };
  let vi = !i;
  let res = vi = l;
  res
}

The loop invariant states that (a) the arrays are pointwise equal up to the current value of the counter, and (b) the boolean b is true if and only if the current value of the counter is less than the length of the arrays and the arrays are equal at that index. While (a) helps proving the final postcondition of compare, (b) is required to maintain the invariant after the counter is incremented in the loop body.

Copy

As our next example, let’s implement a copy function that copies the contents of the array a2 to a1.

fn copy #t (a1 a2:A.array t) (l:SZ.t)
  requires (
    A.pts_to a1 's1 **
    A.pts_to a2 #p2 's2 **
    pure (Seq.length 's1 == Seq.length 's2 /\ Seq.length 's2 == SZ.v l)
  )
  ensures (
    (exists* s1. A.pts_to a1 s1 ** pure (Seq.equal s1 's2)) **
    A.pts_to a2 #p2 's2
  )
{
  let mut i = 0sz;
  while (
    let vi = !i;
    (vi <^ l)
  )
  invariant b.
  exists* vi s1. ( 
    R.pts_to i vi **
    A.pts_to a1 s1 **
    A.pts_to a2 #p2 's2 **
    pure (
      Seq.length s1 == Seq.length 's2 /\
      SZ.v vi <= SZ.v l /\
      (b == (SZ.v vi < SZ.v l)) /\
      (forall (i:nat). i < SZ.v vi ==> Seq.index s1 i == Seq.index 's2 i)
    )
  )
  {
    let vi = !i;
    let v = a2.(vi);
    a1.(vi) <- v;
    i := vi +^ 1sz
  }
}

The loop invariant existentially abstracts over the contents of a1, and maintains that up to the current loop counter, the contents of the two arrays are equal. Rest of the code is straightforward, the loop conditional checks that the loop counter is less than the array lengths and the loop body copies one element at a time.

The reader will notice that the postcondition of copy is a little convoluted. A better signature would be the following, where we directly state that the contents of a1 are same as 's2:

fn copy2 #t (a1 a2:A.array t) (l:SZ.t)
  requires (
    A.pts_to a1 's1 **
    A.pts_to a2 #p2 's2 **
    pure (Seq.length 's1 == Seq.length 's2 /\ Seq.length 's2 == SZ.v l)
  )
  ensures (
    A.pts_to a1 's2 **
    A.pts_to a2 #p2 's2
  )

We can implement this signature, but it requires one step of rewriting at the end after the while loop to get the postcondition in this exact shape:

  // after the loop
  with v1 s1. _; //bind existentially bound witnesses from the invariant
  Seq.lemma_eq_elim s1 's2; //call an F* lemma to prove that s1 == 's2
  ()

We could also rewrite the predicates explicitly, as we saw in a previous chapter.

Stack allocated arrays

Stack arrays can be allocated using the expression [| v; n |]. It allocates an array of size n, with all the array elements initialized to v. The size n must be compile-time constant. It provides the postcondition that the newly create array points to a length n sequence of v. The following example allocates two arrays on the stack and compares them using the compare function above.

fn compare_stack_arrays ()
  requires emp
  ensures emp
{
  // |- emp
  let mut a1 = [| 0; 2sz |];
  // a1:array int |- pts_to a1 (Seq.create 0 (SZ.v 2))
  let mut a2 = [| 0; 2sz |];
  // a1 a2:array int |- pts_to a1 (Seq.create 0 (SZ.v 2)) ** pts_to a2 (Seq.create 0 (SZ.v 2))
  let b = compare a1 a2 2sz;
  assert (pure b)
}

As with the stack references, stack arrays don’t need to be deallocated or dropped, they are reclaimed automatically when the function returns. As a result, returning them from the function is not allowed:

[@@ expect_failure]
```pulse
fn ret_stack_array ()
  requires emp
  returns a:array int
  ensures pts_to a (Seq.create 2 0)
{
  let mut a1 = [| 0; 2sz |];
  a1  // cannot prove pts_to a (Seq.create 0 2) in the context emp
}
```

Heap allocated arrays

The library Pulse.Lib.Vec provides the type vec t, for heap-allocated arrays: vec is to array as box is to ref.

Similar to array, vec is accompanied with a pts_to assertion with support for fractional permissions, share and gather for dividing and combining permissions, and read and write functions. However, unlike array, the Vec library provides allocation and free functions.

module V = Pulse.Lib.Vec

```pulse 
fn heap_arrays ()
  requires emp
  returns a:V.vec int
  ensures V.pts_to a (Seq.create 2 0)
{
  let a1 = V.alloc 0 2sz;
  let a2 = V.alloc 0 2sz;
  V.free a1;
  a2  // returning vec is ok
}
```

As with the heap references, heap allocated arrays can be coerced to array using the coercion vec_to_array. To use the coercion, it is often required to convert Vec.pts_to to Array.pts_to back-and-forth; the library provides to_array_pts_to and to_vec_pts_to lemmas for this purpose.

The following example illustrates the pattern. It copies the contents of a stack array into a heap array, using the copy2 function we wrote above.

fn copy_app (v:V.vec int)
  requires exists* s. V.pts_to v s ** pure (Seq.length s == 2)
  ensures V.pts_to v (Seq.create 2 0)
{
  let mut a = [| 0; 2sz |];
  // v, s |- V.pts_to v s ** ...
  V.to_array_pts_to v;
  // v, s |- pts_to (vec_to_array v) s ** ...
  copy2 (V.vec_to_array v) a 2sz;
  // v, s |- pts_to (vec_to_array v) (Seq.create 2 0) ** ...
  V.to_vec_pts_to v
  // v, s |- V.pts_to v (Seq.create 2 0) ** ...
}

Note how the assertion for v transforms from V.pts_to to pts_to (the points-to assertion for arrays) and back. It means that array algorithms and routines can be implemented with the array t type, and then can be reused for both stack- and heap-allocated arrays.

Finally, though the name vec a evokes the Rust std::Vec library, we don’t yet support automatic resizing.