[plinth][plc][api][agda] Draft of modExpInteger builtin (#6348)

[agda] Added builtin expModInteger

Co-authored-by: Nikolaos Bezirgiannis <bezirg@users.noreply.github.com>

plutus-benchmark/bitwise/src/PlutusBenchmark/Ed25519.hs

@@ -101,7 +101,7 @@ xRecover y =
     xx :: Integer
     xx = (y * y - 1) * inv (d * y * y + 1)
     x :: Integer
-    x = expMod xx ((q + 3) `divide` 8) q
+    x = expModManual xx ((q + 3) `divide` 8) q
     xA :: Integer
     xA = x * i `modulo` q
     xB :: Integer
@@ -113,27 +113,28 @@ xRecover y =
     cond2 :: Bool
     cond2 = if cond1 then odd xA else odd x
     i :: Integer
-    i = expMod 2 ((q - 1) `divide` 4) q
+    i = expModManual 2 ((q - 1) `divide` 4) q
 
 {-# INLINEABLE clearBit #-}
 clearBit :: Integer -> BuiltinByteString -> BuiltinByteString
 clearBit ix bs = writeBits bs [ix] [False]
 
 {-# INLINEABLE inv #-}
 inv :: Integer -> Integer
-inv x = expMod x (q - 2) q
+inv x = expModManual x (q - 2) q
 
 {-# INLINEABLE d #-}
 d :: Integer
 d = (-121665) * inv 121666
 
-{-# INLINEABLE expMod #-}
-expMod :: Integer -> Integer -> Integer -> Integer
-expMod b' e m =
+{-# INLINEABLE expModManual #-}
+-- TODO: switch to the builtin `expMod` (aka ExpModInteger)?
+expModManual :: Integer -> Integer -> Integer -> Integer
+expModManual b' e m =
   if e == 0
     then 1
     else
-      let reduced = expMod b' (e `divide` 2) m
+      let reduced = expModManual b' (e `divide` 2) m
           t = (reduced * reduced) `modulo` m
        in if odd e
             then (t * b') `modulo` m

plutus-benchmark/bitwise/test/9.6/Ed25519.pir.golden

@@ -52,15 +52,15 @@
           ifThenElse {Bool} (equalsInteger 0 (modInteger n 2)) True False
   in
   letrec
-    !expMod : integer -> integer -> integer -> integer
+    !expModManual : integer -> integer -> integer -> integer
       = \(b' : integer) (e : integer) (m : integer) ->
           Bool_match
             (ifThenElse {Bool} (equalsInteger 0 e) True False)
             {all dead. integer}
             (/\dead -> 1)
             (/\dead ->
                let
-                 !reduced : integer = expMod b' (divideInteger e 2) m
+                 !reduced : integer = expModManual b' (divideInteger e 2) m
                  !t : integer = modInteger (multiplyInteger reduced reduced) m
                in
                Bool_match
@@ -76,7 +76,7 @@
        integer
       = multiplyInteger
           -121665
-          (expMod
+          (expModManual
              121666
              57896044618658097711785492504343953926634992332820282019728792003956564819947
              57896044618658097711785492504343953926634992332820282019728792003956564819949)
@@ -86,21 +86,21 @@
           let
             !i :
                integer
-              = expMod
+              = expModManual
                   2
                   14474011154664524427946373126085988481658748083205070504932198000989141204987
                   57896044618658097711785492504343953926634992332820282019728792003956564819949
             !xx :
                integer
               = multiplyInteger
                   (subtractInteger (multiplyInteger y y) 1)
-                  (expMod
+                  (expModManual
                      (addInteger 1 (multiplyInteger (multiplyInteger d y) y))
                      57896044618658097711785492504343953926634992332820282019728792003956564819947
                      57896044618658097711785492504343953926634992332820282019728792003956564819949)
             !x :
                integer
-              = expMod
+              = expModManual
                   xx
                   7237005577332262213973186563042994240829374041602535252466099000494570602494
                   57896044618658097711785492504343953926634992332820282019728792003956564819949
@@ -431,7 +431,7 @@
                             (addInteger
                                (multiplyInteger y y)
                                (multiplyInteger x x))
-                            (expMod
+                            (expModManual
                                (subtractInteger
                                   1
                                   (multiplyInteger
@@ -452,7 +452,7 @@
                             (addInteger
                                (multiplyInteger x y)
                                (multiplyInteger x y))
-                            (expMod
+                            (expModManual
                                (addInteger
                                   1
                                   (multiplyInteger
@@ -575,7 +575,7 @@
          integer
         = multiplyInteger
             4
-            (expMod
+            (expModManual
                5
                57896044618658097711785492504343953926634992332820282019728792003956564819947
                57896044618658097711785492504343953926634992332820282019728792003956564819949)

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/exp-neg-non-inverse1/exp-neg-non-inverse1.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ [ (builtin expModInteger) (con integer 2)] (con integer -3) ] (con integer -4)])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/exp-neg-non-inverse1/exp-neg-non-inverse1.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/exp-neg-non-inverse1/exp-neg-non-inverse1.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/exp-neg-non-inverse2/exp-neg-non-inverse2.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ [ (builtin expModInteger) (con integer 500)] (con integer -5) ] (con integer 5)])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/exp-neg-non-inverse2/exp-neg-non-inverse2.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/exp-neg-non-inverse2/exp-neg-non-inverse2.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod1/expMod1.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ [ (builtin expModInteger) (con integer 500)] (con integer 0) ] (con integer 500)])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod1/expMod1.uplc.budget.expected

@@ -0,0 +1,2 @@
+({cpu: 100000112100
+| mem: 100000000800})

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod1/expMod1.uplc.expected

@@ -0,0 +1 @@
+(program 1.0.0 (con integer 1))

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod2/expMod2.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ [ (builtin expModInteger) (con integer 500)] (con integer 5) ] (con integer 500)])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod2/expMod2.uplc.budget.expected

@@ -0,0 +1,2 @@
+({cpu: 100000112100
+| mem: 100000000800})

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod2/expMod2.uplc.expected

@@ -0,0 +1 @@
+(program 1.0.0 (con integer 0))

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod3/expMod3.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ [ (builtin expModInteger) (con integer 1)] (con integer -3) ] (con integer 4)])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod3/expMod3.uplc.budget.expected

@@ -0,0 +1,2 @@
+({cpu: 100000112100
+| mem: 100000000800})

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod3/expMod3.uplc.expected

@@ -0,0 +1 @@
+(program 1.0.0 (con integer 1))

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod4/expMod4.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ [ (builtin expModInteger) (con integer 2)] (con integer -3) ] (con integer 3)])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod4/expMod4.uplc.budget.expected

@@ -0,0 +1,2 @@
+({cpu: 100000112100
+| mem: 100000000800})

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod4/expMod4.uplc.expected

@@ -0,0 +1 @@
+(program 1.0.0 (con integer 2))

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod5/expMod5.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ [ (builtin expModInteger) (con integer 4)] (con integer -5) ] (con integer 9)])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod5/expMod5.uplc.budget.expected

@@ -0,0 +1,2 @@
+({cpu: 100000112100
+| mem: 100000000800})

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/expMod5/expMod5.uplc.expected

@@ -0,0 +1 @@
+(program 1.0.0 (con integer 4))

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/mod-neg/mod-neg.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ [ (builtin expModInteger) (con integer 1)] (con integer 1) ] (con integer -3)])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/mod-neg/mod-neg.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/mod-neg/mod-neg.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/mod-zero/mod-zero.uplc

@@ -0,0 +1 @@
+(program 1.0.0 [ [ [ (builtin expModInteger) (con integer 1)] (con integer 1) ] (con integer 0)])

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/mod-zero/mod-zero.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/expModInteger/mod-zero/mod-zero.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-core/changelog.d/20240726_124910_bezirg_modexp.md

@@ -0,0 +1,3 @@
+### Added
+
+- An initial DRAFT implementation of 'modularExponentiation' builtin

plutus-core/cost-model/create-cost-model/BuiltinMemoryModels.hs

@@ -169,6 +169,7 @@ builtinMemoryModels = BuiltinCostModelBase
   , paramCountSetBits                    = Id $ ModelOneArgumentConstantCost 1
   , paramFindFirstSetBit                 = Id $ ModelOneArgumentConstantCost 1
   , paramRipemd_160                      = Id $ hashMemModel Hash.ripemd_160
+  , paramExpModInteger                   = Id $ ModelThreeArgumentsConstantCost 100000000000 -- FIXME: stub
   }
   where identityFunction = OneVariableLinearFunction 0 1
 

plutus-core/cost-model/create-cost-model/CreateBuiltinCostModel.hs

@@ -124,7 +124,7 @@ builtinCostModelNames = BuiltinCostModelBase
   , paramCountSetBits                    = "countSetBitsModel"
   , paramFindFirstSetBit                 = "findFirstSetBitModel"
   , paramRipemd_160                      = "ripemd_160Model"
-
+  , paramExpModInteger                   = "expModIntegerModel"
   }
 
 
@@ -264,6 +264,7 @@ createBuiltinCostModel bmfile rfile = do
   paramFindFirstSetBit                 <- getParams readCF1 paramFindFirstSetBit
   -- And another hash function
   paramRipemd_160                      <- getParams readCF1 paramRipemd_160
+  paramExpModInteger                   <- getParams readCF3 paramExpModInteger
 
   pure $ BuiltinCostModelBase {..}
 

plutus-core/cost-model/data/builtinCostModelA.json

@@ -1113,5 +1113,15 @@
             "arguments": 3,
             "type": "constant_cost"
         }
+    },
+    "expModInteger": {
+        "cpu": {
+            "arguments": 100000000000,
+            "type": "constant_cost"
+        },
+        "memory": {
+            "arguments": 100000000000,
+            "type": "constant_cost"
+        }
     }
 }

plutus-core/cost-model/data/builtinCostModelB.json

@@ -1113,5 +1113,15 @@
             "arguments": 3,
             "type": "constant_cost"
         }
+    },
+    "expModInteger": {
+        "cpu": {
+            "arguments": 100000000000,
+            "type": "constant_cost"
+        },
+        "memory": {
+            "arguments": 100000000000,
+            "type": "constant_cost"
+        }
     }
 }

plutus-core/cost-model/data/builtinCostModelC.json

@@ -1131,5 +1131,15 @@
             "arguments": 3,
             "type": "constant_cost"
         }
+    },
+    "expModInteger": {
+        "cpu": {
+            "arguments": 100000000000,
+            "type": "constant_cost"
+        },
+        "memory": {
+            "arguments": 100000000000,
+            "type": "constant_cost"
+        }
     }
 }

plutus-core/cost-model/data/models.R

@@ -131,6 +131,7 @@ arity <- function(name) {
         "Keccak_256" = 1,
         "Blake2b_224" = 1,
         "Ripemd_160" = 1,
+        "ExpModInteger" = 3,
         "IntegerToByteString" = 3,
         "ByteStringToInteger" = 2,
         "AndByteString" = 3,
@@ -470,6 +471,8 @@ modelFun <- function(path) {
     quotientIntegerModel  <- divideIntegerModel
     remainderIntegerModel <- divideIntegerModel
     modIntegerModel       <- divideIntegerModel
+    expModIntegerModel    <- constantModel ("ExpModInteger")   # FIXME: stub
+
 
     ## This could possibly be made constant away from the diagonal; it's harmless
     ## to make it linear everywhere, but may overprice some comparisons a bit.
@@ -805,6 +808,7 @@ modelFun <- function(path) {
         blake2b_256Model                     = blake2b_256Model,
         keccak_256Model                      = keccak_256Model,
         ripemd_160Model                      = ripemd_160Model,
+        expModIntegerModel                   = expModIntegerModel,
         verifyEd25519SignatureModel          = verifyEd25519SignatureModel,
         verifyEcdsaSecp256k1SignatureModel   = verifyEcdsaSecp256k1SignatureModel,
         verifySchnorrSecp256k1SignatureModel = verifySchnorrSecp256k1SignatureModel,

plutus-core/executables/plutus/Debugger/TUI/Event.hs

@@ -16,8 +16,8 @@ import Brick.Focus qualified as B
 import Brick.Main qualified as B
 import Brick.Types qualified as B
 import Brick.Widgets.Edit qualified as BE
--- ghc 9.6 has this in base
-#if __GLASGOW_HASKELL__ < 906
+-- ghc>=9.6 has this in base
+#if ! MIN_VERSION_base(4,18,0)
 import Control.Applicative (liftA2)
 #endif
 import Control.Arrow ((>>>))

plutus-core/plutus-core.cabal

@@ -111,6 +111,7 @@ library
     PlutusCore.Crypto.BLS12_381.G2
     PlutusCore.Crypto.BLS12_381.Pairing
     PlutusCore.Crypto.Ed25519
+    PlutusCore.Crypto.ExpMod
     PlutusCore.Crypto.Hash
     PlutusCore.Crypto.Secp256k1
     PlutusCore.Data

plutus-core/plutus-core/src/PlutusCore/Crypto/ExpMod.hs

@@ -0,0 +1,40 @@
+{-# LANGUAGE CPP         #-}
+{-# LANGUAGE MagicHash   #-}
+{-# LANGUAGE UnboxedSums #-}
+module PlutusCore.Crypto.ExpMod
+    ( expMod
+    ) where
+
+import PlutusCore.Builtin
+
+import GHC.Natural
+
+-- Ghc>=9 has this in base
+#if MIN_VERSION_base(4,15,0)
+import GHC.Num.Integer
+-- similar to `Default.Builtins.nonZeroSecondArg`
+-- We don't really need it because integerPowMod# returns `()` on zero mod, but we put
+-- in case of future implementation changes.
+expMod _ _ 0 = fail "Cannot divide by zero"
+expMod b e m =
+    case integerPowMod# b e m of
+        (# n | #)  -> pure n
+        (# | () #) -> fail "expMod: failure"
+#else
+-- FIXME: fugly stub implementation to make the various test-suites/CI pass for GHC8.10.
+-- This means that we cannot provide random testing for expMod at the moment.
+expMod _ _ 0 = fail "Cannot divide by zero"
+expMod 500 0 500 = pure 1
+expMod 500 5 500 = pure 0
+expMod 1 (-3) 4 = pure 1
+expMod 2 (-3) 3 = pure 2
+expMod 4 (-5) 9 = pure 4
+expMod 2 (-3) 4 = fail "expMod: failure"
+expMod 500 (-5) 5 = fail "expMod: failure"
+-- FIXME: this has to be fixed either by deciding to stop supporting GHC8.10
+-- or by backporting ghc-bignum's integerPowMod# implementation to old ghc8.10/integer-gmp<1.1
+expMod _b _e _m = fail "expMod: FIXME: stub for GHC8.10, report to plutus developers"
+#endif
+
+expMod :: Integer -> Integer -> Natural -> BuiltinResult Natural
+{-# INLINE expMod #-}