4.5.1. Arithmetic🔗

+, -, *, unary -, /, %, /t, and %t operate on numeric values, and both operands must have the same numeric type. For integers there are two division/remainder pairs, and the difference only shows up on negative operands:

• / and % are Euclidean: the remainder is never negative;

• /t truncates the quotient toward zero, and %t is a - b * (a /t b).

procedure divisionFacts()
  opaque
{
  assert -7 / 3 == -3;
  assert -7 % 3 == 2;
  assert -7 /t 3 == -2;
  assert -7 %t 3 == -1
};

All four forms generate a nonzero-divisor proof obligation, so a possible division by zero shows up as a failed precondition at the offending operator rather than as undefined behaviour. There is no source syntax for skipping that check.

Operators are not a separate kind of expression: each is a call to an overloaded built-in procedure, which is why operand admissibility is overload selection and why / can carry a precondition at all. That mechanism is described under Operators.

4.5.2. Boolean operators🔗

procedure booleans(a: bool, b: bool)
  opaque
{
  assert (a & b) == (b & a);      // eager: both sides evaluated
  assert (a | b) == (b | a);      // eager
  assert (a && b) == (b && a);    // b evaluated only when a is true
  assert (a || b) == (b || a);    // b evaluated only when a is false
  assert (a ==> b) == (!a || b);  // b evaluated only when a is true
  assert !(!a) == a
};

The eager and short-circuiting pairs differ only when the right-hand side has an effect, which in Laurel it may: operands can contain assignments and calls. The short-circuit forms mean exactly what the corresponding conditional means — a && b is if a then b else false, a || b is if a then true else b, and a ==> b is if a then b else true.

One caveat: if the right-hand side contains an assert or assume and nothing else effectful, write the conditional explicitly rather than relying on the short-circuit form, because the proof statement can currently escape its guard.

4.5.3. Equality, ordering, and strings🔗

procedure comparisons(x: int, y: int, l: string, r: string)
  opaque
{
  assert (x == y) == !(x != y);
  assert (x < y) ==> (x <= y);
  assert (x > y) ==> (x >= y);
  assert (l ^ r) == (l ^ r);
  assert (l < r) ==> (l <= r)
};

Equality requires operands of consistent types and is available at every type. ^ concatenates two strings.

Ordering is available at int, real, bv n for n in 1, 8, 16, 32 and 64 — those comparisons are signed — and at string. On strings it is the lexicographic order over code points, so "ab" < "abc" and "Z" < "a". A comparison whose operands have a type variable type selects no overload and is an ambiguity error, not a default.

One practical caveat about string ordering: the laws that make it an order rather than just a relation — antisymmetry, totality, transitivity — are discharged by z3 and time out under cvc5, so a proof that leans on them wants --solver z3. Everything else about < on strings, including every counterexample, works under either.

Equality means different things at different types, and the difference matters: on a datatype it is structural, and on a composite it is reference identity. See Aliasing and separation.

4.5.4. Bitwise operations🔗

There is no bitwise operator at int. & and | are the eager boolean operators, ^ is string concatenation, and << / >> are not Laurel syntax at all. Bitwise work is done by calling built-in procedures whose names carry the width and the signedness, because a bitwise operation on a bounded integer needs both and an operator spelling could carry neither:

procedure bits(x: int, y: int)
  requires x >= 0
  requires x <= 4294967295
  requires y >= 0
  requires y <= 4294967295
  opaque
{
  assert $bitAndU8(12, 10) == 8;
  assert $bitOrU8(12, 10) == 14;
  assert $bitXorU8(12, 10) == 6;
  assert $bitAndS32(-2, 3) == 2;
  assert $bitXorU32(x, x) == 0;
  assert $bitAndU32(x, y) <= 4294967295
};

$bitAndU8, $bitOrS32, $bitXorU64, … are available as $bit{And,Or,Xor}{S,U}{8,16,32,64}. Each requires both operands to lie in the width's range for that signedness and returns the two's-complement result in the same range. An out-of-range operand is a failed precondition, not a silent truncation, and since a bitwise and/or/xor of two in-range values is itself in range there is no overflow case to report.

Underneath them the bitvector layer is exposed directly, for widths 1 through 128: $bv{W}{And,Or,Xor,Not,Shl,UShr,SShr} on bv W, plus the three conversions $intToBv{W}, $bv{W}ToInt (signed reading) and $bv{W}ToUInt (unsigned). $intToBv{W} truncates to W bits, so a caller using these directly owns the range premise that makes the round trip exact. Note these all reach the solver through SMT-LIB's int_to_bv/ubv_to_int/sbv_to_int, which cvc5 supports and z3 does not; and prefer $bv{W}ToUInt for symbolic reasoning, because a bound on $bv{W}ToInt at width 32 or above is not something the solver discharges in practice.