mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
5bba75fbb6
a new `Cryptol::Reference` module. Change the evaluator API slightly so that primitives can be bound to expressions, in addition to values. We can use this to inject the reference implementations of the above operations into the symbolic evaluators. Because of the exact way evaluation environments are piped around, the bound expression will be evaluated in the environment that the primitive symbol is declared. So, we can't just reference the name of the reference implementation when we inject it. Instead, we abuse the `EWhere` construct to add local definitions corresponding to the entire module. This works, but is a bit unsatisfying, as any top-level CAFs will not be shared across different invocations. This doesn't matter for these functions, but might for e.g, AES.
1133 lines
31 KiB
Plaintext
1133 lines
31 KiB
Plaintext
/*
|
|
* Copyright (c) 2013-2020 Galois, Inc.
|
|
* Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
*/
|
|
|
|
module Cryptol where
|
|
|
|
infixr 5 ==>
|
|
infixr 10 \/
|
|
infixr 15 /\
|
|
infix 20 ==, ===, !=, !==
|
|
infix 30 >, >=, <, <=, <$, >$, <=$, >=$
|
|
infixr 40 ||
|
|
infixl 45 ^
|
|
infixr 50 &&
|
|
infixr 60 #
|
|
infixl 70 <<, <<<, >>, >>>, >>$
|
|
infixl 80 +, -
|
|
infixl 90 *, /, %, /$, %$, %^, /^
|
|
infixr 95 ^^
|
|
infixl 100 @, @@, !, !!
|
|
|
|
|
|
// Base types -----------------------------------------------------------------------
|
|
|
|
/** The type of boolean values. */
|
|
primitive type Bit : *
|
|
|
|
/** The type of unbounded integers. */
|
|
primitive type Integer : *
|
|
|
|
/**
|
|
* 'Z n' is the type of integers, modulo 'n'.
|
|
*
|
|
* The values of 'Z n' may be thought of as equivalance
|
|
* classes of integers according to the equivalence
|
|
* 'x ~ y' iff 'n' divides 'x - y'. 'Z n' naturally
|
|
* forms a ring, but does not support integral division
|
|
* or indexing.
|
|
*
|
|
* However, you may use the 'fromZ' operation
|
|
* to project values in 'Z n' into the integers if such operations
|
|
* are required. This will compute the reduced representative
|
|
* of the equivalance class. In other words, 'fromZ' computes
|
|
* the (unique) integer value 'i' where '0 <= i < n' and
|
|
* 'i' is in the given equivalance class.
|
|
*
|
|
* If the modulus 'n' is prime, 'Z n' also
|
|
* supports computing inverses and forms a field.
|
|
*/
|
|
primitive type {n : #} (fin n, n >= 1) => Z n : *
|
|
|
|
/**
|
|
* 'Rational' is the type of rational numbers.
|
|
* Rational numbers form a Field (and thus a Ring).
|
|
*
|
|
* The 'ratio' operation may be used to directly create
|
|
* rational values from as a ratio of integers, or
|
|
* the 'fromInteger' method and the field operations
|
|
* can be used.
|
|
*/
|
|
primitive type Rational : *
|
|
|
|
type Bool = Bit
|
|
type Word n = [n]
|
|
type Char = [8]
|
|
type String n = [n]Char
|
|
|
|
// Numeric operators and constraints ----------------------------------------------
|
|
|
|
/** A numeric type representing infinity. */
|
|
primitive type inf : #
|
|
|
|
/** Assert that two numeric types are equal. */
|
|
primitive type (==) : # -> # -> Prop
|
|
|
|
/** Assert that two numeric types are different. */
|
|
primitive type (!=) : # -> # -> Prop
|
|
|
|
/** Assert that the first numeric type is larger than, or equal to the second.*/
|
|
primitive type (>=) : # -> # -> Prop
|
|
|
|
/** Assert that a numeric type is a proper natural number (not 'inf'). */
|
|
primitive type fin : # -> Prop
|
|
|
|
/** Assert that a numeric type is a prime number. */
|
|
primitive type prime : # -> Prop
|
|
|
|
/** Add numeric types. */
|
|
primitive type (+) : # -> # -> #
|
|
|
|
/** Multiply numeric types. */
|
|
primitive type (*) : # -> # -> #
|
|
|
|
/** Subtract numeric types. */
|
|
primitive type
|
|
{m : #, n : # }
|
|
(fin n, m >= n) =>
|
|
m - n : #
|
|
|
|
/** Divide numeric types, rounding down. */
|
|
primitive type
|
|
{ m : #, n : # }
|
|
(fin m, n >= 1) =>
|
|
m / n : #
|
|
|
|
/** Remainder of numeric type division. */
|
|
primitive type
|
|
{ m : #, n : # }
|
|
(fin m, n >= 1) =>
|
|
m % n : #
|
|
|
|
/** Exponentiate numeric types. */
|
|
primitive type (^^) : # -> # -> #
|
|
|
|
/** The number of bits required to represent the value of a numeric type. */
|
|
primitive type width : # -> #
|
|
|
|
/**
|
|
* The ceiling of the base-2 logarithm of a numeric type.
|
|
* We define 'lg2 n = width (n - 1)' for nonzero n, and 'lg2 0 = 0'.
|
|
*/
|
|
type lg2 n = width (max n 1 - 1)
|
|
|
|
/** The smaller of two numeric types. */
|
|
primitive type min : # -> # -> #
|
|
|
|
/** The larger of two numeric types. */
|
|
primitive type max : # -> # -> #
|
|
|
|
/** Divide numeric types, rounding up. */
|
|
primitive type
|
|
{ m : #, n : # }
|
|
(fin m, fin n, n >= 1) =>
|
|
m /^ n : #
|
|
|
|
/** How much we need to add to make a proper multiple of the second argument. */
|
|
primitive type
|
|
{ m : #, n : # }
|
|
(fin m, fin n, n >= 1) =>
|
|
m %^ n : #
|
|
|
|
/** The length of an enumeration. */
|
|
primitive type
|
|
{ start : #, next : #, last : # }
|
|
(fin start, fin next, fin last, start != next) =>
|
|
lengthFromThenTo start next last : #
|
|
|
|
/**
|
|
* Assert that the first numeric type is less than or equal to the second.
|
|
*/
|
|
type constraint i <= j = (j >= i)
|
|
|
|
/**
|
|
* Assert that the first numeric type is greater than the second.
|
|
*/
|
|
type constraint i > j = i >= j + 1
|
|
|
|
/**
|
|
* Assert that the first numeric type is less than the second.
|
|
*/
|
|
type constraint i < j = j >= i + 1
|
|
|
|
|
|
// The Literal class ----------------------------------------------------
|
|
|
|
/** 'Literal n a' asserts that type 'a' contains the number 'n'. */
|
|
primitive type Literal : # -> * -> Prop
|
|
|
|
/**
|
|
* The value corresponding to a numeric type.
|
|
*/
|
|
primitive number : {val, rep} Literal val rep => rep
|
|
|
|
/**
|
|
* An alternative name for 'number', present for backward compatibility.
|
|
*/
|
|
demote : {val, rep} Literal val rep => rep
|
|
demote = number`{val}
|
|
|
|
/**
|
|
* Return the length of a sequence. Note that the result depends only
|
|
* on the type of the argument, not its value.
|
|
*/
|
|
length : {n, a, b} (fin n, Literal n b) => [n]a -> b
|
|
length _ = `n
|
|
|
|
/**
|
|
* A finite sequence counting up from 'first' to 'last'.
|
|
*
|
|
* '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'.
|
|
*/
|
|
primitive fromTo : {first, last, a} (fin last, last >= first,
|
|
Literal first a, Literal last a) =>
|
|
[1 + (last - first)]a
|
|
|
|
/**
|
|
* A finite arithmetic sequence starting with 'first' and 'next',
|
|
* stopping when the values reach or would skip over 'last'.
|
|
*
|
|
* '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'.
|
|
*/
|
|
primitive fromThenTo : {first, next, last, a, len}
|
|
( fin first, fin next, fin last
|
|
, Literal first a, Literal next a, Literal last a
|
|
, first != next
|
|
, lengthFromThenTo first next last == len) => [len]a
|
|
|
|
// Fractional Literals ---------------------
|
|
|
|
/** 'FLiteral m n r a' asserts that the type `a' contains the
|
|
fraction `m/n`. The flag `r` indicates if we should round (`r >= 1`)
|
|
or report an error if the number can't be represented exactly. */
|
|
primitive type FLiteral : # -> # -> # -> * -> Prop
|
|
|
|
/** A fractional literal corresponding to `m/n` */
|
|
primitive
|
|
fraction : { m, n, r, a } FLiteral m n r a => a
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
// The Zero class -------------------------------------------------------
|
|
|
|
/** Value types that have a notion of 'zero'. */
|
|
primitive type Zero : * -> Prop
|
|
|
|
/**
|
|
* 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} (Zero a) => a
|
|
|
|
|
|
// The Logic class ------------------------------------------------------
|
|
|
|
/** Value types that support logical operations. */
|
|
primitive type Logic : * -> Prop
|
|
|
|
/**
|
|
* Logical 'and' over bits. Extends element-wise over sequences, tuples.
|
|
*/
|
|
primitive (&&) : {a} (Logic a) => a -> a -> a
|
|
|
|
/**
|
|
* Logical 'or' over bits. Extends element-wise over sequences, tuples.
|
|
*/
|
|
primitive (||) : {a} (Logic a) => a -> a -> a
|
|
|
|
/**
|
|
* Logical 'exclusive or' over bits. Extends element-wise over sequences, tuples.
|
|
*/
|
|
primitive (^) : {a} (Logic a) => a -> a -> a
|
|
|
|
/**
|
|
* Bitwise complement. The prefix notation '~ x'
|
|
* is syntactic sugar for 'complement x'.
|
|
*/
|
|
primitive complement : {a} (Logic a) => a -> a
|
|
|
|
|
|
// The Ring class -------------------------------------------------------
|
|
|
|
/**
|
|
* Value types that support ring addition and multiplication.
|
|
*
|
|
* Floating-point values are only approximately a ring, but
|
|
* nonetheless inhabit this class.
|
|
*/
|
|
primitive type Ring : * -> Prop
|
|
|
|
/**
|
|
* Converts an unbounded integer to a value in a Ring. When converting
|
|
* to the bitvector type [n], the value is reduced modulo 2^^n. Likewise,
|
|
* when converting to Z n, the value is reduced modulo n. When converting
|
|
* to a floating-point value, the value is rounded to the nearest
|
|
* representable value.
|
|
*/
|
|
primitive fromInteger : {a} (Ring a) => Integer -> a
|
|
|
|
/**
|
|
* Add two values.
|
|
* * For type [n], addition is modulo 2^^n.
|
|
* * Structured values are added element-wise.
|
|
*/
|
|
primitive (+) : {a} (Ring a) => a -> a -> a
|
|
|
|
/**
|
|
* Subtract two values.
|
|
* * For type [n], subtraction is modulo 2^^n.
|
|
* * Structured values are subtracted element-wise.
|
|
* * Satisfies 'a - b = a + negate b'.
|
|
* See also: 'negate'.
|
|
*/
|
|
primitive (-) : {a} (Ring a) => a -> a -> a
|
|
|
|
/**
|
|
* Multiply two values.
|
|
* * For type [n], multiplication is modulo 2^^n.
|
|
* * Structured values are multiplied element-wise.
|
|
*/
|
|
primitive (*) : {a} (Ring a) => a -> a -> a
|
|
|
|
/**
|
|
* Returns the additive inverse of its argument.
|
|
* Over structured values, operates element-wise.
|
|
* The prefix notation '- x' is syntactic sugar
|
|
* for 'negate x'.
|
|
*
|
|
* Satisfies 'a + negate a = 0'.
|
|
* Satisfies 'negate a = ~a + 1' for bitvector values.
|
|
*/
|
|
primitive negate : {a} (Ring a) => a -> a
|
|
|
|
|
|
// The Integral class -------------------------------------------------
|
|
|
|
/**
|
|
* Value types that correspond to a segment of the
|
|
* integers. These types support integer division and
|
|
* modulus, indexing into sequences, and enumeration.
|
|
*/
|
|
primitive type Integral : * -> Prop
|
|
|
|
/**
|
|
* Divide two values, rounding down (toward negative infinity).
|
|
* * For type [n], the arguments are treated as unsigned.
|
|
* * Division by zero is undefined.
|
|
*/
|
|
primitive (/) : {a} (Integral a) => a -> a -> a
|
|
|
|
/**
|
|
* Compute the remainder from dividing two values.
|
|
* * For type [n], the arguments are treated as unsigned.
|
|
* * Remainder of division by zero is undefined.
|
|
* * Satisfies 'x % y == x - (x / y) * y'.
|
|
*/
|
|
primitive (%) : {a} (Integral a) => a -> a -> a
|
|
|
|
/**
|
|
* Converts a value of an integral type to an integer.
|
|
*/
|
|
primitive toInteger : {a} (Integral a) => a -> Integer
|
|
|
|
/**
|
|
* Compute the exponentiation of a value in a ring.
|
|
* * For type [n], the exponent is treated as unsigned.
|
|
* * It is an error to raise a value to a negative integer exponent.
|
|
* * Satisfies: 'x ^^ 0 == fromInteger 1'
|
|
* * Satisfies: 'x ^^ e == x * x ^^ (e-1)' when 'e > 0'.
|
|
*/
|
|
primitive (^^) : {a, e} (Ring a, Integral e) => a -> e -> a
|
|
|
|
/**
|
|
* An infinite sequence counting up from the given starting value.
|
|
* '[x...]' is syntactic sugar for 'infFrom x'.
|
|
*/
|
|
primitive infFrom : {a} (Integral a) => a -> [inf]a
|
|
|
|
/**
|
|
* An infinite arithmetic sequence starting with the given two values.
|
|
* '[x,y...]' is syntactic sugar for 'infFromThen x y'.
|
|
*/
|
|
primitive infFromThen : {a} (Integral a) => a -> a -> [inf]a
|
|
|
|
|
|
// The Field class -------------------------------------------------
|
|
|
|
/**
|
|
* Value types that correspond to a field; that is,
|
|
* a ring also posessing multiplicative inverses for
|
|
* non-zero elements.
|
|
*
|
|
* Floating-point values are only approximately a field,
|
|
* but nonetheless inhabit this class.
|
|
*/
|
|
primitive type Field : * -> Prop
|
|
|
|
/**
|
|
* Reciprocal
|
|
*
|
|
* Compute the multiplicative inverse of an element of a field.
|
|
* The reciprocal of 0 is undefined.
|
|
*/
|
|
primitive recip : {a} (Field a) => a -> a
|
|
|
|
/**
|
|
* Field division
|
|
*
|
|
* The division operation in a field.
|
|
* Satisfies 'x /. y == x * (recip y)'
|
|
*
|
|
* Field division by 0 is undefined.
|
|
*/
|
|
primitive (/.) : {a} (Field a) => a -> a -> a
|
|
|
|
|
|
// The Round class -------------------------------------------------
|
|
|
|
/** Value types that can be rounded to integer values. */
|
|
primitive type Round : * -> Prop
|
|
|
|
/**
|
|
* Ceiling function.
|
|
*
|
|
* Given 'x', compute the smallest integer 'i'
|
|
* such that 'x <= i'.
|
|
*/
|
|
primitive ceiling : {a} (Round a) => a -> Integer
|
|
|
|
/**
|
|
* Floor function.
|
|
*
|
|
* Given 'x', compute the largest integer 'i'
|
|
* such that 'i <= x'.
|
|
*/
|
|
primitive floor : {a} (Round a) => a -> Integer
|
|
|
|
/**
|
|
* Truncate the value toward 0.
|
|
*
|
|
* Given 'x' compute the nearest integer between
|
|
* 'x' and 0. For nonnegative 'x', this is floor,
|
|
* and for negative 'x' this is ceiling.
|
|
*/
|
|
primitive trunc : {a} (Round a) => a -> Integer
|
|
|
|
/**
|
|
* Round to the nearest integer, ties away from 0.
|
|
*
|
|
* Ties are broken away from 0. For nonnegative 'x'
|
|
* this is 'floor (x + 0.5)'. For negative 'x' this
|
|
* is 'ceiling (x - 0.5)'.
|
|
*/
|
|
primitive roundAway : {a} (Round a) => a -> Integer
|
|
|
|
/**
|
|
* Round to the nearest integer, ties to even.
|
|
*
|
|
* Ties are broken to the nearest even integer.
|
|
*/
|
|
primitive roundToEven : {a} (Round a) => a -> Integer
|
|
|
|
|
|
// The Eq class ----------------------------------------------------
|
|
|
|
/** Value types that support equality comparisons. */
|
|
primitive type Eq : * -> Prop
|
|
|
|
/**
|
|
* Compares any two values of the same type for equality.
|
|
*/
|
|
primitive (==) : {a} (Eq a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Compares any two values of the same type for inequality.
|
|
*/
|
|
primitive (!=) : {a} (Eq a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Compare the outputs of two functions for equality.
|
|
*/
|
|
(===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
|
|
f === g = \ x -> f x == g x
|
|
|
|
/**
|
|
* Compare the outputs of two functions for inequality.
|
|
*/
|
|
(!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
|
|
f !== g = \x -> f x != g x
|
|
|
|
|
|
// The Cmp class ---------------------------------------------------
|
|
|
|
/** Value types that support equality and ordering comparisons. */
|
|
primitive type Cmp : * -> Prop
|
|
|
|
/**
|
|
* Less-than. Only works on comparable arguments.
|
|
*
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
primitive (<) : {a} (Cmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Greater-than of two comparable arguments.
|
|
*
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
primitive (>) : {a} (Cmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Less-than or equal of two comparable arguments.
|
|
*
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
primitive (<=) : {a} (Cmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Greater-than or equal of two comparable arguments.
|
|
*
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
primitive (>=) : {a} (Cmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* Returns the smaller of two comparable arguments.
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
min : {a} (Cmp a) => a -> a -> a
|
|
min x y = if x < y then x else y
|
|
|
|
/**
|
|
* Returns the greater of two comparable arguments.
|
|
* Bitvectors are compared using unsigned arithmetic.
|
|
*/
|
|
max : {a} (Cmp a) => a -> a -> a
|
|
max x y = if x > y then x else y
|
|
|
|
/**
|
|
* Compute the absolute value of a value from an ordered ring.
|
|
* Bitvector values are considered unsigned, so this is
|
|
* the identity function on [n].
|
|
*/
|
|
abs : {a} (Cmp a, Ring a) => a -> a
|
|
abs x = if x < fromInteger 0 then negate x else x
|
|
|
|
|
|
// The SignedCmp class ----------------------------------------------
|
|
|
|
/** Value types that support signed comparisons. */
|
|
primitive type SignedCmp : * -> Prop
|
|
|
|
/**
|
|
* 2's complement signed less-than.
|
|
*/
|
|
primitive (<$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
|
|
/**
|
|
* 2's complement signed greater-than.
|
|
*/
|
|
(>$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
x >$ y = y <$ x
|
|
|
|
/**
|
|
* 2's complement signed less-than-or-equal.
|
|
*/
|
|
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
x <=$ y = ~(y <$ x)
|
|
|
|
/**
|
|
* 2's complement signed greater-than-or-equal.
|
|
*/
|
|
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
|
|
x >=$ y = ~(x <$ y)
|
|
|
|
|
|
// Bit specific operations ----------------------------------------
|
|
|
|
/**
|
|
* The constant True. Corresponds to the bit value 1.
|
|
*/
|
|
primitive True : Bit
|
|
|
|
/**
|
|
* The constant False. Corresponds to the bit value 0.
|
|
*/
|
|
primitive False : Bit
|
|
|
|
/**
|
|
* Short-cutting boolean conjunction function.
|
|
* If the first argument is False, the second argument
|
|
* is not evaluated.
|
|
*/
|
|
(/\) : Bit -> Bit -> Bit
|
|
x /\ y = if x then y else False
|
|
|
|
/**
|
|
* Short-cutting boolean disjunction function.
|
|
* If the first argument is True, the second argument
|
|
* is not evaluated.
|
|
*/
|
|
(\/) : Bit -> Bit -> Bit
|
|
x \/ y = if x then True else y
|
|
|
|
/**
|
|
* Short-cutting logical implication.
|
|
* If the first argument is False, the second argument is
|
|
* not evaluated.
|
|
*/
|
|
(==>) : Bit -> Bit -> Bit
|
|
a ==> b = if a then b else True
|
|
|
|
|
|
// Bitvector specific operations ----------------------------------
|
|
|
|
/**
|
|
* 2's complement signed division. Division rounds toward 0.
|
|
* Division by 0 is undefined.
|
|
*
|
|
* * Satisfies 'x == x %$ y + (x /$ y) * y' for 'y != 0'.
|
|
*/
|
|
primitive (/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
|
|
|
|
/**
|
|
* 2's complement signed remainder. Division rounds toward 0.
|
|
* Division by 0 is undefined. Satisfies the following for 'y != 0'
|
|
*
|
|
* * 'x %$ y == x - (x /$ y) * y'.
|
|
* * 'x >=$ 0 ==> x %$ y >=$ 0'
|
|
* * 'x <=$ 0 ==> x %$ y <=$ 0'
|
|
*/
|
|
primitive (%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
|
|
|
|
/**
|
|
* Unsigned carry. Returns true if the unsigned addition of the given
|
|
* bitvector arguments would result in an unsigned overflow.
|
|
*/
|
|
carry : {n} (fin n) => [n] -> [n] -> Bit
|
|
carry x y = (x + y) < x
|
|
|
|
/**
|
|
* Signed carry. Returns true if the 2's complement signed addition of the
|
|
* given bitvector arguments would result in a signed overflow.
|
|
*/
|
|
scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
|
|
scarry x y = (sx == sy) && (sx != sz)
|
|
where
|
|
z = x + y
|
|
sx = x@0
|
|
sy = y@0
|
|
sz = z@0
|
|
|
|
/**
|
|
* Signed borrow. Returns true if the 2's complement signed subtraction of the
|
|
* given bitvector arguments would result in a signed overflow.
|
|
*/
|
|
sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
|
|
sborrow x y = ( x <$ (x-y) ) ^ y@0
|
|
|
|
/**
|
|
* Zero extension of a bitvector.
|
|
*/
|
|
zext : {m, n} (fin m, m >= n) => [n] -> [m]
|
|
zext x = zero # x
|
|
|
|
/**
|
|
* Sign extension of a bitvector.
|
|
*/
|
|
sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
|
|
sext x = newbits # x
|
|
where newbits = if x@0 then ~zero else zero
|
|
|
|
/**
|
|
* 2's complement signed (arithmetic) right shift. The first argument
|
|
* is the sequence to shift (considered as a signed value),
|
|
* the second argument is the number of positions to shift
|
|
* by (considered as an unsigned value).
|
|
*/
|
|
primitive (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
|
|
|
|
/**
|
|
* The ceiling of the base-2 logarithm of an unsigned bitvector.
|
|
* We set 'lg2 0 = 0'.
|
|
*/
|
|
primitive lg2 : {n} (fin n) => [n] -> [n]
|
|
|
|
|
|
// Rational specific operations ----------------------------------------------
|
|
|
|
/**
|
|
* Compute the ratio of two integers as a rational.
|
|
* Ratio is undefined if the denominator is 0.
|
|
*
|
|
* 'ratio x y = (fromInteger x /. fromInteger y) : Rational'
|
|
*/
|
|
primitive ratio : Integer -> Integer -> Rational
|
|
|
|
|
|
// Zn specific operations ----------------------------------------------------
|
|
|
|
/**
|
|
* Converts an integer modulo n to an unbounded integer in the range 0 to n-1.
|
|
*/
|
|
primitive fromZ : {n} (fin n, n >= 1) => Z n -> Integer
|
|
|
|
|
|
// Sequence operations -------------------------------------------------------
|
|
|
|
/**
|
|
* Concatenates two sequences. On bitvectors, the most-significant bits
|
|
* are in the left argument, and the least-significant bits are in the right.
|
|
*/
|
|
primitive (#) : {front, back, a} (fin front) => [front]a -> [back]a
|
|
-> [front + back] a
|
|
|
|
/**
|
|
* Splits a sequence into a pair of sequences.
|
|
* 'splitAt z = (x, y)' iff 'x # y = z'.
|
|
*/
|
|
primitive splitAt : {front, back, a} (fin front) => [front + back]a
|
|
-> ([front]a, [back]a)
|
|
|
|
/**
|
|
* Concatenates a list of sequences.
|
|
* 'join' is the inverse function to 'split'.
|
|
*/
|
|
primitive join : {parts, each, a} (fin each) => [parts][each]a
|
|
-> [parts * each]a
|
|
|
|
/**
|
|
* Splits a sequence into 'parts' groups with 'each' elements.
|
|
* 'split' is the inverse function to 'join'.
|
|
*/
|
|
primitive split : {parts, each, a} (fin each) => [parts * each]a
|
|
-> [parts][each]a
|
|
|
|
/**
|
|
* Reverses the elements in a sequence.
|
|
*/
|
|
primitive reverse : {n, a} (fin n) => [n]a -> [n]a
|
|
|
|
/**
|
|
* Transposes a matrix.
|
|
* Satisfies the property 'transpose m @ i @ j == m @ j @ i'.
|
|
*/
|
|
primitive transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
|
|
|
|
|
|
/**
|
|
* Select the first (left-most) 'front' elements of a sequence.
|
|
*/
|
|
take : {front, back, a} (fin front) => [front + back]a -> [front]a
|
|
take (x # _) = x
|
|
|
|
/**
|
|
* Select all the elements after (to the right of) the 'front' elements of a sequence.
|
|
*/
|
|
drop : {front, back, a} (fin front) => [front + back]a -> [back]a
|
|
drop ((_ : [front] _) # y) = y
|
|
|
|
/**
|
|
* Drop the first (left-most) element of a sequence.
|
|
*/
|
|
tail : {n, a} [1 + n]a -> [n]a
|
|
tail xs = drop`{1} xs
|
|
|
|
/**
|
|
* Return the first (left-most) element of a sequence.
|
|
*/
|
|
head : {n, a} [1 + n]a -> a
|
|
head xs = xs @ 0
|
|
|
|
/**
|
|
* Return the right-most element of a sequence.
|
|
*/
|
|
last : {n, a} (fin n) => [1 + n]a -> a
|
|
last xs = xs ! 0
|
|
|
|
/**
|
|
* Same as 'split', but with a different type argument order.
|
|
* Take a sequence of elements and break it into 'parts' sequences
|
|
* of 'each' elements.
|
|
*/
|
|
groupBy : {each, parts, a} (fin each) => [parts * each]a -> [parts][each]a
|
|
groupBy = split`{parts=parts}
|
|
|
|
/**
|
|
* Left shift. The first argument is the sequence to shift, the second is the
|
|
* number of positions to shift by.
|
|
*/
|
|
primitive (<<) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
|
|
|
|
/**
|
|
* Right shift. The first argument is the sequence to shift, the second is the
|
|
* number of positions to shift by.
|
|
*/
|
|
primitive (>>) : {n, ix, a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
|
|
|
|
/**
|
|
* Left rotate. The first argument is the sequence to rotate, the second is the
|
|
* number of positions to rotate by.
|
|
*/
|
|
primitive (<<<) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a
|
|
|
|
/**
|
|
* Right rotate. The first argument is the sequence to rotate, the second is
|
|
* the number of positions to rotate by.
|
|
*/
|
|
primitive (>>>) : {n, ix, a} (fin n, Integral ix) => [n]a -> ix -> [n]a
|
|
|
|
/**
|
|
* 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 (@) : {n, a, ix} (Integral ix) => [n]a -> ix -> a
|
|
|
|
/**
|
|
* 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.
|
|
*/
|
|
(@@) : {n, k, ix, a} (Integral ix) => [n]a -> [k]ix -> [k]a
|
|
xs @@ is = [ xs @ i | i <- is ]
|
|
|
|
/**
|
|
* 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 (!) : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a
|
|
|
|
/**
|
|
* 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
|
|
* select, starting from the end of the sequence.
|
|
*/
|
|
(!!) : {n, k, ix, a} (fin n, Integral ix) => [n]a -> [k]ix -> [k]a
|
|
xs !! is = [ xs ! i | i <- is ]
|
|
|
|
/**
|
|
* Update the given sequence with new value at the given index position.
|
|
* The first argument is a sequence. The second argument is the zero-based
|
|
* index of the element to update, starting from the front of the sequence.
|
|
* The third argument is the new element. The return value is the
|
|
* initial sequence updated so that the indicated index has the given value.
|
|
*/
|
|
primitive update : {n, a, ix} (Integral ix) => [n]a -> ix -> a -> [n]a
|
|
|
|
/**
|
|
* Update the given sequence with new value at the given index position.
|
|
* The first argument is a sequence. The second argument is the zero-based
|
|
* index of the element to update, starting from the end of the sequence.
|
|
* The third argument is the new element. The return value is the
|
|
* initial sequence updated so that the indicated index has the given value.
|
|
*/
|
|
primitive updateEnd : {n, a, ix} (fin n, Integral ix) => [n]a -> ix -> a -> [n]a
|
|
|
|
/**
|
|
* Perform a series of updates to a sequence. The first argument is
|
|
* the initial sequence to update. The second argument is a sequence
|
|
* of indices, and the third argument is a sequence of values.
|
|
* This function applies the 'update' function in sequence with the
|
|
* given update pairs.
|
|
*/
|
|
updates : {n, k, ix, a} (Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
|
|
updates xs0 idxs vals = xss!0
|
|
where
|
|
xss = [ xs0 ] #
|
|
[ update xs i b
|
|
| xs <- xss
|
|
| i <- idxs
|
|
| b <- vals
|
|
]
|
|
|
|
/**
|
|
* Perform a series of updates to a sequence. The first argument is
|
|
* the initial sequence to update. The second argument is a sequence
|
|
* of indices, and the third argument is a sequence of values.
|
|
* This function applies the 'updateEnd' function in sequence with the
|
|
* given update pairs.
|
|
*/
|
|
updatesEnd : {n, k, ix, a} (fin n, Integral ix, fin k) => [n]a -> [k]ix -> [k]a -> [n]a
|
|
updatesEnd xs0 idxs vals = xss!0
|
|
where
|
|
xss = [ xs0 ] #
|
|
[ updateEnd xs i b
|
|
| xs <- xss
|
|
| i <- idxs
|
|
| b <- vals
|
|
]
|
|
|
|
/**
|
|
* Produce a sequence using a generating function.
|
|
* Satisfies 'generate f @ i == f i' for all 'i' between '0' and 'n-1'.
|
|
*
|
|
* Declarations of the form 'x @ i = e' are syntactic sugar for
|
|
* 'x = generate (\i -> e)'.
|
|
*/
|
|
generate : {n, a, ix} (fin n, n >= 1, Integral ix, Literal (n-1) ix) => (ix -> a) -> [n]a
|
|
generate f = [ f i | i <- [0 .. n-1] ]
|
|
|
|
|
|
// GF_2^n polynomial computations -------------------------------------------
|
|
|
|
/**
|
|
* Performs multiplication of polynomials over GF(2).
|
|
*/
|
|
primitive pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
|
|
|
|
/**
|
|
* Performs division of polynomials over GF(2).
|
|
*/
|
|
primitive pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
|
|
|
|
/**
|
|
* Performs modulus of polynomials over GF(2).
|
|
*/
|
|
primitive pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
|
|
|
|
// Experimental primitives ------------------------------------------------------------
|
|
|
|
/**
|
|
* Parallel map. The given function is applied to each element in the
|
|
* given finite seqeuence, and the results are computed in parallel.
|
|
* The values in the resulting sequence are reduced to normal form,
|
|
* as is done with the deepseq operation.
|
|
*
|
|
* The Eq constraint restricts this operation to types
|
|
* where reduction to normal form makes sense.
|
|
*
|
|
* This function is experimental.
|
|
*/
|
|
primitive parmap : {a, b, n} (Eq b, fin n) => (a -> b) -> [n]a -> [n]b
|
|
|
|
|
|
// Utility operations -----------------------------------------------------------------
|
|
|
|
/**
|
|
* A strictness-increasing operation. The first operand
|
|
* is reduced to normal form before evaluating the second
|
|
* argument.
|
|
*
|
|
* The Eq constraint restricts this operation to types
|
|
* where reduction to normal form makes sense.
|
|
*/
|
|
primitive deepseq : {a, b} Eq a => a -> b -> b
|
|
|
|
/**
|
|
* Reduce to normal form.
|
|
*
|
|
* The Eq constraint restricts this operation to types
|
|
* where reduction to normal form makes sense.
|
|
*/
|
|
rnf : {a} Eq a => a -> a
|
|
rnf x = deepseq x x
|
|
|
|
/**
|
|
* Raise a run-time error with the given message.
|
|
* This function can be called at any type.
|
|
*/
|
|
primitive error : {a, n} (fin n) => String n -> a
|
|
|
|
/**
|
|
* Raise a run-time error with a generic message.
|
|
* This function can be called at any type.
|
|
*/
|
|
undefined : {a} a
|
|
undefined = error "undefined"
|
|
|
|
/**
|
|
* Assert that the given condition holds, and raise an error
|
|
* with the given message if it does not. If the condition
|
|
* holds, return the third argument unchanged.
|
|
*/
|
|
assert : {a, n} (fin n) => Bit -> String n -> a -> a
|
|
assert pred msg x = if pred then x else error msg
|
|
|
|
/**
|
|
* Generates random values from a seed. When called with a function, currently
|
|
* generates a function that always returns zero.
|
|
*/
|
|
primitive random : {a} [256] -> a
|
|
|
|
/**
|
|
* 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} (fin n) => String n -> 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} (fin n) => String n -> a -> a
|
|
traceVal msg x = trace msg x x
|
|
|
|
|
|
/* Functions previously in Cryptol::Extras */
|
|
|
|
/**
|
|
* Conjunction of all bits in a sequence.
|
|
*/
|
|
and : {n} (fin n) => [n]Bit -> Bit
|
|
and xs = ~zero == xs
|
|
|
|
/**
|
|
* Disjunction of all bits in a sequence.
|
|
*/
|
|
or : {n} (fin n) => [n]Bit -> Bit
|
|
or xs = zero != xs
|
|
|
|
/**
|
|
* Conjunction after applying a predicate to all elements.
|
|
*/
|
|
all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
|
|
all f xs = foldl' (/\) True (map f xs)
|
|
|
|
/**
|
|
* Disjunction after applying a predicate to all elements.
|
|
*/
|
|
any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
|
|
any f xs = foldl' (\/) False (map f xs)
|
|
|
|
/**
|
|
* Map a function over a sequence.
|
|
*/
|
|
map : {n, a, b} (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
|
|
*/
|
|
primitive foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
|
|
|
|
/**
|
|
* Functional left fold, with strict evaluation of the accumulator value.
|
|
* The accumulator is reduced to normal form at each step. The Eq constraint
|
|
* restricts the accumulator to types where reduction to normal form makes sense.
|
|
*
|
|
* foldl' (+) 0 [1,2,3] = ((0 + 1) + 2) + 3
|
|
*/
|
|
primitive foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a
|
|
|
|
/**
|
|
* Functional right fold.
|
|
*
|
|
* foldr (-) 0 [1,2,3] = 0 - (1 - (2 - 3))
|
|
*/
|
|
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
|
|
foldr f acc xs = foldl g acc (reverse xs)
|
|
where g b a = f a b
|
|
|
|
/**
|
|
* Functional right fold, with strict evaluation of the accumulator value.
|
|
* The accumulator is reduced to weak head normal form at each step.
|
|
*
|
|
* foldr' (-) 0 [1,2,3] = 0 - (1 - (2 - 3))
|
|
*/
|
|
foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b
|
|
foldr' f acc xs = foldl' g acc (reverse xs)
|
|
where g b a = f a b
|
|
|
|
/**
|
|
* Compute the sum of the values in the sequence.
|
|
*/
|
|
sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
|
|
sum xs = foldl' (+) (fromInteger 0) xs
|
|
|
|
|
|
/**
|
|
* Compute the product of the values in the sequence.
|
|
*/
|
|
product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
|
|
product xs = foldl' (*) (fromInteger 1) xs
|
|
|
|
|
|
/**
|
|
* Scan left is like a foldl that also emits the intermediate values.
|
|
*/
|
|
scanl : {n, b, a} (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 is like a foldr that also emits the intermediate values.
|
|
*/
|
|
scanr : {n, a, b} (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]
|
|
|
|
/**
|
|
* Repeat a value.
|
|
*/
|
|
repeat : {n, a} a -> [n]a
|
|
repeat x = [ x | _ <- zero : [n] ]
|
|
|
|
/**
|
|
* 'elem x xs' returns true if x is equal to a value in xs.
|
|
*/
|
|
elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit
|
|
elem a xs = any (\x -> x == a) xs
|
|
|
|
/**
|
|
* Create a list of tuples from two lists.
|
|
*/
|
|
zip : {n, a, b} [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.
|
|
*/
|
|
zipWith : {n, a, b, c} (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 = xs
|
|
where xs = [x] # [ f v | v <- xs ]
|