Add SMT Array primitives. (#732)

* Add SMT Array primitives.

* Move SMT Array primitives in Array.cry.

* Minor.

lib/Array.cry

@@ -0,0 +1,15 @@
+/*
+ * Copyright (c) 2020 Galois, Inc.
+ * Distributed under the terms of the BSD3 license (see LICENSE file)
+ */
+
+/** The type and operations of the theory of arrays. */
+
+module Array where
+
+primitive type Array : * -> * -> *
+
+primitive arrayConstant : {a, b} b -> (Array a b)
+primitive arrayLookup : {a, b} (Array a b) -> a -> b
+primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b)
+

src/Cryptol/Eval.hs

@@ -426,6 +426,7 @@ etaDelay sym msg env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
       TVBit -> v
       TVInteger -> v
       TVIntMod _ -> v
+      TVArray{} -> v
 
       TVSeq n TVBit ->
           do w <- sDelayFill sym (fromWordVal "during eta-expansion" =<< v) (etaWord sym n v)

src/Cryptol/Eval/Generic.hs

@@ -164,6 +164,9 @@ arithBinary sym opw opi opz = loop
     TVIntMod n ->
       VInteger <$> opz n (fromVInteger l) (fromVInteger r)
 
+    TVArray{} ->
+      evalPanic "arithBinary" ["Array not in class Arith"]
+
     TVSeq w a
       -- words and finite sequences
       | isTBit a -> do
@@ -235,6 +238,9 @@ arithUnary sym opw opi opz = loop
     TVIntMod n ->
       VInteger <$> opz n (fromVInteger v)
 
+    TVArray{} ->
+      evalPanic "arithUnary" ["Array not in class Arith"]
+
     TVSeq w a
       -- words and finite sequences
       | isTBit a -> do
@@ -292,6 +298,8 @@ arithNullary sym opw opi opz = loop
 
         TVIntMod n -> VInteger <$> opz n
 
+        TVArray{} -> evalPanic "arithNullary" ["Array not in class Arith"]
+
         TVSeq w a
           -- words and finite sequences
           | isTBit a -> pure $ VWord w $ (WordVal <$> opw w)
@@ -445,6 +453,8 @@ cmpValue sym fb fw fi fz = cmp
         TVBit         -> fb (fromVBit v1) (fromVBit v2) k
         TVInteger     -> fi (fromVInteger v1) (fromVInteger v2) k
         TVIntMod n    -> fz n (fromVInteger v1) (fromVInteger v2) k
+        TVArray{}     -> panic "Cryptol.Prims.Value.cmpValue"
+                               [ "Arrays are not comparable" ]
         TVSeq n t
           | isTBit t  -> do w1 <- fromVWord sym "cmpValue" v1
                             w2 <- fromVWord sym "cmpValue" v2
@@ -608,6 +618,8 @@ zeroV sym ty = case ty of
   TVIntMod _ ->
     VInteger <$> integerLit sym 0
 
+  TVArray{} -> evalPanic "zeroV" ["Array not in class Zero"]
+
   -- sequences
   TVSeq w ety
       | isTBit ety -> pure $ word sym w 0
@@ -1010,6 +1022,7 @@ logicBinary sym opb opw = loop
     TVBit -> VBit <$> (opb (fromVBit l) (fromVBit r))
     TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]
     TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"]
+    TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"]
     TVSeq w aty
          -- words
          | isTBit aty
@@ -1085,6 +1098,7 @@ logicUnary sym opb opw = loop
 
     TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"]
     TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"]
+    TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"]
 
     TVSeq w ety
          -- words
@@ -1420,6 +1434,7 @@ errorV sym ty msg = case ty of
   TVBit -> cryUserError sym msg
   TVInteger -> cryUserError sym msg
   TVIntMod _ -> cryUserError sym msg
+  TVArray{} -> cryUserError sym msg
 
   -- sequences
   TVSeq w ety

src/Cryptol/Eval/Reference.lhs

@@ -66,6 +66,7 @@ are as follows:
 |:----------------- |:-------------- |:--------------------------- |
 | `Bit`             | booleans       | `TVBit`                     |
 | `Integer`         | integers       | `TVInteger`                 |
+| `Array`           | arrays         | `TVArray`                   |
 | `[n]a`            | finite lists   | `TVSeq n a`                 |
 | `[inf]a`          | infinite lists | `TVStream a`                |
 | `(a, b, c)`       | tuples         | `TVTuple [a,b,c]`           |
@@ -171,6 +172,7 @@ cpo that represents any given schema.
 >         TVBit        -> VBit (fromVBit val)
 >         TVInteger    -> VInteger (fromVInteger val)
 >         TVIntMod _   -> VInteger (fromVInteger val)
+>         TVArray{}    -> evalPanic "copyByTValue" ["Unsupported Array type"]
 >         TVSeq w ety  -> VList (Nat w) (map (go ety) (copyList w (fromVList val)))
 >         TVStream ety -> VList Inf (map (go ety) (copyStream (fromVList val)))
 >         TVTuple etys -> VTuple (zipWith go etys (copyList (genericLength etys) (fromVTuple val)))
@@ -751,6 +753,7 @@ at the same positions.
 >     go TVBit          = VBit b
 >     go TVInteger      = VInteger (fmap (\c -> if c then -1 else 0) b)
 >     go (TVIntMod _)   = VInteger (fmap (const 0) b)
+>     go (TVArray{})    = evalPanic "logicNullary" ["Array not in class Logic"]
 >     go (TVSeq n ety)  = VList (Nat n) (genericReplicate n (go ety))
 >     go (TVStream ety) = VList Inf (repeat (go ety))
 >     go (TVTuple tys)  = VTuple (map go tys)
@@ -768,6 +771,7 @@ at the same positions.
 >         TVBit        -> VBit (fmap op (fromVBit val))
 >         TVInteger    -> evalPanic "logicUnary" ["Integer not in class Logic"]
 >         TVIntMod _   -> evalPanic "logicUnary" ["Z not in class Logic"]
+>         TVArray{}    -> evalPanic "logicUnary" ["Array not in class Logic"]
 >         TVSeq w ety  -> VList (Nat w) (map (go ety) (fromVList val))
 >         TVStream ety -> VList Inf (map (go ety) (fromVList val))
 >         TVTuple etys -> VTuple (zipWith go etys (fromVTuple val))
@@ -785,6 +789,7 @@ at the same positions.
 >         TVBit        -> VBit (liftA2 op (fromVBit l) (fromVBit r))
 >         TVInteger    -> evalPanic "logicBinary" ["Integer not in class Logic"]
 >         TVIntMod _   -> evalPanic "logicBinary" ["Z not in class Logic"]
+>         TVArray{}    -> evalPanic "logicBinary" ["Array not in class Logic"]
 >         TVSeq w ety  -> VList (Nat w) (zipWith (go ety) (fromVList l) (fromVList r))
 >         TVStream ety -> VList Inf (zipWith (go ety) (fromVList l) (fromVList r))
 >         TVTuple etys -> VTuple (zipWith3 go etys (fromVTuple l) (fromVTuple r))
@@ -819,6 +824,8 @@ up of non-empty finite bitvectors.
 >           VInteger i
 >         TVIntMod n ->
 >           VInteger (flip mod n <$> i)
+>         TVArray{} ->
+>           evalPanic "arithNullary" ["Array not in class Arith"]
 >         TVSeq w a
 >           | isTBit a  -> vWord w i
 >           | otherwise -> VList (Nat w) (genericReplicate w (go a))
@@ -852,6 +859,8 @@ up of non-empty finite bitvectors.
 >           case fromVInteger val of
 >             Left e -> Left e
 >             Right i -> flip mod n <$> op i
+>         TVArray{} ->
+>           evalPanic "arithUnary" ["Array not in class Arith"]
 >         TVSeq w a
 >           | isTBit a  -> vWord w (op =<< fromVWord val)
 >           | otherwise -> VList (Nat w) (map (go a) (fromVList val))
@@ -900,6 +909,8 @@ up of non-empty finite bitvectors.
 >               case fromVInteger r of
 >                 Left e -> Left e
 >                 Right j -> flip mod n <$> op i j
+>         TVArray{} ->
+>           evalPanic "arithBinary" ["Array not in class Arith"]
 >         TVSeq w a
 >           | isTBit a  -> vWord w $
 >                          case fromWord l of
@@ -968,6 +979,8 @@ bits to the *left* of that position are equal.
 >       compare <$> fromVInteger l <*> fromVInteger r
 >     TVIntMod _ ->
 >       compare <$> fromVInteger l <*> fromVInteger r
+>     TVArray{} ->
+>       evalPanic "lexCompare" ["invalid type"]
 >     TVSeq _w ety ->
 >       lexList (zipWith (lexCompare ety) (fromVList l) (fromVList r))
 >     TVStream _ ->
@@ -1011,6 +1024,8 @@ fields are compared in alphabetical order.
 >       evalPanic "lexSignedCompare" ["invalid type"]
 >     TVIntMod _ ->
 >       evalPanic "lexSignedCompare" ["invalid type"]
+>     TVArray{} ->
+>       evalPanic "lexSignedCompare" ["invalid type"]
 >     TVSeq _w ety
 >       | isTBit ety ->
 >         case fromSignedVWord l of

src/Cryptol/Eval/Type.hs

@@ -30,6 +30,7 @@ data TValue
   = TVBit                     -- ^ @ Bit @
   | TVInteger                 -- ^ @ Integer @
   | TVIntMod Integer          -- ^ @ Z n @
+  | TVArray TValue TValue     -- ^ @ Array a b @
   | TVSeq Integer TValue      -- ^ @ [n]a @
   | TVStream TValue           -- ^ @ [inf]t @
   | TVTuple [TValue]          -- ^ @ (a, b, c )@
@@ -45,6 +46,7 @@ tValTy tv =
     TVBit       -> tBit
     TVInteger   -> tInteger
     TVIntMod n  -> tIntMod (tNum n)
+    TVArray a b -> tArray (tValTy a) (tValTy b)
     TVSeq n t   -> tSeq (tNum n) (tValTy t)
     TVStream t  -> tSeq tInf (tValTy t)
     TVTuple ts  -> tTuple (map tValTy ts)
@@ -105,6 +107,7 @@ evalType env ty =
         (TCIntMod, [n]) -> case num n of
                              Inf   -> evalPanic "evalType" ["invalid type Z inf"]
                              Nat m -> Right $ TVIntMod m
+        (TCArray, [a, b]) -> Right $ TVArray (val a) (val b)
         (TCSeq, [n, t]) -> Right $ tvSeq (num n) (val t)
         (TCFun, [a, b]) -> Right $ TVFun (val a) (val b)
         (TCTuple _, _)  -> Right $ TVTuple (map val ts)

src/Cryptol/ModuleSystem/Base.hs

@@ -42,14 +42,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, interactiveName
+import Cryptol.Utils.Ident (preludeName, arrayName, interactiveName
                            , modNameChunks, notParamInstModName
                            , isParamInstModName )
 import Cryptol.Utils.PP (pretty)
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.Logger(logPutStrLn, logPrint)
 
-import Cryptol.Prelude (preludeContents)
+import Cryptol.Prelude (preludeContents, arrayContents)
 
 import Cryptol.Transform.MonoValues (rewModule)
 
@@ -259,6 +259,7 @@ findModule n = do
   handleNotFound =
     case n of
       m | m == preludeName -> pure (InMem "Cryptol" preludeContents)
+        | m == arrayName -> pure (InMem "Array" arrayContents)
       _ -> moduleNotFound n =<< getSearchPath
 
   -- generate all possible search paths

src/Cryptol/ModuleSystem/Name.hs

@@ -13,6 +13,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}
 -- for the instances of RunM and BaseM
 {-# LANGUAGE UndecidableInstances #-}
@@ -221,7 +222,10 @@ nameFixity = nFixity
 asPrim :: Name -> Maybe Ident
 asPrim Name { .. } =
   case nInfo of
-    Declared p _ | p == preludeName -> Just nIdent
+    Declared p _
+      | p == preludeName -> Just nIdent
+      | p == arrayName ->
+        Just $ mkIdent $ modNameToText p <> "::" <> identText nIdent
     _ -> Nothing
 
 toParamInstName :: Name -> Name

src/Cryptol/Prelude.hs

@@ -13,7 +13,11 @@
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE OverloadedStrings #-}
 
-module Cryptol.Prelude (preludeContents,cryptolTcContents) where
+module Cryptol.Prelude
+  ( preludeContents
+  , arrayContents
+  , cryptolTcContents
+  ) where
 
 
 import Data.ByteString(ByteString)
@@ -23,6 +27,9 @@ import Text.Heredoc (there)
 preludeContents :: ByteString
 preludeContents = B.pack [there|lib/Cryptol.cry|]
 
+arrayContents :: ByteString
+arrayContents = B.pack [there|lib/Array.cry|]
+
 cryptolTcContents :: String
 cryptolTcContents = [there|lib/CryptolTC.z3|]
 

src/Cryptol/Testing/Random.hs

@@ -348,6 +348,7 @@ typeSize ty =
                               TCon (TC (TCNum n)) _ -> Just n
                               _                     -> Nothing
         (TCIntMod, _)    -> Nothing
+        (TCArray, _)     -> Nothing
         (TCSeq, [sz,el]) -> case tNoUser sz of
                               TCon (TC (TCNum n)) _ -> (^ n) <$> typeSize el
                               _                     -> Nothing
@@ -381,6 +382,7 @@ typeValues ty =
             [ TCon (TC (TCNum n)) _ ] | 0 < n ->
               [ VInteger x | x <- [ 0 .. n - 1 ] ]
             _ -> []
+        TCArray     -> []
         TCSeq       ->
           case map tNoUser ts of
             [ TCon (TC (TCNum n)) _, TCon (TC TCBit) [] ] ->

src/Cryptol/TypeCheck/TCon.hs

@@ -42,6 +42,7 @@ builtInType nm =
   case M.nameInfo nm of
     M.Declared m _
       | m == preludeName -> Map.lookup (M.nameIdent nm) builtInTypes
+      | m == arrayName   -> Map.lookup (M.nameIdent nm) builtInArray
     _ -> Nothing
 
   where
@@ -81,6 +82,11 @@ builtInType nm =
     , "lengthFromThenTo" ~> TF TCLenFromThenTo
     ]
 
+  -- Built-in types from Array.cry
+  builtInArray = Map.fromList
+    [ "Array" ~> TC TCArray
+    ]
+
 
 
 
@@ -115,6 +121,7 @@ instance HasKind TC where
       TCBit     -> KType
       TCInteger -> KType
       TCIntMod  -> KNum :-> KType
+      TCArray   -> KType :-> KType :-> KType
       TCSeq     -> KNum :-> KType :-> KType
       TCFun     -> KType :-> KType :-> KType
       TCTuple n -> foldr (:->) KType (replicate n KType)
@@ -190,6 +197,7 @@ data TC     = TCNum Integer            -- ^ Numbers
             | TCBit                    -- ^ Bit
             | TCInteger                -- ^ Integer
             | TCIntMod                 -- ^ @Z _@
+            | TCArray                  -- ^ @Array _ _@
             | TCSeq                    -- ^ @[_] _@
             | TCFun                    -- ^ @_ -> _@
             | TCTuple Int              -- ^ @(_, _, _)@
@@ -286,6 +294,7 @@ instance PP TC where
       TCBit     -> text "Bit"
       TCInteger -> text "Integer"
       TCIntMod  -> text "Z"
+      TCArray   -> text "Array"
       TCSeq     -> text "[]"
       TCFun     -> text "(->)"
       TCTuple 0 -> text "()"

src/Cryptol/TypeCheck/Type.hs

@@ -489,6 +489,9 @@ tInteger  = TCon (TC TCInteger) []
 tIntMod :: Type -> Type
 tIntMod n = TCon (TC TCIntMod) [n]
 
+tArray :: Type -> Type -> Type
+tArray a b = TCon (TC TCArray) [a, b]
+
 tWord    :: Type -> Type
 tWord a   = tSeq a tBit
 

src/Cryptol/Utils/Ident.hs

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