cryptol package¶
cryptol module¶
-
class
cryptol.cryptol.
Cryptol
(cryptol_server='cryptol-server', addr='tcp://127.0.0.1', port=5555)[source]¶ A Cryptol interpreter session.
Instances of this class are sessions with the Cryptol server. The main way to use one of these instances is to call
load_module()
orprelude()
.Parameters: - cryptol_server (str) – The path to the Cryptol server
executable; pass
None
to instead connect to an already-running server - addr (str) – The interface on which to bind the Cryptol server
- port (int) – The port on which to bind the Cryptol server
Raises: CryptolServerError – if the
cryptol_server
executable can’t be found or exits unexpectedly-
exit
()[source]¶ Close the session.
Any modules loaded in this session will be invalid after calling this method.
- cryptol_server (str) – The path to the Cryptol server
executable; pass
-
class
cryptol.cryptol.
_CryptolModule
(port, req, control_req, filepath=None)[source]¶ Abstract class for Cryptol modules.
Note
Users of this module should not instantiate this class directly.
This class is the basis for the objects returned by
load_module()
andprelude()
.Parameters: - req (Socket) – The request socket for this module context
- filepath (str) – The filepath of the Cryptol module to load, or
None
for loading only the prelude
-
check
(expr, fmtargs=(), limit=100)[source]¶ Randomly test a Cryptol property.
Parameters: - expr (str) – The property to test
- fmtargs – The values to substitute in for
?
inexpr
(seetemplate()
) - limit (int) – The number of test cases to run, or
None
to exhaustively check the property
Returns: A
TestReport
for this propertyRaises: - ValueError – if
expr
is empty - CryptolError – if an error occurs during Cryptol
parsing or typechecking; errors during test evaluation are
reported in the
TestReport
.
-
decl
(name)[source]¶ Return a top-level Cryptol declaration in the current module
Because Cryptol and Python have different syntaxes for identifiers, not all Cryptol declarations can be made into members on the object returned by
load_module()
. Use this method to access other declarations without reevaluating them.Parameters: name (str) – The name of the declaration Returns: A Python value representing the named declaration Raises: CryptolError – if the declaration is not in scope
-
eval
(expr, fmtargs=())[source]¶ Evaluate a Cryptol expression in this module’s context.
Parameters: - expr (str) – The expression to evaluate
- fmtargs – The values to substitute in for
?
inexpr
(seetemplate()
)
Returns: A Python value representing the result of evaluating
expr
Raises: CryptolError – if an error occurs during Cryptol parsing, typechecking, or evaluation
-
exit
()[source]¶ End the Cryptol session for this module.
Note
It is usually not necessary to call this method unless this instance might not be garbage-collected.
-
prove
(expr, fmtargs=(), prover=<Provers.CVC4: 'cvc4'>)[source]¶ Prove validity of a Cryptol property, or find a counterexample.
Parameters: - expr (str) – The property to prove
- fmtargs – The values to substitute in for
?
inexpr
(seetemplate()
)
Returns: A
ProofResult
for this propertyRaises: - ProverError – if an error occurs during prover invocation
- CryptolError – if an error occurs during Cryptol parsing, typechecking, evaluation, or symbolic simulation
-
sat
(expr, fmtargs=(), sat_num=1, prover=<Provers.CVC4: 'cvc4'>)[source]¶ Find satisfying assignments for a Cryptol property.
Parameters: - expr (str) – The property to satisfy
- fmtargs – The values to substitute in for
?
inexpr
(seetemplate()
) - sat_num (int) – The maximum number of satisfying
assignments to return; use
None
for no maximum - prover (Provers) – The prover to use
Returns: Either
SatResult
orAllSatResult
, depending onsat_num
Raises: - ProverError – if an error occurs during prover invocation
- CryptolError – if an error occurs during Cryptol parsing, typechecking, evaluation, or symbolic simulation
-
setopt
(option, value)[source]¶ Set an option in the Cryptol session for this module.
Note
This method is going away in the near future, but is here for completeness at the moment. Values set here may be overwritten by calls to
prove()
andsat()
, among others.Parameters: - option (str) – The option to set
- value (str) – The value to assign to
option
-
static
template
(template, args=())[source]¶ Fill in a Cryptol template string.
This replaces instances of
?
with the provided tuple of arguments converted byto_expr()
, similarly to a format string.Note
The number of
?
s in the template and the number of extra arguments must be equal.Parameters: - template (str) – The template string
- args – A tuple of values to splice into the template, or
a non-tuple value if only one hole exists (to splice a
single tuple, pass it in a Python 1-tuple, e.g.,
((True, False),)
.
Raises: TypeError – if the number of arguments does not match the number of holes in the template
-
typeof
(expr, fmtargs=())[source]¶ Get the type of a Cryptol expression.
Parameters: - expr (str) – The expression to typecheck
- fmtargs – The values to substitute in for
?
inexpr
(seetemplate()
)
Return str: The pretty-printed representation of the type
Raises: CryptolError – if an error occurs during Cryptol parsing or typechecking
-
class
cryptol.cryptol.
AllSatResult
(is_sat, argss)[source]¶ The result of a call to
sat()
withsat_num
other than1
-
class
cryptol.cryptol.
Provers
[source]¶ Available provers for Cryptol
-
ANY
¶ Use all available provers, returning the first answer
-
-
exception
cryptol.cryptol.
CryptolError
[source]¶ Bases:
exceptions.Exception
Base class for errors arising from the Cryptol interpreter
-
exception
cryptol.cryptol.
CryptolServerError
[source]¶ Bases:
cryptol.cryptol.CryptolError
An error starting or communicating with the Cryptol server executable
-
exception
cryptol.cryptol.
ProverError
[source]¶ Bases:
cryptol.cryptol.CryptolError
An error arising from the prover configured for Cryptol
-
exception
cryptol.cryptol.
PycryptolInternalError
(msg)[source]¶ Bases:
exceptions.Exception
An internal error in pycryptol that indicates a bug
This deliberately does not extend
CryptolError
, since it should not be expected during normal execution.