verus
forked from verus-lang/verus
Star 0
Fork 0
Watch
verus source docs guide src spec-arithmetic.md
4.7 kB · 100 lines
Markdown
at master

Arithmetic in spec code #

Note: This reference page is about arithmetic in Verus specification code. This page does not apply to arithmetic in executable Rust code.

For an introduction to Verus arithmetic, see Integers and arithmetic.

Syntax #

V@[arith_expr] ::= V@[spec_expr] \+ V@[spec_expr]
             | V@[spec_expr] - V@[spec_expr]
             | - V@[spec_expr]
             | V@[spec_expr] \* V@[spec_expr]
             | V@[spec_expr] / V@[spec_expr]
             | V@[spec_expr] % V@[spec_expr]

V@[ineq_expr] ::= | V@[spec_expr] <= V@[spec_expr]
              | V@[spec_expr] <  V@[spec_expr]
              | V@[spec_expr] >= V@[spec_expr]
              | V@[spec_expr] >  V@[spec_expr]

Typing #

In spec code, the results of arithmetic are automatically widened to avoid overflow or wrapping. The types of various operators, given as functions of the input types, are summarized in the below table. Note that in most cases, the types of the inputs are not required to be the same.

operation LHS type RHS type result type notes
<= < >= > t1 t2 bool
+ t1 t2 int except for nat + nat
+ nat nat nat
- t1 t2 int
* t1 t2 int except for nat * nat
* nat nat nat
/ t t int for i8...isize, int
/ t t t for u8...usize, nat
% t t t
add(_, _) t t t
sub(_, _) t t t
mul(_, _) t t t

Semantics #

Due to type-widening, the result of any arithmetic operator is the exact result of the arithmetic without any consideration for overflow or truncation, with the exception of the named add, sub, and mul operators, which truncate.

Quotient and remainder. In Verus specifications, / and % are defined by Euclidean division.

For b != 0, the quotient a / b and remainder a % b are defined as the unique integers q and r such that:

  • b * q + r == a
  • 0 <= r < |b|.

Note that:

  • The remainder a % b is always nonnegative
  • The quotient is "floor division" when b is positive
  • The quotient is "ceiling division" when b is negative

Also note that a / b and a % b are unspecified when b == 0. However, because all spec functions are total, division-by-0 or mod-by-0 are not hard errors.

[!DIFF] The / and % in spec code may differ from Rust's / and % operators in executable code when the left operand is negative.

For /:

Verus spec / (Euclidean) Rust /
7 / 3 2 2
7 / (-3) -2 -2
(-7) / 3 -3 -2
(-7) / (-3) 3 2

For %:

Verus spec % (Euclidean) Rust %
7 % 3 1 1
7 % (-3) 1 1
(-7) % 3 2 -1
(-7) % (-3) 2 -1

More advanced arithmetic #

The Verus standard library includes the following additional arithmetic functions usable in spec expressions: