The integer_ring solver

Note

The integer_ring solver requires the Singular tool to be installed. This is not included by default in the Verus binary release. See the installation details.

Tip

See the guide page for practical tips on using the integer_ring solver.

Methods of invocation

As a proof function. The integer_ring solver can be invoked with a by(integer_ring) on a proof function.

proof fn example(...) by(integer_ring)
    requires P
    ensures Q
{ }

This proves P ==> Q via the integer_ring solver.

Supported predicates

The integer_ring mode only supports basic arithmetic (+, -, *, %, and /) and the comparisons == and !=.

Verus checks that the requires clauses state that all divisors are nonzero.

Solver operation

The given predicate is reduced to an integer ring problem, which is proved by the Singular theorem prover.