cryptol package

cryptol module

class cryptol.cryptol.Cryptol(cryptol_server='cryptol-server', addr='tcp://127.0.0.1', port=5555)

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() or prelude().

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()

Close the session.

Any modules loaded in this session will be invalid after calling this method.

load_module(filepath)

Load a Cryptol module.

Returns a Python object with attributes corresponding to constants and methods corresponding to functions defined in the Cryptol module.

Parameters:filepath (str) – The filepath of the Cryptol module to load

prelude()

Load the Cryptol prelude.

class cryptol.cryptol._CryptolModule(port, req, control_req, filepath=None)

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() and prelude().

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

browse()

Browse the definitions in scope in this module.

check(expr, fmtargs=(), limit=100)

Randomly test a Cryptol property.

Parameters:

• expr (str) – The property to test
• fmtargs – The values to substitute in for ? in expr (see template())
• limit (int) – The number of test cases to run, or None to exhaustively check the property

Returns:

A TestReport for this property

Raises:

• 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)

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=())

Evaluate a Cryptol expression in this module’s context.

Parameters:

• expr (str) – The expression to evaluate
• fmtargs – The values to substitute in for ? in expr (see template())

Returns:

A Python value representing the result of evaluating expr

Raises:

CryptolError – if an error occurs during Cryptol parsing, typechecking, or evaluation

exit()

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'>)

Prove validity of a Cryptol property, or find a counterexample.

Parameters:

• expr (str) – The property to prove
• fmtargs – The values to substitute in for ? in expr (see template())

Returns:

A ProofResult for this property

Raises:

• 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'>)

Find satisfying assignments for a Cryptol property.

Parameters:

• expr (str) – The property to satisfy
• fmtargs – The values to substitute in for ? in expr (see template())
• 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 or AllSatResult, depending on sat_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)

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() and sat(), among others.

Parameters:

• option (str) – The option to set
• value (str) – The value to assign to option

static template(template, args=())

Fill in a Cryptol template string.

This replaces instances of ? with the provided tuple of arguments converted by to_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

static to_expr(pyval)

Convert a Python value to a Cryptol expression

typeof(expr, fmtargs=())

Get the type of a Cryptol expression.

Parameters:

• expr (str) – The expression to typecheck
• fmtargs – The values to substitute in for ? in expr (see template())

Return str:

The pretty-printed representation of the type

Raises:

CryptolError – if an error occurs during Cryptol parsing or typechecking

class cryptol.cryptol.ProofResult(is_valid, cex)

The result of a call to prove()

get_counterexample()

Return the counterexample as a tuple of arguments

has_counterexample()

Does the property have a counterexample?

is_valid()

Is the property valid?

class cryptol.cryptol.SatResult(is_sat, args)

The result of a call to sat() with sat_num=1

get_assignment()

Return the satisfying assignment as a tuple of arguments

has_assignment()

Does the property have a satisfying assignment?

is_sat()

Is the property satisfiable?

class cryptol.cryptol.AllSatResult(is_sat, argss)

The result of a call to sat() with sat_num other than 1

assignment_count()

How many satisfying assignments were found?

get_assignments()

Return the satisfying assignments as a list of tuples of arguments

is_sat()

Is the property satisfiable?

class cryptol.cryptol.Provers

Available provers for Cryptol

ANY

Use all available provers, returning the first answer

ABC

Use ABC

BOOLECTOR

Use Boolector

CVC4

Use CVC4

MATHSAT

Use MathSAT

YICES

Use Yices

exception cryptol.cryptol.CryptolError

Bases: exceptions.Exception

Base class for errors arising from the Cryptol interpreter

exception cryptol.cryptol.CryptolServerError

Bases: cryptol.cryptol.CryptolError

An error starting or communicating with the Cryptol server executable

exception cryptol.cryptol.ProverError

Bases: cryptol.cryptol.CryptolError

An error arising from the prover configured for Cryptol

exception cryptol.cryptol.PycryptolInternalError(msg)

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.