examples: add ChaCha20

[thoughtpolice]

This is the same code example I gave in my Compose Conference 2016
talk, along with a simple Makefile for verification. It's also been
slightly modified for rigid RFC-7539 conformity (notably, specifying
the new counter interface).

As a bonus, both the C program and the Cryptol program come equipped
with a test harness matching the RFC test vectors.

Tested with Clang 3.6.2 and SAW 0.2 on amd64/Linux.

[thoughtpolice]

Oh, and bonus timings for this code; about ~35s to verify for all len = 256 based messages:

austin@server-09:~/src/saw-script/examples/chacha20$ make
clang -std=c99 -O2 -DWITH_TESTS -o chacha20.exe chacha20.c
clang -std=c99 -c -emit-llvm -o chacha20.bc chacha20.c
saw chacha20.saw
Loading module Cryptol
Loading file "chacha20.saw"
Loading module chacha20
loading LLVM bitcode...
extracting stream function...
Time: 35.860711s
checking equality...
Valid
Time: 2.043923s

[atomb]

Thanks for this! It looks very nice.

[kiniry]

I’d say! Good stuff!

On Jul 11, 2016, at 08:23, Aaron Tomb [email protected] wrote:

Thanks for this! It looks very nice.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub #160 (comment), or mute the thread https://github.com/notifications/unsubscribe/AAdOv08i0vZvmn7mm6Oz9JXaNHq5sBx2ks5qUl_ugaJpZM4JIfUm.