From ff3b603d6a4d7c7ab326a4de32a238a08ff6b59e Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Thu, 10 Dec 2020 14:14:31 -0800
Subject: [PATCH] First cut at adding real numbers to Cryptol.

There are some tricky unanswered questions about what
to do with models that return algebraic reals.  I'm almost
inclined to make real numbers explicitly compute on the
algebraic reals, but that would be a farily large undertaking.

In addition, we should probably pay more attention to pretty printing
for real and rational values and give more options for decimal
printing, approximation, precision, etc.
---
 lib/Cryptol.cry                       | 28 +++++++-
 src/Cryptol/Backend.hs                | 95 ++++++++++++++++++++++++++-
 src/Cryptol/Backend/Concrete.hs       | 29 ++++++++
 src/Cryptol/Backend/SBV.hs            | 33 ++++++++++
 src/Cryptol/Backend/What4.hs          | 33 ++++++++++
 src/Cryptol/Eval.hs                   |  2 +
 src/Cryptol/Eval/Concrete.hs          |  4 ++
 src/Cryptol/Eval/Generic.hs           | 86 ++++++++++++++++++------
 src/Cryptol/Eval/Reference.lhs        | 25 +++++++
 src/Cryptol/Eval/Type.hs              |  3 +
 src/Cryptol/Eval/Value.hs             | 18 +++++
 src/Cryptol/Symbolic.hs               | 18 +++++
 src/Cryptol/Symbolic/SBV.hs           |  5 ++
 src/Cryptol/Symbolic/What4.hs         |  2 +
 src/Cryptol/Testing/Random.hs         |  6 ++
 src/Cryptol/TypeCheck/Solver/Class.hs | 32 ++++++++-
 src/Cryptol/TypeCheck/TCon.hs         |  4 ++
 src/Cryptol/TypeCheck/Type.hs         | 10 +++
 18 files changed, 410 insertions(+), 23 deletions(-)

diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
index c05c8f03a..8c8e1c622 100644
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -52,7 +52,8 @@ primitive type {n : #} (fin n, n >= 1) => Z n : *
 
 /**
  * 'Rational' is the type of rational numbers.
- * Rational numbers form a Field (and thus a Ring).
+ * Rational numbers form a Field (and thus a Ring),
+ * and rational numbers also inhabit the Round class.
  *
  * The 'ratio' operation may be used to directly create
  * rational values from as a ratio of integers, or
@@ -61,6 +62,23 @@ primitive type {n : #} (fin n, n >= 1) => Z n : *
  */
 primitive type Rational : *
 
+/**
+ * 'Real' is the type of real numbers.
+ * Real numbers form a Field (and thus a Ring),
+ * and real numbers also inhabit the Round class.
+ *
+ * For computation purposes, 'Real' is very similar
+ * to 'Rational'.  However, the logical theory of real
+ * numbers admits algebraic numbers in addition to
+ * rationals.  Counterintuitively, solvers may have a
+ * simpler time solving problems involving the real numbers
+ * than similar problems involving the integers or the
+ * rationals because there are dedicated algorithms that
+ * can be applied to real closed fields.
+ */
+primitive type Real : *
+
+
 type Bool = Bit
 type Word n = [n]
 type Char = [8]
@@ -680,6 +698,14 @@ primitive lg2 : {n} (fin n) => [n] -> [n]
 primitive ratio : Integer -> Integer -> Rational
 
 
+// Real specific operations --------------------------------------------------
+
+/**
+ * Compute the real number corresponding to the given rational.
+ */
+primitive fromRational : Rational -> Real
+
+
 // Zn specific operations ----------------------------------------------------
 
 /**
diff --git a/src/Cryptol/Backend.hs b/src/Cryptol/Backend.hs
index 023a3b2e5..abc7ada98 100644
--- a/src/Cryptol/Backend.hs
+++ b/src/Cryptol/Backend.hs
@@ -213,6 +213,7 @@ class MonadIO (SEval sym) => Backend sym where
   type SWord sym :: Type
   type SInteger sym :: Type
   type SFloat sym :: Type
+  type SReal sym :: Type
   type SEval sym :: Type -> Type
 
   -- ==== Evaluation monad operations ====
@@ -281,7 +282,6 @@ class MonadIO (SEval sym) => Backend sym where
   -- | Pretty-print a floating-point value
   ppFloat :: sym -> PPOpts -> SFloat sym -> Doc
 
-
   -- ==== Identifying literal values ====
 
   -- | Determine if this symbolic bit is a boolean literal
@@ -301,6 +301,9 @@ class MonadIO (SEval sym) => Backend sym where
   -- | Determine if this symbolic integer is a literal
   integerAsLit :: sym -> SInteger sym -> Maybe Integer
 
+  -- | Determine if this symbolic real is a literal
+  realAsLit :: sym -> SReal sym -> Maybe Rational
+
   -- ==== Creating literal values ====
 
   -- | Construct a literal bit value from a boolean.
@@ -319,6 +322,12 @@ class MonadIO (SEval sym) => Backend sym where
     Integer {- ^ Value -} ->
     SEval sym (SInteger sym)
 
+  -- | Construct a literal real value from the given rational
+  realLit ::
+    sym ->
+    Rational ->
+    SEval sym (SReal sym)
+
   -- | Construct a floating point value from the given rational.
   fpLit ::
     sym ->
@@ -335,6 +344,7 @@ class MonadIO (SEval sym) => Backend sym where
   iteBit :: sym -> SBit sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
   iteWord :: sym -> SBit sym -> SWord sym -> SWord sym -> SEval sym (SWord sym)
   iteInteger :: sym -> SBit sym -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)
+  iteReal :: sym -> SBit sym -> SReal sym -> SReal sym -> SEval sym (SReal sym)
 
   -- ==== Bit operations ====
   bitEq  :: sym -> SBit sym -> SBit sym -> SEval sym (SBit sym)
@@ -627,6 +637,89 @@ class MonadIO (SEval sym) => Backend sym where
     SInteger sym ->
     SEval sym (SBit sym)
 
+  -- ==== Real operations =====
+
+  intToReal ::
+    sym ->
+    SInteger sym ->
+    SEval sym (SReal sym)
+
+  realPlus ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realNegate ::
+    sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realMinus ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realMult ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realRecip ::
+    sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realDiv ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SReal sym)
+
+  realEq ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SBit sym)
+
+  realLessThan ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SBit sym)
+
+  realGreaterThan ::
+    sym ->
+    SReal sym ->
+    SReal sym ->
+    SEval sym (SBit sym)
+
+  realFloor ::
+    sym ->
+    SReal sym ->
+    SEval sym (SInteger sym)
+
+  realCeiling ::
+    sym ->
+    SReal sym ->
+    SEval sym (SInteger sym)
+
+  realTrunc ::
+    sym ->
+    SReal sym ->
+    SEval sym (SInteger sym)
+
+  realRoundAway ::
+    sym ->
+    SReal sym ->
+    SEval sym (SInteger sym)
+
+  realRoundToEven ::
+    sym ->
+    SReal sym ->
+    SEval sym (SInteger sym)
 
   -- ==== Operations on Z_n ====
 
diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs
index b653a0d25..d7574ff51 100644
--- a/src/Cryptol/Backend/Concrete.hs
+++ b/src/Cryptol/Backend/Concrete.hs
@@ -134,8 +134,10 @@ instance Backend Concrete where
   type SWord Concrete = BV
   type SInteger Concrete = Integer
   type SFloat Concrete = FP.BF
+  type SReal Concrete = Rational
   type SEval Concrete = Eval
 
+
   raiseError _ err =
     do stk <- getCallStack
        io (X.throwIO (EvalErrorEx stk err))
@@ -186,6 +188,7 @@ instance Backend Concrete where
   iteBit _ b x y  = pure $! if b then x else y
   iteWord _ b x y = pure $! if b then x else y
   iteInteger _ b x y = pure $! if b then x else y
+  iteReal _ b x y = pure $! if b then x else y
 
   wordLit _ w i = pure $! mkBv w i
   wordAsLit _ (BV w i) = Just (w,i)
@@ -309,6 +312,32 @@ instance Backend Concrete where
     do assertSideCondition sym (y /= 0) DivideByZero
        pure $! x `mod` y
 
+  realAsLit _ x = Just x
+  realLit _ x   = pure x
+  intToReal _ x = pure $! (fromInteger x :: Rational)
+  realPlus _ x y  = pure $! x + y
+  realNegate _ x  = pure $! negate x
+  realMinus _ x y = pure $! x - y
+  realMult _ x y  = pure $! x * y
+  realRecip sym x =
+    do assertSideCondition sym (x /= 0) DivideByZero
+       pure $! recip x
+  realDiv sym x y =
+    do assertSideCondition sym (y /= 0) DivideByZero
+       pure $! x / y
+
+  realEq _ x y          = pure $! x == y
+  realLessThan _ x y    = pure $! x < y
+  realGreaterThan _ x y = pure $! x > y
+
+  realFloor _ x       = pure $! floor x
+  realCeiling _ x     = pure $! ceiling x
+  realTrunc _ x       = pure $! truncate x
+  realRoundToEven _ x = pure $! round x
+  realRoundAway _ x
+    | x >= 0    = pure $! floor (x + 0.5)
+    | otherwise = pure $! ceiling (x - 0.5)
+
   intToZn _ 0 _ = evalPanic "intToZn" ["0 modulus not allowed"]
   intToZn _ m x = pure $! x `mod` m
 
diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs
index 78c184374..6a432e8d7 100644
--- a/src/Cryptol/Backend/SBV.hs
+++ b/src/Cryptol/Backend/SBV.hs
@@ -23,6 +23,7 @@ module Cryptol.Backend.SBV
   , freshSBool_
   , freshBV_
   , freshSInteger_
+  , freshSReal_
   , addDefEqn
   , ashr
   , lshr
@@ -37,6 +38,7 @@ import           Control.Concurrent.MVar
 import           Control.Monad.IO.Class (MonadIO(..))
 import           Data.Bits (bit, complement)
 import           Data.List (foldl')
+import           Data.Ratio
 
 import qualified GHC.Integer.GMP.Internals as Integer
 
@@ -94,6 +96,9 @@ freshSInteger_ :: SBV -> IO (SInteger SBV)
 freshSInteger_ (SBV stateVar _) =
   withMVar stateVar (svMkSymVar_ Nothing KUnbounded Nothing)
 
+freshSReal_ :: SBV -> IO (SReal SBV)
+freshSReal_ (SBV stateVar _) =
+  withMVar stateVar (svMkSymVar_ Nothing KReal Nothing)
 
 -- SBV Evaluation monad -------------------------------------------------------
 
@@ -153,6 +158,7 @@ instance Backend SBV where
   type SWord SBV = SVal
   type SInteger SBV = SVal
   type SFloat SBV = ()        -- XXX: not implemented
+  type SReal SBV = SVal
   type SEval SBV = SBVEval
 
   raiseError _ err = SBVEval $
@@ -216,6 +222,7 @@ instance Backend SBV where
   iteBit _ b x y = pure $! svSymbolicMerge KBool True b x y
   iteWord _ b x y = pure $! svSymbolicMerge (kindOf x) True b x y
   iteInteger _ b x y = pure $! svSymbolicMerge KUnbounded True b x y
+  iteReal _ b x y = pure $! svSymbolicMerge KReal True b x y
 
   bitAsLit _ b = svAsBool b
   wordAsLit _ w =
@@ -318,6 +325,32 @@ instance Backend SBV where
        let p = svLessThan z b
        pure $! svSymbolicMerge KUnbounded True p (svRem a b) (svUNeg (svRem (svUNeg a) (svUNeg b)))
 
+  realLit _ q = pure $! svReal q
+  realAsLit _ x =
+    do n <- svNumerator x
+       d <- svDenominator x
+       pure (n % d)
+  intToReal _ i   = pure $! svFromIntegral KReal i
+  realPlus _ x y  = pure $! svPlus x y
+  realNegate _ x  = pure $! SBV.svUNeg x
+  realMinus _ x y = pure $! svMinus x y
+  realMult _ x y  = pure $! svTimes x y
+  realRecip sym x = realDiv sym (svReal 1) x
+  realDiv sym x y =
+    do let z = svReal 0
+       assertSideCondition sym (svNot (svEqual y z)) DivideByZero
+       pure $! svDivide x y
+
+  realEq _ x y          = pure $! svEqual x y
+  realLessThan _ x y    = pure $! svLessThan x y
+  realGreaterThan _ x y = pure $! svGreaterThan x y
+
+  realFloor _ _       = unsupported "real floor"
+  realCeiling _ _     = unsupported "real ceiling"
+  realTrunc _ _       = unsupported "real trunc"
+  realRoundAway _ _   = unsupported "real roundAway"
+  realRoundToEven _ _ = unsupported "real roundToEven"
+
   -- NB, we don't do reduction here
   intToZn _ _m a = pure a
 
diff --git a/src/Cryptol/Backend/What4.hs b/src/Cryptol/Backend/What4.hs
index 1c30726ef..51c1d63a4 100644
--- a/src/Cryptol/Backend/What4.hs
+++ b/src/Cryptol/Backend/What4.hs
@@ -205,13 +205,21 @@ assertIntDivisor sym x =
   do p <- liftIO (W4.notPred (w4 sym) =<< W4.intEq (w4 sym) x =<< W4.intLit (w4 sym) 0)
      assertSideCondition sym p DivideByZero
 
+assertRealDivisor ::
+  W4.IsSymExprBuilder sym => What4 sym -> W4.SymReal sym -> W4Eval sym ()
+assertRealDivisor sym x =
+  do p <- liftIO (W4.notPred (w4 sym) =<< W4.realEq (w4 sym) x =<< W4.realLit (w4 sym) 0)
+     assertSideCondition sym p DivideByZero
+
 instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
   type SBit (What4 sym)     = W4.Pred sym
   type SWord (What4 sym)    = SW.SWord sym
   type SInteger (What4 sym) = W4.SymInteger sym
+  type SReal (What4 sym)    = W4.SymReal sym
   type SFloat (What4 sym)   = FP.SFloat sym
   type SEval (What4 sym)    = W4Eval sym
 
+
   raiseError _ = evalError
 
   assertSideCondition _ cond err
@@ -314,6 +322,7 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
   iteBit sym c x y = liftIO (W4.itePred (w4 sym) c x y)
   iteWord sym c x y = liftIO (SW.bvIte (w4 sym) c x y)
   iteInteger sym c x y = liftIO (W4.intIte (w4 sym) c x y)
+  iteReal sym c x y = liftIO (W4.realIte (w4 sym) c x y)
 
   bitEq  sym x y = liftIO (W4.eqPred (w4 sym) x y)
   bitAnd sym x y = liftIO (W4.andPred (w4 sym) x y)
@@ -425,6 +434,30 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
   intLessThan sym x y = liftIO $ W4.intLt (w4 sym) x y
   intGreaterThan sym x y = liftIO $ W4.intLt (w4 sym) y x
 
+  realAsLit _ x     = W4.asRational x
+  realLit sym x     = liftIO (W4.realLit (w4 sym) x)
+  intToReal sym x   = liftIO (W4.integerToReal (w4 sym) x)
+  realPlus sym x y  = liftIO (W4.realAdd (w4 sym) x y)
+  realNegate sym x  = liftIO (W4.realNeg (w4 sym) x)
+  realMinus sym x y = liftIO (W4.realSub (w4 sym) x y)
+  realMult sym x y  = liftIO (W4.realMul (w4 sym) x y)
+  realRecip sym x   =
+    do one <- liftIO (W4.realLit (w4 sym) 1)
+       realDiv sym one x
+  realDiv sym x y =
+    do assertRealDivisor sym y
+       liftIO (W4.realDiv (w4 sym) x y)
+
+  realEq sym x y          = liftIO (W4.realEq (w4 sym) x y)
+  realLessThan sym x y    = liftIO (W4.realLt (w4 sym) x y)
+  realGreaterThan sym x y = liftIO (W4.realGt (w4 sym) x y)
+
+  realFloor sym x       = liftIO (W4.realFloor (w4 sym) x)
+  realCeiling sym x     = liftIO (W4.realCeil (w4 sym) x)
+  realTrunc sym x       = liftIO (W4.realTrunc (w4 sym) x)
+  realRoundAway sym x   = liftIO (W4.realRound (w4 sym) x)
+  realRoundToEven sym x = liftIO (W4.realRoundEven (w4 sym) x)
+
   -- NB, we don't do reduction here on symbolic values
   intToZn sym m x
     | Just xi <- W4.asInteger x
diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs
index 67718a09c..c66bc7f77 100644
--- a/src/Cryptol/Eval.hs
+++ b/src/Cryptol/Eval.hs
@@ -443,6 +443,7 @@ etaDelay sym env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
       VWord{}     -> x
       VRational{} -> x
       VFloat{}    -> x
+      VReal{}     -> x
       VSeq n xs ->
         case tp of
           TVSeq _nt el -> return $ VSeq n $ IndexSeqMap $ \i -> go stk el (lookupSeqMap xs i)
@@ -484,6 +485,7 @@ etaDelay sym env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
     case tp of
       TVBit -> v
       TVInteger -> v
+      TVReal -> v
       TVFloat {} -> v
       TVIntMod _ -> v
       TVRational -> v
diff --git a/src/Cryptol/Eval/Concrete.hs b/src/Cryptol/Eval/Concrete.hs
index 28c7c0e9f..26530c5c4 100644
--- a/src/Cryptol/Eval/Concrete.hs
+++ b/src/Cryptol/Eval/Concrete.hs
@@ -94,6 +94,9 @@ toExpr prims t0 v0 = findOne (go t0 v0)
         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'
+      VReal r ->
+        do q <- go tRational (VRational (SRational (numerator r) (denominator r)))
+           pure $ EApp (prim "fromRational") q
       VFloat i ->
         do (eT, pT) <- maybe mismatch pure (tIsFloat ty)
            pure (floatToExpr prims eT pT (bfValue i))
@@ -118,6 +121,7 @@ toExpr prims t0 v0 = findOne (go t0 v0)
              , render doc
              ]
 
+
 floatToExpr :: PrimMap -> AST.Type -> AST.Type -> FP.BigFloat -> AST.Expr
 floatToExpr prims eT pT f =
   case FP.bfToRep f of
diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index 750ef4643..48fb4dbd0 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -64,6 +64,7 @@ mkLit sym ty i =
     TVFloat e p                  -> VFloat <$> fpLit sym e p (fromInteger i)
     TVSeq w TVBit                -> pure $ word sym w i
     TVRational                   -> VRational <$> (intToRational sym =<< integerLit sym i)
+    TVReal                       -> VReal <$> realLit sym (fromInteger i :: Rational)
     _                            -> evalPanic "Cryptol.Eval.Prim.evalConst"
                                     [ "Invalid type for number" ]
 
@@ -94,6 +95,7 @@ intV sym i =
     (pure i)
     (\m -> intToZn sym m i)
     (intToRational sym i)
+    (intToReal sym i)
     (\e p -> fpRndMode sym >>= \r -> fpFromInteger sym e p r i)
 
 {-# SPECIALIZE ratioV :: Concrete -> Prim Concrete #-}
@@ -117,6 +119,7 @@ ecFractionV sym =
   PPrim
     case ty of
       TVFloat e p -> VFloat <$> fpLit sym e p (n % d)
+      TVReal -> VReal <$> realLit sym (n % d)
       TVRational ->
         do x <- integerLit sym n
            y <- integerLit sym d
@@ -166,6 +169,7 @@ type BinWord sym = Integer -> SWord sym -> SWord sym -> SEval sym (SWord sym)
       (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
       (Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
       (SRational Concrete -> SRational Concrete -> SEval Concrete (SRational Concrete)) ->
+      (SReal Concrete -> SReal Concrete -> SEval Concrete (SReal Concrete)) ->
       (SFloat Concrete -> SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->
       Binary Concrete
   #-}
@@ -177,9 +181,10 @@ ringBinary :: forall sym.
   (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
   (Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
   (SRational sym -> SRational sym -> SEval sym (SRational sym)) ->
+  (SReal sym -> SReal sym -> SEval sym (SReal sym)) ->
   (SFloat sym -> SFloat sym -> SEval sym (SFloat sym)) ->
   Binary sym
-ringBinary sym opw opi opz opq opfp = loop
+ringBinary sym opw opi opz opq opr opfp = loop
   where
   loop' :: TValue
         -> SEval sym (GenValue sym)
@@ -207,6 +212,9 @@ ringBinary sym opw opi opz opq opfp = loop
     TVRational ->
       VRational <$> opq (fromVRational l) (fromVRational r)
 
+    TVReal ->
+      VReal <$> opr (fromVReal l) (fromVReal r)
+
     TVArray{} ->
       evalPanic "arithBinary" ["Array not in class Ring"]
 
@@ -256,6 +264,7 @@ type UnaryWord sym = Integer -> SWord sym -> SEval sym (SWord sym)
   (SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
   (Integer -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
   (SRational Concrete -> SEval Concrete (SRational Concrete)) ->
+  (SReal Concrete -> SEval Concrete (SReal Concrete)) ->
   (SFloat Concrete -> SEval Concrete (SFloat Concrete)) ->
   Unary Concrete
   #-}
@@ -266,9 +275,10 @@ ringUnary :: forall sym.
   (SInteger sym -> SEval sym (SInteger sym)) ->
   (Integer -> SInteger sym -> SEval sym (SInteger sym)) ->
   (SRational sym -> SEval sym (SRational sym)) ->
+  (SReal sym -> SEval sym (SReal sym)) ->
   (SFloat sym -> SEval sym (SFloat sym)) ->
   Unary sym
-ringUnary sym opw opi opz opq opfp = loop
+ringUnary sym opw opi opz opq opr opfp = loop
   where
   loop' :: TValue -> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
   loop' ty v = loop ty =<< v
@@ -291,6 +301,9 @@ ringUnary sym opw opi opz opq opfp = loop
     TVRational ->
       VRational <$> opq (fromVRational v)
 
+    TVReal ->
+      VReal <$> opr (fromVReal v)
+
     TVArray{} ->
       evalPanic "arithUnary" ["Array not in class Ring"]
 
@@ -329,6 +342,7 @@ ringUnary sym opw opi opz opq opfp = loop
   SEval Concrete (SInteger Concrete) ->
   (Integer -> SEval Concrete (SInteger Concrete)) ->
   SEval Concrete (SRational Concrete) ->
+  SEval Concrete (SReal Concrete) ->
   (Integer -> Integer -> SEval Concrete (SFloat Concrete)) ->
   TValue ->
   SEval Concrete (GenValue Concrete)
@@ -341,10 +355,11 @@ ringNullary :: forall sym.
   SEval sym (SInteger sym) ->
   (Integer -> SEval sym (SInteger sym)) ->
   SEval sym (SRational sym) ->
+  SEval sym (SReal sym) ->
   (Integer -> Integer -> SEval sym (SFloat sym)) ->
   TValue ->
   SEval sym (GenValue sym)
-ringNullary sym opw opi opz opq opfp = loop
+ringNullary sym opw opi opz opq opr opfp = loop
   where
     loop :: TValue -> SEval sym (GenValue sym)
     loop ty =
@@ -359,6 +374,8 @@ ringNullary sym opw opi opz opq opfp = loop
 
         TVRational -> VRational <$> opq
 
+        TVReal -> VReal <$> opr 
+
         TVArray{} -> evalPanic "arithNullary" ["Array not in class Ring"]
 
         TVSeq w a
@@ -431,42 +448,46 @@ fromIntegerV sym =
 
 {-# INLINE addV #-}
 addV :: Backend sym => sym -> Binary sym
-addV sym = ringBinary sym opw opi opz opq opfp
+addV sym = ringBinary sym opw opi opz opq opr opfp
   where
     opw _w x y = wordPlus sym x y
     opi x y = intPlus sym x y
     opz m x y = znPlus sym m x y
     opq x y = rationalAdd sym x y
+    opr x y = realPlus sym x y
     opfp x y = fpRndMode sym >>= \r -> fpPlus sym r x y
 
 {-# INLINE subV #-}
 subV :: Backend sym => sym -> Binary sym
-subV sym = ringBinary sym opw opi opz opq opfp
+subV sym = ringBinary sym opw opi opz opq opr opfp
   where
     opw _w x y = wordMinus sym x y
     opi x y = intMinus sym x y
     opz m x y = znMinus sym m x y
     opq x y = rationalSub sym x y
+    opr x y = realMinus sym x y
     opfp x y = fpRndMode sym >>= \r -> fpMinus sym r x y
 
 {-# INLINE negateV #-}
 negateV :: Backend sym => sym -> Unary sym
-negateV sym = ringUnary sym opw opi opz opq opfp
+negateV sym = ringUnary sym opw opi opz opq opr opfp
   where
     opw _w x = wordNegate sym x
     opi x = intNegate sym x
     opz m x = znNegate sym m x
     opq x = rationalNegate sym x
+    opr x = realNegate sym x
     opfp x = fpNeg sym x
 
 {-# INLINE mulV #-}
 mulV :: Backend sym => sym -> Binary sym
-mulV sym = ringBinary sym opw opi opz opq opfp
+mulV sym = ringBinary sym opw opi opz opq opr opfp
   where
     opw _w x y = wordMult sym x y
     opi x y = intMult sym x y
     opz m x y = znMult sym m x y
     opq x y = rationalMul sym x y
+    opr x y = realMult sym x y
     opfp x y = fpRndMode sym >>= \r -> fpMult sym r x y
 
 --------------------------------------------------
@@ -568,6 +589,7 @@ recipV sym =
   PPrim
     case a of
       TVRational -> VRational <$> (rationalRecip sym . fromVRational =<< x)
+      TVReal -> VReal <$> (realRecip sym . fromVReal =<< x)
       TVFloat e p ->
         do one <- fpLit sym e p 1
            r   <- fpRndMode sym
@@ -588,6 +610,10 @@ fieldDivideV sym =
         do x' <- fromVRational <$> x
            y' <- fromVRational <$> y
            VRational <$> rationalDivide sym x' y'
+      TVReal ->
+        do x' <- fromVReal <$> x
+           y' <- fromVReal <$> y
+           VReal <$> realDiv sym x' y'
       TVFloat _e _p ->
         do xv <- fromVFloat <$> x
            yv <- fromVFloat <$> y
@@ -608,6 +634,7 @@ fieldDivideV sym =
   Concrete ->
   String ->
   (SRational Concrete -> SEval Concrete (SInteger Concrete)) ->
+  (SReal Concrete -> SEval Concrete (SInteger Concrete)) ->
   (SFloat Concrete -> SEval Concrete (SInteger Concrete)) ->
   Unary Concrete #-}
 
@@ -616,47 +643,54 @@ roundOp ::
   sym ->
   String ->
   (SRational sym -> SEval sym (SInteger sym)) ->
+  (SReal sym -> SEval sym (SInteger sym)) ->
   (SFloat sym -> SEval sym (SInteger sym)) ->
   Unary sym
-roundOp _sym nm qop opfp ty v =
+roundOp _sym nm qop rop opfp ty v =
   case ty of
-    TVRational  -> VInteger <$> (qop (fromVRational v))
+    TVRational  -> VInteger <$> qop (fromVRational v)
+    TVReal      -> VInteger <$> rop (fromVReal v)
     TVFloat _ _ -> VInteger <$> opfp (fromVFloat v)
     _ -> evalPanic nm [show ty ++ " is not a Field"]
 
 {-# INLINE floorV #-}
 floorV :: Backend sym => sym -> Unary sym
-floorV sym = roundOp sym "floor" opq opfp
+floorV sym = roundOp sym "floor" opq opr opfp
   where
   opq = rationalFloor sym
+  opr = realFloor sym
   opfp = \x -> fpRndRTN sym >>= \r -> fpToInteger sym "floor" r x
 
 {-# INLINE ceilingV #-}
 ceilingV :: Backend sym => sym -> Unary sym
-ceilingV sym = roundOp sym "ceiling" opq opfp
+ceilingV sym = roundOp sym "ceiling" opq opr opfp
   where
   opq = rationalCeiling sym
+  opr = realCeiling sym
   opfp = \x -> fpRndRTP sym >>= \r -> fpToInteger sym "ceiling" r x
 
 {-# INLINE truncV #-}
 truncV :: Backend sym => sym -> Unary sym
-truncV sym = roundOp sym "trunc" opq opfp
+truncV sym = roundOp sym "trunc" opq opr opfp
   where
   opq = rationalTrunc sym
+  opr = realTrunc sym
   opfp = \x -> fpRndRTZ sym >>= \r -> fpToInteger sym "trunc" r x
 
 {-# INLINE roundAwayV #-}
 roundAwayV :: Backend sym => sym -> Unary sym
-roundAwayV sym = roundOp sym "roundAway" opq opfp
+roundAwayV sym = roundOp sym "roundAway" opq opr opfp
   where
   opq = rationalRoundAway sym
+  opr = realRoundAway sym
   opfp = \x -> fpRndRNA sym >>= \r -> fpToInteger sym "roundAway" r x
 
 {-# INLINE roundToEvenV #-}
 roundToEvenV :: Backend sym => sym -> Unary sym
-roundToEvenV sym = roundOp sym "roundToEven" opq opfp
+roundToEvenV sym = roundOp sym "roundToEven" opq opr opfp
   where
   opq = rationalRoundToEven sym
+  opr = realRoundToEven sym
   opfp = \x -> fpRndRNE sym >>= \r -> fpToInteger sym "roundToEven" r x
 
 --------------------------------------------------------------
@@ -712,6 +746,7 @@ smodV sym  =
   (SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (SRational Concrete -> SRational Concrete -> SEval Concrete a -> SEval Concrete a) ->
+  (SReal Concrete -> SReal Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (SFloat Concrete -> SFloat Concrete -> SEval Concrete a -> SEval Concrete a) ->
   (TValue -> GenValue Concrete -> GenValue Concrete -> SEval Concrete a -> SEval Concrete a)
   #-}
@@ -724,9 +759,10 @@ cmpValue ::
   (SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
   (Integer -> SInteger sym -> SInteger sym -> SEval sym a -> SEval sym a) ->
   (SRational sym -> SRational sym -> SEval sym a -> SEval sym a) ->
+  (SReal sym -> SReal sym -> SEval sym a -> SEval sym a) ->
   (SFloat sym -> SFloat sym -> SEval sym a -> SEval sym a) ->
   (TValue -> GenValue sym -> GenValue sym -> SEval sym a -> SEval sym a)
-cmpValue sym fb fw fi fz fq ff = cmp
+cmpValue sym fb fw fi fz fq fr ff = cmp
   where
     cmp ty v1 v2 k =
       case ty of
@@ -735,6 +771,7 @@ cmpValue sym fb fw fi fz fq ff = cmp
         TVFloat _ _   -> ff (fromVFloat v1) (fromVFloat v2) k
         TVIntMod n    -> fz n (fromVInteger v1) (fromVInteger v2) k
         TVRational    -> fq (fromVRational v1) (fromVRational v2) k
+        TVReal        -> fr (fromVReal v1) (fromVReal v2) k
         TVArray{}     -> panic "Cryptol.Prims.Value.cmpValue"
                                [ "Arrays are not comparable" ]
         TVSeq n t
@@ -777,37 +814,40 @@ bitGreaterThan sym x y = bitLessThan sym y x
 
 {-# INLINE valEq #-}
 valEq :: Backend sym => sym -> TValue -> GenValue sym -> GenValue sym -> SEval sym (SBit sym)
-valEq sym ty v1 v2 = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym True)
+valEq sym ty v1 v2 = cmpValue sym fb fw fi fz fq fr ff ty v1 v2 (pure $ bitLit sym True)
   where
   fb x y k   = eqCombine sym (bitEq  sym x y) k
   fw x y k   = eqCombine sym (wordEq sym x y) k
   fi x y k   = eqCombine sym (intEq  sym x y) k
   fz m x y k = eqCombine sym (znEq sym m x y) k
   fq x y k   = eqCombine sym (rationalEq sym x y) k
+  fr x y k   = eqCombine sym (realEq sym x y) k
   ff x y k   = eqCombine sym (fpEq sym x y) k
 
 {-# INLINE valLt #-}
 valLt :: Backend sym =>
   sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
-valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)
+valLt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq fr ff ty v1 v2 (pure final)
   where
   fb x y k   = lexCombine sym (bitLessThan  sym x y) (bitEq  sym x y) k
   fw x y k   = lexCombine sym (wordLessThan sym x y) (wordEq sym x y) k
   fi x y k   = lexCombine sym (intLessThan  sym x y) (intEq  sym x y) k
   fz _ _ _ _ = panic "valLt" ["Z_n is not in `Cmp`"]
   fq x y k   = lexCombine sym (rationalLessThan sym x y) (rationalEq sym x y) k
+  fr x y k   = lexCombine sym (realLessThan sym x y) (realEq sym x y) k
   ff x y k   = lexCombine sym (fpLessThan   sym x y) (fpEq   sym x y) k
 
 {-# INLINE valGt #-}
 valGt :: Backend sym =>
   sym -> TValue -> GenValue sym -> GenValue sym -> SBit sym -> SEval sym (SBit sym)
-valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure final)
+valGt sym ty v1 v2 final = cmpValue sym fb fw fi fz fq fr ff ty v1 v2 (pure final)
   where
   fb x y k   = lexCombine sym (bitGreaterThan  sym x y) (bitEq  sym x y) k
   fw x y k   = lexCombine sym (wordGreaterThan sym x y) (wordEq sym x y) k
   fi x y k   = lexCombine sym (intGreaterThan  sym x y) (intEq  sym x y) k
   fz _ _ _ _ = panic "valGt" ["Z_n is not in `Cmp`"]
   fq x y k   = lexCombine sym (rationalGreaterThan sym x y) (rationalEq sym x y) k
+  fr x y k   = lexCombine sym (realGreaterThan sym x y) (realEq sym x y) k
   ff x y k   = lexCombine sym (fpGreaterThan   sym x y) (fpEq   sym x y) k
 
 {-# INLINE eqCombine #-}
@@ -856,13 +896,14 @@ greaterThanEqV sym ty v1 v2 = VBit <$> valGt sym ty v1 v2 (bitLit sym True)
 
 {-# INLINE signedLessThanV #-}
 signedLessThanV :: Backend sym => sym -> Binary sym
-signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz fq ff ty v1 v2 (pure $ bitLit sym False)
+signedLessThanV sym ty v1 v2 = VBit <$> cmpValue sym fb fw fi fz fq fr ff ty v1 v2 (pure $ bitLit sym False)
   where
   fb _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on bit type"]
   fw x y k   = lexCombine sym (wordSignedLessThan sym x y) (wordEq sym x y) k
   fi _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Integer type"]
   fz m _ _ _ = panic "signedLessThan" ["Attempted to perform signed comparison on Z_" ++ show m ++ " type"]
   fq _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Rational type"]
+  fr _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Real type"]
   ff _ _ _   = panic "signedLessThan" ["Attempted to perform signed comparison on Float"]
 
 
@@ -894,6 +935,9 @@ zeroV sym ty = case ty of
   TVRational ->
     VRational <$> (intToRational sym =<< integerLit sym 0)
 
+  TVReal ->
+    VReal <$> realLit sym 0
+
   TVArray{} -> evalPanic "zeroV" ["Array not in class Zero"]
 
   -- floating point
@@ -1304,6 +1348,7 @@ logicBinary sym opb opw = loop
     TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]
     TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"]
     TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
+    TVReal     -> evalPanic "logicBinary" ["Real not in class Logic"]
     TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"]
 
     TVFloat {}  -> evalPanic "logicBinary" ["Float not in class Logic"]
@@ -1382,6 +1427,7 @@ logicUnary sym opb opw = loop
     TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"]
     TVFloat {} -> evalPanic "logicUnary" ["Float not in class Logic"]
     TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
+    TVReal     -> evalPanic "logicBinary" ["Real not in class Logic"]
     TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"]
 
     TVSeq w ety
@@ -1837,6 +1883,7 @@ errorV sym ty0 msg =
        TVInteger -> err stk
        TVIntMod _ -> err stk
        TVRational -> err stk
+       TVReal -> err stk
        TVArray{} -> err stk
        TVFloat {} -> err stk
 
@@ -1938,6 +1985,7 @@ mergeValue sym c v1 v2 =
     (VBit b1     , VBit b2     ) -> VBit <$> iteBit sym c b1 b2
     (VInteger i1 , VInteger i2 ) -> VInteger <$> iteInteger sym c i1 i2
     (VRational q1, VRational q2) -> VRational <$> iteRational sym c q1 q2
+    (VReal r1    , VReal r2)     -> VReal <$> iteReal sym c r1 r2
     (VWord n1 w1 , VWord n2 w2 ) | n1 == n2 -> pure $ VWord n1 $ mergeWord' sym c w1 w2
     (VSeq n1 vs1 , VSeq n2 vs2 ) | n1 == n2 -> VSeq n1 <$> memoMap sym (mergeSeqMap sym c vs1 vs2)
     (VStream vs1 , VStream vs2 ) -> VStream <$> memoMap sym (mergeSeqMap sym c vs1 vs2)
diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs
index ad6300f4c..7941260dd 100644
--- a/src/Cryptol/Eval/Reference.lhs
+++ b/src/Cryptol/Eval/Reference.lhs
@@ -78,6 +78,7 @@ are as follows:
 | `Integer`         | integers          | `TVInteger`                 |
 | `Z n`             | integers modulo n | `TVIntMod n`                |
 | `Rational`        | rationals         | `TVRational`                |
+| `Real`            | real numbers      | `TVReal`
 | `Float e p`       | floating point    | `TVFloat`                   |
 | `Array`           | arrays            | `TVArray`                   |
 | `[n]a`            | finite lists      | `TVSeq n a`                 |
@@ -167,6 +168,7 @@ terms by providing an evaluator to an appropriate `Value` type.
 >   = VBit !Bool                 -- ^ @ Bit    @ booleans
 >   | VInteger !Integer          -- ^ @ Integer @  or @Z n@ integers
 >   | VRational !Rational        -- ^ @ Rational @ rationals
+>   | VReal !Rational            -- ^ @ Real @ real numbers
 >   | VFloat !BF                 -- ^ Floating point numbers
 >   | VList Nat' [E Value]       -- ^ @ [n]a   @ finite or infinite lists
 >   | VTuple [E Value]           -- ^ @ ( .. ) @ tuples
@@ -193,6 +195,11 @@ Operations on Values
 > fromVRational (VRational i) = i
 > fromVRational _             = evalPanic "fromVRational" ["Expected a rational"]
 >
+> -- | Destructor for @VReal@.
+> fromVReal :: Value -> Rational
+> fromVReal (VReal i) = i
+> fromVReal _         = evalPanic "fromVReal" ["Expected a real"]
+>
 > fromVFloat :: Value -> BigFloat
 > fromVFloat = bfValue . fromVFloat'
 >
@@ -902,6 +909,7 @@ For functions, `zero` returns the constant function that returns
 > zero TVInteger      = VInteger 0
 > zero TVIntMod{}     = VInteger 0
 > zero TVRational     = VRational 0
+> zero TVReal         = VReal 0
 > zero (TVFloat e p)  = VFloat (fpToBF e p FP.bfPosZero)
 > zero TVArray{}      = evalPanic "zero" ["Array type not in `Zero`"]
 > zero (TVSeq n ety)  = VList (Nat n) (genericReplicate n (pure (zero ety)))
@@ -978,6 +986,7 @@ at the same positions.
 >         TVIntMod _   -> evalPanic "logicUnary" ["Z not in class Logic"]
 >         TVArray{}    -> evalPanic "logicUnary" ["Array not in class Logic"]
 >         TVRational   -> evalPanic "logicUnary" ["Rational not in class Logic"]
+>         TVReal       -> evalPanic "logicUnary" ["Real not in class Logic"]
 >         TVFloat{}    -> evalPanic "logicUnary" ["Float not in class Logic"]
 >         TVAbstract{} -> evalPanic "logicUnary" ["Abstract type not in `Logic`"]
 
@@ -1016,6 +1025,7 @@ at the same positions.
 >         TVIntMod _   -> evalPanic "logicBinary" ["Z not in class Logic"]
 >         TVArray{}    -> evalPanic "logicBinary" ["Array not in class Logic"]
 >         TVRational   -> evalPanic "logicBinary" ["Rational not in class Logic"]
+>         TVReal       -> evalPanic "logicBinary" ["Real not in class Logic"]
 >         TVFloat{}    -> evalPanic "logicBinary" ["Float not in class Logic"]
 >         TVAbstract{} -> evalPanic "logicBinary" ["Abstract type not in `Logic`"]
 
@@ -1048,6 +1058,8 @@ False]`, but to `error "foo"`.
 >           VInteger . flip mod n <$> i
 >         TVRational ->
 >           VRational <$> q
+>         TVReal ->
+>           VReal <$> q
 >         TVFloat e p ->
 >           VFloat . fpToBF e p <$> fl e p
 >         TVArray{} ->
@@ -1086,6 +1098,8 @@ False]`, but to `error "foo"`.
 >           VInteger <$> appOp1 (\i -> flip mod n <$> iop i) (fromVInteger <$> val)
 >         TVRational ->
 >           VRational <$> appOp1 qop (fromVRational <$> val)
+>         TVReal ->
+>           VReal <$> appOp1 qop (fromVReal <$> val)
 >         TVFloat e p ->
 >           VFloat . fpToBF e p <$> appOp1 (flop e p) (fromVFloat <$> val)
 >         TVSeq w a
@@ -1122,6 +1136,8 @@ False]`, but to `error "foo"`.
 >           VInteger <$> appOp2 (\i j -> flip mod n <$> iop i j) (fromVInteger <$> l) (fromVInteger <$> r)
 >         TVRational ->
 >           VRational <$> appOp2 qop (fromVRational <$> l) (fromVRational <$> r)
+>         TVReal ->
+>           VReal <$> appOp2 qop (fromVReal <$> l) (fromVReal <$> r)
 >         TVFloat e p ->
 >           VFloat . fpToBF e p <$>
 >             appOp2 (flop e p) (fromVFloat <$> l) (fromVFloat <$> r)
@@ -1212,6 +1228,7 @@ confused with integral division).
 >               TValue -> E Value -> E Value
 > fieldUnary qop zop flop ty v = case ty of
 >   TVRational  -> VRational <$> appOp1 qop (fromVRational <$> v)
+>   TVReal      -> VReal <$> appOp1 qop (fromVReal <$> v)
 >   TVIntMod m  -> VInteger <$> appOp1 (zop m) (fromVInteger <$> v)
 >   TVFloat e p -> VFloat . fpToBF e p <$> appOp1 (flop e p) (fromVFloat <$> v)
 >   _ -> evalPanic "fieldUnary" [show ty ++ " is not a Field type"]
@@ -1224,6 +1241,8 @@ confused with integral division).
 > fieldBinary qop zop flop ty l r = case ty of
 >   TVRational  -> VRational <$>
 >                    appOp2 qop (fromVRational <$> l) (fromVRational <$> r)
+>   TVReal      -> VReal <$>
+>                    appOp2 qop (fromVReal <$> l) (fromVReal <$> r)
 >   TVIntMod m  -> VInteger <$>
 >                    appOp2 (zop m) (fromVInteger <$> l) (fromVInteger <$> r)
 >   TVFloat e p -> VFloat . fpToBF e p <$>
@@ -1254,6 +1273,7 @@ Round
 >               TValue -> E Value -> E Value
 > roundUnary op flop ty v = case ty of
 >   TVRational -> VInteger . op . fromVRational <$> v
+>   TVReal     -> VInteger . op . fromVReal <$> v
 >   TVFloat {} -> VInteger <$> (flop . fromVFloat' =<< v)
 >   _ -> evalPanic "roundUnary" [show ty ++ " is not a Round type"]
 >
@@ -1306,6 +1326,8 @@ bits to the *left* of that position are equal.
 >       compare <$> (fromVInteger <$> l) <*> (fromVInteger <$> r)
 >     TVRational ->
 >       compare <$> (fromVRational <$> l) <*> (fromVRational <$> r)
+>     TVReal ->
+>       compare <$> (fromVReal <$> l) <*> (fromVReal <$> r)
 >     TVFloat{} ->
 >       compare <$> (fromVFloat <$> l) <*> (fromVFloat <$> r)
 >     TVArray{} ->
@@ -1357,6 +1379,8 @@ fields are compared in alphabetical order.
 >       evalPanic "lexSignedCompare" ["invalid type"]
 >     TVRational ->
 >       evalPanic "lexSignedCompare" ["invalid type"]
+>     TVReal ->
+>       evalPanic "lexSignedCompare" ["invalid type"]
 >     TVFloat{} ->
 >       evalPanic "lexSignedCompare" ["invalid type"]
 >     TVArray{} ->
@@ -1664,6 +1688,7 @@ Pretty Printing
 >     VBit b     -> text (show b)
 >     VInteger i -> text (show i)
 >     VRational q -> text (show q)
+>     VReal q -> text (show q)
 >     VFloat fl -> text (show (FP.fpPP opts fl))
 >     VList l vs ->
 >       case l of
diff --git a/src/Cryptol/Eval/Type.hs b/src/Cryptol/Eval/Type.hs
index 49fad0521..b5ab0128c 100644
--- a/src/Cryptol/Eval/Type.hs
+++ b/src/Cryptol/Eval/Type.hs
@@ -32,6 +32,7 @@ data TValue
   | TVFloat Integer Integer   -- ^ @ Float e p @
   | TVIntMod Integer          -- ^ @ Z n @
   | TVRational                -- ^ @Rational@
+  | TVReal                    -- ^ @Real@
   | TVArray TValue TValue     -- ^ @ Array a b @
   | TVSeq Integer TValue      -- ^ @ [n]a @
   | TVStream TValue           -- ^ @ [inf]t @
@@ -50,6 +51,7 @@ tValTy tv =
     TVFloat e p -> tFloat (tNum e) (tNum p)
     TVIntMod n  -> tIntMod (tNum n)
     TVRational  -> tRational
+    TVReal      -> tReal
     TVArray a b -> tArray (tValTy a) (tValTy b)
     TVSeq n t   -> tSeq (tNum n) (tValTy t)
     TVStream t  -> tSeq tInf (tValTy t)
@@ -109,6 +111,7 @@ evalType env ty =
         (TCBit, [])     -> Right $ TVBit
         (TCInteger, []) -> Right $ TVInteger
         (TCRational, []) -> Right $ TVRational
+        (TCReal, [])    -> Right $ TVReal
         (TCFloat, [e,p])-> Right $ TVFloat (inum e) (inum p)
         (TCIntMod, [n]) -> case num n of
                              Inf   -> evalPanic "evalType" ["invalid type Z inf"]
diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs
index a488034d5..bb0cb667a 100644
--- a/src/Cryptol/Eval/Value.hs
+++ b/src/Cryptol/Eval/Value.hs
@@ -45,6 +45,7 @@ module Cryptol.Eval.Value
   , fromVBit
   , fromVInteger
   , fromVRational
+  , fromVReal
   , fromVFloat
   , fromVSeq
   , fromSeq
@@ -95,6 +96,7 @@ import Data.Bits
 import Data.IORef
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
+import Data.Ratio
 import MonadLib
 
 import Cryptol.Backend
@@ -309,6 +311,7 @@ data GenValue sym
   | VBit !(SBit sym)                           -- ^ @ Bit    @
   | VInteger !(SInteger sym)                   -- ^ @ Integer @ or @ Z n @
   | VRational !(SRational sym)                 -- ^ @ Rational @
+  | VReal !(SReal sym)                         -- ^ @ Real @
   | VFloat !(SFloat sym)
   | VSeq !Integer !(SeqMap sym)                -- ^ @ [n]a   @
                                                --   Invariant: VSeq is never a sequence of bits
@@ -334,6 +337,7 @@ forceValue v = case v of
   VBit b      -> seq b (return ())
   VInteger i  -> seq i (return ())
   VRational q -> seq q (return ())
+  VReal r     -> seq r (return ())
   VFloat f    -> seq f (return ())
   VWord _ wv  -> forceWordValue =<< wv
   VStream _   -> return ()
@@ -350,6 +354,7 @@ instance Backend sym => Show (GenValue sym) where
     VBit _     -> "bit"
     VInteger _ -> "integer"
     VRational _ -> "rational"
+    VReal _    -> "real"
     VFloat _   -> "float"
     VSeq n _   -> "seq:" ++ show n
     VWord n _  -> "word:"  ++ show n
@@ -380,6 +385,14 @@ ppValue x opts = loop
     VBit b             -> return $ ppBit x b
     VInteger i         -> return $ ppInteger x opts i
     VRational q        -> return $ ppRational x opts q
+    VReal r
+      | Just q <- realAsLit x r ->
+          do n <- integerLit x (numerator q)
+             d <- integerLit x (denominator q)
+             let ppq = ppRational x opts (SRational n d)
+             pure (parens (text "fromRational" <+> ppq)) 
+      | otherwise -> return $ text "[?]"
+
     VFloat i           -> return $ ppFloat x opts i
     VSeq sz vals       -> ppWordSeq sz vals
     VWord _ wv         -> ppWordVal =<< wv
@@ -495,6 +508,11 @@ fromVRational val = case val of
   VRational q -> q
   _      -> evalPanic "fromVRational" ["not a Rational"]
 
+fromVReal :: GenValue sym -> SReal sym
+fromVReal val = case val of
+  VReal r -> r
+  _       -> evalPanic "fromVReal" ["not a Real"]
+
 -- | Extract a finite sequence value.
 fromVSeq :: GenValue sym -> SeqMap sym
 fromVSeq val = case val of
diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs
index 02a6afd43..3cb67e9c8 100644
--- a/src/Cryptol/Symbolic.hs
+++ b/src/Cryptol/Symbolic.hs
@@ -140,6 +140,7 @@ data FinType
     | FTInteger
     | FTIntMod Integer
     | FTRational
+    | FTReal
     | FTFloat Integer Integer
     | FTSeq Int FinType
     | FTTuple [FinType]
@@ -157,6 +158,7 @@ finType ty =
     TVInteger        -> Just FTInteger
     TVIntMod n       -> Just (FTIntMod n)
     TVRational       -> Just FTRational
+    TVReal           -> Just FTReal
     TVFloat e p      -> Just (FTFloat e p)
     TVSeq n t        -> FTSeq <$> numType n <*> finType t
     TVTuple ts       -> FTTuple <$> traverse finType ts
@@ -171,6 +173,7 @@ unFinType fty =
     FTInteger    -> tInteger
     FTIntMod n   -> tIntMod (tNum n)
     FTRational   -> tRational
+    FTReal       -> tReal
     FTFloat e p  -> tFloat (tNum e) (tNum p)
     FTSeq l ety  -> tSeq (tNum l) (unFinType ety)
     FTTuple ftys -> tTuple (unFinType <$> ftys)
@@ -181,6 +184,7 @@ data VarShape sym
   = VarBit (SBit sym)
   | VarInteger (SInteger sym)
   | VarRational (SInteger sym) (SInteger sym)
+  | VarReal (SReal sym)
   | VarFloat (SFloat sym)
   | VarWord (SWord sym)
   | VarFinSeq Integer [VarShape sym]
@@ -193,6 +197,7 @@ ppVarShape sym (VarInteger i) = ppInteger sym defaultPPOpts i
 ppVarShape sym (VarFloat f) = ppFloat sym defaultPPOpts f
 ppVarShape sym (VarRational n d) =
   text "(ratio" <+> ppInteger sym defaultPPOpts n <+> ppInteger sym defaultPPOpts d <+> text ")"
+ppVarShape _sym (VarReal _) = text "<<real>>"
 ppVarShape sym (VarWord w) = ppWord sym defaultPPOpts w
 ppVarShape sym (VarFinSeq _ xs) =
   brackets (fsep (punctuate comma (map (ppVarShape sym) xs)))
@@ -210,6 +215,7 @@ varShapeToValue sym var =
     VarBit b     -> VBit b
     VarInteger i -> VInteger i
     VarRational n d -> VRational (SRational n d)
+    VarReal r    -> VReal r
     VarWord w    -> VWord (wordLen sym w) (return (WordVal w))
     VarFloat f   -> VFloat f
     VarFinSeq n vs -> VSeq n (finiteSeqMap (map (pure . varShapeToValue sym) vs))
@@ -221,6 +227,7 @@ data FreshVarFns sym =
   { freshBitVar     :: IO (SBit sym)
   , freshWordVar    :: Integer -> IO (SWord sym)
   , freshIntegerVar :: Maybe Integer -> Maybe Integer -> IO (SInteger sym)
+  , freshRealVar    :: IO (SReal sym)
   , freshFloatVar   :: Integer -> Integer -> IO (SFloat sym)
   }
 
@@ -231,6 +238,7 @@ freshVar fns tp = case tp of
     FTRational    -> VarRational
                         <$> freshIntegerVar fns Nothing Nothing
                         <*> freshIntegerVar fns (Just 1) Nothing
+    FTReal        -> VarReal <$> freshRealVar fns
     FTIntMod 0    -> panic "freshVariable" ["0 modulus not allowed"]
     FTIntMod m    -> VarInteger  <$> freshIntegerVar fns (Just 0) (Just (m-1))
     FTFloat e p   -> VarFloat    <$> freshFloatVar fns e p
@@ -283,6 +291,9 @@ varModelPred sym vx =
          d' <- integerLit sym dlit
          rationalEq sym (SRational n d) (SRational n' d')
 
+    (VarReal r, VarReal rlit) ->
+      realEq sym r =<< realLit sym rlit
+
     (VarWord w, VarWord (Concrete.BV len wlit)) ->
       wordEq sym w =<< wordLit sym len wlit
 
@@ -328,6 +339,13 @@ varToExpr prims = go
             d' = ETApp (ETApp (prim "number") (tNum d)) tInteger
          in EApp (EApp (prim "ratio") n') d'
 
+      (FTReal, VarReal r) ->
+        EProofApp $ ePrim prims (prelPrim "fraction")
+                          `ETApp` tNum (numerator r)
+                          `ETApp` tNum (denominator r)
+                          `ETApp` tNum (0 :: Int)
+                          `ETApp` tReal
+
       (FTFloat e p, VarFloat f) ->
         floatToExpr prims e p (bfValue f)
 
diff --git a/src/Cryptol/Symbolic/SBV.hs b/src/Cryptol/Symbolic/SBV.hs
index 168a4c216..413d4eda6 100644
--- a/src/Cryptol/Symbolic/SBV.hs
+++ b/src/Cryptol/Symbolic/SBV.hs
@@ -492,6 +492,10 @@ parseValue FTInteger cvs =
     Just (x, cvs') -> (VarInteger x, cvs')
     Nothing        -> panic "Cryptol.Symbolic.parseValue" [ "no integer" ]
 parseValue (FTIntMod _) cvs = parseValue FTInteger cvs
+parseValue FTReal cvs =
+  case cvs of
+    (SBV.CV SBV.KReal cv : cvs') -> error "parseValue SBV Real!"
+    _ -> panic "Cryptol.Symbolic.parseValue" [ "no real" ]
 parseValue FTRational cvs =
   fromMaybe (panic "Cryptol.Symbolic.parseValue" ["no rational"]) $
   do (n,cvs')  <- SBV.genParse SBV.KUnbounded cvs
@@ -539,5 +543,6 @@ sbvFreshFns sym =
   { freshBitVar     = freshSBool_ sym
   , freshWordVar    = freshBV_ sym . fromInteger
   , freshIntegerVar = freshBoundedInt sym
+  , freshRealVar    = freshSReal_ sym
   , freshFloatVar   = \_ _ -> return () -- TODO
   }
diff --git a/src/Cryptol/Symbolic/What4.hs b/src/Cryptol/Symbolic/What4.hs
index b53a8af46..22314b0b6 100644
--- a/src/Cryptol/Symbolic/What4.hs
+++ b/src/Cryptol/Symbolic/What4.hs
@@ -223,6 +223,7 @@ what4FreshFns sym =
   { freshBitVar     = W4.freshConstant sym W4.emptySymbol W4.BaseBoolRepr
   , freshWordVar    = SW.freshBV sym W4.emptySymbol
   , freshIntegerVar = W4.freshBoundedInt sym W4.emptySymbol
+  , freshRealVar    = W4.freshConstant sym W4.emptySymbol W4.BaseRealRepr
   , freshFloatVar   = W4.fpFresh sym
   }
 
@@ -544,6 +545,7 @@ varShapeToConcrete evalFn v =
     VarBit b -> VarBit <$> W4.groundEval evalFn b
     VarInteger i -> VarInteger <$> W4.groundEval evalFn i
     VarRational n d -> VarRational <$> W4.groundEval evalFn n <*> W4.groundEval evalFn d
+    VarReal r -> VarReal <$> W4.groundEval evalFn r
     VarWord SW.ZBV -> pure (VarWord (Concrete.mkBv 0 0))
     VarWord (SW.DBV x) ->
       let w = W4.intValue (W4.bvWidth x)
diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs
index 9b5a2926e..442a69769 100644
--- a/src/Cryptol/Testing/Random.hs
+++ b/src/Cryptol/Testing/Random.hs
@@ -134,6 +134,7 @@ randomValue sym ty =
     TVBit         -> Just (randomBit sym)
     TVInteger     -> Just (randomInteger sym)
     TVRational    -> Just (randomRational sym)
+    TVReal        -> Just (randomReal sym)
     TVIntMod m    -> Just (randomIntMod sym m)
     TVFloat e p   -> Just (randomFloat sym e p)
     TVSeq n TVBit -> Just (randomWord sym n)
@@ -200,6 +201,9 @@ randomRational sym w g =
           pure (VRational (SRational n' d'))
        , g3)
 
+randomReal :: (Backend sym, RandomGen g) => sym -> Gen g sym
+randomReal = error "TODO randomReal"
+
 {-# INLINE randomWord #-}
 
 -- | Generate a random word of the given length (i.e., a value of type @[w]@)
@@ -351,6 +355,7 @@ typeSize ty = case ty of
   TVBit -> Just 2
   TVInteger -> Nothing
   TVRational -> Nothing
+  TVReal -> Nothing
   TVIntMod n -> Just n
   TVFloat{} -> Nothing -- TODO?
   TVArray{} -> Nothing
@@ -369,6 +374,7 @@ typeValues ty =
     TVBit      -> [ VBit False, VBit True ]
     TVInteger  -> []
     TVRational -> []
+    TVReal     -> []
     TVIntMod n -> [ VInteger x | x <- [ 0 .. (n-1) ] ]
     TVFloat{}  -> [] -- TODO?
     TVArray{}  -> []
diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs
index 87bd879eb..38d5e9e7c 100644
--- a/src/Cryptol/TypeCheck/Solver/Class.hs
+++ b/src/Cryptol/TypeCheck/Solver/Class.hs
@@ -79,11 +79,12 @@ solveZeroInst ty = case tNoUser ty of
   -- Zero (Z n)
   TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne ]
 
-  -- Zero Real
-
   -- Zero Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Zero Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- ValidVloat e p => Zero (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
@@ -120,6 +121,9 @@ solveLogicInst ty = case tNoUser ty of
   -- Logic Rational fails
   TCon (TC TCRational) [] -> Unsolvable
 
+  -- Logic Real fails
+  TCon (TC TCReal) [] -> Unsolvable
+
   -- Logic (Float e p) fails
   TCon (TC TCFloat) [_, _] -> Unsolvable
 
@@ -166,6 +170,9 @@ solveRingInst ty = case tNoUser ty of
   -- Ring Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Ring Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- ValidFloat e p => Ring (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
@@ -236,6 +243,9 @@ solveFieldInst ty = case tNoUser ty of
   -- Field Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Field Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- ValidFloat e p => Field (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
@@ -278,6 +288,9 @@ solveRoundInst ty = case tNoUser ty of
   -- Round Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Round Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- ValidFloat e p => Round (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
@@ -315,6 +328,9 @@ solveEqInst ty = case tNoUser ty of
   -- Eq Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Eq Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- ValidFloat e p => Eq (Float e p)
   TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ]
 
@@ -352,6 +368,9 @@ solveCmpInst ty = case tNoUser ty of
   -- Cmp Rational
   TCon (TC TCRational) [] -> SolvedIf []
 
+  -- Cmp Real
+  TCon (TC TCReal) [] -> SolvedIf []
+
   -- Cmp (Z n) fails
   TCon (TC TCIntMod) [_] -> Unsolvable
 
@@ -407,6 +426,9 @@ solveSignedCmpInst ty = case tNoUser ty of
   -- SignedCmp Rational fails
   TCon (TC TCRational) [] -> Unsolvable
 
+  -- SignedCmp Real fails
+  TCon (TC TCReal) [] -> Unsolvable
+
   -- SignedCmp (Float e p) fails
   TCon (TC TCFloat) [_, _] -> Unsolvable
 
@@ -442,6 +464,9 @@ solveFLiteralInst numT denT rndT ty
       TCon (TC TCRational) [] ->
         SolvedIf [ pFin numT, pFin denT, denT >== tOne ]
 
+      TCon (TC TCReal) [] ->
+        SolvedIf [ pFin numT, pFin denT, denT >== tOne ]
+
       TCon (TC TCFloat) [e,p]
         | Just 0    <- tIsNum rndT ->
           SolvedIf [ pValidFloat e p
@@ -478,6 +503,9 @@ solveLiteralInst val ty
       -- (fin val) => Literal val Rational
       TCon (TC TCRational) [] -> SolvedIf [ pFin val ]
 
+      -- (fin val) => Literal val Real
+      TCon (TC TCReal) [] -> SolvedIf [ pFin val ]
+
       -- ValidFloat e p => Literal val (Float e p)   if `val` is representable
       TCon (TC TCFloat) [e,p]
         | Just n    <- tIsNum val
diff --git a/src/Cryptol/TypeCheck/TCon.hs b/src/Cryptol/TypeCheck/TCon.hs
index 654286036..8582c2ffe 100644
--- a/src/Cryptol/TypeCheck/TCon.hs
+++ b/src/Cryptol/TypeCheck/TCon.hs
@@ -62,6 +62,7 @@ builtInType nm =
     , "Bit"               ~> TC TCBit
     , "Integer"           ~> TC TCInteger
     , "Rational"          ~> TC TCRational
+    , "Real"              ~> TC TCReal
     , "Z"                 ~> TC TCIntMod
 
       -- Predicate contstructors
@@ -136,6 +137,7 @@ instance HasKind TC where
       TCBit     -> KType
       TCInteger -> KType
       TCRational -> KType
+      TCReal    -> KType
       TCFloat   -> KNum :-> KNum :-> KType
       TCIntMod  -> KNum :-> KType
       TCArray   -> KType :-> KType :-> KType
@@ -232,6 +234,7 @@ data TC     = TCNum Integer            -- ^ Numbers
             | TCFloat                  -- ^ Float
             | TCIntMod                 -- ^ @Z _@
             | TCRational               -- ^ @Rational@
+            | TCReal                   -- ^ @Real@
             | TCArray                  -- ^ @Array _ _@
             | TCSeq                    -- ^ @[_] _@
             | TCFun                    -- ^ @_ -> _@
@@ -330,6 +333,7 @@ instance PP TC where
       TCInteger -> text "Integer"
       TCIntMod  -> text "Z"
       TCRational -> text "Rational"
+      TCReal    -> text "Real"
       TCArray   -> text "Array"
       TCFloat   -> text "Float"
       TCSeq     -> text "[]"
diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs
index 4c664f226..8890fecd6 100644
--- a/src/Cryptol/TypeCheck/Type.hs
+++ b/src/Cryptol/TypeCheck/Type.hs
@@ -439,6 +439,12 @@ tIsRational ty =
     TCon (TC TCRational) [] -> True
     _                       -> False
 
+tIsReal :: Type -> Bool
+tIsReal ty =
+  case tNoUser ty of
+    TCon (TC TCReal) [] -> True
+    _                   -> False
+
 tIsFloat :: Type -> Maybe (Type, Type)
 tIsFloat ty =
   case tNoUser ty of
@@ -593,6 +599,9 @@ tInteger  = TCon (TC TCInteger) []
 tRational :: Type
 tRational  = TCon (TC TCRational) []
 
+tReal :: Type
+tReal = TCon (TC TCReal) []
+
 tFloat   :: Type -> Type -> Type
 tFloat e p = TCon (TC TCFloat) [ e, p ]
 
@@ -939,6 +948,7 @@ instance PP (WithNames Type) where
           (TCBit,   [])       -> text "Bit"
           (TCInteger, [])     -> text "Integer"
           (TCRational, [])    -> text "Rational"
+          (TCReal, [])        -> text "Real"
 
           (TCIntMod, [n])     -> optParens (prec > 3) $ text "Z" <+> go 5 n