    {-# LANGUAGE DataKinds           #-}
    {-# LANGUAGE FlexibleContexts    #-}
    {-# LANGUAGE GADTs               #-}
    {-# LANGUAGE KindSignatures      #-}
    {-# LANGUAGE LambdaCase          #-}
    {-# LANGUAGE PatternSynonyms     #-}
    {-# LANGUAGE RankNTypes          #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications    #-}
    {-# LANGUAGE TypeOperators       #-}

    -- |
    -- Module      : Copilot.Theorem.What4
    -- Description : Prove spec properties using What4.
    -- Copyright   : (c) Ben Selfridge, 2020
    -- Maintainer  : benselfridge@galois.com
    -- Stability   : experimental
    -- Portability : POSIX
    --
    -- Spec properties are translated into the language of SMT solvers using
    -- @What4@. A backend solver is then used to prove the property is true. The
    -- technique is sound, but incomplete. If a property is proved true by this
    -- technique, then it can be guaranteed to be true. However, if a property is
    -- not proved true, that does not mean it isn't true; the proof may fail because
    -- the given property is not inductive.
    --
    -- We perform @k@-induction on all the properties in a given specification where
    -- @k@ is chosen to be the maximum amount of delay on any of the involved
    -- streams. This is a heuristic choice, but often effective.
    --
    -- The functions in this module are only designed to prove universally
    -- quantified propositions (i.e., propositions that use @forAll@). Attempting to
    -- prove an existentially quantified proposition (i.e., propositions that use
    -- @exists@) will cause a 'UnexpectedExistentialProposition' exception to be
    -- thrown.
    module Copilot.Theorem.What4
      ( -- * Proving properties about Copilot specifications
        prove
      , Solver(..)
      , SatResult(..)
      , proveWithCounterExample
      , SatResultCex(..)
      , CounterExample(..)
      , ProveException(..)
        -- * Bisimulation proofs about @copilot-c99@ code
      , computeBisimulationProofBundle
      , BisimulationProofBundle(..)
      , BisimulationProofState(..)
        -- * What4 representations of Copilot expressions
      , XExpr(..)
      , CopilotValue(..)
      , StreamOffset(..)
      ) where

    import qualified Copilot.Core.Expr       as CE
    import qualified Copilot.Core.Spec       as CS
    import qualified Copilot.Core.Type       as CT
    import qualified Copilot.Core.Type.Array as CTA

    import qualified What4.Config                   as WC
    import qualified What4.Expr.Builder             as WB
    import qualified What4.Expr.GroundEval          as WG
    import qualified What4.Interface                as WI
    import qualified What4.InterpretedFloatingPoint as WFP
    import qualified What4.Solver                   as WS
    import qualified What4.Solver.DReal             as WS

    import Control.Exception (Exception, throw)
    import Control.Monad (forM)
    import Control.Monad.State
    import qualified Data.BitVector.Sized as BV
    import Data.Foldable (foldrM)
    import Data.List (genericLength)
    import qualified Data.Map as Map
    import Data.Parameterized.Classes (ShowF)
    import Data.Parameterized.NatRepr
    import Data.Parameterized.Nonce
    import Data.Parameterized.Some
    import qualified Data.Parameterized.Vector as V
    import GHC.Float (castWord32ToFloat, castWord64ToDouble)
    import LibBF (BigFloat, bfToDouble, pattern NearEven)
    import qualified Panic as Panic

    import Copilot.Theorem.What4.Translate

    -- 'prove' function
    --
    -- To prove properties of a spec, we translate them into What4 using the TransM
    -- monad (transformer on top of IO), then negate each property and ask a backend
    -- solver to produce a model for the negation.

    -- | No builder state needed.
    data BuilderState a = EmptyState

    -- | The solvers supported by the what4 backend.
    data Solver = CVC4 | DReal | Yices | Z3

    -- | The 'prove' function returns results of this form for each property in a
    -- spec.
    data SatResult = Valid | Invalid | Unknown
      deriving Int -> SatResult -> ShowS
    [SatResult] -> ShowS
    SatResult -> String
    (Int -> SatResult -> ShowS)
    -> (SatResult -> String)
    -> ([SatResult] -> ShowS)
    -> Show SatResult
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SatResult -> ShowS
    showsPrec :: Int -> SatResult -> ShowS
    $cshow :: SatResult -> String
    show :: SatResult -> String
    $cshowList :: [SatResult] -> ShowS
    showList :: [SatResult] -> ShowS
    Show

    -- | The 'proveWithCounterExample' function returns results of this form for
    -- each property in a spec. This is largely the same as 'SatResult', except that
    -- 'InvalidCex' also records a 'CounterExample'.
    data SatResultCex = ValidCex | InvalidCex CounterExample | UnknownCex
      deriving Int -> SatResultCex -> ShowS
    [SatResultCex] -> ShowS
    SatResultCex -> String
    (Int -> SatResultCex -> ShowS)
    -> (SatResultCex -> String)
    -> ([SatResultCex] -> ShowS)
    -> Show SatResultCex
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SatResultCex -> ShowS
    showsPrec :: Int -> SatResultCex -> ShowS
    $cshow :: SatResultCex -> String
    show :: SatResultCex -> String
    $cshowList :: [SatResultCex] -> ShowS
    showList :: [SatResultCex] -> ShowS
    Show

    -- | Concrete values that cause a property in a Copilot specification to be
    -- invalid. As a simple example, consider the following spec:
    --
    -- @
    -- spec :: Spec
    -- spec = do
    --   let s :: Stream Bool
    --       s = [False] ++ constant True
    --   void $ prop "should be invalid" (forAll s)
    -- @
    --
    -- This defines a stream @s@ where the first value is @False@, but all
    -- subsequent values are @True@'. This is used in a property that asserts that
    -- the values in @s@ will be @True@ at all possible time steps. This is clearly
    -- not true, given that @s@'s first value is @False@. As such, we would expect
    -- that proving this property would yield an 'InvalidCex' result, where one of
    -- the base cases would state that the @s@ stream contains a @False@ value.
    --
    -- We can use the 'proveWithCounterExample' function to query an SMT solver to
    -- compute a counterexample:
    --
    -- @
    -- CounterExample
    --   { 'baseCases' =
    --       [False]
    --   , 'inductionStep' =
    --       True
    --   , 'concreteExternVars' =
    --       fromList []
    --   , 'concreteStreamValues' =
    --       fromList
    --         [ ( (0, 'AbsoluteOffset' 0), False )
    --         , ( (0, 'RelativeOffset' 0), False )
    --         , ( (0, 'RelativeOffset' 1), True )
    --         ]
    --   }
    -- @
    --
    -- Let's go over what this counterexample is saying:
    --
    -- * The 'inductionStep' of the proof is 'True', so that part of the proof was
    --   successful. On the other hand, the 'baseCases' contain a 'False', so the
    --   proof was falsified when proving the base cases. (In this case, the list
    --   has only one element, so there is only a single base case.)
    --
    -- * 'concreteStreamValues' reports the SMT solver's concrete values for each
    --   stream during relevant parts of the proof as a 'Map.Map'.
    --
    --   The keys of the map are pairs. The first element of the pair is the stream
    --   'CE.Id', and in this example, the only 'CE.Id' is @0@, corresponding to the
    --   stream @s@. The second element is the time offset. An 'AbsoluteOffset'
    --   indicates an offset starting from the initial time step, and a
    --   'RelativeOffset' indicates an offset from an arbitrary point in time.
    --   'AbsoluteOffset's are used in the base cases of the proof, and
    --   'RelativeOffset's are used in the induction step of the proof.
    --
    --   The part of the map that is most interesting to us is the
    --   @( (0, 'AbsoluteOffset' 0), False )@ entry, which represents a base case
    --   where there is a value of @False@ in the stream @s@ during the initial time
    --   step. Sure enough, this is enough to falsify the property @forAll s@.
    --
    -- * There are no extern streams in this example, so 'concreteExternVars' is
    --   empty.
    --
    -- We can also see an example of where a proof succeeds in the base cases, but
    -- fails during the induction step:
    --
    -- @
    -- spec :: Spec
    -- spec = do
    --   let t :: Stream Bool
    --       t = [True] ++ constant False
    --   void $ prop "should also be invalid" (forAll t)
    -- @
    --
    -- With the @t@ stream above, the base cases will succeed
    -- ('proveWithCounterExample' uses @k@-induction with a value of @k == 1@ in
    -- this example, so there will only be a single base case). On the other hand,
    -- the induction step will fail, as later values in the stream will be @False@.
    -- If we try to 'proveWithCounterExample' this property, then it will fail with:
    --
    -- @
    -- CounterExample
    --   { 'baseCases' =
    --       [True]
    --   , 'inductionStep' =
    --       False
    --   , 'concreteExternVars' =
    --       fromList []
    --   , 'concreteStreamValues' =
    --       fromList
    --         [ ( (0, 'AbsoluteOffset' 0), True )
    --         , ( (0, 'RelativeOffset' 0), True )
    --         , ( (0, 'RelativeOffset' 1), False )
    --         ]
    --   }
    -- @
    --
    -- This time, the 'inductionStep' is 'False'. If we look at the
    -- 'concreteStreamValues', we see the values at @'RelativeOffset' 0@ and
    -- @'RelativeOffset' 1@ (which are relevant to the induction step) are @True@
    -- and @False@, respectively. Since this is a proof by @k@-induction where
    -- @k == 1@, the fact that the value at @'RelativeOffset 1@ is @False@ indicates
    -- that the induction step was falsified.
    --
    -- Note that this proof does not say /when/ exactly the time steps at
    -- @'RelativeOffset' 0@ or @'RelativeOffset' 1@ occur, only that that will occur
    -- relative to some arbitrary point in time. In this example, they occur
    -- relative to the initial time step, so @'RelativeOffset' 1@ would occur at the
    -- second time step overall. In general, however, these time steps may occur far
    -- in the future, so it is possible that one would need to step through the
    -- execution of the streams for quite some time before finding the
    -- counterexample.
    --
    -- Be aware that counterexamples involving struct values are not currently
    -- supported.
    data CounterExample = CounterExample
        { -- | A list of base cases in the proof, where each entry in the list
          -- corresponds to a particular time step. For instance, the first element
          -- in the list corresponds to the initial time step, the second element
          -- in the list corresponds to the second time step, and so on. A 'False'
          -- entry anywhere in this list will cause the overall proof to be
          -- 'InvalidCex'.
          --
          -- Because the proof uses @k@-induction, the number of base cases (i.e.,
          -- the number of entries in this list) is equal to the value of @k@,
          -- which is chosen using heuristics.
          CounterExample -> [Bool]
    baseCases :: [Bool]
          -- | Whether the induction step of the proof was valid or not. That is,
          -- given an arbitrary time step @n@, if the property is assumed to hold
          -- at time steps @n@, @n+1@, ..., @n+k@, then this will be @True@ is the
          -- property can the be proven to hold at time step @n+k+1@ (and 'False'
          -- otherwise). If this is 'False', then the overall proof will be
          -- 'InvalidCex'.
        , CounterExample -> Bool
    inductionStep :: Bool
          -- | The concrete values in the Copilot specification's extern streams
          -- that lead to the property being invalid.
          --
          -- Each key in the 'Map.Map' is the 'CE.Name' of an extern stream paired
          -- with a 'StreamOffset' representing the time step. The key's
          -- corresponding value is the concrete value of the extern stream at that
          -- time step.
        , CounterExample -> Map (String, StreamOffset) (Some CopilotValue)
    concreteExternValues ::
            Map.Map (CE.Name, StreamOffset) (Some CopilotValue)
          -- | The concrete values in the Copilot specification's streams
          -- (excluding extern streams) that lead to the property being invalid.
          --
          -- Each key in the 'Map.Map' is the 'CE.Id' of a stream paired with a
          -- 'StreamOffset' representing the time step. The key's corresponding
          -- value is the concrete value of the extern stream at that time step.
        , CounterExample -> Map (Int, StreamOffset) (Some CopilotValue)
    concreteStreamValues :: Map.Map (CE.Id, StreamOffset) (Some CopilotValue)
        }
      deriving Int -> CounterExample -> ShowS
    [CounterExample] -> ShowS
    CounterExample -> String
    (Int -> CounterExample -> ShowS)
    -> (CounterExample -> String)
    -> ([CounterExample] -> ShowS)
    -> Show CounterExample
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> CounterExample -> ShowS
    showsPrec :: Int -> CounterExample -> ShowS
    $cshow :: CounterExample -> String
    show :: CounterExample -> String
    $cshowList :: [CounterExample] -> ShowS
    showList :: [CounterExample] -> ShowS
    Show

    -- | Exceptions that can arise when attempting a proof.
    data ProveException
      = UnexpectedExistentialProposition
        -- ^ The functions in "Copilot.Theorem.What4" can only prove properties with
        -- universally quantified propositions. The functions in
        -- "Copilot.Theorem.What4" will throw this exception if they encounter an
        -- existentially quantified proposition.
      deriving Int -> ProveException -> ShowS
    [ProveException] -> ShowS
    ProveException -> String
    (Int -> ProveException -> ShowS)
    -> (ProveException -> String)
    -> ([ProveException] -> ShowS)
    -> Show ProveException
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ProveException -> ShowS
    showsPrec :: Int -> ProveException -> ShowS
    $cshow :: ProveException -> String
    show :: ProveException -> String
    $cshowList :: [ProveException] -> ShowS
    showList :: [ProveException] -> ShowS
    Show

    instance Exception ProveException

    -- | Attempt to prove all of the properties in a spec via an SMT solver (which
    -- must be installed locally on the host). Return an association list mapping
    -- the names of each property to the result returned by the solver.
    --
    -- PRE: All of the properties in the 'CS.Spec' use universally quantified
    -- propositions. Attempting to supply an existentially quantified proposition
    -- will cause a 'UnexpectedExistentialProposition' exception to be thrown.
    prove :: Solver
          -- ^ Solver to use
          -> CS.Spec
          -- ^ Spec
          -> IO [(CE.Name, SatResult)]
    prove :: Solver -> Spec -> IO [(String, SatResult)]
    prove Solver
    solver Spec
    spec = Solver
    -> Spec
    -> (forall sym t (st :: * -> *) (fm :: FloatMode).
        (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
        [Pred sym]
        -> Pred sym
        -> TransState sym
        -> SatResult (GroundEvalFn t) ()
        -> IO SatResult)
    -> IO [(String, SatResult)]
    forall a.
    Solver
    -> Spec
    -> (forall sym t (st :: * -> *) (fm :: FloatMode).
        (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
        [Pred sym]
        -> Pred sym
        -> TransState sym
        -> SatResult (GroundEvalFn t) ()
        -> IO a)
    -> IO [(String, a)]
    proveInternal Solver
    solver Spec
    spec ((forall sym t (st :: * -> *) (fm :: FloatMode).
      (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
      [Pred sym]
      -> Pred sym
      -> TransState sym
      -> SatResult (GroundEvalFn t) ()
      -> IO SatResult)
     -> IO [(String, SatResult)])
    -> (forall sym t (st :: * -> *) (fm :: FloatMode).
        (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
        [Pred sym]
        -> Pred sym
        -> TransState sym
        -> SatResult (GroundEvalFn t) ()
        -> IO SatResult)
    -> IO [(String, SatResult)]
    forall a b. (a -> b) -> a -> b
    $ \[Pred sym]
    _ Pred sym
    _ TransState sym
    _ SatResult (GroundEvalFn t) ()
    satRes ->
      case SatResult (GroundEvalFn t) ()
    satRes of
        WS.Sat GroundEvalFn t
    _   -> SatResult -> IO SatResult
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SatResult
    Invalid
        WS.Unsat ()
    _ -> SatResult -> IO SatResult
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SatResult
    Valid
        SatResult (GroundEvalFn t) ()
    WS.Unknown -> SatResult -> IO SatResult
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SatResult
    Unknown

    -- | Attempt to prove all of the properties in a spec via an SMT solver (which
    -- must be installed locally on the host). Return an association list mapping
    -- the names of each property to the result returned by the solver.
    --
    -- Unlike 'prove', 'proveWithCounterExample' returns a 'SatResultCex'. This
    -- means that if a result is invalid, then it will include a 'CounterExample'
    -- which describes the circumstances under which the property was falsified. See
    -- the Haddocks for 'CounterExample' for more details.
    --
    -- Note that this function does not currently support creating counterexamples
    -- involving struct values, so attempting to call 'proveWithCounterExample' on a
    -- specification that uses structs will raise an error.
    proveWithCounterExample :: Solver
                            -- ^ Solver to use
                            -> CS.Spec
                            -- ^ Spec
                            -> IO [(CE.Name, SatResultCex)]
    proveWithCounterExample :: Solver -> Spec -> IO [(String, SatResultCex)]
    proveWithCounterExample Solver
    solver Spec
    spec =
      Solver
    -> Spec
    -> (forall sym t (st :: * -> *) (fm :: FloatMode).
        (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
        [Pred sym]
        -> Pred sym
        -> TransState sym
        -> SatResult (GroundEvalFn t) ()
        -> IO SatResultCex)
    -> IO [(String, SatResultCex)]
    forall a.
    Solver
    -> Spec
    -> (forall sym t (st :: * -> *) (fm :: FloatMode).
        (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
        [Pred sym]
        -> Pred sym
        -> TransState sym
        -> SatResult (GroundEvalFn t) ()
        -> IO a)
    -> IO [(String, a)]
    proveInternal Solver
    solver Spec
    spec ((forall sym t (st :: * -> *) (fm :: FloatMode).
      (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
      [Pred sym]
      -> Pred sym
      -> TransState sym
      -> SatResult (GroundEvalFn t) ()
      -> IO SatResultCex)
     -> IO [(String, SatResultCex)])
    -> (forall sym t (st :: * -> *) (fm :: FloatMode).
        (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
        [Pred sym]
        -> Pred sym
        -> TransState sym
        -> SatResult (GroundEvalFn t) ()
        -> IO SatResultCex)
    -> IO [(String, SatResultCex)]
    forall a b. (a -> b) -> a -> b
    $ \[Pred sym]
    baseCases Pred sym
    indStep TransState sym
    st SatResult (GroundEvalFn t) ()
    satRes ->
        case SatResult (GroundEvalFn t) ()
    satRes of
          WS.Sat GroundEvalFn t
    ge -> do
            gBaseCases <- (Expr t BaseBoolType -> IO Bool)
    -> [Expr t BaseBoolType] -> IO [Bool]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse (GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge) [Pred sym]
    [Expr t BaseBoolType]
    baseCases
            gIndStep <- WG.groundEval ge indStep
            gExternValues <- traverse (valFromExpr ge) (externVars st)
            gStreamValues <- traverse (valFromExpr ge) (streamValues st)
            let cex = CounterExample
                  { baseCases :: [Bool]
    baseCases            = [Bool]
    gBaseCases
                  , inductionStep :: Bool
    inductionStep        = Bool
    gIndStep
                  , concreteExternValues :: Map (String, StreamOffset) (Some CopilotValue)
    concreteExternValues = Map (String, StreamOffset) (Some CopilotValue)
    gExternValues
                  , concreteStreamValues :: Map (Int, StreamOffset) (Some CopilotValue)
    concreteStreamValues = Map (Int, StreamOffset) (Some CopilotValue)
    gStreamValues
                  }
            pure (InvalidCex cex)
          WS.Unsat ()
    _ -> SatResultCex -> IO SatResultCex
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SatResultCex
    ValidCex
          SatResult (GroundEvalFn t) ()
    WS.Unknown -> SatResultCex -> IO SatResultCex
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure SatResultCex
    UnknownCex

    -- | Attempt to prove all of the properties in a spec via an SMT solver (which
    -- must be installed locally on the host). For each 'WS.SatResult' returned by
    -- the solver, pass it to a continuation along with the relevant parts of the
    -- proof-related state.
    --
    -- This is an internal-only function that is used to power 'prove' and
    -- 'proveWithCounterExample'.
    proveInternal :: Solver
                  -- ^ Solver to use
                  -> CS.Spec
                  -- ^ Spec
                  -> (forall sym t st fm
                       . ( sym ~ WB.ExprBuilder t st (WB.Flags fm)
                         , WI.KnownRepr WB.FloatModeRepr fm )
                      => [WI.Pred sym]
                         -- The proof's base cases
                      -> WI.Pred sym
                         -- The proof's induction step
                      -> TransState sym
                         -- The proof state
                      -> WS.SatResult (WG.GroundEvalFn t) ()
                         -- The overall result of the proof
                      -> IO a)
                  -- ^ Continuation to call on each solver result
                  -> IO [(CE.Name, a)]
    proveInternal :: forall a.
    Solver
    -> Spec
    -> (forall sym t (st :: * -> *) (fm :: FloatMode).
        (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
        [Pred sym]
        -> Pred sym
        -> TransState sym
        -> SatResult (GroundEvalFn t) ()
        -> IO a)
    -> IO [(String, a)]
    proveInternal Solver
    solver Spec
    spec forall sym t (st :: * -> *) (fm :: FloatMode).
    (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
    [Pred sym]
    -> Pred sym
    -> TransState sym
    -> SatResult (GroundEvalFn t) ()
    -> IO a
    k = do
      -- Setup symbolic backend
      Some ng <- IO (Some (NonceGenerator IO))
    newIONonceGenerator
      sym <- WB.newExprBuilder WB.FloatIEEERepr EmptyState ng

      -- Solver-specific options
      case solver of
        Solver
    CVC4 -> [ConfigDesc] -> Config -> IO ()
    WC.extendConfig [ConfigDesc]
    WS.cvc4Options (ExprBuilder x BuilderState (Flags 'FloatIEEE) -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
    sym)
        Solver
    DReal -> [ConfigDesc] -> Config -> IO ()
    WC.extendConfig [ConfigDesc]
    WS.drealOptions (ExprBuilder x BuilderState (Flags 'FloatIEEE) -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
    sym)
        Solver
    Yices -> [ConfigDesc] -> Config -> IO ()
    WC.extendConfig [ConfigDesc]
    WS.yicesOptions (ExprBuilder x BuilderState (Flags 'FloatIEEE) -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
    sym)
        Solver
    Z3 -> [ConfigDesc] -> Config -> IO ()
    WC.extendConfig [ConfigDesc]
    WS.z3Options (ExprBuilder x BuilderState (Flags 'FloatIEEE) -> Config
    forall sym. IsExprBuilder sym => sym -> Config
    WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
    sym)

      -- Compute the maximum amount of delay for any stream in this spec
      let bufLen (CS.Stream Int
    _ [a]
    buf Expr a
    _ Type a
    _) = [a] -> p
    forall i a. Num i => [a] -> i
    genericLength [a]
    buf
          maxBufLen = [Integer] -> Integer
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum (Integer
    0 Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : (Stream -> Integer
    forall {p}. Num p => Stream -> p
    bufLen (Stream -> Integer) -> [Stream] -> [Integer]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Spec -> [Stream]
    CS.specStreams Spec
    spec))

      -- This process performs k-induction where we use @k = maxBufLen@.
      -- The choice for @k@ is heuristic, but often effective.
      let proveProperties = [Property]
    -> (Property
        -> TransM
             (ExprBuilder x BuilderState (Flags 'FloatIEEE)) (String, a))
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE)) [(String, a)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Spec -> [Property]
    CS.specProperties Spec
    spec) ((Property
      -> TransM
           (ExprBuilder x BuilderState (Flags 'FloatIEEE)) (String, a))
     -> TransM
          (ExprBuilder x BuilderState (Flags 'FloatIEEE)) [(String, a)])
    -> (Property
        -> TransM
             (ExprBuilder x BuilderState (Flags 'FloatIEEE)) (String, a))
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE)) [(String, a)]
    forall a b. (a -> b) -> a -> b
    $ \Property
    pr -> do
            -- This function only supports universally quantified propositions, so
            -- throw an exception if we encounter an existentially quantified
            -- proposition.
            let prop :: Expr Bool
    prop = case Property -> Prop
    CS.propertyProp Property
    pr of
                         CS.Forall Expr Bool
    p  -> Expr Bool
    p
                         CS.Exists {} -> ProveException -> Expr Bool
    forall a e. (HasCallStack, Exception e) => e -> a
    throw ProveException
    UnexpectedExistentialProposition
            -- State the base cases for k induction.
            base_cases <- [Integer]
    -> (Integer
        -> TransM
             (ExprBuilder x BuilderState (Flags 'FloatIEEE))
             (Expr x BaseBoolType))
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         [Expr x BaseBoolType]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Integer
    0 .. Integer
    maxBufLen Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1] ((Integer
      -> TransM
           (ExprBuilder x BuilderState (Flags 'FloatIEEE))
           (Expr x BaseBoolType))
     -> TransM
          (ExprBuilder x BuilderState (Flags 'FloatIEEE))
          [Expr x BaseBoolType])
    -> (Integer
        -> TransM
             (ExprBuilder x BuilderState (Flags 'FloatIEEE))
             (Expr x BaseBoolType))
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         [Expr x BaseBoolType]
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i -> do
              xe <- ExprBuilder x BuilderState (Flags 'FloatIEEE)
    -> LocalEnv (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    -> Expr Bool
    -> StreamOffset
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         (XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE)))
    forall sym a.
    IsInterpretedFloatSymExprBuilder sym =>
    sym
    -> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
    translateExpr ExprBuilder x BuilderState (Flags 'FloatIEEE)
    sym LocalEnv (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    forall a. Monoid a => a
    mempty Expr Bool
    prop (Integer -> StreamOffset
    AbsoluteOffset Integer
    i)
              case xe of
                XBool SymExpr
      (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
    p -> Expr x BaseBoolType
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         (Expr x BaseBoolType)
    forall a.
    a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SymExpr
      (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
    Expr x BaseBoolType
    p
                XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    _ -> String
    -> XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         (Expr x BaseBoolType)
    forall (m :: * -> *) sym a.
    (HasCallStack, MonadIO m, IsExprBuilder sym) =>
    String -> XExpr sym -> m a
    expectedBool String
    "Property" XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    xe

            -- Translate the induction hypothesis for all values up to maxBufLen in
            -- the past
            ind_hyps <- forM [0 .. maxBufLen-1] $ \Integer
    i -> do
              xe <- ExprBuilder x BuilderState (Flags 'FloatIEEE)
    -> LocalEnv (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    -> Expr Bool
    -> StreamOffset
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         (XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE)))
    forall sym a.
    IsInterpretedFloatSymExprBuilder sym =>
    sym
    -> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
    translateExpr ExprBuilder x BuilderState (Flags 'FloatIEEE)
    sym LocalEnv (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    forall a. Monoid a => a
    mempty Expr Bool
    prop (Integer -> StreamOffset
    RelativeOffset Integer
    i)
              case xe of
                XBool SymExpr
      (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
    hyp -> Expr x BaseBoolType
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         (Expr x BaseBoolType)
    forall a.
    a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SymExpr
      (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
    Expr x BaseBoolType
    hyp
                XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    _ -> String
    -> XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         (Expr x BaseBoolType)
    forall (m :: * -> *) sym a.
    (HasCallStack, MonadIO m, IsExprBuilder sym) =>
    String -> XExpr sym -> m a
    expectedBool String
    "Property" XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    xe

            -- Translate the predicate for the "current" value
            ind_goal <- do
              xe <- translateExpr sym
                                  mempty
                                  prop
                                  (RelativeOffset maxBufLen)
              case xe of
                XBool SymExpr
      (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
    p -> Expr x BaseBoolType
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         (Expr x BaseBoolType)
    forall a.
    a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SymExpr
      (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
    Expr x BaseBoolType
    p
                XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    _ -> String
    -> XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         (Expr x BaseBoolType)
    forall (m :: * -> *) sym a.
    (HasCallStack, MonadIO m, IsExprBuilder sym) =>
    String -> XExpr sym -> m a
    expectedBool String
    "Property" XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    xe

            -- Compute the predicate (ind_hyps ==> p)
            ind_case <- liftIO $ foldrM (WI.impliesPred sym) ind_goal ind_hyps

            -- Compute the conjunction of the base and inductive cases
            p <- liftIO $ foldrM (WI.andPred sym) ind_case base_cases

            -- Negate the goals for for SAT search
            not_p <- liftIO $ WI.notPred sym p
            let clauses = [Expr x BaseBoolType
    not_p]

            st <- get
            let k' = [SymExpr
       (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType]
    -> SymExpr
         (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
    -> TransState (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    -> SatResult (GroundEvalFn x) ()
    -> IO a
    forall sym t (st :: * -> *) (fm :: FloatMode).
    (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
    [Pred sym]
    -> Pred sym
    -> TransState sym
    -> SatResult (GroundEvalFn t) ()
    -> IO a
    k [SymExpr
       (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType]
    [Expr x BaseBoolType]
    base_cases SymExpr
      (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
    Expr x BaseBoolType
    ind_case TransState (ExprBuilder x BuilderState (Flags 'FloatIEEE))
    st
            satRes <-
              case solver of
                Solver
    CVC4 -> IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall a.
    IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a)
    -> IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall a b. (a -> b) -> a -> b
    $ ExprBuilder x BuilderState (Flags 'FloatIEEE)
    -> LogData
    -> [Expr x BaseBoolType]
    -> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
        -> IO a)
    -> IO a
    forall t (st :: * -> *) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    WS.runCVC4InOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
    sym LogData
    WS.defaultLogData [Expr x BaseBoolType]
    clauses ((SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
      -> IO a)
     -> IO a)
    -> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
        -> IO a)
    -> IO a
    forall a b. (a -> b) -> a -> b
    $ \case
                  WS.Sat (GroundEvalFn x
    ge, Maybe (ExprRangeBindings x)
    _) -> SatResult (GroundEvalFn x) () -> IO a
    k' (GroundEvalFn x -> SatResult (GroundEvalFn x) ()
    forall mdl core. mdl -> SatResult mdl core
    WS.Sat GroundEvalFn x
    ge)
                  WS.Unsat ()
    x -> SatResult (GroundEvalFn x) () -> IO a
    k' (() -> SatResult (GroundEvalFn x) ()
    forall mdl core. core -> SatResult mdl core
    WS.Unsat ()
    x)
                  SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
    WS.Unknown -> SatResult (GroundEvalFn x) () -> IO a
    k' SatResult (GroundEvalFn x) ()
    forall mdl core. SatResult mdl core
    WS.Unknown
                Solver
    DReal -> IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall a.
    IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a)
    -> IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall a b. (a -> b) -> a -> b
    $ ExprBuilder x BuilderState (Flags 'FloatIEEE)
    -> LogData
    -> [Expr x BaseBoolType]
    -> (SatResult (WriterConn x (Writer DReal), DRealBindings) ()
        -> IO a)
    -> IO a
    forall t (st :: * -> *) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (WriterConn t (Writer DReal), DRealBindings) ()
        -> IO a)
    -> IO a
    WS.runDRealInOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
    sym LogData
    WS.defaultLogData [Expr x BaseBoolType]
    clauses ((SatResult (WriterConn x (Writer DReal), DRealBindings) ()
      -> IO a)
     -> IO a)
    -> (SatResult (WriterConn x (Writer DReal), DRealBindings) ()
        -> IO a)
    -> IO a
    forall a b. (a -> b) -> a -> b
    $ \case
                  WS.Sat (WriterConn x (Writer DReal)
    c, DRealBindings
    m) -> do
                    ge <- WriterConn x (Writer DReal) -> DRealBindings -> IO (GroundEvalFn x)
    forall t.
    WriterConn t (Writer DReal) -> DRealBindings -> IO (GroundEvalFn t)
    WS.getAvgBindings WriterConn x (Writer DReal)
    c DRealBindings
    m
                    k' (WS.Sat ge)
                  WS.Unsat ()
    x -> SatResult (GroundEvalFn x) () -> IO a
    k' (() -> SatResult (GroundEvalFn x) ()
    forall mdl core. core -> SatResult mdl core
    WS.Unsat ()
    x)
                  SatResult (WriterConn x (Writer DReal), DRealBindings) ()
    WS.Unknown -> SatResult (GroundEvalFn x) () -> IO a
    k' SatResult (GroundEvalFn x) ()
    forall mdl core. SatResult mdl core
    WS.Unknown
                Solver
    Yices -> IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall a.
    IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a)
    -> IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall a b. (a -> b) -> a -> b
    $ ExprBuilder x BuilderState (Flags 'FloatIEEE)
    -> LogData
    -> [Expr x BaseBoolType]
    -> (SatResult (GroundEvalFn x) () -> IO a)
    -> IO a
    forall t (st :: * -> *) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t) () -> IO a)
    -> IO a
    WS.runYicesInOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
    sym LogData
    WS.defaultLogData [Expr x BaseBoolType]
    clauses ((SatResult (GroundEvalFn x) () -> IO a) -> IO a)
    -> (SatResult (GroundEvalFn x) () -> IO a) -> IO a
    forall a b. (a -> b) -> a -> b
    $ \case
                  WS.Sat GroundEvalFn x
    ge -> SatResult (GroundEvalFn x) () -> IO a
    k' (GroundEvalFn x -> SatResult (GroundEvalFn x) ()
    forall mdl core. mdl -> SatResult mdl core
    WS.Sat GroundEvalFn x
    ge)
                  WS.Unsat ()
    x -> SatResult (GroundEvalFn x) () -> IO a
    k' (() -> SatResult (GroundEvalFn x) ()
    forall mdl core. core -> SatResult mdl core
    WS.Unsat ()
    x)
                  SatResult (GroundEvalFn x) ()
    WS.Unknown -> SatResult (GroundEvalFn x) () -> IO a
    k' SatResult (GroundEvalFn x) ()
    forall mdl core. SatResult mdl core
    WS.Unknown
                Solver
    Z3 -> IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall a.
    IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a)
    -> IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
    forall a b. (a -> b) -> a -> b
    $ ExprBuilder x BuilderState (Flags 'FloatIEEE)
    -> LogData
    -> [Expr x BaseBoolType]
    -> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
        -> IO a)
    -> IO a
    forall t (st :: * -> *) fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a
    WS.runZ3InOverride ExprBuilder x BuilderState (Flags 'FloatIEEE)
    sym LogData
    WS.defaultLogData [Expr x BaseBoolType]
    clauses ((SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
      -> IO a)
     -> IO a)
    -> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
        -> IO a)
    -> IO a
    forall a b. (a -> b) -> a -> b
    $ \case
                  WS.Sat (GroundEvalFn x
    ge, Maybe (ExprRangeBindings x)
    _) -> SatResult (GroundEvalFn x) () -> IO a
    k' (GroundEvalFn x -> SatResult (GroundEvalFn x) ()
    forall mdl core. mdl -> SatResult mdl core
    WS.Sat GroundEvalFn x
    ge)
                  WS.Unsat ()
    x -> SatResult (GroundEvalFn x) () -> IO a
    k' (() -> SatResult (GroundEvalFn x) ()
    forall mdl core. core -> SatResult mdl core
    WS.Unsat ()
    x)
                  SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
    WS.Unknown -> SatResult (GroundEvalFn x) () -> IO a
    k' SatResult (GroundEvalFn x) ()
    forall mdl core. SatResult mdl core
    WS.Unknown

            pure (CS.propertyName pr, satRes)

      -- Execute the action and return the results for each property
      runTransM spec proveProperties

    -- Bisimulation proofs

    -- | Given a Copilot specification, compute all of the symbolic states necessary
    -- to carry out a bisimulation proof that establishes a correspondence between
    -- the states of the Copilot stream program and the C code that @copilot-c99@
    -- would generate for that Copilot program.
    --
    -- PRE: All of the properties in the 'CS.Spec' use universally quantified
    -- propositions. Attempting to supply an existentially quantified proposition
    -- will cause a 'UnexpectedExistentialProposition' exception to be thrown.
    computeBisimulationProofBundle ::
         WFP.IsInterpretedFloatSymExprBuilder sym
      => sym
      -> [String]
      -- ^ Names of properties to assume during verification
      -> CS.Spec
      -- ^ The input Copilot specification
      -> IO (BisimulationProofBundle sym)
    computeBisimulationProofBundle :: forall sym.
    IsInterpretedFloatSymExprBuilder sym =>
    sym -> [String] -> Spec -> IO (BisimulationProofBundle sym)
    computeBisimulationProofBundle sym
    sym [String]
    properties Spec
    spec = do
      iss <- sym -> Spec -> IO (BisimulationProofState sym)
    forall sym.
    IsInterpretedFloatSymExprBuilder sym =>
    sym -> Spec -> IO (BisimulationProofState sym)
    computeInitialStreamState sym
    sym Spec
    spec
      runTransM spec $ do
        prestate  <- computePrestate sym spec
        poststate <- computePoststate sym spec
        triggers  <- computeTriggerState sym spec
        assms     <- computeAssumptions sym properties spec
        externs   <- computeExternalInputs sym
        sideCnds  <- gets sidePreds
        return
          BisimulationProofBundle
            { initialStreamState = iss
            , preStreamState     = prestate
            , postStreamState    = poststate
            , externalInputs     = externs
            , triggerState       = triggers
            , assumptions        = assms
            , sideConds          = sideCnds
            }

    -- | A collection of all of the symbolic states necessary to carry out a
    -- bisimulation proof.
    data BisimulationProofBundle sym =
      BisimulationProofBundle
        { forall sym.
    BisimulationProofBundle sym -> BisimulationProofState sym
    initialStreamState :: BisimulationProofState sym
          -- ^ The state of the global variables at program startup
        , forall sym.
    BisimulationProofBundle sym -> BisimulationProofState sym
    preStreamState :: BisimulationProofState sym
          -- ^ The stream state prior to invoking the step function
        , forall sym.
    BisimulationProofBundle sym -> BisimulationProofState sym
    postStreamState :: BisimulationProofState sym
          -- ^ The stream state after invoking the step function
        , forall sym.
    BisimulationProofBundle sym -> [(String, Some Type, XExpr sym)]
    externalInputs :: [(CE.Name, Some CT.Type, XExpr sym)]
          -- ^ A list of external streams, where each tuple contains:
          --
          -- 1. The name of the stream
          --
          -- 2. The type of the stream
          --
          -- 3. The value of the stream represented as a fresh constant
        , forall sym.
    BisimulationProofBundle sym
    -> [(String, Pred sym, [(Some Type, XExpr sym)])]
    triggerState :: [(CE.Name, WI.Pred sym, [(Some CT.Type, XExpr sym)])]
          -- ^ A list of trigger functions, where each tuple contains:
          --
          -- 1. The name of the function
          --
          -- 2. A formula representing the guarded condition
          --
          -- 3. The arguments to the function, where each argument is represented as
          --    a type-value pair
        , forall sym. BisimulationProofBundle sym -> [Pred sym]
    assumptions :: [WI.Pred sym]
          -- ^ User-provided property assumptions
        , forall sym. BisimulationProofBundle sym -> [Pred sym]
    sideConds :: [WI.Pred sym]
          -- ^ Side conditions related to partial operations
        }

    -- | The state of a bisimulation proof at a particular step.
    newtype BisimulationProofState sym =
      BisimulationProofState
        { forall sym.
    BisimulationProofState sym -> [(Int, Some Type, [XExpr sym])]
    streamState :: [(CE.Id, Some CT.Type, [XExpr sym])]
          -- ^ A list of tuples containing:
          --
          -- 1. The name of a stream
          --
          -- 2. The type of the stream
          --
          -- 3. The list of values in the stream description
        }

    -- | Compute the initial state of the global variables at the start of a Copilot
    -- program.
    computeInitialStreamState ::
         WFP.IsInterpretedFloatSymExprBuilder sym
      => sym
      -> CS.Spec
      -- ^ The input Copilot specification
      -> IO (BisimulationProofState sym)
    computeInitialStreamState :: forall sym.
    IsInterpretedFloatSymExprBuilder sym =>
    sym -> Spec -> IO (BisimulationProofState sym)
    computeInitialStreamState sym
    sym Spec
    spec = do
      xs <- [Stream]
    -> (Stream -> IO (Int, Some Type, [XExpr sym]))
    -> IO [(Int, Some Type, [XExpr sym])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Spec -> [Stream]
    CS.specStreams Spec
    spec) ((Stream -> IO (Int, Some Type, [XExpr sym]))
     -> IO [(Int, Some Type, [XExpr sym])])
    -> (Stream -> IO (Int, Some Type, [XExpr sym]))
    -> IO [(Int, Some Type, [XExpr sym])]
    forall a b. (a -> b) -> a -> b
    $
             \CS.Stream { streamId :: Stream -> Int
    CS.streamId = Int
    nm, streamExprType :: ()
    CS.streamExprType = Type a
    tp
                        , streamBuffer :: ()
    CS.streamBuffer = [a]
    buf } ->
             do vs <- (a -> IO (XExpr sym)) -> [a] -> IO [XExpr sym]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (sym -> Type a -> a -> IO (XExpr sym)
    forall sym a.
    IsInterpretedFloatExprBuilder sym =>
    sym -> Type a -> a -> IO (XExpr sym)
    translateConstExpr sym
    sym Type a
    tp) [a]
    buf
                return (nm, Some tp, vs)
      return (BisimulationProofState xs)

    -- | Compute the stream state of a Copilot program prior to invoking the step
    -- function.
    computePrestate ::
         WFP.IsInterpretedFloatSymExprBuilder sym
      => sym
      -> CS.Spec
      -- ^ The input Copilot specification
      -> TransM sym (BisimulationProofState sym)
    computePrestate :: forall sym.
    IsInterpretedFloatSymExprBuilder sym =>
    sym -> Spec -> TransM sym (BisimulationProofState sym)
    computePrestate sym
    sym Spec
    spec = do
      xs <- [Stream]
    -> (Stream -> TransM sym (Int, Some Type, [XExpr sym]))
    -> TransM sym [(Int, Some Type, [XExpr sym])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Spec -> [Stream]
    CS.specStreams Spec
    spec) ((Stream -> TransM sym (Int, Some Type, [XExpr sym]))
     -> TransM sym [(Int, Some Type, [XExpr sym])])
    -> (Stream -> TransM sym (Int, Some Type, [XExpr sym]))
    -> TransM sym [(Int, Some Type, [XExpr sym])]
    forall a b. (a -> b) -> a -> b
    $
              \CS.Stream { streamId :: Stream -> Int
    CS.streamId = Int
    nm, streamExprType :: ()
    CS.streamExprType = Type a
    tp
                         , streamBuffer :: ()
    CS.streamBuffer = [a]
    buf } ->
              do let buflen :: Integer
    buflen = [a] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [a]
    buf
                 let idxes :: [StreamOffset]
    idxes = Integer -> StreamOffset
    RelativeOffset (Integer -> StreamOffset) -> [Integer] -> [StreamOffset]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Integer
    0 .. Integer
    buflenInteger -> Integer -> Integer
    forall a. Num a => a -> a -> a
    -Integer
    1]
                 vs <- (StreamOffset -> TransM sym (XExpr sym))
    -> [StreamOffset] -> TransM sym [XExpr sym]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (sym -> Int -> StreamOffset -> TransM sym (XExpr sym)
    forall sym.
    IsInterpretedFloatSymExprBuilder sym =>
    sym -> Int -> StreamOffset -> TransM sym (XExpr sym)
    getStreamValue sym
    sym Int
    nm) [StreamOffset]
    idxes
                 return (nm, Some tp, vs)
      return (BisimulationProofState xs)

    -- | Compute ehe stream state of a Copilot program after invoking the step
    -- function.
    computePoststate ::
         WFP.IsInterpretedFloatSymExprBuilder sym
      => sym
      -> CS.Spec
      -- ^ The input Copilot specification
      -> TransM sym (BisimulationProofState sym)
    computePoststate :: forall sym.
    IsInterpretedFloatSymExprBuilder sym =>
    sym -> Spec -> TransM sym (BisimulationProofState sym)
    computePoststate sym
    sym Spec
    spec = do
      xs <- [Stream]
    -> (Stream -> TransM sym (Int, Some Type, [XExpr sym]))
    -> TransM sym [(Int, Some Type, [XExpr sym])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Spec -> [Stream]
    CS.specStreams Spec
    spec) ((Stream -> TransM sym (Int, Some Type, [XExpr sym]))
     -> TransM sym [(Int, Some Type, [XExpr sym])])
    -> (Stream -> TransM sym (Int, Some Type, [XExpr sym]))
    -> TransM sym [(Int, Some Type, [XExpr sym])]
    forall a b. (a -> b) -> a -> b
    $
              \CS.Stream { streamId :: Stream -> Int
    CS.streamId = Int
    nm, streamExprType :: ()
    CS.streamExprType = Type a
    tp
                         , streamBuffer :: ()
    CS.streamBuffer = [a]
    buf } ->
              do let buflen :: Integer
    buflen = [a] -> Integer
    forall i a. Num i => [a] -> i
    genericLength [a]
    buf
                 let idxes :: [StreamOffset]
    idxes = Integer -> StreamOffset
    RelativeOffset (Integer -> StreamOffset) -> [Integer] -> [StreamOffset]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Integer
    1 .. Integer
    buflen]
                 vs <- (StreamOffset -> TransM sym (XExpr sym))
    -> [StreamOffset] -> TransM sym [XExpr sym]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (sym -> Int -> StreamOffset -> TransM sym (XExpr sym)
    forall sym.
    IsInterpretedFloatSymExprBuilder sym =>
    sym -> Int -> StreamOffset -> TransM sym (XExpr sym)
    getStreamValue sym
    sym Int
    nm) [StreamOffset]
    idxes
                 return (nm, Some tp, vs)
      return (BisimulationProofState xs)

    -- | Compute the trigger functions in a Copilot program.
    computeTriggerState ::
         WFP.IsInterpretedFloatSymExprBuilder sym
      => sym
      -> CS.Spec
      -- ^ The input Copilot specification
      -> TransM sym [(CE.Name, WI.Pred sym, [(Some CT.Type, XExpr sym)])]
    computeTriggerState :: forall sym.
    IsInterpretedFloatSymExprBuilder sym =>
    sym
    -> Spec
    -> TransM sym [(String, Pred sym, [(Some Type, XExpr sym)])]
    computeTriggerState sym
    sym Spec
    spec = [Trigger]
    -> (Trigger
        -> TransM sym (String, Pred sym, [(Some Type, XExpr sym)]))
    -> TransM sym [(String, Pred sym, [(Some Type, XExpr sym)])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Spec -> [Trigger]
    CS.specTriggers Spec
    spec) ((Trigger
      -> TransM sym (String, Pred sym, [(Some Type, XExpr sym)]))
     -> TransM sym [(String, Pred sym, [(Some Type, XExpr sym)])])
    -> (Trigger
        -> TransM sym (String, Pred sym, [(Some Type, XExpr sym)]))
    -> TransM sym [(String, Pred sym, [(Some Type, XExpr sym)])]
    forall a b. (a -> b) -> a -> b
    $
        \(CS.Trigger { triggerName :: Trigger -> String
    CS.triggerName = String
    nm, triggerGuard :: Trigger -> Expr Bool
    CS.triggerGuard = Expr Bool
    guard
                     , triggerArgs :: Trigger -> [UExpr]
    CS.triggerArgs = [UExpr]
    args }) ->
          do xguard <- sym
    -> LocalEnv sym
    -> Expr Bool
    -> StreamOffset
    -> TransM sym (XExpr sym)
    forall sym a.
    IsInterpretedFloatSymExprBuilder sym =>
    sym
    -> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
    translateExpr sym
    sym LocalEnv sym
    forall a. Monoid a => a
    mempty Expr Bool
    guard (Integer -> StreamOffset
    RelativeOffset Integer
    0)
             guard' <-
               case xguard of
                 XBool Pred sym
    guard' -> Pred sym -> TransM sym (Pred sym)
    forall a. a -> TransM sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Pred sym
    guard'
                 XExpr sym
    _ -> String -> XExpr sym -> TransM sym (Pred sym)
    forall (m :: * -> *) sym a.
    (HasCallStack, MonadIO m, IsExprBuilder sym) =>
    String -> XExpr sym -> m a
    expectedBool String
    "Trigger guard" XExpr sym
    xguard
             args' <- mapM computeArg args
             return (nm, guard', args')
      where
       computeArg :: UExpr -> TransM sym (Some Type, XExpr sym)
    computeArg (CE.UExpr Type a
    tp Expr a
    ex) = do
         v <- sym
    -> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
    forall sym a.
    IsInterpretedFloatSymExprBuilder sym =>
    sym
    -> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
    translateExpr sym
    sym LocalEnv sym
    forall a. Monoid a => a
    mempty Expr a
    ex (Integer -> StreamOffset
    RelativeOffset Integer
    0)
         return (Some tp, v)

    -- | Compute the values of the external streams in a Copilot program, where each
    -- external stream is represented as a fresh constant.
    computeExternalInputs ::
         WFP.IsInterpretedFloatSymExprBuilder sym
      => sym
      -> TransM sym [(CE.Name, Some CT.Type, XExpr sym)]
    computeExternalInputs :: forall sym.
    IsInterpretedFloatSymExprBuilder sym =>
    sym -> TransM sym [(String, Some Type, XExpr sym)]
    computeExternalInputs sym
    sym = do
      exts <- Map String (Some Type) -> [(String, Some Type)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Map String (Some Type) -> [(String, Some Type)])
    -> TransM sym (Map String (Some Type))
    -> TransM sym [(String, Some Type)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TransState sym -> Map String (Some Type))
    -> TransM sym (Map String (Some Type))
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets TransState sym -> Map String (Some Type)
    forall sym. TransState sym -> Map String (Some Type)
    mentionedExternals
      forM exts $ \(String
    nm, Some Type x
    tp) -> do
        v <- sym -> Type x -> String -> StreamOffset -> TransM sym (XExpr sym)
    forall sym a.
    IsInterpretedFloatSymExprBuilder sym =>
    sym -> Type a -> String -> StreamOffset -> TransM sym (XExpr sym)
    getExternConstant sym
    sym Type x
    tp String
    nm (Integer -> StreamOffset
    RelativeOffset Integer
    0)
        return (nm, Some tp, v)

    -- | Compute the user-provided property assumptions in a Copilot program.
    --
    -- PRE: All of the properties in the 'CS.Spec' use universally quantified
    -- propositions. Attempting to supply an existentially quantified proposition
    -- will cause a 'UnexpectedExistentialProposition' exception to be thrown.
    computeAssumptions ::
         forall sym.
         WFP.IsInterpretedFloatSymExprBuilder sym
      => sym
      -> [String]
      -- ^ Names of properties to assume during verification
      -> CS.Spec
      -- ^ The input Copilot specification
      -> TransM sym [WI.Pred sym]
    computeAssumptions :: forall sym.
    IsInterpretedFloatSymExprBuilder sym =>
    sym -> [String] -> Spec -> TransM sym [Pred sym]
    computeAssumptions sym
    sym [String]
    properties Spec
    spec =
        [[SymExpr sym BaseBoolType]] -> [SymExpr sym BaseBoolType]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[SymExpr sym BaseBoolType]] -> [SymExpr sym BaseBoolType])
    -> TransM sym [[SymExpr sym BaseBoolType]]
    -> TransM sym [SymExpr sym BaseBoolType]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Expr Bool]
    -> (Expr Bool -> TransM sym [SymExpr sym BaseBoolType])
    -> TransM sym [[SymExpr sym BaseBoolType]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Expr Bool]
    specPropertyExprs Expr Bool -> TransM sym [SymExpr sym BaseBoolType]
    computeAssumption
      where
        bufLen :: Stream -> p
    bufLen (CS.Stream Int
    _ [a]
    buf Expr a
    _ Type a
    _) = [a] -> p
    forall i a. Num i => [a] -> i
    genericLength [a]
    buf
        maxBufLen :: Integer
    maxBufLen = [Integer] -> Integer
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    maximum (Integer
    0 Integer -> [Integer] -> [Integer]
    forall a. a -> [a] -> [a]
    : (Stream -> Integer
    forall {p}. Num p => Stream -> p
    bufLen (Stream -> Integer) -> [Stream] -> [Integer]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Spec -> [Stream]
    CS.specStreams Spec
    spec))

        -- Retrieve the boolean-values Copilot expressions corresponding to the
        -- user-provided property assumptions.
        specPropertyExprs :: [CE.Expr Bool]
        specPropertyExprs :: [Expr Bool]
    specPropertyExprs =
          [ Prop -> Expr Bool
    CS.extractProp (Property -> Prop
    CS.propertyProp Property
    p)
          | Property
    p <- Spec -> [Property]
    CS.specProperties Spec
    spec
          , String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    elem (Property -> String
    CS.propertyName Property
    p) [String]
    properties
          , let prop :: Expr Bool
    prop = case Property -> Prop
    CS.propertyProp Property
    p of
                         CS.Forall Expr Bool
    pr -> Expr Bool
    pr
                         CS.Exists {} -> ProveException -> Expr Bool
    forall a e. (HasCallStack, Exception e) => e -> a
    throw ProveException
    UnexpectedExistentialProposition
          ]

        -- Compute all of the what4 predicates corresponding to each user-provided
        -- property assumption.
        computeAssumption :: CE.Expr Bool -> TransM sym [WI.Pred sym]
        computeAssumption :: Expr Bool -> TransM sym [SymExpr sym BaseBoolType]
    computeAssumption Expr Bool
    e = [Integer]
    -> (Integer -> TransM sym (SymExpr sym BaseBoolType))
    -> TransM sym [SymExpr sym BaseBoolType]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [Integer
    0 .. Integer
    maxBufLen] ((Integer -> TransM sym (SymExpr sym BaseBoolType))
     -> TransM sym [SymExpr sym BaseBoolType])
    -> (Integer -> TransM sym (SymExpr sym BaseBoolType))
    -> TransM sym [SymExpr sym BaseBoolType]
    forall a b. (a -> b) -> a -> b
    $ \Integer
    i -> do
          xe <- sym
    -> LocalEnv sym
    -> Expr Bool
    -> StreamOffset
    -> TransM sym (XExpr sym)
    forall sym a.
    IsInterpretedFloatSymExprBuilder sym =>
    sym
    -> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
    translateExpr sym
    sym LocalEnv sym
    forall a. Monoid a => a
    mempty Expr Bool
    e (Integer -> StreamOffset
    RelativeOffset Integer
    i)
          case xe of
            XBool SymExpr sym BaseBoolType
    b -> SymExpr sym BaseBoolType -> TransM sym (SymExpr sym BaseBoolType)
    forall a. a -> TransM sym a
    forall (m :: * -> *) a. Monad m => a -> m a
    return SymExpr sym BaseBoolType
    b
            XExpr sym
    _ -> String -> XExpr sym -> TransM sym (SymExpr sym BaseBoolType)
    forall (m :: * -> *) sym a.
    (HasCallStack, MonadIO m, IsExprBuilder sym) =>
    String -> XExpr sym -> m a
    expectedBool String
    "Property" XExpr sym
    xe

    -- * Auxiliary functions

    -- | A catch-all 'panic' to use when an 'XExpr' is is expected to uphold the
    -- invariant that it is an 'XBool', but the invariant is violated.
    expectedBool :: forall m sym a.
                    (Panic.HasCallStack, MonadIO m, WI.IsExprBuilder sym)
                 => String
                 -- ^ What the 'XExpr' represents
                 -> XExpr sym
                 -> m a
    expectedBool :: forall (m :: * -> *) sym a.
    (HasCallStack, MonadIO m, IsExprBuilder sym) =>
    String -> XExpr sym -> m a
    expectedBool String
    what XExpr sym
    xe =
      [String] -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadIO m) =>
    [String] -> m a
    panic [String
    what String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " expected to have boolean result", XExpr sym -> String
    forall a. Show a => a -> String
    show XExpr sym
    xe]

    -- | A Copilot value paired with its 'CT.Type'.
    data CopilotValue a where
      CopilotValue :: CT.Typed a => CT.Type a -> a -> CopilotValue a

    instance Show (CopilotValue a) where
      showsPrec :: Int -> CopilotValue a -> ShowS
    showsPrec Int
    p (CopilotValue Type a
    ty a
    val) =
        case Type a
    ty of
          Type a
    CT.Bool      -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          Type a
    CT.Int8      -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          Type a
    CT.Int16     -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          Type a
    CT.Int32     -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          Type a
    CT.Int64     -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          Type a
    CT.Word8     -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          Type a
    CT.Word16    -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          Type a
    CT.Word32    -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          Type a
    CT.Word64    -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          Type a
    CT.Float     -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          Type a
    CT.Double    -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          CT.Array {}  -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
          CT.Struct {} -> Int -> a -> ShowS
    forall a. Show a => Int -> a -> ShowS
    showsPrec Int
    p a
    val
    instance ShowF CopilotValue

    -- | Convert a symbolic 'XExpr' into a concrete 'CopilotValue'.
    --
    -- Struct values are not currently supported, so attempting to convert an
    -- 'XStruct' value will raise an error.
    valFromExpr :: forall sym t st fm.
                   ( sym ~ WB.ExprBuilder t st (WB.Flags fm)
                   , WI.KnownRepr WB.FloatModeRepr fm
                   )
                => WG.GroundEvalFn t
                -> XExpr sym
                -> IO (Some CopilotValue)
    valFromExpr :: forall sym t (st :: * -> *) (fm :: FloatMode).
    (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
    GroundEvalFn t -> XExpr sym -> IO (Some CopilotValue)
    valFromExpr GroundEvalFn t
    ge XExpr sym
    xe = case XExpr sym
    xe of
      XBool SymExpr sym BaseBoolType
    e -> CopilotValue Bool -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue Bool -> Some CopilotValue)
    -> (Bool -> CopilotValue Bool) -> Bool -> Some CopilotValue
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type Bool -> Bool -> CopilotValue Bool
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue Type Bool
    CT.Bool (Bool -> Some CopilotValue) -> IO Bool -> IO (Some CopilotValue)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym BaseBoolType
    Expr t BaseBoolType
    e
      XInt8 SymExpr sym (BaseBVType 8)
    e -> CopilotValue Int8 -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue Int8 -> Some CopilotValue)
    -> (BV 8 -> CopilotValue Int8) -> BV 8 -> Some CopilotValue
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type Int8 -> Int8 -> CopilotValue Int8
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue Type Int8
    CT.Int8 (Int8 -> CopilotValue Int8)
    -> (BV 8 -> Int8) -> BV 8 -> CopilotValue Int8
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV 8 -> Int8
    forall a (w :: Nat). Num a => BV w -> a
    fromBV (BV 8 -> Some CopilotValue) -> IO (BV 8) -> IO (Some CopilotValue)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym (BaseBVType 8)
    Expr t (BaseBVType 8)
    e
      XInt16 SymExpr sym (BaseBVType 16)
    e -> CopilotValue Int16 -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue Int16 -> Some CopilotValue)
    -> (BV 16 -> CopilotValue Int16) -> BV 16 -> Some CopilotValue
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type Int16 -> Int16 -> CopilotValue Int16
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue Type Int16
    CT.Int16 (Int16 -> CopilotValue Int16)
    -> (BV 16 -> Int16) -> BV 16 -> CopilotValue Int16
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV 16 -> Int16
    forall a (w :: Nat). Num a => BV w -> a
    fromBV (BV 16 -> Some CopilotValue)
    -> IO (BV 16) -> IO (Some CopilotValue)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym (BaseBVType 16)
    Expr t (BaseBVType 16)
    e
      XInt32 SymExpr sym (BaseBVType 32)
    e -> CopilotValue Int32 -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue Int32 -> Some CopilotValue)
    -> (BV 32 -> CopilotValue Int32) -> BV 32 -> Some CopilotValue
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type Int32 -> Int32 -> CopilotValue Int32
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue Type Int32
    CT.Int32 (Int32 -> CopilotValue Int32)
    -> (BV 32 -> Int32) -> BV 32 -> CopilotValue Int32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV 32 -> Int32
    forall a (w :: Nat). Num a => BV w -> a
    fromBV (BV 32 -> Some CopilotValue)
    -> IO (BV 32) -> IO (Some CopilotValue)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym (BaseBVType 32)
    Expr t (BaseBVType 32)
    e
      XInt64 SymExpr sym (BaseBVType 64)
    e -> CopilotValue Int64 -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue Int64 -> Some CopilotValue)
    -> (BV 64 -> CopilotValue Int64) -> BV 64 -> Some CopilotValue
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type Int64 -> Int64 -> CopilotValue Int64
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue Type Int64
    CT.Int64 (Int64 -> CopilotValue Int64)
    -> (BV 64 -> Int64) -> BV 64 -> CopilotValue Int64
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV 64 -> Int64
    forall a (w :: Nat). Num a => BV w -> a
    fromBV (BV 64 -> Some CopilotValue)
    -> IO (BV 64) -> IO (Some CopilotValue)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym (BaseBVType 64)
    Expr t (BaseBVType 64)
    e
      XWord8 SymExpr sym (BaseBVType 8)
    e -> CopilotValue Word8 -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue Word8 -> Some CopilotValue)
    -> (BV 8 -> CopilotValue Word8) -> BV 8 -> Some CopilotValue
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type Word8 -> Word8 -> CopilotValue Word8
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue Type Word8
    CT.Word8 (Word8 -> CopilotValue Word8)
    -> (BV 8 -> Word8) -> BV 8 -> CopilotValue Word8
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV 8 -> Word8
    forall a (w :: Nat). Num a => BV w -> a
    fromBV (BV 8 -> Some CopilotValue) -> IO (BV 8) -> IO (Some CopilotValue)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym (BaseBVType 8)
    Expr t (BaseBVType 8)
    e
      XWord16 SymExpr sym (BaseBVType 16)
    e -> CopilotValue Word16 -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue Word16 -> Some CopilotValue)
    -> (BV 16 -> CopilotValue Word16) -> BV 16 -> Some CopilotValue
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type Word16 -> Word16 -> CopilotValue Word16
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue Type Word16
    CT.Word16 (Word16 -> CopilotValue Word16)
    -> (BV 16 -> Word16) -> BV 16 -> CopilotValue Word16
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV 16 -> Word16
    forall a (w :: Nat). Num a => BV w -> a
    fromBV (BV 16 -> Some CopilotValue)
    -> IO (BV 16) -> IO (Some CopilotValue)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym (BaseBVType 16)
    Expr t (BaseBVType 16)
    e
      XWord32 SymExpr sym (BaseBVType 32)
    e -> CopilotValue Word32 -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue Word32 -> Some CopilotValue)
    -> (BV 32 -> CopilotValue Word32) -> BV 32 -> Some CopilotValue
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type Word32 -> Word32 -> CopilotValue Word32
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue Type Word32
    CT.Word32 (Word32 -> CopilotValue Word32)
    -> (BV 32 -> Word32) -> BV 32 -> CopilotValue Word32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV 32 -> Word32
    forall a (w :: Nat). Num a => BV w -> a
    fromBV (BV 32 -> Some CopilotValue)
    -> IO (BV 32) -> IO (Some CopilotValue)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym (BaseBVType 32)
    Expr t (BaseBVType 32)
    e
      XWord64 SymExpr sym (BaseBVType 64)
    e -> CopilotValue Word64 -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue Word64 -> Some CopilotValue)
    -> (BV 64 -> CopilotValue Word64) -> BV 64 -> Some CopilotValue
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type Word64 -> Word64 -> CopilotValue Word64
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue Type Word64
    CT.Word64 (Word64 -> CopilotValue Word64)
    -> (BV 64 -> Word64) -> BV 64 -> CopilotValue Word64
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV 64 -> Word64
    forall a (w :: Nat). Num a => BV w -> a
    fromBV (BV 64 -> Some CopilotValue)
    -> IO (BV 64) -> IO (Some CopilotValue)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym (BaseBVType 64)
    Expr t (BaseBVType 64)
    e
      XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
    e ->
        CopilotValue Float -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue Float -> Some CopilotValue)
    -> (Float -> CopilotValue Float) -> Float -> Some CopilotValue
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type Float -> Float -> CopilotValue Float
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue Type Float
    CT.Float (Float -> Some CopilotValue) -> IO Float -> IO (Some CopilotValue)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
          FloatInfoRepr SingleFloat
    -> SymExpr sym (SymInterpretedFloatType sym SingleFloat)
    -> (BigFloat -> Float)
    -> (Rational -> Float)
    -> (forall (w :: Nat). BV w -> Float)
    -> IO Float
    forall (fi :: FloatInfo) r.
    FloatInfoRepr fi
    -> SymExpr sym (SymInterpretedFloatType sym fi)
    -> (BigFloat -> r)
    -> (Rational -> r)
    -> (forall (w :: Nat). BV w -> r)
    -> IO r
    iFloatGroundEval FloatInfoRepr SingleFloat
    WFP.SingleFloatRepr SymExpr sym (SymInterpretedFloatType sym SingleFloat)
    e
                           (Double -> Float
    forall a b. (Real a, Fractional b) => a -> b
    realToFrac (Double -> Float) -> (BigFloat -> Double) -> BigFloat -> Float
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Double, Status) -> Double
    forall a b. (a, b) -> a
    fst ((Double, Status) -> Double)
    -> (BigFloat -> (Double, Status)) -> BigFloat -> Double
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RoundMode -> BigFloat -> (Double, Status)
    bfToDouble RoundMode
    NearEven)
                           Rational -> Float
    forall a. Fractional a => Rational -> a
    fromRational
                           (Word32 -> Float
    castWord32ToFloat (Word32 -> Float) -> (BV w -> Word32) -> BV w -> Float
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Word32
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Word32) -> (BV w -> Integer) -> BV w -> Word32
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned)
      XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
    e ->
        CopilotValue Double -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue Double -> Some CopilotValue)
    -> (Double -> CopilotValue Double) -> Double -> Some CopilotValue
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type Double -> Double -> CopilotValue Double
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue Type Double
    CT.Double (Double -> Some CopilotValue)
    -> IO Double -> IO (Some CopilotValue)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
          FloatInfoRepr DoubleFloat
    -> SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
    -> (BigFloat -> Double)
    -> (Rational -> Double)
    -> (forall (w :: Nat). BV w -> Double)
    -> IO Double
    forall (fi :: FloatInfo) r.
    FloatInfoRepr fi
    -> SymExpr sym (SymInterpretedFloatType sym fi)
    -> (BigFloat -> r)
    -> (Rational -> r)
    -> (forall (w :: Nat). BV w -> r)
    -> IO r
    iFloatGroundEval FloatInfoRepr DoubleFloat
    WFP.DoubleFloatRepr SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
    e
                           ((Double, Status) -> Double
    forall a b. (a, b) -> a
    fst ((Double, Status) -> Double)
    -> (BigFloat -> (Double, Status)) -> BigFloat -> Double
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RoundMode -> BigFloat -> (Double, Status)
    bfToDouble RoundMode
    NearEven)
                           Rational -> Double
    forall a. Fractional a => Rational -> a
    fromRational
                           (Word64 -> Double
    castWord64ToDouble (Word64 -> Double) -> (BV w -> Word64) -> BV w -> Double
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Integer -> Word64
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Word64) -> (BV w -> Integer) -> BV w -> Word64
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned)
      XEmptyArray Type t
    tp ->
        Some CopilotValue -> IO (Some CopilotValue)
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Some CopilotValue -> IO (Some CopilotValue))
    -> Some CopilotValue -> IO (Some CopilotValue)
    forall a b. (a -> b) -> a -> b
    $ CopilotValue (Array 0 t) -> Some CopilotValue
    forall k (f :: k -> *) (x :: k). f x -> Some f
    Some (CopilotValue (Array 0 t) -> Some CopilotValue)
    -> CopilotValue (Array 0 t) -> Some CopilotValue
    forall a b. (a -> b) -> a -> b
    $ Type (Array 0 t) -> Array 0 t -> CopilotValue (Array 0 t)
    forall a. Typed a => Type a -> a -> CopilotValue a
    CopilotValue (forall (n :: Nat) t.
    (KnownNat n, Typed t) =>
    Type t -> Type (Array n t)
    CT.Array @0 Type t
    tp) ([t] -> Array 0 t
    forall (n :: Nat) t. KnownNat n => [t] -> Array n t
    CTA.array [])
      XArray Vector n (XExpr sym)
    es -> do
        (someCVs :: V.Vector n (Some CopilotValue)) <- (XExpr sym -> IO (Some CopilotValue))
    -> Vector n (XExpr sym) -> IO (Vector n (Some CopilotValue))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Vector n a -> f (Vector n b)
    traverse (GroundEvalFn t -> XExpr sym -> IO (Some CopilotValue)
    forall sym t (st :: * -> *) (fm :: FloatMode).
    (sym ~ ExprBuilder t st (Flags fm), KnownRepr FloatModeRepr fm) =>
    GroundEvalFn t -> XExpr sym -> IO (Some CopilotValue)
    valFromExpr GroundEvalFn t
    ge) Vector n (XExpr sym)
    es
        (Some (CopilotValue headTp _headVal), _) <- pure $ V.uncons someCVs
        cvs <-
          traverse
            (\(Some (CopilotValue Type x
    tp x
    val)) ->
              case Type x
    tp Type x -> Type x -> Maybe (x :~: x)
    forall a b. Type a -> Type b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    `testEquality` Type x
    headTp of
                Just x :~: x
    Refl -> x -> IO x
    forall a. a -> IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure x
    x
    val
                Maybe (x :~: x)
    Nothing -> [String] -> IO x
    forall (m :: * -> *) a.
    (HasCallStack, MonadIO m) =>
    [String] -> m a
    panic [ String
    "XArray with mismatched element types"
                                 , Type x -> String
    forall a. Show a => a -> String
    show Type x
    tp
                                 , Type x -> String
    forall a. Show a => a -> String
    show Type x
    headTp
                                 ])
            someCVs
        pure $ Some $ CopilotValue (CT.Array @n headTp) (CTA.array (V.toList cvs))
      XStruct [XExpr sym]
    _ -> String -> IO (Some CopilotValue)
    forall a. HasCallStack => String -> a
    error String
    "valFromExpr: Structs not currently handled"
      where
        fromBV :: forall a w . Num a => BV.BV w -> a
        fromBV :: forall a (w :: Nat). Num a => BV w -> a
    fromBV = Integer -> a
    forall a. Num a => Integer -> a
    fromInteger (Integer -> a) -> (BV w -> Integer) -> BV w -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BV w -> Integer
    forall (w :: Nat). BV w -> Integer
    BV.asUnsigned

        -- Evaluate a (possibly symbolic) floating-point value to a concrete result.
        -- Depending on which @what4@ floating-point mode is in use, the result will
        -- be passed to one of three different continuation arguments.
        iFloatGroundEval ::
          forall fi r.
          WFP.FloatInfoRepr fi ->
          WI.SymExpr sym (WFP.SymInterpretedFloatType sym fi) ->
          (BigFloat -> r) ->
          -- ^ Continuation to use if the IEEE floating-point mode is in use.
          (Rational -> r) ->
          -- ^ Continuation to use if the real floating-point mode is in use.
          (forall w. BV.BV w -> r) ->
          -- ^ Continuation to use if the uninterpreted floating-point mode is in
          -- use.
          IO r
        iFloatGroundEval :: forall (fi :: FloatInfo) r.
    FloatInfoRepr fi
    -> SymExpr sym (SymInterpretedFloatType sym fi)
    -> (BigFloat -> r)
    -> (Rational -> r)
    -> (forall (w :: Nat). BV w -> r)
    -> IO r
    iFloatGroundEval FloatInfoRepr fi
    _ SymExpr sym (SymInterpretedFloatType sym fi)
    e BigFloat -> r
    ieeeK Rational -> r
    realK forall (w :: Nat). BV w -> r
    uninterpK =
          case FloatModeRepr fm
    forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
    WI.knownRepr :: WB.FloatModeRepr fm of
            FloatModeRepr fm
    WB.FloatIEEERepr          -> BigFloat -> r
    ieeeK (BigFloat -> r) -> IO BigFloat -> IO r
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym (SymInterpretedFloatType sym fi)
    Expr t (BaseFloatType (FloatInfoToPrecision fi))
    e
            FloatModeRepr fm
    WB.FloatRealRepr          -> Rational -> r
    realK (Rational -> r) -> IO Rational -> IO r
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym (SymInterpretedFloatType sym fi)
    Expr t BaseRealType
    e
            FloatModeRepr fm
    WB.FloatUninterpretedRepr -> BV (FloatInfoToBitWidth fi) -> r
    forall (w :: Nat). BV w -> r
    uninterpK (BV (FloatInfoToBitWidth fi) -> r)
    -> IO (BV (FloatInfoToBitWidth fi)) -> IO r
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    forall t.
    GroundEvalFn t
    -> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
    WG.groundEval GroundEvalFn t
    ge SymExpr sym (SymInterpretedFloatType sym fi)
    Expr t (BaseBVType (FloatInfoToBitWidth fi))
    e