GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-11 07:00:49 +03:00
Code Issues Projects Releases Wiki Activity

Start manually merging Brian's changes regarding type values and evaluation

Browse Source
This commit is contained in:
Robert Dockins 2016-06-09 13:30:51 -04:00
parent b95b734b74
commit d2789c0214
9 changed files with 249 additions and 237 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
src/Cryptol/Eval.hs
View File

@ -77,7 +77,7 @@ evalExpr env expr = case expr of
| otherwise -> {-# SCC "evalExpr->EList" #-}
VSeq len <$> finiteSeqMap vs
where
tyv = evalType env ty
tyv = evalValType (envTypes env) ty
vs = map (evalExpr env) es
len = genericLength es
@ -101,8 +101,8 @@ evalExpr env expr = case expr of
iteValue b (eval t) (eval f)
EComp n t h gs -> {-# SCC "evalExpr->EComp" #-} do
let len = evalType env n
let elty = evalType env t
let len = evalNumType (envTypes env) n
let elty = evalValType (envTypes env) t
evalComp env len elty h gs
EVar n -> {-# SCC "evalExpr->EVar" #-} do
@ -116,11 +116,15 @@ evalExpr env expr = case expr of
]
ETAbs tv b -> {-# SCC "evalExpr->ETAbs" #-}
return $ VPoly $ \ty -> evalExpr (bindType (tpVar tv) ty env) b
case tpKind tv of
KType -> return $ VPoly $ \ty -> evalExpr (bindType (tpVar tv) (Right ty) env) b
KNum -> return $ VNumPoly $ \n -> evalExpr (bindType (tpVar tv) (Left n) env) b
k -> panic "[Eval] evalExpr" ["invalid kind on type abstraction", show k]
ETApp e ty -> {-# SCC "evalExpr->ETApp" #-} do
eval e >>= \case
VPoly f -> f $! (evalType env ty)
VPoly f -> f $! (evalValType (envTypes env) ty)
VNumPoly f -> f $! (evalNumType (envTypes env) ty)
val -> do vdoc <- ppV val
panic "[Eval] evalExpr"
["expected a polymorphic value"
@ -222,10 +226,14 @@ etaDelay :: BitWord b w
-> Eval (GenValue b w)
etaDelay msg env0 Forall{ sVars = vs, sType = tp0 } = goTpVars env0 vs
where
goTpVars env [] x = go (evalType env tp0) x
goTpVars env [] x = go (evalValType (envTypes env) tp0) x
goTpVars env (v:vs) x =
return $ VPoly $ \t ->
goTpVars (bindType (tpVar v) t env) vs ( ($t) . fromVPoly =<< x )
case tpKind v of
KType -> return $ VPoly $ \t ->
goTpVars (bindType (tpVar v) (Right t) env) vs ( ($t) . fromVPoly =<< x )
KNum -> return $ VNumPoly $ \n ->
goTpVars (bindType (tpVar v) (Left n) env) vs ( ($n) . fromVNumPoly =<< x )
k -> panic "[Eval] etaDelay" ["invalid kind on type abstraction", show k]
go tp (Ready x) =
case x of
@ -260,7 +268,7 @@ etaDelay msg env0 Forall{ sVars = vs, sType = tp0 } = goTpVars env0 vs
= x
| Just (n, el) <- isTSeq tp
, Nat n' <- numTValue n
, Nat n' <- n
, isTBit el
-- TODO! I think we need the alternate blackhole strategy here, where
-- entering the blackhole eta-exapnds to a list of bits
@ -269,7 +277,7 @@ etaDelay msg env0 Forall{ sVars = vs, sType = tp0 } = goTpVars env0 vs
| Just (n, el) <- isTSeq tp
= do x' <- delay (Just msg) (fromSeq "during eta-expansion" =<< x)
case numTValue n of
case n of
Inf -> return $ VStream $ SeqMap $ \i ->
go el (flip lookupSeqMap i =<< x')
Nat n' -> return $ VSeq n' $ SeqMap $ \i -> do
@ -374,7 +382,7 @@ data ListEnv b w = ListEnv
-- ^ Bindings whose values vary by position
, leStatic :: !(Map.Map Name (Eval (GenValue b w)))
-- ^ Bindings whose values are constant
, leTypes :: !(Map.Map TVar TValue)
, leTypes :: !TypeEnv
}
instance Monoid (ListEnv b w) where
@ -419,7 +427,7 @@ bindVarList n vs lenv = lenv { leVars = Map.insert n vs (leVars lenv) }
-- | Evaluate a comprehension.
evalComp :: EvalPrims b w
=> GenEvalEnv b w
-> TValue
-> Nat'
-> TValue
-> Expr
-> [[Match]]
@ -446,7 +454,7 @@ evalMatch lenv m = case m of
-- many envs
From n l ty expr ->
case numTValue len of
case len of
Nat nLen -> do
vss <- memoMap $ SeqMap $ \i -> evalExpr (evalListEnv lenv i) expr
let stutter xs = \i -> xs (i `div` nLen)
@ -472,8 +480,7 @@ evalMatch lenv m = case m of
return $ bindVarList n vs lenv'
where
tyenv = emptyEnv{ envTypes = leTypes lenv }
len = evalType tyenv l
len = evalNumType (leTypes lenv) l
-- XXX we don't currently evaluate these as though they could be recursive, as
-- they are typechecked that way; the read environment to evalExpr is the same

11
src/Cryptol/Eval/Env.hs
View File

@ -17,8 +17,10 @@ import Cryptol.Eval.Type
import Cryptol.Eval.Value
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Solver.InfNat
import Cryptol.Utils.PP
import qualified Data.Map.Strict as Map
import GHC.Generics (Generic)
@ -32,7 +34,7 @@ import Prelude.Compat
data GenEvalEnv b w = EvalEnv
{ envVars :: !(Map.Map Name (Eval (GenValue b w)))
, envTypes :: !(Map.Map TVar TValue)
, envTypes :: !TypeEnv
} deriving (Generic)
instance (NFData b, NFData w) => NFData (GenEvalEnv b w)
@ -84,14 +86,11 @@ lookupVar n env = Map.lookup n (envVars env)
-- | Bind a type variable of kind *.
{-# INLINE bindType #-}
bindType :: TVar -> TValue -> GenEvalEnv b w -> GenEvalEnv b w
bindType :: TVar -> Either Nat' TValue -> GenEvalEnv b w -> GenEvalEnv b w
bindType p ty env = env { envTypes = Map.insert p ty (envTypes env) }
-- | Lookup a type variable.
{-# INLINE lookupType #-}
lookupType :: TVar -> GenEvalEnv b w -> Maybe TValue
lookupType :: TVar -> GenEvalEnv b w -> Maybe (Either Nat' TValue)
lookupType p env = Map.lookup p (envTypes env)
{-# INLINE evalType #-}
evalType :: GenEvalEnv b w -> Type -> TValue
evalType env = evalType' (envTypes env)

164
src/Cryptol/Eval/Type.hs
View File

@ -7,6 +7,7 @@
-- Portability : portable
{-# LANGUAGE Safe, PatternGuards #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.Eval.Type where
@ -22,110 +23,114 @@ import GHC.Generics (Generic)
import Control.DeepSeq
import Control.DeepSeq.Generics
-- | An evaluated type.
-- | An evaluated type of kind *.
-- These types do not contain type variables, type synonyms, or type functions.
newtype TValue = TValue { tValTy :: Type } deriving (Generic)
data TValue
= TVBit
| TVSeq Integer TValue
| TVStream TValue -- ^ [inf]t
| TVTuple [TValue]
| TVRec [(Ident, TValue)]
| TVFun TValue TValue
deriving (Generic, NFData)
instance NFData TValue where rnf = genericRnf
tValTy :: TValue -> Type
tValTy tv =
case tv of
TVBit -> tBit
TVSeq n t -> tSeq (tNum n) (tValTy t)
TVStream t -> tSeq tInf (tValTy t)
TVTuple ts -> tTuple (map tValTy ts)
TVRec fs -> tRec [ (f, tValTy t) | (f, t) <- fs ]
TVFun t1 t2 -> tFun (tValTy t1) (tValTy t2)
instance Show TValue where
showsPrec p (TValue v) = showsPrec p v
showsPrec p v = showsPrec p (tValTy v)
{-
-- TODO? use these instead?
-- Type Values -----------------------------------------------------------------
-- | An easy-to-use alternative representation for type `TValue`.
data TypeVal
= TVBit
| TVSeq Int TypeVal
| TVStream TypeVal
| TVTuple [TypeVal]
| TVRecord [(Ident, TypeVal)]
| TVFun TypeVal TypeVal
toTypeVal :: TValue -> TypeVal
toTypeVal ty
| isTBit ty = TVBit
| Just (n, ety) <- isTSeq ty = case numTValue n of
Nat w -> TVSeq (fromInteger w) (toTypeVal ety)
Inf -> TVStream (toTypeVal ety)
| Just (aty, bty) <- isTFun ty = TVFun (toTypeVal aty) (toTypeVal bty)
| Just (_, tys) <- isTTuple ty = TVTuple (map toTypeVal tys)
| Just fields <- isTRec ty = TVRecord [ (n, toTypeVal aty) | (n, aty) <- fields ]
| otherwise = panic "Cryptol.Symbolic.Prims.toTypeVal" [ "bad TValue" ]
-}
-- Utilities -------------------------------------------------------------------
isTBit :: TValue -> Bool
isTBit (TValue ty) = case ty of
TCon (TC TCBit) [] -> True
_ -> False
isTBit TVBit = True
isTBit _ = False
isTSeq :: TValue -> Maybe (TValue, TValue)
isTSeq (TValue (TCon (TC TCSeq) [t1,t2])) = Just (TValue t1, TValue t2)
isTSeq :: TValue -> Maybe (Nat', TValue)
isTSeq (TVSeq n t) = Just (Nat n, t)
isTSeq (TVStream t) = Just (Inf, t)
isTSeq _ = Nothing
isTFun :: TValue -> Maybe (TValue, TValue)
isTFun (TValue (TCon (TC TCFun) [t1,t2])) = Just (TValue t1, TValue t2)
isTFun (TVFun t1 t2) = Just (t1, t2)
isTFun _ = Nothing
isTTuple :: TValue -> Maybe (Int,[TValue])
isTTuple (TValue (TCon (TC (TCTuple n)) ts)) = Just (n, map TValue ts)
isTTuple (TVTuple ts) = Just (length ts, ts)
isTTuple _ = Nothing
isTRec :: TValue -> Maybe [(Ident, TValue)]
isTRec (TValue (TRec fs)) = Just [ (x, TValue t) | (x,t) <- fs ]
isTRec (TVRec fs) = Just fs
isTRec _ = Nothing
tvSeq :: TValue -> TValue -> TValue
tvSeq (TValue x) (TValue y) = TValue (tSeq x y)
tvSeq :: Nat' -> TValue -> TValue
tvSeq (Nat n) t = TVSeq n t
tvSeq Inf t = TVStream t
numTValue :: TValue -> Nat'
numTValue (TValue ty) =
case ty of
TCon (TC (TCNum x)) _ -> Nat x
TCon (TC TCInf) _ -> Inf
_ -> panic "Cryptol.Eval.Value.numTValue" [ "Not a numeric type:", show ty ]
toNumTValue :: Nat' -> TValue
toNumTValue (Nat n) = TValue (TCon (TC (TCNum n)) [])
toNumTValue Inf = TValue (TCon (TC TCInf) [])
finTValue :: TValue -> Integer
finTValue tval =
case numTValue tval of
finNat' :: Nat' -> Integer
finNat' n' =
case n' of
Nat x -> x
Inf -> panic "Cryptol.Eval.Value.finTValue" [ "Unexpected `inf`" ]
Inf -> panic "Cryptol.Eval.Value.finNat'" [ "Unexpected `inf`" ]
-- Type Evaluation -------------------------------------------------------------
-- | Evaluation for types.
evalType' :: Map.Map TVar TValue -> Type -> TValue
evalType' env = TValue . go
type TypeEnv = Map.Map TVar (Either Nat' TValue)
-- | Evaluation for types (kind * or #).
evalType :: TypeEnv -> Type -> Either Nat' TValue
evalType env ty =
case ty of
TVar tv ->
case Map.lookup tv env of
Just v -> v
Nothing -> evalPanic "evalType" ["type variable not bound", show tv]
TUser _ _ ty' -> evalType env ty'
TRec fields -> Right $ TVRec [ (f, val t) | (f, t) <- fields ]
TCon (TC c) ts ->
case (c, ts) of
(TCBit, []) -> Right $ TVBit
(TCSeq, [n, t]) -> Right $ tvSeq (num n) (val t)
(TCFun, [a, b]) -> Right $ TVFun (val a) (val b)
(TCTuple _, _) -> Right $ TVTuple (map val ts)
(TCNum n, []) -> Left $ Nat n
(TCInf, []) -> Left $ Inf
-- FIXME: What about TCNewtype?
_ -> evalPanic "evalType" ["not a value type", show ty]
TCon (TF f) ts -> Left $ evalTF f (map num ts)
TCon (PC p) _ -> evalPanic "evalType" ["invalid predicate symbol", show p]
where
go ty =
case ty of
TVar tv ->
case Map.lookup tv env of
Just (TValue v) -> v
Nothing -> evalPanic "evalType" ["type variable not bound", show tv]
val = evalValType env
num = evalNumType env
TCon (TF f) ts -> tValTy $ evalTF f $ map (evalType' env) ts
TCon tc ts -> TCon tc (map go ts)
TUser _ _ ty' -> go ty'
TRec fields -> TRec [ (f,go t) | (f,t) <- fields ]
-- | Evaluation for value types (kind *).
evalValType :: TypeEnv -> Type -> TValue
evalValType env ty =
case evalType env ty of
Left _ -> evalPanic "evalValType" ["expected value type, found numeric type"]
Right t -> t
-- | Reduce type functions, rising an exception for undefined values.
evalTF :: TFun -> [TValue] -> TValue
evalTF tf vs = TValue $ cvt $ evalTF' tf $ map numTValue vs
evalNumType :: TypeEnv -> Type -> Nat'
evalNumType env ty =
case evalType env ty of
Left n -> n
Right _ -> evalPanic "evalValType" ["expected numeric type, found value type"]
-- | Reduce type functions, rising an exception for undefined values.
evalTF' :: TFun -> [Nat'] -> Nat'
evalTF' f vs
-- | Reduce type functions, raising an exception for undefined values.
evalTF :: TFun -> [Nat'] -> Nat'
evalTF f vs
| TCAdd <- f, [x,y] <- vs = nAdd x y
| TCSub <- f, [x,y] <- vs = mb $ nSub x y
| TCMul <- f, [x,y] <- vs = nMul x y
@ -141,12 +146,11 @@ evalTF' f vs
["Unexpected type function:", show ty]
where mb = fromMaybe (typeCannotBeDemoted ty)
ty = TCon (TF f) (map cvt vs)
ty = TCon (TF f) (map tNat' vs)
cvt :: Nat' -> Type
cvt (Nat n) = tNum n
cvt Inf = tInf
--cvt :: Nat' -> Type
--cvt (Nat n) = tNum n
--cvt Inf = tInf

19
src/Cryptol/Eval/Value.hs
View File

@ -177,6 +177,7 @@ data GenValue b w
| VStream !(SeqMap b w) -- @ [inf]a @
| VFun (Eval (GenValue b w) -> Eval (GenValue b w)) -- functions
| VPoly (TValue -> Eval (GenValue b w)) -- polymorphic values (kind *)
| VNumPoly (Nat' -> Eval (GenValue b w)) -- polymorphic values (kind #)
deriving (Generic)
@ -427,6 +428,10 @@ wlam f = VFun (\x -> x >>= fromVWord "wlam" >>= f)
tlam :: (TValue -> GenValue b w) -> GenValue b w
tlam f = VPoly (return . f)
-- | A type lambda that expects a @Type@ of kind #.
nlam :: (Nat' -> GenValue b w) -> GenValue b w
nlam f = VNumPoly (return . f)
-- | Generate a stream.
toStream :: [GenValue b w] -> Eval (GenValue b w)
toStream vs =
@ -445,16 +450,16 @@ boolToWord bs = VWord (genericLength bs) $ ready $ WordVal $ packWord bs
-- | Construct either a finite sequence, or a stream. In the finite case,
-- record whether or not the elements were bits, to aid pretty-printing.
toSeq :: BitWord b w
=> TValue -> TValue -> [GenValue b w] -> Eval (GenValue b w)
toSeq len elty vals = case numTValue len of
=> Nat' -> TValue -> [GenValue b w] -> Eval (GenValue b w)
toSeq len elty vals = case len of
Nat n -> toFinSeq n elty vals
Inf -> toStream vals
-- | Construct either a finite sequence, or a stream. In the finite case,
-- record whether or not the elements were bits, to aid pretty-printing.
mkSeq :: TValue -> TValue -> SeqMap b w -> GenValue b w
mkSeq len elty vals = case numTValue len of
mkSeq :: Nat' -> TValue -> SeqMap b w -> GenValue b w
mkSeq len elty vals = case len of
Nat n
| isTBit elty -> VWord n $ return $ BitsVal $ Seq.fromFunction (fromInteger n) $ \i ->
fromVBit <$> lookupSeqMap vals (toInteger i)
@ -526,6 +531,12 @@ fromVPoly val = case val of
VPoly f -> f
_ -> evalPanic "fromVPoly" ["not a polymorphic value"]
-- | Extract a polymorphic function from a value.
fromVNumPoly :: GenValue b w -> (Nat' -> Eval (GenValue b w))
fromVNumPoly val = case val of
VNumPoly f -> f
_ -> evalPanic "fromVNumPoly" ["not a polymorphic value"]
-- | Extract a tuple from a value.
fromVTuple :: GenValue b w -> [Eval (GenValue b w)]
fromVTuple val = case val of

171
src/Cryptol/Prims/Eval.hs
View File

@ -113,8 +113,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
ecDemoteV)
, ("#" , {-# SCC "Prelude::(#)" #-}
tlam $ \ front ->
tlam $ \ back ->
nlam $ \ front ->
nlam $ \ back ->
tlam $ \ elty ->
lam $ \ l -> return $
lam $ \ r -> join (ccatV front back elty <$> l <*> r))
@ -132,8 +132,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
tlam zeroV)
, ("join" , {-# SCC "Prelude::join" #-}
tlam $ \ parts ->
tlam $ \ each ->
nlam $ \ parts ->
nlam $ \ each ->
tlam $ \ a ->
lam $ \ x ->
joinV parts each a =<< x)
@ -142,8 +142,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
ecSplitV)
, ("splitAt" , {-# SCC "Prelude::splitAt" #-}
tlam $ \ front ->
tlam $ \ back ->
nlam $ \ front ->
nlam $ \ back ->
tlam $ \ a ->
lam $ \ x ->
splitAtV front back a =<< x)
@ -161,17 +161,17 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
, ("error" , {-# SCC "Prelude::error" #-}
tlam $ \a ->
tlam $ \_ ->
nlam $ \_ ->
lam $ \s -> errorV a =<< (fromStr =<< s))
, ("reverse" , {-# SCC "Prelude::reverse" #-}
tlam $ \a ->
nlam $ \a ->
tlam $ \b ->
lam $ \xs -> reverseV =<< xs)
, ("transpose" , {-# SCC "Prelude::transpose" #-}
tlam $ \a ->
tlam $ \b ->
nlam $ \a ->
nlam $ \b ->
tlam $ \c ->
lam $ \xs -> transposeV a b c =<< xs)
@ -179,21 +179,21 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
let mul !res !_ !_ 0 = res
mul res bs as n = mul (if even as then res else xor res bs)
(bs `shiftL` 1) (as `shiftR` 1) (n-1)
in tlam $ \(finTValue -> a) ->
tlam $ \(finTValue -> b) ->
in nlam $ \(finNat' -> a) ->
nlam $ \(finNat' -> b) ->
wlam $ \(bvVal -> x) -> return $
wlam $ \(bvVal -> y) -> return $ word (max 1 (a + b) - 1) (mul 0 x y b))
, ("pdiv" , {-# SCC "Prelude::pdiv" #-}
tlam $ \(fromInteger . finTValue -> a) ->
tlam $ \(fromInteger . finTValue -> b) ->
nlam $ \(fromInteger . finNat' -> a) ->
nlam $ \(fromInteger . finNat' -> b) ->
wlam $ \(bvVal -> x) -> return $
wlam $ \(bvVal -> y) -> return $ word (toInteger a)
(fst (divModPoly x a y b)))
, ("pmod" , {-# SCC "Prelude::pmod" #-}
tlam $ \(fromInteger . finTValue -> a) ->
tlam $ \(fromInteger . finTValue -> b) ->
nlam $ \(fromInteger . finNat' -> a) ->
nlam $ \(fromInteger . finNat' -> b) ->
wlam $ \(bvVal -> x) -> return $
wlam $ \(bvVal -> y) -> return $ word (toInteger b)
(snd (divModPoly x a y (b+1))))
@ -201,7 +201,7 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
tlam $ \a ->
wlam $ \(bvVal -> x) -> return $ randomV a x)
, ("trace" , {-# SCC "Prelude::trace" #-}
tlam $ \_n ->
nlam $ \_n ->
tlam $ \_a ->
tlam $ \_b ->
lam $ \s -> return $
@ -221,9 +221,9 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
-- | Make a numeric constant.
ecDemoteV :: BitWord b w => GenValue b w
ecDemoteV = tlam $ \valT ->
tlam $ \bitT ->
case (numTValue valT, numTValue bitT) of
ecDemoteV = nlam $ \valT ->
nlam $ \bitT ->
case (valT, bitT) of
(Nat v, Nat bs) -> word bs v
_ -> evalPanic "Cryptol.Eval.Prim.evalConst"
["Unexpected Inf in constant."
@ -337,7 +337,7 @@ arithBinary op = loop
-> Eval (GenValue b w)
loop ty l r
| Just (len,a) <- isTSeq ty = case numTValue len of
| Just (len,a) <- isTSeq ty = case len of
-- words and finite sequences
Nat w | isTBit a -> do
@ -392,7 +392,7 @@ arithUnary op = loop
loop :: TValue -> GenValue b w -> Eval (GenValue b w)
loop ty x
| Just (len,a) <- isTSeq ty = case numTValue len of
| Just (len,a) <- isTSeq ty = case len of
-- words and finite sequences
Nat w | isTBit a -> do
@ -444,7 +444,7 @@ lexCompare nm ty l r
| Just (_,b) <- isTSeq ty, isTBit b = do
compare <$> (fromWord "compareLeft" l) <*> (fromWord "compareRight" r)
| Just (len,e) <- isTSeq ty = case numTValue len of
| Just (len,e) <- isTSeq ty = case len of
Nat w -> join (zipLexCompare nm (repeat e) <$>
(enumerateSeqMap w <$> fromSeq "lexCompare left" l) <*>
(enumerateSeqMap w <$> fromSeq "lexCompare right" r))
@ -526,7 +526,7 @@ zeroV ty
-- sequences
| Just (n,ety) <- isTSeq ty =
case numTValue n of
case n of
Nat w | isTBit ety -> word w 0
| otherwise -> mkSeq n ety (SeqMap $ \_ -> ready $ zeroV ety)
Inf -> mkSeq n ety (SeqMap $ \_ -> ready $ zeroV ety)
@ -575,28 +575,28 @@ joinWords nParts nEach xs =
joinSeq :: BitWord b w
=> TValue
-> TValue
=> Nat'
-> Nat'
-> TValue
-> SeqMap b w
-> Eval (GenValue b w)
joinSeq parts each a xs
| Nat nEach <- numTValue each
| Nat nEach <- each
= return $ mkSeq $ (SeqMap $ \i -> do
let (q,r) = divMod i nEach
ys <- fromSeq "join seq" =<< lookupSeqMap xs q
lookupSeqMap ys r)
where
len = numTValue parts `nMul` numTValue each
len = parts `nMul` each
mkSeq = case len of
Inf -> VStream
Nat n -> VSeq n
-- | Join a sequence of sequences into a single sequence.
joinV :: BitWord b w
=> TValue
-> TValue
=> Nat'
-> Nat'
-> TValue
-> (GenValue b w)
-> Eval (GenValue b w)
@ -604,8 +604,8 @@ joinV parts each a val
-- Try to join a sequence of words, if we can determine that
-- each element is actually a word. Fall back on sequence
-- join otherwise.
| Nat nParts <- numTValue parts
, Nat nEach <- numTValue each
| Nat nParts <- parts
, Nat nEach <- each
, isTBit a
= do xs <- fromSeq "joinV" val
joinWords nParts nEach xs
@ -627,13 +627,13 @@ splitWordVal leftWidth rightWidth (BitsVal bs) =
in (BitsVal lbs, BitsVal rbs)
splitAtV :: BitWord b w
=> TValue
-> TValue
=> Nat'
-> Nat'
-> TValue
-> (GenValue b w)
-> Eval (GenValue b w)
splitAtV front back a val =
case numTValue back of
case back of
Nat rightWidth | aBit, VWord _ w <- val -> do
ws <- delay Nothing (splitWordVal leftWidth rightWidth <$> w)
@ -663,7 +663,7 @@ splitAtV front back a val =
where
aBit = isTBit a
leftWidth = case numTValue front of
leftWidth = case front of
Nat n -> n
_ -> evalPanic "splitAtV" ["invalid `front` len"]
@ -684,11 +684,11 @@ extractWordVal len start (BitsVal bs) =
ecSplitV :: BitWord b w
=> GenValue b w
ecSplitV =
tlam $ \ parts ->
tlam $ \ each ->
nlam $ \ parts ->
nlam $ \ each ->
tlam $ \ a ->
lam $ \ val ->
case (numTValue parts, numTValue each) of
case (parts, each) of
(Nat p, Nat e) | isTBit a -> do
VWord _ val' <- val
return $ VSeq p $ SeqMap $ \i -> do
@ -723,13 +723,13 @@ reverseV _ =
transposeV :: BitWord b w
=> TValue
-> TValue
=> Nat'
-> Nat'
-> TValue
-> GenValue b w
-> Eval (GenValue b w)
transposeV a b c xs
| isTBit c, Nat na <- numTValue a =
| isTBit c, Nat na <- a =
return $ bseq $ SeqMap $ \bi ->
return $ VWord na $ return $ BitsVal $
Seq.fromFunction (fromInteger na) $ \ai -> do
@ -747,11 +747,11 @@ transposeV a b c xs
where
bseq =
case numTValue b of
case b of
Nat nb -> VSeq nb
Inf -> VStream
aseq =
case numTValue a of
case a of
Nat na -> VSeq na
Inf -> VStream
@ -759,8 +759,8 @@ transposeV a b c xs
ccatV :: (Show b, Show w, BitWord b w)
=> TValue
-> TValue
=> Nat'
-> Nat'
-> TValue
-> (GenValue b w)
-> (GenValue b w)
@ -779,7 +779,7 @@ ccatV front back elty (VWord m l) (VStream r) =
ccatV front back elty l r = do
l'' <- delay Nothing (fromSeq "ccatV left" l)
r'' <- delay Nothing (fromSeq "ccatV right" r)
let Nat n = numTValue front
let Nat n = front
mkSeq (evalTF TCAdd [front,back]) elty <$> return (SeqMap $ \i ->
if i < n then do
ls <- l''
@ -821,7 +821,7 @@ logicBinary opb opw = loop
| isTBit ty = return $ VBit (opb (fromVBit l) (fromVBit r))
| Just (len,aty) <- isTSeq ty =
case numTValue len of
case len of
-- words or finite sequences
Nat w | isTBit aty, VWord _ lw <- l, VWord _ rw <- r
@ -885,7 +885,7 @@ logicUnary opb opw = loop
| Just (len,ety) <- isTSeq ty =
case numTValue len of
case len of
-- words or finite sequences
Nat w | isTBit ety, VWord _ wv <- val
@ -918,11 +918,11 @@ logicShift :: (Integer -> Integer -> Integer -> Integer)
-- ^ The function may assume its arguments are masked.
-- It is responsible for masking its result if needed.
-> (Integer -> Seq.Seq (Eval Bool) -> Integer -> Seq.Seq (Eval Bool))
-> (TValue -> TValue -> SeqValMap -> Integer -> SeqValMap)
-> (Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap)
-> Value
logicShift opW obB opS
= tlam $ \ a ->
tlam $ \ _ ->
= nlam $ \ a ->
nlam $ \ _ ->
tlam $ \ c ->
lam $ \ l -> return $
lam $ \ r -> do
@ -946,9 +946,9 @@ shiftLB w bs by =
Seq.><
Seq.replicate (fromInteger (min w by)) (ready False)
shiftLS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
shiftLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
shiftLS w ety vs by = SeqMap $ \i ->
case numTValue w of
case w of
Nat len
| i+by < len -> lookupSeqMap vs (i+by)
| i < len -> return $ zeroV ety
@ -966,9 +966,9 @@ shiftRB w bs by =
Seq.><
Seq.take (fromInteger (w - min w by)) bs
shiftRS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
shiftRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
shiftRS w ety vs by = SeqMap $ \i ->
case numTValue w of
case w of
Nat len
| i >= by -> lookupSeqMap vs (i-by)
| i < len -> return $ zeroV ety
@ -989,9 +989,9 @@ rotateLB w bs by =
let (hd,tl) = Seq.splitAt (fromInteger (by `mod` w)) bs
in tl Seq.>< hd
rotateLS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
rotateLS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
rotateLS w _ vs by = SeqMap $ \i ->
case numTValue w of
case w of
Nat len -> lookupSeqMap vs ((by + i) `mod` len)
_ -> panic "Cryptol.Eval.Prim.rotateLS" [ "unexpected infinite sequence" ]
@ -1006,9 +1006,9 @@ rotateRB w bs by =
let (hd,tl) = Seq.splitAt (fromInteger (w - (by `mod` w))) bs
in tl Seq.>< hd
rotateRS :: TValue -> TValue -> SeqValMap -> Integer -> SeqValMap
rotateRS :: Nat' -> TValue -> SeqValMap -> Integer -> SeqValMap
rotateRS w _ vs by = SeqMap $ \i ->
case numTValue w of
case w of
Nat len -> lookupSeqMap vs ((len - by + i) `mod` len)
_ -> panic "Cryptol.Eval.Prim.rotateRS" [ "unexpected infinite sequence" ]
@ -1021,9 +1021,9 @@ indexPrimOne :: BitWord b w
-> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w))
-> GenValue b w
indexPrimOne bits_op word_op =
tlam $ \ n ->
nlam $ \ n ->
tlam $ \ a ->
tlam $ \ _i ->
nlam $ \ _i ->
lam $ \ l -> return $
lam $ \ r -> do
vs <- l >>= \case
@ -1032,8 +1032,8 @@ indexPrimOne bits_op word_op =
VStream vs -> return vs
r >>= \case
VWord _ w -> w >>= \case
WordVal w' -> word_op (fromNat (numTValue n)) a vs w'
BitsVal bs -> bits_op (fromNat (numTValue n)) a vs =<< sequence bs
WordVal w' -> word_op (fromNat n) a vs w'
BitsVal bs -> bits_op (fromNat n) a vs =<< sequence bs
_ -> evalPanic "Expected word value" ["indexPrimOne"]
indexFront :: Maybe Integer -> TValue -> SeqValMap -> BV -> Eval Value
@ -1062,10 +1062,10 @@ indexPrimMany :: BitWord b w
-> (Maybe Integer -> TValue -> SeqMap b w -> w -> Eval (GenValue b w))
-> GenValue b w
indexPrimMany bits_op word_op =
tlam $ \ n ->
nlam $ \ n ->
tlam $ \ a ->
tlam $ \ m ->
tlam $ \ _i ->
nlam $ \ m ->
nlam $ \ _i ->
lam $ \ l -> return $
lam $ \ r -> do
vs <- l >>= \case
@ -1076,18 +1076,18 @@ indexPrimMany bits_op word_op =
mkSeq m a <$> memoMap (SeqMap $ \i -> do
lookupSeqMap ixs i >>= \case
VWord _ w -> w >>= \case
WordVal w' -> word_op (fromNat (numTValue n)) a vs w'
BitsVal bs -> bits_op (fromNat (numTValue n)) a vs =<< sequence bs
WordVal w' -> word_op (fromNat n) a vs w'
BitsVal bs -> bits_op (fromNat n) a vs =<< sequence bs
_ -> evalPanic "Expected word value" ["indexPrimMany"])
-- @[ 0, 1 .. ]@
fromThenV :: BitWord b w
=> GenValue b w
fromThenV =
tlamN $ \ first ->
tlamN $ \ next ->
tlamN $ \ bits ->
tlamN $ \ len ->
nlam $ \ first ->
nlam $ \ next ->
nlam $ \ bits ->
nlam $ \ len ->
case (first, next, len, bits) of
(_ , _ , _ , Nat bits')
| bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
@ -1102,9 +1102,9 @@ fromThenV =
fromToV :: BitWord b w
=> GenValue b w
fromToV =
tlamN $ \ first ->
tlamN $ \ lst ->
tlamN $ \ bits ->
nlam $ \ first ->
nlam $ \ lst ->
nlam $ \ bits ->
case (first, lst, bits) of
(_ , _ , Nat bits')
| bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
@ -1119,11 +1119,11 @@ fromToV =
fromThenToV :: BitWord b w
=> GenValue b w
fromThenToV =
tlamN $ \ first ->
tlamN $ \ next ->
tlamN $ \ lst ->
tlamN $ \ bits ->
tlamN $ \ len ->
nlam $ \ first ->
nlam $ \ next ->
nlam $ \ lst ->
nlam $ \ bits ->
nlam $ \ len ->
case (first, next, lst, len, bits) of
(_ , _ , _ , _ , Nat bits')
| bits' >= Arch.maxBigIntWidth -> wordTooWide bits'
@ -1138,7 +1138,7 @@ fromThenToV =
infFromV :: BitWord b w
=> GenValue b w
infFromV =
tlam $ \(finTValue -> bits) ->
nlam $ \(finNat' -> bits) ->
wlam $ \first ->
return $ VStream $ SeqMap $ \i ->
ready $ VWord bits $ return $
@ -1147,7 +1147,7 @@ infFromV =
infFromThenV :: BitWord b w
=> GenValue b w
infFromThenV =
tlam $ \(finTValue -> bits) ->
nlam $ \(finNat' -> bits) ->
wlam $ \first -> return $
wlam $ \next -> do
let diff = wordMinus next first
@ -1173,9 +1173,6 @@ randomV ty seed =
-- Miscellaneous ---------------------------------------------------------------
tlamN :: (Nat' -> GenValue b w) -> GenValue b w
tlamN f = VPoly (\x -> ready $ f (numTValue x))
errorV :: forall b w
. BitWord b w
=> TValue
@ -1187,7 +1184,7 @@ errorV ty msg
-- sequences
| Just (n,ety) <- isTSeq ty =
case numTValue n of
case n of
Nat w | isTBit ety -> return $ VWord w $ return $ BitsVal $
Seq.replicate (fromInteger w) (cryUserError msg)
| otherwise -> return $ mkSeq n ety (SeqMap $ \_ -> errorV ety msg)

12
src/Cryptol/Symbolic.hs
View File

@ -37,7 +37,7 @@ import qualified Cryptol.Eval as Eval
import qualified Cryptol.Eval.Monad as Eval
import qualified Cryptol.Eval.Type as Eval
import qualified Cryptol.Eval.Value as Eval
import Cryptol.Eval.Env (GenEvalEnv(..), evalType)
import Cryptol.Eval.Env (GenEvalEnv(..))
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Solver.InfNat (Nat'(..))
import Cryptol.Utils.Ident (Ident)
@ -275,8 +275,8 @@ data FinType
| FTTuple [FinType]
| FTRecord [(Ident, FinType)]
numType :: TValue -> Maybe Int
numType (Eval.numTValue -> Nat n)
numType :: Nat' -> Maybe Int
numType (Nat n)
| 0 <= n && n <= toInteger (maxBound :: Int) = Just (fromInteger n)
numType _ = Nothing
@ -303,9 +303,9 @@ unFinType fty =
predArgTypes :: Schema -> Either String [FinType]
predArgTypes schema@(Forall ts ps ty)
| null ts && null ps =
case go (evalType mempty ty) of
Just fts -> Right fts
Nothing -> Left $ "Not a valid predicate type:\n" ++ show (pp schema)
case go <$> (Eval.evalType mempty ty) of
Right (Just fts) -> Right fts
_ -> Left $ "Not a valid predicate type:\n" ++ show (pp schema)
| otherwise = Left $ "Not a monomorphic type:\n" ++ show (pp schema)
where
go :: TValue -> Maybe [FinType]

61
src/Cryptol/Symbolic/Prims.hs
View File

@ -24,16 +24,18 @@ import qualified Data.Sequence as Seq
import qualified Data.Foldable as Fold
import Cryptol.Eval.Monad (Eval(..), ready)
import Cryptol.Eval.Type (finNat')
import Cryptol.Eval.Value (BitWord(..), EvalPrims(..), enumerateSeqMap, SeqMap(..),
finiteSeqMap, reverseSeqMap, wlam, WordValue(..),
finiteSeqMap, reverseSeqMap, wlam, nlam, WordValue(..),
asWordVal, asBitsVal, fromWordVal )
import Cryptol.Prims.Eval (binary, unary, tlamN, arithUnary,
import Cryptol.Prims.Eval (binary, unary, arithUnary,
arithBinary, Binary, BinArith,
logicBinary, logicUnary, zeroV,
ccatV, splitAtV, joinV, ecSplitV,
reverseV, infFromV, infFromThenV,
fromThenV, fromToV, fromThenToV,
transposeV, indexPrimOne, indexPrimMany)
transposeV, indexPrimOne, indexPrimMany,
ecDemoteV)
import Cryptol.Symbolic.Value
import Cryptol.TypeCheck.AST (Decl(..))
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..), nMul)
@ -118,34 +120,34 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
Nat n -> Just ((i+n-shft) `mod` n)))
, ("#" , -- {a,b,d} (fin a) => [a] d -> [b] d -> [a + b] d
tlam $ \ front ->
tlam $ \ back ->
nlam $ \ front ->
nlam $ \ back ->
tlam $ \ elty ->
lam $ \ l -> return $
lam $ \ r -> join (ccatV front back elty <$> l <*> r))
, ("splitAt" ,
tlam $ \ front ->
tlam $ \ back ->
nlam $ \ front ->
nlam $ \ back ->
tlam $ \ a ->
lam $ \ x ->
splitAtV front back a =<< x)
, ("join" ,
tlam $ \ parts ->
tlam $ \ each ->
nlam $ \ parts ->
nlam $ \ each ->
tlam $ \ a ->
lam $ \ x ->
joinV parts each a =<< x)
, ("split" , ecSplitV)
, ("reverse" , tlam $ \a ->
, ("reverse" , nlam $ \a ->
tlam $ \b ->
lam $ \xs -> reverseV =<< xs)
, ("transpose" , tlam $ \a ->
tlam $ \b ->
, ("transpose" , nlam $ \a ->
nlam $ \b ->
tlam $ \c ->
lam $ \xs -> transposeV a b c =<< xs)
@ -161,8 +163,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
, ("!!" , indexPrimMany indexBack_bits indexBack)
, ("pmult" , -- {a,b} (fin a, fin b) => [a] -> [b] -> [max 1 (a + b) - 1]
tlam $ \(finTValue -> i) ->
tlam $ \(finTValue -> j) ->
nlam $ \(finNat' -> i) ->
nlam $ \(finNat' -> j) ->
VFun $ \v1 -> return $
VFun $ \v2 -> do
let k = max 1 (i + j) - 1
@ -174,8 +176,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
return $ VWord k $ return $ BitsVal $ Seq.fromList $ map ready zs)
, ("pdiv" , -- {a,b} (fin a, fin b) => [a] -> [b] -> [a]
tlam $ \(finTValue -> i) ->
tlam $ \(finTValue -> j) ->
nlam $ \(finNat' -> i) ->
nlam $ \(finNat' -> j) ->
VFun $ \v1 -> return $
VFun $ \v2 -> do
xs <- sequence . Fold.toList . Seq.reverse . asBitsVal =<< fromWordVal "pdiv 1" =<< v1
@ -184,8 +186,8 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
return $ VWord i $ return $ BitsVal $ Seq.reverse $ Seq.fromList $ map ready zs)
, ("pmod" , -- {a,b} (fin a, fin b) => [a] -> [b+1] -> [b]
tlam $ \(finTValue -> i) ->
tlam $ \(finTValue -> j) ->
nlam $ \(finNat' -> i) ->
nlam $ \(finNat' -> j) ->
VFun $ \v1 -> return $
VFun $ \v2 -> do
xs <- sequence . Fold.toList . Seq.reverse . asBitsVal =<< fromWordVal "pmod 1" =<< v1
@ -196,7 +198,7 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
-- {at,len} (fin len) => [len][8] -> at
, ("error" ,
tlam $ \at ->
tlam $ \(finTValue -> _len) ->
nlam $ \(finNat' -> _len) ->
VFun $ \_msg ->
return $ zeroV at) -- error/undefined, is arbitrarily translated to 0
@ -211,6 +213,7 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
-- values before returing the third in the symbolic
-- evaluator.
, ("trace",
nlam $ \_n ->
tlam $ \_a ->
tlam $ \_b ->
lam $ \s -> return $
@ -233,12 +236,12 @@ logicShift :: String
-> (Nat' -> Integer -> Integer -> Maybe Integer)
-> Value
logicShift nm wop reindex =
tlam $ \m ->
tlam $ \n ->
nlam $ \m ->
nlam $ \n ->
tlam $ \a ->
VFun $ \xs -> return $
VFun $ \y -> do
let Nat len = numTValue n
let Nat len = n
idx <- fromWordVal "<<" =<< y
xs >>= \case
@ -298,7 +301,7 @@ indexFront mblen a xs idx
= lookupSeqMap xs i
| Just n <- mblen
, Just (finTValue -> wlen, a') <- isTSeq a
, Just (finNat' -> wlen, a') <- isTSeq a
, isTBit a'
= do wvs <- traverse (fromWordVal "indexFront" =<<) (enumerateSeqMap n xs)
case asWordList wvs of
@ -377,18 +380,6 @@ asWordList = go id
go _ _ = Nothing
-- | Make a numeric constant.
-- { val, bits } (fin val, fin bits, bits >= width val) => [bits]
ecDemoteV :: Value
ecDemoteV = tlam $ \valT ->
tlam $ \bitT ->
case (numTValue valT, numTValue bitT) of
(Nat v, Nat bs) -> VWord bs $ ready $ WordVal $ literalSWord (fromInteger bs) v
_ -> evalPanic "Cryptol.Prove.evalECon"
["Unexpected Inf in constant."
, show valT
, show bitT
]
liftBinArith :: (SWord -> SWord -> SWord) -> BinArith SWord
liftBinArith op _ = op

4
src/Cryptol/Symbolic/Value.hs
View File

@ -19,7 +19,7 @@ module Cryptol.Symbolic.Value
, forallBV_, existsBV_
, forallSBool_, existsSBool_
, Value
, TValue, numTValue, toNumTValue, finTValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq
, TValue, isTBit, isTFun, isTSeq, isTTuple, isTRec, tvSeq
, GenValue(..), lam, tlam, toStream, toFinSeq, toSeq
, fromVBit, fromVFun, fromVPoly, fromVTuple, fromVRecord, lookupRecord
, fromSeq, fromVWord
@ -34,7 +34,7 @@ import qualified Data.Sequence as Seq
import Data.SBV.Dynamic
--import Cryptol.Eval.Monad
import Cryptol.Eval.Type (TValue, numTValue, toNumTValue, finTValue, isTBit,
import Cryptol.Eval.Type (TValue, isTBit,
isTFun, isTSeq, isTTuple, isTRec, tvSeq)
import Cryptol.Eval.Value ( GenValue(..), BitWord(..), lam, tlam, toStream,
toFinSeq, toSeq, WordValue(..), asWordVal, asBitsVal,

7
src/Cryptol/TypeCheck/Solver/InfNat.hs
View File

@ -10,17 +10,20 @@
-- element, and various arithmetic operators on them.
{-# LANGUAGE Safe #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
module Cryptol.TypeCheck.Solver.InfNat where
import Data.Bits
import Cryptol.Utils.Panic
import GHC.Generics(Generic)
import GHC.Generics (Generic)
import Control.DeepSeq
-- | Natural numbers with an infinity element
data Nat' = Nat Integer | Inf
deriving (Show,Eq,Ord,Generic)
deriving (Show, Eq, Ord, Generic, NFData)
fromNat :: Nat' -> Maybe Integer
fromNat n' =