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. Note that unlike regular division, Euclidian division by 0 is unconstrained. i.e., it can take any value whatsoever.

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

GCD of two numbers divide these numbers. This is part one of the proof, where we are not concerned with maximality. Our goal is to show that the calculated gcd divides both inputs.

Proof

>>> runTP gcdDivides
Lemma: dvdAbs                           Q.E.D.
Lemma: helper
Step: 1                               Q.E.D.
Result:                               Q.E.D.
Inductive lemma (strong): dvdNGCD
Step: Measure is non-negative         Q.E.D.
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.Completeness                Q.E.D.
Result:                               Q.E.D.
Lemma: gcdDivides                       Q.E.D.
[Proven] gcdDivides :: Ɐa ∷ Integer → Ɐb ∷ 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