Reimplement (^^) as a primitive taking the exponent in class Integral

lib/Cryptol.cry

@@ -291,6 +291,12 @@ primitive (%) : {a} (Integral a) => a -> a -> a
  */
 primitive toInteger : {a} (Integral a) => a -> Integer
 
+/**
+ * Compute the exponentiation of a value in a ring.
+ * The exponent is treated as an unsigned bitvector value.
+ */
+primitive (^^) : {a, e} (Ring a, Integral e) => a -> e -> a
+
 /**
  * An infinite sequence counting up from the given starting value.
  * '[x...]' is syntactic sugar for 'infFrom x'.
@@ -577,15 +583,6 @@ sext x = newbits # x
  */
 primitive (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
 
-/**
- * Compute the exponentiation of a value in a ring.
- * The exponent is treated as an unsigned bitvector value.
- */
-(^^) : {a, n} (Ring a, fin n) => a -> [n] -> a
-a ^^ e = foldl squareAndMult (fromInteger 1) e
- where
- squareAndMult x b = if b then a*x*x else x*x
-
 /**
  * Log base two.
  *

src/Cryptol/Eval/Concrete.hs

@@ -152,6 +152,8 @@ primTable = let sym = Concrete in
                     binary (divV sym))
   , ("%"          , {-# SCC "Prelude::(%)" #-}
                     binary (modV sym))
+  , ("^^"         , {-# SCC "Prelude::(^^)" #-}
+                    expV sym)
   , ("infFrom"    , {-# SCC "Prelude::infFrom" #-}
                     infFromV sym)
   , ("infFromThen", {-# SCC "Prelude::infFromThen" #-}

src/Cryptol/Eval/Generic.hs

@@ -410,6 +410,58 @@ divV sym = integralBinary sym opw opi
     opw _w x y = wordDiv sym x y
     opi x y = intDiv sym x y
 
+{-# SPECIALIZE expV :: Concrete -> GenValue Concrete #-}
+expV :: Backend sym => sym -> GenValue sym
+expV sym =
+  tlam $ \aty ->
+  tlam $ \ety ->
+   lam $ \am -> return $
+   lam $ \em ->
+     do a <- am
+        e <- em
+        case ety of
+          TVInteger ->
+            let ei = fromVInteger e in
+            case integerAsLit sym ei of
+              Just n
+                | n == 0 ->
+                   do onei <- integerLit sym 1
+                      intV sym onei aty
+
+                | n > 0 ->
+                    do ebits <- enumerateIntBits' sym n ei
+                       computeExponent sym aty a ebits
+
+                | otherwise -> raiseError sym NegativeExponent
+
+              Nothing -> liftIO (X.throw (UnsupportedSymbolicOp "integer exponentiation"))
+
+          TVSeq _w el | isTBit el ->
+            do ebits <- enumerateWordValue sym =<< fromWordVal "(^^)" e
+               computeExponent sym aty a ebits
+
+          _ -> evalPanic "expV" [show ety ++ " not int class `Integral`"]
+
+
+{-# SPECIALIZE computeExponent ::
+      Concrete -> TValue -> GenValue Concrete -> [SBit Concrete] -> SEval Concrete (GenValue Concrete)
+  #-}
+computeExponent :: Backend sym =>
+  sym -> TValue -> GenValue sym -> [SBit sym] -> SEval sym (GenValue sym)
+computeExponent sym aty a bs0 =
+  do onei <- integerLit sym 1
+     one <- intV sym onei aty
+     loop one bs0
+
+ where
+ loop acc [] = return acc
+ loop acc (b:bs) =
+   do sq <- mulV sym aty acc acc
+      acc' <- iteValue sym b
+                (mulV sym aty a sq)
+                (pure sq)
+      loop acc' bs
+
 {-# INLINE modV #-}
 modV :: Backend sym => sym -> Binary sym
 modV sym = integralBinary sym opw opi

src/Cryptol/Eval/SBV.hs

@@ -366,6 +366,7 @@ primTable  = let sym = SBV in
   , ("toInteger"   , toIntegerV sym)
   , ("/"           , binary (divV sym))
   , ("%"           , binary (modV sym))
+  , ("^^"          , expV sym)
   , ("infFrom"     , infFromV sym)
   , ("infFromThen" , infFromThenV sym)
 

src/Cryptol/Eval/What4.hs

@@ -422,6 +422,7 @@ primTable w4sym = let sym = What4 w4sym in
   , ("toInteger"   , toIntegerV sym)
   , ("/"           , binary (divV sym))
   , ("%"           , binary (modV sym))
+  , ("^^"          , expV sym)
   , ("infFrom"     , infFromV sym)
   , ("infFromThen" , infFromThenV sym)