-- 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
--   https://copilot-language.github.io.
@package copilot-theorem
@version 4.8

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

-- | Output produced by a prover, containing the Status 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 askProver, which takes 3 arguments :
--   
--   
--   
- The prover descriptor
--   
- A list of properties names which are assumptions
--   
- A properties that have to be deduced from these assumptions
--   
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
--   Actions.
type UProof = Writer [Action] ()

-- | A proof scheme is a sequence of computations that compute a result and
--   generate a trace of required prover Actions.
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 True 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 Valid while
--   another indicates that it is Invalid, the combination of both
--   provers will return an Error.
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 SmtFormat to create such commands.
data SmtLib

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

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

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

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

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

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

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

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

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

-- | Initial k 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 debug is set to True, 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 startK and maxK 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:
--   
--   
--   
- A prover producing native inputs for the Kind2 model checker.
--   
- A What4 backend that uses SMT solvers to prove safety
--   properties.
--   
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
--   (passed to Kind2 via its --unroll_max option). A value of 0
--   means unlimited.
[bmcMax] :: Options -> Int

-- | A prover backend based on Kind2.
--   
--   The executable kind2 must exist and its location be in the
--   PATH. Kind2 version 1.0 or newer is required: the native
--   input format and the command-line options this prover uses were
--   introduced in Kind2 1.0, and remain supported as of Kind2 3.0.
kind2Prover :: Options -> Prover
instance Data.Default.Internal.Default Copilot.Theorem.Kind2.Prover.Options

-- | Copilot backend for the Kind 2 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
--   (Int8, Int16, etc.).
data Type
Int :: Type
Real :: Type
Bool :: Type

-- | A node definition.
data Node
Node :: String -> [StateVarDef] -> Term -> Term -> Node

-- | Identifier for the node.
[nodeId] :: Node -> String

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

-- | Predicate that holds for initial states.
[nodeInit] :: Node -> Term

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

-- | 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 node definitions, together with a
--   distinguished top node and a series of propositions about the top
--   node.
--   
--   Kind2 analyzes the last node defined in a file as the top system, so
--   the top node is always printed after all the other nodes.
data File
File :: [Node] -> Node -> [Prop] -> File

-- | Nodes other than the top node, in dependency order (a node may only
--   refer to nodes defined before it).
[fileNodes] :: File -> [Node]

-- | The top node, which the propositions are attached to.
[fileTopNode] :: File -> Node

-- | Propositions about the top node.
[fileProps] :: File -> [Prop]

-- | Produce a Kind2 file that checks the properties specified.
toKind2 :: [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]

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

-- | Spec properties are translated into the language of SMT solvers using
--   What4. A backend solver is then used to prove the property is
--   true. The technique is sound, but incomplete. If a property is proved
--   true by this technique, then it can be guaranteed to be true. However,
--   if a property is not proved true, that does not mean it isn't true;
--   the proof may fail because the given property is not inductive.
--   
--   We perform k-induction on all the properties in a given
--   specification where k is chosen to be the maximum amount of
--   delay on any of the involved streams. This is a heuristic choice, but
--   often effective.
--   
--   The functions in this module are only designed to prove universally
--   quantified propositions (i.e., propositions that use forAll).
--   Attempting to prove an existentially quantified proposition (i.e.,
--   propositions that use exists) will cause a
--   UnexpectedExistentialProposition exception to be thrown.
module Copilot.Theorem.What4

-- | 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 Spec use universally
--   quantified propositions. Attempting to supply an existentially
--   quantified proposition will cause a
--   UnexpectedExistentialProposition 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 prove 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 prove, proveWithCounterExample returns a
--   SatResultCex. This means that if a result is invalid, then it
--   will include a CounterExample which describes the circumstances
--   under which the property was falsified. See the Haddocks for
--   CounterExample for more details.
--   
--   Note that this function does not currently support creating
--   counterexamples involving struct values, so attempting to call
--   proveWithCounterExample on a specification that uses structs
--   will raise an error.
proveWithCounterExample :: Solver -> Spec -> IO [(Name, SatResultCex)]

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

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

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

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

-- | The functions in Copilot.Theorem.What4 can only prove
--   properties with universally quantified propositions. The functions in
--   Copilot.Theorem.What4 will throw this exception if they
--   encounter an existentially quantified proposition.
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 copilot-c99 would generate for that Copilot
--   program.
--   
--   PRE: All of the properties in the Spec use universally
--   quantified propositions. Attempting to supply an existentially
--   quantified proposition will cause a
--   UnexpectedExistentialProposition 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:
--   
--   
--   
- The name of the stream
--   
- The type of the stream
--   
- The value of the stream represented as a fresh constant
--   
[externalInputs] :: BisimulationProofBundle sym -> [(Name, Some Type, XExpr sym)]

-- | A list of trigger functions, where each tuple contains:
--   
--   
--   
- The name of the function
--   
- A formula representing the guarded condition
--   
- The arguments to the function, where each argument is represented
--   as a type-value pair
--   
[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:
--   
--   
--   
- The name of a stream
--   
- The type of the stream
--   
- The list of values in the stream description
--   
[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 XExpr sym 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 Typed constraint and accompanying
--   Type field are necessary in order to record evidence that the
--   array type can be used in a context where Typed is required.
[XEmptyArray] :: forall t sym. Typed t => Type t -> XExpr sym

-- | A non-empty array. The KnownNat constraint is necessary in
--   order to record evidence that the array type can be used in a context
--   for Typed 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 Type.
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 t=0. The "relative" mode is useful for
--   inductive proofs and the offset values are conceptually relative to
--   some arbitrary, but fixed, index j>=0. 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
