-----------------------------------------------------------------------------
-- |
-- 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Bits a => a -> Int -> a
setBit) a
0
 pAdd       = forall a. Bits a => a -> a -> a
xor
 pDiv a
x a
y   = forall a b. (a, b) -> a
fst (forall a. Polynomial a => a -> a -> (a, a)
pDivMod a
x a
y)
 pMod a
x a
y   = forall a b. (a, b) -> b
snd (forall a. Polynomial a => a -> a -> (a, a)
pDivMod a
x a
y)
 showPoly   = forall a. Polynomial a => Bool -> a -> String
showPolynomial Bool
False

instance Polynomial Word8   where {showPolynomial :: Bool -> Word8 -> String
showPolynomial   = forall a. Bits a => Bool -> a -> String
sp;           pMult :: (Word8, Word8, [Int]) -> Word8
pMult = forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word8 -> Word8 -> (Word8, Word8)
pDivMod = forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial Word16  where {showPolynomial :: Bool -> Word16 -> String
showPolynomial   = forall a. Bits a => Bool -> a -> String
sp;           pMult :: (Word16, Word16, [Int]) -> Word16
pMult = forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word16 -> Word16 -> (Word16, Word16)
pDivMod = forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial Word32  where {showPolynomial :: Bool -> Word32 -> String
showPolynomial   = forall a. Bits a => Bool -> a -> String
sp;           pMult :: (Word32, Word32, [Int]) -> Word32
pMult = forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word32 -> Word32 -> (Word32, Word32)
pDivMod = forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial Word64  where {showPolynomial :: Bool -> Word64 -> String
showPolynomial   = forall a. Bits a => Bool -> a -> String
sp;           pMult :: (Word64, Word64, [Int]) -> Word64
pMult = forall a.
SymVal a =>
((SBV a, SBV a, [Int]) -> SBV a) -> (a, a, [Int]) -> a
lift forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult; pDivMod :: Word64 -> Word64 -> (Word64, Word64)
pDivMod = forall a.
SymVal a =>
(SBV a -> SBV a -> (SBV a, SBV a)) -> a -> a -> (a, a)
liftC forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord8  where {showPolynomial :: Bool -> SWord8 -> String
showPolynomial Bool
b = forall a. SymVal a => (a -> String) -> SBV a -> String
liftS (forall a. Bits a => Bool -> a -> String
sp Bool
b); pMult :: (SWord8, SWord8, [Int]) -> SWord8
pMult = forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult;      pDivMod :: SWord8 -> SWord8 -> (SWord8, SWord8)
pDivMod = forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord16 where {showPolynomial :: Bool -> SWord16 -> String
showPolynomial Bool
b = forall a. SymVal a => (a -> String) -> SBV a -> String
liftS (forall a. Bits a => Bool -> a -> String
sp Bool
b); pMult :: (SWord16, SWord16, [Int]) -> SWord16
pMult = forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult;      pDivMod :: SWord16 -> SWord16 -> (SWord16, SWord16)
pDivMod = forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord32 where {showPolynomial :: Bool -> SWord32 -> String
showPolynomial Bool
b = forall a. SymVal a => (a -> String) -> SBV a -> String
liftS (forall a. Bits a => Bool -> a -> String
sp Bool
b); pMult :: (SWord32, SWord32, [Int]) -> SWord32
pMult = forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult;      pDivMod :: SWord32 -> SWord32 -> (SWord32, SWord32)
pDivMod = forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod}
instance Polynomial SWord64 where {showPolynomial :: Bool -> SWord64 -> String
showPolynomial Bool
b = forall a. SymVal a => (a -> String) -> SBV a -> String
liftS (forall a. Bits a => Bool -> a -> String
sp Bool
b); pMult :: (SWord64, SWord64, [Int]) -> SWord64
pMult = forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult;      pDivMod :: SWord64 -> SWord64 -> (SWord64, SWord64)
pDivMod = 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 = forall a. SymVal a => (a -> String) -> SBV a -> String
liftS (forall a. Bits a => Bool -> a -> String
sp Bool
b); pMult :: (SWord n, SWord n, [Int]) -> SWord n
pMult = forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult;      pDivMod :: SWord n -> SWord n -> (SWord n, SWord n)
pDivMod = 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 :: forall a.
SymVal a =>
((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) = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral forall a b. (a -> b) -> a -> b
$ (SBV a, SBV a, [Int]) -> SBV a
f (forall a. SymVal a => a -> SBV a
literal a
x, 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 :: forall a.
SymVal a =>
(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 (forall a. SymVal a => a -> SBV a
literal a
x) (forall a. SymVal a => a -> SBV a
literal a
y) in (forall a. HasCallStack => Maybe a -> a
fromJust (forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
a), forall a. HasCallStack => Maybe a -> a
fromJust (forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
b))
liftS :: SymVal a => (a -> String) -> SBV a -> String
liftS :: forall a. SymVal a => (a -> String) -> SBV a -> String
liftS a -> String
f SBV a
s
  | Just a
x <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s = a -> String
f a
x
  | Bool
True                  = forall a. Show a => a -> String
show SBV a
s

-- | Pretty print as a polynomial
sp :: Bits a => Bool -> a -> String
sp :: forall a. Bits a => Bool -> a -> String
sp Bool
st a
a
 | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
cs = Char
'0' forall a. a -> [a] -> [a]
: String
t
 | Bool
True    = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Int
x String
y -> forall {a}. (Eq a, Num a, Show a) => a -> String
sh Int
x forall a. [a] -> [a] -> [a]
++ String
" + " forall a. [a] -> [a] -> [a]
++ String
y) (forall {a}. (Eq a, Num a, Show a) => a -> String
sh (forall a. [a] -> a
last [Int]
cs)) (forall a. [a] -> [a]
init [Int]
cs) forall a. [a] -> [a] -> [a]
++ String
t
 where t :: String
t | Bool
st   = String
" :: GF(2^" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
")"
         | Bool
True = String
""
       n :: Int
n  = forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
error String
"SBV.Polynomial.sp: Unexpected non-finite usage!") (forall a. Bits a => a -> Maybe Int
bitSizeMaybe a
a)
       is :: [Int]
is = [Int
nforall a. Num a => a -> a -> a
-Int
1, Int
nforall a. Num a => a -> a -> a
-Int
2 .. Int
0]
       cs :: [Int]
cs = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
is (forall a b. (a -> b) -> [a] -> [b]
map (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^" forall a. [a] -> [a] -> [a]
++ 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 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 <- 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) = forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
s SBool
sFalse SBool
b forall a. a -> [a] -> [a]
: [SBool] -> [SBool] -> [SBool]
go [] [SBool]
bs
       go (SBool
a:[SBool]
as) []     = forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
s SBool
a SBool
sFalse forall a. a -> [a] -> [a]
: [SBool] -> [SBool] -> [SBool]
go [SBool]
as []
       go (SBool
a:[SBool]
as) (SBool
b:[SBool]
bs) = forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
s SBool
a SBool
b 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 :: forall a. SFiniteBits a => (SBV a, SBV a, [Int]) -> SBV a
polyMult (SBV a
x, SBV a
y, [Int]
red)
  | forall a. HasKind a => a -> Bool
isReal SBV a
x
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.polyMult: Received a real value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SBV a
x
  | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded SBV a
x)
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.polyMult: Received infinite precision value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SBV a
x
  | Bool
True
  = forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsLE forall a b. (a -> b) -> a -> b
$ forall i a. Integral i => i -> [a] -> [a]
genericTake Int
sz forall a b. (a -> b) -> a -> b
$ [SBool]
r forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat SBool
sFalse
  where ([SBool]
_, [SBool]
r) = [SBool] -> [SBool] -> ([SBool], [SBool])
mdp [SBool]
ms [SBool]
rs
        ms :: [SBool]
ms = forall i a. Integral i => i -> [a] -> [a]
genericTake (Int
2forall a. Num a => a -> a -> a
*Int
sz) forall a b. (a -> b) -> a -> b
$ [SBool] -> [SBool] -> [SBool] -> [SBool]
mul (forall a. SFiniteBits a => SBV a -> [SBool]
blastLE SBV a
x) (forall a. SFiniteBits a => SBV a -> [SBool]
blastLE SBV a
y) [] forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat SBool
sFalse
        rs :: [SBool]
rs = forall i a. Integral i => i -> [a] -> [a]
genericTake (Int
2forall a. Num a => a -> a -> a
*Int
sz) forall a b. (a -> b) -> a -> b
$ [Bool -> SBool
fromBool (Int
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
red) |  Int
i <- [Int
0 .. forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Ord a => a -> a -> a
max Int
0 [Int]
red] ] forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat SBool
sFalse
        sz :: Int
sz = 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
sFalseforall 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 :: forall a. SFiniteBits a => SBV a -> SBV a -> (SBV a, SBV a)
polyDivMod SBV a
x SBV a
y
   | forall a. HasKind a => a -> Bool
isReal SBV a
x
   = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.polyDivMod: Received a real value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SBV a
x
   | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded SBV a
x)
   = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.polyDivMod: Received infinite precision value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SBV a
x
   | Bool
True
   = forall a. Mergeable a => SBool -> a -> a -> a
ite (SBV a
y 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 = forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsLE forall a b. (a -> b) -> a -> b
$ forall i a. Integral i => i -> [a] -> [a]
genericTake Int
sz forall a b. (a -> b) -> a -> b
$ [SBool]
xs forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat SBool
sFalse
         sz :: Int
sz        = forall a. HasKind a => a -> Int
intSizeOf SBV a
x
         ([SBool]
d, [SBool]
r)    = [SBool] -> [SBool] -> ([SBool], [SBool])
mdp (forall a. SFiniteBits a => SBV a -> [SBool]
blastLE SBV a
x) (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 = forall {t}. Num t => t -> [SBool] -> t
walk (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBool]
xs forall a. Num a => a -> a -> a
- Int
1) forall a b. (a -> b) -> a -> b
$ 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 <- forall a. SymVal a => SBV a -> Maybe a
unliteral SBool
b
         = if Bool
t then t
n else t -> [SBool] -> t
walk (t
nforall 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 (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBool]
ys forall a. Num a => a -> a -> a
- Int
1) (forall a. [a] -> [a]
reverse [SBool]
ys)
  where degTop :: Int
degTop  = [SBool] -> Int
degree [SBool]
xs
        go :: Int -> [SBool] -> ([SBool], [SBool])
go Int
_ []     = 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 forall a. Eq a => a -> a -> Bool
== Int
0   = (forall a. [a] -> [a]
reverse [SBool]
qs, [SBool]
rs)
         | Bool
True     = let ([SBool]
rqs, [SBool]
rrs) = Int -> [SBool] -> ([SBool], [SBool])
go (Int
nforall a. Num a => a -> a -> a
-Int
1) [SBool]
bs
                      in (SBool -> [SBool] -> [SBool] -> [SBool]
ites SBool
b (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 forall a. Num a => a -> a -> a
- Int
n
               ys' :: [SBool]
ys' = forall a. Int -> a -> [a]
replicate Int
degQuot SBool
sFalse forall a. [a] -> [a] -> [a]
++ [SBool]
ys
               ([SBool]
qs, [SBool]
rs) = Int -> Int -> [SBool] -> [SBool] -> ([SBool], [SBool])
divx (Int
degQuotforall 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
iforall 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 forall a. Ord a => a -> a -> Bool
<= Int
0 = ([], [SBool]
xs)
divx Int
n Int
i [SBool]
xs [SBool]
ys'        = (SBool
qforall 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
nforall a. Num a => a -> a -> a
-Int
1) (Int
iforall a. Num a => a -> a -> a
-Int
1) [SBool]
xs' (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 = forall a. Int -> [a] -> [a]
take Int
n forall a b. (a -> b) -> a -> b
$ [SBool] -> [SBool] -> [SBool]
go (forall a. Int -> a -> [a]
replicate Int
n SBool
sFalse) ([SBool]
m forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate Int
n SBool
sFalse)
  where mask :: [SBool]
mask = forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBool]
p 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' = forall a. Int -> [a] -> [a]
drop Int
1 [SBool]
c forall a. [a] -> [a] -> [a]
++ [SBool
b]
                next :: [SBool]
next = forall a. Mergeable a => SBool -> a -> a -> a
ite (forall a. [a] -> a
head [SBool]
c) (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 :: forall a b.
(SFiniteBits a, SFiniteBits b) =>
Int -> SBV a -> SBV b -> SBV b
crc Int
n SBV a
m SBV b
p
  | forall a. HasKind a => a -> Bool
isReal SBV a
m Bool -> Bool -> Bool
|| forall a. HasKind a => a -> Bool
isReal SBV b
p
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.crc: Received a real value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (SBV a
m, SBV b
p)
  | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded SBV a
m) Bool -> Bool -> Bool
|| Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded SBV b
p)
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.crc: Received an infinite precision value: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (SBV a
m, SBV b
p)
  | Bool
True
  = forall a. SFiniteBits a => [SBool] -> SBV a
fromBitsBE forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate (Int
sz forall a. Num a => a -> a -> a
- Int
n) SBool
sFalse forall a. [a] -> [a] -> [a]
++ Int -> [SBool] -> [SBool] -> [SBool]
crcBV Int
n (forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SBV a
m) (forall a. SFiniteBits a => SBV a -> [SBool]
blastBE SBV b
p)
  where sz :: Int
sz = forall a. HasKind a => a -> Int
intSizeOf SBV b
p