h$HQ      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                          ! ! ! ! ! ! " " " " " " " " " # # # # # # # # # # # # # # # # # # # # # $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % & & & & & & & & & & & & & & & & & ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' '''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''''((((((((((((((((((((((((((((((((((())))**************************************++++++++++++++++,,,,,,,,,,,,,--.....//000000000000000000000000000000000000000000000011111111111111111111111111111111122333344444444444444444444455666666666666666666666666666666666666666666666666666666666666666666666666666666666666666667777777777777777777777777888888888888888888888888888888888888888888888888889999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999999:;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;<<<<=====>>>>>>>>?????????@@@@@AABBBBBBBBBBBBBBBBBBCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDEEEEEEEEEEEEEEEEEEEEFGGGGGGGGHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHIIIIIIIIIIIIIIIJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKLLLLLLLLLLLLLLLLLLLLLLLLLLLLLMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNOOOOOOOOOOOOOOOOOOOOPPPPPPPPPPPPPPPPPPPPPPPQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRSSSSSSSSSSSSTTTTTTTTTTTUUUUUUUUUUUUUUVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVWWXXXYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYZZZZZZZZZ[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[\\\\]]]]]]]]]]]]]]]]]]]]]]]]]]]]]^______!!!!!!!!!!!!!!!!!``````````````aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbcccccccccccccdddddddddddddddddddddddddeeeeeeeeeeeeeeeffffffffffgggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggghhhhhhhhhhhhhhhhhhhhhhhhiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiii(c) Levent ErkokBSD3erkokl@gmail.com experimental Safe-InferredP3cryptolThe key, which can be 128, 192, or 256 bits. Represented as a sequence of 32-bit words.cryptolAES state. The state consists of four 32-bit words, each of which is in turn treated as four GF28's, i.e., 4 bytes. The T-Box implementation keeps the four-bytes together for efficient representation.cryptolThe  InvMixColumns transformation, as described in Section 5.3.3 of the standard. Note that this transformation is only used explicitly during key-expansion in the T-Box implementation of AES.  (c) 2014-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-InferredR  cryptolThis is the widest word we can have before gmp will fail to allocate and bring down the whole program. According to  ?https://gmplib.org/list-archives/gmp-bugs/2009-July/001538.html the sizes are 2^32-1 for 32-bit, and 2^37 for 64-bit, however experiments show that it's somewhere under 2^37 at least on 64-bit Mac OS X.  (c) 2019 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-InferredS' cryptol'Compute a fingerprint for a bytestring.cryptolAttempt to compute the fingerprint of the file at the given path. Returns  in the case of an error.  j(c) 2015-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe S Safe-Inferred>S !"#$%&&%#$" !(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe8:U/cryptol Information about associativity.3cryptolLet op1 have fixity f1 and op2 have fixity  f2. Then compareFixity f1 f2/ determines how to parse the infix expression x op1 y op2 z@.FCLeft: (x op1 y) op2 zFCRight: x op1 (y op2 z)FCError : no parse4cryptol&The fixity used when none is provided.'()*+,-./01234/012+,-.4'()*3(c) 2015-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred 8:Z ?cryptol2A way to identify primitives: we used to use just A, but this isn't good anymore as now we have primitives in multiple modules. This is used as a key when we need to lookup details about a specific primitive. Also, this is intended to mostly be used internally, so we don't store the fixity flag of the A AcryptolIdentifiers, along with a flag that indicates whether or not they're infix operators. The boolean is present just as cached information from the lexer, and never used during comparisons.BcryptolIdentifies an entitiyGcryptol%Top-level Module names are just text.Hcryptol#Idnetifies a possibly nested moduleKcryptolNamespaces for namesRcryptolCompute a common prefix between two module paths, if any. This is basically "anti-unification" of the two paths, where we compute the longest common prefix, and the remaining differences for each module.XcryptolConvert a parameterized module's name to the name of the module containing the same definitions but with explicit parameters on each definition.mcryptol9A shortcut to make (non-infix) primitives in the prelude.3?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopq3HIJPRQSGTUVZ[\]_^`abcWXYAdefghijklKLMNOBCDEF?@mnqop  Safe-Inferred]Q cryptol:A logger provides simple abstraction for sending messages.cryptol!Send the given string to the log.cryptol0Send the given string with a newline at the end.cryptolSend the given value using its & instance. Adds a newline at the end.cryptol#A logger that ignores all messages.cryptolLog to the given handle.cryptolLog to stdout.cryptolLog to stderr.cryptol#Just use this function for logging.   (c) 2014-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe?^cryptol:Apply a function to all elements of a container. Returns  if nothing changed, and Just container otherwise.cryptol5Apply functions to both elements of a pair. Returns  if neither changed, and  Just pair otherwise. (c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe 8:f}cryptol3Information about an infix expression of some sort.cryptoloperatorcryptol left argumentcryptolright argumentcryptoloperator fixitycryptol&Fixity information for infix operatorscryptolPrint a name in prefix: f a b or (+) a b)cryptol#Print a name as an infix operator: a + bcryptol*How to display names, inspired by the GHC  Outputable module. Getting a value of  from the NameDisp function indicates that the display has no opinion on how this name should be displayed, and some other display should be tried out. cryptolAlways show an exponentcryptolOnly show exponent when neededcryptolUse this many significant digiscryptol*Show this many digits after floating pointcryptol Use the correct number of digitscryptol*How to pretty print things when evaluatingcryptol%Never qualify names from this module.cryptolCompose two naming environments, preferring names from the left environment.cryptol Get the format for a name. When 2 is returned, the name is not currently in scope.cryptol1Produce a document in the context of the current .cryptol5Fix the way that names are displayed inside of a doc.cryptol.Pretty print an infix expression of some sort.cryptol1Display a numeric value as an ordinal (e.g., 2nd)cryptol9The suffix to use when displaying a number as an oridinalcryptolPrint a comma-separated list. Lay out each item on a single line if it will fit. If an item requires multiple lines, then start it on its own line.cryptol1Non-infix leaves are printed with this precedencecryptol+pattern to check if sub-thing is also infixcryptol"Pretty print this infix expression6665 (c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNonehh (c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe>?icryptolThis packages together a type with some names to be used to display the variables. It is used for pretty printing types.cryptolExpand a list of base names into an infinite list of variations. Safe-Inferred8:lcryptolvalue, base, number of digitscryptol value, base.cryptolcharacter literalcryptol(qualified) identifiercryptolstring literalcryptol.hello or .123cryptolkeywordcryptoloperatorcryptolsymbolcryptolvirtual token (for layout)cryptolwhite space tokencryptol error tokencryptol>The named operators are a special case for parsing types, and 8 is used for all other cases that lexed as an operator.cryptol.Virtual tokens, inserted by layout processing.(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe 8:rcryptolSelectors are used for projecting from various components. Each selector has an option spec to specify the shape of the thing that is being selected. Currently, there is no surface syntax for list selectors, but they are used during the desugaring of patterns.cryptolZero-based tuple selection. Optionally specifies the shape of the tuple (one-based).cryptolRecord selection. Optionally specifies the shape of the record.cryptol=List selection. Optionally specifies the length of the list.cryptol3Display the thing selected by the selector, nicely.cryptol2The name of a selector (e.g., used in update code)cryptolShow a list of selectors as they appear in a nested selector in an update.(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe#$5678:scryptolAn empty range.Caution: using this on the LHS of a use of rComb will cause the empty source to propagate.(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Trustworthys(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe8:}Ncryptol(Natural numbers with an infinity elementcryptol&Some algebraic properties of interest: 1 * x = x x * (y * z) = (x * y) * z 0 * x = 0 x * y = y * x x * (a + b) = x * a + x * bcryptol&Some algebraic properties of interest: x ^ 0 = 1 x ^ (n + 1) = x * (x ^ n) x ^ (m + n) = (x ^ m) * (x ^ n) x ^ (m * n) = (x ^ m) ^ ncryptolnSub x y = Just z iff z is the unique value such that Add y z = Just x. cryptol Rounds down. https://github.com/ghc/ghc/blob/master/compiler/parser/Lexer.x0 Safe-Inferred +9cryptolVirtual layout blockcryptol6An explicit layout block, expecting this ending token.cryptol+These tokens start an implicit layout blockcryptol)These tokens end an implicit layout blockcryptolThese tokens start an explicit "paren" layout block. If so, the result contains the corresponding closing paren.cryptol&Make a virtual token of the given type  (c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Trustworthy cryptolReturns the tokens in the last position of the input that we processed. White space is removed, and layout processing is done as requested. This stream is fed to the parser.cryptolReturns the tokens and the last position of the input that we processed. The tokens include whte space tokens.(c) 2015-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Trustworthy  #$8:>?XcryptolA mapping from an identifier defined in some module to its real name.cryptol)A monad for easing the use of the supply.cryptol/Information about the binding site of the name.cryptol2This name refers to a declaration from this modulecryptol+This name is a parameter (function or type)cryptolCompare two names by the way they would be displayed. This is used to order names nicely when showing what's in scopecryptol9Pretty-print a name with its source location information.cryptol;Primtiives must be in a top level module, at least for now.cryptol)Retrieve the next unique from the supply.cryptolThis should only be used once at library initialization, and threaded through the rest of the session. The supply is started at 0x1000 to leave us plenty of room for names that the compiler needs to know about (wired-in constants).cryptol"Make a new name for a declaration.cryptolMake a new parameter name.cryptolIt's assumed that we're looking things up that we know already exist, so this will panic if it doesn't find the name.cryptolIt's assumed that we're looking things up that we know already exist, so this will panic if it doesn't find the name.+HIJKLMN+KLMNHIJSafe 8:3cryptolBuilt-in type functions. If you add additional user-visible constructors, please update primTys in Cryptol.Prims.Types.cryptol  : Num -> Num -> Numcryptol  : Num -> Num -> Numcryptol  : Num -> Num -> Numcryptol  : Num -> Num -> Numcryptol  : Num -> Num -> Numcryptol  : Num -> Num -> Numcryptol  : Num -> Numcryptol  : Num -> Num -> Numcryptol  : Num -> Num -> Numcryptol  : Num -> Num -> Numcryptol  : Num -> Num -> Numcryptol : Num -> Num -> Num -> Num Example: ,[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]cryptol1-1 constants. If you add additional user-visible constructors, please update primTys.cryptolNumberscryptolInfcryptolBitcryptolIntegercryptolFloatcryptol Z _cryptol Rationalcryptol  Array _ _cryptol [_] _cryptol _ -> _cryptol  (_, _, _)cryptolAn abstract typecryptolPredicate symbols. If you add additional user-visible constructors, please update primTys.cryptol _ == _cryptol _ /= _cryptol _ >= _cryptol fin _cryptol prime _cryptolHas sel type field does not appear in schemascryptol Zero _cryptol Logic _cryptol Ring _cryptol  Integral _cryptol Field _cryptol Round _cryptol Eq _cryptol Cmp _cryptol  SignedCmp _cryptol  Literal _ _cryptol LiteralLessThan _ _cryptol FLiteral _ _ _cryptolValidFloat _ _9 constraints on supported floating point representaitonscryptol/This is useful when simplifying things in placecryptolDittocryptolType constants.cryptolKinds, classify types.cryptolThis is used for pretty prinitng. XXX: it would be nice to just rely in the info from the Prelude.5Safe > cryptolCheck that a value satisfies multiple patterns. For example, an "as" pattern is  (__ &&& p).cryptol%Match a value, and modify the result.cryptol*Match a value, and return the given resultcryptol View pattern.cryptolVariable pattern.cryptolConstant pattern.cryptolPredicate patterncryptolCheck for exact value.cryptol3Match a pattern, using the given default if valure.cryptol2Match an irrefutable pattern. Crashes on faliure.(c) 2020 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-InferredcryptolAn "order insensitive" datastructure. The fields can be accessed either according to a "canonical" order, or based on a "display" order, which matches the order in which the fields were originally specified.cryptol*Return the fields in this record as a set.cryptol2The order in which the fields originally appeared.cryptolRetrieve the elements of the record in canonical order of the field namescryptol6Return a list of field/value pairs in canonical order.cryptol4Return a list of field/value pairs in display order.cryptolGenerate a record from a list of field/value pairs. Precondition: each field identifier appears at most once in the given list.cryptolGenerate a record from a list of field/value pairs. If any field name is repeated, the first repeated name/value pair is returned. Otherwise the constructed record is returned.cryptolGenerate a record from a list of field/value pairs, and also provide the "display" order for the fields directly. Precondition: each field identifier appears at most once in each list, and a field name appears in the display order iff it appears in the field list.cryptolLookup the value of a fieldcryptolUpdate the value of a field by applying the given function. If the field is not present in the record, return Nothing.cryptolTraverse the elements of the given record map in canonical order, applying the given action.cryptol5Apply the given function to each element of a record.cryptolThe function recordMapAccum threads an accumulating argument through the map in canonical order of fields.cryptolZip together the fields of two records using the provided action. If some field is present in one record, but not the other, an  Either a a will be returned, indicating which record is missing the field, and returning the name of the missing field.The  displayOrder of the resulting record will be taken from the first argument (rather arbitrarily).cryptolPure version of Safe #$8:>?l,cryptol;The type is "simple" (i.e., it contains no type functions).cryptol#Information about an abstract type.cryptol Named recordscryptol Type synonym.cryptolNamecryptol ParameterscryptolEnsure body is OKcryptol Definitioncryptol Documentationcryptol#The type is supposed to be of kind .cryptol7A type annotated with information on how it came about.cryptol=Explains how this type came to be, for better error messages.cryptolName of module parametercryptolA variable in a signaturecryptolSource code that gave risecryptol DescriptioncryptolType variables.cryptolUnique, kind, ids of bound type variables that are in scope. The last field gives us some info for nicer warnings/errors.cryptolThe internal representation of types. These are assumed to be kind correct.cryptolType constant with argscryptolType variable (free or bound)cryptolThis is just a type annotation, for a type that was written as a type synonym. It is useful so that we can use it to report nicer errors. Example:  TUser T ts t is really just the type t# that was written as T ts by the user. cryptol Record typecryptol A newtypecryptolType parameters.cryptolParameter identifiercryptolKind of parametercryptol#What sort of type parameter is thiscryptol"A description for better messages.cryptol The types of polymorphic values.cryptolA value parameter of a module.cryptolA type parameter of a module.cryptolThe number of the parameter in the module This is used when we move parameters from the module level to individual declarations (type synonyms in particular)cryptol7Get the names of something that is related to the tvar.cryptolCompute the set of all Props that are implied by the given prop via superclass constraints.cryptolSplit up repeated occurances of the given binary type-level function.cryptolMake a function type.cryptol"Eliminate outermost type synonyms.cryptolMake an error value of the given type to replace the given malformed type (the argument to the error function)cryptolEquality for numeric types.cryptol+Make a greater-than-or-equal-to constraint.cryptolA Has1 constraint, used for tuple and record selection.cryptolThe precedence levels used by this pretty-printing instance correspond with parser non-terminals as follows:0-1: type2:  infix_type3: app_type4: dimensions atype5: atypecryptol [8] cryptol [8] a cryptol Bit cryptol 10 cryptol a cryptolA type variable or synonym cryptol `{ x = [8], y = Integer } cryptol { x : [8], y : [32] } cryptol  ([8], [32]) cryptol_, just some type. cryptolLocation information cryptol  (ty) cryptol  ty + ty cryptol  x cryptol  _ cryptol  (x,y,z) cryptol  { x = (a,b,c), y = z } cryptol  [ x, y, z ] cryptol  x : [8] cryptol  (x # y) cryptolLocation information cryptolp <- e cryptol#Are we setting or updating a field. cryptolnon-empty list  x.y = e cryptolDescription of functions. Only trivial information is provided here by the parser. The NoPat pass fills this in as required. cryptol$Name of this function, if it has one cryptolnumber of previous arguments to this function bound in surrounding lambdas (defaults to 0) cryptol  x cryptol  0x10 cryptol  -1 cryptol  ~1 cryptol  generate f cryptol  (1,2,3) cryptol  { x = 1, y = 2 } cryptol  e.l cryptol  { r | x = e } cryptol  [1,2,3] cryptol  [1, 5 .. 117 : t] cryptol  [1 .. 10 by 2 : t ] cryptol  [10 .. 1 down by 2 : t ] cryptol  [ 1 .. < 10 : t ] cryptol  [1, 3 ...] cryptol  [ 1 | x <- xs ] cryptol  f x cryptol  f `{x = 8}, f`{8} cryptol  if ok then e1 else e2 cryptol  1 + x where { x = 2 } cryptol  1 : [8] cryptol `(x + 1), x is a type cryptol  \x y -> x cryptolposition annotation cryptol splitAt x  (Introduced by NoPat) cryptol (e)  (Removed by Fixity) cryptol a + b  (Removed by Fixity) cryptol Literals. cryptol0x10 (HexLit 2) cryptol a cryptol 1.2e3 cryptol "hello" cryptol&Information about fractional literals. cryptol;Infromation about the representation of a numeric constant. cryptoln-digit binary literal cryptoln-digit octal literal cryptoloverloaded decimal literal cryptoln-digit hex literal cryptolpolynomial literal cryptolA top-level module declaration. cryptol%Export information for a declaration. cryptol1Input at the REPL, which can be an expression, a let+ statement, or empty (possibly a comment). cryptol0A declaration for a type with no implementation. cryptol:parameters are in the order used by the type constructor. cryptol Type name cryptol Type params cryptolBody cryptolBindings. Notes:The parser does not associate type signatures and pragmas with their bindings: this is done in a separate pass, after de-sugaring pattern bindings. In this way we can associate pragmas and type signatures with the variables defined by pattern bindings as well.Currently, there is no surface syntax for defining monomorphic bindings (i.e., bindings that will not be automatically generalized by the type checker. However, they are useful when de-sugaring patterns. cryptol Defined thing cryptol Parameters cryptol Definition cryptolOptional type sig cryptolInfix operator? cryptolOptional fixity info cryptolOptional pragmas cryptolIs this a monomorphic binding cryptolOptional doc string cryptol&The list of names following an import. cryptolAn import declaration. cryptolA value parameter cryptolname of value parameter cryptolschema for parameter cryptoloptional documentation cryptolinfo for infix use cryptolA type parameter cryptolname of type parameter cryptolkind of parameter cryptoloptional documentation cryptolinfo for infix use cryptolnumber of the parameter cryptol9A group of recursive bindings, introduced by the renamer. cryptol@newtype T as = t cryptol  include File cryptol parameter type T : # cryptol !parameter type constraint (fin T) cryptol parameter someVal : [256] cryptol Nested module cryptolAn import declaration cryptolA parsed module. cryptolName of the module cryptolFunctor to instantiate (if this is a functor instnaces) , mImports :: [Located Import] -- ^ Imports for the module cryptolDeclartions for the module cryptol#A string with location information. cryptol(An identifier with location information. cryptol!A name with location information. cryptolConversational3 printing of kinds (e.g., to use in error messages)'()*+,-./01234AGghijk AghijkG  /012 +,-.4'()*3    (c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred   l(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe 8:K cryptol=Keep track of the type parameters as they appear in the inputcryptolInput fields are reversed!cryptolInput expression are reversedcryptolWARNING: This is a bit of a hack. It is used to represent anonymous type applications.cryptolGenerate a signature and a primitive binding. The reason for generating both instead of just adding the signature at this point is that it means the primitive declarations don't need to be treated differently in the noPat pass. This is also the reason we add the doc to the TopLevel constructor, instead of just place it on the binding directly. A better solution might be to just have a different constructor for primitives.cryptolFix-up the documentation strings by removing the comment delimiters on each end, and stripping out common prefixes on all the remaining lines.cryptolMake an ordinary modulecryptol'Make an unnamed module---gets the name Main.cryptol/Make a module which defines a functor instance.       "(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred֫ cryptolThe names defined by a newtype. cryptol4The names defined and used by a single declarations. cryptol/The names defined and used by a single binding. cryptolThe names defined by a pattern. These will always be unqualified names. cryptol;Remove some defined variables from a set of free variables. cryptol;Remove some defined variables from a set of free variables. cryptol8The type names defined and used by a single declaration. cryptolThe type names used by a prop. cryptol8Compute the type synonyms/type variables used by a type. #(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred #$8:>x cryptol$Eliminate all patterns in a program. $(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred 8:ڧ cryptolidentifed by location in source cryptol+Multiple imported symbols contain this name cryptol%Some name not bound to any definition cryptol8An environment has produced multiple overlapping symbols cryptolexpected, actual. When a name is missing from the expected namespace, but exists in another cryptol)When the fixity of two operators conflict cryptol5When it's not possible to produce a Prop from a Type. cryptol6When a builtin type/type-function is used incorrectly. cryptol)When a builtin type is named in a binder. cryptol#When record updates overlap (e.g., { r | x = e1, x.y = e2 })  %(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred#$8:2 cryptol Name of thing cryptolType cryptolPragmas cryptolIs this an infix thing cryptolFixity information cryptol Documentation cryptolConstraints on param. types cryptolThe resulting interface generated by a module that has been typechecked. cryptol Module name cryptolExported definitions cryptolPrivate defintiions cryptol+Uninterpreted constants (aka module params) cryptolThe public declarations in all modules, including nested The modules field contains public functors Assumes that we are not a functor. cryptol$Produce a PrimMap from an interface.NOTE: the map will expose both public and private names.' ' & Safe-Inferred8  cryptolAdd a binding name to the export list, if it should be exported. cryptolAdd a type synonym name to the export list, if it should be exported. cryptol&Check to see if a binding is exported. cryptol+Check to see if a type synonym is exported. '(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe #$8:>? cryptolMutually recursive declarations cryptolNon-recursive declaration cryptolType arguments are the length and element type of the sequence expression cryptol"List value (with type of elements) cryptol Tuple value cryptol Record value cryptolElimination for tuplerecordlistcryptolChange the value of a field. The included type gives the type of the record being updatedcryptol If-then-elsecryptolList comprehensions The types cache the length of the sequence and its element type.cryptolUse of a bound variablecryptolFunction ValuecryptolType applicationcryptolFunction applicationcryptolFunction valuecryptolSource location informationcryptolProof abstraction. Because we don't keep proofs around we don't need to name the assumption, but we still need to record the assumption. The assumption is the 0 term, which should be of kind .cryptolIf  e : p => t, then EProofApp e : t+, as long as we can prove p.We don't record the actual proofs, as they are not used for anything. It may be nice to keep them around for sanity checking.cryptolA Cryptol module.cryptolInterfaces of submodules, including functors. This is only the directly nested modules. Info about more nested modules is in the corresponding interface. cryptolIs this a parameterized module?cryptolConstruct a primitive, given a map to the unique primitive name.cryptolMake an expression that is error% pre-applied to a type and a message.cryptolDeconstruct an expression, typically polymorphic, into the types and proofs to which it is applied. Since we don't store the proofs, we just return the number of proof applications. The first type is the one closest to the expr.+,-.       +,-.((c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe 567>)(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred$cryptol&All ways to split a type in the form: a + t1, where a is a variable.cryptol,Check if we can express a type in the form: a + t1.cryptol,Check if we can express a type in the form: k + t1, where k is a constant > 0. This assumes that the type has been simplified already, so that constants are floated to the left. cryptol,Check if we can express a type in the form: k * t1, where k is a constant > 1. This assumes that the type has been simplified already, so that constants are floated to the left. *(c) 2015-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred6 cryptollower bound (inclusive)cryptolupper bound (inclusive) If there is no upper bound, then all *natural* numbers.cryptol!Only meaningful for numeric typescryptol1What we learn about variables from a single prop.cryptolFinite positive number.  [1 .. inf).cryptolReturns  , when the intervals definitely overlap, and   otherwise.cryptolIntersect two intervals, yielding a new one that describes the space where they overlap. If the two intervals are disjoint, the result will be .cryptol Any valuecryptolAny finite valuecryptolExactly this value##+ Safe-Inferred 8:pcryptolSolved, assuming the sub-goals.cryptolWe could not solve the goal.cryptolThe goal can never be solved.  ,(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred( cryptolThis places constraints on the floating point numbers that we can work with. This is a bit of an odd check, as it is really a limitiation of the backend, and not the language itself.On the other hand, it helps us give sane results if one accidentally types a polymorphic float at the REPL. Hopefully, most users will stick to particular FP sizes, so this should be quite transparent.cryptol1Solve a Zero constraint by instance, if possible.cryptol2Solve a Logic constraint by instance, if possible.cryptol1Solve a Ring constraint by instance, if possible.cryptol6Solve an Integral constraint by instance, if possible.cryptol2Solve a Field constraint by instance, if possible.cryptol2Solve a Round constraint by instance, if possible.cryptolSolve Eq constraints.cryptolSolve Cmp constraints.cryptolSolve SignedCmp constraints.cryptol'Solving fractional literal constraints.cryptolSolve Literal constraints.cryptolSolve Literal constraints.  -(c) 2015-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred.Nonencryptol Try to solve t1 = t2cryptol Try to solve t1 /= t2cryptol Try to solve t1 >= t2/ Trustworthy0(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe #$567>?cryptolReplaces free variables. To prevent space leaks when used with large  values, every instance of > should satisfy a strictness property: Forcing evaluation of  s x> should also force the evaluation of all recursive calls to  s7. This ensures that unevaluated thunks will not cause # values to be retained on the heap.cryptol1Reasons to reject a single-variable substitution.cryptol- maps to a type containing the same variable.cryptol maps to a type containing one or more out-of-scope bound variables.cryptol& maps to a type with a different kind.cryptolA 0 value represents a substitution that maps each  to a .(Invariant 1: If there is a mapping from TVFree _ _ tps _ to a type t, then t must not mention (directly or indirectly) any type parameter that is not in tps. In particular, if t contains a variable TVFree _ _ tps2 _, then tps2 must be a subset of tps. This ensures that applying the substitution will not permit any type parameter to escape from its scope.Invariant 2: The substitution must be idempotent, in that applying a substitution to any  in the map should leave that  unchanged. In other words,  values in the range of a  should not mention any  in the domain of the . In particular, this implies that a substitution must not contain any recursive variable mappings.9Invariant 3: The substitution must be kind correct: Each $ in the substitution must map to a  of the same kind.cryptolA defaulting substitution maps all otherwise-unmapped free variables to a kind-appropriate default type (Bit for value types and 0 for numeric types).cryptolMakes a substitution out of a list. WARNING: We do not validate the list in any way, so the caller should ensure that we end up with a valid (e.g., idempotent) substitution.cryptolMakes a substitution out of a list. WARNING: We do not validate the list in any way, so the caller should ensure that we end up with a valid (e.g., idempotent) substitution.cryptol? $55 Safe-Inferred cryptol,Generate an Iface from a typechecked module.6(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe &8:>? cryptolInformation about how a constraint came to be, used in error reporting.cryptol%Computing shape of list comprehensioncryptolUse of a split patterncryptol+A type signature in a pattern or expressioncryptol Instantiation of this expressioncryptol#Just defaulting on the command linecryptolUse of a partial type function.cryptol/Constraints arising from type-checking patternscryptol#Instantiating a parametrized modulecryptolDelayed implication constraints, arising from user-specified type sigs.cryptolSignature that gave rise to this constraint Nothing means module top-levelcryptolA solution for a cryptol3Select a specific field from the input expsression.cryptol?cryptol1An SMT solver packed with a logger for debugging.cryptolStart a fresh solver instancecryptolShut down a solver instancecryptol3Execute a computation with a fresh solver instance.cryptol"Returns goals that were not provedcryptol4Check if the given goals are known to be unsolvable.cryptol Assumes no And  8Safe 8:> 0cryptol?Various errors that might happen during type checking/inferencecryptolExpected kind, inferred kindcryptolNumber of extra parameters, kind of result (which should not be of the form _ -> _)cryptol.A type variable was applied to some arguments.cryptol$Type-synonym, number of extra paramscryptol/Who is missing params, number of missing paramscryptol+The type synonym declarations are recursivecryptolExpected type, inferred typecryptol'Unification results in a recursive typecryptolA constraint that we could not solve, usually because there are some left-over variables that we could not infer.cryptolA constraint that we could not solve and we know it is impossible to do it.cryptol3A constraint (with context) that we could not solvecryptolType wild cards are not allowed in this context (e.g., definitions of type synonyms).cryptolUnification variable depends on quantified variables that are not in scope.cryptolQuantified type variables (of kind *) need to match the given type, so it does not work for all types.cryptolToo many positional type arguments, in an explicit type instantiationcryptolKind other than   or # given to parameter of type synonym, newtype, function signature, etc.cryptolCould not determine the value of a numeric type variable, but we know it must be at least as large as the given type (or unconstrained, if Nothing).cryptol Bare expression of the form `{_}cryptolThis is for errors that don't fit other cateogories. We should not use it much, and is generally to be used for transient errors, which are due to incomplete implementation.cryptol-Should the first error suppress the next one.cryptolWhen we have multiple errors on the same location, we show only the ones with the has highest rating according to this function.cryptol=This picks the names to use when showing errors and warnings.$$9(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe #$+8:GMcryptolThis is what's returned when we lookup variables during kind checking.cryptolLocally bound variable.cryptolAn outer binding.cryptolkinds of (known) vars.cryptol,Do we allow wild cards in the given context.cryptollazy map, with tparams.cryptolare type-wild cards allowed?cryptol"Read-write component of the monad.cryptolCollected errorscryptolCollected warningscryptolAccumulated substitutioncryptolThese keeps track of what existential type variables are available. When we start checking a function, we push a new scope for its arguments, and we pop it when we are done checking the function body. The front element of the list is the current scope, which is the only thing that will be modified, as follows. When we encounter a existential type variable: 1. we look in all scopes to see if it is already defined. 2. if it was not defined, we create a fresh type variable, and we add it to the current scope. 3. it is an error if we encounter an existential variable but we have no current scope.cryptolSelector constraints that have been solved (ref. iSolvedSelectorsLazy)cryptolOrdinary constraintscryptol*Tuple/record projection constraints. The   is the "name" of the constraint, used so that we can name its solution properly. cryptol;Nested scopes we are currently checking, most nested first.cryptolTypes of variables that we know about. We don't worry about scoping here because we assume the bindings all have different names.cryptol!Read-only component of the monad.cryptolSource code being analysedcryptolType of variable that are in scope These are only parameters vars that are in recursive component we are checking at the moment. If a var is not there, keep looking in the cryptolType variable that are in scopecryptolThese are things we know about, but are not part of the modules we are currently constructing. XXX: this sould probably be an interfacecryptolNOTE: This field is lazy in an important way! It is the final version of  in , and the two are tied together through recursion. The field is here so that we can look thing up before they are defined, which is OK because we don't need to know the results until everything is done.cryptolWhen this flag is set to true, bindings that lack signatures in where-blocks will never be generalized. Bindings with type signatures, and all bindings at top level are unaffected.cryptolWhen this flag is true, retain source location information in typechecked termscryptolThe results of type inference.cryptolWe found some errorscryptolType inference was successful.cryptol*This is used for generating various names.cryptol&Information needed for type inference.cryptolLocation of program sourcecryptolVariables that are in scopecryptolType synonyms that are in scopecryptolNewtypes in scopecryptolAbstract types in scopecryptolType parameterscryptolConstraints on parameterscryptolValue parameterscryptolPrivate state of type-checkercryptol=Should local bindings without signatures be monomorphized?cryptolAre we tracking call stacks?cryptol&Where to look for Cryptol theory file.cryptolThis is used when the type-checker needs to refer to a predefined identifier (e.g., number).cryptol$The supply for fresh name generationcryptol"Solver connection for typecheckingcryptolThe initial seeds, used when checking a fresh program. XXX: why does this start at 10?cryptolThe monadic computation is about the given range of source code. This is useful for error reporting.cryptol1This is the current range that we are working on.cryptolReport an error.cryptolReport an error.cryptolRetrieve the mapping between identifiers and declarations in the prelude.cryptolRecord some constraints that need to be solved. The string explains where the constraints came from.cryptolThe constraints are removed, and returned to the caller. The substitution IS applied to them. cryptol'Add a bunch of goals that need solving.cryptolCollect the goals emitted by the given sub-computation. Does not emit any new goals.cryptolRecord a constraint that when we select from the first type, we should get a value of the second type. The returned function should be used to wrap the expression from which we are selecting (i.e., the record or tuple). Plese note that the resulting expression should not be forced before the constraint is solved.cryptol)Add a previously generate has constrainedcryptolGet the Has constraints. Each of this should either be solved, or added back using .cryptolSpecify the solution ( Expr -> Expr) for the given constraint ( ).cryptol=Generate a fresh variable name to be used in a local binding.cryptolGenerate a new name for a goal.cryptol"Generate a new free type variable.cryptolGenerate a new free type variable that depends on these additional type parameters.cryptolCheck that the given "flavor" of parameter is allowed to have the given type, and raise an error if notcryptol"Generate a new free type variable.cryptolGenerate an unknown type. The doc is a note about what is this type about.cryptol8Record that the two types should be syntactically equal.cryptolApply the accumulated substitution to something with free type variables.cryptol5Get the substitution that we have accumulated so far.cryptolAdd to the accumulated substitution, checking that the datatype invariant for  is maintained.cryptolVariables that are either mentioned in the environment or in a selector constraint.cryptolLookup the type of a variable.cryptol Lookup a type variable. Return  if there is no such variable in scope, in which case we must be dealing with a type constant.cryptol(Lookup the definition of a type synonym.cryptol"Lookup the definition of a newtypecryptol#Lookup the kind of a parameter typecryptol+Lookup the schema for a parameter function.cryptolCheck if we already have a name for this existential type variable and, if so, return the definition. If not, try to create a new definition, if this is allowed. If not, returns nothing.cryptol6Returns the type synonyms that are currently in scope.cryptol3Returns the newtype declarations that are in scope.cryptol9Returns the abstract type declarations that are in scope.cryptol,Returns the parameter functions declarationscryptol*Returns the abstract function declarationscryptol'Constraints on the module's parameters.cryptol6Get the set of bound type variables that are in scope.cryptol9Return the keys of the bound variables that are in scope.cryptol.Retrieve the value of the `mono-binds` option.cryptolWe disallow shadowing between type synonyms and type variables because it is confusing. As a bonus, in the implementation we don't need to worry about where we lookup things (i.e., in the variable or type synonym environment. cryptolThe sub-computation is performed with the given type parameter in scope.cryptolExecute the given computation in a new top scope. The sub-computation would typically be validating a module.cryptolUpdate the current scope (first in the list). Assumes there is one.cryptol/Get an environment combining all nested scopes.cryptolThe sub-computation is performed with the given type-synonym in scope.cryptolThe sub-computation is performed with the given abstract function in scope.cryptol)Add some assumptions for an entire modulecryptolPerform the given computation in a new scope (i.e., the subcomputation may use existential type variables). This is a different kind of scope from the nested modules one.cryptolThe sub-computation is performed with the given variable in scope.cryptolThe sub-computation is performed with the given variables in scope.cryptolThe sub-computation is performed with the given variables in scope.cryptol.The arguments to this function are as follows:9(type param. name, kind signature (opt.), type parameter)The type parameter is just a thunk that we should not force. The reason is that the parameter depends on the kind that we are in the process of computing.As a result we return the value of the sub-computation and the computed kinds of the type parameters. cryptol*Check if a name refers to a type variable.cryptol'Are type wild-cards OK in this context?cryptolReports an error.cryptolGenerate a fresh unification variable of the given kind. NOTE: We do not simplify these, because we end up with bottom. See mn* XXX: Perhaps we can avoid the recursion?cryptol(Lookup the definition of a type synonym.cryptol#Lookup the definition of a newtype.cryptol6Replace the given bound variables with concrete types.cryptolRecord the kind for a local type variable. This assumes that we already checked that there was no other valid kind for the variable (if there was one, it gets over-written). cryptolThe sub-computation is about the given range of the source code.cryptol See comment:(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafeK+cryptolSolve has-constraints.cryptolchanges, solved;(c) 2015-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-InferredKcryptolexpected, actualcryptolexpected a mono type, got this< Safe-InferredOcryptol#We default constraints of the form  Literal t a and FLiteral m n r a.For  Literal t a3 we examine the context of constraints on the type a" to decide how to default. If Logic a is required, we cannot do any defaulting. Otherwise, we default to either Integer or Rational/. In particular, if we need to satisfy the Field a, constraint, we choose Rational and otherwise we choose Integer.For  FLiteral t a we always default to Rational.cryptolTry to pick a reasonable instantiation for an expression with the given type. This is useful when we do evaluation at the REPL. The resulting types should satisfy the constraints of the schema. The parameters should be all of numeric kind, and the props should als be numeric =(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe#$QcryptolTry to clean-up any left-over constraints after we've checked everything in a module. Typically these are either trivial things, or constraints on the module's type parameters.cryptolProve an implication, and return any improvements that we computed. Records errors, if any of the goals couldn't be solved.>(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafeScryptolCheck a type signature. Returns validated schema, and any implicit constraints that we inferred.cryptolCheck a module parameter declarations. Nothing much to check, we just translate from one syntax to another.cryptol!Check a type-synonym declaration.cryptol'Check a constraint-synonym declaration.cryptolCheck a newtype declaration. XXX: Do something with constraints.?(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred TE  @(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe #$&+W!cryptolInfer the type of an expression, and translate it to a fully elaborated core term.cryptol!inferBinds isTopLevel isRec binds; performs inference for a strongly-connected component of  s. If any of the members of the recursive group are already marked as monomorphic, then we don't do generalization. If  isTopLevel is true, any bindings without type signatures will be generalized. If it is false, and the mono-binds flag is enabled, no bindings without type signatures will be generalized, but bindings with signatures will be unaffected.A(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred >?X1cryptolNote that this assumes that this pass will be run only once for each module, otherwise we will get name collisions.B Safe-InferredX[C(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred #$+5678:>?c=cryptol"Things that define exported names.cryptolDo somethign in context. If  than we are working with a local declaration. Otherwise we are at the top-level of the given module. cryptolThe  is used by the renamer to determine what identifiers refer to.cryptol&All names mentioned in the environmentcryptol"Get the names in a given namespacecryptol&Resolve a name in the given namespace.cryptolReturn a list of value-level names to which this parsed name may refer.cryptolReturn a list of type-level names to which this parsed name may refer.cryptol7Singleton renaming environment for the given namespace.cryptol*Singleton expression renaming environment.cryptol$Singleton type renaming environment.cryptolMerge two name maps, collapsing cases where the entries are the same, and producing conflicts otherwise.cryptolGenerate a mapping from  PrimIdent to ! for a given naming environment.cryptol8Generate a display format based on a naming environment.cryptol9Produce sets of visible names for types and declarations.NOTE: if entries in the NamingEnv would have produced a name clash, they will be omitted from the resulting sets.cryptolQualify all symbols in a  with the given prefix.cryptol9Like mappend, but when merging, prefer values on the lhs.cryptol Generate a  using an explicit supply.cryptolAdapt the things exported by something to the specific import/open.cryptolInterpret an import in the context of an interface, to produce a name environment for the renamer, and a  for pretty-printing.cryptolGenerate a naming environment from a declaration interface, where none of the names are qualified.cryptolCompute an unqualified naming environment, containing the various module parameters.cryptol0The naming environment for a single declaration.cryptolThe naming environment for a single module. This is the mapping from unqualified names to fully qualified names with uniques.cryptol5Generate the naming environment for a type parameter.cryptolIntroduce the namecryptolGenerate a type renaming environment from the parameters that are bound by this schema.cryptolProduce a naming environment from an interface file, that contains a mapping only from unqualified names to qualified ones.cryptolThe import declarations cryptolAll public things coming in cryptolThe import declarations cryptol Declarations of imported module **D(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred#$+?mcryptolCheck for overlap and shadowingcryptolOnly check for overlapcryptolDon't check the environmentcryptolHow many times did we refer to each name. Used to generate warnings for unused definitions.cryptol/keeps track of names *used* by something. see cryptol1keeps track of the dependencies for things. see cryptolInfo about imported thingscryptol Current module we are working oncryptol'Information needed to do some renaming.cryptolUse to make new namescryptolWe are renaming things in herecryptolThis is what's in scopecryptol;Indicates if a name is in a binding poisition or a use sitecryptol(Record an error. XXX: use a better namecryptolRename something. All name uses in the sub-computation are assumed to be dependenices of the thing.cryptolThis is used when renaming a group of things. The result contains dependencies between names defines and the group, and is intended to be used to order the group members in dependency order.cryptolp-cryptolConvert a module instantiation into a partial module. The resulting module is incomplete because it is missing the definitions from the instantiation.cryptolParametrized module cryptolName of the new module cryptol Type params cryptolValue parameters cryptol ccsfn = ccs ++ dropCommonPrefix ccs ccsfnwheredropCommonPrefix A B -- returns the suffix of B after removing any prefix common -- to both A and B.cryptol+Add a call frame to the top of a call stackcryptolTest if a value is "ready", which means that it requires no computation to return.cryptolDelay the given evaluation computation, returning a thunk which will run the computation when forced. Run the   computation instead if the resulting thunk is forced during its own evaluation.cryptolBegin executing the given operation in a separate thread, returning a thunk which will await the completion of the computation when forced.cryptolProduce a thunk value which can be filled with its associated computation after the fact. A preallocated thunk is returned, along with an operation to fill the thunk with the associated computation. This is used to implement recursive declaration groups.cryptolGet the current call stackcryptol,Execute the action with the given call stackcryptol-Run the given action with a modify call stackcryptol$Execute the given evaluation action.cryptolLift an   computation into the  monad.cryptolPanic from an Eval context.cryptolFor when we know that a word is too wide and will exceed gmp's limits (though words approaching this size will probably cause the system to crash anyway due to lack of memory).cryptol&call stack of the application context cryptol)call stack of the function being applied cryptolComputation to delay cryptol?Optional backup computation to run if a tight loop is detected cryptolmessage for the  loop' exception if a tight loop is detected cryptol%A name to associate with this thunk. $$I Safe-Inferred +; cryptol=Make LibBF options for the given precision and rounding mode.cryptol/Mapping from the rounding modes defined in the op to the rounding modes of LibBF.cryptol.Check that we didn't get an unexpected status.cryptolPretty print a floatcryptolMake a literalcryptolMake a floating point number from a rational, using the given rounding modecryptol;Convert a floating point number to a rational, if possible.cryptol;Convert a floating point number to an integer, if possible.cryptolTurn a float into raw bits. NaN& is represented as a positive "quiet" NaN (most significant bit in the significand is set, the rest of it is 0)cryptolExponent width cryptolPrecision width cryptolExponent width cryptolPrecision widht cryptol Raw bits J Safe-Inferred?BcryptolThis type class defines a collection of operations on bits, words and integers that are necessary to define generic evaluator primitives that operate on both concrete and symbolic values uniformly.cryptolCheck if an operation is "ready", which means its evaluation will be trivial.cryptolProduce a thunk value which can be filled with its associated computation after the fact. A preallocated thunk is returned, along with an operation to fill the thunk with the associated computation. This is used to implement recursive declaration groups.cryptolDelay the given evaluation computation, returning a thunk which will run the computation when forced. Run the retry computation instead if the resulting thunk is forced during its own evaluation.cryptolBegin evaluating the given computation eagerly in a separate thread and return a thunk which will await the completion of the given computation when forced.cryptolPush a call frame on to the current call stack while evaluating the given actioncryptol:Use the given call stack while evaluating the given actioncryptolApply the given function to the current call stack while evaluating the given actioncryptol*Retrieve the current evaluation call stackcryptolAttempt to render a word value as an ASCII character. Return  if the character value is unknown (e.g., for symbolic values).cryptol/Determine if this symbolic integer is a literalcryptol?cryptolThe renamed modulecryptolWhat this module definescryptolWhat's in scope in this modulecryptolImported declarationscryptolNote that after this point the -> updates have an explicit function and there are no more nested updates.cryptolRename a binding.cryptolRename a schema, assuming that none of its type variables are already in scope., , L Safe-InferredcryptolUndefined value namescryptol#Undefined type names (from newtype)cryptol'Undefined type params (e.d. mod params)cryptol9Compute the transitive closure of the given dependencies.cryptolDependencies of top-level declarations in a module. These are dependencies on module parameters or things defined outside the module.  M(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe8:LcryptolAn evaluated type of kind *. These types do not contain type variables, type synonyms, or type functions.cryptol  Bitcryptol  Integercryptol  Float e pcryptol  Z ncryptol Rationalcryptol  Array a bcryptol  [n]acryptol  [inf]tcryptol  (a, b, c )cryptol  { x : a, y : b, z : c }cryptol  a -> bcryptola named newtypecryptolan abstract typecryptol-Convert a type value back into a regular typecryptolTrue if the evaluated value is BitcryptolProduce a sequence type valuecryptolCoerce an extended natural into an integer, for values known to be finitecryptol#Evaluation for types (kind * or #).cryptol9Evaluate the body of a newtype, given evaluated argumentscryptol$Evaluation for value types (kind *).cryptol%Evaluation for number types (kind #).cryptolReduce type functions, raising an exception for undefined values.qDefines numeric compatibility shims that work with both ghc-bignum (GHC 9.0+) and integer-gmp (older GHCs).(c) 2021 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone1 cryptol  x m! computes the modular inverse of x mod m.PRECONDITION: m must be strictly positive.   (c) Galois, Inc.BSD3rdockins@galois.com experimentalNone&cryptolSimple newtype wrapping the BigNat value of the modulus of the underlying field Z p. This modulus is required to be prime.cryptolPoints in the projective plane represented in homogenous coordinates.cryptol!Inject an integer value into the  PrimeModulus/ type. This modulus is required to be prime.cryptolCompute the elliptic curve group doubling operation. In other words, if S> is a projective point on a curve, this operation computes S+S in the ECC group.In geometric terms, this operation computes a tangent line to the curve at S and finds the (unique) intersection point of this line with the curve, R; then returns the point R' , which is R reflected across the x axis.cryptolCompute the elliptic curve group addition operation for values known not to be the identity. In other words, if S and T3 are projective points on a curve, with nonzero z$ coordinate this operation computes S+T in the ECC group.In geometric terms, this operation computes a line that passes through S and T%, and finds the (unique) other point R where the line intersects the curve; then returns the point R' , which is R; reflected across the x axis. In the special case where S == T, we instead call the  ec_double8 operation, which instead computes a tangent line to S .cryptolGiven an integer k and a projective point S', compute the scalar multiplication kS , which is S added to itself k times.cryptolGiven an integer j and a projective point S#, together with another integer k and point T8 compute the "twin" scalar the scalar multiplication jS + kT. This computation can be done essentially the same number of modular arithmetic operations as a single scalar multiplication by doing some additional bookkeeping and setup.N(c) 2020 Galois, Inc.BSD3cryptol@galois.comNone &+5=cryptolThe symbolic value we computed.cryptolA malformed valuecryptolsafety predicate and result: the result only makes sense when the predicate holds.cryptolThis layer has the symbolic back-end, and can keep track of definitional predicates used when working with uninterpreted constants defined via a property. cryptolThis is the monad used for symbolic evaluation. It adds to aspects to ---WConn keeps track of the backend and collects definitional predicates, and + adds support for partially defined values cryptolA value with no context.cryptolA total value.cryptolAccess the symbolic back-endcryptolRecord a definition. addDef :: W4.Pred sym -> W4Conn sym () addDef p = W4Conn _ -> pure W4Defs { w4Defs = p, w4Result = () }Compute conjunction.cryptolCompute negation.cryptolCompute if-then-else.cryptolAdd a definitional equation. This will always be asserted when we make queries to the solver.cryptolAdd s safety condition.cryptol A fully undefined symbolic valuecryptolTry successive powers of 2 to find the first that dominates the input. We could perhaps reduce to using CLZ instead...11O(c) 2013-2020 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone#$%&+̱cryptolConcrete bitvector values: width, value Invariant: The value must be within the range 0 .. 2^width-1cryptolApply an integer function to the values of bitvectors. This function assumes both bitvectors are the same width.cryptolApply an integer function to the values of a bitvector. This function assumes the function will not require masking.cryptolSmart constructor for !s that checks for the width limitcryptol Bit-width cryptolValue cryptolMasked result cryptol Rouding mode P(c) 2013-2021 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone&258:>?_ cryptolA sequence map represents a mapping from nonnegative integer indices to values. These are used to represent both finite and infinite sequences.cryptol4Generate a finite sequence map from a list of valuescryptol9Generate an infinite sequence map from a stream of valuescryptolCreate a finite list of length n of the values from [0..n-1]# in the given the sequence emap.cryptol=Create an infinite stream of all the values in a sequence mapcryptol*Reverse the order of a finite sequence mapcryptolConcatenate the first n values of the first sequence map onto the beginning of the second sequence map.cryptolGiven a number n and a sequence map, return two new sequence maps: the first containing the values from [0..n-1], and the next containing the values from n onward.cryptolDrop the first n elements of the given .cryptolGiven a sequence map, return a new sequence map that is memoized using a finite map memo table.cryptolApply the given evaluation function pointwise to the two given sequence maps.cryptolApply the given function to each value in the given sequence mapcryptolSize of the sequence map cryptolifthenelse operation of values cryptolreindexing operation cryptol zero value cryptolsize of the sequence cryptolsequence to shift cryptol-shift amount, assumed to be in range [0,len] cryptolifthenelse operation of values cryptolconcrete shifting operation cryptolSize of the map being shifted cryptolinitial value cryptol2segments of the shift amount, in big-endian order Q(c) 2013-2021 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone&28>? cryptolFor efficiency reasons, we handle finite sequences of bits as special cases in the evaluator. In cases where we know it is safe to do so, we prefer to used a "packed word" representation of bit sequences. This allows us to rely directly on Integer types (in the concrete evaluator) and SBV's Word types (in the symbolic simulator).However, if we cannot be sure all the bits of the sequence will eventually be forced, we must instead rely on an explicit sequence of bits representation.cryptol$Force the evaluation of a word valuecryptol%Extract a subsequence of bits from a  WordValue. The first integer argument is the number of bits in the resulting word. The second integer argument is the number of less-significant digits to discard. Stated another way, the operation `extractWordVal n i w` is equivalent to first shifting w right by i! bits, and then truncating to n bits.cryptol(Force a word value into packed word formcryptol*Force a word value into a sequence of bitscryptolTurn a word value into a sequence of bits, forcing each bit. The sequence is returned in big-endian order.cryptolTurn a word value into a sequence of bits, forcing each bit. The sequence is returned in reverse of the usual order, which is little-endian order.cryptolCompute the size of a word value TODO, can we get rid of this? If feels like it should be unnecessary.cryptol*Select an individual bit from a word valuecryptolProduce a new $ from the one given by updating the i#th bit with the given bit value.cryptoloperation on word values cryptolreindexing operation cryptolword value to shift cryptol-shift amount, assumed to be in range [0,len] cryptoloperation on word values cryptolreindexing operation cryptolvalue to shift cryptolamount to shift cryptolvalue to update cryptolindex to update at cryptol fresh bit cryptolifthenelse operation of values cryptolreindexing operation cryptol zero value cryptolsize of the sequence cryptolsequence to shift cryptol shift amount R(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone&258:>?g$cryptol8Generic value type, parameterized by bit and word types.NOTE: we maintain an important invariant regarding sequence types.  must never be used for finite sequences of bits. Always use the  constructor instead! Infinite sequences of bits are handled by the & constructor, just as for other types.cryptol  { .. }cryptol  ( .. )cryptol  Bitcryptol Integer  or  Z n cryptol  Rationalcryptol [n]a / Invariant: VSeq is never a sequence of bitscryptol  [n]Bitcryptol  [inf]acryptol functionscryptolpolymorphic values (kind *)cryptolpolymorphic values (kind #)cryptolSome options for evalutaioncryptol Where to print stuff (e.g., for trace)cryptolHow to pretty print things.cryptolForce the evaluation of a valuecryptolCreate a packed word of n bits.cryptolConstruct a function valuecryptol+Functions that assume floating point inputscryptolA type lambda that expects a Type.cryptolA type lambda that expects a Type of kind #.cryptol1A type lambda that expects a finite numeric type.cryptolConstruct either a finite sequence, or a stream. In the finite case, record whether or not the elements were bits, to aid pretty-printing.cryptolExtract a bit value.cryptolExtract an integer value.cryptolExtract a rational value.cryptol Extract a finite sequence value.cryptolExtract a sequence.cryptolExtract a packed word.cryptolIf the given list of values are all fully-evaluated thunks containing bits, return a packed word built from the same bits. However, if any value is not a fully-evaluated bit, return .cryptol Extract a function from a value.cryptol,Extract a polymorphic function from a value.cryptol,Extract a polymorphic function from a value.cryptolExtract a tuple from a value.cryptolExtract a record from a value.cryptolLookup a field in a record.S(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Trustworthy #$?cryptolA test result is either a pass, a failure due to evaluating to False;, or a failure due to an exception raised during evaluationcryptol$Return a collection of random tests.cryptolGiven a (function) type, compute generators for the function's arguments. cryptolA generator for values of the given type. This fails if we are given a type that lacks a suitable random value generator. cryptolGiven a (function) type, compute data necessary for random or exhaustive testing.The first returned component is a count of the number of possible input test vectors, if the input types are finite. The second component is a list of all the types of the function inputs. The third component is a list of all input test vectors for exhaustive testing. This will be empty unless the input types are finite. The final argument is a list of generators for the inputs of the function.This function will return Nothing3 if the input type does not eventually return Bit, or if we cannot compute a generator for one of the inputs.cryptolThe random generator statecryptol%Generators for the function argumentscryptolThe function itselfcryptolHow many tests?cryptol8A list of pairs of random arguments and computed outputscryptolprogress callback cryptolfunction under test cryptolexhaustive set of test values cryptolprogress callback cryptolMaximum number of tests to run cryptolfunction under test cryptolinput value generators cryptolInital random generator  TNonecryptolThis type provides a lightweight syntactic framework for defining Cryptol primitives. The main purpose of this type is to provide an abstraction barrier that insulates the definitions of primitives from possible changes in the representation of values.cryptol-Evaluate a primitive into a value computation  U(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone8:>}cryptol'Evaluation environment with no bindingscryptol.Bind a variable in the evaluation environment.cryptolBind a variable to a value in the evaluation environment, without creating a thunk.cryptol%Lookup a variable in the environment.cryptolBind a type variable of kind *.cryptolLookup a type variable.  V(c) 2013-2020 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone #$%&+?vcryptol/Make a numeric literal value at the given type.cryptolMake a numeric constant.cryptol/Convert an unbounded integer to a value in Ringcryptol)Convert a word to a non-negative integer.cryptol4Join a sequence of sequences into a single sequence.cryptolSplit implementation.cryptolMerge two values given a binop. This is used for and, or and xor.cryptolIndexing operations.cryptolGeneric implementation of shifting. Uses the provided word-level operation to perform the shift, when possible. Otherwise falls back on a barrel shifter that uses the provided reindexing operation to implement the concrete shifting operations. The reindex operation is given the size of the sequence, the requested index value for the new output sequence, and the amount to shift. The return value is an index into the original sequence if in bounds, and Nothing otherwise.cryptolExpect a word value. Mask it to an 8-bits ASCII value and return the associated character, if it is concrete. Otherwise, return a ? charactercryptolProduce a random value with the given seed. If we do not support making values of the given type, return zero of that type. TODO: do better than returning zerocryptol0A helper for definitng floating point constants.cryptol6Make a Cryptol value for a binary arithmetic function.cryptolRounding mode used in FP operations that do not specify it explicitly.cryptolRounding mode used in FP operations that do not specify it explicitly.cryptolRounding mode used in FP operations that do not specify it explicitly.cryptolRounding mode used in FP operations that do not specify it explicitly.cryptolRounding mode used in FP operations that do not specify it explicitly.cryptolRounding mode used in FP operations that do not specify it explicitly.cryptolSequence size bounds cryptol Index value cryptol*operation for range reduction on integers cryptol*word shift operation for positive indices cryptol*word shift operation for negative indices cryptolreindexing operation for positive indices (sequence size, starting index, shift amount cryptolreindexing operation for negative indices (sequence size, starting index, shift amount W(c) 2020 Galois, Inc.BSD3cryptol@galois.comNone &'(+/X(c) 2013-2020 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone #$%&+cryptolGiven an expected type, returns an expression that evaluates to this value, if we can determine it.Y(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone  #$&? cryptolA prover result is either an error message, an empty result (eg for the offline prover), a counterexample or a lazy list of satisfying assignments.cryptolA :prove command can fail either because some input causes the predicate to violate a safety assertion, or because the predicate returns false for some input.cryptolThe type of query to runcryptol+Which prover to use (one of the strings in  proverConfigs)cryptolVerbosity flag passed to SBVcryptol#Model validation flag passed to SBVcryptolRecord timing information herecryptol?Extra declarations to bring into scope for symbolic simulationcryptol,Optionally output the SMTLIB query to a filecryptol&The typechecked expression to evaluatecryptolThe  of pcExprcryptol#Should we ignore safety predicates?cryptolFlatten structured shapes (like tuples and sequences), leaving only a sequence of variable shapes of base type.Z(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone &- cryptolExtend the given evaluation environment with all the declarations contained in the given module.cryptolEvaluate a Cryptol expression to a value. This evaluator is parameterized by the   class, which defines the behavior of bits and words, in addition to providing implementations for all the primitives.cryptolExtend the given evaluation environment with the result of evaluating the given collection of declaration groups.cryptolApply the the given "selector" form to the given value. Note that selectors are expected to apply only to values of the right type, e.g. tuple selectors expect only tuple values. The lifting of tuple an record selectors over functions and sequences has already been resolved earlier in the typechecker.cryptol+Module containing declarations to evaluate cryptolEnvironment to extend cryptolEvaluation environment cryptolExpression to evaluate cryptolDeclaration groups to evaluate cryptolEnvironment to extend (([(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone #$8:(cryptolExtra information we need to carry around to dynamically extend an environment outside the context of a single module. Particularly useful when dealing with interactive declarations as in let or it.cryptol1The name of this module. Should match what's in cryptol=The file path used to load this module (may not be canonical)cryptolAn identifier used to identify the source of the bytes for the module. For files we just use the cononical path, for in memory things we use their label.cryptolWhat's in scope in this modulecryptolThe module's interface.cryptolThe actual type-checked modulecryptol3Invariants: 1) All the dependencies of any module m must precede m= in the list. 2) Does not contain any parameterized modules.cryptolLoaded parameterized modules.cryptolThe location of a modulecryptolLabel, contentcryptolContains enough information to browse what's in scope, or type check new expressions.cryptol=Should contain at least names in NamingEnv, but may have morecryptol!What's in scope inside the modulecryptolShould we run the linter?cryptolDon't run core lintcryptol Run core lintcryptol-This is the current state of the interpreter.cryptol+Information about all loaded modules. See . Contains information such as the file where the module was loaded from, as well as the module's interface, used for type checking.cryptol+A source of new names for the type checker.cryptolThe evaluation environment. Contains the values for all loaded modules, both public and private.cryptol*Should we run the linter to ensure sanity.cryptolAre we assuming that local bindings are monomorphic. XXX: We should probably remove this flag, and set it to  .cryptolThe "current" module. Used to decide how to print names, for example.cryptolWhere we look for things.cryptolThis contains additional definitions that were made at the command line, and so they don't reside in any module.cryptolName source for the renamercryptol7Try to focus a loaded module in the module environment.cryptolGet a list of all the loaded modules. Each module in the resulting list depends only on other modules that precede it. Note that this includes parameterized modules.cryptolGet a list of all the loaded non-parameterized modules. These are the modules that can be used for evaluation, proving etc.cryptol%Are any parameterized modules loaded?cryptolGiven the state of the environment, compute information about what's in scope on the REPL. This includes what's in the focused module, plus any additional definitions from the REPL (e.g., let bound names, and it).cryptolThe name of the content---either the file path, or the provided label.cryptol$Has this module been loaded already.cryptol&Is this a loaded parameterized module.cryptol&Try to find a previously loaded modulecryptolAdd a freshly loaded module. If it was previously loaded, then the new version is ignored.cryptolRemove a previously loaded module. Note that this removes exactly the modules specified by the predicate. One should be carfule to preserve the invariant on .cryptolBuild   that correspond to all of the bindings in the dynamic environment.9XXX: if we add newtypes, etc. at the REPL, revisit this.cryptol'In-memory things are compared by label.>>\None +](c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone&5>^(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone&+5>ir(c) 2014-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Trustworthy s Safe-Inferred  _(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableSafe!(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Trustworthy > ( (  9  9 `(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportable Safe-Inferred#$8: -a(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone 8:?'Ocryptol=Unable to find the module given, tried looking in these pathscryptolUnable to open a filecryptol.Bad UTF-8 encoding in while decoding this filecryptol4Some other IO error occurred while reading this filecryptol=Generated this parse error when parsing the file for module mcryptol!Recursive module group discoveredcryptol"Problems during the renaming phasecryptolProblems during the NoPat phasecryptol#Problems during the NoInclude phasecryptolProblems during type checkingcryptol0Problems after type checking, eg. specializationcryptolModule loaded by 'import'$ statement has the wrong module namecryptolTwo modules loaded from different files have the same module namecryptolAttempt to import a parametrized module that was not instantiated.cryptolFailed to add the module parameters to all definitions in a module.cryptolThis is just a tag on the error, indicating the file containing it. It is convenient when we had to look for the module, and we'd like to communicate the location of pthe problematic module to the handler.cryptolRun the computation, and if it caused and error, tag the error with the given file.cryptolPush an "interactive" context onto the loading stack. A bit of a hack, as it uses a faked module namecryptol(Get the currently focused import source.cryptolRun a  action in a context with a prepended search path. Useful for temporarily looking in other places while resolving imports, for example.cryptol#Usefule for logging. For example: withLogger logPutStrLn Hellob(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone #$?0=cryptol7Rename a module in the context of its imported modules.cryptolRun the noPat pass.cryptol"Parse a module and expand includescryptolLoad a module by its path.cryptol/Load a module, unless it was previously loaded.cryptol>Load dependencies, typecheck, and add to the eval environment.cryptol0Rewrite an import declaration to be of the form: &import foo as foo [ [hiding] (a,b,c) ]cryptolDiscover a module.cryptol'Discover a file. This is distinct from  in that we assume we've already been given a particular file name.cryptolAdd the prelude to the import list if it's not already mentioned.cryptol7Load the dependencies of a module into the environment.cryptolTypecheck a single expression, yielding a renamed parsed expression, typechecked core expression, and a type schema.cryptol"Typecheck a group of declarations.INVARIANT: This assumes that NoPat has already been run on the declarations.cryptolGenerate the primitive map. If the prelude is currently being loaded, this should be generated directly from the naming environment given to the renamer instead.cryptolLoad a module, be it a normal module or a functor instantiation.cryptolTypecheck a single module. If the module is an instantiation of a functor, then this just type-checks the instantiating parameters. See  Note: we assume that includes have already been processedcryptol#Generate input for the typechecker.cryptol quiet mode cryptol9quiet mode: true suppresses the "loading module" message cryptol how to check cryptolwhy are we loading this cryptolmodule to check ##c(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone?4 cryptolFind the file associated with a module name in the module search path.cryptol,Load the module contained in the given file.cryptolLoad the given parsed module.cryptolCheck the type of an expression. Give back the renamed expression, the core expression, and its type schema.cryptolEvaluate an expression.cryptol!Typecheck top-level declarations.cryptol?Evaluate declarations and add them to the extended environment.cryptolRename a *use* of a value name. The distinction between uses and binding is used to keep track of dependencies.cryptolRename a *use* of a type name. The distinction between uses and binding is used to keep track of dependencies.   d(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone;CcryptolThe specializer monad.cryptolA  should have an entry in the  iff it is specializable. Each  starts out with an empty .cryptolAdd a where clause to the given expression containing type-specialized versions of all functions called (transitively) by the body of the expression.cryptolAdd the declarations to the SpecCache, run the given monadic action, and then pull the specialized declarations back out of the SpecCache state. Return the result along with the declarations and a table of names of specialized bindings.cryptolCompute the specialization of  e dgs. A decl within dgs is replicated once for each monomorphic type instance at which it is used; decls not mentioned in e- (even monomorphic ones) are simply dropped.cryptolTransform the given declaration groups into a set of monomorphic declarations. All of the original declarations with monomorphic types are kept; additionally the result set includes instantiated versions of polymorphic decls that are referenced by the monomorphic bindings. We also return a map relating generated names to the names from the original declarations.cryptol)Freshen a name by giving it a new unique.cryptolReduce  length ts! outermost type abstractions and n proof abstractions.e(c) 2013-2020 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone#$&'(+?<cryptol hash consing cryptol warn on uninterpreted functions cryptol hash consing cryptol warn on uninterpreted functions  f(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone #$&??cryptol-The names of all the solvers supported by SBVcryptol.Execute a symbolic ':prove' or ':sat' command.This command returns a pair: the first element is the name of the solver that completes the given query (if any) along with the result of executing the query.cryptolExecute a symbolic ':prove' or ':sat' command when the prover is set to offline. This only prepares the SMT input file for the solver and does not actually invoke the solver.This method returns either an error message or the text of the SMT input file corresponding to the given prover command.g(c) 2013-2016 Galois, Inc.BSD3cryptol@galois.com provisionalportableNone#$&3>H'cryptolREPL exceptions.cryptol#REPL_ context with InputT handling.cryptol3This indicates what the user would like to work on.cryptolWorking on this module.cryptolWorking on this file.cryptol+Run a REPL action with a fresh environment.cryptolRaise an exception.cryptol1Construct the prompt for the current environment.cryptol7Set the name of the currently focused file, loaded via :r.cryptolSet the path for the ':e' command. Note that this does not change the focused module (i.e., what ":r" reloads)cryptolRun a computation in batch mode, restoring the previous isBatch flag afterwardscryptolIs evaluation enabled. If the currently focused module is parameterized, then we cannot evalute.cryptolUpdate the titlecryptol>>>>>>>?????????@@@@@AABBBBBBBBBBBBBBBBBBCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDEEEEEEEEEEEEEEEEEEEEFGGGGGG GGHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHHIIIIIIIIIIIIIIIJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJJKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKKLLLLLLLLLLLLLLLLLLLLLLLLLLLLLMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMMqNNNNNNNNNNNNNNNNNNNNNN NNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNNOOOOOOOOOOOOOOOOOOOOPPPPPPPPPPPPPPPPPPPPPPPQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQQRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRSSSSSSSSSSSSTTTTTTTTTTTUUUUUUUUUUUUUUVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVVWWXXXYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYZZZZZZZZZ[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[\\\\]]]]]]]]]]]]]]]]]]]]]]]]]]]]]^s_____!!!!!!!!!!!!!!!!!``````````````aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaabbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbcccccccccccccdddddddddddddddddddddddddeeeeeeeeeeeeeeeffffffffffggggggggggggggggg ggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggggghhhhhhhhhhhhhhhhhhhhhhhhiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiiitjjjjjjjtkkkkkkkkkkkkkkkkkkkkkkkkkkkkkkkkkkkkllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllllltttttqwxqqqwxwxwxwxqqqqqqqqqqqZrrrsssssss!!h%cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6bCryptol.Utils.PanicCryptol.PrimeEC Cryptol.AESCryptol.Backend.Arch Cryptol.ModuleSystem.Fingerprint Cryptol.SHACryptol.Utils.FixityCryptol.Utils.IdentCryptol.Utils.LoggerCryptol.Utils.MiscCryptol.Utils.PPCryptol.Utils.DebugCryptol.TypeCheck.PPCryptol.Parser.TokenCryptol.Parser.SelectorCryptol.Parser.PositionCryptol.TypeCheck.Solver.InfNat Cryptol.F2Cryptol.REPL.TrieCryptol.Parser.UnlitCryptol.Parser.NameCryptol.Parser.LexerCryptol.Parser.LayoutCryptol.ModuleSystem.NameCryptol.TypeCheck.TConCryptol.Utils.PatternsCryptol.Utils.RecordMapCryptol.TypeCheck.TypeCryptol.TypeCheck.TypePatCryptol.TypeCheck.SimpTypeCryptol.Parser.ASTCryptol.Parser.UtilsCryptol.ParserCryptol.Parser.NamesCryptol.Parser.NoPat"Cryptol.ModuleSystem.Renamer.ErrorCryptol.ModuleSystem.InterfaceCryptol.ModuleSystem.ExportsCryptol.TypeCheck.ASTCryptol.TypeCheck.TypeMapCryptol.TypeCheck.Solver.Utils)Cryptol.TypeCheck.Solver.Numeric.IntervalCryptol.TypeCheck.Solver.TypesCryptol.TypeCheck.Solver.Class$Cryptol.TypeCheck.Solver.Numeric.Fin Cryptol.TypeCheck.Solver.NumericCryptol.TypeCheck.SimpleSolverCryptol.TypeCheck.SubstCryptol.TypeCheck.UnifyCryptol.TypeCheck.TypeOf Cryptol.TypeCheck.Solver.ImproveCryptol.TypeCheck.ParseableCryptol.TypeCheck.InterfaceCryptol.TypeCheck.InferTypesCryptol.TypeCheck.Solver.SMTCryptol.TypeCheck.ErrorCryptol.TypeCheck.Monad!Cryptol.TypeCheck.Solver.SelectorCryptol.TypeCheck.SanityCryptol.TypeCheck.DefaultCryptol.TypeCheck.SolveCryptol.TypeCheck.KindCryptol.TypeCheck.InstantiateCryptol.TypeCheck.InferCryptol.Transform.MonoValuesCryptol.Transform.AddModParamsCryptol.ModuleSystem.NamingEnv"Cryptol.ModuleSystem.Renamer.Monad&Cryptol.ModuleSystem.InstantiateModule%Cryptol.TypeCheck.CheckModuleInstanceCryptol.TypeCheckCryptol.Backend.MonadCryptol.Backend.FloatHelpersCryptol.BackendCryptol.ModuleSystem.RenamerCryptol.IR.FreeVarsCryptol.Eval.TypeCryptol.Backend.What4Cryptol.Backend.ConcreteCryptol.Backend.SeqMapCryptol.Backend.WordValueCryptol.Eval.ValueCryptol.Testing.RandomCryptol.Eval.PrimsCryptol.Eval.EnvCryptol.Eval.GenericCryptol.Eval.What4Cryptol.Eval.ConcreteCryptol.Symbolic Cryptol.EvalCryptol.ModuleSystem.EnvCryptol.REPL.BrowseCryptol.Backend.SBVCryptol.Eval.SBVCryptol.VersionCryptol.Parser.NoIncludeCryptol.ModuleSystem.MonadCryptol.ModuleSystem.BaseCryptol.ModuleSystemCryptol.Transform.SpecializeCryptol.Symbolic.What4Cryptol.Symbolic.SBVCryptol.REPL.MonadCryptol.Eval.ReferenceCryptol.REPL.CommandCryptol.PreludeCryptol.Parser.LexerUtilsCryptol.Parser.ParserUtilsKindhsFloatcryGHC.Num.CompatGitRev Paths_cryptolbaseGHC.Stack.Types HasCallStackinteger-wired-inGHC.Integer.TypebigNatToInteger$panic-0.4.0.1-2mQXWfMBRt44jkFcbaKM4WPanicKeyState invMixColumnskeyExpansionWordsaesRound aesFinalRound aesInvRoundaesInvFinalRoundmaxBigIntWidth Fingerprint fingerprintfingerprintFile$fNFDataFingerprint$fEqFingerprint$fShowFingerprint SHA512Block SHA256Block SHA512StateSHA512S SHA256StateSHA256SinitialSHA224StateinitialSHA256StateinitialSHA384StateinitialSHA512StatepadSHA1 padSHA1Chunks padSHA512padSHA512Chunkscalc_ktoBigEndianSBSfromBigEndianSBSprocessSHA256BlockprocessSHA512Block FixityCmpFCErrorFCLeftFCRightFixityfAssocfLevelAssoc LeftAssoc RightAssocNonAssoc compareFixity defaultFixity$fShowFixityCmp $fEqFixityCmp $fEqFixity$fGenericFixity$fNFDataFixity $fShowFixity $fShowAssoc $fEqAssoc$fGenericAssoc $fNFDataAssoc PrimIdentIdentOrigName ogNamespaceogModuleogNameModNameModPath TopModuleNested NamespaceNSValueNSTypeNSModule allNamespaces apPathRoot topModuleFor modPathCommon modPathSplit modNameToText textToModName modNameChunksisParamInstModNameparamInstModNamenotParamInstModName packModName preludeNamepreludeReferenceName floatName arrayName suiteBName primeECNameinteractiveName noModuleName exprModName packIdent packInfix unpackIdentmkIdentmkInfix isInfixIdent nullIdent identText modParamIdentprelPrim floatPrim suiteBPrim primeECPrim arrayPrim$fNFDataModName $fNFDataIdent$fIsStringIdent $fOrdIdent $fEqIdent$fNFDataPrimIdent $fEqPrimIdent$fOrdPrimIdent$fShowPrimIdent$fGenericPrimIdent $fEqOrigName $fOrdOrigName$fShowOrigName$fGenericOrigName$fNFDataOrigName $fEqModPath $fOrdModPath $fShowModPath$fGenericModPath$fNFDataModPath $fShowIdent$fGenericIdent $fEqModName $fOrdModName $fShowModName$fGenericModName$fGenericNamespace$fShowNamespace$fNFDataNamespace $fEqNamespace$fOrdNamespace$fEnumNamespace$fBoundedNamespaceLogger logPutStr logPutStrLnlogPrint quietLogger handleLogger stdoutLogger stderrLogger funLogger$fNFDataLoggeranyJustanyJust2InfixieOpieLeftieRightieFixityPPName ppNameFixity ppPrefixName ppInfixNamePPppPrecDoc NameFormat UnQualified Qualified NotInScopeNameDisp EmptyNameDisp FieldOrder DisplayOrderCanonicalOrder PPFloatExp ForceExponent AutoExponent PPFloatFormat FloatFixed FloatFrac FloatFreePPOptsuseAsciiuseBase useInfLength useFPBase useFPFormat useFieldOrder asciiMode defaultPPOptsneverQualifyMod neverQualifyextend getNameFormat withNameDisp fixNameDisprunDoc renderOneLinepppretty optParensppInfixordinal ordSuffixliftPPliftPP1liftPP2liftSep<.><+>$$sepfsephsephcatvcatvsepgrouphangnestindentalignparensbracesbracketsquotescommaSep commaSepFillppListppTupleppRecord backtickstextcharintegerintcommacolon$fMonoidNameDisp$fSemigroupNameDisp$fShowNameDisp $fIsStringDoc $fShowDoc $fMonoidDoc$fSemigroupDoc $fPPNamespace $fPPOrigName $fPPModPath $fPPFixity $fPPAssoc $fPPModName $fPPIdent$fPPText$fPPNameModName $fGenericDoc $fNFDataDoc$fGenericNameDisp$fNFDataNameDisp$fShowNameFormat $fShowPPOpts$fBoundedFieldOrder$fEnumFieldOrder$fEqFieldOrder$fOrdFieldOrder$fReadFieldOrder$fShowFieldOrder$fShowPPFloatFormat$fShowPPFloatExptraceppTrace WithNamesNameMap emptyNameMapppWithNamesPrec ppWithNamesdumpnameListTokenTNumFracChrLitStrLitSelectorKWOpSymVirtWhiteErrEOF SelectorTypeRecordSelectorTokTupleSelectorTokTokenErrUnterminatedCommentUnterminatedStringUnterminatedChar InvalidString InvalidChar LexicalErrorMalformedLiteralMalformedSelectorInvalidIndentationTokenSymBarArrLArrRFatArrRLambdaEqDefCommaSemiDotDotDot DotDotDotDotDotLtDotDotGtColonBackTickParenLParenRBracketLBracketRCurlyLCurlyRTriLTriRLtGt UnderscoreTokenOpPlusMinusMulDivExpModEqualLEQGEQ ComplementHashAtOtherTokenKWKW_else KW_externKW_finKW_if KW_private KW_includeKW_infKW_lg2KW_lengthFromThenKW_lengthFromThenToKW_maxKW_min KW_module KW_submodule KW_newtype KW_pragma KW_propertyKW_thenKW_typeKW_whereKW_letKW_x KW_importKW_as KW_hiding KW_infixl KW_infixrKW_infix KW_primitive KW_parameter KW_constraintKW_PropKW_byKW_downTokenW BlockComment LineCommentSpaceDocStrTokenVVCurlyLVCurlyRVSemiToken tokenType tokenText $fPPToken $fShowToken$fGenericToken $fNFDataToken $fEqTokenT $fShowTokenT$fGenericTokenT$fNFDataTokenT $fEqTokenErr$fShowTokenErr$fGenericTokenErr$fNFDataTokenErr$fEqSelectorType$fShowSelectorType$fGenericSelectorType$fNFDataSelectorType $fEqTokenSym$fShowTokenSym$fGenericTokenSym$fNFDataTokenSym $fEqTokenOp $fShowTokenOp$fGenericTokenOp$fNFDataTokenOp $fEqTokenKW $fShowTokenKW$fGenericTokenKW$fNFDataTokenKW $fEqTokenW $fShowTokenW$fGenericTokenW$fNFDataTokenW $fEqTokenV $fShowTokenV$fGenericTokenV$fNFDataTokenVTupleSel RecordSelListSel ppSelectorselName ppNestedSels $fPPSelector $fEqSelector$fShowSelector $fOrdSelector$fGenericSelector$fNFDataSelectorAddLocaddLocdropLocHasLocgetLocRangefromtosourcePositionlinecolLocatedsrcRangething emptyRangestartmovemovesrComb rCombMayberCombsatcombLoc $fPPPosition $fPPRange$fPPNameLocated $fPPLocated $fHasLoc[] $fHasLoc(,)$fHasLocLocated $fHasLocRange$fAddLocLocated $fEqLocated $fOrdLocated $fShowLocated$fGenericLocated$fNFDataLocated$fFunctorLocated$fFoldableLocated$fTraversableLocated $fEqRange $fOrdRange $fShowRange$fGenericRange $fNFDataRange $fEqPosition $fOrdPosition$fShowPosition$fGenericPosition$fNFDataPosition CryptolPanicCryptolpanic$fPanicComponentCryptolNat'NatInffromNatnAddnMulnExpnMinnMaxnSubnDivnModnCeilDivnCeilModnLg2nWidthnLenFromThenTogenLog widthInteger rootExactgenRoot $fShowNat'$fEqNat' $fOrdNat' $fGenericNat' $fNFDataNat'pmultpdivpmodTrieNode emptyTrie insertTrie lookupTrielookupTrieExactleaves $fShowTriePreProcNoneMarkdownLaTeX knownExts guessPreProcunLitPassNoPat MonoValuesPNameUnQualQualNewNamemkUnqualmkQual getModNamegetIdentisGeneratedName $fNFDataPass $fPPNamePName $fPPPName $fNFDataPName $fEqPName $fOrdPName $fShowPName$fGenericPName$fEqPass $fOrdPass $fShowPass $fGenericPassLayoutNoLayoutConfig cfgSourcecfgStart cfgLayout cfgPreProccfgAutoIncludecfgModuleScope defaultConfigBlockVirtualExplicitlayout startsLayout endsLayoutstartsParenBlockvirterrTok $fShowBlocklexer primLexerdbgLexPrimMap primDecls primTypesSupplySupplyTFreshM liftSupply NameSource SystemNameUserNameNameNameInfoDeclared ParametercmpNameDisplay ppLocName nameUnique nameIdent nameNamespacenameInfonameLoc nameFixityasPrimtoParamInstName asParamName asOrigName runSupplyT nextUniqueM emptySupply nextUnique mkDeclared mkParameterparamModRecParamlookupPrimDecllookupPrimType $fPPNameName$fPPName $fOrdName$fEqName$fRunMSupplyTa->$fBaseMSupplyTn$fMonadTSupplyT$fMonadSupplyT$fApplicativeSupplyT$fFunctorSupplyT$fFreshMSupplyT$fFreshMStateT$fFreshMReaderT$fFreshMWriterT$fFreshMExceptionT$fSemigroupPrimMap $fShowPrimMap$fGenericPrimMap$fNFDataPrimMap $fShowSupply$fGenericSupply$fNFDataSupply $fGenericName $fNFDataName $fShowName $fEqNameInfo$fShowNameInfo$fGenericNameInfo$fNFDataNameInfo$fGenericNameSource$fNFDataNameSource$fShowNameSource$fEqNameSourceTFunTCAddTCSubTCMulTCDivTCModTCExpTCWidthTCMinTCMax TCCeilDiv TCCeilModTCLenFromThenToUserTCTCTCNumTCInfTCBit TCIntegerTCFloatTCIntMod TCRationalTCArrayTCSeqTCFunTCTuple TCAbstractPCPEqualPNeqPGeqPFinPPrimePHasPZeroPLogicPRing PIntegralPFieldPRoundPEqPCmp PSignedCmpPLiteralPLiteralLessThan PFLiteral PValidFloatPAndPTrueTConTFTErrorHasKindkindOfKTypeKNumKProp:-> infixPrimTy builtInType$fPPKind$fPPPC $fHasKindPC $fPPUserTC $fOrdUserTC $fEqUserTC$fHasKindUserTC$fPPTC $fHasKindTC$fPPTFun $fHasKindTFun$fPPTCon $fHasKindTCon $fShowTCon$fEqTCon $fOrdTCon $fGenericTCon $fNFDataTCon $fShowTFun$fEqTFun $fOrdTFun $fBoundedTFun $fEnumTFun $fGenericTFun $fNFDataTFun$fShowTC$fEqTC$fOrdTC $fGenericTC $fNFDataTC $fShowUserTC$fGenericUserTC$fNFDataUserTC$fShowPC$fEqPC$fOrdPC $fGenericPC $fNFDataPC$fEqKind $fOrdKind $fShowKind $fGenericKind $fNFDataKindMatchesmatchesPatMatch|||&&&~>~~><~__succeed checkThatlit matchDefaultmatch matchMaybelist><$fMonadPlusMatch$fAlternativeMatch$fMonadFailMatch $fMonadMatch$fApplicativeMatch$fFunctorMatch$fMatchesa(,,,)(,,)$fMatchesa(,,)(,)$fMatchesa(,)r1 RecordMapfieldSet displayOrderrecordElementscanonicalFields displayFieldsrecordFromFieldsrecordFromFieldsErrrecordFromFieldsWithDisplay lookupField adjustFieldtraverseRecordMapmapWithFieldNamerecordMapAccum zipRecordsM zipRecords$fTraversableRecordMap$fFoldableRecordMap$fFunctorRecordMap$fNFDataRecordMap$fShowRecordMap$fOrdRecordMap $fEqRecordMapFVSfvsSType AbstractTypeatNameatKindatCtrs atFixitiyatDocNewtypentNamentParams ntConstraintsntFieldsntDocTySyntsNametsParams tsConstraintstsDeftsDocPropTypeWithSource WithSourcetwsType twsSourcetwsRangeArgDescr argDescrFunargDescrNumber TypeSourceTVFromModParamTVFromSignature TypeWildCardTypeOfRecordFieldTypeOfTupleFieldTypeOfSeqElementLenOfSeqTypeParamInstNamedTypeParamInstPos DefinitionOf LenOfCompGen TypeOfArg TypeOfResFunAppTypeOfIfCondExprTypeFromUserAnnotationGeneratorOfListCompTypeErrorPlaceHolderTVarInfo tvarSourcetvarDescTVarTVFreeTVBoundTypeTUserTRecTNewtypeTPFlavor TPModParam TPUnifyVar TPSchemaParam TPTySynParamTPPropSynParamTPNewtypeParam TPPrimParamTParamtpUniquetpKindtpFlavtpInfoSchemaForallsVarssPropssType ModVParammvpNamemvpTypemvpDoc mvpFixity ModTParammtpNamemtpKind mtpNumbermtpDocmtpParamtMonoisMono schemaParam tySynParam propSynParam newtypeParam modTyParamtpfNametpNametvInfotvUnique noArgDescr tvSourceName quickApply kindResulttpVar superclassSetnewtypeConTypeabstractTypeTCisFreeTV isBoundTVtIsError tHasErrorstIsNat'tIsNumtIsInftIsVartIsFuntIsSeqtIsBit tIsInteger tIsIntMod tIsRationaltIsFloattIsTupletIsRec tIsBinFun tSplitFunpIsFinpIsPrimepIsGeqpIsEqualpIsZeropIsLogicpIsRingpIsField pIsIntegralpIsRoundpIsEqpIsCmp pIsSignedCmp pIsLiteralpIsLiteralLessThan pIsFLiteralpIsTruepIsWidth pIsValidFloattNumtZerotOnetTwotInftNat' tAbstracttNewtypetBittInteger tRationaltFloattIntModtArraytWordtSeqtChartStringtRectTupletFuntNoUsertErrortf1tf2tf3tSubtMultDivtModtExptMintCeilDivtCeilModtLenFromThenTo=#==/=pZeropLogicpRing pIntegralpFieldpRoundpEqpCmp pSignedCmppLiteralpLiteralLessThan>==pHaspTruepAnd pSplitAndpFin pValidFloatpPrimenoFreeVariables freeParams addTNamesppNewtypeShort pickTVarName $fPPArgDescr$fPPTypeSource $fPPTVarInfo $fPPWithNames $fPPTParam $fOrdTParam $fEqTParam$fHasKindTParam$fPPTVar$fPPWithNames0 $fOrdTVar$fEqTVar $fHasKindTVar$fPPType$fPPWithNames1$fPPWithNames2 $fPPNewtype $fOrdType$fEqType$fHasKindNewtype $fHasKindType $fOrdNewtype $fEqNewtype$fPPWithNames3 $fPPTySyn$fHasKindTySyn$fPPWithNames4 $fPPSchema $fFVSSchema$fFVS(,)$fFVS[] $fFVSMaybe $fFVSType$fShowAbstractType$fGenericAbstractType$fNFDataAbstractType$fShowModVParam$fGenericModVParam$fNFDataModVParam $fEqSchema $fShowSchema$fGenericSchema$fNFDataSchema $fShowTySyn$fGenericTySyn $fNFDataTySyn $fShowNewtype$fGenericNewtype$fNFDataNewtype $fShowType $fGenericType $fNFDataType $fShowTVar $fGenericTVar $fNFDataTVar$fGenericTParam$fNFDataTParam $fShowTParam$fShowTVarInfo$fGenericTVarInfo$fNFDataTVarInfo$fShowTypeSource$fGenericTypeSource$fNFDataTypeSource$fShowArgDescr$fGenericArgDescr$fNFDataArgDescr$fGenericTPFlavor$fNFDataTPFlavor$fShowTPFlavor$fShowModTParam$fGenericModTParam$fNFDataModTParamaInfaNataNat'anAdd|-|aMul|^||/||%|aMinaMaxaWidthaCeilDivaCeilModaLenFromThenToaTVar aFreeTVaraBitaSeqaWordaCharaTupleaRec|->|aFin|=||/=||>=|aAndaTrueaLiteralaLiteralLessThanaLogicanError tRebuild'tRebuildtContAddtMaxtWidthtotalop1op2op3tOpNoPosnoPosCTypeTSeqTBitTNumTCharTTyAppTRecordTTupleTWildTLocatedTParensTInfixtpRangeKFunNamednamevaluePatternPVarPWildPTuplePRecordPListPTypedPSplitPLocatedMatchLetTypeInst NamedInstPosInstUpdHowUpdSetUpdFunUpdFieldFunDesc funDescrNamefunDescrArgOffsetExprEVarELitENeg EComplement EGenerateETupleERecordESelEUpdEListEFromTo EFromToBy EFromToDownByEFromToLessThanEInfFromECompEAppEAppTEIfEWhereETypedETypeValEFunELocatedESplitEParensEInfixLiteralECNumECCharECFracECStringFracInfoBinFracOctFracDecFracHexFracNumInfoBinLitOctLitDecLitHexLitPolyLitTopLeveltlExporttlDoctlValue ExportTypePublicPrivate ReplInput ExprInputLetInput EmptyInputPrimType primTName primTKindprimTCts primTFixitynNamenParamsnBodyPragma PragmaNotePragmaPropertyBindDefDPrimDExprLBindDefBindbNamebParamsbDef bSignaturebInfixbFixitybPragmasbMonobDocbExportPropSyn ImportSpecHidingOnlyImportImportGiModuleiAsiSpec ParameterFunpfNamepfSchemapfDocpfFixity ParameterTypeptNameptKindptDocptFixityptNumberDecl DSignatureDFixityDPragmaDBindDRecDPatBindDTypeDPropDLocatedImpNameImpTop ImpNestedTopDecl DPrimType TDNewtypeIncludeDParameterTypeDParameterConstraint DParameterFunDModuleDImport NestedModuleModuleModuleGmName mInstancemDeclsProgramLStringLIdentLPNamemImportsmSubmoduleImportsmodRangepsNametsFixitypsFixity emptyFunDesccppKind $fPPImpName$fPPImportSpec $fPPImportG $fPPPragma $fPPTopLevel$fHasLocTopLevel $fPPLiteral $fPPUpdHow $fHasLocNamed$fPPParameterType$fHasLocParameterType$fAddLocTParam$fHasLocTParam $fAddLocType $fHasLocType $fPPPattern$fHasLocPattern$fAddLocPattern $fPPTypeInst$fHasLocNewtype$fPPProp$fAddLocSchema$fHasLocSchema$fPPParameterFun$fHasLocParameterFun $fPPPrimType$fHasLocPrimType $fPPPropSyn $fPPMatch $fPPUpdField$fPPExpr $fPPBindDef$fPPBind$fPPDecl $fAddLocDecl $fHasLocDecl $fHasLocMatch $fHasLocBind $fHasLocExpr $fAddLocExpr $fPPTopDecl$fPPNestedModule $fPPModuleG$fHasLocNestedModule$fHasLocModuleG$fHasLocTopDecl $fPPProgram $fNoPosProp $fNoPosType $fNoPosTParam $fNoPosSchema$fNoPosPattern $fNoPosMatch$fNoPosTypeInst$fNoPosUpdField $fNoPosExpr$fNoPosPropSyn $fNoPosTySyn $fNoPosPragma $fNoPosBind$fNoPosNewtype $fNoPosDecl$fNoPosTopLevel$fNoPosParameterFun$fNoPosParameterType$fNoPosPrimType$fNoPosTopDecl$fNoPosNestedModule$fNoPosModuleG$fNoPosProgram $fNoPos(,) $fNoPosMaybe $fNoPos[] $fNoPosRange $fNoPosNamed$fNoPosLocated $fShowProgram $fShowTopDecl$fGenericTopDecl$fNFDataTopDecl$fShowNestedModule$fGenericNestedModule$fNFDataNestedModule $fShowModuleG$fGenericModuleG$fNFDataModuleG $fEqReplInput$fShowReplInput$fEqDecl $fShowDecl $fGenericDecl $fNFDataDecl $fFunctorDecl$fEqExpr $fShowExpr $fGenericExpr $fNFDataExpr $fFunctorExpr $fEqMatch $fShowMatch$fGenericMatch $fNFDataMatch$fEqBind $fGenericBind $fNFDataBind $fFunctorBind $fShowBind $fEqBindDef $fShowBindDef$fGenericBindDef$fNFDataBindDef$fFunctorBindDef $fEqUpdField$fShowUpdField$fGenericUpdField$fNFDataUpdField$fFunctorUpdField $fEqPropSyn $fShowPropSyn$fGenericPropSyn$fNFDataPropSyn$fFunctorPropSyn$fShowPrimType$fGenericPrimType$fNFDataPrimType$fEqParameterFun$fShowParameterFun$fGenericParameterFun$fNFDataParameterFun$fFunctorSchema$fEqProp $fShowProp $fGenericProp $fNFDataProp $fFunctorProp $fEqTySyn$fFunctorTySyn $fEqTypeInst$fShowTypeInst$fGenericTypeInst$fNFDataTypeInst$fFunctorTypeInst $fEqPattern $fShowPattern$fGenericPattern$fNFDataPattern$fFunctorPattern $fFunctorType$fFunctorTParam$fEqParameterType$fShowParameterType$fGenericParameterType$fNFDataParameterType $fEqNamed $fShowNamed$fFoldableNamed$fTraversableNamed$fGenericNamed $fNFDataNamed$fFunctorNamed $fEqUpdHow $fShowUpdHow$fGenericUpdHow$fNFDataUpdHow $fEqFunDesc $fShowFunDesc$fGenericFunDesc$fNFDataFunDesc$fFunctorFunDesc $fEqLiteral $fShowLiteral$fGenericLiteral$fNFDataLiteral $fEqFracInfo$fShowFracInfo$fGenericFracInfo$fNFDataFracInfo $fEqNumInfo $fShowNumInfo$fGenericNumInfo$fNFDataNumInfo$fShowTopLevel$fGenericTopLevel$fNFDataTopLevel$fFunctorTopLevel$fFoldableTopLevel$fTraversableTopLevel$fEqExportType$fShowExportType$fOrdExportType$fGenericExportType$fNFDataExportType $fEqPragma $fShowPragma$fGenericPragma$fNFDataPragma $fEqImportG $fShowImportG$fGenericImportG$fNFDataImportG$fEqImportSpec$fShowImportSpec$fGenericImportSpec$fNFDataImportSpec $fShowImpName$fGenericImpName$fNFDataImpName widthIdenttranslateExprToNumT ParseError HappyError HappyErrorMsgHappyUnexpectedHappyOutOfTokensppErrortnamesNTnamesDnamesBnamesP boundNames boundNamesSettnamesDtnamesCtnamesTErrorMultipleSignaturesSignatureNoBind PragmaNoBindMultipleFixities FixityNoBind MultipleDocsRemovePatternsremovePatterns $fPPError $fMonadNoPatM$fApplicativeNoPatM$fFunctorNoPatM$fRemovePatternsNestedModule$fRemovePatterns[]$fRemovePatternsModuleG$fRemovePatternsExpr$fRemovePatternsProgram $fShowError$fGenericError $fNFDataErrorRenamerWarningSymbolShadowed UnusedNameDepName NamedThing ConstratintAt RenamerError MultipleSyms UnboundNameOverlappingSymsWrongNamespace FixityErrorInvalidConstraintMalformedBuiltinBoundReservedTypeOverlappingRecordUpdateInvalidDependency depNameLoc $fPPDepName$fPPRenamerError$fPPRenamerWarning$fOrdRenamerWarning$fEqRenamerWarning$fShowRenamerWarning$fGenericRenamerWarning$fNFDataRenamerWarning$fShowRenamerError$fGenericRenamerError$fNFDataRenamerError $fEqDepName $fOrdDepName $fShowDepName$fGenericDepName$fNFDataDepName IfaceDecl ifDeclName ifDeclSig ifDeclPragmas ifDeclInfix ifDeclFixity ifDeclDoc IfaceNewtype IfaceTySyn IfaceDeclsifTySyns ifNewtypesifAbstractTypesifDecls ifModules IfaceParams ifParamTypesifParamConstraints ifParamFunsIfaceIfaceG ifModNameifPublic ifPrivateifParamsifaceIsFunctorflatPublicIfaceflatPublicDecls emptyIface noIfaceParamsisEmptyIfaceParamsfilterIfaceDeclsifaceDeclsNames ifTySynName ifacePrimMap$fMonoidIfaceDecls$fSemigroupIfaceDecls$fShowIfaceDecls$fGenericIfaceDecls$fNFDataIfaceDecls $fShowIfaceG$fGenericIfaceG$fNFDataIfaceG$fShowIfaceDecl$fGenericIfaceDecl$fNFDataIfaceDecl$fShowIfaceParams$fGenericIfaceParams$fNFDataIfaceParams ExportSpec modExports exportedNamesnames exportNameexported exportBind exportType isExportedisExportedBindisExportedType$fMonoidExportSpec$fSemigroupExportSpec$fNFDataExportSpec$fShowExportSpec$fGenericExportSpecDeclDefdName dSignature dDefinitiondPragmasdInfixdFixitydDoc DeclGroup Recursive NonRecursiveFromLetERecESetETAbsETAppEAbs EProofAbs EProofAppmExports mSubModules mParamTypesmParamConstraints mParamFunsmTySyns mNewtypes mPrimTypes mFunctors emptyModuleisParametrizedModule groupDeclsePrimeErroreStringeCharppLam splitWhilesplitAbs splitTAbs splitProofAbs splitTApp splitProofApp splitExprInst $fPPDeclGroup $fShowDeclDef$fGenericDeclDef$fNFDataDeclDef$fShowDeclGroup$fGenericDeclGroup$fNFDataDeclGroupTypeMapTMtvartcontrectnewtypeTypesMapListLnilconsTrieMapemptyTMnullTMlookupTMalterTMunionTMtoListTMmapMaybeWithKeyTM membersTMinsertTM insertWithTMmapTM mapWithKeyTM mapMaybeTM $fTrieMapMapa$fTrieMapList[] $fShowTypeMap$fTrieMapTypeMapType$fFunctorTypeMap$fFoldableTypeMap$fTraversableTypeMap $fFunctorList$fFoldableList$fTraversableListsplitVarSummandssplitVarSummandsplitConstSummandsplitConstFactorIntervaliLoweriUpperIntervalUpdateNoChangeInvalidInterval NewIntervals typeInterval tvarIntervalupdateIntervalcomputePropIntervals propInterval ppIntervals ppIntervaliIsExactiIsFin iIsPosFiniOverlap iIntersectiAnyiAnyFiniConstiAddiMuliExpiMiniMaxiSubiDiviModiCeilDiviCeilModiWidthiLenFromThenTo$fShowIntervalUpdate $fEqInterval$fShowIntervalSolvedSolvedIfUnsolved UnsolvableCtxt SolverCtxt intervalssaturatedAsmpselseTry solveOpts matchThenguarded $fMonoidCtxt$fSemigroupCtxt $fPPSolved $fShowSolvedsolveValidFloat solveZeroInstsolveLogicInst solveRingInstsolveIntegralInstsolveFieldInstsolveRoundInst solveEqInst solveCmpInstsolveSignedCmpInstsolveFLiteralInstsolveLiteralInstsolveLiteralLessThanInstcryIsFin cryIsFinType cryIsEqual cryIsNotEqualcryIsGeq primeTable cryIsPrimesimplify simplifyStepTVarsapSubst SubstErrorSubstRecursive SubstEscapedSubstKindMismatchSubst emptySubst singleSubstuncheckedSingleSubstsingleTParamSubst@@defaultingSubst listSubstlistParamSubst isEmptySubst substBinds substToList!$.$fmap' apSubstMaybeapplySubstToVarapSubstTypeMapKeys $fPPSubst$fApplicativeDone$fTVarsModuleG$fTVarsDeclDef $fTVarsDecl$fTVarsDeclGroup $fTVarsMatch $fTVarsExpr $fTVarsSchema $fTVarsTySyn $fTVarsMap$fTVarsTypeMap $fTVarsList $fTVarsType $fTVars(,) $fTVars[] $fTVarsMaybe $fFunctorDone$fFoldableDone$fTraversableDone $fShowSubst PathElementTConArg TNewtypeArgTRecArgPathUnificationErrorUniTypeMismatchUniKindMismatchUniTypeLenMismatch UniRecursiveUniNonPolyDepends UniNonPolyResultMGU runResultuniErrorrootPath isRootPathextPathemptyMGUdoMGUmgumguManybindVarppPathEl$fPPPath $fShowPath $fGenericPath $fNFDataPath$fShowPathElement$fGenericPathElement$fNFDataPathElement fastTypeOf fastSchemaOf improveProps improveProp improveLit improveEq ShowParseable showParseable maybeNameDoc$fShowParseableName$fShowParseableTParam$fShowParseableLocated$fShowParseableMaybe$fShowParseable[]$fShowParseableDeclGroup$fShowParseableDeclDef$fShowParseableDecl$fShowParseableMatch$fShowParseableSelector$fShowParseableType$fShowParseableIdent$fShowParseableInt$fShowParseable(,)$fShowParseableExpr mkIfaceDeclgenIfaceConstraintSourceCtComprehension CtSplitPat CtTypeSigCtInst CtSelector CtExactType CtEnumeration CtDefaultingCtPartialTypeFun CtImprovement CtPatternCtModuleInstance DelayedCt dctSource dctForalldctAsmpsdctGoals HasGoalSln hasDoSelecthasDoSetHasGoalhasNamehasGoalGoal goalSource goalRangegoalLitGoalGoalsgoalSetsaturatedPropSet literalGoalsliteralLessThanGoalsVarTypeExtVarCurSCC SolverConfig solverPath solverArgs solverVerbosesolverPreludePathdefaultSolverConfig litGoalToGoal goalToLitGoallitLessThanGoalToGoalgoalToLitLessThanGoal emptyGoals nullGoals fromGoals goalsFromList insertGoalselSrcaddTVarsDescsAfteraddTVarsDescsBeforeppUse$fPPConstraintSource$fTVarsConstraintSource $fTVarsGoal $fFVSGoal $fOrdGoal$fEqGoal$fTVarsDelayedCt$fFVSDelayedCt$fTVarsHasGoal $fTVarsGoals $fShowGoals $fShowHasGoal$fShowDelayedCt$fGenericDelayedCt$fNFDataDelayedCt $fShowGoal $fGenericGoal $fNFDataGoal$fShowConstraintSource$fGenericConstraintSource$fNFDataConstraintSource$fShowSolverConfig$fGenericSolverConfig$fNFDataSolverConfigdebugLogSolver startSolver stopSolver resetSolver withSolver debugBlockproveImpcheckUnsolvable tryGetModel shrinkModel isNumeric$fDebugLogSubst$fDebugLogGoal$fDebugLogType $fDebugLogDoc$fDebugLogMaybe $fDebugLog[]$fDebugLogChar$fMk(,,)$fMk(,)$fMkType$fMkTVar $fMkInteger$fMk() KindMismatchTooManyTypeParamsTyVarWithParamsTooManyTySynParamsTooFewTyParamsRecursiveTypeDecls TypeMismatch RecursiveType UnsolvedGoalsUnsolvableGoalsUnsolvedDelayedCtUnexpectedTypeWildCardTypeVariableEscaped NotForAllTooManyPositionalTypeParamsBadParameterKind%CannotMixPositionalAndNamedTypeParamsUndefinedTypeParameterRepeatedTypeParameter AmbiguousSize BareTypeAppUndefinedExistVar TypeShadowingMissingModTParamMissingModVParamTemporaryErrorWarningDefaultingKindDefaultingWildType DefaultingTo cleanupErrorssubsumeserrorImportanceexplainUnsolvablecomputeFreeVarNames $fPPWarning $fFVSWarning$fTVarsWarning $fFVSError $fTVarsError $fShowWarning$fGenericWarning$fNFDataWarningLkpTyVar TLocalVar TOuterVarKRW typeParamskCtrsAllowWildCards NoWildCardsKRO lazyTParams allowWildKindMKMunKMRWiErrors iWarningsiSubst iExistTVars iSolvedHas iNameSeedsiCtsiHasCtsiScope iBindTypesiSupplyROiRangeiVarsiTVars iExtScopeiSolvedHasLazy iMonoBinds iCallStacksiSolver iPrimNames iSolveCounter ScopeName ExternalScope LocalScope SubModule MTopModuleInferMIMunIM InferOutput InferFailedInferOK NameSeedsseedTVarseedGoal InferInputinpRangeinpVarsinpTSyns inpNewtypesinpAbstractTypes inpParamTypesinpParamConstraints inpParamFuns inpNameSeeds inpMonoBinds inpCallStacks inpSearchPath inpPrimNames inpSupply inpSolver nameSeeds bumpCounter runInferMioinRange inRangeMbcurRange recordErrorrecordErrorLoc recordWarning getSolver getPrimMapnewGoalnewGoalsgetGoalsaddGoals collectGoalssimpGoal simpGoals newHasGoal addHasGoal getHasGoals solveHasGoal newParamNamenewName newGoalNamenewTVarnewTVar'checkParamKind newTParamnewTypeunify applySubstapplySubstPredsapplySubstGoalsgetSubst extendSubst varsWithAsmps lookupVar lookupTParam lookupTSyn lookupNewtypelookupAbstractTypelookupParamTypelookupParamFunexistVargetTSyns getNewtypesgetAbstractTypes getParamFuns getParamTypesgetParamConstraintsgetTVarsgetBoundInScope getMonoBinds getCallStackscheckTShadowing withTParam withTParamsnewScope newLocalScopenewSubmoduleScopenewModuleScopeupdScope endLocalScope endSubmodule endModuleendModuleInstancegetScopeaddDeclsaddTySyn addNewtype addPrimType addParamType addParamFunaddParameterConstraints inNewScope withVarType withVarTypeswithVar withMonoType withMonoTypesrunKindM kLookupTyVarkWildOK kRecordErrorkRecordWarningkIOkNewType kLookupTSynkLookupNewtypekLookupParamTypekLookupAbstractType kExistTVar kInstantiateTkSetKindkInRange kNewGoals kInInferM$fFreshMInferM$fMonadFixInferM$fMonadFailInferM $fMonadInferM$fApplicativeInferM$fFunctorInferM$fMonadFailKindM $fMonadKindM$fApplicativeKindM$fFunctorKindM$fShowInferOutput$fShowNameSeeds$fGenericNameSeeds$fNFDataNameSeeds tryHasGoal ExpectedMonoTupleSelectorOutOfRange MissingFieldUnexpectedTupleShapeUnexpectedRecordShapeUnexpectedSequenceShape BadSelectorBadInstantiationCaptured BadProofNoAbsBadProofTyVarsNotEnoughArgumentsInKindBadApplicationFreeTypeVariableBadTypeApplicationRepeatedVariableInForallBadMatchEmptyArmUndefinedTypeVaraibleUndefinedVariableProofObligationsametcExprtcDeclstcModule $fSameTParam $fSameSchema $fSameType$fSame[] $fMonadTcM$fApplicativeTcM $fFunctorTcMdefaultLiteralsflitDefaultCandidatesimproveByDefaultingWithPuredefaultReplExpr'defaultReplExprdefaultAndSimplifysimplifyAllConstraintsproveModuleTopLevelproveImplication checkSchemacheckParameterType checkTySyn checkPropSyn checkNewtype checkPrimType checkTypecheckParameterConstraintsMaybeCheckedTypeChecked UncheckedTypeArg tyArgName tyArgTypeuncheckedTypeArginstantiateWith inferModulecheckE inferBinds checkSigB checkTopDecls rewModule$fTrieMapRewMap'(,,) addModParams$fAddParamsNewtype$fAddParamsTySyn$fAddParamsDecl$fAddParamsDeclGroup$fAddParamsExpr$fAddParamsType$fAddParamsSchema $fAddParams[] $fInstNewtype $fInstTySyn $fInstType $fInstDeclDef $fInstDecl$fInstDeclGroup $fInstMatch $fInstExpr$fInst[] ImportIface BindsNames namingEnvCollectM NestedModsBuildNamingEnvrunBuildInModule NamingEnvnamingEnvNames namespaceMaplookupNSlookupValNameslookupTypeNames singletonNS singletonE singletonTnamingEnvRenamemerge toPrimMap toNameDisp visibleNamesqualify filterNames shadowing travNamingEnvnewTopnewLocalbuildNamingEnvdefsOfcollectNestedModulescollectNestedModulesDeclscollectNestedModulesDsinterpImportEnvinterpImportIfaceunqualifiedEnvmodParamsNamingEnv moduleDefs $fPPNamingEnv$fMonoidNamingEnv$fSemigroupNamingEnv$fMonoidBuildNamingEnv$fSemigroupBuildNamingEnv$fBindsNamesInModule$fBindsNamesInModule0$fBindsNamesInModule1$fBindsNamesInModule2$fBindsNamesInModule3$fBindsNamesInModule4$fBindsNamesInModule5$fBindsNamesModuleG$fBindsNamesTParam$fBindsNamesInModule6$fBindsNamesSchema$fBindsNames[]$fBindsNamesMaybe$fBindsNamesNamingEnv$fBindsNamesImportIface$fFunctorInModule$fTraversableInModule$fFoldableInModule$fShowInModule$fShowNamingEnv$fGenericNamingEnv$fNFDataNamingEnvEnvCheckCheckAll CheckOverlap CheckNone rwWarningsrwErrorsrwSupplyrwNameUseCount rwCurrentDeps rwDepGraphrwExternalDepsroLocroNamesroIfacesroCurMod roNestedModsRenameM unRenameM RenamerInfo renSupply renContextrenEnv renIfacesNameTypeNameBindNameUse runRenamer setCurMod getCurMod getNamingEnvsetNestedModulenestedModuleOrigrecordcollectIfaceDepsdepsOfdepGroupcurLoclocatedwithLoc shadowNames shadowNames'checkEnvcontainsOverlap recordUseaddDep warnUnused lookupImport$fFreshMRenameM$fMonadRenameM$fApplicativeRenameM$fFunctorRenameM$fMonoidRenameM$fSemigroupRenameM $fEqEnvCheck$fShowEnvCheckinstantiateModule$fDefinesDeclGroup $fDefinesDecl $fDefines[]$fInstAbstractType$fInstExportSpec $fInstUserTC$fInstTC $fInstTCon $fInstSchema $fShowEnvcheckModuleInstance tcModuleInst ppWarningppNamedWarning ppNamedError WordTooWide UnsupportedUnsupportedSymbolicOp EvalErrorEx EvalError InvalidIndex DivideByZeroNegativeExponent LogNegative UserError LoopErrorNoPrimBadRoundingModeBadValueEvalReadyThunk CallStackreadydisplayCallStackcombineCallStacks pushCallFrame maybeReady delayFill evalSpark blackhole getCallStack withCallStackmodifyCallStackrunEval evalPanic wordTooWide$fMonoidCallStack$fSemigroupCallStack$fShowEvalError $fPPEvalError$fExceptionEvalErrorEx$fShowEvalErrorEx$fPPEvalErrorEx $fMonadIOEval $fMonadEval$fApplicativeEval $fFunctorEval$fExceptionUnsupported$fPPUnsupported$fExceptionWordTooWide$fShowWordTooWide$fPPWordTooWide$fShowUnsupportedBF bfExpWidth bfPrecWidthbfValuefpOptsfpRound fpCheckStatusfpPPfpLitfloatFromRationalfloatToRationalfloatToInteger floatFromBits floatToBitsFPArith2BackendSBitSWordSIntegerSFloatSEvalisReady sDeclareHole sDelayFillsSpark sPushFramesWithCallStacksModifyCallStack sGetCallStack mergeEvalassertSideCondition raiseErrorbitAsLitwordLen wordAsLit wordAsChar integerAsLitfpAsLitbitLitwordLit integerLit fpExactLititeBititeWord iteIntegeriteFloatbitEqbitOrbitAndbitXor bitComplementwordBit wordUpdatepackWord unpackWord wordFromIntjoinWord splitWord extractWordwordOrwordAndwordXorwordComplementwordPlus wordMinuswordMultwordDivwordMod wordSignedDiv wordSignedMod wordShiftLeftwordShiftRightwordSignedShiftRightwordRotateLeftwordRotateRight wordNegatewordLg2wordEqwordSignedLessThan wordLessThanwordGreaterThan wordToIntwordToSignedIntintPlus intNegateintMinusintMultintDivintModintEq intLessThanintGreaterThanintToZnznToIntznPlusznNegateznMinusznMultznEqznRecipfpEq fpLessThan fpGreaterThan fpLogicalEqfpNaNfpPosInffpPlusfpMinusfpMultfpDivfpNegfpAbsfpSqrtfpFMAfpIsZerofpIsNegfpIsNaNfpIsInffpIsNorm fpIsSubnormfpToBits fpFromBits fpToInteger fpFromInteger fpToRationalfpFromRational SRationalsNumsDenomIndexDirection IndexForward IndexBackward invalidIndex cryUserErrorcryNoPrimErrorsDelay intToRationalratio rationalReciprationalDivide rationalFloorrationalCeiling rationalTruncrationalRoundAwayrationalRoundToEven rationalAdd rationalSubrationalNegate rationalMul rationalEqrationalLessThanrationalGreaterThan iteRationalenumerateIntBits'enumerateIntBitsRenamerename RenamedModulermModule rmDefines rmInScope rmImported renameModulerenameTopDecls renameVar renameType$fRenamePropSyn $fRenameTySyn $fRenameMatch$fRenameTypeInst $fRenameExpr$fRenameFunDesc$fRenameUpdField$fRenamePattern$fRenameBindDef $fRenameBind $fRenameType $fRenameProp$fRenameTParam$fRenameSchema$fRenameNewtype $fRenameDecl$fRenameParameterFun$fRenameParameterType$fRenamePrimType$fRenameImpName$fRenameWithMods$fRenameWithMods0DefsdefsFreeVarsfreeVarsDepsvalDepstyDepstyParams transDeps moduleDeps $fMonoidDeps$fSemigroupDeps$fFreeVarsNewtype$fFreeVarsTCon$fFreeVarsTVar$fFreeVarsType$fFreeVarsSchema$fFreeVarsMatch$fFreeVarsDeclDef$fFreeVarsDecl $fFreeVars[] $fDefsMatch $fDefsDecl$fDefsDeclGroup$fDefs[]$fFreeVarsExpr$fFreeVarsDeclGroup$fEqDepsTypeEnv envTypeMapTValueTVBit TVIntegerTVFloatTVIntMod TVRationalTVArrayTVSeqTVStreamTVTupleTVRecTVFun TVNewtype TVAbstracttValTytNumTy tNumValTyisTBittvSeqfinNat' lookupTypeVar bindTypeVarevalTypeevalNewtypeBody evalValType evalNumTypeevalTF $fShowTValue$fSemigroupTypeEnv$fMonoidTypeEnv$fGenericTValue$fNFDataTValue $fEqTValueintegerToBigNat PrimeModulusProjectivePointpxpypztoProjectivePoint primeModulus ec_doubleec_add_nonzeroec_mult ec_twin_multW4ResultW4ErrorW4ConnevalConnW4Eval evalPartial SomeSymFn What4FunCacheWhat4w4w4defsw4funsw4uninterpWarnsw4Evalw4ThunkdoEvalgetSymw4Andw4Notw4ITE addDefEqn addSafety evalErrorassertBVDivisorassertIntDivisorsModAddsModSubsModMult sModNegatesLg2lazyItew4bvShlw4bvLshrw4bvAshrw4bvRolw4bvRorfpRoundingMode fpBinArithfpCvtToIntegerfpCvtToRationalfpCvtFromRational sModRecip$fMonadIOW4Conn $fMonadW4Conn$fApplicativeW4Conn$fFunctorW4Conn$fBackendWhat4$fMonadIOW4Eval $fMonadW4Eval$fApplicativeW4Eval$fFunctorW4Eval$fFunctorW4ResultBVConcretebinBVunaryBVbvValmkBvsignedBV signedValue integerToCharlg2ppBVmask liftBinIntMod fpRoundMode$fBackendConcrete$fShowBV$fShowConcrete IndexSegmentBitIndexSegmentWordIndexSegmentSeqMap indexSeqMap lookupSeqMap finiteSeqMapinfiniteSeqMapenumerateSeqMap streamSeqMap reverseSeqMap updateSeqMap concatSeqMap splitSeqMap dropSeqMap delaySeqMapmemoMap zipSeqMap mapSeqMap mergeSeqMapshiftSeqByInteger barrelShifter$fFunctorSeqMap WordValueforceWordValuewordVal bitmapWordVal joinWordVal takeWordVal dropWordValextractWordValwordValLogicOpwordValUnaryOp joinWordsreverseWordVal wordValAsLit asWordValwordValueEqualsInteger asWordList asBitsMapenumerateWordValueenumerateWordValueRevenumerateIndexSegmentsassertWordValueInBoundsdelayWordValueshiftWordByIntegershiftWordByWordupdateWordByWordshiftSeqByWord wordValueSizeindexWordValueupdateWordValue mergeWord mergeWord'$fGenericWordValueGenValueVRecordVTupleVBitVInteger VRationalVFloatVSeqVWordVStreamVFunVPolyVNumPolyEvalOpts evalLogger evalPPOpts forceValueppValuewordlamflamtlamnlamilammkSeqfromVBit fromVInteger fromVRationalfromVSeqfromSeq fromWordValasIndex fromVWordvWordLen tryFromBitsfromVFun fromVPoly fromVNumPoly fromVTuple fromVRecord fromVFloat lookupRecorditeValue mergeValue$fShowGenValue$fGenericGenValue TestResult FailFalse FailErrorGen returnTests dumpableType randomValueisPass testableTypeexhaustiveTests randomTestsPrimPFunPStrictPWordFun PFloatFunPTyPolyPNumPolyPFinPolyPPrimPValevalPrim GenEvalEnvEvalEnvenvVarsenvTypesppEnvemptyEnv bindVarDirectbindType lookupType$fMonoidGenEvalEnv$fSemigroupGenEvalEnv$fGenericGenEvalEnv UnaryWordBinWordUnaryBinarymkLit ecNumberVintVratioV ecFractionVfromZVbinaryunary ringBinary ringUnary ringNullaryintegralBinary fromIntegerVaddVsubVnegateVmulVdivVexpVcomputeExponentmodV toIntegerVrecipV fieldDivideVroundOpfloorVceilingVtruncV roundAwayV roundToEvenVandVorVxorV complementVlg2VsdivVsmodVtoSignedIntegerVcmpValue bitLessThanbitGreaterThanvalEqvalLtvalGt eqCombine lexCombineeqV distinctV lessThanV lessThanEqV greaterThanVgreaterThanEqVsignedLessThanVzeroVjoinSeqjoinVtakeVdropVsplitVreverseV transposeVccatV logicBinary logicUnaryassertIndexInBounds indexPrim updatePrimfromToV fromThenToVfromToLessThanV fromToByVfromToByLessThanV fromToDownByVfromToDownByGreaterThanVinfFromV infFromThenVshiftLeftReindexshiftRightReindexrotateLeftReindexrotateRightReindex logicShift intShifter wordShifter shiftShrink rotateShrinksshrVerrorV valueToChar valueToStringfoldlVfoldl'VscanlVrandomVparmapV sparkParMapfpConst fpBinArithV fpRndModefpRndRNEfpRndRNAfpRndRTPfpRndRTNfpRndRTZgenericFloatTablegenericPrimTableValue primTabletoExpr FreshVarFns freshBitVar freshWordVarfreshIntegerVar freshFloatVarVarShapeVarBit VarInteger VarRationalVarFloatVarWord VarFinSeqVarTuple VarRecordFinTypeFTBit FTIntegerFTIntMod FTRationalFTFloatFTSeqFTTupleFTRecord FTNewtype ProverResult AllSatResult ThmResultCounterExample EmptyResult ProverErrorCounterExampleTypeSafetyViolationPredicateFalsified ProverStats ProverCommand pcQueryType pcProverName pcVerbose pcValidate pcProverStats pcExtraDecls pcSmtFilepcExprpcSchemapcIgnoreSafety QueryTypeSatQuery ProveQuery SafetyQuerySatNumAllSatSomeSat predArgTypesfinType unFinType flattenShapes flattenShapevarShapeToValuefreshVar computeModel modelPred varModelPred varToExpr$fShowQueryType $fShowSatNum moduleEnvevalExprevalNewtypeDecls evalDeclsevalSel evalSetSel$fMonoidListEnv$fSemigroupListEnv DynamicEnvDEnvdeNamesdeDeclsdeTySynsdeEnv LoadedModulelmName lmFilePath lmModuleId lmNamingEnv lmInterfacelmModule lmFingerprint LoadedModuleslmLoadedModuleslmLoadedParamModules ModulePathInFileInMem ModContext mctxParams mctxExported mctxDecls mctxNames mctxNameDispCoreLint NoCoreLint ModuleEnvmeLoadedModules meNameSeeds meEvalEnv meCoreLint meMonoBindsmeFocusedModule meSearchPathmeDynEnvmeSupplyresetModuleEnvinitialModuleEnv focusModule loadedModulesloadedNonParamModulesloadedNewtypeshasParamModules allDeclGroups modContextOf dynModContext focusedEnvmodulePathLabelgetLoadedModulesisLoadedisLoadedParamMod lookupModuleaddLoadedModuleremoveLoadedModule deIfaceDecls$fMonoidModContext$fSemigroupModContext$fPPModulePath$fEqModulePath$fMonoidLoadedModules$fSemigroupLoadedModules$fMonoidDynamicEnv$fSemigroupDynamicEnv$fNFDataModuleEnv$fGenericModuleEnv$fGenericDynamicEnv$fShowLoadedModules$fGenericLoadedModules$fNFDataLoadedModules$fShowLoadedModule$fGenericLoadedModule$fNFDataLoadedModule$fShowModulePath$fGenericModulePath$fNFDataModulePath$fGenericCoreLint$fNFDataCoreLint BrowseHowBrowseExported BrowseInScopebrowseModContextSBVEvalsbvEval SBVResultSBVErrorSBV sbvStateVarsbvDefRelations literalSWordfreshBV_ freshSBool_freshSInteger_ svToInteger svFromIntegerashrlshrshl$fMonadSBVResult$fApplicativeSBVResult$fFunctorSBVResult $fBackendSBV$fMonadIOSBVEval$fMonadSBVEval$fApplicativeSBVEval$fFunctorSBVEvalversion commitHashcommitShortHash commitBranch commitDirtydisplayVersion parseModName parseHelpNameparseProgramWith parseModule parseProgram parseExprWith parseExpr parseDeclWith parseDeclparseDeclsWith parseDeclsparseLetDeclWith parseLetDecl parseReplWith parseReplparseSchemaWith parseSchema IncludeError IncludeFailedIncludeDecodeFailedIncludeParseError IncludeCycleremoveIncludesModuleppIncludeError$fMonadFailNoIncM $fMonadNoIncM$fApplicativeNoIncM$fFunctorNoIncM$fShowIncludeError$fGenericIncludeError$fNFDataIncludeErrorModuleM ModuleInputminpCallStacks minpEvalOptsminpByteReader minpModuleEnv minpTCSolverModuleT unModuleT roLoading roEvalOpts roCallStacks roFileReader roTCSolver ModuleWarningTypeCheckWarningsRenamerWarnings ModuleErrorModuleNotFound CantFindFileBadUtf8 OtherIOErrorModuleParseErrorRecursiveModules RenamerErrors NoPatErrorsNoIncludeErrorsTypeCheckingFailed OtherFailureModuleNameMismatchDuplicateModuleNameImportedParamModuleFailedToParameterizeModDefsNotAParameterizedModule ErrorInFile ImportSource FromModule FromImportFromModuleInstanceimportedModulemoduleNotFound cantFindFilebadUtf8 otherIOErrormoduleParseErrorrecursiveModules renamerErrors noPatErrorsnoIncludeErrorstypeCheckingFailedmoduleNameMismatchduplicateModuleNameimportParamModulefailedToParameterizeModDefsnotAParameterizedModule errorInFilewarntypeCheckWarningsrenamerWarningsemptyRO runModuleT runModuleM getByteReader readBytes getModuleEnv getTCSolver setModuleEnvmodifyModuleEnvgetLoadedMaybe loadingImport loadingModuleloadingModInstance interactiveloadinggetImportSourcegetIface getIfaces getLoaded getNameSeeds getSupply setMonoBinds setNameSeeds setSupply unloadModule loadedModule modifyEvalEnv getEvalEnvgetEvalOptsAction getEvalOptsgetFocusedModulesetFocusedModule getSearchPathwithPrependedSearchPath getFocusedEnv getDynEnv setDynEnv withLogger$fPPImportSource$fEqImportSource$fPPModuleError$fNFDataModuleError$fPPModuleWarning$fMonadIOModuleT$fFreshMModuleT$fMonadTModuleT$fMonadFailModuleT$fMonadModuleT$fApplicativeModuleT$fFunctorModuleT$fShowModuleWarning$fGenericModuleWarning$fNFDataModuleWarning$fShowModuleError$fShowImportSource$fGenericImportSource$fNFDataImportSourceTCActiontcActiontcLintertcPrimsActTCLinter lintCheck lintModulenoPatloadModuleByPathloadModuleFrom doLoadModulefullyQualified moduleFile findModulefindFile addPreludeloadDeps checkExpr checkDecls checkModulecheckSingleModule exprLinter declsLinter moduleLinter typecheck genInferInput ModuleRes ModuleCmdloadModuleByNameSpecMSpecT SpecCacherunSpecT liftSpecT getSpecCache setSpecCachemodifySpecCachemodify specializespecializeExprspecializeMatchwithDeclGroupsspecializeEWherespecializeDeclGroupsspecializeConstdestEProofApps destETApps destEProofAbs destETAbs freshNameinstantiateSchemainstantiateExpr traverseSndW4ProverConfig W4ExceptionW4ExW4PortfolioFailure defaultProver proverNames setupProversatProvesatProveOffline$fExceptionW4Exception$fShowW4Exception$fMonadIOMultiSat$fMonadMultiSat$fApplicativeMultiSat$fFunctorMultiSatSBVProverConfigSBVPortfolioException $fExceptionSBVPortfolioException$fShowSBVPortfolioExceptionSmoke Z3NotFound OptionDescroptName optAliases optDefaultoptCheckoptHelpoptEffEnvVal EnvStringEnvProgEnvNumEnvBool REPLException FileNotFoundDirectoryNotFound NoPatErrorNoIncludeErrorTooWideModuleSystemError EvalPolyErrorTypeNotTestableEvalInParamModule SBVExceptionREPLunREPLlNamelPathrunREPLraisecatchfinallyrethrowEvalError getPrompt resetTCSolver getPPValOptsclearLoadedMod setLoadedMod getLoadedMod setEditPath getEditPath clearEditPath setSearchPathprependSearchPathgetProverConfigshouldContinuestop unlessBatchasBatchvalidEvalContextupdateREPLTitlesetUpdateREPLTitle setPutStr getPutStr getLoggerrPutStr rPutStrLnrPrint getExprNames getTypeNamesgetPropertyNames getModNamesuniqifyparseSearchPathsetUser tryGetUsergetUser getKnownUsergetUserShowProverStatsgetUserProverValidateuserOptionsWithAliases userOptionsparsePPFloatFormatparseFieldOrder getUserSatNum whenDebug smokeTest$fPPREPLException$fExceptionREPLException$fMonadMaskREPL$fMonadCatchREPL$fMonadThrowREPL $fFreshMREPL$fMonadBaseControlIOREPL$fMonadBaseIOREPL $fMonadIOREPL $fMonadREPL$fApplicativeREPL $fFunctorREPL$fIsEnvValFieldOrder $fIsEnvVal[] $fIsEnvVal(,) $fIsEnvValInt$fIsEnvValBool $fPPSmoke $fShowSmoke $fEqSmoke $fShowEnvVal$fShowREPLExceptionVListE evalDeclGroupppEValueevaluate$fMonadE$fApplicativeE $fFunctorE $fMonoidEnv$fSemigroupEnv TestReport reportExpr reportResultreportTestsRunreportTestsPossibleQCModeQCRandom QCExhaustCommandExitCode CommandOk CommandError CommandBodyExprArg FileExprArgDeclsArg ExprTypeArg ModNameArg FilenameArg OptionArgShellArgHelpArgNoArg CommandDescrcNamescArgscBodycHelp cLongHelpCommand AmbiguousUnknown commandList runCommandqcCmdqcExprsatCmdproveCmdonlineProveSatofflineProveSatwithRWTempFile moduleCmd loadPreludeloadCmd setOptionCmd handleCtrlC replParse replParseExprinteractiveConfig liftModuleCmdmoduleCmdResult replCheckExpr replEvalExprsanitize splitCommand findCommandfindCommandExact findNbCommand parseCommand$fOrdCommandDescr$fEqCommandDescr$fShowCommandDescr $fEqQCMode $fShowQCMode GHC.MaybeNothingpreludeContentspreludeReferenceContents floatContents arrayContentssuiteBContentsprimeECContentscryptolTcContentsGHC.ShowShow splitQual fnumTokens dropWhite byteForChar AlexInputInpinputalexInputPrevCharalexPosLexSInCharNormalInString InCommentAction startComment endComment addToCommentstartEndComment startString endString addToString startCharendChar addToChar mkQualIdentmkQualOpemitemitS emitFancynumToken fromDigit selectorToken readDecimal alexGetBytesNextTyParamNummkRecordmkEApp anonTyApp mkPrimDeclmkDocmkModulemkAnonymousModulemkModuleInstanceSsTokenssPrevTokParseMPunP parseStringparselexerP happyError errorMessage customErrorexpected mkModNamemkSchemagetNamegetNumgetChrgetStrnumLitfracLitintValmkFixity fromStrLitvalidDemotedTypeunOpbinOpeFromTo eFromToByeFromToByTyped eFromToDownByeFromToDownByTypedasETyped eFromToTypeeFromToLessThaneFromToLessThanType exprToNumT exportDecl exportNewtype exportModulemkParFun mkParType changeExport mkTypeInstmkTParammkTySyn mkPropSynpolyTermmkPoly mkProperty mkIndexedDecl mkIndexedExpr mkGeneratemkIfmkPrimTypeDecldistrLocmkPropmkNested ufToNamedexprToFieldPath mkSelectorghc-prim GHC.TypesTrueFalseGHC.Base$!$fmapGHC.Num*Int GHC.Conc.SyncretryIOintegerRecipModIntegerISIPINrecipModBigNat shiftRBigNat shiftLBigNat testBitBigNatBigNat# bigNatAdd bigNatIsOne bigNatIsZero bigNatMul bigNatRem bigNatSqr bigNatSubbigNatSubUnsafe oneBigNat zeroBigNat EvalPrimshashbranchdirty getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirgetDataFileNameHappyStk