adding uncommitted work from previous days

README.md

@@ -19,10 +19,13 @@ Simply stated, Cryptol shows the correctness of cryptography. By presenting a fo
 
 - **src:** contains the main development
 - **HMAC:** contains files related to verification of equivalence between cryptol HMAC and the HMAC spec from FCF
+- **SHA256:** contains files related to verification of equivalence between cryptol SHA256 and FCF SHA256 spec (unfinished)
+- **OTP:** contains files related to the verification of a cryptol implmentation of One Time Pad (good first example)
 - **verif:** contains various interesting other proofs
 - **examples:** example cryptol and microcryptol files to target
 - **script:** A script to generate makefiles, called by [configure](configure)
 
+
 ## Build Instructions
 WARNING: This project is its infancy, and under active development.
 
@@ -47,5 +50,5 @@ NOTE: `make` will only build the coq files in the `src` directory. In order to b
 1. Use cryptol to load your favorite cryptol program: `cryptol <filename>`
 1. In the interactive prompt type `:extract-coq` to print out an AST of every current top level declaration
 1. Copy the output and paste it as the right hand side of a variable declaration in Coq
-1. Use the `eval_expr` or `eager_eval_expr` relation to construct arguments that your terms evaluate to what you want
+1. Use the `eager_eval_expr` relation to construct arguments that your terms evaluate to what you want
 

TOUR.md

@@ -0,0 +1,27 @@
+## 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.
+
+
+
+
+Authored by Eric Mullen, August 2017.