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


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

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

-- | 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.
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] :: SymExpr sym BaseBoolType -> XExpr sym
[XInt8] :: SymExpr sym (BaseBVType 8) -> XExpr sym
[XInt16] :: SymExpr sym (BaseBVType 16) -> XExpr sym
[XInt32] :: SymExpr sym (BaseBVType 32) -> XExpr sym
[XInt64] :: SymExpr sym (BaseBVType 64) -> XExpr sym
[XWord8] :: SymExpr sym (BaseBVType 8) -> XExpr sym
[XWord16] :: SymExpr sym (BaseBVType 16) -> XExpr sym
[XWord32] :: SymExpr sym (BaseBVType 32) -> XExpr sym
[XWord64] :: SymExpr sym (BaseBVType 64) -> XExpr sym
[XFloat] :: SymExpr sym (SymInterpretedFloatType sym SingleFloat) -> XExpr sym
[XDouble] :: SymExpr sym (SymInterpretedFloatType sym DoubleFloat) -> XExpr sym
[XEmptyArray] :: XExpr sym
[XArray] :: 1 <= n => Vector n (XExpr sym) -> XExpr sym
[XStruct] :: [XExpr sym] -> XExpr sym
instance GHC.Show.Show Copilot.Theorem.What4.SatResult