TOUR.md

Cryptol Semantics

This repository contains a Coq model for some of the semantics of the Cryptol language. It is not (at this point) meant to be a complete model of the langauge, as there are lots of language features left unmodeled. However, enough of the language has been modeled that this model has been used to verify HMAC, One Time Pad, and a decent amount of progress has been made towards verifying SHA256.

The files specific towards these three verification efforts are in the HMAC, SHA256, and OTP directories respectively. The main development is kept in the src directory, which is the only directory strictly necessary to start verifying an additional cryptol program.

There are several make targets. In order to build just the src directory, use the default make target. In order to build everything, use the verif make target. Build in parallel whenever possible.

Eager and Lazy

One of the key insights of this project is that it is much easier to reason about a cryptol program in an eager setting, than in a lazy one. Consider the example of taking some list of bits, and flipping each bit with an xor. In cryptol it would be written something like:

[x ^ True | x <- l ]

where l is your list of bits. In order to reason about the execution of this expression eagerly, you simply evaluate the expression (x ^ True) under many different environments (generated by evaluating l, and making a different environment for each element of l). We are able to keep all elements of l in a coq list, which makes the proof much easier.

Consider now the same expression evaluated lazily. First, we'll evaluate l to get the first element, and a thunk which produces the rest of l. Next we'll evaluate the expression (x ^ True) with x bound to the first element of l, to get the first element of our result. Next we'll produce a thunk to produce the rest of the list. Due to the complexities of matches in cryptol, the semantics currently model this thunk as (rest l), i.e. drop the first element of l and give back the rest. This results in having to re-evaluate the first element of l at every step after, making the proof quadratic in the size of the list.

Individual files

src/AST.v

Here are the basic declarations of the cryptol AST, defined as such to be parseable from the output of the :extract-coq cryptol command. Also in this file are the declarations of the three kinds of values used this development. The most basic are external values, or ext_val, which do not contain any closures, and are intended for specification writing. They are easily functionally convertible to the other kinds of values. Next are strictval and val, which are the values for eager and lazy evaluation respectively. They both do contain closures, and thus the only possible conversion between them is via a relation.

src/Semantics.v

Mainly in this file are the lazy semantics, as the eval_expr relation. Also here are the conversion functions to_sval and to_val, to convert ext_val values to strict and lazy values respectively.

src/Eager.v

Mainly in this file are the eager semantics, as the eager_eval_expr relation.

src/EagerEvalInd.v

Custom induction schemes for eager_eval_expr and eager_eval_type.

src/Utils.v

List parsing notation for Cryptol program ASTs. Also one helper function.

src/GetEachN.v

Coq model of Cryptol split semantics, and associated lemmas.

src/EagerToLazy.v

Attempt at a proof showing that all terms that evaluate eagerly also evaluate lazily.

src/Builtins.v, src/BuiltinSyntax.v

Here are the definition and arity of cryptol builtins (also called primitives).

src/Prims.v

Here are evaluation facts and Coq models for some builtins.

src/SimpleValues.v

Conversion between lists of bits and numbers. Parameterized to be useful with all value types. Intent is to replace all uses of length indexed bitvectors with these lists, to aid in proofs.

src/Bitvectors.v

Port of Compcert's Integers.v. Hopefully deprecated soon. Currently used for some arithmetic operations.

src/Values.v, src/ExtToBitvector.v, src/StrictToBitvector.v

Conversion between lazy/external/strict values and bitvectors. Also contains mostly completed roundtrip proof. Hopefully deprecated soon, as the length index on the type is very annoying to work with.

src/Lib.v

Some useful lemmas.

src/Bitstream.v

Mainly contains typing relation for ext_val.

src/GlobalExtends.v

Contains lemmas about expressions evaluating to the same value under different environments. In order to prove those facts, it was necessary to know that eager evaluation is deterministic, which is proven here as well.

HMAC/

Folder containing the HMAC cryptol to FCF verification effort

SHA256/

Folder containing the SHA256 cryptol to FCF verification effort (unfinished).

otp/

Folder containing the one time pad cryptol to FCF verification effort. Good, readable example to start understanding.

verif/

Folder containing various small unit test-like proofs, many deprecated and commented out.

Authored by Eric Mullen, August 2017.