h$d\j      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|!Safe'(i}copilot-theoremBinary operators.~copilot-theoremUnary operators.copilot-theoremAn IL specification.copilot-theoremDescription of a sequence.copilot-theoremIdentifier for a property.copilot-theoremA description of a variable (or function) together with its type.copilot-theorem1Idealized representation of a Copilot expression.copilot-theoremConstant boolean.copilot-theoremConstant real.copilot-theoremConstant integer.copilot-theorem If-then-else.copilot-theoremApply a unary operator.copilot-theoremApply a binary operator.copilot-theorem%Refer to a value in another sequence.copilot-theoremFunction application.copilot-theoremIdealized types. These differ from Copilot types in that, notionally, reals actually denote real numbers.copilot-theoremIndex within a sequence.copilot-theorem"An absolute index in the sequence.copilot-theorem+An index relative to the current time-step.copilot-theoremIdentifier of a sequence.copilot-theorem!Return the type of an expression.copilot-theorem.An index to the current element of a sequence.copilot-theorem+An index to a future element of a sequence.copilot-theorem9Evaluate an expression at specific index in the sequence.}~Safe%'(copilot-theorem!Pretty print an IL specification.copilot-theorem)Pretty print an IL constraint expression. Safe !copilot-theoremSimplify IL expressions by partly evaluating operations on booleans, eliminating some boolean literals.For example, an if-then-else in which the condition is literally the constant True or the constant False can be reduced to an operation without choice in which the appropriate branch of the if-then-else is used instead. Safe%'( copilot-theorem9Translate a Copilot specification to an IL specification.copilot-theoremTranslate a Copilot specification to an IL specification, adding constraints for limiting the values of numeric expressions to known bounds based on their specific types (only for integers or natural numbers). Safe }~ Safecopilot-theorem1Datatype to describe a term in the Kind language.copilot-theoremType of the predicate, either belonging to an initial state or a pair of states with a transition. copilot-theorem$Possible flags for a state variable. copilot-theorem5Types 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.).copilot-theorem!A definition of a state variable.copilot-theoremFlags for the variable.copilot-theoremName of the variable.copilot-theoremType of the variable.copilot-theoremA predicate definition.copilot-theoremIdentifier for the predicate.copilot-theoremVariables identifying the states in the underlying state transition system.copilot-theorem)Predicate that holds for initial states.copilot-theoremPredicate that holds for two states, if there is state transition between them.copilot-theorem#A proposition is defined by a term. copilot-theorem4A file is a sequence of predicates and propositions."  !#" Safecopilot-theoremReport an error due to an error detected by Copilot (e.g., user error).copilot-theorem(Report an error due to a bug in Copilot.copilot-theorem(Report an error due to a bug in Copilot.copilot-theorem7Report an unrecoverable error (e.g., incorrect format).copilot-theoremDescription of the error.copilot-theorem+Error information to attach to the message.Safe> copilot-theoremA structured expression is either an atom, or a sequence of expressions, where the first in the sequence denotes the tag or label of the tree.copilot-theoremEmpty string expression.copilot-theoremAtomic expression constructor.copilot-theoremEmpty expression (empty list).copilot-theoremSingle expression.copilot-theoremSequence of expressions.copilot-theoremSequence of expressions with a root or main note, and a series of additional expressions or arguments..copilot-theoremIndent by a given number.copilot-theorem1Pretty print a structured expression as a String.copilot-theorem*Pretty print a structured expression as a , or set of layouts.copilot-theoremParser for strings of characters separated by spaces into a structured tree.Parentheses are interpreted as grouping elements, that is, defining a , which may be empty.copilot-theoremParser for strings of characters separated by spaces into a structured tree.Parentheses are interpreted as grouping elements, that is, defining a , which may be empty.copilot-theorem)True if an expression should be indented.copilot-theorem!Pretty print the value inside as .copilot-theoremRoot of  tree.copilot-theorem)True if an expression should be indented.copilot-theorem!Pretty print the value inside as .copilot-theoremRoot of  tree.SafeS$copilot-theoremPretty print a Kind2 file.$Safefcopilot-theoremTrue if the given list is a subset of the second list, when both are considered as sets.copilot-theoremTrue if both lists contain the same elements, when both are considered as sets.copilot-theoremRemove duplicates from a list. This is an efficient version of  that works for lists with a stronger constraint on the type (i.e., , as opposed of s  constraint).copilot-theorem Variant of * parameterized by the comparison function.copilot-theorem0Create a temporary file and open it for writing.copilot-theorem+Directory where the file should be created.copilot-theorem Base name for the file (prefix).copilot-theoremFile extension.Safe%&'(#j%copilot-theoremProver actions.)copilot-theoremA proof scheme is a sequence of computations that compute a result and generate a trace of required prover %s.+copilot-theoremA sequence of computations that generate a trace of required prover %s.,copilot-theorem A proof scheme with unit result.-copilot-theoremEmpty datatype to mark proofs of existentially quantified predicates..copilot-theoremEmpty datatype to mark proofs of universally quantified predicates./copilot-theoremReference to a property.1copilot-theoremA unique property identifier2copilot-theoremA connection to a prover able to check the satisfiability of specifications.The most important is 6, which takes 3 arguments :The prover descriptor0A list of properties names which are assumptions;A properties that have to be deduced from these assumptions8copilot-theoremStatus returned by a prover when given a specification and a property to prove.>copilot-theorem,Output produced by a prover, containing the 8* of the proof and additional information.@copilot-theorem1Record a requirement for satisfiability checking.Acopilot-theoremTry to prove a property in a specification with a given proof scheme.Return  if a proof of satisfiability or validity is found, false otherwise.Bcopilot-theoremCombine 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 :% while another indicates that it is ;2, the combination of both provers will return an =.%&'()*+,-./012345678=<9:;>?@AB>?8=<9:;2345671/0,+)*%&'(.-@ABSafe$_copilot-theoremParse output of Kind2.copilot-theorem)Property whose validity is being checked.copilot-theoremXML output of Kind2Safe%Tcopilot-theoremSatisfiability result communicated by the SMT solver or theorem prover.Fcopilot-theorem+Backend to an SMT solver or theorem prover.Gcopilot-theoremFormat of SMT-Lib commands.FGSafe%&(`copilot-theorem9A connection with a running SMT solver or theorem prover.copilot-theorem9Create a new solver implemented by the backend specified.The error handle from the backend handle is immediately closed/discarded, and the logic initialized as specifiied by the backend options.copilot-theoremStop a solver, closing all communication handles and terminating the process.copilot-theoremRegister the given expressions as assumptions or axioms with the solver.copilot-theoremCheck if a series of expressions are entailed by the axioms or assumptions already registered with the solver.copilot-theorem-Register the given variables with the solver.Safe'(>)}Hcopilot-theorem(Type used to represent SMT-lib commands.Use the interface in G to create such commands.copilot-theoremParse a satisfiability result.copilot-theorem*Interface for SMT-Lib conforming backends.HSafe'(*oIcopilot-theorem(Type used to represent TPTP expressions."Although this type implements the G interface, only  is actually used.copilot-theoremParse a satisfiability result.I Trustworthy %'(>3TJcopilot-theorem!Options to configure the provers.Lcopilot-theoremInitial k for the k-induction algorithm.Mcopilot-theoremThe maximum number of steps of the k-induction algorithm the prover runs before giving up.Ncopilot-theoremIf debug is set to True, the SMTLib/TPTP queries produced by the prover are displayed in the standard output.Ocopilot-theorem.Tactic to find only a proof of satisfiability.Pcopilot-theorem(Tactic to find only a proof of validity.Qcopilot-theorem/Tactic to find a proof by standard 1-induction.The values for startK and maxK in the options are ignored.Rcopilot-theorem&Tactic to find a proof by k-induction.Scopilot-theorem"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.Tcopilot-theoremBackend 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.Ucopilot-theorem#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.Vcopilot-theorem!Backend to the Z3 theorem prover. The command z3 must be in the user's PATH.Wcopilot-theorem 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.Xcopilot-theorem"Backend to the Mathsat SMT solver."It enables non-linear arithmetic (QF_NRA). The command mathsat must be in the user's PATH.Ycopilot-theorem(Backend to the MetiTaski theorem prover. The command metit must be in the user's PATH.'The argument string is the path to the tptp2 subdirectory of the metitarski install location.Zcopilot-theoremDefault J with a 0 k and a max of 10, steps, and that produce no debugging info.FGHIJKNLMOPQRSTUVWXYFGHISWUYVTXJKNLMQROPSafe4l^copilot-theorem8Instantiate a universal proof into an existential proof._copilot-theorem2Assume that a property, given by reference, holds.`copilot-theorem#Assume that the current goal holds.^_`Safe4,-./1^_`^_`,1/.-Safe5Ncopilot-theorem>Type class for types with additional invariants or contraints.copilot-theorem(Creates an invariant with a description.Safe'(6{copilot-theoremUnknown types.For instance, 'U Expr' is the type of an expression of unknown typecopilot-theorem$A type at both value and type level.Real numbers are mapped to s.copilot-theoremProofs of type equality.Safe'(7copilot-theorem+Synonym for a dynamic type in Copilot core.copilot-theoremTranslation of a Copilot type into Copilot theorem's internal representation.copilot-theorem%Cast a dynamic value to a given type.copilot-theoremApply function to a corresponding type in Copilot theorem's internal representation.Safe'(?ucopilot-theoremUnhandled binary operator.Unhandled operators are monomorphic, and their names are labeled so that each name corresponds to a unique uninterpreted function with a monomorphic type.copilot-theoremUnhandled unary operator.Unhandled operators are monomorphic, and their names are labeled so that each name corresponds to a unique uninterpreted function with a monomorphic type.copilot-theoremBinary operators.copilot-theoremUnary operators.copilot-theoremTranslate an Op1.This function is parameterized so that it can be used to translate in different contexts and with different targets.m. is the monad in which the computation is maderesT> is the desired return type of the expression being translatedcopilot-theoremTranslate an Op2.This function is parameterized so that it can be used to translate in different contexts and with different targets.m. is the monad in which the computation is maderesT> is the desired return type of the expression being translatedcopilot-theorem8Error message for unexpected behavior / internal errors.copilot-theoremThe desired return typecopilot-theorem/The unary operator encountered and its argumentcopilot-theorem/The monadic function to translate an expressioncopilot-theorem/A function to deal with a operators not handledcopilot-theoremThe Op1 constructor of the expr typecopilot-theoremThe desired return typecopilot-theorem1The binary operator encountered and its argumentscopilot-theorem/The monadic function to translate an expressioncopilot-theorem/A function to deal with a operators not handledcopilot-theoremThe Op2 constructor of the expr typecopilot-theoremThe Op1 for boolean negation(Safe'(G;copilot-theorem$A point-wise (time-wise) expression.copilot-theoremA variable definition either as a delay, an operation on variables, or a constraint.copilot-theorem3A description of a variable together with its type.copilot-theoremIdentifer of a variable in the global namespace by specifying both a node name and a variable.copilot-theoremIdentifer of a variable in the local (within one node) namespace.copilot-theoremA node is a set of variables living in a local namespace and corresponding to the  type.copilot-theorem+Nodes from which variables are imported.copilot-theoremLocally defined variables, either as the previous value of another variable (using 2), an expression involving variables (using ') or a set of constraints (using ).copilot-theorem2Binds each imported variable to its local name.copilot-theoremA modular transition system is defined by a graph of nodes and a series of properties, each mapped to a variable.copilot-theorem'Unique name that identifies a property.copilot-theorem#Unique name that identifies a node.copilot-theorem>Constructor for variables identifiers in the global namespace.copilot-theoremApply an arbitrary transformation to the leafs of an expression.copilot-theoremThe set of variables related to a node (union of the local variables and the imported variables after deferencing them).copilot-theoremGiven a modular transition system, produce a map from each node to its dependencies.copilot-theorem3Return the top node of a modular transition system.copilot-theoremTrue if the graph is topologically sorted (i.e., if the dependencies of a node appear in the list of ( before the node that depends on them).Safe %&'(?Hucopilot-theoremTranslate Copilot specifications into a modular transition system. SafeLjcopilot-theoremA monad capable of keeping track of variable renames and of providing fresh names for variables.copilot-theorem$Register a name as reserved or used.copilot-theorem>Produce a fresh new name based on the variable names provided.This function will try to pick a name from the given list and, if not, will use one of the names in the list as a basis for new names.$PRE: the given list cannot be empty.copilot-theorem:Map a name in the global namespace to a new variable name.copilot-theoremReturn a function that maps variables in the global namespace to their new names if any renaming has been registered.copilot-theoremRun a computation in the  monad, providing a result and the renaming function that maps variables in the global namespace to their new local names.copilot-theorem A node Idcopilot-theoremA variable within that nodecopilot-theoremA new name for the variable!SafeRcopilot-theoremMerge all the given nodes, replacing all references to the given node Ids with a reference to a fresh node id (unless the nodes given as argument contain the top node), in which case its ID is chosen instead.copilot-theoremDiscard all the structure of a modular transition system and turn it into a non-modular transition system with only one node.copilot-theoremRemove cycles by merging nodes participating in strongly connected components.&The transition system obtained by the "# module is perfectly consistent. However, it can't be directly translated into the Kind2 native file format. Indeed, it is natural to bind each node to a predicate but the Kind2 file format requires that each predicate only uses previously defined predicates. However, some nodes in our transition system could be mutually recursive. Therefore, the goal of & is to remove such dependency cycles. The function  computes the strongly connected components of the dependency graph and merge each one into a single node using . The complexity of this process is high in the worst case (the square of the total size of the system times the size of the biggest node) but good in practice as few nodes are to be merged in most practical cases.copilot-theoremCompletes each node of a specification with imported variables such that each node contains a copy of all its dependencies.The given specification should have its node sorted by topological order.The top nodes should have all the other nodes as its dependencies.$Safe%'(S~copilot-theoremPretty print a TransSys specification as a Kind2/Lustre specification.%SafeS&Safe%&'(Wacopilot-theoremStyle 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 non-modular transition system with only one node, which can be then converted into a Kind2 file.dcopilot-theorem:Produce a Kind2 file that checks the properties specified.dcopilot-theorem'Style of the file (modular or inlined).copilot-theorem Assumptionscopilot-theoremProperties to be checkedcopilot-theorem1Modular transition system holding the system specabcd TrustworthyY`ecopilot-theoremOptions for Kind2gcopilot-theoremUpper bound on the number of unrolling that base and step will perform. A value of 0 means  unlimited.hcopilot-theorem A prover backend based on Kind2.The executable kind2' must exist and its location be in the PATH.icopilot-theorem;Default options with unlimited unrolling for base and step.efghefghSafeY-  !"#$abcdefgh'$dabc !#"   "Prove spec properties using What4.(c) Ben Selfridge, 2020benselfridge@galois.com experimentalPOSIXNone'(/2?\Rjcopilot-theoremThe s function returns results of this form for each property in a spec.ncopilot-theorem+The solvers supported by the what4 backend.scopilot-theoremAttempt 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.scopilot-theorem Solver to usecopilot-theoremSpec jmklnrpoqs snrpoqjmkl'()'(* + , - . / 0 1 2 3 4 5 6 7 8 9 : : ; < = > > ? @ A B C C D E F F G HIJKLMNOPOQRSSTUUVWXYZ[\]^_``abcdefghijkklmnopqrstuvwxyz{|}~&&&&kkz\]^bT/6<98I       ^[g698"T<"      !!!!$I+copilot-theorem-3.10-9T0jjAYbq866KjSjWPJCcdCopilot.Theorem.Prover.SMTCopilot.Theorem.Kind2Copilot.Theorem.ProveCopilot.TheoremCopilot.Theorem.Kind2.ProverCopilot.Theorem.What4Copilot.Theorem.IL.SpecCopilot.Theorem.IL.PrettyPrintCopilot.Theorem.IL.TransformCopilot.Theorem.IL.TranslateCopilot.Theorem.ILCopilot.Theorem.Kind2.ASTCopilot.Theorem.Misc.ErrorCopilot.Theorem.Misc.SExpr!Copilot.Theorem.Kind2.PrettyPrintCopilot.Theorem.Misc.Utils Data.Listnubnub'Copilot.Theorem.Kind2.OutputCopilot.Theorem.Prover.BackendCopilot.Theorem.Prover.SMTIOCopilot.Theorem.Prover.SMTLibCopilot.Theorem.Prover.TPTPCopilot.Theorem.Tactics#Copilot.Theorem.TransSys.InvariantsCopilot.Theorem.TransSys.TypeCopilot.Theorem.TransSys.Cast"Copilot.Theorem.TransSys.OperatorsCopilot.Theorem.TransSys.Spec"Copilot.Theorem.TransSys.Translate!Copilot.Theorem.TransSys.Renaming"Copilot.Theorem.TransSys.TransformTransSys Translate$Copilot.Theorem.TransSys.PrettyPrintCopilot.Theorem.TransSysCopilot.Theorem.Kind2.Translate1data-default-class-0.1.2.0-IIN1s3V8yfYEDHe5yjxXHVData.Default.ClassDefaultdefTerm ValueLiteralPrimedStateVarStateVarFunAppPredAppPredTypeInitTrans StateVarFlagFConstTypeIntRealBool StateVarDefvarIdvarTypevarFlagsPredDefpredId predStateVarspredInit predTransProppropNamepropTermFile filePreds fileProps prettyPrintActionCheckAssumeAdmit ProofSchemeProofUProof Existential UniversalPropRefPropIdProver proverName startProver askProver closeProverStatusSatValidInvalidUnknownErrorOutputcheckprovecombine$fMonadProofScheme$fApplicativeProofScheme$fFunctorProofSchemeBackend SmtFormatSmtLibTptpOptionsstartKmaxKdebugonlySat onlyValidity induction kInductionyicescvc4altErgoz3dRealmathsatmetit$fDefaultOptions$fShowSolverId $fOrdSolverId $fEqSolverId instantiateassumeadmitStyleInlinedModulartoKind2bmcMax kind2Prover SatResultSolverCVC4DRealYicesZ3$fPanicComponentCopilotWhat4$fMonadFailTransM$fFunctorTransM$fApplicativeTransM $fMonadTransM$fMonadIOTransM$fMonadStateTransStateTransM$fShowSatResult $fShowXExprOp2Op1ILSeqDescrVarDescrExprConstBConstRConstIIteSValSeqIndexFixedVarSeqIdtypeOf_n__n_plusevalAtModEqSubAndOrAddMulFdivPowLeGeLtGtExpNotAbsSqrtLogSinTanCosAsinAtanAcosSinhTanhCoshAsinhAtanhAcoshNeg modelInitmodelRec properties inductiveseqIdseqTypevarNameargsSBV8SBV16SBV32SBV64BV8BV16BV32BV64printConstraintbsimpl translatetranslateWithBoundsbadUse impossible impossible_fatalSExprblankatomunit singletonlistnodeindenttoStringtoDocpretty-1.1.3.6Text.PrettyPrint.HughesPJDocparserList parseSExprAtom isSublistOfnubEqghc-prim GHC.ClassesOrdnubBy' openTempFile GHC.TypesTrue parseOutputUnsat interpretnamecmdcmdOptsinputTerminator incrementallogicassertsetLogiccheckSatpushpopdeclFunstartNewSolverstopentaileddeclVars$fSmtFormatSmtLib HasInvariantsprop invariants checkInvsUDouble$fEqualTypeTypeIntegerDyn castedTypecastcastingbase Data.DynamictoDyn UnhandledOp2 UnhandledOp1 handleOp1 handleOp2 typeErrMsgVarDefExtVarNodenodeDependencies nodeLocalVarsPreConstrsnodeImportedVarsNodeIdmkExtVar transformExpr nodeVarsSetspecDependenciesGraph specTopNodeisTopologicallySorted specNodesConstVarEvarDef extVarNodeextVarLocalPartnodeId nodeConstrs specTopNodeId specPropsRenamingaddReservedName getFreshNamerename getRenamingF runRenaming mergeNodesinline removeCyclescomplete