remove Z n types from class Integral

lib/Cryptol.cry

@@ -608,8 +608,7 @@ primitive ratio : Integer -> Integer -> Rational
 /**
  * Converts an integer modulo n to an unbounded integer in the range 0 to n-1.
  */
-fromZ : {n} (fin n, n >= 1) => Z n -> Integer
-fromZ = toInteger
+primitive fromZ : {n} (fin n, n >= 1) => Z n -> Integer
 
 
 // Sequence operations -------------------------------------------------------

src/Cryptol/Eval/Backend.hs

@@ -631,44 +631,6 @@ class MonadIO (SEval sym) => Backend sym where
 
   -- ==== Z_n operations defined via projection to the integers ====
 
-  -- | Division of integers modulo n, for a concrete positive integer n.
-  --   NOTE: this is integer division on the initial segement of Z,
-  --   and not the multiplicative inverse in Z_p.
-  znDiv ::
-    sym ->
-    Integer {- ^ modulus -} ->
-    SInteger sym ->
-    SInteger sym ->
-    SEval sym (SInteger sym)
-  znDiv sym m x y =
-    do x' <- znToInt sym m x
-       y' <- znToInt sym m y
-       intToZn sym m =<< intDiv sym x' y'
-
-  -- | Modulus of integers modulo n, for a concrete positive integer n.
-  --   NOTE: this is the modulus corresponding to integer division on the initial
-  --   segement of Z, and not related to multiplicative inverse in Z_p.
-  znMod ::
-    sym ->
-    Integer {- ^ modulus -} ->
-    SInteger sym ->
-    SInteger sym ->
-    SEval sym (SInteger sym)
-  znMod sym m x y =
-    do x' <- znToInt sym m x
-       y' <- znToInt sym m y
-       intToZn sym m =<< intMod sym x' y'
-
-  -- | Log base 2 of integers modulo n.
-  znLg2 ::
-    sym ->
-    Integer {- ^ modulus -} ->
-    SInteger sym ->
-    SEval sym (SInteger sym)
-  znLg2 sym m x =
-    do x' <- znToInt sym m x
-       intToZn sym m =<< intLg2 sym x'
-
   -- | Less-than test of integers modulo n.  Note this test
   --   first computes the reduced integers and compares.
   znLessThan ::

src/Cryptol/Eval/Concrete.hs

@@ -267,6 +267,9 @@ primTable = let sym = Concrete in
                     updatePrim sym updateBack_word updateBack)
 
     -- Misc
+  , ("fromZ"      , {-# SCC "Prelice::fromZ" #-}
+                    fromZV sym)
+
   , ("error"      , {-# SCC "Prelude::error" #-}
                       tlam $ \a ->
                       nlam $ \_ ->

src/Cryptol/Eval/Generic.hs

@@ -20,6 +20,8 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Cryptol.Eval.Generic where
 
+import qualified Control.Exception as X
+import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad (join, unless)
 
 import Data.Bits (testBit)
@@ -87,6 +89,12 @@ ratioV sym =
        y' <- fromVInteger <$> y
        VRational <$> ratio sym x' y'
 
+{-# SPECIALIZE fromZV :: Concrete -> GenValue Concrete #-}
+fromZV :: Backend sym => sym -> GenValue sym
+fromZV sym =
+  nlam $ \(finNat' -> n) ->
+  lam $ \v -> VInteger <$> (znToInt sym n . fromVInteger =<< v)
+
 -- Operation Lifting -----------------------------------------------------------
 
 
@@ -320,7 +328,6 @@ ringNullary sym opw opi opz opq = loop
 
 {-# SPECIALIZE integralBinary :: Concrete -> BinWord Concrete ->
       (SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
-      (Integer -> SInteger Concrete -> SInteger Concrete -> SEval Concrete (SInteger Concrete)) ->
       Binary Concrete
   #-}
 
@@ -329,15 +336,11 @@ integralBinary :: forall sym.
   sym ->
   BinWord sym ->
   (SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
-  (Integer -> SInteger sym -> SInteger sym -> SEval sym (SInteger sym)) ->
   Binary sym
-integralBinary sym opw opi opz ty l r = case ty of
+integralBinary sym opw opi ty l r = case ty of
     TVInteger ->
       VInteger <$> opi (fromVInteger l) (fromVInteger r)
 
-    TVIntMod n ->
-      VInteger <$> opz n (fromVInteger l) (fromVInteger r)
-
     -- bitvectors
     TVSeq w a
       | isTBit a ->
@@ -402,19 +405,17 @@ mulV sym = ringBinary sym opw opi opz opq
 
 {-# INLINE divV #-}
 divV :: Backend sym => sym -> Binary sym
-divV sym = integralBinary sym opw opi opz
+divV sym = integralBinary sym opw opi
   where
     opw _w x y = wordDiv sym x y
     opi x y = intDiv sym x y
-    opz m x y = znDiv sym m x y
 
 {-# INLINE modV #-}
 modV :: Backend sym => sym -> Binary sym
-modV sym = integralBinary sym opw opi opz
+modV sym = integralBinary sym opw opi
   where
     opw _w x y = wordMod sym x y
     opi x y = intMod sym x y
-    opz m x y = znMod sym m x y
 
 {-# SPECIALIZE toIntegerV :: Concrete -> GenValue Concrete #-}
 -- | Convert a word to a non-negative integer.
@@ -425,8 +426,6 @@ toIntegerV sym =
     case a of
       TVSeq _w el | isTBit el ->
         VInteger <$> (wordToInt sym =<< (fromVWord sym "toInteger" =<< v))
-      TVIntMod m ->
-        VInteger <$> (znToInt sym m . fromVInteger =<< v)
       TVInteger -> v
       _ -> evalPanic "toInteger" [show a ++ " not in class `Integral`"]
 
@@ -1480,10 +1479,8 @@ enumerateIntBits :: Backend sym =>
   TValue ->
   SInteger sym ->
   SEval sym [SBit sym]
-enumerateIntBits sym (Nat n) (TVIntMod m) idx = enumerateIntBits' sym (min n m) idx
-enumerateIntBits sym Inf (TVIntMod m) idx = enumerateIntBits' sym m idx
 enumerateIntBits sym (Nat n) _ idx = enumerateIntBits' sym n idx
-enumerateIntBits sym Inf _ _ = raiseError sym (UnsupportedSymbolicOp "unbounded integer shifting")
+enumerateIntBits _sym Inf _ _ = liftIO (X.throw (UnsupportedSymbolicOp "unbounded integer shifting"))
 
 -- | Compute the list of bits in an integer in big-endian order.
 --   The integer argument is a concrete upper bound for
@@ -1572,7 +1569,6 @@ logicShift sym nm shrinkRange wop reindex =
 
 shiftShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
 shiftShrink _sym Inf _ x = return x
-shiftShrink _sym (Nat w) (TVIntMod m) x | m <= w = return x
 shiftShrink sym (Nat w) _ x =
   do w' <- integerLit sym w
      p  <- intLessThan sym w' x
@@ -1580,7 +1576,6 @@ shiftShrink sym (Nat w) _ x =
 
 rotateShrink :: Backend sym => sym -> Nat' -> TValue -> SInteger sym -> SEval sym (SInteger sym)
 rotateShrink _sym Inf _ _ = panic "rotateShrink" ["expected finite sequence in rotate"]
-rotateShrink _sym (Nat w) (TVIntMod m) x | m <= w = return x
 rotateShrink sym (Nat 0) _ _ = integerLit sym 0
 rotateShrink sym (Nat w) _ x =
   do w' <- integerLit sym w

src/Cryptol/Eval/SBV.hs

@@ -464,6 +464,8 @@ primTable  = let sym = SBV in
 
     -- Misc
 
+  , ("fromZ"       , fromZV sym)
+
     -- {at,len} (fin len) => [len][8] -> at
   , ("error"       ,
       tlam $ \a ->

src/Cryptol/Eval/Value.hs

@@ -493,7 +493,6 @@ fromWordVal msg _ = evalPanic "fromWordVal" ["not a word value", msg]
 asIndex :: Backend sym =>
   sym -> String -> TValue -> GenValue sym -> SEval sym (Either (SInteger sym) (WordValue sym))
 asIndex _sym _msg TVInteger (VInteger i) = pure (Left i)
-asIndex  sym _msg (TVIntMod m) (VInteger i) = Left <$> znToInt sym m i
 asIndex _sym _msg _ (VWord _ wval) = Right <$> wval
 asIndex _sym  msg _ _ = evalPanic "asIndex" ["not an index value", msg]
 

src/Cryptol/Eval/What4.hs

@@ -508,6 +508,8 @@ primTable w4sym = let sym = What4 w4sym in
 
     -- Misc
 
+  , ("fromZ"       , fromZV sym)
+
     -- {at,len} (fin len) => [len][8] -> at
   , ("error"       ,
       tlam $ \a ->

src/Cryptol/Prelude.hs

@@ -25,3 +25,4 @@ preludeContents = B.pack [there|lib/Cryptol.cry|]
 
 cryptolTcContents :: String
 cryptolTcContents = [there|lib/CryptolTC.z3|]
+

src/Cryptol/TypeCheck/Solver/Class.hs

@@ -157,9 +157,6 @@ solveIntegralInst ty = case tNoUser ty of
   -- Integral Integer
   TCon (TC TCInteger) [] -> SolvedIf []
 
-  -- Integral (Z n)
-  TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne ]
-
   -- fin n => Integral [n]
   TCon (TC TCSeq) [n, elTy] ->
     case tNoUser elTy of