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

    {-# LANGUAGE BangPatterns #-}
    {-# LANGUAGE BlockArguments #-}
    {-# LANGUAGE OverloadedStrings #-}
    {-# LANGUAGE Rank2Types #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeFamilies #-}
    module Cryptol.Eval.Concrete
      ( module Cryptol.Backend.Concrete
      , Value
      , primTable
      , toExpr
      ) where

    import Control.Monad (guard, zipWithM, foldM, mzero)
    import Data.Ratio(numerator,denominator)
    import Data.Word(Word32, Word64)
    import MonadLib( ChoiceT, findOne, lift )
    import qualified LibBF as FP
    import qualified Cryptol.F2 as F2

    import qualified Data.Map.Strict as Map
    import Data.Map(Map)

    import Cryptol.TypeCheck.Solver.InfNat (Nat'(..))

    import Cryptol.Backend
    import Cryptol.Backend.Concrete
    import Cryptol.Backend.FloatHelpers
    import Cryptol.Backend.Monad
    import Cryptol.Backend.SeqMap
    import Cryptol.Backend.WordValue

    import Cryptol.Eval.Generic
    import Cryptol.Eval.Prims
    import Cryptol.Eval.Type
    import Cryptol.Eval.Value
    import qualified Cryptol.SHA as SHA
    import qualified Cryptol.AES as AES
    import qualified Cryptol.PrimeEC as PrimeEC
    import Cryptol.ModuleSystem.Name
    import Cryptol.TypeCheck.AST as AST
    import Cryptol.Utils.Panic (panic)
    import Cryptol.Utils.Ident (PrimIdent,prelPrim,floatPrim,suiteBPrim,primeECPrim)
    import Cryptol.Utils.PP
    import Cryptol.Utils.RecordMap

    type Value = GenValue Concrete

    -- Value to Expression conversion ----------------------------------------------

    -- | Given an expected type, returns an expression that evaluates to
    -- this value, if we can determine it.
    toExpr :: PrimMap -> TValue -> Value -> Eval (Maybe AST.Expr)
    toExpr :: PrimMap -> TValue -> Value -> Eval (Maybe Expr)
    toExpr PrimMap
    prims TValue
    t0 Value
    v0 = ChoiceT Eval Expr -> Eval (Maybe Expr)
    forall (m :: * -> *) a. Monad m => ChoiceT m a -> m (Maybe a)
    findOne (TValue -> Value -> ChoiceT Eval Expr
    go TValue
    t0 Value
    v0)
      where

      prim :: Text -> Expr
    prim Text
    n = PrimMap -> PrimIdent -> Expr
    ePrim PrimMap
    prims (Text -> PrimIdent
    prelPrim Text
    n)

      go :: TValue -> Value -> ChoiceT Eval Expr
      go :: TValue -> Value -> ChoiceT Eval Expr
    go TValue
    ty Value
    val =
        case (TValue
    ty,Value
    val) of
          (TVRec RecordMap Ident TValue
    tfs, VRecord RecordMap Ident (SEval Concrete Value)
    vfs) ->
            do -- NB, vfs first argument to keep their display order
               Either (Either Ident Ident) (RecordMap Ident Expr)
    res <- (Ident -> Eval Value -> TValue -> ChoiceT Eval Expr)
    -> RecordMap Ident (Eval Value)
    -> RecordMap Ident TValue
    -> ChoiceT
         Eval (Either (Either Ident Ident) (RecordMap Ident Expr))
    forall (t :: * -> *) a b c d.
    (Ord a, Monad t) =>
    (a -> b -> c -> t d)
    -> RecordMap a b
    -> RecordMap a c
    -> t (Either (Either a a) (RecordMap a d))
    zipRecordsM (\Ident
    _lbl Eval Value
    v TValue
    t -> TValue -> Value -> ChoiceT Eval Expr
    go TValue
    t (Value -> ChoiceT Eval Expr)
    -> ChoiceT Eval Value -> ChoiceT Eval Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value -> ChoiceT Eval Value
    forall (m :: * -> *) a. Monad m => m a -> ChoiceT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift Eval Value
    v) RecordMap Ident (Eval Value)
    RecordMap Ident (SEval Concrete Value)
    vfs RecordMap Ident TValue
    tfs
               case Either (Either Ident Ident) (RecordMap Ident Expr)
    res of
                 Left Either Ident Ident
    _ -> ChoiceT Eval Expr
    forall a. ChoiceT Eval a
    mismatch -- different fields
                 Right RecordMap Ident Expr
    efs -> Expr -> ChoiceT Eval Expr
    forall a. a -> ChoiceT Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (RecordMap Ident Expr -> Expr
    ERec RecordMap Ident Expr
    efs)

          (TVNewtype Newtype
    nt [Either Nat' TValue]
    ts RecordMap Ident TValue
    tfs, VRecord RecordMap Ident (SEval Concrete Value)
    vfs) ->
            do -- NB, vfs first argument to keep their display order
               Either (Either Ident Ident) (RecordMap Ident Expr)
    res <- (Ident -> Eval Value -> TValue -> ChoiceT Eval Expr)
    -> RecordMap Ident (Eval Value)
    -> RecordMap Ident TValue
    -> ChoiceT
         Eval (Either (Either Ident Ident) (RecordMap Ident Expr))
    forall (t :: * -> *) a b c d.
    (Ord a, Monad t) =>
    (a -> b -> c -> t d)
    -> RecordMap a b
    -> RecordMap a c
    -> t (Either (Either a a) (RecordMap a d))
    zipRecordsM (\Ident
    _lbl Eval Value
    v TValue
    t -> TValue -> Value -> ChoiceT Eval Expr
    go TValue
    t (Value -> ChoiceT Eval Expr)
    -> ChoiceT Eval Value -> ChoiceT Eval Expr
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value -> ChoiceT Eval Value
    forall (m :: * -> *) a. Monad m => m a -> ChoiceT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift Eval Value
    v) RecordMap Ident (Eval Value)
    RecordMap Ident (SEval Concrete Value)
    vfs RecordMap Ident TValue
    tfs
               case Either (Either Ident Ident) (RecordMap Ident Expr)
    res of
                 Left Either Ident Ident
    _ -> ChoiceT Eval Expr
    forall a. ChoiceT Eval a
    mismatch -- different fields
                 Right RecordMap Ident Expr
    efs ->
                   let f :: Expr
    f = (Expr -> Either Nat' TValue -> Expr)
    -> Expr -> [Either Nat' TValue] -> Expr
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (\Expr
    x Either Nat' TValue
    t -> Expr -> Type -> Expr
    ETApp Expr
    x (Either Nat' TValue -> Type
    tNumValTy Either Nat' TValue
    t)) (Name -> Expr
    EVar (Newtype -> Name
    ntConName Newtype
    nt)) [Either Nat' TValue]
    ts
                    in Expr -> ChoiceT Eval Expr
    forall a. a -> ChoiceT Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr -> Expr -> Expr
    EApp Expr
    f (RecordMap Ident Expr -> Expr
    ERec RecordMap Ident Expr
    efs))

          (TVTuple [TValue]
    ts, VTuple [SEval Concrete Value]
    tvs) ->
            do Bool -> ChoiceT Eval ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard ([TValue] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TValue]
    ts Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [Eval Value] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Eval Value]
    [SEval Concrete Value]
    tvs)
               [Expr] -> Expr
    ETuple ([Expr] -> Expr) -> ChoiceT Eval [Expr] -> ChoiceT Eval Expr
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((TValue -> Value -> ChoiceT Eval Expr)
    -> [TValue] -> [Value] -> ChoiceT Eval [Expr]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM TValue -> Value -> ChoiceT Eval Expr
    go [TValue]
    ts ([Value] -> ChoiceT Eval [Expr])
    -> ChoiceT Eval [Value] -> ChoiceT Eval [Expr]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval [Value] -> ChoiceT Eval [Value]
    forall (m :: * -> *) a. Monad m => m a -> ChoiceT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift ([Eval Value] -> Eval [Value]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence [Eval Value]
    [SEval Concrete Value]
    tvs))
          (TValue
    TVBit, VBit SBit Concrete
    b) ->
            Expr -> ChoiceT Eval Expr
    forall a. a -> ChoiceT Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Text -> Expr
    prim (if Bool
    SBit Concrete
    b then Text
    "True" else Text
    "False"))
          (TValue
    TVInteger, VInteger SInteger Concrete
    i) ->
            Expr -> ChoiceT Eval Expr
    forall a. a -> ChoiceT Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Type -> Expr
    ETApp (Expr -> Type -> Expr
    ETApp (Text -> Expr
    prim Text
    "number") (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    SInteger Concrete
    i)) Type
    tInteger
          (TVIntMod Integer
    n, VInteger SInteger Concrete
    i) ->
            Expr -> ChoiceT Eval Expr
    forall a. a -> ChoiceT Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Type -> Expr
    ETApp (Expr -> Type -> Expr
    ETApp (Text -> Expr
    prim Text
    "number") (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    SInteger Concrete
    i)) (Type -> Type
    tIntMod (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n))

          (TValue
    TVRational, VRational (SRational SInteger Concrete
    n SInteger Concrete
    d)) ->
            do let n' :: Expr
    n' = Expr -> Type -> Expr
    ETApp (Expr -> Type -> Expr
    ETApp (Text -> Expr
    prim Text
    "number") (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    SInteger Concrete
    n)) Type
    tInteger
               let d' :: Expr
    d' = Expr -> Type -> Expr
    ETApp (Expr -> Type -> Expr
    ETApp (Text -> Expr
    prim Text
    "number") (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    SInteger Concrete
    d)) Type
    tInteger
               Expr -> ChoiceT Eval Expr
    forall a. a -> ChoiceT Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Expr -> Expr
    EApp (Expr -> Expr -> Expr
    EApp (Text -> Expr
    prim Text
    "ratio") Expr
    n') Expr
    d'

          (TVFloat Integer
    e Integer
    p, VFloat SFloat Concrete
    i) ->
               Expr -> ChoiceT Eval Expr
    forall a. a -> ChoiceT Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (PrimMap -> Type -> Type -> BigFloat -> Expr
    floatToExpr PrimMap
    prims (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    e) (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    p) (BF -> BigFloat
    bfValue BF
    SFloat Concrete
    i))
          (TVSeq Integer
    _ TValue
    b, VSeq Integer
    n SeqMap Concrete Value
    svs) ->
            do [Expr]
    ses <- (Value -> ChoiceT Eval Expr) -> [Value] -> ChoiceT Eval [Expr]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse (TValue -> Value -> ChoiceT Eval Expr
    go TValue
    b) ([Value] -> ChoiceT Eval [Expr])
    -> ChoiceT Eval [Value] -> ChoiceT Eval [Expr]
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval [Value] -> ChoiceT Eval [Value]
    forall (m :: * -> *) a. Monad m => m a -> ChoiceT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift ([Eval Value] -> Eval [Value]
    forall (t :: * -> *) (m :: * -> *) a.
    (Traversable t, Monad m) =>
    t (m a) -> m (t a)
    forall (m :: * -> *) a. Monad m => [m a] -> m [a]
    sequence (Integer -> SeqMap Concrete Value -> [SEval Concrete Value]
    forall sym n a.
    (Backend sym, Integral n) =>
    n -> SeqMap sym a -> [SEval sym a]
    enumerateSeqMap Integer
    n SeqMap Concrete Value
    svs))
               Expr -> ChoiceT Eval Expr
    forall a. a -> ChoiceT Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
    forall a b. (a -> b) -> a -> b
    $ [Expr] -> Type -> Expr
    EList [Expr]
    ses (TValue -> Type
    tValTy TValue
    b)
          (TVSeq Integer
    n TValue
    TVBit, VWord Integer
    _ WordValue Concrete
    wval) ->
            do BV Integer
    _ Integer
    v <- Eval BV -> ChoiceT Eval BV
    forall (m :: * -> *) a. Monad m => m a -> ChoiceT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift (Concrete -> WordValue Concrete -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> SEval sym (SWord sym)
    asWordVal Concrete
    Concrete WordValue Concrete
    wval)
               Expr -> ChoiceT Eval Expr
    forall a. a -> ChoiceT Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
    forall a b. (a -> b) -> a -> b
    $ Expr -> Type -> Expr
    ETApp (Expr -> Type -> Expr
    ETApp (Text -> Expr
    prim Text
    "number") (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    v)) (Type -> Type
    tWord (Integer -> Type
    forall a. Integral a => a -> Type
    tNum Integer
    n))

          (TValue
    _,VStream{})  -> ChoiceT Eval Expr
    forall a. ChoiceT Eval a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
          (TValue
    _,VFun{})     -> ChoiceT Eval Expr
    forall a. ChoiceT Eval a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
          (TValue
    _,VPoly{})    -> ChoiceT Eval Expr
    forall a. ChoiceT Eval a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
          (TValue
    _,VNumPoly{}) -> ChoiceT Eval Expr
    forall a. ChoiceT Eval a
    forall (m :: * -> *) a. MonadPlus m => m a
    mzero
          (TValue, Value)
    _ -> ChoiceT Eval Expr
    forall a. ChoiceT Eval a
    mismatch
        where
          mismatch :: forall a. ChoiceT Eval a
          mismatch :: forall a. ChoiceT Eval a
    mismatch =
            do Doc
    doc <- Eval Doc -> ChoiceT Eval Doc
    forall (m :: * -> *) a. Monad m => m a -> ChoiceT m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift (Concrete -> PPOpts -> Value -> SEval Concrete Doc
    forall sym.
    Backend sym =>
    sym -> PPOpts -> GenValue sym -> SEval sym Doc
    ppValue Concrete
    Concrete PPOpts
    defaultPPOpts Value
    val)
               String -> [String] -> ChoiceT Eval a
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "Cryptol.Eval.Concrete.toExpr"
                 [String
    "type mismatch:"
                 , Type -> String
    forall a. PP a => a -> String
    pretty (TValue -> Type
    tValTy TValue
    ty)
                 , Doc -> String
    forall a. Show a => a -> String
    show Doc
    doc
                 ]

    floatToExpr :: PrimMap -> AST.Type -> AST.Type -> FP.BigFloat -> AST.Expr
    floatToExpr :: PrimMap -> Type -> Type -> BigFloat -> Expr
    floatToExpr PrimMap
    prims Type
    eT Type
    pT BigFloat
    f =
      case BigFloat -> BFRep
    FP.bfToRep BigFloat
    f of
        BFRep
    FP.BFNaN -> Text -> Expr
    mkP Text
    "fpNaN"
        FP.BFRep Sign
    sign BFNum
    num ->
          case (Sign
    sign,BFNum
    num) of
            (Sign
    FP.Pos, BFNum
    FP.Zero)   -> Text -> Expr
    mkP Text
    "fpPosZero"
            (Sign
    FP.Neg, BFNum
    FP.Zero)   -> Text -> Expr
    mkP Text
    "fpNegZero"
            (Sign
    FP.Pos, BFNum
    FP.Inf)    -> Text -> Expr
    mkP Text
    "fpPosInf"
            (Sign
    FP.Neg, BFNum
    FP.Inf)    -> Text -> Expr
    mkP Text
    "fpNegInf"
            (Sign
    _, FP.Num Integer
    m Int64
    e) ->
                let r :: Rational
    r = Integer -> Rational
    forall a. Real a => a -> Rational
    toRational Integer
    m Rational -> Rational -> Rational
    forall a. Num a => a -> a -> a
    * (Rational
    2 Rational -> Int64 -> Rational
    forall a b. (Fractional a, Integral b) => a -> b -> a
    ^^ Int64
    e)
                in Expr -> Expr
    EProofApp (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ PrimMap -> PrimIdent -> Expr
    ePrim PrimMap
    prims (Text -> PrimIdent
    prelPrim Text
    "fraction")
                              Expr -> Type -> Expr
    `ETApp` Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Rational -> Integer
    forall a. Ratio a -> a
    numerator Rational
    r)
                              Expr -> Type -> Expr
    `ETApp` Integer -> Type
    forall a. Integral a => a -> Type
    tNum (Rational -> Integer
    forall a. Ratio a -> a
    denominator Rational
    r)
                              Expr -> Type -> Expr
    `ETApp` Int -> Type
    forall a. Integral a => a -> Type
    tNum (Int
    0 :: Int)
                              Expr -> Type -> Expr
    `ETApp` Type -> Type -> Type
    tFloat Type
    eT Type
    pT
      where
      mkP :: Text -> Expr
    mkP Text
    n = Expr -> Expr
    EProofApp (Expr -> Expr) -> Expr -> Expr
    forall a b. (a -> b) -> a -> b
    $ PrimMap -> PrimIdent -> Expr
    ePrim PrimMap
    prims (Text -> PrimIdent
    floatPrim Text
    n) Expr -> Type -> Expr
    `ETApp` Type
    eT Expr -> Type -> Expr
    `ETApp` Type
    pT

    -- Primitives ------------------------------------------------------------------

    primTable :: IO EvalOpts -> Map PrimIdent (Prim Concrete)
    primTable :: IO EvalOpts -> Map PrimIdent (Prim Concrete)
    primTable IO EvalOpts
    getEOpts = let sym :: Concrete
    sym = Concrete
    Concrete in
      Map PrimIdent (Prim Concrete)
    -> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (Concrete -> IO EvalOpts -> Map PrimIdent (Prim Concrete)
    forall sym.
    Backend sym =>
    sym -> IO EvalOpts -> Map PrimIdent (Prim sym)
    genericPrimTable Concrete
    sym IO EvalOpts
    getEOpts) (Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete))
    -> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
    forall a b. (a -> b) -> a -> b
    $
      Map PrimIdent (Prim Concrete)
    -> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union (Concrete -> Map PrimIdent (Prim Concrete)
    forall sym. Backend sym => sym -> Map PrimIdent (Prim sym)
    genericFloatTable Concrete
    sym) (Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete))
    -> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
    forall a b. (a -> b) -> a -> b
    $
      Map PrimIdent (Prim Concrete)
    -> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map PrimIdent (Prim Concrete)
    suiteBPrims (Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete))
    -> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
    forall a b. (a -> b) -> a -> b
    $
      Map PrimIdent (Prim Concrete)
    -> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map PrimIdent (Prim Concrete)
    primeECPrims (Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete))
    -> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
    forall a b. (a -> b) -> a -> b
    $

      [(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete)
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete))
    -> [(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete)
    forall a b. (a -> b) -> a -> b
    $ ((Text, Prim Concrete) -> (PrimIdent, Prim Concrete))
    -> [(Text, Prim Concrete)] -> [(PrimIdent, Prim Concrete)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Text
    n, Prim Concrete
    v) -> (Text -> PrimIdent
    prelPrim Text
    n, Prim Concrete
    v))

      [ -- Indexing and updates
        (Text
    "@"          , {-# SCC "Prelude::(@)" #-}
                        Concrete
    -> IndexDirection
    -> (Nat'
        -> TValue
        -> SeqMap Concrete Value
        -> TValue
        -> SInteger Concrete
        -> SEval Concrete Value)
    -> (Nat'
        -> TValue
        -> SeqMap Concrete Value
        -> TValue
        -> Integer
        -> [IndexSegment Concrete]
        -> SEval Concrete Value)
    -> Prim Concrete
    forall sym.
    Backend sym =>
    sym
    -> IndexDirection
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> TValue
        -> SInteger sym
        -> SEval sym (GenValue sym))
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> TValue
        -> Integer
        -> [IndexSegment sym]
        -> SEval sym (GenValue sym))
    -> Prim sym
    indexPrim Concrete
    sym IndexDirection
    IndexForward Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> TValue
    -> Integer
    -> Eval Value
    Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> TValue
    -> SInteger Concrete
    -> SEval Concrete Value
    indexFront_int Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> TValue
    -> Integer
    -> [IndexSegment Concrete]
    -> Eval Value
    Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> TValue
    -> Integer
    -> [IndexSegment Concrete]
    -> SEval Concrete Value
    indexFront_segs)
      , (Text
    "!"          , {-# SCC "Prelude::(!)" #-}
                        Concrete
    -> IndexDirection
    -> (Nat'
        -> TValue
        -> SeqMap Concrete Value
        -> TValue
        -> SInteger Concrete
        -> SEval Concrete Value)
    -> (Nat'
        -> TValue
        -> SeqMap Concrete Value
        -> TValue
        -> Integer
        -> [IndexSegment Concrete]
        -> SEval Concrete Value)
    -> Prim Concrete
    forall sym.
    Backend sym =>
    sym
    -> IndexDirection
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> TValue
        -> SInteger sym
        -> SEval sym (GenValue sym))
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> TValue
        -> Integer
        -> [IndexSegment sym]
        -> SEval sym (GenValue sym))
    -> Prim sym
    indexPrim Concrete
    sym IndexDirection
    IndexBackward Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> TValue
    -> Integer
    -> Eval Value
    Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> TValue
    -> SInteger Concrete
    -> SEval Concrete Value
    indexFront_int Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> TValue
    -> Integer
    -> [IndexSegment Concrete]
    -> Eval Value
    Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> TValue
    -> Integer
    -> [IndexSegment Concrete]
    -> SEval Concrete Value
    indexFront_segs)

      , (Text
    "update"     , {-# SCC "Prelude::update" #-}
                        Concrete
    -> (Nat'
        -> TValue
        -> WordValue Concrete
        -> Either (SInteger Concrete) (WordValue Concrete)
        -> SEval Concrete Value
        -> SEval Concrete (WordValue Concrete))
    -> (Nat'
        -> TValue
        -> SeqMap Concrete Value
        -> Either (SInteger Concrete) (WordValue Concrete)
        -> SEval Concrete Value
        -> SEval Concrete (SeqMap Concrete Value))
    -> Prim Concrete
    forall sym.
    Backend sym =>
    sym
    -> (Nat'
        -> TValue
        -> WordValue sym
        -> Either (SInteger sym) (WordValue sym)
        -> SEval sym (GenValue sym)
        -> SEval sym (WordValue sym))
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> Either (SInteger sym) (WordValue sym)
        -> SEval sym (GenValue sym)
        -> SEval sym (SeqMap sym (GenValue sym)))
    -> Prim sym
    updatePrim Concrete
    sym Nat'
    -> TValue
    -> WordValue Concrete
    -> Either Integer (WordValue Concrete)
    -> Eval Value
    -> Eval (WordValue Concrete)
    Nat'
    -> TValue
    -> WordValue Concrete
    -> Either (SInteger Concrete) (WordValue Concrete)
    -> SEval Concrete Value
    -> SEval Concrete (WordValue Concrete)
    updateFront_word Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> Either Integer (WordValue Concrete)
    -> Eval Value
    -> Eval (SeqMap Concrete Value)
    Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> Either (SInteger Concrete) (WordValue Concrete)
    -> SEval Concrete Value
    -> SEval Concrete (SeqMap Concrete Value)
    updateFront)

      , (Text
    "updateEnd"  , {-# SCC "Prelude::updateEnd" #-}
                        Concrete
    -> (Nat'
        -> TValue
        -> WordValue Concrete
        -> Either (SInteger Concrete) (WordValue Concrete)
        -> SEval Concrete Value
        -> SEval Concrete (WordValue Concrete))
    -> (Nat'
        -> TValue
        -> SeqMap Concrete Value
        -> Either (SInteger Concrete) (WordValue Concrete)
        -> SEval Concrete Value
        -> SEval Concrete (SeqMap Concrete Value))
    -> Prim Concrete
    forall sym.
    Backend sym =>
    sym
    -> (Nat'
        -> TValue
        -> WordValue sym
        -> Either (SInteger sym) (WordValue sym)
        -> SEval sym (GenValue sym)
        -> SEval sym (WordValue sym))
    -> (Nat'
        -> TValue
        -> SeqMap sym (GenValue sym)
        -> Either (SInteger sym) (WordValue sym)
        -> SEval sym (GenValue sym)
        -> SEval sym (SeqMap sym (GenValue sym)))
    -> Prim sym
    updatePrim Concrete
    sym Nat'
    -> TValue
    -> WordValue Concrete
    -> Either Integer (WordValue Concrete)
    -> Eval Value
    -> Eval (WordValue Concrete)
    Nat'
    -> TValue
    -> WordValue Concrete
    -> Either (SInteger Concrete) (WordValue Concrete)
    -> SEval Concrete Value
    -> SEval Concrete (WordValue Concrete)
    updateBack_word Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> Either Integer (WordValue Concrete)
    -> Eval Value
    -> Eval (SeqMap Concrete Value)
    Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> Either (SInteger Concrete) (WordValue Concrete)
    -> SEval Concrete Value
    -> SEval Concrete (SeqMap Concrete Value)
    updateBack)

       , (Text
    "pmult",
            (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    u ->
            (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    v ->
            (SWord Concrete -> Prim Concrete) -> Prim Concrete
    forall sym. (SWord sym -> Prim sym) -> Prim sym
    PWordFun \(BV Integer
    _ Integer
    x) ->
            (SWord Concrete -> Prim Concrete) -> Prim Concrete
    forall sym. (SWord sym -> Prim sym) -> Prim sym
    PWordFun \(BV Integer
    _ Integer
    y) ->
            SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
                let z :: Integer
    z = if Integer
    u Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Integer
    v then
                          Int -> Integer -> Integer -> Integer
    F2.pmult (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer
    uInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1)) Integer
    x Integer
    y
                        else
                          Int -> Integer -> Integer -> Integer
    F2.pmult (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer
    vInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    1)) Integer
    y Integer
    x
                 in Value -> Eval Value
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Value -> Eval Value)
    -> (Integer -> Value) -> Integer -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord (Integer
    1Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    uInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    v) (WordValue Concrete -> Value)
    -> (Integer -> WordValue Concrete) -> Integer -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Integer -> BV) -> Integer -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    mkBv (Integer
    1Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    uInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    v) (Integer -> Eval Value) -> Integer -> Eval Value
    forall a b. (a -> b) -> a -> b
    $! Integer
    z)

       , (Text
    "pmod",
            (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    _u ->
            (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    v ->
            (SWord Concrete -> Prim Concrete) -> Prim Concrete
    forall sym. (SWord sym -> Prim sym) -> Prim sym
    PWordFun \(BV Integer
    w Integer
    x) ->
            (SWord Concrete -> Prim Concrete) -> Prim Concrete
    forall sym. (SWord sym -> Prim sym) -> Prim sym
    PWordFun \(BV Integer
    _ Integer
    m) ->
            SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
              do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition Concrete
    sym (Integer
    m Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0) EvalError
    DivideByZero
                 Value -> Eval Value
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Value -> Eval Value)
    -> (Integer -> Value) -> Integer -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    v (WordValue Concrete -> Value)
    -> (Integer -> WordValue Concrete) -> Integer -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Integer -> BV) -> Integer -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    mkBv Integer
    v (Integer -> Eval Value) -> Integer -> Eval Value
    forall a b. (a -> b) -> a -> b
    $! Int -> Integer -> Integer -> Integer
    F2.pmod (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    w) Integer
    x Integer
    m)

      , (Text
    "pdiv",
            (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    _u ->
            (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    _v ->
            (SWord Concrete -> Prim Concrete) -> Prim Concrete
    forall sym. (SWord sym -> Prim sym) -> Prim sym
    PWordFun \(BV Integer
    w Integer
    x) ->
            (SWord Concrete -> Prim Concrete) -> Prim Concrete
    forall sym. (SWord sym -> Prim sym) -> Prim sym
    PWordFun \(BV Integer
    _ Integer
    m) ->
            SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
              do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
    forall sym.
    Backend sym =>
    sym -> SBit sym -> EvalError -> SEval sym ()
    assertSideCondition Concrete
    sym (Integer
    m Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Integer
    0) EvalError
    DivideByZero
                 Value -> Eval Value
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Value -> Eval Value)
    -> (Integer -> Value) -> Integer -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    w (WordValue Concrete -> Value)
    -> (Integer -> WordValue Concrete) -> Integer -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Integer -> BV) -> Integer -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    mkBv Integer
    w (Integer -> Eval Value) -> Integer -> Eval Value
    forall a b. (a -> b) -> a -> b
    $! Int -> Integer -> Integer -> Integer
    F2.pdiv (Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger Integer
    w) Integer
    x Integer
    m)
      ]

    primeECPrims :: Map.Map PrimIdent (Prim Concrete)
    primeECPrims :: Map PrimIdent (Prim Concrete)
    primeECPrims = [(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete)
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete))
    -> [(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete)
    forall a b. (a -> b) -> a -> b
    $ ((Text, Prim Concrete) -> (PrimIdent, Prim Concrete))
    -> [(Text, Prim Concrete)] -> [(PrimIdent, Prim Concrete)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Text
    n,Prim Concrete
    v) -> (Text -> PrimIdent
    primeECPrim Text
    n, Prim Concrete
    v))
      [ (Text
    "ec_double", {-# SCC "PrimeEC::ec_double" #-}
           (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    p ->
           (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    s ->
           SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
              do ProjectivePoint
    s' <- Value -> Eval ProjectivePoint
    toProjectivePoint (Value -> Eval ProjectivePoint)
    -> Eval Value -> Eval ProjectivePoint
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value
    SEval Concrete Value
    s
                 let r :: ProjectivePoint
    r = PrimeModulus -> ProjectivePoint -> ProjectivePoint
    PrimeEC.ec_double (Integer -> PrimeModulus
    PrimeEC.primeModulus Integer
    p) ProjectivePoint
    s'
                 ProjectivePoint -> Eval Value
    fromProjectivePoint (ProjectivePoint -> Eval Value) -> ProjectivePoint -> Eval Value
    forall a b. (a -> b) -> a -> b
    $! ProjectivePoint
    r)

      , (Text
    "ec_add_nonzero", {-# SCC "PrimeEC::ec_add_nonzero" #-}
           (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    p ->
           (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    s ->
           (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    t ->
           SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
              do ProjectivePoint
    s' <- Value -> Eval ProjectivePoint
    toProjectivePoint (Value -> Eval ProjectivePoint)
    -> Eval Value -> Eval ProjectivePoint
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value
    SEval Concrete Value
    s
                 ProjectivePoint
    t' <- Value -> Eval ProjectivePoint
    toProjectivePoint (Value -> Eval ProjectivePoint)
    -> Eval Value -> Eval ProjectivePoint
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value
    SEval Concrete Value
    t
                 let r :: ProjectivePoint
    r = PrimeModulus
    -> ProjectivePoint -> ProjectivePoint -> ProjectivePoint
    PrimeEC.ec_add_nonzero (Integer -> PrimeModulus
    PrimeEC.primeModulus Integer
    p) ProjectivePoint
    s' ProjectivePoint
    t'
                 ProjectivePoint -> Eval Value
    fromProjectivePoint (ProjectivePoint -> Eval Value) -> ProjectivePoint -> Eval Value
    forall a b. (a -> b) -> a -> b
    $! ProjectivePoint
    r)

      , (Text
    "ec_mult", {-# SCC "PrimeEC::ec_mult" #-}
           (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    p ->
           (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    d ->
           (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    s ->
           SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
              do Integer
    d' <- Value -> Integer
    Value -> SInteger Concrete
    forall sym. GenValue sym -> SInteger sym
    fromVInteger (Value -> Integer) -> Eval Value -> Eval Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    d
                 ProjectivePoint
    s' <- Value -> Eval ProjectivePoint
    toProjectivePoint (Value -> Eval ProjectivePoint)
    -> Eval Value -> Eval ProjectivePoint
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value
    SEval Concrete Value
    s
                 let r :: ProjectivePoint
    r = PrimeModulus -> Integer -> ProjectivePoint -> ProjectivePoint
    PrimeEC.ec_mult (Integer -> PrimeModulus
    PrimeEC.primeModulus Integer
    p) Integer
    d' ProjectivePoint
    s'
                 ProjectivePoint -> Eval Value
    fromProjectivePoint (ProjectivePoint -> Eval Value) -> ProjectivePoint -> Eval Value
    forall a b. (a -> b) -> a -> b
    $! ProjectivePoint
    r)

      , (Text
    "ec_twin_mult", {-# SCC "PrimeEC::ec_twin_mult" #-}
           (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    p  ->
           (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    d0 ->
           (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    s  ->
           (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    d1 ->
           (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    t  ->
           SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
              do Integer
    d0' <- Value -> Integer
    Value -> SInteger Concrete
    forall sym. GenValue sym -> SInteger sym
    fromVInteger (Value -> Integer) -> Eval Value -> Eval Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    d0
                 ProjectivePoint
    s'  <- Value -> Eval ProjectivePoint
    toProjectivePoint (Value -> Eval ProjectivePoint)
    -> Eval Value -> Eval ProjectivePoint
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value
    SEval Concrete Value
    s
                 Integer
    d1' <- Value -> Integer
    Value -> SInteger Concrete
    forall sym. GenValue sym -> SInteger sym
    fromVInteger (Value -> Integer) -> Eval Value -> Eval Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    d1
                 ProjectivePoint
    t'  <- Value -> Eval ProjectivePoint
    toProjectivePoint (Value -> Eval ProjectivePoint)
    -> Eval Value -> Eval ProjectivePoint
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value
    SEval Concrete Value
    t
                 let r :: ProjectivePoint
    r = PrimeModulus
    -> Integer
    -> ProjectivePoint
    -> Integer
    -> ProjectivePoint
    -> ProjectivePoint
    PrimeEC.ec_twin_mult (Integer -> PrimeModulus
    PrimeEC.primeModulus Integer
    p) Integer
    d0' ProjectivePoint
    s' Integer
    d1' ProjectivePoint
    t'
                 ProjectivePoint -> Eval Value
    fromProjectivePoint (ProjectivePoint -> Eval Value) -> ProjectivePoint -> Eval Value
    forall a b. (a -> b) -> a -> b
    $! ProjectivePoint
    r)
      ]

    toProjectivePoint :: Value -> Eval PrimeEC.ProjectivePoint
    toProjectivePoint :: Value -> Eval ProjectivePoint
    toProjectivePoint Value
    v = Integer -> Integer -> Integer -> ProjectivePoint
    PrimeEC.toProjectivePoint (Integer -> Integer -> Integer -> ProjectivePoint)
    -> Eval Integer -> Eval (Integer -> Integer -> ProjectivePoint)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Ident -> Eval Integer
    f Ident
    "x" Eval (Integer -> Integer -> ProjectivePoint)
    -> Eval Integer -> Eval (Integer -> ProjectivePoint)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Ident -> Eval Integer
    f Ident
    "y" Eval (Integer -> ProjectivePoint)
    -> Eval Integer -> Eval ProjectivePoint
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Ident -> Eval Integer
    f Ident
    "z"
      where
       f :: Ident -> Eval Integer
    f Ident
    nm = Value -> Integer
    Value -> SInteger Concrete
    forall sym. GenValue sym -> SInteger sym
    fromVInteger (Value -> Integer) -> Eval Value -> Eval Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Ident -> Value -> SEval Concrete Value
    forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
    lookupRecord Ident
    nm Value
    v

    fromProjectivePoint :: PrimeEC.ProjectivePoint -> Eval Value
    fromProjectivePoint :: ProjectivePoint -> Eval Value
    fromProjectivePoint (PrimeEC.ProjectivePoint BigNat#
    x BigNat#
    y BigNat#
    z) =
       Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value)
    -> ([(Ident, Eval Value)] -> Value)
    -> [(Ident, Eval Value)]
    -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RecordMap Ident (Eval Value) -> Value
    RecordMap Ident (SEval Concrete Value) -> Value
    forall sym.
    RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
    VRecord (RecordMap Ident (Eval Value) -> Value)
    -> ([(Ident, Eval Value)] -> RecordMap Ident (Eval Value))
    -> [(Ident, Eval Value)]
    -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [(Ident, Eval Value)] -> RecordMap Ident (Eval Value)
    forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
    recordFromFields ([(Ident, Eval Value)] -> Eval Value)
    -> [(Ident, Eval Value)] -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ [(Ident
    "x", BigNat# -> Eval Value
    forall {sym} {f :: * -> *}.
    (SInteger sym ~ Integer, Applicative f) =>
    BigNat# -> f (GenValue sym)
    f BigNat#
    x), (Ident
    "y", BigNat# -> Eval Value
    forall {sym} {f :: * -> *}.
    (SInteger sym ~ Integer, Applicative f) =>
    BigNat# -> f (GenValue sym)
    f BigNat#
    y), (Ident
    "z", BigNat# -> Eval Value
    forall {sym} {f :: * -> *}.
    (SInteger sym ~ Integer, Applicative f) =>
    BigNat# -> f (GenValue sym)
    f BigNat#
    z)]
      where
       f :: BigNat# -> f (GenValue sym)
    f BigNat#
    i = GenValue sym -> f (GenValue sym)
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (SInteger sym -> GenValue sym
    forall sym. SInteger sym -> GenValue sym
    VInteger (BigNat# -> Integer
    PrimeEC.bigNatToInteger BigNat#
    i))

    suiteBPrims :: Map.Map PrimIdent (Prim Concrete)
    suiteBPrims :: Map PrimIdent (Prim Concrete)
    suiteBPrims = [(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete)
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete))
    -> [(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete)
    forall a b. (a -> b) -> a -> b
    $ ((Text, Prim Concrete) -> (PrimIdent, Prim Concrete))
    -> [(Text, Prim Concrete)] -> [(PrimIdent, Prim Concrete)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Text
    n, Prim Concrete
    v) -> (Text -> PrimIdent
    suiteBPrim Text
    n, Prim Concrete
    v))
      [ (Text
    "processSHA2_224", {-# SCC "SuiteB::processSHA2_224" #-}
         (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    n ->
         (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    xs ->
         SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
            do [Eval Value]
    blks <- Integer -> SeqMap Concrete Value -> [SEval Concrete Value]
    forall sym n a.
    (Backend sym, Integral n) =>
    n -> SeqMap sym a -> [SEval sym a]
    enumerateSeqMap Integer
    n (SeqMap Concrete Value -> [Eval Value])
    -> (Value -> SeqMap Concrete Value) -> Value -> [Eval Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq (Value -> [Eval Value]) -> Eval Value -> Eval [Eval Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    xs
               (SHA.SHA256S Word32
    w0 Word32
    w1 Word32
    w2 Word32
    w3 Word32
    w4 Word32
    w5 Word32
    w6 Word32
    _) <-
                  (SHA256State -> Eval Value -> Eval SHA256State)
    -> SHA256State -> [Eval Value] -> Eval SHA256State
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (\SHA256State
    st Eval Value
    blk -> SHA256State -> Eval SHA256State -> Eval SHA256State
    forall a b. a -> b -> b
    seq SHA256State
    st (SHA256State -> SHA256Block -> SHA256State
    SHA.processSHA256Block SHA256State
    st (SHA256Block -> SHA256State)
    -> Eval SHA256Block -> Eval SHA256State
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> Eval SHA256Block
    toSHA256Block (Value -> Eval SHA256Block) -> Eval Value -> Eval SHA256Block
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value
    blk)))
                        SHA256State
    SHA.initialSHA224State [Eval Value]
    blks
               let f :: Word32 -> Eval Value
                   f :: Word32 -> Eval Value
    f = Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> (Word32 -> Value) -> Word32 -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    32 (WordValue Concrete -> Value)
    -> (Word32 -> WordValue Concrete) -> Word32 -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Word32 -> BV) -> Word32 -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    BV Integer
    32 (Integer -> BV) -> (Word32 -> Integer) -> Word32 -> BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word32 -> Integer
    forall a. Integral a => a -> Integer
    toInteger
                   zs :: SeqMap Concrete Value
    zs = Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap Concrete
    Concrete ((Word32 -> Eval Value) -> [Word32] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Word32 -> Eval Value
    f [Word32
    w0,Word32
    w1,Word32
    w2,Word32
    w3,Word32
    w4,Word32
    w5,Word32
    w6])
               SeqMap Concrete Value -> Eval Value -> Eval Value
    forall a b. a -> b -> b
    seq SeqMap Concrete Value
    zs (Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> SeqMap Concrete Value -> Value
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    7 SeqMap Concrete Value
    zs)))

      , (Text
    "processSHA2_256", {-# SCC "SuiteB::processSHA2_256" #-}
         (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    n ->
         (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    xs ->
         SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
            do [Eval Value]
    blks <- Integer -> SeqMap Concrete Value -> [SEval Concrete Value]
    forall sym n a.
    (Backend sym, Integral n) =>
    n -> SeqMap sym a -> [SEval sym a]
    enumerateSeqMap Integer
    n (SeqMap Concrete Value -> [Eval Value])
    -> (Value -> SeqMap Concrete Value) -> Value -> [Eval Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq (Value -> [Eval Value]) -> Eval Value -> Eval [Eval Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    xs
               (SHA.SHA256S Word32
    w0 Word32
    w1 Word32
    w2 Word32
    w3 Word32
    w4 Word32
    w5 Word32
    w6 Word32
    w7) <-
                 (SHA256State -> Eval Value -> Eval SHA256State)
    -> SHA256State -> [Eval Value] -> Eval SHA256State
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (\SHA256State
    st Eval Value
    blk -> SHA256State -> Eval SHA256State -> Eval SHA256State
    forall a b. a -> b -> b
    seq SHA256State
    st (SHA256State -> SHA256Block -> SHA256State
    SHA.processSHA256Block SHA256State
    st (SHA256Block -> SHA256State)
    -> Eval SHA256Block -> Eval SHA256State
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> Eval SHA256Block
    toSHA256Block (Value -> Eval SHA256Block) -> Eval Value -> Eval SHA256Block
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value
    blk)))
                       SHA256State
    SHA.initialSHA256State [Eval Value]
    blks
               let f :: Word32 -> Eval Value
                   f :: Word32 -> Eval Value
    f = Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> (Word32 -> Value) -> Word32 -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    32 (WordValue Concrete -> Value)
    -> (Word32 -> WordValue Concrete) -> Word32 -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Word32 -> BV) -> Word32 -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    BV Integer
    32 (Integer -> BV) -> (Word32 -> Integer) -> Word32 -> BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word32 -> Integer
    forall a. Integral a => a -> Integer
    toInteger
                   zs :: SeqMap Concrete Value
    zs = Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap Concrete
    Concrete ((Word32 -> Eval Value) -> [Word32] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Word32 -> Eval Value
    f [Word32
    w0,Word32
    w1,Word32
    w2,Word32
    w3,Word32
    w4,Word32
    w5,Word32
    w6,Word32
    w7])
               SeqMap Concrete Value -> Eval Value -> Eval Value
    forall a b. a -> b -> b
    seq SeqMap Concrete Value
    zs (Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> SeqMap Concrete Value -> Value
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    8 SeqMap Concrete Value
    zs)))

      , (Text
    "processSHA2_384", {-# SCC "SuiteB::processSHA2_384" #-}
         (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    n ->
         (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    xs ->
         SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
            do [Eval Value]
    blks <- Integer -> SeqMap Concrete Value -> [SEval Concrete Value]
    forall sym n a.
    (Backend sym, Integral n) =>
    n -> SeqMap sym a -> [SEval sym a]
    enumerateSeqMap Integer
    n (SeqMap Concrete Value -> [Eval Value])
    -> (Value -> SeqMap Concrete Value) -> Value -> [Eval Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq (Value -> [Eval Value]) -> Eval Value -> Eval [Eval Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    xs
               (SHA.SHA512S Word64
    w0 Word64
    w1 Word64
    w2 Word64
    w3 Word64
    w4 Word64
    w5 Word64
    _ Word64
    _) <-
                 (SHA512State -> Eval Value -> Eval SHA512State)
    -> SHA512State -> [Eval Value] -> Eval SHA512State
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (\SHA512State
    st Eval Value
    blk -> SHA512State -> Eval SHA512State -> Eval SHA512State
    forall a b. a -> b -> b
    seq SHA512State
    st (SHA512State -> SHA512Block -> SHA512State
    SHA.processSHA512Block SHA512State
    st (SHA512Block -> SHA512State)
    -> Eval SHA512Block -> Eval SHA512State
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> Eval SHA512Block
    toSHA512Block (Value -> Eval SHA512Block) -> Eval Value -> Eval SHA512Block
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value
    blk)))
                       SHA512State
    SHA.initialSHA384State [Eval Value]
    blks
               let f :: Word64 -> Eval Value
                   f :: Word64 -> Eval Value
    f = Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> (Word64 -> Value) -> Word64 -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    64 (WordValue Concrete -> Value)
    -> (Word64 -> WordValue Concrete) -> Word64 -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Word64 -> BV) -> Word64 -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    BV Integer
    64 (Integer -> BV) -> (Word64 -> Integer) -> Word64 -> BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word64 -> Integer
    forall a. Integral a => a -> Integer
    toInteger
                   zs :: SeqMap Concrete Value
    zs = Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap Concrete
    Concrete ((Word64 -> Eval Value) -> [Word64] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Word64 -> Eval Value
    f [Word64
    w0,Word64
    w1,Word64
    w2,Word64
    w3,Word64
    w4,Word64
    w5])
               SeqMap Concrete Value -> Eval Value -> Eval Value
    forall a b. a -> b -> b
    seq SeqMap Concrete Value
    zs (Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> SeqMap Concrete Value -> Value
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    6 SeqMap Concrete Value
    zs)))

      , (Text
    "processSHA2_512", {-# SCC "SuiteB::processSHA2_512" #-}
         (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    n ->
         (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    xs ->
         SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
            do [Eval Value]
    blks <- Integer -> SeqMap Concrete Value -> [SEval Concrete Value]
    forall sym n a.
    (Backend sym, Integral n) =>
    n -> SeqMap sym a -> [SEval sym a]
    enumerateSeqMap Integer
    n (SeqMap Concrete Value -> [Eval Value])
    -> (Value -> SeqMap Concrete Value) -> Value -> [Eval Value]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq (Value -> [Eval Value]) -> Eval Value -> Eval [Eval Value]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    xs
               (SHA.SHA512S Word64
    w0 Word64
    w1 Word64
    w2 Word64
    w3 Word64
    w4 Word64
    w5 Word64
    w6 Word64
    w7) <-
                 (SHA512State -> Eval Value -> Eval SHA512State)
    -> SHA512State -> [Eval Value] -> Eval SHA512State
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (\SHA512State
    st Eval Value
    blk -> SHA512State -> Eval SHA512State -> Eval SHA512State
    forall a b. a -> b -> b
    seq SHA512State
    st (SHA512State -> SHA512Block -> SHA512State
    SHA.processSHA512Block SHA512State
    st (SHA512Block -> SHA512State)
    -> Eval SHA512Block -> Eval SHA512State
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Value -> Eval SHA512Block
    toSHA512Block (Value -> Eval SHA512Block) -> Eval Value -> Eval SHA512Block
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Eval Value
    blk)))
                       SHA512State
    SHA.initialSHA512State [Eval Value]
    blks
               let f :: Word64 -> Eval Value
                   f :: Word64 -> Eval Value
    f = Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> (Word64 -> Value) -> Word64 -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    64 (WordValue Concrete -> Value)
    -> (Word64 -> WordValue Concrete) -> Word64 -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Word64 -> BV) -> Word64 -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    BV Integer
    64 (Integer -> BV) -> (Word64 -> Integer) -> Word64 -> BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word64 -> Integer
    forall a. Integral a => a -> Integer
    toInteger
                   zs :: SeqMap Concrete Value
    zs = Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap Concrete
    Concrete ((Word64 -> Eval Value) -> [Word64] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Word64 -> Eval Value
    f [Word64
    w0,Word64
    w1,Word64
    w2,Word64
    w3,Word64
    w4,Word64
    w5,Word64
    w6,Word64
    w7])
               SeqMap Concrete Value -> Eval Value -> Eval Value
    forall a b. a -> b -> b
    seq SeqMap Concrete Value
    zs (Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> SeqMap Concrete Value -> Value
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    8 SeqMap Concrete Value
    zs)))

      , (Text
    "AESKeyExpand", {-# SCC "SuiteB::AESKeyExpand" #-}
          (Integer -> Prim Concrete) -> Prim Concrete
    forall sym. (Integer -> Prim sym) -> Prim sym
    PFinPoly \Integer
    k ->
          (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun     \SEval Concrete Value
    seed ->
          SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
             do SeqMap Concrete Value
    ss <- Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq (Value -> SeqMap Concrete Value)
    -> Eval Value -> Eval (SeqMap Concrete Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    seed
                let toWord :: Integer -> Eval Word32
                    toWord :: Integer -> Eval Word32
    toWord Integer
    i = Integer -> Word32
    forall a. Num a => Integer -> a
    fromInteger(Integer -> Word32) -> (BV -> Integer) -> BV -> Word32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV -> Integer
    bvVal (BV -> Word32) -> Eval BV -> Eval Word32
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Concrete -> String -> Value -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> String -> GenValue sym -> SEval sym (SWord sym)
    fromVWord Concrete
    Concrete String
    "AESInfKeyExpand" (Value -> Eval BV) -> Eval Value -> Eval BV
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SeqMap Concrete Value -> Integer -> SEval Concrete Value
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap Concrete Value
    ss Integer
    i)
                let fromWord :: Word32 -> Eval Value
                    fromWord :: Word32 -> Eval Value
    fromWord = Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> (Word32 -> Value) -> Word32 -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    32 (WordValue Concrete -> Value)
    -> (Word32 -> WordValue Concrete) -> Word32 -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Word32 -> BV) -> Word32 -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    BV Integer
    32 (Integer -> BV) -> (Word32 -> Integer) -> Word32 -> BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word32 -> Integer
    forall a. Integral a => a -> Integer
    toInteger
                [Word32]
    kws <- (Integer -> Eval Word32) -> [Integer] -> Eval [Word32]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Integer -> Eval Word32
    toWord [Integer
    0 .. Integer
    kInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1]
                let ws :: [Word32]
    ws = Integer -> [Word32] -> [Word32]
    AES.keyExpansionWords Integer
    k [Word32]
    kws
                let len :: Integer
    len = Integer
    4Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *(Integer
    kInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    +Integer
    7)
                Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Integer -> SeqMap Concrete Value -> Value
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    len (Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap Concrete
    Concrete ((Word32 -> Eval Value) -> [Word32] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Word32 -> Eval Value
    fromWord [Word32]
    ws))))

      , (Text
    "AESInvMixColumns", {-# SCC "SuiteB::AESInvMixColumns" #-}
          (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun \SEval Concrete Value
    st ->
          SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
             do SeqMap Concrete Value
    ss <- Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq (Value -> SeqMap Concrete Value)
    -> Eval Value -> Eval (SeqMap Concrete Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    st
                let toWord :: Integer -> Eval Word32
                    toWord :: Integer -> Eval Word32
    toWord Integer
    i = Integer -> Word32
    forall a. Num a => Integer -> a
    fromInteger(Integer -> Word32) -> (BV -> Integer) -> BV -> Word32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV -> Integer
    bvVal (BV -> Word32) -> Eval BV -> Eval Word32
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Concrete -> String -> Value -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> String -> GenValue sym -> SEval sym (SWord sym)
    fromVWord Concrete
    Concrete String
    "AESInvMixColumns" (Value -> Eval BV) -> Eval Value -> Eval BV
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SeqMap Concrete Value -> Integer -> SEval Concrete Value
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap Concrete Value
    ss Integer
    i)
                let fromWord :: Word32 -> Eval Value
                    fromWord :: Word32 -> Eval Value
    fromWord = Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> (Word32 -> Value) -> Word32 -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    32 (WordValue Concrete -> Value)
    -> (Word32 -> WordValue Concrete) -> Word32 -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Word32 -> BV) -> Word32 -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    BV Integer
    32 (Integer -> BV) -> (Word32 -> Integer) -> Word32 -> BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word32 -> Integer
    forall a. Integral a => a -> Integer
    toInteger
                [Word32]
    ws <- (Integer -> Eval Word32) -> [Integer] -> Eval [Word32]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Integer -> Eval Word32
    toWord [Integer
    0,Integer
    1,Integer
    2,Integer
    3]
                let ws' :: [Word32]
    ws' = [Word32] -> [Word32]
    AES.invMixColumns [Word32]
    ws
                Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value)
    -> ([Word32] -> Value) -> [Word32] -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> SeqMap Concrete Value -> Value
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    4 (SeqMap Concrete Value -> Value)
    -> ([Word32] -> SeqMap Concrete Value) -> [Word32] -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap Concrete
    Concrete ([Eval Value] -> SeqMap Concrete Value)
    -> ([Word32] -> [Eval Value]) -> [Word32] -> SeqMap Concrete Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Word32 -> Eval Value) -> [Word32] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Word32 -> Eval Value
    fromWord ([Word32] -> Eval Value) -> [Word32] -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ [Word32]
    ws')

      , (Text
    "AESEncRound", {-# SCC "SuiteB::AESEncRound" #-}
          (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun \SEval Concrete Value
    st ->
          SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
             do SeqMap Concrete Value
    ss <- Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq (Value -> SeqMap Concrete Value)
    -> Eval Value -> Eval (SeqMap Concrete Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    st
                let toWord :: Integer -> Eval Word32
                    toWord :: Integer -> Eval Word32
    toWord Integer
    i = Integer -> Word32
    forall a. Num a => Integer -> a
    fromInteger(Integer -> Word32) -> (BV -> Integer) -> BV -> Word32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV -> Integer
    bvVal (BV -> Word32) -> Eval BV -> Eval Word32
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Concrete -> String -> Value -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> String -> GenValue sym -> SEval sym (SWord sym)
    fromVWord Concrete
    Concrete String
    "AESEncRound" (Value -> Eval BV) -> Eval Value -> Eval BV
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SeqMap Concrete Value -> Integer -> SEval Concrete Value
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap Concrete Value
    ss Integer
    i)
                let fromWord :: Word32 -> Eval Value
                    fromWord :: Word32 -> Eval Value
    fromWord = Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> (Word32 -> Value) -> Word32 -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    32 (WordValue Concrete -> Value)
    -> (Word32 -> WordValue Concrete) -> Word32 -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Word32 -> BV) -> Word32 -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    BV Integer
    32 (Integer -> BV) -> (Word32 -> Integer) -> Word32 -> BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word32 -> Integer
    forall a. Integral a => a -> Integer
    toInteger
                [Word32]
    ws <- (Integer -> Eval Word32) -> [Integer] -> Eval [Word32]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Integer -> Eval Word32
    toWord [Integer
    0,Integer
    1,Integer
    2,Integer
    3]
                let ws' :: [Word32]
    ws' = [Word32] -> [Word32]
    AES.aesRound [Word32]
    ws
                Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value)
    -> ([Word32] -> Value) -> [Word32] -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> SeqMap Concrete Value -> Value
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    4 (SeqMap Concrete Value -> Value)
    -> ([Word32] -> SeqMap Concrete Value) -> [Word32] -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap Concrete
    Concrete ([Eval Value] -> SeqMap Concrete Value)
    -> ([Word32] -> [Eval Value]) -> [Word32] -> SeqMap Concrete Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Word32 -> Eval Value) -> [Word32] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Word32 -> Eval Value
    fromWord ([Word32] -> Eval Value) -> [Word32] -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ [Word32]
    ws')

      , (Text
    "AESEncFinalRound", {-# SCC "SuiteB::AESEncFinalRound" #-}
         (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun \SEval Concrete Value
    st ->
         SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
             do SeqMap Concrete Value
    ss <- Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq (Value -> SeqMap Concrete Value)
    -> Eval Value -> Eval (SeqMap Concrete Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    st
                let toWord :: Integer -> Eval Word32
                    toWord :: Integer -> Eval Word32
    toWord Integer
    i = Integer -> Word32
    forall a. Num a => Integer -> a
    fromInteger(Integer -> Word32) -> (BV -> Integer) -> BV -> Word32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV -> Integer
    bvVal (BV -> Word32) -> Eval BV -> Eval Word32
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Concrete -> String -> Value -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> String -> GenValue sym -> SEval sym (SWord sym)
    fromVWord Concrete
    Concrete String
    "AESEncFinalRound" (Value -> Eval BV) -> Eval Value -> Eval BV
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SeqMap Concrete Value -> Integer -> SEval Concrete Value
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap Concrete Value
    ss Integer
    i)
                let fromWord :: Word32 -> Eval Value
                    fromWord :: Word32 -> Eval Value
    fromWord = Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> (Word32 -> Value) -> Word32 -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    32 (WordValue Concrete -> Value)
    -> (Word32 -> WordValue Concrete) -> Word32 -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Word32 -> BV) -> Word32 -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    BV Integer
    32 (Integer -> BV) -> (Word32 -> Integer) -> Word32 -> BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word32 -> Integer
    forall a. Integral a => a -> Integer
    toInteger
                [Word32]
    ws <- (Integer -> Eval Word32) -> [Integer] -> Eval [Word32]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Integer -> Eval Word32
    toWord [Integer
    0,Integer
    1,Integer
    2,Integer
    3]
                let ws' :: [Word32]
    ws' = [Word32] -> [Word32]
    AES.aesFinalRound [Word32]
    ws
                Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value)
    -> ([Word32] -> Value) -> [Word32] -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> SeqMap Concrete Value -> Value
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    4 (SeqMap Concrete Value -> Value)
    -> ([Word32] -> SeqMap Concrete Value) -> [Word32] -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap Concrete
    Concrete ([Eval Value] -> SeqMap Concrete Value)
    -> ([Word32] -> [Eval Value]) -> [Word32] -> SeqMap Concrete Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Word32 -> Eval Value) -> [Word32] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Word32 -> Eval Value
    fromWord ([Word32] -> Eval Value) -> [Word32] -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ [Word32]
    ws')

      , (Text
    "AESDecRound", {-# SCC "SuiteB::AESDecRound" #-}
          (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun \SEval Concrete Value
    st ->
          SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
             do SeqMap Concrete Value
    ss <- Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq (Value -> SeqMap Concrete Value)
    -> Eval Value -> Eval (SeqMap Concrete Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    st
                let toWord :: Integer -> Eval Word32
                    toWord :: Integer -> Eval Word32
    toWord Integer
    i = Integer -> Word32
    forall a. Num a => Integer -> a
    fromInteger(Integer -> Word32) -> (BV -> Integer) -> BV -> Word32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV -> Integer
    bvVal (BV -> Word32) -> Eval BV -> Eval Word32
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Concrete -> String -> Value -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> String -> GenValue sym -> SEval sym (SWord sym)
    fromVWord Concrete
    Concrete String
    "AESDecRound" (Value -> Eval BV) -> Eval Value -> Eval BV
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SeqMap Concrete Value -> Integer -> SEval Concrete Value
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap Concrete Value
    ss Integer
    i)
                let fromWord :: Word32 -> Eval Value
                    fromWord :: Word32 -> Eval Value
    fromWord = Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> (Word32 -> Value) -> Word32 -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    32 (WordValue Concrete -> Value)
    -> (Word32 -> WordValue Concrete) -> Word32 -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Word32 -> BV) -> Word32 -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    BV Integer
    32 (Integer -> BV) -> (Word32 -> Integer) -> Word32 -> BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word32 -> Integer
    forall a. Integral a => a -> Integer
    toInteger
                [Word32]
    ws <- (Integer -> Eval Word32) -> [Integer] -> Eval [Word32]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Integer -> Eval Word32
    toWord [Integer
    0,Integer
    1,Integer
    2,Integer
    3]
                let ws' :: [Word32]
    ws' = [Word32] -> [Word32]
    AES.aesInvRound [Word32]
    ws
                Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value)
    -> ([Word32] -> Value) -> [Word32] -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> SeqMap Concrete Value -> Value
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    4 (SeqMap Concrete Value -> Value)
    -> ([Word32] -> SeqMap Concrete Value) -> [Word32] -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap Concrete
    Concrete ([Eval Value] -> SeqMap Concrete Value)
    -> ([Word32] -> [Eval Value]) -> [Word32] -> SeqMap Concrete Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Word32 -> Eval Value) -> [Word32] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Word32 -> Eval Value
    fromWord ([Word32] -> Eval Value) -> [Word32] -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ [Word32]
    ws')

      , (Text
    "AESDecFinalRound", {-# SCC "SuiteB::AESDecFinalRound" #-}
         (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
    PFun \SEval Concrete Value
    st ->
         SEval Concrete Value -> Prim Concrete
    forall sym. SEval sym (GenValue sym) -> Prim sym
    PPrim
             do SeqMap Concrete Value
    ss <- Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq (Value -> SeqMap Concrete Value)
    -> Eval Value -> Eval (SeqMap Concrete Value)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    SEval Concrete Value
    st
                let toWord :: Integer -> Eval Word32
                    toWord :: Integer -> Eval Word32
    toWord Integer
    i = Integer -> Word32
    forall a. Num a => Integer -> a
    fromInteger(Integer -> Word32) -> (BV -> Integer) -> BV -> Word32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV -> Integer
    bvVal (BV -> Word32) -> Eval BV -> Eval Word32
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Concrete -> String -> Value -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> String -> GenValue sym -> SEval sym (SWord sym)
    fromVWord Concrete
    Concrete String
    "AESDecFinalRound" (Value -> Eval BV) -> Eval Value -> Eval BV
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SeqMap Concrete Value -> Integer -> SEval Concrete Value
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap Concrete Value
    ss Integer
    i)
                let fromWord :: Word32 -> Eval Value
                    fromWord :: Word32 -> Eval Value
    fromWord = Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value) -> (Word32 -> Value) -> Word32 -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> WordValue Concrete -> Value
    forall sym. Integer -> WordValue sym -> GenValue sym
    VWord Integer
    32 (WordValue Concrete -> Value)
    -> (Word32 -> WordValue Concrete) -> Word32 -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SWord Concrete -> WordValue Concrete
    BV -> WordValue Concrete
    forall sym. SWord sym -> WordValue sym
    wordVal (BV -> WordValue Concrete)
    -> (Word32 -> BV) -> Word32 -> WordValue Concrete
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Integer -> BV
    BV Integer
    32 (Integer -> BV) -> (Word32 -> Integer) -> Word32 -> BV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Word32 -> Integer
    forall a. Integral a => a -> Integer
    toInteger
                [Word32]
    ws <- (Integer -> Eval Word32) -> [Integer] -> Eval [Word32]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM Integer -> Eval Word32
    toWord [Integer
    0,Integer
    1,Integer
    2,Integer
    3]
                let ws' :: [Word32]
    ws' = [Word32] -> [Word32]
    AES.aesInvFinalRound [Word32]
    ws
                Value -> Eval Value
    forall a. a -> Eval a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Value -> Eval Value)
    -> ([Word32] -> Value) -> [Word32] -> Eval Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> SeqMap Concrete Value -> Value
    forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
    VSeq Integer
    4 (SeqMap Concrete Value -> Value)
    -> ([Word32] -> SeqMap Concrete Value) -> [Word32] -> Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
    forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
    finiteSeqMap Concrete
    Concrete ([Eval Value] -> SeqMap Concrete Value)
    -> ([Word32] -> [Eval Value]) -> [Word32] -> SeqMap Concrete Value
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Word32 -> Eval Value) -> [Word32] -> [Eval Value]
    forall a b. (a -> b) -> [a] -> [b]
    map Word32 -> Eval Value
    fromWord ([Word32] -> Eval Value) -> [Word32] -> Eval Value
    forall a b. (a -> b) -> a -> b
    $ [Word32]
    ws')
      ]

    toSHA256Block :: Value -> Eval SHA.SHA256Block
    toSHA256Block :: Value -> Eval SHA256Block
    toSHA256Block Value
    blk =
      do let ws :: SeqMap Concrete Value
    ws = Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq Value
    blk
         let toWord :: Integer -> Eval Word32
    toWord Integer
    i = Integer -> Word32
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Word32) -> (BV -> Integer) -> BV -> Word32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV -> Integer
    bvVal (BV -> Word32) -> Eval BV -> Eval Word32
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Concrete -> String -> Value -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> String -> GenValue sym -> SEval sym (SWord sym)
    fromVWord Concrete
    Concrete String
    "toSHA256Block" (Value -> Eval BV) -> Eval Value -> Eval BV
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SeqMap Concrete Value -> Integer -> SEval Concrete Value
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap Concrete Value
    ws Integer
    i)
         Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> Word32
    -> SHA256Block
    SHA.SHA256Block (Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> Word32
     -> SHA256Block)
    -> Eval Word32
    -> Eval
         (Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> SHA256Block)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
            (Integer -> Eval Word32
    toWord Integer
    0) Eval
      (Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> SHA256Block)
    -> Eval Word32
    -> Eval
         (Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    1) Eval
      (Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> SHA256Block)
    -> Eval Word32
    -> Eval
         (Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    2) Eval
      (Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> SHA256Block)
    -> Eval Word32
    -> Eval
         (Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    3) Eval
      (Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> SHA256Block)
    -> Eval Word32
    -> Eval
         (Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    4) Eval
      (Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> SHA256Block)
    -> Eval Word32
    -> Eval
         (Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    5) Eval
      (Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> SHA256Block)
    -> Eval Word32
    -> Eval
         (Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    6) Eval
      (Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> SHA256Block)
    -> Eval Word32
    -> Eval
         (Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    7) Eval
      (Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> SHA256Block)
    -> Eval Word32
    -> Eval
         (Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> Word32
          -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    8) Eval
      (Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> Word32
       -> SHA256Block)
    -> Eval Word32
    -> Eval
         (Word32
          -> Word32 -> Word32 -> Word32 -> Word32 -> Word32 -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    9) Eval
      (Word32
       -> Word32 -> Word32 -> Word32 -> Word32 -> Word32 -> SHA256Block)
    -> Eval Word32
    -> Eval
         (Word32 -> Word32 -> Word32 -> Word32 -> Word32 -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    10) Eval
      (Word32 -> Word32 -> Word32 -> Word32 -> Word32 -> SHA256Block)
    -> Eval Word32
    -> Eval (Word32 -> Word32 -> Word32 -> Word32 -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    11) Eval (Word32 -> Word32 -> Word32 -> Word32 -> SHA256Block)
    -> Eval Word32 -> Eval (Word32 -> Word32 -> Word32 -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    12) Eval (Word32 -> Word32 -> Word32 -> SHA256Block)
    -> Eval Word32 -> Eval (Word32 -> Word32 -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    13) Eval (Word32 -> Word32 -> SHA256Block)
    -> Eval Word32 -> Eval (Word32 -> SHA256Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    14) Eval (Word32 -> SHA256Block) -> Eval Word32 -> Eval SHA256Block
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word32
    toWord Integer
    15)

    toSHA512Block :: Value -> Eval SHA.SHA512Block
    toSHA512Block :: Value -> Eval SHA512Block
    toSHA512Block Value
    blk =
      do let ws :: SeqMap Concrete Value
    ws = Value -> SeqMap Concrete Value
    forall sym. GenValue sym -> SeqMap sym (GenValue sym)
    fromVSeq Value
    blk
         let toWord :: Integer -> Eval Word64
    toWord Integer
    i = Integer -> Word64
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Word64) -> (BV -> Integer) -> BV -> Word64
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV -> Integer
    bvVal (BV -> Word64) -> Eval BV -> Eval Word64
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Concrete -> String -> Value -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> String -> GenValue sym -> SEval sym (SWord sym)
    fromVWord Concrete
    Concrete String
    "toSHA512Block" (Value -> Eval BV) -> Eval Value -> Eval BV
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SeqMap Concrete Value -> Integer -> SEval Concrete Value
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap Concrete Value
    ws Integer
    i)
         Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> Word64
    -> SHA512Block
    SHA.SHA512Block (Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> Word64
     -> SHA512Block)
    -> Eval Word64
    -> Eval
         (Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> SHA512Block)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
            (Integer -> Eval Word64
    toWord Integer
    0) Eval
      (Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> SHA512Block)
    -> Eval Word64
    -> Eval
         (Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    1) Eval
      (Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> SHA512Block)
    -> Eval Word64
    -> Eval
         (Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    2) Eval
      (Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> SHA512Block)
    -> Eval Word64
    -> Eval
         (Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    3) Eval
      (Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> SHA512Block)
    -> Eval Word64
    -> Eval
         (Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    4) Eval
      (Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> SHA512Block)
    -> Eval Word64
    -> Eval
         (Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    5) Eval
      (Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> SHA512Block)
    -> Eval Word64
    -> Eval
         (Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    6) Eval
      (Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> SHA512Block)
    -> Eval Word64
    -> Eval
         (Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    7) Eval
      (Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> SHA512Block)
    -> Eval Word64
    -> Eval
         (Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> Word64
          -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    8) Eval
      (Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> Word64
       -> SHA512Block)
    -> Eval Word64
    -> Eval
         (Word64
          -> Word64 -> Word64 -> Word64 -> Word64 -> Word64 -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    9) Eval
      (Word64
       -> Word64 -> Word64 -> Word64 -> Word64 -> Word64 -> SHA512Block)
    -> Eval Word64
    -> Eval
         (Word64 -> Word64 -> Word64 -> Word64 -> Word64 -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    10) Eval
      (Word64 -> Word64 -> Word64 -> Word64 -> Word64 -> SHA512Block)
    -> Eval Word64
    -> Eval (Word64 -> Word64 -> Word64 -> Word64 -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    11) Eval (Word64 -> Word64 -> Word64 -> Word64 -> SHA512Block)
    -> Eval Word64 -> Eval (Word64 -> Word64 -> Word64 -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    12) Eval (Word64 -> Word64 -> Word64 -> SHA512Block)
    -> Eval Word64 -> Eval (Word64 -> Word64 -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    13) Eval (Word64 -> Word64 -> SHA512Block)
    -> Eval Word64 -> Eval (Word64 -> SHA512Block)
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    14) Eval (Word64 -> SHA512Block) -> Eval Word64 -> Eval SHA512Block
    forall a b. Eval (a -> b) -> Eval a -> Eval b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*>
            (Integer -> Eval Word64
    toWord Integer
    15)

    -- Sequence Primitives ---------------------------------------------------------

    indexFront_int :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> Integer -> Eval Value
    indexFront_int :: Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> TValue
    -> Integer
    -> Eval Value
    indexFront_int Nat'
    _mblen TValue
    _a SeqMap Concrete Value
    vs TValue
    _ix Integer
    idx = SeqMap Concrete Value -> Integer -> SEval Concrete Value
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap Concrete Value
    vs Integer
    idx

    indexFront_segs :: Nat' -> TValue -> SeqMap Concrete (GenValue Concrete) -> TValue -> Integer -> [IndexSegment Concrete] -> Eval Value
    indexFront_segs :: Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> TValue
    -> Integer
    -> [IndexSegment Concrete]
    -> Eval Value
    indexFront_segs Nat'
    _mblen TValue
    _a SeqMap Concrete Value
    vs TValue
    _ix Integer
    idx_bits [IndexSegment Concrete]
    segs = SeqMap Concrete Value -> Integer -> SEval Concrete Value
    forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
    lookupSeqMap SeqMap Concrete Value
    vs (Integer -> Eval Value) -> Integer -> Eval Value
    forall a b. (a -> b) -> a -> b
    $! Integer -> [IndexSegment Concrete] -> Integer
    packSegments Integer
    idx_bits [IndexSegment Concrete]
    segs

    packSegments :: Integer -> [IndexSegment Concrete] -> Integer
    packSegments :: Integer -> [IndexSegment Concrete] -> Integer
    packSegments = Integer -> Integer -> [IndexSegment Concrete] -> Integer
    forall {sym}.
    (SWord sym ~ BV, SBit sym ~ Bool) =>
    Integer -> Integer -> [IndexSegment sym] -> Integer
    loop Integer
    0
      where
      loop :: Integer -> Integer -> [IndexSegment sym] -> Integer
    loop !Integer
    val !Integer
    n [IndexSegment sym]
    segs =
        case [IndexSegment sym]
    segs of
          [] -> Integer
    val
          [WordIndexSegment (BV Integer
    _ Integer
    x)] -> Integer
    val Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    x
          WordIndexSegment (BV Integer
    xlen Integer
    x) : [IndexSegment sym]
    bs ->
            let n' :: Integer
    n' = Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    xlen
             in Integer -> Integer -> [IndexSegment sym] -> Integer
    loop (Integer
    val Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + (Integer
    xInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    *Integer
    2Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    n')) Integer
    n' [IndexSegment sym]
    bs
          BitIndexSegment Bool
    SBit sym
    True : [IndexSegment sym]
    bs ->
            let n' :: Integer
    n' = Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1
             in Integer -> Integer -> [IndexSegment sym] -> Integer
    loop (Integer
    val Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    2Integer -> Integer -> Integer
    forall a b. (Num a, Integral b) => a -> b -> a
    ^Integer
    n') Integer
    n' [IndexSegment sym]
    bs
          BitIndexSegment Bool
    SBit sym
    False : [IndexSegment sym]
    bs ->
            let n' :: Integer
    n' = Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1
             in Integer -> Integer -> [IndexSegment sym] -> Integer
    loop Integer
    val Integer
    n' [IndexSegment sym]
    bs

    updateFront ::
      Nat'               {- ^ length of the sequence -} ->
      TValue             {- ^ type of values in the sequence -} ->
      SeqMap Concrete (GenValue Concrete) {- ^ sequence to update -} ->
      Either Integer (WordValue Concrete) {- ^ index -} ->
      Eval Value         {- ^ new value at index -} ->
      Eval (SeqMap Concrete (GenValue Concrete))
    updateFront :: Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> Either Integer (WordValue Concrete)
    -> Eval Value
    -> Eval (SeqMap Concrete Value)
    updateFront Nat'
    _len TValue
    _eltTy SeqMap Concrete Value
    vs (Left Integer
    idx) Eval Value
    val = do
      SeqMap Concrete Value -> Eval (SeqMap Concrete Value)
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap Concrete Value -> Eval (SeqMap Concrete Value))
    -> SeqMap Concrete Value -> Eval (SeqMap Concrete Value)
    forall a b. (a -> b) -> a -> b
    $ SeqMap Concrete Value
    -> Integer -> SEval Concrete Value -> SeqMap Concrete Value
    forall sym a.
    SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
    updateSeqMap SeqMap Concrete Value
    vs Integer
    idx Eval Value
    SEval Concrete Value
    val

    updateFront Nat'
    _len TValue
    _eltTy SeqMap Concrete Value
    vs (Right WordValue Concrete
    w) Eval Value
    val = do
      Integer
    idx <- BV -> Integer
    bvVal (BV -> Integer) -> Eval BV -> Eval Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Concrete -> WordValue Concrete -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> SEval sym (SWord sym)
    asWordVal Concrete
    Concrete WordValue Concrete
    w
      SeqMap Concrete Value -> Eval (SeqMap Concrete Value)
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap Concrete Value -> Eval (SeqMap Concrete Value))
    -> SeqMap Concrete Value -> Eval (SeqMap Concrete Value)
    forall a b. (a -> b) -> a -> b
    $ SeqMap Concrete Value
    -> Integer -> SEval Concrete Value -> SeqMap Concrete Value
    forall sym a.
    SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
    updateSeqMap SeqMap Concrete Value
    vs Integer
    idx Eval Value
    SEval Concrete Value
    val

    updateFront_word ::
      Nat'               {- ^ length of the sequence -} ->
      TValue             {- ^ type of values in the sequence -} ->
      WordValue Concrete {- ^ bit sequence to update -} ->
      Either Integer (WordValue Concrete) {- ^ index -} ->
      Eval Value         {- ^ new value at index -} ->
      Eval (WordValue Concrete)
    updateFront_word :: Nat'
    -> TValue
    -> WordValue Concrete
    -> Either Integer (WordValue Concrete)
    -> Eval Value
    -> Eval (WordValue Concrete)
    updateFront_word Nat'
    _len TValue
    _eltTy WordValue Concrete
    bs (Left Integer
    idx) Eval Value
    val = do
      Concrete
    -> WordValue Concrete
    -> Integer
    -> SEval Concrete (SBit Concrete)
    -> SEval Concrete (WordValue Concrete)
    forall sym.
    Backend sym =>
    sym
    -> WordValue sym
    -> Integer
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    updateWordValue Concrete
    Concrete WordValue Concrete
    bs Integer
    idx (Value -> Bool
    Value -> SBit Concrete
    forall sym. GenValue sym -> SBit sym
    fromVBit (Value -> Bool) -> Eval Value -> Eval Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    val)

    updateFront_word Nat'
    _len TValue
    _eltTy WordValue Concrete
    bs (Right WordValue Concrete
    w) Eval Value
    val = do
      Integer
    idx <- BV -> Integer
    bvVal (BV -> Integer) -> Eval BV -> Eval Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Concrete -> WordValue Concrete -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> SEval sym (SWord sym)
    asWordVal Concrete
    Concrete WordValue Concrete
    w
      Concrete
    -> WordValue Concrete
    -> Integer
    -> SEval Concrete (SBit Concrete)
    -> SEval Concrete (WordValue Concrete)
    forall sym.
    Backend sym =>
    sym
    -> WordValue sym
    -> Integer
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    updateWordValue Concrete
    Concrete WordValue Concrete
    bs Integer
    idx (Value -> Bool
    Value -> SBit Concrete
    forall sym. GenValue sym -> SBit sym
    fromVBit (Value -> Bool) -> Eval Value -> Eval Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    val)

    updateBack ::
      Nat'               {- ^ length of the sequence -} ->
      TValue             {- ^ type of values in the sequence -} ->
      SeqMap Concrete (GenValue Concrete) {- ^ sequence to update -} ->
      Either Integer (WordValue Concrete) {- ^ index -} ->
      Eval Value         {- ^ new value at index -} ->
      Eval (SeqMap Concrete (GenValue Concrete))
    updateBack :: Nat'
    -> TValue
    -> SeqMap Concrete Value
    -> Either Integer (WordValue Concrete)
    -> Eval Value
    -> Eval (SeqMap Concrete Value)
    updateBack Nat'
    Inf TValue
    _eltTy SeqMap Concrete Value
    _vs Either Integer (WordValue Concrete)
    _w Eval Value
    _val =
      String -> [String] -> Eval (SeqMap Concrete Value)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "Unexpected infinite sequence in updateEnd" []
    updateBack (Nat Integer
    n) TValue
    _eltTy SeqMap Concrete Value
    vs (Left Integer
    idx) Eval Value
    val = do
      SeqMap Concrete Value -> Eval (SeqMap Concrete Value)
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap Concrete Value -> Eval (SeqMap Concrete Value))
    -> SeqMap Concrete Value -> Eval (SeqMap Concrete Value)
    forall a b. (a -> b) -> a -> b
    $ SeqMap Concrete Value
    -> Integer -> SEval Concrete Value -> SeqMap Concrete Value
    forall sym a.
    SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
    updateSeqMap SeqMap Concrete Value
    vs (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    idx Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) Eval Value
    SEval Concrete Value
    val
    updateBack (Nat Integer
    n) TValue
    _eltTy SeqMap Concrete Value
    vs (Right WordValue Concrete
    w) Eval Value
    val = do
      Integer
    idx <- BV -> Integer
    bvVal (BV -> Integer) -> Eval BV -> Eval Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Concrete -> WordValue Concrete -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> SEval sym (SWord sym)
    asWordVal Concrete
    Concrete WordValue Concrete
    w
      SeqMap Concrete Value -> Eval (SeqMap Concrete Value)
    forall a. a -> Eval a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SeqMap Concrete Value -> Eval (SeqMap Concrete Value))
    -> SeqMap Concrete Value -> Eval (SeqMap Concrete Value)
    forall a b. (a -> b) -> a -> b
    $ SeqMap Concrete Value
    -> Integer -> SEval Concrete Value -> SeqMap Concrete Value
    forall sym a.
    SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
    updateSeqMap SeqMap Concrete Value
    vs (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    idx Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) Eval Value
    SEval Concrete Value
    val

    updateBack_word ::
      Nat'               {- ^ length of the sequence -} ->
      TValue             {- ^ type of values in the sequence -} ->
      WordValue Concrete {- ^ bit sequence to update -} ->
      Either Integer (WordValue Concrete) {- ^ index -} ->
      Eval Value         {- ^ new value at index -} ->
      Eval (WordValue Concrete)
    updateBack_word :: Nat'
    -> TValue
    -> WordValue Concrete
    -> Either Integer (WordValue Concrete)
    -> Eval Value
    -> Eval (WordValue Concrete)
    updateBack_word Nat'
    Inf TValue
    _eltTy WordValue Concrete
    _bs Either Integer (WordValue Concrete)
    _w Eval Value
    _val =
      String -> [String] -> Eval (WordValue Concrete)
    forall a. HasCallStack => String -> [String] -> a
    evalPanic String
    "Unexpected infinite sequence in updateEnd" []
    updateBack_word (Nat Integer
    n) TValue
    _eltTy WordValue Concrete
    bs (Left Integer
    idx) Eval Value
    val = do
      Concrete
    -> WordValue Concrete
    -> Integer
    -> SEval Concrete (SBit Concrete)
    -> SEval Concrete (WordValue Concrete)
    forall sym.
    Backend sym =>
    sym
    -> WordValue sym
    -> Integer
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    updateWordValue Concrete
    Concrete WordValue Concrete
    bs (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    idx Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) (Value -> Bool
    Value -> SBit Concrete
    forall sym. GenValue sym -> SBit sym
    fromVBit (Value -> Bool) -> Eval Value -> Eval Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    val)
    updateBack_word (Nat Integer
    n) TValue
    _eltTy WordValue Concrete
    bs (Right WordValue Concrete
    w) Eval Value
    val = do
      Integer
    idx <- BV -> Integer
    bvVal (BV -> Integer) -> Eval BV -> Eval Integer
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Concrete -> WordValue Concrete -> SEval Concrete (SWord Concrete)
    forall sym.
    Backend sym =>
    sym -> WordValue sym -> SEval sym (SWord sym)
    asWordVal Concrete
    Concrete WordValue Concrete
    w
      Concrete
    -> WordValue Concrete
    -> Integer
    -> SEval Concrete (SBit Concrete)
    -> SEval Concrete (WordValue Concrete)
    forall sym.
    Backend sym =>
    sym
    -> WordValue sym
    -> Integer
    -> SEval sym (SBit sym)
    -> SEval sym (WordValue sym)
    updateWordValue Concrete
    Concrete WordValue Concrete
    bs (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    idx Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1) (Value -> Bool
    Value -> SBit Concrete
    forall sym. GenValue sym -> SBit sym
    fromVBit (Value -> Bool) -> Eval Value -> Eval Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Eval Value
    val)