mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
adding some examples
This commit is contained in:
parent
a67e350175
commit
3dfb3e147e
72
examples/HMAC.cry
Normal file
72
examples/HMAC.cry
Normal file
@ -0,0 +1,72 @@
|
||||
////////////////////////////////////////////////////////////////
|
||||
// Copyright 2016 Galois, Inc. All Rights Reserved
|
||||
//
|
||||
// Authors:
|
||||
// Aaron Tomb : atomb@galois.com
|
||||
// Nathan Collins : conathan@galois.com
|
||||
// Joey Dodds : jdodds@galois.com
|
||||
//
|
||||
// Licensed under the Apache License, Version 2.0 (the "License").
|
||||
// You may not use this file except in compliance with the License.
|
||||
// A copy of the License is located at
|
||||
//
|
||||
// http://aws.amazon.com/apache2.0
|
||||
//
|
||||
// or in the "license" file accompanying this file. This file is distributed
|
||||
// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
|
||||
// express or implied. See the License for the specific language governing
|
||||
// permissions and limitations under the License.
|
||||
//
|
||||
////////////////////////////////////////////////////////////////
|
||||
|
||||
module HMAC where
|
||||
|
||||
import SHA256
|
||||
|
||||
//////// Functional version ////////
|
||||
|
||||
hmacSHA256 : {pwBytes, msgBytes}
|
||||
(fin pwBytes, fin msgBytes
|
||||
, 32 >= width msgBytes
|
||||
, 64 >= width (8*pwBytes)
|
||||
, 64 >= width (8 * (64 + msgBytes))
|
||||
) => [pwBytes][8] -> [msgBytes][8] -> [256]
|
||||
hmacSHA256 = hmac `{blockLength=64} SHA256 SHA256 SHA256
|
||||
|
||||
kinit : { pwBytes, blockLength, digest }
|
||||
( fin pwBytes, fin blockLength, fin digest )
|
||||
=> ([pwBytes][8] -> [8*digest])
|
||||
-> [pwBytes][8]
|
||||
-> [blockLength][8]
|
||||
kinit hash key =
|
||||
if `pwBytes > (`blockLength : [max (width pwBytes) (width blockLength)])
|
||||
then take `{blockLength} (split (hash key) # (zero : [blockLength][8]))
|
||||
else take `{blockLength} (key # (zero : [blockLength][8]))
|
||||
|
||||
// Due to limitations of the type system we must accept two
|
||||
// separate arguments (both aledgedly the same) for two
|
||||
// separate length inputs.
|
||||
hmac : { msgBytes, pwBytes, digest, blockLength }
|
||||
( fin pwBytes, fin digest, fin blockLength )
|
||||
=> ([blockLength + msgBytes][8] -> [8*digest])
|
||||
-> ([blockLength + digest][8] -> [8*digest])
|
||||
-> ([pwBytes][8] -> [8*digest])
|
||||
-> [pwBytes][8]
|
||||
-> [msgBytes][8]
|
||||
-> [digest*8]
|
||||
hmac hash hash2 hash3 key message = hash2 (okey # internal)
|
||||
where
|
||||
ks : [blockLength][8]
|
||||
ks = kinit hash3 key
|
||||
okey = [k ^ 0x5C | k <- ks]
|
||||
ikey = [k ^ 0x36 | k <- ks]
|
||||
internal = split (hash (ikey # message))
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
38
examples/builtins.cry
Normal file
38
examples/builtins.cry
Normal file
@ -0,0 +1,38 @@
|
||||
//Here's a test of some builtin operators
|
||||
//nothing too deep, just making sure they all work out
|
||||
|
||||
t : [8]
|
||||
t = if True then 5 else 4 //5
|
||||
|
||||
f : [8]
|
||||
f = if False then 3 else 5 //5
|
||||
|
||||
times : [8]
|
||||
times = 5 * 1 * 2 * 3 //30
|
||||
|
||||
div : [8]
|
||||
div = (((30/1)/2)/3) //5
|
||||
|
||||
mod : [8]
|
||||
mod = 205%10 //5
|
||||
|
||||
exp : [8]
|
||||
exp = 2^^7 //128
|
||||
|
||||
lgtest : [8]
|
||||
lgtest = lg2 128 //7
|
||||
|
||||
p : [8]
|
||||
p = 3+2 //5
|
||||
|
||||
m : [8]
|
||||
m = 8-3 //5
|
||||
|
||||
neg : [8]
|
||||
neg = -(-5) //5
|
||||
|
||||
comp : [8]
|
||||
comp = ~250 //5
|
||||
|
||||
|
||||
|
28
examples/mini.cry
Normal file
28
examples/mini.cry
Normal file
@ -0,0 +1,28 @@
|
||||
id : [32] -> [32]
|
||||
id x = rec x
|
||||
where rec k = if (k == 0) then 0 else 1 + rec (k + (-1))
|
||||
|
||||
|
||||
inflist = [1 ... ] : [_][8]
|
||||
|
||||
rc = {x = 3 : [8], y = 5 : [8]}
|
||||
|
||||
my_true = rc.x
|
||||
|
||||
tup = (1 : [8], 2 : [8], 3 : [8], 4 : [8])
|
||||
|
||||
my_3 = tup.2
|
||||
|
||||
sup = y where y = 3 : [8]
|
||||
|
||||
|
||||
gf28Add : {n} (fin n) => [n][8] -> [8]
|
||||
gf28Add ps = sums ! 0
|
||||
where sums = [zero] # [ p ^ s | p <- ps | s <- sums ]
|
||||
|
||||
gex = gf28Add [1,2]
|
||||
|
||||
sum : [_][8] -> [_][8]
|
||||
sum x = rec
|
||||
where rec = [ p + q | p <- x | q <- [1,2,3,4] ]
|
||||
|
Loading…
Reference in New Issue
Block a user