GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 09:23:04 +03:00
Code Issues Projects Releases Wiki Activity

polishing

Browse Source
This commit is contained in:
Dylan McNamee 2014-04-21 11:40:07 -07:00
parent e937d172d3
commit 4f57c0a93f
2 changed files with 45 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
README.md
View File

@ -105,6 +105,32 @@ binary at `.cabal-sandbox/bin/cryptol` in your source directory. You
can either use that binary directly, or use the results of `tarball` can either use that binary directly, or use the results of `tarball`
or `dist` to install Cryptol in a location of your choice. or `dist` to install Cryptol in a location of your choice.
## Verifying your Installation
Run Cryptol, and at the prompt type:
_ _
___ _ __ _ _ _ __ | |_ ___ | |
/ __| '__| | | | '_ \| __/ _ \| |
| (__| | | |_| | |_) | || (_) | |
\___|_| \__, | .__/ \__\___/|_|
|___/|_| version 2.0.424
Loading module Cryptol
Cryptol> :prove True
If Cryptol responds
Q.E.D.
then your installation is correct. If it prints something like
*** An error occurred.
*** Unable to locate executable for cvc4
*** Executable specified: "cvc4"
then make sure you've installed CVC4, and that the binary is on your `PATH`.
# Contributing # Contributing
We believe that anyone who uses Cryptol is making an important We believe that anyone who uses Cryptol is making an important
@ -113,10 +139,18 @@ to get involved.
## Users ## Users
If you run into a bug in Cryptol, if something doesn't make sense in If you write Cryptol programs that you think would benefit the community, fork the GitHub repository, and
the documentation, if you think something could be better, or if you add them to the `examples/contrib` directory and submit
just have a cool use of Cryptol that you'd like to share with us, use a pull request.
the issues page on [GitHub](https://github.com/GaloisInc/cryptol), or
We host a Cryptol mailing list, which
you can [join here](http://community.galois.com/mailman/listinfo/cryptol-users).
If you run into a bug in Cryptol, if something
doesn't make sense in the documentation, if you
think something could be better, or if you
just have a cool use of Cryptol that you'd like to share with us, use the issues page on
[GitHub](https://github.com/GaloisInc/cryptol), or
send email to <cryptol@galois.com>. send email to <cryptol@galois.com>.
## Developers ## Developers
@ -149,9 +183,7 @@ incorprate your changes.
The `docs` directory of the installation package contains an The `docs` directory of the installation package contains an
introductory book, the `examples` directory contains a number of introductory book, the `examples` directory contains a number of
algorithms specified in Cryptol. We host a Cryptol mailing list, which algorithms specified in Cryptol.
you can join (TODO). If you find bugs, or would like to submit a
patch, please use GitHub to report an issue or send us a pull request.
If you are familiar with version 1 of Cryptol, you should read the If you are familiar with version 1 of Cryptol, you should read the
`Version2Changes` document in the `docs` directory. `Version2Changes` document in the `docs` directory.

13
examples/SHA1.cry
View File

@ -38,13 +38,12 @@ pad : {msgLen,contentLen,chunks,padding}
pad msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64])) pad msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64]))
f : ([8], [32], [32], [32]) -> [32] f : ([8], [32], [32], [32]) -> [32]
f (t, B, C, D) = f (t, x, y, z) =
if (0 <= t) && (t <= 19) then (B && C) || (~B && D) if (0 <= t) && (t <= 19) then (x && y) || (~x && z)
else if (20 <= t) && (t <= 39) then B ^ C ^ D | (20 <= t) && (t <= 39) then x ^ y ^ z
else if (40 <= t) && (t <= 59) then (B && C) || (B && D) || (C && D) | (40 <= t) && (t <= 59) then (x && y) || (x && z) || (y && z)
else if (60 <= t) && (t <= 80) then B ^ C ^ D | (60 <= t) && (t <= 80) then x ^ y ^ z
else error "f: t out of range" else error "f: t out of range"
Ks : [80][32] Ks : [80][32]
Ks = [ 0x5a827999 | t <- [0..19] ] Ks = [ 0x5a827999 | t <- [0..19] ]