Module cryptol 

Functions

load

Load a Cryptol definition. module_path must be the path to a Cryptol module file, and name must be an identifier defined within that module. The type parameter F must be a function pointer type matching the type of the Cryptol definition. For example, if the Cryptol definition has type [8] -> [8] -> [8], then F must be fn(u8, u8) -> u8, fn(i8, i8) -> u8, or some similar combination.

munge

Convert all what4 expressions within x to saw-core and back. The resulting expressions will be equivalent but not necessarily identical.

override_

Load the Cryptol function name from module_path and install it as an override for the function f. f must be a function definition, not a function pointer or closure, and its signature must match the signature of the Cryptol function. For example, if the Cryptol definition has type [8] -> [8] -> [8], then f must have the signature fn(u8, u8) -> u8, fn(i8, i8) -> u8, or some similar combination.

uninterp

Mark the given Cryptol name to be treated as uninterpreted for the duration of the current test.