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

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

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

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

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

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

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

type Value = GenValue Concrete

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

-- | Given an expected type, returns an expression that evaluates to
-- this value, if we can determine it.
toExpr :: PrimMap -> TValue -> Value -> Eval (Maybe AST.Expr)
toExpr :: PrimMap -> TValue -> Value -> Eval (Maybe Expr)
toExpr PrimMap
prims TValue
t0 Value
v0 = 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 <- 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift Eval Value
v) RecordMap Ident (SEval Concrete Value)
vfs RecordMap Ident TValue
tfs
           case Either (Either Ident Ident) (RecordMap Ident Expr)
res of
             Left Either Ident Ident
_ -> forall a. ChoiceT Eval a
mismatch -- different fields
             Right RecordMap Ident Expr
efs -> 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 <- 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 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift Eval Value
v) RecordMap Ident (SEval Concrete Value)
vfs RecordMap Ident TValue
tfs
           case Either (Either Ident Ident) (RecordMap Ident Expr)
res of
             Left Either Ident Ident
_ -> forall a. ChoiceT Eval a
mismatch -- different fields
             Right RecordMap Ident Expr
efs ->
               let f :: Expr
f = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Expr
x Either Nat' TValue
t -> Expr -> Type -> Expr
ETApp Expr
x (Either Nat' TValue -> Type
tNumValTy Either Nat' TValue
t)) (Name -> Expr
EVar (Newtype -> Name
ntConName Newtype
nt)) [Either Nat' TValue]
ts
                in 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 forall (f :: * -> *). Alternative f => Bool -> f ()
guard (forall (t :: * -> *) a. Foldable t => t a -> Int
length [TValue]
ts forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [SEval Concrete Value]
tvs)
           [Expr] -> Expr
ETuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM TValue -> Value -> ChoiceT Eval Expr
go [TValue]
ts forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [SEval Concrete Value]
tvs))
      (TValue
TVBit, VBit SBit Concrete
b) ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Expr
prim (if SBit Concrete
b then Text
"True" else Text
"False"))
      (TValue
TVInteger, VInteger SInteger Concrete
i) ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Expr -> Type -> Expr
ETApp (Expr -> Type -> Expr
ETApp (Text -> Expr
prim Text
"number") (forall a. Integral a => a -> Type
tNum SInteger Concrete
i)) Type
tInteger
      (TVIntMod Integer
n, VInteger SInteger Concrete
i) ->
        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Expr -> Type -> Expr
ETApp (Expr -> Type -> Expr
ETApp (Text -> Expr
prim Text
"number") (forall a. Integral a => a -> Type
tNum SInteger Concrete
i)) (Type -> Type
tIntMod (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") (forall a. Integral a => a -> Type
tNum SInteger Concrete
n)) Type
tInteger
           let d' :: Expr
d' = Expr -> Type -> Expr
ETApp (Expr -> Type -> Expr
ETApp (Text -> Expr
prim Text
"number") (forall a. Integral a => a -> Type
tNum SInteger Concrete
d)) Type
tInteger
           forall (f :: * -> *) a. Applicative f => a -> f a
pure 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) ->
           forall (f :: * -> *) a. Applicative f => a -> f a
pure (PrimMap -> Type -> Type -> BigFloat -> Expr
floatToExpr PrimMap
prims (forall a. Integral a => a -> Type
tNum Integer
e) (forall a. Integral a => a -> Type
tNum Integer
p) (BF -> BigFloat
bfValue SFloat Concrete
i))
      (TVSeq Integer
_ TValue
b, VSeq Integer
n SeqMap Concrete Value
svs) ->
        do [Expr]
ses <- 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) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n SeqMap Concrete Value
svs))
           forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ [Expr] -> Type -> Expr
EList [Expr]
ses (TValue -> Type
tValTy TValue
b)
      (TVSeq Integer
n TValue
TVBit, VWord Integer
_ WordValue Concrete
wval) ->
        do BV Integer
_ Integer
v <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal Concrete
Concrete WordValue Concrete
wval)
           forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Expr -> Type -> Expr
ETApp (Expr -> Type -> Expr
ETApp (Text -> Expr
prim Text
"number") (forall a. Integral a => a -> Type
tNum Integer
v)) (Type -> Type
tWord (forall a. Integral a => a -> Type
tNum Integer
n))

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

floatToExpr :: PrimMap -> AST.Type -> AST.Type -> FP.BigFloat -> AST.Expr
floatToExpr :: PrimMap -> Type -> Type -> BigFloat -> Expr
floatToExpr PrimMap
prims Type
eT Type
pT BigFloat
f =
  case BigFloat -> BFRep
FP.bfToRep BigFloat
f of
    BFRep
FP.BFNaN -> Text -> Expr
mkP Text
"fpNaN"
    FP.BFRep Sign
sign BFNum
num ->
      case (Sign
sign,BFNum
num) of
        (Sign
FP.Pos, BFNum
FP.Zero)   -> Text -> Expr
mkP Text
"fpPosZero"
        (Sign
FP.Neg, BFNum
FP.Zero)   -> Text -> Expr
mkP Text
"fpNegZero"
        (Sign
FP.Pos, BFNum
FP.Inf)    -> Text -> Expr
mkP Text
"fpPosInf"
        (Sign
FP.Neg, BFNum
FP.Inf)    -> Text -> Expr
mkP Text
"fpNegInf"
        (Sign
_, FP.Num Integer
m Int64
e) ->
            let r :: Rational
r = forall a. Real a => a -> Rational
toRational Integer
m forall a. Num a => a -> a -> a
* (Rational
2 forall a b. (Fractional a, Integral b) => a -> b -> a
^^ Int64
e)
            in Expr -> Expr
EProofApp forall a b. (a -> b) -> a -> b
$ PrimMap -> PrimIdent -> Expr
ePrim PrimMap
prims (Text -> PrimIdent
prelPrim Text
"fraction")
                          Expr -> Type -> Expr
`ETApp` forall a. Integral a => a -> Type
tNum (forall a. Ratio a -> a
numerator Rational
r)
                          Expr -> Type -> Expr
`ETApp` forall a. Integral a => a -> Type
tNum (forall a. Ratio a -> a
denominator Rational
r)
                          Expr -> Type -> Expr
`ETApp` 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 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
  forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall sym.
Backend sym =>
sym -> IO EvalOpts -> Map PrimIdent (Prim sym)
genericPrimTable Concrete
sym IO EvalOpts
getEOpts) forall a b. (a -> b) -> a -> b
$
  forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall sym. Backend sym => sym -> Map PrimIdent (Prim sym)
genericFloatTable Concrete
sym) forall a b. (a -> b) -> a -> b
$
  forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map PrimIdent (Prim Concrete)
suiteBPrims forall a b. (a -> b) -> a -> b
$
  forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map PrimIdent (Prim Concrete)
primeECPrims forall a b. (a -> b) -> a -> b
$

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

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

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

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

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

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

  , (Text
"pdiv",
        forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_u ->
        forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
_v ->
        forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \(BV Integer
w Integer
x) ->
        forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \(BV Integer
_ Integer
m) ->
        forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
          do forall sym.
Backend sym =>
sym -> SBit sym -> EvalError -> SEval sym ()
assertSideCondition Concrete
sym (Integer
m forall a. Eq a => a -> a -> Bool
/= Integer
0) EvalError
DivideByZero
             forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. SWord sym -> WordValue sym
wordVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BV
mkBv Integer
w forall a b. (a -> b) -> a -> b
$! Int -> Integer -> Integer -> Integer
F2.pdiv (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 = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ 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" #-}
       forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p ->
       forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
s ->
       forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
          do ProjectivePoint
s' <- Value -> Eval ProjectivePoint
toProjectivePoint forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< 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 forall a b. (a -> b) -> a -> b
$! ProjectivePoint
r)

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

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

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

toProjectivePoint :: Value -> Eval PrimeEC.ProjectivePoint
toProjectivePoint :: Value -> Eval ProjectivePoint
toProjectivePoint Value
v = Integer -> Integer -> Integer -> ProjectivePoint
PrimeEC.toProjectivePoint forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ident -> Eval Integer
f Ident
"x" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ident -> Eval Integer
f Ident
"y" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ident -> Eval Integer
f Ident
"z"
  where
   f :: Ident -> Eval Integer
f Ident
nm = forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) =
   forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields forall a b. (a -> b) -> a -> b
$ [(Ident
"x", forall {sym} {f :: * -> *}.
(SInteger sym ~ Integer, Applicative f) =>
BigNat# -> f (GenValue sym)
f BigNat#
x), (Ident
"y", forall {sym} {f :: * -> *}.
(SInteger sym ~ Integer, Applicative f) =>
BigNat# -> f (GenValue sym)
f BigNat#
y), (Ident
"z", forall {sym} {f :: * -> *}.
(SInteger sym ~ Integer, Applicative f) =>
BigNat# -> f (GenValue sym)
f BigNat#
z)]
  where
   f :: BigNat# -> f (GenValue sym)
f BigNat#
i = forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ 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" #-}
     forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
     forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval Concrete Value
xs ->
     forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
        do [Eval Value]
blks <- forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval Concrete Value
xs
           (SHA.SHA256S Word32
w0 Word32
w1 Word32
w2 Word32
w3 Word32
w4 Word32
w5 Word32
w6 Word32
_) <-
              forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SHA256State
st Eval Value
blk -> seq :: forall a b. a -> b -> b
seq SHA256State
st (SHA256State -> SHA256Block -> SHA256State
SHA.processSHA256Block SHA256State
st forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Eval SHA256Block
toSHA256Block 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
32 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. SWord sym -> WordValue sym
wordVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BV
BV Integer
32 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
               zs :: SeqMap Concrete Value
zs = forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
finiteSeqMap Concrete
Concrete (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])
           seq :: forall a b. a -> b -> b
seq SeqMap Concrete Value
zs (forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
7 SeqMap Concrete Value
zs)))

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

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

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

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

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

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

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

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

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


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


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


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

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

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

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

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

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

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