What4.hs

{-# LANGUAGE GADTs, TypeFamilies, ScopedTypeVariables #-}
{-|
Module      : Data.RME.What4
Description : What4 solver adapter for the RME backend.
Copyright   : (c) 2025 Galois
License     : BSD3
Maintainer  : cryptol@galois.com

This module implements a What4 solver adapter that translates What4 expressions
into RME (Reed–Muller expansion) terms and uses the RME backend for
symbolic reasoning.

Reference:
  * https://en.wikipedia.org/wiki/Reed–Muller_expansion

-}
module Data.RME.What4 (rmeAdapter) where

import Control.Monad (replicateM, ap, (<$!>))
import Data.BitVector.Sized qualified as BV
import Data.Foldable (msum)
import Data.IntSet (IntSet)
import Data.IntSet qualified as IntSet
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Parameterized (traverseFC, (::>), Some (..), OrdF (compareF), OrderingF (..), lexCompareF)
import Data.Parameterized.Context (Assignment, pattern Empty, pattern (:>))
import Data.Parameterized.Context qualified as Ctx
import Data.Parameterized.Map (MapF)
import Data.Parameterized.Map qualified as MapF
import Data.Parameterized.NatRepr ( NatRepr(..) )
import Data.Parameterized.Nonce (Nonce)
import Data.RME
import Data.Vector qualified as V
import What4.Expr.App qualified as W4
import What4.Expr.BoolMap qualified as W4
import What4.Expr.Builder qualified as W4
import What4.Expr.GroundEval qualified as W4
import What4.Expr.UnaryBV qualified as UnaryBV
import What4.Expr.WeightedSum qualified as Sum
import What4.Interface qualified as W4
import What4.SatResult qualified as W4
import What4.SemiRing qualified as W4
import What4.Solver

-- | Adapter for @rme@ package based satisfiability checker.
rmeAdapter :: SolverAdapter st
rmeAdapter =
  SolverAdapter
  { solver_adapter_name = "RME"
  , solver_adapter_config_options = []
  , solver_adapter_check_sat = rmeAdapterCheckSat
  , solver_adapter_write_smt2 = \_ _ _ -> pure ()
  }

-- | Satisfiability checker using 'RME' representation.
rmeAdapterCheckSat ::
  forall t st fs a.
  W4.ExprBuilder t st fs ->
  LogData ->
  [W4.BoolExpr t] {- ^ list of assertions -} ->
  (SatResult (W4.GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) ->
  IO a
rmeAdapterCheckSat _ logger asserts k =
 do logCallback logger "Starting RME"
    let m = foldl conj true <$!> traverse evalExpr asserts
    case runM m of
      Left e ->
       do logCallback logger e
          putStrLn e
          k W4.Unknown
      Right (rme, s) ->
        k case cegar rme (uninterps s) of
          Nothing -> Unsat ()
          Just trueVars ->
            W4.Sat (W4.GroundEvalFn (groundEval trueVars (nonceCache s)), Nothing)

-- | Counter-example guided abstraction refinement
--
-- Given an RME term, compute a satisfying assigment for that term.
-- Then check that the satisfying assignment generates
cegar :: RME -> MapF k UninterpFnData -> Maybe IntSet
cegar rme a =
  case sat rme of
    Nothing -> Nothing
    Just model ->
      let trueVars = IntSet.fromList [x | (x, True) <- model] in
      case msum (fmap (findRefinement trueVars) (MapF.elems a)) of
        Nothing -> Just trueVars
        Just refinement -> cegar (conj refinement rme) a

-- | Search for a contradiction in the chosen interpretation of an
-- uninterpreted function. Each of the points at which the function
-- was defined are computed to ground values. If there is a contradiction
-- in the current model for a pair of points, an RME term is returned
-- that should have been true in a valid model.
findRefinement ::
  IntSet {- ^ Variables assigned true in the satisfying model -} ->
  Some UninterpFnData {- ^ Defined points in the function -} ->
  Maybe RME
findRefinement trueVars (Some (UninterpFnData retT points)) = go Map.empty (Map.toList points)
  where
    go _ [] = Nothing
    go seen ((AbstractKey argTs k, v) : rest) =
      case Map.lookup k' seen of
        Nothing -> go seen' rest
        Just (old_k, old_v, old_v')
          | gvwEq retT old_v' v' -> go seen rest
          | otherwise -> Just (makeRefinement argTs old_k k retT old_v v)
        where
          k' = ConcreteKey argTs (Ctx.zipWith (evalR trueVars) argTs k)
          v' = evalR trueVars retT v
          seen' = Map.insert k' (k, v, v') seen

-- | Equality of two ground value terms.
gvwEq :: RMERepr a -> W4.GroundValueWrapper a -> W4.GroundValueWrapper a -> Bool
gvwEq BitRepr (W4.GVW x) (W4.GVW y) = x == y
gvwEq BVRepr{} (W4.GVW x) (W4.GVW y) = x == y
gvwEq IntRepr (W4.GVW x) (W4.GVW y) = x == y 

-- | Literal equality of the symbolic boolean formulas. Two RME values
-- are considered equal when they compute the same expression under all
-- interpretations. Because RME keeps terms in a normal for, we can use
-- derived equality to answer this question.
rmeEq :: RMERepr a -> R' a -> R' a -> Bool
rmeEq BitRepr (R x) (R y) = x == y
rmeEq BVRepr{} (R x) (R y) = x == y
rmeEq IntRepr (R x) (R y) = x == y

data AbstractKey args where
  AbstractKey ::
    Assignment RMERepr args ->
    Assignment R' args ->
    AbstractKey args

instance Eq (AbstractKey args) where
  AbstractKey a b == AbstractKey _ c = go a b c
    where
      go :: Assignment RMERepr a -> Assignment R' a -> Assignment R' a -> Bool
      go Empty Empty Empty = True
      go (ts :> t) (xs :> x) (ys :> y) = rmeEq t x y && go ts xs ys

instance Ord (AbstractKey args) where
  AbstractKey a b `compare` AbstractKey _ c = go a b c
    where
      go :: Assignment RMERepr a -> Assignment R' a -> Assignment R' a -> Ordering
      go Empty Empty Empty = EQ
      go (ts :> t) (xs :> x) (ys :> y) = compareR t x y <> go ts xs ys

      compareR :: RMERepr a -> R' a -> R' a -> Ordering
      compareR BitRepr (R x) (R y) = compare x y
      compareR BVRepr{} (R x) (R y) = compare x y
      compareR IntRepr (R x) (R y) = compare x y

data ConcreteKey args where
  ConcreteKey ::
    Assignment RMERepr args ->
    Assignment W4.GroundValueWrapper args ->
    ConcreteKey args

instance Eq (ConcreteKey args) where
  ConcreteKey a b == ConcreteKey _ c = go a b c
    where
      go :: Assignment RMERepr a -> Assignment W4.GroundValueWrapper a -> Assignment W4.GroundValueWrapper a -> Bool
      go Empty Empty Empty = True
      go (ts :> t) (xs :> x) (ys :> y) = gvwEq t x y && go ts xs ys

instance Ord (ConcreteKey args) where
  ConcreteKey a b `compare` ConcreteKey _ c = go a b c
    where
      go :: Assignment RMERepr a -> Assignment W4.GroundValueWrapper a -> Assignment W4.GroundValueWrapper a -> Ordering
      go Empty Empty Empty = EQ
      go (ts :> t) (xs :> x) (ys :> y) = compareGVW t x y <> go ts xs ys

      compareGVW :: RMERepr a -> W4.GroundValueWrapper a -> W4.GroundValueWrapper a -> Ordering
      compareGVW BitRepr (W4.GVW x) (W4.GVW y) = compare x y
      compareGVW BVRepr{} (W4.GVW x) (W4.GVW y) = compare x y
      compareGVW IntRepr (W4.GVW x) (W4.GVW y) = compare x y

makeRefinement ::
  Assignment RMERepr a -> Assignment R' a -> Assignment R' a ->
  RMERepr r -> R' r -> R' r ->
  RME
makeRefinement Empty Empty Empty rt rx ry = sameR rt rx ry
makeRefinement (ts :> t) (xs :> x) (ys :> y) rt rx ry = sameR t x y ==> makeRefinement ts xs ys rt rx ry
  where
    p ==> q = compl p `disj` q

-- | Computes the symbolic term that is true when the two arguments are equal
sameR :: RMERepr a -> R' a -> R' a -> RME
sameR BitRepr (R l) (R r) = conj l r
sameR BVRepr{} (R l) (R r) = eq l r
sameR IntRepr (R l) (R r) = constant (l == r)

-- | Given a satisfying model, compute the ground value of an RME term.
evalR :: IntSet -> RMERepr a -> R' a -> W4.GroundValueWrapper a
evalR trueVars BitRepr (R x) = W4.GVW (evalRME trueVars x)
evalR trueVars (BVRepr w) (R x) = W4.GVW (bitsToBV w (fmap (evalRME trueVars) x))
evalR _ IntRepr (R x) = W4.GVW x

-- | Evaluate an RME term given the set of true variables.
evalRME :: IntSet -> RME -> Bool
evalRME trueVars x = eval x (`IntSet.member` trueVars)

-- | Ground evaluation function. Given a satisfying assignment (set of true variables)
-- this function will used the cached results to evaluate an expression.
groundEval :: IntSet -> MapF (Nonce t) R' -> W4.Expr t tp -> IO (W4.GroundValue tp)
groundEval trueVars nonces e =
  case (flip MapF.lookup nonces =<< W4.exprMaybeId e, W4.exprType e) of
    (Just (R n), W4.BaseBoolRepr) -> pure $! evalRME trueVars n
    (Just (R n), W4.BaseBVRepr w) -> pure $! bitsToBV w (fmap (evalRME trueVars) n)
    _ -> W4.evalGroundExpr (groundEval trueVars nonces) e

-- | Build a 'BV.BV' from a vector of booleans.
bitsToBV :: NatRepr w -> V.Vector Bool -> BV.BV w
bitsToBV w bs = BV.mkBV w (foldl (\acc x -> if x then 1 + acc*2 else acc*2) 0 bs)

-- | Evaluation is run in a context with a state, an error continuation, and a success continuation.
newtype M t a = M { unM :: forall k. S t -> (String -> k) -> (a -> S t -> k) -> k }

runM :: M t a -> Either String (a, S t)
runM m = unM m emptyS Left (curry Right)

instance Functor (M t) where
  fmap f (M m) = M (\s e k -> m s e (k . f))

instance Applicative (M t) where
  pure x = M (\s _ k -> k x s)
  (<*>) = ap

instance Monad (M t) where
  M m1 >>= f = M (\s0 e t -> m1 s0 e (\a s1 -> unM (f a) s1 e t))

instance MonadFail (M t) where
  fail str = M (\_ e _ -> e str)

-- | Get the current evaluation state
get :: M t (S t)
get = M (\s _ t -> t s s)

-- | Set the current evaluation state
set :: S t -> M t ()
set s = M (\_ _ t -> t () s)

-- | The state of evaluating an 'Expr' into an 'RME' term
data S t = S
  { nextVar :: !Int -- ^ next fresh variable to be used with RME lit
  , nonceCache :: !(MapF (Nonce t) R') -- ^ previously translated w4 expressions
  , uninterps :: !(MapF (FnKey t) UninterpFnData) -- ^ uninterpreted function interpretations
  }

data FnKey t as where
  FnKey    :: Nonce t args -> FnKey t args
  FnArrKey :: Nonce t (args Ctx.::> W4.BaseArrayType i e) -> FnKey t (args Ctx.<+> i Ctx.::> e)

instance W4.TestEquality (FnKey t) where
  testEquality (FnKey x) (FnKey y) = W4.testEquality x y
  testEquality (FnArrKey x) (FnArrKey y) | Just W4.Refl <- W4.testEquality x y = Just W4.Refl
  testEquality _ _ = Nothing

instance OrdF (FnKey t) where
  compareF (FnKey x) (FnKey y) = compareF x y
  compareF (FnArrKey x) (FnArrKey y) = lexCompareF x y EQF
  compareF FnKey{} FnArrKey{} = LTF
  compareF FnArrKey{} FnKey{} = GTF
  
  

-- | Type-information and point-wise definition of an uninterpreted function.
data UninterpFnData tp where
  UninterpFnData ::
    RMERepr ret ->
    Map (AbstractKey args) (R' ret) ->
    UninterpFnData (args ::> ret)

-- | The initial evaluation state
emptyS :: S t
emptyS = S
  { nextVar = 0
  , nonceCache = MapF.empty
  , uninterps = MapF.empty
  }

-- | Produce a fresh RME term
freshRME :: M t RME
freshRME =
 do s <- get
    if nextVar s == maxBound then
      fail "Fresh variables exhausted"
    else do
      set $! s{ nextVar = nextVar s + 1 }
      pure (lit (nextVar s))

-- | Map what4 base types to RME representations
type family R (t :: W4.BaseType) where
  R W4.BaseBoolType = RME
  R (W4.BaseBVType n) = RMEV
  R W4.BaseIntegerType = Integer

-- | Newtype wrapper for the 't:R' type family for use with 'Assignment'
newtype R' tp = R (R tp)

-- | Representation type use to determine which RME representation is being used
data RMERepr (t :: W4.BaseType) where
  -- | A single RME bit
  BitRepr :: RMERepr W4.BaseBoolType
  -- | A vector of w RME bits
  BVRepr  :: !(NatRepr w) -> RMERepr (W4.BaseBVType w)
  -- | An integer
  IntRepr :: RMERepr W4.BaseIntegerType
  
-- | Helper for memoizing evaluation. Given a nonced and a way to evaluation
-- action this will either return the cached value for that nonce or
-- evaluate the given action and store it in the cache before returning it.
cached :: Nonce t tp -> M t (R tp) -> M t (R tp)
cached nonce gen =
 do mb <- fmap (MapF.lookup nonce . nonceCache) get
    case mb of
      Just (R r) -> pure r
      Nothing ->
       do r <- gen
          s <- get
          set $! s{ nonceCache = MapF.insert nonce (R r) (nonceCache s) }
          pure r

-- | A version of what4's SemiRingRepr that matches the semi-rings that this backend supports
data SemiRingRepr sr where
  SemiRingBVRepr :: !(W4.BVFlavorRepr fv) -> !Int -> SemiRingRepr (W4.SemiRingBV fv w)
  SemiRingIntRepr :: SemiRingRepr W4.SemiRingInteger

-- | Converts a BV width into the Int type used by Vector.
-- In the extreme case that the NatRepr is out of range of
-- Int, this operation will fail.
evalWidth :: NatRepr w -> M t Int
evalWidth w =
  let n = natValue w in
  if n > fromIntegral (maxBound :: Int)
    then fail "Bit-vector width too wide!"
    else pure (fromIntegral n)

-- | Convert a generic what4 base type to an RME base-type.
-- Reports an error for unsupported base types.
evalTypeRepr :: W4.BaseTypeRepr tp -> M t (RMERepr tp)
evalTypeRepr = \case
  W4.BaseBoolRepr -> pure BitRepr
  W4.BaseBVRepr w -> pure $! BVRepr w
  W4.BaseIntegerRepr -> pure IntRepr
  r -> fail ("RME does not support " ++ show r)

-- | Convert a generic what4 semiring type to an RME semiring type.
-- Reports an error for unsupported semiring types.
evalSemiRingRepr :: W4.SemiRingRepr sr -> M t (SemiRingRepr sr)
evalSemiRingRepr = \case
      W4.SemiRingIntegerRepr -> pure SemiRingIntRepr
      W4.SemiRingRealRepr -> fail "RME does not support real numbers"
      W4.SemiRingBVRepr flv w ->
       do w' <- evalWidth w
          pure $! SemiRingBVRepr flv w'

-- | Evaluate an expression, if possible, into an RME term.
evalExpr :: W4.Expr t tp -> M t (R tp)
evalExpr = \case
  W4.BoolExpr x _ -> pure $! constant x
  W4.AppExpr x -> cached (W4.appExprId x) (evalApp (W4.appExprApp x))
  W4.BoundVarExpr x -> cached (W4.bvarId x) (allocateVar =<< evalTypeRepr (W4.bvarType x))
  W4.SemiRingLiteral rpr c _ ->
   do rpr' <- evalSemiRingRepr rpr
      pure $! case rpr' of
        SemiRingBVRepr _ w | BV.BV ci <- c -> integer w ci
        SemiRingIntRepr -> c
  W4.FloatExpr{} -> fail "RME does not support floating point numbers"
  W4.StringExpr{} -> fail "RME does not support string literals"
  W4.NonceAppExpr x -> cached (W4.nonceExprId x) (evalNonceApp (W4.nonceExprApp x))

-- | Evaluate a NonceApp expression. In most cases this will result in
-- failure with a message explaining what feature was unsupported.
evalNonceApp :: W4.NonceApp t (W4.Expr t) tp -> M t (R tp)
evalNonceApp = \case
  W4.Annotation _ _ e -> evalExpr e
  W4.Forall{} -> fail "RME does not support 'Forall' quantifiers"
  W4.Exists{} -> fail "RME does not support 'Exists' quantifiers"
  W4.ArrayFromFn{} -> fail "RME does not support 'ArrayFromFn' expressions"
  W4.MapOverArrays{} -> fail "RME does not support 'MapOverArrays' expressions"
  W4.ArrayTrueOnEntries{} -> fail "RME does not support 'ArrayTrueOnEntries' expressions"
  W4.FnApp fn args ->
   do args' <- traverseFC (\x -> R <$> evalExpr x) args
      argTypes <- traverseFC evalTypeRepr (W4.symFnArgTypes fn)
      retType <- evalTypeRepr (W4.symFnReturnType fn)
      let nonce = FnKey (W4.symFnId fn)
      let key = AbstractKey argTypes args'
      mbOldFnData <- fmap (MapF.lookup nonce . uninterps) get

      -- Allocate a new point in the uninterpreted function and add it to the existing ones
      let allocatePoint points =
           do r <- allocateVar =<< evalTypeRepr (W4.symFnReturnType fn)
              s <- get
              let newFnData = UninterpFnData retType (Map.insert key (R r) points)
              set $! s{ uninterps = MapF.insert nonce newFnData (uninterps s) }
              pure r

      case mbOldFnData of
        Just (UninterpFnData _ points) ->
          case Map.lookup key points of
            Just (R ret) -> pure ret
            Nothing -> allocatePoint points
        Nothing -> allocatePoint Map.empty

-- | Allocates an unconstrainted RME term at the given type.
allocateVar :: RMERepr tp -> M t (R tp)
allocateVar = \case
  BitRepr -> freshRME
  BVRepr w ->
   do w' <- evalWidth w
      V.fromList <$!> replicateM w' freshRME
  IntRepr -> fail "RME does not support symbolic Integers"

-- | Convert a what4 App into an RME term for the operations that the
-- RME backend supports.
evalApp :: W4.App (W4.Expr t) tp -> M t (R tp)
evalApp = \case

  W4.BaseEq rpr x y ->
   do x1 <- evalExpr x
      y1 <- evalExpr y
      r <- evalTypeRepr rpr
      pure $! case r of
        BitRepr -> iff x1 y1
        BVRepr{} -> eq x1 y1
        IntRepr -> constant (x1 == y1)

  W4.BaseIte rpr _ b t e ->
   do b1 <- evalExpr b
      t1 <- evalExpr t
      e1 <- evalExpr e
      r <- evalTypeRepr rpr
      case r of
        BitRepr -> pure $! mux b1 t1 e1
        BVRepr{} -> pure $! V.zipWith (mux b1) t1 e1
        IntRepr ->
          if t1 == e1 then pure t1 else fail "Can not mux integers"

  W4.NotPred x ->
   do x1 <- evalExpr x
      pure $! compl x1

  W4.ConjPred c ->
    case W4.viewConjMap c of
      W4.ConjTrue -> pure true
      W4.ConjFalse -> pure false
      W4.Conjuncts y ->
       do let f (x, W4.Positive) = evalExpr x
              f (x, W4.Negative) = compl <$!> evalExpr x
          foldl1 conj <$!> traverse f y

  W4.BVTestBit i ve ->
   do v <- evalExpr ve
      pure $! v V.! (length v - fromIntegral i - 1) -- little-endian index

  W4.BVSlt x y ->
   do x' <- evalExpr x
      y' <- evalExpr y
      pure $! slt x' y'

  W4.BVUlt x y ->
   do x' <- evalExpr x
      y' <- evalExpr y
      pure $! ult x' y'

  W4.BVConcat _ x y ->
   do x' <- evalExpr x
      y' <- evalExpr y
      pure $! x' <> y'

  W4.BVShl _ x y ->
    do x' <- evalExpr x
       y' <- evalExpr y
       pure $! shl x' y'

  W4.BVCountTrailingZeros _ v -> countTrailingZeros <$!> evalExpr v

  W4.BVCountLeadingZeros _ v -> countLeadingZeros <$!> evalExpr v

  W4.BVPopcount _ v -> popcount <$!> evalExpr v

  W4.BVOrBits w s ->
   do vs <- traverse evalExpr (W4.bvOrToList s)
      w' <- evalWidth w
      pure $! foldl (V.zipWith disj) (V.replicate w' false) vs

  W4.BVSelect i n v ->
   do v' <- evalExpr v
      i' <- evalWidth i
      n' <- evalWidth n
      let start = length v' - n' - i' -- i is given as a little endian index
      pure $! V.take n' (V.drop start v')

  W4.BVFill w b ->
   do w' <- evalWidth w
      b' <- evalExpr b
      pure $! V.replicate w' b'

  W4.BVLshr _ x i ->
   do x' <- evalExpr x
      i' <- evalExpr i
      pure $! lshr x' i'

  W4.BVAshr _ x i ->
   do x' <- evalExpr x
      i' <- evalExpr i
      pure $! ashr x' i'

  W4.BVRol _ x i ->
   do x' <- evalExpr x
      i' <- evalExpr i
      pure $! rol x' i'

  W4.BVRor _ x i ->
   do x' <- evalExpr x
      i' <- evalExpr i
      pure $! ror x' i'

  W4.BVZext w v ->
   do v' <- evalExpr v
      w' <- evalWidth w
      let l = w' - length v'
      pure (V.replicate l false <> v')

  W4.BVSext w v ->
   do v' <- evalExpr v
      w' <- evalWidth w
      let l = w' - length v'
      pure (V.replicate l (V.head v') <> v')

  W4.SemiRingSum s ->
   do rpr <- evalSemiRingRepr (Sum.sumRepr s)
      case rpr of
        SemiRingIntRepr ->
          Sum.evalM
            (\x y -> pure $! x + y)
            (\c r ->
             do r' <- evalExpr r
                pure $! c * r')
            (\c   -> pure c)
            s

        SemiRingBVRepr flv w ->
          case flv of
            -- modular addition
            W4.BVArithRepr ->
              Sum.evalM
                (\x y -> pure $! add x y)
                (\(BV.BV c) r ->
                 do v <- evalExpr r
                    pure $! mul v (integer w c))
                (\(BV.BV c) -> pure $! integer w c)
                s

            -- bitwise xor
            W4.BVBitsRepr ->
              Sum.evalM
                (\x y -> pure $! V.zipWith xor x y)
                (\(BV.BV c) r ->
                 do v <- evalExpr r
                    pure $! V.zipWith conj (integer w c) v)
                (\(BV.BV c) -> pure $! integer w c)
                s

  W4.SemiRingProd p ->
   do rpr <- evalSemiRingRepr (Sum.prodRepr p)
      case rpr of
        SemiRingIntRepr ->
         do mb <- Sum.prodEvalM
                  (\x y -> pure $! x * y)
                  evalExpr
                  p
            pure $! case mb of
              Nothing -> 1
              Just r -> r

        SemiRingBVRepr flv w ->
          case flv of
          -- arithmetic multiplication
            W4.BVArithRepr ->
             do mb <- Sum.prodEvalM
                  (\x y -> pure $! mul x y)
                  evalExpr
                  p
                pure $! case mb of
                  Nothing -> integer w 1
                  Just r -> r
    
            -- bitwise conjunction
            W4.BVBitsRepr ->
             do mb <- Sum.prodEvalM
                      (\x y -> pure $! V.zipWith conj x y)
                      evalExpr
                      p
                pure $! case mb of
                  Nothing -> V.replicate w true -- ~0
                  Just r -> r

  W4.BVUdiv _ x y ->
   do x' <- evalExpr x
      y' <- evalExpr y
      pure $! udiv x' y'

  W4.BVUrem _ x y ->
   do x' <- evalExpr x
      y' <- evalExpr y
      pure $! urem x' y'

  W4.BVSdiv _ x y ->
   do x' <- evalExpr x
      y' <- evalExpr y
      pure $! sdiv x' y'

  W4.BVSrem _ x y ->
   do x' <- evalExpr x
      y' <- evalExpr y
      pure $! srem x' y'

  W4.BVUnaryTerm u ->
   do let constEval x =
           do x' <- evalExpr x
              case isBool x' of
                Nothing -> fail "Unary term not constant"
                Just r -> pure r
      w' <- evalWidth (UnaryBV.width u)
      u' <- UnaryBV.evaluate constEval u
      pure $! integer w' u'

  -- This translation allows us to treat uninterpreted functions with the shape:
  --
  --   Args -> Array Indexes Elt
  --
  -- as if they were actually:
  --
  --   Args -> Indexes -> Elt
  --
  -- Expressions of the form @select (FnApp f args) ixs@ are generated
  -- by SAW when it is processing uninterpreted functions in order
  -- to reduce the number of uninterpreted function applications. This means
  -- we never actually need to construct the array itself; we treat it
  -- as though it was just an extension of the uninterpreted function.
  W4.SelectArray retType (W4.NonceAppExpr nae) ixs ->
    case W4.nonceExprApp nae of
      W4.FnApp fn args ->
       do args' <- traverseFC (\x -> R <$> evalExpr x) args
          ixs'  <- traverseFC (\x -> R <$> evalExpr x) ixs
          argTypes <- traverseFC evalTypeRepr (W4.symFnArgTypes fn)
          let indexTypes = W4.arrayTypeIndices (W4.symFnReturnType fn)
          indexTypes' <- traverseFC evalTypeRepr indexTypes
          retType' <- evalTypeRepr retType
          let nonce = FnArrKey (W4.symFnId fn)
          let key = AbstractKey (argTypes Ctx.<++> indexTypes') (args' Ctx.<++> ixs')
          mbOldFnData <- fmap (MapF.lookup nonce . uninterps) get
    
          -- Allocate a new point in the uninterpreted function and add it to the existing ones
          let allocatePoint points =
               do r <- allocateVar retType'
                  s <- get
                  let newFnData = UninterpFnData retType' (Map.insert key (R r) points)
                  set $! s{ uninterps = MapF.insert nonce newFnData (uninterps s) }
                  pure r
    
          case mbOldFnData of
            Just (UninterpFnData _ points) ->
              case Map.lookup key points of
                Just (R ret) -> pure ret
                Nothing -> allocatePoint points
            Nothing -> allocatePoint Map.empty
      _ -> fail "select only implemented for arrays emitted from symbolic functions"
  e -> fail ("RME does not support " ++ show e)