h&`      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~"Safe)*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')* bcopilot-theorem*A state monad over the translation state ().copilot-theoremTranslation state.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-theoremName of the variable.copilot-theoremType of the variable.copilot-theoremFlags for 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."  #"! Safe3copilot-theoremTag used with error messages to help users locate the component that failed or reports the error.copilot-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.SafeB 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.SafeQ copilot-theorem6A tree of expressions, in which the leafs are strings.copilot-theoremReserved keyword prime.$copilot-theoremPretty print a Kind2 file.copilot-theorem2Define the indentation policy of the S-Expressionscopilot-theorem.Convert a file into a sequence of expressions.copilot-theoremConvert a sequence of propositions into command to check each of them.copilot-theorem)Convert a proposition into an expression.copilot-theorem'Convert a predicate into an expression.copilot-theorem7Convert a state variable definition into an expression.copilot-theorem"Convert a type into an expression.copilot-theorem"Convert a term into an expression.$Safe dcopilot-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'()*'h%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)Rcopilot-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-theoremOutput a debugging message if debugging is enabled for the solver.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)*.Icopilot-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 ')*7copilot-theorem1Checks the Copilot specification with k-inductionJcopilot-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.FGHIJKNLMOPQRSTUVWXYFGHISWUYVTXJKNLMQROPSafe9^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.^_`Safe9/,-./1^_`^_`,1/.-Safe9copilot-theorem>Type class for types with additional invariants or contraints.copilot-theorem(Creates an invariant with a description.Safe)*;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)*<copilot-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)*Dcopilot-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)*Kcopilot-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 '()*Mcopilot-theoremTranslate Copilot specifications into a modular transition system. SafeQgcopilot-theoremState needed to keep track of variable renames and reserved names.copilot-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!SafeWcopilot-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')*X{copilot-theoremPretty print a TransSys specification as a Kind2/Lustre specification.%SafeX&Safe'()*\acopilot-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 Trustworthy^]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.efghefghSafe^-  #!"$abcdefgh'$dabc #"!   '+Translate Copilot specifications into What4(c) Galois Inc., 2021-2022robdockins@galois.com experimentalPOSIX Safe-Inferred)*15wNcopilot-theoremStreams 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>=02. 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.jcopilot-theoremThe 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.copilot-theoremThe sign of a bitvector -- this indicates whether it is to be interpreted as a signed  or an unsigned .copilot-theoremA view of an XExpr as a bitvector expression, a natrepr for its width, its signed/unsigned status, and the constructor used to reconstruct an XExpr from it. This is a useful view for translation, as many of the operations can be grouped together for all words/ints/floats.copilot-theoremAn environment used to translate local Copilot variables to What4.copilot-theoremThe state for translating Copilot expressions into What4 expressions. As we translate, we generate fresh symbolic constants for external variables and for stream variables. We need to only generate one constant per variable, so we allocate them in a map. When we need the constant for a particular variable, we check if it is already in the map, and return it if it is; if it isn't, we generate a fresh constant at that point, store it in the map, and return it.We also store , an immutable field, in this state, rather than wrap it up in another monad transformer layer. This is initialized prior to translation and is never modified. This maps from stream ids to the core stream definitions.copilot-theoremMap keeping track of all external variables encountered during translation.copilot-theoremMemo table for external variables, indexed by the external stream name and a stream offset.copilot-theorem4Memo table for stream values, indexed by the stream  and offset.copilot-theoremMap from stream ids to the streams themselves. This value is never modified, but I didn't want to make this an RWS, so it's represented as a stateful value.copilot-theoremA list of side conditions that must be true in order for all applications of partial functions (e.g., ) to be well defined.copilot-theorem2Translate a Copilot specification using the given  computation.copilot-theoremCompute the value of a stream expression at the given offset in the given local environment.copilot-theoremCompute and cache the value of a stream with the given identifier at the given offset.copilot-theoremCompute and cache the value of an external stream with the given name at the given offset.copilot-theoremIf the inner expression can be viewed as a bitvector, we project out a view of it as such.copilot-theoremIf an j is a bitvector expression, use it to generate a side condition involving an application of a partial function. Otherwise, do nothing.copilot-theoremIf two js are both bitvector expressions of the same type and signedness, use them to generate a side condition involving an application of a partial function. Otherwise, do nothing.copilot-theoremTranslate a constant expression by creating a what4 literal and packaging it up into an j.copilot-theoremGenerate a fresh constant for a given copilot type. This will be called whenever we attempt to get the constant for a given external variable or stream variable, but that variable has not been accessed yet and therefore has no constant allocated.copilot-theorem*Retrieve a stream definition given its id.copilot-theoremAdd a side condition originating from an application of a partial function.copilot-theoremConstruct an expression that indexes into an array by building a chain of if expressions, where each expression checks if the current index is equal to a given index in the array. If the indices are equal, return the element of the array at that index. Otherwise, proceed to the next if7 expression, which checks the next index in the array.copilot-theorem Construct an if$ expression of the appropriate type.copilot-theoremCast an j to another j of a possibly differing type.copilot-theorem+Increment a stream offset by a drop amount.copilot-theoremWe assume round-near-even throughout, but this variable can be changed if needed.copilot-theoremUse this function rather than an error monad since it indicates that something in the implementation of copilot-theorem is incorrect.copilot-theoremEnvironment for local variablescopilot-theoremExpression to translatecopilot-theoremOffset to computecopilot-theoremOriginal value we are translating (only used for error messages)copilot-theoremOriginal value we are translating (only used for error messages)copilot-theoremOriginal value we are translating (only used for error messages)copilot-theoremIndexcopilot-theoremElementscopilot-theoremOriginal value we are translating (only used for error messages)copilot-theoremType we are casting tocopilot-theorem Value to cast!jlmnopqrsktuvwx"Prove spec properties using What4.(c) Ben Selfridge, 2020benselfridge@galois.com experimentalPOSIX Safe-Inferred)*15ycopilot-theorem7The state of a bisimulation proof at a particular step.{copilot-theoremA list of tuples containing: The name of a streamThe type of the stream,The list of values in the stream description|copilot-theoremA collection of all of the symbolic states necessary to carry out a bisimulation proof.~copilot-theorem4The state of the global variables at program startupcopilot-theorem4The stream state prior to invoking the step functioncopilot-theorem1The stream state after invoking the step functioncopilot-theorem6A list of external streams, where each tuple contains: The name of the streamThe type of the stream7The value of the stream represented as a fresh constantcopilot-theorem7A list of trigger functions, where each tuple contains: The name of the function,A formula representing the guarded conditionThe arguments to the function, where each argument is represented as a type-value paircopilot-theorem"User-provided property assumptionscopilot-theorem-Side conditions related to partial operationscopilot-theoremThe  function returns results of this form for each property in a spec.copilot-theorem+The solvers supported by the what4 backend.copilot-theoremNo builder state needed.copilot-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.copilot-theoremGiven 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.copilot-theoremCompute the initial state of the global variables at the start of a Copilot program.copilot-theoremCompute the stream state of a Copilot program prior to invoking the step function.copilot-theoremCompute ehe stream state of a Copilot program after invoking the step function.copilot-theorem3Compute the trigger functions in a Copilot program.copilot-theoremCompute the values of the external streams in a Copilot program, where each external stream is represented as a fresh constant.copilot-theoremCompute the user-provided property assumptions in a Copilot program.copilot-theorem A catch-all  to use when an j7 is is expected to uphold the invariant that it is an k , but the invariant is violated.copilot-theorem Solver to usecopilot-theoremSpeccopilot-theorem1Names of properties to assume during verificationcopilot-theoremThe input Copilot specificationcopilot-theoremThe input Copilot specificationcopilot-theoremThe input Copilot specificationcopilot-theoremThe input Copilot specificationcopilot-theoremThe input Copilot specificationcopilot-theorem1Names of properties to assume during verificationcopilot-theoremThe input Copilot specificationcopilot-theorem What the j represents&jlmnopqrsktuvwxyz{|}~&|}~yz{jlmnopqrsktuvwx()*()+ , - . / 0 1 2 3 4 5 6 7 8 9 : ; ; < = > ? ? @ A B C D D E F G G H IJKLMNOPQPRSTTUVVWXYZ[\]^_`aabcdefghijkllmnopqrstuvwxyz{|}~&&&&ll{''''''''''''''']^_cU07=:9J  4        _\ho7:9"U="       !!!!$J''8''''''''''''''''''''''''''''''''+copilot-theorem-3.15-A6jitz2R318EXkSM2RQpZ7Copilot.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.TranslateCopilot.Theorem.What4.Translate1data-default-class-0.1.2.0-CQYBH38PFES4dDyailJWvdData.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 kind2ProverXExprXBoolXInt8XInt16XInt32XInt64XWord8XWord16XWord32XWord64XFloatXDouble XEmptyArrayXArrayXStructBisimulationProofState streamStateBisimulationProofBundleinitialStreamStatepreStreamStatepostStreamStateexternalInputs triggerState assumptions sideConds SatResultSolverCVC4DRealYicesZ3computeBisimulationProofBundle$fShowSatResultOp2Op1ILSeqDescrVarDescrExprConstBConstRConstIIteSValSeqIndexFixedVarSeqIdtypeOf_n__n_plusevalAtEqModAndSubOrAddMulFdivPowLeGeLtGtNotExpAbsSqrtLogSinTanCosAsinAtanAcosSinhTanhCoshAsinhAtanhAcoshNeg modelInitmodelRec properties inductiveseqIdseqTypevarNameargsSBV8SBV16SBV32SBV64BV8BV16BV32BV64printConstraintbsimplTransST translatetranslateWithBounds errorHeaderbadUse impossible impossible_fatalSExprblankatomunit singletonlistnodeindenttoStringtoDocpretty-1.1.3.6Text.PrettyPrint.HughesPJDocparserList parseSExprAtomSSExprkwPrime shouldIndentppFileppPropsppProp ppPredDef ppStateVarDefppTypeppTerm isSublistOfnubEqghc-prim GHC.ClassesOrdnubBy' openTempFile GHC.TypesTrue parseOutputUnsatname interpretcmdcmdOptsinputTerminator incrementallogicassertsetLogiccheckSatpushpopdeclFunstartNewSolverstopentaileddeclVars$fSmtFormatSmtLib ProofScript HasInvariantsprop invariants checkInvsUDouble$fTestEqualityTYPETypeIntegerDyn castedTypecastcastingbase Data.DynamictoDyn UnhandledOp2 UnhandledOp1 handleOp1 handleOp2 typeErrMsgVarDefExtVarNodenodeDependencies nodeLocalVarsPreConstrsnodeImportedVarsNodeIdmkExtVar transformExpr nodeVarsSetspecDependenciesGraph specTopNodeisTopologicallySorted specNodesConstVarEvarDef extVarNodeextVarLocalPartnodeId nodeConstrs specTopNodeId specProps RenamingSTRenamingaddReservedName getFreshNamerename getRenamingF runRenaming mergeNodesinline removeCyclescomplete StreamOffsetBVSignWord SomeBVExprLocalEnv TransStatestreamsmentionedExternals externVars streamValues(copilot-core-3.15-CkLpZYxqFJBJXjPHS4feTaCopilot.Core.ExprId sidePredsCopilot.Core.OperatorsDiv runTransMTransM translateExprgetStreamValuegetExternConstantasBVExpraddBVSidePred1addBVSidePred2translateConstExprfreshCPConstant getStreamDef addSidePredbuildIndexExprmkItecastOp addOffsetfpRMpanic translateOp1 translateOp2 translateOp3AbsoluteOffsetRelativeOffset BuilderStatecomputeInitialStreamStatecomputePrestatecomputePoststatecomputeTriggerStatecomputeExternalInputscomputeAssumptions expectedBool