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))

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.

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.