# 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.