mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 09:23:04 +03:00
Merge remote-tracking branch 'origin/master' into abstract-types
# Conflicts: # src/Cryptol/REPL/Monad.hs
This commit is contained in:
Iavor S. Diatchki
commit
7dc7be45bb
@ -1,20 +1,15 @@
|
||||
install:
|
||||
# Using '-y' and 'refreshenv' as a workaround to:
|
||||
# https://github.com/haskell/cabal/issues/3687
|
||||
- choco install -y ghc --version 8.0.2
|
||||
- choco install -y ghc --version 8.2.1
|
||||
- refreshenv
|
||||
# See http://help.appveyor.com/discussions/problems/6312-curl-command-not-found#comment_42195491
|
||||
# NB: Do this after refreshenv, otherwise it will be clobbered!
|
||||
- set PATH=C:\Program Files\Git\mingw64\bin;%PATH%;C:\msys64\usr\bin
|
||||
- curl -o cabal.zip --progress-bar https://www.haskell.org/cabal/release/cabal-install-1.24.0.0/cabal-install-1.24.0.0-x86_64-unknown-mingw32.zip
|
||||
- 7z x -bd cabal.zip
|
||||
- cabal --version
|
||||
- cabal update
|
||||
- curl -o z3.zip -L https://github.com/Z3Prover/z3/releases/download/z3-4.5.0/z3-4.5.0-x64-win.zip
|
||||
- 7z x -bd z3.zip
|
||||
- cp z3-4.5.0-x64-win/bin/z3.exe .
|
||||
|
||||
build_script:
|
||||
- cabal sandbox init
|
||||
- cabal install Cabal
|
||||
- make
|
||||
- cabal update
|
||||
- cabal new-build -j
|
||||
|
||||
20
.travis.yml
20
.travis.yml
@ -3,13 +3,18 @@ sudo: false
|
||||
|
||||
language: c
|
||||
|
||||
cache:
|
||||
directories:
|
||||
- $HOME/.ghc
|
||||
- $HOME/.cabal
|
||||
|
||||
matrix:
|
||||
include:
|
||||
- env: CABALVER="1.24" GHCVER="8.2.1"
|
||||
- env: CABALVER="2.0" GHCVER="8.2.1"
|
||||
compiler: ": #GHC 8.2.1"
|
||||
addons: {apt: {packages: [cabal-install-1.24,ghc-8.2.1], sources: [hvr-ghc]}}
|
||||
addons: {apt: {packages: [cabal-install-2.0,ghc-8.2.1], sources: [hvr-ghc]}}
|
||||
- os: osx
|
||||
env: CABALVER="1.24" GHCVER="8.2.1"
|
||||
env: CABALVER="2.0" GHCVER="8.2.1"
|
||||
compiler: ": #GHC 8.2.1"
|
||||
|
||||
before_install:
|
||||
@ -29,14 +34,9 @@ before_install:
|
||||
fi
|
||||
- env
|
||||
|
||||
install:
|
||||
- cabal update
|
||||
- cabal sandbox init
|
||||
- cabal install Cabal
|
||||
- make
|
||||
|
||||
script:
|
||||
- make test DIFF=""
|
||||
- cabal update
|
||||
- cabal new-build -j
|
||||
|
||||
notifications:
|
||||
email: false
|
||||
|
||||
@ -35,6 +35,7 @@ import qualified Cryptol.TypeCheck as T
|
||||
import qualified Cryptol.TypeCheck.AST as T
|
||||
|
||||
import qualified Cryptol.Utils.Ident as I
|
||||
import Cryptol.Utils.Logger(quietLogger)
|
||||
|
||||
import qualified Data.SBV.Dynamic as SBV
|
||||
|
||||
@ -74,6 +75,13 @@ main = do
|
||||
]
|
||||
]
|
||||
|
||||
-- | Evaluation options, mostly used by `trace`.
|
||||
-- Since the benchmarks likely do not use base, these don't matter very much
|
||||
evOpts :: E.EvalOpts
|
||||
evOpts = E.EvalOpts { E.evalLogger = quietLogger
|
||||
, E.evalPPOpts = E.defaultPPOpts
|
||||
}
|
||||
|
||||
-- | Make a benchmark for parsing a Cryptol module
|
||||
parser :: String -> FilePath -> Benchmark
|
||||
parser name path =
|
||||
@ -100,7 +108,7 @@ tc cd name path =
|
||||
}
|
||||
Right pm = P.parseModule cfg bytes
|
||||
menv <- M.initialModuleEnv
|
||||
(Right ((prims, scm, tcEnv), menv'), _) <- M.runModuleM menv $ withLib $ do
|
||||
(Right ((prims, scm, tcEnv), menv'), _) <- M.runModuleM (evOpts,menv) $ withLib $ do
|
||||
-- code from `loadModule` and `checkModule` in
|
||||
-- `Cryptol.ModuleSystem.Base`
|
||||
let pm' = M.addPrelude pm
|
||||
@ -114,7 +122,7 @@ tc cd name path =
|
||||
return (prims, scm, tcEnv)
|
||||
return (prims, scm, tcEnv, menv')
|
||||
in env setup $ \ ~(prims, scm, tcEnv, menv) ->
|
||||
bench name $ nfIO $ M.runModuleM menv $ withLib $ do
|
||||
bench name $ nfIO $ M.runModuleM (evOpts,menv) $ withLib $ do
|
||||
let act = M.TCAction { M.tcAction = T.tcModule
|
||||
, M.tcLinter = M.moduleLinter (P.thing (P.mName scm))
|
||||
, M.tcPrims = prims
|
||||
@ -126,7 +134,7 @@ ceval cd name path expr =
|
||||
let withLib = M.withPrependedSearchPath [cd </> "lib"] in
|
||||
let setup = do
|
||||
menv <- M.initialModuleEnv
|
||||
(Right (texpr, menv'), _) <- M.runModuleM menv $ withLib $ do
|
||||
(Right (texpr, menv'), _) <- M.runModuleM (evOpts,menv) $ withLib $ do
|
||||
m <- M.loadModuleByPath path
|
||||
M.setFocusedModule (T.mName m)
|
||||
let Right pexpr = P.parseExpr expr
|
||||
@ -134,7 +142,7 @@ ceval cd name path expr =
|
||||
return texpr
|
||||
return (texpr, menv')
|
||||
in env setup $ \ ~(texpr, menv) ->
|
||||
bench name $ nfIO $ E.runEval $ do
|
||||
bench name $ nfIO $ E.runEval evOpts $ do
|
||||
env' <- E.evalDecls (S.allDeclGroups menv) mempty
|
||||
(e :: E.Value) <- E.evalExpr env' texpr
|
||||
E.forceValue e
|
||||
@ -145,7 +153,7 @@ seval cd name path expr =
|
||||
let withLib = M.withPrependedSearchPath [cd </> "lib"] in
|
||||
let setup = do
|
||||
menv <- M.initialModuleEnv
|
||||
(Right (texpr, menv'), _) <- M.runModuleM menv $ withLib $ do
|
||||
(Right (texpr, menv'), _) <- M.runModuleM (evOpts,menv) $ withLib $ do
|
||||
m <- M.loadModuleByPath path
|
||||
M.setFocusedModule (T.mName m)
|
||||
let Right pexpr = P.parseExpr expr
|
||||
@ -153,7 +161,7 @@ seval cd name path expr =
|
||||
return texpr
|
||||
return (texpr, menv')
|
||||
in env setup $ \ ~(texpr, menv) ->
|
||||
bench name $ nfIO $ E.runEval $ do
|
||||
bench name $ nfIO $ E.runEval evOpts $ do
|
||||
env' <- E.evalDecls (S.allDeclGroups menv) mempty
|
||||
(e :: S.Value) <- E.evalExpr env' texpr
|
||||
E.io $ SBV.generateSMTBenchmark False $
|
||||
|
||||
2
cabal.project
Normal file
2
cabal.project
Normal file
@ -0,0 +1,2 @@
|
||||
packages:
|
||||
cryptol.cabal
|
||||
@ -248,7 +248,7 @@ removeWorker workers port _result =
|
||||
atomicModifyIORef workers $ \s -> (Map.delete port s, ())
|
||||
|
||||
runRepl :: Socket Rep -> IO ()
|
||||
runRepl rep = runREPL False $ do -- TODO: batch mode?
|
||||
runRepl rep = runREPL False stdoutLogger $ do -- TODO: batch mode?
|
||||
mCryptolPath <- io $ lookupEnv "CRYPTOLPATH"
|
||||
case mCryptolPath of
|
||||
Nothing -> return ()
|
||||
|
||||
@ -100,6 +100,7 @@ library
|
||||
Cryptol.Utils.Debug,
|
||||
Cryptol.Utils.Misc,
|
||||
Cryptol.Utils.Patterns,
|
||||
Cryptol.Utils.Logger,
|
||||
Cryptol.Version,
|
||||
|
||||
Cryptol.ModuleSystem,
|
||||
@ -206,6 +207,7 @@ executable cryptol
|
||||
, process
|
||||
, random
|
||||
, sbv >= 7.0
|
||||
, text
|
||||
, tf-random
|
||||
, transformers
|
||||
GHC-options: -Wall -O2 -threaded -rtsopts "-with-rtsopts=-N1 -A64m"
|
||||
|
||||
@ -16,6 +16,7 @@ import Cryptol.REPL.Command
|
||||
import Cryptol.REPL.Monad
|
||||
import Cryptol.REPL.Trie
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Logger(stdoutLogger)
|
||||
|
||||
import qualified Control.Exception as X
|
||||
import Control.Monad (guard, join)
|
||||
@ -25,6 +26,7 @@ import Data.Char (isAlphaNum, isSpace)
|
||||
import Data.Maybe(isJust)
|
||||
import Data.Function (on)
|
||||
import Data.List (isPrefixOf,nub,sortBy,sort)
|
||||
import qualified Data.Text as T (unpack)
|
||||
import System.IO (stdout)
|
||||
import System.Console.ANSI (setTitle, hSupportsANSI)
|
||||
import System.Console.Haskeline
|
||||
@ -111,7 +113,7 @@ loadCryRC cryrc =
|
||||
-- | Haskeline-specific repl implementation.
|
||||
repl :: Cryptolrc -> Maybe FilePath -> Bool -> REPL () -> IO CommandExitCode
|
||||
repl cryrc mbBatch stopOnError begin =
|
||||
runREPL (isJust mbBatch) $
|
||||
runREPL (isJust mbBatch) stdoutLogger $
|
||||
do status <- loadCryRC cryrc
|
||||
case status of
|
||||
CommandOk -> begin >> crySession mbBatch stopOnError
|
||||
@ -226,6 +228,7 @@ cmdArgument ct cursor@(l,_) = case ct of
|
||||
ExprArg _ -> completeExpr cursor
|
||||
DeclsArg _ -> (completeExpr +++ completeType) cursor
|
||||
ExprTypeArg _ -> (completeExpr +++ completeType) cursor
|
||||
ModNameArg _ -> completeModName cursor
|
||||
FilenameArg _ -> completeFilename cursor
|
||||
ShellArg _ -> completeFilename cursor
|
||||
OptionArg _ -> completeOption cursor
|
||||
@ -259,6 +262,14 @@ completeType (l,_) = do
|
||||
vars = filter (n `isPrefixOf`) ns
|
||||
return (l,map (nameComp n) vars)
|
||||
|
||||
-- | Complete a name from the list of loaded modules.
|
||||
completeModName :: CompletionFunc REPL
|
||||
completeModName (l, _) = do
|
||||
ns <- map T.unpack <$> getModNames
|
||||
let n = reverse (takeIdent l)
|
||||
vars = filter (n `isPrefixOf`) ns
|
||||
return (l, map (nameComp n) vars)
|
||||
|
||||
-- | Generate a completion from a prefix and a name.
|
||||
nameComp :: String -> String -> Completion
|
||||
nameComp prefix c = Completion
|
||||
|
||||
Binary file not shown.
@ -190,12 +190,12 @@ the same value, so {\tt a} and {\tt A} both represent 10.
|
||||
|
||||
A tuple is a simple collection of arbitrary ordered values of
|
||||
arbitrary types, written in parentheses.\indTheTupleType A tuple is at
|
||||
least a pair; it has at least two elements\footnote{Tuples with zero
|
||||
least a pair; it has at least two elements,\footnote{Tuples with zero
|
||||
and one element are part of the underlying mathematics of Cryptol's
|
||||
tuple theory but are not supported in its concrete syntax because
|
||||
doing so unnecessarily complicates the parser and program
|
||||
comprehension.}, and can be arbitrarily nested with other types.
|
||||
Elements are comma separated.
|
||||
comprehension.} and can be arbitrarily nested with other types.
|
||||
Elements are comma separated.
|
||||
|
||||
Two tuples are equal in the standard fashion: if they have the same
|
||||
arity, their types are pairwise comparable
|
||||
@ -622,10 +622,10 @@ Try the following infinite enumerations:
|
||||
\begin{Answer}\ansref{ex:seq:9}
|
||||
When you type in an infinite sequence, Cryptol will only print the
|
||||
first 5 elements of it and will indicate that it is an infinite value
|
||||
by putting $\ldots$ at the end\footnote{You can change this behavior
|
||||
by putting $\ldots$ at the end.\footnote{You can change this behavior
|
||||
by setting the {\tt infLength} variable, like so: {\tt Cryptol>
|
||||
:set infLength=10} will show the first 10 elements of infinite
|
||||
sequences}. Here are the responses:
|
||||
sequences} Here are the responses:
|
||||
\begin{Verbatim}
|
||||
[1, 2, 3, 4, 5, ...]
|
||||
[1, 3, 5, 7, 9, ...]
|
||||
@ -1079,12 +1079,12 @@ shift a word, say {\tt 12:[6]} by one to the right:
|
||||
\end{Verbatim}
|
||||
That is shifting right by one effectively divides the word by 2. This
|
||||
is due to Cryptol's ``big-endian'' representation of
|
||||
numbers\footnote{This is a significant change from Cryptol version 1,
|
||||
numbers.\footnote{This is a significant change from Cryptol version 1,
|
||||
which interpreted the leftmost element of a sequence as the
|
||||
lowest-ordered bit (and thus shifting right was multiplying by 2,
|
||||
and shifting left was dividing by 2). The way it is handled now
|
||||
matches the traditional
|
||||
interpretation.}.\indRotLeft\indRotRight\indShiftLeft\indShiftRight
|
||||
interpretation.}\indRotLeft\indRotRight\indShiftLeft\indShiftRight
|
||||
|
||||
\begin{Exercise}\label{ex:words:6}
|
||||
Try the following examples of shifting/rotating words:
|
||||
@ -1160,10 +1160,10 @@ operations on them; including arithmetic:
|
||||
|
||||
In Cryptol, records are simply collections of named fields. In this
|
||||
sense, they are very similar to tuples (Section~\ref{sec:tuple}),
|
||||
which can be thought of records without field names\footnote{In fact,
|
||||
which can be thought of records without field names.\footnote{In fact,
|
||||
the fields of a tuple {\it can} be accessed via the dot-notation,
|
||||
with their names being their 0-indexed position in the tuple. So
|
||||
{\tt (1,2).1 == 2}.}. Like a tuple, the fields of a record can be of
|
||||
{\tt (1,2).1 == 2}.} Like a tuple, the fields of a record can be of
|
||||
any type. We construct records by listing the fields inside
|
||||
curly braces, separated by commas. We project fields out of a record
|
||||
with the usual dot-notation. Note that the order of fields in a
|
||||
@ -1510,9 +1510,9 @@ Here are Cryptol's responses:\indModular\indEnum\indInfSeq
|
||||
[0, 0, 0, 0, 0, ...]
|
||||
\end{Verbatim}
|
||||
as opposed to \texttt{[0, 1, 0, 1, 0, ...]}, as one might
|
||||
expect\footnote{This is one of the subtle changes from Cryptol 1. The
|
||||
expect.\footnote{This is one of the subtle changes from Cryptol 1. The
|
||||
previous behavior can be achieved by dropping the first element from
|
||||
\texttt{[1 ...]}.}. This behavior follows from the specification that
|
||||
\texttt{[1 ...]}.} This behavior follows from the specification that
|
||||
the width of the elements of the sequence are derived from the width of
|
||||
the elements in the seed, which in this case is 0.
|
||||
\end{Answer}
|
||||
@ -1542,11 +1542,11 @@ element is at least $4$ bits wide.
|
||||
% \label{sec:types}
|
||||
\sectionWithAnswers{Types}{sec:types}
|
||||
|
||||
Cryptol's type system is one of its key features\footnote{The Cryptol
|
||||
Cryptol's type system is one of its key features.\footnote{The Cryptol
|
||||
type system is based on the traditional Hindley-Milner style,
|
||||
extended with size types and arithmetic
|
||||
predicates (for details, see~\cite{erkok-carlsson-wick-cryptolCoverification-09,
|
||||
erkok-matthews-cryptolEqChecking-09, Hin97})}. You have seen that
|
||||
erkok-matthews-cryptolEqChecking-09, Hin97})} You have seen that
|
||||
types can be used to specify the exact width of values, or shapes of
|
||||
sequences using a rich yet concise notation. In some cases, it may
|
||||
make sense to omit a type signature and let Cryptol {\em infer} the
|
||||
@ -1841,9 +1841,9 @@ In general, type predicates exclusively describe \textit{arithmetic
|
||||
constraints on type variables}. Cryptol does not have a
|
||||
general-purpose dependent type system, but a \emph{size-polymorphic
|
||||
type system}. Often type variables' values are of finite size,
|
||||
indicated with the constraint {\tt fin a}\indFin, otherwise no
|
||||
constraint is mentioned or an explicit \texttt{inf a} is
|
||||
denoted\indInf, and the variables' values are unbounded. Arithmetic
|
||||
indicated with the constraint {\tt fin a}\indFin; otherwise no
|
||||
constraint is mentioned, and the variables' values are unbounded,
|
||||
possibly taking the value \texttt{inf}\indInf. Arithmetic
|
||||
relations are arbitrary relations over all type variables, such as
|
||||
{\tt 2*a+b >= c}. We shall see more examples as we work through
|
||||
programs later on.
|
||||
@ -1964,10 +1964,10 @@ be very precisely specified and the programs can be statically
|
||||
guaranteed to respect these sizes.
|
||||
|
||||
Opponents of type systems typically argue that the type system gets in
|
||||
the way\footnote{Another complaint is that ``strong types are for
|
||||
the way.\footnote{Another complaint is that ``strong types are for
|
||||
weak minds.'' We do not disagree here: Cryptol programmers want to
|
||||
use the type system so we do not have to think as hard about writing
|
||||
correct code as we would without strong types.}. It is true that
|
||||
correct code as we would without strong types.} It is true that
|
||||
the type system will reject some programs that makes perfect
|
||||
sense. But what is more important is that the type system will reject
|
||||
programs that will indeed go wrong at run-time. And the price you pay
|
||||
@ -1988,16 +1988,11 @@ for~\cite{lewis2003}.
|
||||
|
||||
So far, we used Cryptol as a calculator: we typed in expressions and
|
||||
it gave us answers. This is great for experimenting, and exploring
|
||||
Cryptol itself. The next fundamental Cryptol idiom is the notion of a
|
||||
Cryptol itself. The next fundamental Cryptol idiom is the notion of a
|
||||
function. You have already used built-in functions {\tt +}, {\tt
|
||||
take}, etc.\indPlus\indLg Of course, users can define their own
|
||||
functions as well. Currently the Cryptol interpreter does not support
|
||||
defining functions, so you must define them in a file and load it, as
|
||||
in the next exercises.
|
||||
|
||||
\todo[inline]{Is the inability to define top-level symbols at the REPL a
|
||||
feature forever, will we allow this, or should we document it
|
||||
above?}
|
||||
functions as well. The recommended method is to define them in a file
|
||||
and load it, as in the next exercises.
|
||||
|
||||
\note{Reviewing the contents of Section~\ref{sec:technicalities} might
|
||||
help at this point. Especially the commands that will let you load
|
||||
@ -2042,6 +2037,45 @@ argument of the wrong size: 912 is too big to fit into 8 bits.
|
||||
to pass a negative argument, e.g. \texttt{increment(-2)} (recall
|
||||
Exercise~\autoref{ex:arith:5}).}\indFunApp
|
||||
|
||||
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
\subsection{Definitions in the interpreter with \texttt{let}}
|
||||
\label{sec:interpreter-let}
|
||||
As an alternative to creating and loading files, the Cryptol
|
||||
interpreter also supports simple definitions with \texttt{let}. Unlike
|
||||
file-based definitions, \texttt{let}-definitions are not persistent:
|
||||
They exist only until the same name is redefined or the interpreter
|
||||
exits with \texttt{:q}.
|
||||
\begin{code}
|
||||
Cryptol> let r = {a = True, b = False}
|
||||
Cryptol> r.a
|
||||
True
|
||||
\end{code}
|
||||
Simple functions can be defined in the interpreter with \texttt{let},
|
||||
with some restrictions: They must be entered on a single line, and
|
||||
they cannot have a separate type signature. If we want a function to
|
||||
have a more specific type than the inferred one, we must add type
|
||||
annotations to variables or other parts of the body of the definition.
|
||||
\begin{Exercise}\label{ex:fn:0b}
|
||||
Enter the following definition into the Cryptol interpreter and check
|
||||
its type with \texttt{:t}.
|
||||
\begin{code}
|
||||
let increment x = x+1
|
||||
\end{code}
|
||||
Modify the \texttt{let}-definition of \texttt{increment} so that it
|
||||
will have type \texttt{[8] -> [8]}.
|
||||
\end{Exercise}
|
||||
\begin{Answer}\ansref{ex:fn:0b}
|
||||
Any of the following definitions will have the desired type:
|
||||
\begin{Verbatim}
|
||||
Cryptol> let increment (x : [8]) = x + 1
|
||||
Cryptol> let increment x = (x : [8]) + 1
|
||||
Cryptol> let increment x = x + (1 : [8])
|
||||
Cryptol> let increment x = x + 1 : [8]
|
||||
Cryptol> :t increment
|
||||
increment : [8] -> [8]
|
||||
\end{Verbatim}
|
||||
\end{Answer}
|
||||
|
||||
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
\subsection{Local names: {\ttfamily{\textbf where}} clauses}
|
||||
\label{sec:local-names:-ttfam}
|
||||
@ -2805,24 +2839,41 @@ This operator type is interpreted ``equality is an operator that takes
|
||||
two objects of any single type that can be compared and returns a
|
||||
Bit.''
|
||||
|
||||
Cryptol defines exactly two basic type classes: {\tt Cmp} and {\tt
|
||||
Arith}. These appear in the type signature of operators and
|
||||
functions that require them. If a function you define calls, for
|
||||
example, {\tt +}, on two arguments both of type {\tt a}, the type
|
||||
constraints for {\tt a} will include {\tt (Arith a)}.
|
||||
Cryptol defines a collection of basic type classes: \texttt{Logic},
|
||||
\texttt{Zero}, \texttt{Cmp}, \texttt{SignedCmp}, and \texttt{Arith}.
|
||||
These appear in the type signature of operators and functions that
|
||||
require them. If a function you define calls, for example, {\tt +}, on
|
||||
two arguments both of type {\tt a}, the type constraints for {\tt a}
|
||||
will include {\tt (Arith a)}.
|
||||
|
||||
The \texttt{Logic} typeclass includes the binary logical operators
|
||||
\texttt{\&\&}, \texttt{||}, and \verb+^+, as well as the unary
|
||||
operator \verb+~+.
|
||||
|
||||
The \texttt{Zero} typeclass includes the special constant
|
||||
\texttt{zero}. The shifting operators \texttt{<<} and \texttt{>>} are
|
||||
also in class \texttt{Zero}, because they can shift in zero values.
|
||||
All of the built-in types of Cryptol are instances of class
|
||||
\texttt{Zero}.
|
||||
|
||||
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 is defined on function types (i.e.,
|
||||
\texttt{\{a b\} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit}). Unlike
|
||||
in many other languages, equality and comparison are bundled into a
|
||||
single typeclass.
|
||||
\todo[inline]{``many'' other languages? Like what?}
|
||||
\todo[inline]{``equality is defined on function types'' is misleading, can't use == for this.}
|
||||
\texttt{max}. Note that equality and other comparisons are bundled
|
||||
into a single typeclass. Function types are not in class \texttt{Cmp}
|
||||
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}.
|
||||
|
||||
The \texttt{Arith} typeclass include the binary operators \texttt{+},
|
||||
\texttt{-}, \texttt{*}, \texttt{/}, \verb+%+, \verb+^^+, as well
|
||||
The \texttt{SignedCmp} typeclass includes the binary relation
|
||||
operators \texttt{<\$}, \texttt{>\$}, \texttt{<=\$}, and
|
||||
\texttt{>=\$}. These are like \texttt{<}, \texttt{>}, \texttt{<=}, and
|
||||
\texttt{>=}, except that they interpret bitvectors as \emph{signed}
|
||||
2's complement numbers, whereas the \texttt{Cmp} operations use the
|
||||
\emph{unsigned} ordering.
|
||||
|
||||
The \texttt{Arith} typeclass includes the binary operators \texttt{+},
|
||||
\texttt{-}, \texttt{*}, \texttt{/}, \verb+%+, and \verb+^^+, as well
|
||||
as the unary operators \texttt{lg2} and \texttt{-}.
|
||||
|
||||
\begin{Exercise}\label{ex:tvar:1}
|
||||
@ -2844,7 +2895,7 @@ yields the inferred type:
|
||||
\end{Answer}
|
||||
|
||||
%=====================================================================
|
||||
\section{Type vs. value variables}\indTypeVariables
|
||||
\section{Type vs.\ value variables}\indTypeVariables
|
||||
\label{sec:type-vs.-value}
|
||||
|
||||
\todo[inline]{Rewrite this whole section to better clarify object- vs. type
|
||||
@ -2881,13 +2932,13 @@ A \emph{type variable}, on the other hand, allows you to express
|
||||
interesting (arithmetic) constraints on \emph{types}. These variables
|
||||
express things like lengths of sequences or relationships between
|
||||
lengths of sequences. Type variable values are computed
|
||||
statically---they never change at runtime\footnote{In this way,
|
||||
statically---they never change at runtime.\footnote{In this way,
|
||||
they are similar (but more expressive than) templates in languages
|
||||
like C++ or Java. If you want to learn more about this area, look up
|
||||
the term ``type-level naturals''.}.
|
||||
the term ``type-level naturals''.}
|
||||
|
||||
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
\subsection{Positional vs. named type
|
||||
\subsection{Positional vs.\ named type
|
||||
arguments}\indTypePositionalArguments
|
||||
\label{sec:positional-vs.-named}
|
||||
|
||||
@ -2935,7 +2986,7 @@ clear, as in:
|
||||
resolution, in the presence of positional arguments.}
|
||||
|
||||
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
||||
\subsection{Type context vs. variable context}\indTypeContext
|
||||
\subsection{Type context vs.\ variable context}\indTypeContext
|
||||
\label{sec:type-context-vs}
|
||||
|
||||
You have seen, in the discussion of type variables above, that Cryptol
|
||||
|
||||
@ -352,10 +352,10 @@ user the proof is complete.\indQED\indProve
|
||||
Cryptol will use Microsoft Research's Z3 SMT solver under the hood,
|
||||
but it can be configured to use other SAT/SMT solvers as well, such
|
||||
as SRI's Yices~\cite{YicesWWW}\indYices, or CVC4
|
||||
~\cite{cvc4WWW}\footnote{To do this, first install the package(s)
|
||||
~\cite{cvc4WWW}.\footnote{To do this, first install the package(s)
|
||||
from the URLs provided in the bibliography. Once a prover has been
|
||||
installed you can activate it with, for example, {\tt :set
|
||||
prover=cvc4}.}. Note that the {\tt :prove} command is a
|
||||
prover=cvc4}.} Note that the {\tt :prove} command is a
|
||||
push-button tool: once the proof starts there is no user
|
||||
involvement. Of course, the external tool used may not be able to
|
||||
complete all the proofs in a feasible amount of time, naturally.
|
||||
@ -532,11 +532,10 @@ $$
|
||||
$$
|
||||
Obviously, this relationship holds only when $y \not= 0$. The idea
|
||||
behind a conditional Cryptol property\indThmCond is that we would like
|
||||
to capture these side-conditions formally in our specifications.
|
||||
to capture these side-conditions formally in our specifications.
|
||||
|
||||
We simply use an ordinary {\tt if-then-else} expression in Cryptol to
|
||||
write conditional properties (at least until we add boolean logic
|
||||
operators to Cryptol). If the condition is invalid, we simply return
|
||||
We can use ordinary {\tt if-then-else} expressions in Cryptol to
|
||||
write conditional properties. If the condition is invalid, we simply return
|
||||
{\tt True}, indicating that we are not interested in that particular
|
||||
case. Depending on how natural it is to express the side-condition or
|
||||
its negation, you can use one of the following two patterns:
|
||||
@ -547,6 +546,17 @@ its negation, you can use one of the following two patterns:
|
||||
else True else \emph{property-expression}
|
||||
\end{Verbatim}
|
||||
|
||||
Alternatively, Cryptol provides a few logical connectives
|
||||
(\texttt{==>}, \texttt{\textbackslash/}, and \texttt{/\textbackslash})
|
||||
that are useful for writing conditional properties. Each is defined in
|
||||
terms of \texttt{if-then-else} as follows:
|
||||
|
||||
\begin{Verbatim}
|
||||
a ==> b = if a then b else True
|
||||
a \/ b = if a then True else b
|
||||
a /\ b = if a then b else False
|
||||
\end{Verbatim}
|
||||
|
||||
\begin{Exercise}\label{ex:cond:1}
|
||||
Express the relationship between division, multiplication, and
|
||||
modulus using a conditional Cryptol property. Prove the property
|
||||
|
||||
@ -21,7 +21,7 @@
|
||||
\usepackage{xcolor}
|
||||
\usepackage{pdfpages}
|
||||
\usepackage[answerdelayed,lastexercise]{utils/exercise}
|
||||
\usepackage[xetex,bookmarks=true,pagebackref=true,linktocpage=true]{hyperref}
|
||||
\usepackage[xetex,bookmarks=true,pagebackref=true,linktocpage=false]{hyperref}
|
||||
\usepackage[style=list]{utils/glossary}
|
||||
\usepackage{adjustbox}
|
||||
|
||||
|
||||
@ -8,13 +8,14 @@ primsPlaceHolder=1;
|
||||
|
||||
\paragraph*{Bitwise operations}
|
||||
\begin{Verbatim}
|
||||
&&, ||, ^ : {a} a -> a -> a
|
||||
~ : {a} a -> a
|
||||
&&, ||, ^ : {a} (Logic a) => a -> a -> a
|
||||
~ : {a} (Logic a) => a -> a
|
||||
\end{Verbatim}
|
||||
\paragraph*{Comparisons}
|
||||
\begin{Verbatim}
|
||||
==, != : {a} (Cmp a) => a -> a -> Bit
|
||||
<, >, <=, >= : {a} (Cmp a) => a -> a -> Bit
|
||||
<$ : {a} (SignedCmp a) => a -> a -> Bit
|
||||
\end{Verbatim}
|
||||
\paragraph*{Arithmetic}
|
||||
\begin{Verbatim}
|
||||
@ -26,7 +27,7 @@ primsPlaceHolder=1;
|
||||
\begin{Verbatim}
|
||||
pdiv : {a, b} (fin a, fin b) => [a] -> [b] -> [a]
|
||||
pmod : {a, b} (fin a, fin b) => [a] -> [1 + b] -> [b]
|
||||
pmult : {a, b} (fin a, fin b) => [a] -> [b] -> [max 1 (a + b) - 1]
|
||||
pmult : {a, b} (fin a, fin b) => [1 + a] -> [1 + b] -> [1 + a + b]
|
||||
\end{Verbatim}
|
||||
\paragraph*{Sequences}
|
||||
\begin{Verbatim}
|
||||
@ -35,7 +36,7 @@ primsPlaceHolder=1;
|
||||
drop : {front, back, elem} (fin front)
|
||||
=> [front + back]elem -> [front]elem
|
||||
tail : {a, b} [a+1]b -> [a]b
|
||||
# : {front, back, a} (fin front) =>
|
||||
# : {front, back, a} (fin front)
|
||||
=> [front]a -> [back]a -> [front + back]a
|
||||
join : {parts, each, a} (fin each)
|
||||
=> [parts][each]a -> [parts * each]a
|
||||
@ -58,12 +59,12 @@ primsPlaceHolder=1;
|
||||
\end{Verbatim}
|
||||
\paragraph*{Shifting, rotating}
|
||||
\begin{Verbatim}
|
||||
>>, << : {a, b, c} (fin b) => [a]c -> [b] -> [a]c
|
||||
>>, << : {a, b, c} (fin b, Zero c) => [a]c -> [b] -> [a]c
|
||||
>>>, <<< : {a, b, c} (fin a, fin b) => [a]c -> [b] -> [a]c
|
||||
\end{Verbatim}
|
||||
\paragraph*{Miscellaneous}
|
||||
\begin{Verbatim}
|
||||
zero : {a} a
|
||||
zero : {a} (Zero a) => a
|
||||
transpose : {a, b, c} [a][b]c -> [b][a]c
|
||||
min, max : {a} (Cmp a) => a -> a -> a
|
||||
\end{Verbatim}
|
||||
|
||||
@ -37,9 +37,9 @@ loop. On a Linux/Mac machine, this simply amounts to typing:
|
||||
|
||||
\noindent Of course, your version number may be different, but for
|
||||
this document we will assume you are running at least version
|
||||
2.0\footnote{Version 2.0 of cryptol is a significant change from
|
||||
2.0.\footnote{Version 2.0 of cryptol is a significant change from
|
||||
version 1. If you are already familiar with Cryptol version 1, there
|
||||
is a document in the Cryptol release that summarizes the changes.}.
|
||||
is a document in the Cryptol release that summarizes the changes.}
|
||||
|
||||
On Windows, you typically click on the desktop icon to run Cryptol in
|
||||
a command window. Otherwise, the interaction mode is exactly the
|
||||
|
||||
@ -136,15 +136,19 @@ to surround the operator with {\tt ()}, like this:
|
||||
\paragraph*{Browsing definitions}
|
||||
The command {\tt :browse} (or {\tt :b} for short) will display all the
|
||||
names you have defined, along with their types.\indCmdBrowse
|
||||
Using \texttt{:browse} with the name of a loaded module will show
|
||||
the declarations from that module only.
|
||||
|
||||
\paragraph*{Getting help}
|
||||
The command {\tt :help} will show you all the available
|
||||
commands.\indCmdHelp Other useful implicit help invocations are:
|
||||
(a)~to type tab at the {\tt Cryptol>} prompt, which will list all of
|
||||
the operators available in Cryptol code, (b)~typing {\tt :set} with no
|
||||
argument, which shows you the parameters that can be set, and (c), as
|
||||
noted elsewhere, {\tt :browse} to see the names of functions and type
|
||||
aliases you have defined, along with their types.
|
||||
commands.\indCmdHelp Using \texttt{:help} with the name of a defined
|
||||
function or type synonym will display its corresponding help text.
|
||||
Other useful implicit help invocations are: (a)~to type tab at the
|
||||
{\tt Cryptol>} prompt, which will list all of the operators available
|
||||
in Cryptol code, (b)~typing {\tt :set} with no argument, which shows
|
||||
you the parameters that can be set, and (c), as noted elsewhere,
|
||||
\texttt{:browse} to see the names of functions and type aliases you
|
||||
have defined, along with their types.
|
||||
|
||||
\todo[inline]{What should \texttt{:help symbolname} do, especially for
|
||||
prelude functions and types? How about for commands?}
|
||||
@ -214,6 +218,7 @@ platform-dependent.
|
||||
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
|
||||
either one or zero arguments. If one argument is provided, then that
|
||||
property is the focus of the command; otherwise all properties in the
|
||||
|
||||
Binary file not shown.
@ -1079,8 +1079,8 @@ takes a 256-bit key and 96-bit nonce as follows:
|
||||
|
||||
//ct in this function has tag removed
|
||||
AeadConstruction (AAD : [n][8]) (CT : [m][8]) = (AAD # padding1 # CT # padding2 # adlen # ptlen) where
|
||||
padding1 = (zero:[(16-n%16)%16][8])
|
||||
padding2 = (zero:[(16-m%16)%16][8])
|
||||
padding1 = (zero:[n %^ 16][8])
|
||||
padding2 = (zero:[m %^ 16][8])
|
||||
adlen : [8][8]
|
||||
adlen = groupBy`{8}(littleendian (groupBy`{8}(`n:[64])))
|
||||
ptlen : [8][8]
|
||||
|
||||
@ -6,13 +6,8 @@
|
||||
fnv1a : {n} (fin n) => [n] -> [64]
|
||||
fnv1a ws = fnv1a' (pad ws)
|
||||
|
||||
pad : {msgLen,chunks,padding}
|
||||
( fin msgLen
|
||||
, chunks == (msgLen+7) / 8
|
||||
, padding == (8 - msgLen % 8) % 8
|
||||
)
|
||||
=> [msgLen] -> [chunks][8]
|
||||
pad msg = split (msg # (zero:[padding]))
|
||||
pad : {msgLen} (fin msgLen) => [msgLen] -> [msgLen /^ 8][8]
|
||||
pad msg = split (msg # (zero:[msgLen %^ 8]))
|
||||
|
||||
fnv1a' : {chunks} (fin chunks) => [chunks][8] -> [64]
|
||||
fnv1a' msg = Ss ! 0
|
||||
@ -23,8 +18,8 @@ fnv1a' msg = Ss ! 0
|
||||
| m <- msg
|
||||
]
|
||||
|
||||
block : {padding} ( padding == 64 - 8) => [64] -> [8] -> [64]
|
||||
block state val = (state ^ ((zero : [padding]) # val)) * fnv1a_prime
|
||||
block : {padLen} ( padLen == 64 - 8) => [64] -> [8] -> [64]
|
||||
block state val = (state ^ ((zero : [padLen]) # val)) * fnv1a_prime
|
||||
|
||||
fnv1a_offset_basis : [64]
|
||||
fnv1a_offset_basis = 14695981039346656037
|
||||
|
||||
@ -53,15 +53,12 @@ K = [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x
|
||||
/*
|
||||
* Preprocessing (padding and parsing) for SHA256 : Section 5.1.1 and 5.2.1
|
||||
*/
|
||||
preprocess : {msgLen,contentLen,chunks,padding}
|
||||
preprocess : {msgLen}
|
||||
( fin msgLen
|
||||
, 64 >= width msgLen // message width fits in a word
|
||||
, contentLen == msgLen + 65 // message + header
|
||||
, chunks == (contentLen+511) / 512
|
||||
, padding == (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0
|
||||
)
|
||||
=> [msgLen] -> [chunks][512]
|
||||
preprocess msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64]))
|
||||
=> [msgLen] -> [(msgLen + 65) /^ 512][512]
|
||||
preprocess msg = split (msg # [True] # (zero:[(msgLen + 65) %^ 512]) # (`msgLen:[64]))
|
||||
|
||||
/*
|
||||
* SHA256 Initial Hash Value : Section 5.3.3
|
||||
|
||||
@ -27,15 +27,14 @@ As a summary, a "1" followed by m "0"s followed by a 64-
|
||||
SHA-1 as n 512-bit blocks.
|
||||
*/
|
||||
|
||||
pad : {msgLen,chunks}
|
||||
pad : {msgLen}
|
||||
( fin msgLen
|
||||
, 64 >= width msgLen // message width fits in a word
|
||||
, chunks == (msgLen + 65 + 511) / 512
|
||||
)
|
||||
=> [msgLen] -> [chunks][512]
|
||||
pad msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64]))
|
||||
=> [msgLen] -> [(msgLen + 65) /^ 512][512]
|
||||
pad msg = split (msg # [True] # (zero:[padLen]) # (`msgLen:[64]))
|
||||
where type contentLen = msgLen + 65 // message + header
|
||||
type padding = (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0
|
||||
type padLen = (msgLen + 65) %^ 512
|
||||
|
||||
f : ([8], [32], [32], [32]) -> [32]
|
||||
f (t, x, y, z) =
|
||||
|
||||
@ -53,15 +53,12 @@ K = [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x
|
||||
/*
|
||||
* Preprocessing (padding and parsing) for SHA256 : Section 5.1.1 and 5.2.1
|
||||
*/
|
||||
preprocess : {msgLen,contentLen,chunks,padding}
|
||||
preprocess : {msgLen}
|
||||
( fin msgLen
|
||||
, 64 >= width msgLen // message width fits in a word
|
||||
, contentLen == msgLen + 65 // message + header
|
||||
, chunks == (contentLen+511) / 512
|
||||
, padding == (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0
|
||||
)
|
||||
=> [msgLen] -> [chunks][512]
|
||||
preprocess msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64]))
|
||||
=> [msgLen] -> [(msgLen + 65) /^ 512][512]
|
||||
preprocess msg = split (msg # [True] # (zero:[(msgLen + 65) %^ 512]) # (`msgLen:[64]))
|
||||
|
||||
/*
|
||||
* SHA256 Initial Hash Value : Section 5.3.3
|
||||
|
||||
457
examples/contrib/CAST5.cry
Normal file
457
examples/contrib/CAST5.cry
Normal file
@ -0,0 +1,457 @@
|
||||
/*
|
||||
* CAST5 (RFC 2144)
|
||||
*/
|
||||
|
||||
module CAST5 where
|
||||
|
||||
import Cipher
|
||||
|
||||
CAST128 : Cipher 128 64
|
||||
CAST128 =
|
||||
{ encrypt key pt = cast5_16 pt (expandKey key)
|
||||
, decrypt key ct = cast5_16 ct (bireverse (expandKey key))
|
||||
}
|
||||
|
||||
CAST5_80 : Cipher 80 64
|
||||
CAST5_80 =
|
||||
{ encrypt key pt = cast5_12 pt (expandKey key)
|
||||
, decrypt key ct = cast5_12 ct (bireverse (expandKey key))
|
||||
}
|
||||
|
||||
CAST5_64 : Cipher 64 64
|
||||
CAST5_64 =
|
||||
{ encrypt key pt = cast5_12 pt (expandKey key)
|
||||
, decrypt key ct = cast5_12 ct (bireverse (expandKey key))
|
||||
}
|
||||
|
||||
CAST5_40 : Cipher 40 64
|
||||
CAST5_40 =
|
||||
{ encrypt key pt = cast5_12 pt (expandKey key)
|
||||
, decrypt key ct = cast5_12 ct (bireverse (expandKey key))
|
||||
}
|
||||
|
||||
bireverse (x,y) = (reverse x, reverse y)
|
||||
|
||||
cast5_16 pt (km,kr) = result where
|
||||
result = R16#L16
|
||||
[L0,R0] = split pt
|
||||
L1 = R0
|
||||
R1 = L0 ^ f1 (R0, km@0, kr@0)
|
||||
L2 = R1
|
||||
R2 = L1 ^ f2 (R1, km@1, kr@1)
|
||||
L3 = R2
|
||||
R3 = L2 ^ f3 (R2, km@2, kr@2)
|
||||
L4 = R3
|
||||
R4 = L3 ^ f1 (R3, km@3, kr@3)
|
||||
L5 = R4
|
||||
R5 = L4 ^ f2 (R4, km@4, kr@4)
|
||||
L6 = R5
|
||||
R6 = L5 ^ f3 (R5, km@5, kr@5)
|
||||
L7 = R6
|
||||
R7 = L6 ^ f1 (R6, km@6, kr@6)
|
||||
L8 = R7
|
||||
R8 = L7 ^ f2 (R7, km@7, kr@7)
|
||||
L9 = R8
|
||||
R9 = L8 ^ f3 (R8, km@8, kr@8)
|
||||
L10 = R9
|
||||
R10 = L9 ^ f1 (R9, km@9, kr@9)
|
||||
L11 = R10
|
||||
R11 = L10 ^ f2 (R10, km@10, kr@10)
|
||||
L12 = R11
|
||||
R12 = L11 ^ f3 (R11, km@11, kr@11)
|
||||
L13 = R12
|
||||
R13 = L12 ^ f1 (R12, km@12, kr@12)
|
||||
L14 = R13
|
||||
R14 = L13 ^ f2 (R13, km@13, kr@13)
|
||||
L15 = R14
|
||||
R15 = L14 ^ f3 (R14, km@14, kr@14)
|
||||
L16 = R15
|
||||
R16 = L15 ^ f1 (R15, km@15, kr@15)
|
||||
|
||||
cast5_12 pt (km,kr) = result where
|
||||
result = R12#L12
|
||||
[L0,R0] = split pt
|
||||
L1 = R0
|
||||
R1 = L0 ^ f1 (R0, km@0, kr@0)
|
||||
L2 = R1
|
||||
R2 = L1 ^ f2 (R1, km@1, kr@1)
|
||||
L3 = R2
|
||||
R3 = L2 ^ f3 (R2, km@2, kr@2)
|
||||
L4 = R3
|
||||
R4 = L3 ^ f1 (R3, km@3, kr@3)
|
||||
L5 = R4
|
||||
R5 = L4 ^ f2 (R4, km@4, kr@4)
|
||||
L6 = R5
|
||||
R6 = L5 ^ f3 (R5, km@5, kr@5)
|
||||
L7 = R6
|
||||
R7 = L6 ^ f1 (R6, km@6, kr@6)
|
||||
L8 = R7
|
||||
R8 = L7 ^ f2 (R7, km@7, kr@7)
|
||||
L9 = R8
|
||||
R9 = L8 ^ f3 (R8, km@8, kr@8)
|
||||
L10 = R9
|
||||
R10 = L9 ^ f1 (R9, km@9, kr@9)
|
||||
L11 = R10
|
||||
R11 = L10 ^ f2 (R10, km@10, kr@10)
|
||||
L12 = R11
|
||||
R12 = L11 ^ f3 (R11, km@11, kr@11)
|
||||
|
||||
blockEncrypt : {k} (16 >= k, k >= 5) => ([k*8],[64]) -> [64]
|
||||
blockEncrypt (k,plaintext) = if wid k > 80 then cast5_16 plaintext key else cast5_12 plaintext key
|
||||
where wid (x:[w]a) = `w
|
||||
key = expandKey k
|
||||
|
||||
f1, f2, f3 : ([32],[32],[5]) -> [32]
|
||||
f1 (d, kmi, kri) = ((s1@ia ^ s2@ib) - s3@ic) + s4@id where
|
||||
[ia,ib,ic,id] = split i
|
||||
i = (kmi + d) <<< kri
|
||||
|
||||
f2 (d, kmi, kri) = ((s1@ia - s2@ib) + s3@ic) ^ s4@id where
|
||||
[ia,ib,ic,id] = split i
|
||||
i = (kmi ^ d) <<< kri
|
||||
|
||||
f3 (d, kmi, kri) = ((s1@ia + s2@ib) ^ s3@ic) - s4@id where
|
||||
[ia,ib,ic,id] = split i
|
||||
i = (kmi - d) <<< kri
|
||||
|
||||
expandKey : {k} (16 >= k, k >= 5) => [k*8] -> ([16][32],[16][5])
|
||||
expandKey key = (firstHalf, secondHalf) where
|
||||
(firstHalf, newkey) = halfKeySchedule paddedKey
|
||||
secondHalf = [x@@[27..31] | x <- fst (halfKeySchedule newkey)]
|
||||
fst (x, y) = x
|
||||
paddedKey = key#zero
|
||||
|
||||
halfKeySchedule : [128] -> ([16][32],[128])
|
||||
halfKeySchedule key = ([K1,K2,K3,K4,K5,K6,K7,K8,K9,K10,K11,K12,K13,K14,K15,K16],newkey) where
|
||||
[x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,xA,xB,xC,xD,xE,xF] = split key
|
||||
[z0,z1,z2,z3] = split ((x0#x1#x2#x3) ^ s5@xD ^ s6@xF ^ s7@xC ^ s8@xE ^ s7@x8)
|
||||
[z4,z5,z6,z7] = split ((x8#x9#xA#xB) ^ s5@z0 ^ s6@z2 ^ s7@z1 ^ s8@z3 ^ s8@xA)
|
||||
[z8,z9,zA,zB] = split ((xC#xD#xE#xF) ^ s5@z7 ^ s6@z6 ^ s7@z5 ^ s8@z4 ^ s5@x9)
|
||||
[zC,zD,zE,zF] = split ((x4#x5#x6#x7) ^ s5@zA ^ s6@z9 ^ s7@zB ^ s8@z8 ^ s6@xB)
|
||||
K1 = s5@z8 ^ s6@z9 ^ s7@z7 ^ s8@z6 ^ s5@z2
|
||||
K2 = s5@zA ^ s6@zB ^ s7@z5 ^ s8@z4 ^ s6@z6
|
||||
K3 = s5@zC ^ s6@zD ^ s7@z3 ^ s8@z2 ^ s7@z9
|
||||
K4 = s5@zE ^ s6@zF ^ s7@z1 ^ s8@z0 ^ s8@zC
|
||||
[a0,a1,a2,a3] = split ((z8#z9#zA#zB) ^ s5@z5 ^ s6@z7 ^ s7@z4 ^ s8@z6 ^ s7@z0)
|
||||
[a4,a5,a6,a7] = split ((z0#z1#z2#z3) ^ s5@a0 ^ s6@a2 ^ s7@a1 ^ s8@a3 ^ s8@z2)
|
||||
[a8,a9,aA,aB] = split ((z4#z5#z6#z7) ^ s5@a7 ^ s6@a6 ^ s7@a5 ^ s8@a4 ^ s5@z1)
|
||||
[aC,aD,aE,aF] = split ((zC#zD#zE#zF) ^ s5@aA ^ s6@a9 ^ s7@aB ^ s8@a8 ^ s6@z3)
|
||||
K5 = s5@a3 ^ s6@a2 ^ s7@aC ^ s8@aD ^ s5@a8
|
||||
K6 = s5@a1 ^ s6@a0 ^ s7@aE ^ s8@aF ^ s6@aD
|
||||
K7 = s5@a7 ^ s6@a6 ^ s7@a8 ^ s8@a9 ^ s7@a3
|
||||
K8 = s5@a5 ^ s6@a4 ^ s7@aA ^ s8@aB ^ s8@a7
|
||||
[b0,b1,b2,b3] = split ((a0#a1#a2#a3) ^ s5@aD ^ s6@aF ^ s7@aC ^ s8@aE ^ s7@a8)
|
||||
[b4,b5,b6,b7] = split ((a8#a9#aA#aB) ^ s5@b0 ^ s6@b2 ^ s7@b1 ^ s8@b3 ^ s8@aA)
|
||||
[b8,b9,bA,bB] = split ((aC#aD#aE#aF) ^ s5@b7 ^ s6@b6 ^ s7@b5 ^ s8@b4 ^ s5@a9)
|
||||
[bC,bD,bE,bF] = split ((a4#a5#a6#a7) ^ s5@bA ^ s6@b9 ^ s7@bB ^ s8@b8 ^ s6@aB)
|
||||
K9 = s5@b3 ^ s6@b2 ^ s7@bC ^ s8@bD ^ s5@b9
|
||||
K10 = s5@b1 ^ s6@b0 ^ s7@bE ^ s8@bF ^ s6@bC
|
||||
K11 = s5@b7 ^ s6@b6 ^ s7@b8 ^ s8@b9 ^ s7@b2
|
||||
K12 = s5@b5 ^ s6@b4 ^ s7@bA ^ s8@bB ^ s8@b6
|
||||
[c0,c1,c2,c3] = split ((b8#b9#bA#bB) ^ s5@b5 ^ s6@b7 ^ s7@b4 ^ s8@b6 ^ s7@b0)
|
||||
[c4,c5,c6,c7] = split ((b0#b1#b2#b3) ^ s5@c0 ^ s6@c2 ^ s7@c1 ^ s8@c3 ^ s8@b2)
|
||||
[c8,c9,cA,cB] = split ((b4#b5#b6#b7) ^ s5@c7 ^ s6@c6 ^ s7@c5 ^ s8@c4 ^ s5@b1)
|
||||
[cC,cD,cE,cF] = split ((bC#bD#bE#bF) ^ s5@cA ^ s6@c9 ^ s7@cB ^ s8@c8 ^ s6@b3)
|
||||
K13 = s5@c8 ^ s6@c9 ^ s7@c7 ^ s8@c6 ^ s5@c3
|
||||
K14 = s5@cA ^ s6@cB ^ s7@c5 ^ s8@c4 ^ s6@c7
|
||||
K15 = s5@cC ^ s6@cD ^ s7@c3 ^ s8@c2 ^ s7@c8
|
||||
K16 = s5@cE ^ s6@cF ^ s7@c1 ^ s8@c0 ^ s8@cD
|
||||
newkey = c0#c1#c2#c3#c4#c5#c6#c7#c8#c9#cA#cB#cC#cD#cE#cF
|
||||
|
||||
// sboxes
|
||||
s1, s2, s3, s4, s5, s6, s7, s8 : [256][32]
|
||||
s1 = [
|
||||
0x30fb40d4, 0x9fa0ff0b, 0x6beccd2f, 0x3f258c7a, 0x1e213f2f, 0x9c004dd3, 0x6003e540, 0xcf9fc949,
|
||||
0xbfd4af27, 0x88bbbdb5, 0xe2034090, 0x98d09675, 0x6e63a0e0, 0x15c361d2, 0xc2e7661d, 0x22d4ff8e,
|
||||
0x28683b6f, 0xc07fd059, 0xff2379c8, 0x775f50e2, 0x43c340d3, 0xdf2f8656, 0x887ca41a, 0xa2d2bd2d,
|
||||
0xa1c9e0d6, 0x346c4819, 0x61b76d87, 0x22540f2f, 0x2abe32e1, 0xaa54166b, 0x22568e3a, 0xa2d341d0,
|
||||
0x66db40c8, 0xa784392f, 0x004dff2f, 0x2db9d2de, 0x97943fac, 0x4a97c1d8, 0x527644b7, 0xb5f437a7,
|
||||
0xb82cbaef, 0xd751d159, 0x6ff7f0ed, 0x5a097a1f, 0x827b68d0, 0x90ecf52e, 0x22b0c054, 0xbc8e5935,
|
||||
0x4b6d2f7f, 0x50bb64a2, 0xd2664910, 0xbee5812d, 0xb7332290, 0xe93b159f, 0xb48ee411, 0x4bff345d,
|
||||
0xfd45c240, 0xad31973f, 0xc4f6d02e, 0x55fc8165, 0xd5b1caad, 0xa1ac2dae, 0xa2d4b76d, 0xc19b0c50,
|
||||
0x882240f2, 0x0c6e4f38, 0xa4e4bfd7, 0x4f5ba272, 0x564c1d2f, 0xc59c5319, 0xb949e354, 0xb04669fe,
|
||||
0xb1b6ab8a, 0xc71358dd, 0x6385c545, 0x110f935d, 0x57538ad5, 0x6a390493, 0xe63d37e0, 0x2a54f6b3,
|
||||
0x3a787d5f, 0x6276a0b5, 0x19a6fcdf, 0x7a42206a, 0x29f9d4d5, 0xf61b1891, 0xbb72275e, 0xaa508167,
|
||||
0x38901091, 0xc6b505eb, 0x84c7cb8c, 0x2ad75a0f, 0x874a1427, 0xa2d1936b, 0x2ad286af, 0xaa56d291,
|
||||
0xd7894360, 0x425c750d, 0x93b39e26, 0x187184c9, 0x6c00b32d, 0x73e2bb14, 0xa0bebc3c, 0x54623779,
|
||||
0x64459eab, 0x3f328b82, 0x7718cf82, 0x59a2cea6, 0x04ee002e, 0x89fe78e6, 0x3fab0950, 0x325ff6c2,
|
||||
0x81383f05, 0x6963c5c8, 0x76cb5ad6, 0xd49974c9, 0xca180dcf, 0x380782d5, 0xc7fa5cf6, 0x8ac31511,
|
||||
0x35e79e13, 0x47da91d0, 0xf40f9086, 0xa7e2419e, 0x31366241, 0x051ef495, 0xaa573b04, 0x4a805d8d,
|
||||
0x548300d0, 0x00322a3c, 0xbf64cddf, 0xba57a68e, 0x75c6372b, 0x50afd341, 0xa7c13275, 0x915a0bf5,
|
||||
0x6b54bfab, 0x2b0b1426, 0xab4cc9d7, 0x449ccd82, 0xf7fbf265, 0xab85c5f3, 0x1b55db94, 0xaad4e324,
|
||||
0xcfa4bd3f, 0x2deaa3e2, 0x9e204d02, 0xc8bd25ac, 0xeadf55b3, 0xd5bd9e98, 0xe31231b2, 0x2ad5ad6c,
|
||||
0x954329de, 0xadbe4528, 0xd8710f69, 0xaa51c90f, 0xaa786bf6, 0x22513f1e, 0xaa51a79b, 0x2ad344cc,
|
||||
0x7b5a41f0, 0xd37cfbad, 0x1b069505, 0x41ece491, 0xb4c332e6, 0x032268d4, 0xc9600acc, 0xce387e6d,
|
||||
0xbf6bb16c, 0x6a70fb78, 0x0d03d9c9, 0xd4df39de, 0xe01063da, 0x4736f464, 0x5ad328d8, 0xb347cc96,
|
||||
0x75bb0fc3, 0x98511bfb, 0x4ffbcc35, 0xb58bcf6a, 0xe11f0abc, 0xbfc5fe4a, 0xa70aec10, 0xac39570a,
|
||||
0x3f04442f, 0x6188b153, 0xe0397a2e, 0x5727cb79, 0x9ceb418f, 0x1cacd68d, 0x2ad37c96, 0x0175cb9d,
|
||||
0xc69dff09, 0xc75b65f0, 0xd9db40d8, 0xec0e7779, 0x4744ead4, 0xb11c3274, 0xdd24cb9e, 0x7e1c54bd,
|
||||
0xf01144f9, 0xd2240eb1, 0x9675b3fd, 0xa3ac3755, 0xd47c27af, 0x51c85f4d, 0x56907596, 0xa5bb15e6,
|
||||
0x580304f0, 0xca042cf1, 0x011a37ea, 0x8dbfaadb, 0x35ba3e4a, 0x3526ffa0, 0xc37b4d09, 0xbc306ed9,
|
||||
0x98a52666, 0x5648f725, 0xff5e569d, 0x0ced63d0, 0x7c63b2cf, 0x700b45e1, 0xd5ea50f1, 0x85a92872,
|
||||
0xaf1fbda7, 0xd4234870, 0xa7870bf3, 0x2d3b4d79, 0x42e04198, 0x0cd0ede7, 0x26470db8, 0xf881814c,
|
||||
0x474d6ad7, 0x7c0c5e5c, 0xd1231959, 0x381b7298, 0xf5d2f4db, 0xab838653, 0x6e2f1e23, 0x83719c9e,
|
||||
0xbd91e046, 0x9a56456e, 0xdc39200c, 0x20c8c571, 0x962bda1c, 0xe1e696ff, 0xb141ab08, 0x7cca89b9,
|
||||
0x1a69e783, 0x02cc4843, 0xa2f7c579, 0x429ef47d, 0x427b169c, 0x5ac9f049, 0xdd8f0f00, 0x5c8165bf
|
||||
]
|
||||
s2 = [
|
||||
0x1f201094, 0xef0ba75b, 0x69e3cf7e, 0x393f4380, 0xfe61cf7a, 0xeec5207a, 0x55889c94, 0x72fc0651,
|
||||
0xada7ef79, 0x4e1d7235, 0xd55a63ce, 0xde0436ba, 0x99c430ef, 0x5f0c0794, 0x18dcdb7d, 0xa1d6eff3,
|
||||
0xa0b52f7b, 0x59e83605, 0xee15b094, 0xe9ffd909, 0xdc440086, 0xef944459, 0xba83ccb3, 0xe0c3cdfb,
|
||||
0xd1da4181, 0x3b092ab1, 0xf997f1c1, 0xa5e6cf7b, 0x01420ddb, 0xe4e7ef5b, 0x25a1ff41, 0xe180f806,
|
||||
0x1fc41080, 0x179bee7a, 0xd37ac6a9, 0xfe5830a4, 0x98de8b7f, 0x77e83f4e, 0x79929269, 0x24fa9f7b,
|
||||
0xe113c85b, 0xacc40083, 0xd7503525, 0xf7ea615f, 0x62143154, 0x0d554b63, 0x5d681121, 0xc866c359,
|
||||
0x3d63cf73, 0xcee234c0, 0xd4d87e87, 0x5c672b21, 0x071f6181, 0x39f7627f, 0x361e3084, 0xe4eb573b,
|
||||
0x602f64a4, 0xd63acd9c, 0x1bbc4635, 0x9e81032d, 0x2701f50c, 0x99847ab4, 0xa0e3df79, 0xba6cf38c,
|
||||
0x10843094, 0x2537a95e, 0xf46f6ffe, 0xa1ff3b1f, 0x208cfb6a, 0x8f458c74, 0xd9e0a227, 0x4ec73a34,
|
||||
0xfc884f69, 0x3e4de8df, 0xef0e0088, 0x3559648d, 0x8a45388c, 0x1d804366, 0x721d9bfd, 0xa58684bb,
|
||||
0xe8256333, 0x844e8212, 0x128d8098, 0xfed33fb4, 0xce280ae1, 0x27e19ba5, 0xd5a6c252, 0xe49754bd,
|
||||
0xc5d655dd, 0xeb667064, 0x77840b4d, 0xa1b6a801, 0x84db26a9, 0xe0b56714, 0x21f043b7, 0xe5d05860,
|
||||
0x54f03084, 0x066ff472, 0xa31aa153, 0xdadc4755, 0xb5625dbf, 0x68561be6, 0x83ca6b94, 0x2d6ed23b,
|
||||
0xeccf01db, 0xa6d3d0ba, 0xb6803d5c, 0xaf77a709, 0x33b4a34c, 0x397bc8d6, 0x5ee22b95, 0x5f0e5304,
|
||||
0x81ed6f61, 0x20e74364, 0xb45e1378, 0xde18639b, 0x881ca122, 0xb96726d1, 0x8049a7e8, 0x22b7da7b,
|
||||
0x5e552d25, 0x5272d237, 0x79d2951c, 0xc60d894c, 0x488cb402, 0x1ba4fe5b, 0xa4b09f6b, 0x1ca815cf,
|
||||
0xa20c3005, 0x8871df63, 0xb9de2fcb, 0x0cc6c9e9, 0x0beeff53, 0xe3214517, 0xb4542835, 0x9f63293c,
|
||||
0xee41e729, 0x6e1d2d7c, 0x50045286, 0x1e6685f3, 0xf33401c6, 0x30a22c95, 0x31a70850, 0x60930f13,
|
||||
0x73f98417, 0xa1269859, 0xec645c44, 0x52c877a9, 0xcdff33a6, 0xa02b1741, 0x7cbad9a2, 0x2180036f,
|
||||
0x50d99c08, 0xcb3f4861, 0xc26bd765, 0x64a3f6ab, 0x80342676, 0x25a75e7b, 0xe4e6d1fc, 0x20c710e6,
|
||||
0xcdf0b680, 0x17844d3b, 0x31eef84d, 0x7e0824e4, 0x2ccb49eb, 0x846a3bae, 0x8ff77888, 0xee5d60f6,
|
||||
0x7af75673, 0x2fdd5cdb, 0xa11631c1, 0x30f66f43, 0xb3faec54, 0x157fd7fa, 0xef8579cc, 0xd152de58,
|
||||
0xdb2ffd5e, 0x8f32ce19, 0x306af97a, 0x02f03ef8, 0x99319ad5, 0xc242fa0f, 0xa7e3ebb0, 0xc68e4906,
|
||||
0xb8da230c, 0x80823028, 0xdcdef3c8, 0xd35fb171, 0x088a1bc8, 0xbec0c560, 0x61a3c9e8, 0xbca8f54d,
|
||||
0xc72feffa, 0x22822e99, 0x82c570b4, 0xd8d94e89, 0x8b1c34bc, 0x301e16e6, 0x273be979, 0xb0ffeaa6,
|
||||
0x61d9b8c6, 0x00b24869, 0xb7ffce3f, 0x08dc283b, 0x43daf65a, 0xf7e19798, 0x7619b72f, 0x8f1c9ba4,
|
||||
0xdc8637a0, 0x16a7d3b1, 0x9fc393b7, 0xa7136eeb, 0xc6bcc63e, 0x1a513742, 0xef6828bc, 0x520365d6,
|
||||
0x2d6a77ab, 0x3527ed4b, 0x821fd216, 0x095c6e2e, 0xdb92f2fb, 0x5eea29cb, 0x145892f5, 0x91584f7f,
|
||||
0x5483697b, 0x2667a8cc, 0x85196048, 0x8c4bacea, 0x833860d4, 0x0d23e0f9, 0x6c387e8a, 0x0ae6d249,
|
||||
0xb284600c, 0xd835731d, 0xdcb1c647, 0xac4c56ea, 0x3ebd81b3, 0x230eabb0, 0x6438bc87, 0xf0b5b1fa,
|
||||
0x8f5ea2b3, 0xfc184642, 0x0a036b7a, 0x4fb089bd, 0x649da589, 0xa345415e, 0x5c038323, 0x3e5d3bb9,
|
||||
0x43d79572, 0x7e6dd07c, 0x06dfdf1e, 0x6c6cc4ef, 0x7160a539, 0x73bfbe70, 0x83877605, 0x4523ecf1
|
||||
]
|
||||
s3 = [
|
||||
0x8defc240, 0x25fa5d9f, 0xeb903dbf, 0xe810c907, 0x47607fff, 0x369fe44b, 0x8c1fc644, 0xaececa90,
|
||||
0xbeb1f9bf, 0xeefbcaea, 0xe8cf1950, 0x51df07ae, 0x920e8806, 0xf0ad0548, 0xe13c8d83, 0x927010d5,
|
||||
0x11107d9f, 0x07647db9, 0xb2e3e4d4, 0x3d4f285e, 0xb9afa820, 0xfade82e0, 0xa067268b, 0x8272792e,
|
||||
0x553fb2c0, 0x489ae22b, 0xd4ef9794, 0x125e3fbc, 0x21fffcee, 0x825b1bfd, 0x9255c5ed, 0x1257a240,
|
||||
0x4e1a8302, 0xbae07fff, 0x528246e7, 0x8e57140e, 0x3373f7bf, 0x8c9f8188, 0xa6fc4ee8, 0xc982b5a5,
|
||||
0xa8c01db7, 0x579fc264, 0x67094f31, 0xf2bd3f5f, 0x40fff7c1, 0x1fb78dfc, 0x8e6bd2c1, 0x437be59b,
|
||||
0x99b03dbf, 0xb5dbc64b, 0x638dc0e6, 0x55819d99, 0xa197c81c, 0x4a012d6e, 0xc5884a28, 0xccc36f71,
|
||||
0xb843c213, 0x6c0743f1, 0x8309893c, 0x0feddd5f, 0x2f7fe850, 0xd7c07f7e, 0x02507fbf, 0x5afb9a04,
|
||||
0xa747d2d0, 0x1651192e, 0xaf70bf3e, 0x58c31380, 0x5f98302e, 0x727cc3c4, 0x0a0fb402, 0x0f7fef82,
|
||||
0x8c96fdad, 0x5d2c2aae, 0x8ee99a49, 0x50da88b8, 0x8427f4a0, 0x1eac5790, 0x796fb449, 0x8252dc15,
|
||||
0xefbd7d9b, 0xa672597d, 0xada840d8, 0x45f54504, 0xfa5d7403, 0xe83ec305, 0x4f91751a, 0x925669c2,
|
||||
0x23efe941, 0xa903f12e, 0x60270df2, 0x0276e4b6, 0x94fd6574, 0x927985b2, 0x8276dbcb, 0x02778176,
|
||||
0xf8af918d, 0x4e48f79e, 0x8f616ddf, 0xe29d840e, 0x842f7d83, 0x340ce5c8, 0x96bbb682, 0x93b4b148,
|
||||
0xef303cab, 0x984faf28, 0x779faf9b, 0x92dc560d, 0x224d1e20, 0x8437aa88, 0x7d29dc96, 0x2756d3dc,
|
||||
0x8b907cee, 0xb51fd240, 0xe7c07ce3, 0xe566b4a1, 0xc3e9615e, 0x3cf8209d, 0x6094d1e3, 0xcd9ca341,
|
||||
0x5c76460e, 0x00ea983b, 0xd4d67881, 0xfd47572c, 0xf76cedd9, 0xbda8229c, 0x127dadaa, 0x438a074e,
|
||||
0x1f97c090, 0x081bdb8a, 0x93a07ebe, 0xb938ca15, 0x97b03cff, 0x3dc2c0f8, 0x8d1ab2ec, 0x64380e51,
|
||||
0x68cc7bfb, 0xd90f2788, 0x12490181, 0x5de5ffd4, 0xdd7ef86a, 0x76a2e214, 0xb9a40368, 0x925d958f,
|
||||
0x4b39fffa, 0xba39aee9, 0xa4ffd30b, 0xfaf7933b, 0x6d498623, 0x193cbcfa, 0x27627545, 0x825cf47a,
|
||||
0x61bd8ba0, 0xd11e42d1, 0xcead04f4, 0x127ea392, 0x10428db7, 0x8272a972, 0x9270c4a8, 0x127de50b,
|
||||
0x285ba1c8, 0x3c62f44f, 0x35c0eaa5, 0xe805d231, 0x428929fb, 0xb4fcdf82, 0x4fb66a53, 0x0e7dc15b,
|
||||
0x1f081fab, 0x108618ae, 0xfcfd086d, 0xf9ff2889, 0x694bcc11, 0x236a5cae, 0x12deca4d, 0x2c3f8cc5,
|
||||
0xd2d02dfe, 0xf8ef5896, 0xe4cf52da, 0x95155b67, 0x494a488c, 0xb9b6a80c, 0x5c8f82bc, 0x89d36b45,
|
||||
0x3a609437, 0xec00c9a9, 0x44715253, 0x0a874b49, 0xd773bc40, 0x7c34671c, 0x02717ef6, 0x4feb5536,
|
||||
0xa2d02fff, 0xd2bf60c4, 0xd43f03c0, 0x50b4ef6d, 0x07478cd1, 0x006e1888, 0xa2e53f55, 0xb9e6d4bc,
|
||||
0xa2048016, 0x97573833, 0xd7207d67, 0xde0f8f3d, 0x72f87b33, 0xabcc4f33, 0x7688c55d, 0x7b00a6b0,
|
||||
0x947b0001, 0x570075d2, 0xf9bb88f8, 0x8942019e, 0x4264a5ff, 0x856302e0, 0x72dbd92b, 0xee971b69,
|
||||
0x6ea22fde, 0x5f08ae2b, 0xaf7a616d, 0xe5c98767, 0xcf1febd2, 0x61efc8c2, 0xf1ac2571, 0xcc8239c2,
|
||||
0x67214cb8, 0xb1e583d1, 0xb7dc3e62, 0x7f10bdce, 0xf90a5c38, 0x0ff0443d, 0x606e6dc6, 0x60543a49,
|
||||
0x5727c148, 0x2be98a1d, 0x8ab41738, 0x20e1be24, 0xaf96da0f, 0x68458425, 0x99833be5, 0x600d457d,
|
||||
0x282f9350, 0x8334b362, 0xd91d1120, 0x2b6d8da0, 0x642b1e31, 0x9c305a00, 0x52bce688, 0x1b03588a,
|
||||
0xf7baefd5, 0x4142ed9c, 0xa4315c11, 0x83323ec5, 0xdfef4636, 0xa133c501, 0xe9d3531c, 0xee353783
|
||||
]
|
||||
s4 = [
|
||||
0x9db30420, 0x1fb6e9de, 0xa7be7bef, 0xd273a298, 0x4a4f7bdb, 0x64ad8c57, 0x85510443, 0xfa020ed1,
|
||||
0x7e287aff, 0xe60fb663, 0x095f35a1, 0x79ebf120, 0xfd059d43, 0x6497b7b1, 0xf3641f63, 0x241e4adf,
|
||||
0x28147f5f, 0x4fa2b8cd, 0xc9430040, 0x0cc32220, 0xfdd30b30, 0xc0a5374f, 0x1d2d00d9, 0x24147b15,
|
||||
0xee4d111a, 0x0fca5167, 0x71ff904c, 0x2d195ffe, 0x1a05645f, 0x0c13fefe, 0x081b08ca, 0x05170121,
|
||||
0x80530100, 0xe83e5efe, 0xac9af4f8, 0x7fe72701, 0xd2b8ee5f, 0x06df4261, 0xbb9e9b8a, 0x7293ea25,
|
||||
0xce84ffdf, 0xf5718801, 0x3dd64b04, 0xa26f263b, 0x7ed48400, 0x547eebe6, 0x446d4ca0, 0x6cf3d6f5,
|
||||
0x2649abdf, 0xaea0c7f5, 0x36338cc1, 0x503f7e93, 0xd3772061, 0x11b638e1, 0x72500e03, 0xf80eb2bb,
|
||||
0xabe0502e, 0xec8d77de, 0x57971e81, 0xe14f6746, 0xc9335400, 0x6920318f, 0x081dbb99, 0xffc304a5,
|
||||
0x4d351805, 0x7f3d5ce3, 0xa6c866c6, 0x5d5bcca9, 0xdaec6fea, 0x9f926f91, 0x9f46222f, 0x3991467d,
|
||||
0xa5bf6d8e, 0x1143c44f, 0x43958302, 0xd0214eeb, 0x022083b8, 0x3fb6180c, 0x18f8931e, 0x281658e6,
|
||||
0x26486e3e, 0x8bd78a70, 0x7477e4c1, 0xb506e07c, 0xf32d0a25, 0x79098b02, 0xe4eabb81, 0x28123b23,
|
||||
0x69dead38, 0x1574ca16, 0xdf871b62, 0x211c40b7, 0xa51a9ef9, 0x0014377b, 0x041e8ac8, 0x09114003,
|
||||
0xbd59e4d2, 0xe3d156d5, 0x4fe876d5, 0x2f91a340, 0x557be8de, 0x00eae4a7, 0x0ce5c2ec, 0x4db4bba6,
|
||||
0xe756bdff, 0xdd3369ac, 0xec17b035, 0x06572327, 0x99afc8b0, 0x56c8c391, 0x6b65811c, 0x5e146119,
|
||||
0x6e85cb75, 0xbe07c002, 0xc2325577, 0x893ff4ec, 0x5bbfc92d, 0xd0ec3b25, 0xb7801ab7, 0x8d6d3b24,
|
||||
0x20c763ef, 0xc366a5fc, 0x9c382880, 0x0ace3205, 0xaac9548a, 0xeca1d7c7, 0x041afa32, 0x1d16625a,
|
||||
0x6701902c, 0x9b757a54, 0x31d477f7, 0x9126b031, 0x36cc6fdb, 0xc70b8b46, 0xd9e66a48, 0x56e55a79,
|
||||
0x026a4ceb, 0x52437eff, 0x2f8f76b4, 0x0df980a5, 0x8674cde3, 0xedda04eb, 0x17a9be04, 0x2c18f4df,
|
||||
0xb7747f9d, 0xab2af7b4, 0xefc34d20, 0x2e096b7c, 0x1741a254, 0xe5b6a035, 0x213d42f6, 0x2c1c7c26,
|
||||
0x61c2f50f, 0x6552daf9, 0xd2c231f8, 0x25130f69, 0xd8167fa2, 0x0418f2c8, 0x001a96a6, 0x0d1526ab,
|
||||
0x63315c21, 0x5e0a72ec, 0x49bafefd, 0x187908d9, 0x8d0dbd86, 0x311170a7, 0x3e9b640c, 0xcc3e10d7,
|
||||
0xd5cad3b6, 0x0caec388, 0xf73001e1, 0x6c728aff, 0x71eae2a1, 0x1f9af36e, 0xcfcbd12f, 0xc1de8417,
|
||||
0xac07be6b, 0xcb44a1d8, 0x8b9b0f56, 0x013988c3, 0xb1c52fca, 0xb4be31cd, 0xd8782806, 0x12a3a4e2,
|
||||
0x6f7de532, 0x58fd7eb6, 0xd01ee900, 0x24adffc2, 0xf4990fc5, 0x9711aac5, 0x001d7b95, 0x82e5e7d2,
|
||||
0x109873f6, 0x00613096, 0xc32d9521, 0xada121ff, 0x29908415, 0x7fbb977f, 0xaf9eb3db, 0x29c9ed2a,
|
||||
0x5ce2a465, 0xa730f32c, 0xd0aa3fe8, 0x8a5cc091, 0xd49e2ce7, 0x0ce454a9, 0xd60acd86, 0x015f1919,
|
||||
0x77079103, 0xdea03af6, 0x78a8565e, 0xdee356df, 0x21f05cbe, 0x8b75e387, 0xb3c50651, 0xb8a5c3ef,
|
||||
0xd8eeb6d2, 0xe523be77, 0xc2154529, 0x2f69efdf, 0xafe67afb, 0xf470c4b2, 0xf3e0eb5b, 0xd6cc9876,
|
||||
0x39e4460c, 0x1fda8538, 0x1987832f, 0xca007367, 0xa99144f8, 0x296b299e, 0x492fc295, 0x9266beab,
|
||||
0xb5676e69, 0x9bd3ddda, 0xdf7e052f, 0xdb25701c, 0x1b5e51ee, 0xf65324e6, 0x6afce36c, 0x0316cc04,
|
||||
0x8644213e, 0xb7dc59d0, 0x7965291f, 0xccd6fd43, 0x41823979, 0x932bcdf6, 0xb657c34d, 0x4edfd282,
|
||||
0x7ae5290c, 0x3cb9536b, 0x851e20fe, 0x9833557e, 0x13ecf0b0, 0xd3ffb372, 0x3f85c5c1, 0x0aef7ed2
|
||||
]
|
||||
s5 = [
|
||||
0x7ec90c04, 0x2c6e74b9, 0x9b0e66df, 0xa6337911, 0xb86a7fff, 0x1dd358f5, 0x44dd9d44, 0x1731167f,
|
||||
0x08fbf1fa, 0xe7f511cc, 0xd2051b00, 0x735aba00, 0x2ab722d8, 0x386381cb, 0xacf6243a, 0x69befd7a,
|
||||
0xe6a2e77f, 0xf0c720cd, 0xc4494816, 0xccf5c180, 0x38851640, 0x15b0a848, 0xe68b18cb, 0x4caadeff,
|
||||
0x5f480a01, 0x0412b2aa, 0x259814fc, 0x41d0efe2, 0x4e40b48d, 0x248eb6fb, 0x8dba1cfe, 0x41a99b02,
|
||||
0x1a550a04, 0xba8f65cb, 0x7251f4e7, 0x95a51725, 0xc106ecd7, 0x97a5980a, 0xc539b9aa, 0x4d79fe6a,
|
||||
0xf2f3f763, 0x68af8040, 0xed0c9e56, 0x11b4958b, 0xe1eb5a88, 0x8709e6b0, 0xd7e07156, 0x4e29fea7,
|
||||
0x6366e52d, 0x02d1c000, 0xc4ac8e05, 0x9377f571, 0x0c05372a, 0x578535f2, 0x2261be02, 0xd642a0c9,
|
||||
0xdf13a280, 0x74b55bd2, 0x682199c0, 0xd421e5ec, 0x53fb3ce8, 0xc8adedb3, 0x28a87fc9, 0x3d959981,
|
||||
0x5c1ff900, 0xfe38d399, 0x0c4eff0b, 0x062407ea, 0xaa2f4fb1, 0x4fb96976, 0x90c79505, 0xb0a8a774,
|
||||
0xef55a1ff, 0xe59ca2c2, 0xa6b62d27, 0xe66a4263, 0xdf65001f, 0x0ec50966, 0xdfdd55bc, 0x29de0655,
|
||||
0x911e739a, 0x17af8975, 0x32c7911c, 0x89f89468, 0x0d01e980, 0x524755f4, 0x03b63cc9, 0x0cc844b2,
|
||||
0xbcf3f0aa, 0x87ac36e9, 0xe53a7426, 0x01b3d82b, 0x1a9e7449, 0x64ee2d7e, 0xcddbb1da, 0x01c94910,
|
||||
0xb868bf80, 0x0d26f3fd, 0x9342ede7, 0x04a5c284, 0x636737b6, 0x50f5b616, 0xf24766e3, 0x8eca36c1,
|
||||
0x136e05db, 0xfef18391, 0xfb887a37, 0xd6e7f7d4, 0xc7fb7dc9, 0x3063fcdf, 0xb6f589de, 0xec2941da,
|
||||
0x26e46695, 0xb7566419, 0xf654efc5, 0xd08d58b7, 0x48925401, 0xc1bacb7f, 0xe5ff550f, 0xb6083049,
|
||||
0x5bb5d0e8, 0x87d72e5a, 0xab6a6ee1, 0x223a66ce, 0xc62bf3cd, 0x9e0885f9, 0x68cb3e47, 0x086c010f,
|
||||
0xa21de820, 0xd18b69de, 0xf3f65777, 0xfa02c3f6, 0x407edac3, 0xcbb3d550, 0x1793084d, 0xb0d70eba,
|
||||
0x0ab378d5, 0xd951fb0c, 0xded7da56, 0x4124bbe4, 0x94ca0b56, 0x0f5755d1, 0xe0e1e56e, 0x6184b5be,
|
||||
0x580a249f, 0x94f74bc0, 0xe327888e, 0x9f7b5561, 0xc3dc0280, 0x05687715, 0x646c6bd7, 0x44904db3,
|
||||
0x66b4f0a3, 0xc0f1648a, 0x697ed5af, 0x49e92ff6, 0x309e374f, 0x2cb6356a, 0x85808573, 0x4991f840,
|
||||
0x76f0ae02, 0x083be84d, 0x28421c9a, 0x44489406, 0x736e4cb8, 0xc1092910, 0x8bc95fc6, 0x7d869cf4,
|
||||
0x134f616f, 0x2e77118d, 0xb31b2be1, 0xaa90b472, 0x3ca5d717, 0x7d161bba, 0x9cad9010, 0xaf462ba2,
|
||||
0x9fe459d2, 0x45d34559, 0xd9f2da13, 0xdbc65487, 0xf3e4f94e, 0x176d486f, 0x097c13ea, 0x631da5c7,
|
||||
0x445f7382, 0x175683f4, 0xcdc66a97, 0x70be0288, 0xb3cdcf72, 0x6e5dd2f3, 0x20936079, 0x459b80a5,
|
||||
0xbe60e2db, 0xa9c23101, 0xeba5315c, 0x224e42f2, 0x1c5c1572, 0xf6721b2c, 0x1ad2fff3, 0x8c25404e,
|
||||
0x324ed72f, 0x4067b7fd, 0x0523138e, 0x5ca3bc78, 0xdc0fd66e, 0x75922283, 0x784d6b17, 0x58ebb16e,
|
||||
0x44094f85, 0x3f481d87, 0xfcfeae7b, 0x77b5ff76, 0x8c2302bf, 0xaaf47556, 0x5f46b02a, 0x2b092801,
|
||||
0x3d38f5f7, 0x0ca81f36, 0x52af4a8a, 0x66d5e7c0, 0xdf3b0874, 0x95055110, 0x1b5ad7a8, 0xf61ed5ad,
|
||||
0x6cf6e479, 0x20758184, 0xd0cefa65, 0x88f7be58, 0x4a046826, 0x0ff6f8f3, 0xa09c7f70, 0x5346aba0,
|
||||
0x5ce96c28, 0xe176eda3, 0x6bac307f, 0x376829d2, 0x85360fa9, 0x17e3fe2a, 0x24b79767, 0xf5a96b20,
|
||||
0xd6cd2595, 0x68ff1ebf, 0x7555442c, 0xf19f06be, 0xf9e0659a, 0xeeb9491d, 0x34010718, 0xbb30cab8,
|
||||
0xe822fe15, 0x88570983, 0x750e6249, 0xda627e55, 0x5e76ffa8, 0xb1534546, 0x6d47de08, 0xefe9e7d4
|
||||
]
|
||||
s6 = [
|
||||
0xf6fa8f9d, 0x2cac6ce1, 0x4ca34867, 0xe2337f7c, 0x95db08e7, 0x016843b4, 0xeced5cbc, 0x325553ac,
|
||||
0xbf9f0960, 0xdfa1e2ed, 0x83f0579d, 0x63ed86b9, 0x1ab6a6b8, 0xde5ebe39, 0xf38ff732, 0x8989b138,
|
||||
0x33f14961, 0xc01937bd, 0xf506c6da, 0xe4625e7e, 0xa308ea99, 0x4e23e33c, 0x79cbd7cc, 0x48a14367,
|
||||
0xa3149619, 0xfec94bd5, 0xa114174a, 0xeaa01866, 0xa084db2d, 0x09a8486f, 0xa888614a, 0x2900af98,
|
||||
0x01665991, 0xe1992863, 0xc8f30c60, 0x2e78ef3c, 0xd0d51932, 0xcf0fec14, 0xf7ca07d2, 0xd0a82072,
|
||||
0xfd41197e, 0x9305a6b0, 0xe86be3da, 0x74bed3cd, 0x372da53c, 0x4c7f4448, 0xdab5d440, 0x6dba0ec3,
|
||||
0x083919a7, 0x9fbaeed9, 0x49dbcfb0, 0x4e670c53, 0x5c3d9c01, 0x64bdb941, 0x2c0e636a, 0xba7dd9cd,
|
||||
0xea6f7388, 0xe70bc762, 0x35f29adb, 0x5c4cdd8d, 0xf0d48d8c, 0xb88153e2, 0x08a19866, 0x1ae2eac8,
|
||||
0x284caf89, 0xaa928223, 0x9334be53, 0x3b3a21bf, 0x16434be3, 0x9aea3906, 0xefe8c36e, 0xf890cdd9,
|
||||
0x80226dae, 0xc340a4a3, 0xdf7e9c09, 0xa694a807, 0x5b7c5ecc, 0x221db3a6, 0x9a69a02f, 0x68818a54,
|
||||
0xceb2296f, 0x53c0843a, 0xfe893655, 0x25bfe68a, 0xb4628abc, 0xcf222ebf, 0x25ac6f48, 0xa9a99387,
|
||||
0x53bddb65, 0xe76ffbe7, 0xe967fd78, 0x0ba93563, 0x8e342bc1, 0xe8a11be9, 0x4980740d, 0xc8087dfc,
|
||||
0x8de4bf99, 0xa11101a0, 0x7fd37975, 0xda5a26c0, 0xe81f994f, 0x9528cd89, 0xfd339fed, 0xb87834bf,
|
||||
0x5f04456d, 0x22258698, 0xc9c4c83b, 0x2dc156be, 0x4f628daa, 0x57f55ec5, 0xe2220abe, 0xd2916ebf,
|
||||
0x4ec75b95, 0x24f2c3c0, 0x42d15d99, 0xcd0d7fa0, 0x7b6e27ff, 0xa8dc8af0, 0x7345c106, 0xf41e232f,
|
||||
0x35162386, 0xe6ea8926, 0x3333b094, 0x157ec6f2, 0x372b74af, 0x692573e4, 0xe9a9d848, 0xf3160289,
|
||||
0x3a62ef1d, 0xa787e238, 0xf3a5f676, 0x74364853, 0x20951063, 0x4576698d, 0xb6fad407, 0x592af950,
|
||||
0x36f73523, 0x4cfb6e87, 0x7da4cec0, 0x6c152daa, 0xcb0396a8, 0xc50dfe5d, 0xfcd707ab, 0x0921c42f,
|
||||
0x89dff0bb, 0x5fe2be78, 0x448f4f33, 0x754613c9, 0x2b05d08d, 0x48b9d585, 0xdc049441, 0xc8098f9b,
|
||||
0x7dede786, 0xc39a3373, 0x42410005, 0x6a091751, 0x0ef3c8a6, 0x890072d6, 0x28207682, 0xa9a9f7be,
|
||||
0xbf32679d, 0xd45b5b75, 0xb353fd00, 0xcbb0e358, 0x830f220a, 0x1f8fb214, 0xd372cf08, 0xcc3c4a13,
|
||||
0x8cf63166, 0x061c87be, 0x88c98f88, 0x6062e397, 0x47cf8e7a, 0xb6c85283, 0x3cc2acfb, 0x3fc06976,
|
||||
0x4e8f0252, 0x64d8314d, 0xda3870e3, 0x1e665459, 0xc10908f0, 0x513021a5, 0x6c5b68b7, 0x822f8aa0,
|
||||
0x3007cd3e, 0x74719eef, 0xdc872681, 0x073340d4, 0x7e432fd9, 0x0c5ec241, 0x8809286c, 0xf592d891,
|
||||
0x08a930f6, 0x957ef305, 0xb7fbffbd, 0xc266e96f, 0x6fe4ac98, 0xb173ecc0, 0xbc60b42a, 0x953498da,
|
||||
0xfba1ae12, 0x2d4bd736, 0x0f25faab, 0xa4f3fceb, 0xe2969123, 0x257f0c3d, 0x9348af49, 0x361400bc,
|
||||
0xe8816f4a, 0x3814f200, 0xa3f94043, 0x9c7a54c2, 0xbc704f57, 0xda41e7f9, 0xc25ad33a, 0x54f4a084,
|
||||
0xb17f5505, 0x59357cbe, 0xedbd15c8, 0x7f97c5ab, 0xba5ac7b5, 0xb6f6deaf, 0x3a479c3a, 0x5302da25,
|
||||
0x653d7e6a, 0x54268d49, 0x51a477ea, 0x5017d55b, 0xd7d25d88, 0x44136c76, 0x0404a8c8, 0xb8e5a121,
|
||||
0xb81a928a, 0x60ed5869, 0x97c55b96, 0xeaec991b, 0x29935913, 0x01fdb7f1, 0x088e8dfa, 0x9ab6f6f5,
|
||||
0x3b4cbf9f, 0x4a5de3ab, 0xe6051d35, 0xa0e1d855, 0xd36b4cf1, 0xf544edeb, 0xb0e93524, 0xbebb8fbd,
|
||||
0xa2d762cf, 0x49c92f54, 0x38b5f331, 0x7128a454, 0x48392905, 0xa65b1db8, 0x851c97bd, 0xd675cf2f
|
||||
]
|
||||
s7 = [
|
||||
0x85e04019, 0x332bf567, 0x662dbfff, 0xcfc65693, 0x2a8d7f6f, 0xab9bc912, 0xde6008a1, 0x2028da1f,
|
||||
0x0227bce7, 0x4d642916, 0x18fac300, 0x50f18b82, 0x2cb2cb11, 0xb232e75c, 0x4b3695f2, 0xb28707de,
|
||||
0xa05fbcf6, 0xcd4181e9, 0xe150210c, 0xe24ef1bd, 0xb168c381, 0xfde4e789, 0x5c79b0d8, 0x1e8bfd43,
|
||||
0x4d495001, 0x38be4341, 0x913cee1d, 0x92a79c3f, 0x089766be, 0xbaeeadf4, 0x1286becf, 0xb6eacb19,
|
||||
0x2660c200, 0x7565bde4, 0x64241f7a, 0x8248dca9, 0xc3b3ad66, 0x28136086, 0x0bd8dfa8, 0x356d1cf2,
|
||||
0x107789be, 0xb3b2e9ce, 0x0502aa8f, 0x0bc0351e, 0x166bf52a, 0xeb12ff82, 0xe3486911, 0xd34d7516,
|
||||
0x4e7b3aff, 0x5f43671b, 0x9cf6e037, 0x4981ac83, 0x334266ce, 0x8c9341b7, 0xd0d854c0, 0xcb3a6c88,
|
||||
0x47bc2829, 0x4725ba37, 0xa66ad22b, 0x7ad61f1e, 0x0c5cbafa, 0x4437f107, 0xb6e79962, 0x42d2d816,
|
||||
0x0a961288, 0xe1a5c06e, 0x13749e67, 0x72fc081a, 0xb1d139f7, 0xf9583745, 0xcf19df58, 0xbec3f756,
|
||||
0xc06eba30, 0x07211b24, 0x45c28829, 0xc95e317f, 0xbc8ec511, 0x38bc46e9, 0xc6e6fa14, 0xbae8584a,
|
||||
0xad4ebc46, 0x468f508b, 0x7829435f, 0xf124183b, 0x821dba9f, 0xaff60ff4, 0xea2c4e6d, 0x16e39264,
|
||||
0x92544a8b, 0x009b4fc3, 0xaba68ced, 0x9ac96f78, 0x06a5b79a, 0xb2856e6e, 0x1aec3ca9, 0xbe838688,
|
||||
0x0e0804e9, 0x55f1be56, 0xe7e5363b, 0xb3a1f25d, 0xf7debb85, 0x61fe033c, 0x16746233, 0x3c034c28,
|
||||
0xda6d0c74, 0x79aac56c, 0x3ce4e1ad, 0x51f0c802, 0x98f8f35a, 0x1626a49f, 0xeed82b29, 0x1d382fe3,
|
||||
0x0c4fb99a, 0xbb325778, 0x3ec6d97b, 0x6e77a6a9, 0xcb658b5c, 0xd45230c7, 0x2bd1408b, 0x60c03eb7,
|
||||
0xb9068d78, 0xa33754f4, 0xf430c87d, 0xc8a71302, 0xb96d8c32, 0xebd4e7be, 0xbe8b9d2d, 0x7979fb06,
|
||||
0xe7225308, 0x8b75cf77, 0x11ef8da4, 0xe083c858, 0x8d6b786f, 0x5a6317a6, 0xfa5cf7a0, 0x5dda0033,
|
||||
0xf28ebfb0, 0xf5b9c310, 0xa0eac280, 0x08b9767a, 0xa3d9d2b0, 0x79d34217, 0x021a718d, 0x9ac6336a,
|
||||
0x2711fd60, 0x438050e3, 0x069908a8, 0x3d7fedc4, 0x826d2bef, 0x4eeb8476, 0x488dcf25, 0x36c9d566,
|
||||
0x28e74e41, 0xc2610aca, 0x3d49a9cf, 0xbae3b9df, 0xb65f8de6, 0x92aeaf64, 0x3ac7d5e6, 0x9ea80509,
|
||||
0xf22b017d, 0xa4173f70, 0xdd1e16c3, 0x15e0d7f9, 0x50b1b887, 0x2b9f4fd5, 0x625aba82, 0x6a017962,
|
||||
0x2ec01b9c, 0x15488aa9, 0xd716e740, 0x40055a2c, 0x93d29a22, 0xe32dbf9a, 0x058745b9, 0x3453dc1e,
|
||||
0xd699296e, 0x496cff6f, 0x1c9f4986, 0xdfe2ed07, 0xb87242d1, 0x19de7eae, 0x053e561a, 0x15ad6f8c,
|
||||
0x66626c1c, 0x7154c24c, 0xea082b2a, 0x93eb2939, 0x17dcb0f0, 0x58d4f2ae, 0x9ea294fb, 0x52cf564c,
|
||||
0x9883fe66, 0x2ec40581, 0x763953c3, 0x01d6692e, 0xd3a0c108, 0xa1e7160e, 0xe4f2dfa6, 0x693ed285,
|
||||
0x74904698, 0x4c2b0edd, 0x4f757656, 0x5d393378, 0xa132234f, 0x3d321c5d, 0xc3f5e194, 0x4b269301,
|
||||
0xc79f022f, 0x3c997e7e, 0x5e4f9504, 0x3ffafbbd, 0x76f7ad0e, 0x296693f4, 0x3d1fce6f, 0xc61e45be,
|
||||
0xd3b5ab34, 0xf72bf9b7, 0x1b0434c0, 0x4e72b567, 0x5592a33d, 0xb5229301, 0xcfd2a87f, 0x60aeb767,
|
||||
0x1814386b, 0x30bcc33d, 0x38a0c07d, 0xfd1606f2, 0xc363519b, 0x589dd390, 0x5479f8e6, 0x1cb8d647,
|
||||
0x97fd61a9, 0xea7759f4, 0x2d57539d, 0x569a58cf, 0xe84e63ad, 0x462e1b78, 0x6580f87e, 0xf3817914,
|
||||
0x91da55f4, 0x40a230f3, 0xd1988f35, 0xb6e318d2, 0x3ffa50bc, 0x3d40f021, 0xc3c0bdae, 0x4958c24c,
|
||||
0x518f36b2, 0x84b1d370, 0x0fedce83, 0x878ddada, 0xf2a279c7, 0x94e01be8, 0x90716f4b, 0x954b8aa3
|
||||
]
|
||||
s8 = [
|
||||
0xe216300d, 0xbbddfffc, 0xa7ebdabd, 0x35648095, 0x7789f8b7, 0xe6c1121b, 0x0e241600, 0x052ce8b5,
|
||||
0x11a9cfb0, 0xe5952f11, 0xece7990a, 0x9386d174, 0x2a42931c, 0x76e38111, 0xb12def3a, 0x37ddddfc,
|
||||
0xde9adeb1, 0x0a0cc32c, 0xbe197029, 0x84a00940, 0xbb243a0f, 0xb4d137cf, 0xb44e79f0, 0x049eedfd,
|
||||
0x0b15a15d, 0x480d3168, 0x8bbbde5a, 0x669ded42, 0xc7ece831, 0x3f8f95e7, 0x72df191b, 0x7580330d,
|
||||
0x94074251, 0x5c7dcdfa, 0xabbe6d63, 0xaa402164, 0xb301d40a, 0x02e7d1ca, 0x53571dae, 0x7a3182a2,
|
||||
0x12a8ddec, 0xfdaa335d, 0x176f43e8, 0x71fb46d4, 0x38129022, 0xce949ad4, 0xb84769ad, 0x965bd862,
|
||||
0x82f3d055, 0x66fb9767, 0x15b80b4e, 0x1d5b47a0, 0x4cfde06f, 0xc28ec4b8, 0x57e8726e, 0x647a78fc,
|
||||
0x99865d44, 0x608bd593, 0x6c200e03, 0x39dc5ff6, 0x5d0b00a3, 0xae63aff2, 0x7e8bd632, 0x70108c0c,
|
||||
0xbbd35049, 0x2998df04, 0x980cf42a, 0x9b6df491, 0x9e7edd53, 0x06918548, 0x58cb7e07, 0x3b74ef2e,
|
||||
0x522fffb1, 0xd24708cc, 0x1c7e27cd, 0xa4eb215b, 0x3cf1d2e2, 0x19b47a38, 0x424f7618, 0x35856039,
|
||||
0x9d17dee7, 0x27eb35e6, 0xc9aff67b, 0x36baf5b8, 0x09c467cd, 0xc18910b1, 0xe11dbf7b, 0x06cd1af8,
|
||||
0x7170c608, 0x2d5e3354, 0xd4de495a, 0x64c6d006, 0xbcc0c62c, 0x3dd00db3, 0x708f8f34, 0x77d51b42,
|
||||
0x264f620f, 0x24b8d2bf, 0x15c1b79e, 0x46a52564, 0xf8d7e54e, 0x3e378160, 0x7895cda5, 0x859c15a5,
|
||||
0xe6459788, 0xc37bc75f, 0xdb07ba0c, 0x0676a3ab, 0x7f229b1e, 0x31842e7b, 0x24259fd7, 0xf8bef472,
|
||||
0x835ffcb8, 0x6df4c1f2, 0x96f5b195, 0xfd0af0fc, 0xb0fe134c, 0xe2506d3d, 0x4f9b12ea, 0xf215f225,
|
||||
0xa223736f, 0x9fb4c428, 0x25d04979, 0x34c713f8, 0xc4618187, 0xea7a6e98, 0x7cd16efc, 0x1436876c,
|
||||
0xf1544107, 0xbedeee14, 0x56e9af27, 0xa04aa441, 0x3cf7c899, 0x92ecbae6, 0xdd67016d, 0x151682eb,
|
||||
0xa842eedf, 0xfdba60b4, 0xf1907b75, 0x20e3030f, 0x24d8c29e, 0xe139673b, 0xefa63fb8, 0x71873054,
|
||||
0xb6f2cf3b, 0x9f326442, 0xcb15a4cc, 0xb01a4504, 0xf1e47d8d, 0x844a1be5, 0xbae7dfdc, 0x42cbda70,
|
||||
0xcd7dae0a, 0x57e85b7a, 0xd53f5af6, 0x20cf4d8c, 0xcea4d428, 0x79d130a4, 0x3486ebfb, 0x33d3cddc,
|
||||
0x77853b53, 0x37effcb5, 0xc5068778, 0xe580b3e6, 0x4e68b8f4, 0xc5c8b37e, 0x0d809ea2, 0x398feb7c,
|
||||
0x132a4f94, 0x43b7950e, 0x2fee7d1c, 0x223613bd, 0xdd06caa2, 0x37df932b, 0xc4248289, 0xacf3ebc3,
|
||||
0x5715f6b7, 0xef3478dd, 0xf267616f, 0xc148cbe4, 0x9052815e, 0x5e410fab, 0xb48a2465, 0x2eda7fa4,
|
||||
0xe87b40e4, 0xe98ea084, 0x5889e9e1, 0xefd390fc, 0xdd07d35b, 0xdb485694, 0x38d7e5b2, 0x57720101,
|
||||
0x730edebc, 0x5b643113, 0x94917e4f, 0x503c2fba, 0x646f1282, 0x7523d24a, 0xe0779695, 0xf9c17a8f,
|
||||
0x7a5b2121, 0xd187b896, 0x29263a4d, 0xba510cdf, 0x81f47c9f, 0xad1163ed, 0xea7b5965, 0x1a00726e,
|
||||
0x11403092, 0x00da6d77, 0x4a0cdd61, 0xad1f4603, 0x605bdfb0, 0x9eedc364, 0x22ebe6a8, 0xcee7d28a,
|
||||
0xa0e736a0, 0x5564a6b9, 0x10853209, 0xc7eb8f37, 0x2de705ca, 0x8951570f, 0xdf09822b, 0xbd691a6c,
|
||||
0xaa12e4f2, 0x87451c0f, 0xe0f6a27a, 0x3ada4819, 0x4cf1764f, 0x0d771c2b, 0x67cdb156, 0x350d8384,
|
||||
0x5938fa0f, 0x42399ef3, 0x36997b07, 0x0e84093d, 0x4aa93e61, 0x8360d87b, 0x1fa98b0c, 0x1149382c,
|
||||
0xe97625a5, 0x0614d1b7, 0x0e25244b, 0x0c768347, 0x589e8d82, 0x0d2059d1, 0xa466bb1e, 0xf8da0a82,
|
||||
0x04f19130, 0xba6e4ec0, 0x99265164, 0x1ee7230d, 0x50b2ad80, 0xeaee6801, 0x8db2a283, 0xea8bf59e
|
||||
]
|
||||
|
||||
// Test vectors from RFC2144
|
||||
|
||||
Key1 : [128]
|
||||
Key1 = 0x0123456712345678234567893456789A
|
||||
Key2 : [80]
|
||||
Key2 = 0x01234567123456782345
|
||||
Key3 : [40]
|
||||
Key3 = 0x0123456712
|
||||
|
||||
Plaintext : [64]
|
||||
Plaintext = 0x0123456789ABCDEF
|
||||
|
||||
C1, C2, C3 : [64]
|
||||
C1 = 0x238B4FE5847E44B2
|
||||
C2 = 0xEB6A711A2C02271B
|
||||
C3 = 0x7AC816D16E9B302E
|
||||
|
||||
test_B1_1 = blockEncrypt (Key1, Plaintext) == C1
|
||||
test_B1_2 = blockEncrypt (Key2, Plaintext) == C2
|
||||
test_B1_3 = blockEncrypt (Key3, Plaintext) == C3
|
||||
|
||||
property passesTests = [test_B1_1, test_B1_2, test_B1_3] == ~zero
|
||||
@ -23,19 +23,21 @@
|
||||
// Specification of the Keccak (SHA-3) hash function
|
||||
// Author: David Lazar
|
||||
|
||||
SHA_3_224 M = take`{224} (Keccak `{r = 1152, c = 448} M)
|
||||
SHA_3_256 M = take`{256} (Keccak `{r = 1088, c = 512} M)
|
||||
SHA_3_384 M = take`{384} (Keccak `{r = 832, c = 768} M)
|
||||
SHA_3_512 M = take`{512} (Keccak `{r = 576, c = 1024} M)
|
||||
SHA_3_224 M = take`{224} (Keccak `{r = 1152, c = 448} (M # 0b01))
|
||||
SHA_3_256 M = take`{256} (Keccak `{r = 1088, c = 512} (M # 0b01))
|
||||
SHA_3_384 M = take`{384} (Keccak `{r = 832, c = 768} (M # 0b01))
|
||||
SHA_3_512 M = take`{512} (Keccak `{r = 576, c = 1024} (M # 0b01))
|
||||
SHAKE128 M = Keccak`{r = 1344, c = 256} (M # 0b1111)
|
||||
SHAKE256 M = Keccak`{r = 1088, c = 512} (M # 0b1111)
|
||||
|
||||
Keccak : {r, c, m, n}
|
||||
( fin r, fin c, fin m, fin n
|
||||
Keccak : {r, c, m}
|
||||
( fin r, fin c, fin m
|
||||
, r >= 1
|
||||
, (r + c) % 25 == 0
|
||||
, 64 >= (r + c) / 25
|
||||
, r * n >= 2 + m
|
||||
) => [m] -> [inf]
|
||||
Keccak M = squeeze `{r = r} (absorb `{w = (r + c) / 25} Ps)
|
||||
where Ps = pad `{r = r, n = n} M
|
||||
where Ps = pad `{r = r} M
|
||||
|
||||
squeeze : {r, w} (fin r, fin w, 64 >= w, r >= 0, 25 * w >= r) => [5][5][w] -> [inf]
|
||||
squeeze A = take`{r} (flatten A) # squeeze`{r = r} (Keccak_f A)
|
||||
@ -45,16 +47,16 @@ absorb Ps = as ! 0
|
||||
where
|
||||
as = [zero] # [ Keccak_f `{w = w} (s ^ (unflatten p)) | s <- as | p <- Ps ]
|
||||
|
||||
pad : {r, m, n}
|
||||
( fin r, fin m, fin n
|
||||
, r * n >= 2 + m
|
||||
) => [m] -> [n][r]
|
||||
pad M = split (M # [True] # (zero : [r*n-2-m]) # [True])
|
||||
pad : {r, m}
|
||||
( fin r, fin m
|
||||
, r >= 1
|
||||
) => [m] -> [(m + 2) /^ r][r]
|
||||
pad M = split (M # [True] # zero # [True])
|
||||
|
||||
Keccak_f : {w} (fin w, 64 >= w) => [5][5][w] -> [5][5][w]
|
||||
Keccak_f A = rounds ! 0
|
||||
Keccak_f A0 = rounds ! 0
|
||||
where
|
||||
rounds = [A] # [ Round RC A | RC <- RCs`{w = w} | A <- rounds ]
|
||||
rounds = [A0] # [ Round RC A | RC <- RCs`{w = w} | A <- rounds ]
|
||||
|
||||
Round : {w} (fin w) => [5][5][w] -> [5][5][w] -> [5][5][w]
|
||||
Round RC A = ι RC (χ (π (ρ (θ A))))
|
||||
@ -63,14 +65,14 @@ Round RC A = ι RC (χ (π (ρ (θ A))))
|
||||
θ A = A'
|
||||
where
|
||||
C = [ xor a | a <- A ]
|
||||
D = [ C @ x ^ (C @ y <<< 1)
|
||||
| x <- [0 .. 4] >>> 1
|
||||
| y <- [0 .. 4] <<< 1
|
||||
D = [ C @ x ^ (C @ y <<< 1)
|
||||
| (x:[8]) <- [4,0,1,2,3]
|
||||
| (y:[8]) <- [1,2,3,4,0]
|
||||
]
|
||||
A' = [ [ a ^ (D @ x) | a <- A @ x ] | x <- [0 .. 4] ]
|
||||
A' = [ [ a ^ (D @ x) | a <- A @ x ] | (x:[8]) <- [0 .. 4] ]
|
||||
|
||||
ρ : {w} (fin w) => [5][5][w] -> [5][5][w]
|
||||
ρ A = groupBy`{5} [ a <<< r | a <- join A | r <- R ]
|
||||
ρ A = groupBy`{5} [ a <<< r | a <- join A | (r:[8]) <- R ]
|
||||
where R = [00, 36, 03, 41, 18,
|
||||
01, 44, 10, 45, 02,
|
||||
62, 06, 43, 15, 61,
|
||||
@ -78,24 +80,21 @@ Round RC A = ι RC (χ (π (ρ (θ A))))
|
||||
27, 20, 39, 08, 14]
|
||||
|
||||
π : {w} (fin w) => [5][5][w] -> [5][5][w]
|
||||
π A = groupBy`{5} [ A @ ((x + (3:[8]) * y) % 5) @ x
|
||||
| x <- [0..4], y <- [0..4]
|
||||
π A = groupBy`{5} [ A @ ((x + 3*y) % 5) @ x
|
||||
| (x:[8]) <- [0..4], (y:[8]) <- [0..4]
|
||||
]
|
||||
|
||||
χ : {w} (fin w) => [5][5][w] -> [5][5][w]
|
||||
χ A = groupBy`{5} [ (A @ x @ y) ^ (~ A @ ((x + 1) % 5) @ y
|
||||
&& A @ ((x + 2) % 5) @ y)
|
||||
| x <- [0..4], y <- [0..4]
|
||||
| (x:[8]) <- [0..4], (y:[8]) <- [0..4]
|
||||
]
|
||||
|
||||
ι : {w} (fin w) => [5][5][w] -> [5][5][w] -> [5][5][w]
|
||||
ι RC A = A ^ RC
|
||||
|
||||
RCs : {w, n} (fin w, fin n, 24 >= n, n == 12 + 2 * (lg2 w)) => [n][5][5][w]
|
||||
RCs = [ [[take`{w} RC] # zero] # zero
|
||||
| RC <- RCs64
|
||||
| _ <- zero:[n]
|
||||
]
|
||||
RCs = take`{n} [ [[take`{w} RC] # zero] # zero | RC <- RCs64 ]
|
||||
|
||||
RCs64 : [24][64]
|
||||
RCs64 = join (transpose [
|
||||
@ -114,11 +113,69 @@ RCs64 = join (transpose [
|
||||
])
|
||||
|
||||
unflatten : {r, w} (fin w, 25*w >= r) => [r] -> [5][5][w]
|
||||
unflatten p = transpose (groupBy`{5} (groupBy`{w} (p # zero)))
|
||||
unflatten p = transpose (groupBy`{5} (reverse (groupBy`{w} (reverse (p # zero)))))
|
||||
|
||||
flatten : {w} (fin w) => [5][5][w] -> [5 * 5 * w]
|
||||
flatten A = join (join (transpose A))
|
||||
flatten A = reverse (join (reverse (join (transpose A))))
|
||||
|
||||
xor : {a, b} (fin a) => [a][b] -> [b]
|
||||
xor xs = xors ! 0
|
||||
where xors = [zero] # [ x ^ z | x <- xs | z <- xors ]
|
||||
|
||||
property RC_correct i j =
|
||||
(i:[8]) < 24 ==> (j:[8]) < 7 ==> RCs64@i!(2^^j - 1) == lfsr@(j + 7*i)
|
||||
|
||||
lfsr : [inf]
|
||||
lfsr = [ p!0 | p <- ps ]
|
||||
where
|
||||
/* powers of x modulo m */
|
||||
ps = [0x01] # [ pmod (pmult p 0b10) m | p <- ps ]
|
||||
m = <| x^^8 + x^^6 + x^^5 + x^^4 + 1 |>
|
||||
|
||||
/* See https://keccak.team/files/Keccak-reference-3.0.pdf, Section 1.2 */
|
||||
property unflatten_correct x y z p =
|
||||
x < 5 ==> y < 5 ==> z < (64:[12]) ==>
|
||||
p@((5*y + x)*64 + z) == unflatten`{1600,64} p @ x @ y ! z
|
||||
|
||||
property flatten_correct s =
|
||||
unflatten`{1600,64} (flatten`{64} s) == s
|
||||
|
||||
/** Splits a list of bits into bytes, using little-endian bit order. **/
|
||||
toBytes : {n} (fin n) => [8*n] -> [n][8]
|
||||
toBytes s = reverse (split (reverse s))
|
||||
|
||||
/** Joins a list of bytes into a list of bits, using little-endian bit order. **/
|
||||
fromBytes : {n} (fin n) => [n][8] -> [8*n]
|
||||
fromBytes bs = reverse (join (reverse bs))
|
||||
|
||||
/*
|
||||
Test vectors from
|
||||
https://csrc.nist.gov/projects/cryptographic-standards-and-guidelines/example-values#aHashing
|
||||
*/
|
||||
|
||||
property t1 = join (toBytes (SHA_3_224 [])) ==
|
||||
0x6b4e03423667dbb73b6e15454f0eb1abd4597f9a1b078e3f5b5a6bc7
|
||||
property t2 = join (toBytes (SHA_3_256 [])) ==
|
||||
0xa7ffc6f8bf1ed76651c14756a061d662f580ff4de43b49fa82d80a4b80f8434a
|
||||
property t3 = join (toBytes (SHA_3_384 [])) ==
|
||||
0x0c63a75b845e4f7d01107d852e4c2485c51a50aaaa94fc61995e71bbee983a2ac3713831264adb47fb6bd1e058d5f004
|
||||
property t4 = join (toBytes (SHA_3_512 [])) ==
|
||||
0xa69f73cca23a9ac5c8b567dc185a756e97c982164fe25859e0d1dcc1475c80a615b2123af1f5f94c11e3e9402c3ac558f500199d95b6d3e301758586281dcd26
|
||||
|
||||
property u1 = join (toBytes (SHA_3_224 0b11001)) ==
|
||||
0xffbad5da96bad71789330206dc6768ecaeb1b32dca6b3301489674ab
|
||||
property u2 = join (toBytes (SHA_3_256 0b11001)) ==
|
||||
0x7b0047cf5a456882363cbf0fb05322cf65f4b7059a46365e830132e3b5d957af
|
||||
property u3 = join (toBytes (SHA_3_384 0b11001)) ==
|
||||
0x737c9b491885e9bf7428e792741a7bf8dca9653471c3e148473f2c236b6a0a6455eb1dce9f779b4b6b237fef171b1c64
|
||||
property u4 = join (toBytes (SHA_3_512 0b11001)) ==
|
||||
0xa13e01494114c09800622a70288c432121ce70039d753cadd2e006e4d961cb27544c1481e5814bdceb53be6733d5e099795e5e81918addb058e22a9f24883f37
|
||||
|
||||
msg1600 : [1600]
|
||||
msg1600 = join [ 0b11000101 | _ <- zero : [200] ]
|
||||
|
||||
property v1 = join (toBytes (SHA_3_224 msg1600)) ==
|
||||
0x9376816aba503f72f96ce7eb65ac095deee3be4bf9bbc2a1cb7e11e0
|
||||
|
||||
property w1 = join (toBytes (SHA_3_224 (msg1600 # 0b11000))) ==
|
||||
0x22d2f7bb0b173fd8c19686f9173166e3ee62738047d7eadd69efb228
|
||||
|
||||
@ -123,15 +123,12 @@ As a summary, a "1" followed by m "0"s followed by a 64-
|
||||
SHA-1 as n 512-bit blocks.
|
||||
*/
|
||||
|
||||
pad : {msgLen,contentLen,chunks,padding}
|
||||
pad : {msgLen}
|
||||
( fin msgLen
|
||||
, 64 >= width msgLen // message width fits in a word
|
||||
, contentLen == msgLen + 65 // message + header
|
||||
, chunks == (contentLen+padding) / 512
|
||||
, padding == (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0
|
||||
)
|
||||
=> [msgLen] -> [chunks][512]
|
||||
pad msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64]))
|
||||
=> [msgLen] -> [(msgLen + 65) /^ 512][512]
|
||||
pad msg = split (msg # [True] # (zero:[(msgLen + 65) %^ 512]) # (`msgLen:[64]))
|
||||
|
||||
f : ([8], [32], [32], [32]) -> [32]
|
||||
f (t, x, y, z) =
|
||||
|
||||
@ -266,6 +266,18 @@
|
||||
))
|
||||
)
|
||||
|
||||
(define-fun cryCeilDiv ((x InfNat) (y InfNat)) InfNat
|
||||
(ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr
|
||||
(ite (= (value y) 0) cryErr (cryNat (- (div (- (value x)) (value y)))))
|
||||
)
|
||||
)
|
||||
|
||||
(define-fun cryCeilMod ((x InfNat) (y InfNat)) InfNat
|
||||
(ite (or (isErr x) (isErr y) (not (isFin x)) (not (isFin y))) cryErr
|
||||
(ite (= (value y) 0) cryErr (cryNat (mod (- (value x)) (value y))))
|
||||
)
|
||||
)
|
||||
|
||||
(define-fun cryLenFromThenTo ((x InfNat) (y InfNat) (z InfNat)) InfNat
|
||||
(ite (or (isErr x) (not (isFin x))
|
||||
(isErr y) (not (isFin y))
|
||||
|
||||
@ -17,6 +17,9 @@
|
||||
module Cryptol.Eval (
|
||||
moduleEnv
|
||||
, runEval
|
||||
, EvalOpts(..)
|
||||
, PPOpts(..)
|
||||
, defaultPPOpts
|
||||
, Eval
|
||||
, EvalEnv
|
||||
, emptyEnv
|
||||
|
||||
@ -14,7 +14,7 @@
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
module Cryptol.Eval.Env where
|
||||
|
||||
import Cryptol.Eval.Monad( Eval, delay, ready )
|
||||
import Cryptol.Eval.Monad( Eval, delay, ready, PPOpts )
|
||||
import Cryptol.Eval.Type
|
||||
import Cryptol.Eval.Value
|
||||
import Cryptol.ModuleSystem.Name
|
||||
|
||||
@ -14,6 +14,9 @@ module Cryptol.Eval.Monad
|
||||
( -- * Evaluation monad
|
||||
Eval(..)
|
||||
, runEval
|
||||
, EvalOpts(..)
|
||||
, getEvalOpts
|
||||
, PPOpts(..)
|
||||
, io
|
||||
, delay
|
||||
, delayFill
|
||||
@ -42,22 +45,42 @@ import qualified Control.Exception as X
|
||||
|
||||
import Cryptol.Utils.Panic
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Logger(Logger)
|
||||
import Cryptol.TypeCheck.AST(Type)
|
||||
|
||||
-- | A computation that returns an already-evaluated value.
|
||||
ready :: a -> Eval a
|
||||
ready a = Ready a
|
||||
|
||||
-- | How to pretty print things when evaluating
|
||||
data PPOpts = PPOpts
|
||||
{ useAscii :: Bool
|
||||
, useBase :: Int
|
||||
, useInfLength :: Int
|
||||
}
|
||||
|
||||
-- | Some options for evalutaion
|
||||
data EvalOpts = EvalOpts
|
||||
{ evalLogger :: Logger -- ^ Where to print stuff (e.g., for @trace@)
|
||||
, evalPPOpts :: PPOpts -- ^ How to pretty print things.
|
||||
}
|
||||
|
||||
|
||||
-- | The monad for Cryptol evaluation.
|
||||
data Eval a
|
||||
= Ready !a
|
||||
| Thunk !(IO a)
|
||||
| Thunk !(EvalOpts -> IO a)
|
||||
|
||||
data ThunkState a
|
||||
= Unforced -- ^ This thunk has not yet been forced
|
||||
| BlackHole -- ^ This thunk is currently being evaluated
|
||||
| Forced !a -- ^ This thunk has previously been forced, and has the given value
|
||||
|
||||
|
||||
-- | Access the evaluation options.
|
||||
getEvalOpts :: Eval EvalOpts
|
||||
getEvalOpts = Thunk return
|
||||
|
||||
{-# INLINE delay #-}
|
||||
-- | Delay the given evaluation computation, returning a thunk
|
||||
-- which will run the computation when forced. Raise a loop
|
||||
@ -66,11 +89,11 @@ delay :: Maybe String -- ^ Optional name to print if a loop is detected
|
||||
-> Eval a -- ^ Computation to delay
|
||||
-> Eval (Eval a)
|
||||
delay _ (Ready a) = Ready (Ready a)
|
||||
delay msg (Thunk x) = Thunk $ do
|
||||
delay msg (Thunk x) = Thunk $ \opts -> do
|
||||
let msg' = maybe "" ("while evaluating "++) msg
|
||||
let retry = cryLoopError msg'
|
||||
r <- newIORef Unforced
|
||||
return $ unDelay retry r x
|
||||
return $ unDelay retry r (x opts)
|
||||
|
||||
{-# INLINE delayFill #-}
|
||||
|
||||
@ -82,9 +105,9 @@ delayFill :: Eval a -- ^ Computation to delay
|
||||
-> Eval a -- ^ Backup computation to run if a tight loop is detected
|
||||
-> Eval (Eval a)
|
||||
delayFill (Ready x) _ = Ready (Ready x)
|
||||
delayFill (Thunk x) retry = Thunk $ do
|
||||
delayFill (Thunk x) retry = Thunk $ \opts -> do
|
||||
r <- newIORef Unforced
|
||||
return $ unDelay retry r x
|
||||
return $ unDelay retry r (x opts)
|
||||
|
||||
-- | Produce a thunk value which can be filled with its associated computation
|
||||
-- after the fact. A preallocated thunk is returned, along with an operation to
|
||||
@ -112,18 +135,18 @@ unDelay retry r x = do
|
||||
return val
|
||||
|
||||
-- | Execute the given evaluation action.
|
||||
runEval :: Eval a -> IO a
|
||||
runEval (Ready a) = return a
|
||||
runEval (Thunk x) = x
|
||||
runEval :: EvalOpts -> Eval a -> IO a
|
||||
runEval _ (Ready a) = return a
|
||||
runEval opts (Thunk x) = x opts
|
||||
|
||||
{-# INLINE evalBind #-}
|
||||
evalBind :: Eval a -> (a -> Eval b) -> Eval b
|
||||
evalBind (Ready a) f = f a
|
||||
evalBind (Thunk x) f = Thunk (x >>= runEval . f)
|
||||
evalBind (Thunk x) f = Thunk $ \opts -> x opts >>= runEval opts . f
|
||||
|
||||
instance Functor Eval where
|
||||
fmap f (Ready x) = Ready (f x)
|
||||
fmap f (Thunk m) = Thunk (f <$> m)
|
||||
fmap f (Thunk m) = Thunk $ \opts -> f <$> m opts
|
||||
{-# INLINE fmap #-}
|
||||
|
||||
instance Applicative Eval where
|
||||
@ -134,7 +157,7 @@ instance Applicative Eval where
|
||||
|
||||
instance Monad Eval where
|
||||
return = Ready
|
||||
fail = Thunk . fail
|
||||
fail x = Thunk (\_ -> fail x)
|
||||
(>>=) = evalBind
|
||||
{-# INLINE return #-}
|
||||
{-# INLINE (>>=) #-}
|
||||
@ -147,11 +170,11 @@ instance NFData a => NFData (Eval a) where
|
||||
rnf (Thunk _) = ()
|
||||
|
||||
instance MonadFix Eval where
|
||||
mfix f = Thunk $ mfix (\x -> runEval (f x))
|
||||
mfix f = Thunk $ \opts -> mfix (\x -> runEval opts (f x))
|
||||
|
||||
-- | Lift an 'IO' computation into the 'Eval' monad.
|
||||
io :: IO a -> Eval a
|
||||
io = Thunk
|
||||
io m = Thunk (\_ -> m)
|
||||
{-# INLINE io #-}
|
||||
|
||||
|
||||
@ -192,11 +215,11 @@ typeCannotBeDemoted t = X.throw (TypeCannotBeDemoted t)
|
||||
|
||||
-- | For division by 0.
|
||||
divideByZero :: Eval a
|
||||
divideByZero = Thunk (X.throwIO DivideByZero)
|
||||
divideByZero = io (X.throwIO DivideByZero)
|
||||
|
||||
-- | For exponentiation by a negative integer.
|
||||
negativeExponent :: Eval a
|
||||
negativeExponent = Thunk (X.throwIO NegativeExponent)
|
||||
negativeExponent = io (X.throwIO NegativeExponent)
|
||||
|
||||
-- | For when we know that a word is too wide and will exceed gmp's
|
||||
-- limits (though words approaching this size will probably cause the
|
||||
@ -206,12 +229,12 @@ wordTooWide w = X.throw (WordTooWide w)
|
||||
|
||||
-- | For the Cryptol @error@ function.
|
||||
cryUserError :: String -> Eval a
|
||||
cryUserError msg = Thunk (X.throwIO (UserError msg))
|
||||
cryUserError msg = io (X.throwIO (UserError msg))
|
||||
|
||||
-- | For cases where we can detect tight loops.
|
||||
cryLoopError :: String -> Eval a
|
||||
cryLoopError msg = Thunk (X.throwIO (LoopError msg))
|
||||
cryLoopError msg = io (X.throwIO (LoopError msg))
|
||||
|
||||
-- | A sequencing operation has gotten an invalid index.
|
||||
invalidIndex :: Integer -> Eval a
|
||||
invalidIndex i = Thunk (X.throwIO (InvalidIndex i))
|
||||
invalidIndex i = io (X.throwIO (InvalidIndex i))
|
||||
|
||||
@ -63,6 +63,7 @@ are as follows:
|
||||
| Cryptol type | Description | `TValue` representation |
|
||||
|:----------------- |:-------------- |:--------------------------- |
|
||||
| `Bit` | booleans | `TVBit` |
|
||||
| `Integer` | integers | `TVInteger` |
|
||||
| `[n]a` | finite lists | `TVSeq n a` |
|
||||
| `[inf]a` | infinite lists | `TVStream a` |
|
||||
| `(a, b, c)` | tuples | `TVTuple [a,b,c]` |
|
||||
@ -87,6 +88,10 @@ Accordingly, *M*(`Bit`) is a flat cpo with values for `True`,
|
||||
`False`, run-time errors of type `EvalError`, and $\bot$; we
|
||||
represent it with the Haskell type `Either EvalError Bool`.
|
||||
|
||||
Similarly, *M*(`Integer`) is a flat cpo with values for integers,
|
||||
run-time errors, and $\bot$; we represent it with the Haskell type
|
||||
`Either EvalError Integer`.
|
||||
|
||||
The cpos for lists, tuples, and records are cartesian products. The
|
||||
cpo ordering is pointwise, and the bottom element $\bot$ is the
|
||||
list/tuple/record whose elements are all $\bot$. Trivial types `[0]t`,
|
||||
@ -133,10 +138,10 @@ Copy Functions
|
||||
Functions `copyBySchema` and `copyByTValue` make a copy of the given
|
||||
value, building the spine based only on the type without forcing the
|
||||
value argument. This ensures that undefinedness appears inside `VBit`
|
||||
values only, and never on any constructors of the `Value` type. In
|
||||
turn, this gives the appropriate semantics to recursive definitions:
|
||||
The bottom value for a compound type is equal to a value of the same
|
||||
type where every individual bit is bottom.
|
||||
and `VInteger` values only, and never on any constructors of the
|
||||
`Value` type. In turn, this gives the appropriate semantics to
|
||||
recursive definitions: The bottom value for a compound type is equal
|
||||
to a value of the same type where every individual bit is bottom.
|
||||
|
||||
For each Cryptol type `t`, the cpo *M*(`t`) can be represented as a
|
||||
subset of values of type `Value` that satisfy the datatype invariant.
|
||||
@ -771,7 +776,7 @@ at the same positions.
|
||||
> go ty val =
|
||||
> case ty of
|
||||
> TVBit -> VBit (fmap op (fromVBit val))
|
||||
> TVInteger -> VInteger (Left (UserError "FIXME: logicBinary Integer"))
|
||||
> TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"]
|
||||
> TVSeq _w ety -> VList (map (go ety) (fromVList val))
|
||||
> TVStream ety -> VList (map (go ety) (fromVList val))
|
||||
> TVTuple etys -> VTuple (zipWith go etys (fromVTuple val))
|
||||
@ -785,7 +790,7 @@ at the same positions.
|
||||
> go ty l r =
|
||||
> case ty of
|
||||
> TVBit -> VBit (liftA2 op (fromVBit l) (fromVBit r))
|
||||
> TVInteger -> VInteger (Left (UserError "FIXME: logicBinary Integer"))
|
||||
> TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]
|
||||
> TVSeq _w ety -> VList (zipWith (go ety) (fromVList l) (fromVList r))
|
||||
> TVStream ety -> VList (zipWith (go ety) (fromVList l) (fromVList r))
|
||||
> TVTuple etys -> VTuple (zipWith3 go etys (fromVTuple l) (fromVTuple r))
|
||||
@ -1119,7 +1124,7 @@ This module implements the core functionality of the `:eval
|
||||
running the reference evaluator on an expression.
|
||||
|
||||
> evaluate :: Expr -> M.ModuleCmd Value
|
||||
> evaluate expr modEnv = return (Right (evalExpr env expr, modEnv), [])
|
||||
> evaluate expr (_,modEnv) = return (Right (evalExpr env expr, modEnv), [])
|
||||
> where
|
||||
> extDgs = concatMap mDecls (M.loadedModules modEnv)
|
||||
> env = foldl evalDeclGroup mempty extDgs
|
||||
|
||||
@ -135,6 +135,8 @@ evalTF f vs
|
||||
| TCExp <- f, [x,y] <- vs = nExp x y
|
||||
| TCMin <- f, [x,y] <- vs = nMin x y
|
||||
| TCMax <- f, [x,y] <- vs = nMax x y
|
||||
| TCCeilDiv <- f, [x,y] <- vs = mb $ nCeilDiv x y
|
||||
| TCCeilMod <- f, [x,y] <- vs = mb $ nCeilMod x y
|
||||
| TCLenFromThen <- f, [x,y,z] <- vs = mb $ nLenFromThen x y z
|
||||
| TCLenFromThenTo <- f, [x,y,z] <- vs = mb $ nLenFromThenTo x y z
|
||||
| otherwise = evalPanic "evalTF"
|
||||
|
||||
@ -332,12 +332,6 @@ type Value = GenValue Bool BV Integer
|
||||
|
||||
-- Pretty Printing -------------------------------------------------------------
|
||||
|
||||
data PPOpts = PPOpts
|
||||
{ useAscii :: Bool
|
||||
, useBase :: Int
|
||||
, useInfLength :: Int
|
||||
}
|
||||
|
||||
defaultPPOpts :: PPOpts
|
||||
defaultPPOpts = PPOpts { useAscii = False, useBase = 10, useInfLength = 5 }
|
||||
|
||||
|
||||
@ -32,6 +32,7 @@ module Cryptol.ModuleSystem (
|
||||
, IfaceTySyn, IfaceDecl(..)
|
||||
) where
|
||||
|
||||
import qualified Cryptol.Eval as E
|
||||
import qualified Cryptol.Eval.Value as E
|
||||
import Cryptol.ModuleSystem.Env
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
@ -48,7 +49,7 @@ import qualified Cryptol.Utils.Ident as M
|
||||
|
||||
-- Public Interface ------------------------------------------------------------
|
||||
|
||||
type ModuleCmd a = ModuleEnv -> IO (ModuleRes a)
|
||||
type ModuleCmd a = (E.EvalOpts,ModuleEnv) -> IO (ModuleRes a)
|
||||
|
||||
type ModuleRes a = (Either ModuleError (a,ModuleEnv), [ModuleWarning])
|
||||
|
||||
@ -61,7 +62,7 @@ findModule n env = runModuleM env (Base.findModule n)
|
||||
|
||||
-- | Load the module contained in the given file.
|
||||
loadModuleByPath :: FilePath -> ModuleCmd T.Module
|
||||
loadModuleByPath path env = runModuleM (resetModuleEnv env) $ do
|
||||
loadModuleByPath path (evo,env) = runModuleM (evo,resetModuleEnv env) $ do
|
||||
-- unload the module if it already exists
|
||||
unloadModule path
|
||||
|
||||
|
||||
@ -1,3 +1,4 @@
|
||||
|
||||
-- |
|
||||
-- Module : $Header$
|
||||
-- Copyright : (c) 2013-2016 Galois, Inc.
|
||||
@ -5,12 +6,13 @@
|
||||
-- Maintainer : cryptol@galois.com
|
||||
-- Stability : provisional
|
||||
-- Portability : portable
|
||||
--
|
||||
-- This is the main driver---it provides entry points for the
|
||||
-- various passes.
|
||||
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
|
||||
-- | This is the main driver---it provides entry points for the
|
||||
-- various passes.
|
||||
module Cryptol.ModuleSystem.Base where
|
||||
|
||||
import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls)
|
||||
@ -37,6 +39,7 @@ import qualified Cryptol.TypeCheck.Sanity as TcSanity
|
||||
import Cryptol.Utils.Ident (preludeName, preludeExtrasName, interactiveName,unpackModName)
|
||||
import Cryptol.Utils.PP (pretty)
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.Utils.Logger(logPutStrLn, logPrint)
|
||||
|
||||
import Cryptol.Prelude (writePreludeContents, writePreludeExtrasContents)
|
||||
|
||||
@ -170,8 +173,7 @@ loadModule path pm = do
|
||||
let pm' = addPrelude pm
|
||||
loadDeps pm'
|
||||
|
||||
-- XXX make it possible to configure output
|
||||
io (putStrLn ("Loading module " ++ pretty (P.thing (P.mName pm'))))
|
||||
withLogger logPutStrLn ("Loading module " ++ pretty (P.thing (P.mName pm')))
|
||||
|
||||
tcm <- checkModule path pm'
|
||||
|
||||
@ -427,7 +429,9 @@ typecheck act i env = do
|
||||
case meCoreLint menv of
|
||||
NoCoreLint -> return ()
|
||||
CoreLint -> case lintCheck (tcLinter act) o input of
|
||||
Right as -> io $ mapM_ (print . T.pp) as
|
||||
Right as ->
|
||||
let ppIt l = mapM_ (logPrint l . T.pp)
|
||||
in withLogger ppIt as
|
||||
Left err -> panic "Core lint failed:" [show err]
|
||||
return o
|
||||
|
||||
@ -465,14 +469,16 @@ evalExpr :: T.Expr -> ModuleM E.Value
|
||||
evalExpr e = do
|
||||
env <- getEvalEnv
|
||||
denv <- getDynEnv
|
||||
io $ E.runEval $ (E.evalExpr (env <> deEnv denv) e)
|
||||
evopts <- getEvalOpts
|
||||
io $ E.runEval evopts $ (E.evalExpr (env <> deEnv denv) e)
|
||||
|
||||
evalDecls :: [T.DeclGroup] -> ModuleM ()
|
||||
evalDecls dgs = do
|
||||
env <- getEvalEnv
|
||||
denv <- getDynEnv
|
||||
evOpts <- getEvalOpts
|
||||
let env' = env <> deEnv denv
|
||||
deEnv' <- io $ E.runEval $ E.evalDecls dgs env'
|
||||
deEnv' <- io $ E.runEval evOpts $ E.evalDecls dgs env'
|
||||
let denv' = denv { deDecls = deDecls denv ++ dgs
|
||||
, deEnv = deEnv'
|
||||
}
|
||||
|
||||
@ -62,9 +62,8 @@ data ModuleEnv = ModuleEnv
|
||||
-- ^ The evaluation environment. Contains the values for all loaded
|
||||
-- modules, both public and private.
|
||||
|
||||
|
||||
, meCoreLint :: CoreLint
|
||||
-- ^ Should we run the linter to ensure snaity.
|
||||
-- ^ Should we run the linter to ensure sanity.
|
||||
|
||||
, meMonoBinds :: !Bool
|
||||
-- ^ Are we assuming that local bindings are monomorphic.
|
||||
@ -85,7 +84,9 @@ data ModuleEnv = ModuleEnv
|
||||
, meSupply :: !Supply
|
||||
-- ^ Name source for the renamer
|
||||
|
||||
} deriving (Generic, NFData)
|
||||
} deriving Generic
|
||||
|
||||
instance NFData ModuleEnv
|
||||
|
||||
-- | Should we run the linter?
|
||||
data CoreLint = NoCoreLint -- ^ Don't run core lint
|
||||
@ -102,7 +103,7 @@ resetModuleEnv env = env
|
||||
}
|
||||
|
||||
initialModuleEnv :: IO ModuleEnv
|
||||
initialModuleEnv = do
|
||||
initialModuleEnv = do
|
||||
curDir <- getCurrentDirectory
|
||||
#ifndef RELOCATABLE
|
||||
dataDir <- getDataDir
|
||||
@ -197,17 +198,19 @@ dynamicEnv me = (decls,names,R.toNameDisp names)
|
||||
decls = deIfaceDecls (meDynEnv me)
|
||||
names = R.unqualifiedEnv decls
|
||||
|
||||
-- | Retrieve all 'IfaceDecls' referenced by a module, as well as all of its
|
||||
-- public and private declarations, checking expressions
|
||||
-- | Retrieve the combined 'IfaceDecls' needed by the the currently focused
|
||||
-- module. This includes the declarations of the focused module and all
|
||||
-- of its imports. This is the "view from within the module" used
|
||||
-- for type-checking expressions on the command line.
|
||||
qualifiedEnv :: ModuleEnv -> IfaceDecls
|
||||
qualifiedEnv me = fold $
|
||||
do fm <- meFocusedModule me
|
||||
lm <- lookupModule fm me
|
||||
deps <- mapM loadImport (T.mImports (lmModule lm))
|
||||
let Iface { .. } = lmInterface lm
|
||||
do focusedName <- meFocusedModule me
|
||||
focusedModule <- lookupModule focusedName me
|
||||
deps <- mapM getImportIface (T.mImports (lmModule focusedModule))
|
||||
let Iface { .. } = lmInterface focusedModule
|
||||
return (mconcat (ifPublic : ifPrivate : deps))
|
||||
where
|
||||
loadImport imp =
|
||||
getImportIface imp =
|
||||
do lm <- lookupModule (iModule imp) me
|
||||
return (ifPublic (lmInterface lm))
|
||||
|
||||
@ -227,19 +230,27 @@ instance Monoid LoadedModules where
|
||||
|
||||
data LoadedModule = LoadedModule
|
||||
{ lmName :: ModName
|
||||
, lmFilePath :: FilePath -- ^ The file path used to load this module (may not be canonical)
|
||||
, lmCanonicalPath :: FilePath -- ^ The canonical version of the path of this module
|
||||
, lmFilePath :: FilePath
|
||||
-- ^ The file path used to load this module (may not be canonical)
|
||||
, lmCanonicalPath :: FilePath
|
||||
-- ^ The canonical version of the path of this module
|
||||
, lmInterface :: Iface
|
||||
, lmModule :: T.Module
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
-- | Has this module been loaded already.
|
||||
isLoaded :: ModName -> LoadedModules -> Bool
|
||||
isLoaded mn lm = any ((mn ==) . lmName) (getLoadedModules lm)
|
||||
|
||||
-- | Try to find a previously loaded module
|
||||
lookupModule :: ModName -> ModuleEnv -> Maybe LoadedModule
|
||||
lookupModule mn env = List.find ((mn ==) . lmName) (getLoadedModules (meLoadedModules env))
|
||||
lookupModule mn env = List.find ((mn ==) . lmName)
|
||||
(getLoadedModules (meLoadedModules env))
|
||||
|
||||
addLoadedModule :: FilePath -> FilePath -> T.Module -> LoadedModules -> LoadedModules
|
||||
-- | Add a freshly loaded module. If it was previously loaded, then
|
||||
-- the new version is ignored.
|
||||
addLoadedModule ::
|
||||
FilePath -> FilePath -> T.Module -> LoadedModules -> LoadedModules
|
||||
addLoadedModule path canonicalPath tm lm
|
||||
| isLoaded (T.mName tm) lm = lm
|
||||
| otherwise = LoadedModules (getLoadedModules lm ++ [loaded])
|
||||
@ -252,6 +263,7 @@ addLoadedModule path canonicalPath tm lm
|
||||
, lmModule = tm
|
||||
}
|
||||
|
||||
-- | Remove a previously loaded module.
|
||||
removeLoadedModule :: FilePath -> LoadedModules -> LoadedModules
|
||||
removeLoadedModule path (LoadedModules ms) = LoadedModules (remove ms)
|
||||
where
|
||||
|
||||
@ -11,7 +11,7 @@
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
module Cryptol.ModuleSystem.Monad where
|
||||
|
||||
import Cryptol.Eval (EvalEnv)
|
||||
import Cryptol.Eval (EvalEnv,EvalOpts(..))
|
||||
|
||||
import qualified Cryptol.Eval.Monad as E
|
||||
import Cryptol.ModuleSystem.Env
|
||||
@ -30,6 +30,7 @@ import qualified Cryptol.TypeCheck.AST as T
|
||||
import Cryptol.Parser.Position (Range)
|
||||
import Cryptol.Utils.Ident (interactiveName, packModName)
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Logger(Logger)
|
||||
|
||||
import Control.Monad.IO.Class
|
||||
import Control.Exception (IOException)
|
||||
@ -233,12 +234,12 @@ renamerWarnings ws
|
||||
|
||||
-- Module System Monad ---------------------------------------------------------
|
||||
|
||||
data RO = RO
|
||||
{ roLoading :: [ImportSource]
|
||||
}
|
||||
data RO = RO { roLoading :: [ImportSource]
|
||||
, roEvalOpts :: EvalOpts
|
||||
}
|
||||
|
||||
emptyRO :: RO
|
||||
emptyRO = RO { roLoading = [] }
|
||||
emptyRO :: EvalOpts -> RO
|
||||
emptyRO ev = RO { roLoading = [], roEvalOpts = ev }
|
||||
|
||||
newtype ModuleT m a = ModuleT
|
||||
{ unModuleT :: ReaderT RO (StateT ModuleEnv
|
||||
@ -280,21 +281,19 @@ instance MonadIO m => MonadIO (ModuleT m) where
|
||||
liftIO m = lift $ liftIO m
|
||||
|
||||
runModuleT :: Monad m
|
||||
=> ModuleEnv
|
||||
=> (EvalOpts,ModuleEnv)
|
||||
-> ModuleT m a
|
||||
-> m (Either ModuleError (a, ModuleEnv), [ModuleWarning])
|
||||
runModuleT env m =
|
||||
runModuleT (ev,env) m =
|
||||
runWriterT
|
||||
$ runExceptionT
|
||||
$ runStateT env
|
||||
$ runReaderT emptyRO
|
||||
$ runReaderT (emptyRO ev)
|
||||
$ unModuleT m
|
||||
|
||||
-- runM (unModuleT m) emptyRO env
|
||||
|
||||
type ModuleM = ModuleT IO
|
||||
|
||||
runModuleM :: ModuleEnv -> ModuleM a
|
||||
runModuleM :: (EvalOpts, ModuleEnv) -> ModuleM a
|
||||
-> IO (Either ModuleError (a,ModuleEnv),[ModuleWarning])
|
||||
runModuleM = runModuleT
|
||||
|
||||
@ -394,12 +393,16 @@ modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM ()
|
||||
modifyEvalEnv f = ModuleT $ do
|
||||
env <- get
|
||||
let evalEnv = meEvalEnv env
|
||||
evalEnv' <- inBase $ E.runEval (f evalEnv)
|
||||
evOpts <- unModuleT getEvalOpts
|
||||
evalEnv' <- inBase $ E.runEval evOpts (f evalEnv)
|
||||
set $! env { meEvalEnv = evalEnv' }
|
||||
|
||||
getEvalEnv :: ModuleM EvalEnv
|
||||
getEvalEnv = ModuleT (meEvalEnv `fmap` get)
|
||||
|
||||
getEvalOpts :: ModuleM EvalOpts
|
||||
getEvalOpts = ModuleT (roEvalOpts `fmap` ask)
|
||||
|
||||
getFocusedModule :: ModuleM (Maybe P.ModName)
|
||||
getFocusedModule = ModuleT (meFocusedModule `fmap` get)
|
||||
|
||||
@ -448,3 +451,9 @@ getSolverConfig :: ModuleM T.SolverConfig
|
||||
getSolverConfig = ModuleT $ do
|
||||
me <- get
|
||||
return (meSolverConfig me)
|
||||
|
||||
-- | Usefule for logging. For example: @withLogger logPutStrLn "Hello"@
|
||||
withLogger :: (Logger -> a -> IO b) -> a -> ModuleM b
|
||||
withLogger f a = do l <- getEvalOpts
|
||||
io (f (evalLogger l) a)
|
||||
|
||||
|
||||
@ -356,7 +356,7 @@ mkPoly rng terms = mk 0 (map fromInteger bits)
|
||||
mkProperty :: LPName -> [Pattern PName] -> Expr PName -> Decl PName
|
||||
mkProperty f ps e = DBind Bind { bName = f
|
||||
, bParams = reverse ps
|
||||
, bDef = at e (Located emptyRange (DExpr (ETyped e TBit)))
|
||||
, bDef = at e (Located emptyRange (DExpr e))
|
||||
, bSignature = Nothing
|
||||
, bPragmas = [PragmaProperty]
|
||||
, bMono = False
|
||||
|
||||
@ -11,6 +11,7 @@
|
||||
{-# LANGUAGE TupleSections #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE NamedFieldPuns #-}
|
||||
{-# LANGUAGE Rank2Types #-}
|
||||
{-# LANGUAGE PatternGuards #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
@ -32,6 +33,7 @@ import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.ModuleSystem.Name (asPrim)
|
||||
import Cryptol.Utils.Ident (Ident,mkIdent)
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Logger(logPrint)
|
||||
|
||||
import qualified Data.Foldable as Fold
|
||||
import Data.List (sortBy)
|
||||
@ -233,13 +235,11 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
|
||||
lam $ \x -> return $
|
||||
lam $ \y -> do
|
||||
msg <- fromStr =<< s
|
||||
-- FIXME? get PPOPts from elsewhere?
|
||||
doc <- ppValue defaultPPOpts =<< x
|
||||
EvalOpts { evalPPOpts, evalLogger } <- getEvalOpts
|
||||
doc <- ppValue evalPPOpts =<< x
|
||||
yv <- y
|
||||
io $ putStrLn $ show $ if null msg then
|
||||
doc
|
||||
else
|
||||
text msg <+> doc
|
||||
io $ logPrint evalLogger
|
||||
$ if null msg then doc else text msg <+> doc
|
||||
return yv)
|
||||
]
|
||||
|
||||
|
||||
@ -32,6 +32,8 @@ data TFun
|
||||
| TCWidth -- ^ @ : Num -> Num @
|
||||
| TCMin -- ^ @ : Num -> Num -> Num @
|
||||
| TCMax -- ^ @ : Num -> Num -> Num @
|
||||
| TCCeilDiv -- ^ @ : Num -> Num -> Num @
|
||||
| TCCeilMod -- ^ @ : Num -> Num -> Num @
|
||||
|
||||
-- Computing the lengths of explicit enumerations
|
||||
| TCLenFromThen -- ^ @ : Num -> Num -> Num -> Num@
|
||||
@ -50,7 +52,7 @@ tBinOpPrec = mkMap t_table
|
||||
-- lowest to highest
|
||||
t_table =
|
||||
[ (LeftAssoc, [ TCAdd, TCSub ])
|
||||
, (LeftAssoc, [ TCMul, TCDiv, TCMod ])
|
||||
, (LeftAssoc, [ TCMul, TCDiv, TCMod, TCCeilDiv, TCCeilMod ])
|
||||
, (RightAssoc, [ TCExp ])
|
||||
]
|
||||
|
||||
@ -66,6 +68,8 @@ tfunNames = Map.fromList
|
||||
, tprefix "width" 1 TCWidth
|
||||
, tprefix "min" 2 TCMin
|
||||
, tprefix "max" 2 TCMax
|
||||
, tprefix "/^" 2 TCCeilDiv
|
||||
, tprefix "%^" 2 TCCeilMod
|
||||
, tprefix "lengthFromThen" 3 TCLenFromThen
|
||||
, tprefix "lengthFromThenTo" 3 TCLenFromThenTo
|
||||
]
|
||||
@ -77,21 +81,25 @@ tfunNames = Map.fromList
|
||||
instance PPName TFun where
|
||||
ppNameFixity f = Map.lookup f tBinOpPrec
|
||||
|
||||
ppPrefixName TCAdd = text "(+)"
|
||||
ppPrefixName TCSub = text "(-)"
|
||||
ppPrefixName TCMul = text "(*)"
|
||||
ppPrefixName TCDiv = text "(/)"
|
||||
ppPrefixName TCMod = text "(%)"
|
||||
ppPrefixName TCExp = text "(^^)"
|
||||
ppPrefixName f = pp f
|
||||
ppPrefixName TCAdd = text "(+)"
|
||||
ppPrefixName TCSub = text "(-)"
|
||||
ppPrefixName TCMul = text "(*)"
|
||||
ppPrefixName TCDiv = text "(/)"
|
||||
ppPrefixName TCMod = text "(%)"
|
||||
ppPrefixName TCExp = text "(^^)"
|
||||
ppPrefixName TCCeilDiv = text "(/^)"
|
||||
ppPrefixName TCCeilMod = text "(%^)"
|
||||
ppPrefixName f = pp f
|
||||
|
||||
ppInfixName TCAdd = text "+"
|
||||
ppInfixName TCSub = text "-"
|
||||
ppInfixName TCMul = text "*"
|
||||
ppInfixName TCDiv = text "/"
|
||||
ppInfixName TCMod = text "%"
|
||||
ppInfixName TCExp = text "^^"
|
||||
ppInfixName f = error $ "Not a prefix type function: " ++ show (pp f)
|
||||
ppInfixName TCAdd = text "+"
|
||||
ppInfixName TCSub = text "-"
|
||||
ppInfixName TCMul = text "*"
|
||||
ppInfixName TCDiv = text "/"
|
||||
ppInfixName TCMod = text "%"
|
||||
ppInfixName TCExp = text "^^"
|
||||
ppInfixName TCCeilDiv = text "/^"
|
||||
ppInfixName TCCeilMod = text "%^"
|
||||
ppInfixName f = error $ "Not a prefix type function: " ++ show (pp f)
|
||||
|
||||
instance PP TFun where
|
||||
ppPrec _ tcon =
|
||||
@ -105,6 +113,8 @@ instance PP TFun where
|
||||
TCWidth -> text "width"
|
||||
TCMin -> text "min"
|
||||
TCMax -> text "max"
|
||||
TCCeilDiv -> text "/^"
|
||||
TCCeilMod -> text "%^"
|
||||
|
||||
TCLenFromThen -> text "lengthFromThen"
|
||||
TCLenFromThenTo -> text "lengthFromThenTo"
|
||||
|
||||
@ -103,6 +103,8 @@ import qualified Data.Text as ST
|
||||
import qualified Data.Text.Lazy as T
|
||||
import Data.IORef(newIORef,readIORef)
|
||||
|
||||
import GHC.Float (log1p, expm1)
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
|
||||
@ -139,6 +141,7 @@ data CommandBody
|
||||
| FileExprArg (FilePath -> String -> REPL ())
|
||||
| DeclsArg (String -> REPL ())
|
||||
| ExprTypeArg (String -> REPL ())
|
||||
| ModNameArg (String -> REPL ())
|
||||
| FilenameArg (FilePath -> REPL ())
|
||||
| OptionArg (String -> REPL ())
|
||||
| ShellArg (String -> REPL ())
|
||||
@ -168,7 +171,7 @@ nbCommandList :: [CommandDescr]
|
||||
nbCommandList =
|
||||
[ CommandDescr [ ":t", ":type" ] (ExprArg typeOfCmd)
|
||||
"check the type of an expression"
|
||||
, CommandDescr [ ":b", ":browse" ] (ExprTypeArg browseCmd)
|
||||
, CommandDescr [ ":b", ":browse" ] (ModNameArg browseCmd)
|
||||
"display the current environment"
|
||||
, CommandDescr [ ":?", ":help" ] (ExprArg helpCmd)
|
||||
"display a brief description of a function or a type"
|
||||
@ -254,6 +257,12 @@ getPPValOpts =
|
||||
, E.useInfLength = infLength
|
||||
}
|
||||
|
||||
getEvalOpts :: REPL E.EvalOpts
|
||||
getEvalOpts =
|
||||
do ppOpts <- getPPValOpts
|
||||
l <- getLogger
|
||||
return E.EvalOpts { E.evalPPOpts = ppOpts, E.evalLogger = l }
|
||||
|
||||
evalCmd :: String -> REPL ()
|
||||
evalCmd str = do
|
||||
letEnabled <- getLetEnabled
|
||||
@ -264,7 +273,7 @@ evalCmd str = do
|
||||
P.ExprInput expr -> do
|
||||
(val,_ty) <- replEvalExpr expr
|
||||
ppOpts <- getPPValOpts
|
||||
valDoc <- io $ rethrowEvalError $ E.runEval $ E.ppValue ppOpts val
|
||||
valDoc <- rEvalRethrow (E.ppValue ppOpts val)
|
||||
|
||||
-- This is the point where the value gets forced. We deepseq the
|
||||
-- pretty-printed representation of it, rather than the value
|
||||
@ -282,7 +291,7 @@ evalCmd str = do
|
||||
printCounterexample :: Bool -> P.Expr P.PName -> [E.Value] -> REPL ()
|
||||
printCounterexample isSat pexpr vs =
|
||||
do ppOpts <- getPPValOpts
|
||||
docs <- mapM (io . E.runEval . E.ppValue ppOpts) vs
|
||||
docs <- mapM (rEval . E.ppValue ppOpts) vs
|
||||
let doc = ppPrec 3 pexpr -- function application has precedence 3
|
||||
rPrint $ hang doc 2 (sep docs) <+>
|
||||
text (if isSat then "= True" else "= False")
|
||||
@ -313,7 +322,8 @@ qcCmd qcMode str =
|
||||
let f _ [] = panic "Cryptol.REPL.Command"
|
||||
["Exhaustive testing ran out of test cases"]
|
||||
f _ (vs : vss1) = do
|
||||
result <- io $ runOneTest val vs
|
||||
evo <- getEvalOpts
|
||||
result <- io $ runOneTest evo val vs
|
||||
return (result, vss1)
|
||||
testSpec = TestSpec {
|
||||
testFn = f
|
||||
@ -336,8 +346,10 @@ qcCmd qcMode str =
|
||||
Nothing -> raise (TypeNotTestable ty)
|
||||
Just gens -> do
|
||||
rPutStrLn "Using random testing."
|
||||
evo <- getEvalOpts
|
||||
let testSpec = TestSpec {
|
||||
testFn = \sz' g -> io $ TestR.runOneTest val gens sz' g
|
||||
testFn = \sz' g ->
|
||||
io $ TestR.runOneTest evo val gens sz' g
|
||||
, testProp = str
|
||||
, testTotal = toInteger testNum
|
||||
, testPossible = sz
|
||||
@ -351,23 +363,27 @@ qcCmd qcMode str =
|
||||
prt testingMsg
|
||||
g <- io newTFGen
|
||||
report <- runTests testSpec g
|
||||
when (isPass (reportResult report)) $ do
|
||||
let szD = fromIntegral sz :: Double
|
||||
percent = fromIntegral (testNum * 100) / szD
|
||||
showValNum
|
||||
| sz > 2 ^ (20::Integer) =
|
||||
"2^^" ++ show (lg2 sz)
|
||||
| otherwise = show sz
|
||||
rPutStrLn $ "Coverage: "
|
||||
++ showFFloat (Just 2) percent "% ("
|
||||
++ show testNum ++ " of "
|
||||
++ showValNum ++ " values)"
|
||||
when (isPass (reportResult report)) $
|
||||
rPutStrLn $ coverageString testNum sz
|
||||
return [report]
|
||||
Nothing -> return []
|
||||
|
||||
where
|
||||
testingMsg = "testing..."
|
||||
|
||||
coverageString testNum sz =
|
||||
let (percent, expectedUnique) = expectedCoverage testNum sz
|
||||
showValNum
|
||||
| sz > 2 ^ (20::Integer) =
|
||||
"2^^" ++ show (lg2 sz)
|
||||
| otherwise = show sz
|
||||
in "Expected test coverage: "
|
||||
++ showFFloat (Just 2) percent "% ("
|
||||
++ showFFloat (Just 0) expectedUnique " of "
|
||||
++ showValNum
|
||||
++ " values)"
|
||||
|
||||
|
||||
totProgressWidth = 4 -- 100%
|
||||
|
||||
lg2 :: Integer -> Integer
|
||||
@ -401,10 +417,53 @@ qcCmd qcMode str =
|
||||
rPrint (pp err)
|
||||
FailError err vs -> do
|
||||
prtLn "ERROR for the following inputs:"
|
||||
mapM_ (\v -> rPrint =<< (io $ E.runEval $ E.ppValue opts v)) vs
|
||||
mapM_ (\v -> rPrint =<< (rEval $ E.ppValue opts v)) vs
|
||||
rPrint (pp err)
|
||||
Pass -> panic "Cryptol.REPL.Command" ["unexpected Test.Pass"]
|
||||
|
||||
|
||||
-- | This function computes the expected coverage percentage and
|
||||
-- expected number of unique test vectors when using random testing.
|
||||
--
|
||||
-- The expected test coverage proportion is:
|
||||
-- @1 - ((n-1)/n)^k@
|
||||
--
|
||||
-- This formula takes into account the fact that test vectors are chosen
|
||||
-- uniformly at random _with replacement_, and thus the same vectors
|
||||
-- may be generated multiple times. If the test vectors were chosen
|
||||
-- randomly without replacement, the proportion would instead be @k/n@.
|
||||
--
|
||||
-- We compute raising to the @k@ power in the log domain to improve
|
||||
-- numerical precision. The equivalant comptutation is:
|
||||
-- @-expm1( k * log1p (-1/n) )@
|
||||
--
|
||||
-- Where @expm1(x) = exp(x) - 1@ and @log1p(x) = log(1 + x)@.
|
||||
--
|
||||
-- However, if @sz@ is large enough, even carefully preserving
|
||||
-- precision may not be enough to get sensible results. In such
|
||||
-- situations, we expect the naive approximation @k/n@ to be very
|
||||
-- close to accurate and the expected number of unique values is
|
||||
-- essentially equal to the number of tests.
|
||||
expectedCoverage :: Int -> Integer -> (Double, Double)
|
||||
expectedCoverage testNum sz =
|
||||
-- If the Double computation has enough precision, use the
|
||||
-- "with replacement" formula.
|
||||
if testNum > 0 && proportion > 0 then
|
||||
(100.0 * proportion, szD * proportion)
|
||||
else
|
||||
(100.0 * naiveProportion, numD)
|
||||
|
||||
where
|
||||
szD :: Double
|
||||
szD = fromInteger sz
|
||||
|
||||
numD :: Double
|
||||
numD = fromIntegral testNum
|
||||
|
||||
naiveProportion = numD / szD
|
||||
|
||||
proportion = negate (expm1 (numD * log1p (negate (recip szD))))
|
||||
|
||||
satCmd, proveCmd :: String -> REPL ()
|
||||
satCmd = cmdProveSat True
|
||||
proveCmd = cmdProveSat False
|
||||
@ -604,7 +663,6 @@ typeOfCmd str = do
|
||||
(_re,def,sig) <- replCheckExpr expr
|
||||
|
||||
-- XXX need more warnings from the module system
|
||||
--io (mapM_ printWarning ws)
|
||||
whenDebug (rPutStrLn (dump def))
|
||||
(_,_,names) <- getFocusedEnv
|
||||
-- type annotation ':' has precedence 2
|
||||
@ -638,13 +696,23 @@ writeFileCmd file str = do
|
||||
(\(n,b) -> T.tIsBit b && T.tIsNum n == Just 8)
|
||||
(T.tIsSeq x)
|
||||
serializeValue (E.VSeq n vs) = do
|
||||
ws <- io $ E.runEval (mapM (>>=E.fromVWord "serializeValue") $ E.enumerateSeqMap n vs)
|
||||
ws <- rEval
|
||||
(mapM (>>=E.fromVWord "serializeValue") $ E.enumerateSeqMap n vs)
|
||||
return $ BS.pack $ map serializeByte ws
|
||||
serializeValue _ =
|
||||
panic "Cryptol.REPL.Command.writeFileCmd"
|
||||
["Impossible: Non-VSeq value of type [n][8]."]
|
||||
serializeByte (E.BV _ v) = fromIntegral (v .&. 0xFF)
|
||||
|
||||
|
||||
rEval :: E.Eval a -> REPL a
|
||||
rEval m = do ev <- getEvalOpts
|
||||
io (E.runEval ev m)
|
||||
|
||||
rEvalRethrow :: E.Eval a -> REPL a
|
||||
rEvalRethrow m = do ev <- getEvalOpts
|
||||
io $ rethrowEvalError $ E.runEval ev m
|
||||
|
||||
reloadCmd :: REPL ()
|
||||
reloadCmd = do
|
||||
mb <- getLoadedMod
|
||||
@ -709,18 +777,26 @@ quitCmd = stop
|
||||
|
||||
|
||||
browseCmd :: String -> REPL ()
|
||||
browseCmd pfx = do
|
||||
browseCmd input = do
|
||||
(iface,names,disp) <- getFocusedEnv
|
||||
|
||||
let mnames = map ST.pack (words input)
|
||||
validModNames <- getModNames
|
||||
let checkModName m =
|
||||
unless (m `elem` validModNames) $
|
||||
rPutStrLn ("error: " ++ show m ++ " is not a loaded module.")
|
||||
mapM_ checkModName mnames
|
||||
|
||||
let (visibleTypes,visibleDecls) = M.visibleNames names
|
||||
|
||||
(visibleType,visibleDecl)
|
||||
| null pfx =
|
||||
| null mnames =
|
||||
((`Set.member` visibleTypes)
|
||||
,(`Set.member` visibleDecls))
|
||||
|
||||
| otherwise =
|
||||
(\n -> n `Set.member` visibleTypes && pfx `isNamePrefix` n
|
||||
,\n -> n `Set.member` visibleDecls && pfx `isNamePrefix` n)
|
||||
(\n -> n `Set.member` visibleTypes && hasAnyModName mnames n
|
||||
,\n -> n `Set.member` visibleDecls && hasAnyModName mnames n)
|
||||
|
||||
browseTSyns visibleType iface disp
|
||||
browseNewtypes visibleType iface disp
|
||||
@ -900,22 +976,13 @@ handleCtrlC a = do rPutStrLn "Ctrl-C"
|
||||
|
||||
-- Utilities -------------------------------------------------------------------
|
||||
|
||||
isNamePrefix :: String -> M.Name -> Bool
|
||||
isNamePrefix pfx =
|
||||
let pfx' = ST.pack pfx
|
||||
in \n -> case M.nameInfo n of
|
||||
M.Declared _ -> pfx' `ST.isPrefixOf` M.identText (M.nameIdent n)
|
||||
M.Parameter -> False
|
||||
hasAnyModName :: [M.ModName] -> M.Name -> Bool
|
||||
hasAnyModName mnames n =
|
||||
case M.nameInfo n of
|
||||
M.Declared m -> m `elem` mnames
|
||||
M.Parameter -> False
|
||||
|
||||
|
||||
{-
|
||||
printWarning :: (Range,Warning) -> IO ()
|
||||
printWarning = print . ppWarning
|
||||
|
||||
printError :: (Range,Error) -> IO ()
|
||||
printError = print . ppError
|
||||
-}
|
||||
|
||||
-- | Lift a parsing action into the REPL monad.
|
||||
replParse :: (String -> Either ParseError a) -> String -> REPL a
|
||||
replParse parse str = case parse str of
|
||||
@ -935,7 +1002,10 @@ getPrimMap :: REPL M.PrimMap
|
||||
getPrimMap = liftModuleCmd M.getPrimMap
|
||||
|
||||
liftModuleCmd :: M.ModuleCmd a -> REPL a
|
||||
liftModuleCmd cmd = moduleCmdResult =<< io . cmd =<< getModuleEnv
|
||||
liftModuleCmd cmd =
|
||||
do evo <- getEvalOpts
|
||||
env <- getModuleEnv
|
||||
moduleCmdResult =<< io (cmd (evo,env))
|
||||
|
||||
moduleCmdResult :: M.ModuleRes a -> REPL a
|
||||
moduleCmdResult (res,ws0) = do
|
||||
@ -1141,6 +1211,7 @@ parseCommand findCmd line = do
|
||||
ExprArg body -> Just (Command (body args'))
|
||||
DeclsArg body -> Just (Command (body args'))
|
||||
ExprTypeArg body -> Just (Command (body args'))
|
||||
ModNameArg body -> Just (Command (body args'))
|
||||
FilenameArg body -> Just (Command (body =<< expandHome args'))
|
||||
OptionArg body -> Just (Command (body args'))
|
||||
ShellArg body -> Just (Command (body args'))
|
||||
|
||||
@ -39,6 +39,7 @@ module Cryptol.REPL.Monad (
|
||||
, getExprNames
|
||||
, getTypeNames
|
||||
, getPropertyNames
|
||||
, getModNames
|
||||
, LoadedModule(..), getLoadedMod, setLoadedMod
|
||||
, setSearchPath, prependSearchPath
|
||||
, getPrompt
|
||||
@ -61,6 +62,7 @@ module Cryptol.REPL.Monad (
|
||||
|
||||
-- ** Configurable Output
|
||||
, getPutStr
|
||||
, getLogger
|
||||
, setPutStr
|
||||
|
||||
-- ** Smoke Test
|
||||
@ -85,6 +87,7 @@ import qualified Cryptol.TypeCheck as T
|
||||
import qualified Cryptol.Utils.Ident as I
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic (panic)
|
||||
import Cryptol.Utils.Logger(Logger, logPutStr, funLogger)
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.Symbolic (proverNames, lookupProver, SatNum(..))
|
||||
|
||||
@ -111,6 +114,7 @@ import Prelude.Compat
|
||||
|
||||
-- REPL Environment ------------------------------------------------------------
|
||||
|
||||
-- | The currently focused module.
|
||||
data LoadedModule = LoadedModule
|
||||
{ lName :: Maybe P.ModName -- ^ Focused module
|
||||
, lPath :: FilePath -- ^ Focused file
|
||||
@ -119,18 +123,35 @@ data LoadedModule = LoadedModule
|
||||
-- | REPL RW Environment.
|
||||
data RW = RW
|
||||
{ eLoadedMod :: Maybe LoadedModule
|
||||
-- ^ This is the name of the currently "focused" module.
|
||||
-- This is what we edit (:e) or reload (:r)
|
||||
|
||||
, eContinue :: Bool
|
||||
-- ^ Should we keep going when we encounter an error, or give up.
|
||||
|
||||
, eIsBatch :: Bool
|
||||
-- ^ Are we in batch mode.
|
||||
|
||||
, eModuleEnv :: M.ModuleEnv
|
||||
-- ^ The current environment of all things loaded.
|
||||
|
||||
, eUserEnv :: UserEnv
|
||||
, ePutStr :: String -> IO ()
|
||||
-- ^ User settings
|
||||
|
||||
, eLogger :: Logger
|
||||
-- ^ Use this to send messages to the user
|
||||
|
||||
, eLetEnabled :: Bool
|
||||
-- ^ Should we allow `let` on the command line
|
||||
|
||||
, eUpdateTitle :: REPL ()
|
||||
-- ^ Execute this every time we load a module.
|
||||
-- This is used to change the title of terminal when loading a module.
|
||||
}
|
||||
|
||||
-- | Initial, empty environment.
|
||||
defaultRW :: Bool -> IO RW
|
||||
defaultRW isBatch = do
|
||||
defaultRW :: Bool -> Logger -> IO RW
|
||||
defaultRW isBatch l = do
|
||||
env <- M.initialModuleEnv
|
||||
return RW
|
||||
{ eLoadedMod = Nothing
|
||||
@ -138,7 +159,7 @@ defaultRW isBatch = do
|
||||
, eIsBatch = isBatch
|
||||
, eModuleEnv = env
|
||||
, eUserEnv = mkUserEnv userOptions
|
||||
, ePutStr = putStr
|
||||
, eLogger = l
|
||||
, eLetEnabled = True
|
||||
, eUpdateTitle = return ()
|
||||
}
|
||||
@ -155,9 +176,9 @@ mkPrompt rw
|
||||
newtype REPL a = REPL { unREPL :: IORef RW -> IO a }
|
||||
|
||||
-- | Run a REPL action with a fresh environment.
|
||||
runREPL :: Bool -> REPL a -> IO a
|
||||
runREPL isBatch m = do
|
||||
ref <- newIORef =<< defaultRW isBatch
|
||||
runREPL :: Bool -> Logger -> REPL a -> IO a
|
||||
runREPL isBatch l m = do
|
||||
ref <- newIORef =<< defaultRW isBatch l
|
||||
unREPL m ref
|
||||
|
||||
instance Functor REPL where
|
||||
@ -336,18 +357,23 @@ setUpdateREPLTitle m = modifyRW_ (\rw -> rw { eUpdateTitle = m })
|
||||
|
||||
-- | Set the REPL's string-printer
|
||||
setPutStr :: (String -> IO ()) -> REPL ()
|
||||
setPutStr fn = modifyRW_ (\rw -> rw { ePutStr = fn })
|
||||
setPutStr fn = modifyRW_ $ \rw -> rw { eLogger = funLogger fn }
|
||||
|
||||
-- | Get the REPL's string-printer
|
||||
getPutStr :: REPL (String -> IO ())
|
||||
getPutStr = fmap ePutStr getRW
|
||||
getPutStr =
|
||||
do rw <- getRW
|
||||
return (logPutStr (eLogger rw))
|
||||
|
||||
getLogger :: REPL Logger
|
||||
getLogger = eLogger <$> getRW
|
||||
|
||||
|
||||
-- | Use the configured output action to print a string
|
||||
rPutStr :: String -> REPL ()
|
||||
rPutStr str = do
|
||||
rw <- getRW
|
||||
io $ ePutStr rw str
|
||||
f <- getPutStr
|
||||
io (f str)
|
||||
|
||||
-- | Use the configured output action to print a string with a trailing newline
|
||||
rPutStrLn :: String -> REPL ()
|
||||
@ -426,6 +452,11 @@ getPropertyNames =
|
||||
|
||||
return (ps, names)
|
||||
|
||||
getModNames :: REPL [I.ModName]
|
||||
getModNames =
|
||||
do me <- getModuleEnv
|
||||
return $ map M.lmName $ M.getLoadedModules $ M.meLoadedModules me
|
||||
|
||||
getModuleEnv :: REPL M.ModuleEnv
|
||||
getModuleEnv = eModuleEnv `fmap` getRW
|
||||
|
||||
@ -440,6 +471,7 @@ setDynEnv denv = do
|
||||
me <- getModuleEnv
|
||||
setModuleEnv (me { M.meDynEnv = denv })
|
||||
|
||||
|
||||
-- | Given an existing qualified name, prefix it with a
|
||||
-- relatively-unique string. We make it unique by prefixing with a
|
||||
-- character @#@ that is not lexically valid in a module name.
|
||||
@ -493,31 +525,21 @@ setUser :: String -> String -> REPL ()
|
||||
setUser name val = case lookupTrieExact name userOptions of
|
||||
|
||||
[opt] -> setUserOpt opt
|
||||
[] -> io (putStrLn ("Unknown env value `" ++ name ++ "`"))
|
||||
_ -> io (putStrLn ("Ambiguous env value `" ++ name ++ "`"))
|
||||
[] -> rPutStrLn ("Unknown env value `" ++ name ++ "`")
|
||||
_ -> rPutStrLn ("Ambiguous env value `" ++ name ++ "`")
|
||||
|
||||
where
|
||||
setUserOpt opt = case optDefault opt of
|
||||
EnvString _ -> do r <- io (optCheck opt (EnvString val))
|
||||
case r of
|
||||
Just err -> io (putStrLn err)
|
||||
Nothing -> writeEnv (EnvString val)
|
||||
EnvString _ -> doCheck (EnvString val)
|
||||
|
||||
EnvProg _ _ ->
|
||||
case splitOptArgs val of
|
||||
prog:args -> do r <- io (optCheck opt (EnvProg prog args))
|
||||
case r of
|
||||
Just err -> io (putStrLn err)
|
||||
Nothing -> writeEnv (EnvProg prog args)
|
||||
[] -> io (putStrLn ("Failed to parse command for field, `" ++ name ++ "`"))
|
||||
prog:args -> doCheck (EnvProg prog args)
|
||||
[] -> rPutStrLn ("Failed to parse command for field, `" ++ name ++ "`")
|
||||
|
||||
EnvNum _ -> case reads val of
|
||||
[(x,_)] -> do r <- io (optCheck opt (EnvNum x))
|
||||
case r of
|
||||
Just err -> io (putStrLn err)
|
||||
Nothing -> writeEnv (EnvNum x)
|
||||
|
||||
_ -> io (putStrLn ("Failed to parse number for field, `" ++ name ++ "`"))
|
||||
[(x,_)] -> doCheck (EnvNum x)
|
||||
_ -> rPutStrLn ("Failed to parse number for field, `" ++ name ++ "`")
|
||||
|
||||
EnvBool _
|
||||
| any (`isPrefixOf` val) ["enable","on","yes"] ->
|
||||
@ -525,12 +547,16 @@ setUser name val = case lookupTrieExact name userOptions of
|
||||
| any (`isPrefixOf` val) ["disable","off","no"] ->
|
||||
writeEnv (EnvBool False)
|
||||
| otherwise ->
|
||||
io (putStrLn ("Failed to parse boolean for field, `" ++ name ++ "`"))
|
||||
rPutStrLn ("Failed to parse boolean for field, `" ++ name ++ "`")
|
||||
where
|
||||
|
||||
doCheck v = do (r,ws) <- io (optCheck opt v)
|
||||
case r of
|
||||
Just err -> rPutStrLn err
|
||||
Nothing -> do mapM_ rPutStrLn ws
|
||||
writeEnv v
|
||||
writeEnv ev =
|
||||
do optEff opt ev
|
||||
modifyRW_ (\rw -> rw { eUserEnv = Map.insert name ev (eUserEnv rw) })
|
||||
modifyRW_ (\rw -> rw { eUserEnv = Map.insert (optName opt) ev (eUserEnv rw) })
|
||||
|
||||
splitOptArgs :: String -> [String]
|
||||
splitOptArgs = unfoldr (parse "")
|
||||
@ -582,16 +608,24 @@ mkOptionMap = foldl insert emptyTrie
|
||||
where
|
||||
insert m d = insertTrie (optName d) d m
|
||||
|
||||
-- | Returns maybe an error, and some warnings
|
||||
type Checker = EnvVal -> IO (Maybe String, [String])
|
||||
|
||||
noCheck :: Checker
|
||||
noCheck _ = return (Nothing, [])
|
||||
|
||||
noWarns :: Maybe String -> IO (Maybe String, [String])
|
||||
noWarns mb = return (mb, [])
|
||||
|
||||
data OptionDescr = OptionDescr
|
||||
{ optName :: String
|
||||
, optDefault :: EnvVal
|
||||
, optCheck :: EnvVal -> IO (Maybe String)
|
||||
, optCheck :: Checker
|
||||
, optHelp :: String
|
||||
, optEff :: EnvVal -> REPL ()
|
||||
}
|
||||
|
||||
simpleOpt :: String -> EnvVal -> (EnvVal -> IO (Maybe String)) -> String
|
||||
-> OptionDescr
|
||||
simpleOpt :: String -> EnvVal -> Checker -> String -> OptionDescr
|
||||
simpleOpt optName optDefault optCheck optHelp =
|
||||
OptionDescr { optEff = \ _ -> return (), .. }
|
||||
|
||||
@ -599,32 +633,32 @@ userOptions :: OptionMap
|
||||
userOptions = mkOptionMap
|
||||
[ simpleOpt "base" (EnvNum 16) checkBase
|
||||
"the base to display words at"
|
||||
, simpleOpt "debug" (EnvBool False) (const $ return Nothing)
|
||||
, simpleOpt "debug" (EnvBool False) noCheck
|
||||
"enable debugging output"
|
||||
, simpleOpt "ascii" (EnvBool False) (const $ return Nothing)
|
||||
, simpleOpt "ascii" (EnvBool False) noCheck
|
||||
"display 7- or 8-bit words using ASCII notation."
|
||||
, simpleOpt "infLength" (EnvNum 5) checkInfLength
|
||||
"The number of elements to display for infinite sequences."
|
||||
, simpleOpt "tests" (EnvNum 100) (const $ return Nothing)
|
||||
, simpleOpt "tests" (EnvNum 100) noCheck
|
||||
"The number of random tests to try."
|
||||
, simpleOpt "satNum" (EnvString "1") checkSatNum
|
||||
"The maximum number of :sat solutions to display (\"all\" for no limit)."
|
||||
, simpleOpt "prover" (EnvString "z3") checkProver $
|
||||
"The external SMT solver for :prove and :sat (" ++ proverListString ++ ")."
|
||||
, simpleOpt "warnDefaulting" (EnvBool True) (const $ return Nothing)
|
||||
, simpleOpt "warnDefaulting" (EnvBool True) noCheck
|
||||
"Choose if we should display warnings when defaulting."
|
||||
, simpleOpt "warnShadowing" (EnvBool True) (const $ return Nothing)
|
||||
, simpleOpt "warnShadowing" (EnvBool True) noCheck
|
||||
"Choose if we should display warnings when shadowing symbols."
|
||||
, simpleOpt "smtfile" (EnvString "-") (const $ return Nothing)
|
||||
, simpleOpt "smtfile" (EnvString "-") noCheck
|
||||
"The file to use for SMT-Lib scripts (for debugging or offline proving)"
|
||||
, OptionDescr "mono-binds" (EnvBool True) (const $ return Nothing)
|
||||
, OptionDescr "mono-binds" (EnvBool True) noCheck
|
||||
"Whether or not to generalize bindings in a where-clause" $
|
||||
\case EnvBool b -> do me <- getModuleEnv
|
||||
setModuleEnv me { M.meMonoBinds = b }
|
||||
_ -> return ()
|
||||
|
||||
, OptionDescr "tc-solver" (EnvProg "z3" [ "-smt2", "-t:5000", "-in" ])
|
||||
(const (return Nothing)) -- TODO: check for the program in the path
|
||||
, OptionDescr "tc-solver" (EnvProg "z3" [ "-smt2", "-in" ])
|
||||
noCheck -- TODO: check for the program in the path
|
||||
"The solver that will be used by the type checker" $
|
||||
\case EnvProg prog args -> do me <- getModuleEnv
|
||||
let cfg = M.meSolverConfig me
|
||||
@ -634,14 +668,14 @@ userOptions = mkOptionMap
|
||||
_ -> return ()
|
||||
|
||||
, OptionDescr "tc-debug" (EnvNum 0)
|
||||
(const (return Nothing))
|
||||
noCheck
|
||||
"Enable type-checker debugging output" $
|
||||
\case EnvNum n -> do me <- getModuleEnv
|
||||
let cfg = M.meSolverConfig me
|
||||
setModuleEnv me { M.meSolverConfig = cfg{ T.solverVerbose = fromIntegral n } }
|
||||
_ -> return ()
|
||||
, OptionDescr "core-lint" (EnvBool False)
|
||||
(const (return Nothing))
|
||||
noCheck
|
||||
"Enable sanity checking of type-checker" $
|
||||
let setIt x = do me <- getModuleEnv
|
||||
setModuleEnv me { M.meCoreLint = x }
|
||||
@ -649,50 +683,53 @@ userOptions = mkOptionMap
|
||||
EnvBool False -> setIt M.NoCoreLint
|
||||
_ -> return ()
|
||||
|
||||
, simpleOpt "prover-stats" (EnvBool True) (const (return Nothing))
|
||||
, simpleOpt "prover-stats" (EnvBool True) noCheck
|
||||
"Enable prover timing statistics."
|
||||
]
|
||||
|
||||
|
||||
-- | Check the value to the `base` option.
|
||||
checkBase :: EnvVal -> IO (Maybe String)
|
||||
checkBase :: Checker
|
||||
checkBase val = case val of
|
||||
EnvNum n
|
||||
| n >= 2 && n <= 36 -> return Nothing
|
||||
| otherwise -> return $ Just "base must fall between 2 and 36"
|
||||
_ -> return $ Just "unable to parse a value for base"
|
||||
| n >= 2 && n <= 36 -> noWarns Nothing
|
||||
| otherwise -> noWarns $ Just "base must fall between 2 and 36"
|
||||
_ -> noWarns $ Just "unable to parse a value for base"
|
||||
|
||||
checkInfLength :: EnvVal -> IO (Maybe String)
|
||||
checkInfLength :: Checker
|
||||
checkInfLength val = case val of
|
||||
EnvNum n
|
||||
| n >= 0 -> return Nothing
|
||||
| otherwise -> return $ Just "the number of elements should be positive"
|
||||
_ -> return $ Just "unable to parse a value for infLength"
|
||||
| n >= 0 -> noWarns Nothing
|
||||
| otherwise -> noWarns $ Just "the number of elements should be positive"
|
||||
_ -> noWarns $ Just "unable to parse a value for infLength"
|
||||
|
||||
checkProver :: EnvVal -> IO (Maybe String)
|
||||
checkProver :: Checker
|
||||
checkProver val = case val of
|
||||
EnvString s
|
||||
| s `notElem` proverNames -> return $ Just $ "Prover must be " ++ proverListString
|
||||
| s `elem` ["offline", "any"] -> return Nothing
|
||||
| otherwise -> do let prover = lookupProver s
|
||||
available <- sbvCheckSolverInstallation prover
|
||||
unless available $
|
||||
putStrLn $ "Warning: " ++ s ++ " installation not found"
|
||||
return Nothing
|
||||
| s `notElem` proverNames ->
|
||||
noWarns $ Just $ "Prover must be " ++ proverListString
|
||||
| s `elem` ["offline", "any"] -> noWarns Nothing
|
||||
| otherwise ->
|
||||
do let prover = lookupProver s
|
||||
available <- sbvCheckSolverInstallation prover
|
||||
let ws = if available
|
||||
then []
|
||||
else ["Warning: " ++ s ++ " installation not found"]
|
||||
return (Nothing, ws)
|
||||
|
||||
_ -> return $ Just "unable to parse a value for prover"
|
||||
_ -> noWarns $ Just "unable to parse a value for prover"
|
||||
|
||||
proverListString :: String
|
||||
proverListString = concatMap (++ ", ") (init proverNames) ++ "or " ++ last proverNames
|
||||
|
||||
checkSatNum :: EnvVal -> IO (Maybe String)
|
||||
checkSatNum :: Checker
|
||||
checkSatNum val = case val of
|
||||
EnvString "all" -> return Nothing
|
||||
EnvString "all" -> noWarns Nothing
|
||||
EnvString s ->
|
||||
case readMaybe s :: Maybe Int of
|
||||
Just n | n >= 1 -> return Nothing
|
||||
_ -> return $ Just "must be an integer > 0 or \"all\""
|
||||
_ -> return $ Just "unable to parse a value for satNum"
|
||||
Just n | n >= 1 -> noWarns Nothing
|
||||
_ -> noWarns $ Just "must be an integer > 0 or \"all\""
|
||||
_ -> noWarns $ Just "unable to parse a value for satNum"
|
||||
|
||||
getUserSatNum :: REPL SatNum
|
||||
getUserSatNum = do
|
||||
|
||||
@ -43,6 +43,7 @@ import Cryptol.TypeCheck.AST
|
||||
import Cryptol.Utils.Ident (Ident)
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.Logger(logPutStrLn)
|
||||
|
||||
import Prelude ()
|
||||
import Prelude.Compat
|
||||
@ -124,13 +125,14 @@ thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult]
|
||||
thmSMTResults (SBV.ThmResult r) = [r]
|
||||
|
||||
proverError :: String -> M.ModuleCmd (Maybe SBV.Solver, ProverResult)
|
||||
proverError msg modEnv =
|
||||
proverError msg (_,modEnv) =
|
||||
return (Right ((Nothing, ProverError msg), modEnv), [])
|
||||
|
||||
satProve :: ProverCommand -> M.ModuleCmd (Maybe SBV.Solver, ProverResult)
|
||||
satProve ProverCommand {..} =
|
||||
protectStack proverError $ \modEnv ->
|
||||
M.runModuleM modEnv $ do
|
||||
protectStack proverError $ \(evo,modEnv) ->
|
||||
|
||||
M.runModuleM (evo,modEnv) $ do
|
||||
let (isSat, mSatNum) = case pcQueryType of
|
||||
ProveQuery -> (False, Nothing)
|
||||
SatQuery sn -> case sn of
|
||||
@ -145,14 +147,19 @@ satProve ProverCommand {..} =
|
||||
|
||||
let provers' = [ p { SBV.timing = SaveTiming pcProverStats, SBV.verbose = pcVerbose } | p <- provers ]
|
||||
let tyFn = if isSat then existsFinType else forallFinType
|
||||
let lPutStrLn = M.withLogger logPutStrLn
|
||||
let doEval :: MonadIO m => Eval.Eval a -> m a
|
||||
doEval m = liftIO $ Eval.runEval evo m
|
||||
let runProver fn tag e = do
|
||||
case provers of
|
||||
[prover] -> do
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Trying proof with " ++ show (SBV.name (SBV.solver prover))
|
||||
when pcVerbose $
|
||||
lPutStrLn $ "Trying proof with " ++
|
||||
show (SBV.name (SBV.solver prover))
|
||||
res <- M.io (fn prover e)
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Got result from " ++ show (SBV.name (SBV.solver prover))
|
||||
when pcVerbose $
|
||||
lPutStrLn $ "Got result from " ++
|
||||
show (SBV.name (SBV.solver prover))
|
||||
return (Just (SBV.name (SBV.solver prover)), tag res)
|
||||
_ ->
|
||||
return ( Nothing
|
||||
@ -162,12 +169,13 @@ satProve ProverCommand {..} =
|
||||
| prover <- provers ]
|
||||
)
|
||||
runProvers fn tag e = do
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Trying proof with " ++
|
||||
intercalate ", " (map (show . SBV.name . SBV.solver) provers)
|
||||
when pcVerbose $
|
||||
lPutStrLn $ "Trying proof with " ++
|
||||
intercalate ", " (map (show . SBV.name . SBV.solver) provers)
|
||||
(firstProver, timeElapsed, res) <- M.io (fn provers' e)
|
||||
when pcVerbose $ M.io $
|
||||
putStrLn $ "Got result from " ++ show firstProver ++ ", time: " ++ showTDiff timeElapsed
|
||||
when pcVerbose $
|
||||
lPutStrLn $ "Got result from " ++ show firstProver ++
|
||||
", time: " ++ showTDiff timeElapsed
|
||||
return (Just firstProver, tag res)
|
||||
let runFn = case pcQueryType of
|
||||
ProveQuery -> runProvers SBV.proveWithAny thmSMTResults
|
||||
@ -176,15 +184,14 @@ satProve ProverCommand {..} =
|
||||
_ -> runProver SBV.allSatWith allSatSMTResults
|
||||
case predArgTypes pcSchema of
|
||||
Left msg -> return (Nothing, ProverError msg)
|
||||
Right ts -> do when pcVerbose $ M.io $ putStrLn "Simulating..."
|
||||
v <- M.io $ Eval.runEval $ do
|
||||
env <- Eval.evalDecls extDgs mempty
|
||||
Eval.evalExpr env pcExpr
|
||||
Right ts -> do when pcVerbose $ lPutStrLn "Simulating..."
|
||||
v <- doEval $ do env <- Eval.evalDecls extDgs mempty
|
||||
Eval.evalExpr env pcExpr
|
||||
prims <- M.getPrimMap
|
||||
runRes <- runFn $ do
|
||||
args <- mapM tyFn ts
|
||||
b <- liftIO $ Eval.runEval
|
||||
(fromVBit <$> foldM fromVFun v (map Eval.ready args))
|
||||
b <- doEval (fromVBit <$>
|
||||
foldM fromVFun v (map Eval.ready args))
|
||||
return b
|
||||
let (firstProver, results') = runRes
|
||||
results = maybe results' (\n -> take n results') mSatNum
|
||||
@ -199,8 +206,8 @@ satProve ProverCommand {..} =
|
||||
let Right (_, cws) = SBV.getModelAssignment result
|
||||
(vs, _) = parseValues ts cws
|
||||
sattys = unFinType <$> ts
|
||||
satexprs <- liftIO $ Eval.runEval
|
||||
(zipWithM (Eval.toExpr prims) sattys vs)
|
||||
satexprs <-
|
||||
doEval (zipWithM (Eval.toExpr prims) sattys vs)
|
||||
case zip3 sattys <$> (sequence satexprs) <*> pure vs of
|
||||
Nothing ->
|
||||
panic "Cryptol.Symbolic.sat"
|
||||
@ -221,7 +228,8 @@ satProve ProverCommand {..} =
|
||||
|
||||
satProveOffline :: ProverCommand -> M.ModuleCmd (Either String String)
|
||||
satProveOffline ProverCommand {..} =
|
||||
protectStack (\msg modEnv -> return (Right (Left msg, modEnv), [])) $ \modEnv -> do
|
||||
protectStack (\msg (_,modEnv) -> return (Right (Left msg, modEnv), [])) $
|
||||
\(evOpts,modEnv) -> do
|
||||
let isSat = case pcQueryType of
|
||||
ProveQuery -> False
|
||||
SatQuery _ -> True
|
||||
@ -230,14 +238,14 @@ satProveOffline ProverCommand {..} =
|
||||
case predArgTypes pcSchema of
|
||||
Left msg -> return (Right (Left msg, modEnv), [])
|
||||
Right ts ->
|
||||
do when pcVerbose $ putStrLn "Simulating..."
|
||||
v <- liftIO $ Eval.runEval $
|
||||
do when pcVerbose $ logPutStrLn (Eval.evalLogger evOpts) "Simulating..."
|
||||
v <- liftIO $ Eval.runEval evOpts $
|
||||
do env <- Eval.evalDecls extDgs mempty
|
||||
Eval.evalExpr env pcExpr
|
||||
smtlib <- SBV.generateSMTBenchmark isSat $ do
|
||||
args <- mapM tyFn ts
|
||||
liftIO $ Eval.runEval
|
||||
(fromVBit <$> foldM fromVFun v (map Eval.ready args))
|
||||
liftIO $ Eval.runEval evOpts
|
||||
(fromVBit <$> foldM fromVFun v (map Eval.ready args))
|
||||
return (Right (Right smtlib, modEnv), [])
|
||||
|
||||
protectStack :: (String -> M.ModuleCmd a)
|
||||
|
||||
@ -341,16 +341,19 @@ indexFront mblen a xs idx
|
||||
case asWordList wvs of
|
||||
Just ws ->
|
||||
return $ VWord n $ ready $ WordVal $ SBV.svSelect ws (wordLit wlen 0) idx
|
||||
Nothing -> foldr f def [0 .. 2^w - 1]
|
||||
Nothing -> foldr f def idxs
|
||||
|
||||
| otherwise
|
||||
= foldr f def [0 .. 2^w - 1]
|
||||
= foldr f def idxs
|
||||
|
||||
where
|
||||
k = SBV.kindOf idx
|
||||
w = SBV.intSizeOf idx
|
||||
def = ready $ zeroV a
|
||||
f n y = iteValue (SBV.svEqual idx (SBV.svInteger k n)) (lookupSeqMap xs n) y
|
||||
idxs = case mblen of
|
||||
Just n | n < 2^w -> [0 .. n-1]
|
||||
_ -> [0 .. 2^w - 1]
|
||||
|
||||
|
||||
indexBack :: Maybe Integer
|
||||
|
||||
@ -37,11 +37,11 @@ isPass _ = False
|
||||
-- Note that this function assumes that the values come from a call to
|
||||
-- `testableType` (i.e., things are type-correct). We run in the IO
|
||||
-- monad in order to catch any @EvalError@s.
|
||||
runOneTest :: Value -> [Value] -> IO TestResult
|
||||
runOneTest v0 vs0 = run `X.catch` handle
|
||||
runOneTest :: EvalOpts -> Value -> [Value] -> IO TestResult
|
||||
runOneTest evOpts v0 vs0 = run `X.catch` handle
|
||||
where
|
||||
run = do
|
||||
result <- runEval (go v0 vs0)
|
||||
result <- runEval evOpts (go v0 vs0)
|
||||
if result
|
||||
then return Pass
|
||||
else return (FailFalse vs0)
|
||||
|
||||
@ -11,7 +11,7 @@
|
||||
{-# LANGUAGE BangPatterns #-}
|
||||
module Cryptol.Testing.Random where
|
||||
|
||||
import Cryptol.Eval.Monad (ready)
|
||||
import Cryptol.Eval.Monad (ready,EvalOpts)
|
||||
import Cryptol.Eval.Value (BV(..),Value,GenValue(..),SeqMap(..), WordValue(..), BitWord(..))
|
||||
import qualified Cryptol.Testing.Concrete as Conc
|
||||
import Cryptol.TypeCheck.AST (Type(..),TCon(..),TC(..),tNoUser)
|
||||
@ -35,15 +35,16 @@ type Gen g b w i = Integer -> g -> (GenValue b w i, g)
|
||||
the supplied value, otherwise we'll panic.
|
||||
-}
|
||||
runOneTest :: RandomGen g
|
||||
=> Value -- ^ Function under test
|
||||
=> EvalOpts -- ^ how to evaluate things
|
||||
-> Value -- ^ Function under test
|
||||
-> [Gen g Bool BV Integer] -- ^ Argument generators
|
||||
-> Integer -- ^ Size
|
||||
-> g
|
||||
-> IO (Conc.TestResult, g)
|
||||
runOneTest fun argGens sz g0 = do
|
||||
runOneTest evOpts fun argGens sz g0 = do
|
||||
let (args, g1) = foldr mkArg ([], g0) argGens
|
||||
mkArg argGen (as, g) = let (a, g') = argGen sz g in (a:as, g')
|
||||
result <- Conc.runOneTest fun args
|
||||
result <- Conc.runOneTest evOpts fun args
|
||||
return (result, g1)
|
||||
|
||||
{- | Given a (function) type, compute generators for
|
||||
@ -140,11 +141,4 @@ randomRecord gens sz = go [] gens
|
||||
let (v, g1) = mkElem sz g
|
||||
in seq v (go ((l,ready v) : els) more g1)
|
||||
|
||||
{-
|
||||
test = do
|
||||
g <- newStdGen
|
||||
let (s,_) = randomSequence 100 (randomWord 256) 100 g
|
||||
print $ ppValue defaultPPOpts { useBase = 16 } s
|
||||
-}
|
||||
|
||||
|
||||
|
||||
@ -62,13 +62,13 @@ modify f = get >>= (set . f)
|
||||
-- type-specialized versions of all functions called (transitively) by
|
||||
-- the body of the expression.
|
||||
specialize :: Expr -> M.ModuleCmd Expr
|
||||
specialize expr modEnv = run $ do
|
||||
specialize expr (ev,modEnv) = run $ do
|
||||
let extDgs = allDeclGroups modEnv
|
||||
let (tparams, expr') = destETAbs expr
|
||||
spec' <- specializeEWhere expr' extDgs
|
||||
return (foldr ETAbs spec' tparams)
|
||||
where
|
||||
run = M.runModuleT modEnv . fmap fst . runSpecT Map.empty
|
||||
run = M.runModuleT (ev,modEnv) . fmap fst . runSpecT Map.empty
|
||||
|
||||
specializeExpr :: Expr -> SpecM Expr
|
||||
specializeExpr expr =
|
||||
|
||||
@ -1,4 +1,4 @@
|
||||
module Cryptol.TypeCheck.CheckModuleInstance (inferModuleInstance) where
|
||||
module Cryptol.TypeCheck.CheckModuleInstance (checkModuleInstance) where
|
||||
|
||||
import Data.Map ( Map )
|
||||
import qualified Data.Map as Map
|
||||
|
||||
@ -3,7 +3,7 @@ module Cryptol.TypeCheck.SimpType where
|
||||
|
||||
import Control.Applicative((<|>))
|
||||
import Cryptol.TypeCheck.Type hiding
|
||||
(tSub,tMul,tDiv,tMod,tExp,tMin,tWidth,tLenFromThen,tLenFromThenTo)
|
||||
(tSub,tMul,tDiv,tMod,tExp,tMin,tWidth,tCeilDiv,tCeilMod,tLenFromThen,tLenFromThenTo)
|
||||
import Cryptol.TypeCheck.TypePat
|
||||
import Cryptol.TypeCheck.Solver.InfNat
|
||||
import Control.Monad(msum,guard)
|
||||
@ -33,6 +33,8 @@ tRebuild' withUser = go
|
||||
(TCMin,[x,y]) -> tMin x y
|
||||
(TCMax,[x,y]) -> tMax x y
|
||||
(TCWidth,[x]) -> tWidth x
|
||||
(TCCeilDiv,[x,y]) -> tCeilDiv x y
|
||||
(TCCeilMod,[x,y]) -> tCeilMod x y
|
||||
(TCLenFromThen,[x,y,z]) -> tLenFromThen x y z
|
||||
(TCLenFromThenTo,[x,y,z]) -> tLenFromThenTo x y z
|
||||
_ -> TCon tc ts
|
||||
@ -166,7 +168,6 @@ tDiv x y
|
||||
| Just 0 <- tIsNum y = tBadNumber $ TCErrorMessage "Division by 0."
|
||||
| otherwise = tf2 TCDiv x y
|
||||
|
||||
|
||||
tMod :: Type -> Type -> Type
|
||||
tMod x y
|
||||
| Just t <- tOp TCMod (op2 nMod) [x,y] = t
|
||||
@ -174,6 +175,22 @@ tMod x y
|
||||
| Just 0 <- tIsNum x = tBadNumber $ TCErrorMessage "Modulus by 0."
|
||||
| otherwise = tf2 TCMod x y
|
||||
|
||||
tCeilDiv :: Type -> Type -> Type
|
||||
tCeilDiv x y
|
||||
| Just t <- tOp TCCeilDiv (op2 nCeilDiv) [x,y] = t
|
||||
| tIsInf x = tBadNumber $ TCErrorMessage "CeilDiv of `inf`."
|
||||
| tIsInf y = tBadNumber $ TCErrorMessage "CeilDiv by `inf`."
|
||||
| Just 0 <- tIsNum y = tBadNumber $ TCErrorMessage "CeilDiv by 0."
|
||||
| otherwise = tf2 TCCeilDiv x y
|
||||
|
||||
tCeilMod :: Type -> Type -> Type
|
||||
tCeilMod x y
|
||||
| Just t <- tOp TCCeilMod (op2 nCeilMod) [x,y] = t
|
||||
| tIsInf x = tBadNumber $ TCErrorMessage "CeilMod of `inf`."
|
||||
| tIsInf y = tBadNumber $ TCErrorMessage "CeilMod by `inf`."
|
||||
| Just 0 <- tIsNum x = tBadNumber $ TCErrorMessage "CeilMod to size 0."
|
||||
| otherwise = tf2 TCCeilMod x y
|
||||
|
||||
tExp :: Type -> Type -> Type
|
||||
tExp x y
|
||||
| Just t <- tOp TCExp (total (op2 nExp)) [x,y] = t
|
||||
|
||||
@ -121,6 +121,26 @@ nMod Inf _ = Nothing
|
||||
nMod (Nat x) (Nat y) = Just (Nat (mod x y))
|
||||
nMod (Nat x) Inf = Just (Nat x) -- inf * 0 + x = 0 + x
|
||||
|
||||
-- | @nCeilDiv msgLen blockSize@ computes the least @n@ such that
|
||||
-- @msgLen <= blockSize * n@. It is undefined when @blockSize = 0@.
|
||||
-- It is also undefined when either input is infinite; perhaps this
|
||||
-- could be relaxed later.
|
||||
nCeilDiv :: Nat' -> Nat' -> Maybe Nat'
|
||||
nCeilDiv _ (Nat 0) = Nothing
|
||||
nCeilDiv Inf _ = Nothing
|
||||
nCeilDiv (Nat _) Inf = Nothing
|
||||
nCeilDiv (Nat x) (Nat y) = Just (Nat (- div (- x) y))
|
||||
|
||||
-- | @nCeilMod msgLen blockSize@ computes the least @k@ such that
|
||||
-- @blockSize@ divides @msgLen + k@. It is undefined when @blockSize = 0@.
|
||||
-- It is also undefined when either input is infinite; perhaps this
|
||||
-- could be relaxed later.
|
||||
nCeilMod :: Nat' -> Nat' -> Maybe Nat'
|
||||
nCeilMod _ (Nat 0) = Nothing
|
||||
nCeilMod Inf _ = Nothing
|
||||
nCeilMod (Nat _) Inf = Nothing
|
||||
nCeilMod (Nat x) (Nat y) = Just (Nat (mod (- x) y))
|
||||
|
||||
-- | Rounds up.
|
||||
-- @lg2 x = y@, iff @y@ is the smallest number such that @x <= 2 ^ y@
|
||||
nLg2 :: Nat' -> Nat'
|
||||
|
||||
@ -86,6 +86,8 @@ cryIsFinType varInfo ty =
|
||||
|
||||
(TCMax, [t1,t2]) -> SolvedIf [ pFin t1, pFin t2 ]
|
||||
(TCWidth, [t1]) -> SolvedIf [ pFin t1 ]
|
||||
(TCCeilDiv, [_,_]) -> SolvedIf []
|
||||
(TCCeilMod, [_,_]) -> SolvedIf []
|
||||
(TCLenFromThen,[_,_,_]) -> SolvedIf []
|
||||
(TCLenFromThenTo,[_,_,_]) -> SolvedIf []
|
||||
|
||||
|
||||
@ -319,6 +319,8 @@ toSMT tvs ty = matchDefault (panic "toSMT" [ "Unexpected type", show ty ])
|
||||
, aMin ~> "cryMin"
|
||||
, aMax ~> "cryMax"
|
||||
, aWidth ~> "cryWidth"
|
||||
, aCeilDiv ~> "cryCeilDiv"
|
||||
, aCeilMod ~> "cryCeilMod"
|
||||
, aLenFromThen ~> "cryLenFromThen"
|
||||
, aLenFromThenTo ~> "cryLenFromThenTo"
|
||||
|
||||
|
||||
@ -126,6 +126,8 @@ apSubstMaybe su ty =
|
||||
(TCMin,[t1,t2]) -> Simp.tMin t1 t2
|
||||
(TCMax,[t1,t2]) -> Simp.tMax t1 t2
|
||||
(TCWidth,[t1]) -> Simp.tWidth t1
|
||||
(TCCeilDiv,[t1,t2]) -> Simp.tCeilDiv t1 t2
|
||||
(TCCeilMod,[t1,t2]) -> Simp.tCeilMod t1 t2
|
||||
(TCLenFromThen,[t1,t2,t3]) -> Simp.tLenFromThen t1 t2 t3
|
||||
(TCLenFromThenTo,[t1,t2,t3]) -> Simp.tLenFromThenTo t1 t2 t3
|
||||
_ -> panic "apSubstMaybe" ["Unexpected type function", show t]
|
||||
|
||||
@ -234,16 +234,18 @@ instance HasKind PC where
|
||||
instance HasKind TFun where
|
||||
kindOf tfun =
|
||||
case tfun of
|
||||
TCWidth -> KNum :-> KNum
|
||||
TCWidth -> KNum :-> KNum
|
||||
|
||||
TCAdd -> KNum :-> KNum :-> KNum
|
||||
TCSub -> KNum :-> KNum :-> KNum
|
||||
TCMul -> KNum :-> KNum :-> KNum
|
||||
TCDiv -> KNum :-> KNum :-> KNum
|
||||
TCMod -> KNum :-> KNum :-> KNum
|
||||
TCExp -> KNum :-> KNum :-> KNum
|
||||
TCMin -> KNum :-> KNum :-> KNum
|
||||
TCMax -> KNum :-> KNum :-> KNum
|
||||
TCAdd -> KNum :-> KNum :-> KNum
|
||||
TCSub -> KNum :-> KNum :-> KNum
|
||||
TCMul -> KNum :-> KNum :-> KNum
|
||||
TCDiv -> KNum :-> KNum :-> KNum
|
||||
TCMod -> KNum :-> KNum :-> KNum
|
||||
TCExp -> KNum :-> KNum :-> KNum
|
||||
TCMin -> KNum :-> KNum :-> KNum
|
||||
TCMax -> KNum :-> KNum :-> KNum
|
||||
TCCeilDiv -> KNum :-> KNum :-> KNum
|
||||
TCCeilMod -> KNum :-> KNum :-> KNum
|
||||
|
||||
TCLenFromThen -> KNum :-> KNum :-> KNum :-> KNum
|
||||
TCLenFromThenTo -> KNum :-> KNum :-> KNum :-> KNum
|
||||
@ -582,6 +584,12 @@ tMin = tf2 TCMin
|
||||
tWidth :: Type -> Type
|
||||
tWidth = tf1 TCWidth
|
||||
|
||||
tCeilDiv :: Type -> Type -> Type
|
||||
tCeilDiv = tf2 TCCeilDiv
|
||||
|
||||
tCeilMod :: Type -> Type -> Type
|
||||
tCeilMod = tf2 TCCeilMod
|
||||
|
||||
tLenFromThen :: Type -> Type -> Type -> Type
|
||||
tLenFromThen = tf3 TCLenFromThen
|
||||
|
||||
|
||||
@ -4,6 +4,7 @@ module Cryptol.TypeCheck.TypePat
|
||||
, anAdd, (|-|), aMul, (|^|), (|/|), (|%|)
|
||||
, aMin, aMax
|
||||
, aWidth
|
||||
, aCeilDiv, aCeilMod
|
||||
, aLenFromThen, aLenFromThenTo
|
||||
|
||||
, aTVar
|
||||
@ -101,6 +102,12 @@ aMax = tf TCMax ar2
|
||||
aWidth :: Pat Type Type
|
||||
aWidth = tf TCWidth ar1
|
||||
|
||||
aCeilDiv :: Pat Type (Type,Type)
|
||||
aCeilDiv = tf TCCeilDiv ar2
|
||||
|
||||
aCeilMod :: Pat Type (Type,Type)
|
||||
aCeilMod = tf TCCeilMod ar2
|
||||
|
||||
aLenFromThen :: Pat Type (Type,Type,Type)
|
||||
aLenFromThen = tf TCLenFromThen ar3
|
||||
|
||||
|
||||
56
src/Cryptol/Utils/Logger.hs
Normal file
56
src/Cryptol/Utils/Logger.hs
Normal file
@ -0,0 +1,56 @@
|
||||
-- | A simple system so that the Cryptol driver can communicate
|
||||
-- with users (or not).
|
||||
module Cryptol.Utils.Logger
|
||||
( Logger
|
||||
|
||||
, stdoutLogger
|
||||
, handleLogger
|
||||
, quietLogger
|
||||
, funLogger
|
||||
|
||||
, logPutStr
|
||||
, logPutStrLn
|
||||
, logPrint
|
||||
) where
|
||||
|
||||
import System.IO(Handle, hPutStr, stdout)
|
||||
import Control.DeepSeq(NFData(..))
|
||||
|
||||
-- | A logger provides simple abstraction for sending messages.
|
||||
newtype Logger = Logger (String -> IO ())
|
||||
|
||||
instance NFData Logger where
|
||||
rnf (Logger x) = rnf x
|
||||
|
||||
-- | Send the given string to the log.
|
||||
logPutStr :: Logger -> String -> IO ()
|
||||
logPutStr (Logger f) = f
|
||||
|
||||
-- | Send the given string with a newline at the end.
|
||||
logPutStrLn :: Logger -> String -> IO ()
|
||||
logPutStrLn l s = logPutStr l (s ++ "\n")
|
||||
|
||||
-- | Send the given value using its 'Show' instance.
|
||||
-- Adds a newline at the end.
|
||||
logPrint :: Show a => Logger -> a -> IO ()
|
||||
logPrint l a = logPutStrLn l (show a)
|
||||
|
||||
-- | A logger that ignores all messages.
|
||||
quietLogger :: Logger
|
||||
quietLogger = Logger (const (return ()))
|
||||
|
||||
-- | Log to the given handle.
|
||||
handleLogger :: Handle -> Logger
|
||||
handleLogger h = Logger (hPutStr h)
|
||||
|
||||
-- | Log to stdout.
|
||||
stdoutLogger :: Logger
|
||||
stdoutLogger = handleLogger stdout
|
||||
|
||||
-- | Just use this function for logging.
|
||||
funLogger :: (String -> IO ()) -> Logger
|
||||
funLogger = Logger
|
||||
|
||||
|
||||
|
||||
|
||||
@ -6,10 +6,10 @@ testing...passed 1 tests.
|
||||
Q.E.D.
|
||||
property t1 Using random testing.
|
||||
testing...passed 100 tests.
|
||||
Coverage: 0.00% (100 of 2^^32 values)
|
||||
Expected test coverage: 0.00% (100 of 2^^32 values)
|
||||
property t2 Using random testing.
|
||||
testing...passed 100 tests.
|
||||
Coverage: 0.00% (100 of 2^^64 values)
|
||||
Expected test coverage: 0.00% (100 of 2^^64 values)
|
||||
property f0 Using exhaustive testing.
|
||||
testing...f0 = False
|
||||
:prove t0
|
||||
|
||||
@ -1,7 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Using random testing.
|
||||
testing...passed 100 tests.
|
||||
Coverage: 39.06% (100 of 256 values)
|
||||
Expected test coverage: 32.39% (83 of 256 values)
|
||||
Using exhaustive testing.
|
||||
testing...passed 256 tests.
|
||||
Q.E.D.
|
||||
|
||||
@ -1 +0,0 @@
|
||||
https://github.com/GaloisInc/cryptol/issues/224
|
||||
@ -3,4 +3,4 @@ Loading module Cryptol
|
||||
Loading module Karatsuba
|
||||
Using random testing.
|
||||
testing...passed 100 tests.
|
||||
Coverage: 0.00% (100 of 2^^118 values)
|
||||
Expected test coverage: 0.00% (100 of 2^^118 values)
|
||||
|
||||
@ -9,7 +9,7 @@ testing...passed 1 tests.
|
||||
Q.E.D.
|
||||
property moderately_bogus_property Using random testing.
|
||||
testing...passed 100 tests.
|
||||
Coverage: 39.06% (100 of 256 values)
|
||||
Expected test coverage: 32.39% (83 of 256 values)
|
||||
property x_eval Using exhaustive testing.
|
||||
testing...passed 1 tests.
|
||||
Q.E.D.
|
||||
|
||||
1
tests/issues/issue463.icry
Normal file
1
tests/issues/issue463.icry
Normal file
@ -0,0 +1 @@
|
||||
:prove \(i:[4]) (x:[10]) -> i < 10 ==> x@i == x@i
|
||||
2
tests/issues/issue463.icry.stdout
Normal file
2
tests/issues/issue463.icry.stdout
Normal file
@ -0,0 +1,2 @@
|
||||
Loading module Cryptol
|
||||
Q.E.D.
|
||||
@ -1,15 +1,15 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
Hi! 0
|
||||
Hi! 1
|
||||
Hi! 2
|
||||
Hi! 3
|
||||
Hi! 4
|
||||
Hi! 5
|
||||
Hi! 6
|
||||
Hi! 7
|
||||
Hi! 8
|
||||
Hi! 9
|
||||
Hi! 10
|
||||
Hi! 0x00
|
||||
Hi! 0x01
|
||||
Hi! 0x02
|
||||
Hi! 0x03
|
||||
Hi! 0x04
|
||||
Hi! 0x05
|
||||
Hi! 0x06
|
||||
Hi! 0x07
|
||||
Hi! 0x08
|
||||
Hi! 0x09
|
||||
Hi! 0x0a
|
||||
[0x14, 0x15, 0x16, 0x17, 0x18, 0x19, 0x1a, 0x1b, 0x1c, 0x1d, 0x1e]
|
||||
|
||||
@ -18,7 +18,7 @@ test3 x = x
|
||||
/**
|
||||
* Test that doc strings work on property declarations
|
||||
*/
|
||||
property test4 x = x
|
||||
property test4 x = (x : Bit)
|
||||
|
||||
/**
|
||||
* Test that doc strings work on fixity declarations
|
||||
|
||||
@ -9,4 +9,4 @@ testing...passed 1 tests.
|
||||
Q.E.D.
|
||||
Using random testing.
|
||||
testing...passed 100 tests.
|
||||
Coverage: 0.00% (100 of 2^^30 values)
|
||||
Expected test coverage: 0.00% (100 of 2^^30 values)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user