verus
forked from verus-lang/verus
Star 0
Fork 0
Watch
verus source docs guide src reference-prover-mode-integer-ring.md
1.0 kB · 33 lines
Markdown
at master

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.