GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-24 15:08:58 +03:00
Code Issues Projects Releases Wiki Activity

Merge Cryptol/Extras.cry with Cryptol.cry

Browse Source 
Closes #427.
This commit is contained in:
Aaron Tomb 2018-05-23 15:48:31 -07:00
parent ddfe615a14
commit 99f3fdbf37
13 changed files with 137 additions and 736 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
bench/Main.hs
View File

@ -48,7 +48,6 @@ main = do
defaultMain [
bgroup "parser" [
parser "Prelude" "lib/Cryptol.cry"
, parser "Extras" "lib/Cryptol/Extras.cry"
, parser "PreludeWithExtras" "bench/data/PreludeWithExtras.cry"
, parser "BigSequence" "bench/data/BigSequence.cry"
, parser "BigSequenceHex" "bench/data/BigSequenceHex.cry"
@ -57,7 +56,6 @@ main = do
]
, bgroup "typechecker" [
tc cd "Prelude" "lib/Cryptol.cry"
, tc cd "Extras" "lib/Cryptol/Extras.cry"
, tc cd "PreludeWithExtras" "bench/data/PreludeWithExtras.cry"
, tc cd "BigSequence" "bench/data/BigSequence.cry"
, tc cd "BigSequenceHex" "bench/data/BigSequenceHex.cry"

179
cryptol-server/Cryptol/Aeson.hs
View File

@ -1,179 +0,0 @@
-- |
-- Module : Cryptol.Aeson
-- Copyright : (c) 2015-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
-- Orphan 'FromJSON' and 'ToJSON' instances for certain Cryptol
-- types. Since these are meant to be consumed over a wire, they are
-- mostly focused on base values and interfaces rather than a full
-- serialization of internal ASTs and such.
{-# LANGUAGE ExtendedDefaultRules #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -Wall -fno-warn-orphans -fno-warn-type-defaults #-}
module Cryptol.Aeson where
import Control.Applicative
import Control.Exception
import Data.Aeson
import Data.Aeson.TH
import qualified Data.Map as M
import qualified Data.Text as T
import qualified Cryptol.Eval.Error as E
import qualified Cryptol.Eval.Value as E
import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Monad as M
import qualified Cryptol.ModuleSystem.Renamer as M
import Cryptol.ModuleSystem.Interface
import Cryptol.ModuleSystem.Name
import qualified Cryptol.Parser as P
import qualified Cryptol.Parser.AST as P
import qualified Cryptol.Parser.Lexer as P
import qualified Cryptol.Parser.NoInclude as P
import qualified Cryptol.Parser.NoPat as NoPat
import qualified Cryptol.Parser.Position as P
import Cryptol.REPL.Monad
import qualified Cryptol.Testing.Concrete as Test
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.InferTypes as T
import Cryptol.Utils.Ident
import Cryptol.Utils.PP hiding (empty)
instance ToJSON Doc where
toJSON = String . T.pack . render
instance ToJSON E.Value where
toJSON = \case
E.VRecord fs -> object
[ "record" .= fs ]
E.VTuple vs -> object
[ "tuple" .= vs ]
E.VBit b -> object
[ "bit" .= b ]
E.VSeq isWord xs -> object
[ "sequence" .= object [ "isWord" .= isWord, "elements" .= xs ] ]
E.VWord w -> object
[ "word" .= w ]
E.VStream _ -> object
[ "stream" .= object [ "@note" .= "streams not supported" ] ]
E.VFun _ -> object
[ "function" .= object [ "@note" .= "functions not supported" ] ]
E.VPoly _ -> object
[ "poly" .= object [ "@note" .= "polymorphic values not supported" ] ]
instance FromJSON E.Value where
parseJSON = withObject "Value" $ \o ->
E.VRecord <$> o .: "record"
<|> E.VTuple <$> o .: "tuple"
<|> E.VBit <$> o .: "bit"
<|> do s <- o .: "sequence"
E.VSeq <$> s .: "isWord" <*> s .: "elements"
<|> E.VWord <$> o .: "word"
<|> error ("unexpected JSON value: " ++ show o)
instance ToJSON P.Token where
toJSON = toJSON . pp
instance ToJSON REPLException where
toJSON = \case
ParseError pe -> object
[ "ParseError" .= pe ]
FileNotFound fp -> object
[ "FileNotFound" .= fp ]
DirectoryNotFound fp -> object
[ "DirectoryNotFound" .= fp ]
NoPatError npe -> object
[ "NoPatError" .= npe ]
NoIncludeError nie -> object
[ "NoIncludeError" .= nie ]
EvalError ee -> object
[ "EvalError" .= ee ]
ModuleSystemError _nameDisp me -> object
[ "ModuleSystemError" .= me ]
EvalPolyError sch -> object
[ "EvalPolyError" .= sch ]
TypeNotTestable ty -> object
[ "TypeNotTestable" .= ty ]
instance ToJSON IOException where
toJSON exn = object
[ "IOException" .= show exn ]
instance ToJSON M.RenamerError where
toJSON err = object
[ "renamerError" .= pp err ]
instance ToJSON T.Error where
toJSON err = object
[ "inferError" .= pp err ]
instance ToJSON E.BV where
toJSON = \case
E.BV w v -> object
[ "bitvector" .= object [ "width" .= w, "value" .= v ] ]
instance FromJSON E.BV where
parseJSON = withObject "BV" $ \o -> do
bv <- o .: "bitvector"
E.BV <$> bv .: "width" <*> bv .: "value"
instance ToJSON Test.TestResult where
toJSON = \case
Test.Pass -> object [ "Pass" .= Null ]
Test.FailFalse args -> object [ "FailFalse" .= args ]
Test.FailError err args -> object
[ "FailError" .= show (pp err), "args" .= args ]
instance (ToJSON v) => ToJSON (M.Map Name v) where
toJSON = toJSON . M.mapKeys (unpackIdent . nameIdent)
{-# INLINE toJSON #-}
$(deriveJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''NameInfo)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''E.EvalError)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.ParseError)
$(deriveJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Position)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Located)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.IncludeError)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Schema)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Type)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.TParam)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Prop)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Named)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Kind)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''NoPat.Error)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''M.ModuleError)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''M.ImportSource)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Import)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.ImportSpec)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Type)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TParam)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Kind)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TVar)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TCon)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.PC)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TC)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.UserTC)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Schema)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TFun)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Selector)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } { fieldLabelModifier = drop 1 } ''T.Fixity)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Pragma)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Assoc)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Name)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''IfaceDecl)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.Newtype)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''T.TySyn)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''IfaceDecls)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Iface)
$(deriveJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Ident)
$(deriveJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Range)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.PName)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''P.Pass)
$(deriveToJSON defaultOptions { sumEncoding = ObjectWithSingleField } ''Test.TestReport)

386
cryptol-server/Main.hs
View File

@ -1,386 +0,0 @@
-- |
-- Module : Main
-- Copyright : (c) 2015-2016 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
-- Alpha version of a Cryptol server that communicates via JSON over
-- ZeroMQ. This API is highly unstable and extremely likely to change
-- in the near future.
{-# LANGUAGE CPP #-}
{-# LANGUAGE ExtendedDefaultRules #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -Wall -fno-warn-type-defaults #-}
module Main where
import Control.Concurrent
import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.Trans.Control
import qualified Control.Exception as X
import Data.Aeson
import Data.Aeson.Encode.Pretty
import qualified Data.ByteString.Char8 as BS
import qualified Data.ByteString.Lazy.Char8 as BSL
import Data.Char
import Data.IORef
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Text (Text)
import qualified Data.Text as T
import Data.Word
import Options.Applicative
import System.Environment
import System.Exit
import System.FilePath
import System.Posix.Signals
import System.ZMQ4
import Text.Read
import qualified Cryptol.Eval.Value as E
import Cryptol.REPL.Command
import Cryptol.REPL.Monad
import Cryptol.Symbolic (ProverResult(..))
import qualified Cryptol.Testing.Concrete as Test
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.ModuleSystem as M
import Cryptol.Utils.PP hiding ((<>))
import Cryptol.Aeson ()
import Prelude ()
import Prelude.Compat
data RCommand
= RCEvalExpr Text
| RCApplyFun FunHandle E.Value
| RCTypeOf Text
| RCSetOpt Text Text
| RCCheck Text
| RCExhaust Text
| RCProve Text
| RCSat Text
| RCLoadPrelude
| RCLoadModule FilePath
| RCDecls
| RCUnknownCmd Text
| RCExit
instance FromJSON RCommand where
parseJSON = withObject "RCommand" $ \o -> do
tag <- o .: "tag"
flip (withText "tag") tag $ \case
"evalExpr" -> RCEvalExpr <$> o .: "expr"
"applyFun" -> RCApplyFun <$> o .: "handle" <*> o .: "arg"
"typeOf" -> RCTypeOf <$> o .: "expr"
"setOpt" -> RCSetOpt <$> o .: "key" <*> o .: "value"
"check" -> RCCheck <$> o .: "expr"
"exhaust" -> RCExhaust <$> o .: "expr"
"prove" -> RCProve <$> o .: "expr"
"sat" -> RCSat <$> o .: "expr"
"loadPrelude" -> return RCLoadPrelude
"loadModule" -> RCLoadModule . T.unpack <$> o .: "filePath"
"browse" -> return RCDecls
"exit" -> return RCExit
unknown -> return (RCUnknownCmd unknown)
newtype FunHandle = FH Int
deriving (Eq, Ord, Enum, Bounded, Show)
instance ToJSON FunHandle where
toJSON (FH i) = toJSON i
instance FromJSON FunHandle where
parseJSON v = FH <$> parseJSON v
data RResult
= RRValue E.Value
| RRFunValue FunHandle T.Type
| RRType T.Schema String -- pretty-printed type
| RRDecls M.IfaceDecls
| RRCheck [Test.TestReport]
| RRExhaust [Test.TestReport]
| RRSat [[E.Value]]
-- ^ A list of satisfying assignments. Empty list means unsat, max
-- length determined by @satNum@ interpreter option
| RRProve (Maybe [E.Value])
-- ^ Counterexample if invalid or 'Nothing' if valid
| RRProverError String
| RRInteractiveError REPLException String -- pretty-printed exception
| RRUnknownCmd Text
| RRBadMessage BS.ByteString String
| RROk
| RRInterrupted
instance ToJSON RResult where
toJSON = \case
RRValue v -> object
[ "tag" .= "value", "value" .= v ]
RRFunValue fh t -> object
[ "tag" .= "funValue", "handle" .= fh, "type" .= t ]
RRType s pps -> object
[ "tag" .= "type", "value" .= s, "pp" .= pps ]
RRDecls ifds -> object
[ "tag" .= "decls", "decls" .= ifds ]
RRCheck out -> object
[ "tag" .= "check", "testReport" .= out ]
RRExhaust out -> object
[ "tag" .= "exhaust", "testReport" .= out ]
RRSat out -> object
[ "tag" .= "sat", "assignments" .= out ]
RRProve out -> object
[ "tag" .= "prove", "counterexample" .= out ]
RRProverError msg -> object
[ "tag" .= "proverError", "message" .= msg ]
RRInteractiveError err pps -> object
[ "tag" .= "interactiveError", "error" .= err, "pp" .= pps ]
RRUnknownCmd txt -> object
[ "tag" .= "unknownCommand", "command" .= txt ]
RRBadMessage msg err -> object
[ "tag" .= "badMessage", "message" .= BS.unpack msg, "error" .= err ]
RROk -> object
[ "tag" .= "ok" ]
RRInterrupted -> object
[ "tag" .= "interrupted" ]
data ControlMsg
= CMConnect
-- ^ Request a new Cryptol context and connection
| CMInterrupt Word16
-- ^ Request an interrupt of all current Cryptol contexts
| CMExit
-- ^ Request that the entire server shut down
| CMUnknown Text
-- ^ Unknown message
instance FromJSON ControlMsg where
parseJSON = withObject "ControlMsg" $ \o -> do
tag <- o .: "tag"
flip (withText "tag") tag $ \case
"connect" -> return CMConnect
"interrupt" -> CMInterrupt <$> o .: "port"
"exit" -> return CMExit
other -> return $ CMUnknown other
data ControlReply
= CRConnect Word16
-- ^ Return the port for a new connection
| CRInterrupted
-- ^ Acknowledge receipt of an interrupt command
| CRExiting
-- ^ Acknowledge receipt of an exit command
| CRBadMessage BS.ByteString String
-- ^ Acknowledge receipt of an ill-formed control message
instance ToJSON ControlReply where
toJSON = \case
CRConnect port -> object
[ "tag" .= "connect", "port" .= port ]
CRInterrupted -> object
[ "tag" .= "interrupted" ]
CRExiting -> object
[ "tag" .= "exiting" ]
CRBadMessage msg err -> object
[ "tag" .= "badMessage", "message" .= BS.unpack msg, "error" .= err ]
server :: Word16 -> IO ()
server port =
withContext $ \ctx ->
withSocket ctx Rep $ \rep -> do
let addr = "tcp://127.0.0.1:" ++ show port
putStrLn ("[cryptol-server] coming online at " ++ addr)
bind rep addr
workers <- newIORef Map.empty
let loop = do
msg <- receive rep
putStrLn "[cryptol-server] received message:"
case decodeStrict msg of
Nothing -> BS.putStrLn msg
Just js -> BSL.putStrLn (encodePretty (js :: Value))
case eitherDecodeStrict msg of
Left err -> reply rep $ CRBadMessage msg err
Right CMConnect -> do
putStrLn "[cryptol-server] handling new incoming connection"
newRep <- socket ctx Rep
bind newRep "tcp://127.0.0.1:*"
newAddr <- lastEndpoint newRep
let portStr = reverse . takeWhile isDigit . reverse $ newAddr
workerPort = read portStr
putStrLn ("[cryptol-server] starting worker on interface " ++ newAddr)
tid <- forkFinally (runRepl newRep) (removeWorker workers port)
addNewWorker workers workerPort tid
reply rep $ CRConnect workerPort
Right (CMInterrupt port') -> do
s <- readIORef workers
case Map.lookup port' s of
Nothing -> reply rep $ CRBadMessage msg "invalid worker port"
Just tid -> do
throwTo tid X.UserInterrupt
reply rep $ CRInterrupted
Right CMExit -> do
putStrLn "[cryptol-server] shutting down"
reply rep $ CRExiting
exitSuccess
Right (CMUnknown cmd) -> do
putStrLn ("[cryptol-server] unknown control command: " ++ T.unpack cmd)
reply rep $ CRBadMessage msg "unknown control command"
loop
loop
reply :: (ToJSON a, MonadIO m) => Socket Rep -> a -> m ()
reply rep msg = liftIO $ do
let bmsg = BS.concat . BSL.toChunks . encodePretty $ msg
putStrLn "[cryptol-server] sending response:"
BS.putStrLn bmsg
send rep [] bmsg
addNewWorker :: IORef (Map Word16 ThreadId) -> Word16 -> ThreadId -> IO ()
addNewWorker workers port tid =
atomicModifyIORef workers $ \s -> (Map.insert port tid s, ())
removeWorker :: IORef (Map Word16 ThreadId) -> Word16 -> a -> IO ()
removeWorker workers port _result =
atomicModifyIORef workers $ \s -> (Map.delete port s, ())
runRepl :: Socket Rep -> IO ()
runRepl rep = runREPL False stdoutLogger $ do -- TODO: batch mode?
mCryptolPath <- io $ lookupEnv "CRYPTOLPATH"
case mCryptolPath of
Nothing -> return ()
Just path -> prependSearchPath path'
#if defined(mingw32_HOST_OS) || defined(__MINGW32__)
-- Windows paths search from end to beginning
where path' = reverse (splitSearchPath path)
#else
where path' = splitSearchPath path
#endif
funHandles <- io $ newIORef (Map.empty, minBound :: FunHandle)
let handle err = reply rep (RRInteractiveError err (show (pp err)))
handleAsync :: X.AsyncException -> IO ()
handleAsync _int = reply rep RRInterrupted
loop = liftBaseWith $ \run -> X.handle handleAsync $ run $ do
msg <- io $ receive rep
io $ putStrLn "[cryptol-worker] received message:"
case decodeStrict msg of
Nothing -> io $ BS.putStrLn msg
Just js -> io $ BSL.putStrLn (encodePretty (js :: Value))
flip catch handle $ case eitherDecodeStrict msg of
Left cmdErr -> reply rep (RRBadMessage msg cmdErr)
Right rc -> case rc of
RCEvalExpr txt -> do
expr <- replParseExpr (T.unpack txt)
(val, ty) <- replEvalExpr expr
case val of
E.VFun f -> do
fh <- io $ atomicModifyIORef' funHandles $ \(m, fh) ->
let m' = Map.insert fh f m
fh' = succ fh
in ((m', fh'), fh)
reply rep (RRFunValue fh ty)
_ -> reply rep (RRValue val)
RCApplyFun fh arg -> do
(m, _) <- io $ readIORef funHandles
case Map.lookup fh m of
Nothing -> reply rep (RRBadMessage "invalid function handle" (show fh))
Just f -> do
case f arg of
E.VFun g -> do
gh <- io $ atomicModifyIORef' funHandles $ \(m', gh) ->
let m'' = Map.insert gh g m'
gh' = succ gh
in ((m'', gh'), gh)
-- TODO: bookkeeping to track the type of this value
reply rep (RRFunValue gh T.tZero)
val -> reply rep (RRValue val)
RCTypeOf txt -> do
expr <- replParseExpr (T.unpack txt)
(_expr, _def, sch) <- replCheckExpr expr
reply rep (RRType sch (show (pp sch)))
RCSetOpt key val -> do
setOptionCmd (T.unpack key ++ "=" ++ T.unpack val)
reply rep RROk
RCCheck expr -> do
reports <- qcCmd QCRandom (T.unpack expr)
reply rep (RRCheck reports)
RCExhaust expr -> do
reports <- qcCmd QCExhaust (T.unpack expr)
reply rep (RRExhaust reports)
RCProve expr -> do
result <- onlineProveSat False (T.unpack expr) Nothing
case result of
AllSatResult [cex] ->
reply rep (RRProve (Just (map (\(_,_,v) -> v) cex)))
ThmResult _ ->
reply rep (RRProve Nothing)
ProverError err ->
reply rep (RRProverError err)
_ ->
reply rep (RRProverError "unexpected prover result")
RCSat expr -> do
result <- onlineProveSat True (T.unpack expr) Nothing
case result of
AllSatResult sas ->
reply rep (RRSat (map (map (\(_,_,v) -> v)) sas))
ThmResult _ ->
reply rep (RRSat [])
ProverError err ->
reply rep (RRProverError err)
_ ->
reply rep (RRProverError "unexpected prover result")
RCLoadPrelude -> do
loadPrelude
reply rep RROk
RCLoadModule fp -> do
loadCmd fp
reply rep RROk
RCDecls -> do
(decls, _namingEnv, _nameDisp) <- getFocusedEnv
reply rep (RRDecls decls)
RCUnknownCmd cmd -> reply rep (RRUnknownCmd cmd)
RCExit -> do
reply rep RROk
io $ close rep
io $ putStrLn "[cryptol-worker] shutting down"
void $ forever loop
withCapturedOutput :: REPL a -> REPL (a, String)
withCapturedOutput m = do
old <- getPutStr
buf <- io $ newIORef ""
setPutStr $ \s -> modifyIORef' buf (++ s)
x <- m
s <- io $ readIORef buf
setPutStr old
return (x, s)
data Server = Server { serverPort :: Word16
, serverMaskSIGINT :: Bool }
deriving Show
main :: IO ()
main = execParser opts >>= mainWith
where
opts =
info (helper <*> serverOpts)
( fullDesc
<> progDesc "Run Cryptol as a server via ZeroMQ and JSON"
<> header "cryptol-server" )
serverOpts =
Server
<$> option auto
( long "port"
<> short 'p'
<> metavar "PORT"
<> value 5555
<> help "TCP port to bind" )
<*> switch
( long "mask-interrupts"
<> help "Suppress interrupt signals" )
mainWith Server {..} = do
when serverMaskSIGINT $ void $ installHandler sigINT Ignore Nothing
server serverPort

2
cryptol.cabal
View File

@ -14,7 +14,7 @@ Build-type: Simple
Cabal-version: >= 1.18
extra-source-files: bench/data/*.cry
data-files: *.cry Cryptol/*.cry *.z3
data-files: *.cry *.z3
data-dir: lib
source-repository head

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

@ -3155,7 +3155,6 @@ blocksize = 576
\begin{verbatim}
module Hash::SHA3 where
import Hash::SHA3
import Cryptol::Extras
hmac : {keySize, msgSize} (fin keySize, fin msgSize) => [keySize] -> [msgSize] -> [512]
hmac k m = sha3 (ko # sha3 (ki # m))

2
examples/MiniLock/prim/Base58.cry
View File

@ -4,8 +4,6 @@
*/
module Base58 where
import Cryptol::Extras
// Base 58 is a dependent format - the length of the encoded value depends on
// the value being encoded This does not play well with Cryptol, which expects
// a static type. Thus we must consume the worst-case number of bytes and

2
examples/MiniLock/prim/Base64.cry
View File

@ -4,8 +4,6 @@
*/
module Base64 where
import Cryptol::Extras
type Enc64 n = 4*(((3-(n%3))%3) + n)/3
base64enc : {n,m,padZ} (4*(padZ + n)/3 == m, fin n, fin m, padZ == (3-(n%3))%3, 2>=padZ)

2
examples/MiniLock/prim/Blake2s.cry
View File

@ -4,8 +4,6 @@
*/
module Blake2s where
import Cryptol::Extras
type Block = [16][32]
type State = [8][32]
type LocalState = [16][32]

134
lib/Cryptol.cry
View File

@ -604,3 +604,137 @@ primitive trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
*/
traceVal : {n, a} (fin n) => [n][8] -> a -> a
traceVal msg x = trace msg x x
/* Functions previously in Cryptol::Extras */
/**
* Logical negation
*/
not : {a} (Logic a) => a -> a
not a = ~ a
/**
* Conjunction of all bits in a sequence
*/
and : {n} (fin n) => [n]Bit -> Bit
and xs = ~zero == xs
/**
* Disjunction of all bits in a sequence
*/
or : {n} (fin n) => [n]Bit -> Bit
or xs = zero != xs
/**
* Conjunction after applying a predicate to all elements.
*/
all : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit
all f xs = and (map f xs)
/**
* Disjunction after applying a predicate to all elements.
*/
any : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit
any f xs = or (map f xs)
/**
* Map a function over an array.
*/
map : {a, b, n} (a -> b) -> [n]a -> [n]b
map f xs = [f x | x <- xs]
/**
* Functional left fold.
*
* foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3
*/
foldl : {a, b, n} (fin n) => (a -> b -> a) -> a -> [n]b -> a
foldl f acc xs = ys ! 0
where ys = [acc] # [f a x | a <- ys | x <- xs]
/**
* Functional right fold.
*
* foldr (-) 0 [1,2,3] = 0 - (1 - (2 - 3))
*/
foldr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> b
foldr f acc xs = ys ! 0
where ys = [acc] # [f x a | a <- ys | x <- reverse xs]
/**
* Compute the sum of the words in the array.
*/
sum : {a,n} (fin n, Zero a, Arith a) => [n]a -> a
sum xs = foldl (+) zero xs
/**
* Scan left is like a fold that emits the intermediate values.
*/
scanl : {b, a, n} (b -> a -> b) -> b -> [n]a -> [n+1]b
scanl f acc xs = ys
where
ys = [acc] # [f a x | a <- ys | x <- xs]
/**
* Scan right
*/
scanr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
scanr f acc xs = reverse ys
where
ys = [acc] # [f x a | a <- ys | x <- reverse xs]
/**
* Zero extension
*/
extend : {total,n} (fin total, fin n, total >= n) => [n]Bit -> [total]Bit
extend n = zero # n
/**
* Signed extension. `extendSigned 0bwxyz : [8] == 0bwwwwwxyz`.
*/
extendSigned : {total,n} (fin total, fin n, n >= 1, total >= n+1) => [n]Bit -> [total]Bit
extendSigned xs = repeat (xs @ 0) # xs
/**
* Repeat a value.
*/
repeat : {n, a} a -> [n]a
repeat x = [ x | _ <- zero : [n] ]
/**
* `elem x xs` Returns true if x is equal to a value in xs.
*/
elem : {n,a} (fin n, Cmp a) => a -> [n]a -> Bit
elem a xs = any (\x -> x == a) xs
/**
* Create a list of tuples from two lists.
*/
zip : {a,b,n} [n]a -> [n]b -> [n](a,b)
zip xs ys = [(x,y) | x <- xs | y <- ys]
/**
* Create a list by applying the function to each pair of elements in the input.
* lists
*/
zipWith : {a,b,c,n} (a -> b -> c) -> [n]a -> [n]b -> [n]c
zipWith f xs ys = [f x y | x <- xs | y <- ys]
/**
* Transform a function into uncurried form.
*/
uncurry : {a,b,c} (a -> b -> c) -> (a,b) -> c
uncurry f = \(a,b) -> f a b
/**
* Transform a function into curried form.
*/
curry : {a,b,c} ((a, b) -> c) -> a -> b -> c
curry f = \a b -> f (a,b)
/**
* Map a function iteratively over a seed value, producing an infinite
* list of successive function applications.
*/
iterate : { a } (a -> a) -> a -> [inf]a
iterate f x = [x] # [ f v | v <- iterate f x ]

142
lib/Cryptol/Extras.cry
View File

@ -1,142 +0,0 @@
/*
* Copyright (c) 2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*
* This module contains definitions that we wish to eventually promote
* into the Prelude, but which currently cause typechecking of the
* Prelude to take too long (see #299)
*/
module Cryptol::Extras where
/**
* Logical negation
*/
not : {a} (Logic a) => a -> a
not a = ~ a
/**
* Conjunction
*/
and : {n} (fin n) => [n]Bit -> Bit
and xs = ~zero == xs
/**
* Disjunction
*/
or : {n} (fin n) => [n]Bit -> Bit
or xs = zero != xs
/**
* Conjunction after applying a predicate to all elements.
*/
all : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit
all f xs = and (map f xs)
/**
* Disjunction after applying a predicate to all elements.
*/
any : {a,n} (fin n) => (a -> Bit) -> [n]a -> Bit
any f xs = or (map f xs)
/**
* Map a function over an array.
*/
map : {a, b, n} (a -> b) -> [n]a -> [n]b
map f xs = [f x | x <- xs]
/**
* Functional left fold.
*
* foldl (+) 0 [1,2,3] = ((0 + 1) + 2) + 3
*/
foldl : {a, b, n} (fin n) => (a -> b -> a) -> a -> [n]b -> a
foldl f acc xs = ys ! 0
where ys = [acc] # [f a x | a <- ys | x <- xs]
/**
* Functional right fold.
*
* foldr (-) 0 [1,2,3] = 0 - (1 - (2 - 3))
*/
foldr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> b
foldr f acc xs = ys ! 0
where ys = [acc] # [f x a | a <- ys | x <- reverse xs]
/**
* Compute the sum of the words in the array.
*/
sum : {a,n} (fin n, Zero a, Arith a) => [n]a -> a
sum xs = foldl (+) zero xs
/**
* Scan left is like a fold that emits the intermediate values.
*/
scanl : {b, a, n} (b -> a -> b) -> b -> [n]a -> [n+1]b
scanl f acc xs = ys
where
ys = [acc] # [f a x | a <- ys | x <- xs]
/**
* Scan right
*/
scanr : {a,b,n} (fin n) => (a -> b -> b) -> b -> [n]a -> [n+1]b
scanr f acc xs = reverse ys
where
ys = [acc] # [f x a | a <- ys | x <- reverse xs]
/**
* Zero extension
*/
extend : {total,n} (fin total, fin n, total >= n) => [n]Bit -> [total]Bit
extend n = zero # n
/**
* Signed extension. `extendSigned 0bwxyz : [8] == 0bwwwwwxyz`.
*/
extendSigned : {total,n} (fin total, fin n, n >= 1, total >= n+1) => [n]Bit -> [total]Bit
extendSigned xs = repeat (xs @ 0) # xs
/**
* Repeat a value.
*/
repeat : {n, a} a -> [n]a
repeat x = [ x | _ <- zero : [n] ]
/**
* `elem x xs` Returns true if x is equal to a value in xs.
*/
elem : {n,a} (fin n, Cmp a) => a -> [n]a -> Bit
elem a xs = any (\x -> x == a) xs
/**
* Create a list of tuples from two lists.
*/
zip : {a,b,n} [n]a -> [n]b -> [n](a,b)
zip xs ys = [(x,y) | x <- xs | y <- ys]
/**
* Create a list by applying the function to each pair of elements in the input.
* lists
*/
zipWith : {a,b,c,n} (a -> b -> c) -> [n]a -> [n]b -> [n]c
zipWith f xs ys = [f x y | x <- xs | y <- ys]
/**
* Transform a function into uncurried form.
*/
uncurry : {a,b,c} (a -> b -> c) -> (a,b) -> c
uncurry f = \(a,b) -> f a b
/**
* Transform a function into curried form.
*/
curry : {a,b,c} ((a, b) -> c) -> a -> b -> c
curry f = \a b -> f (a,b)
/**
* Map a function iteratively over a seed value, producing an infinite
* list of successive function applications.
*/
iterate : { a } (a -> a) -> a -> [inf]a
iterate f x = [x] # [ f v | v <- iterate f x ]

5
src/Cryptol/ModuleSystem/Base.hs
View File

@ -37,14 +37,14 @@ import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.PP as T
import qualified Cryptol.TypeCheck.Sanity as TcSanity
import Cryptol.Transform.AddModParams (addModParams)
import Cryptol.Utils.Ident (preludeName, preludeExtrasName, interactiveName
import Cryptol.Utils.Ident (preludeName, interactiveName
, modNameChunks, notParamInstModName
, isParamInstModName )
import Cryptol.Utils.PP (pretty)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Logger(logPutStrLn, logPrint)
import Cryptol.Prelude (writePreludeContents, writePreludeExtrasContents)
import Cryptol.Prelude (writePreludeContents)
import Cryptol.Transform.MonoValues (rewModule)
@ -232,7 +232,6 @@ findModule n = do
handleNotFound =
case n of
m | m == preludeName -> io writePreludeContents
m | m == preludeExtrasName -> io writePreludeExtrasContents
_ -> moduleNotFound n =<< getSearchPath
-- generate all possible search paths

12
src/Cryptol/Prelude.hs
View File

@ -15,7 +15,6 @@
module Cryptol.Prelude (
writePreludeContents,
writePreludeExtrasContents,
cryptolTcContents
) where
@ -37,17 +36,6 @@ writePreludeContents = do
hClose h
return path
preludeExtrasContents :: String
preludeExtrasContents = [there|lib/Cryptol/Extras.cry|]
writePreludeExtrasContents :: IO FilePath
writePreludeExtrasContents = do
tmpdir <- getTemporaryDirectory
(path, h) <- openTempFile tmpdir "CryptolExtras.cry"
hPutStr h preludeExtrasContents
hClose h
return path
cryptolTcContents :: String
cryptolTcContents = [there|lib/CryptolTC.z3|]

4
src/Cryptol/Utils/Ident.hs
View File

@ -16,7 +16,6 @@ module Cryptol.Utils.Ident
, modNameChunks
, packModName
, preludeName
, preludeExtrasName
, interactiveName
, noModuleName
, exprModName
@ -101,9 +100,6 @@ modInstPref = "`"
preludeName :: ModName
preludeName = packModName ["Cryptol"]
preludeExtrasName :: ModName
preludeExtrasName = packModName ["Cryptol", "Extras"]
interactiveName :: ModName
interactiveName = packModName ["<interactive>"]