GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-27 01:43:36 +03:00
Code Issues Projects Releases Wiki Activity

integrate MiniLock example

Browse Source
This commit is contained in:
Adam C. Foltzer 2016-01-19 16:18:27 -08:00
parent a4e42b8429
commit bf294a60b8
6 changed files with 25 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Makefile
View File

@ -188,9 +188,12 @@ PKG_EXFUNSTUFF_FILES := examples/funstuff/Coins.cry \
examples/funstuff/NQueens.cry \
examples/funstuff/marble.cry \
PKG_MINILOCK_FILES := $(shell find examples/MiniLock)
${PKG}: ${CRYPTOL_EXE} \
docs/*.md docs/*.pdf LICENSE LICENSE.rtf \
${PKG_EXAMPLE_FILES} ${PKG_EXCONTRIB_FILES} ${PKG_EXFUNSTUFF_FILES}
${PKG_EXAMPLE_FILES} ${PKG_EXCONTRIB_FILES} ${PKG_EXFUNSTUFF_FILES} \
${PKG_MINILOCK_FILES}
$(CABAL) copy ${DESTDIR_ARG}
mkdir -p ${PKG_CRY}
mkdir -p ${PKG_DOC}
@ -204,6 +207,8 @@ ${PKG}: ${CRYPTOL_EXE} \
cp $$EXAMPLE ${PKG_EXCONTRIB}; done
for EXAMPLE in ${PKG_EXFUNSTUFF_FILES}; do \
cp $$EXAMPLE ${PKG_EXFUNSTUFF}; done
cp -r examples/MiniLock ${PKG_EXAMPLES}
# cleanup unwanted files
# don't want to bundle the cryptol library in the binary distribution
rm -rf ${PKG_PREFIX}/lib; rm -rf ${PKG_PREFIX}/*windows-ghc*

3
examples/MiniLock/File.md
View File

@ -1,3 +1,6 @@
Copyright (c) 2013-2016 Galois, Inc.
Distributed under the terms of the BSD3 license (see LICENSE file)
Define the minilock file format, encoding only.
```cryptol

4
examples/MiniLock/Keys.cry
View File

@ -1,3 +1,7 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module Keys where
import CfrgCurves

5
examples/MiniLock/README.md
View File

@ -36,3 +36,8 @@ miniLock [(theirID, nonceA)] filename contents (myPrivKey, myPubKey) key nonceF
Note SCrypt, and thus miniLock ID and key derivation from user passwords, is too
expensive for the Cryptol interpreter to compute on all but todays more powerful
computers. The ID generation can be done using `mkID` from `Keys.cry`.
# License
Copyright (c) 2013-2016 Galois, Inc.
Distributed under the terms of the BSD3 license (see LICENSE file)

3
examples/MiniLock/prim/SHA256.cry
View File

@ -1,4 +1,7 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*
* @tmd - 24 April 2015 - took Ian's SHA512, converted to SHA256
* @ian - 15 August 2015 - he lies, probably ment 2014.
*

4
examples/MiniLock/prim/TestHMAC.cry
View File

@ -1,3 +1,7 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module TestHMAC where
import HMAC