Cryptol Reference Manual

Cryptol Reference Manual

• Basic Syntax
  • Declarations
  • Type Signatures
  • Layout
  • Comments
  • Identifiers
  • Keywords and Built-in Operators
  • Built-in Type-level Operators
  • Numeric Literals
• Expressions
  • Calling Functions
  • Prefix Operators
  • Infix Functions
  • Type Annotations
  • Explicit Type Instantiation
  • Local Declarations
  • Block Arguments
  • Conditionals
  • Demoting Numeric Types to Values
• Basic Types
  • Tuples and Records
    • Accessing Fields
    • Updating Fields
  • Sequences
  • Functions
• Overloaded Operations
  • Equality
  • Comparisons
  • Signed Comparisons
  • Zero
  • Logical Operations
  • Basic Arithmetic
  • Integral Operations
  • Division
  • Rounding
• Type Declarations
  • Type Synonyms
  • Newtypes
• Modules
  • Hierarchical Module Names
  • Module Imports
    • Import Lists
    • Hiding Imports
    • Qualified Module Imports
  • Private Blocks
  • Nested Modules
    • Implicit Imports
    • Managing Module Names
  • Parameterized Modules
    • Interface Modules
    • Importing an Interface Module
    • Interface Constraints
    • Instantiating a Parameterized Module
    • Anonymous Interface Modules
    • Anonymous Instantiation Arguments
    • Anonymous Import Instantiations
    • Passing Through Module Parameters
• Properties
  • Testing
    • Numeric Literal Sampling
    • Configuration
  • Proving
    • Configuration
• Foreign Function Interface
  • Platform support
  • Basic usage
  • Compiling C code
  • Converting between Cryptol and C types
    • Overall structure
    • Type parameters
    • Bit
    • Integral types
    • Floating point types
    • Sequences
    • Tuples and records
    • Type synonyms
    • Return values
    • Quick reference
  • Memory
  • Evaluation
  • Example