Add primitives toZ and fromZ for converting integers to/from Z n.

lib/Cryptol.cry

@@ -297,6 +297,16 @@ primitive toInteger : {a} (fin a) => [a] -> Integer
  */
 primitive fromInteger : {a} (fin a) => Integer -> [a]
 
+/**
+ * Converts an unbounded integer to an integer modulo n.
+ */
+primitive toZ : {n} (fin n, n >= 1) => Integer -> Z n
+
+/**
+ * Converts an integer modulo n to an unbounded integer in the range 0 to n-1.
+ */
+primitive fromZ : {n} (fin n, n >= 1) => Z n -> Integer
+
 /**
  * Left shift.  The first argument is the sequence to shift, the second is the
  * number of positions to shift by.

src/Cryptol/Prims/Eval.hs

@@ -113,6 +113,16 @@ primTable = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
                     unary  (logicUnary complement (unaryBV complement)))
   , ("toInteger"  , ecToIntegerV)
   , ("fromInteger", ecFromIntegerV)
+  , ("toZ"        , {-# SCC "Prelude::toZ" #-}
+                    nlam $ \ modulus ->
+                    lam  $ \ x -> do
+                      val <- x
+                      case (modulus, val) of
+                        (Nat n, VInteger i) -> return $ VInteger (i `mod` n)
+                        _                   -> evalPanic "toZ" ["Invalid arguments"])
+  , ("fromZ"      , {-# SCC "Prelude::fromZ" #-}
+                    nlam $ \ _modulus ->
+                    lam  $ \ x -> x)
   , ("<<"         , {-# SCC "Prelude::(<<)" #-}
                     logicShift shiftLW shiftLB shiftLS)
   , (">>"         , {-# SCC "Prelude::(>>)" #-}

src/Cryptol/Symbolic/Prims.hs

@@ -119,6 +119,14 @@ primTable  = Map.fromList $ map (\(n, v) -> (mkIdent (T.pack n), v))
   , ("zero"        , tlam zeroV)
   , ("toInteger"   , ecToIntegerV)
   , ("fromInteger" , ecFromIntegerV)
+  , ("toZ"        , nlam $ \ _modulus ->
+                    lam  $ \ x -> x)
+  , ("fromZ"      , nlam $ \ modulus ->
+                    lam  $ \ x -> do
+                      val <- x
+                      case (modulus, val) of
+                        (Nat n, VInteger i) -> return $ VInteger (SBV.svRem i (integerLit n))
+                        _                   -> evalPanic "fromZ" ["Invalid arguments"])
   , ("<<"          , logicShift "<<"
                        SBV.svShiftLeft
                        (\sz i shft ->