-- |
-- 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 (guard, zipWithM, foldM, mzero)
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.Prims
import Cryptol.Eval.Type
import Cryptol.Eval.Value
import qualified Cryptol.SHA as SHA
import qualified Cryptol.AES as AES
import qualified Cryptol.PrimeEC as PrimeEC
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.AST as AST
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Ident (PrimIdent,prelPrim,floatPrim,suiteBPrim,primeECPrim)
import Cryptol.Utils.PP
import Cryptol.Utils.RecordMap

type Value = GenValue Concrete

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

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

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


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

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

      (TVTuple [TValue]
ts, VTuple [SEval Concrete Value]
tvs) ->
        do Bool -> ChoiceT Eval ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ([TValue] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TValue]
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
<$> ((TValue -> Value -> ChoiceT Eval Expr)
-> [TValue] -> [Value] -> ChoiceT Eval [Expr]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM TValue -> Value -> ChoiceT Eval Expr
go [TValue]
ts ([Value] -> ChoiceT Eval [Expr])
-> ChoiceT Eval [Value] -> ChoiceT Eval [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval [Value] -> ChoiceT Eval [Value]
forall (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))
      (TValue
TVBit, 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"))
      (TValue
TVInteger, VInteger SInteger Concrete
i) ->
        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
tInteger
      (TVIntMod Integer
n, VInteger SInteger Concrete
i) ->
        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 -> Type
tIntMod (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
n))

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

      (TVFloat Integer
e Integer
p, VFloat SFloat Concrete
i) ->
           Expr -> ChoiceT Eval Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PrimMap -> Type -> Type -> BigFloat -> Expr
floatToExpr PrimMap
prims (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
e) (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
p) (BF -> BigFloat
bfValue BF
SFloat Concrete
i))
      (TVSeq Integer
_ TValue
b, VSeq Integer
n SeqMap Concrete
svs) ->
        do [Expr]
ses <- (Value -> ChoiceT Eval Expr) -> [Value] -> ChoiceT Eval [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (TValue -> Value -> ChoiceT Eval Expr
go TValue
b) ([Value] -> ChoiceT Eval [Expr])
-> ChoiceT Eval [Value] -> ChoiceT Eval [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval [Value] -> ChoiceT Eval [Value]
forall (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 (TValue -> Type
tValTy TValue
b)
      (TVSeq Integer
n TValue
TVBit, 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 -> Type
tWord (Integer -> Type
forall a. Integral a => a -> Type
tNum Integer
n))

      (TValue
_,VStream{})  -> ChoiceT Eval Expr
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      (TValue
_,VFun{})     -> ChoiceT Eval Expr
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      (TValue
_,VPoly{})    -> ChoiceT Eval Expr
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      (TValue
_,VNumPoly{}) -> ChoiceT Eval Expr
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      (TValue, Value)
_ -> ChoiceT Eval Expr
forall a. ChoiceT Eval a
mismatch
    where
      mismatch :: forall a. ChoiceT Eval a
      mismatch :: 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 (TValue -> Type
tValTy TValue
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 :: IO EvalOpts -> Map PrimIdent (Prim Concrete)
primTable :: IO EvalOpts -> Map PrimIdent (Prim Concrete)
primTable IO EvalOpts
getEOpts = let sym :: Concrete
sym = Concrete
Concrete in
  Map PrimIdent (Prim Concrete)
-> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Concrete -> IO EvalOpts -> Map PrimIdent (Prim Concrete)
forall sym.
Backend sym =>
sym -> IO EvalOpts -> Map PrimIdent (Prim sym)
genericPrimTable Concrete
sym IO EvalOpts
getEOpts) (Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete))
-> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
forall a b. (a -> b) -> a -> b
$
  Map PrimIdent (Prim Concrete)
-> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Concrete -> Map PrimIdent (Prim Concrete)
forall sym. Backend sym => sym -> Map PrimIdent (Prim sym)
genericFloatTable Concrete
sym) (Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete))
-> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
forall a b. (a -> b) -> a -> b
$
  Map PrimIdent (Prim Concrete)
-> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map PrimIdent (Prim Concrete)
suiteBPrims (Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete))
-> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
forall a b. (a -> b) -> a -> b
$
  Map PrimIdent (Prim Concrete)
-> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map PrimIdent (Prim Concrete)
primeECPrims (Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete))
-> Map PrimIdent (Prim Concrete) -> Map PrimIdent (Prim Concrete)
forall a b. (a -> b) -> a -> b
$

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

  [ (Text
">>$"        , {-# SCC "Prelude::(>>$)" #-}
                    Prim Concrete
sshrV)

    -- Shifts and rotates
  , (Text
"<<"         , {-# SCC "Prelude::(<<)" #-}
                    (Integer -> Integer -> Integer -> Integer)
-> (Nat'
    -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)
-> Prim Concrete
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)
-> Prim Concrete
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)
-> Prim Concrete
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)
-> Prim Concrete
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)
-> Prim Concrete
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))
-> Prim 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)
-> Prim Concrete
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))
-> Prim 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))
-> Prim Concrete
forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> WordValue sym
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (WordValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (SeqMap sym))
-> Prim sym
updatePrim Concrete
sym Nat'
-> TValue
-> WordValue Concrete
-> Either Integer (WordValue Concrete)
-> Eval Value
-> Eval (WordValue Concrete)
Nat'
-> TValue
-> WordValue Concrete
-> Either (SInteger Concrete) (WordValue Concrete)
-> SEval Concrete Value
-> SEval Concrete (WordValue Concrete)
updateFront_word Nat'
-> TValue
-> SeqMap Concrete
-> 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))
-> Prim Concrete
forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> WordValue sym
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (WordValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (SeqMap sym))
-> Prim sym
updatePrim Concrete
sym Nat'
-> TValue
-> WordValue Concrete
-> Either Integer (WordValue Concrete)
-> Eval Value
-> Eval (WordValue Concrete)
Nat'
-> TValue
-> WordValue Concrete
-> Either (SInteger Concrete) (WordValue Concrete)
-> SEval Concrete Value
-> SEval Concrete (WordValue Concrete)
updateBack_word Nat'
-> TValue
-> SeqMap Concrete
-> 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)

   , (Text
"pmult",
        (Integer -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
u ->
        (Integer -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
v ->
        (SWord Concrete -> Prim Concrete) -> Prim Concrete
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \(BV _ x) ->
        (SWord Concrete -> Prim Concrete) -> Prim Concrete
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \(BV _ y) ->
        SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
            let z :: Integer
z = if Integer
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
v then
                      Int -> Integer -> Integer -> Integer
F2.pmult (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
uInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)) Integer
x Integer
y
                    else
                      Int -> Integer -> Integer -> Integer
F2.pmult (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer
vInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1)) Integer
y Integer
x
             in Value -> Eval Value
forall (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 -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_u ->
        (Integer -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
v ->
        (SWord Concrete -> Prim Concrete) -> Prim Concrete
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \(BV w x) ->
        (SWord Concrete -> Prim Concrete) -> Prim Concrete
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \(BV _ m) ->
        SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
          do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
             Value -> Eval Value
forall (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 -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_u ->
        (Integer -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_v ->
        (SWord Concrete -> Prim Concrete) -> Prim Concrete
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \(BV w x) ->
        (SWord Concrete -> Prim Concrete) -> Prim Concrete
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \(BV _ m) ->
        SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
          do Concrete -> SBit Concrete -> EvalError -> SEval Concrete ()
forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
             Value -> Eval Value
forall (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 (Prim Concrete)
primeECPrims :: Map PrimIdent (Prim Concrete)
primeECPrims = [(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete))
-> [(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete)
forall a b. (a -> b) -> a -> b
$ ((Text, Prim Concrete) -> (PrimIdent, Prim Concrete))
-> [(Text, Prim Concrete)] -> [(PrimIdent, Prim Concrete)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Text
n,Prim Concrete
v) -> (Text -> PrimIdent
primeECPrim Text
n, Prim Concrete
v))
  [ (Text
"ec_double", {-# SCC "PrimeEC::ec_double" #-}
       (Integer -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p ->
       (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
s ->
       SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
          do ProjectivePoint
s' <- Value -> Eval ProjectivePoint
toProjectivePoint (Value -> Eval ProjectivePoint)
-> Eval Value -> Eval ProjectivePoint
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value
SEval Concrete Value
s
             let r :: ProjectivePoint
r = PrimeModulus -> ProjectivePoint -> ProjectivePoint
PrimeEC.ec_double (Integer -> PrimeModulus
PrimeEC.primeModulus Integer
p) ProjectivePoint
s'
             ProjectivePoint -> Eval Value
fromProjectivePoint (ProjectivePoint -> Eval Value) -> ProjectivePoint -> Eval Value
forall a b. (a -> b) -> a -> b
$! ProjectivePoint
r)

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

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

  , (Text
"ec_twin_mult", {-# SCC "PrimeEC::ec_twin_mult" #-}
       (Integer -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p  ->
       (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
d0 ->
       (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
s  ->
       (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
d1 ->
       (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
t  ->
       SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
          do Integer
d0' <- Value -> Integer
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 (Prim Concrete)
suiteBPrims :: Map PrimIdent (Prim Concrete)
suiteBPrims = [(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete))
-> [(PrimIdent, Prim Concrete)] -> Map PrimIdent (Prim Concrete)
forall a b. (a -> b) -> a -> b
$ ((Text, Prim Concrete) -> (PrimIdent, Prim Concrete))
-> [(Text, Prim Concrete)] -> [(PrimIdent, Prim Concrete)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Text
n, Prim Concrete
v) -> (Text -> PrimIdent
suiteBPrim Text
n, Prim Concrete
v))
  [ (Text
"processSHA2_224", {-# SCC "SuiteB::processSHA2_224" #-}
     (Integer -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
     (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
xs ->
     SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
        do [Eval Value]
blks <- Integer -> SeqMap Concrete -> [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 = [SEval Concrete Value] -> SeqMap Concrete
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ((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 -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
     (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
xs ->
     SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
        do [Eval Value]
blks <- Integer -> SeqMap Concrete -> [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 = [SEval Concrete Value] -> SeqMap Concrete
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ((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 -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
     (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
xs ->
     SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
        do [Eval Value]
blks <- Integer -> SeqMap Concrete -> [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 = [SEval Concrete Value] -> SeqMap Concrete
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ((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 -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
     (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
xs ->
     SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
        do [Eval Value]
blks <- Integer -> SeqMap Concrete -> [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 = [SEval Concrete Value] -> SeqMap Concrete
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ((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 -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
k ->
      (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
seed ->
      SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do SeqMap Concrete
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 ([SEval Concrete Value] -> SeqMap Concrete
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ((Word32 -> Eval Value) -> [Word32] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Word32 -> Eval Value
fromWord [Word32]
ws))))

  , (Text
"AESInvMixColumns", {-# SCC "SuiteB::AESInvMixColumns" #-}
      (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval Concrete Value
st ->
      SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do SeqMap Concrete
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
. [Eval Value] -> SeqMap Concrete
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ([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 -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval Concrete Value
st ->
      SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do SeqMap Concrete
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
. [Eval Value] -> SeqMap Concrete
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ([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 -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval Concrete Value
st ->
     SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do SeqMap Concrete
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
. [Eval Value] -> SeqMap Concrete
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ([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 -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval Concrete Value
st ->
      SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do SeqMap Concrete
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
. [Eval Value] -> SeqMap Concrete
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ([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 -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval Concrete Value
st ->
     SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do SeqMap Concrete
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
. [Eval Value] -> SeqMap Concrete
forall sym. [SEval sym (GenValue sym)] -> SeqMap sym
finiteSeqMap ([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 :: Prim Concrete
sshrV :: Prim Concrete
sshrV =
  (Nat' -> Prim Concrete) -> Prim Concrete
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
_n ->
  (TValue -> Prim Concrete) -> Prim Concrete
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly  \TValue
ix ->
  (SWord Concrete -> Prim Concrete) -> Prim Concrete
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \(BV w x) ->
  (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
y ->
  SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
   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)
           -> Prim Concrete
logicShift :: (Integer -> Integer -> Integer -> Integer)
-> (Nat'
    -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete)
-> Prim Concrete
logicShift Integer -> Integer -> Integer -> Integer
opW Nat' -> TValue -> SeqMap Concrete -> Integer -> SeqMap Concrete
opS =
  (Nat' -> Prim Concrete) -> Prim Concrete
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
a ->
  (TValue -> Prim Concrete) -> Prim Concrete
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly  \TValue
_ix ->
  (TValue -> Prim Concrete) -> Prim Concrete
forall sym. (TValue -> Prim sym) -> Prim sym
PTyPoly  \TValue
c ->
  (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
l ->
  (SEval Concrete Value -> Prim Concrete) -> Prim Concrete
forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
r ->
  SEval Concrete Value -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
     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)