mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
add benchmarks for Extras
There are separate benchmarks for the Extras.cry module and the combined Prelude + Extras module because the performance characteristics are nonlinear.
This commit is contained in:
Adam C. Foltzer
parent
9ad1ff98c6
commit
1a68b4f640
@ -42,6 +42,8 @@ main :: IO ()
|
||||
main = defaultMain [
|
||||
bgroup "parser" [
|
||||
parser "Prelude" "lib/Cryptol.cry"
|
||||
, parser "Extras" "lib/Cryptol/Extras.cry"
|
||||
, parser "PreludeWithExtras" "bench/data/PreludeWithExtras.cry"
|
||||
, parser "BigSequence" "bench/data/BigSequence.cry"
|
||||
, parser "BigSequenceHex" "bench/data/BigSequenceHex.cry"
|
||||
, parser "AES" "bench/data/AES.cry"
|
||||
@ -49,6 +51,8 @@ main = defaultMain [
|
||||
]
|
||||
, bgroup "typechecker" [
|
||||
tc "Prelude" "lib/Cryptol.cry"
|
||||
, tc "Extras" "lib/Cryptol/Extras.cry"
|
||||
, tc "PreludeWithExtras" "bench/data/PreludeWithExtras.cry"
|
||||
, tc "BigSequence" "bench/data/BigSequence.cry"
|
||||
, tc "BigSequenceHex" "bench/data/BigSequenceHex.cry"
|
||||
, tc "AES" "bench/data/AES.cry"
|
||||
|
||||
506
bench/data/PreludeWithExtras.cry
Normal file
506
bench/data/PreludeWithExtras.cry
Normal file
@ -0,0 +1,506 @@
|
||||
/*
|
||||
* Copyright (c) 2013-2016 Galois, Inc.
|
||||
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
||||
*/
|
||||
|
||||
module Cryptol where
|
||||
|
||||
/**
|
||||
* The value corresponding to a numeric type.
|
||||
*/
|
||||
primitive demote : {val, bits} (fin val, fin bits, bits >= width val) => [bits]
|
||||
|
||||
infixr 10 ||
|
||||
infixr 20 &&
|
||||
infix 30 ==, ===, !=, !==
|
||||
infix 40 >, >=, <, <=
|
||||
infixl 50 ^
|
||||
infixr 60 #
|
||||
infixl 70 <<, <<<, >>, >>>
|
||||
infixl 80 +, -
|
||||
infixl 90 *, /, %
|
||||
infixr 95 ^^
|
||||
infixl 100 @, @@, !, !!
|
||||
|
||||
/**
|
||||
* Add two values.
|
||||
* * For words, addition uses modulo arithmetic.
|
||||
* * Structured values are added element-wise.
|
||||
*/
|
||||
primitive (+) : {a} (Arith a) => a -> a -> a
|
||||
|
||||
/**
|
||||
* For words, subtraction uses modulo arithmetic.
|
||||
* Structured values are subtracted element-wise. Defined as:
|
||||
* a - b = a + negate b
|
||||
* See also: `negate'.
|
||||
*/
|
||||
primitive (-) : {a} (Arith a) => a -> a -> a
|
||||
|
||||
/**
|
||||
* For words, multiplies two words, modulus 2^^a.
|
||||
* Structured values are multiplied element-wise.
|
||||
*/
|
||||
primitive (*) : {a} (Arith a) => a -> a -> a
|
||||
|
||||
/**
|
||||
* For words, divides two words, modulus 2^^a.
|
||||
* Structured values are divided element-wise.
|
||||
*/
|
||||
primitive (/) : {a} (Arith a) => a -> a -> a
|
||||
|
||||
/**
|
||||
* For words, takes the modulus of two words, modulus 2^^a.
|
||||
* Over structured values, operates element-wise.
|
||||
* Be careful, as this will often give unexpected results due to interaction of
|
||||
* the two moduli.
|
||||
*/
|
||||
primitive (%) : {a} (Arith a) => a -> a -> a
|
||||
|
||||
/**
|
||||
* For words, takes the exponent of two words, modulus 2^^a.
|
||||
* Over structured values, operates element-wise.
|
||||
* Be careful, due to its fast-growing nature, exponentiation is prone to
|
||||
* interacting poorly with defaulting.
|
||||
*/
|
||||
primitive (^^) : {a} (Arith a) => a -> a -> a
|
||||
|
||||
/**
|
||||
* Log base two.
|
||||
*
|
||||
* For words, computes the ceiling of log, base 2, of a number.
|
||||
* Over structured values, operates element-wise.
|
||||
*/
|
||||
primitive lg2 : {a} (Arith a) => a -> a
|
||||
|
||||
|
||||
type Bool = Bit
|
||||
|
||||
/**
|
||||
* The constant True. Corresponds to the bit value 1.
|
||||
*/
|
||||
primitive True : Bit
|
||||
|
||||
/**
|
||||
* The constant False. Corresponds to the bit value 0.
|
||||
*/
|
||||
primitive False : Bit
|
||||
|
||||
/**
|
||||
* Returns the twos complement of its argument.
|
||||
* Over structured values, operates element-wise.
|
||||
* negate a = ~a + 1
|
||||
*/
|
||||
primitive negate : {a} (Arith a) => a -> a
|
||||
|
||||
/**
|
||||
* Binary complement.
|
||||
*/
|
||||
primitive complement : {a} a -> a
|
||||
|
||||
/**
|
||||
* Operator form of binary complement.
|
||||
*/
|
||||
(~) : {a} a -> a
|
||||
(~) = complement
|
||||
|
||||
/**
|
||||
* Less-than. Only works on comparable arguments.
|
||||
*/
|
||||
primitive (<) : {a} (Cmp a) => a -> a -> Bit
|
||||
|
||||
/**
|
||||
* Greater-than of two comparable arguments.
|
||||
*/
|
||||
primitive (>) : {a} (Cmp a) => a -> a -> Bit
|
||||
|
||||
/**
|
||||
* Less-than or equal of two comparable arguments.
|
||||
*/
|
||||
primitive (<=) : {a} (Cmp a) => a -> a -> Bit
|
||||
|
||||
/**
|
||||
* Greater-than or equal of two comparable arguments.
|
||||
*/
|
||||
primitive (>=) : {a} (Cmp a) => a -> a -> Bit
|
||||
|
||||
/**
|
||||
* Compares any two values of the same type for equality.
|
||||
*/
|
||||
primitive (==) : {a} (Cmp a) => a -> a -> Bit
|
||||
|
||||
/**
|
||||
* Compares any two values of the same type for inequality.
|
||||
*/
|
||||
primitive (!=) : {a} (Cmp a) => a -> a -> Bit
|
||||
|
||||
/**
|
||||
* Compare the outputs of two functions for equality
|
||||
*/
|
||||
(===) : {a,b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)
|
||||
f === g = \ x -> f x == g x
|
||||
|
||||
/**
|
||||
* Compare the outputs of two functions for inequality
|
||||
*/
|
||||
(!==) : {a,b} (Cmp b) => (a -> b) -> (a -> b) -> (a -> Bit)
|
||||
f !== g = \x -> f x != g x
|
||||
|
||||
/**
|
||||
* Returns the smaller of two comparable arguments.
|
||||
*/
|
||||
min : {a} (Cmp a) => a -> a -> a
|
||||
min x y = if x < y then x else y
|
||||
|
||||
/**
|
||||
* Returns the greater of two comparable arguments.
|
||||
*/
|
||||
max : {a} (Cmp a) => a -> a -> a
|
||||
max x y = if x > y then x else y
|
||||
|
||||
/**
|
||||
* Logical `and' over bits. Extends element-wise over sequences, tuples.
|
||||
*/
|
||||
primitive (&&) : {a} a -> a -> a
|
||||
|
||||
/**
|
||||
* Logical `or' over bits. Extends element-wise over sequences, tuples.
|
||||
*/
|
||||
primitive (||) : {a} a -> a -> a
|
||||
|
||||
/**
|
||||
* Logical `exclusive or' over bits. Extends element-wise over sequences, tuples.
|
||||
*/
|
||||
primitive (^) : {a} a -> a -> a
|
||||
|
||||
/**
|
||||
* Gives an arbitrary shaped value whose bits are all False.
|
||||
* ~zero likewise gives an arbitrary shaped value whose bits are all True.
|
||||
*/
|
||||
primitive zero : {a} a
|
||||
|
||||
/**
|
||||
* Left shift. The first argument is the sequence to shift, the second is the
|
||||
* number of positions to shift by.
|
||||
*/
|
||||
primitive (<<) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
|
||||
|
||||
/**
|
||||
* Right shift. The first argument is the sequence to shift, the second is the
|
||||
* number of positions to shift by.
|
||||
*/
|
||||
primitive (>>) : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
|
||||
|
||||
/**
|
||||
* Left rotate. The first argument is the sequence to rotate, the second is the
|
||||
* number of positions to rotate by.
|
||||
*/
|
||||
primitive (<<<) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
|
||||
|
||||
/**
|
||||
* Right rotate. The first argument is the sequence to rotate, the second is
|
||||
* the number of positions to rotate by.
|
||||
*/
|
||||
primitive (>>>) : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
|
||||
|
||||
primitive (#) : {front, back, a} (fin front) => [front]a -> [back]a
|
||||
-> [front + back] a
|
||||
|
||||
|
||||
/**
|
||||
* Split a sequence into a tuple of sequences.
|
||||
*/
|
||||
primitive splitAt : {front, back, a} (fin front) => [front + back]a
|
||||
-> ([front]a, [back]a)
|
||||
/**
|
||||
* Joins sequences.
|
||||
*/
|
||||
primitive join : {parts, each, a} (fin each) => [parts][each]a
|
||||
-> [parts * each]a
|
||||
|
||||
/**
|
||||
* Splits a sequence into 'parts' groups with 'each' elements.
|
||||
*/
|
||||
primitive split : {parts, each, a} (fin each) => [parts * each]a
|
||||
-> [parts][each]a
|
||||
|
||||
/**
|
||||
* Reverses the elements in a sequence.
|
||||
*/
|
||||
primitive reverse : {a, b} (fin a) => [a]b -> [a]b
|
||||
|
||||
/**
|
||||
* Transposes an [a][b] matrix into a [b][a] matrix.
|
||||
*/
|
||||
primitive transpose : {a, b, c} [a][b]c -> [b][a]c
|
||||
|
||||
/**
|
||||
* Index operator. The first argument is a sequence. The second argument is
|
||||
* the zero-based index of the element to select from the sequence.
|
||||
*/
|
||||
primitive (@) : {a, b, c} (fin c) => [a]b -> [c] -> b
|
||||
|
||||
/**
|
||||
* Bulk index operator. The first argument is a sequence. The second argument
|
||||
* is a sequence of the zero-based indices of the elements to select.
|
||||
*/
|
||||
primitive (@@) : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b
|
||||
|
||||
/**
|
||||
* Reverse index operator. The first argument is a finite sequence. The second
|
||||
* argument is the zero-based index of the element to select, starting from the
|
||||
* end of the sequence.
|
||||
*/
|
||||
primitive (!) : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b
|
||||
|
||||
/**
|
||||
* Bulk reverse index operator. The first argument is a finite sequence. The
|
||||
* second argument is a sequence of the zero-based indices of the elements to
|
||||
z select, starting from the end of the sequence.
|
||||
*/
|
||||
primitive (!!) : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b
|
||||
|
||||
primitive fromThen : {first, next, bits, len}
|
||||
( fin first, fin next, fin bits
|
||||
, bits >= width first, bits >= width next
|
||||
, lengthFromThen first next bits == len) => [len][bits]
|
||||
|
||||
primitive fromTo : {first, last, bits} (fin last, fin bits, last >= first,
|
||||
bits >= width last) => [1 + (last - first)][bits]
|
||||
|
||||
primitive fromThenTo : {first, next, last, bits, len} (fin first, fin next,
|
||||
fin last, fin bits, bits >= width first,
|
||||
bits >= width next, bits >= width last,
|
||||
lengthFromThenTo first next last == len) => [len][bits]
|
||||
|
||||
primitive infFrom : {bits} (fin bits) => [bits] -> [inf][bits]
|
||||
|
||||
primitive infFromThen : {bits} (fin bits) => [bits] -> [bits] -> [inf][bits]
|
||||
|
||||
primitive error : {at, len} (fin len) => [len][8] -> at
|
||||
|
||||
|
||||
/**
|
||||
* Performs multiplication of polynomials over GF(2).
|
||||
*/
|
||||
primitive pmult : {a, b} (fin a, fin b) => [a] -> [b] -> [max 1 (a + b) - 1]
|
||||
|
||||
/**
|
||||
* Performs division of polynomials over GF(2).
|
||||
*/
|
||||
primitive pdiv : {a, b} (fin a, fin b) => [a] -> [b] -> [a]
|
||||
|
||||
/**
|
||||
* Performs modulus of polynomials over GF(2).
|
||||
*/
|
||||
primitive pmod : {a, b} (fin a, fin b) => [a] -> [1 + b] -> [b]
|
||||
|
||||
/**
|
||||
* Generates random values from a seed. When called with a function, currently
|
||||
* generates a function that always returns zero.
|
||||
*/
|
||||
primitive random : {a} [256] -> a
|
||||
|
||||
type String n = [n][8]
|
||||
type Word n = [n]
|
||||
type Char = [8]
|
||||
|
||||
take : {front,back,elem} (fin front) => [front + back] elem -> [front] elem
|
||||
take (x # _) = x
|
||||
|
||||
drop : {front,back,elem} (fin front) => [front + back] elem -> [back] elem
|
||||
drop ((_ : [front] _) # y) = y
|
||||
|
||||
tail : {a, b} [1 + a]b -> [a]b
|
||||
tail xs = drop`{1} xs
|
||||
|
||||
width : {bits,len,elem} (fin len, fin bits, bits >= width len) => [len] elem -> [bits]
|
||||
width _ = `len
|
||||
|
||||
undefined : {a} a
|
||||
undefined = error "undefined"
|
||||
|
||||
groupBy : {each,parts,elem} (fin each) =>
|
||||
[parts * each] elem -> [parts][each]elem
|
||||
groupBy = split`{parts=parts}
|
||||
|
||||
/**
|
||||
* Define the base 2 logarithm function in terms of width
|
||||
*/
|
||||
type lg2 n = width (max n 1 - 1)
|
||||
|
||||
/**
|
||||
* Debugging function for tracing. The first argument is a string,
|
||||
* which is prepended to the printed value of the second argument.
|
||||
* This combined string is then printed when the trace function is
|
||||
* evaluated. The return value is equal to the third argument.
|
||||
*
|
||||
* The exact timing and number of times the trace message is printed
|
||||
* depend on the internal details of the Cryptol evaluation order,
|
||||
* which are unspecified. Thus, the output produced by this
|
||||
* operation may be difficult to predict.
|
||||
*/
|
||||
primitive trace : {n, a, b} [n][8] -> a -> b -> b
|
||||
|
||||
/**
|
||||
* Debugging function for tracing values. The first argument is a string,
|
||||
* which is prepended to the printed value of the second argument.
|
||||
* This combined string is then printed when the trace function is
|
||||
* evaluated. The return value is equal to the second argument.
|
||||
*
|
||||
* The exact timing and number of times the trace message is printed
|
||||
* depend on the internal details of the Cryptol evaluation order,
|
||||
* which are unspecified. Thus, the output produced by this
|
||||
* operation may be difficult to predict.
|
||||
*/
|
||||
traceVal : {n, a} [n][8] -> a -> a
|
||||
traceVal msg x = trace msg x x
|
||||
|
||||
/*
|
||||
* Copyright (c) 2016 Galois, Inc.
|
||||
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
||||
*
|
||||
* This module contains definitions that we wish to eventually promote
|
||||
* into the Prelude, but which currently cause typechecking of the
|
||||
* Prelude to take too long (see #299)
|
||||
*/
|
||||
|
||||
infixr 5 ==>
|
||||
|
||||
/**
|
||||
* Logical implication
|
||||
*/
|
||||
(==>) : Bit -> Bit -> Bit
|
||||
a ==> b = if a then b else True
|
||||
|
||||
/**
|
||||
* Logical negation
|
||||
*/
|
||||
not : {a} a -> a
|
||||
not a = ~ a
|
||||
|
||||
/**
|
||||
* Conjunction
|
||||
*/
|
||||
and : {n} (fin n) => [n]Bit -> Bit
|
||||
and xs = ~zero == xs
|
||||
|
||||
/**
|
||||
* Disjunction
|
||||
*/
|
||||
or : {n} (fin n) => [n]Bit -> Bit
|
||||
or xs = zero != xs
|
||||
|
||||
/**
|
||||
* Conjunction after applying a predicate to all elements.
|
||||
*/
|
||||
all : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit
|
||||
all f xs = and (map f xs)
|
||||
|
||||
/**
|
||||
* Disjunction after applying a predicate to all elements.
|
||||
*/
|
||||
any : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit
|
||||
any f xs = or (map f xs)
|
||||
|
||||
/**
|
||||
* Map a function over an array.
|
||||
*/
|
||||
map : {a, b, n} (a -> b) -> [n]a -> [n]b
|
||||
map f xs = [f x | x <- xs]
|
||||
|
||||
/**
|
||||
* Functional left fold.
|
||||
*
|
||||
* foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3
|
||||
*/
|
||||
foldl : {a, b, n} (fin n) => (a -> b -> a) -> a -> [n]b -> a
|
||||
foldl f acc xs = ys ! 0
|
||||
where ys = [acc] # [f a x | a <- ys | x <- xs]
|
||||
|
||||
/**
|
||||
* Functional right fold.
|
||||
*
|
||||
* foldr (-) 0 [1,2,3] = 0 - (1 - (2 - 3))
|
||||
*/
|
||||
foldr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> b
|
||||
foldr f acc xs = ys ! 0
|
||||
where ys = [acc] # [f x a | a <- ys | x <- reverse xs]
|
||||
|
||||
/**
|
||||
* Compute the sum of the words in the array.
|
||||
*/
|
||||
sum : {a,n} (fin n, Arith a) => [n]a -> a
|
||||
sum xs = foldl (+) zero xs
|
||||
|
||||
/**
|
||||
* Scan left is like a fold that emits the intermediate values.
|
||||
*/
|
||||
scanl : {b, a, n} (b -> a -> b) -> b -> [n]a -> [n+1]b
|
||||
scanl f acc xs = ys
|
||||
where
|
||||
ys = [acc] # [f a x | a <- ys | x <- xs]
|
||||
|
||||
/**
|
||||
* Scan right
|
||||
*/
|
||||
scanr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
|
||||
scanr f acc xs = reverse ys
|
||||
where
|
||||
ys = [acc] # [f x a | a <- ys | x <- reverse xs]
|
||||
|
||||
/**
|
||||
* Zero extension
|
||||
*/
|
||||
extend : {total,n} (fin total, fin n, total >= n) => [n]Bit -> [total]Bit
|
||||
extend n = zero # n
|
||||
|
||||
/**
|
||||
* Signed extension. `extendSigned 0bwxyz : [8] == 0bwwwwwxyz`.
|
||||
*/
|
||||
extendSigned : {total,n} (fin total, fin n, n >= 1, total >= n+1) => [n]Bit -> [total]Bit
|
||||
extendSigned xs = repeat (xs @ 0) # xs
|
||||
|
||||
/**
|
||||
* Repeat a value.
|
||||
*/
|
||||
repeat : {n, a} a -> [n]a
|
||||
repeat x = [ x | _ <- zero ]
|
||||
|
||||
/**
|
||||
* `elem x xs` Returns true if x is equal to a value in xs.
|
||||
*/
|
||||
elem : {n,a} (fin n, Cmp a) => a -> [n]a -> Bit
|
||||
elem a xs = any (\x -> x == a) xs
|
||||
|
||||
/**
|
||||
* Create a list of tuples from two lists.
|
||||
*/
|
||||
zip : {a,b,n} [n]a -> [n]b -> [n](a,b)
|
||||
zip xs ys = [(x,y) | x <- xs | y <- ys]
|
||||
|
||||
/**
|
||||
* Create a list by applying the function to each pair of elements in the input.
|
||||
* lists
|
||||
*/
|
||||
zipWith : {a,b,c,n} (a -> b -> c) -> [n]a -> [n]b -> [n]c
|
||||
zipWith f xs ys = [f x y | x <- xs | y <- ys]
|
||||
|
||||
/**
|
||||
* Transform a function into uncurried form.
|
||||
*/
|
||||
uncurry : {a,b,c} (a -> b -> c) -> (a,b) -> c
|
||||
uncurry f = \(a,b) -> f a b
|
||||
|
||||
/**
|
||||
* Transform a function into curried form.
|
||||
*/
|
||||
curry : {a,b,c} ((a, b) -> c) -> a -> b -> c
|
||||
curry f = \a b -> f (a,b)
|
||||
|
||||
/**
|
||||
* Map a function iteratively over a seed value, producing an infinite
|
||||
* list of successive function applications.
|
||||
*/
|
||||
iterate : { a } (a -> a) -> a -> [inf]a
|
||||
iterate f x = [x] # [ f v | v <- iterate f x ]
|
||||
Loading…
Reference in New Issue
Block a user