-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Tools.Polynomial
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Implementation of polynomial arithmetic
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE PatternGuards        #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.Polynomial (
        -- * Polynomial arithmetic and CRCs
        Polynomial(..), crc, crcBV, ites, mdp, addPoly
        ) where

import Data.Bits  (Bits(..))
import Data.List  (genericTake)
import Data.Maybe (fromJust, fromMaybe)
import Data.Word  (Word8, Word16, Word32, Word64)

import Data.SBV.Core.Data
import Data.SBV.Core.Kind
import Data.SBV.Core.Sized
import Data.SBV.Core.Model

import GHC.TypeLits

-- | Implements polynomial addition, multiplication, division, and modulus operations
-- over GF(2^n).  NB. Similar to 'sQuotRem', division by @0@ is interpreted as follows:
--
--     @x `pDivMod` 0 = (0, x)@
--
-- for all @x@ (including @0@)
--
-- Minimal complete definition: 'pMult', 'pDivMod', 'showPolynomial'
class (Num a, Bits a) => Polynomial a where
 -- | Given bit-positions to be set, create a polynomial
 -- For instance
 --
 --     @polynomial [0, 1, 3] :: SWord8@
 -- 
 -- will evaluate to @11@, since it sets the bits @0@, @1@, and @3@. Mathematicians would write this polynomial
 -- as @x^3 + x + 1@. And in fact, 'showPoly' will show it like that.
 polynomial :: [Int] -> a
 -- | Add two polynomials in GF(2^n).
 pAdd  :: a -> a -> a
 -- | Multiply two polynomials in GF(2^n), and reduce it by the irreducible specified by
 -- the polynomial as specified by coefficients of the third argument. Note that the third
 -- argument is specifically left in this form as it is usually in GF(2^(n+1)), which is not available in our
 -- formalism. (That is, we would need SWord9 for SWord8 multiplication, etc.) Also note that we do not
 -- support symbolic irreducibles, which is a minor shortcoming. (Most GF's will come with fixed irreducibles,
 -- so this should not be a problem in practice.)
 --
 -- Passing [] for the third argument will multiply the polynomials and then ignore the higher bits that won't
 -- fit into the resulting size.
 pMult :: (a, a, [Int]) -> a
 -- | Divide two polynomials in GF(2^n), see above note for division by 0.
 pDiv  :: a -> a -> a
 -- | Compute modulus of two polynomials in GF(2^n), see above note for modulus by 0.
 pMod  :: a -> a -> a
 -- | Division and modulus packed together.
 pDivMod :: a -> a -> (a, a)
 -- | Display a polynomial like a mathematician would (over the monomial @x@), with a type.
 showPoly :: a -> String
 -- | Display a polynomial like a mathematician would (over the monomial @x@), the first argument
 -- controls if the final type is shown as well.
 showPolynomial :: Bool -> a -> String

 {-# MINIMAL pMult, pDivMod, showPolynomial #-}
 polynomial = (Int -> a -> a) -> a -> [Int] -> a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((a -> Int -> a) -> Int -> a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Int -> a
forall a. Bits a => a -> Int -> a
setBit) a
0
 pAdd       = a -> a -> a
forall a. Bits a => a -> a -> a
xor
 pDiv a
x a
y   = (a, a) -> a
forall a b. (a, b) -> a
fst (a -> a -> (a, a)
forall a. Polynomial a => a -> a -> (a, a)
pDivMod a
x a
y)
 pMod a
x a
y   = (a, a) -> a
forall a b. (a, b) -> b
snd (a -> a -> (a, a)
forall a. Polynomial a => a -> a -> (a, a)
pDivMod a
x a
y)
 showPoly   = Bool -> a -> String
forall a. Polynomial a => Bool -> a -> String
showPolynomial Bool
False

instance Polynomial Word8   where {showPolynomial :: Bool -> Word8 -> String
showPolynomial   = Bool -> Word8 -> String
forall a. Bits a => Bool -> a -> String
sp;           pMult :: (Word8, Word8, [Int]) -> Word8
pMult = ((SBV Word8, SBV Word8, [Int]) -> SBV Word8)
-> (Word8, Word8, [Int]) -> Word8
forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift (SBV Word8, SBV Word8, [Int]) -> SBV Word8
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word8 -> Word8 -> (Word8, Word8)
pDivMod = (SBV Word8 -> SBV Word8 -> (SBV Word8, SBV Word8))
-> Word8 -> Word8 -> (Word8, Word8)
forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC SBV Word8 -> SBV Word8 -> (SBV Word8, SBV Word8)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial Word16  where {showPolynomial :: Bool -> Word16 -> String
showPolynomial   = Bool -> Word16 -> String
forall a. Bits a => Bool -> a -> String
sp;           pMult :: (Word16, Word16, [Int]) -> Word16
pMult = ((SBV Word16, SBV Word16, [Int]) -> SBV Word16)
-> (Word16, Word16, [Int]) -> Word16
forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift (SBV Word16, SBV Word16, [Int]) -> SBV Word16
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word16 -> Word16 -> (Word16, Word16)
pDivMod = (SBV Word16 -> SBV Word16 -> (SBV Word16, SBV Word16))
-> Word16 -> Word16 -> (Word16, Word16)
forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC SBV Word16 -> SBV Word16 -> (SBV Word16, SBV Word16)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial Word32  where {showPolynomial :: Bool -> Word32 -> String
showPolynomial   = Bool -> Word32 -> String
forall a. Bits a => Bool -> a -> String
sp;           pMult :: (Word32, Word32, [Int]) -> Word32
pMult = ((SBV Word32, SBV Word32, [Int]) -> SBV Word32)
-> (Word32, Word32, [Int]) -> Word32
forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift (SBV Word32, SBV Word32, [Int]) -> SBV Word32
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word32 -> Word32 -> (Word32, Word32)
pDivMod = (SBV Word32 -> SBV Word32 -> (SBV Word32, SBV Word32))
-> Word32 -> Word32 -> (Word32, Word32)
forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC SBV Word32 -> SBV Word32 -> (SBV Word32, SBV Word32)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial Word64  where {showPolynomial :: Bool -> Word64 -> String
showPolynomial   = Bool -> Word64 -> String
forall a. Bits a => Bool -> a -> String
sp;           pMult :: (Word64, Word64, [Int]) -> Word64
pMult = ((SBV Word64, SBV Word64, [Int]) -> SBV Word64)
-> (Word64, Word64, [Int]) -> Word64
forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift (SBV Word64, SBV Word64, [Int]) -> SBV Word64
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word64 -> Word64 -> (Word64, Word64)
pDivMod = (SBV Word64 -> SBV Word64 -> (SBV Word64, SBV Word64))
-> Word64 -> Word64 -> (Word64, Word64)
forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC SBV Word64 -> SBV Word64 -> (SBV Word64, SBV Word64)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord8  where {showPolynomial :: Bool -> SBV Word8 -> String
showPolynomial Bool
b = (Word8 -> String) -> SBV Word8 -> String
forall a. SymVal a => (a -> String) -> SBV a -> String
liftS (Bool -> Word8 -> String
forall a. Bits a => Bool -> a -> String
sp Bool
b); pMult :: (SBV Word8, SBV Word8, [Int]) -> SBV Word8
pMult = (SBV Word8, SBV Word8, [Int]) -> SBV Word8
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult;      pDivMod :: SBV Word8 -> SBV Word8 -> (SBV Word8, SBV Word8)
pDivMod = SBV Word8 -> SBV Word8 -> (SBV Word8, SBV Word8)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord16 where {showPolynomial :: Bool -> SBV Word16 -> String
showPolynomial Bool
b = (Word16 -> String) -> SBV Word16 -> String
forall a. SymVal a => (a -> String) -> SBV a -> String
liftS (Bool -> Word16 -> String
forall a. Bits a => Bool -> a -> String
sp Bool
b); pMult :: (SBV Word16, SBV Word16, [Int]) -> SBV Word16
pMult = (SBV Word16, SBV Word16, [Int]) -> SBV Word16
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult;      pDivMod :: SBV Word16 -> SBV Word16 -> (SBV Word16, SBV Word16)
pDivMod = SBV Word16 -> SBV Word16 -> (SBV Word16, SBV Word16)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord32 where {showPolynomial :: Bool -> SBV Word32 -> String
showPolynomial Bool
b = (Word32 -> String) -> SBV Word32 -> String
forall a. SymVal a => (a -> String) -> SBV a -> String
liftS (Bool -> Word32 -> String
forall a. Bits a => Bool -> a -> String
sp Bool
b); pMult :: (SBV Word32, SBV Word32, [Int]) -> SBV Word32
pMult = (SBV Word32, SBV Word32, [Int]) -> SBV Word32
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult;      pDivMod :: SBV Word32 -> SBV Word32 -> (SBV Word32, SBV Word32)
pDivMod = SBV Word32 -> SBV Word32 -> (SBV Word32, SBV Word32)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord64 where {showPolynomial :: Bool -> SBV Word64 -> String
showPolynomial Bool
b = (Word64 -> String) -> SBV Word64 -> String
forall a. SymVal a => (a -> String) -> SBV a -> String
liftS (Bool -> Word64 -> String
forall a. Bits a => Bool -> a -> String
sp Bool
b); pMult :: (SBV Word64, SBV Word64, [Int]) -> SBV Word64
pMult = (SBV Word64, SBV Word64, [Int]) -> SBV Word64
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult;      pDivMod :: SBV Word64 -> SBV Word64 -> (SBV Word64, SBV Word64)
pDivMod = SBV Word64 -> SBV Word64 -> (SBV Word64, SBV Word64)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}

instance (KnownNat n, BVIsNonZero n) => Polynomial (SWord n) where {showPolynomial :: Bool -> SWord n -> String
showPolynomial Bool
b = (WordN n -> String) -> SWord n -> String
forall a. SymVal a => (a -> String) -> SBV a -> String
liftS (Bool -> WordN n -> String
forall a. Bits a => Bool -> a -> String
sp Bool
b); pMult :: (SWord n, SWord n, [Int]) -> SWord n
pMult = (SWord n, SWord n, [Int]) -> SWord n
forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult;      pDivMod :: SWord n -> SWord n -> (SWord n, SWord n)
pDivMod = SWord n -> SWord n -> (SWord n, SWord n)
forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}

lift :: SymVal a => ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift :: ((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift (SBV a, SBV a, [Int]) -> SBV a
f (a
x, a
y, [Int]
z) = Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe a -> a) -> Maybe a -> a
forall a b. (a -> b) -> a -> b
$ SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral (SBV a -> Maybe a) -> SBV a -> Maybe a
forall a b. (a -> b) -> a -> b
$ (SBV a, SBV a, [Int]) -> SBV a
f (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
x, a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
y, [Int]
z)
liftC :: SymVal a => (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC :: (SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC SBV a -> SBV a -> (SBV a, SBV a)
f a
x a
y = let (SBV a
a, SBV a
b) = SBV a -> SBV a -> (SBV a, SBV a)
f (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
x) (a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
y) in (Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a), Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
b))
liftS :: SymVal a => (a -> String) -> SBV a -> String
liftS :: (a -> String) -> SBV a -> String
liftS a -> String
f SBV a
s
  | Just a
x <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s = a -> String
f a
x
  | Bool
True                  = SBV a -> String
forall a. Show a => a -> String
show SBV a
s

-- | Pretty print as a polynomial
sp :: Bits a => Bool -> a -> String
sp :: Bool -> a -> String
sp Bool
st a
a
 | [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
cs = Char
'0' Char -> String -> String
forall a. a -> [a] -> [a]
: String
t
 | Bool
True    = (Int -> String -> String) -> String -> [Int] -> String
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Int
x String
y -> Int -> String
forall a. (Eq a, Num a, Show a) => a -> String
sh Int
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" + " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y) (Int -> String
forall a. (Eq a, Num a, Show a) => a -> String
sh ([Int] -> Int
forall a. [a] -> a
last [Int]
cs)) ([Int] -> [Int]
forall a. [a] -> [a]
init [Int]
cs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
 where t :: String
t | Bool
st   = String
" :: GF(2^" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
         | Bool
True = String
""
       n :: Int
n  = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Int
forall a. HasCallStack => String -> a
error String
"SBV.Polynomial.sp: Unexpected non-finite usage!") (a -> Maybe Int
forall a. Bits a => a -> Maybe Int
bitSizeMaybe a
a)
       is :: [Int]
is = [Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1, Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2 .. Int
0]
       cs :: [Int]
cs = ((Int, Bool) -> Int) -> [(Int, Bool)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Bool) -> Int
forall a b. (a, b) -> a
fst ([(Int, Bool)] -> [Int]) -> [(Int, Bool)] -> [Int]
forall a b. (a -> b) -> a -> b
$ ((Int, Bool) -> Bool) -> [(Int, Bool)] -> [(Int, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd ([(Int, Bool)] -> [(Int, Bool)]) -> [(Int, Bool)] -> [(Int, Bool)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
is ((Int -> Bool) -> [Int] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit a
a) [Int]
is)
       sh :: a -> String
sh a
0 = String
"1"
       sh a
1 = String
"x"
       sh a
i = String
"x^" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i

-- | Add two polynomials
addPoly :: [SBool] -> [SBool] -> [SBool]
addPoly :: [SBool] -> [SBool] -> [SBool]
addPoly [SBool]
xs    []      = [SBool]
xs
addPoly []    [SBool]
ys      = [SBool]
ys
addPoly (SBool
x:[SBool]
xs) (SBool
y:[SBool]
ys) = SBool
x SBool -> SBool -> SBool
.<+> SBool
y SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [SBool] -> [SBool] -> [SBool]
addPoly [SBool]
xs [SBool]
ys

-- | Run down a boolean condition over two lists. Note that this is
-- different than zipWith as shorter list is assumed to be filled with
-- sFalse at the end (i.e., zero-bits); which nicely pads it when
-- considered as an unsigned number in little-endian form.
ites :: SBool -> [SBool] -> [SBool] -> [SBool]
ites :: SBool -> [SBool] -> [SBool] -> [SBool]
ites SBool
s [SBool]
xs [SBool]
ys
 | Just Bool
t <- SBool -> Maybe Bool
forall a. SymVal a => SBV a -> Maybe a
unliteral SBool
s
 = if Bool
t then [SBool]
xs else [SBool]
ys
 | Bool
True
 = [SBool] -> [SBool] -> [SBool]
go [SBool]
xs [SBool]
ys
 where go :: [SBool] -> [SBool] -> [SBool]
go []     []     = []
       go []     (SBool
b:[SBool]
bs) = SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
s SBool
sFalse SBool
b SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [SBool] -> [SBool] -> [SBool]
go [] [SBool]
bs
       go (SBool
a:[SBool]
as) []     = SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
s SBool
a SBool
sFalse SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [SBool] -> [SBool] -> [SBool]
go [SBool]
as []
       go (SBool
a:[SBool]
as) (SBool
b:[SBool]
bs) = SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
s SBool
a SBool
b SBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
: [SBool] -> [SBool] -> [SBool]
go [SBool]
as [SBool]
bs

-- | Multiply two polynomials and reduce by the third (concrete) irreducible, given by its coefficients.
-- See the remarks for the 'pMult' function for this design choice
polyMult :: SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult :: (SBV a, SBV a, [Int]) -> SBV a
polyMult (SBV a
x, SBV a
y, [Int]
red)
  | SBV a -> Bool
forall a. HasKind a => a -> Bool
isReal SBV a
x
  = String -> SBV a
forall a. HasCallStack => String -> a
error (String -> SBV a) -> String -> SBV a
forall a b. (a -> b) -> a -> b
$ String
"SBV.polyMult: Received a real value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall a. Show a => a -> String
show SBV a
x
  | Bool -> Bool
not (SBV a -> Bool
forall a. HasKind a => a -> Bool
isBounded SBV a
x)
  = String -> SBV a
forall a. HasCallStack => String -> a
error (String -> SBV a) -> String -> SBV a
forall a b. (a -> b) -> a -> b
$ String
"SBV.polyMult: Received infinite precision value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall a. Show a => a -> String
show SBV a
x
  | Bool
True
  = [SBool] -> SBV a
forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsLE ([SBool] -> SBV a) -> [SBool] -> SBV a
forall a b. (a -> b) -> a -> b
$ Int -> [SBool] -> [SBool]
forall i a. Integral i => i -> [a] -> [a]
genericTake Int
sz ([SBool] -> [SBool]) -> [SBool] -> [SBool]
forall a b. (a -> b) -> a -> b
$ [SBool]
r [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ SBool -> [SBool]
forall a. a -> [a]
repeat SBool
sFalse
  where ([SBool]
_, [SBool]
r) = [SBool] -> [SBool] -> ([SBool], [SBool])
mdp [SBool]
ms [SBool]
rs
        ms :: [SBool]
ms = Int -> [SBool] -> [SBool]
forall i a. Integral i => i -> [a] -> [a]
genericTake (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
sz) ([SBool] -> [SBool]) -> [SBool] -> [SBool]
forall a b. (a -> b) -> a -> b
$ [SBool] -> [SBool] -> [SBool] -> [SBool]
mul (SBV a -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastLE SBV a
x) (SBV a -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastLE SBV a
y) [] [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ SBool -> [SBool]
forall a. a -> [a]
repeat SBool
sFalse
        rs :: [SBool]
rs = Int -> [SBool] -> [SBool]
forall i a. Integral i => i -> [a] -> [a]
genericTake (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
sz) ([SBool] -> [SBool]) -> [SBool] -> [SBool]
forall a b. (a -> b) -> a -> b
$ [Bool -> SBool
fromBool (Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
red) |  Int
i <- [Int
0 .. (Int -> Int -> Int) -> Int -> [Int] -> Int
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 [Int]
red] ] [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ SBool -> [SBool]
forall a. a -> [a]
repeat SBool
sFalse
        sz :: Int
sz = SBV a -> Int
forall a. HasKind a => a -> Int
intSizeOf SBV a
x
        mul :: [SBool] -> [SBool] -> [SBool] -> [SBool]
mul [SBool]
_  []     [SBool]
ps = [SBool]
ps
        mul [SBool]
as (SBool
b:[SBool]
bs) [SBool]
ps = [SBool] -> [SBool] -> [SBool] -> [SBool]
mul (SBool
sFalseSBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
:[SBool]
as) [SBool]
bs (SBool -> [SBool] -> [SBool] -> [SBool]
ites SBool
b ([SBool]
as [SBool] -> [SBool] -> [SBool]
`addPoly` [SBool]
ps) [SBool]
ps)

polyDivMod :: SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod :: SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod SBV a
x SBV a
y
   | SBV a -> Bool
forall a. HasKind a => a -> Bool
isReal SBV a
x
   = String -> (SBV a, SBV a)
forall a. HasCallStack => String -> a
error (String -> (SBV a, SBV a)) -> String -> (SBV a, SBV a)
forall a b. (a -> b) -> a -> b
$ String
"SBV.polyDivMod: Received a real value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall a. Show a => a -> String
show SBV a
x
   | Bool -> Bool
not (SBV a -> Bool
forall a. HasKind a => a -> Bool
isBounded SBV a
x)
   = String -> (SBV a, SBV a)
forall a. HasCallStack => String -> a
error (String -> (SBV a, SBV a)) -> String -> (SBV a, SBV a)
forall a b. (a -> b) -> a -> b
$ String
"SBV.polyDivMod: Received infinite precision value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall a. Show a => a -> String
show SBV a
x
   | Bool
True
   = SBool -> (SBV a, SBV a) -> (SBV a, SBV a) -> (SBV a, SBV a)
forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
y SBV a -> SBV a -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV a
0) (SBV a
0, SBV a
x) ([SBool] -> SBV a
adjust [SBool]
d, [SBool] -> SBV a
adjust [SBool]
r)
   where adjust :: [SBool] -> SBV a
adjust [SBool]
xs = [SBool] -> SBV a
forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsLE ([SBool] -> SBV a) -> [SBool] -> SBV a
forall a b. (a -> b) -> a -> b
$ Int -> [SBool] -> [SBool]
forall i a. Integral i => i -> [a] -> [a]
genericTake Int
sz ([SBool] -> [SBool]) -> [SBool] -> [SBool]
forall a b. (a -> b) -> a -> b
$ [SBool]
xs [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ SBool -> [SBool]
forall a. a -> [a]
repeat SBool
sFalse
         sz :: Int
sz        = SBV a -> Int
forall a. HasKind a => a -> Int
intSizeOf SBV a
x
         ([SBool]
d, [SBool]
r)    = [SBool] -> [SBool] -> ([SBool], [SBool])
mdp (SBV a -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastLE SBV a
x) (SBV a -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastLE SBV a
y)

-- conservative over-approximation of the degree
degree :: [SBool] -> Int
degree :: [SBool] -> Int
degree [SBool]
xs = Int -> [SBool] -> Int
forall t. Num t => t -> [SBool] -> t
walk ([SBool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBool]
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ([SBool] -> Int) -> [SBool] -> Int
forall a b. (a -> b) -> a -> b
$ [SBool] -> [SBool]
forall a. [a] -> [a]
reverse [SBool]
xs
  where walk :: t -> [SBool] -> t
walk t
n []     = t
n
        walk t
n (SBool
b:[SBool]
bs)
         | Just Bool
t <- SBool -> Maybe Bool
forall a. SymVal a => SBV a -> Maybe a
unliteral SBool
b
         = if Bool
t then t
n else t -> [SBool] -> t
walk (t
nt -> t -> t
forall a. Num a => a -> a -> a
-t
1) [SBool]
bs
         | Bool
True
         = t
n -- over-estimate

-- | Compute modulus/remainder of polynomials on bit-vectors.
mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
mdp [SBool]
xs [SBool]
ys = Int -> [SBool] -> ([SBool], [SBool])
go ([SBool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBool]
ys Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ([SBool] -> [SBool]
forall a. [a] -> [a]
reverse [SBool]
ys)
  where degTop :: Int
degTop  = [SBool] -> Int
degree [SBool]
xs
        go :: Int -> [SBool] -> ([SBool], [SBool])
go Int
_ []     = String -> ([SBool], [SBool])
forall a. HasCallStack => String -> a
error String
"SBV.Polynomial.mdp: Impossible happened; exhausted ys before hitting 0"
        go Int
n (SBool
b:[SBool]
bs)
         | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0   = ([SBool] -> [SBool]
forall a. [a] -> [a]
reverse [SBool]
qs, [SBool]
rs)
         | Bool
True     = let ([SBool]
rqs, [SBool]
rrs) = Int -> [SBool] -> ([SBool], [SBool])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [SBool]
bs
                      in (SBool -> [SBool] -> [SBool] -> [SBool]
ites SBool
b ([SBool] -> [SBool]
forall a. [a] -> [a]
reverse [SBool]
qs) [SBool]
rqs, SBool -> [SBool] -> [SBool] -> [SBool]
ites SBool
b [SBool]
rs [SBool]
rrs)
         where degQuot :: Int
degQuot = Int
degTop Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n
               ys' :: [SBool]
ys' = Int -> SBool -> [SBool]
forall a. Int -> a -> [a]
replicate Int
degQuot SBool
sFalse [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ [SBool]
ys
               ([SBool]
qs, [SBool]
rs) = Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
divx (Int
degQuotInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int
degTop [SBool]
xs [SBool]
ys'

-- return the element at index i; if not enough elements, return sFalse
-- N.B. equivalent to '(xs ++ repeat sFalse) !! i', but more efficient
idx :: [SBool] -> Int -> SBool
idx :: [SBool] -> Int -> SBool
idx []     Int
_ = SBool
sFalse
idx (SBool
x:[SBool]
_)  Int
0 = SBool
x
idx (SBool
_:[SBool]
xs) Int
i = [SBool] -> Int -> SBool
idx [SBool]
xs (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
divx :: Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
divx Int
n Int
_ [SBool]
xs [SBool]
_ | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = ([], [SBool]
xs)
divx Int
n Int
i [SBool]
xs [SBool]
ys'        = (SBool
qSBool -> [SBool] -> [SBool]
forall a. a -> [a] -> [a]
:[SBool]
qs, [SBool]
rs)
  where q :: SBool
q        = [SBool]
xs [SBool] -> Int -> SBool
`idx` Int
i
        xs' :: [SBool]
xs'      = SBool -> [SBool] -> [SBool] -> [SBool]
ites SBool
q ([SBool]
xs [SBool] -> [SBool] -> [SBool]
`addPoly` [SBool]
ys') [SBool]
xs
        ([SBool]
qs, [SBool]
rs) = Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
divx (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [SBool]
xs' ([SBool] -> [SBool]
forall a. [a] -> [a]
tail [SBool]
ys')

-- | Compute CRCs over bit-vectors. The call @crcBV n m p@ computes
-- the CRC of the message @m@ with respect to polynomial @p@. The
-- inputs are assumed to be blasted big-endian. The number
-- @n@ specifies how many bits of CRC is needed. Note that @n@
-- is actually the degree of the polynomial @p@, and thus it seems
-- redundant to pass it in. However, in a typical proof context,
-- the polynomial can be symbolic, so we cannot compute the degree
-- easily. While this can be worked-around by generating code that
-- accounts for all possible degrees, the resulting code would
-- be unnecessarily big and complicated, and much harder to reason
-- with. (Also note that a CRC is just the remainder from the
-- polynomial division, but this routine is much faster in practice.)
--
-- NB. The @n@th bit of the polynomial @p@ /must/ be set for the CRC
-- to be computed correctly. Note that the polynomial argument @p@ will
-- not even have this bit present most of the time, as it will typically
-- contain bits @0@ through @n-1@ as usual in the CRC literature. The higher
-- order @n@th bit is simply assumed to be set, as it does not make
-- sense to use a polynomial of a lesser degree. This is usually not a problem
-- since CRC polynomials are designed and expressed this way.
--
-- NB. The literature on CRC's has many variants on how CRC's are computed.
-- We follow the following simple procedure:
--
--     * Extend the message @m@ by adding @n@ 0 bits on the right
--
--     * Divide the polynomial thus obtained by the @p@
--
--     * The remainder is the CRC value.
--
-- There are many variants on final XOR's, reversed polynomials etc., so
-- it is essential to double check you use the correct /algorithm/.
crcBV :: Int -> [SBool] -> [SBool] -> [SBool]
crcBV :: Int -> [SBool] -> [SBool] -> [SBool]
crcBV Int
n [SBool]
m [SBool]
p = Int -> [SBool] -> [SBool]
forall a. Int -> [a] -> [a]
take Int
n ([SBool] -> [SBool]) -> [SBool] -> [SBool]
forall a b. (a -> b) -> a -> b
$ [SBool] -> [SBool] -> [SBool]
go (Int -> SBool -> [SBool]
forall a. Int -> a -> [a]
replicate Int
n SBool
sFalse) ([SBool]
m [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ Int -> SBool -> [SBool]
forall a. Int -> a -> [a]
replicate Int
n SBool
sFalse)
  where mask :: [SBool]
mask = Int -> [SBool] -> [SBool]
forall a. Int -> [a] -> [a]
drop ([SBool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBool]
p Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) [SBool]
p
        go :: [SBool] -> [SBool] -> [SBool]
go [SBool]
c []     = [SBool]
c
        go [SBool]
c (SBool
b:[SBool]
bs) = [SBool] -> [SBool] -> [SBool]
go [SBool]
next [SBool]
bs
          where c' :: [SBool]
c' = Int -> [SBool] -> [SBool]
forall a. Int -> [a] -> [a]
drop Int
1 [SBool]
c [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ [SBool
b]
                next :: [SBool]
next = SBool -> [SBool] -> [SBool] -> [SBool]
forall a. Mergeable a => SBool -> a -> a -> a
ite ([SBool] -> SBool
forall a. [a] -> a
head [SBool]
c) ((SBool -> SBool -> SBool) -> [SBool] -> [SBool] -> [SBool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SBool -> SBool -> SBool
(.<+>) [SBool]
c' [SBool]
mask) [SBool]
c'

-- | Compute CRC's over polynomials, i.e., symbolic words. The first
-- 'Int' argument plays the same role as the one in the 'crcBV' function.
crc :: (SFiniteBits a, SFiniteBits b) => Int -> SBV a -> SBV b -> SBV b
crc :: Int -> SBV a -> SBV b -> SBV b
crc Int
n SBV a
m SBV b
p
  | SBV a -> Bool
forall a. HasKind a => a -> Bool
isReal SBV a
m Bool -> Bool -> Bool
|| SBV b -> Bool
forall a. HasKind a => a -> Bool
isReal SBV b
p
  = String -> SBV b
forall a. HasCallStack => String -> a
error (String -> SBV b) -> String -> SBV b
forall a b. (a -> b) -> a -> b
$ String
"SBV.crc: Received a real value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SBV a, SBV b) -> String
forall a. Show a => a -> String
show (SBV a
m, SBV b
p)
  | Bool -> Bool
not (SBV a -> Bool
forall a. HasKind a => a -> Bool
isBounded SBV a
m) Bool -> Bool -> Bool
|| Bool -> Bool
not (SBV b -> Bool
forall a. HasKind a => a -> Bool
isBounded SBV b
p)
  = String -> SBV b
forall a. HasCallStack => String -> a
error (String -> SBV b) -> String -> SBV b
forall a b. (a -> b) -> a -> b
$ String
"SBV.crc: Received an infinite precision value: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SBV a, SBV b) -> String
forall a. Show a => a -> String
show (SBV a
m, SBV b
p)
  | Bool
True
  = [SBool] -> SBV b
forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE ([SBool] -> SBV b) -> [SBool] -> SBV b
forall a b. (a -> b) -> a -> b
$ Int -> SBool -> [SBool]
forall a. Int -> a -> [a]
replicate (Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) SBool
sFalse [SBool] -> [SBool] -> [SBool]
forall a. [a] -> [a] -> [a]
++ Int -> [SBool] -> [SBool] -> [SBool]
crcBV Int
n (SBV a -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SBV a
m) (SBV b -> [SBool]
forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SBV b
p)
  where sz :: Int
sz = SBV b -> Int
forall a. HasKind a => a -> Int
intSizeOf SBV b
p