-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | k-induction for Copilot.
--   
--   Some tools to prove properties on Copilot programs with k-induction
--   model checking.
--   
--   Copilot is a stream (i.e., infinite lists) domain-specific language
--   (DSL) in Haskell that compiles into embedded C. Copilot contains an
--   interpreter, multiple back-end compilers, and other verification
--   tools.
--   
--   A tutorial, examples, and other information are available at
--   <a>https://copilot-language.github.io</a>.
@package copilot-theorem
@version 4.6.1


-- | Connection to theorem provers.
module Copilot.Theorem.Prove

-- | Output produced by a prover, containing the <a>Status</a> of the proof
--   and additional information.
data Output
Output :: Status -> [String] -> Output

-- | Status returned by a prover when given a specification and a property
--   to prove.
data Status
Sat :: Status
Valid :: Status
Invalid :: Status
Unknown :: Status
Error :: Status

-- | A connection to a prover able to check the satisfiability of
--   specifications.
--   
--   The most important is <a>askProver</a>, which takes 3 arguments :
--   
--   <ul>
--   <li>The prover descriptor</li>
--   <li>A list of properties names which are assumptions</li>
--   <li>A properties that have to be deduced from these assumptions</li>
--   </ul>
data Prover
Prover :: String -> (Spec -> IO r) -> (r -> [PropId] -> [PropId] -> IO Output) -> (r -> IO ()) -> Prover
[proverName] :: Prover -> String
[startProver] :: Prover -> Spec -> IO r
[askProver] :: Prover -> r -> [PropId] -> [PropId] -> IO Output
[closeProver] :: Prover -> r -> IO ()

-- | A unique property identifier
type PropId = String

-- | Reference to a property.
data PropRef a
[PropRef] :: forall a. PropId -> PropRef a

-- | A proof scheme with unit result.
type Proof a = ProofScheme a ()

-- | A sequence of computations that generate a trace of required prover
--   <a>Action</a>s.
type UProof = Writer [Action] ()

-- | A proof scheme is a sequence of computations that compute a result and
--   generate a trace of required prover <a>Action</a>s.
data ProofScheme a b
[Proof] :: forall b a. Writer [Action] b -> ProofScheme a b

-- | Prover actions.
data Action
[Check] :: Prover -> Action
[Assume] :: PropId -> Action
[Admit] :: Action

-- | Empty datatype to mark proofs of universally quantified predicates.
data Universal

-- | Empty datatype to mark proofs of existentially quantified predicates.
data Existential

-- | Record a requirement for satisfiability checking.
check :: Prover -> Proof a

-- | Try to prove a property in a specification with a given proof scheme.
--   
--   Return <a>True</a> if a proof of satisfiability or validity is found,
--   false otherwise.
prove :: Spec -> PropId -> UProof -> IO Bool

-- | Combine two provers producing a new prover that will run both provers
--   in parallel and combine their outputs.
--   
--   The results produced by the provers must be consistent. For example,
--   if one of the provers indicates that a property is <a>Valid</a> while
--   another indicates that it is <a>Invalid</a>, the combination of both
--   provers will return an <a>Error</a>.
combine :: Prover -> Prover -> Prover
instance GHC.Internal.Base.Applicative (Copilot.Theorem.Prove.ProofScheme a)
instance GHC.Internal.Base.Functor (Copilot.Theorem.Prove.ProofScheme a)
instance GHC.Internal.Base.Monad (Copilot.Theorem.Prove.ProofScheme a)


-- | Connections to various SMT solvers and theorem provers.
module Copilot.Theorem.Prover.SMT

-- | Backend to an SMT solver or theorem prover.
data Backend a

-- | Format of SMT-Lib commands.
class Show a => SmtFormat a

-- | Type used to represent SMT-lib commands.
--   
--   Use the interface in <a>SmtFormat</a> to create such commands.
data SmtLib

-- | Type used to represent TPTP expressions.
--   
--   Although this type implements the <a>SmtFormat</a> interface, only
--   <a>assert</a> is actually used.
data Tptp

-- | Backend to the Yices 2 SMT solver.
--   
--   It enables non-linear arithmetic (<tt>QF_NRA</tt>), which means MCSat
--   will be used.
--   
--   The command <tt>yices-smt2</tt> must be in the user's <tt>PATH</tt>.
yices :: Backend SmtLib

-- | Backend to the dReal SMT solver.
--   
--   It enables non-linear arithmetic (<tt>QF_NRA</tt>).
--   
--   The libraries for dReal must be installed and <tt>perl</tt> must be in
--   the user's <tt>PATH</tt>.
dReal :: Backend SmtLib

-- | Backend to the Alt-Ergo SMT solver.
--   
--   It enables support for uninterpreted functions and mixed nonlinear
--   arithmetic (<tt>QF_NIRA</tt>).
--   
--   The command <tt>alt-ergo.opt</tt> must be in the user's <tt>PATH</tt>.
altErgo :: Backend SmtLib

-- | Backend to the MetiTaski theorem prover.
--   
--   The command <tt>metit</tt> must be in the user's <tt>PATH</tt>.
--   
--   The argument string is the path to the <tt>tptp</tt> subdirectory of
--   the metitarski install location.
metit :: String -> Backend Tptp

-- | Backend to the Z3 theorem prover.
--   
--   The command <tt>z3</tt> must be in the user's <tt>PATH</tt>.
z3 :: Backend SmtLib

-- | Backend to the cvc4 SMT solver.
--   
--   It enables support for uninterpreted functions and mixed nonlinear
--   arithmetic (<tt>QF_NIRA</tt>).
--   
--   The command <tt>cvc4</tt> must be in the user's <tt>PATH</tt>.
cvc4 :: Backend SmtLib

-- | Backend to the Mathsat SMT solver.
--   
--   It enables non-linear arithmetic (<tt>QF_NRA</tt>).
--   
--   The command <tt>mathsat</tt> must be in the user's <tt>PATH</tt>.
mathsat :: Backend SmtLib

-- | Options to configure the provers.
data Options
Options :: Word32 -> Word32 -> Bool -> Options

-- | Initial <tt>k</tt> for the k-induction algorithm.
[startK] :: Options -> Word32

-- | The maximum number of steps of the k-induction algorithm the prover
--   runs before giving up.
[maxK] :: Options -> Word32

-- | If <tt>debug</tt> is set to <tt>True</tt>, the SMTLib/TPTP queries
--   produced by the prover are displayed in the standard output.
[debug] :: Options -> Bool

-- | Tactic to find a proof by standard 1-induction.
--   
--   The values for <tt>startK</tt> and <tt>maxK</tt> in the options are
--   ignored.
induction :: SmtFormat a => Options -> Backend a -> Proof Universal

-- | Tactic to find a proof by k-induction.
kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal

-- | Tactic to find only a proof of satisfiability.
onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential

-- | Tactic to find only a proof of validity.
onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal
instance Data.Default.Internal.Default Copilot.Theorem.Prover.SMT.Options
instance GHC.Classes.Eq Copilot.Theorem.Prover.SMT.SolverId
instance GHC.Classes.Ord Copilot.Theorem.Prover.SMT.SolverId
instance GHC.Internal.Show.Show Copilot.Theorem.Prover.SMT.SolverId


-- | Highly automated proof techniques are a necessary step for the
--   widespread adoption of formal methods in the software industry.
--   Moreover, it could provide a partial answer to one of its main issue
--   which is scalability.
--   
--   Copilot-theorem is a Copilot library aimed at checking automatically
--   some safety properties on Copilot programs. It includes:
--   
--   <ul>
--   <li>A prover producing native inputs for the Kind2 model checker.</li>
--   <li>A What4 backend that uses SMT solvers to prove safety
--   properties.</li>
--   </ul>
module Copilot.Theorem

-- | Instantiate a universal proof into an existential proof.
instantiate :: Proof Universal -> Proof Existential

-- | Assume that a property, given by reference, holds.
assume :: PropRef Universal -> Proof a

-- | Assume that the current goal holds.
admit :: Proof a

-- | A proof scheme with unit result.
type Proof a = ProofScheme a ()

-- | A unique property identifier
type PropId = String

-- | Reference to a property.
data PropRef a

-- | Empty datatype to mark proofs of universally quantified predicates.
data Universal

-- | Empty datatype to mark proofs of existentially quantified predicates.
data Existential


-- | A prover backend based on Kind2.
module Copilot.Theorem.Kind2.Prover

-- | Options for Kind2
data Options
Options :: Int -> Options

-- | Upper bound on the number of unrolling that base and step will
--   perform. A value of 0 means <i>unlimited</i>.
[bmcMax] :: Options -> Int

-- | A prover backend based on Kind2.
--   
--   The executable <tt>kind2</tt> must exist and its location be in the
--   <tt>PATH</tt>.
kind2Prover :: Options -> Prover
instance Data.Default.Internal.Default Copilot.Theorem.Kind2.Prover.Options


-- | Copilot backend for the <a>Kind 2</a> SMT based model checker.
module Copilot.Theorem.Kind2

-- | Datatype to describe a term in the Kind language.
data Term
ValueLiteral :: String -> Term
PrimedStateVar :: String -> Term
StateVar :: String -> Term
FunApp :: String -> [Term] -> Term
PredApp :: String -> PredType -> [Term] -> Term

-- | Types used in Kind2 files to represent Copilot types.
--   
--   The Kind2 backend provides functions to, additionally, constrain the
--   range of numeric values depending on their Copilot type
--   (<tt>Int8</tt>, <tt>Int16</tt>, etc.).
data Type
Int :: Type
Real :: Type
Bool :: Type

-- | A proposition is defined by a term.
data Prop
Prop :: String -> Term -> Prop
[propName] :: Prop -> String
[propTerm] :: Prop -> Term

-- | Pretty print a Kind2 file.
prettyPrint :: File -> String

-- | A file is a sequence of predicates and propositions.
data File
File :: [PredDef] -> [Prop] -> File
[filePreds] :: File -> [PredDef]
[fileProps] :: File -> [Prop]

-- | Style of the Kind2 files produced: modular (with multiple separate
--   nodes), or all inlined (with only one node).
--   
--   In the modular style, the graph is simplified to remove cycles by
--   collapsing all nodes participating in a strongly connected components.
--   
--   In the inlined style, the structure of the modular transition system
--   is discarded and the graph is first turned into a <i>non-modular
--   transition</i> <i>system</i> with only one node, which can be then
--   converted into a Kind2 file.
data Style
Inlined :: Style
Modular :: Style

-- | Produce a Kind2 file that checks the properties specified.
toKind2 :: Style -> [PropId] -> [PropId] -> TransSys -> File

-- | Type of the predicate, either belonging to an initial state or a pair
--   of states with a transition.
data PredType
Init :: PredType
Trans :: PredType

-- | A definition of a state variable.
data StateVarDef
StateVarDef :: String -> Type -> [StateVarFlag] -> StateVarDef

-- | Name of the variable.
[varId] :: StateVarDef -> String

-- | Type of the variable.
[varType] :: StateVarDef -> Type

-- | Flags for the variable.
[varFlags] :: StateVarDef -> [StateVarFlag]

-- | A predicate definition.
data PredDef
PredDef :: String -> [StateVarDef] -> Term -> Term -> PredDef

-- | Identifier for the predicate.
[predId] :: PredDef -> String

-- | Variables identifying the states in the underlying state transition
--   system.
[predStateVars] :: PredDef -> [StateVarDef]

-- | Predicate that holds for initial states.
[predInit] :: PredDef -> Term

-- | Predicate that holds for two states, if there is state transition
--   between them.
[predTrans] :: PredDef -> Term

-- | Possible flags for a state variable.
data StateVarFlag
FConst :: StateVarFlag


-- | Spec properties are translated into the language of SMT solvers using
--   <tt>What4</tt>. 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 <tt>k</tt>-induction on all the properties in a given
--   specification where <tt>k</tt> is chosen to be the maximum amount of
--   delay on any of the involved streams. This is a heuristic choice, but
--   often effective.
--   
--   The functions in this module are only designed to prove universally
--   quantified propositions (i.e., propositions that use <tt>forAll</tt>).
--   Attempting to prove an existentially quantified proposition (i.e.,
--   propositions that use <tt>exists</tt>) will cause a
--   <a>UnexpectedExistentialProposition</a> exception to be thrown.
module Copilot.Theorem.What4

-- | Attempt to prove all of the properties in a spec via an SMT solver
--   (which must be installed locally on the host). Return an association
--   list mapping the names of each property to the result returned by the
--   solver.
--   
--   PRE: All of the properties in the <a>Spec</a> use universally
--   quantified propositions. Attempting to supply an existentially
--   quantified proposition will cause a
--   <a>UnexpectedExistentialProposition</a> exception to be thrown.
prove :: Solver -> Spec -> IO [(Name, SatResult)]

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

-- | The <a>prove</a> function returns results of this form for each
--   property in a spec.
data SatResult
Valid :: SatResult
Invalid :: SatResult
Unknown :: SatResult

-- | Attempt to prove all of the properties in a spec via an SMT solver
--   (which must be installed locally on the host). Return an association
--   list mapping the names of each property to the result returned by the
--   solver.
--   
--   Unlike <a>prove</a>, <a>proveWithCounterExample</a> returns a
--   <a>SatResultCex</a>. This means that if a result is invalid, then it
--   will include a <a>CounterExample</a> which describes the circumstances
--   under which the property was falsified. See the Haddocks for
--   <a>CounterExample</a> for more details.
--   
--   Note that this function does not currently support creating
--   counterexamples involving struct values, so attempting to call
--   <a>proveWithCounterExample</a> on a specification that uses structs
--   will raise an error.
proveWithCounterExample :: Solver -> Spec -> IO [(Name, SatResultCex)]

-- | The <a>proveWithCounterExample</a> function returns results of this
--   form for each property in a spec. This is largely the same as
--   <a>SatResult</a>, except that <a>InvalidCex</a> also records a
--   <a>CounterExample</a>.
data SatResultCex
ValidCex :: SatResultCex
InvalidCex :: CounterExample -> SatResultCex
UnknownCex :: SatResultCex

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

-- | A list of base cases in the proof, where each entry in the list
--   corresponds to a particular time step. For instance, the first element
--   in the list corresponds to the initial time step, the second element
--   in the list corresponds to the second time step, and so on. A
--   <a>False</a> entry anywhere in this list will cause the overall proof
--   to be <a>InvalidCex</a>.
--   
--   Because the proof uses <tt>k</tt>-induction, the number of base cases
--   (i.e., the number of entries in this list) is equal to the value of
--   <tt>k</tt>, which is chosen using heuristics.
[baseCases] :: CounterExample -> [Bool]

-- | Whether the induction step of the proof was valid or not. That is,
--   given an arbitrary time step <tt>n</tt>, if the property is assumed to
--   hold at time steps <tt>n</tt>, <tt>n+1</tt>, ..., <tt>n+k</tt>, then
--   this will be <tt>True</tt> is the property can the be proven to hold
--   at time step <tt>n+k+1</tt> (and <a>False</a> otherwise). If this is
--   <a>False</a>, then the overall proof will be <a>InvalidCex</a>.
[inductionStep] :: CounterExample -> Bool

-- | The concrete values in the Copilot specification's extern streams that
--   lead to the property being invalid.
--   
--   Each key in the <a>Map</a> is the <a>Name</a> of an extern stream
--   paired with a <a>StreamOffset</a> representing the time step. The
--   key's corresponding value is the concrete value of the extern stream
--   at that time step.
[concreteExternValues] :: CounterExample -> Map (Name, StreamOffset) (Some CopilotValue)

-- | The concrete values in the Copilot specification's streams (excluding
--   extern streams) that lead to the property being invalid.
--   
--   Each key in the <a>Map</a> is the <a>Id</a> of a stream paired with a
--   <a>StreamOffset</a> representing the time step. The key's
--   corresponding value is the concrete value of the extern stream at that
--   time step.
[concreteStreamValues] :: CounterExample -> Map (Id, StreamOffset) (Some CopilotValue)

-- | Exceptions that can arise when attempting a proof.
data ProveException

-- | The functions in <a>Copilot.Theorem.What4</a> can only prove
--   properties with universally quantified propositions. The functions in
--   <a>Copilot.Theorem.What4</a> will throw this exception if they
--   encounter an existentially quantified proposition.
UnexpectedExistentialProposition :: ProveException

-- | 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 <tt>copilot-c99</tt> would generate for that Copilot
--   program.
--   
--   PRE: All of the properties in the <a>Spec</a> use universally
--   quantified propositions. Attempting to supply an existentially
--   quantified proposition will cause a
--   <a>UnexpectedExistentialProposition</a> exception to be thrown.
computeBisimulationProofBundle :: IsInterpretedFloatSymExprBuilder sym => sym -> [String] -> Spec -> IO (BisimulationProofBundle sym)

-- | A collection of all of the symbolic states necessary to carry out a
--   bisimulation proof.
data BisimulationProofBundle sym
BisimulationProofBundle :: BisimulationProofState sym -> BisimulationProofState sym -> BisimulationProofState sym -> [(Name, Some Type, XExpr sym)] -> [(Name, Pred sym, [(Some Type, XExpr sym)])] -> [Pred sym] -> [Pred sym] -> BisimulationProofBundle sym

-- | The state of the global variables at program startup
[initialStreamState] :: BisimulationProofBundle sym -> BisimulationProofState sym

-- | The stream state prior to invoking the step function
[preStreamState] :: BisimulationProofBundle sym -> BisimulationProofState sym

-- | The stream state after invoking the step function
[postStreamState] :: BisimulationProofBundle sym -> BisimulationProofState sym

-- | A list of external streams, where each tuple contains:
--   
--   <ol>
--   <li>The name of the stream</li>
--   <li>The type of the stream</li>
--   <li>The value of the stream represented as a fresh constant</li>
--   </ol>
[externalInputs] :: BisimulationProofBundle sym -> [(Name, Some Type, XExpr sym)]

-- | A list of trigger functions, where each tuple contains:
--   
--   <ol>
--   <li>The name of the function</li>
--   <li>A formula representing the guarded condition</li>
--   <li>The arguments to the function, where each argument is represented
--   as a type-value pair</li>
--   </ol>
[triggerState] :: BisimulationProofBundle sym -> [(Name, Pred sym, [(Some Type, XExpr sym)])]

-- | User-provided property assumptions
[assumptions] :: BisimulationProofBundle sym -> [Pred sym]

-- | Side conditions related to partial operations
[sideConds] :: BisimulationProofBundle sym -> [Pred sym]

-- | The state of a bisimulation proof at a particular step.
newtype BisimulationProofState sym
BisimulationProofState :: [(Id, Some Type, [XExpr sym])] -> BisimulationProofState sym

-- | A list of tuples containing:
--   
--   <ol>
--   <li>The name of a stream</li>
--   <li>The type of the stream</li>
--   <li>The list of values in the stream description</li>
--   </ol>
[streamState] :: BisimulationProofState sym -> [(Id, Some Type, [XExpr sym])]

-- | The What4 representation of a copilot expression. We do not attempt to
--   track the type of the inner expression at the type level, but instead
--   lump everything together into the <tt>XExpr sym</tt> type. The only
--   reason this is a GADT is for the array case; we need to know that the
--   array length is strictly positive.
data XExpr sym
[XBool] :: forall sym. SymExpr sym BaseBoolType -> XExpr sym
[XInt8] :: forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
[XInt16] :: forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
[XInt32] :: forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
[XInt64] :: forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
[XWord8] :: forall sym. SymExpr sym (BaseBVType 8) -> XExpr sym
[XWord16] :: forall sym. SymExpr sym (BaseBVType 16) -> XExpr sym
[XWord32] :: forall sym. SymExpr sym (BaseBVType 32) -> XExpr sym
[XWord64] :: forall sym. SymExpr sym (BaseBVType 64) -> XExpr sym
[XFloat] :: forall sym. SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
[XDouble] :: forall sym. SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym

-- | An empty array. The <a>Typed</a> constraint and accompanying
--   <a>Type</a> field are necessary in order to record evidence that the
--   array type can be used in a context where <a>Typed</a> is required.
[XEmptyArray] :: forall t sym. Typed t => Type t -> XExpr sym

-- | A non-empty array. The <a>KnownNat</a> constraint is necessary in
--   order to record evidence that the array type can be used in a context
--   for <a>Typed</a> is required.
[XArray] :: forall (n :: Nat) sym. (KnownNat n, 1 <= n) => Vector n (XExpr sym) -> XExpr sym
[XStruct] :: forall sym. [XExpr sym] -> XExpr sym

-- | A Copilot value paired with its <a>Type</a>.
data CopilotValue a
[CopilotValue] :: forall a. Typed a => Type a -> a -> CopilotValue a

-- | Streams expressions are evaluated in two possible modes. The
--   "absolute" mode computes the value of a stream expression relative to
--   the beginning of time <tt>t=0</tt>. The "relative" mode is useful for
--   inductive proofs and the offset values are conceptually relative to
--   some arbitrary, but fixed, index <tt>j&gt;=0</tt>. In both cases,
--   negative indexes are not allowed.
--   
--   The main difference between these modes is the interpretation of
--   streams for the first values, which are in the "buffer" range. For
--   absolute indices, the actual fixed values for the streams are
--   returned; for relative indices, uninterpreted values are generated for
--   the values in the stream buffer. For both modes, stream values after
--   their buffer region are defined by their recurrence expression.
data StreamOffset
AbsoluteOffset :: !Integer -> StreamOffset
RelativeOffset :: !Integer -> StreamOffset
instance GHC.Internal.Exception.Type.Exception Copilot.Theorem.What4.ProveException
instance Data.Parameterized.Classes.ShowF Copilot.Theorem.What4.CopilotValue
instance GHC.Internal.Show.Show (Copilot.Theorem.What4.CopilotValue a)
instance GHC.Internal.Show.Show Copilot.Theorem.What4.CounterExample
instance GHC.Internal.Show.Show Copilot.Theorem.What4.ProveException
instance GHC.Internal.Show.Show Copilot.Theorem.What4.SatResult
instance GHC.Internal.Show.Show Copilot.Theorem.What4.SatResultCex
