Advanced testing infrastructure

cryptol-remote-api/src/CryptolServer/Data/Expression.hs

@@ -28,14 +28,15 @@ import qualified Data.Vector as V
 import Data.Text.Encoding (encodeUtf8)
 import Numeric (showHex)
 
+import Cryptol.Backend (enumerateSeqMap)
 import Cryptol.Backend.Monad
 import Cryptol.Backend.Concrete hiding (Concrete)
 import qualified Cryptol.Backend.Concrete as C
 
 import Cryptol.Eval (evalSel)
 import Cryptol.Eval.Concrete (Value)
 import Cryptol.Eval.Type (TValue(..), tValTy)
-import Cryptol.Eval.Value (GenValue(..), asWordVal, enumerateSeqMap)
+import Cryptol.Eval.Value (GenValue(..), asWordVal)
 import Cryptol.Parser
 import Cryptol.Parser.AST (Bind(..), BindDef(..), Decl(..), Expr(..), Named(Named), TypeInst(NamedInst), Type(..), PName(..), Literal(..), NumInfo(..), Type)
 import Cryptol.Parser.Position (Located(..), emptyRange)

cryptol-remote-api/src/CryptolServer/EvalExpr.hs

@@ -6,7 +6,7 @@ import Data.Aeson as JSON
 
 
 import Cryptol.ModuleSystem (checkExpr, evalExpr)
-import Cryptol.ModuleSystem.Env (meSolverConfig,deEnv,meDynEnv,loadedNewtypes)
+import Cryptol.ModuleSystem.Env (meSolverConfig,deEnv,meDynEnv)
 import Cryptol.TypeCheck.Solve (defaultReplExpr)
 import Cryptol.TypeCheck.Subst (apSubst, listParamSubst)
 import Cryptol.TypeCheck.Type (Schema(..))

lib/Cryptol.cry

@@ -558,6 +558,19 @@ x <=$ y = ~(y <$ x)
 x >=$ y = ~(x <$ y)
 
 
+// Random value generation  ---------------------------------------
+
+/**
+ * Values that support random generation.
+ */
+primitive type Generate : * -> Prop
+
+/**
+ * Generates random values from a seed.
+ */
+primitive random : {a} Generate a => [256] -> a
+
+
 // Bit specific operations ----------------------------------------
 
 /**
@@ -958,12 +971,6 @@ undefined = error "undefined"
 assert : {a, n} (fin n) => Bit -> String n -> a -> a
 assert pred msg x = if pred then x else error msg
 
-/**
- * Generates random values from a seed.  When called with a function, currently
- * generates a function that always returns zero.
- */
-primitive random : {a} [256] -> a
-
 /**
  * Debugging function for tracing.  The first argument is a string,
  * which is prepended to the printed value of the second argument.
@@ -991,6 +998,15 @@ primitive trace : {n, a, b} (fin n) => String n -> a -> b -> b
 traceVal : {n, a} (fin n) => String n -> a -> a
 traceVal msg x = trace msg x x
 
+/**
+ * Debugging function that combines the ability
+ * to print runtime values with the 'error' function that
+ * causes runtime errors.  The given error message is prepended
+ * to the printed value of the second argument.  This combined
+ * string is used to raise a runtime error.
+ */
+primitive traceError : {a, b, n} (fin n) => String n -> b -> a
+
 
 /* Functions previously in Cryptol::Extras */
 
@@ -1051,7 +1067,8 @@ foldr f acc xs = foldl g acc (reverse xs)
 
 /**
  * Functional right fold, with strict evaluation of the accumulator value.
- * The accumulator is reduced to weak head normal form at each step.
+ * The accumulator is reduced to normal form at each step. The Eq constraint
+ * restricts the accumulator to types where reduction to normal form makes sense.
  *
  * foldr' (-) 0 [1,2,3] = 0 - (1 - (2 - 3))
  */

lib/Testing.cry

@@ -0,0 +1,140 @@
+module Testing where
+
+infixl 1 >>=
+infixl 3 <|>
+infixl 4 <$>
+infixl 4 <*>
+
+primitive type Gen : * -> *
+
+primitive runGen : {a} [8] -> [256] -> Gen a -> a
+
+primitive return : {a} a -> Gen a
+primitive (>>=)  : {a,b} Gen a -> (a -> Gen b) -> Gen b
+primitive (<$>)  : {a,b} (a -> b) -> Gen a -> Gen b
+primitive genStream : {a} Gen a -> Gen ([inf]a)
+
+(<*>)  : {a,b} Gen (a -> b) -> Gen a -> Gen b
+(<*>) mf mx = mf >>= \f -> f <$> mx
+
+primitive withSize : {a} [8] -> Gen a -> Gen a
+
+// primitive type RandGen : *
+// primitive seedGen  : [8] -> [256] -> RandGen
+// primitive genSize  : RandGen -> [8]
+// primitive genResize : [8] -> RandGen -> RandGen
+// primitive splitGen : {n} (fin n, 2 <= n, width n <= 32) => RandGen -> [n]RandGen
+
+//type Gen a = RandGen -> (a, RandGen)
+
+///runGen : {a} [8] -> [256] -> Gen a -> a
+//runGen sz seed m = (m (seedGen sz seed)).0
+
+//return : {a} a -> Gen a
+//return a = \g -> (a,g)
+
+//(>>=) : {a,b} Gen a -> (a -> Gen b) -> Gen b
+//(>>=) m f = \g -> uncurry f (m g)
+
+//(<$>) : {a,b} (a -> b) -> Gen a -> Gen b
+//(<$>) f m = \g -> ((f x,g') where (x,g') = m g)
+
+//(<*>) : {a,b} Gen (a -> b) -> Gen a -> Gen b
+//(<*>) mf m = \g ->
+//    ((f x,g2) where
+//                (f,g1) = mf g
+//		(x,g2) = m g1)
+
+// private
+//   mkStream : {a} Gen a -> RandGen -> [inf]a
+//   mkStream m g = xs.0
+//     where
+//       xs = [ m g ] # [ m g' | (_,g') <- xs ]
+
+// genStreams : {n,a} (fin n, n>=1, width (n+1) <= 32) => Gen a -> Gen ([n][inf]a)
+// genStreams m = \g0 -> ( (map (mkStream m) gs, g') where gs#[g'] = splitGen`{n+1} g0 )
+
+// genStream : {a} Gen a -> Gen ([inf]a)
+// genStream m = \g0 -> ((mkStream m g1, g2) where [g1,g2] = splitGen g0)
+
+
+primitive generate : {a} Generate a => Gen a
+
+unboundedInteger : Gen Integer
+unboundedInteger = generate`{Integer}
+
+primitive boundedInteger : (Integer, Integer) -> Gen Integer
+primitive boundedBelowInteger : Integer -> Gen Integer
+primitive boundedAboveInteger : Integer -> Gen Integer
+
+unboundedWord : {n} (fin n) => Gen [n]
+unboundedWord = generate`{[n]}
+
+primitive boundedWord : {n} (fin n) => ([n],[n]) -> Gen [n]
+primitive boundedSignedWord : {n} (fin n) => ([n],[n]) -> Gen [n]
+
+primitive suchThat : {a} Gen a -> (a -> Bool) -> Gen a
+
+(<|>) : {a} Gen a -> Gen a -> Gen a
+(<|>) x y = generate`{Bit} >>= \b -> if b then x else y
+
+choose : {n,a} (fin n, n >= 1) => [n](Gen a) -> Gen a
+choose gs = boundedInteger (0,`(n-1)) >>= \i -> gs@i
+
+oneOf : {n,a} (fin n, n >= 1) => [n]a -> Gen a
+oneOf xs = choose (map return xs)
+
+genSequence : {n,a} (fin n) => Gen a -> Gen ([n]a)
+genSequence m = take`{n} <$> genStream m
+
+genPair : {a,b} Gen a -> Gen b -> Gen (a,b)
+genPair ma mb =
+  ma >>= \a ->
+  mb >>= \b ->
+  return (a,b)
+
+
+isEven : Integer -> Bit
+isEven i = i%2 == 0
+
+isOdd : Integer -> Bit
+isOdd i = i%2 == 1
+
+evenInteger : Gen Integer
+evenInteger = suchThat generate isEven
+
+oddInteger : Gen Integer
+oddInteger = suchThat generate isOdd
+
+addOddProp : Gen Bit
+property addOddProp = evenSum <$> oddInteger <*> oddInteger
+  where
+    evenSum x y = isEven (x + y)
+
+runTests : Integer -> Gen Bit -> [256] -> Bit
+runTests num m seed = runGen 100 seed (loop 0)
+  where
+    loop n = if n >= num then return True else go n
+    go n = withSize (sz n) m >>= \b -> if b then loop (n+1) else return False
+    sz n = fromInteger (1 + ((n * 100) / num))
+
+withCounterexample : {a,n} (fin n) => String n -> a -> Bit -> Bit
+withCounterexample msg vals test = test \/ traceError ("counterexample " # msg) vals
+
+addOddPropWrong : Gen Bit
+property addOddPropWrong = evenSum <$> oddInteger <*> evenInteger
+  where
+    evenSum x y = withCounterexample "evenSum" (x,y) (isEven (x+y))
+
+
+addNoOverflow : Gen Bit
+property addNoOverflow = noOverflow <$> boundedBelowInteger 0 <*> boundedBelowInteger 0
+  where
+   noOverflow : Integer -> Integer -> Bit
+   noOverflow x y = withCounterexample "noOverflow" (x,y) (x <= (x+y) /\ y <= (x+y))
+
+addNoWordOverflow : Gen Bit
+property addNoWordOverflow = noOverflow <$> boundedWord (0,0x8FFFFFFF) <*> boundedWord (0,0x7FFFFFFF)
+  where
+   noOverflow : [32] -> [32] -> Bit
+   noOverflow x y = withCounterexample "noOverflow" (x,y) (x <= (x+y) /\ y <= (x+y))