mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
Update documentation and reference interpreter
This commit is contained in:
parent
a1cf62e81d
commit
9822d5fd9a
@ -36,7 +36,7 @@ Literals
|
|||||||
, Literal first a, Literal next a, Literal last a
|
, Literal first a, Literal next a, Literal last a
|
||||||
, first != next
|
, first != next
|
||||||
, lengthFromThenTo first next last == len) =>
|
, lengthFromThenTo first next last == len) =>
|
||||||
[len]a
|
[len]a
|
||||||
|
|
||||||
Fractional Literals
|
Fractional Literals
|
||||||
-------------------
|
-------------------
|
||||||
@ -143,6 +143,7 @@ Arithmetic
|
|||||||
instance Ring Integer
|
instance Ring Integer
|
||||||
instance (fin n, n>=1) => Ring (Z n)
|
instance (fin n, n>=1) => Ring (Z n)
|
||||||
instance Ring Rational
|
instance Ring Rational
|
||||||
|
instance (ValidFloat e p) => Ring (Float e p)
|
||||||
|
|
||||||
Note that because there is no instance for `Ring Bit`
|
Note that because there is no instance for `Ring Bit`
|
||||||
the top two instances do not actually overlap.
|
the top two instances do not actually overlap.
|
||||||
@ -151,8 +152,11 @@ the top two instances do not actually overlap.
|
|||||||
instance (fin n) => Integral ([n]Bit)
|
instance (fin n) => Integral ([n]Bit)
|
||||||
|
|
||||||
instance Field Rational
|
instance Field Rational
|
||||||
|
instance (prime p) => Field (Z p)
|
||||||
|
instance (ValidFloat e p) => Field (Float e p)
|
||||||
|
|
||||||
instance Round Rational
|
instance Round Rational
|
||||||
|
instance (ValidFloat e p) => Round (Float e p)
|
||||||
|
|
||||||
|
|
||||||
Equality Comparisons
|
Equality Comparisons
|
||||||
@ -169,8 +173,8 @@ Equality Comparisons
|
|||||||
instance (Eq a, fin n) => Eq [n]a
|
instance (Eq a, fin n) => Eq [n]a
|
||||||
instance (Eq a, Eq b) => Eq (a, b)
|
instance (Eq a, Eq b) => Eq (a, b)
|
||||||
instance (Eq a, Eq b) => Eq { x : a, y : b }
|
instance (Eq a, Eq b) => Eq { x : a, y : b }
|
||||||
instance Eq Integer
|
instance Eq Integer
|
||||||
instance Eq Rational
|
instance Eq Rational
|
||||||
instance (fin n, n>=1) => Eq (Z n)
|
instance (fin n, n>=1) => Eq (Z n)
|
||||||
// No instance for functions.
|
// No instance for functions.
|
||||||
|
|
||||||
@ -311,16 +315,16 @@ Random Values
|
|||||||
Errors and Assertions
|
Errors and Assertions
|
||||||
---------------------
|
---------------------
|
||||||
|
|
||||||
undefined : {a} a
|
undefined : {a} a
|
||||||
error : {a,n} (fin n) => String n -> a
|
error : {a,n} (fin n) => String n -> a
|
||||||
assert : {a,n} (fin n) => Bit -> String n -> a -> a
|
assert : {a,n} (fin n) => Bit -> String n -> a -> a
|
||||||
|
|
||||||
|
|
||||||
Debugging
|
Debugging
|
||||||
---------
|
---------
|
||||||
|
|
||||||
trace : {n, a, b} (fin n) => String n -> a -> b -> b
|
trace : {n, a, b} (fin n) => String n -> a -> b -> b
|
||||||
traceVal : {n, a} (fin n) => String n -> a -> a
|
traceVal : {n, a} (fin n) => String n -> a -> a
|
||||||
|
|
||||||
|
|
||||||
Utility operations
|
Utility operations
|
||||||
@ -332,12 +336,18 @@ Utility operations
|
|||||||
any : {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
|
elem : {n, a} (fin n, Eq a) => a -> [n]a -> Bit
|
||||||
|
|
||||||
map : {n, a, b} (a -> b) -> [n]a -> [n]b
|
deepseq : {a, b} Eq a => a -> b -> b
|
||||||
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
|
rnf : {a} Eq a => a -> 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
|
map : {n, a, b} (a -> b) -> [n]a -> [n]b
|
||||||
scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
|
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
|
||||||
sum : {n, a} (fin n, Ring a) => [n]a -> a
|
foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a
|
||||||
|
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
|
||||||
|
foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a
|
||||||
|
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, Eq a, Ring a) => [n]a -> a
|
||||||
|
product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
|
||||||
|
|
||||||
iterate : {a} (a -> a) -> a -> [inf]a
|
iterate : {a} (a -> a) -> a -> [inf]a
|
||||||
repeat : {n, a} a -> [n]a
|
repeat : {n, a} a -> [n]a
|
||||||
|
Binary file not shown.
Binary file not shown.
@ -237,6 +237,7 @@ is 17. The final result is also due to wraparound: \texttt{- 0x5}
|
|||||||
evaluates to \texttt{0xb} or 11, which is $-5 + 16$.
|
evaluates to \texttt{0xb} or 11, which is $-5 + 16$.
|
||||||
\end{Answer}
|
\end{Answer}
|
||||||
|
|
||||||
|
\paragraph*{Bounded integers}
|
||||||
In addition to the unbounded \texttt{Integer} type, there are also a
|
In addition to the unbounded \texttt{Integer} type, there are also a
|
||||||
collection of bounded integer types: \texttt{Z n} for each finite
|
collection of bounded integer types: \texttt{Z n} for each finite
|
||||||
positive \texttt{n}. \texttt{Z n} represents the ring of integers modulo \texttt{n}.
|
positive \texttt{n}. \texttt{Z n} represents the ring of integers modulo \texttt{n}.
|
||||||
@ -258,6 +259,44 @@ Here are Cryptol's responses:
|
|||||||
\end{Verbatim}
|
\end{Verbatim}
|
||||||
\end{Answer}
|
\end{Answer}
|
||||||
|
|
||||||
|
\paragraph*{Prime moduli}
|
||||||
|
It is a consequence of Fermat's little theorem that when \texttt{p} is
|
||||||
|
a prime number, every nonzero value of \texttt{Z p} has a
|
||||||
|
multiplicitive inverse. In other words, for every \texttt{x : Z p}
|
||||||
|
where \texttt{x != 0} there is some other value
|
||||||
|
\texttt{y : Z p} where \texttt{x*y == 1}. We can use this fact to
|
||||||
|
implement the \texttt{Field} operations for \texttt{Z p}.
|
||||||
|
The type \texttt{Z p} is also known as the
|
||||||
|
``prime field of characteristic \texttt{p}'' when \texttt{p} is prime.
|
||||||
|
|
||||||
|
\begin{Exercise}\label{ex:int:3}
|
||||||
|
What are the results of evalauting the following expressions?
|
||||||
|
\begin{Verbatim}
|
||||||
|
recip 5 : Z 7
|
||||||
|
1 /. 3 : Z 7
|
||||||
|
(recip 5) * 5 : Z 7
|
||||||
|
recip 0 : Z 7
|
||||||
|
recip (3+4) : Z 7
|
||||||
|
(recip 5) * 5 : Z 8
|
||||||
|
\end{Verbatim}
|
||||||
|
\end{Exercise}
|
||||||
|
\begin{Answer}\ansref{ex:int:3}
|
||||||
|
Here are Cryptol's responses:
|
||||||
|
\begin{Verbatim}
|
||||||
|
3
|
||||||
|
5
|
||||||
|
1
|
||||||
|
division by 0
|
||||||
|
division by 0
|
||||||
|
Unsolvable constraints:
|
||||||
|
* prime 8
|
||||||
|
arising from
|
||||||
|
use of expression (/.)
|
||||||
|
at <interactive>:1:2--1:8
|
||||||
|
* Reason: 8 is not a prime number
|
||||||
|
\end{Verbatim}
|
||||||
|
\end{Answer}
|
||||||
|
|
||||||
%=====================================================================
|
%=====================================================================
|
||||||
\section{Rationals}
|
\section{Rationals}
|
||||||
\label{sec:rational}
|
\label{sec:rational}
|
||||||
@ -269,7 +308,8 @@ the \texttt{ratio} function, which accepts the numerator and denominator
|
|||||||
as integer values, or you can create a rational value from an
|
as integer values, or you can create a rational value from an
|
||||||
integer using the \texttt{fromInteger} function. Rational values can
|
integer using the \texttt{fromInteger} function. Rational values can
|
||||||
also be created directly from literals the same way as for
|
also be created directly from literals the same way as for
|
||||||
\texttt{Integer}.
|
\texttt{Integer}, or from fractional literals, which can be written
|
||||||
|
in decimal, hex and binary forms, as well as using scientific notation.
|
||||||
|
|
||||||
For example, all of the following expression create the same
|
For example, all of the following expression create the same
|
||||||
value representing one half:
|
value representing one half:
|
||||||
@ -279,6 +319,11 @@ value representing one half:
|
|||||||
(1 /. 2) : Rational
|
(1 /. 2) : Rational
|
||||||
(recip 2) : Rational
|
(recip 2) : Rational
|
||||||
(fromInteger (-1) /. fromInteger (-2)) : Rational
|
(fromInteger (-1) /. fromInteger (-2)) : Rational
|
||||||
|
0.5 : Rational
|
||||||
|
0x0.8 : Rational
|
||||||
|
0b0.1 : Rational
|
||||||
|
50.0e-2 : Rational
|
||||||
|
0x8.0p-4 : Rational
|
||||||
\end{Verbatim}
|
\end{Verbatim}
|
||||||
|
|
||||||
Note, the division operation on \texttt{Rational} is
|
Note, the division operation on \texttt{Rational} is
|
||||||
@ -298,10 +343,10 @@ module called \texttt{Float} so to use it you'd need to either import
|
|||||||
it in you Cryptol specification or use \texttt{:m Float} on the
|
it in you Cryptol specification or use \texttt{:m Float} on the
|
||||||
Cryptol REPL.
|
Cryptol REPL.
|
||||||
|
|
||||||
Floating point numbers may be written using either integral or fractioanl
|
Floating point numbers may be written using either integral or fractional
|
||||||
literals. In general, literals that cannot be represented exactly are
|
literals. In general, literals that cannot be represented exactly are
|
||||||
rejected with a type error, with the exception of decimal fractional litrals
|
rejected with a type error, with the exception of decimal fractional litrals
|
||||||
which are rounded to the nearest even representable numbers.
|
which are rounded to the nearest even representable number.
|
||||||
|
|
||||||
Floating point numbers may be manipulated and compared using
|
Floating point numbers may be manipulated and compared using
|
||||||
standard Cryptol operators, such as \texttt{+}, \texttt{==}, and \texttt{/.}
|
standard Cryptol operators, such as \texttt{+}, \texttt{==}, and \texttt{/.}
|
||||||
|
@ -90,10 +90,13 @@ primsPlaceHolder=1;
|
|||||||
zip : {n, a, b} [n]a -> [n]b -> [n](a, b)
|
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
|
zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c
|
||||||
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
|
foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
|
||||||
|
foldl' : {n, a, b} (fin n, Eq a) => (a -> b -> a) -> a -> [n]b -> a
|
||||||
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
|
foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
|
||||||
|
foldr' : {n, a, b} (fin n, Eq b) => (a -> b -> b) -> b -> [n]a -> b
|
||||||
scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [1 + n]b
|
scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [1 + n]b
|
||||||
scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b
|
scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b
|
||||||
sum : {n, a} (fin n, Arith a) => [n]a -> a
|
sum : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
|
||||||
|
product : {n, a} (fin n, Eq a, Ring a) => [n]a -> a
|
||||||
and, or : {n} (fin n) => [n] -> Bit
|
and, or : {n} (fin n) => [n] -> Bit
|
||||||
all, any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
|
all, any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
|
||||||
curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
|
curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
|
||||||
@ -102,6 +105,8 @@ primsPlaceHolder=1;
|
|||||||
\end{Verbatim}
|
\end{Verbatim}
|
||||||
\paragraph*{Miscellaneous}
|
\paragraph*{Miscellaneous}
|
||||||
\begin{Verbatim}
|
\begin{Verbatim}
|
||||||
|
deepseq : {a, b} Eq a => a -> b -> b
|
||||||
|
rnf : {a} Eq a => a -> a
|
||||||
length : {n, a, b} (fin n, Literal n b) => [n]a -> b
|
length : {n, a, b} (fin n, Literal n b) => [n]a -> b
|
||||||
zero : {a} (Zero a) => a
|
zero : {a} (Zero a) => a
|
||||||
\end{Verbatim}
|
\end{Verbatim}
|
||||||
|
Binary file not shown.
@ -44,6 +44,9 @@ primitive type Integer : *
|
|||||||
* of the equivalance class. In other words, 'fromZ' computes
|
* of the equivalance class. In other words, 'fromZ' computes
|
||||||
* the (unique) integer value 'i' where '0 <= i < n' and
|
* the (unique) integer value 'i' where '0 <= i < n' and
|
||||||
* 'i' is in the given equivalance class.
|
* '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 : *
|
primitive type {n : #} (fin n, n >= 1) => Z n : *
|
||||||
|
|
||||||
|
@ -31,6 +31,7 @@
|
|||||||
> import qualified Data.Text as T (pack)
|
> import qualified Data.Text as T (pack)
|
||||||
> import LibBF (BigFloat)
|
> import LibBF (BigFloat)
|
||||||
> import qualified LibBF as FP
|
> import qualified LibBF as FP
|
||||||
|
> import qualified GHC.Integer.GMP.Internals as Integer
|
||||||
>
|
>
|
||||||
> import Cryptol.ModuleSystem.Name (asPrim)
|
> import Cryptol.ModuleSystem.Name (asPrim)
|
||||||
> import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
|
> import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
|
||||||
@ -611,11 +612,11 @@ by corresponding type classes:
|
|||||||
> ringExp aty a =<< cryToInteger ety e
|
> ringExp aty a =<< cryToInteger ety e
|
||||||
>
|
>
|
||||||
> -- Field
|
> -- Field
|
||||||
> , "/." ~> binary (fieldBinary ratDiv
|
> , "/." ~> binary (fieldBinary ratDiv zDiv
|
||||||
> (fpBin FP.bfDiv fpImplicitRound)
|
> (fpBin FP.bfDiv fpImplicitRound)
|
||||||
> )
|
> )
|
||||||
>
|
>
|
||||||
> , "recip" ~> unary (fieldUnary ratRecip fpRecip)
|
> , "recip" ~> unary (fieldUnary ratRecip zRecip fpRecip)
|
||||||
>
|
>
|
||||||
> -- Round
|
> -- Round
|
||||||
> , "floor" ~> unary (roundUnary floor
|
> , "floor" ~> unary (roundUnary floor
|
||||||
@ -1203,20 +1204,25 @@ a reciprocal operator and a field division operator (not to be
|
|||||||
confused with integral division).
|
confused with integral division).
|
||||||
|
|
||||||
> fieldUnary :: (Rational -> E Rational) ->
|
> fieldUnary :: (Rational -> E Rational) ->
|
||||||
|
> (Integer -> Integer -> E Integer) ->
|
||||||
> (Integer -> Integer -> BigFloat -> E BigFloat) ->
|
> (Integer -> Integer -> BigFloat -> E BigFloat) ->
|
||||||
> TValue -> E Value -> E Value
|
> TValue -> E Value -> E Value
|
||||||
> fieldUnary qop flop ty v = case ty of
|
> fieldUnary qop zop flop ty v = case ty of
|
||||||
> TVRational -> VRational <$> appOp1 qop (fromVRational <$> v)
|
> TVRational -> VRational <$> appOp1 qop (fromVRational <$> v)
|
||||||
|
> TVIntMod m -> VInteger <$> appOp1 (zop m) (fromVInteger <$> v)
|
||||||
> TVFloat e p -> VFloat . fpToBF e p <$> appOp1 (flop e p) (fromVFloat <$> v)
|
> TVFloat e p -> VFloat . fpToBF e p <$> appOp1 (flop e p) (fromVFloat <$> v)
|
||||||
> _ -> evalPanic "fieldUnary" [show ty ++ " is not a Field type"]
|
> _ -> evalPanic "fieldUnary" [show ty ++ " is not a Field type"]
|
||||||
>
|
>
|
||||||
> fieldBinary ::
|
> fieldBinary ::
|
||||||
> (Rational -> Rational -> E Rational) ->
|
> (Rational -> Rational -> E Rational) ->
|
||||||
|
> (Integer -> Integer -> Integer -> E Integer) ->
|
||||||
> (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat) ->
|
> (Integer -> Integer -> BigFloat -> BigFloat -> E BigFloat) ->
|
||||||
> TValue -> E Value -> E Value -> E Value
|
> TValue -> E Value -> E Value -> E Value
|
||||||
> fieldBinary qop flop ty l r = case ty of
|
> fieldBinary qop zop flop ty l r = case ty of
|
||||||
> TVRational -> VRational <$>
|
> TVRational -> VRational <$>
|
||||||
> appOp2 qop (fromVRational <$> l) (fromVRational <$> r)
|
> appOp2 qop (fromVRational <$> l) (fromVRational <$> r)
|
||||||
|
> TVIntMod m -> VInteger <$>
|
||||||
|
> appOp2 (zop m) (fromVInteger <$> l) (fromVInteger <$> r)
|
||||||
> TVFloat e p -> VFloat . fpToBF e p <$>
|
> TVFloat e p -> VFloat . fpToBF e p <$>
|
||||||
> appOp2 (flop e p) (fromVFloat <$> l) (fromVFloat <$> r)
|
> appOp2 (flop e p) (fromVFloat <$> l) (fromVFloat <$> r)
|
||||||
> _ -> evalPanic "fieldBinary" [show ty ++ " is not a Field type"]
|
> _ -> evalPanic "fieldBinary" [show ty ++ " is not a Field type"]
|
||||||
@ -1228,7 +1234,14 @@ confused with integral division).
|
|||||||
> ratRecip :: Rational -> E Rational
|
> ratRecip :: Rational -> E Rational
|
||||||
> ratRecip 0 = cryError DivideByZero
|
> ratRecip 0 = cryError DivideByZero
|
||||||
> ratRecip x = pure (recip x)
|
> ratRecip x = pure (recip x)
|
||||||
|
>
|
||||||
|
> zRecip :: Integer -> Integer -> E Integer
|
||||||
|
> zRecip m x = if r == 0 then cryError DivideByZero else pure r
|
||||||
|
> where r = Integer.recipModInteger x m
|
||||||
|
>
|
||||||
|
> zDiv :: Integer -> Integer -> Integer -> E Integer
|
||||||
|
> zDiv m x y = f <$> zRecip m y
|
||||||
|
> where f yinv = (x * yinv) `mod` m
|
||||||
|
|
||||||
Round
|
Round
|
||||||
-----
|
-----
|
||||||
|
Loading…
Reference in New Issue
Block a user