mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-19 01:49:11 +03:00
41613ade02
It is convenient for Coq extraction for the constant 1 factor to be on the left of the addition symbol.
1209 lines
34 KiB
Plaintext
1209 lines
34 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 equivalence
|
|
* 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 equivalence class. In other words, 'fromZ' computes
|
|
* the (unique) integer value 'i' where '0 <= i < n' and
|
|
* 'i' is in the given equivalence 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 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 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
|
|
|
|
/**
|
|
* 'LiteralLessThan n a' asserts that the type 'a' contains all the
|
|
* natural numbers strictly below 'n'. Note that we may have 'n = inf',
|
|
* in which case the type 'a' must be unbounded.
|
|
*/
|
|
primitive type LiteralLessThan : # -> * -> 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'.
|
|
*
|
|
* '[x .. y]' is syntactic sugar for 'fromTo`{first=x,last=y}'.
|
|
*/
|
|
primitive fromTo : {first, last, a}
|
|
(fin last, last >= first, Literal last a) =>
|
|
[1 + (last - first)]a
|
|
|
|
/**
|
|
* A possibly infinite sequence counting up from 'first' up to (but not including) 'bound'.
|
|
*
|
|
* '[ x ..< y ]' is syntactic sugar for 'fromToLessThan`{first=x,bound=y}'.
|
|
*
|
|
* Note that if 'first' = 'bound' then the sequence will be empty. If 'bound = inf'
|
|
* then the sequence will be infinite, and will eventually wrap around for bounded types.
|
|
*/
|
|
primitive fromToLessThan :
|
|
{first, bound, a} (fin first, bound >= first, LiteralLessThan bound a) =>
|
|
[bound - first]a
|
|
|
|
/**
|
|
* A finite sequence counting up from 'first' to 'last' by 'stride'.
|
|
* Note that 'last' will only be an element of the enumeration if
|
|
* 'stride' divides 'last - first' evenly.
|
|
*
|
|
* '[x .. y by n]' is syntactic sugar for 'fromToBy`{first=x,last=y,stride=n}'.
|
|
*/
|
|
primitive fromToBy : {first, last, stride, a}
|
|
(fin last, fin stride, stride >= 1, last >= first, Literal last a) =>
|
|
[1 + (last - first)/stride]a
|
|
|
|
/**
|
|
* A finite sequence counting from 'first' up to (but not including) 'bound'
|
|
* by 'stride'. Note that if 'first = bound' then the sequence will
|
|
* be empty. If 'bound = inf' then the sequence will be infinite, and will
|
|
* eventually wrap around for bounded types.
|
|
*
|
|
* '[x ..< y by n]' is syntactic sugar for 'fromToByLessThan`{first=x,bound=y,stride=n}'.
|
|
*/
|
|
primitive fromToByLessThan : {first, bound, stride, a}
|
|
(fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>
|
|
[(bound - first)/^stride]a
|
|
|
|
/**
|
|
* A finite sequence counting from 'first' down to 'last' by 'stride'.
|
|
* Note that 'last' will only be an element of the enumeration if
|
|
* 'stride' divides 'first - last' evenly.
|
|
*
|
|
* '[x .. y down by n]' is syntactic sugar for 'fromToDownBy`{first=x,last=y,stride=n}'.
|
|
*/
|
|
primitive fromToDownBy : {first, last, stride, a}
|
|
(fin first, fin stride, stride >= 1, first >= last, Literal first a) =>
|
|
[1 + (first - last)/stride]a
|
|
|
|
/**
|
|
* A finite sequence counting from 'first' down to (but not including)
|
|
* 'bound' by 'stride'.
|
|
*
|
|
* '[x ..> y down by n]' is syntactic sugar for
|
|
* 'fromToDownByGreaterThan`{first=x,bound=y,stride=n}'.
|
|
*
|
|
* Note that if 'first = bound' the sequence will be empty.
|
|
*/
|
|
primitive fromToDownByGreaterThan : {first, bound, stride, a}
|
|
(fin first, fin stride, stride >= 1, first >= bound, Literal first a) =>
|
|
[(first - bound)/^stride]a
|
|
|
|
/**
|
|
* A finite arithmetic sequence starting with 'first' and 'next',
|
|
* stopping when the values reach or would skip over 'last'.
|
|
*
|
|
* '[x,y..z]' is syntactic sugar for 'fromThenTo`{first=x,next=y,last=z}'.
|
|
*/
|
|
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 possessing 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]
|
|
|
|
/**
|
|
* Convert a signed 2's complement bitvector to an integer.
|
|
*/
|
|
primitive toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer
|
|
|
|
|
|
// 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'.
|
|
*/
|
|
splitAt : {front, back, a} (fin front) => [front + back]a
|
|
-> ([front]a, [back]a)
|
|
splitAt xs = (take`{front,back} xs, drop`{front,back} xs)
|
|
|
|
/**
|
|
* 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.
|
|
*/
|
|
primitive take : {front, back, a} [front + back]a -> [front]a
|
|
|
|
/**
|
|
* Select all the elements after (to the right of) the 'front' elements of a sequence.
|
|
*/
|
|
primitive drop : {front, back, a} (fin front) => [front + back]a -> [back]a
|
|
|
|
/**
|
|
* 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 = foldl upd xs0 (zip idxs vals)
|
|
where
|
|
upd xs (i,b) = update xs i b
|
|
|
|
/**
|
|
* 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 = foldl upd xs0 (zip idxs vals)
|
|
where
|
|
upd xs (i,b) = updateEnd xs i b
|
|
|
|
/**
|
|
* 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} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a
|
|
generate f = [ f i | i <- [0 .. <n] ]
|
|
|
|
|
|
/**
|
|
* Sort a sequence of elements. Equivalent to 'sortBy (<=)'.
|
|
*/
|
|
sort : {a, n} (Cmp a, fin n) => [n]a -> [n]a
|
|
sort = sortBy (<=)
|
|
|
|
/**
|
|
* Sort a sequence according to the given less-than-or-equal relation.
|
|
* The sorting is stable, so it preserves the relative position of any
|
|
* pair of elements that are equivalent according to the order relation.
|
|
*/
|
|
sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a
|
|
sortBy le ((xs : [n/2]a) # (ys : [n/^2]a)) = take zs.0
|
|
where
|
|
xs' = if `(n/2) == 1 then xs else sortBy le xs
|
|
ys' = if `(n/^2) == 1 then ys else sortBy le ys
|
|
zs = [ if i == `(n/2) then (ys'@j, i , j+1)
|
|
| j == `(n/^2) then (xs'@i, i+1, j )
|
|
| le (xs'@i) (ys'@j) then (xs'@i, i+1, j )
|
|
else (ys'@j, i , j+1)
|
|
| (_, i, j) <- [ (undefined, 0, 0) ] # zs
|
|
]
|
|
|
|
// 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 sequence, 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.
|
|
*/
|
|
primitive scanl : {n, a, b} (a -> b -> a) -> a -> [n]b -> [1+n]a
|
|
|
|
/**
|
|
* Scan right is like a foldr that also emits the intermediate values.
|
|
*/
|
|
scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1+n]b
|
|
scanr f acc xs = reverse (scanl (\a b -> f b a) acc (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 z = scanl (\x _ -> f x) z (zero:[inf]())
|