Make 'random' compute on concrete inputs in the symbolic evaluator.

This patch does not add a warning when using 'random' in symbolic expressions.
We currently don't have any organized mechanism for generating warnings during
evaluation, and the value of emitting such a warning is debatable.

Fixes #364

src/Cryptol/Prims/Eval.hs

@@ -1271,7 +1271,7 @@ infFromThenV =
 -- | Produce a random value with the given seed. If we do not support
 -- making values of the given type, return zero of that type.
 -- TODO: do better than returning zero
-randomV :: TValue -> Integer -> Value
+randomV :: BitWord b w => TValue -> Integer -> GenValue b w
 randomV ty seed =
   case randomValue (tValTy ty) of
     Nothing -> zeroV ty

src/Cryptol/Symbolic/Prims.hs

@@ -25,7 +25,7 @@ import Data.Ord (comparing)
 import qualified Data.Sequence as Seq
 import qualified Data.Foldable as Fold
 
-import Cryptol.Eval.Monad (Eval(..), ready, invalidIndex)
+import Cryptol.Eval.Monad (Eval(..), ready, invalidIndex, cryUserError)
 import Cryptol.Eval.Type  (finNat', TValue(..))
 import Cryptol.Eval.Value (BitWord(..), EvalPrims(..), enumerateSeqMap, SeqMap(..),
                           reverseSeqMap, wlam, nlam, WordValue(..),
@@ -38,7 +38,7 @@ import Cryptol.Prims.Eval (binary, unary, arithUnary,
                            reverseV, infFromV, infFromThenV,
                            fromThenV, fromToV, fromThenToV,
                            transposeV, indexPrimOne, indexPrimMany,
-                           ecDemoteV, updatePrim)
+                           ecDemoteV, updatePrim, randomV)
 import Cryptol.Symbolic.Value
 import Cryptol.TypeCheck.AST (Decl(..))
 import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
@@ -209,11 +209,11 @@ primTable  = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
         return $ zeroV at) -- error/undefined, is arbitrarily translated to 0
 
   , ("random"      ,
-      tlam $ \_a ->
-      wlam $ \_x ->
-         Thunk $ return $ panic
-            "Cryptol.Symbolic.Prims.evalECon"
-            [ "can't symbolically evaluate ECRandom" ])
+      tlam $ \a ->
+      wlam $ \x ->
+         case SBV.svAsInteger x of
+           Just i  -> return $ randomV a i
+           Nothing -> cryUserError "cannot evaluatate 'random' with symbolic inputs")
 
      -- The trace function simply forces its first two
      -- values before returing the third in the symbolic

src/Cryptol/Testing/Random.hs

@@ -12,7 +12,7 @@
 module Cryptol.Testing.Random where
 
 import Cryptol.Eval.Monad     (ready)
-import Cryptol.Eval.Value     (BV(..),Value,GenValue(..),SeqMap(..), WordValue(..))
+import Cryptol.Eval.Value     (BV(..),Value,GenValue(..),SeqMap(..), WordValue(..), BitWord(..))
 import qualified Cryptol.Testing.Concrete as Conc
 import Cryptol.TypeCheck.AST  (Type(..),TCon(..),TC(..),tNoUser)
 import Cryptol.TypeCheck.SimpType(tRebuild')
@@ -24,7 +24,7 @@ import Data.List              (unfoldr, genericTake, genericIndex)
 import System.Random          (RandomGen, split, random, randomR)
 import qualified Data.Sequence as Seq
 
-type Gen g = Integer -> g -> (Value, g)
+type Gen g b w = Integer -> g -> (GenValue b w, g)
 
 
 {- | Apply a testable value to some randomly-generated arguments.
@@ -36,7 +36,7 @@ type Gen g = Integer -> g -> (Value, g)
  -}
 runOneTest :: RandomGen g
         => Value   -- ^ Function under test
-        -> [Gen g] -- ^ Argument generators
+        -> [Gen g Bool BV] -- ^ Argument generators
         -> Integer -- ^ Size
         -> g
         -> IO (Conc.TestResult, g)
@@ -49,7 +49,7 @@ runOneTest fun argGens sz g0 = do
 {- | Given a (function) type, compute generators for
 the function's arguments. Currently we do not support polymorphic functions.
 In principle, we could apply these to random types, and test the results. -}
-testableType :: RandomGen g => Type -> Maybe [Gen g]
+testableType :: RandomGen g => Type -> Maybe [Gen g Bool BV]
 testableType ty =
   case tNoUser ty of
     TCon (TC TCFun) [t1,t2] ->
@@ -62,7 +62,7 @@ testableType ty =
 
 {- | A generator for values of the given type.  This fails if we are
 given a type that lacks a suitable random value generator. -}
-randomValue :: RandomGen g => Type -> Maybe (Gen g)
+randomValue :: (BitWord b w, RandomGen g) => Type -> Maybe (Gen g b w)
 randomValue ty =
   case ty of
     TCon tc ts  ->
@@ -93,28 +93,28 @@ randomValue ty =
                       return (randomRecord gs)
 
 -- | Generate a random bit value.
-randomBit :: RandomGen g => Gen g
+randomBit :: (BitWord b w, RandomGen g) => Gen g b w
 randomBit _ g =
   let (b,g1) = random g
-  in (VBit b, g1)
+  in (VBit (bitLit b), g1)
 
 -- | Generate a random word of the given length (i.e., a value of type @[w]@)
 -- The size parameter is assumed to vary between 1 and 100, and we use
 -- it to generate smaller numbers first.
-randomWord :: RandomGen g => Integer -> Gen g
+randomWord :: (BitWord b w, RandomGen g) => Integer -> Gen g b w
 randomWord w _sz g =
    let (val, g1) = randomR (0,2^w-1) g
-   in (VWord w (ready (WordVal (BV w val))), g1)
+   in (VWord w (ready (WordVal (wordLit w val))), g1)
 
 -- | Generate a random infinite stream value.
-randomStream :: RandomGen g => Gen g -> Gen g
+randomStream :: RandomGen g => Gen g b w -> Gen g b w
 randomStream mkElem sz g =
   let (g1,g2) = split g
   in (VStream $ IndexSeqMap $ genericIndex (map ready (unfoldr (Just . mkElem sz) g1)), g2)
 
 {- | Generate a random sequence.  This should be used for sequences
 other than bits.  For sequences of bits use "randomWord". -}
-randomSequence :: RandomGen g => Integer -> Gen g -> Gen g
+randomSequence :: RandomGen g => Integer -> Gen g b w -> Gen g b w
 randomSequence w mkElem sz g0 = do
   let (g1,g2) = split g0
   let f g = let (x,g') = mkElem sz g
@@ -123,7 +123,7 @@ randomSequence w mkElem sz g0 = do
   seq xs (VSeq w $ IndexSeqMap $ (Seq.index xs . fromInteger), g2)
 
 -- | Generate a random tuple value.
-randomTuple :: RandomGen g => [Gen g] -> Gen g
+randomTuple :: RandomGen g => [Gen g b w] -> Gen g b w
 randomTuple gens sz = go [] gens
   where
   go els [] g = (VTuple (reverse els), g)
@@ -132,7 +132,7 @@ randomTuple gens sz = go [] gens
     in seq v (go (ready v : els) more g1)
 
 -- | Generate a random record value.
-randomRecord :: RandomGen g => [(Ident, Gen g)] -> Gen g
+randomRecord :: RandomGen g => [(Ident, Gen g b w)] -> Gen g b w
 randomRecord gens sz = go [] gens
   where
   go els [] g = (VRecord (reverse els), g)

tests/issues/issue364.cry

@@ -0,0 +1,11 @@
+x : [64]
+x = random 123
+
+x_val : [64]
+x_val = 0x80b483887be1a6e5
+
+property x_eval = x == x_val
+property x_distinct = ~ (x == zero)
+
+property moderately_bogus_property (seed:[8]) =
+  ~(random (zero#seed) == (0:[64]))

tests/issues/issue364.icry

@@ -0,0 +1,5 @@
+:set prover-stats=off
+:l issue364.cry
+:check
+:exhaust
+:prove

tests/issues/issue364.icry.stdout

@@ -0,0 +1,28 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+property x_eval Using exhaustive testing.
+testing...passed 1 tests.
+Q.E.D.
+property x_distinct Using exhaustive testing.
+testing...passed 1 tests.
+Q.E.D.
+property moderately_bogus_property Using random testing.
+testing...passed 100 tests.
+Coverage: 39.06% (100 of 256 values)
+property x_eval Using exhaustive testing.
+testing...passed 1 tests.
+Q.E.D.
+property x_distinct Using exhaustive testing.
+testing...passed 1 tests.
+Q.E.D.
+property moderately_bogus_property Using exhaustive testing.
+testing...passed 256 tests.
+Q.E.D.
+:prove x_eval
+	Q.E.D.
+:prove x_distinct
+	Q.E.D.
+:prove moderately_bogus_property
+	
+Run-time error: cannot evaluatate 'random' with symbolic inputs