-- |
-- Module      :  Cryptol.Eval.What4
-- Copyright   :  (c) 2020 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
module Cryptol.Eval.What4
  ( Value
  , primTable
  ) where

import qualified Control.Exception as X
import           Control.Concurrent.MVar
import           Control.Monad (foldM)
import           Control.Monad.IO.Class

import qualified Data.Map as Map
import qualified Data.Set as Set
import           Data.Text (Text)
import qualified Data.Text as Text
import           Data.Parameterized.Context
import           Data.Parameterized.TraversableFC
import           Data.Parameterized.Some
import qualified Data.BitVector.Sized as BV

import qualified What4.Interface as W4
import qualified What4.SWord as SW
import qualified What4.Utils.AbstractDomains as W4

import Cryptol.Backend
import Cryptol.Backend.Monad ( EvalError(..), Unsupported(..) )
import Cryptol.Backend.SeqMap
import Cryptol.Backend.WordValue
import Cryptol.Backend.What4

import Cryptol.Eval.Generic
import Cryptol.Eval.Prims
import Cryptol.Eval.Type (TValue(..))
import Cryptol.Eval.Value


import qualified Cryptol.SHA as SHA

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

import Cryptol.Utils.Ident
import Cryptol.Utils.Panic
import Cryptol.Utils.RecordMap

type Value sym = GenValue (What4 sym)

-- See also Cryptol.Prims.Eval.primTable
primTable :: W4.IsSymExprBuilder sym => What4 sym -> IO EvalOpts -> Map.Map PrimIdent (Prim (What4 sym))
primTable :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> IO EvalOpts -> Map PrimIdent (Prim (What4 sym))
primTable What4 sym
sym IO EvalOpts
getEOpts =
  forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall sym.
IsSymExprBuilder sym =>
What4 sym -> Map PrimIdent (Prim (What4 sym))
suiteBPrims What4 sym
sym) forall a b. (a -> b) -> a -> b
$
  forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall sym.
IsSymExprBuilder sym =>
What4 sym -> Map PrimIdent (Prim (What4 sym))
primeECPrims What4 sym
sym) forall a b. (a -> b) -> a -> b
$
  forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall sym. Backend sym => sym -> Map PrimIdent (Prim sym)
genericFloatTable What4 sym
sym) forall a b. (a -> b) -> a -> b
$
  forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall sym.
Backend sym =>
sym -> IO EvalOpts -> Map PrimIdent (Prim sym)
genericPrimTable What4 sym
sym IO EvalOpts
getEOpts) forall a b. (a -> b) -> a -> b
$

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

  [ -- Indexing and updates
    (Text
"@"           , 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 What4 sym
sym IndexDirection
IndexForward  (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> SInteger (What4 sym)
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_int What4 sym
sym) (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> Integer
-> [IndexSegment (What4 sym)]
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_segs What4 sym
sym))
  , (Text
"!"           , 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 What4 sym
sym IndexDirection
IndexBackward (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> SInteger (What4 sym)
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_int What4 sym
sym) (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> Integer
-> [IndexSegment (What4 sym)]
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_segs What4 sym
sym))

  , (Text
"update"      , forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> WordValue sym
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (WordValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym (GenValue sym)
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (SeqMap sym (GenValue sym)))
-> Prim sym
updatePrim What4 sym
sym (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> WordValue (What4 sym)
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (WordValue (What4 sym))
updateFrontSym_word What4 sym
sym) (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateFrontSym What4 sym
sym))
  , (Text
"updateEnd"   , forall sym.
Backend sym =>
sym
-> (Nat'
    -> TValue
    -> WordValue sym
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (WordValue sym))
-> (Nat'
    -> TValue
    -> SeqMap sym (GenValue sym)
    -> Either (SInteger sym) (WordValue sym)
    -> SEval sym (GenValue sym)
    -> SEval sym (SeqMap sym (GenValue sym)))
-> Prim sym
updatePrim What4 sym
sym (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> WordValue (What4 sym)
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (WordValue (What4 sym))
updateBackSym_word What4 sym
sym)  (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateBackSym What4 sym
sym))

  ]

primeECPrims :: W4.IsSymExprBuilder sym => What4 sym -> Map.Map PrimIdent (Prim (What4 sym))
primeECPrims :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> Map PrimIdent (Prim (What4 sym))
primeECPrims What4 sym
sym = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [ (Text -> PrimIdent
primeECPrim Text
n, Prim (What4 sym)
v) | (Text
n,Prim (What4 sym)
v) <- [(Text, Prim (What4 sym))]
prims ]
 where
 ~> :: a -> b -> (a, b)
(~>) = (,)

 prims :: [(Text, Prim (What4 sym))]
prims =
  [ -- {p} (prime p, p > 3) => ProjectivePoint p -> ProjectivePoint p
    Text
"ec_double" forall a b. a -> b -> (a, b)
~>
      forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p ->
      forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
s ->
      forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do SymExpr sym BaseIntegerType
p' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym Integer
p
            SymExpr sym ProjectivePoint
s' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
s
            forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"Prime ECC"
            SymFn
  sym
  ((EmptyCtx ::> BaseIntegerType) ::> ProjectivePoint)
  ProjectivePoint
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"ec_double"
                              (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr) BaseTypeRepr ProjectivePoint
projectivePointRepr
            SymExpr sym ProjectivePoint
z  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
  sym
  ((EmptyCtx ::> BaseIntegerType) ::> ProjectivePoint)
  ProjectivePoint
fn (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
p' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
s')
            forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint What4 sym
sym SymExpr sym ProjectivePoint
z

    -- {p} (prime p, p > 3) => ProjectivePoint p -> ProjectivePoint p -> ProjectivePoint p
  , Text
"ec_add_nonzero" forall a b. a -> b -> (a, b)
~>
      forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p ->
      forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
s ->
      forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
t ->
      forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do SymExpr sym BaseIntegerType
p' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym Integer
p
            SymExpr sym ProjectivePoint
s' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
s
            SymExpr sym ProjectivePoint
t' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
t
            forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"Prime ECC"
            SymFn
  sym
  (((EmptyCtx ::> BaseIntegerType) ::> ProjectivePoint)
   ::> ProjectivePoint)
  ProjectivePoint
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"ec_add_nonzero"
                              (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr) BaseTypeRepr ProjectivePoint
projectivePointRepr
            SymExpr sym ProjectivePoint
z  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
  sym
  (((EmptyCtx ::> BaseIntegerType) ::> ProjectivePoint)
   ::> ProjectivePoint)
  ProjectivePoint
fn (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
p' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
s' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
t')
            forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint What4 sym
sym SymExpr sym ProjectivePoint
z

    -- {p} (prime p, p > 3) => Z p -> ProjectivePoint p -> ProjectivePoint p
  , Text
"ec_mult" forall a b. a -> b -> (a, b)
~>
      forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p ->
      forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
k ->
      forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
s ->
      forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do SymExpr sym BaseIntegerType
p' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym Integer
p
            SymExpr sym BaseIntegerType
k' <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
k
            SymExpr sym ProjectivePoint
s' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
s
            forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"Prime ECC"
            SymFn
  sym
  (((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
   ::> ProjectivePoint)
  ProjectivePoint
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"ec_mult"
                              (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr) BaseTypeRepr ProjectivePoint
projectivePointRepr
            SymExpr sym ProjectivePoint
z  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
  sym
  (((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
   ::> ProjectivePoint)
  ProjectivePoint
fn (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
p' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
k' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
s')
            forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint What4 sym
sym SymExpr sym ProjectivePoint
z

    -- {p} (prime p, p > 3) => Z p -> ProjectivePoint p -> Z p -> ProjectivePoint p -> ProjectivePoint p
  , Text
"ec_twin_mult" forall a b. a -> b -> (a, b)
~>
      forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
p ->
      forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
j ->
      forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
s ->
      forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
k ->
      forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
t ->
      forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do SymExpr sym BaseIntegerType
p' <- forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym Integer
p
            SymExpr sym BaseIntegerType
j' <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
j
            SymExpr sym ProjectivePoint
s' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
s
            SymExpr sym BaseIntegerType
k' <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
k
            SymExpr sym ProjectivePoint
t' <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
t
            forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"Prime ECC"
            SymFn
  sym
  (((((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
     ::> ProjectivePoint)
    ::> BaseIntegerType)
   ::> ProjectivePoint)
  ProjectivePoint
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"ec_twin_mult"
                              (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
                                                              BaseTypeRepr BaseIntegerType
W4.BaseIntegerRepr forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> BaseTypeRepr ProjectivePoint
projectivePointRepr)
                              BaseTypeRepr ProjectivePoint
projectivePointRepr
            SymExpr sym ProjectivePoint
z  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
  sym
  (((((EmptyCtx ::> BaseIntegerType) ::> BaseIntegerType)
     ::> ProjectivePoint)
    ::> BaseIntegerType)
   ::> ProjectivePoint)
  ProjectivePoint
fn (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
p' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
j' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
s' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
k' forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym ProjectivePoint
t')
            forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint What4 sym
sym SymExpr sym ProjectivePoint
z
  ]

type ProjectivePoint = W4.BaseStructType (EmptyCtx ::> W4.BaseIntegerType ::> W4.BaseIntegerType ::> W4.BaseIntegerType)

projectivePointRepr :: W4.BaseTypeRepr ProjectivePoint
projectivePointRepr :: BaseTypeRepr ProjectivePoint
projectivePointRepr = forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
W4.knownRepr

toProjectivePoint :: W4.IsSymExprBuilder sym =>
  What4 sym -> Value sym -> SEval (What4 sym) (W4.SymExpr sym ProjectivePoint)
toProjectivePoint :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Value sym -> SEval (What4 sym) (SymExpr sym ProjectivePoint)
toProjectivePoint What4 sym
sym Value sym
v =
  do SymExpr sym BaseIntegerType
x <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
"x" Value sym
v
     SymExpr sym BaseIntegerType
y <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
"y" Value sym
v
     SymExpr sym BaseIntegerType
z <- forall sym. GenValue sym -> SInteger sym
fromVInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym. Ident -> GenValue sym -> SEval sym (GenValue sym)
lookupRecord Ident
"z" Value sym
v
     forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
W4.mkStruct (forall sym. What4 sym -> sym
w4 What4 sym
sym) (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
x forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
y forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym BaseIntegerType
z)

fromProjectivePoint :: W4.IsSymExprBuilder sym =>
  What4 sym -> W4.SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym ProjectivePoint -> SEval (What4 sym) (Value sym)
fromProjectivePoint What4 sym
sym SymExpr sym ProjectivePoint
p = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
  do Value sym
x <- forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym ProjectivePoint
p (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @0)
     Value sym
y <- forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym ProjectivePoint
p (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @1)
     Value sym
z <- forall sym. SInteger sym -> GenValue sym
VInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym ProjectivePoint
p (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @2)
     forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord forall a b. (a -> b) -> a -> b
$ forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields [ (String -> Ident
packIdent String
"x",forall (f :: * -> *) a. Applicative f => a -> f a
pure Value sym
x), (String -> Ident
packIdent String
"y",forall (f :: * -> *) a. Applicative f => a -> f a
pure Value sym
y),(String -> Ident
packIdent String
"z",forall (f :: * -> *) a. Applicative f => a -> f a
pure Value sym
z) ]


suiteBPrims :: W4.IsSymExprBuilder sym => What4 sym -> Map.Map PrimIdent (Prim (What4 sym))
suiteBPrims :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> Map PrimIdent (Prim (What4 sym))
suiteBPrims What4 sym
sym = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [ (Text -> PrimIdent
suiteBPrim Text
n, Prim (What4 sym)
v) | (Text
n,Prim (What4 sym)
v) <- [(Text, Prim (What4 sym))]
prims ]
 where
 ~> :: a -> b -> (a, b)
(~>) = (,)

 prims :: [(Text, Prim (What4 sym))]
prims =
  [ Text
"AESEncRound" forall a b. a -> b -> (a, b)
~>
       forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
st ->
       forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES encryption"
            forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
"AESEncRound" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
st
  , Text
"AESEncFinalRound" forall a b. a -> b -> (a, b)
~>
       forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
st ->
       forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES encryption"
            forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
"AESEncFinalRound" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
st
  , Text
"AESDecRound" forall a b. a -> b -> (a, b)
~>
       forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
st ->
       forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES decryption"
            forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
"AESDecRound" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
st
  , Text
"AESDecFinalRound" forall a b. a -> b -> (a, b)
~>
       forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
st ->
       forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES decryption"
            forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
"AESDecFinalRound" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
st
  , Text
"AESInvMixColumns" forall a b. a -> b -> (a, b)
~>
       forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun \SEval (What4 sym) (GenValue (What4 sym))
st ->
       forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
         do forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES key expansion"
            forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
"AESInvMixColumns" forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval (What4 sym) (GenValue (What4 sym))
st

    -- {k} (fin k, k >= 4, 8 >= k) => [k][32] -> [4*(k+7)][32]
  , Text
"AESKeyExpand" forall a b. a -> b -> (a, b)
~>
       forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
k ->
       forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
st ->
       forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
          do SeqMap (What4 sym) (GenValue (What4 sym))
ss <- forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
st
             -- pack the arguments into a k-tuple of 32-bit values
             Some Assignment (SymExpr sym) x
ws <- forall {k} (m :: * -> *) (f :: k -> *).
Applicative m =>
Int -> (Int -> m (Some f)) -> m (Some (Assignment f))
generateSomeM (forall a. Num a => Integer -> a
fromInteger Integer
k) (\Int
i -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"AESKeyExpand" SeqMap (What4 sym) (GenValue (What4 sym))
ss (forall a. Integral a => a -> Integer
toInteger Int
i))
             -- get the types of the arguments
             let args :: Assignment BaseTypeRepr x
args = forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Assignment (SymExpr sym) x
ws
             -- compute the return type which is a tuple of @4*(k+7)@ 32-bit values
             Some Assignment BaseTypeRepr x
ret <- forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall {k} (f :: k -> *).
Int -> (Int -> Some f) -> Some (Assignment f)
generateSome (Int
4forall a. Num a => a -> a -> a
*(forall a. Num a => Integer -> a
fromInteger Integer
k forall a. Num a => a -> a -> a
+ Int
7)) (\Int
_ -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32)))
             -- retrieve the relevant uninterpreted function and apply it to the arguments
             forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"AES key expansion"
             SymFn sym x ('BaseStructType x)
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym (Text
"AESKeyExpand" forall a. Semigroup a => a -> a -> a
<> String -> Text
Text.pack (forall a. Show a => a -> String
show Integer
k)) Assignment BaseTypeRepr x
args (forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx -> BaseTypeRepr ('BaseStructType ctx)
W4.BaseStructRepr Assignment BaseTypeRepr x
ret)
             SymExpr sym ('BaseStructType x)
z  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn sym x ('BaseStructType x)
fn Assignment (SymExpr sym) x
ws
             -- compute a sequence that projects the relevant fields from the outout tuple
             forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq (Integer
4forall a. Num a => a -> a -> a
*(Integer
kforall a. Num a => a -> a -> a
+Integer
7)) forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
               case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex (forall a. Num a => Integer -> a
fromInteger Integer
i) (forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
size Assignment BaseTypeRepr x
ret) of
                 Just (Some Index x x
idx) | Just x :~: BaseBVType 32
W4.Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (Assignment BaseTypeRepr x
retforall {k} (f :: k -> *) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
!Index x x
idx) (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32)) ->
                   forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym ('BaseStructType x)
z Index x x
idx)
                 Maybe (Some (Index x))
_ -> forall a. String -> [String] -> a
evalPanic String
"AESKeyExpand" [String
"Index out of range", forall a. Show a => a -> String
show Integer
k, forall a. Show a => a -> String
show Integer
i]

    -- {n} (fin n) => [n][16][32] -> [7][32]
  , Text
"processSHA2_224" forall a b. a -> b -> (a, b)
~>
    forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
xs ->
    forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
       do [W4Eval sym (GenValue (What4 sym))]
blks <- forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
xs
          forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"SHA-224"
          SymExpr sym (BaseStructType SHA256State)
initSt <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA256State -> IO (SymExpr sym (BaseStructType SHA256State))
mkSHA256InitialState What4 sym
sym SHA256State
SHA.initialSHA224State)
          SymExpr sym (BaseStructType SHA256State)
finalSt <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SymExpr sym (BaseStructType SHA256State)
st W4Eval sym (GenValue (What4 sym))
blk -> forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA256State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA256State))
processSHA256Block What4 sym
sym SymExpr sym (BaseStructType SHA256State)
st forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< W4Eval sym (GenValue (What4 sym))
blk) SymExpr sym (BaseStructType SHA256State)
initSt [W4Eval sym (GenValue (What4 sym))]
blks
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
7 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
i ->
            case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex (forall a. Num a => Integer -> a
fromInteger Integer
i) (forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize :: Size SHA256State) of
              Just (Some Index SHA256State x
idx) ->
                do SymExpr sym x
z <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym (BaseStructType SHA256State)
finalSt Index SHA256State x
idx
                   case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym x
z) (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32)) of
                     Just x :~: BaseBVType 32
W4.Refl -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 SymExpr sym x
z
                     Maybe (x :~: BaseBVType 32)
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_224" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
              Maybe (Some (Index SHA256State))
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_224" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]

    -- {n} (fin n) => [n][16][32] -> [8][32]
  , Text
"processSHA2_256" forall a b. a -> b -> (a, b)
~>
    forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
xs ->
    forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
       do [W4Eval sym (GenValue (What4 sym))]
blks <- forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
xs
          forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"SHA-256"
          SymExpr sym (BaseStructType SHA256State)
initSt <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA256State -> IO (SymExpr sym (BaseStructType SHA256State))
mkSHA256InitialState What4 sym
sym SHA256State
SHA.initialSHA256State)
          SymExpr sym (BaseStructType SHA256State)
finalSt <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SymExpr sym (BaseStructType SHA256State)
st W4Eval sym (GenValue (What4 sym))
blk -> forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA256State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA256State))
processSHA256Block What4 sym
sym SymExpr sym (BaseStructType SHA256State)
st forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< W4Eval sym (GenValue (What4 sym))
blk) SymExpr sym (BaseStructType SHA256State)
initSt [W4Eval sym (GenValue (What4 sym))]
blks
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
8 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
i ->
            case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex (forall a. Num a => Integer -> a
fromInteger Integer
i) (forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize :: Size SHA256State) of
              Just (Some Index SHA256State x
idx) ->
                do SymExpr sym x
z <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym (BaseStructType SHA256State)
finalSt Index SHA256State x
idx
                   case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym x
z) (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32)) of
                     Just x :~: BaseBVType 32
W4.Refl -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 SymExpr sym x
z
                     Maybe (x :~: BaseBVType 32)
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_256" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
              Maybe (Some (Index SHA256State))
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_256" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]

    -- {n} (fin n) => [n][16][64] -> [6][64]
  , Text
"processSHA2_384" forall a b. a -> b -> (a, b)
~>
    forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
xs ->
    forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
       do [W4Eval sym (GenValue (What4 sym))]
blks <- forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
xs
          forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"SHA-384"
          SymExpr sym (BaseStructType SHA512State)
initSt <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA512State -> IO (SymExpr sym (BaseStructType SHA512State))
mkSHA512InitialState What4 sym
sym SHA512State
SHA.initialSHA384State)
          SymExpr sym (BaseStructType SHA512State)
finalSt <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SymExpr sym (BaseStructType SHA512State)
st W4Eval sym (GenValue (What4 sym))
blk -> forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA512State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA512State))
processSHA512Block What4 sym
sym SymExpr sym (BaseStructType SHA512State)
st forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< W4Eval sym (GenValue (What4 sym))
blk) SymExpr sym (BaseStructType SHA512State)
initSt [W4Eval sym (GenValue (What4 sym))]
blks
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
6 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
i ->
            case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex (forall a. Num a => Integer -> a
fromInteger Integer
i) (forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize :: Size SHA512State) of
              Just (Some Index SHA512State x
idx) ->
                do SymExpr sym x
z <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym (BaseStructType SHA512State)
finalSt Index SHA512State x
idx
                   case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym x
z) (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @64)) of
                     Just x :~: BaseBVType 64
W4.Refl -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 64 -> SEval (What4 sym) (Value sym)
fromWord64 SymExpr sym x
z
                     Maybe (x :~: BaseBVType 64)
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_384" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
              Maybe (Some (Index SHA512State))
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_384" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]

    -- {n} (fin n) => [n][16][64] -> [8][64]
  , Text
"processSHA2_512" forall a b. a -> b -> (a, b)
~>
    forall sym. (Integer -> Prim sym) -> Prim sym
PFinPoly \Integer
n ->
    forall sym. (SEval sym (GenValue sym) -> Prim sym) -> Prim sym
PFun     \SEval (What4 sym) (GenValue (What4 sym))
xs ->
    forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim
       do [W4Eval sym (GenValue (What4 sym))]
blks <- forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap Integer
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
xs
          forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
"SHA-512"
          SymExpr sym (BaseStructType SHA512State)
initSt <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA512State -> IO (SymExpr sym (BaseStructType SHA512State))
mkSHA512InitialState What4 sym
sym SHA512State
SHA.initialSHA512State)
          SymExpr sym (BaseStructType SHA512State)
finalSt <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\SymExpr sym (BaseStructType SHA512State)
st W4Eval sym (GenValue (What4 sym))
blk -> forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA512State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA512State))
processSHA512Block What4 sym
sym SymExpr sym (BaseStructType SHA512State)
st forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< W4Eval sym (GenValue (What4 sym))
blk) SymExpr sym (BaseStructType SHA512State)
initSt [W4Eval sym (GenValue (What4 sym))]
blks
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
8 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
i ->
            case forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
intIndex (forall a. Num a => Integer -> a
fromInteger Integer
i) (forall k (ctx :: Ctx k). KnownContext ctx => Size ctx
knownSize :: Size SHA512State) of
              Just (Some Index SHA512State x
idx) ->
                do SymExpr sym x
z <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr sym (BaseStructType SHA512State)
finalSt Index SHA512State x
idx
                   case forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym x
z) (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W4.BaseBVRepr (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @64)) of
                     Just x :~: BaseBVType 64
W4.Refl -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 64 -> SEval (What4 sym) (Value sym)
fromWord64 SymExpr sym x
z
                     Maybe (x :~: BaseBVType 64)
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_512" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
              Maybe (Some (Index SHA512State))
Nothing -> forall a. String -> [String] -> a
evalPanic String
"processSHA2_512" [String
"Index out of range", forall a. Show a => a -> String
show Integer
i]
  ]


type SHA256State =
  EmptyCtx ::>
    W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::>
    W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32

type SHA512State =
  EmptyCtx ::>
    W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64 ::>
    W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64 ::> W4.BaseBVType 64


mkSHA256InitialState :: W4.IsSymExprBuilder sym =>
  What4 sym ->
  SHA.SHA256State ->
  IO (W4.SymExpr sym (W4.BaseStructType SHA256State))
mkSHA256InitialState :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA256State -> IO (SymExpr sym (BaseStructType SHA256State))
mkSHA256InitialState What4 sym
sym (SHA.SHA256S Word32
s0 Word32
s1 Word32
s2 Word32
s3 Word32
s4 Word32
s5 Word32
s6 Word32
s7) =
  do SymExpr sym (BaseBVType 32)
z0 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s0
     SymExpr sym (BaseBVType 32)
z1 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s1
     SymExpr sym (BaseBVType 32)
z2 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s2
     SymExpr sym (BaseBVType 32)
z3 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s3
     SymExpr sym (BaseBVType 32)
z4 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s4
     SymExpr sym (BaseBVType 32)
z5 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s5
     SymExpr sym (BaseBVType 32)
z6 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s6
     SymExpr sym (BaseBVType 32)
z7 <- Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
s7
     forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
W4.mkStruct (forall sym. What4 sym -> sym
w4 What4 sym
sym) (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z0 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z1 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z2 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z3 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z4 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z5 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z6 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
z7)
 where lit :: Word32 -> IO (SymExpr sym (BaseBVType 32))
lit Word32
w = forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32) (Word32 -> BV 32
BV.word32 Word32
w)

mkSHA512InitialState :: W4.IsSymExprBuilder sym =>
  What4 sym ->
  SHA.SHA512State ->
  IO (W4.SymExpr sym (W4.BaseStructType SHA512State))
mkSHA512InitialState :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SHA512State -> IO (SymExpr sym (BaseStructType SHA512State))
mkSHA512InitialState What4 sym
sym (SHA.SHA512S Word64
s0 Word64
s1 Word64
s2 Word64
s3 Word64
s4 Word64
s5 Word64
s6 Word64
s7) =
  do SymExpr sym (BaseBVType 64)
z0 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s0
     SymExpr sym (BaseBVType 64)
z1 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s1
     SymExpr sym (BaseBVType 64)
z2 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s2
     SymExpr sym (BaseBVType 64)
z3 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s3
     SymExpr sym (BaseBVType 64)
z4 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s4
     SymExpr sym (BaseBVType 64)
z5 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s5
     SymExpr sym (BaseBVType 64)
z6 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s6
     SymExpr sym (BaseBVType 64)
z7 <- Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
s7
     forall sym (flds :: Ctx BaseType).
IsExprBuilder sym =>
sym -> Assignment (SymExpr sym) flds -> IO (SymStruct sym flds)
W4.mkStruct (forall sym. What4 sym -> sym
w4 What4 sym
sym) (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z0 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z1 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z2 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z3 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z4 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z5 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z6 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
z7)
 where lit :: Word64 -> IO (SymExpr sym (BaseBVType 64))
lit Word64
w = forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W4.bvLit (forall sym. What4 sym -> sym
w4 What4 sym
sym) (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @64) (Word64 -> BV 64
BV.word64 Word64
w)

processSHA256Block :: W4.IsSymExprBuilder sym =>
  What4 sym ->
  W4.SymExpr sym (W4.BaseStructType SHA256State) ->
  Value sym ->
  SEval (What4 sym) (W4.SymExpr sym (W4.BaseStructType SHA256State))
processSHA256Block :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA256State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA256State))
processSHA256Block What4 sym
sym SymExpr sym (BaseStructType SHA256State)
st Value sym
blk =
  do let ss :: SeqMap (What4 sym) (Value sym)
ss = forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq Value sym
blk
     SymExpr sym (BaseBVType 32)
b0  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
0
     SymExpr sym (BaseBVType 32)
b1  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
1
     SymExpr sym (BaseBVType 32)
b2  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
2
     SymExpr sym (BaseBVType 32)
b3  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
3
     SymExpr sym (BaseBVType 32)
b4  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
4
     SymExpr sym (BaseBVType 32)
b5  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
5
     SymExpr sym (BaseBVType 32)
b6  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
6
     SymExpr sym (BaseBVType 32)
b7  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
7
     SymExpr sym (BaseBVType 32)
b8  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
8
     SymExpr sym (BaseBVType 32)
b9  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
9
     SymExpr sym (BaseBVType 32)
b10 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
10
     SymExpr sym (BaseBVType 32)
b11 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
11
     SymExpr sym (BaseBVType 32)
b12 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
12
     SymExpr sym (BaseBVType 32)
b13 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
13
     SymExpr sym (BaseBVType 32)
b14 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
14
     SymExpr sym (BaseBVType 32)
b15 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
"processSHA256Block" SeqMap (What4 sym) (Value sym)
ss Integer
15
     let args :: Assignment
  (SymExpr sym)
  (((((((((((((((((EmptyCtx ::> BaseStructType SHA256State)
                  ::> BaseBVType 32)
                 ::> BaseBVType 32)
                ::> BaseBVType 32)
               ::> BaseBVType 32)
              ::> BaseBVType 32)
             ::> BaseBVType 32)
            ::> BaseBVType 32)
           ::> BaseBVType 32)
          ::> BaseBVType 32)
         ::> BaseBVType 32)
        ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32)
     ::> BaseBVType 32)
    ::> BaseBVType 32)
   ::> BaseBVType 32)
args = forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseStructType SHA256State)
st  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
                  SymExpr sym (BaseBVType 32)
b0  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b1  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b2  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b3 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
                  SymExpr sym (BaseBVType 32)
b4  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b5  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b6  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b7 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
                  SymExpr sym (BaseBVType 32)
b8  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b9  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b10 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b11 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
                  SymExpr sym (BaseBVType 32)
b12 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b13 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b14 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
b15
     let ret :: BaseTypeRepr (BaseStructType SHA256State)
ret = forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym (BaseStructType SHA256State)
st
     SymFn
  sym
  (((((((((((((((((EmptyCtx ::> BaseStructType SHA256State)
                  ::> BaseBVType 32)
                 ::> BaseBVType 32)
                ::> BaseBVType 32)
               ::> BaseBVType 32)
              ::> BaseBVType 32)
             ::> BaseBVType 32)
            ::> BaseBVType 32)
           ::> BaseBVType 32)
          ::> BaseBVType 32)
         ::> BaseBVType 32)
        ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32)
     ::> BaseBVType 32)
    ::> BaseBVType 32)
   ::> BaseBVType 32)
  (BaseStructType SHA256State)
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"processSHA256Block" (forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Assignment
  (SymExpr sym)
  (((((((((((((((((EmptyCtx ::> BaseStructType SHA256State)
                  ::> BaseBVType 32)
                 ::> BaseBVType 32)
                ::> BaseBVType 32)
               ::> BaseBVType 32)
              ::> BaseBVType 32)
             ::> BaseBVType 32)
            ::> BaseBVType 32)
           ::> BaseBVType 32)
          ::> BaseBVType 32)
         ::> BaseBVType 32)
        ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32)
     ::> BaseBVType 32)
    ::> BaseBVType 32)
   ::> BaseBVType 32)
args) BaseTypeRepr (BaseStructType SHA256State)
ret
     forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
  sym
  (((((((((((((((((EmptyCtx ::> BaseStructType SHA256State)
                  ::> BaseBVType 32)
                 ::> BaseBVType 32)
                ::> BaseBVType 32)
               ::> BaseBVType 32)
              ::> BaseBVType 32)
             ::> BaseBVType 32)
            ::> BaseBVType 32)
           ::> BaseBVType 32)
          ::> BaseBVType 32)
         ::> BaseBVType 32)
        ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32)
     ::> BaseBVType 32)
    ::> BaseBVType 32)
   ::> BaseBVType 32)
  (BaseStructType SHA256State)
fn Assignment
  (SymExpr sym)
  (((((((((((((((((EmptyCtx ::> BaseStructType SHA256State)
                  ::> BaseBVType 32)
                 ::> BaseBVType 32)
                ::> BaseBVType 32)
               ::> BaseBVType 32)
              ::> BaseBVType 32)
             ::> BaseBVType 32)
            ::> BaseBVType 32)
           ::> BaseBVType 32)
          ::> BaseBVType 32)
         ::> BaseBVType 32)
        ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32)
     ::> BaseBVType 32)
    ::> BaseBVType 32)
   ::> BaseBVType 32)
args


processSHA512Block :: W4.IsSymExprBuilder sym =>
  What4 sym ->
  W4.SymExpr sym (W4.BaseStructType SHA512State) ->
  Value sym ->
  SEval (What4 sym) (W4.SymExpr sym (W4.BaseStructType SHA512State))
processSHA512Block :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> SymExpr sym (BaseStructType SHA512State)
-> Value sym
-> SEval (What4 sym) (SymExpr sym (BaseStructType SHA512State))
processSHA512Block What4 sym
sym SymExpr sym (BaseStructType SHA512State)
st Value sym
blk =
  do let ss :: SeqMap (What4 sym) (Value sym)
ss = forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq Value sym
blk
     SymExpr sym (BaseBVType 64)
b0  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
0
     SymExpr sym (BaseBVType 64)
b1  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
1
     SymExpr sym (BaseBVType 64)
b2  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
2
     SymExpr sym (BaseBVType 64)
b3  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
3
     SymExpr sym (BaseBVType 64)
b4  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
4
     SymExpr sym (BaseBVType 64)
b5  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
5
     SymExpr sym (BaseBVType 64)
b6  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
6
     SymExpr sym (BaseBVType 64)
b7  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
7
     SymExpr sym (BaseBVType 64)
b8  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
8
     SymExpr sym (BaseBVType 64)
b9  <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
9
     SymExpr sym (BaseBVType 64)
b10 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
10
     SymExpr sym (BaseBVType 64)
b11 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
11
     SymExpr sym (BaseBVType 64)
b12 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
12
     SymExpr sym (BaseBVType 64)
b13 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
13
     SymExpr sym (BaseBVType 64)
b14 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
14
     SymExpr sym (BaseBVType 64)
b15 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
"processSHA512Block" SeqMap (What4 sym) (Value sym)
ss Integer
15
     let args :: Assignment
  (SymExpr sym)
  (((((((((((((((((EmptyCtx ::> BaseStructType SHA512State)
                  ::> BaseBVType 64)
                 ::> BaseBVType 64)
                ::> BaseBVType 64)
               ::> BaseBVType 64)
              ::> BaseBVType 64)
             ::> BaseBVType 64)
            ::> BaseBVType 64)
           ::> BaseBVType 64)
          ::> BaseBVType 64)
         ::> BaseBVType 64)
        ::> BaseBVType 64)
       ::> BaseBVType 64)
      ::> BaseBVType 64)
     ::> BaseBVType 64)
    ::> BaseBVType 64)
   ::> BaseBVType 64)
args = forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseStructType SHA512State)
st  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
                  SymExpr sym (BaseBVType 64)
b0  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b1  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b2  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b3 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
                  SymExpr sym (BaseBVType 64)
b4  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b5  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b6  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b7 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
                  SymExpr sym (BaseBVType 64)
b8  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b9  forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b10 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b11 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:>
                  SymExpr sym (BaseBVType 64)
b12 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b13 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b14 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 64)
b15
     let ret :: BaseTypeRepr (BaseStructType SHA512State)
ret = forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType SymExpr sym (BaseStructType SHA512State)
st
     SymFn
  sym
  (((((((((((((((((EmptyCtx ::> BaseStructType SHA512State)
                  ::> BaseBVType 64)
                 ::> BaseBVType 64)
                ::> BaseBVType 64)
               ::> BaseBVType 64)
              ::> BaseBVType 64)
             ::> BaseBVType 64)
            ::> BaseBVType 64)
           ::> BaseBVType 64)
          ::> BaseBVType 64)
         ::> BaseBVType 64)
        ::> BaseBVType 64)
       ::> BaseBVType 64)
      ::> BaseBVType 64)
     ::> BaseBVType 64)
    ::> BaseBVType 64)
   ::> BaseBVType 64)
  (BaseStructType SHA512State)
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
"processSHA512Block" (forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) (g :: k -> *).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
fmapFC forall (e :: BaseType -> *) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W4.exprType Assignment
  (SymExpr sym)
  (((((((((((((((((EmptyCtx ::> BaseStructType SHA512State)
                  ::> BaseBVType 64)
                 ::> BaseBVType 64)
                ::> BaseBVType 64)
               ::> BaseBVType 64)
              ::> BaseBVType 64)
             ::> BaseBVType 64)
            ::> BaseBVType 64)
           ::> BaseBVType 64)
          ::> BaseBVType 64)
         ::> BaseBVType 64)
        ::> BaseBVType 64)
       ::> BaseBVType 64)
      ::> BaseBVType 64)
     ::> BaseBVType 64)
    ::> BaseBVType 64)
   ::> BaseBVType 64)
args) BaseTypeRepr (BaseStructType SHA512State)
ret
     forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
  sym
  (((((((((((((((((EmptyCtx ::> BaseStructType SHA512State)
                  ::> BaseBVType 64)
                 ::> BaseBVType 64)
                ::> BaseBVType 64)
               ::> BaseBVType 64)
              ::> BaseBVType 64)
             ::> BaseBVType 64)
            ::> BaseBVType 64)
           ::> BaseBVType 64)
          ::> BaseBVType 64)
         ::> BaseBVType 64)
        ::> BaseBVType 64)
       ::> BaseBVType 64)
      ::> BaseBVType 64)
     ::> BaseBVType 64)
    ::> BaseBVType 64)
   ::> BaseBVType 64)
  (BaseStructType SHA512State)
fn Assignment
  (SymExpr sym)
  (((((((((((((((((EmptyCtx ::> BaseStructType SHA512State)
                  ::> BaseBVType 64)
                 ::> BaseBVType 64)
                ::> BaseBVType 64)
               ::> BaseBVType 64)
              ::> BaseBVType 64)
             ::> BaseBVType 64)
            ::> BaseBVType 64)
           ::> BaseBVType 64)
          ::> BaseBVType 64)
         ::> BaseBVType 64)
        ::> BaseBVType 64)
       ::> BaseBVType 64)
      ::> BaseBVType 64)
     ::> BaseBVType 64)
    ::> BaseBVType 64)
   ::> BaseBVType 64)
args


addUninterpWarning :: MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning :: forall (m :: * -> *) sym. MonadIO m => What4 sym -> Text -> m ()
addUninterpWarning What4 sym
sym Text
nm = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a. MVar a -> (a -> IO a) -> IO ()
modifyMVar_ (forall sym. What4 sym -> MVar (Set Text)
w4uninterpWarns What4 sym
sym) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => a -> Set a -> Set a
Set.insert Text
nm))

-- | Retrieve the named uninterpreted function, with the given argument types and
--   return type, from a cache.  Create a fresh function if it has not previously
--   been requested.  A particular named function is required to be used with
--   consistent types every time it is requested; otherwise this function will panic.
getUninterpFn :: W4.IsSymExprBuilder sym =>
  What4 sym ->
  Text {- ^ Function name -} ->
  Assignment W4.BaseTypeRepr args {- ^ function argument types -} ->
  W4.BaseTypeRepr ret {- ^ function return type -} ->
  IO (W4.SymFn sym args ret)
getUninterpFn :: forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
funNm Assignment BaseTypeRepr args
args BaseTypeRepr ret
ret =
  forall a b. MVar a -> (a -> IO (a, b)) -> IO b
modifyMVar (forall sym. What4 sym -> MVar (What4FunCache sym)
w4funs What4 sym
sym) forall a b. (a -> b) -> a -> b
$ \What4FunCache sym
m ->
    case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
funNm What4FunCache sym
m of
      Maybe (SomeSymFn sym)
Nothing ->
        do SymFn sym args ret
fn <- forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SolverSymbol
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
W4.freshTotalUninterpFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) (String -> SolverSymbol
W4.safeSymbol (Text -> String
Text.unpack Text
funNm)) Assignment BaseTypeRepr args
args BaseTypeRepr ret
ret
           let m' :: What4FunCache sym
m' = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Text
funNm (forall sym (args :: Ctx BaseType) (ret :: BaseType).
SymFn sym args ret -> SomeSymFn sym
SomeSymFn SymFn sym args ret
fn) What4FunCache sym
m
           forall (m :: * -> *) a. Monad m => a -> m a
return (What4FunCache sym
m', SymFn sym args ret
fn)

      Just (SomeSymFn SymFn sym args ret
fn)
        | Just args :~: args
W4.Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality Assignment BaseTypeRepr args
args (forall (fn :: Ctx BaseType -> BaseType -> *) (args :: Ctx BaseType)
       (ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
W4.fnArgTypes SymFn sym args ret
fn)
        , Just ret :~: ret
W4.Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality BaseTypeRepr ret
ret (forall (fn :: Ctx BaseType -> BaseType -> *) (args :: Ctx BaseType)
       (ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
W4.fnReturnType SymFn sym args ret
fn)
        -> forall (m :: * -> *) a. Monad m => a -> m a
return (What4FunCache sym
m, SymFn sym args ret
fn)

        | Bool
otherwise -> forall a. HasCallStack => String -> [String] -> a
panic String
"getUninterpFn"
                           [ String
"Function" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Text
funNm forall a. [a] -> [a] -> [a]
++ String
"used at incompatible types"
                           , String
"Created with types:"
                           , forall a. Show a => a -> String
show (forall (fn :: Ctx BaseType -> BaseType -> *) (args :: Ctx BaseType)
       (ret :: BaseType).
IsSymFn fn =>
fn args ret -> Assignment BaseTypeRepr args
W4.fnArgTypes SymFn sym args ret
fn) forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (fn :: Ctx BaseType -> BaseType -> *) (args :: Ctx BaseType)
       (ret :: BaseType).
IsSymFn fn =>
fn args ret -> BaseTypeRepr ret
W4.fnReturnType SymFn sym args ret
fn)
                           , String
"Requested at types:"
                           , forall a. Show a => a -> String
show Assignment BaseTypeRepr args
args forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BaseTypeRepr ret
ret
                           ]

toWord32 :: W4.IsSymExprBuilder sym =>
  What4 sym -> String -> SeqMap (What4 sym) (GenValue (What4 sym)) -> Integer -> SEval (What4 sym) (W4.SymBV sym 32)
toWord32 :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
nm SeqMap (What4 sym) (GenValue (What4 sym))
ss Integer
i =
  do SWord sym
x <- forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord What4 sym
sym String
nm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
ss Integer
i
     case SWord sym
x of
       SW.DBV SymBV sym w
x' | Just w :~: 32
W4.Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth SymBV sym w
x') (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @32) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SymBV sym w
x'
       SWord sym
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
nm [String
"Unexpected word size", forall a. Show a => a -> String
show (forall sym. SWord sym -> Integer
SW.bvWidth SWord sym
x)]

fromWord32 :: W4.IsSymExprBuilder sym => W4.SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 :: forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
32 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. SWord sym -> WordValue sym
wordVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
SW.DBV

toWord64 :: W4.IsSymExprBuilder sym =>
  What4 sym -> String -> SeqMap (What4 sym) (GenValue (What4 sym)) -> Integer -> SEval (What4 sym) (W4.SymBV sym 64)
toWord64 :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 64)
toWord64 What4 sym
sym String
nm SeqMap (What4 sym) (GenValue (What4 sym))
ss Integer
i =
  do SWord sym
x <- forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord What4 sym
sym String
nm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
ss Integer
i
     case SWord sym
x of
       SW.DBV SymBV sym w
x' | Just w :~: 64
W4.Refl <- forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
W4.testEquality (forall (e :: BaseType -> *) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W4.bvWidth SymBV sym w
x') (forall (n :: Natural). KnownNat n => NatRepr n
W4.knownNat @64) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SymBV sym w
x'
       SWord sym
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
nm [String
"Unexpected word size", forall a. Show a => a -> String
show (forall sym. SWord sym -> Integer
SW.bvWidth SWord sym
x)]

fromWord64 :: W4.IsSymExprBuilder sym => W4.SymBV sym 64 -> SEval (What4 sym) (Value sym)
fromWord64 :: forall sym.
IsSymExprBuilder sym =>
SymBV sym 64 -> SEval (What4 sym) (Value sym)
fromWord64 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. Integer -> WordValue sym -> GenValue sym
VWord Integer
64 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym. SWord sym -> WordValue sym
wordVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
SW.DBV



-- | Apply the named uninterpreted function to a sequence of @[4][32]@ values,
--   and return a sequence of @[4][32]@ values.  This shape of function is used
--   for most of the SuiteB AES primitives.
applyAESStateFunc :: forall sym. W4.IsSymExprBuilder sym =>
  What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc :: forall sym.
IsSymExprBuilder sym =>
What4 sym -> Text -> Value sym -> SEval (What4 sym) (Value sym)
applyAESStateFunc What4 sym
sym Text
funNm Value sym
x =
  do let ss :: SeqMap (What4 sym) (Value sym)
ss = forall sym. GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq Value sym
x
     SymExpr sym (BaseBVType 32)
w0 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
nm SeqMap (What4 sym) (Value sym)
ss Integer
0
     SymExpr sym (BaseBVType 32)
w1 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
nm SeqMap (What4 sym) (Value sym)
ss Integer
1
     SymExpr sym (BaseBVType 32)
w2 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
nm SeqMap (What4 sym) (Value sym)
ss Integer
2
     SymExpr sym (BaseBVType 32)
w3 <- forall sym.
IsSymExprBuilder sym =>
What4 sym
-> String
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Integer
-> SEval (What4 sym) (SymBV sym 32)
toWord32 What4 sym
sym String
nm SeqMap (What4 sym) (Value sym)
ss Integer
3
     SymFn
  sym
  ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
    ::> BaseBVType 32)
   ::> BaseBVType 32)
  ('BaseStructType
     ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32))
fn <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
What4 sym
-> Text
-> Assignment BaseTypeRepr args
-> BaseTypeRepr ret
-> IO (SymFn sym args ret)
getUninterpFn What4 sym
sym Text
funNm Assignment
  BaseTypeRepr
  ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
    ::> BaseBVType 32)
   ::> BaseBVType 32)
argCtx (forall (ctx :: Ctx BaseType).
Assignment BaseTypeRepr ctx -> BaseTypeRepr ('BaseStructType ctx)
W4.BaseStructRepr Assignment
  BaseTypeRepr
  ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
    ::> BaseBVType 32)
   ::> BaseBVType 32)
argCtx)
     SymExpr
  sym
  ('BaseStructType
     ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32))
z  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym (args :: Ctx BaseType) (ret :: BaseType).
IsSymExprBuilder sym =>
sym
-> SymFn sym args ret
-> Assignment (SymExpr sym) args
-> IO (SymExpr sym ret)
W4.applySymFn (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymFn
  sym
  ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
    ::> BaseBVType 32)
   ::> BaseBVType 32)
  ('BaseStructType
     ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32))
fn (forall {k} (ctx :: Ctx k) (f :: k -> *).
(ctx ~ EmptyCtx) =>
Assignment f ctx
Empty forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
w0 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
w1 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
w2 forall {k} (ctx' :: Ctx k) (f :: k -> *) (ctx :: Ctx k) (tp :: k).
(ctx' ~ (ctx ::> tp)) =>
Assignment f ctx -> f tp -> Assignment f ctx'
:> SymExpr sym (BaseBVType 32)
w3)
     forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall sym. Integer -> SeqMap sym (GenValue sym) -> GenValue sym
VSeq Integer
4 forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap \Integer
i ->
       if | Integer
i forall a. Eq a => a -> a -> Bool
== Integer
0 -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr
  sym
  ('BaseStructType
     ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32))
z (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @0))
          | Integer
i forall a. Eq a => a -> a -> Bool
== Integer
1 -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr
  sym
  ('BaseStructType
     ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32))
z (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @1))
          | Integer
i forall a. Eq a => a -> a -> Bool
== Integer
2 -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr
  sym
  ('BaseStructType
     ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32))
z (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @2))
          | Integer
i forall a. Eq a => a -> a -> Bool
== Integer
3 -> forall sym.
IsSymExprBuilder sym =>
SymBV sym 32 -> SEval (What4 sym) (Value sym)
fromWord32 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym (flds :: Ctx BaseType) (tp :: BaseType).
IsExprBuilder sym =>
sym -> SymStruct sym flds -> Index flds tp -> IO (SymExpr sym tp)
W4.structField (forall sym. What4 sym -> sym
w4 What4 sym
sym) SymExpr
  sym
  ('BaseStructType
     ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
       ::> BaseBVType 32)
      ::> BaseBVType 32))
z (forall {k} (n :: Natural) (ctx :: Ctx k) (r :: k).
Idx n ctx r =>
Index ctx r
natIndex @3))
          | Bool
otherwise -> forall a. String -> [String] -> a
evalPanic String
"applyAESStateFunc" [String
"Index out of range", forall a. Show a => a -> String
show Text
funNm, forall a. Show a => a -> String
show Integer
i]

 where
   nm :: String
nm = Text -> String
Text.unpack Text
funNm

   argCtx :: Assignment W4.BaseTypeRepr
                 (EmptyCtx ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32 ::> W4.BaseBVType 32)
   argCtx :: Assignment
  BaseTypeRepr
  ((((EmptyCtx ::> BaseBVType 32) ::> BaseBVType 32)
    ::> BaseBVType 32)
   ::> BaseBVType 32)
argCtx = forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
W4.knownRepr


indexFront_int ::
  W4.IsSymExprBuilder sym =>
  What4 sym ->
  Nat' ->
  TValue ->
  SeqMap (What4 sym) (GenValue (What4 sym)) ->
  TValue ->
  SInteger (What4 sym) ->
  SEval (What4 sym) (Value sym)
indexFront_int :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> SInteger (What4 sym)
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_int What4 sym
sym Nat'
mblen TValue
_a SeqMap (What4 sym) (GenValue (What4 sym))
xs TValue
_ix SInteger (What4 sym)
idx
  | Just Integer
i <- forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SInteger (What4 sym)
idx
  = forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
i

  | (Integer
lo, Just Integer
hi) <- (Integer, Maybe Integer)
bounds
  = case forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer
-> Maybe (W4Eval sym (GenValue (What4 sym)))
-> Maybe (W4Eval sym (GenValue (What4 sym)))
f forall a. Maybe a
Nothing [Integer
lo .. Integer
hi] of
      Maybe (W4Eval sym (GenValue (What4 sym)))
Nothing -> forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError What4 sym
sym (Maybe Integer -> EvalError
InvalidIndex forall a. Maybe a
Nothing)
      Just W4Eval sym (GenValue (What4 sym))
m  -> W4Eval sym (GenValue (What4 sym))
m

  | Bool
otherwise
  = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall a e. Exception e => e -> a
X.throw (String -> Unsupported
UnsupportedSymbolicOp String
"unbounded integer indexing"))

 where
    w4sym :: sym
w4sym = forall sym. What4 sym -> sym
w4 What4 sym
sym

    f :: Integer
-> Maybe (W4Eval sym (GenValue (What4 sym)))
-> Maybe (W4Eval sym (GenValue (What4 sym)))
f Integer
n (Just W4Eval sym (GenValue (What4 sym))
y) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
       do SymExpr sym BaseBoolType
p <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall sym.
IsExprBuilder sym =>
sym -> SymInteger sym -> SymInteger sym -> IO (Pred sym)
W4.intEq sym
w4sym SInteger (What4 sym)
idx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W4.intLit sym
w4sym Integer
n)
          forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
p (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
n) W4Eval sym (GenValue (What4 sym))
y
    f Integer
n Maybe (W4Eval sym (GenValue (What4 sym)))
Nothing = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
n

    bounds :: (Integer, Maybe Integer)
bounds =
      (case forall tp. ValueRange tp -> ValueBound tp
W4.rangeLowBound (forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> ValueRange Integer
W4.integerBounds SInteger (What4 sym)
idx) of
        W4.Inclusive Integer
l -> forall a. Ord a => a -> a -> a
max Integer
l Integer
0
        ValueBound Integer
_ -> Integer
0
      , case (Maybe Integer
maxIdx, forall tp. ValueRange tp -> ValueBound tp
W4.rangeHiBound (forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> ValueRange Integer
W4.integerBounds SInteger (What4 sym)
idx)) of
          (Just Integer
n, W4.Inclusive Integer
h) -> forall a. a -> Maybe a
Just (forall a. Ord a => a -> a -> a
min Integer
n Integer
h)
          (Just Integer
n, ValueBound Integer
_)              -> forall a. a -> Maybe a
Just Integer
n
          (Maybe Integer, ValueBound Integer)
_                        -> forall a. Maybe a
Nothing
      )

    -- Maximum possible in-bounds index given the length
    -- of the sequence. If the sequence is infinite, there
    -- isn't much we can do.
    maxIdx :: Maybe Integer
maxIdx =
      case Nat'
mblen of
        Nat Integer
n -> forall a. a -> Maybe a
Just (Integer
n forall a. Num a => a -> a -> a
- Integer
1)
        Nat'
Inf   -> forall a. Maybe a
Nothing
indexFront_segs ::
  W4.IsSymExprBuilder sym =>
  What4 sym ->
  Nat' ->
  TValue ->
  SeqMap (What4 sym) (GenValue (What4 sym)) ->
  TValue ->
  Integer ->
  [IndexSegment (What4 sym)] ->
  SEval (What4 sym) (Value sym)
indexFront_segs :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> TValue
-> Integer
-> [IndexSegment (What4 sym)]
-> SEval (What4 sym) (GenValue (What4 sym))
indexFront_segs What4 sym
sym Nat'
mblen TValue
_a SeqMap (What4 sym) (GenValue (What4 sym))
xs TValue
_ix Integer
_idx_bits [WordIndexSegment SWord (What4 sym)
idx]
  | Just Integer
i <- forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
SW.bvAsUnsignedInteger SWord (What4 sym)
idx
  = forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
i

  | Bool
otherwise
  = case forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Integer
-> Maybe (W4Eval sym (GenValue (What4 sym)))
-> Maybe (W4Eval sym (GenValue (What4 sym)))
f forall a. Maybe a
Nothing [Integer]
idxs of
      Maybe (W4Eval sym (GenValue (What4 sym)))
Nothing -> forall sym a. Backend sym => sym -> EvalError -> SEval sym a
raiseError What4 sym
sym (Maybe Integer -> EvalError
InvalidIndex forall a. Maybe a
Nothing)
      Just W4Eval sym (GenValue (What4 sym))
m  -> W4Eval sym (GenValue (What4 sym))
m

 where
    w4sym :: sym
w4sym = forall sym. What4 sym -> sym
w4 What4 sym
sym

    w :: Integer
w = forall sym. SWord sym -> Integer
SW.bvWidth SWord (What4 sym)
idx

    f :: Integer
-> Maybe (W4Eval sym (GenValue (What4 sym)))
-> Maybe (W4Eval sym (GenValue (What4 sym)))
f Integer
n (Just W4Eval sym (GenValue (What4 sym))
y) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
       do SymExpr sym BaseBoolType
p <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (PredBin
SW.bvEq sym
w4sym SWord (What4 sym)
idx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
SW.bvLit sym
w4sym Integer
w Integer
n)
          forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
p (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
n) W4Eval sym (GenValue (What4 sym))
y
    f Integer
n Maybe (W4Eval sym (GenValue (What4 sym)))
Nothing = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
n

    -- maximum possible in-bounds index given the bitwidth
    -- of the index value and the length of the sequence
    maxIdx :: Integer
maxIdx =
      case Nat'
mblen of
        Nat Integer
n | Integer
n forall a. Ord a => a -> a -> Bool
< Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
w -> Integer
nforall a. Num a => a -> a -> a
-Integer
1
        Nat'
_ -> Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^Integer
w forall a. Num a => a -> a -> a
- Integer
1

    -- concrete indices to consider, intersection of the
    -- range of values the index value might take with
    -- the legal values
    idxs :: [Integer]
idxs =
      case forall sym.
IsExprBuilder sym =>
SWord sym -> Maybe (Integer, Integer)
SW.unsignedBVBounds SWord (What4 sym)
idx of
        Just (Integer
lo, Integer
hi) -> [Integer
lo .. forall a. Ord a => a -> a -> a
min Integer
hi Integer
maxIdx]
        Maybe (Integer, Integer)
_ -> [Integer
0 .. Integer
maxIdx]

indexFront_segs What4 sym
sym Nat'
mblen TValue
_a SeqMap (What4 sym) (GenValue (What4 sym))
xs TValue
_ix Integer
idx_bits [IndexSegment (What4 sym)]
segs =
  do SeqMap (What4 sym) (GenValue (What4 sym))
xs' <- forall sym a.
Backend sym =>
sym
-> (SBit sym -> a -> a -> SEval sym a)
-> (SeqMap sym a -> Integer -> SEval sym (SeqMap sym a))
-> Nat'
-> SeqMap sym a
-> Integer
-> [IndexSegment sym]
-> SEval sym (SeqMap sym a)
barrelShifter What4 sym
sym (forall sym.
Backend sym =>
sym
-> SBit sym
-> GenValue sym
-> GenValue sym
-> SEval sym (GenValue sym)
mergeValue What4 sym
sym) forall {sym} {sym} {f :: * -> *} {a}.
(SEval sym ~ SEval sym, Backend sym, Applicative f) =>
SeqMap sym a -> Integer -> f (SeqMap sym a)
shiftOp Nat'
mblen SeqMap (What4 sym) (GenValue (What4 sym))
xs Integer
idx_bits [IndexSegment (What4 sym)]
segs
     forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
xs' Integer
0
  where
    shiftOp :: SeqMap sym a -> Integer -> f (SeqMap sym a)
shiftOp SeqMap sym a
vs Integer
amt = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap (\Integer
i -> forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap sym a
vs forall a b. (a -> b) -> a -> b
$! Integer
amtforall a. Num a => a -> a -> a
+Integer
i))


updateFrontSym ::
  W4.IsSymExprBuilder sym =>
  What4 sym ->
  Nat' ->
  TValue ->
  SeqMap (What4 sym) (GenValue (What4 sym)) ->
  Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
  SEval (What4 sym) (Value sym) ->
  SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateFrontSym :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateFrontSym What4 sym
sym Nat'
_len TValue
_eltTy SeqMap (What4 sym) (GenValue (What4 sym))
vs (Left SInteger (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
  case forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SInteger (What4 sym)
idx of
    Just Integer
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a.
SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
i SEval (What4 sym) (GenValue (What4 sym))
val
    Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
      do SymExpr sym BaseBoolType
b <- forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq What4 sym
sym SInteger (What4 sym)
idx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym Integer
i
         forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
b SEval (What4 sym) (GenValue (What4 sym))
val (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
i)

updateFrontSym What4 sym
sym Nat'
len TValue
_eltTy SeqMap (What4 sym) (GenValue (What4 sym))
vs (Right WordValue (What4 sym)
wv) SEval (What4 sym) (GenValue (What4 sym))
val =
  forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit What4 sym
sym WordValue (What4 sym)
wv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Integer
j -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a.
SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
j SEval (What4 sym) (GenValue (What4 sym))
val
    Maybe Integer
Nothing ->
      forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap What4 sym
sym Nat'
len forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
      do SymExpr sym BaseBoolType
b <- forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
wordValueEqualsInteger What4 sym
sym WordValue (What4 sym)
wv Integer
i
         forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
b SEval (What4 sym) (GenValue (What4 sym))
val (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
i)

updateBackSym ::
  W4.IsSymExprBuilder sym =>
  What4 sym ->
  Nat' ->
  TValue ->
  SeqMap (What4 sym) (GenValue (What4 sym)) ->
  Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
  SEval (What4 sym) (Value sym) ->
  SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateBackSym :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> SeqMap (What4 sym) (GenValue (What4 sym))
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (SeqMap (What4 sym) (GenValue (What4 sym)))
updateBackSym What4 sym
_ Nat'
Inf TValue
_ SeqMap (What4 sym) (GenValue (What4 sym))
_ Either (SInteger (What4 sym)) (WordValue (What4 sym))
_ SEval (What4 sym) (GenValue (What4 sym))
_ = forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"updateBackSym"]

updateBackSym What4 sym
sym (Nat Integer
n) TValue
_eltTy SeqMap (What4 sym) (GenValue (What4 sym))
vs (Left SInteger (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
  case forall (e :: BaseType -> *).
IsExpr e =>
e BaseIntegerType -> Maybe Integer
W4.asInteger SInteger (What4 sym)
idx of
    Just Integer
i -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a.
SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs (Integer
n forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
i) SEval (What4 sym) (GenValue (What4 sym))
val
    Maybe Integer
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
      do SymExpr sym BaseBoolType
b <- forall sym.
Backend sym =>
sym -> SInteger sym -> SInteger sym -> SEval sym (SBit sym)
intEq What4 sym
sym SInteger (What4 sym)
idx forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
Backend sym =>
sym -> Integer -> SEval sym (SInteger sym)
integerLit What4 sym
sym (Integer
n forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
i)
         forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
b SEval (What4 sym) (GenValue (What4 sym))
val (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
i)

updateBackSym What4 sym
sym (Nat Integer
n) TValue
_eltTy SeqMap (What4 sym) (GenValue (What4 sym))
vs (Right WordValue (What4 sym)
wv) SEval (What4 sym) (GenValue (What4 sym))
val =
  forall sym.
Backend sym =>
sym -> WordValue sym -> SEval sym (Maybe Integer)
wordValAsLit What4 sym
sym WordValue (What4 sym)
wv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Integer
j ->
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall sym a.
SeqMap sym a -> Integer -> SEval sym a -> SeqMap sym a
updateSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs (Integer
n forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
j) SEval (What4 sym) (GenValue (What4 sym))
val
    Maybe Integer
Nothing ->
      forall sym a.
Backend sym =>
sym -> Nat' -> SeqMap sym a -> SEval sym (SeqMap sym a)
memoMap What4 sym
sym (Integer -> Nat'
Nat Integer
n) forall a b. (a -> b) -> a -> b
$ forall sym a. (Integer -> SEval sym a) -> SeqMap sym a
indexSeqMap forall a b. (a -> b) -> a -> b
$ \Integer
i ->
      do SymExpr sym BaseBoolType
b <- forall sym.
Backend sym =>
sym -> WordValue sym -> Integer -> SEval sym (SBit sym)
wordValueEqualsInteger What4 sym
sym WordValue (What4 sym)
wv (Integer
n forall a. Num a => a -> a -> a
- Integer
1 forall a. Num a => a -> a -> a
- Integer
i)
         forall sym.
Backend sym =>
sym
-> SBit sym
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
iteValue What4 sym
sym SymExpr sym BaseBoolType
b SEval (What4 sym) (GenValue (What4 sym))
val (forall sym a. Backend sym => SeqMap sym a -> Integer -> SEval sym a
lookupSeqMap SeqMap (What4 sym) (GenValue (What4 sym))
vs Integer
i)


updateFrontSym_word ::
  W4.IsSymExprBuilder sym =>
  What4 sym ->
  Nat' ->
  TValue ->
  WordValue (What4 sym) ->
  Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
  SEval (What4 sym) (GenValue (What4 sym)) ->
  SEval (What4 sym) (WordValue (What4 sym))
updateFrontSym_word :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> WordValue (What4 sym)
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (WordValue (What4 sym))
updateFrontSym_word What4 sym
_ Nat'
Inf TValue
_ WordValue (What4 sym)
_ Either (SInteger (What4 sym)) (WordValue (What4 sym))
_ SEval (What4 sym) (GenValue (What4 sym))
_ = forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"updateFrontSym_word"]

updateFrontSym_word What4 sym
sym (Nat Integer
n) TValue
_eltTy WordValue (What4 sym)
w (Left SInteger (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
  do SWord sym
idx' <- forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
wordFromInt What4 sym
sym Integer
n SInteger (What4 sym)
idx
     forall sym.
Backend sym =>
sym
-> IndexDirection
-> WordValue sym
-> WordValue sym
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordByWord What4 sym
sym IndexDirection
IndexForward WordValue (What4 sym)
w (forall sym. SWord sym -> WordValue sym
wordVal SWord sym
idx') (forall sym. GenValue sym -> SBit sym
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
val)
updateFrontSym_word What4 sym
sym (Nat Integer
_n) TValue
_eltTy WordValue (What4 sym)
w (Right WordValue (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
  forall sym.
Backend sym =>
sym
-> IndexDirection
-> WordValue sym
-> WordValue sym
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordByWord What4 sym
sym IndexDirection
IndexForward WordValue (What4 sym)
w WordValue (What4 sym)
idx (forall sym. GenValue sym -> SBit sym
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
val)


updateBackSym_word ::
  W4.IsSymExprBuilder sym =>
  What4 sym ->
  Nat' ->
  TValue ->
  WordValue (What4 sym) ->
  Either (SInteger (What4 sym)) (WordValue (What4 sym)) ->
  SEval (What4 sym) (GenValue (What4 sym)) ->
  SEval (What4 sym) (WordValue (What4 sym))
updateBackSym_word :: forall sym.
IsSymExprBuilder sym =>
What4 sym
-> Nat'
-> TValue
-> WordValue (What4 sym)
-> Either (SInteger (What4 sym)) (WordValue (What4 sym))
-> SEval (What4 sym) (GenValue (What4 sym))
-> SEval (What4 sym) (WordValue (What4 sym))
updateBackSym_word What4 sym
_ Nat'
Inf TValue
_ WordValue (What4 sym)
_ Either (SInteger (What4 sym)) (WordValue (What4 sym))
_ SEval (What4 sym) (GenValue (What4 sym))
_ = forall a. String -> [String] -> a
evalPanic String
"Expected finite sequence" [String
"updateFrontSym_word"]

updateBackSym_word What4 sym
sym (Nat Integer
n) TValue
_eltTy WordValue (What4 sym)
w (Left SInteger (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
  do SWord sym
idx' <- forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SWord sym)
wordFromInt What4 sym
sym Integer
n SInteger (What4 sym)
idx
     forall sym.
Backend sym =>
sym
-> IndexDirection
-> WordValue sym
-> WordValue sym
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordByWord What4 sym
sym IndexDirection
IndexBackward WordValue (What4 sym)
w (forall sym. SWord sym -> WordValue sym
wordVal SWord sym
idx') (forall sym. GenValue sym -> SBit sym
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
val)
updateBackSym_word What4 sym
sym (Nat Integer
_n) TValue
_eltTy WordValue (What4 sym)
w (Right WordValue (What4 sym)
idx) SEval (What4 sym) (GenValue (What4 sym))
val =
  forall sym.
Backend sym =>
sym
-> IndexDirection
-> WordValue sym
-> WordValue sym
-> SEval sym (SBit sym)
-> SEval sym (WordValue sym)
updateWordByWord What4 sym
sym IndexDirection
IndexBackward WordValue (What4 sym)
w WordValue (What4 sym)
idx (forall sym. GenValue sym -> SBit sym
fromVBit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SEval (What4 sym) (GenValue (What4 sym))
val)