div package:sbv

Division.

Division overflow. Only signed, since unsigned division does not overflow.

The state for the division program, parameterized over a base type a.

The SDivisible class captures the essence of division. Unfortunately we cannot use Haskell's Integral class since the Real and Enum superclasses are not implementable for symbolic bit-vectors. However, quotRem and divMod both make perfect sense, and the SDivisible class captures this operation. One issue is how division by 0 behaves. The verification technology requires total functions, and there are several design choices here. We follow Isabelle/HOL approach of assigning the value 0 for division by 0. Therefore, we impose the following pair of laws:

x sQuotRem 0 = (0, x)
x sDivMod  0 = (0, x)

Note that our instances implement this law even when x is 0 itself. NB. quot truncates toward zero, while div truncates toward negative infinity.

C code generation of division operations

In the case of division or modulo of a minimal signed value (e.g. -128 for SInt8) by -1, SMTLIB and Haskell agree on what the result should be. Unfortunately the result in C code depends on CPU architecture and compiler settings, as this is undefined behaviour in C. **SBV does not guarantee** what will happen in generated C code in this corner case.

Divide two floating point values, using the given rounding mode

Does the concrete positive number n divide the given integer?

Euclidian division.

Euclidian division and modulus.

Division.

Bit-vector division. Unsigned division neither underflows nor overflows. Signed division can only overflow. In fact, for each signed bitvector type, there's precisely one pair that overflows, when x is minBound and y is -1:

>>> allSat $ \x y -> x `bvDivO` (y::SInt8)
Solution #1:
s0 = -128 :: Int8
s1 =   -1 :: Int8
This is the only solution.

Divide two polynomials in GF(2^n), see above note for division by 0.

Division and modulus packed together.

Demonstrates SBV's assertion checking facilities

A simple variant of division, where we explicitly require the caller to make sure the divisor is not 0.

States that the usual multiplication rule holds over GF(2^n) polynomials Checks:

if (a, b) = x pDivMod y then x = y pMult a + b

being careful about y = 0. When divisor is 0, then quotient is defined to be 0 and the remainder is the numerator. (Note that addition is simply xor in GF(2^8).)

Symbolic version of the constructor Divide.

Prove that 2n^2 + n + 1 is not divisible by 3. We have:

>>> notDiv3
Lemma: notDiv3
Step: 1 (3 way case split)
Step: 1.1                           Q.E.D.
Step: 1.2                           Q.E.D.
Step: 1.3                           Q.E.D.
Step: 1.Completeness                Q.E.D.
Result:                               Q.E.D.
[Proven] notDiv3 :: Ɐn ∷ Integer → Bool

Proof

>>> runCached powerOfThreeMod13VarDivisor
Inductive lemma: onePower
Step: Base                            Q.E.D.
Step: 1 (unfold power)                Q.E.D.
Step: 2                               Q.E.D.
Result:                               Q.E.D.
Inductive lemma: modAddMultiple
Step: Base                            Q.E.D.
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Result:                               Q.E.D.
Lemma: modAddRight
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Result:                               Q.E.D.
Lemma: modAddLeft
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Result:                               Q.E.D.
Cached: modAddMultiple                  Q.E.D.
Cached: modAddRight                     Q.E.D.
Inductive lemma: modMulRightNonneg
Step: Base                            Q.E.D.
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Step: 4                               Q.E.D.
Step: 5                               Q.E.D.
Step: 6                               Q.E.D.
Result:                               Q.E.D.
Cached: modAddMultiple                  Q.E.D.
Cached: modAddRight                     Q.E.D.
Cached: modAddLeft                      Q.E.D.
Cached: modAddMultiple                  Q.E.D.
Lemma: modSubRight
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Result:                               Q.E.D.
Inductive lemma: modMulRightNeg
Step: Base                            Q.E.D.
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Step: 4                               Q.E.D.
Step: 5                               Q.E.D.
Step: 6                               Q.E.D.
Result:                               Q.E.D.
Lemma: modMulRight
Step: 1 (2 way case split)
Step: 1.1                           Q.E.D.
Step: 1.2.1                         Q.E.D.
Step: 1.2.2                         Q.E.D.
Step: 1.2.3                         Q.E.D.
Step: 1.Completeness                Q.E.D.
Result:                               Q.E.D.
Lemma: modMulLeft
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Result:                               Q.E.D.
Cached: modAddMultiple                  Q.E.D.
Cached: modAddRight                     Q.E.D.
Cached: modAddLeft                      Q.E.D.
Cached: modAddMultiple                  Q.E.D.
Cached: modAddRight                     Q.E.D.
Cached: modMulRightNonneg               Q.E.D.
Cached: modAddMultiple                  Q.E.D.
Cached: modAddRight                     Q.E.D.
Cached: modAddLeft                      Q.E.D.
Cached: modAddMultiple                  Q.E.D.
Cached: modSubRight                     Q.E.D.
Cached: modMulRightNeg                  Q.E.D.
Cached: modMulRight                     Q.E.D.
Inductive lemma: powerModInduct
Step: Base                            Q.E.D.
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Step: 4                               Q.E.D.
Step: 5                               Q.E.D.
Step: 6                               Q.E.D.
Result:                               Q.E.D.
Lemma: powerMod                         Q.E.D.
Lemma: powerOf27
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Step: 4                               Q.E.D.
Result:                               Q.E.D.
Lemma: powerOfThreeMod13VarDivisor
Step: 1                               Q.E.D.
Result:                               Q.E.D.
[Proven. Cached: modAddLeft, modAddMultiple, modAddRight, modMulRight] powerOfThreeMod13VarDivisor :: Ɐn ∷ Integer → Ɐm ∷ Integer → Bool

Proof of correctness of an imperative integer division algorithm, using weakest preconditions. The algorithm simply keeps subtracting the divisor until the desired quotient and the remainder is found.