First cut at adding real numbers to Cryptol

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 ----------------------------------------------------
 
 /**

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 ====
 

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
 

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
 

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

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