{-# 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
(
prove
, Solver(..)
, SatResult(..)
, computeBisimulationProofBundle
, BisimulationProofBundle(..)
, BisimulationProofState(..)
, 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.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
data BuilderState a = EmptyState
data Solver = CVC4 | DReal | Yices | Z3
data SatResult = Valid | Invalid | Unknown
deriving Int -> SatResult -> ShowS
[SatResult] -> ShowS
SatResult -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SatResult] -> ShowS
$cshowList :: [SatResult] -> ShowS
show :: SatResult -> String
$cshow :: SatResult -> String
showsPrec :: Int -> SatResult -> ShowS
$cshowsPrec :: Int -> SatResult -> ShowS
Show
type CounterExample = [(String, Some CopilotValue)]
prove :: Solver
-> CS.Spec
-> IO [(CE.Name, SatResult)]
prove :: Solver -> Spec -> IO [(String, SatResult)]
prove Solver
solver Spec
spec = do
Some NonceGenerator IO x
ng <- IO (Some (NonceGenerator IO))
newIONonceGenerator
ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym <- forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
WB.newExprBuilder FloatModeRepr 'FloatIEEE
WB.FloatIEEERepr forall a. BuilderState a
EmptyState NonceGenerator IO x
ng
case Solver
solver of
Solver
CVC4 -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.cvc4Options (forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)
Solver
DReal -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.drealOptions (forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)
Solver
Yices -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.yicesOptions (forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)
Solver
Z3 -> [ConfigDesc] -> Config -> IO ()
WC.extendConfig [ConfigDesc]
WS.z3Options (forall sym. IsExprBuilder sym => sym -> Config
WI.getConfiguration ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym)
let bufLen :: Stream -> p
bufLen (CS.Stream Int
_ [a]
buf Expr a
_ Type a
_) = forall i a. Num i => [a] -> i
genericLength [a]
buf
maxBufLen :: Integer
maxBufLen = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Integer
0 forall a. a -> [a] -> [a]
: (forall {p}. Num p => Stream -> p
bufLen forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec -> [Stream]
CS.specStreams Spec
spec))
let proveProperties :: TransM
(ExprBuilder x BuilderState (Flags 'FloatIEEE))
[(String, SatResult)]
proveProperties = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec -> [Property]
CS.specProperties Spec
spec) forall a b. (a -> b) -> a -> b
$ \Property
pr -> do
[Expr x BaseBoolType]
base_cases <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Integer
0 .. Integer
maxBufLen forall a. Num a => a -> a -> a
- Integer
1] forall a b. (a -> b) -> a -> b
$ \Integer
i -> do
XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
xe <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr
(ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
p
XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
_ -> forall (m :: * -> *) sym a.
(HasCallStack, MonadIO m, IsExprBuilder sym) =>
String -> XExpr sym -> m a
expectedBool String
"Property" XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
xe
[Expr x BaseBoolType]
ind_hyps <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Integer
0 .. Integer
maxBufLenforall a. Num a => a -> a -> a
-Integer
1] forall a b. (a -> b) -> a -> b
$ \Integer
i -> do
XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
xe <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr
(ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
hyp
XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
_ -> forall (m :: * -> *) sym a.
(HasCallStack, MonadIO m, IsExprBuilder sym) =>
String -> XExpr sym -> m a
expectedBool String
"Property" XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
xe
Expr x BaseBoolType
ind_goal <- do
XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
xe <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym
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 -> forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr
(ExprBuilder x BuilderState (Flags 'FloatIEEE)) BaseBoolType
p
XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
_ -> forall (m :: * -> *) sym a.
(HasCallStack, MonadIO m, IsExprBuilder sym) =>
String -> XExpr sym -> m a
expectedBool String
"Property" XExpr (ExprBuilder x BuilderState (Flags 'FloatIEEE))
xe
Expr x BaseBoolType
ind_case <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (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
Expr x BaseBoolType
p <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (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
Expr x BaseBoolType
not_p <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall sym. IsExprBuilder sym => sym -> Pred sym -> IO (Pred sym)
WI.notPred ExprBuilder x BuilderState (Flags 'FloatIEEE)
sym Expr x BaseBoolType
p
let clauses :: [Expr x BaseBoolType]
clauses = [Expr x BaseBoolType
not_p]
case Solver
solver of
Solver
CVC4 -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ \case
WS.Sat (GroundEvalFn x
_ge, Maybe (ExprRangeBindings x)
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
WS.Unsat ()
_ -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
Solver
DReal -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ \case
WS.Sat (WriterConn x (Writer DReal)
_ge, DRealBindings
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
WS.Unsat ()
_ -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
Solver
Yices -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ \case
WS.Sat GroundEvalFn x
_ge -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
WS.Unsat ()
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Valid)
SatResult (GroundEvalFn x) ()
WS.Unknown -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
Solver
Z3 -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ \case
WS.Sat (GroundEvalFn x
_ge, Maybe (ExprRangeBindings x)
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Invalid)
WS.Unsat ()
_ -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> String
CS.propertyName Property
pr, SatResult
Unknown)
forall sym a. Spec -> TransM sym a -> IO a
runTransM Spec
spec TransM
(ExprBuilder x BuilderState (Flags 'FloatIEEE))
[(String, SatResult)]
proveProperties
computeBisimulationProofBundle ::
WFP.IsInterpretedFloatSymExprBuilder sym
=> sym
-> [String]
-> CS.Spec
-> 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 <- forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Spec -> IO (BisimulationProofState sym)
computeInitialStreamState sym
sym Spec
spec
forall sym a. Spec -> TransM sym a -> IO a
runTransM Spec
spec forall a b. (a -> b) -> a -> b
$ do
BisimulationProofState sym
prestate <- forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Spec -> TransM sym (BisimulationProofState sym)
computePrestate sym
sym Spec
spec
BisimulationProofState sym
poststate <- forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Spec -> TransM sym (BisimulationProofState sym)
computePoststate sym
sym Spec
spec
[(String, SymExpr sym BaseBoolType, [(Some Type, XExpr sym)])]
triggers <- forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> Spec
-> TransM sym [(String, Pred sym, [(Some Type, XExpr sym)])]
computeTriggerState sym
sym Spec
spec
[SymExpr sym BaseBoolType]
assms <- forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> [String] -> Spec -> TransM sym [Pred sym]
computeAssumptions sym
sym [String]
properties Spec
spec
[(String, Some Type, XExpr sym)]
externs <- forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> TransM sym [(String, Some Type, XExpr sym)]
computeExternalInputs sym
sym
[SymExpr sym BaseBoolType]
sideCnds <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall sym. TransState sym -> [Pred sym]
sidePreds
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
}
data BisimulationProofBundle sym =
BisimulationProofBundle
{ forall sym.
BisimulationProofBundle sym -> BisimulationProofState sym
initialStreamState :: BisimulationProofState sym
, forall sym.
BisimulationProofBundle sym -> BisimulationProofState sym
preStreamState :: BisimulationProofState sym
, forall sym.
BisimulationProofBundle sym -> BisimulationProofState sym
postStreamState :: BisimulationProofState sym
, forall sym.
BisimulationProofBundle sym -> [(String, Some Type, XExpr sym)]
externalInputs :: [(CE.Name, Some CT.Type, XExpr sym)]
, forall sym.
BisimulationProofBundle sym
-> [(String, Pred sym, [(Some Type, XExpr sym)])]
triggerState :: [(CE.Name, WI.Pred sym, [(Some CT.Type, XExpr sym)])]
, forall sym. BisimulationProofBundle sym -> [Pred sym]
assumptions :: [WI.Pred sym]
, forall sym. BisimulationProofBundle sym -> [Pred sym]
sideConds :: [WI.Pred sym]
}
newtype BisimulationProofState sym =
BisimulationProofState
{ forall sym.
BisimulationProofState sym -> [(Int, Some Type, [XExpr sym])]
streamState :: [(CE.Id, Some CT.Type, [XExpr sym])]
}
computeInitialStreamState ::
WFP.IsInterpretedFloatSymExprBuilder sym
=> sym
-> CS.Spec
-> 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec -> [Stream]
CS.specStreams Spec
spec) 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym a.
IsInterpretedFloatExprBuilder sym =>
sym -> Type a -> a -> IO (XExpr sym)
translateConstExpr sym
sym Type a
tp) [a]
buf
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nm, forall k (f :: k -> *) (x :: k). f x -> Some f
Some Type a
tp, [XExpr sym]
vs)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym.
[(Int, Some Type, [XExpr sym])] -> BisimulationProofState sym
BisimulationProofState [(Int, Some Type, [XExpr sym])]
xs)
computePrestate ::
WFP.IsInterpretedFloatSymExprBuilder sym
=> sym
-> CS.Spec
-> 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec -> [Stream]
CS.specStreams Spec
spec) 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 = forall i a. Num i => [a] -> i
genericLength [a]
buf
let idxes :: [StreamOffset]
idxes = Integer -> StreamOffset
RelativeOffset forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
0 .. Integer
buflenforall a. Num a => a -> a -> a
-Integer
1]
[XExpr sym]
vs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Int -> StreamOffset -> TransM sym (XExpr sym)
getStreamValue sym
sym Int
nm) [StreamOffset]
idxes
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nm, forall k (f :: k -> *) (x :: k). f x -> Some f
Some Type a
tp, [XExpr sym]
vs)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym.
[(Int, Some Type, [XExpr sym])] -> BisimulationProofState sym
BisimulationProofState [(Int, Some Type, [XExpr sym])]
xs)
computePoststate ::
WFP.IsInterpretedFloatSymExprBuilder sym
=> sym
-> CS.Spec
-> 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec -> [Stream]
CS.specStreams Spec
spec) 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 = forall i a. Num i => [a] -> i
genericLength [a]
buf
let idxes :: [StreamOffset]
idxes = Integer -> StreamOffset
RelativeOffset forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
1 .. Integer
buflen]
[XExpr sym]
vs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> Int -> StreamOffset -> TransM sym (XExpr sym)
getStreamValue sym
sym Int
nm) [StreamOffset]
idxes
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nm, forall k (f :: k -> *) (x :: k). f x -> Some f
Some Type a
tp, [XExpr sym]
vs)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall sym.
[(Int, Some Type, [XExpr sym])] -> BisimulationProofState sym
BisimulationProofState [(Int, Some Type, [XExpr sym])]
xs)
computeTriggerState ::
WFP.IsInterpretedFloatSymExprBuilder sym
=> sym
-> CS.Spec
-> 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 = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Spec -> [Trigger]
CS.specTriggers Spec
spec) 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 <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
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' -> forall (m :: * -> *) a. Monad m => a -> m a
return Pred sym
guard'
XExpr 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' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM UExpr -> TransM sym (Some Type, XExpr sym)
computeArg [UExpr]
args
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 <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
sym forall a. Monoid a => a
mempty Expr a
ex (Integer -> StreamOffset
RelativeOffset Integer
0)
forall (m :: * -> *) a. Monad m => a -> m a
return (forall k (f :: k -> *) (x :: k). f x -> Some f
Some Type a
tp, XExpr sym
v)
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 <- forall k a. Map k a -> [(k, a)]
Map.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall sym. TransState sym -> Map String (Some Type)
mentionedExternals
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(String, Some Type)]
exts forall a b. (a -> b) -> a -> b
$ \(String
nm, Some Type x
tp) -> do
XExpr sym
v <- 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)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
nm, forall k (f :: k -> *) (x :: k). f x -> Some f
Some Type x
tp, XExpr sym
v)
computeAssumptions ::
forall sym.
WFP.IsInterpretedFloatSymExprBuilder sym
=> sym
-> [String]
-> CS.Spec
-> TransM sym [WI.Pred sym]
computeAssumptions :: forall sym.
IsInterpretedFloatSymExprBuilder sym =>
sym -> [String] -> Spec -> TransM sym [Pred sym]
computeAssumptions sym
sym [String]
properties Spec
spec =
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
_) = forall i a. Num i => [a] -> i
genericLength [a]
buf
maxBufLen :: Integer
maxBufLen = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Integer
0 forall a. a -> [a] -> [a]
: (forall {p}. Num p => Stream -> p
bufLen forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Spec -> [Stream]
CS.specStreams Spec
spec))
specPropertyExprs :: [CE.Expr Bool]
specPropertyExprs :: [Expr Bool]
specPropertyExprs =
[ Property -> Expr Bool
CS.propertyExpr Property
p
| Property
p <- Spec -> [Property]
CS.specProperties Spec
spec
, forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Property -> String
CS.propertyName Property
p) [String]
properties
]
computeAssumption :: CE.Expr Bool -> TransM sym [WI.Pred sym]
computeAssumption :: Expr Bool -> TransM sym [SymExpr sym BaseBoolType]
computeAssumption Expr Bool
e = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Integer
0 .. Integer
maxBufLen] forall a b. (a -> b) -> a -> b
$ \Integer
i -> do
XExpr sym
xe <- forall sym a.
IsInterpretedFloatSymExprBuilder sym =>
sym
-> LocalEnv sym -> Expr a -> StreamOffset -> TransM sym (XExpr sym)
translateExpr sym
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 -> forall (m :: * -> *) a. Monad m => a -> m a
return SymExpr sym BaseBoolType
b
XExpr sym
_ -> forall (m :: * -> *) sym a.
(HasCallStack, MonadIO m, IsExprBuilder sym) =>
String -> XExpr sym -> m a
expectedBool String
"Property" XExpr sym
xe
expectedBool :: forall m sym a.
(Panic.HasCallStack, MonadIO m, WI.IsExprBuilder sym)
=> String
-> 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 =
forall (m :: * -> *) a.
(HasCallStack, MonadIO m) =>
[String] -> m a
panic [String
what forall a. [a] -> [a] -> [a]
++ String
" expected to have boolean result", 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 -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Bool
CT.Bool forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym BaseBoolType
e
XInt8 SymExpr sym (BaseBVType 8)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int8
CT.Int8 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Nat). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym (BaseBVType 8)
e
XInt16 SymExpr sym (BaseBVType 16)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int16
CT.Int16 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Nat). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym (BaseBVType 16)
e
XInt32 SymExpr sym (BaseBVType 32)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int32
CT.Int32 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Nat). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym (BaseBVType 32)
e
XInt64 SymExpr sym (BaseBVType 64)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Int64
CT.Int64 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Nat). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym (BaseBVType 64)
e
XWord8 SymExpr sym (BaseBVType 8)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word8
CT.Word8 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Nat). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym (BaseBVType 8)
e
XWord16 SymExpr sym (BaseBVType 16)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word16
CT.Word16 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Nat). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym (BaseBVType 16)
e
XWord32 SymExpr sym (BaseBVType 32)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word32
CT.Word32 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Nat). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym (BaseBVType 32)
e
XWord64 SymExpr sym (BaseBVType 64)
e -> forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Word64
CT.Word64 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (w :: Nat). Num a => BV w -> a
fromBV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym (BaseBVType 64)
e
XFloat SymExpr sym (SymInterpretedFloatType sym SingleFloat)
e ->
forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Float
CT.Float forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
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
(forall a b. (Real a, Fractional b) => a -> b
realToFrac forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. RoundMode -> BigFloat -> (Double, Status)
bfToDouble RoundMode
NearEven)
forall a. Fractional a => Rational -> a
fromRational
(Word32 -> Float
castWord32ToFloat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Nat). BV w -> Integer
BV.asUnsigned)
XDouble SymExpr sym (SymInterpretedFloatType sym DoubleFloat)
e ->
forall k (f :: k -> *) (x :: k). f x -> Some f
Some forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Type a -> a -> CopilotValue a
CopilotValue Type Double
CT.Double forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
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
(forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. RoundMode -> BigFloat -> (Double, Status)
bfToDouble RoundMode
NearEven)
forall a. Fractional a => Rational -> a
fromRational
(Word64 -> Double
castWord64ToDouble forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Nat). BV w -> Integer
BV.asUnsigned)
XExpr sym
_ -> 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 = forall a. Num a => Integer -> a
fromInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Nat). BV w -> Integer
BV.asUnsigned
iFloatGroundEval ::
forall fi r.
WFP.FloatInfoRepr fi ->
WI.SymExpr sym (WFP.SymInterpretedFloatType sym fi) ->
(BigFloat -> r) ->
(Rational -> r) ->
(forall w. BV.BV w -> r) ->
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 forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
WI.knownRepr :: WB.FloatModeRepr fm of
FloatModeRepr fm
WB.FloatIEEERepr -> BigFloat -> r
ieeeK forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym (SymInterpretedFloatType sym fi)
e
FloatModeRepr fm
WB.FloatRealRepr -> Rational -> r
realK forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym (SymInterpretedFloatType sym fi)
e
FloatModeRepr fm
WB.FloatUninterpretedRepr -> forall (w :: Nat). BV w -> r
uninterpK forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t.
GroundEvalFn t
-> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
WG.groundEval GroundEvalFn t
ge SymExpr sym (SymInterpretedFloatType sym fi)
e