## Quantification

Slang Contracts include bounded quantification expressions and these can be used to state properties/constraints in assertions as well as other Slang Contracts constructs. Slang also has unbounded quantification expressions that can be used in proof contexts, but in Slang Contracts quantification is always bounded.

Quantification expressions are most often used when reasoning about values of
integer ranges and Slang collections including sequences, sets, and
maps. Technically, Slang’s bounded quantification can only be applied
to integer ranges and sequence elements (both for immutable and
mutable sequences), but one can the `elements`

method for sets and
`keys`

for maps to obtain sequences that can quantified over.

## Quantification over Integer Ranges

The most common bounded quantification is over integer (`Z`

) ranges, and
the general form for these expressions is as follows::

```
*q* (*m* until/to *n*) (*i* => ... *i* ...)
```

where

*q*is a quantifier`All`

or`Exists`

,*m*is an expression of type`Z`

and is first element of the range to quantify over*n*is an expression of type`Z`

and is the upper bound of the range,`to`

indicates that the range is a closed interval (includes*n*) where was`until`

indicates that the range goes up to but does not include*n*,*i*is the quantified (bound) variable, and- “…
*i*…” is a boolean expression containing*i*.

Given the following sequence of integers::

```
val s1 = ISZ(1,2,3,4)
```

one can use quantified expressions to assert properties of the sequence::

```
assert(All(0 until s1.size)(i => s1(i) >= 0))
assert(Exists(0 until s1.size)(j => s1(j) == 2))
assert(Exists(0 until s1.size)(j => s1(j) < 0)) // fails
```

The upper and lower bounds of the range can be expressions, which is useful for reasoning about segments of a sequence::

```
assert(All(0 to ((s1.size / 2) - 1))(k => s1(k) > 0 & s1(k) < 3))
assert(All((s1.size / 2) until s1.size))(k => s1(k) >= 3))
```

Tip

**Note:** Following the data structure-based representation of Slang Contracts,
`All`

and `Exists`

are actually object constructors where the
first argument in the examples above is a sequence of `Z`

representing the range, and the second argument is a lambda expression
`... => ...`

that introduces the quantified variable as the argument
of the lambda expression and has a body of boolean type.

Slang’s bounded quantification expressions can be used in
specification contexts and proof contexts.
Since the assertion specification is also executable,
quantification expressions must be executable.

To get an executable form of a quantification expression,
the Slang compiler transforms the expression into a loop.
For example, the following pseudo-code shows the structure of the loop
implementation of the `All`

quantifier when it is applied to ranges
of type `Z`

::

```
def all(seq: ISZ[Z])(p: Z => Boolean): B = {
for (e <- seq) {
if (!p(e)) {
return F
}
}
return T
}
```

When quantifying over sequence indices, Slang provides some syntactic
sugar than enables one to use the `indices`

method inspired from Scala collections libraries and write::

```
assert(All(s.indices)(i => s(i) >= 0))
```

Behind the scenes, this gets represented as something equivalent to::

```
assert(All(0 until s1.size)(i => s1(i) >= 0))
```

Quantifiers can be nested, as illustrated in the following examples::

```
val s3 = ISZ(ISZ(1,2,3),ISZ(11,12,13),ISZ(21,22,23))
// illustrating nested quantification
assert(All(s3.indices)(i => All(s3(i).indices)(j => s3(i)(j) > i * 10)))
assert(Exists(s3.indices)(i => All(s3(i).indices)(j => (s3(i)(j) >= 11) & (s3(i)(j) <= 13))))
assert(Exists(s3.indices)(i => Exists(s3(i).indices)(j => (s3(i)(j) == 12))))
```

In the first example, with zero-based indexing, the assertion uses
nested `All`

to check
that successive sub-sequences have values greater than 0 (0 * 10), 10
(1 * 10), and 20 (2 * 10), respectively.

The second example uses an existential
quantification to state that there *exists* a sub-sequence with an index
`i`

where *all* the index positions `j`

of the sub-sequence have
values between 11 and 13.

The third example, states that there
exists a sub-sequence with index `i`

such that there exists a index
`j`

within the sub-sequence where the value is 12.

Tip

**Note:** In the current syntax of Slang, one *cannot* mimic familiar
abbreviations from logic notation such as *Ax,y. … x .. y …*, that
is, one *cannot* write something like `All(0 to 5, 10 to 15)((x,y) => ...)`

.

## Quantification over Sequences Elements

Slang also provides bounded quantification over sequence elements,
enabled by various forms of syntactic sugar. For example, one can
state constraints of sequence elements directly (as opposed to
“looking up” the element `v`

at a particular index `i`

via
`s1(i)`

) as follows::

```
assert(All(s1)(v => v >= 0)) // direct quantification over sequence elements
```

Behind the scenes, this gets represented as something equivalent to::

```
assert(All(0 until s1.size)(i => (v => v >= 0) s1(i))
```

which in turn is equivalent to::

```
assert(All(0 until s1.size)(i => s1(i) >= 0))
```

This style of quantification also applies to sequences of
pairs/tuples (**Robby: couldn’t get this to work**)::

```
// assert(All(s2)((v1,v2) => v1 == v2))
```

Slang doesn’t (yet) provide bounded quantification over set and map elements, but one can use associated methods that yield sequences.

For sets, the `elements`

method can be used::

```
val set1: Set[Z] = Set.empty[Z] ++ ISZ(1,2,3,4)
// state a constraint that applies to all elements of a set
assert(All(set1.elements)(v => v < 5))
```

For maps, both the `keys`

and `values`

methods can be used::

```
val m: Map[C,Z] = Map[C,Z](ISZ(('a',1),('b',2),('c',3)))
assert(All(m.keys)(c => c < 'd'))
assert(All(m.values)(n => n < 4))
```

**Robby: I couldn’t get quantification over entries to work**.

**Robby: Help me with explaining the desugarings for the above, e.g.,
as a numerical range over the size of the key sets.**

Using the sequence element quantification notation, the examples of nested quantification above can be re-stated more concisely::

```
// rephrasing the nested quantification examples above, in a more compact form
// by quantifying directly over sequence elements (when possible)
// original: (All(s3.indices)(i => All(s3(i).indices)(j => s3(i)(j) > i * 10)))
assert(All(s3.indices)(i => All(s3(i))(v => v > i * 10)))
// original: assert(Exists(s3.indices)(i => All(s3(i).indices)(j => (s3(i)(j) >= 11) & (s3(i)(j) <= 13))))
assert(Exists(s3)(ss => All(ss)(v => (v >= 11) & (v <= 13))))
// original: assert(Exists(s3.indices)(i => Exists(s3(i).indices)(j => (s3(i)(j) == 12))))
assert(Exists(s3)(ss => Exists(ss)(v => v == 12)))
```

In the first example, the first quantication `All(s3.indices)(i => ...)`

cannot be restated because the index `i`

is used in a
calculation. However, second quantification can now be stated
directly over values `v`

in the subsequence `s(i)`

.

The second example can now be understood as there *exists* a
sub-sequence `ss`

such that *all* values `v`

of the sub-sequence lie
between and 13.

The third example can now be understood as there *exists* a
sub-sequence `ss`

such that there *exists* a value `v`

of the
sub-sequence that equals 12.