-- |
-- 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 LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
module Cryptol.Eval.Concrete
  ( module Cryptol.Backend.Concrete
  , Value
  , primTable
  , toExpr
  ) where

import Control.Monad (join, guard, zipWithM, foldM)
import Data.Bits (Bits(..))
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.Eval.Generic hiding (logicShift)
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.Logger(logPrint)
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 -> AST.Type -> Value -> Eval (Maybe AST.Expr)
toExpr :: PrimMap -> Type -> Value -> Eval (Maybe Expr)
toExpr PrimMap
prims Type
t0 Value
v0 = ChoiceT Eval Expr -> Eval (Maybe Expr)
forall (m :: * -> *) a. Monad m => ChoiceT m a -> m (Maybe a)
findOne (Type -> Value -> ChoiceT Eval Expr
go Type
t0 Value
v0)
  where

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


  go :: AST.Type -> Value -> ChoiceT Eval Expr
  go :: Type -> Value -> ChoiceT Eval Expr
go Type
ty Value
val =
    case Value
val of
      VRecord RecordMap Ident (SEval Concrete Value)
vfs ->
        do RecordMap Ident Type
tfs <- ChoiceT Eval (RecordMap Ident Type)
-> (RecordMap Ident Type -> ChoiceT Eval (RecordMap Ident Type))
-> Maybe (RecordMap Ident Type)
-> ChoiceT Eval (RecordMap Ident Type)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ChoiceT Eval (RecordMap Ident Type)
forall a. ChoiceT Eval a
mismatch RecordMap Ident Type -> ChoiceT Eval (RecordMap Ident Type)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Maybe (RecordMap Ident Type)
tIsRec Type
ty)
           -- NB, vfs first argument to keep their display order
           Either (Either Ident Ident) (RecordMap Ident Expr)
res <- (Ident -> Eval Value -> Type -> ChoiceT Eval Expr)
-> RecordMap Ident (Eval Value)
-> RecordMap Ident Type
-> 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 Type
t -> Type -> Value -> ChoiceT Eval Expr
go Type
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 (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 Type
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 (f :: * -> *) a. Applicative f => a -> f a
pure (RecordMap Ident Expr -> Expr
ERec RecordMap Ident Expr
efs)
      VTuple [SEval Concrete Value]
tvs ->
        do [Type]
ts <- ChoiceT Eval [Type]
-> ([Type] -> ChoiceT Eval [Type])
-> Maybe [Type]
-> ChoiceT Eval [Type]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ChoiceT Eval [Type]
forall a. ChoiceT Eval a
mismatch [Type] -> ChoiceT Eval [Type]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Maybe [Type]
tIsTuple Type
ty)
           Bool -> ChoiceT Eval ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Eval Value] -> 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
<$> ((Type -> Value -> ChoiceT Eval Expr)
-> [Type] -> [Value] -> ChoiceT Eval [Expr]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Type -> Value -> ChoiceT Eval Expr
go [Type]
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 (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)
sequence [Eval Value]
[SEval Concrete Value]
tvs))
      VBit SBit Concrete
b ->
        Expr -> ChoiceT Eval Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Expr
prim (if Bool
SBit Concrete
b then Text
"True" else Text
"False"))
      VInteger SInteger Concrete
i ->
        -- This works uniformly for values of type Integer or Z n
        Expr -> ChoiceT Eval Expr
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
ty
      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 (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'
      VFloat SFloat Concrete
i ->
        do (Type
eT, Type
pT) <- ChoiceT Eval (Type, Type)
-> ((Type, Type) -> ChoiceT Eval (Type, Type))
-> Maybe (Type, Type)
-> ChoiceT Eval (Type, Type)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ChoiceT Eval (Type, Type)
forall a. ChoiceT Eval a
mismatch (Type, Type) -> ChoiceT Eval (Type, Type)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Maybe (Type, Type)
tIsFloat Type
ty)
           Expr -> ChoiceT Eval Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PrimMap -> Type -> Type -> BigFloat -> Expr
floatToExpr PrimMap
prims Type
eT Type
pT (BF -> BigFloat
bfValue BF
SFloat Concrete
i))
      VSeq Integer
n SeqMap Concrete
svs ->
        do (Type
_a, Type
b) <- ChoiceT Eval (Type, Type)
-> ((Type, Type) -> ChoiceT Eval (Type, Type))
-> Maybe (Type, Type)
-> ChoiceT Eval (Type, Type)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ChoiceT Eval (Type, Type)
forall a. ChoiceT Eval a
mismatch (Type, Type) -> ChoiceT Eval (Type, Type)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Maybe (Type, Type)
tIsSeq Type
ty)
           [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)
traverse (Type -> Value -> ChoiceT Eval Expr
go Type
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 (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)
sequence (Integer -> SeqMap Concrete -> [SEval Concrete Value]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n SeqMap Concrete
svs))
           Expr -> ChoiceT Eval Expr
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 Type
b
      VWord Integer
_ SEval Concrete (WordValue Concrete)
wval ->
        do BV Integer
_ Integer
v <- Eval BV -> ChoiceT Eval BV
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 -> Eval BV)
-> Eval (WordValue Concrete) -> Eval BV
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (WordValue Concrete)
SEval Concrete (WordValue Concrete)
wval)
           Expr -> ChoiceT Eval Expr
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
ty
      VStream SeqMap Concrete
_  -> String -> ChoiceT Eval Expr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"cannot construct infinite expressions"
      VFun SEval Concrete Value -> SEval Concrete Value
_     -> String -> ChoiceT Eval Expr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"cannot convert function values to expressions"
      VPoly TValue -> SEval Concrete Value
_    -> String -> ChoiceT Eval Expr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"cannot convert polymorphic values to expressions"
      VNumPoly Nat' -> SEval Concrete Value
_ -> String -> ChoiceT Eval Expr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"cannot convert polymorphic values to expressions"
    where
      mismatch :: forall a. ChoiceT Eval a
      mismatch :: ChoiceT Eval a
mismatch =
        do Doc
doc <- Eval Doc -> ChoiceT Eval Doc
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 Type
ty
             , Doc -> String
render 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 :: EvalOpts -> Map PrimIdent Value
primTable :: EvalOpts -> Map PrimIdent Value
primTable EvalOpts
eOpts = let sym :: Concrete
sym = Concrete
Concrete in
  Map PrimIdent Value -> Map PrimIdent Value -> Map PrimIdent Value
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Concrete -> Map PrimIdent Value
floatPrims Concrete
sym) (Map PrimIdent Value -> Map PrimIdent Value)
-> Map PrimIdent Value -> Map PrimIdent Value
forall a b. (a -> b) -> a -> b
$
  Map PrimIdent Value -> Map PrimIdent Value -> Map PrimIdent Value
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map PrimIdent Value
suiteBPrims (Map PrimIdent Value -> Map PrimIdent Value)
-> Map PrimIdent Value -> Map PrimIdent Value
forall a b. (a -> b) -> a -> b
$
  Map PrimIdent Value -> Map PrimIdent Value -> Map PrimIdent Value
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map PrimIdent Value
primeECPrims (Map PrimIdent Value -> Map PrimIdent Value)
-> Map PrimIdent Value -> Map PrimIdent Value
forall a b. (a -> b) -> a -> b
$

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

  [ -- Literals
    (Text
"True"       , SBit Concrete -> Value
forall sym. SBit sym -> GenValue sym
VBit (Concrete -> Bool -> SBit Concrete
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit Concrete
sym Bool
True))
  , (Text
"False"      , SBit Concrete -> Value
forall sym. SBit sym -> GenValue sym
VBit (Concrete -> Bool -> SBit Concrete
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit Concrete
sym Bool
False))
  , (Text
"number"     , {-# SCC "Prelude::number" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
ecNumberV Concrete
sym)
  , (Text
"ratio"      , {-# SCC "Prelude::ratio" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
ratioV Concrete
sym)
  , (Text
"fraction"   , Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
ecFractionV Concrete
sym)


    -- Zero
  , (Text
"zero"       , {-# SCC "Prelude::zero" #-}
                    (TValue -> SEval Concrete Value) -> Value
forall sym. (TValue -> SEval sym (GenValue sym)) -> GenValue sym
VPoly (Concrete -> TValue -> SEval Concrete Value
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV Concrete
sym))

    -- Logic
  , (Text
"&&"         , {-# SCC "Prelude::(&&)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
andV Concrete
sym))
  , (Text
"||"         , {-# SCC "Prelude::(||)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
orV Concrete
sym))
  , (Text
"^"          , {-# SCC "Prelude::(^)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
xorV Concrete
sym))
  , (Text
"complement" , {-# SCC "Prelude::complement" #-}
                    Unary Concrete -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary  (Concrete -> Unary Concrete
forall sym. Backend sym => sym -> Unary sym
complementV Concrete
sym))

    -- Ring
  , (Text
"fromInteger", {-# SCC "Prelude::fromInteger" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
fromIntegerV Concrete
sym)
  , (Text
"+"          , {-# SCC "Prelude::(+)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
addV Concrete
sym))
  , (Text
"-"          , {-# SCC "Prelude::(-)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
subV Concrete
sym))
  , (Text
"*"          , {-# SCC "Prelude::(*)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
mulV Concrete
sym))
  , (Text
"negate"     , {-# SCC "Prelude::negate" #-}
                    Unary Concrete -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (Concrete -> Unary Concrete
forall sym. Backend sym => sym -> Unary sym
negateV Concrete
sym))

    -- Integral
  , (Text
"toInteger"  , {-# SCC "Prelude::toInteger" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
toIntegerV Concrete
sym)
  , (Text
"/"          , {-# SCC "Prelude::(/)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
divV Concrete
sym))
  , (Text
"%"          , {-# SCC "Prelude::(%)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
modV Concrete
sym))
  , (Text
"^^"         , {-# SCC "Prelude::(^^)" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
expV Concrete
sym)
  , (Text
"infFrom"    , {-# SCC "Prelude::infFrom" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
infFromV Concrete
sym)
  , (Text
"infFromThen", {-# SCC "Prelude::infFromThen" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
infFromThenV Concrete
sym)

    -- Field
  , (Text
"recip"      , {-# SCC "Prelude::recip" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
recipV Concrete
sym)
  , (Text
"/."         , {-# SCC "Prelude::(/.)" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
fieldDivideV Concrete
sym)

    -- Round
  , (Text
"floor"      , {-# SCC "Prelude::floor" #-}
                    Unary Concrete -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (Concrete -> Unary Concrete
forall sym. Backend sym => sym -> Unary sym
floorV Concrete
sym))
  , (Text
"ceiling"    , {-# SCC "Prelude::ceiling" #-}
                    Unary Concrete -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (Concrete -> Unary Concrete
forall sym. Backend sym => sym -> Unary sym
ceilingV Concrete
sym))
  , (Text
"trunc"      , {-# SCC "Prelude::trunc" #-}
                    Unary Concrete -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (Concrete -> Unary Concrete
forall sym. Backend sym => sym -> Unary sym
truncV Concrete
sym))
  , (Text
"roundAway"  , {-# SCC "Prelude::roundAway" #-}
                    Unary Concrete -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (Concrete -> Unary Concrete
forall sym. Backend sym => sym -> Unary sym
roundAwayV Concrete
sym))
  , (Text
"roundToEven", {-# SCC "Prelude::roundToEven" #-}
                    Unary Concrete -> Value
forall sym. Backend sym => Unary sym -> GenValue sym
unary (Concrete -> Unary Concrete
forall sym. Backend sym => sym -> Unary sym
roundToEvenV Concrete
sym))

    -- Bitvector specific operations
  , (Text
"/$"         , {-# SCC "Prelude::(/$)" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
sdivV Concrete
sym)
  , (Text
"%$"         , {-# SCC "Prelude::(%$)" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
smodV Concrete
sym)
  , (Text
"lg2"        , {-# SCC "Prelude::lg2" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
lg2V Concrete
sym)
  , (Text
">>$"        , {-# SCC "Prelude::(>>$)" #-}
                    Value
sshrV)

    -- Cmp
  , (Text
"<"          , {-# SCC "Prelude::(<)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
lessThanV Concrete
sym))
  , (Text
">"          , {-# SCC "Prelude::(>)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
greaterThanV Concrete
sym))
  , (Text
"<="         , {-# SCC "Prelude::(<=)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
lessThanEqV Concrete
sym))
  , (Text
">="         , {-# SCC "Prelude::(>=)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
greaterThanEqV Concrete
sym))
  , (Text
"=="         , {-# SCC "Prelude::(==)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
eqV Concrete
sym))
  , (Text
"!="         , {-# SCC "Prelude::(!=)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
distinctV Concrete
sym))

    -- SignedCmp
  , (Text
"<$"         , {-# SCC "Prelude::(<$)" #-}
                    Binary Concrete -> Value
forall sym. Backend sym => Binary sym -> GenValue sym
binary (Concrete -> Binary Concrete
forall sym. Backend sym => sym -> Binary sym
signedLessThanV Concrete
sym))

    -- Finite enumerations
  , (Text
"fromTo"     , {-# SCC "Prelude::fromTo" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
fromToV Concrete
sym)
  , (Text
"fromThenTo" , {-# SCC "Prelude::fromThenTo" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
fromThenToV Concrete
sym)

    -- Sequence manipulations
  , (Text
"#"          , {-# SCC "Prelude::(#)" #-}
                    (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ Nat'
front ->
                    (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ Nat'
back  ->
                    (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ TValue
elty  ->
                    (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ SEval Concrete Value
l     -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
                    (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ SEval Concrete Value
r     -> Eval (Eval Value) -> Eval Value
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (Concrete -> Nat' -> Nat' -> Binary Concrete
forall sym.
Backend sym =>
sym
-> Nat'
-> Nat'
-> TValue
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
ccatV Concrete
sym Nat'
front Nat'
back TValue
elty (Value -> Value -> Eval Value)
-> Eval Value -> Eval (Value -> Eval Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval Value
SEval Concrete Value
l Eval (Value -> Eval Value) -> Eval Value -> Eval (Eval Value)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Eval Value
SEval Concrete Value
r))


  , (Text
"join"       , {-# SCC "Prelude::join" #-}
                    (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ Nat'
parts ->
                    (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ (Nat' -> Integer
finNat' -> Integer
each)  ->
                    (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ TValue
a     ->
                    (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ SEval Concrete Value
x     ->
                      Concrete -> Nat' -> Integer -> Unary Concrete
forall sym.
Backend sym =>
sym
-> Nat'
-> Integer
-> TValue
-> GenValue sym
-> SEval sym (GenValue sym)
joinV Concrete
sym Nat'
parts Integer
each TValue
a (Value -> Eval Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value
SEval Concrete Value
x)

  , (Text
"split"      , {-# SCC "Prelude::split" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
ecSplitV Concrete
sym)

  , (Text
"splitAt"    , {-# SCC "Prelude::splitAt" #-}
                    (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ Nat'
front ->
                    (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ Nat'
back  ->
                    (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ TValue
a     ->
                    (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ SEval Concrete Value
x     ->
                       Concrete -> Nat' -> Nat' -> Unary Concrete
forall sym.
Backend sym =>
sym
-> Nat'
-> Nat'
-> TValue
-> GenValue sym
-> SEval sym (GenValue sym)
splitAtV Concrete
sym Nat'
front Nat'
back TValue
a (Value -> Eval Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value
SEval Concrete Value
x)

  , (Text
"reverse"    , {-# SCC "Prelude::reverse" #-}
                    (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
_a ->
                    (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
_b ->
                     (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
xs -> Concrete -> Value -> SEval Concrete Value
forall sym.
Backend sym =>
sym -> GenValue sym -> SEval sym (GenValue sym)
reverseV Concrete
sym (Value -> Eval Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value
SEval Concrete Value
xs)

  , (Text
"transpose"  , {-# SCC "Prelude::transpose" #-}
                    (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
a ->
                    (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
b ->
                    (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
c ->
                     (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
xs -> Concrete -> Nat' -> Nat' -> Unary Concrete
forall sym.
Backend sym =>
sym
-> Nat'
-> Nat'
-> TValue
-> GenValue sym
-> SEval sym (GenValue sym)
transposeV Concrete
sym Nat'
a Nat'
b TValue
c (Value -> Eval Value) -> Eval Value -> Eval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value
SEval Concrete Value
xs)

    -- Shifts and rotates
  , (Text
"<<"         , {-# SCC "Prelude::(<<)" #-}
                    (Integer -> Integer -> Integer -> Integer)
-> (Nat'
    -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)
-> Value
logicShift Integer -> Integer -> Integer -> Integer
shiftLW Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
shiftLS)
  , (Text
">>"         , {-# SCC "Prelude::(>>)" #-}
                    (Integer -> Integer -> Integer -> Integer)
-> (Nat'
    -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)
-> Value
logicShift Integer -> Integer -> Integer -> Integer
shiftRW Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
shiftRS)
  , (Text
"<<<"        , {-# SCC "Prelude::(<<<)" #-}
                    (Integer -> Integer -> Integer -> Integer)
-> (Nat'
    -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)
-> Value
logicShift Integer -> Integer -> Integer -> Integer
rotateLW Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
rotateLS)
  , (Text
">>>"        , {-# SCC "Prelude::(>>>)" #-}
                    (Integer -> Integer -> Integer -> Integer)
-> (Nat'
    -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)
-> Value
logicShift Integer -> Integer -> Integer -> Integer
rotateRW Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
rotateRS)

    -- Indexing and updates
  , (Text
"@"          , {-# SCC "Prelude::(@)" #-}
                    Concrete
-> (Nat'
    -> TValue
    -> SeqMap Concrete
    -> TValue
    -> SInteger Concrete
    -> SEval Concrete Value)
-> (Nat'
    -> TValue
    -> SeqMap Concrete
    -> TValue
    -> [SBit Concrete]
    -> SEval Concrete Value)
-> (Nat'
    -> TValue
    -> SeqMap Concrete
    -> TValue
    -> SWord Concrete
    -> SEval Concrete Value)
-> Value
forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SInteger sym
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> [SBit sym]
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SWord sym
    -> SEval sym (GenValue sym))
-> GenValue sym
indexPrim Concrete
sym Nat'
-> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value
Nat'
-> TValue
-> SeqMap Concrete
-> TValue
-> SInteger Concrete
-> SEval Concrete Value
indexFront_int Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value
Nat'
-> TValue
-> SeqMap Concrete
-> TValue
-> [SBit Concrete]
-> SEval Concrete Value
indexFront_bits Nat'
-> TValue
-> SeqMap Concrete
-> TValue
-> SWord Concrete
-> SEval Concrete Value
Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
indexFront)
  , (Text
"!"          , {-# SCC "Prelude::(!)" #-}
                    Concrete
-> (Nat'
    -> TValue
    -> SeqMap Concrete
    -> TValue
    -> SInteger Concrete
    -> SEval Concrete Value)
-> (Nat'
    -> TValue
    -> SeqMap Concrete
    -> TValue
    -> [SBit Concrete]
    -> SEval Concrete Value)
-> (Nat'
    -> TValue
    -> SeqMap Concrete
    -> TValue
    -> SWord Concrete
    -> SEval Concrete Value)
-> Value
forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SInteger sym
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> [SBit sym]
    -> SEval sym (GenValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> TValue
    -> SWord sym
    -> SEval sym (GenValue sym))
-> GenValue sym
indexPrim Concrete
sym Nat'
-> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value
Nat'
-> TValue
-> SeqMap Concrete
-> TValue
-> SInteger Concrete
-> SEval Concrete Value
indexBack_int Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value
Nat'
-> TValue
-> SeqMap Concrete
-> TValue
-> [SBit Concrete]
-> SEval Concrete Value
indexBack_bits Nat'
-> TValue
-> SeqMap Concrete
-> TValue
-> SWord Concrete
-> SEval Concrete Value
Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
indexBack)

  , (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
    -> Either (SInteger Concrete) (WordValue Concrete)
    -> SEval Concrete Value
    -> SEval Concrete (SeqMap Concrete))
-> Value
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
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (SeqMap sym))
-> GenValue 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
-> Either Integer (WordValue Concrete)
-> Eval Value
-> Eval (SeqMap Concrete)
Nat'
-> TValue
-> SeqMap Concrete
-> Either (SInteger Concrete) (WordValue Concrete)
-> SEval Concrete Value
-> SEval Concrete (SeqMap Concrete)
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
    -> Either (SInteger Concrete) (WordValue Concrete)
    -> SEval Concrete Value
    -> SEval Concrete (SeqMap Concrete))
-> Value
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
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (SeqMap sym))
-> GenValue 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
-> Either Integer (WordValue Concrete)
-> Eval Value
-> Eval (SeqMap Concrete)
Nat'
-> TValue
-> SeqMap Concrete
-> Either (SInteger Concrete) (WordValue Concrete)
-> SEval Concrete Value
-> SEval Concrete (SeqMap Concrete)
updateBack)

    -- Misc
  , (Text
"foldl"      , {-# SCC "Prelude::foldl" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
foldlV Concrete
sym)

  , (Text
"foldl'"     , {-# SCC "Prelude::foldl'" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
foldl'V Concrete
sym)

  , (Text
"deepseq"    , {-# SCC "Prelude::deepseq" #-}
                    (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
_a ->
                    (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
_b ->
                     (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
x -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
                     (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
y ->
                       do ()
_ <- Value -> Eval ()
forall sym. Backend sym => GenValue sym -> SEval sym ()
forceValue (Value -> Eval ()) -> Eval Value -> Eval ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value
SEval Concrete Value
x
                          Eval Value
SEval Concrete Value
y)

  , (Text
"parmap"     , {-# SCC "Prelude::parmap" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
parmapV Concrete
sym)

  , (Text
"fromZ"      , {-# SCC "Prelude::fromZ" #-}
                    Concrete -> Value
forall sym. Backend sym => sym -> GenValue sym
fromZV Concrete
sym)

  , (Text
"error"      , {-# SCC "Prelude::error" #-}
                      (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
a ->
                      (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
_ ->
                       (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
s -> Concrete -> TValue -> String -> SEval Concrete Value
forall sym.
Backend sym =>
sym -> TValue -> String -> SEval sym (GenValue sym)
errorV Concrete
sym TValue
a (String -> Eval Value) -> Eval String -> Eval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Concrete -> Value -> SEval Concrete String
forall sym. Backend sym => sym -> GenValue sym -> SEval sym String
valueToString Concrete
sym (Value -> Eval String) -> Eval Value -> Eval String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value
SEval Concrete Value
s))

  , (Text
"random"      , {-# SCC "Prelude::random" #-}
                     (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
a ->
                     Concrete -> (SWord Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam Concrete
sym ((SWord Concrete -> SEval Concrete Value) -> Value)
-> (SWord Concrete -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \(SWord Concrete -> Integer
BV -> Integer
bvVal -> Integer
x) -> Concrete -> TValue -> Integer -> SEval Concrete Value
forall sym.
Backend sym =>
sym -> TValue -> Integer -> SEval sym (GenValue sym)
randomV Concrete
sym TValue
a Integer
x)

  , (Text
"trace"       , {-# SCC "Prelude::trace" #-}
                     (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
_n ->
                     (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
_a ->
                     (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
_b ->
                      (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
s -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
                      (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
x -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
                      (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
y -> do
                         String
msg <- Concrete -> Value -> SEval Concrete String
forall sym. Backend sym => sym -> GenValue sym -> SEval sym String
valueToString Concrete
sym (Value -> Eval String) -> Eval Value -> Eval String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value
SEval Concrete Value
s
                         let EvalOpts { PPOpts
evalPPOpts :: EvalOpts -> PPOpts
evalPPOpts :: PPOpts
evalPPOpts, Logger
evalLogger :: EvalOpts -> Logger
evalLogger :: Logger
evalLogger } = EvalOpts
eOpts
                         Doc
doc <- Concrete -> PPOpts -> Value -> SEval Concrete Doc
forall sym.
Backend sym =>
sym -> PPOpts -> GenValue sym -> SEval sym Doc
ppValue Concrete
sym PPOpts
evalPPOpts (Value -> Eval Doc) -> Eval Value -> Eval Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value
SEval Concrete Value
x
                         Value
yv <- Eval Value
SEval Concrete Value
y
                         IO () -> Eval ()
forall a. IO a -> Eval a
io (IO () -> Eval ()) -> IO () -> Eval ()
forall a b. (a -> b) -> a -> b
$ Logger -> Doc -> IO ()
forall a. Show a => Logger -> a -> IO ()
logPrint Logger
evalLogger
                             (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
msg then Doc
doc else String -> Doc
text String
msg Doc -> Doc -> Doc
<+> Doc
doc
                         Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
yv)

   , (Text
"pmult",
        (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
u ->
        (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
v ->
          Concrete -> (SWord Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam Concrete
Concrete ((SWord Concrete -> SEval Concrete Value) -> Value)
-> (SWord Concrete -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \(BV _ x) -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
          Concrete -> (SWord Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam Concrete
Concrete ((SWord Concrete -> SEval Concrete Value) -> Value)
-> (SWord Concrete -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \(BV _ y) ->
            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 (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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (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) (Eval (WordValue Concrete) -> Value)
-> (Integer -> Eval (WordValue Concrete)) -> Integer -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Integer -> WordValue Concrete)
-> Integer
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
_u ->
        (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
v ->
        Concrete -> (SWord Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam Concrete
Concrete ((SWord Concrete -> SEval Concrete Value) -> Value)
-> (SWord Concrete -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \(BV w x) -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
        Concrete -> (SWord Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam Concrete
Concrete ((SWord Concrete -> SEval Concrete Value) -> Value)
-> (SWord Concrete -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \(BV _ m) ->
          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 (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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
v (Eval (WordValue Concrete) -> Value)
-> (Integer -> Eval (WordValue Concrete)) -> Integer -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Integer -> WordValue Concrete)
-> Integer
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
_u ->
        (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
_v ->
        Concrete -> (SWord Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam Concrete
Concrete ((SWord Concrete -> SEval Concrete Value) -> Value)
-> (SWord Concrete -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \(BV w x) -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
        Concrete -> (SWord Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam Concrete
Concrete ((SWord Concrete -> SEval Concrete Value) -> Value)
-> (SWord Concrete -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \(BV _ m) ->
          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 (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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (Eval (WordValue Concrete) -> Value)
-> (Integer -> Eval (WordValue Concrete)) -> Integer -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Integer -> WordValue Concrete)
-> Integer
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 Value
primeECPrims :: Map PrimIdent Value
primeECPrims = [(PrimIdent, Value)] -> Map PrimIdent Value
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(PrimIdent, Value)] -> Map PrimIdent Value)
-> [(PrimIdent, Value)] -> Map PrimIdent Value
forall a b. (a -> b) -> a -> b
$ ((Text, Value) -> (PrimIdent, Value))
-> [(Text, Value)] -> [(PrimIdent, Value)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Text
n,Value
v) -> (Text -> PrimIdent
primeECPrim Text
n, Value
v))
  [ (Text
"ec_double", {-# SCC "PrimeEC::ec_double" #-}
       (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
p ->
        (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
s ->
          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 -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
p ->
        (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
s -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
        (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
t ->
          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 -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
p ->
        (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
d -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
        (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
s ->
          do Integer
d' <- Value -> Integer
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 -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
p ->
        (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
d0 -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
        (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
s  -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
        (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
d1 -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
        (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
t  ->
          do Integer
d0' <- Value -> Integer
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
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 = BigNat -> BigNat -> BigNat -> ProjectivePoint
PrimeEC.ProjectivePoint (BigNat -> BigNat -> BigNat -> ProjectivePoint)
-> Eval BigNat -> Eval (BigNat -> BigNat -> ProjectivePoint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ident -> Eval BigNat
f Ident
"x" Eval (BigNat -> BigNat -> ProjectivePoint)
-> Eval BigNat -> Eval (BigNat -> ProjectivePoint)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ident -> Eval BigNat
f Ident
"y" Eval (BigNat -> ProjectivePoint)
-> Eval BigNat -> Eval ProjectivePoint
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ident -> Eval BigNat
f Ident
"z"
  where
   f :: Ident -> Eval BigNat
f Ident
nm = Integer -> BigNat
PrimeEC.integerToBigNat (Integer -> BigNat) -> (Value -> Integer) -> Value -> BigNat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> Integer
forall sym. GenValue sym -> SInteger sym
fromVInteger (Value -> BigNat) -> Eval Value -> Eval BigNat
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 (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
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 (f :: * -> *) sym.
(Applicative f, SInteger sym ~ Integer) =>
BigNat -> f (GenValue sym)
f BigNat
x), (Ident
"y", BigNat -> Eval Value
forall (f :: * -> *) sym.
(Applicative f, SInteger sym ~ Integer) =>
BigNat -> f (GenValue sym)
f BigNat
y), (Ident
"z", BigNat -> Eval Value
forall (f :: * -> *) sym.
(Applicative f, SInteger sym ~ Integer) =>
BigNat -> f (GenValue sym)
f BigNat
z)]
  where
   f :: BigNat -> f (GenValue sym)
f BigNat
i = GenValue sym -> f (GenValue sym)
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 Value
suiteBPrims :: Map PrimIdent Value
suiteBPrims = [(PrimIdent, Value)] -> Map PrimIdent Value
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(PrimIdent, Value)] -> Map PrimIdent Value)
-> [(PrimIdent, Value)] -> Map PrimIdent Value
forall a b. (a -> b) -> a -> b
$ ((Text, Value) -> (PrimIdent, Value))
-> [(Text, Value)] -> [(PrimIdent, Value)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Text
n, Value
v) -> (Text -> PrimIdent
suiteBPrim Text
n, Value
v))
  [ (Text
"processSHA2_224", {-# SCC "SuiteB::processSHA2_224" #-}
                      (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
n ->
                       (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
xs ->
                         do [Eval Value]
blks <- Integer -> SeqMap Concrete -> [SEval Concrete Value]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n (SeqMap Concrete -> [Eval Value])
-> (Value -> SeqMap Concrete) -> Value -> [Eval Value]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap 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
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 (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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
32 (Eval (WordValue Concrete) -> Value)
-> (Word32 -> Eval (WordValue Concrete)) -> Word32 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Word32 -> WordValue Concrete)
-> Word32
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
zs = Concrete -> [SEval Concrete Value] -> SeqMap Concrete
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
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 -> Eval Value -> Eval Value
seq SeqMap Concrete
zs (Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SeqMap Concrete -> Value
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
7 SeqMap Concrete
zs)))

  , (Text
"processSHA2_256", {-# SCC "SuiteB::processSHA2_256" #-}
                      (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
n ->
                       (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
xs ->
                         do [Eval Value]
blks <- Integer -> SeqMap Concrete -> [SEval Concrete Value]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n (SeqMap Concrete -> [Eval Value])
-> (Value -> SeqMap Concrete) -> Value -> [Eval Value]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap 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
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 (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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
32 (Eval (WordValue Concrete) -> Value)
-> (Word32 -> Eval (WordValue Concrete)) -> Word32 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Word32 -> WordValue Concrete)
-> Word32
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
zs = Concrete -> [SEval Concrete Value] -> SeqMap Concrete
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
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 -> Eval Value -> Eval Value
seq SeqMap Concrete
zs (Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SeqMap Concrete -> Value
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
8 SeqMap Concrete
zs)))

  , (Text
"processSHA2_384", {-# SCC "SuiteB::processSHA2_384" #-}
                      (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
n ->
                       (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
xs ->
                         do [Eval Value]
blks <- Integer -> SeqMap Concrete -> [SEval Concrete Value]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n (SeqMap Concrete -> [Eval Value])
-> (Value -> SeqMap Concrete) -> Value -> [Eval Value]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap 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
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 (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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
64 (Eval (WordValue Concrete) -> Value)
-> (Word64 -> Eval (WordValue Concrete)) -> Word64 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Word64 -> WordValue Concrete)
-> Word64
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
zs = Concrete -> [SEval Concrete Value] -> SeqMap Concrete
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
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 -> Eval Value -> Eval Value
seq SeqMap Concrete
zs (Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SeqMap Concrete -> Value
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
6 SeqMap Concrete
zs)))

  , (Text
"processSHA2_512", {-# SCC "SuiteB::processSHA2_512" #-}
                      (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
n ->
                       (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
xs ->
                         do [Eval Value]
blks <- Integer -> SeqMap Concrete -> [SEval Concrete Value]
forall n sym.
Integral n =>
n -> SeqMap sym -> [SEval sym (GenValue sym)]
enumerateSeqMap Integer
n (SeqMap Concrete -> [Eval Value])
-> (Value -> SeqMap Concrete) -> Value -> [Eval Value]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap 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
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 (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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
64 (Eval (WordValue Concrete) -> Value)
-> (Word64 -> Eval (WordValue Concrete)) -> Word64 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Word64 -> WordValue Concrete)
-> Word64
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
zs = Concrete -> [SEval Concrete Value] -> SeqMap Concrete
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
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 -> Eval Value -> Eval Value
seq SeqMap Concrete
zs (Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SeqMap Concrete -> Value
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
8 SeqMap Concrete
zs)))

  , (Text
"AESKeyExpand", {-# SCC "SuiteB::AESKeyExpand" #-}
      (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam ((Integer -> Value) -> Value) -> (Integer -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Integer
k ->
       (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
seed ->
         do SeqMap Concrete
ss <- Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap sym
fromVSeq (Value -> SeqMap Concrete) -> Eval Value -> Eval (SeqMap Concrete)
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 -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
ss Integer
i)
            let fromWord :: Word32 -> Eval Value
                fromWord :: Word32 -> Eval Value
fromWord = Value -> Eval Value
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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
32 (Eval (WordValue Concrete) -> Value)
-> (Word32 -> Eval (WordValue Concrete)) -> Word32 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Word32 -> WordValue Concrete)
-> Word32
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
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 (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SeqMap Concrete -> Value
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
len (Concrete -> [SEval Concrete Value] -> SeqMap Concrete
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
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 -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
st ->
         do SeqMap Concrete
ss <- Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap sym
fromVSeq (Value -> SeqMap Concrete) -> Eval Value -> Eval (SeqMap Concrete)
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 -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
ss Integer
i)
            let fromWord :: Word32 -> Eval Value
                fromWord :: Word32 -> Eval Value
fromWord = Value -> Eval Value
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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
32 (Eval (WordValue Concrete) -> Value)
-> (Word32 -> Eval (WordValue Concrete)) -> Word32 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Word32 -> WordValue Concrete)
-> Word32
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
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 (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
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
4 (SeqMap Concrete -> Value)
-> ([Word32] -> SeqMap Concrete) -> [Word32] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete -> [SEval Concrete Value] -> SeqMap Concrete
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap Concrete
Concrete ([Eval Value] -> SeqMap Concrete)
-> ([Word32] -> [Eval Value]) -> [Word32] -> SeqMap Concrete
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 -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
st ->
         do SeqMap Concrete
ss <- Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap sym
fromVSeq (Value -> SeqMap Concrete) -> Eval Value -> Eval (SeqMap Concrete)
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 -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
ss Integer
i)
            let fromWord :: Word32 -> Eval Value
                fromWord :: Word32 -> Eval Value
fromWord = Value -> Eval Value
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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
32 (Eval (WordValue Concrete) -> Value)
-> (Word32 -> Eval (WordValue Concrete)) -> Word32 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Word32 -> WordValue Concrete)
-> Word32
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
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 (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
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
4 (SeqMap Concrete -> Value)
-> ([Word32] -> SeqMap Concrete) -> [Word32] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete -> [SEval Concrete Value] -> SeqMap Concrete
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap Concrete
Concrete ([Eval Value] -> SeqMap Concrete)
-> ([Word32] -> [Eval Value]) -> [Word32] -> SeqMap Concrete
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 -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
st ->
         do SeqMap Concrete
ss <- Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap sym
fromVSeq (Value -> SeqMap Concrete) -> Eval Value -> Eval (SeqMap Concrete)
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 -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
ss Integer
i)
            let fromWord :: Word32 -> Eval Value
                fromWord :: Word32 -> Eval Value
fromWord = Value -> Eval Value
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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
32 (Eval (WordValue Concrete) -> Value)
-> (Word32 -> Eval (WordValue Concrete)) -> Word32 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Word32 -> WordValue Concrete)
-> Word32
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
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 (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
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
4 (SeqMap Concrete -> Value)
-> ([Word32] -> SeqMap Concrete) -> [Word32] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete -> [SEval Concrete Value] -> SeqMap Concrete
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap Concrete
Concrete ([Eval Value] -> SeqMap Concrete)
-> ([Word32] -> [Eval Value]) -> [Word32] -> SeqMap Concrete
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 -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
st ->
         do SeqMap Concrete
ss <- Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap sym
fromVSeq (Value -> SeqMap Concrete) -> Eval Value -> Eval (SeqMap Concrete)
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 -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
ss Integer
i)
            let fromWord :: Word32 -> Eval Value
                fromWord :: Word32 -> Eval Value
fromWord = Value -> Eval Value
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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
32 (Eval (WordValue Concrete) -> Value)
-> (Word32 -> Eval (WordValue Concrete)) -> Word32 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Word32 -> WordValue Concrete)
-> Word32
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
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 (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
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
4 (SeqMap Concrete -> Value)
-> ([Word32] -> SeqMap Concrete) -> [Word32] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete -> [SEval Concrete Value] -> SeqMap Concrete
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap Concrete
Concrete ([Eval Value] -> SeqMap Concrete)
-> ([Word32] -> [Eval Value]) -> [Word32] -> SeqMap Concrete
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 -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
st ->
         do SeqMap Concrete
ss <- Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap sym
fromVSeq (Value -> SeqMap Concrete) -> Eval Value -> Eval (SeqMap Concrete)
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 -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
ss Integer
i)
            let fromWord :: Word32 -> Eval Value
                fromWord :: Word32 -> Eval Value
fromWord = Value -> Eval Value
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 -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
32 (Eval (WordValue Concrete) -> Value)
-> (Word32 -> Eval (WordValue Concrete)) -> Word32 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> (Word32 -> WordValue Concrete)
-> Word32
-> Eval (WordValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
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 (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
forall sym. Integer -> SeqMap sym -> GenValue sym
VSeq Integer
4 (SeqMap Concrete -> Value)
-> ([Word32] -> SeqMap Concrete) -> [Word32] -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete -> [SEval Concrete Value] -> SeqMap Concrete
forall sym.
Backend sym =>
sym -> [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap Concrete
Concrete ([Eval Value] -> SeqMap Concrete)
-> ([Word32] -> [Eval Value]) -> [Word32] -> SeqMap Concrete
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
ws = Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap 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 -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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
ws = Value -> SeqMap Concrete
forall sym. GenValue sym -> SeqMap 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 -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
        (Integer -> Eval Word64
toWord Integer
15)

--------------------------------------------------------------------------------

sshrV :: Value
sshrV :: Value
sshrV =
  (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \Nat'
_n ->
  (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \TValue
ix ->
  Concrete -> (SWord Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam Concrete
Concrete ((SWord Concrete -> SEval Concrete Value) -> Value)
-> (SWord Concrete -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \(BV w x) -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
  (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \SEval Concrete Value
y ->
   do Integer
idx <- Eval Value
SEval Concrete Value
y Eval Value
-> (Value -> Eval (Either Integer (WordValue Concrete)))
-> Eval (Either Integer (WordValue Concrete))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Concrete
-> String
-> TValue
-> Value
-> SEval Concrete (Either (SInteger Concrete) (WordValue Concrete))
forall sym.
Backend sym =>
sym
-> String
-> TValue
-> GenValue sym
-> SEval sym (Either (SInteger sym) (WordValue sym))
asIndex Concrete
Concrete String
">>$" TValue
ix Eval (Either Integer (WordValue Concrete))
-> (Either Integer (WordValue Concrete) -> Eval Integer)
-> Eval Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                 Left Integer
idx -> Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
idx
                 Right WordValue Concrete
wv -> 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
wv
      Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Integer -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SEval Concrete (WordValue Concrete) -> Value)
-> SEval Concrete (WordValue Concrete) -> Value
forall a b. (a -> b) -> a -> b
$ WordValue Concrete -> Eval (WordValue Concrete)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WordValue Concrete -> Eval (WordValue Concrete))
-> WordValue Concrete -> Eval (WordValue Concrete)
forall a b. (a -> b) -> a -> b
$ SWord Concrete -> WordValue Concrete
forall sym. SWord sym -> WordValue sym
WordVal (SWord Concrete -> WordValue Concrete)
-> SWord Concrete -> WordValue Concrete
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> BV
mkBv Integer
w (Integer -> BV) -> Integer -> BV
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer -> Integer
signedShiftRW Integer
w Integer
x Integer
idx

logicShift :: (Integer -> Integer -> Integer -> Integer)
              -- ^ The function may assume its arguments are masked.
              -- It is responsible for masking its result if needed.
           -> (Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)
           -> Value
logicShift :: (Integer -> Integer -> Integer -> Integer)
-> (Nat'
    -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)
-> Value
logicShift Integer -> Integer -> Integer -> Integer
opW Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
opS
  = (Nat' -> Value) -> Value
forall sym. Backend sym => (Nat' -> GenValue sym) -> GenValue sym
nlam ((Nat' -> Value) -> Value) -> (Nat' -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ Nat'
a ->
    (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ TValue
_ix ->
    (TValue -> Value) -> Value
forall sym. Backend sym => (TValue -> GenValue sym) -> GenValue sym
tlam ((TValue -> Value) -> Value) -> (TValue -> Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ TValue
c ->
     (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ SEval Concrete Value
l -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
     (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam  ((SEval Concrete Value -> SEval Concrete Value) -> Value)
-> (SEval Concrete Value -> SEval Concrete Value) -> Value
forall a b. (a -> b) -> a -> b
$ \ SEval Concrete Value
r -> do
        Integer
i <- Eval Value
SEval Concrete Value
r Eval Value -> (Value -> Eval Integer) -> Eval Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          VInteger SInteger Concrete
i -> Integer -> Eval Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
SInteger Concrete
i
          VWord Integer
_ SEval Concrete (WordValue Concrete)
wval -> 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 -> Eval BV)
-> Eval (WordValue Concrete) -> Eval BV
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval (WordValue Concrete)
SEval Concrete (WordValue Concrete)
wval)
          Value
_ -> String -> [String] -> Eval Integer
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"logicShift" [String
"not an index"]
        Eval Value
SEval Concrete Value
l Eval Value -> (Value -> Eval Value) -> Eval Value
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          VWord Integer
w SEval Concrete (WordValue Concrete)
wv -> Value -> Eval Value
forall (m :: * -> *) a. Monad m => a -> m a
return (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Integer -> SEval Concrete (WordValue Concrete) -> Value
forall sym. Integer -> SEval sym (WordValue sym) -> GenValue sym
VWord Integer
w (SEval Concrete (WordValue Concrete) -> Value)
-> SEval Concrete (WordValue Concrete) -> Value
forall a b. (a -> b) -> a -> b
$ Eval (WordValue Concrete)
SEval Concrete (WordValue Concrete)
wv Eval (WordValue Concrete)
-> (WordValue Concrete -> Eval (WordValue Concrete))
-> Eval (WordValue Concrete)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                          WordVal (BV _ x) -> WordValue Concrete -> Eval (WordValue Concrete)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue Concrete -> Eval (WordValue Concrete))
-> WordValue Concrete -> Eval (WordValue Concrete)
forall a b. (a -> b) -> a -> b
$ SWord Concrete -> WordValue Concrete
forall sym. SWord sym -> WordValue sym
WordVal (Integer -> Integer -> BV
BV Integer
w (Integer -> Integer -> Integer -> Integer
opW Integer
w Integer
x Integer
i))
                          LargeBitsVal Integer
n SeqMap Concrete
xs -> WordValue Concrete -> Eval (WordValue Concrete)
forall (m :: * -> *) a. Monad m => a -> m a
return (WordValue Concrete -> Eval (WordValue Concrete))
-> WordValue Concrete -> Eval (WordValue Concrete)
forall a b. (a -> b) -> a -> b
$ Integer -> SeqMap Concrete -> WordValue Concrete
forall sym. Integer -> SeqMap sym -> WordValue sym
LargeBitsVal Integer
n (SeqMap Concrete -> WordValue Concrete)
-> SeqMap Concrete -> WordValue Concrete
forall a b. (a -> b) -> a -> b
$ Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
opS (Integer -> Nat'
Nat Integer
n) TValue
c SeqMap Concrete
xs Integer
i

          Value
_ -> Nat' -> TValue -> SeqMap Concrete -> Value
forall sym.
Backend sym =>
Nat' -> TValue -> SeqMap sym -> GenValue sym
mkSeq Nat'
a TValue
c (SeqMap Concrete -> Value) -> Eval (SeqMap Concrete) -> Eval Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
opS Nat'
a TValue
c (SeqMap Concrete -> Integer -> SeqMap Concrete)
-> Eval (SeqMap Concrete) -> Eval (Integer -> SeqMap Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Value -> SEval Concrete (SeqMap Concrete)
forall sym.
Backend sym =>
String -> GenValue sym -> SEval sym (SeqMap sym)
fromSeq String
"logicShift" (Value -> Eval (SeqMap Concrete))
-> Eval Value -> Eval (SeqMap Concrete)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value
SEval Concrete Value
l) Eval (Integer -> SeqMap Concrete)
-> Eval Integer -> Eval (SeqMap Concrete)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> Eval Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
i)

-- Left shift for words.
shiftLW :: Integer -> Integer -> Integer -> Integer
shiftLW :: Integer -> Integer -> Integer -> Integer
shiftLW Integer
w Integer
ival Integer
by
  | Integer
by Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<  Integer
0   = Integer -> Integer -> Integer -> Integer
shiftRW Integer
w Integer
ival (Integer -> Integer
forall a. Num a => a -> a
negate Integer
by)
  | Integer
by Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
w   = Integer
0
  | Integer
by Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound :: Int) = String -> [String] -> Integer
forall a. HasCallStack => String -> [String] -> a
panic String
"shiftLW" [String
"Shift amount too large", Integer -> String
forall a. Show a => a -> String
show Integer
by]
  | Bool
otherwise = Integer -> Integer -> Integer
mask Integer
w (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftL Integer
ival (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
by))

-- Right shift for words
shiftRW :: Integer -> Integer -> Integer -> Integer
shiftRW :: Integer -> Integer -> Integer -> Integer
shiftRW Integer
w Integer
ival Integer
by
  | Integer
by Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<  Integer
0   = Integer -> Integer -> Integer -> Integer
shiftLW Integer
w Integer
ival (Integer -> Integer
forall a. Num a => a -> a
negate Integer
by)
  | Integer
by Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
w   = Integer
0
  | Integer
by Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound :: Int) = String -> [String] -> Integer
forall a. HasCallStack => String -> [String] -> a
panic String
"shiftRW" [String
"Shift amount too large", Integer -> String
forall a. Show a => a -> String
show Integer
by]
  | Bool
otherwise = Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
ival (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
by)

-- signed right shift for words
signedShiftRW :: Integer -> Integer -> Integer -> Integer
signedShiftRW :: Integer -> Integer -> Integer -> Integer
signedShiftRW Integer
w Integer
ival Integer
by
  | Integer
by Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0    = Integer -> Integer -> Integer -> Integer
shiftLW Integer
w Integer
ival (Integer -> Integer
forall a. Num a => a -> a
negate Integer
by)
  | Bool
otherwise =
     let by' :: Integer
by' = Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
w Integer
by in
     if Integer
by' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int
forall a. Bounded a => a
maxBound :: Int) then
       String -> [String] -> Integer
forall a. HasCallStack => String -> [String] -> a
panic String
"signedShiftRW" [String
"Shift amount too large", Integer -> String
forall a. Show a => a -> String
show Integer
by]
     else
       Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR (Integer -> Integer -> Integer
signedValue Integer
w Integer
ival) (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
by')

shiftLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
shiftLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
shiftLS Nat'
w TValue
ety SeqMap Concrete
vs Integer
by
  | Integer
by Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
shiftRS Nat'
w TValue
ety SeqMap Concrete
vs (Integer -> Integer
forall a. Num a => a -> a
negate Integer
by)

shiftLS Nat'
w TValue
ety SeqMap Concrete
vs Integer
by = (Integer -> SEval Concrete Value) -> SeqMap Concrete
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval Concrete Value) -> SeqMap Concrete)
-> (Integer -> SEval Concrete Value) -> SeqMap Concrete
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
  case Nat'
w of
    Nat Integer
len
      | Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
by Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
len -> SeqMap Concrete -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
vs (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
by)
      | Integer
i    Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
len -> Concrete -> TValue -> SEval Concrete Value
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV Concrete
Concrete TValue
ety
      | Bool
otherwise  -> String -> [String] -> Eval Value
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"shiftLS" [String
"Index out of bounds"]
    Nat'
Inf            -> SeqMap Concrete -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
vs (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
by)

shiftRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
shiftRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
shiftRS Nat'
w TValue
ety SeqMap Concrete
vs Integer
by
  | Integer
by Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
shiftLS Nat'
w TValue
ety SeqMap Concrete
vs (Integer -> Integer
forall a. Num a => a -> a
negate Integer
by)

shiftRS Nat'
w TValue
ety SeqMap Concrete
vs Integer
by = (Integer -> SEval Concrete Value) -> SeqMap Concrete
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval Concrete Value) -> SeqMap Concrete)
-> (Integer -> SEval Concrete Value) -> SeqMap Concrete
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
  case Nat'
w of
    Nat Integer
len
      | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
by   -> SeqMap Concrete -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
vs (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
by)
      | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
len   -> Concrete -> TValue -> SEval Concrete Value
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV Concrete
Concrete TValue
ety
      | Bool
otherwise -> String -> [String] -> Eval Value
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"shiftLS" [String
"Index out of bounds"]
    Nat'
Inf
      | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
by   -> SeqMap Concrete -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
vs (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
by)
      | Bool
otherwise -> Concrete -> TValue -> SEval Concrete Value
forall sym.
Backend sym =>
sym -> TValue -> SEval sym (GenValue sym)
zeroV Concrete
Concrete TValue
ety


-- XXX integer doesn't implement rotateL, as there's no bit bound
rotateLW :: Integer -> Integer -> Integer -> Integer
rotateLW :: Integer -> Integer -> Integer -> Integer
rotateLW Integer
0 Integer
i Integer
_  = Integer
i
rotateLW Integer
w Integer
i Integer
by = Integer -> Integer -> Integer
mask Integer
w (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
b) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b))
  where b :: Int
b = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
by Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
w)

rotateLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
rotateLS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
rotateLS Nat'
w TValue
_ SeqMap Concrete
vs Integer
by = (Integer -> SEval Concrete Value) -> SeqMap Concrete
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval Concrete Value) -> SeqMap Concrete)
-> (Integer -> SEval Concrete Value) -> SeqMap Concrete
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
  case Nat'
w of
    Nat Integer
len -> SeqMap Concrete -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
vs ((Integer
by Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
len)
    Nat'
_ -> String -> [String] -> Eval Value
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Eval.Prim.rotateLS" [ String
"unexpected infinite sequence" ]

-- XXX integer doesn't implement rotateR, as there's no bit bound
rotateRW :: Integer -> Integer -> Integer -> Integer
rotateRW :: Integer -> Integer -> Integer -> Integer
rotateRW Integer
0 Integer
i Integer
_  = Integer
i
rotateRW Integer
w Integer
i Integer
by = Integer -> Integer -> Integer
mask Integer
w (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
b) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
b))
  where b :: Int
b = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
by Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
w)

rotateRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
rotateRS :: Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
rotateRS Nat'
w TValue
_ SeqMap Concrete
vs Integer
by = (Integer -> SEval Concrete Value) -> SeqMap Concrete
forall sym. (Integer -> SEval sym (GenValue sym)) -> SeqMap sym
IndexSeqMap ((Integer -> SEval Concrete Value) -> SeqMap Concrete)
-> (Integer -> SEval Concrete Value) -> SeqMap Concrete
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
  case Nat'
w of
    Nat Integer
len -> SeqMap Concrete -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
vs ((Integer
len Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
by Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i) Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
len)
    Nat'
_ -> String -> [String] -> Eval Value
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.Eval.Prim.rotateRS" [ String
"unexpected infinite sequence" ]


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

indexFront :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
indexFront :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
indexFront Nat'
_mblen TValue
_a SeqMap Concrete
vs TValue
_ix (BV -> Integer
bvVal -> Integer
ix) = SeqMap Concrete -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
vs Integer
ix

indexFront_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value
indexFront_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value
indexFront_bits Nat'
mblen TValue
a SeqMap Concrete
vs TValue
ix [Bool]
bs = Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
indexFront Nat'
mblen TValue
a SeqMap Concrete
vs TValue
ix (BV -> Eval Value) -> Eval BV -> Eval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Concrete -> [SBit Concrete] -> SEval Concrete (SWord Concrete)
forall sym.
Backend sym =>
sym -> [SBit sym] -> SEval sym (SWord sym)
packWord Concrete
Concrete [Bool]
[SBit Concrete]
bs

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

indexBack :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
indexBack :: Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
indexBack Nat'
mblen TValue
a SeqMap Concrete
vs TValue
ix (BV -> Integer
bvVal -> Integer
idx) = Nat'
-> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value
indexBack_int Nat'
mblen TValue
a SeqMap Concrete
vs TValue
ix Integer
idx

indexBack_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value
indexBack_bits :: Nat' -> TValue -> SeqMap Concrete -> TValue -> [Bool] -> Eval Value
indexBack_bits Nat'
mblen TValue
a SeqMap Concrete
vs TValue
ix [Bool]
bs = Nat' -> TValue -> SeqMap Concrete -> TValue -> BV -> Eval Value
indexBack Nat'
mblen TValue
a SeqMap Concrete
vs TValue
ix (BV -> Eval Value) -> Eval BV -> Eval Value
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Concrete -> [SBit Concrete] -> SEval Concrete (SWord Concrete)
forall sym.
Backend sym =>
sym -> [SBit sym] -> SEval sym (SWord sym)
packWord Concrete
Concrete [Bool]
[SBit Concrete]
bs

indexBack_int :: Nat' -> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value
indexBack_int :: Nat'
-> TValue -> SeqMap Concrete -> TValue -> Integer -> Eval Value
indexBack_int Nat'
mblen TValue
_a SeqMap Concrete
vs TValue
_ix Integer
idx =
  case Nat'
mblen of
    Nat Integer
len -> SeqMap Concrete -> Integer -> SEval Concrete Value
forall sym. SeqMap sym -> Integer -> SEval sym (GenValue sym)
lookupSeqMap SeqMap Concrete
vs (Integer
len Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
idx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
    Nat'
Inf     -> String -> [String] -> Eval Value
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"indexBack" [String
"unexpected infinite sequence"]

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

updateFront Nat'
_len TValue
_eltTy SeqMap Concrete
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 -> Eval (SeqMap Concrete)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap Concrete -> Eval (SeqMap Concrete))
-> SeqMap Concrete -> Eval (SeqMap Concrete)
forall a b. (a -> b) -> a -> b
$ SeqMap Concrete
-> Integer -> SEval Concrete Value -> SeqMap Concrete
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap Concrete
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
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
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    {- ^ sequence to update -} ->
  Either Integer (WordValue Concrete) {- ^ index -} ->
  Eval Value         {- ^ new value at index -} ->
  Eval (SeqMap Concrete)
updateBack :: Nat'
-> TValue
-> SeqMap Concrete
-> Either Integer (WordValue Concrete)
-> Eval Value
-> Eval (SeqMap Concrete)
updateBack Nat'
Inf TValue
_eltTy SeqMap Concrete
_vs Either Integer (WordValue Concrete)
_w Eval Value
_val =
  String -> [String] -> Eval (SeqMap Concrete)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"Unexpected infinite sequence in updateEnd" []
updateBack (Nat Integer
n) TValue
_eltTy SeqMap Concrete
vs (Left Integer
idx) Eval Value
val = do
  SeqMap Concrete -> Eval (SeqMap Concrete)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap Concrete -> Eval (SeqMap Concrete))
-> SeqMap Concrete -> Eval (SeqMap Concrete)
forall a b. (a -> b) -> a -> b
$ SeqMap Concrete
-> Integer -> SEval Concrete Value -> SeqMap Concrete
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap Concrete
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
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 -> Eval (SeqMap Concrete)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqMap Concrete -> Eval (SeqMap Concrete))
-> SeqMap Concrete -> Eval (SeqMap Concrete)
forall a b. (a -> b) -> a -> b
$ SeqMap Concrete
-> Integer -> SEval Concrete Value -> SeqMap Concrete
forall sym.
SeqMap sym -> Integer -> SEval sym (GenValue sym) -> SeqMap sym
updateSeqMap SeqMap Concrete
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
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
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)


floatPrims :: Concrete -> Map PrimIdent Value
floatPrims :: Concrete -> Map PrimIdent Value
floatPrims Concrete
sym = [(PrimIdent, Value)] -> Map PrimIdent Value
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Text -> PrimIdent
floatPrim Text
i,Value
v) | (Text
i,Value
v) <- [(Text, Value)]
nonInfixTable ]
  where
  ~> :: a -> b -> (a, b)
(~>) = (,)
  nonInfixTable :: [(Text, Value)]
nonInfixTable =
    [ Text
"fpNaN"       Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
e -> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
p ->
                        SFloat Concrete -> Value
forall sym. SFloat sym -> GenValue sym
VFloat BF :: Integer -> Integer -> BigFloat -> BF
BF { bfValue :: BigFloat
bfValue = BigFloat
FP.bfNaN
                                  , bfExpWidth :: Integer
bfExpWidth = Integer
e, bfPrecWidth :: Integer
bfPrecWidth = Integer
p }

    , Text
"fpPosInf"    Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
e -> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
p ->
                       SFloat Concrete -> Value
forall sym. SFloat sym -> GenValue sym
VFloat BF :: Integer -> Integer -> BigFloat -> BF
BF { bfValue :: BigFloat
bfValue = BigFloat
FP.bfPosInf
                                 , bfExpWidth :: Integer
bfExpWidth = Integer
e, bfPrecWidth :: Integer
bfPrecWidth = Integer
p }

    , Text
"fpFromBits"  Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
e -> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
p -> Concrete -> (SWord Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam Concrete
sym \SWord Concrete
bv ->
                       Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ SFloat Concrete -> Value
forall sym. SFloat sym -> GenValue sym
VFloat (SFloat Concrete -> Value) -> SFloat Concrete -> Value
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer -> BF
floatFromBits Integer
e Integer
p (Integer -> BF) -> Integer -> BF
forall a b. (a -> b) -> a -> b
$ BV -> Integer
bvVal SWord Concrete
BV
bv

    , Text
"fpToBits"    Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
e -> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
p -> (SFloat Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
(SFloat sym -> SEval sym (GenValue sym)) -> GenValue sym
flam \SFloat Concrete
x ->
                       Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ Concrete -> Integer -> Integer -> Value
forall sym.
Backend sym =>
sym -> Integer -> Integer -> GenValue sym
word Concrete
sym (Integer
e Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
p)
                            (Integer -> Value) -> Integer -> Value
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> BigFloat -> Integer
floatToBits Integer
e Integer
p
                            (BigFloat -> Integer) -> BigFloat -> Integer
forall a b. (a -> b) -> a -> b
$ BF -> BigFloat
bfValue BF
SFloat Concrete
x
    , Text
"=.="         Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
_ -> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
_ -> (SFloat Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
(SFloat sym -> SEval sym (GenValue sym)) -> GenValue sym
flam \SFloat Concrete
x -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ (SFloat Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
(SFloat sym -> SEval sym (GenValue sym)) -> GenValue sym
flam \SFloat Concrete
y ->
                       Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ SBit Concrete -> Value
forall sym. SBit sym -> GenValue sym
VBit
                            (SBit Concrete -> Value) -> SBit Concrete -> Value
forall a b. (a -> b) -> a -> b
$ Concrete -> Bool -> SBit Concrete
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit Concrete
sym
                            (Bool -> SBit Concrete) -> Bool -> SBit Concrete
forall a b. (a -> b) -> a -> b
$ BigFloat -> BigFloat -> Ordering
FP.bfCompare (BF -> BigFloat
bfValue BF
SFloat Concrete
x) (BF -> BigFloat
bfValue BF
SFloat Concrete
y) Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

    , Text
"fpIsFinite"  Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
_ -> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
_ -> (SFloat Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
(SFloat sym -> SEval sym (GenValue sym)) -> GenValue sym
flam \SFloat Concrete
x ->
                       Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ SBit Concrete -> Value
forall sym. SBit sym -> GenValue sym
VBit (SBit Concrete -> Value) -> SBit Concrete -> Value
forall a b. (a -> b) -> a -> b
$ Concrete -> Bool -> SBit Concrete
forall sym. Backend sym => sym -> Bool -> SBit sym
bitLit Concrete
sym (Bool -> SBit Concrete) -> Bool -> SBit Concrete
forall a b. (a -> b) -> a -> b
$ BigFloat -> Bool
FP.bfIsFinite (BigFloat -> Bool) -> BigFloat -> Bool
forall a b. (a -> b) -> a -> b
$ BF -> BigFloat
bfValue BF
SFloat Concrete
x

      -- From Backend class
    , Text
"fpAdd"      Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~> Concrete -> FPArith2 Concrete -> Value
forall sym. Backend sym => sym -> FPArith2 sym -> GenValue sym
fpBinArithV Concrete
sym FPArith2 Concrete
forall sym. Backend sym => FPArith2 sym
fpPlus
    , Text
"fpSub"      Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~> Concrete -> FPArith2 Concrete -> Value
forall sym. Backend sym => sym -> FPArith2 sym -> GenValue sym
fpBinArithV Concrete
sym FPArith2 Concrete
forall sym. Backend sym => FPArith2 sym
fpMinus
    , Text
"fpMul"      Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~> Concrete -> FPArith2 Concrete -> Value
forall sym. Backend sym => sym -> FPArith2 sym -> GenValue sym
fpBinArithV Concrete
sym FPArith2 Concrete
forall sym. Backend sym => FPArith2 sym
fpMult
    , Text
"fpDiv"      Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~> Concrete -> FPArith2 Concrete -> Value
forall sym. Backend sym => sym -> FPArith2 sym -> GenValue sym
fpBinArithV Concrete
sym FPArith2 Concrete
forall sym. Backend sym => FPArith2 sym
fpDiv

    , Text
"fpFromRational" Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~>
      (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
e -> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
p -> Concrete -> (SWord Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
sym -> (SWord sym -> SEval sym (GenValue sym)) -> GenValue sym
wlam Concrete
sym \SWord Concrete
r -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$ (SEval Concrete Value -> SEval Concrete Value) -> Value
forall sym.
(SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> GenValue sym
lam \SEval Concrete Value
x ->
        do SRational Concrete
rat <- Value -> SRational Concrete
forall sym. GenValue sym -> SRational sym
fromVRational (Value -> SRational Concrete)
-> Eval Value -> Eval (SRational Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval Value
SEval Concrete Value
x
           BF -> Value
forall sym. SFloat sym -> GenValue sym
VFloat (BF -> Value) -> Eval BF -> Eval Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do RoundMode
mode <- Concrete -> SWord Concrete -> SEval Concrete RoundMode
fpRoundMode Concrete
sym SWord Concrete
r
                         BF -> Eval BF
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BF -> Eval BF) -> BF -> Eval BF
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> RoundMode -> Rational -> BF
floatFromRational Integer
e Integer
p RoundMode
mode
                              (Rational -> BF) -> Rational -> BF
forall a b. (a -> b) -> a -> b
$ SRational Concrete -> SInteger Concrete
forall sym. SRational sym -> SInteger sym
sNum SRational Concrete
rat Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% SRational Concrete -> SInteger Concrete
forall sym. SRational sym -> SInteger sym
sDenom SRational Concrete
rat
    , Text
"fpToRational" Text -> Value -> (Text, Value)
forall a b. a -> b -> (a, b)
~>
      (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
_e -> (Integer -> Value) -> Value
forall sym.
Backend sym =>
(Integer -> GenValue sym) -> GenValue sym
ilam \Integer
_p -> (SFloat Concrete -> SEval Concrete Value) -> Value
forall sym.
Backend sym =>
(SFloat sym -> SEval sym (GenValue sym)) -> GenValue sym
flam \SFloat Concrete
fp ->
      case String -> BF -> Either EvalError Rational
floatToRational String
"fpToRational" BF
SFloat Concrete
fp of
        Left EvalError
err -> Concrete -> EvalError -> SEval Concrete Value
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError Concrete
sym EvalError
err
        Right Rational
r  -> Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Value -> Eval Value) -> Value -> Eval Value
forall a b. (a -> b) -> a -> b
$
                      SRational Concrete -> Value
forall sym. SRational sym -> GenValue sym
VRational
                        SRational :: forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational { sNum :: SInteger Concrete
sNum = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r, sDenom :: SInteger Concrete
sDenom = Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r }
    ]