{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures             #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiWayIf                 #-}
{-# LANGUAGE PatternSynonyms            #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TupleSections              #-}
{-# 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.
module Copilot.Theorem.What4
  ( -- * Proving properties about Copilot specifications
    prove
  , Solver(..)
  , SatResult(..)
    -- * Bisimulation proofs about @copilot-c99@ code
  , computeBisimulationProofBundle
  , BisimulationProofBundle(..)
  , BisimulationProofState(..)
    -- * What4 representations of Copilot expressions
  , XExpr(..)
  ) where

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

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.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.NatRepr
import Data.Parameterized.Nonce
import Data.Parameterized.Some
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

type CounterExample = [(String, Some CopilotValue)]

-- | 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.
prove :: Solver
      -- ^ Solver to use
      -> CS.Spec
      -- ^ Spec
      -> IO [(CE.Name, SatResult)]
prove :: Solver -> Spec -> IO [(String, SatResult)]
prove Solver
solver Spec
spec = do
  -- Setup symbolic backend
  Some NonceGenerator IO x
ng <- IO (Some (NonceGenerator IO))
newIONonceGenerator
  ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym <- FloatModeRepr 'FloatIEEE
-> BuilderState x
-> NonceGenerator IO x
-> IO (ExprBuilder x BuilderState (Flags 'FloatIEEE))
forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
WB.newExprBuilder FloatModeRepr 'FloatIEEE
WB.FloatIEEERepr BuilderState x
forall a. BuilderState a
EmptyState NonceGenerator IO x
ng

  -- Solver-specific options
  case Solver
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 :: 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))

  -- This process performs k-induction where we use @k = maxBufLen@.
  -- The choice for @k@ is heuristic, but often effective.
  let proveProperties :: TransM
  (ExprBuilder x BuilderState (Flags 'FloatIEEE))
  [(String, SatResult)]
proveProperties = [Property]
-> (Property
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         (String, SatResult))
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE))
     [(String, SatResult)]
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, SatResult))
 -> TransM
      (ExprBuilder x BuilderState (Flags 'FloatIEEE))
      [(String, SatResult)])
-> (Property
    -> TransM
         (ExprBuilder x BuilderState (Flags 'FloatIEEE))
         (String, SatResult))
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE))
     [(String, SatResult)]
forall a b. (a -> b) -> a -> b
$ \Property
pr -> do
        -- State the base cases for k induction.
        [Expr x BaseBoolType]
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
          XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
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 (Property -> Expr Bool
CS.propertyExpr Property
pr) (Integer -> StreamOffset
AbsoluteOffset Integer
i)
          case XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
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
        [Expr x BaseBoolType]
ind_hyps <- [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
maxBufLenInteger -> 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
          XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
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 (Property -> Expr Bool
CS.propertyExpr Property
pr) (Integer -> StreamOffset
RelativeOffset Integer
i)
          case XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
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
        Expr x BaseBoolType
ind_goal <- do
          XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
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
                              (Property -> Expr Bool
CS.propertyExpr Property
pr)
                              (Integer -> StreamOffset
RelativeOffset Integer
maxBufLen)
          case XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
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)
        Expr x BaseBoolType
ind_case <- IO (Expr x BaseBoolType)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE))
     (Expr x BaseBoolType)
forall a.
IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Expr x BaseBoolType)
 -> TransM
      (ExprBuilder x BuilderState (Flags 'FloatIEEE))
      (Expr x BaseBoolType))
-> IO (Expr x BaseBoolType)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE))
     (Expr x BaseBoolType)
forall a b. (a -> b) -> a -> b
$ (Expr x BaseBoolType
 -> Expr x BaseBoolType -> IO (Expr x BaseBoolType))
-> Expr x BaseBoolType
-> [Expr x BaseBoolType]
-> IO (Expr x BaseBoolType)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> SymExpr
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
-> SymExpr
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
-> IO
     (SymExpr
        (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.impliesPred ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym) Expr x BaseBoolType
ind_goal [Expr x BaseBoolType]
ind_hyps

        -- Compute the conjunction of the base and inductive cases
        Expr x BaseBoolType
p <- IO (Expr x BaseBoolType)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE))
     (Expr x BaseBoolType)
forall a.
IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Expr x BaseBoolType)
 -> TransM
      (ExprBuilder x BuilderState (Flags 'FloatIEEE))
      (Expr x BaseBoolType))
-> IO (Expr x BaseBoolType)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE))
     (Expr x BaseBoolType)
forall a b. (a -> b) -> a -> b
$ (Expr x BaseBoolType
 -> Expr x BaseBoolType -> IO (Expr x BaseBoolType))
-> Expr x BaseBoolType
-> [Expr x BaseBoolType]
-> IO (Expr x BaseBoolType)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> SymExpr
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
-> SymExpr
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
-> IO
     (SymExpr
        (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType)
forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> IO (Pred sym)
WI.andPred ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym) Expr x BaseBoolType
ind_case [Expr x BaseBoolType]
base_cases

        -- Negate the goals for for SAT search
        Expr x BaseBoolType
not_p <- IO (Expr x BaseBoolType)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE))
     (Expr x BaseBoolType)
forall a.
IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Expr x BaseBoolType)
 -> TransM
      (ExprBuilder x BuilderState (Flags 'FloatIEEE))
      (Expr x BaseBoolType))
-> IO (Expr x BaseBoolType)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE))
     (Expr x BaseBoolType)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> SymExpr
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
-> IO
     (SymExpr
        (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType)
forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym SymExpr
  (ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
Expr x BaseBoolType
p
        let clauses :: [Expr x BaseBoolType]
clauses = [Expr x BaseBoolType
not_p]

        case Solver
solver of
          Solver
CVC4 -> IO (String, SatResult)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) (String, SatResult)
forall a.
IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult)
 -> TransM
      (ExprBuilder x BuilderState (Flags 'FloatIEEE))
      (String, SatResult))
-> IO (String, SatResult)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
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 (String, SatResult))
 -> IO (String, SatResult))
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat (GroundEvalFn x
_ge, Maybe (ExprRangeBindings x)
_) -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
          Solver
DReal -> IO (String, SatResult)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) (String, SatResult)
forall a.
IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult)
 -> TransM
      (ExprBuilder x BuilderState (Flags 'FloatIEEE))
      (String, SatResult))
-> IO (String, SatResult)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (WriterConn x (Writer DReal), DRealBindings) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
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 (String, SatResult))
 -> IO (String, SatResult))
-> (SatResult (WriterConn x (Writer DReal), DRealBindings) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat (WriterConn x (Writer DReal)
_ge, DRealBindings
_) -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (WriterConn x (Writer DReal), DRealBindings) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
          Solver
Yices -> IO (String, SatResult)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) (String, SatResult)
forall a.
IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult)
 -> TransM
      (ExprBuilder x BuilderState (Flags 'FloatIEEE))
      (String, SatResult))
-> IO (String, SatResult)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (GroundEvalFn x) () -> IO (String, SatResult))
-> IO (String, SatResult)
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 (String, SatResult))
 -> IO (String, SatResult))
-> (SatResult (GroundEvalFn x) () -> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat GroundEvalFn x
_ge -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (GroundEvalFn x) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
          Solver
Z3 -> IO (String, SatResult)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) (String, SatResult)
forall a.
IO a -> TransM (ExprBuilder x BuilderState (Flags 'FloatIEEE)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (String, SatResult)
 -> TransM
      (ExprBuilder x BuilderState (Flags 'FloatIEEE))
      (String, SatResult))
-> IO (String, SatResult)
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE)) (String, SatResult)
forall a b. (a -> b) -> a -> b
$ ExprBuilder x BuilderState (Flags 'FloatIEEE)
-> LogData
-> [Expr x BaseBoolType]
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
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 (String, SatResult))
 -> IO (String, SatResult))
-> (SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
    -> IO (String, SatResult))
-> IO (String, SatResult)
forall a b. (a -> b) -> a -> b
$ \case
            WS.Sat (GroundEvalFn x
_ge, Maybe (ExprRangeBindings x)
_) -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
            WS.Unsat ()
_ -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
            SatResult (GroundEvalFn x, Maybe (ExprRangeBindings x)) ()
WS.Unknown -> (String, SatResult) -> IO (String, SatResult)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)

  -- Execute the action and return the results for each property
  Spec
-> TransM
     (ExprBuilder x BuilderState (Flags 'FloatIEEE))
     [(String, SatResult)]
-> IO [(String, SatResult)]
forall sym a. Spec -> TransM sym a -> IO a
runTransM Spec
spec TransM
  (ExprBuilder x BuilderState (Flags 'FloatIEEE))
  [(String, SatResult)]
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.
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
  BisimulationProofState sym
iss <- sym -> Spec -> IO (BisimulationProofState sym)
forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Spec -> IO (BisimulationProofState sym)
computeInitialStreamState sym
sym Spec
spec
  Spec
-> TransM sym (BisimulationProofBundle sym)
-> IO (BisimulationProofBundle sym)
forall sym a. Spec -> TransM sym a -> IO a
runTransM Spec
spec (TransM sym (BisimulationProofBundle sym)
 -> IO (BisimulationProofBundle sym))
-> TransM sym (BisimulationProofBundle sym)
-> IO (BisimulationProofBundle sym)
forall a b. (a -> b) -> a -> b
$ do
    BisimulationProofState sym
prestate  <- sym -> Spec -> TransM sym (BisimulationProofState sym)
forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Spec -> TransM sym (BisimulationProofState sym)
computePrestate sym
sym Spec
spec
    BisimulationProofState sym
poststate <- sym -> Spec -> TransM sym (BisimulationProofState sym)
forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Spec -> TransM sym (BisimulationProofState sym)
computePoststate sym
sym Spec
spec
    [(String, SymExpr sym BaseBoolType, [(Some Type, XExpr sym)])]
triggers  <- sym
-> Spec
-> TransM
     sym [(String, SymExpr sym BaseBoolType, [(Some Type, XExpr sym)])]
forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> Spec
-> TransM sym [(String, Pred sym, [(Some Type, XExpr sym)])]
computeTriggerState sym
sym Spec
spec
    [SymExpr sym BaseBoolType]
assms     <- sym -> [String] -> Spec -> TransM sym [SymExpr sym BaseBoolType]
forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> [String] -> Spec -> TransM sym [Pred sym]
computeAssumptions sym
sym [String]
properties Spec
spec
    [(String, Some Type, XExpr sym)]
externs   <- sym -> TransM sym [(String, Some Type, XExpr sym)]
forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> TransM sym [(String, Some Type, XExpr sym)]
computeExternalInputs sym
sym
    [SymExpr sym BaseBoolType]
sideCnds  <- (TransState sym -> [SymExpr sym BaseBoolType])
-> TransM sym [SymExpr sym BaseBoolType]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets TransState sym -> [SymExpr sym BaseBoolType]
forall sym. TransState sym -> [Pred sym]
sidePreds
    BisimulationProofBundle sym
-> TransM sym (BisimulationProofBundle sym)
forall a. a -> TransM sym a
forall (m :: * -> *) a. Monad m => a -> m a
return
      BisimulationProofBundle
        { initialStreamState :: BisimulationProofState sym
initialStreamState = BisimulationProofState sym
iss
        , preStreamState :: BisimulationProofState sym
preStreamState     = BisimulationProofState sym
prestate
        , postStreamState :: BisimulationProofState sym
postStreamState    = BisimulationProofState sym
poststate
        , externalInputs :: [(String, Some Type, XExpr sym)]
externalInputs     = [(String, Some Type, XExpr sym)]
externs
        , triggerState :: [(String, SymExpr sym BaseBoolType, [(Some Type, XExpr sym)])]
triggerState       = [(String, SymExpr sym BaseBoolType, [(Some Type, XExpr sym)])]
triggers
        , assumptions :: [SymExpr sym BaseBoolType]
assumptions        = [SymExpr sym BaseBoolType]
assms
        , sideConds :: [SymExpr sym BaseBoolType]
sideConds          = [SymExpr sym BaseBoolType]
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
  [(Int, Some Type, [XExpr sym])]
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 [XExpr sym]
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
            (Int, Some Type, [XExpr sym]) -> IO (Int, Some Type, [XExpr sym])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nm, Type a -> Some Type
forall k (f :: k -> *) (x :: k). f x -> Some f
Some Type a
tp, [XExpr sym]
vs)
  BisimulationProofState sym -> IO (BisimulationProofState sym)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, Some Type, [XExpr sym])] -> BisimulationProofState sym
forall sym.
[(Int, Some Type, [XExpr sym])] -> BisimulationProofState sym
BisimulationProofState [(Int, Some Type, [XExpr sym])]
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
  [(Int, Some Type, [XExpr sym])]
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]
             [XExpr sym]
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
             (Int, Some Type, [XExpr sym])
-> TransM sym (Int, Some Type, [XExpr sym])
forall a. a -> TransM sym a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nm, Type a -> Some Type
forall k (f :: k -> *) (x :: k). f x -> Some f
Some Type a
tp, [XExpr sym]
vs)
  BisimulationProofState sym
-> TransM sym (BisimulationProofState sym)
forall a. a -> TransM sym a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, Some Type, [XExpr sym])] -> BisimulationProofState sym
forall sym.
[(Int, Some Type, [XExpr sym])] -> BisimulationProofState sym
BisimulationProofState [(Int, Some Type, [XExpr sym])]
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
  [(Int, Some Type, [XExpr sym])]
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]
             [XExpr sym]
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
             (Int, Some Type, [XExpr sym])
-> TransM sym (Int, Some Type, [XExpr sym])
forall a. a -> TransM sym a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nm, Type a -> Some Type
forall k (f :: k -> *) (x :: k). f x -> Some f
Some Type a
tp, [XExpr sym]
vs)
  BisimulationProofState sym
-> TransM sym (BisimulationProofState sym)
forall a. a -> TransM sym a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, Some Type, [XExpr sym])] -> BisimulationProofState sym
forall sym.
[(Int, Some Type, [XExpr sym])] -> BisimulationProofState sym
BisimulationProofState [(Int, Some Type, [XExpr sym])]
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 XExpr sym
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)
         Pred sym
guard' <-
           case XExpr sym
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
         [(Some Type, XExpr sym)]
args' <- (UExpr -> TransM sym (Some Type, XExpr sym))
-> [UExpr] -> TransM sym [(Some Type, 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 UExpr -> TransM sym (Some Type, XExpr sym)
computeArg [UExpr]
args
         (String, Pred sym, [(Some Type, XExpr sym)])
-> TransM sym (String, Pred sym, [(Some Type, XExpr sym)])
forall a. a -> TransM sym a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
nm, Pred sym
guard', [(Some Type, XExpr sym)]
args')
  where
   computeArg :: UExpr -> TransM sym (Some Type, XExpr sym)
computeArg (CE.UExpr { uExprType :: ()
CE.uExprType = Type a
tp, uExprExpr :: ()
CE.uExprExpr = Expr a
ex }) = do
     XExpr sym
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)
     (Some Type, XExpr sym) -> TransM sym (Some Type, XExpr sym)
forall a. a -> TransM sym a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type a -> Some Type
forall k (f :: k -> *) (x :: k). f x -> Some f
Some Type a
tp, XExpr sym
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
  [(String, Some Type)]
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
  [(String, Some Type)]
-> ((String, Some Type)
    -> TransM sym (String, Some Type, XExpr sym))
-> TransM sym [(String, Some Type, XExpr sym)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(String, Some Type)]
exts (((String, Some Type) -> TransM sym (String, Some Type, XExpr sym))
 -> TransM sym [(String, Some Type, XExpr sym)])
-> ((String, Some Type)
    -> TransM sym (String, Some Type, XExpr sym))
-> TransM sym [(String, Some Type, XExpr sym)]
forall a b. (a -> b) -> a -> b
$ \(String
nm, Some Type x
tp) -> do
    XExpr sym
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)
    (String, Some Type, XExpr sym)
-> TransM sym (String, Some Type, XExpr sym)
forall a. a -> TransM sym a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
nm, Type x -> Some Type
forall k (f :: k -> *) (x :: k). f x -> Some f
Some Type x
tp, XExpr sym
v)

-- | Compute the user-provided property assumptions in a Copilot program.
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 =
      [ Property -> Expr Bool
CS.propertyExpr 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
      ]

    -- 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
      XExpr sym
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 XExpr sym
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]

data CopilotValue a = CopilotValue { forall a. CopilotValue a -> Type a
cvType :: CT.Type a
                                   , forall a. CopilotValue a -> a
cvVal :: a
                                   }

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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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)
  XExpr sym
_ -> String -> IO (Some CopilotValue)
forall a. HasCallStack => String -> a
error String
"valFromExpr unhandled case"
  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