    -- |
    -- Module      :  Cryptol.Backend.Concrete
    -- Copyright   :  (c) 2013-2020 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE BangPatterns #-}
    {-# LANGUAGE BlockArguments #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE NamedFieldPuns #-}
    {-# LANGUAGE PatternGuards #-}
    {-# LANGUAGE Rank2Types #-}
    {-# LANGUAGE RecordWildCards #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TupleSections #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE ViewPatterns #-}
    module Cryptol.Backend.Concrete
      ( BV(..)
      , binBV
      , unaryBV
      , bvVal
      , ppBV
      , mkBv
      , mask
      , signedBV
      , signedValue
      , integerToChar
      , lg2
      , Concrete(..)
      , liftBinIntMod
      , fpBinArith
      , fpRoundMode
      ) where

    import qualified Control.Exception as X
    import Data.Bits
    import Data.Ratio
    import Numeric (showIntAtBase)
    import qualified LibBF as FP
    import qualified GHC.Num.Compat as Integer

    import qualified Cryptol.Backend.Arch as Arch
    import qualified Cryptol.Backend.FloatHelpers as FP
    import Cryptol.Backend
    import Cryptol.Backend.Monad
    import Cryptol.TypeCheck.Solver.InfNat (genLog)
    import Cryptol.Utils.Panic (panic)
    import Cryptol.Utils.PP

    data Concrete = Concrete deriving Int -> Concrete -> ShowS
    [Concrete] -> ShowS
    Concrete -> String
    (Int -> Concrete -> ShowS)
    -> (Concrete -> String) -> ([Concrete] -> ShowS) -> Show Concrete
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Concrete -> ShowS
    showsPrec :: Int -> Concrete -> ShowS
    $cshow :: Concrete -> String
    show :: Concrete -> String
    $cshowList :: [Concrete] -> ShowS
    showList :: [Concrete] -> ShowS
    Show

    -- | Concrete bitvector values: width, value
    -- Invariant: The value must be within the range 0 .. 2^width-1
    data BV = BV !Integer !Integer

    instance Show BV where
      show :: BV -> String
    show = Integer -> String
    forall a. Show a => a -> String
    show (Integer -> String) -> (BV -> Integer) -> BV -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV -> Integer
    bvVal

    -- | Apply an integer function to the values of bitvectors.
    --   This function assumes both bitvectors are the same width.
    binBV :: Applicative m => (Integer -> Integer -> Integer) -> BV -> BV -> m BV
    binBV :: forall (m :: * -> *).
    Applicative m =>
    (Integer -> Integer -> Integer) -> BV -> BV -> m BV
    binBV Integer -> Integer -> Integer
    f (BV Integer
    w Integer
    x) (BV Integer
    _ Integer
    y) = BV -> m BV
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> m BV) -> BV -> m BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    w (Integer -> Integer -> Integer
    f Integer
    x Integer
    y)
    {-# INLINE binBV #-}

    -- | Apply an integer function to the values of a bitvector.
    --   This function assumes the function will not require masking.
    unaryBV :: (Integer -> Integer) -> BV -> BV
    unaryBV :: (Integer -> Integer) -> BV -> BV
    unaryBV Integer -> Integer
    f (BV Integer
    w Integer
    x) = Integer -> Integer -> BV
    mkBv Integer
    w (Integer -> BV) -> Integer -> BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer
    f Integer
    x
    {-# INLINE unaryBV #-}

    bvVal :: BV -> Integer
    bvVal :: BV -> Integer
    bvVal (BV Integer
    _w Integer
    x) = Integer
    x
    {-# INLINE bvVal #-}

    -- | Smart constructor for 'BV's that checks for the width limit
    mkBv :: Integer -> Integer -> BV
    mkBv :: Integer -> Integer -> BV
    mkBv Integer
    w Integer
    i = Integer -> Integer -> BV
    BV Integer
    w (Integer -> Integer -> Integer
    mask Integer
    w Integer
    i)

    signedBV :: BV -> Integer
    signedBV :: BV -> Integer
    signedBV (BV Integer
    i Integer
    x) = Integer -> Integer -> Integer
    signedValue Integer
    i Integer
    x

    signedValue :: Integer -> Integer -> Integer
    signedValue :: Integer -> Integer -> Integer
    signedValue Integer
    i Integer
    x = if Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    testBit Integer
    x (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer
    iInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1)) then Integer
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - (Int -> Integer
    forall a. Bits a => Int -> a
    bit (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    i)) else Integer
    x

    integerToChar :: Integer -> Char
    integerToChar :: Integer -> Char
    integerToChar = Int -> Char
    forall a. Enum a => Int -> a
    toEnum (Int -> Char) -> (Integer -> Int) -> Integer -> Char
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger

    lg2 :: Integer -> Integer
    lg2 :: Integer -> Integer
    lg2 Integer
    i = case Integer -> Integer -> Maybe (Integer, Bool)
    genLog Integer
    i Integer
    2 of
      Just (Integer
    i',Bool
    isExact) | Bool
    isExact   -> Integer
    i'
                        | Bool
    otherwise -> Integer
    i' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1
      Maybe (Integer, Bool)
    Nothing                       -> Integer
    0

    ppBV :: PPOpts -> BV -> Doc
    ppBV :: PPOpts -> BV -> Doc
    ppBV PPOpts
    opts (BV Integer
    width Integer
    i)
      | Int
    base Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    36 = Integer -> Doc
    integer Integer
    i -- not sure how to rule this out
      | PPOpts -> Integer -> Bool
    asciiMode PPOpts
    opts Integer
    width = String -> Doc
    text (Char -> String
    forall a. Show a => a -> String
    show (Int -> Char
    forall a. Enum a => Int -> a
    toEnum (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    i) :: Char))
      | Bool
    otherwise = Doc
    prefix Doc -> Doc -> Doc
    <.> String -> Doc
    text String
    value
      where
      base :: Int
    base = PPOpts -> Int
    useBase PPOpts
    opts

      padding :: Int -> Doc
    padding Int
    bitsPerDigit = String -> Doc
    text (Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate Int
    padLen Char
    '0')
        where
        padLen :: Int
    padLen | Int
    m Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0     = Int
    d Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1
               | Bool
    otherwise = Int
    d

        (Int
    d,Int
    m) = (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    width Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    value Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * Int
    bitsPerDigit))
                       Int -> Int -> (Int, Int)
    forall a. Integral a => a -> a -> (a, a)
    `divMod` Int
    bitsPerDigit

      prefix :: Doc
    prefix = case Int
    base of
        Int
    2  -> String -> Doc
    text String
    "0b" Doc -> Doc -> Doc
    <.> Int -> Doc
    padding Int
    1
        Int
    8  -> String -> Doc
    text String
    "0o" Doc -> Doc -> Doc
    <.> Int -> Doc
    padding Int
    3
        Int
    10 -> Doc
    forall a. Monoid a => a
    mempty
        Int
    16 -> String -> Doc
    text String
    "0x" Doc -> Doc -> Doc
    <.> Int -> Doc
    padding Int
    4
        Int
    _  -> String -> Doc
    text String
    "0"  Doc -> Doc -> Doc
    <.> Char -> Doc
    char Char
    '<' Doc -> Doc -> Doc
    <.> Int -> Doc
    int Int
    base Doc -> Doc -> Doc
    <.> Char -> Doc
    char Char
    '>'

      value :: String
    value  = Integer -> (Int -> Char) -> Integer -> ShowS
    forall a. Integral a => a -> (Int -> Char) -> a -> ShowS
    showIntAtBase (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    base) (String
    digits String -> Int -> Char
    forall a. HasCallStack => [a] -> Int -> a
    !!) Integer
    i String
    ""
      digits :: String
    digits = String
    "0123456789abcdefghijklmnopqrstuvwxyz"

    -- Concrete Big-endian Words ------------------------------------------------------------

    mask ::
      Integer  {- ^ Bit-width -} ->
      Integer  {- ^ Value -} ->
      Integer  {- ^ Masked result -}
    mask :: Integer -> Integer -> Integer
    mask Integer
    w Integer
    i | Integer
    w Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    Arch.maxBigIntWidth = Integer -> Integer
    forall a. Integer -> a
    wordTooWide Integer
    w
             | Bool
    otherwise                = Integer
    i Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. (Int -> Integer
    forall a. Bits a => Int -> a
    bit (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    w) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1)

    instance Backend Concrete where
      type SBit Concrete = Bool
      type SWord Concrete = BV
      type SInteger Concrete = Integer
      type SFloat Concrete = FP.BF
      type SEval Concrete = Eval

      raiseError :: forall a. Concrete -> EvalError -> SEval Concrete a
    raiseError Concrete
    _ EvalError
    err =
        do CallStack
    stk <- Eval CallStack
    getCallStack
           IO a -> Eval a
    forall a. IO a -> Eval a
    io (EvalErrorEx -> IO a
    forall e a. Exception e => e -> IO a
    X.throwIO (CallStack -> EvalError -> EvalErrorEx
    EvalErrorEx CallStack
    stk EvalError
    err))

      assertSideCondition :: Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
    assertSideCondition Concrete
    _ Bool
    SBit Concrete
    True EvalError
    _ = () -> Eval ()
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
      assertSideCondition Concrete
    sym Bool
    SBit Concrete
    False EvalError
    err = Concrete -> EvalError -> SEval Concrete ()
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    forall a. Concrete -> EvalError -> SEval Concrete a
    raiseError Concrete
    sym EvalError
    err

      wordLen :: Concrete -> SWord Concrete -> Integer
    wordLen Concrete
    _ (BV Integer
    w Integer
    _) = Integer
    w
      wordAsChar :: Concrete -> SWord Concrete -> Maybe Char
    wordAsChar Concrete
    _ (BV Integer
    _ Integer
    x) = Char -> Maybe Char
    forall a. a -> Maybe a
    Just (Char -> Maybe Char) -> Char -> Maybe Char
    forall a b. (a -> b) -> a -> b
    $! Integer -> Char
    integerToChar Integer
    x

      wordBit :: Concrete
    -> SWord Concrete -> Integer -> SEval Concrete (SBit Concrete)
    wordBit Concrete
    _ (BV Integer
    w Integer
    x) Integer
    idx = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    testBit Integer
    x (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    idx))

      wordUpdate :: Concrete
    -> SWord Concrete
    -> Integer
    -> SBit Concrete
    -> SEval Concrete (SWord Concrete)
    wordUpdate Concrete
    _ (BV Integer
    w Integer
    x) Integer
    idx Bool
    SBit Concrete
    True  = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    BV Integer
    w (Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    setBit   Integer
    x (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    idx)))
      wordUpdate Concrete
    _ (BV Integer
    w Integer
    x) Integer
    idx Bool
    SBit Concrete
    False = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    BV Integer
    w (Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    clearBit Integer
    x (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer
    w Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1 Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    idx)))

      isReady :: forall a. Concrete -> SEval Concrete a -> SEval Concrete (Maybe a)
    isReady Concrete
    _ = Eval a -> Eval (Maybe a)
    SEval Concrete a -> SEval Concrete (Maybe a)
    forall a. Eval a -> Eval (Maybe a)
    maybeReady

      mergeEval :: forall a.
    Concrete
    -> (SBit Concrete -> a -> a -> SEval Concrete a)
    -> SBit Concrete
    -> SEval Concrete a
    -> SEval Concrete a
    -> SEval Concrete a
    mergeEval Concrete
    _sym SBit Concrete -> a -> a -> SEval Concrete a
    f SBit Concrete
    c SEval Concrete a
    mx SEval Concrete a
    my =
        do a
    x <- Eval a
    SEval Concrete a
    mx
           a
    y <- Eval a
    SEval Concrete a
    my
           SBit Concrete -> a -> a -> SEval Concrete a
    f SBit Concrete
    c a
    x a
    y

      sDeclareHole :: forall a.
    Concrete
    -> String
    -> SEval
         Concrete (SEval Concrete a, SEval Concrete a -> SEval Concrete ())
    sDeclareHole Concrete
    _ = String -> Eval (Eval a, Eval a -> Eval ())
    String
    -> SEval
         Concrete (SEval Concrete a, SEval Concrete a -> SEval Concrete ())
    forall a. String -> Eval (Eval a, Eval a -> Eval ())
    blackhole
      sDelayFill :: forall a.
    Concrete
    -> SEval Concrete a
    -> Maybe (SEval Concrete a)
    -> String
    -> SEval Concrete (SEval Concrete a)
    sDelayFill Concrete
    _ = Eval a -> Maybe (Eval a) -> String -> Eval (Eval a)
    SEval Concrete a
    -> Maybe (SEval Concrete a)
    -> String
    -> SEval Concrete (SEval Concrete a)
    forall a. Eval a -> Maybe (Eval a) -> String -> Eval (Eval a)
    delayFill
      sSpark :: forall a.
    Concrete -> SEval Concrete a -> SEval Concrete (SEval Concrete a)
    sSpark Concrete
    _ = Eval a -> Eval (Eval a)
    SEval Concrete a -> SEval Concrete (SEval Concrete a)
    forall a. Eval a -> Eval (Eval a)
    evalSpark
      sModifyCallStack :: forall a.
    Concrete
    -> (CallStack -> CallStack) -> SEval Concrete a -> SEval Concrete a
    sModifyCallStack Concrete
    _ CallStack -> CallStack
    f SEval Concrete a
    m = (CallStack -> CallStack) -> Eval a -> Eval a
    forall a. (CallStack -> CallStack) -> Eval a -> Eval a
    modifyCallStack CallStack -> CallStack
    f Eval a
    SEval Concrete a
    m
      sGetCallStack :: Concrete -> SEval Concrete CallStack
    sGetCallStack Concrete
    _ = Eval CallStack
    SEval Concrete CallStack
    getCallStack

      bitLit :: Concrete -> Bool -> SBit Concrete
    bitLit Concrete
    _ Bool
    b = Bool
    SBit Concrete
    b
      bitAsLit :: Concrete -> SBit Concrete -> Maybe Bool
    bitAsLit Concrete
    _ SBit Concrete
    b = Bool -> Maybe Bool
    forall a. a -> Maybe a
    Just Bool
    SBit Concrete
    b

      bitEq :: Concrete
    -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
    bitEq Concrete
    _  SBit Concrete
    x SBit Concrete
    y = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Bool
    SBit Concrete
    x Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    SBit Concrete
    y
      bitOr :: Concrete
    -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
    bitOr Concrete
    _  SBit Concrete
    x SBit Concrete
    y = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Bool
    SBit Concrete
    x Bool -> Bool -> Bool
    forall a. Bits a => a -> a -> a
    .|. Bool
    SBit Concrete
    y
      bitAnd :: Concrete
    -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
    bitAnd Concrete
    _ SBit Concrete
    x SBit Concrete
    y = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Bool
    SBit Concrete
    x Bool -> Bool -> Bool
    forall a. Bits a => a -> a -> a
    .&. Bool
    SBit Concrete
    y
      bitXor :: Concrete
    -> SBit Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
    bitXor Concrete
    _ SBit Concrete
    x SBit Concrete
    y = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Bool
    SBit Concrete
    x Bool -> Bool -> Bool
    forall a. Bits a => a -> a -> a
    `xor` Bool
    SBit Concrete
    y
      bitComplement :: Concrete -> SBit Concrete -> SEval Concrete (SBit Concrete)
    bitComplement Concrete
    _ SBit Concrete
    x = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Bool -> Bool
    forall a. Bits a => a -> a
    complement Bool
    SBit Concrete
    x

      iteBit :: Concrete
    -> SBit Concrete
    -> SBit Concrete
    -> SBit Concrete
    -> SEval Concrete (SBit Concrete)
    iteBit Concrete
    _ SBit Concrete
    b SBit Concrete
    x SBit Concrete
    y  = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! if Bool
    SBit Concrete
    b then Bool
    SBit Concrete
    x else Bool
    SBit Concrete
    y
      iteWord :: Concrete
    -> SBit Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    iteWord Concrete
    _ SBit Concrete
    b SWord Concrete
    x SWord Concrete
    y = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! if Bool
    SBit Concrete
    b then SWord Concrete
    BV
    x else SWord Concrete
    BV
    y
      iteInteger :: Concrete
    -> SBit Concrete
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    iteInteger Concrete
    _ SBit Concrete
    b SInteger Concrete
    x SInteger Concrete
    y = Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Eval Integer) -> Integer -> Eval Integer
    forall a b. (a -> b) -> a -> b
    $! if Bool
    SBit Concrete
    b then Integer
    SInteger Concrete
    x else Integer
    SInteger Concrete
    y
      iteFloat :: Concrete
    -> SBit Concrete
    -> SFloat Concrete
    -> SFloat Concrete
    -> SEval Concrete (SFloat Concrete)
    iteFloat Concrete
    _ SBit Concrete
    b SFloat Concrete
    x SFloat Concrete
    y   = BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BF -> Eval BF) -> BF -> Eval BF
    forall a b. (a -> b) -> a -> b
    $! if Bool
    SBit Concrete
    b then BF
    SFloat Concrete
    x else BF
    SFloat Concrete
    y

      wordLit :: Concrete -> Integer -> Integer -> SEval Concrete (SWord Concrete)
    wordLit Concrete
    _ Integer
    w Integer
    i = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    w Integer
    i
      wordAsLit :: Concrete -> SWord Concrete -> Maybe (Integer, Integer)
    wordAsLit Concrete
    _ (BV Integer
    w Integer
    i) = (Integer, Integer) -> Maybe (Integer, Integer)
    forall a. a -> Maybe a
    Just (Integer
    w,Integer
    i)
      integerLit :: Concrete -> Integer -> SEval Concrete (SInteger Concrete)
    integerLit Concrete
    _ Integer
    i = Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Integer
    i
      integerAsLit :: Concrete -> SInteger Concrete -> Maybe Integer
    integerAsLit Concrete
    _ = Integer -> Maybe Integer
    SInteger Concrete -> Maybe Integer
    forall a. a -> Maybe a
    Just

      wordToInt :: Concrete -> SWord Concrete -> SEval Concrete (SInteger Concrete)
    wordToInt Concrete
    _ (BV Integer
    _ Integer
    x) = Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Integer
    x
      wordToSignedInt :: Concrete -> SWord Concrete -> SEval Concrete (SInteger Concrete)
    wordToSignedInt Concrete
    _ (BV Integer
    w Integer
    x) = Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Eval Integer) -> Integer -> Eval Integer
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> Integer
    signedValue Integer
    w Integer
    x
      wordFromInt :: Concrete
    -> Integer -> SInteger Concrete -> SEval Concrete (SWord Concrete)
    wordFromInt Concrete
    _ Integer
    w SInteger Concrete
    x = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    w Integer
    SInteger Concrete
    x

      packWord :: Concrete -> [SBit Concrete] -> SEval Concrete (SWord Concrete)
    packWord Concrete
    _ [SBit Concrete]
    bits = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    BV (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    w) Integer
    a
        where
          w :: Int
    w = case [Bool] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Bool]
    [SBit Concrete]
    bits of
                Int
    len | Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    len Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    Arch.maxBigIntWidth -> Integer -> Int
    forall a. Integer -> a
    wordTooWide (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    len)
                    | Bool
    otherwise                  -> Int
    len
          a :: Integer
    a = (Integer -> (Int, Bool) -> Integer)
    -> Integer -> [(Int, Bool)] -> Integer
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Integer -> (Int, Bool) -> Integer
    forall {a}. Bits a => a -> (Int, Bool) -> a
    setb Integer
    0 ([Int] -> [Bool] -> [(Int, Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1, Int
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    2 .. Int
    0] [Bool]
    [SBit Concrete]
    bits)
          setb :: a -> (Int, Bool) -> a
    setb a
    acc (Int
    n,Bool
    b) | Bool
    b         = a -> Int -> a
    forall a. Bits a => a -> Int -> a
    setBit a
    acc Int
    n
                         | Bool
    otherwise = a
    acc

      unpackWord :: Concrete -> SWord Concrete -> SEval Concrete [SBit Concrete]
    unpackWord Concrete
    _ (BV Integer
    w Integer
    a) = [Bool] -> Eval [Bool]
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [ Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    testBit Integer
    a Int
    n | Int
    n <- [Int
    w' Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1, Int
    w' Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    2 .. Int
    0] ]
        where
          w' :: Int
    w' = Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    w

      joinWord :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    joinWord Concrete
    _ (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y) =
        BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    BV (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    j) (Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    shiftL Integer
    x (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    j) Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    y)

      splitWord :: Concrete
    -> Integer
    -> Integer
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete, SWord Concrete)
    splitWord Concrete
    _ Integer
    leftW Integer
    rightW (BV Integer
    _ Integer
    x) =
        (BV, BV) -> Eval (BV, BV)
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ( Integer -> Integer -> BV
    BV Integer
    leftW (Integer
    x Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftR` (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    rightW)), Integer -> Integer -> BV
    mkBv Integer
    rightW Integer
    x )

      extractWord :: Concrete
    -> Integer
    -> Integer
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    extractWord Concrete
    _ Integer
    n Integer
    i (BV Integer
    _ Integer
    x) = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    n (Integer
    x Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftR` (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    i))

      wordEq :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SBit Concrete)
    wordEq Concrete
    _ (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Integer
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    y
        | Bool
    otherwise = String -> [String] -> Eval Bool
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to compare words of different sizes: wordEq" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordSignedLessThan :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SBit Concrete)
    wordSignedLessThan Concrete
    _ (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> Integer
    signedValue Integer
    i Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer -> Integer -> Integer
    signedValue Integer
    i Integer
    y
        | Bool
    otherwise = String -> [String] -> Eval Bool
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to compare words of different sizes: wordSignedLessThan" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordLessThan :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SBit Concrete)
    wordLessThan Concrete
    _ (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    y
        | Bool
    otherwise = String -> [String] -> Eval Bool
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to compare words of different sizes: wordLessThan" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordGreaterThan :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SBit Concrete)
    wordGreaterThan Concrete
    _ (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Integer
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    y
        | Bool
    otherwise = String -> [String] -> Eval Bool
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to compare words of different sizes: wordGreaterThan" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordAnd :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordAnd Concrete
    _ (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .&. Integer
    y)
        | Bool
    otherwise = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to AND words of different sizes: wordPlus" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordOr :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordOr Concrete
    _ (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. Integer
    y)
        | Bool
    otherwise = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to OR words of different sizes: wordPlus" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordXor :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordXor Concrete
    _ (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer
    x Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    `xor` Integer
    y)
        | Bool
    otherwise = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to XOR words of different sizes: wordPlus" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordComplement :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)
    wordComplement Concrete
    _ (BV Integer
    i Integer
    x) = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer -> Integer
    forall a. Bits a => a -> a
    complement Integer
    x)

      wordPlus :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordPlus Concrete
    _ (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    y)
        | Bool
    otherwise = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to add words of different sizes: wordPlus" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordNegate :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)
    wordNegate Concrete
    _ (BV Integer
    i Integer
    x) = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    x)

      wordMinus :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordMinus Concrete
    _ (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    y)
        | Bool
    otherwise = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to subtract words of different sizes: wordMinus" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordMult :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordMult Concrete
    _ (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    y)
        | Bool
    otherwise = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to multiply words of different sizes: wordMult" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordDiv :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordDiv Concrete
    sym (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 Bool -> Bool -> Bool
    && Integer
    j Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    0 Integer
    0
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j =
            do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition Concrete
    sym (Integer
    y Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0) EvalError
    DivideByZero
               BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    y)
        | Bool
    otherwise = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to divide words of different sizes: wordDiv" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordMod :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordMod Concrete
    sym (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 Bool -> Bool -> Bool
    && Integer
    j Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    0 Integer
    0
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j =
            do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition Concrete
    sym (Integer
    y Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0) EvalError
    DivideByZero
               BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    y)
        | Bool
    otherwise = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to mod words of different sizes: wordMod" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordSignedDiv :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordSignedDiv Concrete
    sym (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 Bool -> Bool -> Bool
    && Integer
    j Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    0 Integer
    0
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j =
            do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition Concrete
    sym (Integer
    y Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0) EvalError
    DivideByZero
               let sx :: Integer
    sx = Integer -> Integer -> Integer
    signedValue Integer
    i Integer
    x
                   sy :: Integer
    sy = Integer -> Integer -> Integer
    signedValue Integer
    i Integer
    y
               BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer
    sx Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `quot` Integer
    sy)
        | Bool
    otherwise = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to divide words of different sizes: wordSignedDiv" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordSignedMod :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordSignedMod Concrete
    sym (BV Integer
    i Integer
    x) (BV Integer
    j Integer
    y)
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 Bool -> Bool -> Bool
    && Integer
    j Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0 = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    0 Integer
    0
        | Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j =
            do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition Concrete
    sym (Integer
    y Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0) EvalError
    DivideByZero
               let sx :: Integer
    sx = Integer -> Integer -> Integer
    signedValue Integer
    i Integer
    x
                   sy :: Integer
    sy = Integer -> Integer -> Integer
    signedValue Integer
    i Integer
    y
               BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer
    sx Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `rem` Integer
    sy)
        | Bool
    otherwise = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Attempt to mod words of different sizes: wordSignedMod" [Integer -> String
    forall a. Show a => a -> String
    show Integer
    i, Integer -> String
    forall a. Show a => a -> String
    show Integer
    j]

      wordShiftLeft :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordShiftLeft Concrete
    _sym (BV Integer
    w Integer
    ival) (BV Integer
    _ Integer
    by)
        | Integer
    by Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    w   = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    BV Integer
    w Integer
    0
        | Integer
    by Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int
    forall a. Bounded a => a
    maxBound :: Int) = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "shl" [String
    "Shift amount too large", Integer -> String
    forall a. Show a => a -> String
    show Integer
    by]
        | Bool
    otherwise = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    w (Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    shiftL Integer
    ival (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    by))

      wordShiftRight :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordShiftRight Concrete
    _sym (BV Integer
    w Integer
    ival) (BV Integer
    _ Integer
    by)
        | Integer
    by Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    w   = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    BV Integer
    w Integer
    0
        | Integer
    by Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int
    forall a. Bounded a => a
    maxBound :: Int) = String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "lshr" [String
    "Shift amount too large", Integer -> String
    forall a. Show a => a -> String
    show Integer
    by]
        | Bool
    otherwise = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    BV Integer
    w (Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    shiftR Integer
    ival (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    by))

      wordSignedShiftRight :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordSignedShiftRight Concrete
    _sym (BV Integer
    w Integer
    ival) (BV Integer
    _ Integer
    by) =
        let by' :: Integer
    by' = Integer -> Integer -> Integer
    forall a. Ord a => a -> a -> a
    min Integer
    w Integer
    by in
        if Integer
    by' Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int
    forall a. Bounded a => a
    maxBound :: Int) then
          String -> [String] -> Eval BV
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "wordSignedShiftRight" [String
    "Shift amount too large", Integer -> String
    forall a. Show a => a -> String
    show Integer
    by]
        else
          BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    w (Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    shiftR (Integer -> Integer -> Integer
    signedValue Integer
    w Integer
    ival) (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    by'))

      wordRotateRight :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordRotateRight Concrete
    _sym (BV Integer
    0 Integer
    i) SWord Concrete
    _ = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Integer -> BV
    BV Integer
    0 Integer
    i)
      wordRotateRight Concrete
    _sym (BV Integer
    w Integer
    i) (BV Integer
    _ Integer
    by) =
          BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> (Integer -> BV) -> Integer -> Eval BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    mkBv Integer
    w (Integer -> Eval BV) -> Integer -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! (Integer
    i Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftR` Int
    b) Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. (Integer
    i Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftL` (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    b))
        where b :: Int
    b = Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer
    by Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    w)

      wordRotateLeft :: Concrete
    -> SWord Concrete
    -> SWord Concrete
    -> SEval Concrete (SWord Concrete)
    wordRotateLeft Concrete
    _sym (BV Integer
    0 Integer
    i) SWord Concrete
    _ = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Integer -> BV
    BV Integer
    0 Integer
    i)
      wordRotateLeft Concrete
    _sym (BV Integer
    w Integer
    i) (BV Integer
    _ Integer
    by) =
          BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> (Integer -> BV) -> Integer -> Eval BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    mkBv Integer
    w (Integer -> Eval BV) -> Integer -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! (Integer
    i Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftL` Int
    b) Integer -> Integer -> Integer
    forall a. Bits a => a -> a -> a
    .|. (Integer
    i Integer -> Int -> Integer
    forall a. Bits a => a -> Int -> a
    `shiftR` (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    w Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    b))
        where b :: Int
    b = Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer
    by Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    w)

      wordLg2 :: Concrete -> SWord Concrete -> SEval Concrete (SWord Concrete)
    wordLg2 Concrete
    _ (BV Integer
    i Integer
    x) = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BV -> Eval BV) -> BV -> Eval BV
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer -> BV
    mkBv Integer
    i (Integer -> Integer
    lg2 Integer
    x)

      intEq :: Concrete
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SBit Concrete)
    intEq Concrete
    _ SInteger Concrete
    x SInteger Concrete
    y = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Integer
    SInteger Concrete
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    SInteger Concrete
    y
      intLessThan :: Concrete
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SBit Concrete)
    intLessThan Concrete
    _ SInteger Concrete
    x SInteger Concrete
    y = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Integer
    SInteger Concrete
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    < Integer
    SInteger Concrete
    y
      intGreaterThan :: Concrete
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SBit Concrete)
    intGreaterThan Concrete
    _ SInteger Concrete
    x SInteger Concrete
    y = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Integer
    SInteger Concrete
    x Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    > Integer
    SInteger Concrete
    y

      intPlus :: Concrete
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    intPlus  Concrete
    _ SInteger Concrete
    x SInteger Concrete
    y = Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Eval Integer) -> Integer -> Eval Integer
    forall a b. (a -> b) -> a -> b
    $! Integer
    SInteger Concrete
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    SInteger Concrete
    y
      intMinus :: Concrete
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    intMinus Concrete
    _ SInteger Concrete
    x SInteger Concrete
    y = Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Eval Integer) -> Integer -> Eval Integer
    forall a b. (a -> b) -> a -> b
    $! Integer
    SInteger Concrete
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    SInteger Concrete
    y
      intNegate :: Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)
    intNegate Concrete
    _ SInteger Concrete
    x  = Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Eval Integer) -> Integer -> Eval Integer
    forall a b. (a -> b) -> a -> b
    $! Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    SInteger Concrete
    x
      intMult :: Concrete
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    intMult  Concrete
    _ SInteger Concrete
    x SInteger Concrete
    y = Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Eval Integer) -> Integer -> Eval Integer
    forall a b. (a -> b) -> a -> b
    $! Integer
    SInteger Concrete
    x Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    SInteger Concrete
    y
      intDiv :: Concrete
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    intDiv Concrete
    sym SInteger Concrete
    x SInteger Concrete
    y =
        do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition Concrete
    sym (Integer
    SInteger Concrete
    y Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0) EvalError
    DivideByZero
           Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Eval Integer) -> Integer -> Eval Integer
    forall a b. (a -> b) -> a -> b
    $! Integer
    SInteger Concrete
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `div` Integer
    SInteger Concrete
    y
      intMod :: Concrete
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    intMod Concrete
    sym SInteger Concrete
    x SInteger Concrete
    y =
        do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition Concrete
    sym (Integer
    SInteger Concrete
    y Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0) EvalError
    DivideByZero
           Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Eval Integer) -> Integer -> Eval Integer
    forall a b. (a -> b) -> a -> b
    $! Integer
    SInteger Concrete
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    SInteger Concrete
    y

      intToZn :: Concrete
    -> Integer
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    intToZn Concrete
    _ Integer
    0 SInteger Concrete
    _ = String -> [String] -> Eval Integer
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "intToZn" [String
    "0 modulus not allowed"]
      intToZn Concrete
    _ Integer
    m SInteger Concrete
    x = Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Eval Integer) -> Integer -> Eval Integer
    forall a b. (a -> b) -> a -> b
    $! Integer
    SInteger Concrete
    x Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    m

      -- NB: requires we maintain the invariant that
      --     Z_n is in reduced form
      znToInt :: Concrete
    -> Integer
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    znToInt Concrete
    _ Integer
    _m SInteger Concrete
    x = Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Integer
    SInteger Concrete
    x
      znEq :: Concrete
    -> Integer
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SBit Concrete)
    znEq Concrete
    _ Integer
    _m SInteger Concrete
    x SInteger Concrete
    y = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool -> Eval Bool) -> Bool -> Eval Bool
    forall a b. (a -> b) -> a -> b
    $! Integer
    SInteger Concrete
    x Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    SInteger Concrete
    y

      -- NB: under the precondition that `m` is prime,
      -- the only values for which no inverse exists are
      -- congruent to 0 modulo m.
      znRecip :: Concrete
    -> Integer
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    znRecip Concrete
    sym Integer
    m SInteger Concrete
    x =
        case Integer -> Integer -> Maybe Integer
    Integer.integerRecipMod Integer
    SInteger Concrete
    x Integer
    m of
          Just Integer
    r  -> Concrete -> Integer -> SEval Concrete (SInteger Concrete)
    forall sym.
    Backend sym =>
    sym -> Integer -> SEval sym (SInteger sym)
    integerLit Concrete
    sym Integer
    r
          Maybe Integer
    Nothing -> Concrete -> EvalError -> SEval Concrete Integer
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    forall a. Concrete -> EvalError -> SEval Concrete a
    raiseError Concrete
    sym EvalError
    DivideByZero

      znPlus :: Concrete
    -> Integer
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    znPlus  Concrete
    _ = (Integer -> Integer -> Integer)
    -> Integer -> Integer -> Integer -> Eval Integer
    forall (m :: * -> *).
    Monad m =>
    (Integer -> Integer -> Integer)
    -> Integer -> Integer -> Integer -> m Integer
    liftBinIntMod Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (+)
      znMinus :: Concrete
    -> Integer
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    znMinus Concrete
    _ = (Integer -> Integer -> Integer)
    -> Integer -> Integer -> Integer -> Eval Integer
    forall (m :: * -> *).
    Monad m =>
    (Integer -> Integer -> Integer)
    -> Integer -> Integer -> Integer -> m Integer
    liftBinIntMod (-)
      znMult :: Concrete
    -> Integer
    -> SInteger Concrete
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    znMult  Concrete
    _ = (Integer -> Integer -> Integer)
    -> Integer -> Integer -> Integer -> Eval Integer
    forall (m :: * -> *).
    Monad m =>
    (Integer -> Integer -> Integer)
    -> Integer -> Integer -> Integer -> m Integer
    liftBinIntMod Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    (*)
      znNegate :: Concrete
    -> Integer
    -> SInteger Concrete
    -> SEval Concrete (SInteger Concrete)
    znNegate Concrete
    _ Integer
    0 SInteger Concrete
    _ = String -> [String] -> Eval Integer
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "znNegate" [String
    "0 modulus not allowed"]
      znNegate Concrete
    _ Integer
    m SInteger Concrete
    x = Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Eval Integer) -> Integer -> Eval Integer
    forall a b. (a -> b) -> a -> b
    $! (Integer -> Integer
    forall a. Num a => a -> a
    negate Integer
    SInteger Concrete
    x) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    m

      ------------------------------------------------------------------------
      -- Floating Point
      fpLit :: Concrete
    -> Integer
    -> Integer
    -> Rational
    -> SEval Concrete (SFloat Concrete)
    fpLit Concrete
    _sym Integer
    e Integer
    p Rational
    rat     = BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Integer -> Rational -> BF
    FP.fpLit Integer
    e Integer
    p Rational
    rat)

      fpNaN :: Concrete -> Integer -> Integer -> SEval Concrete (SFloat Concrete)
    fpNaN Concrete
    _sym Integer
    e Integer
    p         = BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Integer -> BigFloat -> BF
    FP.BF Integer
    e Integer
    p BigFloat
    FP.bfNaN)
      fpPosInf :: Concrete -> Integer -> Integer -> SEval Concrete (SFloat Concrete)
    fpPosInf Concrete
    _sym Integer
    e Integer
    p      = BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Integer -> BigFloat -> BF
    FP.BF Integer
    e Integer
    p BigFloat
    FP.bfPosInf)

      fpAsLit :: Concrete -> SFloat Concrete -> Maybe BF
    fpAsLit Concrete
    _ SFloat Concrete
    f            = BF -> Maybe BF
    forall a. a -> Maybe a
    Just BF
    SFloat Concrete
    f
      fpExactLit :: Concrete -> BF -> SEval Concrete (SFloat Concrete)
    fpExactLit Concrete
    _sym BF
    bf     = BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure BF
    bf
      fpEq :: Concrete
    -> SFloat Concrete
    -> SFloat Concrete
    -> SEval Concrete (SBit Concrete)
    fpEq Concrete
    _sym SFloat Concrete
    x SFloat Concrete
    y          = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x BigFloat -> BigFloat -> Bool
    forall a. Eq a => a -> a -> Bool
    == BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    y)
      fpLogicalEq :: Concrete
    -> SFloat Concrete
    -> SFloat Concrete
    -> SEval Concrete (SBit Concrete)
    fpLogicalEq Concrete
    _sym SFloat Concrete
    x SFloat Concrete
    y   = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BigFloat -> BigFloat -> Ordering
    FP.bfCompare (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x) (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    y) Ordering -> Ordering -> Bool
    forall a. Eq a => a -> a -> Bool
    == Ordering
    EQ)
      fpLessThan :: Concrete
    -> SFloat Concrete
    -> SFloat Concrete
    -> SEval Concrete (SBit Concrete)
    fpLessThan Concrete
    _sym SFloat Concrete
    x SFloat Concrete
    y    = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x BigFloat -> BigFloat -> Bool
    forall a. Ord a => a -> a -> Bool
    <  BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    y)
      fpGreaterThan :: Concrete
    -> SFloat Concrete
    -> SFloat Concrete
    -> SEval Concrete (SBit Concrete)
    fpGreaterThan Concrete
    _sym SFloat Concrete
    x SFloat Concrete
    y = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x BigFloat -> BigFloat -> Bool
    forall a. Ord a => a -> a -> Bool
    >  BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    y)
      fpPlus :: FPArith2 Concrete
    fpPlus  = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> FPArith2 Concrete
    fpBinArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfAdd
      fpMinus :: FPArith2 Concrete
    fpMinus = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> FPArith2 Concrete
    fpBinArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfSub
      fpMult :: FPArith2 Concrete
    fpMult  = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> FPArith2 Concrete
    fpBinArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfMul
      fpDiv :: FPArith2 Concrete
    fpDiv   = (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> FPArith2 Concrete
    fpBinArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfDiv
      fpNeg :: Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)
    fpNeg Concrete
    _ SFloat Concrete
    x = BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BF -> Eval BF) -> BF -> Eval BF
    forall a b. (a -> b) -> a -> b
    $! BF
    SFloat Concrete
    x { bfValue :: BigFloat
    FP.bfValue = BigFloat -> BigFloat
    FP.bfNeg (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x) }

      fpAbs :: Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)
    fpAbs Concrete
    _ SFloat Concrete
    x = BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BF -> Eval BF) -> BF -> Eval BF
    forall a b. (a -> b) -> a -> b
    $! BF
    SFloat Concrete
    x { bfValue :: BigFloat
    FP.bfValue = BigFloat -> BigFloat
    FP.bfAbs (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x) }
      fpSqrt :: Concrete
    -> SWord Concrete
    -> SFloat Concrete
    -> SEval Concrete (SFloat Concrete)
    fpSqrt Concrete
    sym SWord Concrete
    r SFloat Concrete
    x =
        do RoundMode
    r' <- Concrete -> SWord Concrete -> SEval Concrete RoundMode
    fpRoundMode Concrete
    sym SWord Concrete
    r
           let opts :: BFOpts
    opts = Integer -> Integer -> RoundMode -> BFOpts
    FP.fpOpts (BF -> Integer
    FP.bfExpWidth BF
    SFloat Concrete
    x) (BF -> Integer
    FP.bfPrecWidth BF
    SFloat Concrete
    x) RoundMode
    r'
           BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BF -> Eval BF) -> BF -> Eval BF
    forall a b. (a -> b) -> a -> b
    $! BF
    SFloat Concrete
    x{ bfValue :: BigFloat
    FP.bfValue = (BigFloat, Status) -> BigFloat
    FP.fpCheckStatus (BFOpts -> BigFloat -> (BigFloat, Status)
    FP.bfSqrt BFOpts
    opts (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x)) }

      fpFMA :: Concrete
    -> SWord Concrete
    -> SFloat Concrete
    -> SFloat Concrete
    -> SFloat Concrete
    -> SEval Concrete (SFloat Concrete)
    fpFMA Concrete
    sym SWord Concrete
    r SFloat Concrete
    x SFloat Concrete
    y SFloat Concrete
    z =
        do RoundMode
    r' <- Concrete -> SWord Concrete -> SEval Concrete RoundMode
    fpRoundMode Concrete
    sym SWord Concrete
    r
           let opts :: BFOpts
    opts = Integer -> Integer -> RoundMode -> BFOpts
    FP.fpOpts (BF -> Integer
    FP.bfExpWidth BF
    SFloat Concrete
    x) (BF -> Integer
    FP.bfPrecWidth BF
    SFloat Concrete
    x) RoundMode
    r'
           BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BF -> Eval BF) -> BF -> Eval BF
    forall a b. (a -> b) -> a -> b
    $! BF
    SFloat Concrete
    x { bfValue :: BigFloat
    FP.bfValue = (BigFloat, Status) -> BigFloat
    FP.fpCheckStatus (BFOpts -> BigFloat -> BigFloat -> BigFloat -> (BigFloat, Status)
    FP.bfFMA BFOpts
    opts (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x) (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    y) (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    z)) }

      fpIsZero :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
    fpIsZero Concrete
    _ SFloat Concrete
    x = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BigFloat -> Bool
    FP.bfIsZero (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x))
      fpIsNeg :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
    fpIsNeg Concrete
    _ SFloat Concrete
    x  = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BigFloat -> Bool
    FP.bfIsNeg (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x))
      fpIsNaN :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
    fpIsNaN Concrete
    _ SFloat Concrete
    x  = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BigFloat -> Bool
    FP.bfIsNaN (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x))
      fpIsInf :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
    fpIsInf Concrete
    _ SFloat Concrete
    x  = Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BigFloat -> Bool
    FP.bfIsInf (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x))
      fpIsNorm :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
    fpIsNorm Concrete
    _ SFloat Concrete
    x =
        let opts :: BFOpts
    opts = Integer -> Integer -> RoundMode -> BFOpts
    FP.fpOpts (BF -> Integer
    FP.bfExpWidth BF
    SFloat Concrete
    x) (BF -> Integer
    FP.bfPrecWidth BF
    SFloat Concrete
    x) RoundMode
    FP.NearEven
         in Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BFOpts -> BigFloat -> Bool
    FP.bfIsNormal BFOpts
    opts (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x))
      fpIsSubnorm :: Concrete -> SFloat Concrete -> SEval Concrete (SBit Concrete)
    fpIsSubnorm Concrete
    _ SFloat Concrete
    x =
        let opts :: BFOpts
    opts = Integer -> Integer -> RoundMode -> BFOpts
    FP.fpOpts (BF -> Integer
    FP.bfExpWidth BF
    SFloat Concrete
    x) (BF -> Integer
    FP.bfPrecWidth BF
    SFloat Concrete
    x) RoundMode
    FP.NearEven
         in Bool -> Eval Bool
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BFOpts -> BigFloat -> Bool
    FP.bfIsSubnormal BFOpts
    opts (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x))

      fpFromBits :: Concrete
    -> Integer
    -> Integer
    -> SWord Concrete
    -> SEval Concrete (SFloat Concrete)
    fpFromBits Concrete
    _sym Integer
    e Integer
    p SWord Concrete
    bv = BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Integer -> Integer -> BF
    FP.floatFromBits Integer
    e Integer
    p (BV -> Integer
    bvVal SWord Concrete
    BV
    bv))
      fpToBits :: Concrete -> SFloat Concrete -> SEval Concrete (SWord Concrete)
    fpToBits Concrete
    _sym (FP.BF Integer
    e Integer
    p BigFloat
    v) = BV -> Eval BV
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Integer -> BV
    mkBv (Integer
    eInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    p) (Integer -> Integer -> BigFloat -> Integer
    FP.floatToBits Integer
    e Integer
    p BigFloat
    v))

      fpFromInteger :: Concrete
    -> Integer
    -> Integer
    -> SWord Concrete
    -> SInteger Concrete
    -> SEval Concrete (SFloat Concrete)
    fpFromInteger Concrete
    sym Integer
    e Integer
    p SWord Concrete
    r SInteger Concrete
    x =
        do RoundMode
    r' <- Concrete -> SWord Concrete -> SEval Concrete RoundMode
    fpRoundMode Concrete
    sym SWord Concrete
    r
           BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure FP.BF { bfExpWidth :: Integer
    FP.bfExpWidth = Integer
    e
                      , bfPrecWidth :: Integer
    FP.bfPrecWidth = Integer
    p
                      , bfValue :: BigFloat
    FP.bfValue = (BigFloat, Status) -> BigFloat
    FP.fpCheckStatus ((BigFloat, Status) -> BigFloat) -> (BigFloat, Status) -> BigFloat
    forall a b. (a -> b) -> a -> b
    $
                                     RoundMode -> BigFloat -> (BigFloat, Status)
    FP.bfRoundInt RoundMode
    r' (Integer -> BigFloat
    FP.bfFromInteger Integer
    SInteger Concrete
    x)
                      }
      fpToInteger :: Concrete
    -> String
    -> SWord Concrete
    -> SFloat Concrete
    -> SEval Concrete (SInteger Concrete)
    fpToInteger = Concrete
    -> String
    -> SWord Concrete
    -> SFloat Concrete
    -> SEval Concrete (SInteger Concrete)
    fpCvtToInteger

      fpFromRational :: Concrete
    -> Integer
    -> Integer
    -> SWord Concrete
    -> SRational Concrete
    -> SEval Concrete (SFloat Concrete)
    fpFromRational Concrete
    sym Integer
    e Integer
    p SWord Concrete
    r SRational Concrete
    x =
        do RoundMode
    mode <- Concrete -> SWord Concrete -> SEval Concrete RoundMode
    fpRoundMode Concrete
    sym SWord Concrete
    r
           BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> Integer -> RoundMode -> Rational -> BF
    FP.floatFromRational Integer
    e Integer
    p RoundMode
    mode (SRational Concrete -> SInteger Concrete
    forall sym. SRational sym -> SInteger sym
    sNum SRational Concrete
    x Integer -> Integer -> Rational
    forall a. Integral a => a -> a -> Ratio a
    % SRational Concrete -> SInteger Concrete
    forall sym. SRational sym -> SInteger sym
    sDenom SRational Concrete
    x))

      fpToRational :: Concrete -> SFloat Concrete -> SEval Concrete (SRational Concrete)
    fpToRational Concrete
    sym SFloat Concrete
    fp =
          case String -> BF -> Either EvalError Rational
    FP.floatToRational String
    "fpToRational" BF
    SFloat Concrete
    fp of
            Left EvalError
    err -> Concrete -> EvalError -> SEval Concrete (SRational Concrete)
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    forall a. Concrete -> EvalError -> SEval Concrete a
    raiseError Concrete
    sym EvalError
    err
            Right Rational
    r  -> SRational Concrete -> SEval Concrete (SRational Concrete)
    forall a. a -> SEval Concrete a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SRational Concrete -> SEval Concrete (SRational Concrete))
    -> SRational Concrete -> SEval Concrete (SRational Concrete)
    forall a b. (a -> b) -> a -> b
    $ SRational { sNum :: SInteger Concrete
    sNum = Rational -> Integer
    forall a. Ratio a -> a
    numerator Rational
    r, sDenom :: SInteger Concrete
    sDenom = Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    r }

    {-# INLINE liftBinIntMod #-}
    liftBinIntMod :: Monad m =>
      (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer -> m Integer
    liftBinIntMod :: forall (m :: * -> *).
    Monad m =>
    (Integer -> Integer -> Integer)
    -> Integer -> Integer -> Integer -> m Integer
    liftBinIntMod Integer -> Integer -> Integer
    op Integer
    m Integer
    x Integer
    y
      | Integer
    m Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    0    = String -> [String] -> m Integer
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "znArithmetic" [String
    "0 modulus not allowed"]
      | Bool
    otherwise = Integer -> m Integer
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> m Integer) -> Integer -> m Integer
    forall a b. (a -> b) -> a -> b
    $ (Integer -> Integer -> Integer
    op Integer
    x Integer
    y) Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    `mod` Integer
    m

    {-# INLINE fpBinArith #-}
    fpBinArith ::
      (FP.BFOpts -> FP.BigFloat -> FP.BigFloat -> (FP.BigFloat, FP.Status)) ->
      Concrete ->
      SWord Concrete  {- ^ Rouding mode -} ->
      SFloat Concrete ->
      SFloat Concrete ->
      SEval Concrete (SFloat Concrete)
    fpBinArith :: (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status))
    -> FPArith2 Concrete
    fpBinArith BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    fun = \Concrete
    sym SWord Concrete
    r SFloat Concrete
    x SFloat Concrete
    y ->
      do BFOpts
    opts <- Integer -> Integer -> RoundMode -> BFOpts
    FP.fpOpts (BF -> Integer
    FP.bfExpWidth BF
    SFloat Concrete
    x) (BF -> Integer
    FP.bfPrecWidth BF
    SFloat Concrete
    x)
                                                      (RoundMode -> BFOpts) -> Eval RoundMode -> Eval BFOpts
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Concrete -> SWord Concrete -> SEval Concrete RoundMode
    fpRoundMode Concrete
    sym SWord Concrete
    r
         BF -> Eval BF
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (BF -> Eval BF) -> BF -> Eval BF
    forall a b. (a -> b) -> a -> b
    $! BF
    SFloat Concrete
    x { bfValue :: BigFloat
    FP.bfValue = (BigFloat, Status) -> BigFloat
    FP.fpCheckStatus
                                    (BFOpts -> BigFloat -> BigFloat -> (BigFloat, Status)
    fun BFOpts
    opts (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    x) (BF -> BigFloat
    FP.bfValue BF
    SFloat Concrete
    y)) }

    fpCvtToInteger ::
      Concrete ->
      String ->
      SWord Concrete {- ^ Rounding mode -} ->
      SFloat Concrete ->
      SEval Concrete (SInteger Concrete)
    fpCvtToInteger :: Concrete
    -> String
    -> SWord Concrete
    -> SFloat Concrete
    -> SEval Concrete (SInteger Concrete)
    fpCvtToInteger Concrete
    sym String
    fun SWord Concrete
    rnd SFloat Concrete
    flt =
      do RoundMode
    mode <- Concrete -> SWord Concrete -> SEval Concrete RoundMode
    fpRoundMode Concrete
    sym SWord Concrete
    rnd
         case String -> RoundMode -> BF -> Either EvalError Integer
    FP.floatToInteger String
    fun RoundMode
    mode BF
    SFloat Concrete
    flt of
           Right Integer
    i -> Integer -> Eval Integer
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Integer
    i
           Left EvalError
    err -> Concrete -> EvalError -> SEval Concrete Integer
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    forall a. Concrete -> EvalError -> SEval Concrete a
    raiseError Concrete
    sym EvalError
    err

    fpRoundMode :: Concrete -> SWord Concrete -> SEval Concrete FP.RoundMode
    fpRoundMode :: Concrete -> SWord Concrete -> SEval Concrete RoundMode
    fpRoundMode Concrete
    sym SWord Concrete
    w =
      case Integer -> Either EvalError RoundMode
    FP.fpRound (BV -> Integer
    bvVal SWord Concrete
    BV
    w) of
        Left EvalError
    err -> Concrete -> EvalError -> SEval Concrete RoundMode
    forall sym a. Backend sym => sym -> EvalError -> SEval sym a
    forall a. Concrete -> EvalError -> SEval Concrete a
    raiseError Concrete
    sym EvalError
    err
        Right RoundMode
    a  -> RoundMode -> Eval RoundMode
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure RoundMode
    a