cryptol 2.9.0 → 2.9.1

raw patch · 12 files changed

+155/−107 lines, 12 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGES.md +20/−5
• cryptol.cabal +2/−2
• cryptol/Main.hs +2/−14
• lib/Cryptol.cry +1/−1
• src/Cryptol/Eval.hs +36/−23
• src/Cryptol/Eval/Concrete.hs +42/−42
• src/Cryptol/Eval/Generic.hs +16/−15
• src/Cryptol/Eval/Value.hs +4/−4
• src/Cryptol/Parser/Unlit.hs +1/−0
• src/Cryptol/REPL/Command.hs +7/−1
• src/Cryptol/TypeCheck/Type.hs +12/−0
• src/Cryptol/Version.hs +12/−0

@@ -1,3 +1,17 @@+# 2.9.1++## Language changes++* The type of `generate` which is used for `a@i` sequence definitions,+   is generalized so that the index type can be any `Integral` type+   large enough to index the entire array being defined.++## Bug Fixes++* Closed issues #848, #850, #851, #859, and #861.++* Fixed Windows installer paths.+ # 2.9.0  ## Language changes@@ -18,14 +32,14 @@   The new `Field` class contains types representing mathematical   fields (or types that are approximately fields). It is currently   inhabited by the new `Rational` type, and the `Float`-  family of types.  It will  eventually also contain the+  family of types.  It will eventually also contain the   `Real` type. It has the operation `recip` for reciprocal   and `(/.)` for field division (not to be confused for `(/)`,   which is Euclidean integral division).    There is also a new `Round` class for types that can sensibly be   rounded to integers.  This class has the methods `floor`, `ceiling`,-  `trunc`, `roundToEven`  and `roundAway` for performing different+  `trunc`, `roundToEven` and `roundAway` for performing different   kinds of integer rounding.  `Rational` and `Float` inhabit `Round`.    The type of `(^^)` is modified to be@@ -33,7 +47,7 @@   that the semantics are iterated multiplication, which makes sense   in any ring. -  Finally, the `lg2`, `(/$)` and `(%$)` methods of Arith have+  Finally, the `lg2`, `(/$)` and `(%$)` methods of `Arith` have   had their types specialized so they operate only on bitvectors.  * Added an `Eq` class, and moved the equality operations@@ -119,8 +133,9 @@  ## Bug fixes -* Closed issues #346, #444, #614, #617, #636, #660, #662, #663, #664, #667, #670,-  #702, #711, #712, #716, #723, #725, #731+* Closed issues #346, #444, #614, #617, #636, #660, #662, #663, #664,+  #667, #670, #702, #711, #712, #716, #723, #725, #731, #835, #836,+  #839, #840, and #845  # 2.8.0 (September 4, 2019) 

@@ -1,5 +1,5 @@ Name:                cryptol-Version:             2.9.0+Version:             2.9.1 Synopsis:            Cryptol: The Language of Cryptography Description: Cryptol is a domain-specific language for specifying cryptographic algorithms. A Cryptol implementation of an algorithm resembles its mathematical specification more closely than an implementation in a general purpose language. For more, see <http://www.cryptol.net/>. License:             BSD3@@ -25,7 +25,7 @@ source-repository this   type:     git   location: https://github.com/GaloisInc/cryptol.git-  tag:      2.9.0+  tag:      2.9.1  flag static   default: False

@@ -23,12 +23,10 @@ import REPL.Logo  import Cryptol.Utils.PP-import Cryptol.Version (commitHash, commitBranch, commitDirty)-import Paths_cryptol (version)+import Cryptol.Version (displayVersion)  import Control.Monad (when) import Data.Maybe (isJust)-import Data.Version (showVersion) import GHC.IO.Encoding (setLocaleEncoding, utf8) import System.Console.GetOpt     (OptDescr(..),ArgOrder(..),ArgDescr(..),getOpt,usageInfo)@@ -169,16 +167,6 @@   (ps,[],[]) -> runOptParser defaultOptions (mconcat ps)   (_,_,errs) -> Left errs -displayVersion :: IO ()-displayVersion = do-    let ver = showVersion version-    putStrLn ("Cryptol " ++ ver)-    putStrLn ("Git commit " ++ commitHash)-    putStrLn ("    branch " ++ commitBranch ++ dirtyLab)-      where-      dirtyLab | commitDirty = " (non-committed files present during build)"-               | otherwise   = ""- displayHelp :: [String] -> IO () displayHelp errs = do   prog <- getProgName@@ -213,7 +201,7 @@      Right opts       | optHelp opts    -> displayHelp []-      | optVersion opts -> displayVersion+      | optVersion opts -> displayVersion putStrLn       | otherwise       -> do           (opts', mCleanup) <- setupCmdScript opts           status <- repl (optCryptolrc opts')

@@ -874,7 +874,7 @@  * Declarations of the form 'x @ i = e' are syntactic sugar for  * 'x = generate (\i -> e)'.  */-generate : {n, a} (fin n, n >= 1) => (Integer -> a) -> [n]a+generate : {n, a, ix} (fin n, n >= 1, Integral ix, Literal (n-1) ix) => (ix -> a) -> [n]a generate f = [ f i | i <- [0 .. n-1] ]  

@@ -397,34 +397,47 @@       k     -> panic "[Eval] etaDelay" ["invalid kind on type abstraction", show k]    go tp x | isReady sym x = x >>= \case-      VBit _     -> x-      VInteger _ -> x-      VWord _ _  -> x-      VSeq n xs-        | TVSeq _nt el <- tp-        -> return $ VSeq n $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i)+      VBit{}      -> x+      VInteger{}  -> x+      VWord{}     -> x+      VRational{} -> x+      VFloat{}    -> x+      VSeq n xs ->+        case tp of+          TVSeq _nt el -> return $ VSeq n $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i)+          _ -> evalPanic "type mismatch during eta-expansion" ["Expected sequence type, but got " ++ show tp] -      VStream xs-        | TVStream el <- tp-        -> return $ VStream $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i)+      VStream xs ->+        case tp of+          TVStream el -> return $ VStream $ IndexSeqMap $ \i -> go el (lookupSeqMap xs i)+          _ -> evalPanic "type mismatch during eta-expansion" ["Expected stream type, but got " ++ show tp] -      VTuple xs-        | TVTuple ts <- tp-        -> return $ VTuple (zipWith go ts xs)+      VTuple xs ->+        case tp of+          TVTuple ts | length ts == length xs -> return $ VTuple (zipWith go ts xs)+          _ -> evalPanic "type mismatch during eta-expansion" ["Expected tuple type with " ++ show (length xs)+                                   ++ " elements, but got " ++ show tp] -      VRecord fs-        | TVRec fts <- tp-        -> do let res = zipRecords (\_ v t -> go t v) fs fts-              case res of-                Left (Left f)  -> evalPanic "type mismatch during eta-expansion" ["missing field " ++ show f]-                Left (Right f) -> evalPanic "type mismatch during eta-expansion" ["unexpected field " ++ show f]-                Right fs' -> return (VRecord fs')+      VRecord fs ->+        case tp of+          TVRec fts ->+            do let res = zipRecords (\_ v t -> go t v) fs fts+               case res of+                 Left (Left f)  -> evalPanic "type mismatch during eta-expansion" ["missing field " ++ show f]+                 Left (Right f) -> evalPanic "type mismatch during eta-expansion" ["unexpected field " ++ show f]+                 Right fs' -> return (VRecord fs')+          _ -> evalPanic "type mismatch during eta-expansion" ["Expected record type, but got " ++ show tp] -      VFun f-        | TVFun _t1 t2 <- tp-        -> return $ VFun $ \a -> go t2 (f a)+      VFun f ->+        case tp of+          TVFun _t1 t2 -> return $ VFun $ \a -> go t2 (f a)+          _ -> evalPanic "type mismatch during eta-expansion" ["Expected function type but got " ++ show tp] -      _ -> evalPanic "type mismatch during eta-expansion" []+      VPoly{} ->+        evalPanic "type mismatch during eta-expansion" ["Encountered polymorphic value"]++      VNumPoly{} ->+        evalPanic "type mismatch during eta-expansion" ["Encountered numeric polymorphic value"]    go tp v =     case tp of

@@ -24,7 +24,7 @@   , toExpr   ) where -import Control.Monad (join,guard,zipWithM,mzero)+import Control.Monad (join, guard, zipWithM) import Data.Bits (Bits(..)) import Data.Ratio(numerator,denominator) import MonadLib( ChoiceT, findOne, lift )@@ -55,8 +55,6 @@  -- | Given an expected type, returns an expression that evaluates to -- this value, if we can determine it.------ XXX: View patterns would probably clean up this definition a lot. toExpr :: PrimMap -> AST.Type -> Value -> Eval (Maybe AST.Expr) toExpr prims t0 v0 = findOne (go t0 v0)   where@@ -65,45 +63,47 @@     go :: AST.Type -> Value -> ChoiceT Eval Expr-  go ty val = case (tNoUser ty, val) of-    (TRec tfs, VRecord vfs) -> do-      -- NB, vfs first argument to keep their display order-      res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs-      case res of-        Left _ -> mzero -- different fields-        Right efs -> pure (ERec efs)-    (TCon (TC (TCTuple tl)) ts, VTuple tvs) -> do-      guard (tl == (length tvs))-      ETuple `fmap` (zipWithM go ts =<< lift (sequence tvs))-    (TCon (TC TCBit) [], VBit True ) -> return (prim "True")-    (TCon (TC TCBit) [], VBit False) -> return (prim "False")-    (TCon (TC TCInteger) [], VInteger i) ->-      return $ ETApp (ETApp (prim "number") (tNum i)) ty-    (TCon (TC TCIntMod) [_n], VInteger i) ->-      return $ ETApp (ETApp (prim "number") (tNum i)) ty-    (TCon (TC TCRational) [], VRational (SRational n d)) ->-      do let n' = ETApp (ETApp (prim "number") (tNum n)) (TCon (TC TCInteger) [])-             d' = ETApp (ETApp (prim "number") (tNum d)) (TCon (TC TCInteger) [])-         return $ EApp (EApp (prim "ratio") n') d'-    (TCon (TC TCFloat) [eT,pT], VFloat i) ->-      pure (floatToExpr prims eT pT (bfValue i))--    (TCon (TC TCSeq) [a,b], VSeq 0 _) -> do-      guard (a == tZero)-      return $ EList [] b-    (TCon (TC TCSeq) [a,b], VSeq n svs) -> do-      guard (a == tNum n)-      ses <- mapM (go b) =<< lift (sequence (enumerateSeqMap n svs))-      return $ EList ses b-    (TCon (TC TCSeq) [a,(TCon (TC TCBit) [])], VWord _ wval) -> do-      BV w v <- lift (asWordVal Concrete =<< wval)-      guard (a == tNum w)-      return $ ETApp (ETApp (prim "number") (tNum v)) ty-    (_, VStream _) -> fail "cannot construct infinite expressions"-    (_, VFun    _) -> fail "cannot convert function values to expressions"-    (_, VPoly   _) -> fail "cannot convert polymorphic values to expressions"-    _ -> do doc <- lift (ppValue Concrete defaultPPOpts val)-            panic "Cryptol.Eval.Concrete.toExpr"+  go ty val =+    case val of+      VRecord vfs ->+        do tfs <- maybe mismatch pure (tIsRec ty)+           -- NB, vfs first argument to keep their display order+           res <- zipRecordsM (\_lbl v t -> go t =<< lift v) vfs tfs+           case res of+             Left _ -> mismatch -- different fields+             Right efs -> pure (ERec efs)+      VTuple tvs ->+        do ts <- maybe mismatch pure (tIsTuple ty)+           guard (length ts == length tvs)+           ETuple <$> (zipWithM go ts =<< lift (sequence tvs))+      VBit b ->+        pure (prim (if b then "True" else "False"))+      VInteger i ->+        -- This works uniformly for values of type Integer or Z n+        pure $ ETApp (ETApp (prim "number") (tNum i)) ty+      VRational (SRational n d) ->+        do let n' = ETApp (ETApp (prim "number") (tNum n)) tInteger+           let d' = ETApp (ETApp (prim "number") (tNum d)) tInteger+           pure $ EApp (EApp (prim "ratio") n') d'+      VFloat i ->+        do (eT, pT) <- maybe mismatch pure (tIsFloat ty)+           pure (floatToExpr prims eT pT (bfValue i))+      VSeq n svs ->+        do (_a, b) <- maybe mismatch pure (tIsSeq ty)+           ses <- traverse (go b) =<< lift (sequence (enumerateSeqMap n svs))+           pure $ EList ses b+      VWord _ wval ->+        do BV _ v <- lift (asWordVal Concrete =<< wval)+           pure $ ETApp (ETApp (prim "number") (tNum v)) ty+      VStream _  -> fail "cannot construct infinite expressions"+      VFun _     -> fail "cannot convert function values to expressions"+      VPoly _    -> fail "cannot convert polymorphic values to expressions"+      VNumPoly _ -> fail "cannot convert polymorphic values to expressions"+    where+      mismatch :: forall a. ChoiceT Eval a+      mismatch =+        do doc <- lift (ppValue Concrete defaultPPOpts val)+           panic "Cryptol.Eval.Concrete.toExpr"              ["type mismatch:"              , pretty ty              , render doc

@@ -1407,10 +1407,23 @@   Either (SInteger sym) (WordValue sym) {- ^ Index value -} ->   SEval sym () --- Can't index out of bounds for an infinite sequence-assertIndexInBounds _sym Inf _ =-  return ()+-- All nonnegative integers are in bounds for an infinite sequence+assertIndexInBounds sym Inf (Left idx) =+  do ppos <- bitComplement sym =<< intLessThan sym idx =<< integerLit sym 0+     assertSideCondition sym ppos (InvalidIndex (integerAsLit sym idx)) +-- If the index is an integer, test that it+-- is nonnegative and less than the concrete value of n.+assertIndexInBounds sym (Nat n) (Left idx) =+  do n' <- integerLit sym n+     ppos <- bitComplement sym =<< intLessThan sym idx =<< integerLit sym 0+     pn <- intLessThan sym idx n'+     p <- bitAnd sym ppos pn+     assertSideCondition sym p (InvalidIndex (integerAsLit sym idx))++-- Bitvectors can't index out of bounds for an infinite sequence+assertIndexInBounds _sym Inf (Right _) = return ()+ -- Can't index out of bounds for a sequence that is -- longer than the expressible index values assertIndexInBounds sym (Nat n) (Right idx)@@ -1418,21 +1431,9 @@   = return ()  -- If the index is concrete, test it directly-assertIndexInBounds sym (Nat n) (Left idx)-  | Just i <- integerAsLit sym idx-  = unless (i < n) (raiseError sym (InvalidIndex (Just i)))---- If the index is concrete, test it directly assertIndexInBounds sym (Nat n) (Right (WordVal idx))   | Just (_w,i) <- wordAsLit sym idx   = unless (i < n) (raiseError sym (InvalidIndex (Just i)))---- If the index is an integer, test that it--- is less than the concrete value of n.-assertIndexInBounds sym (Nat n) (Left idx) =-  do n' <- integerLit sym n-     p <- intLessThan sym idx n'-     assertSideCondition sym p (InvalidIndex Nothing)  -- If the index is a packed word, test that it -- is less than the concrete value of n, which

@@ -272,21 +272,21 @@ -- | Select an individual bit from a word value indexWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) indexWordValue sym (WordVal w) idx-   | idx < wordLen sym w = wordBit sym w idx+   | 0 <= idx && idx < wordLen sym w = wordBit sym w idx    | otherwise = invalidIndex sym idx indexWordValue sym (LargeBitsVal n xs) idx-   | idx < n   = fromVBit <$> lookupSeqMap xs idx+   | 0 <= idx && idx < n = fromVBit <$> lookupSeqMap xs idx    | otherwise = invalidIndex sym idx  -- | Produce a new 'WordValue' from the one given by updating the @i@th bit with the --   given bit value. updateWordValue :: Backend sym => sym -> WordValue sym -> Integer -> SEval sym (SBit sym) -> SEval sym (WordValue sym) updateWordValue sym (WordVal w) idx b -   | idx >= wordLen sym w = invalidIndex sym idx+   | idx < 0 || idx >= wordLen sym w = invalidIndex sym idx    | isReady sym b = WordVal <$> (wordUpdate sym w idx =<< b)  updateWordValue sym wv idx b-   | idx < wordValueSize sym wv =+   | 0 <= idx && idx < wordValueSize sym wv =         pure $ LargeBitsVal (wordValueSize sym wv) $ updateSeqMap (asBitsMap sym wv) idx (VBit <$> b)    | otherwise = invalidIndex sym idx 

@@ -78,6 +78,7 @@   where   comment current []    = mk Comment current   comment current (l : ls)+    | Just op <- isOpenFence l = mk Comment (l : current) ++ fenced op [] ls     | isBlank l         = blanks (l : current) ls     | otherwise         = comment (l : current) ls 

@@ -88,6 +88,7 @@   ) import qualified Cryptol.Symbolic.SBV as SBV import qualified Cryptol.Symbolic.What4 as W4+import Cryptol.Version (displayVersion)  import qualified Control.Exception as X import Control.Monad hiding (mapM, mapM)@@ -194,6 +195,9 @@   , CommandDescr [ ":b", ":browse" ] ["[ MODULE ]"] (ModNameArg browseCmd)     "Display environment for all loaded modules, or for a specific module."     ""+  , CommandDescr [ ":version"] [] (NoArg versionCmd)+    "Display the version of this Cryptol executable"+    ""   , CommandDescr [ ":?", ":help" ] ["[ TOPIC ]"] (HelpArg helpCmd)     "Display a brief description of a function, type, or command. (e.g. :help :help)"     (unlines@@ -1068,9 +1072,11 @@        M.InMem {} -> clearEditPath      setDynEnv mempty +versionCmd :: REPL ()+versionCmd = displayVersion rPutStrLn+ quitCmd :: REPL () quitCmd  = stop-  browseCmd :: String -> REPL () browseCmd input = do

@@ -393,6 +393,18 @@                  TCon (TC TCIntMod) [n] -> Just n                  _                      -> Nothing +tIsRational :: Type -> Bool+tIsRational ty =+  case tNoUser ty of+    TCon (TC TCRational) [] -> True+    _                       -> False++tIsFloat :: Type -> Maybe (Type, Type)+tIsFloat ty =+  case tNoUser ty of+    TCon (TC TCFloat) [e, p] -> Just (e, p)+    _                        -> Nothing+ tIsTuple :: Type -> Maybe [Type] tIsTuple ty = case tNoUser ty of                 TCon (TC (TCTuple _)) ts -> Just ts

@@ -14,10 +14,12 @@   , commitBranch   , commitDirty   , version+  , displayVersion   ) where  import Paths_cryptol import qualified GitRev+import Data.Version (showVersion)  commitHash :: String commitHash = GitRev.hash@@ -30,3 +32,13 @@  commitDirty :: Bool commitDirty = GitRev.dirty++displayVersion :: Monad m => (String -> m ()) -> m ()+displayVersion putLn = do+    let ver = showVersion version+    putLn ("Cryptol " ++ ver)+    putLn ("Git commit " ++ commitHash)+    putLn ("    branch " ++ commitBranch ++ dirtyLab)+      where+      dirtyLab | commitDirty = " (non-committed files present during build)"+               | otherwise   = ""