# Existential Quantification

A very common specification style in Pulse involves the use of the existential quantifier. Before we can start to write interesting examples, let’s take a brief look at how existential quantification works.

As mentioned in the introduction to Pulse, one
of the connectives of Pulse’s separation logic is the existential
quantifier. Its syntax is similar to F*’s existential quantifier,
except it is written `exists*`

instead of just `exists`

, and its
body is a `vprop`

, as in the examples shown below.

```
exists* (v:nat). pts_to x v
exists* v. pts_to x v
exists* v1 v2. pts_to x v1 ** pts_to y v2
...
```

## Some simple examples

Looking back to the `assign`

example from the previous chapter
(shown below), you may have wondered why we bothered to bind a logical
variable `'v`

in precondition of the specification, since it is
never actually used in any other predicate.

```
fn assign (#a:Type) (r:ref a) (v:a)
requires pts_to r 'v
ensures pts_to r v
{
r := v;
}
```

And indeed, another way to write the specification of `assign`

, without
the logical variable argument, is shown below.

```
fn assign #a (x:ref a) (v:a)
requires
exists* w. pts_to x w
ensures
pts_to x v
{
x := v
}
```

This time, in the precondition, we use an existential quantifier to
say that `assign`

is callable in a context where `x`

points to any
value `w`

.

Usually, however, the postcondition of a function *relates* the
initial state prior to the call to the state after the call and
existential variables are only in scope as far to the right as
possible of the enclosing `vprop`

. So, existential quantifiers in
the precondition of a function are not so common.

To illustrate, the following attempted specification of `incr`

does
not work, since the existentially bound `w0`

is not in scope for the
postcondition.

```
[@@expect_failure]
```pulse
fn incr #a (x:ref int)
requires
exists* w0. pts_to x w
ensures
pts_to x (w0 + 1) //w0 is not in scope here
{
let w = !x
x := w + 1
}
```
```

However, existential quantification often appears in postconditions,
e.g., in order to abstract the behavior of function by underspecifying
it. To illustrate, consider the function `make_even`

below. It’s
type states that it sets the contents of `x`

to some even number
`w1`

, without specifying `w1`

exactly. It also uses an existential
quantification in its precondition, since its postcondition does not
depend on the initial value of `x`

.

```
fn make_even (x:ref int)
requires
exists* w0. pts_to x w0
ensures
exists* w1. pts_to x w1 ** pure (w1 % 2 == 0)
{
let v = !x;
x := v + v;
}
```

## Manipulating existentials

In a previous chapter on handling classical connectives, we saw how F* provides various constructs for introducing and eliminating logical connectives, including the existential quantifier. Pulse also provides constructs for working explicitly with existential quantifiers, though, usually, Pulse automation takes care of introducing and eliminating existentials behind the scenes. However, the explicit operations are sometimes useful, and we show a first example of how they work below

```
fn make_even_explicit (x:ref int)
requires
exists* w0. pts_to x w0
ensures
exists* w1. pts_to x w1 ** pure (w1 % 2 == 0)
{
with w0. assert (pts_to x w0);
let v = !x; // v:int; _:squash(v==w0); Ctxt=pts_to x v
x := v + v; // ... pts_to x (v + v)
introduce
exists* w1. pts_to x w1 ** pure (w1 % 2 == 0)
with (v + v);
}
```

### Eliminating existentials

The form `with w0...wn. assert p; rest`

is often used as an
eliminator for an existential. When the context contains ```
exists*
x0...xn. p
```

, the `with`

construct binds `w0 ... wn`

to the
existentially bound variables in the remainder of the scope `rest`

.

A `show_proof_state`

immediately after the ```
with w0. assert (pts_to
x w0)
```

prints the following:

```
- Current context:
pts_to x (reveal w0) **
emp
- In typing environment:
[w0#2 : erased int,
x#1 : ref int]
```

That is, we have `w0:erased int`

in scope, and ```
pts_to x (reveal
w0)
```

in context.

Here is another example usage of `with`

, this time with multiple
binders.

```
fn make_even_explicit_alt (x y:ref int)
requires
exists* wx wy. pts_to x wx ** pts_to y wy ** pure (wx % 2 == wy % 2)
ensures
exists* wx' wy'. pts_to x wx' ** pts_to y wy' ** pure (wx' % 2 == 0)
{
with wx wy. _;
let vx = !x;
let vy = !y;
x := vx + vy;
introduce exists* wx' wy'. pts_to x wx' ** pts_to y wy' ** pure (wx' % 2 == 0)
with (vx + vy) vy;
}
```

When there is a single existential formula in the context, one can
write `with x1..xn. _`

to “open” the formula, binding its witnesses
in scope. A `show_proof_state`

after the first line prints:

```
- Current context:
pts_to x (reveal wx) **
pts_to y (reveal wy) **
pure (eq2 (op_Modulus (reveal wx) 2) (op_Modulus (reveal wy) 2)) **
emp
- In typing environment:
[_#5 : squash (eq2 (op_Modulus (reveal wx) 2) (op_Modulus (reveal wy) 2)),
wy#4 : erased int,
wx#3 : erased int,
y#2 : ref int,
x#1 : ref int]
```

### Introducing existentials

The Pulse checker will automatically introduce existential formulas by
introduces new unification variables for each existentially bound
variable, and then trying to find solutions for those variables by
matching `vprops`

in the goal with those in the context.

However, one can also introduce existential formulas explicitly, using
the `introduce exists*`

syntax, as seen in the two examples
above. In general, one can write

```
introduce exists* x1 .. xn. p
with w1...wn
```

explicitly providing witnesses `w1..wn`

for each of the
existentially bound variables `x1..xn`

.