-- |
-- 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.Ratio(numerator,denominator)
import Data.Word(Word32, Word64)
import MonadLib( ChoiceT, findOne, lift )
import qualified LibBF as FP
import qualified Cryptol.F2 as F2

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

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

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

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

type Value = GenValue Concrete

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

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

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


  go :: TValue -> Value -> ChoiceT Eval Expr
  go :: TValue -> Value -> ChoiceT Eval Expr
go TValue
ty Value
val =
    case (TValue
ty,Value
val) of
      (TVRec RecordMap Ident TValue
tfs, VRecord RecordMap Ident (SEval Concrete Value)
vfs) ->
        do -- NB, vfs first argument to keep their display order
           Either (Either Ident Ident) (RecordMap Ident Expr)
res <- (Ident -> Eval Value -> TValue -> ChoiceT Eval Expr)
-> RecordMap Ident (Eval Value)
-> RecordMap Ident TValue
-> ChoiceT
     Eval (Either (Either Ident Ident) (RecordMap Ident Expr))
forall (t :: * -> *) a b c d.
(Ord a, Monad t) =>
(a -> b -> c -> t d)
-> RecordMap a b
-> RecordMap a c
-> t (Either (Either a a) (RecordMap a d))
zipRecordsM (\Ident
_lbl Eval Value
v TValue
t -> TValue -> Value -> ChoiceT Eval Expr
go TValue
t (Value -> ChoiceT Eval Expr)
-> ChoiceT Eval Value -> ChoiceT Eval Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Eval Value -> ChoiceT Eval Value
forall (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 Value
svs) ->
        do [Expr]
ses <- (Value -> ChoiceT Eval Expr) -> [Value] -> ChoiceT Eval [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
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 Value -> [SEval Concrete Value]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n SeqMap Concrete Value
svs))
           Expr -> ChoiceT Eval Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> ChoiceT Eval Expr) -> Expr -> ChoiceT Eval Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Type -> Expr
EList [Expr]
ses (TValue -> Type
tValTy TValue
b)
      (TVSeq Integer
n TValue
TVBit, VWord Integer
_ WordValue Concrete
wval) ->
        do BV Integer
_ Integer
v <- Eval BV -> ChoiceT Eval BV
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadT t, Monad m) =>
m a -> t m a
lift (Concrete -> WordValue Concrete -> SEval Concrete (SWord Concrete)
forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (SWord sym)
asWordVal Concrete
Concrete WordValue Concrete
wval)
           Expr -> ChoiceT Eval Expr
forall (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
forall a. Show a => a -> String
show Doc
doc
             ]

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

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

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

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

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

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

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

   , (Text
"pmult",
        (Integer -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
u ->
        (Integer -> Prim Concrete) -> Prim Concrete
forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
v ->
        (SWord Concrete -> Prim Concrete) -> Prim Concrete
forall sym. (SWord sym -> Prim sym) -> Prim sym
PWordFun \(BV _ 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 -> WordValue Concrete -> Value
forall sym. Integer -> WordValue sym -> GenValue sym
VWord (Integer
1Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
uInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
v) (WordValue Concrete -> Value)
-> (Integer -> WordValue Concrete) -> Integer -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> WordValue Concrete -> Value
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
v (WordValue Concrete -> Value)
-> (Integer -> WordValue Concrete) -> Integer -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 -> WordValue Concrete -> Value
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
w (WordValue Concrete -> Value)
-> (Integer -> WordValue Concrete) -> Integer -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = Integer -> Integer -> Integer -> ProjectivePoint
PrimeEC.toProjectivePoint (Integer -> Integer -> Integer -> ProjectivePoint)
-> Eval Integer -> Eval (Integer -> Integer -> ProjectivePoint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ident -> Eval Integer
f Ident
"x" Eval (Integer -> Integer -> ProjectivePoint)
-> Eval Integer -> Eval (Integer -> ProjectivePoint)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ident -> Eval Integer
f Ident
"y" Eval (Integer -> ProjectivePoint)
-> Eval Integer -> Eval ProjectivePoint
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ident -> Eval Integer
f Ident
"z"
  where
   f :: Ident -> Eval Integer
f Ident
nm = Value -> Integer
forall sym. GenValue sym -> SInteger sym
fromVInteger (Value -> Integer) -> Eval Value -> Eval Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ident -> Value -> SEval Concrete Value
forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
nm Value
v

fromProjectivePoint :: PrimeEC.ProjectivePoint -> Eval Value
fromProjectivePoint :: ProjectivePoint -> Eval Value
fromProjectivePoint (PrimeEC.ProjectivePoint BigNat#
x BigNat#
y BigNat#
z) =
   Value -> Eval Value
forall (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 Value -> [SEval Concrete Value]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n (SeqMap Concrete Value -> [Eval Value])
-> (Value -> SeqMap Concrete Value) -> Value -> [Eval Value]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> SeqMap Concrete Value
forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq (Value -> [Eval Value]) -> Eval Value -> Eval [Eval Value]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Eval Value
SEval Concrete Value
xs
           (SHA.SHA256S Word32
w0 Word32
w1 Word32
w2 Word32
w3 Word32
w4 Word32
w5 Word32
w6 Word32
_) <-
              (SHA256State -> Eval Value -> Eval SHA256State)
-> SHA256State -> [Eval Value] -> Eval SHA256State
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SHA256State
st Eval Value
blk -> SHA256State -> Eval SHA256State -> Eval SHA256State
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 -> WordValue Concrete -> Value
forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
32 (WordValue Concrete -> Value)
-> (Word32 -> WordValue Concrete) -> Word32 -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> WordValue Concrete
forall sym. SWord sym -> WordValue sym
wordVal (BV -> WordValue Concrete)
-> (Word32 -> BV) -> Word32 -> WordValue Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BV
BV Integer
32 (Integer -> BV) -> (Word32 -> Integer) -> Word32 -> BV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger
               zs :: SeqMap Concrete Value
zs = Concrete -> [SEval Concrete Value] -> SeqMap Concrete Value
forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
finiteSeqMap Concrete
Concrete ((Word32 -> Eval Value) -> [Word32] -> [Eval Value]
forall a b. (a -> b) -> [a] -> [b]
map Word32 -> Eval Value
f [Word32
w0,Word32
w1,Word32
w2,Word32
w3,Word32
w4,Word32
w5,Word32
w6])
           SeqMap Concrete Value -> Eval Value -> Eval Value
seq SeqMap Concrete Value
zs (Value -> Eval Value
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> SeqMap Concrete Value -> Value
forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
7 SeqMap Concrete Value
zs)))

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

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

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

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

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

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

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

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

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


toSHA256Block :: Value -> Eval SHA.SHA256Block
toSHA256Block :: Value -> Eval SHA256Block
toSHA256Block Value
blk =
  do let ws :: SeqMap Concrete Value
ws = Value -> SeqMap Concrete Value
forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq Value
blk
     let toWord :: Integer -> Eval Word32
toWord Integer
i = Integer -> Word32
forall a. Num a => Integer -> a
fromInteger (Integer -> Word32) -> (BV -> Integer) -> BV -> Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> Integer
bvVal (BV -> Word32) -> Eval BV -> Eval Word32
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Concrete -> String -> Value -> SEval Concrete (SWord Concrete)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord Concrete
Concrete String
"toSHA256Block" (Value -> Eval BV) -> Eval Value -> Eval BV
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SeqMap Concrete Value -> Integer -> SEval Concrete Value
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap Concrete Value
ws Integer
i)
     Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> Word32
-> SHA256Block
SHA.SHA256Block (Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> Word32
 -> SHA256Block)
-> Eval Word32
-> Eval
     (Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> SHA256Block)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        (Integer -> Eval Word32
toWord Integer
0) Eval
  (Word32
   -> Word32
   -> Word32
   -> Word32
   -> Word32
   -> Word32
   -> Word32
   -> Word32
   -> Word32
   -> Word32
   -> Word32
   -> Word32
   -> Word32
   -> Word32
   -> Word32
   -> SHA256Block)
-> Eval Word32
-> Eval
     (Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> Word32
      -> SHA256Block)
forall (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 Value
ws = Value -> SeqMap Concrete Value
forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq Value
blk
     let toWord :: Integer -> Eval Word64
toWord Integer
i = Integer -> Word64
forall a. Num a => Integer -> a
fromInteger (Integer -> Word64) -> (BV -> Integer) -> BV -> Word64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> Integer
bvVal (BV -> Word64) -> Eval BV -> Eval Word64
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Concrete -> String -> Value -> SEval Concrete (SWord Concrete)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord Concrete
Concrete String
"toSHA512Block" (Value -> Eval BV) -> Eval Value -> Eval BV
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SeqMap Concrete Value -> Integer -> SEval Concrete Value
forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap Concrete Value
ws Integer
i)
     Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> Word64
-> SHA512Block
SHA.SHA512Block (Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> Word64
 -> SHA512Block)
-> Eval Word64
-> Eval
     (Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> SHA512Block)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        (Integer -> Eval Word64
toWord Integer
0) Eval
  (Word64
   -> Word64
   -> Word64
   -> Word64
   -> Word64
   -> Word64
   -> Word64
   -> Word64
   -> Word64
   -> Word64
   -> Word64
   -> Word64
   -> Word64
   -> Word64
   -> Word64
   -> SHA512Block)
-> Eval Word64
-> Eval
     (Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> Word64
      -> SHA512Block)
forall (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)


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

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

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

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

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

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

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

updateBack_word ::
  Nat'               {- ^ length of the sequence -} ->
  TValue             {- ^ type of values in the sequence -} ->
  WordValue Concrete {- ^ bit sequence to update -} ->
  Either Integer (WordValue Concrete) {- ^ index -} ->
  Eval Value         {- ^ new value at index -} ->
  Eval (WordValue Concrete)
updateBack_word :: Nat'
-> TValue
-> WordValue Concrete
-> Either Integer (WordValue Concrete)
-> Eval Value
-> Eval (WordValue Concrete)
updateBack_word Nat'
Inf TValue
_eltTy WordValue Concrete
_bs Either Integer (WordValue Concrete)
_w Eval Value
_val =
  String -> [String] -> Eval (WordValue Concrete)
forall a. HasCallStack => String -> [String] -> a
evalPanic String
"Unexpected infinite sequence in updateEnd" []
updateBack_word (Nat Integer
n) TValue
_eltTy WordValue Concrete
bs (Left Integer
idx) Eval Value
val = do
  Concrete
-> WordValue Concrete
-> Integer
-> SEval Concrete (SBit Concrete)
-> SEval Concrete (WordValue Concrete)
forall sym.
Backend sym =>
sym
-> WordValue sym
-> Integer
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordValue Concrete
Concrete WordValue Concrete
bs (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
idx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) (Value -> Bool
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)