-- 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 3.7


-- | 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] :: 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] :: 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.Base.Functor (Copilot.Theorem.Prove.ProofScheme a)
instance GHC.Base.Applicative (Copilot.Theorem.Prove.ProofScheme a)
instance GHC.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

-- | A class for types with a default value.
class Default a

-- | The default value for this type.
def :: Default a => a
instance GHC.Classes.Eq Copilot.Theorem.Prover.SMT.SolverId
instance GHC.Classes.Ord Copilot.Theorem.Prover.SMT.SolverId
instance GHC.Show.Show Copilot.Theorem.Prover.SMT.SolverId
instance Data.Default.Class.Default Copilot.Theorem.Prover.SMT.Options


-- | 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.Class.Default Copilot.Theorem.Kind2.Prover.Options


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

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

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

-- | 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

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

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

-- | 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

-- | A definition of a state variable.
data StateVarDef

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

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

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

-- | 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

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

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

-- | 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


-- | 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.
--   Very simple specifications are unprovable by this technique,
--   including:
--   
--   <pre>
--   a = True : a
--   </pre>
--   
--   The above specification will not be proved true. The reason is that
--   this technique does not perform any sort of induction. When proving
--   the inner <tt>a</tt> expression, the technique merely allocates a
--   fresh constant standing for "<tt>a</tt>, one timestep in the past."
--   Nothing is asserted about the fresh constant.
--   
--   An example of a property that is provable by this approach is:
--   
--   <pre>
--   a = True : b
--   b = not a
--   
--   -- Property: a || b
--   </pre>
--   
--   By allocating a fresh constant, <tt>b_-1</tt>, standing for "the value
--   of <tt>b</tt> one timestep in the past", the equation for <tt>a ||
--   b</tt> at some arbitrary point in the future reduces to <tt>b_-1 ||
--   not b_-1</tt>, which is always true.
--   
--   In addition to proving that the stream expression is true at some
--   arbitrary point in the future, we also prove it for the first
--   <tt>k</tt> timesteps, where <tt>k</tt> is the maximum buffer length of
--   all streams in the given spec. This amounts to simply interpreting the
--   spec, although external variables are still represented as constants
--   with unknown values.
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.
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
instance GHC.Show.Show Copilot.Theorem.What4.SatResult
instance Control.Monad.State.Class.MonadState (Copilot.Theorem.What4.TransState t) (Copilot.Theorem.What4.TransM t)
instance Control.Monad.IO.Class.MonadIO (Copilot.Theorem.What4.TransM t)
instance GHC.Base.Monad (Copilot.Theorem.What4.TransM t)
instance GHC.Base.Applicative (Copilot.Theorem.What4.TransM t)
instance GHC.Base.Functor (Copilot.Theorem.What4.TransM t)
instance GHC.Show.Show (Copilot.Theorem.What4.XExpr t)
instance Control.Monad.Fail.MonadFail (Copilot.Theorem.What4.TransM t)
instance Panic.PanicComponent Copilot.Theorem.What4.CopilotWhat4