GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-17 18:00:52 +03:00
Code Issues Projects Releases Wiki Activity

Documentation updates (#779)

Browse Source 
* Add docstrings for all prelude functions and fix minor style issues.

Fixes #771

* Update `CryptolPrims` documentation

* Minor updates to the prelude

* Update CHANGES

* Updates to the cryptol book and CryptolPrims

* Fix several additional docstrings

* Specify and document properties of signed bitvector division.

Fixes #677

* Fixup test

* typos and style

* Regenerate PDFs
This commit is contained in:
robdockins 2020-06-30 10:58:25 -07:00 committed by GitHub
parent e291e8c827
commit 87d5edab00
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
15 changed files with 536 additions and 193 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
CHANGES.md
View File

@ -24,8 +24,9 @@
There is also a new `Round` class for types that can sensibly be
rounded to integers. This class has the methods `floor`, `ceiling`,
`trunc` and `round` for performing different kinds of
integer rounding. Currently `Rational` is the only meber of `Round`.
`trunc`, `roundToEven` and `roundAway` for performing different
kinds of integer rounding. Currently `Rational` is the only member
of `Round`.
The type of `(^^)` is modified to be
`{a, e} (Ring a, Integral e) => a -> e -> a`. This makes it clear
@ -35,6 +36,10 @@
Finally, the `lg2`, `(/$)` and `(%$)` methods of Arith have
had their types specialized so operate only on bitvectors.
* Added an `Eq` class, and moved the equality operations
from `Cmp` into `Eq`. The `Z` type becomes a member of `Eq`
but not `Cmp`.
* Added a base `Rational` type. It is implemented as a pair of
integers, quotiented in the usual way. As such, it reduces to the
theory of integers and requires no new solver support (beyond
@ -45,6 +50,10 @@
* The `generate` function (and thus `x @ i= e` definitions) has had
its type specialized so the index type is always `Integer`.
* The new typeclasses are arranged into a class hierarchy, and the
typechecker will use that information to infer superclass instances
from subclasses.
## New features
* Document the behavior of lifted selectors.
@ -57,10 +66,23 @@
* More detailed information about the status of various symbols
in the output of the `:browse` command (issue #688).
* The `:safe` command will attempt to prove that a given Cryptol
term is safe; in other words, that it will not encounter a run-time
error for all inputs. Run-time errors arise from things like
division-by-zero, index-out-of-bounds situations and
explicit calls to `error` or `assert`.
* The `:prove` and `:sat` commands now incorporate safety predicates
by default. In a `:sat` call, models will only be found that do not
cause run-time errors. For `:prove` calls, the safety conditions are
added as additional proof goals. The prior behavior
(which ignored safety conditions) can be restored using
`:set ignore-safety = on`.
## Bug fixes
* Closed issues #346, #444, #614, #617, #660, #662, #663, #664, #667, #670,
#711
* Closed issues #346, #444, #614, #617, #636, #660, #662, #663, #664, #667, #670,
#702, #711, #712, #716, #723, #725, #731
# 2.8.0 (September 4, 2019)

BIN
docs/Cryptol.pdf
View File

Binary file not shown.

359
docs/CryptolPrims.md
View File

@ -1,102 +1,59 @@
Comparisons and Ordering
------------------------
(==) : {a} (Cmp a) => a -> a -> Bit
(!=) : {a} (Cmp a) => a -> a -> Bit
(===) : {a,b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
(!==) : {a,b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
(<) : {a} (Cmp a) => a -> a -> Bit
(>) : {a} (Cmp a) => a -> a -> Bit
(<=) : {a} (Cmp a) => a -> a -> Bit
(>=) : {a} (Cmp a) => a -> a -> Bit
min : {a} (Cmp a) => a -> a -> a
max : {a} (Cmp a) => a -> a -> a
instance Cmp Bit
// No instance for functions.
instance (Cmp a, fin n) => Cmp [n]a
instance (Cmp a, Cmp b) => Cmp (a, b)
instance (Cmp a, Cmp b) => Cmp { x : a, y : b }
instance Cmp Integer
instance (fin n, n>=1) => Cmp (Z n)
instance Cmp Rational
Signed Comparisons
Typeclass Heriarchy
---------------------
(<$) : {a} (SignedCmp a) => a -> a -> Bit
(>$) : {a} (SignedCmp a) => a -> a -> Bit
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
Zero
/ \
Logic Ring Eq
/ \ / \
Integral Field Cmp SignedCmp
\ /
Round
This diagram describes how the various typeclasses in
Cryptol are related. A type which is an instance of a
subclass is also always a member of all of its superclasses.
For example, any type which is a member of `Field` is also
a member of `Ring` and `Zero`.
Literals
-----------------------
type Literal : # -> * -> Prop
number : {val, rep} Literal val rep => rep
length : {n, a, b} (fin n, Literal n b) => [n]a -> b
// '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'
fromTo : {first, last, a}
(fin last, last >= first,
Literal first a, Literal last a) =>
[1 + (last - first)]a
// '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'
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
// No instance for Bit
// No instance for functions.
instance (fin n, n >= 1) => SignedCmp [n]
instance (SignedCmp a, fin n) => SignedCmp [n]a
// (for [n]a, where a is other than Bit)
instance (SignedCmp a, SignedCmp b) => SignedCmp (a, b)
instance (SignedCmp a, SignedCmp b) => SignedCmp { x : a, y : b }
Zero
----
type Zero : * -> Prop
zero : {a} (Zero a) => a
Every base and structured type in Cryptol is a member of class `Zero`.
Arithmetic
----------
(+) : {a} (Ring a) => a -> a -> a
(-) : {a} (Ring a) => a -> a -> a
(*) : {a} (Ring a) => a -> a -> a
negate : {a} (Ring a) => a -> a
(/) : {a} (Integral a) => a -> a -> a
(%) : {a} (Integral a) => a -> a -> a
(/.) : {a} (Field a) => a -> a -> a
recip : {a} (Field a) => a -> a
floor : {a} (Round a) => a -> Integer
ceiling : {a} (Round a) => a -> Integer
trunc : {a} (Round a) => a -> Integer
round : {a} (Round a) => a -> Integer
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
(/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
(%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
lg2 : {n} (fin n) => [n] -> [n]
The prefix notation `- x` is syntactic sugar for `negate x`.
// No instance for `Bit`.
instance (fin n) => Ring ([n]Bit)
instance (Ring a) => Ring ([n]a)
instance (Ring b) => Ring (a -> b)
instance (Ring a, Ring b) => Ring (a, b)
instance (Ring a, Ring b) => Ring { x : a, y : b }
instance Ring Integer
instance (fin n, n>=1) => Ring (Z n)
instance Ring Rational
Note that because there is no instance for `Ring Bit`
the top two instances do not actually overlap.
instance Integral Integer
instance (fin n) => Integral ([n]Bit)
instance Field Rational
instance Round Rational
Boolean
-------
type Logic : * -> Prop
False : Bit
True : Bit
@ -104,6 +61,8 @@ Boolean
(||) : {a} (Logic a) => a -> a -> a
(^) : {a} (Logic a) => a -> a -> a
complement : {a} (Logic a) => a -> a
// The prefix notation '~ x' is syntactic
// sugar for 'complement x'.
(==>) : Bit -> Bit -> Bit
(/\) : Bit -> Bit -> Bit
@ -118,17 +77,174 @@ Boolean
// No instance for `Logic (Z n)`.
// No instance for `Logic Rational`.
Arithmetic
----------
type Ring : * -> Prop
fromInteger : {a} (Ring a) => Integer -> a
(+) : {a} (Ring a) => a -> a -> a
(-) : {a} (Ring a) => a -> a -> a
(*) : {a} (Ring a) => a -> a -> a
negate : {a} (Ring a) => a -> a
// The prefix notation `- x` is syntactic
// sugar for `negate x`.
type Integral : * -> Prop
(/) : {a} (Integral a) => a -> a -> a
(%) : {a} (Integral a) => a -> a -> a
toInteger : {a} (Integral a) => a -> Integer
infFrom : {a} (Integral a) => a -> [inf]a
// '[x...]' is syntactic sugar for 'infFrom x'
infFromThen : {a} (Integral a) => a -> a -> [inf]a
// [x,y...]' is syntactic sugar for 'infFromThen x y'
type Field : * -> Prop
(/.) : {a} (Field a) => a -> a -> a
recip : {a} (Field a) => a -> a
type Round : * -> Prop
floor : {a} (Round a) => a -> Integer
ceiling : {a} (Round a) => a -> Integer
trunc : {a} (Round a) => a -> Integer
roundAway : {a} (Round a) => a -> Integer
roundToEven : {a} (Round a) => a -> Integer
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
// No instance for `Bit`.
instance (fin n) => Ring ([n]Bit)
instance (Ring a) => Ring ([n]a)
instance (Ring b) => Ring (a -> b)
instance (Ring a, Ring b) => Ring (a, b)
instance (Ring a, Ring b) => Ring { x : a, y : b }
instance Ring Integer
instance (fin n, n>=1) => Ring (Z n)
instance Ring Rational
Note that because there is no instance for `Ring Bit`
the top two instances do not actually overlap.
instance Integral Integer
instance (fin n) => Integral ([n]Bit)
instance Field Rational
instance Round Rational
Equality Comparisons
------------------------
type Eq : * -> Prop
(==) : {a} (Eq a) => a -> a -> Bit
(!=) : {a} (Eq a) => a -> a -> Bit
(===) : {a,b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit
(!==) : {a,b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit
instance Eq Bit
instance (Eq a, fin n) => Eq [n]a
instance (Eq a, Eq b) => Eq (a, b)
instance (Eq a, Eq b) => Eq { x : a, y : b }
instance Eq Integer
instance Eq Rational
instance (fin n, n>=1) => Eq (Z n)
// No instance for functions.
Comparisons and Ordering
------------------------
type Cmp : * -> Prop
(<) : {a} (Cmp a) => a -> a -> Bit
(>) : {a} (Cmp a) => a -> a -> Bit
(<=) : {a} (Cmp a) => a -> a -> Bit
(>=) : {a} (Cmp a) => a -> a -> Bit
min : {a} (Cmp a) => a -> a -> a
max : {a} (Cmp a) => a -> a -> a
abs : {a} (Cmp a, Ring a) => a -> a
instance Cmp Bit
instance (Cmp a, fin n) => Cmp [n]a
instance (Cmp a, Cmp b) => Cmp (a, b)
instance (Cmp a, Cmp b) => Cmp { x : a, y : b }
instance Cmp Integer
instance Cmp Rational
// No instance for functions.
Signed Comparisons
---------------------
type SignedCmp : * -> Prop
(<$) : {a} (SignedCmp a) => a -> a -> Bit
(>$) : {a} (SignedCmp a) => a -> a -> Bit
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
// No instance for Bit
instance (fin n, n >= 1) => SignedCmp [n]
instance (SignedCmp a, fin n) => SignedCmp [n]a
// (for [n]a, where a is other than Bit)
instance (SignedCmp a, SignedCmp b) => SignedCmp (a, b)
instance (SignedCmp a, SignedCmp b) => SignedCmp { x : a, y : b }
// No instance for functions.
Bitvectors
-----------
(/$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
(%$) : {n} (fin n, n >= 1) => [n] -> [n] -> [n]
carry : {n} (fin n) => [n] -> [n] -> Bit
scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
zext : {m, n} (fin m, m >= n) => [n] -> [m]
sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
lg2 : {n} (fin n) => [n] -> [n]
// Arithmetic shift only for bitvectors
(>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
Rationals
---------
ratio : Integer -> Integer -> Rational
Z(n)
-----
fromZ : {n} (fin n, n >= 1) => Z n -> Integer
Sequences
---------
join : {parts,each,a} (fin each) => [parts][each]a -> [parts * each]a
split : {parts,each,a} (fin each) => [parts * each]a -> [parts][each]a
join : {parts,each,a} (fin each) => [parts][each]a -> [parts * each]a
split : {parts,each,a} (fin each) => [parts * each]a -> [parts][each]a
(#) : {front,back,a} (fin front) => [front]a -> [back]a -> [front + back]a
splitAt : {front,back,a} (fin front) => [from + back] a -> ([front] a, [back] a)
(#) : {front,back,a} (fin front) => [front]a -> [back]a -> [front + back]a
splitAt : {front,back,a} (fin front) => [from + back] a -> ([front] a, [back] a)
reverse : {n,a} (fin n) => [n]a -> [n]a
transpose : {n,m,a} [n][m]a -> [m][n]a
reverse : {n,a} (fin n) => [n]a -> [n]a
transpose : {n,m,a} [n][m]a -> [m][n]a
(@) : {n,a,ix} (Integral ix) => [n]a -> ix -> a
(@@) : {n,k,ix,a} (Integral ix) => [n]a -> [k]ix -> [k]a
@ -145,6 +261,10 @@ Sequences
tail : {a, b} [1 + a]b -> [a]b
last : {a, b} [1 + a]b -> b
// Declarations of the form 'x @ i = e' are syntactic
// sugar for 'x = generate (\i -> e)'.
generate : {n, a} (fin n, n >= 1) => (Integer -> a) -> [n]a
groupBy : {each,parts,elem} (fin each) => [parts * each]elem -> [parts][each]elem
Function `groupBy` is the same as `split` but with its type arguments
@ -153,23 +273,60 @@ in a different order.
Shift And Rotate
----------------
(<<) : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
(>>) : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
(<<<) : {n,ix,a} (fin n, Integral ix) => [n]a -> ix -> [n]a
(>>>) : {n,ix,a} (fin n, Integral ix) => [n]a -> ix -> [n]a
(<<) : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
(>>) : {n,ix,a} (Integral ix, Zero a) => [n]a -> ix -> [n]a
(<<<) : {n,ix,a} (fin n, Integral ix) => [n]a -> ix -> [n]a
(>>>) : {n,ix,a} (fin n, Integral ix) => [n]a -> ix -> [n]a
GF(2) polynomials
-----------------
pmult : {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + u + v]
pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
// Arithmetic shift only for bitvectors
(>>$) : {n,ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
Random Values
-------------
random : {a} => [256] -> a
random : {a} => [256] -> a
Errors and Assertions
---------------------
undefined : {a} a
error : {a,n} (fin n) => String n -> a
assert : {a,n} (fin n) => Bit -> String n -> a -> a
Debugging
---------
undefined : {a} a
error : {n a} [n][8] -> a
trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
traceVal : {n, a} (fin n) => [n][8] -> a -> a
trace : {n, a, b} (fin n) => String n -> a -> b -> b
traceVal : {n, a} (fin n) => String n -> a -> a
Utility operations
------------------
and : {n} (fin n) => [n]Bit -> Bit
or : {n} (fin n) => [n]Bit -> Bit
all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit
map : {n, a, b} (a -> b) -> [n]a -> [n]b
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [n+1]b
scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
sum : {n, a} (fin n, Ring a) => [n]a -> a
iterate : {a} (a -> a) -> a -> [inf]a
repeat : {n, a} a -> [n]a
zip : {n, a, b} [n]a -> [n]b -> [n](a, b)
zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c
uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c
curry : {a, b, c} ((a, b) -> c) -> a -> b -> c

BIN
docs/CryptolPrims.pdf
View File

Binary file not shown.

BIN
docs/ProgrammingCryptol.pdf
View File

Binary file not shown.

31
docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
View File

@ -2667,10 +2667,11 @@ automatically, to get the answers:
\begin{Exercise}\label{ex:recfun:4:1}
Define a function {\tt elem} with the following signature:\indElem
\begin{code}
elem : {n, t} (fin n, Cmp t) => (t, [n]t) -> Bit
elem : {n, t} (fin n, Eq t) => (t, [n]t) -> Bit
\end{code}
such that {\tt elem (x, xs)} returns {\tt True} if {\tt x} appears in
{\tt xs}, and {\tt False} otherwise.
{\tt xs}, and {\tt False} otherwise.\footnote{Note: this function
is already present in the Cryptol prelude.}
\end{Exercise}
\begin{Answer}\ansref{ex:recfun:4:1}
Using a fold, it is easy to write {\tt elem}:
@ -2922,7 +2923,7 @@ Type classes are a way of describing behaviors shared by multiple
types. As an example, consider the type of the function {\tt ==}:
\begin{Verbatim}
Cryptol> :t (==)
(==) : {a} (Cmp a) => a -> a -> Bit
(==) : {a} (Eq a) => a -> a -> Bit
\end{Verbatim}
This type signature may be read as, ``equality is an operator that
@ -2930,7 +2931,7 @@ takes two objects of any single type that can be compared and returns
a Bit.''
Cryptol defines a collection of basic type classes: \texttt{Logic},
\texttt{Zero}, \texttt{Cmp}, \texttt{SignedCmp}, \texttt{Ring},
\texttt{Zero}, \texttt{Eq}, \texttt{Cmp}, \texttt{SignedCmp}, \texttt{Ring},
\texttt{Integral}, \texttt{Field}, \texttt{Round}, and
\texttt{Literal}. These appear in the type signature of operators and
functions that require them. If a function you define calls, for
@ -2952,15 +2953,17 @@ All of the built-in types of Cryptol are instances of class
\texttt{Zero}.
\item
The \texttt{Cmp} typeclass includes the binary relation operators
\texttt{<}, \texttt{>}, \texttt{<=}, \texttt{>=}, \texttt{==}, and
\texttt{!=}, as well as the binary functions \texttt{min} and
\texttt{max}. Note that equality and other comparisons are bundled
into a single typeclass. Function types are not in class \texttt{Cmp}
The \texttt{Eq} typeclass includes the equality testing operations
\texttt{==} and \texttt{!=}. Function types are not in class \texttt{Eq}
and cannot be compared with \texttt{==}, but Cryptol does provide a
special pointwise comparison operator for functions, \texttt{(===) :
\{a b\} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit}.
\item
The \texttt{Cmp} typeclass includes the binary relation operators
\texttt{<}, \texttt{>}, \texttt{<=}, \texttt{>=}, as well as the
binary functions \texttt{min} and \texttt{max}.
\item
The \texttt{SignedCmp} typeclass includes the binary relation
operators \texttt{<\$}, \texttt{>\$}, \texttt{<=\$}, and
@ -2996,9 +2999,9 @@ Currently, only type \texttt{Rational} is a member of this class.
\item
The \texttt{Round} typeclass contains types that can be
rounded to integers. It includes \texttt{floor}, \texttt{ceiling},
\texttt{trunc} and \texttt{round} operations, which are all different
ways of rounding values to integers.
Currently, only type \texttt{Rational} is a member of this class.
\texttt{trunc}, \texttt{roundAway} and \texttt{roundToEven}
operations, which are all different ways of rounding values to
integers. Currently, only type \texttt{Rational} is a member of this class.
\item
The \texttt{Literal} typeclass includes numeric literals.
@ -3008,7 +3011,7 @@ The \texttt{Literal} typeclass includes numeric literals.
Without including an explicit type declaration, define a function
that Cryptol infers has the following type:
\begin{Verbatim}
cmpRing : {a,b} (Cmp a, Ring b) => a -> a -> b -> b
cmpRing : {a,b} (Eq a, Ring b) => a -> a -> b -> b
\end{Verbatim}
\end{Exercise}
\begin{Answer}\ansref{ex:tvar:1}
@ -3018,7 +3021,7 @@ This code:
\end{code}
yields the inferred type:
\begin{Verbatim}
cmpRing : {a, b} (Cmp a, Ring b) => a -> a -> b -> b
cmpRing : {a, b} (Eq a, Ring b) => a -> a -> b -> b
\end{Verbatim}
\end{Answer}

2
docs/ProgrammingCryptol/highAssurance/HighAssurance.tex
View File

@ -213,7 +213,7 @@ a different value: a property we might expect to hold
intuitively. Here is the type of {\tt flipNeverIdentity}:
\begin{Verbatim}
Cryptol> :t flipNeverIdentity
flipNeverIdentity : {a} (Cmp a, Logic a) => a -> Bit
flipNeverIdentity : {a} (Eq a, Logic a) => a -> Bit
\end{Verbatim}
So, the only requirement on \texttt{flipNeverIdentity} is that it
receives some type that supports comparisons and logical operations.

13
docs/ProgrammingCryptol/prims/Primitives.tex
View File

@ -15,11 +15,11 @@ primsPlaceHolder=1;
\end{Verbatim}
\paragraph*{Comparisons}
\begin{Verbatim}
==, != : {a} (Cmp a) => a -> a -> Bit
==, != : {a} (Eq a) => a -> a -> Bit
<, >, <=, >= : {a} (Cmp a) => a -> a -> Bit
<$, >$, <=$, >=$ : {a} (SignedCmp a) => a -> a -> Bit
min, max : {a} (Cmp a) => a -> a -> a
===, !== : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
===, !== : {a, b} (Eq b) => (a -> b) -> (a -> b) -> a -> Bit
\end{Verbatim}
\paragraph*{Arithmetic}
\begin{Verbatim}
@ -42,9 +42,10 @@ primsPlaceHolder=1;
floor : {a} (Round a) => a -> Integer
ceiling : {a} (Round a) => a -> Integer
trunc : {a} (Round a) => a -> Integer
round : {a} (Round a) => a -> Integer
roundAway : {a} (Round a) => a -> Integer
roundToEven : {a} (Round a) => a -> Integer
\end{Verbatim}
\paragraph*{Polynomial arithmetic}
\paragraph*{GF(2) polynomial arithmetic}
\begin{Verbatim}
pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
@ -97,6 +98,7 @@ primsPlaceHolder=1;
all, any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c
elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit
\end{Verbatim}
\paragraph*{Miscellaneous}
\begin{Verbatim}
@ -105,8 +107,9 @@ primsPlaceHolder=1;
\end{Verbatim}
\paragraph*{Representing exceptions}
\begin{Verbatim}
error : {a, len} (fin len) => [len][8] -> a
undefined : {a} a
error : {a, n} (fin n) => String n -> a
assert : {a, n} (fin n) => Bit -> String n -> a -> a
trace : {n, a, b} [n][8] -> a -> b -> b
traceVal : {n, a} [n][8] -> a -> a
\end{Verbatim}

32
docs/ProgrammingCryptol/technicalities/TechAppendix.tex
View File

@ -130,7 +130,7 @@ type of an infix operator (e.g., {\tt +}, {\tt ==}, etc.) you will need
to surround the operator with {\tt ()}, like this:
\begin{Verbatim}
Cryptol> :t (+)
(+) : {a} (Arith a) => a -> a -> a
(+) : {a} (Ring a) => a -> a -> a
\end{Verbatim}
\paragraph*{Browsing definitions}
@ -158,14 +158,15 @@ have defined, along with their types.
\hline
\textbf{Option} & \textbf{Default value} & \textbf{Meaning} \\
\hline
\texttt{ascii} & \texttt{off} & print sequences of bytes as a string \\
\texttt{ascii} & \texttt{off} & print sequences of bytes as a string \\
\texttt{base} & \texttt{16} & numeric base for printing words \\
\texttt{debug} & \texttt{off} & whether to print verbose debugging information \\
\texttt{ignore-safety} & \texttt{off} & ignore safety predicates when performing \texttt{:sat} or \texttt{:prove} checks \\
\texttt{infLength} & \texttt{5} & number of elements to show from an infinite sequence \\
\texttt{prover} & \texttt{z3} & which SMT solver to use for \texttt{:prove} \\
\texttt{satNum} & \texttt{1} & maximum number of solutions to show for \texttt{:sat} \\
\texttt{show-examples} & \texttt{on} & whether to print counterexamples and models \\
\texttt{smtfile} & \texttt{-} & file to write SMT problems when \texttt{prover = offline} \\
\texttt{tests} & \texttt{100} & number of tests to run for \texttt{:check} \\
\texttt{warnDefaulting} & \texttt{on} & \todo[inline]{talk to Iavor} \\
\hline
\end{tabular*}
\label{tab:set_options}
@ -173,8 +174,9 @@ have defined, along with their types.
\paragraph*{Environment options}
A variety of environment options are set through the use of the
\texttt{:set} command. These options may change over time and some
options may be available only on specific platforms. The current
options are summarized in~\autoref{tab:set_options}.
options may be available only on specific platforms. The most useful
configuration options are summarized in~\autoref{tab:set_options}.
Help information about all flags can found by typing {\tt :help :set flag}.
\todo[inline]{Ensure index references exist for all commands.}
@ -220,7 +222,7 @@ At the Cryptol prompt you can load a module by name with the {\tt
:module} command.\indCmdLoadModule
\paragraph*{}
The next three commands all operate on \emph{properties}. All take
The next commands all operate on \emph{properties}. All take
either one or zero arguments. If one argument is provided, then that
property is the focus of the command; otherwise all properties in the
current context are checked. All three commands are covered in detail
@ -231,16 +233,30 @@ The \texttt{:check} command performs random value testing on a
property to increase one's confidence that the property is valid.
See~\autoref{sec:quickcheck} for more detailed information.
\paragraph*{Checking a property through exhaustive testing}
The \texttt{:exhaust} command enumerates all the possible input values
of a property to test that it is correct for every possible value.
This is infeasible except for properties with quite small input
domains!
\paragraph*{Verifying a property through automated theorem proving}
The \texttt{:prove} command uses an external SMT solver to attempt to
automatically formally prove that a given property is valid.
See~\autoref{sec:formal-proofs} for more detailed information.
\paragraph*{Finding a satisfying assignment for a property}
The \texttt{:sat} command uses an external SAT solver to attempt to
The \texttt{:sat} command uses an external SMT solver to attempt to
find a satisfying assignment to a property. See~\autoref{sec:sat} for
more detailed information.
\paragraph*{Proving that a property is safe}
The \texttt{:safe} command uses an external SMT solver to attempt to
prove that the given term is safe for all inputs, which means it cannot
encounter a run-time error. Unlike the other commands in this section,
\texttt{:safe} \emph{must} be given an argument and can be called on
values that compute types other than \texttt{Bit}. Most types, except
infinite streams and functions, are allowed in the result type.
% \paragraph*{Type specialization}
% Discuss \texttt{:debug\_specialize}. \todo[inline]{Dylan?}

BIN
docs/Semantics.pdf
View File

Binary file not shown.

153
lib/Cryptol.cry
View File

@ -1,5 +1,5 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Copyright (c) 2013-2020 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
@ -29,31 +29,33 @@ 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.
*/
/**
* '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.
*/
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.
*/
/**
* '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
@ -255,13 +257,20 @@ primitive complement : {a} (Logic a) => a -> a
// The Ring class -------------------------------------------------------
/** Value types that support ring addition and multiplication. */
/**
* 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 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
@ -302,10 +311,11 @@ 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.
*/
/**
* 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
/**
@ -332,8 +342,8 @@ 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`.
* * 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
@ -352,21 +362,22 @@ 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.
*/
/**
* 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 zero is undefined.
*/
* Reciprocal
*
* Compute the multiplicative inverse of an element of a field.
* The reciprocal of 0 is undefined.
*/
primitive recip : {a} (Field a) => a -> a
/**
@ -581,11 +592,19 @@ a ==> b = if a then b else True
/**
* 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]
@ -640,7 +659,7 @@ primitive (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
* Log base two.
*
* For words, computes the ceiling of log, base 2, of a number.
* We set `lg2 0 = 0`
* We set 'lg2 0 = 0'
*/
primitive lg2 : {n} (fin n) => [n] -> [n]
@ -649,7 +668,9 @@ primitive lg2 : {n} (fin n) => [n] -> [n]
/**
* Compute the ratio of two integers as a rational.
* ratio x y = (fromInteger x /. fromInteger y) : Rational
* Ratio is undefined if the denominator is 0.
*
* 'ratio x y = (fromInteger x /. fromInteger y) : Rational'
*/
primitive ratio : Integer -> Integer -> Rational
@ -704,17 +725,26 @@ primitive reverse : {n, a} (fin n) => [n]a -> [n]a
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 left-most element of a sequence.
* Return the first (left-most) element of a sequence.
*/
head : {n, a} [1 + n]a -> a
head xs = xs @ 0
@ -725,13 +755,18 @@ head xs = xs @ 0
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
/**
@ -890,19 +925,27 @@ pmod x y = if y == 0 then 0/0 else last zs
// Utility operations -----------------------------------------------------------------
primitive error : {a, len} (fin len) => String len -> a
/**
* 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.
* with the given message if it does not. If the condition
* holds, return the third argument unchanged.
*/
assert : {a, len} (fin len) => Bit -> String len -> a -> a
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.
@ -920,7 +963,7 @@ primitive random : {a} [256] -> a
* which are unspecified. Thus, the output produced by this
* operation may be difficult to predict.
*/
primitive trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
primitive trace : {n, a, b} (fin n) => String n -> a -> b -> b
/**
* Debugging function for tracing values. The first argument is a string,
@ -933,7 +976,7 @@ primitive trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
* which are unspecified. Thus, the output produced by this
* operation may be difficult to predict.
*/
traceVal : {n, a} (fin n) => [n][8] -> a -> a
traceVal : {n, a} (fin n) => String n -> a -> a
traceVal msg x = trace msg x x
@ -1016,7 +1059,7 @@ repeat x = [ x | _ <- zero : [n] ]
/**
* '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 : {n, a} (fin n, Eq a) => a -> [n]a -> Bit
elem a xs = any (\x -> x == a) xs
/**

10
tests/issues/issue226.icry.stdout
View File

@ -117,15 +117,15 @@ Symbols
all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
and : {n} (fin n) => [n] -> Bit
any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
assert : {a, len} (fin len) => Bit -> String len -> a -> a
assert : {a, n} (fin n) => Bit -> String n -> a -> a
carry : {n} (fin n) => [n] -> [n] -> Bit
ceiling : {a} (Round a) => a -> Integer
complement : {a} (Logic a) => a -> a
curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
demote : {val, rep} (Literal val rep) => rep
drop : {front, back, a} (fin front) => [front + back]a -> [back]a
elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
error : {a, len} (fin len) => String len -> a
elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit
error : {a, n} (fin n) => String n -> a
False : Bit
floor : {a} (Round a) => a -> Integer
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
@ -186,8 +186,8 @@ Symbols
tail : {n, a} [1 + n]a -> [n]a
take : {front, back, a} (fin front) => [front + back]a -> [front]a
toInteger : {a} (Integral a) => a -> Integer
trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
traceVal : {n, a} (fin n) => [n][8] -> a -> a
trace : {n, a, b} (fin n) => String n -> a -> b -> b
traceVal : {n, a} (fin n) => String n -> a -> a
transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
trunc : {a} (Round a) => a -> Integer
uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c

70
tests/regression/bvdiv.cry Normal file
View File

@ -0,0 +1,70 @@
// unsigned division properties
bvdiv_euc : {n} (fin n) => [n] -> [n] -> Bit
bvdiv_euc x y = y != 0 ==> (x/y)*y + x%y == x
bvdiv_char : {n} (fin n) => [n] -> [n] -> Bit
bvdiv_char x y = y != 0 ==> floor r == toInteger (x / y)
where
r = ratio (toInteger x) (toInteger y)
bvdiv_mod : {n} (fin n) => [n] -> [n] -> Bit
bvdiv_mod x y = y != 0 ==> (0 <= m /\ m < y)
where
m = x%y
// some utility definitions
sabs : {n} (fin n, n>=1) => [n] -> [n]
sabs x = if x <=$ 0 then negate x else x
toSignedInteger : {n} (fin n, n >=1 ) => [n] -> Integer
toSignedInteger x = if x <=$ 0 then negate (toInteger (negate x)) else toInteger x
minint : {n} (fin n, n >= 1) => [n]
minint = 0b1 # zero
maxint : {n} (fin n, n >= 1) => [n]
maxint = ~minint
// signed division properties
bvsdiv_euc : {n} (fin n, n>=1) => [n] -> [n] -> Bit
bvsdiv_euc x y = y != 0 ==> (x/$y)*y + x%$y == x
bvsdiv_char : {n} (fin n, n>=1) => [n] -> [n] -> Bit
bvsdiv_char x y = y != 0 ==> overflow \/ trunc r == toSignedInteger (x /$ y)
where
overflow = x == minint /\ y == (-1)
r = ratio (toSignedInteger x) (toSignedInteger y)
bvsdiv_mod : {n} (fin n, n>=1) => [n] -> [n] -> Bit
bvsdiv_mod x y = y != 0 ==> (0 <= m /\ m < sabs y)
where
m = sabs (x%$y)
bvsdiv_mod_sign : {n} (fin n, n>=1) => [n] -> [n] -> Bit
bvsdiv_mod_sign x y =
y != 0 ==>
if x >=$ 0 then x%$y >=$ 0 else x%$y <=$ 0
bvsdiv_doc_properties : {n} (fin n, n>=1) => [n] -> [n] -> Bit
bvsdiv_doc_properties x y =
y != 0 ==>
(x %$ y == x - (x /$ y) * y) /\
(x >=$ 0 ==> x%$y >=$ 0) /\
(x <=$ 0 ==> x%$y <=$ 0)
// property instances to check
property d1 = bvdiv_euc`{8}
property c1 = bvdiv_char`{8}
property m1 = bvdiv_mod`{8}
property d2 = bvsdiv_euc`{8}
property c2 = bvsdiv_char`{8}
property m2 = bvsdiv_mod`{8}
property m3 = bvsdiv_mod_sign`{8}
property sdiv = bvsdiv_doc_properties`{8}

2
tests/regression/bvdiv.icry Normal file
View File

@ -0,0 +1,2 @@
:l bvdiv.cry
:exhaust

27
tests/regression/bvdiv.icry.stdout Normal file
View File

@ -0,0 +1,27 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
property d1 Using exhaustive testing.
Testing... Passed 65536 tests.
Q.E.D.
property c1 Using exhaustive testing.
Testing... Passed 65536 tests.
Q.E.D.
property m1 Using exhaustive testing.
Testing... Passed 65536 tests.
Q.E.D.
property d2 Using exhaustive testing.
Testing... Passed 65536 tests.
Q.E.D.
property c2 Using exhaustive testing.
Testing... Passed 65536 tests.
Q.E.D.
property m2 Using exhaustive testing.
Testing... Passed 65536 tests.
Q.E.D.
property m3 Using exhaustive testing.
Testing... Passed 65536 tests.
Q.E.D.
property sdiv Using exhaustive testing.
Testing... Passed 65536 tests.
Q.E.D.